Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.Eq3_2 (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
g : R → S
hg : ShiftGood23 g
x : R
⊢ (g (x + 1) - g (x - 1)) ^ 2 = 2 ^ 4 * g x
Tactic:
rcases oneVarLift_exists hg x with
  ⟨R', R'comm, φ, -, ⟨x, rfl⟩, S', S'comm, S'nzd, ρ, -, g', h0, hg'⟩
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
g : R → S
hg : ShiftGood23 g
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
g' : R' → S'
h0 : ∀ (a : R'), g (φ a) = ρ (g' a)
hg' : ShiftGood23 g'
⊢ (g (φ x + 1) - g (φ x - 1)) ^ 2 = 2 ^ 4 * g (φ x)

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
g : R → S
hg : ShiftGood23 g
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
g' : R' → S'
h0 : ∀ (a : R'), g (φ a) = ρ (g' a)
hg' : ShiftGood23 g'
⊢ (g (φ x + 1) - g (φ x - 1)) ^ 2 = 2 ^ 4 * g (φ x)
Tactic:
rw [← φ.map_one, ← φ.map_add, ← φ.map_sub, h0, h0, ← ρ.map_sub, ← ρ.map_pow,
  CommCase.Eq3_2 hg', h0, ρ.map_mul, ρ.map_pow, map_ofNat]
State after:
no goals