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
P : ℕ → Sort u
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x : ℕ
ih : (k : ℕ) → k < 2 * (x + 2) + 1 → P k
a : P (x + 1)
⊢ P (2 * (x + 2) + 1)
have a₁ : P (x + 2)
Tactic: apply odd
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
P : ℕ → Sort u
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x : ℕ
ih : (k : ℕ) → k < 2 * (x + 2) + 1 → P k
a : P (x + 1)
a₁ : P (x + 2)
⊢ P (2 * (x + 2) + 1)
have a₂ : P (x + 3)
Tactic: apply odd
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
P : ℕ → Sort u
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x : ℕ
ih : (k : ℕ) → k < 2 * (x + 2) + 1 → P k
a : P (x + 1)
a₁ : P (x + 2)
a₂ : P (x + 3)
⊢ P (2 * (x + 2) + 1)
have a₃ : P (x + 4)
Tactic: apply odd
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
P : ℕ → Sort u
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x : ℕ
ih : (k : ℕ) → k < 2 * (x + 2) + 1 → P k
⊢ x + 1 < 2 * (x + 2) + 1
have linarith : 2 * (x + 2) + 1 ≤ x + 1 →
  HMul.hMul (α := ℤ) 4 (-1) + HSub.hSub (α := ℤ) 0 (↑x : ℤ) +
      (2 * HAdd.hAdd (α := ℤ) (↑x : ℤ) 2 + 1 - HAdd.hAdd (α := ℤ) (↑x : ℤ) 1) =
    0
Tactic: linarith only
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
P : ℕ → Sort u
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x : ℕ
ih : (k : ℕ) → k < 2 * (x + 2) + 1 → P k
linarith :
  2 * (x + 2) + 1 ≤ x + 1 →
    HMul.hMul (α := ℤ) 4 (-1) + HSub.hSub (α := ℤ) 0 (↑x : ℤ) +
        (2 * HAdd.hAdd (α := ℤ) (↑x : ℤ) 2 + 1 - HAdd.hAdd (α := ℤ) (↑x : ℤ) 1) =
      0
⊢ x + 1 < 2 * (x + 2) + 1
have linarith₁ : 2 * (x + 2) + 1 ≤ x + 1 → GT.gt (α := ℤ) 4 0
Tactic: linarith only
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
P : ℕ → Sort u
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x : ℕ
ih : (k : ℕ) → k < 2 * (x + 2) + 1 → P k
⊢ x + 2 < 2 * (x + 2) + 1
have linarith : 2 * (x + 2) + 1 ≤ x + 2 →
  HMul.hMul (α := ℤ) 3 (-1) + HSub.hSub (α := ℤ) 0 (↑x : ℤ) +
      (2 * HAdd.hAdd (α := ℤ) (↑x : ℤ) 2 + 1 - HAdd.hAdd (α := ℤ) (↑x : ℤ) 2) =
    0
Tactic: linarith only
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
P : ℕ → Sort u
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x : ℕ
ih : (k : ℕ) → k < 2 * (x + 2) + 1 → P k
linarith :
  2 * (x + 2) + 1 ≤ x + 2 →
    HMul.hMul (α := ℤ) 3 (-1) + HSub.hSub (α := ℤ) 0 (↑x : ℤ) +
        (2 * HAdd.hAdd (α := ℤ) (↑x : ℤ) 2 + 1 - HAdd.hAdd (α := ℤ) (↑x : ℤ) 2) =
      0
⊢ x + 2 < 2 * (x + 2) + 1
have linarith₁ : 2 * (x + 2) + 1 ≤ x + 2 → GT.gt (α := ℤ) 3 0
Tactic: linarith only
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
P : ℕ → Sort u
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x : ℕ
ih : (k : ℕ) → k < 2 * (x + 2) + 1 → P k
⊢ x + 3 < 2 * (x + 2) + 1
have linarith : 2 * (x + 2) + 1 ≤ x + 3 →
  HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) 0 (↑x : ℤ) +
      (2 * HAdd.hAdd (α := ℤ) (↑x : ℤ) 2 + 1 - HAdd.hAdd (α := ℤ) (↑x : ℤ) 3) =
    0
Tactic: linarith only
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
P : ℕ → Sort u
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x : ℕ
ih : (k : ℕ) → k < 2 * (x + 2) + 1 → P k
linarith :
  2 * (x + 2) + 1 ≤ x + 3 →
    HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) 0 (↑x : ℤ) +
        (2 * HAdd.hAdd (α := ℤ) (↑x : ℤ) 2 + 1 - HAdd.hAdd (α := ℤ) (↑x : ℤ) 3) =
      0
