Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.ReductionLemmas.Lem6 (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
⊢ f (r * r * (r + 1) * x + 1) = 0
Tactic:
have h0 : ∃ y, r * r * (r + 1) * x + 1 = r * r * y + 1 :=
  ⟨(r + 1) * x, by rw [← mul_assoc]⟩
State after:
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, r * r * (r + 1) * x + 1 = r * r * y + 1
⊢ f (r * r * (r + 1) * x + 1) = 0

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, r * r * (r + 1) * x + 1 = r * r * y + 1
⊢ f (r * r * (r + 1) * x + 1) = 0
Tactic:
apply Lem5 hS hf h at h0
State after:
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 : f ((r * r + r) * (r * r + r) + (r * r * (r + 1) * x + 1)) = f (r * r * (r + 1) * x + 1)
⊢ f (r * r * (r + 1) * x + 1) = 0

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 : f ((r * r + r) * (r * r + r) + (r * r * (r + 1) * x + 1)) = f (r * r * (r + 1) * x + 1)
⊢ f (r * r * (r + 1) * x + 1) = 0
Tactic:
have h1 : ∃ y, r * r * (r + 1) * x + 1 = (r * r + r) * y + 1 :=
  ⟨r * x, by rw [← mul_assoc, add_mul, mul_add_one (r * r)]⟩
State after:
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 : f ((r * r + r) * (r * r + r) + (r * r * (r + 1) * x + 1)) = f (r * r * (r + 1) * x + 1)
h1 : ∃ y, r * r * (r + 1) * x + 1 = (r * r + r) * y + 1
⊢ f (r * r * (r + 1) * x + 1) = 0

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 : f ((r * r + r) * (r * r + r) + (r * r * (r + 1) * x + 1)) = f (r * r * (r + 1) * x + 1)
h1 : ∃ y, r * r * (r + 1) * x + 1 = (r * r + r) * y + 1
⊢ f (r * r * (r + 1) * x + 1) = 0
Tactic:
apply Lem4 hf (Lem2 hS hf h) at h1
State after:
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 : f ((r * r + r) * (r * r + r) + (r * r * (r + 1) * x + 1)) = f (r * r * (r + 1) * x + 1)
h1 : f ((r * r + r) * (r * r + r) + (r * r * (r + 1) * x + 1)) = -f (r * r * (r + 1) * x + 1)
⊢ f (r * r * (r + 1) * x + 1) = 0

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 : f ((r * r + r) * (r * r + r) + (r * r * (r + 1) * x + 1)) = f (r * r * (r + 1) * x + 1)
h1 : f ((r * r + r) * (r * r + r) + (r * r * (r + 1) * x + 1)) = -f (r * r * (r + 1) * x + 1)
⊢ f (r * r * (r + 1) * x + 1) = 0
Tactic:
rw [h1, neg_eq_iff_add_eq_zero, ← two_mul, mul_eq_zero] at h0
State after:
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 : 2 = 0 ∨ f (r * r * (r + 1) * x + 1) = 0
h1 : f ((r * r + r) * (r * r + r) + (r * r * (r + 1) * x + 1)) = -f (r * r * (r + 1) * x + 1)
⊢ f (r * r * (r + 1) * x + 1) = 0

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 : 2 = 0 ∨ f (r * r * (r + 1) * x + 1) = 0
h1 : f ((r * r + r) * (r * r + r) + (r * r * (r + 1) * x + 1)) = -f (r * r * (r + 1) * x + 1)
⊢ f (r * r * (r + 1) * x + 1) = 0
Tactic:
exact h0.resolve_left hS
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
⊢ r * r * (r + 1) * x + 1 = r * r * ((r + 1) * 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
h0 : f ((r * r + r) * (r * r + r) + (r * r * (r + 1) * x + 1)) = f (r * r * (r + 1) * x + 1)
⊢ r * r * (r + 1) * x + 1 = (r * r + r) * (r * x) + 1
Tactic:
rw [← mul_assoc, add_mul, mul_add_one (r * r)]
State after:
no goals