Theorem: IMOSL.IMO2012A5.Case2.GoodCase2.Eq7 (IMOSLLean4/IMO2012/A5/A5Cases/Case2.lean)

State before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h1 : f 2 ≠ 1
x : R
⊢ (f (x + 1) + 1) * (f (x - 1) + 1) = f x ^ 2
Tactic:
rcases oneVarLift_exists hf x with
  ⟨R', R'comm, φ, -, ⟨x, rfl⟩, S', S'comm, S'nzd, ρ, -, f', h0, 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✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h1 : f 2 ≠ 1
R' : Type u_2
R'comm : CommRing R'
φ : R' →+* R
x : R'
S' : Type u_1
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
f' : R' → S'
h0 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : GoodCase2 f'
⊢ (f (φ x + 1) + 1) * (f (φ x - 1) + 1) = f (φ x) ^ 2

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✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h1 : f 2 ≠ 1
R' : Type u_2
R'comm : CommRing R'
φ : R' →+* R
x : R'
S' : Type u_1
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
f' : R' → S'
h0 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : GoodCase2 f'
⊢ (f (φ x + 1) + 1) * (f (φ x - 1) + 1) = f (φ x) ^ 2
Tactic:
have h2 : f' 2 ≠ 1 := λ h2 ↦ h1 <| by rw [← map_ofNat φ 2, h0, h2, ρ.map_one]
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✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h1 : f 2 ≠ 1
R' : Type u_2
R'comm : CommRing R'
φ : R' →+* R
x : R'
S' : Type u_1
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
f' : R' → S'
h0 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : GoodCase2 f'
h2 : f' 2 ≠ 1
⊢ (f (φ x + 1) + 1) * (f (φ x - 1) + 1) = f (φ x) ^ 2

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✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h1 : f 2 ≠ 1
R' : Type u_2
R'comm : CommRing R'
φ : R' →+* R
x : R'
S' : Type u_1
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
f' : R' → S'
h0 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : GoodCase2 f'
h2 : f' 2 ≠ 1
⊢ (f (φ x + 1) + 1) * (f (φ x - 1) + 1) = f (φ x) ^ 2
Tactic:
rw [h0, ← φ.map_one, ← φ.map_sub, ← φ.map_add, h0, h0, ← ρ.map_one,
  ← ρ.map_add, ← ρ.map_add, ← ρ.map_mul, ← ρ.map_pow]
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✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h1 : f 2 ≠ 1
R' : Type u_2
R'comm : CommRing R'
φ : R' →+* R
x : R'
S' : Type u_1
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
f' : R' → S'
h0 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : GoodCase2 f'
h2 : f' 2 ≠ 1
⊢ ρ ((f' (x + 1) + 1) * (f' (x - 1) + 1)) = ρ (f' x ^ 2)

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✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h1 : f 2 ≠ 1
R' : Type u_2
R'comm : CommRing R'
φ : R' →+* R
x : R'
S' : Type u_1
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
f' : R' → S'
h0 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : GoodCase2 f'
h2 : f' 2 ≠ 1
⊢ ρ ((f' (x + 1) + 1) * (f' (x - 1) + 1)) = ρ (f' x ^ 2)
Tactic:
exact congrArg ρ
  (CommCase.Eq7 hf'.toNontrivialGood hf'.map_even hf'.map_two_ne_neg_one h2 x)
State after:
no goals

State before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h1 : f 2 ≠ 1
R' : Type u_2
R'comm : CommRing R'
φ : R' →+* R
x : R'
S' : Type u_1
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
f' : R' → S'
h0 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : GoodCase2 f'
h2 : f' 2 = 1
⊢ f 2 = 1
Tactic:
rw [← map_ofNat φ 2, h0, h2, ρ.map_one]
State after:
no goals