-- Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean
lemma degree_norm_ne_one [IsDomain R] (x : W.CoordinateRing) :
    (Algebra.norm R[X] x).degree ≠ 1

Proof state:
case intro.intro
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
⊢ 2 • p.degree ⊔ (2 • q.degree + 3) ≠ 1

Tactic:
rcases p.degree with (_ | _ | _ | _) <;> cases q.degree

Result:
case intro.intro.none.bot
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
⊢ 2 • none ⊔ (2 • ⊥ + 3) ≠ 1

case intro.intro.none.coe
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
a✝ : ℕ
⊢ 2 • none ⊔ (2 • ↑a✝ + 3) ≠ 1

case intro.intro.some.zero.bot
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
⊢ 2 • some 0 ⊔ (2 • ⊥ + 3) ≠ 1

case intro.intro.some.zero.coe
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
a✝ : ℕ
⊢ 2 • some 0 ⊔ (2 • ↑a✝ + 3) ≠ 1

case intro.intro.some.succ.zero.bot
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
⊢ 2 • some (0 + 1) ⊔ (2 • ⊥ + 3) ≠ 1

case intro.intro.some.succ.zero.coe
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
a✝ : ℕ
⊢ 2 • some (0 + 1) ⊔ (2 • ↑a✝ + 3) ≠ 1

case intro.intro.some.succ.succ.bot
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
n✝ : ℕ
⊢ 2 • some (n✝ + 1 + 1) ⊔ (2 • ⊥ + 3) ≠ 1

case intro.intro.some.succ.succ.coe
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
n✝ a✝ : ℕ
⊢ 2 • some (n✝ + 1 + 1) ⊔ (2 • ↑a✝ + 3) ≠ 1

Proof state:
case intro.intro.none.bot
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
⊢ 2 • none ⊔ (2 • ⊥ + 3) ≠ 1

case intro.intro.none.coe
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
a✝ : ℕ
⊢ 2 • none ⊔ (2 • ↑a✝ + 3) ≠ 1

case intro.intro.some.zero.bot
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
⊢ 2 • some 0 ⊔ (2 • ⊥ + 3) ≠ 1

case intro.intro.some.zero.coe
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
a✝ : ℕ
⊢ 2 • some 0 ⊔ (2 • ↑a✝ + 3) ≠ 1

case intro.intro.some.succ.zero.bot
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
⊢ 2 • some (0 + 1) ⊔ (2 • ⊥ + 3) ≠ 1

case intro.intro.some.succ.zero.coe
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
a✝ : ℕ
⊢ 2 • some (0 + 1) ⊔ (2 • ↑a✝ + 3) ≠ 1

case intro.intro.some.succ.succ.bot
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
n✝ : ℕ
⊢ 2 • some (n✝ + 1 + 1) ⊔ (2 • ⊥ + 3) ≠ 1

case intro.intro.some.succ.succ.coe
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
n✝ a✝ : ℕ
⊢ 2 • some (n✝ + 1 + 1) ⊔ (2 • ↑a✝ + 3) ≠ 1

Tactic:
any_goals rintro (_ | _)

Result:
case intro.intro.some.succ.succ.coe
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
n✝ a✝ : ℕ
⊢ 2 • some (n✝ + 1 + 1) ⊔ (2 • ↑a✝ + 3) ≠ 1

Proof state:
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
n✝ a✝ : ℕ
⊢ 1 < 2 • ↑a✝ + 3

Tactic:
exact (cmp_eq_lt_iff ..).mp rfl

Result:
no goals

Proof state:
case intro.intro
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 ≠ 1

Tactic:
rw [degree_norm_smul_basis]

Result:
case intro.intro
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
⊢ 2 • p.degree ⊔ (2 • q.degree + 3) ≠ 1

Proof state:
case intro.intro.some.succ.succ.coe
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
n✝ a✝ : ℕ
⊢ 2 • some (n✝ + 1 + 1) ⊔ (2 • ↑a✝ + 3) ≠ 1

Tactic:
rintro (_ | _)

Result:
no goals

Proof state:
case intro.intro.some.succ.succ.coe
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
n✝ a✝ : ℕ
⊢ 2 • some (n✝ + 1 + 1) ⊔ (2 • ↑a✝ + 3) ≠ 1

Tactic:
exact (lt_max_of_lt_right <| by exact (cmp_eq_lt_iff ..).mp rfl).ne'

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
x : W.CoordinateRing
⊢ ((Algebra.norm R[X]) x).degree ≠ 1

Tactic:
rcases exists_smul_basis_eq x with ⟨p, q, rfl⟩

Result:
case intro.intro
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 ≠ 1