awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
m : ℕ
rw :
  (have this := ⋯;
    HPow.hPow (β := ℕ) (preNormEDS' b c d ((2 * m + 1) / 2 + 2)) 2 * preNormEDS' b c d ((2 * m + 1) / 2 + 3) *
        preNormEDS' b c d ((2 * m + 1) / 2 + 5) -
      preNormEDS' b c d ((2 * m + 1) / 2 + 1) * preNormEDS' b c d ((2 * m + 1) / 2 + 3) *
        HPow.hPow (β := ℕ) (preNormEDS' b c d ((2 * m + 1) / 2 + 4)) 2) =
    HPow.hPow (β := ℕ) (preNormEDS' b c d (m + 2)) 2 * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 5) -
      preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) * HPow.hPow (β := ℕ) (preNormEDS' b c d (m + 4)) 2
⊢ preNormEDS' b c d (2 * (m + 3)) =
    HPow.hPow (β := ℕ) (preNormEDS' b c d (m + 2)) 2 * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 5) -
      preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) * HPow.hPow (β := ℕ) (preNormEDS' b c d (m + 4)) 2

Tactic:
rw [show 2 * (m + 3) = 2 * m + 1 + 5 by rfl, preNormEDS', dif_neg m.not_even_two_mul_add_one]

Premises used: dif_neg, Nat.not_even_two_mul_add_one, preNormEDS'
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
m : ℕ
⊢ (have this := ⋯;
    HPow.hPow (β := ℕ) (preNormEDS' b c d ((2 * m + 1) / 2 + 2)) 2 * preNormEDS' b c d ((2 * m + 1) / 2 + 3) *
        preNormEDS' b c d ((2 * m + 1) / 2 + 5) -
      preNormEDS' b c d ((2 * m + 1) / 2 + 1) * preNormEDS' b c d ((2 * m + 1) / 2 + 3) *
        HPow.hPow (β := ℕ) (preNormEDS' b c d ((2 * m + 1) / 2 + 4)) 2) =
    HPow.hPow (β := ℕ) (preNormEDS' b c d (m + 2)) 2 * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 5) -
      preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) * HPow.hPow (β := ℕ) (preNormEDS' b c d (m + 4)) 2

Tactic:
simp [Nat.mul_add_div two_pos]

Premises used: Nat.mul_add_div, two_pos
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
m : ℕ
⊢ 2 * (m + 2) + 1 = 2 * m + 5

Tactic:
rfl
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
m : ℕ
rw :
  preNormEDS' b c d (2 * m + 5) =
    (preNormEDS' b c d (m + 4) * HPow.hPow (β := ℕ) (preNormEDS' b c d (m + 2)) 3 * if Even m then b else 1) -
      preNormEDS' b c d (m + 1) * HPow.hPow (β := ℕ) (preNormEDS' b c d (m + 3)) 3 * if Even m then 1 else b
rw₁ :
  (if hn : Even (2 * m) then
      (preNormEDS' b c d (2 * m / 2 + 4) * HPow.hPow (β := ℕ) (preNormEDS' b c d (2 * m / 2 + 2)) 3 *
          if Even (2 * m / 2) then b else 1) -
        preNormEDS' b c d (2 * m / 2 + 1) * HPow.hPow (β := ℕ) (preNormEDS' b c d (2 * m / 2 + 3)) 3 *
          if Even (2 * m / 2) then 1 else b
    else
      have this := ⋯;
      HPow.hPow (β := ℕ) (preNormEDS' b c d (2 * m / 2 + 2)) 2 * preNormEDS' b c d (2 * m / 2 + 3) *
          preNormEDS' b c d (2 * m / 2 + 5) -
        preNormEDS' b c d (2 * m / 2 + 1) * preNormEDS' b c d (2 * m / 2 + 3) *
          HPow.hPow (β := ℕ) (preNormEDS' b c d (2 * m / 2 + 4)) 2) =
    (preNormEDS' b c d (m + 4) * HPow.hPow (β := ℕ) (preNormEDS' b c d (m + 2)) 3 * if Even m then b else 1) -
      preNormEDS' b c d (m + 1) * HPow.hPow (β := ℕ) (preNormEDS' b c d (m + 3)) 3 * if Even m then 1 else b
rw₂ :
  ((preNormEDS' b c d (2 * m / 2 + 4) * HPow.hPow (β := ℕ) (preNormEDS' b c d (2 * m / 2 + 2)) 3 *
        if Even (2 * m / 2) then b else 1) -
      preNormEDS' b c d (2 * m / 2 + 1) * HPow.hPow (β := ℕ) (preNormEDS' b c d (2 * m / 2 + 3)) 3 *
        if Even (2 * m / 2) then 1 else b) =
    (preNormEDS' b c d (m + 4) * HPow.hPow (β := ℕ) (preNormEDS' b c d (m + 2)) 3 * if Even m then b else 1) -
      preNormEDS' b c d (m + 1) * HPow.hPow (β := ℕ) (preNormEDS' b c d (m + 3)) 3 * if Even m then 1 else b
rw₃ rw₄ :
  ((preNormEDS' b c d (m + 4) * HPow.hPow (β := ℕ) (preNormEDS' b c d (m + 2)) 3 * if Even m then b else 1) -
      preNormEDS' b c d (m + 1) * HPow.hPow (β := ℕ) (preNormEDS' b c d (m + 3)) 3 * if Even m then 1 else b) =
    (preNormEDS' b c d (m + 4) * HPow.hPow (β := ℕ) (preNormEDS' b c d (m + 2)) 3 * if Even m then b else 1) -
      preNormEDS' b c d (m + 1) * HPow.hPow (β := ℕ) (preNormEDS' b c d (m + 3)) 3 * if Even m then 1 else b
