-- Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
lemma preNormEDS_odd (m : ℤ) : preNormEDS b c d (2 * m + 1) =
    preNormEDS b c d (m + 2) * preNormEDS b c d m ^ 3 * (if Even m then b else 1) -
      preNormEDS b c d (m - 1) * preNormEDS b c d (m + 1) ^ 3 * (if Even m then 1 else b)

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

Tactic:
ring1

Result:
no goals

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

Tactic:
rfl

Result:
no goals

Proof state:
case nat.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) + 2) * preNormEDS b c d ↑(m + 1 + 1) ^ 3 * if Even ↑(m + 1 + 1) then b else 1) -
      preNormEDS b c d (↑(m + 1 + 1) - 1) * preNormEDS b c d (↑(m + 1 + 1) + 1) ^ 3 * if Even ↑(m + 1 + 1) then 1 else b

Tactic:
simp only [Int.natCast_add, Nat.cast_one, Int.even_add_one, not_not, Int.even_coe_nat]

Result:
case nat.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 + 2) * preNormEDS b c d (↑m + 1 + 1) ^ 3 * if Even m then b else 1) -
      preNormEDS b c d (↑m + 1 + 1 - 1) * preNormEDS b c d (↑m + 1 + 1 + 1) ^ 3 * if Even m then 1 else b

Proof state:
case nat.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 + 2) * preNormEDS b c d (↑m + 1 + 1) ^ 3 * if Even m then b else 1) -
      preNormEDS b c d (↑m + 1) * preNormEDS b c d (↑m + 1 + 1 + 1) ^ 3 * if Even m then 1 else b

Tactic:
exact preNormEDS_odd_ofNat ..

Result:
no goals

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

Tactic:
omega

Result:
no goals

Proof state:
case nat.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 + 2) * preNormEDS b c d (↑m + 1 + 1) ^ 3 * if Even m then b else 1) -
      preNormEDS b c d (↑m + 1 + 1 - 1) * preNormEDS b c d (↑m + 1 + 1 + 1) ^ 3 * if Even m then 1 else b

Tactic:
rw [Int.add_sub_cancel]

Result:
case nat.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 + 2) * preNormEDS b c d (↑m + 1 + 1) ^ 3 * if Even m then b else 1) -
      preNormEDS b c d (↑m + 1) * preNormEDS b c d (↑m + 1 + 1 + 1) ^ 3 * if Even m then 1 else b

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

Tactic:
omega

Result:
no goals

Proof state:
case neg.zero
R : Type u
inst✝ : CommRing R
b c d : R
h :
  ∀ (n : ℕ),
    preNormEDS b c d (2 * ↑n + 1) =
      (preNormEDS b c d (↑n + 2) * preNormEDS b c d ↑n ^ 3 * if Even ↑n then b else 1) -
        preNormEDS b c d (↑n - 1) * preNormEDS b c d (↑n + 1) ^ 3 * if Even ↑n then 1 else b
⊢ preNormEDS b c d (2 * -↑0 + 1) =
    (preNormEDS b c d (-↑0 + 2) * preNormEDS b c d (-↑0) ^ 3 * if Even (-↑0) then b else 1) -
      preNormEDS b c d (-↑0 - 1) * preNormEDS b c d (-↑0 + 1) ^ 3 * if Even (-↑0) then 1 else b

Tactic:
simp

Result:
no goals

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

Tactic:
simp_rw [Int.natCast_add, Nat.cast_one, show 2 * -(m + 1 : ℤ) + 1 = -(2 * m + 1) by rfl,
  show -(m + 1 : ℤ) + 2 = -(m - 1) by omega, show -(m + 1 : ℤ) - 1 = -(m + 2) by rfl,
  show -(m + 1 : ℤ) + 1 = -m by omega, preNormEDS_neg, even_neg, Int.even_add_one, ite_not,
  h m]

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

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

Tactic:
rfl

Result:
no goals

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

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 + 1) =
    (preNormEDS b c d (↑0 + 2) * preNormEDS b c d ↑0 ^ 3 * if Even ↑0 then b else 1) -
      preNormEDS b c d (↑0 - 1) * preNormEDS b c d (↑0 + 1) ^ 3 * if Even ↑0 then 1 else b

case nat.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) + 2) * preNormEDS b c d ↑(0 + 1) ^ 3 * if Even ↑(0 + 1) then b else 1) -
      preNormEDS b c d (↑(0 + 1) - 1) * preNormEDS b c d (↑(0 + 1) + 1) ^ 3 * if Even ↑(0 + 1) then 1 else b

case nat.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) + 2) * preNormEDS b c d ↑(m + 1 + 1) ^ 3 * if Even ↑(m + 1 + 1) then b else 1) -
      preNormEDS b c d (↑(m + 1 + 1) - 1) * preNormEDS b c d (↑(m + 1 + 1) + 1) ^ 3 * if Even ↑(m + 1 + 1) then 1 else b