awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
rs :
  (((((if 4 = 0 + HMul.hMul (α := ℕ) 4 1 then
              (↑(if Eq (α := ℕ) 0 0 then 3 else 0) : R) *
                if HMul.hMul (α := ℕ) 4 1 = HMul.hMul (α := ℕ) 4 1 then
                  HPow.hPow (α := R) (β := ℕ) (if Eq (α := ℕ) 1 1 then 1 else 0) 4
                else 0
            else 0) +
            if 4 = 0 + HMul.hMul (α := ℕ) 3 1 then
              (if Eq (α := ℕ) 0 0 then W.b₂ else 0) *
                if HMul.hMul (α := ℕ) 3 1 = HMul.hMul (α := ℕ) 3 1 then
                  HPow.hPow (α := R) (β := ℕ) (if Eq (α := ℕ) 1 1 then 1 else 0) 3
                else 0
            else 0) +
          if 4 = HAdd.hAdd (α := ℕ) 0 0 + HMul.hMul (α := ℕ) 2 1 then
            (if HAdd.hAdd (α := ℕ) 0 0 = HAdd.hAdd (α := ℕ) 0 0 then
                (↑(if Eq (α := ℕ) 0 0 then 3 else 0) : R) * if Eq (α := ℕ) 0 0 then W.b₄ else 0
              else 0) *
              if HMul.hMul (α := ℕ) 2 1 = HMul.hMul (α := ℕ) 2 1 then
                HPow.hPow (α := R) (β := ℕ) (if Eq (α := ℕ) 1 1 then 1 else 0) 2
              else 0
          else 0) +
        if 4 = HAdd.hAdd (α := ℕ) 0 0 + 1 then
          (if HAdd.hAdd (α := ℕ) 0 0 = HAdd.hAdd (α := ℕ) 0 0 then
              (↑(if Eq (α := ℕ) 0 0 then 3 else 0) : R) * if Eq (α := ℕ) 0 0 then W.b₆ else 0
            else 0) *
            if Eq (α := ℕ) 1 1 then 1 else 0
        else 0) +
      if Eq (α := ℕ) 4 0 then W.b₈ else 0) =
    3
h : HAdd.hAdd (α := ℕ) 0 0 + 1 ≤ 4
h₁ : HAdd.hAdd (α := ℕ) 0 0 + HMul.hMul (α := ℕ) 2 1 ≤ 4
h₂ : 0 + HMul.hMul (α := ℕ) 4 1 ≤ 4
h₃ : 0 + HMul.hMul (α := ℕ) 3 1 ≤ 4
h₄ h₅ : HAdd.hAdd (α := ℕ) 0 0 ≤ HAdd.hAdd (α := ℕ) 0 0
⊢ (HAdd.hAdd (β := R[X])
          (3 * HPow.hPow (α := R[X]) (β := ℕ) X 4 +
                HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W.b₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
              HMul.hMul (α := R[X]) (β := R[X]) (3 : R[X]) ((C : (a : R) → R[X]) W.b₄ : R[X]) *
                HPow.hPow (α := R[X]) (β := ℕ) X 2 +
            HMul.hMul (α := R[X]) (β := R[X]) (3 : R[X]) ((C : (a : R) → R[X]) W.b₆ : R[X]) * X)
          ((C : (a : R) → R[X]) W.b₈ : R[X])).coeff
      4 =
    3
have h₆ : HMul.hMul (α := ℕ) 2 1 ≤ HMul.hMul (α := ℕ) 2 1
Tactic: compute_degree!
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
rs :
  (((((if 4 = 0 + HMul.hMul (α := ℕ) 4 1 then
              (↑(if Eq (α := ℕ) 0 0 then 3 else 0) : R) *
                if HMul.hMul (α := ℕ) 4 1 = HMul.hMul (α := ℕ) 4 1 then
                  HPow.hPow (α := R) (β := ℕ) (if Eq (α := ℕ) 1 1 then 1 else 0) 4
                else 0
            else 0) +
            if 4 = 0 + HMul.hMul (α := ℕ) 3 1 then
              (if Eq (α := ℕ) 0 0 then W.b₂ else 0) *
                if HMul.hMul (α := ℕ) 3 1 = HMul.hMul (α := ℕ) 3 1 then
                  HPow.hPow (α := R) (β := ℕ) (if Eq (α := ℕ) 1 1 then 1 else 0) 3
                else 0
            else 0) +
          if 4 = HAdd.hAdd (α := ℕ) 0 0 + HMul.hMul (α := ℕ) 2 1 then
            (if HAdd.hAdd (α := ℕ) 0 0 = HAdd.hAdd (α := ℕ) 0 0 then
                (↑(if Eq (α := ℕ) 0 0 then 3 else 0) : R) * if Eq (α := ℕ) 0 0 then W.b₄ else 0
              else 0) *
              if HMul.hMul (α := ℕ) 2 1 = HMul.hMul (α := ℕ) 2 1 then
                HPow.hPow (α := R) (β := ℕ) (if Eq (α := ℕ) 1 1 then 1 else 0) 2
              else 0
          else 0) +
        if 4 = HAdd.hAdd (α := ℕ) 0 0 + 1 then
          (if HAdd.hAdd (α := ℕ) 0 0 = HAdd.hAdd (α := ℕ) 0 0 then
              (↑(if Eq (α := ℕ) 0 0 then 3 else 0) : R) * if Eq (α := ℕ) 0 0 then W.b₆ else 0
            else 0) *
            if Eq (α := ℕ) 1 1 then 1 else 0
        else 0) +
      if Eq (α := ℕ) 4 0 then W.b₈ else 0) =
    3
