-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma irreducible_polynomial [IsDomain R] : Irreducible W'.polynomial

Proof state:
case intro.intro.intro.inr.inl
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W'.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W'.a₁, d := W'.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 1 ∧ g.degree = 2
⊢ 1 < (f + g).degree

case intro.intro.intro.inr.inr.inl
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W'.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W'.a₁, d := W'.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 2 ∧ g.degree = 1
⊢ 1 < (f + g).degree

case intro.intro.intro.inr.inr.inr
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W'.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W'.a₁, d := W'.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 3 ∧ g.degree = 0
⊢ 1 < (f + g).degree

Tactic:
rw [degree_add_eq_right_of_degree_lt] <;> simp only [h] <;> decide

Result:
case intro.intro.intro.inr.inr.inl
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W'.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W'.a₁, d := W'.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 2 ∧ g.degree = 1
⊢ 1 < (f + g).degree

case intro.intro.intro.inr.inr.inr
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W'.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W'.a₁, d := W'.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 3 ∧ g.degree = 0
⊢ 1 < (f + g).degree

Proof state:
case intro.intro.intro
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
h : ¬Irreducible W'.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W'.a₁, d := W'.a₃ }.toPoly.degree = (f + g).degree
⊢ False

Tactic:
apply (h1.symm.le.trans Cubic.degree_of_b_eq_zero').not_lt

Result:
case intro.intro.intro
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
h : ¬Irreducible W'.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W'.a₁, d := W'.a₃ }.toPoly.degree = (f + g).degree
⊢ 1 < (f + g).degree

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
⊢ Irreducible W'.polynomial

Tactic:
by_contra h

Result:
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
h : ¬Irreducible W'.polynomial
⊢ False

Proof state:
case intro.intro.intro
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
h : ¬Irreducible W'.polynomial
f g : R[X]
h0 : { a := -1, b := -W'.a₂, c := -W'.a₄, d := -W'.a₆ }.toPoly = f * g
h1 : { a := 0, b := 0, c := W'.a₁, d := W'.a₃ }.toPoly = f + g
⊢ False

Tactic:
apply_fun degree at h0 h1

Result:
case intro.intro.intro
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
h : ¬Irreducible W'.polynomial
f g : R[X]
h0 : { a := -1, b := -W'.a₂, c := -W'.a₄, d := -W'.a₆ }.toPoly.degree = (f * g).degree
h1 : { a := 0, b := 0, c := W'.a₁, d := W'.a₃ }.toPoly.degree = (f + g).degree
⊢ False

Proof state:
case intro.intro.intro.inr.inr.inl
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W'.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W'.a₁, d := W'.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 2 ∧ g.degree = 1
⊢ 1 < (f + g).degree

case intro.intro.intro.inr.inr.inr
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W'.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W'.a₁, d := W'.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 3 ∧ g.degree = 0
⊢ 1 < (f + g).degree

Tactic:
iterate 2 rw [degree_add_eq_left_of_degree_lt] <;> simp only [h] <;> decide

Result:
no goals

Proof state:
case intro.intro.intro
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
h : ¬Irreducible W'.polynomial
f g : R[X]
h0 : W'.polynomial.coeff 0 = f * g
h1 : W'.polynomial.coeff 1 = f + g
⊢ False

Tactic:
simp only [polynomial_eq, Cubic.coeff_eq_c, Cubic.coeff_eq_d] at h0 h1

Result:
case intro.intro.intro
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
h : ¬Irreducible W'.polynomial
f g : R[X]
h0 : { a := -1, b := -W'.a₂, c := -W'.a₄, d := -W'.a₆ }.toPoly = f * g
h1 : { a := 0, b := 0, c := W'.a₁, d := W'.a₃ }.toPoly = f + g
⊢ False

Proof state:
case intro.intro.intro.inr.inr.inr
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W'.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W'.a₁, d := W'.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 3 ∧ g.degree = 0
⊢ 1 < (f + g).degree

Tactic:
rw [degree_add_eq_left_of_degree_lt] <;> simp only [h] <;> decide

Result:
no goals

Proof state:
case intro.intro.intro
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
h : ¬Irreducible W'.polynomial
f g : R[X]
h0 : { a := -1, b := -W'.a₂, c := -W'.a₄, d := -W'.a₆ }.toPoly.degree = (f * g).degree
h1 : { a := 0, b := 0, c := W'.a₁, d := W'.a₃ }.toPoly.degree = (f + g).degree
⊢ False

Tactic:
rw [Cubic.degree_of_a_ne_zero' <| neg_ne_zero.mpr <| one_ne_zero' R, degree_mul] at h0

Result:
case intro.intro.intro
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
h : ¬Irreducible W'.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W'.a₁, d := W'.a₃ }.toPoly.degree = (f + g).degree
⊢ False

Proof state:
case intro.intro.intro.inl
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W'.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W'.a₁, d := W'.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 0 ∧ g.degree = 3
⊢ 1 < (f + g).degree

case intro.intro.intro.inr.inl
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W'.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W'.a₁, d := W'.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 1 ∧ g.degree = 2
⊢ 1 < (f + g).degree

case intro.intro.intro.inr.inr.inl
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W'.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W'.a₁, d := W'.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 2 ∧ g.degree = 1
⊢ 1 < (f + g).degree

case intro.intro.intro.inr.inr.inr
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W'.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W'.a₁, d := W'.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 3 ∧ g.degree = 0
⊢ 1 < (f + g).degree

Tactic:
iterate 2 rw [degree_add_eq_right_of_degree_lt] <;> simp only [h] <;> decide

Result:
case intro.intro.intro.inr.inr.inl
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W'.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W'.a₁, d := W'.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 2 ∧ g.degree = 1
⊢ 1 < (f + g).degree

case intro.intro.intro.inr.inr.inr
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W'.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W'.a₁, d := W'.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 3 ∧ g.degree = 0
⊢ 1 < (f + g).degree

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
h : ¬Irreducible W'.polynomial
⊢ False

Tactic:
rcases (monic_polynomial.not_irreducible_iff_exists_add_mul_eq_coeff natDegree_polynomial).mp h
  with ⟨f, g, h0, h1⟩

Result:
case intro.intro.intro
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
h : ¬Irreducible W'.polynomial
f g : R[X]
h0 : W'.polynomial.coeff 0 = f * g
h1 : W'.polynomial.coeff 1 = f + g
⊢ False