⊢ x + 3 < 2 * (x + 2) + 1
have linarith₁ : 2 * (x + 2) + 1 ≤ x + 3 → GT.gt (α := ℤ) 2 0
Tactic: linarith only
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
P : ℕ → Sort u
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x : ℕ
ih : (k : ℕ) → k < 2 * (x + 2) + 1 → P k
⊢ x + 4 < 2 * (x + 2) + 1
have linarith : 2 * (x + 2) + 1 ≤ x + 4 →
  -1 + HSub.hSub (α := ℤ) 0 (↑x : ℤ) + (2 * HAdd.hAdd (α := ℤ) (↑x : ℤ) 2 + 1 - HAdd.hAdd (α := ℤ) (↑x : ℤ) 4) = 0
Tactic: linarith only
-- 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 0 = 0
have rw : Eq.{u + 1} (α := R) 0 0
Tactic: rw [complEDS']
-- 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 1 = 1
have rw : Eq.{u + 1} (α := R) 1 1
Tactic: rw [complEDS']
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
m : ℕ
⊢ complEDS' b c d k (2 * (m + 1)) = complEDS' b c d k (m + 1) * complEDS₂ b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k)
have rw : complEDS' b c d k (2 * m + 2) = complEDS' b c d k (m + 1) * complEDS₂ b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k)
Tactic: rw [show 2 * (m + 1) = 2 * m + 2 by rfl, complEDS', dif_pos <| even_two_mul m,
    m.mul_div_cancel_left two_pos, Nat.cast_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
m : ℕ
rw : complEDS' b c d k (2 * m + 2) = complEDS' b c d k (m + 1) * complEDS₂ b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k)
⊢ complEDS' b c d k (2 * (m + 1)) = complEDS' b c d k (m + 1) * complEDS₂ b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k)
have rw₁ : (if hn : Even (2 * m) then complEDS' b c d k (2 * m / 2 + 1) * complEDS₂ b c d ((↑(2 * m / 2 + 1) : ℤ) * k)
  else
    have this := sorry;
    HPow.hPow (β := ℕ) (complEDS' b c d k (2 * m / 2 + 1)) 2 *
          normEDS b c d (HAdd.hAdd (α := ℤ) (↑(2 * m / 2 + 1) : ℤ) 1 * k + 1) *
        normEDS b c d (HAdd.hAdd (α := ℤ) (↑(2 * m / 2 + 1) : ℤ) 1 * k - 1) -
      HPow.hPow (β := ℕ) (complEDS' b c d k (2 * m / 2 + 1 + 1)) 2 * normEDS b c d ((↑(2 * m / 2 + 1) : ℤ) * k + 1) *
        normEDS b c d ((↑(2 * m / 2 + 1) : ℤ) * k - 1)) =
  complEDS' b c d k (m + 1) * complEDS₂ b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k)
Tactic: rw [show 2 * (m + 1) = 2 * m + 2 by rfl, complEDS', dif_pos <| even_two_mul m,
    m.mul_div_cancel_left two_pos, Nat.cast_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
m : ℕ
rw : complEDS' b c d k (2 * m + 2) = complEDS' b c d k (m + 1) * complEDS₂ b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k)
rw₁ :
  (if hn : Even (2 * m) then complEDS' b c d k (2 * m / 2 + 1) * complEDS₂ b c d ((↑(2 * m / 2 + 1) : ℤ) * k)
    else
      have this := ⋯;
      HPow.hPow (β := ℕ) (complEDS' b c d k (2 * m / 2 + 1)) 2 *
            normEDS b c d (HAdd.hAdd (α := ℤ) (↑(2 * m / 2 + 1) : ℤ) 1 * k + 1) *
          normEDS b c d (HAdd.hAdd (α := ℤ) (↑(2 * m / 2 + 1) : ℤ) 1 * k - 1) -
        HPow.hPow (β := ℕ) (complEDS' b c d k (2 * m / 2 + 1 + 1)) 2 * normEDS b c d ((↑(2 * m / 2 + 1) : ℤ) * k + 1) *
          normEDS b c d ((↑(2 * m / 2 + 1) : ℤ) * k - 1)) =
    complEDS' b c d k (m + 1) * complEDS₂ b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k)
⊢ complEDS' b c d k (2 * (m + 1)) = complEDS' b c d k (m + 1) * complEDS₂ b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k)
have rw₂ : complEDS' b c d k (2 * m / 2 + 1) * complEDS₂ b c d ((↑(2 * m / 2 + 1) : ℤ) * k) =
  complEDS' b c d k (m + 1) * complEDS₂ b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k)
Tactic: rw [show 2 * (m + 1) = 2 * m + 2 by rfl, complEDS', dif_pos <| even_two_mul m,
    m.mul_div_cancel_left two_pos, Nat.cast_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
m : ℕ
rw : complEDS' b c d k (2 * m + 2) = complEDS' b c d k (m + 1) * complEDS₂ b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k)
rw₁ :
  (if hn : Even (2 * m) then complEDS' b c d k (2 * m / 2 + 1) * complEDS₂ b c d ((↑(2 * m / 2 + 1) : ℤ) * k)
    else
      have this := ⋯;
      HPow.hPow (β := ℕ) (complEDS' b c d k (2 * m / 2 + 1)) 2 *
            normEDS b c d (HAdd.hAdd (α := ℤ) (↑(2 * m / 2 + 1) : ℤ) 1 * k + 1) *
          normEDS b c d (HAdd.hAdd (α := ℤ) (↑(2 * m / 2 + 1) : ℤ) 1 * k - 1) -
        HPow.hPow (β := ℕ) (complEDS' b c d k (2 * m / 2 + 1 + 1)) 2 * normEDS b c d ((↑(2 * m / 2 + 1) : ℤ) * k + 1) *
          normEDS b c d ((↑(2 * m / 2 + 1) : ℤ) * k - 1)) =
    complEDS' b c d k (m + 1) * complEDS₂ b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k)
rw₂ :
  complEDS' b c d k (2 * m / 2 + 1) * complEDS₂ b c d ((↑(2 * m / 2 + 1) : ℤ) * k) =
    complEDS' b c d k (m + 1) * complEDS₂ b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k)
⊢ complEDS' b c d k (2 * (m + 1)) = complEDS' b c d k (m + 1) * complEDS₂ b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k)
have rw₃ : complEDS' b c d k (m + 1) * complEDS₂ b c d ((↑(m + 1) : ℤ) * k) =
  complEDS' b c d k (m + 1) * complEDS₂ b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k)
Tactic: rw [show 2 * (m + 1) = 2 * m + 2 by rfl, complEDS', dif_pos <| even_two_mul m,
    m.mul_div_cancel_left two_pos, Nat.cast_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
m : ℕ
rw : complEDS' b c d k (2 * m + 2) = complEDS' b c d k (m + 1) * complEDS₂ b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k)
rw₁ :
  (if hn : Even (2 * m) then complEDS' b c d k (2 * m / 2 + 1) * complEDS₂ b c d ((↑(2 * m / 2 + 1) : ℤ) * k)
    else
      have this := ⋯;
      HPow.hPow (β := ℕ) (complEDS' b c d k (2 * m / 2 + 1)) 2 *
            normEDS b c d (HAdd.hAdd (α := ℤ) (↑(2 * m / 2 + 1) : ℤ) 1 * k + 1) *
          normEDS b c d (HAdd.hAdd (α := ℤ) (↑(2 * m / 2 + 1) : ℤ) 1 * k - 1) -
        HPow.hPow (β := ℕ) (complEDS' b c d k (2 * m / 2 + 1 + 1)) 2 * normEDS b c d ((↑(2 * m / 2 + 1) : ℤ) * k + 1) *
          normEDS b c d ((↑(2 * m / 2 + 1) : ℤ) * k - 1)) =
    complEDS' b c d k (m + 1) * complEDS₂ b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k)
rw₂ :
  complEDS' b c d k (2 * m / 2 + 1) * complEDS₂ b c d ((↑(2 * m / 2 + 1) : ℤ) * k) =
    complEDS' b c d k (m + 1) * complEDS₂ b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k)
rw₃ :
  complEDS' b c d k (m + 1) * complEDS₂ b c d ((↑(m + 1) : ℤ) * k) =
    complEDS' b c d k (m + 1) * complEDS₂ b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k)
⊢ complEDS' b c d k (2 * (m + 1)) = complEDS' b c d k (m + 1) * complEDS₂ b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k)
have rw₄ : complEDS' b c d k (m + 1) * complEDS₂ b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k) =
  complEDS' b c d k (m + 1) * complEDS₂ b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k)
Tactic: rw [show 2 * (m + 1) = 2 * m + 2 by rfl, complEDS', dif_pos <| even_two_mul m,
    m.mul_div_cancel_left two_pos, Nat.cast_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
m : ℕ
⊢ complEDS' b c d k (2 * (m + 1) + 1) =
    HPow.hPow (β := ℕ) (complEDS' b c d k (m + 1)) 2 * normEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * k + 1) *
        normEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * k - 1) -
      HPow.hPow (β := ℕ) (complEDS' b c d k (m + 2)) 2 * normEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k + 1) *
        normEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k - 1)
have rw : (have this := sorry;
  HPow.hPow (β := ℕ) (complEDS' b c d k ((2 * m + 1) / 2 + 1)) 2 *
        normEDS b c d (HAdd.hAdd (α := ℤ) (↑((2 * m + 1) / 2 + 1) : ℤ) 1 * k + 1) *
      normEDS b c d (HAdd.hAdd (α := ℤ) (↑((2 * m + 1) / 2 + 1) : ℤ) 1 * k - 1) -
    HPow.hPow (β := ℕ) (complEDS' b c d k ((2 * m + 1) / 2 + 1 + 1)) 2 *
        normEDS b c d ((↑((2 * m + 1) / 2 + 1) : ℤ) * k + 1) *
      normEDS b c d ((↑((2 * m + 1) / 2 + 1) : ℤ) * k - 1)) =
  HPow.hPow (β := ℕ) (complEDS' b c d k (m + 1)) 2 * normEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * k + 1) *
      normEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * k - 1) -
    HPow.hPow (β := ℕ) (complEDS' b c d k (m + 2)) 2 * normEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k + 1) *
      normEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k - 1)
Tactic: rw [show 2 * (m + 1) + 1 = 2 * m + 3 by rfl, complEDS', 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
k : ℤ
n : ℕ
⊢ complEDS b c d k (↑n : ℤ) = complEDS' b c d k n
have pos : ∀ (hn : n = 0), complEDS b c d k (↑n : ℤ) = complEDS' b c d k 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
k : ℤ
n : ℕ
pos : ∀ (hn : n = 0), complEDS b c d k (↑n : ℤ) = complEDS' b c d k n
⊢ complEDS b c d k (↑n : ℤ) = complEDS' b c d k n
have neg : ∀ (hn : ¬n = 0), complEDS b c d k (↑n : ℤ) = complEDS' b c d k 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
k : ℤ
m : ℕ
⊢ complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑m : ℤ)) = complEDS b c d k (↑m : ℤ) * complEDS₂ b c d ((↑m : ℤ) * k)
have nat : complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑0 : ℤ)) = complEDS b c d k (↑0 : ℤ) * complEDS₂ b c d ((↑0 : ℤ) * k)
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
k : ℤ
m : ℕ
nat : complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑0 : ℤ)) = complEDS b c d k (↑0 : ℤ) * complEDS₂ b c d ((↑0 : ℤ) * k)
⊢ complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑m : ℤ)) = complEDS b c d k (↑m : ℤ) * complEDS₂ b c d ((↑m : ℤ) * k)
have nat₁ : ∀ (n : ℕ),
  complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑(n + 1) : ℤ)) =
    complEDS b c d k (↑(n + 1) : ℤ) * complEDS₂ b c d ((↑(n + 1) : ℤ) * k)
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
k : ℤ
ih :
  ∀ (n : ℕ),
    complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑n : ℤ)) = complEDS b c d k (↑n : ℤ) * complEDS₂ b c d ((↑n : ℤ) * k)