⊢ preNormEDS' b c d (2 * (m + 2) + 1) =
    (preNormEDS' b c d (m + 4) * HPow.hPow (β := ℕ) (preNormEDS' b c d (m + 2)) 3 * if Even m then b else 1) -
      preNormEDS' b c d (m + 1) * HPow.hPow (β := ℕ) (preNormEDS' b c d (m + 3)) 3 * if Even m then 1 else b

Tactic:
rw [show 2 * (m + 2) + 1 = 2 * m + 5 by rfl, preNormEDS', dif_pos <| even_two_mul m,
    m.mul_div_cancel_left two_pos]

Premises used: Nat.mul_div_cancel_left, two_pos, dif_pos, even_two_mul, preNormEDS'
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
n : ℕ
pos : ∀ (hn : n = 0), preNormEDS b c d (↑n : ℤ) = preNormEDS' b c d n
neg : ∀ (hn : ¬n = 0), preNormEDS b c d (↑n : ℤ) = preNormEDS' b c d n
⊢ preNormEDS b c d (↑n : ℤ) = preNormEDS' b c d n

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
n : ℕ
hn : n = 0
⊢ preNormEDS b c d (↑n : ℤ) = preNormEDS' b c d n

Tactic:
simp [hn, preNormEDS]

Premises used: preNormEDS
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
n : ℕ
hn : ¬n = 0
⊢ preNormEDS b c d (↑n : ℤ) = preNormEDS' b c d n

Tactic:
simp [preNormEDS, Int.sign_natCast_of_ne_zero hn]

Premises used: Int.sign_natCast_of_ne_zero, preNormEDS
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
⊢ preNormEDS b c d 0 = 0

Tactic:
simp [preNormEDS]

Premises used: preNormEDS
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
⊢ preNormEDS b c d 1 = 1

Tactic:
simp [preNormEDS]

Premises used: preNormEDS
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
⊢ preNormEDS b c d 2 = 1

Tactic:
simp [preNormEDS, Int.sign_eq_one_of_pos]

Premises used: Int.sign_eq_one_of_pos, preNormEDS
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
⊢ preNormEDS b c d 3 = c

Tactic:
simp [preNormEDS, Int.sign_eq_one_of_pos]

Premises used: Int.sign_eq_one_of_pos, preNormEDS
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
⊢ preNormEDS b c d 4 = d

Tactic:
simp [preNormEDS, Int.sign_eq_one_of_pos]

Premises used: Int.sign_eq_one_of_pos, preNormEDS
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
n : ℤ
⊢ preNormEDS b c d (-n) = -preNormEDS b c d n

Tactic:
simp [preNormEDS]

Premises used: preNormEDS
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
m : ℕ
nat :
  preNormEDS b c d (HMul.hMul (α := ℤ) 2 (↑0 : ℤ)) =
    HPow.hPow (β := ℕ) (preNormEDS b c d (HSub.hSub (α := ℤ) (↑0 : ℤ) 1)) 2 * preNormEDS b c d (↑0 : ℤ) *
        preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 2) -
      preNormEDS b c d (HSub.hSub (α := ℤ) (↑0 : ℤ) 2) * preNormEDS b c d (↑0 : ℤ) *
        HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1)) 2
