awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EffectiveEpi
Goal:
X Y : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
π : X ⟶ Y
inst_2 : Surjective π
inst_3 : Flat π
this_1 : Epi π
Z : Scheme
f : X ⟶ Z
hf : Eq (α := pullback π π ⟶ Z) (pullback.fst π π ≫ f) (pullback.snd π π ≫ f)
𝒰 : Y.OpenCover
u : (i : 𝒰.I₀) → 𝒰.X i ⟶ Z
hfac : ∀ (i : 𝒰.I₀), Eq (α := pullback π (𝒰.f i) ⟶ Z) (pullback.fst π (𝒰.f i) ≫ f) (pullback.snd π (𝒰.f i) ≫ u i)
i j : 𝒰.I₀
this :
  Epi (X := pullback (Y := pullback (𝒰.f i) (𝒰.f j)) π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
    (pullback.snd π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
⊢ Eq (α := pullback (Y := pullback (𝒰.f i) (𝒰.f j)) π (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j) ⟶ Z)
    (CategoryStruct.comp (Y := pullback (Y := pullback (𝒰.f i) (𝒰.f j)) π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
        (Iso.hom (pullback.congrHom ⋯ ⋯) :
          pullback (Y := pullback (𝒰.f i) (𝒰.f j)) π (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j) ⟶
            pullback (Y := pullback (𝒰.f i) (𝒰.f j)) π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
        (CategoryStruct.comp (Y :=
            pullback (X := pullback π (𝒰.f i)) (Y := pullback (𝒰.f i) (𝒰.f j)) (pullback.snd π (𝒰.f i))
              (pullback.fst (𝒰.f i) (𝒰.f j)))
            (Iso.inv (pullbackLeftPullbackSndIso π (𝒰.f i) (pullback.fst (𝒰.f i) (𝒰.f j))))
            (pullback.fst (pullback.snd π (𝒰.f i)) (pullback.fst (𝒰.f i) (𝒰.f j)) ≫ pullback.fst π (𝒰.f i) ≫ f) :
          pullback (Y := pullback (𝒰.f i) (𝒰.f j)) π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) ⟶ Z) :
      pullback (Y := pullback (𝒰.f i) (𝒰.f j)) π (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j) ⟶ Z)
    (CategoryStruct.comp (Y :=
        pullback (X := pullback π (𝒰.f j)) (Y := pullback (𝒰.f i) (𝒰.f j)) (pullback.snd π (𝒰.f j))
          (pullback.snd (𝒰.f i) (𝒰.f j)))
        (Iso.inv (pullbackLeftPullbackSndIso π (𝒰.f j) (pullback.snd (𝒰.f i) (𝒰.f j))))
        (pullback.fst (pullback.snd π (𝒰.f j)) (pullback.snd (𝒰.f i) (𝒰.f j)) ≫ pullback.fst π (𝒰.f j) ≫ f) :
      pullback (Y := pullback (𝒰.f i) (𝒰.f j)) π (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j) ⟶ Z)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.EffectiveEpi
Goal:
X Y : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
π : X ⟶ Y
inst_2 : Surjective π
inst_3 : Flat π
this : Epi π
Z : Scheme
f : X ⟶ Z
hf : Eq (α := pullback π π ⟶ Z) (pullback.fst π π ≫ f) (pullback.snd π π ≫ f)
𝒰 : Y.OpenCover
u : (i : 𝒰.I₀) → 𝒰.X i ⟶ Z
hfac : ∀ (i : 𝒰.I₀), Eq (α := pullback π (𝒰.f i) ⟶ Z) (pullback.fst π (𝒰.f i) ≫ f) (pullback.snd π (𝒰.f i) ≫ u i)
refine_2 :
  ∀ (x : (Precoverage.ZeroHypercover.pullback₁ π 𝒰).I₀),
    (Precoverage.ZeroHypercover.pullback₁ π 𝒰).f x ≫ π ≫ Cover.glueMorphisms 𝒰 u ⋯ =
      (Precoverage.ZeroHypercover.pullback₁ π 𝒰).f x ≫ f
⊢ π ≫ Cover.glueMorphisms 𝒰 u ⋯ = f

Tactic:
apply Cover.hom_ext (𝒰.pullback₁ π)

Premises used: CategoryTheory.Precoverage.ZeroHypercover.pullback₁, AlgebraicGeometry.Scheme.Cover.hom_ext
-- Module: Mathlib.AlgebraicGeometry.EffectiveEpi
Goal:
X Y : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
π : X ⟶ Y
inst_2 : Surjective π
inst_3 : Flat π
this : Epi π
Z : Scheme
f : X ⟶ Z
hf : Eq (α := pullback π π ⟶ Z) (pullback.fst π π ≫ f) (pullback.snd π π ≫ f)
𝒰 : Y.OpenCover
u : (i : 𝒰.I₀) → 𝒰.X i ⟶ Z
hfac : ∀ (i : 𝒰.I₀), Eq (α := pullback π (𝒰.f i) ⟶ Z) (pullback.fst π (𝒰.f i) ≫ f) (pullback.snd π (𝒰.f i) ≫ u i)
i : (Precoverage.ZeroHypercover.pullback₁ π 𝒰).I₀
⊢ (Precoverage.ZeroHypercover.pullback₁ π 𝒰).f i ≫ π ≫ Cover.glueMorphisms 𝒰 u ⋯ =
    (Precoverage.ZeroHypercover.pullback₁ π 𝒰).f i ≫ f

Tactic:
simp [pullback.condition_assoc, hfac]

Premises used: CategoryTheory.Limits.pullback.condition_assoc
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
simp_rw :
  HSub.hSub (β := R[X][Y])
      (HPow.hPow (α := R[X][Y]) (β := ℕ) Y 2 +
        HMul.hMul (α := R[X][Y]) (β := R[X][Y])
          ((C : (a : R[X]) → R[X][Y])
              (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W.a₁ : R[X]) X)
                ((C : (a : R) → R[X]) W.a₃ : R[X])) :
            R[X][Y])
          Y)
      ((C : (a : R[X]) → R[X][Y])
          (HAdd.hAdd (β := R[X])
            (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
                HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
              HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W.a₄ : R[X]) X)
            ((C : (a : R) → R[X]) W.a₆ : R[X])) :
        R[X][Y]) =
    HAdd.hAdd (β := R[X][Y])
      ((C : (a : R[X]) → R[X][Y]) 0 * HPow.hPow (α := R[X][Y]) (β := ℕ) Y 3 +
          (C : (a : R[X]) → R[X][Y]) 1 * HPow.hPow (α := R[X][Y]) (β := ℕ) Y 2 +
        HMul.hMul (α := R[X][Y]) (β := R[X][Y])
          ((C : (a : R[X]) → R[X][Y])
              (HAdd.hAdd (β := R[X])
                ((C : (a : R) → R[X]) 0 * HPow.hPow (α := R[X]) (β := ℕ) X 3 +
                    (C : (a : R) → R[X]) 0 * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
                  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W.a₁ : R[X]) X)
                ((C : (a : R) → R[X]) W.a₃ : R[X])) :
            R[X][Y])
          Y)
      ((C : (a : R[X]) → R[X][Y])
          (HAdd.hAdd (β := R[X])
            ((C : (a : R) → R[X]) (-1) * HPow.hPow (α := R[X]) (β := ℕ) X 3 +
                HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (-W.a₂) : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
              HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (-W.a₄) : R[X]) X)
            ((C : (a : R) → R[X]) (-W.a₆) : R[X])) :
        R[X][Y])