n : ℕ
⊢ complEDS b c d k (HMul.hMul (α := ℤ) 2 (-(↑n : ℤ))) = complEDS b c d k (-(↑n : ℤ)) * complEDS₂ b c d (-(↑n : ℤ) * k)
have neg : complEDS b c d k (-HMul.hMul (α := ℤ) 2 (↑n : ℤ)) = complEDS b c d k (-(↑n : ℤ)) * complEDS₂ b c d (-(↑n : ℤ) * k)
Tactic: simp_rw [mul_neg, complEDS_neg, ih, neg_mul, complEDS₂_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
ih :
  ∀ (n : ℕ),
    complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑n : ℤ)) = complEDS b c d k (↑n : ℤ) * complEDS₂ b c d ((↑n : ℤ) * k)
n : ℕ
neg : complEDS b c d k (-HMul.hMul (α := ℤ) 2 (↑n : ℤ)) = complEDS b c d k (-(↑n : ℤ)) * complEDS₂ b c d (-(↑n : ℤ) * k)
⊢ complEDS b c d k (HMul.hMul (α := ℤ) 2 (-(↑n : ℤ))) = complEDS b c d k (-(↑n : ℤ)) * complEDS₂ b c d (-(↑n : ℤ) * k)
have neg₁ : -complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑n : ℤ)) = -complEDS b c d k (↑n : ℤ) * complEDS₂ b c d (-(↑n : ℤ) * k)
Tactic: simp_rw [mul_neg, complEDS_neg, ih, neg_mul, complEDS₂_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
ih :
  ∀ (n : ℕ),
    complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑n : ℤ)) = complEDS b c d k (↑n : ℤ) * complEDS₂ b c d ((↑n : ℤ) * k)
