【Lean4】linarith

linarith

線形な等式・不等式から結論を導く

Plaintext

example (x y : ℝ)
    (h₁ : x ≤ y)
    (h₂ : y ≤ x) :
    x = y := by
  linarith

example (x y : ℝ)
    (h₁ : x ≤ y)
    (h₂ : y ≤ x) :
    x = y := by
  linarith