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

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

Tactic:
simp only [normEDS, preNormEDS_even, if_pos <| even_two_mul m, show m + 2 = m + 1 + 1 by ring1,
  Int.even_add_one, show m - 2 = m - 1 - 1 by ring1, 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) ^ 2 * preNormEDS (b ^ 4) c d m * preNormEDS (b ^ 4) c d (m + 1 + 1) -
          preNormEDS (b ^ 4) c d (m - 1 - 1) * preNormEDS (b ^ 4) c d m * preNormEDS (b ^ 4) c d (m + 1) ^ 2) *
        b *
      b =
    (preNormEDS (b ^ 4) c d (m - 1) * if Even m then 1 else b) ^ 2 *
          (preNormEDS (b ^ 4) c d m * if Even m then b else 1) *
        (preNormEDS (b ^ 4) c d (m + 1 + 1) * if Even m then b else 1) -
      (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) *
        (preNormEDS (b ^ 4) c d (m + 1) * if Even m then 1 else b) ^ 2

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:
case neg
R : Type u
inst✝ : CommRing R
b c d : R
m : ℤ
hm : ¬Even m
⊢ (preNormEDS (b ^ 4) c d (m - 1) ^ 2 * preNormEDS (b ^ 4) c d m * preNormEDS (b ^ 4) c d (m + 1 + 1) -
          preNormEDS (b ^ 4) c d (m - 1 - 1) * preNormEDS (b ^ 4) c d m * preNormEDS (b ^ 4) c d (m + 1) ^ 2) *
        b *
      b =
    (preNormEDS (b ^ 4) c d (m - 1) * if Even m then 1 else b) ^ 2 *
          (preNormEDS (b ^ 4) c d m * if Even m then b else 1) *
        (preNormEDS (b ^ 4) c d (m + 1 + 1) * if Even m then b else 1) -
      (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) *
        (preNormEDS (b ^ 4) c d (m + 1) * if Even m then 1 else b) ^ 2

Tactic:
simp only [if_neg hm]

Result:
case neg
R : Type u
inst✝ : CommRing R
b c d : R
m : ℤ
hm : ¬Even m
⊢ (preNormEDS (b ^ 4) c d (m - 1) ^ 2 * preNormEDS (b ^ 4) c d m * preNormEDS (b ^ 4) c d (m + 1 + 1) -
          preNormEDS (b ^ 4) c d (m - 1 - 1) * preNormEDS (b ^ 4) c d m * preNormEDS (b ^ 4) c d (m + 1) ^ 2) *
        b *
      b =
    (preNormEDS (b ^ 4) c d (m - 1) * b) ^ 2 * (preNormEDS (b ^ 4) c d m * 1) *
        (preNormEDS (b ^ 4) c d (m + 1 + 1) * 1) -
      preNormEDS (b ^ 4) c d (m - 1 - 1) * 1 * (preNormEDS (b ^ 4) c d m * 1) * (preNormEDS (b ^ 4) c d (m + 1) * b) ^ 2

Proof state:
case neg
R : Type u
inst✝ : CommRing R
b c d : R
m : ℤ
hm : ¬Even m
⊢ (preNormEDS (b ^ 4) c d (m - 1) ^ 2 * preNormEDS (b ^ 4) c d m * preNormEDS (b ^ 4) c d (m + 1 + 1) -
          preNormEDS (b ^ 4) c d (m - 1 - 1) * preNormEDS (b ^ 4) c d m * preNormEDS (b ^ 4) c d (m + 1) ^ 2) *
        b *
      b =
    (preNormEDS (b ^ 4) c d (m - 1) * b) ^ 2 * (preNormEDS (b ^ 4) c d m * 1) *
        (preNormEDS (b ^ 4) c d (m + 1 + 1) * 1) -
      preNormEDS (b ^ 4) c d (m - 1 - 1) * 1 * (preNormEDS (b ^ 4) c d m * 1) * (preNormEDS (b ^ 4) c d (m + 1) * b) ^ 2

Tactic:
ring1

Result:
no goals

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

Tactic:
by_cases hm : Even m

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

case neg
R : Type u
inst✝ : CommRing R
b c d : R
m : ℤ
hm : ¬Even m
⊢ (preNormEDS (b ^ 4) c d (m - 1) ^ 2 * preNormEDS (b ^ 4) c d m * preNormEDS (b ^ 4) c d (m + 1 + 1) -
          preNormEDS (b ^ 4) c d (m - 1 - 1) * preNormEDS (b ^ 4) c d m * preNormEDS (b ^ 4) c d (m + 1) ^ 2) *
        b *
      b =
    (preNormEDS (b ^ 4) c d (m - 1) * if Even m then 1 else b) ^ 2 *
          (preNormEDS (b ^ 4) c d m * if Even m then b else 1) *
        (preNormEDS (b ^ 4) c d (m + 1 + 1) * if Even m then b else 1) -
      (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) *
        (preNormEDS (b ^ 4) c d (m + 1) * if Even m then 1 else b) ^ 2

Proof state:
case pos
R : Type u
inst✝ : CommRing R
b c d : R
m : ℤ
hm : Even m
⊢ (preNormEDS (b ^ 4) c d (m - 1) ^ 2 * preNormEDS (b ^ 4) c d m * preNormEDS (b ^ 4) c d (m + 1 + 1) -
          preNormEDS (b ^ 4) c d (m - 1 - 1) * preNormEDS (b ^ 4) c d m * preNormEDS (b ^ 4) c d (m + 1) ^ 2) *
        b *
      b =
    (preNormEDS (b ^ 4) c d (m - 1) * 1) ^ 2 * (preNormEDS (b ^ 4) c d m * b) *
        (preNormEDS (b ^ 4) c d (m + 1 + 1) * b) -
      preNormEDS (b ^ 4) c d (m - 1 - 1) * b * (preNormEDS (b ^ 4) c d m * b) * (preNormEDS (b ^ 4) c d (m + 1) * 1) ^ 2

Tactic:
ring1

Result:
no goals

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

Tactic:
simp only [if_pos hm]

Result:
case pos
R : Type u
inst✝ : CommRing R
b c d : R
m : ℤ
hm : Even m
⊢ (preNormEDS (b ^ 4) c d (m - 1) ^ 2 * preNormEDS (b ^ 4) c d m * preNormEDS (b ^ 4) c d (m + 1 + 1) -
          preNormEDS (b ^ 4) c d (m - 1 - 1) * preNormEDS (b ^ 4) c d m * preNormEDS (b ^ 4) c d (m + 1) ^ 2) *
        b *
      b =
    (preNormEDS (b ^ 4) c d (m - 1) * 1) ^ 2 * (preNormEDS (b ^ 4) c d m * b) *
        (preNormEDS (b ^ 4) c d (m + 1 + 1) * b) -
      preNormEDS (b ^ 4) c d (m - 1 - 1) * b * (preNormEDS (b ^ 4) c d m * b) * (preNormEDS (b ^ 4) c d (m + 1) * 1) ^ 2

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

Tactic:
ring1

Result:
no goals