awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (hypothesis)
Goal:
F : Type u
inst : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
⊢ HMul.hMul (α := Ideal W.CoordinateRing) (XYIdeal W x ((C : (a : F) → F[X]) (W.negY x y)))
      (XYIdeal W x ((C : (a : F) → F[X]) y)) =
    XIdeal W x
have Y_rw : HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) y) : F[X][Y]) *
      HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y
        ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (W.negY x y)) : F[X][Y]) -
    HMul.hMul (α := F[X][Y])
      ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x : F[X])) : F[X][Y])
      (HSub.hSub (α := F[X][Y])
        ((C : (a : F[X]) → F[X][Y])
            (HAdd.hAdd (β := F[X])
              (HPow.hPow (α := F[X]) (β := ℕ) X 2 +
                HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (x + W.a₂) : F[X]) X)
              ((C : (a : F) → F[X]) (HPow.hPow (β := ℕ) x 2 + W.a₂ * x + W.a₄) : F[X])) :
          F[X][Y])
        (HMul.hMul (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₁) : F[X][Y])
          Y)) =
  HMul.hMul (α := F[X][Y]) W.polynomial 1
Tactic: have Y_rw : (Y - C (C y)) * (Y - C (C <| W.negY x y)) -
      C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
        W.polynomial * 1 := by
    linear_combination (norm := (rw [negY, polynomial]; C_simp; ring1))
      congr_arg C (congr_arg C ((equation_iff ..).mp h.left).symm)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
F : Type u
inst : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
Y_rw :
  HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) y) : F[X][Y]) *
        HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y
          ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (W.negY x y)) : F[X][Y]) -
      HMul.hMul (α := F[X][Y])
        ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x : F[X])) : F[X][Y])
        (HSub.hSub (α := F[X][Y])
          ((C : (a : F[X]) → F[X][Y])
              (HAdd.hAdd (β := F[X])
                (HPow.hPow (α := F[X]) (β := ℕ) X 2 +
                  HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (x + W.a₂) : F[X]) X)
                ((C : (a : F) → F[X]) (HPow.hPow (β := ℕ) x 2 + W.a₂ * x + W.a₄) : F[X])) :
            F[X][Y])
          (HMul.hMul (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₁) : F[X][Y])
            Y)) =
    HMul.hMul (α := F[X][Y]) W.polynomial 1
⊢ Eq (α := Ideal F[X][Y])
    (span
      (insert (α := F[X][Y])
        ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x : F[X])) : F[X][Y])
        {HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) y) : F[X][Y]),
          HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y
            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (W.negY x y)) : F[X][Y]),
          HSub.hSub (α := F[X][Y])
            ((C : (a : F[X]) → F[X][Y])
                (HAdd.hAdd (β := F[X])
                  (HPow.hPow (α := F[X]) (β := ℕ) X 2 +
                    HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (x + W.a₂) : F[X]) X)
                  ((C : (a : F) → F[X]) (HPow.hPow (β := ℕ) x 2 + W.a₂ * x + W.a₄) : F[X])) :
              F[X][Y])
            (HMul.hMul (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₁) : F[X][Y])
              Y)}))
    ⊤
have h₁ : ∃ (a : F[X][Y]) (a_1 : F[X][Y]) (a_2 : F[X][Y]) (a_3 : F[X][Y]),
  a_3 *
      HSub.hSub (α := F[X][Y])
        ((C : (a : F[X]) → F[X][Y])
            (HAdd.hAdd (β := F[X])
              (HPow.hPow (α := F[X]) (β := ℕ) X 2 +
                HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (x + W.a₂) : F[X]) X)
              ((C : (a : F) → F[X]) (HPow.hPow (β := ℕ) x 2 + W.a₂ * x + W.a₄) : F[X])) :
          F[X][Y])
        (HMul.hMul (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₁) : F[X][Y]) Y) =
    1 +
          HMul.hMul (β := F[X][Y]) a
            ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x : F[X])) :
              F[X][Y]) +
        a_1 *
          HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) y) : F[X][Y]) +
      a_2 *
        HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y
          ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (W.negY x y)) : F[X][Y])
