awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
m : ℕ
⊢ HPow.hPow (β := ℕ) (HMul.hMul (α := ℤ) 2 (↑m : ℤ) + 6) 2 - 4 =
    2 * (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2) 2 - if Even m then 4 else 1) +
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 3) 2 - if Even m then 1 else 4) +
      (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 5) 2 - if Even m then 1 else 4)
have pos : Even m →
  HPow.hPow (β := ℕ) (HMul.hMul (α := ℤ) 2 (↑m : ℤ) + 6) 2 - 4 =
    2 * (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2) 2 - 4) +
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 3) 2 - 1) +
      (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 5) 2 - 1)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
m : ℕ
pos :
  Even m →
    HPow.hPow (β := ℕ) (HMul.hMul (α := ℤ) 2 (↑m : ℤ) + 6) 2 - 4 =
      2 * (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2) 2 - 4) +
          (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 3) 2 - 1) +
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 5) 2 - 1)
⊢ HPow.hPow (β := ℕ) (HMul.hMul (α := ℤ) 2 (↑m : ℤ) + 6) 2 - 4 =
    2 * (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2) 2 - if Even m then 4 else 1) +
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 3) 2 - if Even m then 1 else 4) +
      (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 5) 2 - if Even m then 1 else 4)
have neg : ¬Even m →
  HPow.hPow (β := ℕ) (HMul.hMul (α := ℤ) 2 (↑m : ℤ) + 6) 2 - 4 =
    2 * (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2) 2 - 1) +
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 3) 2 - 4) +
      (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 5) 2 - 4)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
m : ℕ
⊢ HPow.hPow (β := ℕ) (HMul.hMul (α := ℤ) 2 (↑m : ℤ) + 6) 2 - 4 =
    (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) 2 - if Even m then 1 else 4) +
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 3) 2 - if Even m then 1 else 4) +
      2 * (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 4) 2 - if Even m then 4 else 1)
have pos : Even m →
  HPow.hPow (β := ℕ) (HMul.hMul (α := ℤ) 2 (↑m : ℤ) + 6) 2 - 4 =
    HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) 2 - 1 +
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 3) 2 - 1) +
      2 * (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 4) 2 - 4)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
m : ℕ
pos :
  Even m →
    HPow.hPow (β := ℕ) (HMul.hMul (α := ℤ) 2 (↑m : ℤ) + 6) 2 - 4 =
      HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) 2 - 1 +
          (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 3) 2 - 1) +
        2 * (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 4) 2 - 4)
⊢ HPow.hPow (β := ℕ) (HMul.hMul (α := ℤ) 2 (↑m : ℤ) + 6) 2 - 4 =
    (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) 2 - if Even m then 1 else 4) +
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 3) 2 - if Even m then 1 else 4) +
      2 * (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 4) 2 - if Even m then 4 else 1)
have neg : ¬Even m →
  HPow.hPow (β := ℕ) (HMul.hMul (α := ℤ) 2 (↑m : ℤ) + 6) 2 - 4 =
    HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) 2 - 4 +
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 3) 2 - 4) +
      2 * (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 4) 2 - 1)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
m : ℕ
⊢ HPow.hPow (β := ℕ) (HMul.hMul (α := ℤ) 2 (↑m : ℤ) + 4 + 1) 2 - 1 =
    (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 4) 2 - if Even m then 4 else 1) +
        3 * (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2) 2 - if Even m then 4 else 1) +
      HMul.hMul (α := ℤ) 2 (if Even m then 6 else 0)
have pos : Even m →
  HPow.hPow (β := ℕ) (HMul.hMul (α := ℤ) 2 (↑m : ℤ) + 4 + 1) 2 - 1 =
    HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 4) 2 - 4 +
        3 * (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2) 2 - 4) +
      HMul.hMul (α := ℤ) 2 6
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
m : ℕ
pos :
  Even m →
    HPow.hPow (β := ℕ) (HMul.hMul (α := ℤ) 2 (↑m : ℤ) + 4 + 1) 2 - 1 =
      HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 4) 2 - 4 +
          3 * (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2) 2 - 4) +
        HMul.hMul (α := ℤ) 2 6
⊢ HPow.hPow (β := ℕ) (HMul.hMul (α := ℤ) 2 (↑m : ℤ) + 4 + 1) 2 - 1 =
    (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 4) 2 - if Even m then 4 else 1) +
        3 * (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2) 2 - if Even m then 4 else 1) +
      HMul.hMul (α := ℤ) 2 (if Even m then 6 else 0)
