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

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

Tactic:
simp only [preNormEDS'_even, if_pos <| even_two_mul _, Nat.even_add_one, ite_not]

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

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

Tactic:
repeat erw [normEDS_ofNat]

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

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

Tactic:
split_ifs <;> ring1

Result:
no goals

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

Tactic:
erw [normEDS_ofNat]

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