n : ℕ
neg : complEDS b c d k (-HMul.hMul (α := ℤ) 2 (↑n : ℤ)) = complEDS b c d k (-(↑n : ℤ)) * complEDS₂ b c d (-(↑n : ℤ) * k)
neg₁ : -complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑n : ℤ)) = -complEDS b c d k (↑n : ℤ) * complEDS₂ b c d (-(↑n : ℤ) * k)
⊢ complEDS b c d k (HMul.hMul (α := ℤ) 2 (-(↑n : ℤ))) = complEDS b c d k (-(↑n : ℤ)) * complEDS₂ b c d (-(↑n : ℤ) * k)
have neg₂ : -(complEDS b c d k (↑n : ℤ) * complEDS₂ b c d ((↑n : ℤ) * k)) =
  -complEDS b c d k (↑n : ℤ) * complEDS₂ b c d (-(↑n : ℤ) * k)
Tactic: simp_rw [mul_neg, complEDS_neg, ih, neg_mul, complEDS₂_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
ih :
  ∀ (n : ℕ),
    complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑n : ℤ)) = complEDS b c d k (↑n : ℤ) * complEDS₂ b c d ((↑n : ℤ) * k)
n : ℕ
neg : complEDS b c d k (-HMul.hMul (α := ℤ) 2 (↑n : ℤ)) = complEDS b c d k (-(↑n : ℤ)) * complEDS₂ b c d (-(↑n : ℤ) * k)
neg₁ : -complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑n : ℤ)) = -complEDS b c d k (↑n : ℤ) * complEDS₂ b c d (-(↑n : ℤ) * k)
neg₂ :
  -(complEDS b c d k (↑n : ℤ) * complEDS₂ b c d ((↑n : ℤ) * k)) =
    -complEDS b c d k (↑n : ℤ) * complEDS₂ b c d (-(↑n : ℤ) * k)