Tactic: simp_rw [eq_top_iff_one, mem_span_insert', mem_span_singleton']
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
x x_1 c x_2 : Ideal W.CoordinateRing
⊢ x ⊔ (x_1 ⊔ (c ⊔ x_2)) = x ⊔ x_2 ⊔ x_1 ⊔ c
have rw : x ⊔ x_1 ⊔ (c ⊔ x_2) = x ⊔ x_2 ⊔ x_1 ⊔ c
Tactic: rw [← sup_assoc, sup_comm c, sup_sup_sup_comm, ← sup_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
x x_1 c x_2 : Ideal W.CoordinateRing
rw : x ⊔ x_1 ⊔ (c ⊔ x_2) = x ⊔ x_2 ⊔ x_1 ⊔ c
⊢ x ⊔ (x_1 ⊔ (c ⊔ x_2)) = x ⊔ x_2 ⊔ x_1 ⊔ c
have rw₁ : x ⊔ x_1 ⊔ (x_2 ⊔ c) = x ⊔ x_2 ⊔ x_1 ⊔ c
Tactic: rw [← sup_assoc, sup_comm c, sup_sup_sup_comm, ← sup_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
x x_1 c x_2 : Ideal W.CoordinateRing
rw : x ⊔ x_1 ⊔ (c ⊔ x_2) = x ⊔ x_2 ⊔ x_1 ⊔ c
rw₁ : x ⊔ x_1 ⊔ (x_2 ⊔ c) = x ⊔ x_2 ⊔ x_1 ⊔ c
⊢ x ⊔ (x_1 ⊔ (c ⊔ x_2)) = x ⊔ x_2 ⊔ x_1 ⊔ c
have rw₂ : x ⊔ x_2 ⊔ (x_1 ⊔ c) = x ⊔ x_2 ⊔ x_1 ⊔ c
Tactic: rw [← sup_assoc, sup_comm c, sup_sup_sup_comm, ← sup_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
x x_1 c x_2 : Ideal W.CoordinateRing
rw : x ⊔ x_1 ⊔ (c ⊔ x_2) = x ⊔ x_2 ⊔ x_1 ⊔ c
rw₁ : x ⊔ x_1 ⊔ (x_2 ⊔ c) = x ⊔ x_2 ⊔ x_1 ⊔ c
rw₂ : x ⊔ x_2 ⊔ (x_1 ⊔ c) = x ⊔ x_2 ⊔ x_1 ⊔ c
⊢ x ⊔ (x_1 ⊔ (c ⊔ x_2)) = x ⊔ x_2 ⊔ x_1 ⊔ c
have rw₃ : x ⊔ x_2 ⊔ x_1 ⊔ c = x ⊔ x_2 ⊔ x_1 ⊔ c
Tactic: rw [← sup_assoc, sup_comm c, sup_sup_sup_comm, ← sup_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (hypothesis)
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ XIdeal W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) *
      HMul.hMul (α := Ideal W.CoordinateRing) (XYIdeal W x₁ ((C : (a : F) → F[X]) y₁))
        (XYIdeal W x₂ ((C : (a : F) → F[X]) y₂)) =
    HMul.hMul (α := Ideal W.CoordinateRing) (YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))
      (XYIdeal W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) ((C : (a : F) → F[X]) (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))))
have sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
Tactic: have sup_rw : ∀ a b c d : Ideal W.CoordinateRing, a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c :=
    fun _ _ c _ => by rw [← sup_assoc, sup_comm c, sup_sup_sup_comm, ← sup_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
⊢ XIdeal W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) *
      HMul.hMul (α := Ideal W.CoordinateRing) (XYIdeal W x₁ ((C : (a : F) → F[X]) y₁))
        (XYIdeal W x₂ ((C : (a : F) → F[X]) y₂)) =
    HMul.hMul (α := Ideal W.CoordinateRing) (YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))
      (XYIdeal W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) ((C : (a : F) → F[X]) (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))))
