Orlando Nkwoji

Stream: new members

[Orlando Nkwoji]

example {x : ℚ} (h1 : x ^ 2 = 4) (h2 : 1 < x) : x = 2 := by

have h3 :=

calc

(x - 2)*(x + 2) = x^2 - 4 := by ring

_ = 4 - 4 := by rw [h1]

_ = 0 := by numbers

_ = 0*(x + 2) := by ring

cancel x + 2 at h3

addarith [h3]

[Matt Diamond]

Please post a #mwe using #backticks and include more information on exactly what you need help with