internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2012A5.Case3.CommCase.Thm1
Proof state before:
case inr.h.inr
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
h0 : f x ^ 2 - 1 = 0
h1 : f (x * x) = 0
h : f (x * x + 1) * f (x * x * (x * x) + x * x) = (f (x * x) ^ 2 - 1) * (f (x * x) - 1) + f (x * x + 1) * f (x * x)
⊢ 2 * f x = 1
Tactic:
rw [h1, mul_zero, add_zero, sq, zero_mul, zero_sub,
  neg_mul_neg, one_mul, Eq2 hf, h0, zero_mul] at h
Proof state after:
case inr.h.inr
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
h0 : f x ^ 2 - 1 = 0
h1 : f (x * x) = 0
h : 0 = 1
⊢ 2 * f x = 1
Theorem: IMOSL.IMO2012A5.Case3.CommCase.Thm1
Proof state before:
case inr.h.inr
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
h0 : f x ^ 2 - 1 = 0
h1 : f (x * x) = 0
h : 0 = 1
⊢ 2 * f x = 1
Tactic:
rw [← mul_one (2 * f x), ← h, mul_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.CommCase.Thm1
Proof state before:
case inl
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
h : f x ^ 2 + f (x + 1) ^ 2 = 1 ∨ f x + f (x + 1) = 1
⊢ f x ^ 2 + f (x + 1) ^ 2 = 1 ∨ f x + f (x + 1) = 1
Tactic:
exact h
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.CommCase.Thm1
Proof state before:
case inr.h.inl
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
h : f x = f (x + 1)
h0 : 1 - 2 * f x = 0
⊢ 2 * f x = 1
Tactic:
exact (eq_of_sub_eq_zero h0).symm
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.CommCase.Thm1
Proof state before:
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
h : f x = f (x + 1)
h0 : f x ^ 2 - 1 = 0
⊢ f (x * x) = 0
Tactic:
rw [Eq2_v2 hf, ← h, h0]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.CommCase.SCharTwo_map_add_one
Proof state before:
R : Type u_2
S : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CharTwo R
inst✝² : CommRing S
inst✝¹ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
inst✝ : CharTwo S
x : R
⊢ f (x + 1) = f x + 1
Tactic:
have h := Thm1 hf x
Proof state after:
R : Type u_2
S : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CharTwo R
inst✝² : CommRing S
inst✝¹ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
inst✝ : CharTwo S
x : R
h : f x ^ 2 + f (x + 1) ^ 2 = 1 ∨ f x + f (x + 1) = 1
⊢ f (x + 1) = f x + 1
Theorem: IMOSL.IMO2012A5.Case3.CommCase.SCharTwo_map_add_one
Proof state before:
R : Type u_2
S : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CharTwo R
inst✝² : CommRing S
inst✝¹ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
inst✝ : CharTwo S
x : R
h : f x ^ 2 + f (x + 1) ^ 2 = 1 ∨ f x + f (x + 1) = 1
⊢ f (x + 1) = f x + 1
Tactic:
rwa [← CharTwo.add_sq, CharTwo.sq_eq_one_iff, or_self, add_eq_iff_eq_add''] at h
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.CommCase.pow_four_Eq1
Proof state before:
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
⊢ f ((x ^ 2) ^ 2) = (f x ^ 2 - 1) ^ 2 - 1
Tactic:
rw [← add_add_cancel_right (x ^ 2) 1, add_one_sq, sq, sq, Eq2 hf, Eq2 hf]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.CommCase.pow_four_Eq2
Proof state before:
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
⊢ f ((x ^ 2) ^ 2 + 1) = (f (x + 1) ^ 2 - 1) ^ 2 - 1
Tactic:
rw [← pow_four_Eq1 hf, add_one_sq, add_one_sq]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.CommCase.SCharNeTwo_main_ring_id
Proof state before:
R : Type ?u.57818
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
a b : S
⊢ ((a - 1) ^ 2 - 1) * ((b - 1) ^ 2 - 1) - ((a * b - 1) ^ 2 - 1) = 2 * (a * b * (2 + 1 - (a + b)))
Tactic:
ring
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.CommCase.SCharNeTwo_cases
Proof state before:
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : 2 ≠ 0
x : R
⊢ (f x = 0 ∨ f (x + 1) = 0) ∨ f x + f (x + 1) = 1 ∧ f x * f (x + 1) = -1
Tactic:
have h0 := pow_four_Eq2 hf (x * (x + 1))
Proof state after:
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : 2 ≠ 0
x : R
h0 : f (((x * (x + 1)) ^ 2) ^ 2 + 1) = (f (x * (x + 1) + 1) ^ 2 - 1) ^ 2 - 1
⊢ (f x = 0 ∨ f (x + 1) = 0) ∨ f x + f (x + 1) = 1 ∧ f x * f (x + 1) = -1
Theorem: IMOSL.IMO2012A5.Case3.CommCase.SCharNeTwo_cases
Proof state before:
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : 2 ≠ 0
x : R
h0 : f (((x * (x + 1)) ^ 2) ^ 2 + 1) = (f (x * (x + 1) + 1) ^ 2 - 1) ^ 2 - 1
⊢ (f x = 0 ∨ f (x + 1) = 0) ∨ f x + f (x + 1) = 1 ∧ f x * f (x + 1) = -1
Tactic:
rw [Eq1 hf, mul_pow, mul_pow, add_one_sq, add_one_sq, Eq1 hf, pow_four_Eq1 hf,
  pow_four_Eq2 hf, ← sub_eq_zero, mul_pow, SCharNeTwo_main_ring_id, mul_eq_zero,
  or_iff_right h, mul_eq_zero, ← mul_pow, sq_eq_zero_iff] at h0
Proof state after:
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : 2 ≠ 0
x : R
h0 : f x * f (x + 1) = 0 ∨ 2 + 1 - (f x ^ 2 + f (x + 1) ^ 2) = 0
⊢ (f x = 0 ∨ f (x + 1) = 0) ∨ f x + f (x + 1) = 1 ∧ f x * f (x + 1) = -1
Theorem: IMOSL.IMO2012A5.Case3.CommCase.SCharNeTwo_cases
Proof state before:
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : 2 ≠ 0
x : R
h0 : f x * f (x + 1) = 0 ∨ 2 + 1 - (f x ^ 2 + f (x + 1) ^ 2) = 0
⊢ (f x = 0 ∨ f (x + 1) = 0) ∨ f x + f (x + 1) = 1 ∧ f x * f (x + 1) = -1
Tactic:
revert h0
Proof state after:
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : 2 ≠ 0
x : R
⊢ f x * f (x + 1) = 0 ∨ 2 + 1 - (f x ^ 2 + f (x + 1) ^ 2) = 0 →
    (f x = 0 ∨ f (x + 1) = 0) ∨ f x + f (x + 1) = 1 ∧ f x * f (x + 1) = -1
Theorem: IMOSL.IMO2012A5.Case3.CommCase.SCharNeTwo_cases
Proof state before:
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : 2 ≠ 0
x : R
⊢ f x * f (x + 1) = 0 ∨ 2 + 1 - (f x ^ 2 + f (x + 1) ^ 2) = 0 →
    (f x = 0 ∨ f (x + 1) = 0) ∨ f x + f (x + 1) = 1 ∧ f x * f (x + 1) = -1
Tactic:
refine Or.imp mul_eq_zero.mp λ h0 ↦ ?_
Proof state after:
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : 2 ≠ 0
x : R
h0 : 2 + 1 - (f x ^ 2 + f (x + 1) ^ 2) = 0
⊢ f x + f (x + 1) = 1 ∧ f x * f (x + 1) = -1
Theorem: IMOSL.IMO2012A5.Case3.CommCase.SCharNeTwo_cases
Proof state before:
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : 2 ≠ 0
x : R
h0 : 2 + 1 - (f x ^ 2 + f (x + 1) ^ 2) = 0
⊢ f x + f (x + 1) = 1 ∧ f x * f (x + 1) = -1
Tactic:
rw [sub_eq_zero, eq_comm] at h0
Proof state after:
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : 2 ≠ 0
x : R
h0 : f x ^ 2 + f (x + 1) ^ 2 = 2 + 1
⊢ f x + f (x + 1) = 1 ∧ f x * f (x + 1) = -1
Theorem: IMOSL.IMO2012A5.Case3.CommCase.SCharNeTwo_cases
Proof state before:
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : 2 ≠ 0
x : R
h0 : f x ^ 2 + f (x + 1) ^ 2 = 2 + 1
⊢ f x + f (x + 1) = 1 ∧ f x * f (x + 1) = -1
Tactic:
refine (Thm1 hf x).elim (λ h1 ↦ Not.elim h ?_) (λ h1 ↦ ⟨h1, ?_⟩)
Proof state after:
case refine_1
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : 2 ≠ 0
x : R
h0 : f x ^ 2 + f (x + 1) ^ 2 = 2 + 1
h1 : f x ^ 2 + f (x + 1) ^ 2 = 1
⊢ 2 = 0

case refine_2
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : 2 ≠ 0
x : R
h0 : f x ^ 2 + f (x + 1) ^ 2 = 2 + 1
h1 : f x + f (x + 1) = 1
⊢ f x * f (x + 1) = -1
Theorem: IMOSL.IMO2012A5.Case3.CommCase.SCharNeTwo_cases
Proof state before:
case refine_2
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : 2 ≠ 0
x : R
h0 : f x ^ 2 + f (x + 1) ^ 2 = 2 + 1
h1 : f x + f (x + 1) = 1
⊢ f x * f (x + 1) = -1
Tactic:
apply congrArg (λ y ↦ y ^ 2) at h1
Proof state after:
case refine_2
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : 2 ≠ 0
x : R
h0 : f x ^ 2 + f (x + 1) ^ 2 = 2 + 1
h1 : (f x + f (x + 1)) ^ 2 = 1 ^ 2
⊢ f x * f (x + 1) = -1
Theorem: IMOSL.IMO2012A5.Case3.CommCase.SCharNeTwo_cases
Proof state before:
case refine_2
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : 2 ≠ 0
x : R
h0 : f x ^ 2 + f (x + 1) ^ 2 = 2 + 1
h1 : (f x + f (x + 1)) ^ 2 = 1 ^ 2
⊢ f x * f (x + 1) = -1
Tactic:
rw [one_pow, add_sq', h0, add_right_comm, add_left_eq_self,
   mul_assoc, ← mul_one_add (2 : S), mul_eq_zero] at h1
Proof state after:
case refine_2
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : 2 ≠ 0
x : R
h0 : f x ^ 2 + f (x + 1) ^ 2 = 2 + 1
h1 : 2 = 0 ∨ 1 + f x * f (x + 1) = 0
⊢ f x * f (x + 1) = -1
Theorem: IMOSL.IMO2012A5.Case3.CommCase.SCharNeTwo_cases
Proof state before:
case refine_2
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : 2 ≠ 0
x : R
h0 : f x ^ 2 + f (x + 1) ^ 2 = 2 + 1
h1 : 2 = 0 ∨ 1 + f x * f (x + 1) = 0
⊢ f x * f (x + 1) = -1
Tactic:
exact eq_neg_of_add_eq_zero_right (h1.resolve_left h)
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.CommCase.SCharNeTwo_cases
Proof state before:
case refine_1
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : 2 ≠ 0
x : R
h0 : f x ^ 2 + f (x + 1) ^ 2 = 2 + 1
h1 : f x ^ 2 + f (x + 1) ^ 2 = 1
⊢ 2 = 0
Tactic:
rwa [h0, add_left_eq_self] at h1
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharTwo.solution
Proof state before:
R : Type u_2
S : Type u_1
inst✝⁴ : Ring R
inst✝³ : CharTwo R
inst✝² : Ring S
inst✝¹ : NoZeroDivisors S
inst✝ : CharTwo S
f : R → S
hf : NontrivialGood f
x : R
⊢ f (x + 1) = f x + 1
Tactic:
rcases CommSubring.oneVarCommLiftDomain_exists hf x with
  ⟨R', R'comm, φ, hφ, ⟨x, rfl⟩, S', S'comm, S'nzd, ρ, hρ, f', h, hf'⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_2
S : Type u_1
inst✝⁴ : Ring R
inst✝³ : CharTwo R
inst✝² : Ring S
inst✝¹ : NoZeroDivisors S
inst✝ : CharTwo S
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
hρ : Function.Injective ⇑ρ
f' : R' → S'
h : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
⊢ f (φ x + 1) = f (φ x) + 1
Theorem: IMOSL.IMO2012A5.Case3.SCharTwo.solution
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_2
S : Type u_1
inst✝⁴ : Ring R
inst✝³ : CharTwo R
inst✝² : Ring S
inst✝¹ : NoZeroDivisors S
inst✝ : CharTwo S
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
hρ : Function.Injective ⇑ρ
f' : R' → S'
h : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
⊢ f (φ x + 1) = f (φ x) + 1
Tactic:
have R'char := pullback_of_inj φ.toAddMonoidHom hφ
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_2
S : Type u_1
inst✝⁴ : Ring R
inst✝³ : CharTwo R
inst✝² : Ring S
inst✝¹ : NoZeroDivisors S
inst✝ : CharTwo S
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
hρ : Function.Injective ⇑ρ
f' : R' → S'
h : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
R'char : CharTwo R'
⊢ f (φ x + 1) = f (φ x) + 1
Theorem: IMOSL.IMO2012A5.Case3.SCharTwo.solution
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_2
S : Type u_1
inst✝⁴ : Ring R
inst✝³ : CharTwo R
inst✝² : Ring S
inst✝¹ : NoZeroDivisors S
inst✝ : CharTwo S
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
hρ : Function.Injective ⇑ρ
f' : R' → S'
h : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
R'char : CharTwo R'
⊢ f (φ x + 1) = f (φ x) + 1
Tactic:
have S'char := pullback_of_inj ρ.toAddMonoidHom hρ
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_2
S : Type u_1
inst✝⁴ : Ring R
inst✝³ : CharTwo R
inst✝² : Ring S
inst✝¹ : NoZeroDivisors S
inst✝ : CharTwo S
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
hρ : Function.Injective ⇑ρ
f' : R' → S'
h : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
R'char : CharTwo R'
S'char : CharTwo S'
⊢ f (φ x + 1) = f (φ x) + 1
Theorem: IMOSL.IMO2012A5.Case3.SCharTwo.solution
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_2
S : Type u_1
inst✝⁴ : Ring R
inst✝³ : CharTwo R
inst✝² : Ring S
inst✝¹ : NoZeroDivisors S
inst✝ : CharTwo S
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
hρ : Function.Injective ⇑ρ
f' : R' → S'
h : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
R'char : CharTwo R'
S'char : CharTwo S'
⊢ f (φ x + 1) = f (φ x) + 1
Tactic:
rw [h, ← φ.map_one, ← φ.map_add, h, ← ρ.map_one, ← ρ.map_add]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_2
S : Type u_1
inst✝⁴ : Ring R
inst✝³ : CharTwo R
inst✝² : Ring S
inst✝¹ : NoZeroDivisors S
inst✝ : CharTwo S
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
hρ : Function.Injective ⇑ρ
f' : R' → S'
h : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
R'char : CharTwo R'
S'char : CharTwo S'
⊢ ρ (f' (x + 1)) = ρ (f' x + 1)
Theorem: IMOSL.IMO2012A5.Case3.SCharTwo.solution
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_2
S : Type u_1
inst✝⁴ : Ring R
inst✝³ : CharTwo R
inst✝² : Ring S
inst✝¹ : NoZeroDivisors S
inst✝ : CharTwo S
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
hρ : Function.Injective ⇑ρ
f' : R' → S'
h : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
R'char : CharTwo R'
S'char : CharTwo S'
⊢ ρ (f' (x + 1)) = ρ (f' x + 1)
Tactic:
exact ρ.congr_arg (CommCase.SCharTwo_map_add_one hf' x)
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.main_cases
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 = 0 ∨ f (x + 1) = 0) ∨ f x + f (x + 1) = 1 ∧ f x * f (x + 1) = -1
Tactic:
rcases CommSubring.oneVarCommLiftDomain_exists hf x with
  ⟨R', R'comm, φ, hφ, ⟨x, rfl⟩, S', S'comm, S'nzd, ρ, -, f', h, hf'⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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
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'
⊢ (f (φ x) = 0 ∨ f (φ x + 1) = 0) ∨ f (φ x) + f (φ x + 1) = 1 ∧ f (φ x) * f (φ x + 1) = -1
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.main_cases
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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
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'
⊢ (f (φ x) = 0 ∨ f (φ x + 1) = 0) ∨ f (φ x) + f (φ x + 1) = 1 ∧ f (φ x) * f (φ x + 1) = -1
Tactic:
have R'char := pullback_of_inj φ.toAddMonoidHom hφ
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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
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'
⊢ (f (φ x) = 0 ∨ f (φ x + 1) = 0) ∨ f (φ x) + f (φ x + 1) = 1 ∧ f (φ x) * f (φ x + 1) = -1
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.main_cases
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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
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'
⊢ (f (φ x) = 0 ∨ f (φ x + 1) = 0) ∨ f (φ x) + f (φ x + 1) = 1 ∧ f (φ x) * f (φ x + 1) = -1
Tactic:
have S'char : (2 : S') ≠ 0 := λ h1 ↦ hS <| by rw [← map_ofNat ρ 2, h1, ρ.map_zero]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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
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
⊢ (f (φ x) = 0 ∨ f (φ x + 1) = 0) ∨ f (φ x) + f (φ x + 1) = 1 ∧ f (φ x) * f (φ x + 1) = -1
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.main_cases
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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
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
⊢ (f (φ x) = 0 ∨ f (φ x + 1) = 0) ∨ f (φ x) + f (φ x + 1) = 1 ∧ f (φ x) * f (φ x + 1) = -1
Tactic:
rw [h, ← φ.map_one, ← φ.map_add, h, ← ρ.map_zero]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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
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
⊢ (ρ (f' x) = ρ 0 ∨ ρ (f' (x + 1)) = ρ 0) ∨ ρ (f' x) + ρ (f' (x + 1)) = 1 ∧ ρ (f' x) * ρ (f' (x + 1)) = -1
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.main_cases
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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
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
⊢ (ρ (f' x) = ρ 0 ∨ ρ (f' (x + 1)) = ρ 0) ∨ ρ (f' x) + ρ (f' (x + 1)) = 1 ∧ ρ (f' x) * ρ (f' (x + 1)) = -1
Tactic:
refine (CommCase.SCharNeTwo_cases hf' S'char x).imp
  (Or.imp ρ.congr_arg ρ.congr_arg) (And.imp (λ h0 ↦ ?_) (λ h0 ↦ ?_))
Proof state after:
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

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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.main_cases
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
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'
h1 : 2 = 0
⊢ 2 = 0
Tactic:
rw [← map_ofNat ρ 2, h1, ρ.map_zero]
Proof state after:
no goals