nat₁ :
  preNormEDS b c d (HMul.hMul (α := ℤ) 2 (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ)) =
    HPow.hPow (β := ℕ) (preNormEDS b c d (HSub.hSub (α := ℤ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ) 1)) 2 *
          preNormEDS b c d (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ) *
        preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ) 2) -
      preNormEDS b c d (HSub.hSub (α := ℤ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ) 2) *
          preNormEDS b c d (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ) *
        HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ) 1)) 2
nat₂ :
  preNormEDS b c d (HMul.hMul (α := ℤ) 2 (↑(HAdd.hAdd (α := ℕ) 0 1 + 1) : ℤ)) =
    HPow.hPow (β := ℕ) (preNormEDS b c d (HSub.hSub (α := ℤ) (↑(HAdd.hAdd (α := ℕ) 0 1 + 1) : ℤ) 1)) 2 *
          preNormEDS b c d (↑(HAdd.hAdd (α := ℕ) 0 1 + 1) : ℤ) *
        preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑(HAdd.hAdd (α := ℕ) 0 1 + 1) : ℤ) 2) -
      preNormEDS b c d (HSub.hSub (α := ℤ) (↑(HAdd.hAdd (α := ℕ) 0 1 + 1) : ℤ) 2) *
          preNormEDS b c d (↑(HAdd.hAdd (α := ℕ) 0 1 + 1) : ℤ) *
        HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑(HAdd.hAdd (α := ℕ) 0 1 + 1) : ℤ) 1)) 2
nat₃ :
  ∀ (m : ℕ),
    preNormEDS b c d (HMul.hMul (α := ℤ) 2 (↑(m + 1 + 1 + 1) : ℤ)) =
      HPow.hPow (β := ℕ) (preNormEDS b c d (HSub.hSub (α := ℤ) (↑(m + 1 + 1 + 1) : ℤ) 1)) 2 *
            preNormEDS b c d (↑(m + 1 + 1 + 1) : ℤ) *
          preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑(m + 1 + 1 + 1) : ℤ) 2) -
        preNormEDS b c d (HSub.hSub (α := ℤ) (↑(m + 1 + 1 + 1) : ℤ) 2) * preNormEDS b c d (↑(m + 1 + 1 + 1) : ℤ) *
          HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑(m + 1 + 1 + 1) : ℤ) 1)) 2
⊢ preNormEDS b c d (HMul.hMul (α := ℤ) 2 (↑m : ℤ)) =
    HPow.hPow (β := ℕ) (preNormEDS b c d (HSub.hSub (α := ℤ) (↑m : ℤ) 1)) 2 * preNormEDS b c d (↑m : ℤ) *
        preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2) -
      preNormEDS b c d (HSub.hSub (α := ℤ) (↑m : ℤ) 2) * preNormEDS b c d (↑m : ℤ) *
        HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) 2

Tactic:
rcases m with _ | _ | _ | m
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
⊢ preNormEDS b c d (HMul.hMul (α := ℤ) 2 (↑0 : ℤ)) =
    HPow.hPow (β := ℕ) (preNormEDS b c d (HSub.hSub (α := ℤ) (↑0 : ℤ) 1)) 2 * preNormEDS b c d (↑0 : ℤ) *
        preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 2) -
      preNormEDS b c d (HSub.hSub (α := ℤ) (↑0 : ℤ) 2) * preNormEDS b c d (↑0 : ℤ) *
        HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1)) 2

Tactic:
simp
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
⊢ preNormEDS b c d (HMul.hMul (α := ℤ) 2 (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ)) =
    HPow.hPow (β := ℕ) (preNormEDS b c d (HSub.hSub (α := ℤ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ) 1)) 2 *
          preNormEDS b c d (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ) *
        preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ) 2) -
      preNormEDS b c d (HSub.hSub (α := ℤ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ) 2) *
          preNormEDS b c d (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ) *
        HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ) 1)) 2

Tactic:
simp
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
⊢ preNormEDS b c d (HMul.hMul (α := ℤ) 2 (↑(HAdd.hAdd (α := ℕ) 0 1 + 1) : ℤ)) =
    HPow.hPow (β := ℕ) (preNormEDS b c d (HSub.hSub (α := ℤ) (↑(HAdd.hAdd (α := ℕ) 0 1 + 1) : ℤ) 1)) 2 *
          preNormEDS b c d (↑(HAdd.hAdd (α := ℕ) 0 1 + 1) : ℤ) *
        preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑(HAdd.hAdd (α := ℕ) 0 1 + 1) : ℤ) 2) -
      preNormEDS b c d (HSub.hSub (α := ℤ) (↑(HAdd.hAdd (α := ℕ) 0 1 + 1) : ℤ) 2) *
          preNormEDS b c d (↑(HAdd.hAdd (α := ℕ) 0 1 + 1) : ℤ) *
        HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑(HAdd.hAdd (α := ℕ) 0 1 + 1) : ℤ) 1)) 2