h : HAdd.hAdd (α := ℕ) 0 0 + 1 ≤ 4
h₁ : HAdd.hAdd (α := ℕ) 0 0 + HMul.hMul (α := ℕ) 2 1 ≤ 4
h₂ : 0 + HMul.hMul (α := ℕ) 4 1 ≤ 4
h₃ : 0 + HMul.hMul (α := ℕ) 3 1 ≤ 4
h₄ h₅ : HAdd.hAdd (α := ℕ) 0 0 ≤ HAdd.hAdd (α := ℕ) 0 0
h₆ : HMul.hMul (α := ℕ) 2 1 ≤ HMul.hMul (α := ℕ) 2 1
h₇ : HMul.hMul (α := ℕ) 4 1 ≤ HMul.hMul (α := ℕ) 4 1
⊢ (HAdd.hAdd (β := R[X])
          (3 * HPow.hPow (α := R[X]) (β := ℕ) X 4 +
                HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W.b₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
              HMul.hMul (α := R[X]) (β := R[X]) (3 : R[X]) ((C : (a : R) → R[X]) W.b₄ : R[X]) *
                HPow.hPow (α := R[X]) (β := ℕ) X 2 +
            HMul.hMul (α := R[X]) (β := R[X]) (3 : R[X]) ((C : (a : R) → R[X]) W.b₆ : R[X]) * X)
          ((C : (a : R) → R[X]) W.b₈ : R[X])).coeff
      4 =
    3
have h₈ : HMul.hMul (α := ℕ) 3 1 ≤ HMul.hMul (α := ℕ) 3 1
Tactic: compute_degree!
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
h : Ne.{u + 1} (α := R) 3 0
⊢ leadingCoeff W.Ψ₃ = 3
have rw : coeff W.Ψ₃ (natDegree W.Ψ₃) = 3
Tactic: rw [leadingCoeff, W.natDegree_Ψ₃ h, coeff_Ψ₃]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
h : Ne.{u + 1} (α := R) 3 0
rw : coeff W.Ψ₃ (natDegree W.Ψ₃) = 3
⊢ leadingCoeff W.Ψ₃ = 3
have rw₁ : coeff W.Ψ₃ 4 = 3
Tactic: rw [leadingCoeff, W.natDegree_Ψ₃ h, coeff_Ψ₃]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
h : Ne.{u + 1} (α := R) 3 0
rw : coeff W.Ψ₃ (natDegree W.Ψ₃) = 3
rw₁ : coeff W.Ψ₃ 4 = 3
⊢ leadingCoeff W.Ψ₃ = 3
have rw₂ : Eq.{u + 1} (α := R) 3 3
Tactic: rw [leadingCoeff, W.natDegree_Ψ₃ h, coeff_Ψ₃]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
⊢ (HAdd.hAdd (β := R[X])
        (2 * HPow.hPow (α := R[X]) (β := ℕ) X 6 +
                  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W.b₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 5) +
                HMul.hMul (α := R[X]) (β := R[X]) (5 : R[X]) ((C : (a : R) → R[X]) W.b₄ : R[X]) *
                  HPow.hPow (α := R[X]) (β := ℕ) X 4 +
              HMul.hMul (α := R[X]) (β := R[X]) (10 : R[X]) ((C : (a : R) → R[X]) W.b₆ : R[X]) *
                HPow.hPow (α := R[X]) (β := ℕ) X 3 +
            HMul.hMul (α := R[X]) (β := R[X]) (10 : R[X]) ((C : (a : R) → R[X]) W.b₈ : R[X]) *
              HPow.hPow (α := R[X]) (β := ℕ) X 2 +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (W.b₂ * W.b₈ - W.b₄ * W.b₆) : R[X]) X)
        ((C : (a : R) → R[X]) (W.b₄ * W.b₈ - HPow.hPow (β := ℕ) W.b₆ 2) : R[X])).natDegree ≤
    6
