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

State before:
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
h : f r = -1
⊢ r = 0
Tactic:
let hf' := hf.toNontrivialGood
State after:
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
h : f r = -1
hf' : NontrivialGood f := hf.toNontrivialGood
⊢ r = 0

State before:
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
h : f r = -1
hf' : NontrivialGood f := hf.toNontrivialGood
⊢ r = 0
Tactic:
have h0 : (r * r + r) * (r * r + r) = 0 := by
  refine (QuasiPeriodic.reduced_eq_zero_iff hf ?_).mpr
    (ReductionLemmas.Lem1 hS hf' (ReductionLemmas.Lem2 hS hf' h))
  have h0 : Commute (r * r) r := mul_assoc r r r
  rw [add_mul_self_of_Commute h0, ← mul_add_one (r * r), ← add_one_mul_self, ← mul_assoc]
  exact (ReductionLemmas.Lem6 hS hf' h).mul_right hf' (r + 1)
State after:
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
h : f r = -1
hf' : NontrivialGood f := hf.toNontrivialGood
h0 : (r * r + r) * (r * r + r) = 0
⊢ r = 0

State before:
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
h : f r = -1
hf' : NontrivialGood f := hf.toNontrivialGood
h0 : (r * r + r) * (r * r + r) = 0
⊢ r = 0
Tactic:
replace h0 : r * r + r = 0 := by
  refine (QuasiPeriodic.reduced_eq_zero_iff hf <|
    (QuasiPeriodic.iff_left2 hf').mpr λ x ↦ ?_).mpr (ReductionLemmas.Lem2 hS hf' h)
  have h1 := ReductionLemmas.Lem4 hf' (ReductionLemmas.Lem2 hS hf' h) ⟨x, rfl⟩
  rw [h0, zero_add, eq_neg_iff_add_eq_zero, ← two_mul, mul_eq_zero] at h1
  exact h1.resolve_left hS
State after:
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
h : f r = -1
hf' : NontrivialGood f := hf.toNontrivialGood
h0 : r * r + r = 0
⊢ r = 0

State before:
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
h : f r = -1
hf' : NontrivialGood f := hf.toNontrivialGood
h0 : r * r + r = 0
⊢ r = 0
Tactic:
refine (QuasiPeriodic.reduced_eq_zero_iff hf <|
  (QuasiPeriodic.iff_left2 hf').mpr λ x ↦ ?_).mpr h
State after:
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
h : f r = -1
hf' : NontrivialGood f := hf.toNontrivialGood
h0 : r * r + r = 0
x : R
⊢ f (r * x + 1) = 0

State before:
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
h : f r = -1
hf' : NontrivialGood f := hf.toNontrivialGood
h0 : r * r + r = 0
x : R
⊢ f (r * x + 1) = 0
Tactic:
have h1 := hf.is_good (r + 1) (r * (x - 1))
State after:
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
h : f r = -1
hf' : NontrivialGood f := hf.toNontrivialGood
h0 : r * r + r = 0
x : R
h1 : f ((r + 1) * (r * (x - 1)) + 1) = f (r + 1) * f (r * (x - 1)) + f (r + 1 + r * (x - 1))
⊢ f (r * x + 1) = 0

State before:
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
h : f r = -1
hf' : NontrivialGood f := hf.toNontrivialGood
h0 : r * r + r = 0
x : R
h1 : f ((r + 1) * (r * (x - 1)) + 1) = f (r + 1) * f (r * (x - 1)) + f (r + 1 + r * (x - 1))
⊢ f (r * x + 1) = 0
Tactic:
rwa [map_eq_neg_one_imp_map_add_one hS hf' h, zero_mul, zero_add,
  ← mul_assoc, add_one_mul r, h0, zero_mul, zero_add, hf.map_one,
  ← add_rotate, ← mul_add_one r, sub_add_cancel, eq_comm] at h1
State after:
no goals

State before:
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
h : f r = -1
hf' : NontrivialGood f := hf.toNontrivialGood
⊢ (r * r + r) * (r * r + r) = 0
Tactic:
refine (QuasiPeriodic.reduced_eq_zero_iff hf ?_).mpr
  (ReductionLemmas.Lem1 hS hf' (ReductionLemmas.Lem2 hS hf' h))
State after:
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
h : f r = -1
hf' : NontrivialGood f := hf.toNontrivialGood
⊢ QuasiPeriodic f ((r * r + r) * (r * r + r))

State before:
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
h : f r = -1
hf' : NontrivialGood f := hf.toNontrivialGood
⊢ QuasiPeriodic f ((r * r + r) * (r * r + r))
Tactic:
have h0 : Commute (r * r) r := mul_assoc r r r
State after:
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
h : f r = -1
hf' : NontrivialGood f := hf.toNontrivialGood
h0 : Commute (r * r) r
⊢ QuasiPeriodic f ((r * r + r) * (r * r + r))

State before:
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
h : f r = -1
hf' : NontrivialGood f := hf.toNontrivialGood
h0 : Commute (r * r) r
⊢ QuasiPeriodic f ((r * r + r) * (r * r + r))
Tactic:
rw [add_mul_self_of_Commute h0, ← mul_add_one (r * r), ← add_one_mul_self, ← mul_assoc]
State after:
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
h : f r = -1
hf' : NontrivialGood f := hf.toNontrivialGood
h0 : Commute (r * r) r
⊢ QuasiPeriodic f (r * r * (r + 1) * (r + 1))

State before:
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
h : f r = -1
hf' : NontrivialGood f := hf.toNontrivialGood
h0 : Commute (r * r) r
⊢ QuasiPeriodic f (r * r * (r + 1) * (r + 1))
Tactic:
exact (ReductionLemmas.Lem6 hS hf' h).mul_right hf' (r + 1)
State after:
no goals

State before:
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
h : f r = -1
hf' : NontrivialGood f := hf.toNontrivialGood
h0 : (r * r + r) * (r * r + r) = 0
⊢ r * r + r = 0
Tactic:
refine (QuasiPeriodic.reduced_eq_zero_iff hf <|
  (QuasiPeriodic.iff_left2 hf').mpr λ x ↦ ?_).mpr (ReductionLemmas.Lem2 hS hf' h)
State after:
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
h : f r = -1
hf' : NontrivialGood f := hf.toNontrivialGood
h0 : (r * r + r) * (r * r + r) = 0
x : R
⊢ f ((r * r + r) * x + 1) = 0

State before:
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
h : f r = -1
hf' : NontrivialGood f := hf.toNontrivialGood
h0 : (r * r + r) * (r * r + r) = 0
x : R
⊢ f ((r * r + r) * x + 1) = 0
Tactic:
have h1 := ReductionLemmas.Lem4 hf' (ReductionLemmas.Lem2 hS hf' h) ⟨x, rfl⟩
State after:
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
h : f r = -1
hf' : NontrivialGood f := hf.toNontrivialGood
h0 : (r * r + r) * (r * r + r) = 0
x : R
h1 : f ((r * r + r) * (r * r + r) + ((r * r + r) * x + 1)) = -f ((r * r + r) * x + 1)
⊢ f ((r * r + r) * x + 1) = 0

State before:
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
h : f r = -1
hf' : NontrivialGood f := hf.toNontrivialGood
h0 : (r * r + r) * (r * r + r) = 0
x : R
h1 : f ((r * r + r) * (r * r + r) + ((r * r + r) * x + 1)) = -f ((r * r + r) * x + 1)
⊢ f ((r * r + r) * x + 1) = 0
Tactic:
rw [h0, zero_add, eq_neg_iff_add_eq_zero, ← two_mul, mul_eq_zero] at h1
State after:
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
h : f r = -1
hf' : NontrivialGood f := hf.toNontrivialGood
h0 : (r * r + r) * (r * r + r) = 0
x : R
h1 : 2 = 0 ∨ f ((r * r + r) * x + 1) = 0
⊢ f ((r * r + r) * x + 1) = 0

State before:
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
h : f r = -1
hf' : NontrivialGood f := hf.toNontrivialGood
h0 : (r * r + r) * (r * r + r) = 0
x : R
h1 : 2 = 0 ∨ f ((r * r + r) * x + 1) = 0
⊢ f ((r * r + r) * x + 1) = 0
Tactic:
exact h1.resolve_left hS
State after:
no goals