awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EffectiveEpi (goal)
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)
⊢ π ≫ Cover.glueMorphisms 𝒰 u ⋯ = f
have refine_2 : ∀ (x : (Precoverage.ZeroHypercover.pullback₁ π 𝒰).I₀),
  (Precoverage.ZeroHypercover.pullback₁ π 𝒰).f x ≫ π ≫ Cover.glueMorphisms 𝒰 u sorry =
    (Precoverage.ZeroHypercover.pullback₁ π 𝒰).f x ≫ f
Tactic: apply Cover.hom_ext (𝒰.pullback₁ π)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
⊢ 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 })
have 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])
Tactic: simp_rw [polynomial, Cubic.toPoly]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : Nontrivial R
⊢ Ne (α := R[X][Y]) W.polynomial 0
have 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
Tactic: rw [polynomial_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : Nontrivial R
⊢ degree (R := R[X]) W.polynomial = 2
have 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
Tactic: rw [polynomial_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : Nontrivial R
⊢ natDegree (R := R[X]) W.polynomial = 2
have 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
Tactic: rw [polynomial_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : IsDomain R
⊢ Irreducible (M := R[X][Y]) W.polynomial
have by_contra : ∀ (h : ¬Irreducible (M := R[X][Y]) W.polynomial), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : IsDomain R
h : ¬Irreducible (M := R[X][Y]) W.polynomial
⊢ False
have rcases : ∀ (f g : R[X]) (h0 : coeff W.polynomial 0 = f * g) (h1 : coeff W.polynomial 1 = f + g), False
Tactic: rcases (monic_polynomial.not_irreducible_iff_exists_add_mul_eq_coeff natDegree_polynomial).mp h
    with ⟨f, g, h0, h1⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (hypothesis)
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
⊢ False
have h0₁ : { 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
Cleared hypotheses: h0, h1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (hypothesis)
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
⊢ False
have h1₁ : { 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
Cleared hypotheses: h0, h1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (hypothesis)
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
⊢ False
have h0₁ : 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
Cleared hypotheses: h0, h1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (hypothesis)
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
⊢ False
have h1₁ : degree { a := 0, b := 0, c := W.a₁, d := W.a₃ : Cubic R }.toPoly = (f + g).degree
Tactic: apply_fun degree at h0 h1
Cleared hypotheses: h0, h1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (hypothesis)
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
⊢ False
have h0₁ : 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
Cleared hypotheses: h0, h1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
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
⊢ False
have apply : 1 < (f + g).degree
Tactic: apply (h1.symm.le.trans Cubic.degree_of_b_eq_zero').not_gt
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
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
⊢ 1 < (f + g).degree
have inl : ∀ (h : f.degree = 0 ∧ g.degree = 3), 1 < (f + g).degree
Tactic: rcases Nat.WithBot.add_eq_three_iff.mp h0.symm with h | h | h | h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
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
⊢ 1 < (f + g).degree
have inr : ∀ (h : f.degree = 1 ∧ g.degree = 2), 1 < (f + g).degree
Tactic: rcases Nat.WithBot.add_eq_three_iff.mp h0.symm with h | h | h | h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
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
⊢ 1 < (f + g).degree
have inr₁ : ∀ (h : f.degree = 2 ∧ g.degree = 1), 1 < (f + g).degree
Tactic: rcases Nat.WithBot.add_eq_three_iff.mp h0.symm with h | h | h | h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
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
⊢ 1 < (f + g).degree
have inr₂ : ∀ (h : f.degree = 3 ∧ g.degree = 0), 1 < (f + g).degree
Tactic: rcases Nat.WithBot.add_eq_three_iff.mp h0.symm with h | h | h | h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
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
⊢ 1 < (f + g).degree
have inl : 1 < g.degree
Tactic: rw [degree_add_eq_right_of_degree_lt]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
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
⊢ 1 < (f + g).degree
have inl₁ : f.degree < g.degree
Tactic: rw [degree_add_eq_right_of_degree_lt]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
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
⊢ 1 < g.degree
have inl : LT.lt (α := WithBot ℕ) 1 3
Tactic: simp only [h]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
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
⊢ f.degree < g.degree
have inl : LT.lt (α := WithBot ℕ) 0 3
Tactic: simp only [h]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
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
⊢ 1 < (f + g).degree
have inr : 1 < g.degree
Tactic: rw [degree_add_eq_right_of_degree_lt]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
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
⊢ 1 < (f + g).degree
have inr₁ : f.degree < g.degree
Tactic: rw [degree_add_eq_right_of_degree_lt]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
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
⊢ 1 < g.degree
have inr : LT.lt (α := WithBot ℕ) 1 2
Tactic: simp only [h]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
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
⊢ f.degree < g.degree
have inr : LT.lt (α := WithBot ℕ) 1 2
Tactic: simp only [h]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
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
⊢ 1 < (f + g).degree
have inr : 1 < f.degree
Tactic: rw [degree_add_eq_left_of_degree_lt]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
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
⊢ 1 < (f + g).degree
have inr₁ : g.degree < f.degree
Tactic: rw [degree_add_eq_left_of_degree_lt]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
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
⊢ 1 < f.degree
have inr : LT.lt (α := WithBot ℕ) 1 2
Tactic: simp only [h]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
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
⊢ g.degree < f.degree
have inr : LT.lt (α := WithBot ℕ) 1 2
Tactic: simp only [h]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
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
⊢ 1 < (f + g).degree
have inr : 1 < f.degree
Tactic: rw [degree_add_eq_left_of_degree_lt]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
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
⊢ 1 < (f + g).degree
have inr₁ : g.degree < f.degree
Tactic: rw [degree_add_eq_left_of_degree_lt]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
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
⊢ 1 < f.degree
have inr : LT.lt (α := WithBot ℕ) 1 3
Tactic: simp only [h]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
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
⊢ g.degree < f.degree
have inr : LT.lt (α := WithBot ℕ) 0 3
Tactic: simp only [h]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
⊢ evalEval x y
      (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])) =
    HPow.hPow (β := ℕ) y 2 + W.a₁ * x * y + W.a₃ * y -
      (HPow.hPow (β := ℕ) x 3 + W.a₂ * HPow.hPow (β := ℕ) x 2 + W.a₄ * x + W.a₆)
have eval_simp : HPow.hPow (β := ℕ) y 2 + (W.a₁ * x + W.a₃) * y -
    (HPow.hPow (β := ℕ) x 3 + W.a₂ * HPow.hPow (β := ℕ) x 2 + W.a₄ * x + W.a₆) =
  HPow.hPow (β := ℕ) y 2 + W.a₁ * x * y + W.a₃ * y -
    (HPow.hPow (β := ℕ) x 3 + W.a₂ * HPow.hPow (β := ℕ) x 2 + W.a₄ * x + W.a₆)
Tactic: eval_simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
⊢ HPow.hPow (β := ℕ) y 2 + (W.a₁ * x + W.a₃) * y -
      (HPow.hPow (β := ℕ) x 3 + W.a₂ * HPow.hPow (β := ℕ) x 2 + W.a₄ * x + W.a₆) =
    HPow.hPow (β := ℕ) y 2 + W.a₁ * x * y + W.a₃ * y -
      (HPow.hPow (β := ℕ) x 3 + W.a₂ * HPow.hPow (β := ℕ) x 2 + W.a₄ * x + W.a₆)
have rw : HPow.hPow (β := ℕ) y 2 + (W.a₁ * x * y + W.a₃ * y) -
    (HPow.hPow (β := ℕ) x 3 + W.a₂ * HPow.hPow (β := ℕ) x 2 + W.a₄ * x + W.a₆) =
  HPow.hPow (β := ℕ) y 2 + W.a₁ * x * y + W.a₃ * y -
    (HPow.hPow (β := ℕ) x 3 + W.a₂ * HPow.hPow (β := ℕ) x 2 + W.a₄ * x + W.a₆)
Tactic: rw [add_mul, ← add_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
rw :
  HPow.hPow (β := ℕ) y 2 + (W.a₁ * x * y + W.a₃ * y) -
      (HPow.hPow (β := ℕ) x 3 + W.a₂ * HPow.hPow (β := ℕ) x 2 + W.a₄ * x + W.a₆) =
    HPow.hPow (β := ℕ) y 2 + W.a₁ * x * y + W.a₃ * y -
      (HPow.hPow (β := ℕ) x 3 + W.a₂ * HPow.hPow (β := ℕ) x 2 + W.a₄ * x + W.a₆)
⊢ HPow.hPow (β := ℕ) y 2 + (W.a₁ * x + W.a₃) * y -
      (HPow.hPow (β := ℕ) x 3 + W.a₂ * HPow.hPow (β := ℕ) x 2 + W.a₄ * x + W.a₆) =
    HPow.hPow (β := ℕ) y 2 + W.a₁ * x * y + W.a₃ * y -
      (HPow.hPow (β := ℕ) x 3 + W.a₂ * HPow.hPow (β := ℕ) x 2 + W.a₄ * x + W.a₆)
have rw₁ : HPow.hPow (β := ℕ) y 2 + W.a₁ * x * y + W.a₃ * y -
    (HPow.hPow (β := ℕ) x 3 + W.a₂ * HPow.hPow (β := ℕ) x 2 + W.a₄ * x + W.a₆) =
  HPow.hPow (β := ℕ) y 2 + W.a₁ * x * y + W.a₃ * y -
    (HPow.hPow (β := ℕ) x 3 + W.a₂ * HPow.hPow (β := ℕ) x 2 + W.a₄ * x + W.a₆)
Tactic: rw [add_mul, ← add_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
⊢ W.Equation x y ↔
    HPow.hPow (β := ℕ) y 2 + W.a₁ * x * y + W.a₃ * y -
        (HPow.hPow (β := ℕ) x 3 + W.a₂ * HPow.hPow (β := ℕ) x 2 + W.a₄ * x + W.a₆) =
      0
have rw : evalEval x y W.polynomial = 0 ↔
  HPow.hPow (β := ℕ) y 2 + W.a₁ * x * y + W.a₃ * y -
      (HPow.hPow (β := ℕ) x 3 + W.a₂ * HPow.hPow (β := ℕ) x 2 + W.a₄ * x + W.a₆) =
    0
Tactic: rw [Equation, evalEval_polynomial]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
rw :
  evalEval x y W.polynomial = 0 ↔
    HPow.hPow (β := ℕ) y 2 + W.a₁ * x * y + W.a₃ * y -
        (HPow.hPow (β := ℕ) x 3 + W.a₂ * HPow.hPow (β := ℕ) x 2 + W.a₄ * x + W.a₆) =
      0
⊢ W.Equation x y ↔
    HPow.hPow (β := ℕ) y 2 + W.a₁ * x * y + W.a₃ * y -
        (HPow.hPow (β := ℕ) x 3 + W.a₂ * HPow.hPow (β := ℕ) x 2 + W.a₄ * x + W.a₆) =
      0
have rw₁ : HPow.hPow (β := ℕ) y 2 + W.a₁ * x * y + W.a₃ * y -
      (HPow.hPow (β := ℕ) x 3 + W.a₂ * HPow.hPow (β := ℕ) x 2 + W.a₄ * x + W.a₆) =
    0 ↔
  HPow.hPow (β := ℕ) y 2 + W.a₁ * x * y + W.a₃ * y -
      (HPow.hPow (β := ℕ) x 3 + W.a₂ * HPow.hPow (β := ℕ) x 2 + W.a₄ * x + W.a₆) =
    0
Tactic: rw [Equation, evalEval_polynomial]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
⊢ W.Equation x y ↔
    HPow.hPow (β := ℕ) y 2 + W.a₁ * x * y + W.a₃ * y =
      HPow.hPow (β := ℕ) x 3 + W.a₂ * HPow.hPow (β := ℕ) x 2 + W.a₄ * x + W.a₆
have rw : HPow.hPow (β := ℕ) y 2 + W.a₁ * x * y + W.a₃ * y -
      (HPow.hPow (β := ℕ) x 3 + W.a₂ * HPow.hPow (β := ℕ) x 2 + W.a₄ * x + W.a₆) =
    0 ↔
  HPow.hPow (β := ℕ) y 2 + W.a₁ * x * y + W.a₃ * y =
    HPow.hPow (β := ℕ) x 3 + W.a₂ * HPow.hPow (β := ℕ) x 2 + W.a₄ * x + W.a₆
Tactic: rw [equation_iff', sub_eq_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
rw :
  HPow.hPow (β := ℕ) y 2 + W.a₁ * x * y + W.a₃ * y -
        (HPow.hPow (β := ℕ) x 3 + W.a₂ * HPow.hPow (β := ℕ) x 2 + W.a₄ * x + W.a₆) =
      0 ↔
    HPow.hPow (β := ℕ) y 2 + W.a₁ * x * y + W.a₃ * y =
      HPow.hPow (β := ℕ) x 3 + W.a₂ * HPow.hPow (β := ℕ) x 2 + W.a₄ * x + W.a₆
⊢ W.Equation x y ↔
    HPow.hPow (β := ℕ) y 2 + W.a₁ * x * y + W.a₃ * y =
      HPow.hPow (β := ℕ) x 3 + W.a₂ * HPow.hPow (β := ℕ) x 2 + W.a₄ * x + W.a₆
have rw₁ : HPow.hPow (β := ℕ) y 2 + W.a₁ * x * y + W.a₃ * y =
    HPow.hPow (β := ℕ) x 3 + W.a₂ * HPow.hPow (β := ℕ) x 2 + W.a₄ * x + W.a₆ ↔
  HPow.hPow (β := ℕ) y 2 + W.a₁ * x * y + W.a₃ * y =
    HPow.hPow (β := ℕ) x 3 + W.a₂ * HPow.hPow (β := ℕ) x 2 + W.a₄ * x + W.a₆
Tactic: rw [equation_iff', sub_eq_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
⊢ W.Equation 0 0 ↔ W.a₆ = 0
have rw : evalEval 0 0 W.polynomial = 0 ↔ W.a₆ = 0
Tactic: rw [Equation, evalEval_polynomial_zero, neg_eq_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
rw : evalEval 0 0 W.polynomial = 0 ↔ W.a₆ = 0
⊢ W.Equation 0 0 ↔ W.a₆ = 0
have rw₁ : -W.a₆ = 0 ↔ W.a₆ = 0
Tactic: rw [Equation, evalEval_polynomial_zero, neg_eq_zero]