have neg : ¬Even m →
  HPow.hPow (β := ℕ) (HMul.hMul (α := ℤ) 2 (↑m : ℤ) + 4 + 1) 2 - 1 =
    HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 4) 2 - 1 +
        3 * (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2) 2 - 1) +
      HMul.hMul (α := ℤ) 2 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
m : ℕ
⊢ HPow.hPow (β := ℕ) (HMul.hMul (α := ℤ) 2 (↑m : ℤ) + 4 + 1) 2 - 1 =
    (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) 2 - if Even m then 1 else 4) +
        3 * (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 3) 2 - if Even m then 1 else 4) +
      HMul.hMul (α := ℤ) 2 (if Even m then 0 else 6)
have pos : Even m →
  HPow.hPow (β := ℕ) (HMul.hMul (α := ℤ) 2 (↑m : ℤ) + 4 + 1) 2 - 1 =
    HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) 2 - 1 +
        3 * (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 3) 2 - 1) +
      HMul.hMul (α := ℤ) 2 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
m : ℕ
pos :
  Even m →
    HPow.hPow (β := ℕ) (HMul.hMul (α := ℤ) 2 (↑m : ℤ) + 4 + 1) 2 - 1 =
      HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) 2 - 1 +
          3 * (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 3) 2 - 1) +
        HMul.hMul (α := ℤ) 2 0
⊢ HPow.hPow (β := ℕ) (HMul.hMul (α := ℤ) 2 (↑m : ℤ) + 4 + 1) 2 - 1 =
    (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) 2 - if Even m then 1 else 4) +
        3 * (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 3) 2 - if Even m then 1 else 4) +
      HMul.hMul (α := ℤ) 2 (if Even m then 0 else 6)
have neg : ¬Even m →
  HPow.hPow (β := ℕ) (HMul.hMul (α := ℤ) 2 (↑m : ℤ) + 4 + 1) 2 - 1 =
    HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) 2 - 4 +
        3 * (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 3) 2 - 4) +
      HMul.hMul (α := ℤ) 2 6
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
n : ℕ
⊢ (↑(expCoeff n) : ℚ) = if Even n then HDiv.hDiv (α := ℚ) (↑n : ℚ) 2 else (↑n : ℚ)
have inl : ∀ (n : ℕ), (↑(expCoeff (2 * n)) : ℚ) = if Even (2 * n) then HDiv.hDiv (α := ℚ) (↑(2 * n) : ℚ) 2 else (↑(2 * n) : ℚ)
Tactic: rcases n.even_or_odd' with ⟨n, rfl | rfl⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
n : ℕ
inl :
  ∀ (n : ℕ), (↑(expCoeff (2 * n)) : ℚ) = if Even (2 * n) then HDiv.hDiv (α := ℚ) (↑(2 * n) : ℚ) 2 else (↑(2 * n) : ℚ)
⊢ (↑(expCoeff n) : ℚ) = if Even n then HDiv.hDiv (α := ℚ) (↑n : ℚ) 2 else (↑n : ℚ)
have inr : ∀ (n : ℕ),
  (↑(expCoeff (2 * n + 1)) : ℚ) =
    if Even (2 * n + 1) then HDiv.hDiv (α := ℚ) (↑(2 * n + 1) : ℚ) 2 else (↑(2 * n + 1) : ℚ)
Tactic: rcases n.even_or_odd' with ⟨n, rfl | rfl⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
m : ℕ
⊢ expCoeff (2 * (m + 3)) =
      HPow.hPow (β := ℕ) (expCoeff (m + 2)) 2 * expCoeff (m + 3) * expCoeff (m + 5) -
        expCoeff (m + 1) * expCoeff (m + 3) * HPow.hPow (β := ℕ) (expCoeff (m + 4)) 2 ∧
    expCoeff (2 * (m + 2) + 1) =
      (expCoeff (m + 4) * HPow.hPow (β := ℕ) (expCoeff (m + 2)) 3 *
          if Even m then HPow.hPow (α := ℤ) (β := ℕ) 4 2 else 1) -
        expCoeff (m + 1) * HPow.hPow (β := ℕ) (expCoeff (m + 3)) 3 *
          if Even m then 1 else HPow.hPow (α := ℤ) (β := ℕ) 4 2
