awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
m : ℕ
push_cast :
  (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) ∧
      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)) ∧
    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) ∧
      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)
⊢ ((HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 6) : ℤ) 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 2) : ℤ) 2 - if Even (m + 2) then 4 else 1) +
            (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 3) : ℤ) 2 - if Even (m + 3) then 4 else 1) +
          (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 5) : ℤ) 2 - if Even (m + 5) then 4 else 1) ∧
      (HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 6) : ℤ) 2 - if Even (2 * m + 6) then 4 else 1) =
        (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 1) : ℤ) 2 - if Even (m + 1) then 4 else 1) +
            (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 3) : ℤ) 2 - if Even (m + 3) then 4 else 1) +
          2 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 4) : ℤ) 2 - if Even (m + 4) then 4 else 1)) ∧
    (HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 4 + 1) : ℤ) 2 - if Even (2 * m + 4 + 1) then 4 else 1) =
        (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 4) : ℤ) 2 - if Even (m + 4) then 4 else 1) +
            3 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 2) : ℤ) 2 - if Even (m + 2) then 4 else 1) +
          HMul.hMul (α := ℤ) 2 (if Even m then 6 else 0) ∧
      (HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 4 + 1) : ℤ) 2 - if Even (2 * m + 4 + 1) then 4 else 1) =
        (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 1) : ℤ) 2 - if Even (m + 1) then 4 else 1) +
            3 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 3) : ℤ) 2 - if Even (m + 3) then 4 else 1) +
          HMul.hMul (α := ℤ) 2 (if Even m then 0 else 6)

Tactic:
push_cast [Nat.even_add_one, ite_not, even_two_mul]

Premises used: Nat.even_add_one, even_two_mul, ite_not
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
m : ℕ
left :
  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) ∧
    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)
right :
  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) ∧
    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)
⊢ (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) ∧
      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)) ∧
    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) ∧
      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)

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
m : ℕ
left :
  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)
left₁ :
  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)
⊢ 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) ∧
    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)

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
m : ℕ
right :
  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)
right₁ :
  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)
⊢ 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) ∧
    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)

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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)
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)
⊢ 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)

Tactic:
split_ifs
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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)
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)
⊢ 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)

Tactic:
split_ifs
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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
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
⊢ 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)

Tactic:
split_ifs
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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
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
⊢ 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)

Tactic:
split_ifs
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
m : ℕ
h : 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:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
m : ℕ
h : ¬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:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
m : ℕ
h : 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:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
m : ℕ
h : ¬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:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
m : ℕ
h : 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:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
m : ℕ
h : ¬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:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
m : ℕ
h : 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:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
m : ℕ
h : ¬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:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
n : ℕ
inl :
  ∀ (n : ℕ), (↑(expCoeff (2 * n)) : ℚ) = if Even (2 * n) then HDiv.hDiv (α := ℚ) (↑(2 * n) : ℚ) 2 else (↑(2 * n) : ℚ)
inr :
  ∀ (n : ℕ),
    (↑(expCoeff (2 * n + 1)) : ℚ) =
      if Even (2 * n + 1) then HDiv.hDiv (α := ℚ) (↑(2 * n + 1) : ℚ) 2 else (↑(2 * n + 1) : ℚ)
⊢ (↑(expCoeff n) : ℚ) = if Even n then HDiv.hDiv (α := ℚ) (↑n : ℚ) 2 else (↑n : ℚ)

Tactic:
rcases n.even_or_odd' with ⟨n, rfl | rfl⟩

Premises used: Nat.even_or_odd', rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
n : ℕ
⊢ (↑(expCoeff (2 * n)) : ℚ) = if Even (2 * n) then HDiv.hDiv (α := ℚ) (↑(2 * n) : ℚ) 2 else (↑(2 * n) : ℚ)

Tactic:
simp [expCoeff, n.not_even_two_mul_add_one]

Premises used: Nat.not_even_two_mul_add_one, _private.0.WeierstrassCurve.expCoeff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
n : ℕ
⊢ (↑(expCoeff (2 * n + 1)) : ℚ) =
    if Even (2 * n + 1) then HDiv.hDiv (α := ℚ) (↑(2 * n + 1) : ℚ) 2 else (↑(2 * n + 1) : ℚ)

Tactic:
simp [expCoeff, n.not_even_two_mul_add_one]

Premises used: Nat.not_even_two_mul_add_one, _private.0.WeierstrassCurve.expCoeff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
m : ℕ
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
⊢ 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

Tactic:
push_cast [← @Int.cast_inj ℚ, expCoeff_cast, even_two_mul, m.not_even_two_mul_add_one,
    Nat.even_add_one, ite_not]

Premises used: Nat.even_add_one, Int.cast_inj, _private.0.WeierstrassCurve.expCoeff_cast, even_two_mul, Nat.not_even_two_mul_add_one, ite_not
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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
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
⊢ 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:
constructor
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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
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
⊢ 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:
split_ifs
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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
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
⊢ 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:
split_ifs
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
m : ℕ
h : 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:
ring1