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

Proof state:
case neg
R : Type u
inst✝ : CommRing R
b c d : R
h :
  ∀ (n : ℕ),
    preNormEDS b c d (2 * ↑n) =
      preNormEDS b c d (↑n - 1) ^ 2 * preNormEDS b c d ↑n * preNormEDS b c d (↑n + 2) -
        preNormEDS b c d (↑n - 2) * preNormEDS b c d ↑n * preNormEDS b c d (↑n + 1) ^ 2
m : ℕ
⊢ -(preNormEDS b c d (↑m - 1) ^ 2 * preNormEDS b c d ↑m * preNormEDS b c d (↑m + 2) -
        preNormEDS b c d (↑m - 2) * preNormEDS b c d ↑m * preNormEDS b c d (↑m + 1) ^ 2) =
    (-preNormEDS b c d (↑m + 1)) ^ 2 * -preNormEDS b c d ↑m * -preNormEDS b c d (↑m - 2) -
      -preNormEDS b c d (↑m + 2) * -preNormEDS b c d ↑m * (-preNormEDS b c d (↑m - 1)) ^ 2

Tactic:
ring1

Result:
no goals

Proof state:
case nat.succ.zero
R : Type u
inst✝ : CommRing R
b c d : R
⊢ preNormEDS b c d (2 * ↑(0 + 1)) =
    preNormEDS b c d (↑(0 + 1) - 1) ^ 2 * preNormEDS b c d ↑(0 + 1) * preNormEDS b c d (↑(0 + 1) + 2) -
      preNormEDS b c d (↑(0 + 1) - 2) * preNormEDS b c d ↑(0 + 1) * preNormEDS b c d (↑(0 + 1) + 1) ^ 2

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
h :
  ∀ (n : ℕ),
    preNormEDS b c d (2 * ↑n) =
      preNormEDS b c d (↑n - 1) ^ 2 * preNormEDS b c d ↑n * preNormEDS b c d (↑n + 2) -
        preNormEDS b c d (↑n - 2) * preNormEDS b c d ↑n * preNormEDS b c d (↑n + 1) ^ 2
m : ℕ
⊢ -↑m + 1 = -(↑m - 1)

Tactic:
omega

Result:
no goals

Proof state:
case nat.succ.succ.zero
R : Type u
inst✝ : CommRing R
b c d : R
⊢ preNormEDS b c d (2 * ↑(0 + 1 + 1)) =
    preNormEDS b c d (↑(0 + 1 + 1) - 1) ^ 2 * preNormEDS b c d ↑(0 + 1 + 1) * preNormEDS b c d (↑(0 + 1 + 1) + 2) -
      preNormEDS b c d (↑(0 + 1 + 1) - 2) * preNormEDS b c d ↑(0 + 1 + 1) * preNormEDS b c d (↑(0 + 1 + 1) + 1) ^ 2

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
h :
  ∀ (n : ℕ),
    preNormEDS b c d (2 * ↑n) =
      preNormEDS b c d (↑n - 1) ^ 2 * preNormEDS b c d ↑n * preNormEDS b c d (↑n + 2) -
        preNormEDS b c d (↑n - 2) * preNormEDS b c d ↑n * preNormEDS b c d (↑n + 1) ^ 2
m : ℕ
⊢ 2 * -↑m = -(2 * ↑m)

Tactic:
omega

Result:
no goals

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

Tactic:
rcases m with _ | _ | _ | m

Result:
case nat.zero
R : Type u
inst✝ : CommRing R
b c d : R
⊢ preNormEDS b c d (2 * ↑0) =
    preNormEDS b c d (↑0 - 1) ^ 2 * preNormEDS b c d ↑0 * preNormEDS b c d (↑0 + 2) -
      preNormEDS b c d (↑0 - 2) * preNormEDS b c d ↑0 * preNormEDS b c d (↑0 + 1) ^ 2

case nat.succ.zero
R : Type u
inst✝ : CommRing R
b c d : R
⊢ preNormEDS b c d (2 * ↑(0 + 1)) =
    preNormEDS b c d (↑(0 + 1) - 1) ^ 2 * preNormEDS b c d ↑(0 + 1) * preNormEDS b c d (↑(0 + 1) + 2) -
      preNormEDS b c d (↑(0 + 1) - 2) * preNormEDS b c d ↑(0 + 1) * preNormEDS b c d (↑(0 + 1) + 1) ^ 2

case nat.succ.succ.zero
R : Type u
inst✝ : CommRing R
b c d : R
⊢ preNormEDS b c d (2 * ↑(0 + 1 + 1)) =
    preNormEDS b c d (↑(0 + 1 + 1) - 1) ^ 2 * preNormEDS b c d ↑(0 + 1 + 1) * preNormEDS b c d (↑(0 + 1 + 1) + 2) -
      preNormEDS b c d (↑(0 + 1 + 1) - 2) * preNormEDS b c d ↑(0 + 1 + 1) * preNormEDS b c d (↑(0 + 1 + 1) + 1) ^ 2

case nat.succ.succ.succ
R : Type u
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS b c d (2 * ↑(m + 1 + 1 + 1)) =
    preNormEDS b c d (↑(m + 1 + 1 + 1) - 1) ^ 2 * preNormEDS b c d ↑(m + 1 + 1 + 1) *
        preNormEDS b c d (↑(m + 1 + 1 + 1) + 2) -
      preNormEDS b c d (↑(m + 1 + 1 + 1) - 2) * preNormEDS b c d ↑(m + 1 + 1 + 1) *
        preNormEDS b c d (↑(m + 1 + 1 + 1) + 1) ^ 2

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

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
h :
  ∀ (n : ℕ),
    preNormEDS b c d (2 * ↑n) =
      preNormEDS b c d (↑n - 1) ^ 2 * preNormEDS b c d ↑n * preNormEDS b c d (↑n + 2) -
        preNormEDS b c d (↑n - 2) * preNormEDS b c d ↑n * preNormEDS b c d (↑n + 1) ^ 2
