internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.main_cases
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
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 : NontrivialGood f
R' : Type u_2
R'comm : CommRing R'
φ : R' →+* R
hφ : Function.Injective ⇑φ
x : R'
S' : Type u_1
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
f' : R' → S'
h : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
R'char : CharTwo R'
S'char : 2 ≠ 0
h0 : f' x + f' (x + 1) = 1
⊢ ρ (f' x) + ρ (f' (x + 1)) = 1
Tactic:
rw [← ρ.map_add, h0, ρ.map_one]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.main_cases
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
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 : NontrivialGood f
R' : Type u_2
R'comm : CommRing R'
φ : R' →+* R
hφ : Function.Injective ⇑φ
x : R'
S' : Type u_1
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
f' : R' → S'
h : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
R'char : CharTwo R'
S'char : 2 ≠ 0
h0 : f' x * f' (x + 1) = -1
⊢ ρ (f' x) * ρ (f' (x + 1)) = -1
Tactic:
rw [← ρ.map_mul, h0, ρ.map_neg, ρ.map_one]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.map_add_one_eq_zero_iff_map_eq
Proof 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 : NontrivialGood f
x : R
⊢ f (x + 1) = 0 ↔ f x ^ 2 = 1
Tactic:
refine ⟨λ h0 ↦ ?_, λ h0 ↦ ?_⟩
Proof state after:
case refine_1
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 : NontrivialGood f
x : R
h0 : f (x + 1) = 0
⊢ f x ^ 2 = 1

case refine_2
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 : NontrivialGood f
x : R
h0 : f x ^ 2 = 1
⊢ f (x + 1) = 0
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.map_add_one_eq_zero_iff_map_eq
Proof state before:
case refine_1
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 : NontrivialGood f
x : R
h0 : f (x + 1) = 0
⊢ f x ^ 2 = 1
Tactic:
have h1 := Eq3_v2 hf x
Proof state after:
case refine_1
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 : NontrivialGood f
x : R
h0 : f (x + 1) = 0
h1 : f (x + 1) * f (x * x + x) = (f x ^ 2 - 1) * (f x - 1) + f (x + 1) * f x
⊢ f x ^ 2 = 1
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.map_add_one_eq_zero_iff_map_eq
Proof state before:
case refine_1
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 : NontrivialGood f
x : R
h0 : f (x + 1) = 0
h1 : f (x + 1) * f (x * x + x) = (f x ^ 2 - 1) * (f x - 1) + f (x + 1) * f x
⊢ f x ^ 2 = 1
Tactic:
rw [h0, zero_mul, zero_mul, add_zero, zero_eq_mul] at h1
Proof state after:
case refine_1
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 : NontrivialGood f
x : R
h0 : f (x + 1) = 0
h1 : f x ^ 2 - 1 = 0 ∨ f x - 1 = 0
⊢ f x ^ 2 = 1
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.map_add_one_eq_zero_iff_map_eq
Proof state before:
case refine_1
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 : NontrivialGood f
x : R
h0 : f (x + 1) = 0
h1 : f x ^ 2 - 1 = 0 ∨ f x - 1 = 0
⊢ f x ^ 2 = 1
Tactic:
exact h1.elim eq_of_sub_eq_zero λ h1 ↦ eq_of_sub_eq_zero h1 ▸ one_pow 2
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.map_add_one_eq_zero_iff_map_eq
Proof state before:
case refine_2
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 : NontrivialGood f
x : R
h0 : f x ^ 2 = 1
⊢ f (x + 1) = 0
Tactic:
rcases main_cases hS hf x with (h1 | h1) | ⟨h1, h2⟩
Proof state after:
case refine_2.inl.inl
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 : NontrivialGood f
x : R
h0 : f x ^ 2 = 1
h1 : f x = 0
⊢ f (x + 1) = 0

case refine_2.inl.inr
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 : NontrivialGood f
x : R
h0 : f x ^ 2 = 1
h1 : f (x + 1) = 0
⊢ f (x + 1) = 0

