Theorem: IMOSL.IMO2012A5.Case2.GoodCase2.Eq6 (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
x : R
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)
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
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) + f (φ x - 1) = (f (φ x) + 1) * (f 2 - 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✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
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) + f (φ x - 1) = (f (φ x) + 1) * (f 2 - 1)
Tactic:
rw [h0, ← φ.map_one, ← φ.map_sub, ← φ.map_add, h0, h0, ← map_ofNat φ 2, h0,
  ← ρ.map_one, ← ρ.map_add, ← ρ.map_add, ← ρ.map_sub, ← ρ.map_mul]
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
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) + f' (x - 1)) = ρ ((f' x + 1) * (f' (OfNat.ofNat 2) - 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✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
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) + f' (x - 1)) = ρ ((f' x + 1) * (f' (OfNat.ofNat 2) - 1))
Tactic:
exact congrArg ρ
  (CommCase.Eq6 hf'.toNontrivialGood hf'.map_even hf'.map_two_ne_neg_one x)
State after:
no goals