Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.main_cases (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 : 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'⟩
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

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φ
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

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]
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

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]
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

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 ↦ ?_))
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

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]
State after:
no goals

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]
State after:
no goals

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]
State after:
no goals