⊢ Eq (α := R[X][Y]) W.polynomial
    (Cubic.toPoly
      { a := 0, b := 1, c := { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly,
        d := { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ }.toPoly })

Tactic:
simp_rw [polynomial, Cubic.toPoly]

Premises used: Cubic.toPoly, WeierstrassCurve.Affine.polynomial
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
⊢ HPow.hPow (α := R[X][Y]) (β := ℕ) Y 2 +
        HAdd.hAdd (β := R[X][Y])
            (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.a₁) : R[X][Y])
              ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]))
            ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.a₃) : R[X][Y]) *
          Y -
      HAdd.hAdd (β := R[X][Y])
        (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) 3 +
            HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.a₂) : R[X][Y])
              (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) 2) +
          HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.a₄) : R[X][Y])
            ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]))
        ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.a₆) : R[X][Y]) =
    0 * HPow.hPow (α := R[X][Y]) (β := ℕ) Y 3 + 1 * HPow.hPow (α := R[X][Y]) (β := ℕ) Y 2 +
        HAdd.hAdd (β := R[X][Y])
            (0 * HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) 3 +
                0 * HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) 2 +
              HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.a₁) : R[X][Y])
                ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]))
            ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.a₃) : R[X][Y]) *
          Y +
      HAdd.hAdd (β := R[X][Y])
        (-1 * HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) 3 +
            HMul.hMul (α := R[X][Y]) (-(C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.a₂) : R[X][Y])
              (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) 2) +
          HMul.hMul (α := R[X][Y]) (β := R[X][Y]) (-(C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.a₄) : R[X][Y])
            ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]))
        (-(C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.a₆) : R[X][Y])

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : Nontrivial R
rw :
  Ne (α := R[X][Y])
    (Cubic.toPoly
      { a := 0, b := 1, c := { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly,
        d := { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ }.toPoly })
    0
⊢ Ne (α := R[X][Y]) W.polynomial 0

Tactic:
rw [polynomial_eq]

Premises used: WeierstrassCurve.Affine.polynomial_eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : Nontrivial R
⊢ Ne (α := R[X][Y])
    (Cubic.toPoly
      { a := 0, b := 1, c := { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly,
        d := { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ }.toPoly })
    0

Tactic:
Cubic.ne_zero_of_b_ne_zero one_ne_zero

Premises used: Cubic.ne_zero_of_b_ne_zero, one_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : Nontrivial R
⊢ Ne (α := R[X][Y])
    (Cubic.toPoly
      { a := 0, b := 1, c := { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly,
        d := { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ }.toPoly })
    0

Tactic:
exact Cubic.ne_zero_of_b_ne_zero one_ne_zero

Premises used: Cubic.ne_zero_of_b_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : Nontrivial R
rw :
  degree (R := R[X])
      (Cubic.toPoly
        { a := 0, b := 1, c := { a := 0, b := 0, c := W.a₁, d := W.a₃ : Cubic R }.toPoly,
          d := { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ : Cubic R }.toPoly : Cubic R[X] }) =
    2
⊢ degree (R := R[X]) W.polynomial = 2

Tactic:
rw [polynomial_eq]

Premises used: WeierstrassCurve.Affine.polynomial_eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : Nontrivial R
⊢ degree (R := R[X])
      (Cubic.toPoly
        { a := 0, b := 1, c := { a := 0, b := 0, c := W.a₁, d := W.a₃ : Cubic R }.toPoly,
          d := { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ : Cubic R }.toPoly : Cubic R[X] }) =
    2

Tactic:
Cubic.degree_of_b_ne_zero' one_ne_zero

Premises used: Cubic.degree_of_b_ne_zero', one_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : Nontrivial R
⊢ degree (R := R[X])
      (Cubic.toPoly
        { a := 0, b := 1, c := { a := 0, b := 0, c := W.a₁, d := W.a₃ : Cubic R }.toPoly,
          d := { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ : Cubic R }.toPoly : Cubic R[X] }) =
    2

Tactic:
exact Cubic.degree_of_b_ne_zero' one_ne_zero

Premises used: Cubic.degree_of_b_ne_zero', one_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : Nontrivial R
rw :
  natDegree (R := R[X])
      (Cubic.toPoly
        { a := 0, b := 1, c := { a := 0, b := 0, c := W.a₁, d := W.a₃ : Cubic R }.toPoly,
          d := { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ : Cubic R }.toPoly : Cubic R[X] }) =
    2
⊢ natDegree (R := R[X]) W.polynomial = 2

Tactic:
rw [polynomial_eq]

Premises used: WeierstrassCurve.Affine.polynomial_eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : Nontrivial R
⊢ natDegree (R := R[X])
      (Cubic.toPoly
        { a := 0, b := 1, c := { a := 0, b := 0, c := W.a₁, d := W.a₃ : Cubic R }.toPoly,
          d := { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ : Cubic R }.toPoly : Cubic R[X] }) =
    2

Tactic:
Cubic.natDegree_of_b_ne_zero' one_ne_zero

Premises used: Cubic.natDegree_of_b_ne_zero', one_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : Nontrivial R
⊢ natDegree (R := R[X])
      (Cubic.toPoly
        { a := 0, b := 1, c := { a := 0, b := 0, c := W.a₁, d := W.a₃ : Cubic R }.toPoly,
          d := { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ : Cubic R }.toPoly : Cubic R[X] }) =
    2

Tactic:
exact Cubic.natDegree_of_b_ne_zero' one_ne_zero

Premises used: Cubic.natDegree_of_b_ne_zero', one_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
⊢ Monic (R := R[X]) W.polynomial

Tactic:
simpa only [polynomial_eq] using Cubic.monic_of_b_eq_one'

Premises used: WeierstrassCurve.Affine.polynomial_eq, Cubic.monic_of_b_eq_one'
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : IsDomain R
by_contra : ∀ (h : ¬Irreducible (M := R[X][Y]) W.polynomial), False
⊢ Irreducible (M := R[X][Y]) W.polynomial

Tactic:
by_contra h
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : IsDomain R
h : ¬Irreducible (M := R[X][Y]) W.polynomial
rcases : ∀ (f g : R[X]) (h0 : coeff W.polynomial 0 = f * g) (h1 : coeff W.polynomial 1 = f + g), False
⊢ False

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

Premises used: WeierstrassCurve.Affine.monic_polynomial, WeierstrassCurve.Affine.natDegree_polynomial, Iff.mp, Polynomial.Monic.not_irreducible_iff_exists_add_mul_eq_coeff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : IsDomain R
h : ¬Irreducible (M := R[X][Y]) W.polynomial
f g : R[X]
h0 : coeff W.polynomial 0 = f * g
h1 : coeff W.polynomial 1 = f + g
⊢ { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ }.toPoly = f * g

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

Premises used: Cubic.coeff_eq_c, WeierstrassCurve.Affine.polynomial_eq, Cubic.coeff_eq_d
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : IsDomain R
h : ¬Irreducible (M := R[X][Y]) W.polynomial
f g : R[X]
h0 : coeff W.polynomial 0 = f * g
h1 : coeff W.polynomial 1 = f + g
h0₁ : { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ }.toPoly = f * g
⊢ { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly = f + g

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

Premises used: Cubic.coeff_eq_c, WeierstrassCurve.Affine.polynomial_eq, Cubic.coeff_eq_d
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : IsDomain R
h : ¬Irreducible (M := R[X][Y]) 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
⊢ degree { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ : Cubic R }.toPoly = (f * g).degree

Tactic:
apply_fun degree at h0 h1

Premises used: Polynomial.degree
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : IsDomain R
h : ¬Irreducible (M := R[X][Y]) 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
h0₁ : degree { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ : Cubic R }.toPoly = (f * g).degree
⊢ degree { a := 0, b := 0, c := W.a₁, d := W.a₃ : Cubic R }.toPoly = (f + g).degree

Tactic:
apply_fun degree at h0 h1

Premises used: Polynomial.degree
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : IsDomain R
h : ¬Irreducible (M := R[X][Y]) W.polynomial
f g : R[X]
h0 : degree { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ : Cubic R }.toPoly = (f * g).degree
h1 : degree { a := 0, b := 0, c := W.a₁, d := W.a₃ : Cubic R }.toPoly = (f + g).degree
⊢ 3 = f.degree + g.degree

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

Premises used: Iff.mpr, one_ne_zero', Cubic.degree_of_a_ne_zero', neg_ne_zero, Polynomial.degree_mul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : IsDomain R
h : ¬Irreducible (M := R[X][Y]) W.polynomial
f g : R[X]
h0 : degree { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ : Cubic R }.toPoly = (f * g).degree
h1 : degree { a := 0, b := 0, c := W.a₁, d := W.a₃ : Cubic R }.toPoly = (f + g).degree
h0₁ : 3 = f.degree + g.degree
⊢ degree { a := 0, b := 0, c := W.a₁, d := W.a₃ : Cubic R }.toPoly = (f + g).degree

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

Premises used: Iff.mpr, one_ne_zero', Cubic.degree_of_a_ne_zero', neg_ne_zero, Polynomial.degree_mul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : IsDomain R
h : ¬Irreducible (M := R[X][Y]) W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : degree { a := 0, b := 0, c := W.a₁, d := W.a₃ : Cubic R }.toPoly = (f + g).degree
apply : 1 < (f + g).degree
⊢ False

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

Premises used: Eq.le, LE.le.not_gt, Cubic.degree_of_b_eq_zero', LE.le.trans, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : IsDomain R
h : ¬Irreducible (M := R[X][Y]) W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : degree { a := 0, b := 0, c := W.a₁, d := W.a₃ : Cubic R }.toPoly = (f + g).degree
inl : ∀ (h : f.degree = 0 ∧ g.degree = 3), 1 < (f + g).degree
inr : ∀ (h : f.degree = 1 ∧ g.degree = 2), 1 < (f + g).degree
inr₁ : ∀ (h : f.degree = 2 ∧ g.degree = 1), 1 < (f + g).degree
inr₂ : ∀ (h : f.degree = 3 ∧ g.degree = 0), 1 < (f + g).degree
⊢ 1 < (f + g).degree

Tactic:
rcases Nat.WithBot.add_eq_three_iff.mp h0.symm with h | h | h | h

Premises used: Nat.WithBot.add_eq_three_iff, Iff.mp, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : IsDomain R
h_1 : ¬Irreducible (M := R[X][Y]) W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : degree { a := 0, b := 0, c := W.a₁, d := W.a₃ : Cubic R }.toPoly = (f + g).degree
h : f.degree = 0 ∧ g.degree = 3
inl : 1 < g.degree
inl₁ : f.degree < g.degree
⊢ 1 < (f + g).degree

Tactic:
rw [degree_add_eq_right_of_degree_lt]

Premises used: Polynomial.degree_add_eq_right_of_degree_lt
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : IsDomain R
h_1 : ¬Irreducible (M := R[X][Y]) W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : degree { a := 0, b := 0, c := W.a₁, d := W.a₃ : Cubic R }.toPoly = (f + g).degree
h : f.degree = 0 ∧ g.degree = 3
inl : LT.lt (α := WithBot ℕ) 1 3
⊢ 1 < g.degree

Tactic:
simp only [h]
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : IsDomain R
h_1 : ¬Irreducible (M := R[X][Y]) W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : degree { a := 0, b := 0, c := W.a₁, d := W.a₃ : Cubic R }.toPoly = (f + g).degree
h : f.degree = 0 ∧ g.degree = 3
inl : LT.lt (α := WithBot ℕ) 0 3
⊢ f.degree < g.degree

Tactic:
simp only [h]
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : IsDomain R
h_1 : ¬Irreducible (M := R[X][Y]) W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : degree { a := 0, b := 0, c := W.a₁, d := W.a₃ : Cubic R }.toPoly = (f + g).degree
h : f.degree = 0 ∧ g.degree = 3
⊢ LT.lt (α := WithBot ℕ) 1 3

Tactic:
decide
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : IsDomain R
h_1 : ¬Irreducible (M := R[X][Y]) W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : degree { a := 0, b := 0, c := W.a₁, d := W.a₃ : Cubic R }.toPoly = (f + g).degree
h : f.degree = 0 ∧ g.degree = 3
⊢ LT.lt (α := WithBot ℕ) 0 3

Tactic:
decide
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : IsDomain R
h_1 : ¬Irreducible (M := R[X][Y]) W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : degree { a := 0, b := 0, c := W.a₁, d := W.a₃ : Cubic R }.toPoly = (f + g).degree
h : f.degree = 1 ∧ g.degree = 2
inr : 1 < g.degree
inr₁ : f.degree < g.degree
⊢ 1 < (f + g).degree

Tactic:
rw [degree_add_eq_right_of_degree_lt]

Premises used: Polynomial.degree_add_eq_right_of_degree_lt
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : IsDomain R
h_1 : ¬Irreducible (M := R[X][Y]) W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : degree { a := 0, b := 0, c := W.a₁, d := W.a₃ : Cubic R }.toPoly = (f + g).degree
h : f.degree = 1 ∧ g.degree = 2
inr : LT.lt (α := WithBot ℕ) 1 2
⊢ 1 < g.degree

Tactic:
simp only [h]
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : IsDomain R
h_1 : ¬Irreducible (M := R[X][Y]) W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : degree { a := 0, b := 0, c := W.a₁, d := W.a₃ : Cubic R }.toPoly = (f + g).degree
h : f.degree = 1 ∧ g.degree = 2
inr : LT.lt (α := WithBot ℕ) 1 2
⊢ f.degree < g.degree

Tactic:
simp only [h]
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : IsDomain R
h_1 : ¬Irreducible (M := R[X][Y]) W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : degree { a := 0, b := 0, c := W.a₁, d := W.a₃ : Cubic R }.toPoly = (f + g).degree
h : f.degree = 1 ∧ g.degree = 2
⊢ LT.lt (α := WithBot ℕ) 1 2

Tactic:
decide
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : IsDomain R
h_1 : ¬Irreducible (M := R[X][Y]) W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : degree { a := 0, b := 0, c := W.a₁, d := W.a₃ : Cubic R }.toPoly = (f + g).degree
h : f.degree = 2 ∧ g.degree = 1
inr : 1 < f.degree
inr₁ : g.degree < f.degree
⊢ 1 < (f + g).degree

Tactic:
rw [degree_add_eq_left_of_degree_lt]

Premises used: Polynomial.degree_add_eq_left_of_degree_lt
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : IsDomain R
h_1 : ¬Irreducible (M := R[X][Y]) W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : degree { a := 0, b := 0, c := W.a₁, d := W.a₃ : Cubic R }.toPoly = (f + g).degree
h : f.degree = 2 ∧ g.degree = 1
inr : LT.lt (α := WithBot ℕ) 1 2
⊢ 1 < f.degree

Tactic:
simp only [h]
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : IsDomain R
h_1 : ¬Irreducible (M := R[X][Y]) W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : degree { a := 0, b := 0, c := W.a₁, d := W.a₃ : Cubic R }.toPoly = (f + g).degree
h : f.degree = 2 ∧ g.degree = 1
inr : LT.lt (α := WithBot ℕ) 1 2
⊢ g.degree < f.degree

Tactic:
simp only [h]
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : IsDomain R
h_1 : ¬Irreducible (M := R[X][Y]) W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : degree { a := 0, b := 0, c := W.a₁, d := W.a₃ : Cubic R }.toPoly = (f + g).degree
h : f.degree = 2 ∧ g.degree = 1
⊢ LT.lt (α := WithBot ℕ) 1 2

Tactic:
decide
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : IsDomain R
h_1 : ¬Irreducible (M := R[X][Y]) W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : degree { a := 0, b := 0, c := W.a₁, d := W.a₃ : Cubic R }.toPoly = (f + g).degree
h : f.degree = 3 ∧ g.degree = 0
inr : 1 < f.degree
inr₁ : g.degree < f.degree
⊢ 1 < (f + g).degree

Tactic:
rw [degree_add_eq_left_of_degree_lt]

Premises used: Polynomial.degree_add_eq_left_of_degree_lt