internlm/Lean-Github huggingface dataset:
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
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
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
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))
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
⊢ QuasiPeriodic f ((r * r + r) * (r * r + r))
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
⊢ QuasiPeriodic f ((r * r + r) * (r * r + r))
Tactic:
have h0 : Commute (r * r) r := mul_assoc r r r
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 : Commute (r * r) r
⊢ QuasiPeriodic f ((r * r + r) * (r * r + r))
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 : 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]
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 : Commute (r * r) r
⊢ QuasiPeriodic f (r * r * (r + 1) * (r + 1))
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 : Commute (r * r) r
⊢ QuasiPeriodic f (r * r * (r + 1) * (r + 1))
Tactic:
exact (ReductionLemmas.Lem6 hS hf' h).mul_right hf' (r + 1)
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
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)
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
x : R
⊢ f ((r * r + 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) * (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⟩
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
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
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
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
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
x : R
h1 : 2 = 0 ∨ f ((r * r + r) * x + 1) = 0
⊢ f ((r * r + 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) * (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
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.map_add_one_eq_zero_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
x : R
h : f (x + 1) = 0
⊢ f (x * x) = -1
Tactic:
rw [Eq2_v2 hf.toNontrivialGood, h, sq, zero_mul, zero_sub]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.reduced_𝔽₂ε_iff
Proof state before:
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
⊢ r * r = 0 ↔ f (r + 1) = 0
Tactic:
rw [reduced_eq_zero_iff hS hf, Eq2_v2 hf.toNontrivialGood,
  sub_eq_neg_self, sq_eq_zero_iff]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.reduced_𝔽₄_iff
Proof state before:
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
⊢ r * (r + 1) + 1 = 0 ↔ f r + f (r + 1) = 1 ∧ f r * f (r + 1) = -1
Tactic:
rw [reduced_eq_zero_iff hS hf, Eq1 hf.toNontrivialGood, iff_and_self]
Proof state after:
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
⊢ f r * f (r + 1) = -1 → f r + f (r + 1) = 1
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.reduced_𝔽₄_iff
Proof state before:
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
⊢ f r * f (r + 1) = -1 → f r + f (r + 1) = 1
Tactic:
intro h
Proof state after:
R : Type u_1
S : Type u_2
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 * f (r + 1) = -1
⊢ f r + f (r + 1) = 1
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.reduced_𝔽₄_iff
Proof state before:
R : Type u_1
S : Type u_2
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 * f (r + 1) = -1
⊢ f r + f (r + 1) = 1
Tactic:
refine (main_cases hS hf.toNontrivialGood r).elim (λ h0 ↦ ?_) And.left
Proof state after:
R : Type u_1
S : Type u_2
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 * f (r + 1) = -1
h0 : f r = 0 ∨ f (r + 1) = 0
⊢ f r + f (r + 1) = 1
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.reduced_𝔽₄_iff
Proof state before:
R : Type u_1
S : Type u_2
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 * f (r + 1) = -1
h0 : f r = 0 ∨ f (r + 1) = 0
⊢ f r + f (r + 1) = 1
Tactic:
rw [← mul_eq_zero, h, neg_eq_zero] at h0
Proof state after:
R : Type u_1
S : Type u_2
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 * f (r + 1) = -1
h0 : 1 = 0
⊢ f r + f (r + 1) = 1
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.reduced_𝔽₄_iff
Proof state before:
R : Type u_1
S : Type u_2
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 * f (r + 1) = -1
h0 : 1 = 0
⊢ f r + f (r + 1) = 1
Tactic:
rw [← mul_one (_ + _), h0, mul_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_cases
Proof state before:
R : Type u_1
S : Type ?u.155523
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
⊢ ((r + 1) * (r + 1) = 0 ∨ r * r = 0) ∨ r * (r + 1) + 1 = 0
Tactic:
rw [reduced_𝔽₂ε_iff hS hf, reduced_𝔽₂ε_iff hS hf,
  reduced_𝔽₄_iff hS hf, add_add_cancel_right]
Proof state after:
R : Type u_1
S : Type ?u.155523
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
⊢ (f r = 0 ∨ f (r + 1) = 0) ∨ f r + f (r + 1) = 1 ∧ f r * f (r + 1) = -1
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_cases
Proof state before:
R : Type u_1
S : Type ?u.155523
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
⊢ (f r = 0 ∨ f (r + 1) = 0) ∨ f r + f (r + 1) = 1 ∧ f r * f (r + 1) = -1
Tactic:
exact main_cases hS hf.toNontrivialGood r
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim1
Proof state before:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : r * s * (r * s) = 0
⊢ r = 0 ∨ s = 0 ∨ r = s
Tactic:
rw [reduced_𝔽₂ε_iff hS hf, hf.is_good] at h
Proof state after:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : f r * f s + f (r + s) = 0
⊢ r = 0 ∨ s = 0 ∨ r = s
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim1
Proof state before:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : f r * f s + f (r + s) = 0
⊢ r = 0 ∨ s = 0 ∨ r = s
Tactic:
rw [reduced_𝔽₂ε_iff hS hf, map_add_one_eq_zero_iff_map_eq hS hf.toNontrivialGood,
  _root_.sq_eq_one_iff, or_comm] at hr hs
Proof state after:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : f r = -1 ∨ f r = 1
hs : f s = -1 ∨ f s = 1
h : f r * f s + f (r + s) = 0
⊢ r = 0 ∨ s = 0 ∨ r = s
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim1
Proof state before:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : f r = -1 ∨ f r = 1
hs : f s = -1 ∨ f s = 1
h : f r * f s + f (r + s) = 0
⊢ r = 0 ∨ s = 0 ∨ r = s
Tactic:
have h0 {x} : f x = -1 → x = 0 := map_eq_neg_one_reduced_imp hS hf
Proof state after:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : f r = -1 ∨ f r = 1
hs : f s = -1 ∨ f s = 1
h : f r * f s + f (r + s) = 0
h0 : ∀ {x : R}, f x = -1 → x = 0
⊢ r = 0 ∨ s = 0 ∨ r = s
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim1
Proof state before:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : f r = -1 ∨ f r = 1
hs : f s = -1 ∨ f s = 1
h : f r * f s + f (r + s) = 0
h0 : ∀ {x : R}, f x = -1 → x = 0
⊢ r = 0 ∨ s = 0 ∨ r = s
Tactic:
revert hr
Proof state after:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hs : f s = -1 ∨ f s = 1
h : f r * f s + f (r + s) = 0
h0 : ∀ {x : R}, f x = -1 → x = 0
⊢ f r = -1 ∨ f r = 1 → r = 0 ∨ s = 0 ∨ r = s
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim1
Proof state before:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hs : f s = -1 ∨ f s = 1
h : f r * f s + f (r + s) = 0
h0 : ∀ {x : R}, f x = -1 → x = 0
⊢ f r = -1 ∨ f r = 1 → r = 0 ∨ s = 0 ∨ r = s
Tactic:
refine Or.imp h0 λ hr ↦ ?_
Proof state after:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hs : f s = -1 ∨ f s = 1
h : f r * f s + f (r + s) = 0
h0 : ∀ {x : R}, f x = -1 → x = 0
hr : f r = 1
⊢ s = 0 ∨ r = s
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim1
Proof state before:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hs : f s = -1 ∨ f s = 1
h : f r * f s + f (r + s) = 0
h0 : ∀ {x : R}, f x = -1 → x = 0
hr : f r = 1
⊢ s = 0 ∨ r = s
Tactic:
revert hs
Proof state after:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
h : f r * f s + f (r + s) = 0
h0 : ∀ {x : R}, f x = -1 → x = 0
hr : f r = 1
⊢ f s = -1 ∨ f s = 1 → s = 0 ∨ r = s
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim1
Proof state before:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
h : f r * f s + f (r + s) = 0
h0 : ∀ {x : R}, f x = -1 → x = 0
hr : f r = 1
⊢ f s = -1 ∨ f s = 1 → s = 0 ∨ r = s
Tactic:
refine Or.imp h0 λ hs ↦ ?_
Proof state after:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
h : f r * f s + f (r + s) = 0
h0 : ∀ {x : R}, f x = -1 → x = 0
hr : f r = 1
hs : f s = 1
⊢ r = s
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim1
Proof state before:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
h : f r * f s + f (r + s) = 0
h0 : ∀ {x : R}, f x = -1 → x = 0
hr : f r = 1
hs : f s = 1
⊢ r = s
Tactic:
rw [hr, hs, mul_one, ← neg_eq_iff_add_eq_zero, eq_comm] at h
Proof state after:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
h : f (r + s) = -1
h0 : ∀ {x : R}, f x = -1 → x = 0
hr : f r = 1
hs : f s = 1
⊢ r = s
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim1
Proof state before:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
h : f (r + s) = -1
h0 : ∀ {x : R}, f x = -1 → x = 0
hr : f r = 1
hs : f s = 1
⊢ r = s
Tactic:
exact add_eq_zero_iff_eq.mp (h0 h)
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim1
Proof state before:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
⊢ r * s * (r * s) = 0
Tactic:
have h : (r + s) * (r + s) = r * s + s * r := by
  rw [add_mul, mul_add, hr, zero_add, mul_add, hs, add_zero]
Proof state after:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
⊢ r * s * (r * s) = 0
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim1
Proof state before:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
⊢ r * s * (r * s) = 0
Tactic:
rcases R_elts_cases hS hf (r + s) with (h0 | h0) | h0
Proof state after:
case inl.inl
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : (r + s + 1) * (r + s + 1) = 0
⊢ r * s * (r * s) = 0

case inl.inr
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : (r + s) * (r + s) = 0
⊢ r * s * (r * s) = 0

case inr
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : (r + s) * (r + s + 1) + 1 = 0
⊢ r * s * (r * s) = 0
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim1
Proof state before:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
⊢ (r + s) * (r + s) = r * s + s * r
Tactic:
rw [add_mul, mul_add, hr, zero_add, mul_add, hs, add_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim1
Proof state before:
case inl.inl
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : (r + s + 1) * (r + s + 1) = 0
⊢ r * s * (r * s) = 0
Tactic:
rw [add_one_mul_self, h, add_eq_zero_iff_eq] at h0
Proof state after:
case inl.inl
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : r * s + s * r = 1
⊢ r * s * (r * s) = 0
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim1
Proof state before:
case inl.inl
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : r * s + s * r = 1
⊢ r * s * (r * s) = 0
Tactic:
have h1 : (r * s) * (r * s) = r * s := by
  apply congrArg (λ x ↦ r * x * s) at h0
  rwa [mul_add, ← mul_assoc, hr, zero_mul, zero_add,
    mul_one, mul_assoc, mul_assoc, ← mul_assoc] at h0
Proof state after:
case inl.inl
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : r * s + s * r = 1
h1 : r * s * (r * s) = r * s
⊢ r * s * (r * s) = 0
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim1
Proof state before:
case inl.inl
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : r * s + s * r = 1
h1 : r * s * (r * s) = r * s
⊢ r * s * (r * s) = 0
Tactic:
rcases R_elts_cases hS hf (r * s) with (h2 | h2) | h2
Proof state after:
case inl.inl.inl.inl
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : r * s + s * r = 1
h1 : r * s * (r * s) = r * s
h2 : (r * s + 1) * (r * s + 1) = 0
⊢ r * s * (r * s) = 0

case inl.inl.inl.inr
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : r * s + s * r = 1
h1 : r * s * (r * s) = r * s
h2 : r * s * (r * s) = 0
⊢ r * s * (r * s) = 0

case inl.inl.inr
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : r * s + s * r = 1
h1 : r * s * (r * s) = r * s
h2 : r * s * (r * s + 1) + 1 = 0
⊢ r * s * (r * s) = 0
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim1
Proof state before:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : r * s + s * r = 1
⊢ r * s * (r * s) = r * s
Tactic:
apply congrArg (λ x ↦ r * x * s) at h0
Proof state after:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : r * (r * s + s * r) * s = r * 1 * s
⊢ r * s * (r * s) = r * s
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim1
Proof state before:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : r * (r * s + s * r) * s = r * 1 * s
⊢ r * s * (r * s) = r * s
Tactic:
rwa [mul_add, ← mul_assoc, hr, zero_mul, zero_add,
  mul_one, mul_assoc, mul_assoc, ← mul_assoc] at h0
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim1
Proof state before:
case inl.inl.inl.inl
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : r * s + s * r = 1
h1 : r * s * (r * s) = r * s
h2 : (r * s + 1) * (r * s + 1) = 0
⊢ r * s * (r * s) = 0
Tactic:
rw [add_one_mul_self, h1, add_eq_zero_iff_eq] at h2
Proof state after:
case inl.inl.inl.inl
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : r * s + s * r = 1
h1 : r * s * (r * s) = r * s
h2 : r * s = 1
⊢ r * s * (r * s) = 0