Theorem: sq_diophantine (meetings/ex2.lean)

State before:
x y : ℝ
⊢ x ^ 2 + 5 * y = y ^ 2 + 5 * x → x = y ∨ x + y = 5
Tactic:
intro h
State after:
x y : ℝ
h : x ^ 2 + 5 * y = y ^ 2 + 5 * x
⊢ x = y ∨ x + y = 5

State before:
x y : ℝ
h : x ^ 2 + 5 * y = y ^ 2 + 5 * x
⊢ x = y ∨ x + y = 5
Tactic:
apply_fun (λ eq => eq - 5 * y - y ^ 2) at h
State after:
x y : ℝ
h : x ^ 2 + 5 * y - 5 * y - y ^ 2 = y ^ 2 + 5 * x - 5 * y - y ^ 2
⊢ x = y ∨ x + y = 5

State before:
x y : ℝ
h : x ^ 2 + 5 * y - 5 * y - y ^ 2 = y ^ 2 + 5 * x - 5 * y - y ^ 2
⊢ x = y ∨ x + y = 5
Tactic:
ring_nf at h
State after:
x y : ℝ
h : x ^ 2 - y ^ 2 = x * 5 - y * 5
⊢ x = y ∨ x + y = 5

State before:
x y : ℝ
h : x ^ 2 - y ^ 2 = x * 5 - y * 5
⊢ x = y ∨ x + y = 5
Tactic:
rw [sq_sub_sq, ←mul_sub_right_distrib, mul_comm] at h
State after:
x y : ℝ
h : (x - y) * (x + y) = (x - y) * 5
⊢ x = y ∨ x + y = 5

State before:
x y : ℝ
h : (x - y) * (x + y) = (x - y) * 5
⊢ x = y ∨ x + y = 5
Tactic:
rw [mul_eq_mul_left_iff, sub_eq_zero, or_comm] at h
State after:
x y : ℝ
h : x = y ∨ x + y = 5
⊢ x = y ∨ x + y = 5

State before:
x y : ℝ
h : x = y ∨ x + y = 5
⊢ x = y ∨ x + y = 5
Tactic:
exact h
State after:
no goals