Tactic:
simp
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
m : ℕ
⊢ HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 + 1 + 1 = HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 + 2

Tactic:
rfl
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
m : ℕ
nat :
  preNormEDS b c d (2 * (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 + 2)) =
    HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 + 1)) 2 *
          preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 + 2) *
        preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 + 2 + 2) -
      preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) * preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 + 2) *
        HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 + 2 + 1)) 2
⊢ preNormEDS b c d (HMul.hMul (α := ℤ) 2 (↑(m + 1 + 1 + 1) : ℤ)) =
    HPow.hPow (β := ℕ) (preNormEDS b c d (HSub.hSub (α := ℤ) (↑(m + 1 + 1 + 1) : ℤ) 1)) 2 *
          preNormEDS b c d (↑(m + 1 + 1 + 1) : ℤ) *
        preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑(m + 1 + 1 + 1) : ℤ) 2) -
      preNormEDS b c d (HSub.hSub (α := ℤ) (↑(m + 1 + 1 + 1) : ℤ) 2) * preNormEDS b c d (↑(m + 1 + 1 + 1) : ℤ) *
        HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑(m + 1 + 1 + 1) : ℤ) 1)) 2

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

Premises used: Nat.cast_succ, Int.add_sub_cancel
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
m : ℕ
nat :
  preNormEDS b c d (↑(2 * (m + 1 + 2)) : ℤ) =
    HPow.hPow (β := ℕ) (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) : ℤ) *
        HPow.hPow (β := ℕ) (preNormEDS b c d (↑(m + 1 + 2 + 1) : ℤ)) 2
⊢ preNormEDS b c d (2 * (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 + 2)) =
    HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 + 1)) 2 *
          preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 + 2) *
        preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 + 2 + 2) -
      preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) * preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 + 2) *
        HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 + 2 + 1)) 2

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS b c d (↑(2 * (m + 1 + 2)) : ℤ) =
    HPow.hPow (β := ℕ) (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) : ℤ) *
        HPow.hPow (β := ℕ) (preNormEDS b c d (↑(m + 1 + 2 + 1) : ℤ)) 2

Tactic:
simpa only [preNormEDS_ofNat] using preNormEDS'_even ..

Premises used: preNormEDS_ofNat, preNormEDS'_even
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
ih :
  ∀ (n : ℕ),
    preNormEDS b c d (HMul.hMul (α := ℤ) 2 (↑n : ℤ)) =
      HPow.hPow (β := ℕ) (preNormEDS b c d (HSub.hSub (α := ℤ) (↑n : ℤ) 1)) 2 * preNormEDS b c d (↑n : ℤ) *
          preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) -
        preNormEDS b c d (HSub.hSub (α := ℤ) (↑n : ℤ) 2) * preNormEDS b c d (↑n : ℤ) *
          HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) 2
m : ℕ
neg :
  -(HPow.hPow (β := ℕ) (preNormEDS b c d (HSub.hSub (α := ℤ) (↑m : ℤ) 1)) 2 * preNormEDS b c d (↑m : ℤ) *
          preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2) -
        preNormEDS b c d (HSub.hSub (α := ℤ) (↑m : ℤ) 2) * preNormEDS b c d (↑m : ℤ) *
          HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) 2) =
    HPow.hPow (β := ℕ) (-preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) 2 * -preNormEDS b c d (↑m : ℤ) *
        -preNormEDS b c d (HSub.hSub (α := ℤ) (↑m : ℤ) 2) -
      -preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2) * -preNormEDS b c d (↑m : ℤ) *
        HPow.hPow (β := ℕ) (-preNormEDS b c d (HSub.hSub (α := ℤ) (↑m : ℤ) 1)) 2
⊢ preNormEDS b c d (HMul.hMul (α := ℤ) 2 (-(↑m : ℤ))) =
    HPow.hPow (β := ℕ) (preNormEDS b c d (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) 2 * preNormEDS b c d (-(↑m : ℤ)) *
        preNormEDS b c d (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 2) -
      preNormEDS b c d (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 2) * preNormEDS b c d (-(↑m : ℤ)) *
        HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1)) 2