have rw : HMul.hMul (α := Ideal W.CoordinateRing)
    (span
      {HMul.hMul (α := W.CoordinateRing) (XClass W x₁) (XClass W x₂),
        HMul.hMul (α := W.CoordinateRing) (XClass W x₁) (YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))),
        HMul.hMul (α := W.CoordinateRing) (YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) (XClass W x₂),
        HMul.hMul (α := W.CoordinateRing) (YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))
          (YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))})
    (span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))}) =
  HMul.hMul (α := Ideal W.CoordinateRing) (YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))
    (span
        (singleton (α := W.CoordinateRing)
          ((mk W : (a : F[X][Y]) → W.CoordinateRing)
              (HSub.hSub (α := F[X][Y]) (β := F[X][Y]) W.negPolynomial
                ((C : (a : F[X]) → F[X][Y]) (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) : F[X][Y])) :
            W.CoordinateRing)) ⊔
      span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))})
Tactic: rw [XYIdeal_add_eq, XIdeal, mul_comm, XYIdeal_eq₁ x₁ y₁ <| W.slope x₁ x₂ y₁ y₂, XYIdeal,
    XYIdeal_eq₂ h₁ h₂ hxy, XYIdeal, span_pair_mul_span_pair]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
⊢ HMul.hMul (α := Ideal W.CoordinateRing)
      (span
        {HMul.hMul (α := W.CoordinateRing) (XClass W x₁) (XClass W x₂),
          HMul.hMul (α := W.CoordinateRing) (XClass W x₁) (YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))),
          HMul.hMul (α := W.CoordinateRing) (YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) (XClass W x₂),
          HMul.hMul (α := W.CoordinateRing) (YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))
            (YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))})
      (span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))}) =
    HMul.hMul (α := Ideal W.CoordinateRing) (YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))
      (span
          (singleton (α := W.CoordinateRing)
            ((mk W : (a : F[X][Y]) → W.CoordinateRing)
                (HSub.hSub (α := F[X][Y]) (β := F[X][Y]) W.negPolynomial
                  ((C : (a : F[X]) → F[X][Y]) (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) : F[X][Y])) :
              W.CoordinateRing)) ⊔
        span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))})
have simp_rw : span {HMul.hMul (α := W.CoordinateRing) (XClass W x₁) (XClass W x₂) * XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔
        span
          {HMul.hMul (α := W.CoordinateRing) (YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))
                (YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) *
              XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔
      span
        {HMul.hMul (α := W.CoordinateRing) (XClass W x₁) (YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) *
            XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔
    span
      {HMul.hMul (α := W.CoordinateRing) (YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) (XClass W x₂) *
          XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} =
  HMul.hMul (α := Ideal W.CoordinateRing) (YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))
    (span
        (singleton (α := W.CoordinateRing)
          ((mk W : (a : F[X][Y]) → W.CoordinateRing)
              (HSub.hSub (α := F[X][Y]) (β := F[X][Y]) W.negPolynomial
                ((C : (a : F[X]) → F[X][Y]) (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) : F[X][Y])) :
            W.CoordinateRing)) ⊔
      span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))})
Tactic: simp_rw [span_insert, sup_rw, Ideal.sup_mul, span_singleton_mul_span_singleton]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
⊢ span
        (singleton (α := W.CoordinateRing)
          ((mk W : (a : F[X][Y]) → W.CoordinateRing)
              (HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y
                ((C : (a : F[X]) → F[X][Y]) (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) : F[X][Y])) :
            W.CoordinateRing)) *
      (span
          (singleton (α := W.CoordinateRing)
            ((mk W : (a : F[X][Y]) → W.CoordinateRing)
                (HSub.hSub (α := F[X][Y]) (β := F[X][Y]) W.negPolynomial
                  ((C : (a : F[X]) → F[X][Y]) (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) : F[X][Y])) :
              W.CoordinateRing)) ⊔
        HMul.hMul (α := Ideal W.CoordinateRing)
          (span {XClass W x₁} ⊔
            (span {XClass W x₂} ⊔
              span
                (singleton (α := W.CoordinateRing)
                  ((mk W : (a : F[X][Y]) → W.CoordinateRing) (HSub.hSub (α := F[X][Y]) Y W.negPolynomial) :
                    W.CoordinateRing))))
          (span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))})) =
    HMul.hMul (α := Ideal W.CoordinateRing) (YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))
      (span
          (singleton (α := W.CoordinateRing)
            ((mk W : (a : F[X][Y]) → W.CoordinateRing)
                (HSub.hSub (α := F[X][Y]) (β := F[X][Y]) W.negPolynomial
                  ((C : (a : F[X]) → F[X][Y]) (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) : F[X][Y])) :
              W.CoordinateRing)) ⊔
        span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))})