have push_cast : 2 * HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2 =
    ((HPow.hPow (β := ℕ) (if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 2 / 2 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 2) 2 *
          if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2) *
        if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 5 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 5 / 2) -
      ((if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 1 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 1 / 2) *
          if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2) *
        HPow.hPow (β := ℕ) (if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 4 / 2 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 4) 2 ∧
  2 * HAdd.hAdd (α := ℚ) (↑m : ℚ) 2 + 1 =
    ((if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 4 / 2 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 4) *
          HPow.hPow (β := ℕ) (if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 2 / 2 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 2) 3 *
        if Even m then 16 else 1) -
      (if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 1 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 1 / 2) *
          HPow.hPow (β := ℕ) (if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2) 3 *
        if Even m then 1 else 16
Tactic: push_cast [← @Int.cast_inj ℚ, expCoeff_cast, even_two_mul, m.not_even_two_mul_add_one,
    Nat.even_add_one, ite_not]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
m : ℕ
⊢ 2 * HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2 =
      ((HPow.hPow (β := ℕ) (if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 2 / 2 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 2) 2 *
            if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2) *
          if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 5 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 5 / 2) -
        ((if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 1 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 1 / 2) *
            if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2) *
          HPow.hPow (β := ℕ) (if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 4 / 2 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 4) 2 ∧
    2 * HAdd.hAdd (α := ℚ) (↑m : ℚ) 2 + 1 =
      ((if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 4 / 2 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 4) *
            HPow.hPow (β := ℕ) (if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 2 / 2 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 2) 3 *
          if Even m then 16 else 1) -
        (if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 1 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 1 / 2) *
            HPow.hPow (β := ℕ) (if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2) 3 *
          if Even m then 1 else 16
have left : 2 * HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2 =
  ((HPow.hPow (β := ℕ) (if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 2 / 2 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 2) 2 *
        if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2) *
      if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 5 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 5 / 2) -
    ((if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 1 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 1 / 2) *
        if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2) *
      HPow.hPow (β := ℕ) (if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 4 / 2 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 4) 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
m : ℕ
left :
  2 * HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2 =
    ((HPow.hPow (β := ℕ) (if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 2 / 2 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 2) 2 *
          if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2) *
        if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 5 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 5 / 2) -
      ((if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 1 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 1 / 2) *
          if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2) *
        HPow.hPow (β := ℕ) (if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 4 / 2 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 4) 2
⊢ 2 * HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2 =
      ((HPow.hPow (β := ℕ) (if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 2 / 2 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 2) 2 *
            if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2) *
          if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 5 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 5 / 2) -
        ((if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 1 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 1 / 2) *
            if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2) *
          HPow.hPow (β := ℕ) (if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 4 / 2 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 4) 2 ∧
    2 * HAdd.hAdd (α := ℚ) (↑m : ℚ) 2 + 1 =
      ((if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 4 / 2 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 4) *
            HPow.hPow (β := ℕ) (if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 2 / 2 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 2) 3 *
          if Even m then 16 else 1) -
        (if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 1 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 1 / 2) *
            HPow.hPow (β := ℕ) (if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2) 3 *
          if Even m then 1 else 16
have right : 2 * HAdd.hAdd (α := ℚ) (↑m : ℚ) 2 + 1 =
  ((if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 4 / 2 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 4) *
        HPow.hPow (β := ℕ) (if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 2 / 2 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 2) 3 *
      if Even m then 16 else 1) -
    (if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 1 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 1 / 2) *
        HPow.hPow (β := ℕ) (if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2) 3 *
      if Even m then 1 else 16
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
m : ℕ
⊢ 2 * HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2 =
    ((HPow.hPow (β := ℕ) (if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 2 / 2 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 2) 2 *
          if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2) *
        if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 5 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 5 / 2) -
      ((if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 1 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 1 / 2) *
          if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2) *
        HPow.hPow (β := ℕ) (if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 4 / 2 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 4) 2
