【Lean4】show

show

現在の目標を、定義上同じ別の形で表示し直す

Plaintext

example (n : ℕ) : n + 0 = n := by
  show n + 0 = n
  exact Nat.add_zero n

example (n : ℕ) : n + 0 = n := by
  show n + 0 = n
  exact Nat.add_zero n

定義を展開した形を明示したいときに便利

証明の意味を読みやすくするためにも使える