Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.Eq2 (IMOSLLean4/IMO2012/A5/A5Cases/Case2.lean)

State before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
⊢ f (x + 1) * f (x - 1) = (f x + 1) * f x
Tactic:
have h0 : f 2 ≠ 1 := λ h0 ↦ hf.map_two_ne_neg_one <| by rw [h, zero_eq_neg, ← h, ← h0]
State after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
h0 : f 2 ≠ 1
⊢ f (x + 1) * f (x - 1) = (f x + 1) * f x

State before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
h0 : f 2 ≠ 1
⊢ f (x + 1) * f (x - 1) = (f x + 1) * f x
Tactic:
rw [add_one_mul (f x), ← sq, ← hf.toGoodCase2.Eq7 h0, add_one_mul (f _),
  mul_add_one (f _), add_assoc, add_assoc, self_eq_add_right,
  add_right_comm, ← add_assoc, ← add_assoc, Eq1 hf h, neg_add_self]
State after:
no goals

State before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
h0 : f 2 = 1
⊢ f 2 = -1
Tactic:
rw [h, zero_eq_neg, ← h, ← h0]
State after:
no goals