have pos : Even m →
  2 * HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2 =
    HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑m : ℚ) 2 / 2) 2 * HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 *
        HAdd.hAdd (α := ℚ) (↑m : ℚ) 5 -
      HAdd.hAdd (α := ℚ) (↑m : ℚ) 1 * HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 *
        HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑m : ℚ) 4 / 2) 2
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
m : ℕ
pos :
  Even m →
    2 * HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2 =
      HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑m : ℚ) 2 / 2) 2 * HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 *
          HAdd.hAdd (α := ℚ) (↑m : ℚ) 5 -
        HAdd.hAdd (α := ℚ) (↑m : ℚ) 1 * HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 *
          HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑m : ℚ) 4 / 2) 2
⊢ 2 * HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2 =
    ((HPow.hPow (β := ℕ) (if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 2 / 2 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 2) 2 *
          if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2) *
        if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 5 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 5 / 2) -
      ((if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 1 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 1 / 2) *
          if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2) *
        HPow.hPow (β := ℕ) (if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 4 / 2 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 4) 2
have neg : ¬Even m →
  2 * HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2 =
    HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑m : ℚ) 2) 2 * (HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2) *
        (HAdd.hAdd (α := ℚ) (↑m : ℚ) 5 / 2) -
      HAdd.hAdd (α := ℚ) (↑m : ℚ) 1 / 2 * (HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2) *
        HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑m : ℚ) 4) 2
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
m : ℕ
⊢ 2 * HAdd.hAdd (α := ℚ) (↑m : ℚ) 2 + 1 =
    ((if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 4 / 2 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 4) *
          HPow.hPow (β := ℕ) (if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 2 / 2 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 2) 3 *
        if Even m then 16 else 1) -
      (if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 1 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 1 / 2) *
          HPow.hPow (β := ℕ) (if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2) 3 *
        if Even m then 1 else 16
have pos : Even m →
  2 * HAdd.hAdd (α := ℚ) (↑m : ℚ) 2 + 1 =
    HAdd.hAdd (α := ℚ) (↑m : ℚ) 4 / 2 * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑m : ℚ) 2 / 2) 3 * 16 -
      HAdd.hAdd (α := ℚ) (↑m : ℚ) 1 * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑m : ℚ) 3) 3 * 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
m : ℕ
pos :
  Even m →
    2 * HAdd.hAdd (α := ℚ) (↑m : ℚ) 2 + 1 =
      HAdd.hAdd (α := ℚ) (↑m : ℚ) 4 / 2 * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑m : ℚ) 2 / 2) 3 * 16 -
        HAdd.hAdd (α := ℚ) (↑m : ℚ) 1 * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑m : ℚ) 3) 3 * 1
⊢ 2 * HAdd.hAdd (α := ℚ) (↑m : ℚ) 2 + 1 =
    ((if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 4 / 2 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 4) *
          HPow.hPow (β := ℕ) (if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 2 / 2 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 2) 3 *
        if Even m then 16 else 1) -
      (if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 1 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 1 / 2) *
          HPow.hPow (β := ℕ) (if Even m then HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 else HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2) 3 *
        if Even m then 1 else 16
