-- 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
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)

Tactic:
rcases hp' : p.degree with _ | dp

Result:
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)

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)

Proof state:
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
⊢ ((Algebra.norm R[X]) (p • 1 + q • (mk W) Y)).degree = 2 • p.degree ⊔ (2 • q.degree + 3)

Tactic:
have hdq :
    (q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)).degree = 2 • q.degree + 3 := by
  rw [degree_mul, degree_pow, ← one_mul <| X ^ 3, ← C_1, degree_cubic <| one_ne_zero' R]

Result:
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
⊢ ((Algebra.norm R[X]) (p • 1 + q • (mk W) Y)).degree = 2 • p.degree ⊔ (2 • q.degree + 3)

Proof state:
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
hdp : (p ^ 2).degree = 2 • p.degree
⊢ (p * q * (C W.a₁ * X + C W.a₃)).degree ≤ p.degree + q.degree + 1

Tactic:
simpa only [degree_mul] using add_le_add_left degree_linear_le (p.degree + q.degree)

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 < 2 * dq + 3

Tactic:
linarith only [hpq]

Result:
no goals

Proof state:
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
⊢ (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:
by_cases hp : p = 0

Result:
case pos
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
⊢ (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)

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
⊢ (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.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)

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 <;> rw [hdq] <;>
    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]
hdp : (p ^ 2).degree = 2 • p.degree
hdpq : (p * q * (C W.a₁ * X + C W.a₃)).degree ≤ p.degree + q.degree + 1
⊢ (q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)).degree = 2 • q.degree + 3

Tactic:
rw [degree_mul, degree_pow, ← one_mul <| X ^ 3, ← C_1, degree_cubic <| one_ne_zero' R]

Result:
no goals

Proof state:
case pos
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:
simpa only [hq, hdp, sub_zero, zero_mul, mul_zero, zero_pow two_ne_zero] using
  (max_bot_right _).symm

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]
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)

Tactic:
rw [hq'] at hdpq hdq

Result:
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)