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
m : ℕ
⊢ 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
have 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
Tactic: rcases m with _ | _ | _
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 : ℤ) + 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
⊢ 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
have 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
Tactic: rcases m with _ | _ | _
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 : ℤ) + 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
⊢ 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
have 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
Tactic: rcases m with _ | _ | _
Cleared hypotheses: m
-- 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 (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
have 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
Tactic: simp_rw [Nat.cast_succ, Int.add_sub_cancel, Int.even_add_one, not_not, Int.even_coe_nat]
-- 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 (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
have nat : preNormEDS b c d (↑(2 * (n + 1 + 1) + 1) : ℤ) =
  (preNormEDS b c d (↑(n + 1 + 1 + 2) : ℤ) * HPow.hPow (β := ℕ) (preNormEDS b c d (↑(n + 1 + 1) : ℤ)) 3 *
      if Even n then b else 1) -
    preNormEDS b c d (↑(n + 1) : ℤ) * HPow.hPow (β := ℕ) (preNormEDS b c d (↑(n + 1 + 1 + 1) : ℤ)) 3 *
      if Even n then 1 else b
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 : ℤ) + 1) =
      (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) * HPow.hPow (β := ℕ) (preNormEDS b c d (↑n : ℤ)) 3 *
          if Even (α := ℤ) (↑n : ℤ) then b else 1) -
        preNormEDS b c d (HSub.hSub (α := ℤ) (↑n : ℤ) 1) *
            HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) 3 *
          if Even (α := ℤ) (↑n : ℤ) then 1 else b
m : ℕ
⊢ 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
have neg : 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: 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
ih :
  ∀ (n : ℕ),
    preNormEDS b c d (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 1) =
      (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) * HPow.hPow (β := ℕ) (preNormEDS b c d (↑n : ℤ)) 3 *
          if Even (α := ℤ) (↑n : ℤ) then b else 1) -
        preNormEDS b c d (HSub.hSub (α := ℤ) (↑n : ℤ) 1) *
            HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) 3 *
          if Even (α := ℤ) (↑n : ℤ) then 1 else b
m : ℕ
neg :
  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
⊢ 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
have neg₁ : ∀ (m : ℕ),
  preNormEDS b c d (HMul.hMul (α := ℤ) 2 (-(↑(m + 1) : ℤ)) + 1) =
    (preNormEDS b c d (HAdd.hAdd (α := ℤ) (-(↑(m + 1) : ℤ)) 2) *
          HPow.hPow (β := ℕ) (preNormEDS b c d (-(↑(m + 1) : ℤ))) 3 *
        if Even (α := ℤ) (-(↑(m + 1) : ℤ)) then b else 1) -
      preNormEDS b c d (HSub.hSub (α := ℤ) (-(↑(m + 1) : ℤ)) 1) *
          HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (-(↑(m + 1) : ℤ)) 1)) 3 *
        if Even (α := ℤ) (-(↑(m + 1) : ℤ)) then 1 else b
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
ih :
  ∀ (n : ℕ),
    preNormEDS b c d (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 1) =
      (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) * HPow.hPow (β := ℕ) (preNormEDS b c d (↑n : ℤ)) 3 *
          if Even (α := ℤ) (↑n : ℤ) then b else 1) -
        preNormEDS b c d (HSub.hSub (α := ℤ) (↑n : ℤ) 1) *
            HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) 3 *
          if Even (α := ℤ) (↑n : ℤ) then 1 else b
m : ℕ
⊢ preNormEDS b c d (HMul.hMul (α := ℤ) 2 (-(↑(m + 1) : ℤ)) + 1) =
    (preNormEDS b c d (HAdd.hAdd (α := ℤ) (-(↑(m + 1) : ℤ)) 2) *
          HPow.hPow (β := ℕ) (preNormEDS b c d (-(↑(m + 1) : ℤ))) 3 *
        if Even (α := ℤ) (-(↑(m + 1) : ℤ)) then b else 1) -
      preNormEDS b c d (HSub.hSub (α := ℤ) (-(↑(m + 1) : ℤ)) 1) *
          HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (-(↑(m + 1) : ℤ)) 1)) 3 *
        if Even (α := ℤ) (-(↑(m + 1) : ℤ)) then 1 else b