have neg : ¬Even m →
  2 * HAdd.hAdd (α := ℚ) (↑m : ℚ) 2 + 1 =
    HAdd.hAdd (α := ℚ) (↑m : ℚ) 4 * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑m : ℚ) 2) 3 * 1 -
      HAdd.hAdd (α := ℚ) (↑m : ℚ) 1 / 2 * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2) 3 * 16
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m := ⋯
m : ℕ
h₁ :
  natDegree (W.preΨ' (m + 1)) ≤ expDegree (m + 1) ∧
    coeff (W.preΨ' (m + 1)) (expDegree (m + 1)) = (↑(expCoeff (m + 1)) : R)
h₂ :
  natDegree (W.preΨ' (m + 2)) ≤ expDegree (m + 2) ∧
    coeff (W.preΨ' (m + 2)) (expDegree (m + 2)) = (↑(expCoeff (m + 2)) : R)
h₃ :
  natDegree (W.preΨ' (m + 3)) ≤ expDegree (m + 3) ∧
    coeff (W.preΨ' (m + 3)) (expDegree (m + 3)) = (↑(expCoeff (m + 3)) : R)
h₄ :
  natDegree (W.preΨ' (m + 4)) ≤ expDegree (m + 4) ∧
    coeff (W.preΨ' (m + 4)) (expDegree (m + 4)) = (↑(expCoeff (m + 4)) : R)
h₅ :
  natDegree (W.preΨ' (m + 5)) ≤ expDegree (m + 5) ∧
    coeff (W.preΨ' (m + 5)) (expDegree (m + 5)) = (↑(expCoeff (m + 5)) : R)
⊢ natDegree (W.preΨ' (2 * (m + 3))) ≤ expDegree (2 * (m + 3)) ∧
    coeff (W.preΨ' (2 * (m + 3))) (expDegree (2 * (m + 3))) = (↑(expCoeff (2 * (m + 3))) : R)
have even : natDegree (W.preΨ' (2 * (m + 3))) ≤ expDegree (2 * (m + 3))
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m := ⋯
m : ℕ
h₁ :
  natDegree (W.preΨ' (m + 1)) ≤ expDegree (m + 1) ∧
    coeff (W.preΨ' (m + 1)) (expDegree (m + 1)) = (↑(expCoeff (m + 1)) : R)
h₂ :
  natDegree (W.preΨ' (m + 2)) ≤ expDegree (m + 2) ∧
    coeff (W.preΨ' (m + 2)) (expDegree (m + 2)) = (↑(expCoeff (m + 2)) : R)
h₃ :
  natDegree (W.preΨ' (m + 3)) ≤ expDegree (m + 3) ∧
    coeff (W.preΨ' (m + 3)) (expDegree (m + 3)) = (↑(expCoeff (m + 3)) : R)
h₄ :
  natDegree (W.preΨ' (m + 4)) ≤ expDegree (m + 4) ∧
    coeff (W.preΨ' (m + 4)) (expDegree (m + 4)) = (↑(expCoeff (m + 4)) : R)
h₅ :
  natDegree (W.preΨ' (m + 5)) ≤ expDegree (m + 5) ∧
    coeff (W.preΨ' (m + 5)) (expDegree (m + 5)) = (↑(expCoeff (m + 5)) : R)
even : natDegree (W.preΨ' (2 * (m + 3))) ≤ expDegree (2 * (m + 3))
⊢ natDegree (W.preΨ' (2 * (m + 3))) ≤ expDegree (2 * (m + 3)) ∧
    coeff (W.preΨ' (2 * (m + 3))) (expDegree (2 * (m + 3))) = (↑(expCoeff (2 * (m + 3))) : R)
have even₁ : coeff (W.preΨ' (2 * (m + 3))) (expDegree (2 * (m + 3))) = (↑(expCoeff (2 * (m + 3))) : R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m := ⋯
m : ℕ
h₁ :
  natDegree (W.preΨ' (m + 1)) ≤ expDegree (m + 1) ∧
    coeff (W.preΨ' (m + 1)) (expDegree (m + 1)) = (↑(expCoeff (m + 1)) : R)
h₂ :
  natDegree (W.preΨ' (m + 2)) ≤ expDegree (m + 2) ∧
    coeff (W.preΨ' (m + 2)) (expDegree (m + 2)) = (↑(expCoeff (m + 2)) : R)
h₃ :
  natDegree (W.preΨ' (m + 3)) ≤ expDegree (m + 3) ∧
    coeff (W.preΨ' (m + 3)) (expDegree (m + 3)) = (↑(expCoeff (m + 3)) : R)
h₄ :
  natDegree (W.preΨ' (m + 4)) ≤ expDegree (m + 4) ∧
    coeff (W.preΨ' (m + 4)) (expDegree (m + 4)) = (↑(expCoeff (m + 4)) : R)
h₅ :
  natDegree (W.preΨ' (m + 5)) ≤ expDegree (m + 5) ∧
    coeff (W.preΨ' (m + 5)) (expDegree (m + 5)) = (↑(expCoeff (m + 5)) : R)
⊢ natDegree (W.preΨ' (2 * (m + 3))) ≤ expDegree (2 * (m + 3))
have even : (HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (m + 2)) 2 * W.preΨ' (m + 3) * W.preΨ' (m + 5) -
      HMul.hMul (α := R[X]) (W.preΨ' (m + 1)) (W.preΨ' (m + 3)) *
        HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (m + 4)) 2).natDegree ≤
  max (2 * expDegree (m + 2) + expDegree (m + 3) + expDegree (m + 5))
    (expDegree (m + 1) + expDegree (m + 3) + 2 * expDegree (m + 4))
Tactic: nth_rw 1 [preΨ'_even, ← max_self <| expDegree _, (expDegree_rec m).1.1, (expDegree_rec m).1.2]