Tactic:
simp_rw [mul_neg, ← sub_neg_eq_add, ← neg_sub', ← neg_add', preNormEDS_neg, ih]

Premises used: preNormEDS_neg, neg_add', neg_sub', sub_neg_eq_add, mul_neg
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
ih :
  ∀ (n : ℕ),
    preNormEDS b c d (HMul.hMul (α := ℤ) 2 (↑n : ℤ)) =
      HPow.hPow (β := ℕ) (preNormEDS b c d (HSub.hSub (α := ℤ) (↑n : ℤ) 1)) 2 * preNormEDS b c d (↑n : ℤ) *
          preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) -
        preNormEDS b c d (HSub.hSub (α := ℤ) (↑n : ℤ) 2) * preNormEDS b c d (↑n : ℤ) *
          HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) 2
m : ℕ
⊢ -(HPow.hPow (β := ℕ) (preNormEDS b c d (HSub.hSub (α := ℤ) (↑m : ℤ) 1)) 2 * preNormEDS b c d (↑m : ℤ) *
          preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2) -
        preNormEDS b c d (HSub.hSub (α := ℤ) (↑m : ℤ) 2) * preNormEDS b c d (↑m : ℤ) *
          HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) 2) =
    HPow.hPow (β := ℕ) (-preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) 2 * -preNormEDS b c d (↑m : ℤ) *
        -preNormEDS b c d (HSub.hSub (α := ℤ) (↑m : ℤ) 2) -
      -preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2) * -preNormEDS b c d (↑m : ℤ) *
        HPow.hPow (β := ℕ) (-preNormEDS b c d (HSub.hSub (α := ℤ) (↑m : ℤ) 1)) 2

Tactic:
ring1
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
m : ℤ
nat :
  ∀ (m : ℕ),
    preNormEDS b c d (HMul.hMul (α := ℤ) 2 (↑m : ℤ)) =
      HPow.hPow (β := ℕ) (preNormEDS b c d (HSub.hSub (α := ℤ) (↑m : ℤ) 1)) 2 * preNormEDS b c d (↑m : ℤ) *
          preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2) -
        preNormEDS b c d (HSub.hSub (α := ℤ) (↑m : ℤ) 2) * preNormEDS b c d (↑m : ℤ) *
          HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) 2
neg :
  ∀
    (ih :
      ∀ (n : ℕ),
        preNormEDS b c d (HMul.hMul (α := ℤ) 2 (↑n : ℤ)) =
          HPow.hPow (β := ℕ) (preNormEDS b c d (HSub.hSub (α := ℤ) (↑n : ℤ) 1)) 2 * preNormEDS b c d (↑n : ℤ) *
              preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) -
            preNormEDS b c d (HSub.hSub (α := ℤ) (↑n : ℤ) 2) * preNormEDS b c d (↑n : ℤ) *
              HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) 2)
    (m : ℕ),
    preNormEDS b c d (HMul.hMul (α := ℤ) 2 (-(↑m : ℤ))) =
      HPow.hPow (β := ℕ) (preNormEDS b c d (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) 2 * preNormEDS b c d (-(↑m : ℤ)) *
          preNormEDS b c d (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 2) -
        preNormEDS b c d (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 2) * preNormEDS b c d (-(↑m : ℤ)) *
          HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1)) 2
⊢ preNormEDS b c d (2 * m) =
    HPow.hPow (β := ℕ) (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 * HPow.hPow (β := ℕ) (preNormEDS b c d (m + 1)) 2

Tactic:
induction m using Int.negInduction with
  | nat m =>
    rcases m with _ | _ | _ | m
    iterate 3 simp
    simp_rw [Nat.cast_succ, Int.add_sub_cancel, show (m : ℤ) + 1 + 1 + 1 = m + 1 + 2 by rfl,
      Int.add_sub_cancel]
    norm_cast
    simpa only [preNormEDS_ofNat] using preNormEDS'_even ..
  | neg ih m =>
    simp_rw [mul_neg, ← sub_neg_eq_add, ← neg_sub', ← neg_add', preNormEDS_neg, ih]
    ring1

Premises used: Nat.cast_succ, preNormEDS_ofNat, preNormEDS_neg, Int.add_sub_cancel, neg_add', neg_sub', preNormEDS'_even, sub_neg_eq_add, mul_neg
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
m : ℕ
nat :
  preNormEDS b c d (HMul.hMul (α := ℤ) 2 (↑0 : ℤ) + 1) =
    (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 2) * HPow.hPow (β := ℕ) (preNormEDS b c d (↑0 : ℤ)) 3 *
        if Even (α := ℤ) (↑0 : ℤ) then b else 1) -
      preNormEDS b c d (HSub.hSub (α := ℤ) (↑0 : ℤ) 1) *
          HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1)) 3 *
        if Even (α := ℤ) (↑0 : ℤ) then 1 else b
