【Lean4】exact

exact

Plaintext

example (P : Prop) (h : P) : P := by
  exact h
  
/-
hがまさに目標Pの証明なので、「exact h」で終了する
-/

example (P : Prop) (h : P) : P := by
  exact h
  
/-
hがまさに目標Pの証明なので、「exact h」で終了する
-/