-- Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
lemma normEDS_odd (m : ℤ) : normEDS b c d (2 * m + 1) =
    normEDS b c d (m + 2) * normEDS b c d m ^ 3 -
      normEDS b c d (m - 1) * normEDS b c d (m + 1) ^ 3

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
m : ℤ
⊢ (preNormEDS (b ^ 4) c d (m + 2) * preNormEDS (b ^ 4) c d m ^ 3 * (if Even m then b else 1) ^ 4 -
        preNormEDS (b ^ 4) c d (m - 1) * preNormEDS (b ^ 4) c d (m + 1) ^ 3 * (if Even m then 1 else b) ^ 4) *
      1 ^ 4 =
    (preNormEDS (b ^ 4) c d (m + 2) * if Even (m + 2) then b else 1) *
        (preNormEDS (b ^ 4) c d m * if Even m then b else 1) ^ 3 -
      (preNormEDS (b ^ 4) c d (m - 1) * if Even (m - 1) then b else 1) *
        (preNormEDS (b ^ 4) c d (m + 1) * if Even (m + 1) then b else 1) ^ 3

Tactic:
simp only [show m + 2 = m + 1 + 1 by ring1, Int.even_add_one, Int.even_sub_one, ite_not]

Result:
R : Type u
inst✝ : CommRing R
b c d : R
m : ℤ
⊢ (preNormEDS (b ^ 4) c d (m + 1 + 1) * preNormEDS (b ^ 4) c d m ^ 3 * (if Even m then b else 1) ^ 4 -
        preNormEDS (b ^ 4) c d (m - 1) * preNormEDS (b ^ 4) c d (m + 1) ^ 3 * (if Even m then 1 else b) ^ 4) *
      1 ^ 4 =
    (preNormEDS (b ^ 4) c d (m + 1 + 1) * if Even m then b else 1) *
        (preNormEDS (b ^ 4) c d m * if Even m then b else 1) ^ 3 -
      (preNormEDS (b ^ 4) c d (m - 1) * if Even m then 1 else b) *
        (preNormEDS (b ^ 4) c d (m + 1) * if Even m then 1 else b) ^ 3

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
m : ℤ
⊢ (preNormEDS (b ^ 4) c d (m + 1 + 1) * preNormEDS (b ^ 4) c d m ^ 3 * (if Even m then b else 1) ^ 4 -
        preNormEDS (b ^ 4) c d (m - 1) * preNormEDS (b ^ 4) c d (m + 1) ^ 3 * (if Even m then 1 else b) ^ 4) *
      1 ^ 4 =
    (preNormEDS (b ^ 4) c d (m + 1 + 1) * if Even m then b else 1) *
        (preNormEDS (b ^ 4) c d m * if Even m then b else 1) ^ 3 -
      (preNormEDS (b ^ 4) c d (m - 1) * if Even m then 1 else b) *
        (preNormEDS (b ^ 4) c d (m + 1) * if Even m then 1 else b) ^ 3

Tactic:
ring1

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
m : ℤ
⊢ normEDS b c d (2 * m + 1) =
    normEDS b c d (m + 2) * normEDS b c d m ^ 3 - normEDS b c d (m - 1) * normEDS b c d (m + 1) ^ 3

Tactic:
simp only [normEDS, preNormEDS_odd, if_neg m.not_even_two_mul_add_one]

Result:
R : Type u
inst✝ : CommRing R
b c d : R
m : ℤ
⊢ ((preNormEDS (b ^ 4) c d (m + 2) * preNormEDS (b ^ 4) c d m ^ 3 * if Even m then b ^ 4 else 1) -
        preNormEDS (b ^ 4) c d (m - 1) * preNormEDS (b ^ 4) c d (m + 1) ^ 3 * if Even m then 1 else b ^ 4) *
      1 =
    (preNormEDS (b ^ 4) c d (m + 2) * if Even (m + 2) then b else 1) *
        (preNormEDS (b ^ 4) c d m * if Even m then b else 1) ^ 3 -
      (preNormEDS (b ^ 4) c d (m - 1) * if Even (m - 1) then b else 1) *
        (preNormEDS (b ^ 4) c d (m + 1) * if Even (m + 1) then b else 1) ^ 3

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
m : ℤ
⊢ m + 2 = m + 1 + 1

Tactic:
ring1

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
m : ℤ
⊢ ((preNormEDS (b ^ 4) c d (m + 2) * preNormEDS (b ^ 4) c d m ^ 3 * if Even m then b ^ 4 else 1) -
        preNormEDS (b ^ 4) c d (m - 1) * preNormEDS (b ^ 4) c d (m + 1) ^ 3 * if Even m then 1 else b ^ 4) *
      1 =
    (preNormEDS (b ^ 4) c d (m + 2) * if Even (m + 2) then b else 1) *
        (preNormEDS (b ^ 4) c d m * if Even m then b else 1) ^ 3 -
      (preNormEDS (b ^ 4) c d (m - 1) * if Even (m - 1) then b else 1) *
        (preNormEDS (b ^ 4) c d (m + 1) * if Even (m + 1) then b else 1) ^ 3

Tactic:
conv_lhs => rw [← @one_pow R _ 4, ← ite_pow, ← ite_pow]

Result:
R : Type u
inst✝ : CommRing R
b c d : R
m : ℤ
⊢ (preNormEDS (b ^ 4) c d (m + 2) * preNormEDS (b ^ 4) c d m ^ 3 * (if Even m then b else 1) ^ 4 -
        preNormEDS (b ^ 4) c d (m - 1) * preNormEDS (b ^ 4) c d (m + 1) ^ 3 * (if Even m then 1 else b) ^ 4) *
      1 ^ 4 =
    (preNormEDS (b ^ 4) c d (m + 2) * if Even (m + 2) then b else 1) *
        (preNormEDS (b ^ 4) c d m * if Even m then b else 1) ^ 3 -
      (preNormEDS (b ^ 4) c d (m - 1) * if Even (m - 1) then b else 1) *
        (preNormEDS (b ^ 4) c d (m + 1) * if Even (m + 1) then b else 1) ^ 3