have a : max
    (max
      (max
        (max
          (max (max (0 + HMul.hMul (α := ℕ) 6 1) (0 + HMul.hMul (α := ℕ) 5 1))
            (HAdd.hAdd (α := ℕ) 0 0 + HMul.hMul (α := ℕ) 4 1))
          (HAdd.hAdd (α := ℕ) 0 0 + HMul.hMul (α := ℕ) 3 1))
        (HAdd.hAdd (α := ℕ) 0 0 + HMul.hMul (α := ℕ) 2 1))
      (HAdd.hAdd (α := ℕ) 0 1))
    0 ≤
  6
Tactic: compute_degree
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
h : Ne.{u + 1} (α := R) 2 0
⊢ 0 < natDegree W.preΨ₄
have linarith : natDegree W.preΨ₄ ≤ 0 →
  HMul.hMul (α := ℤ) 6 (-1) + HSub.hSub (α := ℤ) (↑(natDegree W.preΨ₄) : ℤ) 0 +
      -HSub.hSub (α := ℤ) (↑(natDegree W.preΨ₄) : ℤ) 6 =
    0
Tactic: linarith only [W.natDegree_preΨ₄ h]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
h : Ne.{u + 1} (α := R) 2 0
linarith :
  natDegree W.preΨ₄ ≤ 0 →
    HMul.hMul (α := ℤ) 6 (-1) + HSub.hSub (α := ℤ) (↑(natDegree W.preΨ₄) : ℤ) 0 +
        -HSub.hSub (α := ℤ) (↑(natDegree W.preΨ₄) : ℤ) 6 =
      0
⊢ 0 < natDegree W.preΨ₄
have linarith₁ : natDegree W.preΨ₄ ≤ 0 → GT.gt (α := ℤ) 6 0
Tactic: linarith only [W.natDegree_preΨ₄ h]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
h : Ne.{u + 1} (α := R) 2 0
⊢ leadingCoeff W.preΨ₄ = 2
have rw : coeff W.preΨ₄ (natDegree W.preΨ₄) = 2
Tactic: rw [leadingCoeff, W.natDegree_preΨ₄ h, coeff_preΨ₄]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
h : Ne.{u + 1} (α := R) 2 0
rw : coeff W.preΨ₄ (natDegree W.preΨ₄) = 2
⊢ leadingCoeff W.preΨ₄ = 2
have rw₁ : coeff W.preΨ₄ 6 = 2
Tactic: rw [leadingCoeff, W.natDegree_preΨ₄ h, coeff_preΨ₄]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
h : Ne.{u + 1} (α := R) 2 0
rw : coeff W.preΨ₄ (natDegree W.preΨ₄) = 2
rw₁ : coeff W.preΨ₄ 6 = 2
⊢ leadingCoeff W.preΨ₄ = 2
have rw₂ : Eq.{u + 1} (α := R) 2 2
Tactic: rw [leadingCoeff, W.natDegree_preΨ₄ h, coeff_preΨ₄]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ HMul.hMul (α := ℤ) 2 (↑(expDegree n) : ℤ) = HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - if Even n then 4 else 1
have inl : ∀ (n : ℕ) (hn : 2 * n ≠ 0),
  HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * n)) : ℤ) =
    HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * n) : ℤ) 2 - if Even (2 * n) then 4 else 1
Tactic: rcases n.even_or_odd' with ⟨n, rfl | rfl⟩
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
n : ℕ
hn : n ≠ 0
inl :
  ∀ (n : ℕ) (hn : 2 * n ≠ 0),
    HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * n)) : ℤ) =
      HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * n) : ℤ) 2 - if Even (2 * n) then 4 else 1
⊢ HMul.hMul (α := ℤ) 2 (↑(expDegree n) : ℤ) = HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - if Even n then 4 else 1
have inr : ∀ (n : ℕ) (hn : 2 * n + 1 ≠ 0),
  HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * n + 1)) : ℤ) =
    HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * n + 1) : ℤ) 2 - if Even (2 * n + 1) then 4 else 1
Tactic: rcases n.even_or_odd' with ⟨n, rfl | rfl⟩
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
n : ℕ
hn : 2 * n ≠ 0
⊢ HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * n)) : ℤ) =
    HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * n) : ℤ) 2 - if Even (2 * n) then 4 else 1
have inl : ∀ (hn : HMul.hMul (α := ℕ) 2 0 ≠ 0),
  HMul.hMul (α := ℤ) 2 (↑(expDegree (HMul.hMul (α := ℕ) 2 0)) : ℤ) =
    HPow.hPow (α := ℤ) (β := ℕ) (↑(HMul.hMul (α := ℕ) 2 0) : ℤ) 2 - if Even (HMul.hMul (α := ℕ) 2 0) then 4 else 1
