Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.ReductionLemmas.Lem4 (IMOSLLean4/IMO2012/A5/A5Cases/Case3.lean)

State before:
R : Type u_1
S : Type u_2
r : R
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : NontrivialGood f
h : f r = -1
x : R
h0 : ∃ y, x = r * y + 1
⊢ f (r * r + x) = -f x
Tactic:
rcases h0 with ⟨x, rfl⟩
State after:
case intro
R : Type u_1
S : Type u_2
r : R
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : NontrivialGood f
h : f r = -1
x : R
⊢ f (r * r + (r * x + 1)) = -f (r * x + 1)

State before:
case intro
R : Type u_1
S : Type u_2
r : R
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : NontrivialGood f
h : f r = -1
x : R
⊢ f (r * r + (r * x + 1)) = -f (r * x + 1)
Tactic:
rw [Lem3 hf h, ← add_assoc, ← mul_add, Lem3 hf h, add_add_cancel_left, neg_sub]
State after:
no goals