have apply : HMul.hMul (α := Ideal W.CoordinateRing)
    (span {XClass W x₁} ⊔
      (span {XClass W x₂} ⊔
        span
          (singleton (α := W.CoordinateRing)
            ((mk W : (a : F[X][Y]) → W.CoordinateRing) (HSub.hSub (α := F[X][Y]) Y W.negPolynomial) :
              W.CoordinateRing))))
    (span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))}) =
  span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))}
Tactic: apply congr_arg (_ ∘ _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
⊢ HMul.hMul (α := Ideal W.CoordinateRing)
      (span {XClass W x₁} ⊔
        (span {XClass W x₂} ⊔
          span
            (singleton (α := W.CoordinateRing)
              ((mk W : (a : F[X][Y]) → W.CoordinateRing) (HSub.hSub (α := F[X][Y]) Y W.negPolynomial) :
                W.CoordinateRing))))
      (span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))}) =
    span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))}
have h : Eq (α := Ideal W.CoordinateRing)
  (span {XClass W x₁} ⊔
    (span {XClass W x₂} ⊔
      span
        (singleton (α := W.CoordinateRing)
          ((mk W : (a : F[X][Y]) → W.CoordinateRing) (HSub.hSub (α := F[X][Y]) Y W.negPolynomial) : W.CoordinateRing))))
  ⊤
Tactic: convert! top_mul (_ : Ideal W.CoordinateRing)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
⊢ Eq (α := Ideal W.CoordinateRing)
    (span {XClass W x₁} ⊔
      (span {XClass W x₂} ⊔
        span
          (singleton (α := W.CoordinateRing)
            ((mk W : (a : F[X][Y]) → W.CoordinateRing) (HSub.hSub (α := F[X][Y]) Y W.negPolynomial) :
              W.CoordinateRing))))
    ⊤
have h : ∃ (x : F[X][Y]),
  (∃ (a : F[X][Y]) (a_1 : F[X][Y]) (a_2 : F[X][Y]),
      a_2 * HSub.hSub (α := F[X][Y]) Y W.negPolynomial =
        x +
            HMul.hMul (β := F[X][Y]) a
              ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])) :
                F[X][Y]) +
          HMul.hMul (β := F[X][Y]) a_1
            ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₂ : F[X])) :
              F[X][Y])) ∧
    Eq (α := AdjoinRoot (R := F[X]) W.polynomial)
      ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial) x : AdjoinRoot (R := F[X]) W.polynomial)
      (1 : W.CoordinateRing)
Tactic: simp_rw [XClass, ← Set.image_singleton (f := mk W), ← map_span, ← Ideal.map_sup, eq_top_iff_one,
    mem_map_iff_of_surjective _ AdjoinRoot.mk_surjective, ← span_insert, mem_span_insert',
    mem_span_singleton']
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
⊢ ∃ (x : F[X][Y]),
    (∃ (a : F[X][Y]) (a_1 : F[X][Y]) (a_2 : F[X][Y]),
        a_2 * HSub.hSub (α := F[X][Y]) Y W.negPolynomial =
          x +
              HMul.hMul (β := F[X][Y]) a
                ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])) :
                  F[X][Y]) +
            HMul.hMul (β := F[X][Y]) a_1
              ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₂ : F[X])) :
                F[X][Y])) ∧
      Eq (α := AdjoinRoot (R := F[X]) W.polynomial)
        ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial) x : AdjoinRoot (R := F[X]) W.polynomial)
        (1 : W.CoordinateRing)
