-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
rs :
  (((((((if 6 = 0 + HMul.hMul (α := ℕ) 6 1 then
                  (↑(if Eq (α := ℕ) 0 0 then 2 else 0) : R) *
                    if HMul.hMul (α := ℕ) 6 1 = HMul.hMul (α := ℕ) 6 1 then
                      HPow.hPow (α := R) (β := ℕ) (if Eq (α := ℕ) 1 1 then 1 else 0) 6
                    else 0
                else 0) +
                if 6 = 0 + HMul.hMul (α := ℕ) 5 1 then
                  (if Eq (α := ℕ) 0 0 then W.b₂ else 0) *
                    if HMul.hMul (α := ℕ) 5 1 = HMul.hMul (α := ℕ) 5 1 then
                      HPow.hPow (α := R) (β := ℕ) (if Eq (α := ℕ) 1 1 then 1 else 0) 5
                    else 0
                else 0) +
              if 6 = HAdd.hAdd (α := ℕ) 0 0 + HMul.hMul (α := ℕ) 4 1 then
                (if HAdd.hAdd (α := ℕ) 0 0 = HAdd.hAdd (α := ℕ) 0 0 then
                    (↑(if Eq (α := ℕ) 0 0 then 5 else 0) : R) * if Eq (α := ℕ) 0 0 then W.b₄ else 0
                  else 0) *
                  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 6 = HAdd.hAdd (α := ℕ) 0 0 + HMul.hMul (α := ℕ) 3 1 then
              (if HAdd.hAdd (α := ℕ) 0 0 = HAdd.hAdd (α := ℕ) 0 0 then
                  (↑(if Eq (α := ℕ) 0 0 then 10 else 0) : R) * if Eq (α := ℕ) 0 0 then W.b₆ else 0
                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 6 = HAdd.hAdd (α := ℕ) 0 0 + HMul.hMul (α := ℕ) 2 1 then
            (if HAdd.hAdd (α := ℕ) 0 0 = HAdd.hAdd (α := ℕ) 0 0 then
                (↑(if Eq (α := ℕ) 0 0 then 10 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 6 = HAdd.hAdd (α := ℕ) 0 1 then
          (if Eq (α := ℕ) 0 0 then W.b₂ * W.b₈ - W.b₄ * W.b₆ else 0) * if Eq (α := ℕ) 1 1 then 1 else 0
        else 0) +
      if Eq (α := ℕ) 6 0 then W.b₄ * W.b₈ - HPow.hPow (β := ℕ) W.b₆ 2 else 0) =
    2
h : HAdd.hAdd (α := ℕ) 0 1 ≤ 6
h₁ : HAdd.hAdd (α := ℕ) 0 0 + HMul.hMul (α := ℕ) 2 1 ≤ 6
h₂ : HAdd.hAdd (α := ℕ) 0 0 + HMul.hMul (α := ℕ) 3 1 ≤ 6
h₃ : HAdd.hAdd (α := ℕ) 0 0 + HMul.hMul (α := ℕ) 4 1 ≤ 6
h₄ : HAdd.hAdd (α := ℕ) 0 0 ≤ HAdd.hAdd (α := ℕ) 0 0
h₅ : HMul.hMul (α := ℕ) 2 1 ≤ HMul.hMul (α := ℕ) 2 1
h₆ : 0 + HMul.hMul (α := ℕ) 6 1 ≤ 6
h₇ : 0 + HMul.hMul (α := ℕ) 5 1 ≤ 6
h₈ : HAdd.hAdd (α := ℕ) 0 0 ≤ HAdd.hAdd (α := ℕ) 0 0
⊢ (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])).coeff
      6 =
    2
have h₉ : HMul.hMul (α := ℕ) 3 1 ≤ HMul.hMul (α := ℕ) 3 1
Tactic: compute_degree!