-- Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
lemma map_preNormEDS' (n : ℕ) : f (preNormEDS' b c d n) = preNormEDS' (f b) (f c) (f d) n

Proof state:
R : Type u
inst✝¹ : CommRing R
b c d : R
S : Type v
inst✝ : CommRing S
f : R →+* S
n : ℕ
⊢ f (preNormEDS' b c d n) = preNormEDS' (f b) (f c) (f d) n

Tactic:
induction n using normEDSRec' with
| zero => rw [preNormEDS'_zero, map_zero, preNormEDS'_zero]
| one => rw [preNormEDS'_one, map_one, preNormEDS'_one]
| two => rw [preNormEDS'_two, map_one, preNormEDS'_two]
| three => rw [preNormEDS'_three, preNormEDS'_three]
| four => rw [preNormEDS'_four, preNormEDS'_four]
| _ _ ih =>
  simp only [preNormEDS'_odd, preNormEDS'_even, map_one, map_sub, map_mul, map_pow, apply_ite f]
  repeat rw [ih _ <| by linarith only]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
b c d : R
S : Type v
inst✝ : CommRing S
f : R →+* S
m✝ : ℕ
ih : ∀ k < 2 * (m✝ + 2) + 1, f (preNormEDS' b c d k) = preNormEDS' (f b) (f c) (f d) k
⊢ m✝ + 3 < 2 * (m✝ + 2) + 1

Tactic:
linarith only

Result:
no goals

Proof state:
case one
R : Type u
inst✝¹ : CommRing R
b c d : R
S : Type v
inst✝ : CommRing S
f : R →+* S
⊢ f (preNormEDS' b c d 1) = preNormEDS' (f b) (f c) (f d) 1

Tactic:
rw [preNormEDS'_one, map_one, preNormEDS'_one]

Result:
no goals

Proof state:
case zero
R : Type u
inst✝¹ : CommRing R
b c d : R
S : Type v
inst✝ : CommRing S
f : R →+* S
⊢ f (preNormEDS' b c d 0) = preNormEDS' (f b) (f c) (f d) 0

Tactic:
rw [preNormEDS'_zero, map_zero, preNormEDS'_zero]

Result:
no goals

Proof state:
case two
R : Type u
inst✝¹ : CommRing R
b c d : R
S : Type v
inst✝ : CommRing S
f : R →+* S
⊢ f (preNormEDS' b c d 2) = preNormEDS' (f b) (f c) (f d) 2

Tactic:
rw [preNormEDS'_two, map_one, preNormEDS'_two]

Result:
no goals

Proof state:
case odd
R : Type u
inst✝¹ : CommRing R
b c d : R
S : Type v
inst✝ : CommRing S
f : R →+* S
m✝ : ℕ
ih : ∀ k < 2 * (m✝ + 2) + 1, f (preNormEDS' b c d k) = preNormEDS' (f b) (f c) (f d) k
⊢ f (preNormEDS' b c d (2 * (m✝ + 2) + 1)) = preNormEDS' (f b) (f c) (f d) (2 * (m✝ + 2) + 1)

Tactic:
simp only [preNormEDS'_odd, preNormEDS'_even, map_one, map_sub, map_mul, map_pow, apply_ite f]

Result:
case odd
R : Type u
inst✝¹ : CommRing R
b c d : R
S : Type v
inst✝ : CommRing S
f : R →+* S
m✝ : ℕ
ih : ∀ k < 2 * (m✝ + 2) + 1, f (preNormEDS' b c d k) = preNormEDS' (f b) (f c) (f d) k
⊢ ((f (preNormEDS' b c d (m✝ + 4)) * f (preNormEDS' b c d (m✝ + 2)) ^ 3 * if Even m✝ then f b else 1) -
      f (preNormEDS' b c d (m✝ + 1)) * f (preNormEDS' b c d (m✝ + 3)) ^ 3 * if Even m✝ then 1 else f b) =
    (preNormEDS' (f b) (f c) (f d) (m✝ + 4) * preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 3 * if Even m✝ then f b else 1) -
      preNormEDS' (f b) (f c) (f d) (m✝ + 1) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) ^ 3 * if Even m✝ then 1 else f b

Proof state:
case four
R : Type u
inst✝¹ : CommRing R
b c d : R
S : Type v
inst✝ : CommRing S
f : R →+* S
⊢ f (preNormEDS' b c d 4) = preNormEDS' (f b) (f c) (f d) 4

Tactic:
rw [preNormEDS'_four, preNormEDS'_four]

Result:
no goals

Proof state:
case three
R : Type u
inst✝¹ : CommRing R
b c d : R
S : Type v
inst✝ : CommRing S
f : R →+* S
⊢ f (preNormEDS' b c d 3) = preNormEDS' (f b) (f c) (f d) 3

Tactic:
rw [preNormEDS'_three, preNormEDS'_three]

Result:
no goals

Proof state:
case odd
R : Type u
inst✝¹ : CommRing R
b c d : R
S : Type v
inst✝ : CommRing S
f : R →+* S
m✝ : ℕ
ih : ∀ k < 2 * (m✝ + 2) + 1, f (preNormEDS' b c d k) = preNormEDS' (f b) (f c) (f d) k
⊢ ((preNormEDS' (f b) (f c) (f d) (m✝ + 4) * preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 3 * if Even m✝ then f b else 1) -
      preNormEDS' (f b) (f c) (f d) (m✝ + 1) * f (preNormEDS' b c d (m✝ + 3)) ^ 3 * if Even m✝ then 1 else f b) =
    (preNormEDS' (f b) (f c) (f d) (m✝ + 4) * preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 3 * if Even m✝ then f b else 1) -
      preNormEDS' (f b) (f c) (f d) (m✝ + 1) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) ^ 3 * if Even m✝ then 1 else f b

Tactic:
rw [ih _ <| by linarith only]

Result:
no goals

Proof state:
case odd
R : Type u
inst✝¹ : CommRing R
b c d : R
S : Type v
inst✝ : CommRing S
f : R →+* S
m✝ : ℕ
ih : ∀ k < 2 * (m✝ + 2) + 1, f (preNormEDS' b c d k) = preNormEDS' (f b) (f c) (f d) k
⊢ ((f (preNormEDS' b c d (m✝ + 4)) * f (preNormEDS' b c d (m✝ + 2)) ^ 3 * if Even m✝ then f b else 1) -
      f (preNormEDS' b c d (m✝ + 1)) * f (preNormEDS' b c d (m✝ + 3)) ^ 3 * if Even m✝ then 1 else f b) =
    (preNormEDS' (f b) (f c) (f d) (m✝ + 4) * preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 3 * if Even m✝ then f b else 1) -
      preNormEDS' (f b) (f c) (f d) (m✝ + 1) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) ^ 3 * if Even m✝ then 1 else f b

Tactic:
repeat rw [ih _ <| by linarith only]

Result:
no goals