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

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

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

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

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