⊢ complEDS b c d k (HMul.hMul (α := ℤ) 2 (-(↑n : ℤ))) = complEDS b c d k (-(↑n : ℤ)) * complEDS₂ b c d (-(↑n : ℤ) * k)
have neg₃ : -(complEDS b c d k (↑n : ℤ) * complEDS₂ b c d ((↑n : ℤ) * k)) =
  -(complEDS b c d k (↑n : ℤ) * complEDS₂ b c d (-((↑n : ℤ) * k)))
Tactic: simp_rw [mul_neg, complEDS_neg, ih, neg_mul, complEDS₂_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
k m : ℤ
⊢ complEDS b c d k (2 * m) = complEDS b c d k m * complEDS₂ b c d (m * k)
have nat : ∀ (m : ℕ), complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑m : ℤ)) = complEDS b c d k (↑m : ℤ) * complEDS₂ b c d ((↑m : ℤ) * k)
Tactic: induction m using Int.negInduction with
  | nat m =>
    rcases m with _ | _
    · simp
    norm_cast
    simpa only [complEDS_ofNat] using complEDS'_even ..
  | neg ih => simp_rw [mul_neg, complEDS_neg, ih, neg_mul, complEDS₂_neg]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
k m : ℤ
nat :
  ∀ (m : ℕ),
    complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑m : ℤ)) = complEDS b c d k (↑m : ℤ) * complEDS₂ b c d ((↑m : ℤ) * k)