nat₁ :
  preNormEDS b c d (HMul.hMul (α := ℤ) 2 (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ) + 1) =
    (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ) 2) *
          HPow.hPow (β := ℕ) (preNormEDS b c d (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ)) 3 *
        if Even (α := ℤ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ) then b else 1) -
      preNormEDS b c d (HSub.hSub (α := ℤ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ) 1) *
          HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ) 1)) 3 *
        if Even (α := ℤ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ) then 1 else b
nat₂ :
  ∀ (n : ℕ),
    preNormEDS b c d (HMul.hMul (α := ℤ) 2 (↑(n + 1 + 1) : ℤ) + 1) =
      (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑(n + 1 + 1) : ℤ) 2) *
            HPow.hPow (β := ℕ) (preNormEDS b c d (↑(n + 1 + 1) : ℤ)) 3 *
          if Even (α := ℤ) (↑(n + 1 + 1) : ℤ) then b else 1) -
        preNormEDS b c d (HSub.hSub (α := ℤ) (↑(n + 1 + 1) : ℤ) 1) *
            HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑(n + 1 + 1) : ℤ) 1)) 3 *
          if Even (α := ℤ) (↑(n + 1 + 1) : ℤ) then 1 else b
⊢ preNormEDS b c d (HMul.hMul (α := ℤ) 2 (↑m : ℤ) + 1) =
    (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2) * HPow.hPow (β := ℕ) (preNormEDS b c d (↑m : ℤ)) 3 *
        if Even (α := ℤ) (↑m : ℤ) then b else 1) -
      preNormEDS b c d (HSub.hSub (α := ℤ) (↑m : ℤ) 1) *
          HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) 3 *
        if Even (α := ℤ) (↑m : ℤ) then 1 else b

Tactic:
rcases m with _ | _ | _
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
⊢ preNormEDS b c d (HMul.hMul (α := ℤ) 2 (↑0 : ℤ) + 1) =
    (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 2) * HPow.hPow (β := ℕ) (preNormEDS b c d (↑0 : ℤ)) 3 *
        if Even (α := ℤ) (↑0 : ℤ) then b else 1) -
      preNormEDS b c d (HSub.hSub (α := ℤ) (↑0 : ℤ) 1) *
          HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1)) 3 *
        if Even (α := ℤ) (↑0 : ℤ) then 1 else b

Tactic:
simp
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
⊢ preNormEDS b c d (HMul.hMul (α := ℤ) 2 (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ) + 1) =
    (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ) 2) *
          HPow.hPow (β := ℕ) (preNormEDS b c d (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ)) 3 *
        if Even (α := ℤ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ) then b else 1) -
      preNormEDS b c d (HSub.hSub (α := ℤ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ) 1) *
          HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ) 1)) 3 *
        if Even (α := ℤ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ) then 1 else b

Tactic:
simp
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
n : ℕ
nat :
  preNormEDS b c d (2 * (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) + 1) =
    (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1 + 2) *
          HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) 3 *
        if Even n then b else 1) -
      preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) *
          HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1 + 1)) 3 *
        if Even n then 1 else b
⊢ preNormEDS b c d (HMul.hMul (α := ℤ) 2 (↑(n + 1 + 1) : ℤ) + 1) =
    (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑(n + 1 + 1) : ℤ) 2) *
          HPow.hPow (β := ℕ) (preNormEDS b c d (↑(n + 1 + 1) : ℤ)) 3 *
        if Even (α := ℤ) (↑(n + 1 + 1) : ℤ) then b else 1) -
      preNormEDS b c d (HSub.hSub (α := ℤ) (↑(n + 1 + 1) : ℤ) 1) *
          HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑(n + 1 + 1) : ℤ) 1)) 3 *
        if Even (α := ℤ) (↑(n + 1 + 1) : ℤ) then 1 else b

Tactic:
simp_rw [Nat.cast_succ, Int.add_sub_cancel, Int.even_add_one, not_not, Int.even_coe_nat]

Premises used: Nat.cast_succ, Classical.not_not, Int.add_sub_cancel, Int.even_add_one, Int.even_coe_nat