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

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ ((preNormEDS' (b ^ 4) c d (m + 4) * preNormEDS' (b ^ 4) c d (m + 2) ^ 3 * if Even m then b ^ 4 else 1) -
        preNormEDS' (b ^ 4) c d (m + 1) * preNormEDS' (b ^ 4) c d (m + 3) ^ 3 * if Even m then 1 else b ^ 4) *
      1 =
    (preNormEDS' (b ^ 4) c d (m + 4) * if Even m then b else 1) *
        (preNormEDS' (b ^ 4) c d (m + 2) * 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 + 3) * if Even m then 1 else b) ^ 3

Tactic:
split_ifs <;> ring1

Result:
no goals

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

Tactic:
repeat erw [normEDS_ofNat]

Result:
R : Type u
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ (preNormEDS' (b ^ 4) c d (2 * (m + 2) + 1) * if Even (2 * (m + 2) + 1) then b else 1) =
    (preNormEDS' (b ^ 4) c d (m + 4) * if Even (m + 4) then b else 1) *
        (preNormEDS' (b ^ 4) c d (m + 2) * if Even (m + 2) 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 + 3) * if Even (m + 3) then b else 1) ^ 3

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

Tactic:
erw [normEDS_ofNat]

Result:
R : Type u
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ (preNormEDS' (b ^ 4) c d (2 * (m + 2) + 1) * if Even (2 * (m + 2) + 1) then b else 1) =
    (preNormEDS' (b ^ 4) c d (m + 4) * if Even (m + 4) then b else 1) *
        (preNormEDS' (b ^ 4) c d (m + 2) * if Even (m + 2) 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 + 3) * if Even (m + 3) then b else 1) ^ 3

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ (preNormEDS' (b ^ 4) c d (2 * (m + 2) + 1) * if Even (2 * (m + 2) + 1) then b else 1) =
    (preNormEDS' (b ^ 4) c d (m + 4) * if Even (m + 4) then b else 1) *
        (preNormEDS' (b ^ 4) c d (m + 2) * if Even (m + 2) 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 + 3) * if Even (m + 3) then b else 1) ^ 3

Tactic:
simp_rw [preNormEDS'_odd, if_neg (m + 2).not_even_two_mul_add_one, Nat.even_add_one, ite_not]

Result:
R : Type u
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ ((preNormEDS' (b ^ 4) c d (m + 4) * preNormEDS' (b ^ 4) c d (m + 2) ^ 3 * if Even m then b ^ 4 else 1) -
        preNormEDS' (b ^ 4) c d (m + 1) * preNormEDS' (b ^ 4) c d (m + 3) ^ 3 * if Even m then 1 else b ^ 4) *
      1 =
    (preNormEDS' (b ^ 4) c d (m + 4) * if Even m then b else 1) *
        (preNormEDS' (b ^ 4) c d (m + 2) * 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 + 3) * if Even m then 1 else b) ^ 3