⊢ complEDS b c d k (2 * m) = complEDS b c d k m * complEDS₂ b c d (m * k)
have neg : ∀
  (ih :
    ∀ (n : ℕ),
      complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑n : ℤ)) = complEDS b c d k (↑n : ℤ) * complEDS₂ b c d ((↑n : ℤ) * k))
  (n : ℕ),
  complEDS b c d k (HMul.hMul (α := ℤ) 2 (-(↑n : ℤ))) = complEDS b c d k (-(↑n : ℤ)) * complEDS₂ b c d (-(↑n : ℤ) * k)
Tactic: induction m using Int.negInduction with
  | nat m =>
    rcases m with _ | _
    · simp
    norm_cast
    simpa only [complEDS_ofNat] using complEDS'_even ..
  | neg ih => simp_rw [mul_neg, complEDS_neg, ih, neg_mul, complEDS₂_neg]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
m : ℕ
⊢ complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑m : ℤ) + 1) =
    HPow.hPow (β := ℕ) (complEDS b c d k (↑m : ℤ)) 2 * normEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k + 1) *
        normEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k - 1) -
      HPow.hPow (β := ℕ) (complEDS b c d k (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) 2 * normEDS b c d ((↑m : ℤ) * k + 1) *
        normEDS b c d ((↑m : ℤ) * k - 1)
have nat : complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑0 : ℤ) + 1) =
  HPow.hPow (β := ℕ) (complEDS b c d k (↑0 : ℤ)) 2 * normEDS b c d (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1 * k + 1) *
      normEDS b c d (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1 * k - 1) -
    HPow.hPow (β := ℕ) (complEDS b c d k (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1)) 2 * normEDS b c d ((↑0 : ℤ) * k + 1) *
      normEDS b c d ((↑0 : ℤ) * k - 1)
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
k : ℤ
m : ℕ
nat :
  complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑0 : ℤ) + 1) =
    HPow.hPow (β := ℕ) (complEDS b c d k (↑0 : ℤ)) 2 * normEDS b c d (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1 * k + 1) *
        normEDS b c d (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1 * k - 1) -
      HPow.hPow (β := ℕ) (complEDS b c d k (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1)) 2 * normEDS b c d ((↑0 : ℤ) * k + 1) *
        normEDS b c d ((↑0 : ℤ) * k - 1)
⊢ complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑m : ℤ) + 1) =
    HPow.hPow (β := ℕ) (complEDS b c d k (↑m : ℤ)) 2 * normEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k + 1) *
        normEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k - 1) -
      HPow.hPow (β := ℕ) (complEDS b c d k (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) 2 * normEDS b c d ((↑m : ℤ) * k + 1) *
        normEDS b c d ((↑m : ℤ) * k - 1)
have nat₁ : ∀ (n : ℕ),
  complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑(n + 1) : ℤ) + 1) =
    HPow.hPow (β := ℕ) (complEDS b c d k (↑(n + 1) : ℤ)) 2 *
          normEDS b c d (HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1 * k + 1) *
        normEDS b c d (HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1 * k - 1) -
      HPow.hPow (β := ℕ) (complEDS b c d k (HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1)) 2 *
          normEDS b c d ((↑(n + 1) : ℤ) * k + 1) *
        normEDS b c d ((↑(n + 1) : ℤ) * k - 1)
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
k : ℤ
n : ℕ
⊢ complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑(n + 1) : ℤ) + 1) =
    HPow.hPow (β := ℕ) (complEDS b c d k (↑(n + 1) : ℤ)) 2 *
          normEDS b c d (HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1 * k + 1) *
        normEDS b c d (HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1 * k - 1) -
      HPow.hPow (β := ℕ) (complEDS b c d k (HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1)) 2 *
          normEDS b c d ((↑(n + 1) : ℤ) * k + 1) *
        normEDS b c d ((↑(n + 1) : ℤ) * k - 1)
have nat : complEDS b c d k (↑(2 * (n + 1) + 1) : ℤ) =
  HPow.hPow (β := ℕ) (complEDS b c d k (↑(n + 1) : ℤ)) 2 * normEDS b c d ((↑(n + 1 + 1) : ℤ) * k + 1) *
      normEDS b c d ((↑(n + 1 + 1) : ℤ) * k - 1) -
    HPow.hPow (β := ℕ) (complEDS b c d k (↑(n + 1 + 1) : ℤ)) 2 * normEDS b c d ((↑(n + 1) : ℤ) * k + 1) *
      normEDS b c d ((↑(n + 1) : ℤ) * k - 1)
Tactic: norm_cast