-- 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 = 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:
by_cases hq : q = 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
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)

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)

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

Tactic:
have hdpq : (p * q * (C W.a₁ * X + C W.a₃)).degree ≤ p.degree + q.degree + 1 := by
  simpa only [degree_mul] using add_le_add_left degree_linear_le (p.degree + q.degree)

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

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

Tactic:
rw [norm_smul_basis]

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

Tactic:
simpa only [hp, hdq, neg_zero, zero_sub, zero_mul, zero_pow two_ne_zero, degree_neg] using
  (max_bot_left _).symm

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
⊢ ((Algebra.norm R[X]) (p • 1 + q • (mk W) Y)).degree = 2 • p.degree ⊔ (2 • q.degree + 3)

Tactic:
have hdp : (p ^ 2).degree = 2 • p.degree := degree_pow p 2

Result:
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
hdp : (p ^ 2).degree = 2 • p.degree
⊢ ((Algebra.norm R[X]) (p • 1 + q • (mk W) Y)).degree = 2 • p.degree ⊔ (2 • q.degree + 3)

Proof state:
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)

Tactic:
exact (hq hq').elim

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 : dq + 1 < dp
⊢ (fun x1 x2 => x1 + x2) (2 • dq) ↑3 < 2 • dp

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 : dq + 1 < dp
⊢ 2 * dq + 3 < 2 * dp