awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
m : ℕ
⊢ ((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) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 1)) : ℤ) +
            (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 3) : ℤ) 2 - if Even (m + 3) then 4 else 1) +
          2 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 4)) : ℤ)) ∧
    HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 4)) : ℤ) +
            3 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 2) : ℤ) 2 - if Even (m + 2) then 4 else 1) +
          HMul.hMul (α := ℤ) 2 (if Even m then 6 else 0) ∧
      HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 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)
have rw : ((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 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 4)) : ℤ)) ∧
  HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
      HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 4)) : ℤ) +
          3 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 2) : ℤ) 2 - if Even (m + 2) then 4 else 1) +
        HMul.hMul (α := ℤ) 2 (if Even m then 6 else 0) ∧
    HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 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: rw [expDegree_cast <| by lia]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
m : ℕ
⊢ ((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 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 4)) : ℤ)) ∧
    HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 4)) : ℤ) +
            3 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 2) : ℤ) 2 - if Even (m + 2) then 4 else 1) +
          HMul.hMul (α := ℤ) 2 (if Even m then 6 else 0) ∧
      HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 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)
have rw : ((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)) ∧
  HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 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) ∧
    HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 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: rw [expDegree_cast <| by lia]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
m : ℕ
⊢ ((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)) ∧
    HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 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) ∧
      HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 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)
have rw : ((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: rw [expDegree_cast <| by lia]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
m : ℕ
⊢ (HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 6)) : ℤ) =
        2 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 2)) : ℤ) + HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 3)) : ℤ) +
          HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 5)) : ℤ) ∧
      HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 6)) : ℤ) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 1)) : ℤ) + HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 3)) : ℤ) +
          2 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 4)) : ℤ)) ∧
    HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 4)) : ℤ) + 3 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 2)) : ℤ) +
          HMul.hMul (α := ℤ) 2 (if Even m then 6 else 0) ∧
      HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 1)) : ℤ) + 3 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 3)) : ℤ) +
          HMul.hMul (α := ℤ) 2 (if Even m then 0 else 6)
have repeat : ((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: repeat rw [expDegree_cast <| by lia]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
m : ℕ
⊢ ((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)
have 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)
Tactic: push_cast [Nat.even_add_one, ite_not, even_two_mul]
-- 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) ∧
      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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
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)
⊢ (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)
have 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)
Tactic: constructor
-- 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) ∧
    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 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
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 =
      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)
have 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)
Tactic: constructor
-- 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) ∧
    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 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
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)
⊢ 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)
have 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)
Tactic: constructor