-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (HPow.hPow (β := ℕ) p 2).degree = HSMul.hSMul (α := ℕ) 2 (some dp)
hp' : p.degree = some dp
dq : ℕ
hdq :
  (HPow.hPow (β := ℕ) q 2 *
        HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
          ((C : (a : R) → R[X]) W'.a₆ : R[X])).degree =
    HSMul.hSMul (α := ℕ) 2 (some dq) + 3
hdpq :
  (p * q *
        HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
          ((C : (a : R) → R[X]) W'.a₃ : R[X])).degree ≤
    some dp + some dq + 1
hq' : q.degree = some dq
hpq : dp ≤ dq + 1
h :
  HSMul.hSMul (α := ℕ) 2 (some dq) + 3 =
    (HPow.hPow (β := ℕ) q 2 *
        HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
          ((C : (a : R) → R[X]) W'.a₆ : R[X])).degree
neg :
  HSMul.hSMul (α := ℕ) 2 (some dp) <
    (HPow.hPow (β := ℕ) q 2 *
        HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
          ((C : (a : R) → R[X]) W'.a₆ : R[X])).degree
neg₁ :
  some dp + some dq + 1 <
    (HPow.hPow (β := ℕ) q 2 *
        HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
          ((C : (a : R) → R[X]) W'.a₆ : R[X])).degree
neg₂ :
  HSMul.hSMul (α := ℕ) 2 (some dp) <
    (HPow.hPow (β := ℕ) q 2 *
        HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
          ((C : (a : R) → R[X]) W'.a₆ : R[X])).degree
⊢ (HPow.hPow (β := ℕ) p 2 -
          p * q *
            HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
              ((C : (a : R) → R[X]) W'.a₃ : R[X]) -
        HPow.hPow (β := ℕ) q 2 *
          HAdd.hAdd (β := R[X])
            (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
                HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
              HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
            ((C : (a : R) → R[X]) W'.a₆ : R[X])).degree =
    max (HSMul.hSMul (α := ℕ) 2 (some dp)) (HSMul.hSMul (α := ℕ) 2 (some dq) + 3)

Tactic:
convert!
            (degree_sub_eq_right_of_degree_lt <|
                  (degree_sub_le _ _).trans_lt <|
                    max_lt_iff.mpr ⟨hdp.trans_lt _, hdpq.trans_lt _⟩).trans
              (max_eq_right_of_lt _).symm

Premises used: Iff.mpr, max_eq_right_of_lt, max_lt_iff, Polynomial.degree_sub_le, And.intro, Eq.trans_lt, Eq.symm, LE.le.trans_lt, Eq.trans, Polynomial.degree_sub_eq_right_of_degree_lt