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

State before:
R : Type u_2
S : Type u_1
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
⊢ f (r * r + r) = -1
Tactic:
have h0 := Eq3 hf r
State after:
R : Type u_2
S : Type u_1
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
h0 : f r * f (r * r + r) = (f (r + 1) ^ 2 - 1) * (f (r + 1) - 1) + f r * f (r + 1)
⊢ f (r * r + r) = -1

State before:
R : Type u_2
S : Type u_1
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
h0 : f r * f (r * r + r) = (f (r + 1) ^ 2 - 1) * (f (r + 1) - 1) + f r * f (r + 1)
⊢ f (r * r + r) = -1
Tactic:
rwa [map_eq_neg_one_imp_map_add_one hS hf h, mul_zero, add_zero,
  sq, mul_zero, zero_sub, mul_neg_one, h, neg_one_mul, neg_inj] at h0
State after:
no goals