Tactic: rcases n with _ | n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
n : ℕ
hn : 2 * n ≠ 0
inl :
  ∀ (hn : HMul.hMul (α := ℕ) 2 0 ≠ 0),
    HMul.hMul (α := ℤ) 2 (↑(expDegree (HMul.hMul (α := ℕ) 2 0)) : ℤ) =
      HPow.hPow (α := ℤ) (β := ℕ) (↑(HMul.hMul (α := ℕ) 2 0) : ℤ) 2 - if Even (HMul.hMul (α := ℕ) 2 0) then 4 else 1
⊢ HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * n)) : ℤ) =
    HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * n) : ℤ) 2 - if Even (2 * n) then 4 else 1
have inl₁ : ∀ (n : ℕ) (hn : 2 * (n + 1) ≠ 0),
  HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * (n + 1))) : ℤ) =
    HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * (n + 1)) : ℤ) 2 - if Even (2 * (n + 1)) then 4 else 1
Tactic: rcases n with _ | n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
n : ℕ
hn : 2 * (n + 1) ≠ 0
⊢ HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * (n + 1))) : ℤ) =
    HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * (n + 1)) : ℤ) 2 - if Even (2 * (n + 1)) then 4 else 1
have inl : 2 * (HMul.hMul (α := ℤ) 2 (↑n : ℤ) * HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) =
  HPow.hPow (β := ℕ) (2 * HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) 2 - 4
Tactic: push_cast [expDegree, show (2 * (n + 1)) ^ 2 = 2 * (2 * n * (n + 2)) + 4 by ring1, even_two_mul,
      Nat.add_sub_cancel, Nat.mul_div_cancel_left _ two_pos]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
n : ℕ
hn : 2 * n + 1 ≠ 0
⊢ HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * n + 1)) : ℤ) =
    HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * n + 1) : ℤ) 2 - if Even (2 * n + 1) then 4 else 1
have inr : 2 * (HMul.hMul (α := ℤ) 2 (↑n : ℤ) * HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
  HPow.hPow (β := ℕ) (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 1) 2 - 1
Tactic: push_cast [expDegree, show (2 * n + 1) ^ 2 = 2 * (2 * n * (n + 1)) + 1 by ring1,
      n.not_even_two_mul_add_one, Nat.add_sub_cancel, Nat.mul_div_cancel_left _ two_pos]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
m : ℕ
⊢ (expDegree (2 * (m + 3)) = 2 * expDegree (m + 2) + expDegree (m + 3) + expDegree (m + 5) ∧
      expDegree (2 * (m + 3)) = expDegree (m + 1) + expDegree (m + 3) + 2 * expDegree (m + 4)) ∧
    (expDegree (2 * (m + 2) + 1) =
        expDegree (m + 4) + 3 * expDegree (m + 2) + if Even m then HMul.hMul (α := ℕ) 2 3 else 0) ∧
      expDegree (2 * (m + 2) + 1) =
        expDegree (m + 1) + 3 * expDegree (m + 3) + if Even m then 0 else HMul.hMul (α := ℕ) 2 3
have push_cast : (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)
Tactic: push_cast [← @Nat.cast_inj ℤ, ← mul_left_cancel_iff_of_pos (b := (expDegree _ : ℤ)) two_pos,
    mul_add, mul_left_comm (2 : ℤ)]
-- 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 rw : ((HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 6) : ℤ) 2 - if Even (2 * m + 6) then 4 else 1) =
      2 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 2)) : ℤ) + HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 3)) : ℤ) +
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 5)) : ℤ) ∧
    (HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 6) : ℤ) 2 - if Even (2 * m + 6) then 4 else 1) =
      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)
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 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 2)) : ℤ) + HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 3)) : ℤ) +
          HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 5)) : ℤ) ∧
      (HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 6) : ℤ) 2 - if Even (2 * m + 6) then 4 else 1) =
        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 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) +
          HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 3)) : ℤ) +
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 5)) : ℤ) ∧
    (HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 6) : ℤ) 2 - if Even (2 * m + 6) then 4 else 1) =
      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 * (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 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 3)) : ℤ) +
        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) +
            HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 3)) : ℤ) +
          HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 5)) : ℤ) ∧
      (HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 6) : ℤ) 2 - if Even (2 * m + 6) then 4 else 1) =
        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 * (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 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 3)) : ℤ) +
          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) +
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 5)) : ℤ) ∧
    (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)
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) +
          HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 5)) : ℤ) ∧
      (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) =
      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)
Tactic: rw [expDegree_cast <| by lia]