Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.ReductionLemmas.Lem5 (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 * r * y + 1
⊢ f ((r * r + r) * (r * 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) * (r * r + r) + (r * r * x + 1)) = f (r * 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) * (r * r + r) + (r * r * x + 1)) = f (r * r * x + 1)
Tactic:
have h1 : Commute (r * r) r := mul_assoc r r r
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
h1 : Commute (r * r) r
⊢ f ((r * r + r) * (r * r + r) + (r * r * x + 1)) = f (r * 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
h1 : Commute (r * r) r
⊢ f ((r * r + r) * (r * r + r) + (r * r * x + 1)) = f (r * r * x + 1)
Tactic:
rw [add_mul_self_of_Commute h1, add_assoc, Lem4 hf (Lem1 hS hf h), Lem4 hf h, neg_neg]
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
h1 : Commute (r * r) r
⊢ ∃ y, r * r * x + 1 = r * y + 1

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
h1 : Commute (r * r) r
⊢ ∃ y, r * r + (r * r * x + 1) = r * r * y + 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
h1 : Commute (r * r) r
⊢ ∃ y, r * r * x + 1 = r * y + 1

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
h1 : Commute (r * r) r
⊢ ∃ y, r * r + (r * r * x + 1) = r * r * y + 1
Tactic:
exacts [⟨r * x, by rw [mul_assoc]⟩, ⟨1 + x, by rw [← add_assoc, mul_one_add (r * r)]⟩]
State after:
no goals

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
h1 : Commute (r * r) r
⊢ r * r * x + 1 = r * (r * x) + 1
Tactic:
rw [mul_assoc]
State after:
no goals

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
h1 : Commute (r * r) r
⊢ r * r + (r * r * x + 1) = r * r * (1 + x) + 1
Tactic:
rw [← add_assoc, mul_one_add (r * r)]
State after:
no goals