m : ℕ
⊢ -↑m - 1 = -(↑m + 1)

Tactic:
omega

Result:
no goals

Proof state:
case nat.succ.succ.succ
R : Type u
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS b c d (2 * (↑m + 1 + 1 + 1)) =
    preNormEDS b c d (↑m + 1 + 1 + 1 - 1) ^ 2 * preNormEDS b c d (↑m + 1 + 1 + 1) *
        preNormEDS b c d (↑m + 1 + 1 + 1 + 2) -
      preNormEDS b c d (↑m + 1 + 1 + 1 - 2) * preNormEDS b c d (↑m + 1 + 1 + 1) *
        preNormEDS b c d (↑m + 1 + 1 + 1 + 1) ^ 2

Tactic:
rw [Int.add_sub_cancel, show (m : ℤ) + 1 + 1 + 1 = m + 1 + 2 by rfl, Int.add_sub_cancel]

Result:
case nat.succ.succ.succ
R : Type u
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS b c d (2 * (↑m + 1 + 2)) =
    preNormEDS b c d (↑m + 1 + 1) ^ 2 * preNormEDS b c d (↑m + 1 + 2) * preNormEDS b c d (↑m + 1 + 2 + 2) -
      preNormEDS b c d (↑m + 1) * preNormEDS b c d (↑m + 1 + 2) * preNormEDS b c d (↑m + 1 + 2 + 1) ^ 2

Proof state:
case neg
R : Type u
inst✝ : CommRing R
b c d : R
h :
  ∀ (n : ℕ),
    preNormEDS b c d (2 * ↑n) =
      preNormEDS b c d (↑n - 1) ^ 2 * preNormEDS b c d ↑n * preNormEDS b c d (↑n + 2) -
        preNormEDS b c d (↑n - 2) * preNormEDS b c d ↑n * preNormEDS b c d (↑n + 1) ^ 2
m : ℕ
⊢ preNormEDS b c d (2 * -↑m) =
    preNormEDS b c d (-↑m - 1) ^ 2 * preNormEDS b c d (-↑m) * preNormEDS b c d (-↑m + 2) -
      preNormEDS b c d (-↑m - 2) * preNormEDS b c d (-↑m) * preNormEDS b c d (-↑m + 1) ^ 2

Tactic:
simp_rw [show 2 * -(m : ℤ) = -(2 * m) by omega, show -(m : ℤ) - 1 = -(m + 1) by omega,
  show -(m : ℤ) + 2 = -(m - 2) by omega, show -(m : ℤ) - 2 = -(m + 2) by omega,
  show -(m : ℤ) + 1 = -(m - 1) by omega, preNormEDS_neg, h m]

Result:
case neg
R : Type u
inst✝ : CommRing R
b c d : R
h :
  ∀ (n : ℕ),
    preNormEDS b c d (2 * ↑n) =
      preNormEDS b c d (↑n - 1) ^ 2 * preNormEDS b c d ↑n * preNormEDS b c d (↑n + 2) -
        preNormEDS b c d (↑n - 2) * preNormEDS b c d ↑n * preNormEDS b c d (↑n + 1) ^ 2
m : ℕ
⊢ -(preNormEDS b c d (↑m - 1) ^ 2 * preNormEDS b c d ↑m * preNormEDS b c d (↑m + 2) -
        preNormEDS b c d (↑m - 2) * preNormEDS b c d ↑m * preNormEDS b c d (↑m + 1) ^ 2) =
    (-preNormEDS b c d (↑m + 1)) ^ 2 * -preNormEDS b c d ↑m * -preNormEDS b c d (↑m - 2) -
      -preNormEDS b c d (↑m + 2) * -preNormEDS b c d ↑m * (-preNormEDS b c d (↑m - 1)) ^ 2

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
h :
  ∀ (n : ℕ),
    preNormEDS b c d (2 * ↑n) =
      preNormEDS b c d (↑n - 1) ^ 2 * preNormEDS b c d ↑n * preNormEDS b c d (↑n + 2) -
        preNormEDS b c d (↑n - 2) * preNormEDS b c d ↑n * preNormEDS b c d (↑n + 1) ^ 2
m : ℕ
⊢ -↑m + 2 = -(↑m - 2)

Tactic:
omega

Result:
no goals

Proof state:
case nat.succ.succ.succ
R : Type u
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS b c d (2 * (↑m + 1 + 2)) =
    preNormEDS b c d (↑m + 1 + 1) ^ 2 * preNormEDS b c d (↑m + 1 + 2) * preNormEDS b c d (↑m + 1 + 2 + 2) -
      preNormEDS b c d (↑m + 1) * preNormEDS b c d (↑m + 1 + 2) * preNormEDS b c d (↑m + 1 + 2 + 1) ^ 2

Tactic:
exact preNormEDS_even_ofNat ..

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
h :
  ∀ (n : ℕ),
    preNormEDS b c d (2 * ↑n) =
      preNormEDS b c d (↑n - 1) ^ 2 * preNormEDS b c d ↑n * preNormEDS b c d (↑n + 2) -
        preNormEDS b c d (↑n - 2) * preNormEDS b c d ↑n * preNormEDS b c d (↑n + 1) ^ 2
m : ℕ
⊢ -↑m - 2 = -(↑m + 2)

Tactic:
omega

Result:
no goals