awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
⊢ preNormEDS' b c d 0 = 0
have rw : Eq.{u + 1} (α := R) 0 0
Tactic: rw [preNormEDS']
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
⊢ preNormEDS' b c d 1 = 1
have rw : Eq.{u + 1} (α := R) 1 1
Tactic: rw [preNormEDS']
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
⊢ preNormEDS' b c d 2 = 1
have rw : Eq.{u + 1} (α := R) 1 1
Tactic: rw [preNormEDS']
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
⊢ preNormEDS' b c d 3 = c
have rw : c = c
Tactic: rw [preNormEDS']
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
⊢ preNormEDS' b c d 4 = d
have rw : d = d
Tactic: rw [preNormEDS']
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
m : ℕ
⊢ 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
have rw : (have this := sorry;
  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: rw [show 2 * (m + 3) = 2 * m + 1 + 5 by rfl, preNormEDS', dif_neg m.not_even_two_mul_add_one]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
m : ℕ
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
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
⊢ 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
have 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 := sorry;
    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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
n : ℕ
⊢ preNormEDS b c d (↑n : ℤ) = preNormEDS' b c d n
have pos : ∀ (hn : n = 0), preNormEDS b c d (↑n : ℤ) = preNormEDS' b c d n
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
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
⊢ preNormEDS b c d (↑n : ℤ) = preNormEDS' b c d n
have neg : ∀ (hn : ¬n = 0), preNormEDS b c d (↑n : ℤ) = preNormEDS' b c d n
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
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
have 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
Tactic: rcases m with _ | _ | _ | m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
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
⊢ 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
have 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
Tactic: rcases m with _ | _ | _ | m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
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
⊢ 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
have 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
Tactic: rcases m with _ | _ | _ | m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
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
⊢ 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
have 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
Tactic: rcases m with _ | _ | _ | m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
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
have 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
Tactic: simp_rw [Nat.cast_succ, Int.add_sub_cancel, show (m : ℤ) + 1 + 1 + 1 = m + 1 + 2 by rfl,
      Int.add_sub_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
m : ℕ
⊢ 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
have 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
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
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 : ℕ
⊢ 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
have 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
Tactic: simp_rw [mul_neg, ← sub_neg_eq_add, ← neg_sub', ← neg_add', preNormEDS_neg, ih]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
m : ℤ
⊢ 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
have 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
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
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
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
⊢ 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
have 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
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
Cleared hypotheses: m