have pos : ∀ (hx : x₁ = x₂),
  ∃ (x : F[X][Y]),
    (∃ (a : F[X][Y]) (a_1 : F[X][Y]) (a_2 : F[X][Y]),
        a_2 * HSub.hSub (α := F[X][Y]) Y W.negPolynomial =
          x +
              HMul.hMul (β := F[X][Y]) a
                ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])) :
                  F[X][Y]) +
            HMul.hMul (β := F[X][Y]) a_1
              ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₂ : F[X])) :
                F[X][Y])) ∧
      Eq (α := AdjoinRoot (R := F[X]) W.polynomial)
        ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial) x : AdjoinRoot (R := F[X]) W.polynomial)
        (1 : W.CoordinateRing)
Tactic: by_cases hx : x₁ = x₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
pos :
  ∀ (hx : x₁ = x₂),
    ∃ (x : F[X][Y]),
      (∃ (a : F[X][Y]) (a_1 : F[X][Y]) (a_2 : F[X][Y]),
          a_2 * HSub.hSub (α := F[X][Y]) Y W.negPolynomial =
            x +
                HMul.hMul (β := F[X][Y]) a
                  ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])) :
                    F[X][Y]) +
              HMul.hMul (β := F[X][Y]) a_1
                ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₂ : F[X])) :
                  F[X][Y])) ∧
        Eq (α := AdjoinRoot (R := F[X]) W.polynomial)
          ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial) x :
            AdjoinRoot (R := F[X]) W.polynomial)
          (1 : W.CoordinateRing)
⊢ ∃ (x : F[X][Y]),
    (∃ (a : F[X][Y]) (a_1 : F[X][Y]) (a_2 : F[X][Y]),
        a_2 * HSub.hSub (α := F[X][Y]) Y W.negPolynomial =
          x +
              HMul.hMul (β := F[X][Y]) a
                ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])) :
                  F[X][Y]) +
            HMul.hMul (β := F[X][Y]) a_1
              ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₂ : F[X])) :
                F[X][Y])) ∧
      Eq (α := AdjoinRoot (R := F[X]) W.polynomial)
        ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial) x : AdjoinRoot (R := F[X]) W.polynomial)
        (1 : W.CoordinateRing)
have neg : ∀ (hx : ¬x₁ = x₂),
  ∃ (x : F[X][Y]),
    (∃ (a : F[X][Y]) (a_1 : F[X][Y]) (a_2 : F[X][Y]),
        a_2 * HSub.hSub (α := F[X][Y]) Y W.negPolynomial =
          x +
              HMul.hMul (β := F[X][Y]) a
                ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])) :
                  F[X][Y]) +
            HMul.hMul (β := F[X][Y]) a_1
              ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₂ : F[X])) :
                F[X][Y])) ∧
      Eq (α := AdjoinRoot (R := F[X]) W.polynomial)
        ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial) x : AdjoinRoot (R := F[X]) W.polynomial)
        (1 : W.CoordinateRing)
Tactic: by_cases hx : x₁ = x₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (hypothesis)
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
hx : x₁ = x₂
⊢ ∃ (x : F[X][Y]),
    (∃ (a : F[X][Y]) (a_1 : F[X][Y]) (a_2 : F[X][Y]),
        a_2 * HSub.hSub (α := F[X][Y]) Y W.negPolynomial =
          x +
              HMul.hMul (β := F[X][Y]) a
                ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])) :
                  F[X][Y]) +
            HMul.hMul (β := F[X][Y]) a_1
              ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₂ : F[X])) :
                F[X][Y])) ∧
      Eq (α := AdjoinRoot (R := F[X]) W.polynomial)
        ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial) x : AdjoinRoot (R := F[X]) W.polynomial)
        (1 : W.CoordinateRing)
have hy : y₁ ≠ W.negY x₂ y₂
Tactic: have hy : y₁ ≠ W.negY x₂ y₂ := fun h => hxy ⟨hx, h⟩