awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
inst_2 : Algebra R S
A : Type u
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type v
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
n : ℤ
rw : Eq (α := B[X][Y]) ((W⁄B).φ n) (((W⁄A).map (↑f : A →+* B)).φ n)
⊢ Eq (α := B[X][Y]) ((W⁄B).φ n) (Polynomial.map (R := A[X]) (mapRingHom (↑f : A →+* B)) ((W⁄A).φ n))
have rw₁ : Eq (α := B[X][Y]) ((W⁄B).φ n) ((W⁄B).φ n)
Tactic: rw [← map_φ, map_baseChange]
-- 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])
        ((C : (a : R) → R[X]) 4 * HPow.hPow (α := R[X]) (β := ℕ) X 3 +
            HMul.hMul (α := 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]) (2 * W.b₄) : R[X]) X)
        ((C : (a : R) → R[X]) W.b₆ : R[X])).natDegree ≤
    3
have a : max (max (max (0 + HMul.hMul (α := ℕ) 3 1) (0 + HMul.hMul (α := ℕ) 2 1)) (HAdd.hAdd (α := ℕ) 0 1)) 0 ≤ 3
Tactic: compute_degree
-- 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])
          ((C : (a : R) → R[X]) 4 * HPow.hPow (α := R[X]) (β := ℕ) X 3 +
              HMul.hMul (α := 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]) (2 * W.b₄) : R[X]) X)
          ((C : (a : R) → R[X]) W.b₆ : R[X])).coeff
      3 =
    4
have rs : ((((if 3 = 0 + HMul.hMul (α := ℕ) 3 1 then
          (if Eq (α := ℕ) 0 0 then 4 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 3 = 0 + HMul.hMul (α := ℕ) 2 1 then
          (if Eq (α := ℕ) 0 0 then W.b₂ 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 3 = HAdd.hAdd (α := ℕ) 0 1 then (if Eq (α := ℕ) 0 0 then 2 * W.b₄ else 0) * if Eq (α := ℕ) 1 1 then 1 else 0
      else 0) +
    if Eq (α := ℕ) 3 0 then W.b₆ else 0) =
  4
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 3 = 0 + HMul.hMul (α := ℕ) 3 1 then
            (if Eq (α := ℕ) 0 0 then 4 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 3 = 0 + HMul.hMul (α := ℕ) 2 1 then
            (if Eq (α := ℕ) 0 0 then W.b₂ 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 3 = HAdd.hAdd (α := ℕ) 0 1 then (if Eq (α := ℕ) 0 0 then 2 * W.b₄ else 0) * if Eq (α := ℕ) 1 1 then 1 else 0
        else 0) +
      if Eq (α := ℕ) 3 0 then W.b₆ else 0) =
    4
⊢ (HAdd.hAdd (β := R[X])
          ((C : (a : R) → R[X]) 4 * HPow.hPow (α := R[X]) (β := ℕ) X 3 +
              HMul.hMul (α := 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]) (2 * W.b₄) : R[X]) X)
          ((C : (a : R) → R[X]) W.b₆ : R[X])).coeff
      3 =
    4
have h : HAdd.hAdd (α := ℕ) 0 1 ≤ 3
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 3 = 0 + HMul.hMul (α := ℕ) 3 1 then
            (if Eq (α := ℕ) 0 0 then 4 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 3 = 0 + HMul.hMul (α := ℕ) 2 1 then
            (if Eq (α := ℕ) 0 0 then W.b₂ 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 3 = HAdd.hAdd (α := ℕ) 0 1 then (if Eq (α := ℕ) 0 0 then 2 * W.b₄ else 0) * if Eq (α := ℕ) 1 1 then 1 else 0
        else 0) +
      if Eq (α := ℕ) 3 0 then W.b₆ else 0) =
    4
h : HAdd.hAdd (α := ℕ) 0 1 ≤ 3
⊢ (HAdd.hAdd (β := R[X])
          ((C : (a : R) → R[X]) 4 * HPow.hPow (α := R[X]) (β := ℕ) X 3 +
              HMul.hMul (α := 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]) (2 * W.b₄) : R[X]) X)
          ((C : (a : R) → R[X]) W.b₆ : R[X])).coeff
      3 =
    4
have h₁ : 0 + HMul.hMul (α := ℕ) 3 1 ≤ 3
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 3 = 0 + HMul.hMul (α := ℕ) 3 1 then
            (if Eq (α := ℕ) 0 0 then 4 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 3 = 0 + HMul.hMul (α := ℕ) 2 1 then
            (if Eq (α := ℕ) 0 0 then W.b₂ 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 3 = HAdd.hAdd (α := ℕ) 0 1 then (if Eq (α := ℕ) 0 0 then 2 * W.b₄ else 0) * if Eq (α := ℕ) 1 1 then 1 else 0
        else 0) +
      if Eq (α := ℕ) 3 0 then W.b₆ else 0) =
    4