case refine_2.inr.intro
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 : NontrivialGood f
x : R
h0 : f x ^ 2 = 1
h1 : f x + f (x + 1) = 1
h2 : f x * f (x + 1) = -1
⊢ f (x + 1) = 0
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.map_add_one_eq_zero_iff_map_eq
Proof state before:
case refine_2.inl.inl
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 : NontrivialGood f
x : R
h0 : f x ^ 2 = 1
h1 : f x = 0
⊢ f (x + 1) = 0
Tactic:
rw [h1, sq, zero_mul] at h0
Proof state after:
case refine_2.inl.inl
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 : NontrivialGood f
x : R
h0 : 0 = 1
h1 : f x = 0
⊢ f (x + 1) = 0
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.map_add_one_eq_zero_iff_map_eq
Proof state before:
case refine_2.inl.inl
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 : NontrivialGood f
x : R
h0 : 0 = 1
h1 : f x = 0
⊢ f (x + 1) = 0
Tactic:
rw [← mul_one (f _), ← h0, mul_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.map_add_one_eq_zero_iff_map_eq
Proof state before:
case refine_2.inl.inr
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 : NontrivialGood f
x : R
h0 : f x ^ 2 = 1
h1 : f (x + 1) = 0
⊢ f (x + 1) = 0
Tactic:
exact h1
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.map_add_one_eq_zero_iff_map_eq
Proof state before:
case refine_2.inr.intro
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 : NontrivialGood f
x : R
h0 : f x ^ 2 = 1
h1 : f x + f (x + 1) = 1
h2 : f x * (f x * f (x + 1)) = f x * -1
⊢ f (x + 1) = 0
Tactic:
rw [← mul_assoc, ← sq, h0, one_mul, mul_neg_one] at h2
Proof state after:
case refine_2.inr.intro
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 : NontrivialGood f
x : R
h0 : f x ^ 2 = 1
h1 : f x + f (x + 1) = 1
h2 : f (x + 1) = -f x
⊢ f (x + 1) = 0
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.map_add_one_eq_zero_iff_map_eq
Proof state before:
case refine_2.inr.intro
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 : NontrivialGood f
x : R
h0 : f x ^ 2 = 1
h1 : f x + f (x + 1) = 1
h2 : f (x + 1) = -f x
⊢ f (x + 1) = 0
Tactic:
rw [h2, add_neg_self] at h1
Proof state after:
case refine_2.inr.intro
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 : NontrivialGood f
x : R
h0 : f x ^ 2 = 1
h1 : 0 = 1
h2 : f (x + 1) = -f x
⊢ f (x + 1) = 0
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.map_add_one_eq_zero_iff_map_eq
Proof state before:
case refine_2.inr.intro
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 : NontrivialGood f
x : R
h0 : f x ^ 2 = 1
h1 : 0 = 1
h2 : f (x + 1) = -f x
⊢ f (x + 1) = 0
Tactic:
rw [← mul_one (f _), ← h1, mul_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.ReductionLemmas.Lem1
Proof 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) = -1
Tactic:
rw [Eq2_v2 hf, map_eq_neg_one_imp_map_add_one hS hf h, sq, zero_mul, zero_sub]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.ReductionLemmas.Lem2
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.ReductionLemmas.Lem2
Proof 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
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.ReductionLemmas.Lem3
Proof 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
x : R
⊢ f (r * x + 1) = f (r + x) - f x
Tactic:
rw [hf.is_good, h, neg_one_mul, neg_add_eq_sub]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.ReductionLemmas.Lem4
Proof 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⟩
Proof 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)
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.ReductionLemmas.Lem4
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.ReductionLemmas.Lem5
Proof 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⟩
Proof 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)
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.ReductionLemmas.Lem5
Proof 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
Proof 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)
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.ReductionLemmas.Lem5
Proof 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]
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.ReductionLemmas.Lem5
Proof 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)]⟩]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.ReductionLemmas.Lem5
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.ReductionLemmas.Lem5
Proof 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)]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.ReductionLemmas.Lem6
Proof 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]⟩
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.ReductionLemmas.Lem6
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.ReductionLemmas.Lem6
Proof 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)]⟩
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.ReductionLemmas.Lem6
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.ReductionLemmas.Lem6
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.ReductionLemmas.Lem6
Proof 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
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.ReductionLemmas.Lem6
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.ReductionLemmas.Lem6
Proof 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)]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.map_eq_neg_one_reduced_imp
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.map_eq_neg_one_reduced_imp
Proof 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)
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.map_eq_neg_one_reduced_imp
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.map_eq_neg_one_reduced_imp
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.map_eq_neg_one_reduced_imp
Proof 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))
Proof 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