Theorem: IMOSL.IMO2012A5.Case2.CharTwo'_of_map_two (IMOSLLean4/IMO2012/A5/A5Cases/Case2.lean)

State before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
h : f (-1) = 0
h0 : f 2 = -1
⊢ 2 = 0
Tactic:
refine hf.period_imp_zero λ x ↦ ?_
State after:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
h : f (-1) = 0
h0 : f 2 = -1
x : R
⊢ f (x + 2) = f x

State before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
h : f (-1) = 0
h0 : f 2 = -1
x : R
⊢ f (x + 2) = f x
Tactic:
rcases CommSubring.oneVarCommLiftDomain_exists hf.toNontrivialGood x with
  ⟨R', R'comm, φ, -, ⟨x, rfl⟩, S', S'comm, S'nzd, ρ, hρ, f', h1, hf'⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
h : f (-1) = 0
h0 : f 2 = -1
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
x : R'
S' : Type u_1
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h1 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
⊢ f (φ x + 2) = f (φ x)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
h : f (-1) = 0
h0 : f 2 = -1
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
x : R'
S' : Type u_1
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h1 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
⊢ f (φ x + 2) = f (φ x)
Tactic:
rw [← map_ofNat φ 2, ← φ.map_add, h1, h1, CommCase.two_periodic_of_map_two hf']
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.h
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
h : f (-1) = 0
h0 : f 2 = -1
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
x : R'
S' : Type u_1
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h1 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
⊢ ∀ (x : R'), f' (-x) = f' x

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.h0
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
h : f (-1) = 0
h0 : f 2 = -1
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
x : R'
S' : Type u_1
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h1 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
⊢ f' 2 = -1

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.h
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
h : f (-1) = 0
h0 : f 2 = -1
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
x : R'
S' : Type u_1
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h1 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
⊢ ∀ (x : R'), f' (-x) = f' x
Tactic:
refine map_even_of_map_one hf'.is_good (hρ ?_)
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.h
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
h : f (-1) = 0
h0 : f 2 = -1
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
x : R'
S' : Type u_1
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h1 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
⊢ ρ (f' (-1)) = ρ 0

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.h
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
h : f (-1) = 0
h0 : f 2 = -1
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
x : R'
S' : Type u_1
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h1 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
⊢ ρ (f' (-1)) = ρ 0
Tactic:
rw [← h1, φ.map_neg, φ.map_one, h, ρ.map_zero]
State after:
no goals

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.h0
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
h : f (-1) = 0
h0 : f 2 = -1
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
x : R'
S' : Type u_1
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h1 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
⊢ f' 2 = -1
Tactic:
apply hρ
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.h0.a
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
h : f (-1) = 0
h0 : f 2 = -1
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
x : R'
S' : Type u_1
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h1 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
⊢ ρ (f' 2) = ρ (-1)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.h0.a
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
h : f (-1) = 0
h0 : f 2 = -1
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
x : R'
S' : Type u_1
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h1 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
⊢ ρ (f' 2) = ρ (-1)
Tactic:
rw [← h1, map_ofNat, h0, ρ.map_neg, ρ.map_one]
State after:
no goals