have neg : -((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) =
  (-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) -
    -preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2) * HPow.hPow (β := ℕ) (-preNormEDS b c d (↑m : ℤ)) 3 *
      if Even (α := ℤ) (↑m : ℤ) then b else 1
Tactic: simp_rw [Nat.cast_succ, show 2 * -(m + 1 : ℤ) + 1 = -(2 * m + 1) by rfl,
      show -(m + 1 : ℤ) + 2 = -(m - 1) by ring1, show -(m + 1 : ℤ) - 1 = -(m + 2) by rfl,
      show -(m + 1 : ℤ) + 1 = -m by ring1, preNormEDS_neg, even_neg, Int.even_add_one, ite_not, 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 + 1) =
    (preNormEDS b c d (m + 2) * HPow.hPow (β := ℕ) (preNormEDS b c d m) 3 * if Even m then b else 1) -
      preNormEDS b c d (m - 1) * HPow.hPow (β := ℕ) (preNormEDS b c d (m + 1)) 3 * if Even m then 1 else b
have nat : ∀ (m : ℕ),
  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: induction m using Int.negInduction with
  | nat m =>
    rcases m with _ | _ | _
    iterate 2 simp
    simp_rw [Nat.cast_succ, Int.add_sub_cancel, Int.even_add_one, not_not, Int.even_coe_nat]
    norm_cast
    simpa only [preNormEDS_ofNat] using preNormEDS'_odd ..
  | neg ih m =>
    rcases m with _ | m
    · simp
    simp_rw [Nat.cast_succ, show 2 * -(m + 1 : ℤ) + 1 = -(2 * m + 1) by rfl,
      show -(m + 1 : ℤ) + 2 = -(m - 1) by ring1, show -(m + 1 : ℤ) - 1 = -(m + 2) by rfl,
      show -(m + 1 : ℤ) + 1 = -m by ring1, preNormEDS_neg, even_neg, Int.even_add_one, ite_not, 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 : ℤ) + 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
⊢ preNormEDS b c d (2 * m + 1) =
    (preNormEDS b c d (m + 2) * HPow.hPow (β := ℕ) (preNormEDS b c d m) 3 * if Even m then b else 1) -
      preNormEDS b c d (m - 1) * HPow.hPow (β := ℕ) (preNormEDS b c d (m + 1)) 3 * if Even m then 1 else b
have neg : ∀
  (ih :
    ∀ (n : ℕ),
      preNormEDS b c d (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 1) =
        (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) * HPow.hPow (β := ℕ) (preNormEDS b c d (↑n : ℤ)) 3 *
            if Even (α := ℤ) (↑n : ℤ) then b else 1) -
          preNormEDS b c d (HSub.hSub (α := ℤ) (↑n : ℤ) 1) *
              HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) 3 *
            if Even (α := ℤ) (↑n : ℤ) then 1 else b)
  (m : ℕ),
  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: induction m using Int.negInduction with
  | nat m =>
    rcases m with _ | _ | _
    iterate 2 simp
    simp_rw [Nat.cast_succ, Int.add_sub_cancel, Int.even_add_one, not_not, Int.even_coe_nat]
    norm_cast
    simpa only [preNormEDS_ofNat] using preNormEDS'_odd ..
  | neg ih m =>
    rcases m with _ | m
    · simp
    simp_rw [Nat.cast_succ, show 2 * -(m + 1 : ℤ) + 1 = -(2 * m + 1) by rfl,
      show -(m + 1 : ℤ) + 2 = -(m - 1) by ring1, show -(m + 1 : ℤ) - 1 = -(m + 2) by rfl,
      show -(m + 1 : ℤ) + 1 = -m by ring1, preNormEDS_neg, even_neg, Int.even_add_one, ite_not, 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
k : ℤ
⊢ complEDS₂ b c d (-k) = complEDS₂ b c d k
have simp_rw : ((HPow.hPow (β := ℕ) (-preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - -1)) 2 *
        -preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - 2) -
      -preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - -2) *
        HPow.hPow (β := ℕ) (-preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - 1)) 2) *
    if Even k then 1 else b) =
  (HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - 1)) 2 *
        preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - -2) -
      preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - 2) *
        HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - -1)) 2) *
    if Even k then 1 else b