h : HAdd.hAdd (α := ℕ) 0 1 ≤ 3
h₁ : 0 + HMul.hMul (α := ℕ) 3 1 ≤ 3
⊢ (HAdd.hAdd (β := R[X])
          ((C : (a : R) → R[X]) 4 * HPow.hPow (α := R[X]) (β := ℕ) X 3 +
              HMul.hMul (α := 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]) (2 * W.b₄) : R[X]) X)
          ((C : (a : R) → R[X]) W.b₆ : R[X])).coeff
      3 =
    4
have h₂ : 0 + HMul.hMul (α := ℕ) 2 1 ≤ 3
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 3 = 0 + HMul.hMul (α := ℕ) 3 1 then
            (if Eq (α := ℕ) 0 0 then 4 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 3 = 0 + HMul.hMul (α := ℕ) 2 1 then
            (if Eq (α := ℕ) 0 0 then W.b₂ 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 3 = HAdd.hAdd (α := ℕ) 0 1 then (if Eq (α := ℕ) 0 0 then 2 * W.b₄ else 0) * if Eq (α := ℕ) 1 1 then 1 else 0
        else 0) +
      if Eq (α := ℕ) 3 0 then W.b₆ else 0) =
    4
h : HAdd.hAdd (α := ℕ) 0 1 ≤ 3
h₁ : 0 + HMul.hMul (α := ℕ) 3 1 ≤ 3
h₂ : 0 + HMul.hMul (α := ℕ) 2 1 ≤ 3
h₃ : HMul.hMul (α := ℕ) 3 1 ≤ HMul.hMul (α := ℕ) 3 1
⊢ (HAdd.hAdd (β := R[X])
          ((C : (a : R) → R[X]) 4 * HPow.hPow (α := R[X]) (β := ℕ) X 3 +
              HMul.hMul (α := 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]) (2 * W.b₄) : R[X]) X)
          ((C : (a : R) → R[X]) W.b₆ : R[X])).coeff
      3 =
    4
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
h : Ne.{u + 1} (α := R) 4 0
⊢ leadingCoeff W.Ψ₂Sq = 4
have rw : coeff W.Ψ₂Sq (natDegree W.Ψ₂Sq) = 4
Tactic: rw [leadingCoeff, W.natDegree_Ψ₂Sq h, coeff_Ψ₂Sq]
-- 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) 4 0
rw : coeff W.Ψ₂Sq (natDegree W.Ψ₂Sq) = 4
⊢ leadingCoeff W.Ψ₂Sq = 4
have rw₁ : coeff W.Ψ₂Sq 3 = 4
Tactic: rw [leadingCoeff, W.natDegree_Ψ₂Sq h, coeff_Ψ₂Sq]
-- 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) 4 0
rw : coeff W.Ψ₂Sq (natDegree W.Ψ₂Sq) = 4
rw₁ : coeff W.Ψ₂Sq 3 = 4
⊢ leadingCoeff W.Ψ₂Sq = 4
have rw₂ : Eq.{u + 1} (α := R) 4 4
Tactic: rw [leadingCoeff, W.natDegree_Ψ₂Sq h, coeff_Ψ₂Sq]
-- 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])
        (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])).natDegree ≤
    4
have a : max
    (max
      (max (max (0 + HMul.hMul (α := ℕ) 4 1) (0 + HMul.hMul (α := ℕ) 3 1))
        (HAdd.hAdd (α := ℕ) 0 0 + HMul.hMul (α := ℕ) 2 1))
      (HAdd.hAdd (α := ℕ) 0 0 + 1))
    0 ≤
  4
Tactic: compute_degree
-- 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])
          (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 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
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
⊢ (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 : HAdd.hAdd (α := ℕ) 0 0 + 1 ≤ 4
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
⊢ (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₁ : HAdd.hAdd (α := ℕ) 0 0 + HMul.hMul (α := ℕ) 2 1 ≤ 4
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
⊢ (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₂ : 0 + HMul.hMul (α := ℕ) 4 1 ≤ 4
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
⊢ (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₃ : 0 + HMul.hMul (α := ℕ) 3 1 ≤ 4
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
⊢ (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₄ : HAdd.hAdd (α := ℕ) 0 0 ≤ HAdd.hAdd (α := ℕ) 0 0
Tactic: compute_degree!