-- Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean
lemma degree_norm_smul_basis [IsDomain R] (p q : R[X]) :
    (Algebra.norm R[X] <| p • (1 : W.CoordinateRing) + q • mk W Y).degree =
      max (2 • p.degree) (2 • q.degree + 3)

Proof state:
case neg.some
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
hdq : (q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)).degree = 2 • q.degree + 3
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdpq : (p * q * (C W.a₁ * X + C W.a₃)).degree ≤ some dp + q.degree + 1
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
⊢ (p ^ 2 - p * q * (C W.a₁ * X + C W.a₃) - q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)).degree =
    2 • some dp ⊔ (2 • q.degree + 3)

Tactic:
rcases hq' : q.degree with _ | dq

Result:
case neg.some.none
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
hdq : (q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)).degree = 2 • q.degree + 3
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdpq : (p * q * (C W.a₁ * X + C W.a₃)).degree ≤ some dp + q.degree + 1
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
hq' : q.degree = none
⊢ (p ^ 2 - p * q * (C W.a₁ * X + C W.a₃) - q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)).degree =
    2 • some dp ⊔ (2 • none + 3)

case neg.some.some
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
hdq : (q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)).degree = 2 • q.degree + 3
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdpq : (p * q * (C W.a₁ * X + C W.a₃)).degree ≤ some dp + q.degree + 1
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hq' : q.degree = some dq
⊢ (p ^ 2 - p * q * (C W.a₁ * X + C W.a₃) - q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)).degree =
    2 • some dp ⊔ (2 • some dq + 3)

Proof state:
case neg.some.some.inr
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W.a₁ * X + C W.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dq + 1 < dp
⊢ (p ^ 2 - (p * q * (C W.a₁ * X + C W.a₃) + q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆))).degree =
    2 • some dp ⊔ (2 • some dq + 3)

Tactic:
convert (degree_sub_eq_left_of_degree_lt <| (degree_add_le _ _).trans_lt <|
          max_lt_iff.mpr ⟨hdpq.trans_lt _, hdq.trans_lt _⟩).trans
  (max_eq_left_of_lt _).symm <;> rw [hdp] <;>
    exact WithBot.coe_lt_coe.mpr <| by dsimp; linarith only [hpq]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W.a₁ * X + C W.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dp ≤ dq + 1
⊢ 2 • dp < (fun x1 x2 => x1 + x2) (2 • dq) ↑3

Tactic:
dsimp

Result:
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W.a₁ * X + C W.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dp ≤ dq + 1
⊢ 2 * dp < 2 * dq + 3

Proof state:
case neg.none
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
hdp : (p ^ 2).degree = 2 • p.degree
hdpq : (p * q * (C W.a₁ * X + C W.a₃)).degree ≤ p.degree + q.degree + 1
hdq : (q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)).degree = 2 • q.degree + 3
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
hp' : p.degree = none
⊢ (p ^ 2 - p * q * (C W.a₁ * X + C W.a₃) - q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)).degree =
    2 • none ⊔ (2 • q.degree + 3)

Tactic:
exact (hp hp').elim

Result:
no goals

Proof state:
case neg.some.some
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W.a₁ * X + C W.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
⊢ (p ^ 2 - p * q * (C W.a₁ * X + C W.a₃) - q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)).degree =
    2 • some dp ⊔ (2 • some dq + 3)

Tactic:
rcases le_or_lt dp (dq + 1) with hpq | hpq

Result:
case neg.some.some.inl
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W.a₁ * X + C W.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dp ≤ dq + 1
⊢ (p ^ 2 - p * q * (C W.a₁ * X + C W.a₃) - q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)).degree =
    2 • some dp ⊔ (2 • some dq + 3)

case neg.some.some.inr
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W.a₁ * X + C W.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dq + 1 < dp
⊢ (p ^ 2 - p * q * (C W.a₁ * X + C W.a₃) - q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)).degree =
    2 • some dp ⊔ (2 • some dq + 3)

Proof state:
case neg
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
hdp : (p ^ 2).degree = 2 • p.degree
hdpq : (p * q * (C W.a₁ * X + C W.a₃)).degree ≤ p.degree + q.degree + 1
hdq : (q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)).degree = 2 • q.degree + 3
hp : ¬p = 0
hq : ¬q = 0
⊢ (p ^ 2 - p * q * (C W.a₁ * X + C W.a₃) - q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)).degree =
    2 • p.degree ⊔ (2 • q.degree + 3)

Tactic:
rw [← not_congr degree_eq_bot] at hp hq

Result:
case neg
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
hdp : (p ^ 2).degree = 2 • p.degree
hdpq : (p * q * (C W.a₁ * X + C W.a₃)).degree ≤ p.degree + q.degree + 1
hdq : (q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)).degree = 2 • q.degree + 3
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
⊢ (p ^ 2 - p * q * (C W.a₁ * X + C W.a₃) - q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)).degree =
    2 • p.degree ⊔ (2 • q.degree + 3)

Proof state:
case neg.some
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
hdp : (p ^ 2).degree = 2 • p.degree
hdpq : (p * q * (C W.a₁ * X + C W.a₃)).degree ≤ p.degree + q.degree + 1
hdq : (q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)).degree = 2 • q.degree + 3
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hp' : p.degree = some dp
⊢ (p ^ 2 - p * q * (C W.a₁ * X + C W.a₃) - q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)).degree =
    2 • some dp ⊔ (2 • q.degree + 3)

Tactic:
rw [hp'] at hdp hdpq

Result:
case neg.some
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
hdq : (q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)).degree = 2 • q.degree + 3
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdpq : (p * q * (C W.a₁ * X + C W.a₃)).degree ≤ some dp + q.degree + 1
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
⊢ (p ^ 2 - p * q * (C W.a₁ * X + C W.a₃) - q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)).degree =
    2 • some dp ⊔ (2 • q.degree + 3)