【Lean4】have

have

証明の途中で補助的な事実を作る

Plaintext

example (a b c : ℕ)
    (h₁ : a = b)
    (h₂ : b = c) :
    a = c := by
  have h₃ : a = c := by
    exact Eq.trans h₁ h₂
  exact h₃

example (a b c : ℕ)
    (h₁ : a = b)
    (h₂ : b = c) :
    a = c := by
  have h₃ : a = c := by
    exact Eq.trans h₁ h₂
  exact h₃