Tactic: simp_rw [complEDS₂, ← neg_add', ← sub_neg_eq_add, ← neg_sub', preNormEDS_neg, even_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
⊢ preNormEDS (HPow.hPow (β := ℕ) b 4) c d k * complEDS₂ b c d k =
    preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * if Even k then 1 else b
have rw : preNormEDS (HPow.hPow (β := ℕ) b 4) c d k *
    ((HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - 1)) 2 *
          preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k + 2) -
        preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - 2) *
          HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k + 1)) 2) *
      if Even k then 1 else b) =
  (HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - 1)) 2 * preNormEDS (HPow.hPow (β := ℕ) b 4) c d k *
        preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k + 2) -
      preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - 2) * preNormEDS (HPow.hPow (β := ℕ) b 4) c d k *
        HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k + 1)) 2) *
    if Even k then 1 else b
Tactic: rw [complEDS₂, preNormEDS_even]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
n : ℤ
⊢ normEDS b c d (-n) = -normEDS b c d n
have simp_rw : (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (-n) * if Even (-n) then b else 1) =
  -(preNormEDS (HPow.hPow (β := ℕ) b 4) c d n * if Even n then b else 1)
Tactic: simp_rw [normEDS, preNormEDS_neg, even_neg, neg_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
n : ℤ
simp_rw :
  (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (-n) * if Even (-n) then b else 1) =
    -(preNormEDS (HPow.hPow (β := ℕ) b 4) c d n * if Even n then b else 1)
⊢ normEDS b c d (-n) = -normEDS b c d n
have simp_rw₁ : (-preNormEDS (HPow.hPow (β := ℕ) b 4) c d n * if Even (-n) then b else 1) =
  -(preNormEDS (HPow.hPow (β := ℕ) b 4) c d n * if Even n then b else 1)
Tactic: simp_rw [normEDS, preNormEDS_neg, even_neg, neg_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
n : ℤ
simp_rw :
  (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (-n) * if Even (-n) then b else 1) =
    -(preNormEDS (HPow.hPow (β := ℕ) b 4) c d n * if Even n then b else 1)
simp_rw₁ :
  (-preNormEDS (HPow.hPow (β := ℕ) b 4) c d n * if Even (-n) then b else 1) =
    -(preNormEDS (HPow.hPow (β := ℕ) b 4) c d n * if Even n then b else 1)
⊢ normEDS b c d (-n) = -normEDS b c d n
have simp_rw₂ : (-preNormEDS (HPow.hPow (β := ℕ) b 4) c d n * if Even n then b else 1) =
  -(preNormEDS (HPow.hPow (β := ℕ) b 4) c d n * if Even n then b else 1)
Tactic: simp_rw [normEDS, preNormEDS_neg, even_neg, neg_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
⊢ normEDS b c d k * complEDS₂ b c d k = normEDS b c d (2 * k)
have simp_rw : (preNormEDS (HPow.hPow (β := ℕ) b 4) c d k * if Even k then b else 1) * complEDS₂ b c d k =
  preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * if Even (2 * k) then b else 1
Tactic: simp_rw [normEDS, mul_right_comm, preNormEDS_mul_complEDS₂, mul_assoc, apply_ite₂, one_mul,
    mul_one, ite_self, if_pos <| even_two_mul k]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
simp_rw :
  (preNormEDS (HPow.hPow (β := ℕ) b 4) c d k * if Even k then b else 1) * complEDS₂ b c d k =
    preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * if Even (2 * k) then b else 1
⊢ normEDS b c d k * complEDS₂ b c d k = normEDS b c d (2 * k)
have simp_rw₁ : (preNormEDS (HPow.hPow (β := ℕ) b 4) c d k * complEDS₂ b c d k * if Even k then b else 1) =
  preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * if Even (2 * k) then b else 1
Tactic: simp_rw [normEDS, mul_right_comm, preNormEDS_mul_complEDS₂, mul_assoc, apply_ite₂, one_mul,
    mul_one, ite_self, if_pos <| even_two_mul k]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
simp_rw :
  (preNormEDS (HPow.hPow (β := ℕ) b 4) c d k * if Even k then b else 1) * complEDS₂ b c d k =
    preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * if Even (2 * k) then b else 1
simp_rw₁ :
  (preNormEDS (HPow.hPow (β := ℕ) b 4) c d k * complEDS₂ b c d k * if Even k then b else 1) =
    preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * if Even (2 * k) then b else 1
⊢ normEDS b c d k * complEDS₂ b c d k = normEDS b c d (2 * k)
have simp_rw₂ : ((preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * if Even k then 1 else b) * if Even k then b else 1) =
  preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * if Even (2 * k) then b else 1
Tactic: simp_rw [normEDS, mul_right_comm, preNormEDS_mul_complEDS₂, mul_assoc, apply_ite₂, one_mul,
    mul_one, ite_self, if_pos <| even_two_mul k]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
simp_rw :
  (preNormEDS (HPow.hPow (β := ℕ) b 4) c d k * if Even k then b else 1) * complEDS₂ b c d k =
    preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * if Even (2 * k) then b else 1
simp_rw₁ :
  (preNormEDS (HPow.hPow (β := ℕ) b 4) c d k * complEDS₂ b c d k * if Even k then b else 1) =
    preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * if Even (2 * k) then b else 1
simp_rw₂ :
  ((preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * if Even k then 1 else b) * if Even k then b else 1) =
    preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * if Even (2 * k) then b else 1
⊢ normEDS b c d k * complEDS₂ b c d k = normEDS b c d (2 * k)
have simp_rw₃ : preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * ((if Even k then 1 else b) * if Even k then b else 1) =
  preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * if Even (2 * k) then b else 1
Tactic: simp_rw [normEDS, mul_right_comm, preNormEDS_mul_complEDS₂, mul_assoc, apply_ite₂, one_mul,
    mul_one, ite_self, if_pos <| even_two_mul k]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
simp_rw :
  (preNormEDS (HPow.hPow (β := ℕ) b 4) c d k * if Even k then b else 1) * complEDS₂ b c d k =
    preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * if Even (2 * k) then b else 1
simp_rw₁ :
  (preNormEDS (HPow.hPow (β := ℕ) b 4) c d k * complEDS₂ b c d k * if Even k then b else 1) =
    preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * if Even (2 * k) then b else 1
simp_rw₂ :
  ((preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * if Even k then 1 else b) * if Even k then b else 1) =
    preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * if Even (2 * k) then b else 1
simp_rw₃ :
  preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * ((if Even k then 1 else b) * if Even k then b else 1) =
    preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * if Even (2 * k) then b else 1
⊢ normEDS b c d k * complEDS₂ b c d k = normEDS b c d (2 * k)
have simp_rw₄ : (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * if Even k then 1 * b else b * 1) =
  preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * if Even (2 * k) then b else 1
Tactic: simp_rw [normEDS, mul_right_comm, preNormEDS_mul_complEDS₂, mul_assoc, apply_ite₂, one_mul,
    mul_one, ite_self, if_pos <| even_two_mul k]