【Lean4】refine

refine

証明の一部を与え、残りを穴?_として新しい目標にする

Plaintext

example (P : ℕ → Prop) (n : ℕ) (h : P n) :
    ∃ m, P m := by
  refine ⟨n, ?_⟩
  exact h
  
/-
refine ⟨n, ?_⟩は、
存在する元としてnを選ぶ。残りのP nは後で証明する
という意味
-/

example (P : ℕ → Prop) (n : ℕ) (h : P n) :
    ∃ m, P m := by
  refine ⟨n, ?_⟩
  exact h
  
/-
refine ⟨n, ?_⟩は、
存在する元としてnを選ぶ。残りのP nは後で証明する
という意味
-/