awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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
⊢ IsTwoSided (α := W.CoordinateRing)
    (span
      (singleton (α := W.CoordinateRing)
        ((mk W : (a : F[X][Y]) → W.CoordinateRing)
            ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x : F[X]))) :
          W.CoordinateRing)))

Tactic:
on_goal 2 => infer_instance
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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 W.CoordinateRing) (Ideal.map (R := F[X][Y]) (F := F[X][Y] →+* W.CoordinateRing) (mk W) ⊤) ⊤

Tactic:
map_top (R := F[X][Y]) (mk W)

Premises used: WeierstrassCurve.Affine.CoordinateRing.mk, Ideal.map_top
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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
hx : W.a₁ * y - (3 * HPow.hPow (β := ℕ) x 2 + 2 * W.a₂ * x + W.a₄) ≠ 0
W_X : F := W.a₁ * y - (3 * HPow.hPow (β := ℕ) x 2 + 2 * W.a₂ * x + W.a₄)
⊢ ∃ (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:
⟨C <| C W_X⁻¹ * -(X + C (2 * x + W.a₂)), C <| C <| W_X⁻¹ * W.a₁, 0, C <| C <| W_X⁻¹ * -1, ?_⟩

Premises used: Polynomial.C, HMul.hMul, WeierstrassCurve.a₂, Inv.inv, HAdd.hAdd, Exists.intro, OfNat.ofNat, Polynomial.X, DFunLike.coe, Neg.neg, WeierstrassCurve.a₁
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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
hy : 2 * y + W.a₁ * x + W.a₃ ≠ 0
W_Y : F := 2 * y + W.a₁ * x + W.a₃
⊢ ∃ (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:
⟨0, C <| C W_Y⁻¹, C <| C <| W_Y⁻¹ * -1, 0, ?_⟩

Premises used: Polynomial.C, HMul.hMul, Inv.inv, Exists.intro, OfNat.ofNat, DFunLike.coe, Neg.neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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
rw₃ 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

Tactic:
rw [← sup_assoc, sup_comm c, sup_sup_sup_comm, ← sup_assoc]

Premises used: sup_sup_sup_comm, sup_assoc, sup_comm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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₂)
⊢ ∀ (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]
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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
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₂))})
⊢ 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₂))))

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]

Premises used: WeierstrassCurve.Affine.CoordinateRing.XYIdeal_eq₂, WeierstrassCurve.Affine.slope, WeierstrassCurve.Affine.CoordinateRing.XYIdeal_add_eq, WeierstrassCurve.Affine.CoordinateRing.XYIdeal, WeierstrassCurve.Affine.CoordinateRing.XYIdeal_eq₁, WeierstrassCurve.Affine.CoordinateRing.XIdeal, mul_comm, Ideal.span_pair_mul_span_pair
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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
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₂))})
⊢ 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:
simp_rw [span_insert, sup_rw, Ideal.sup_mul, span_singleton_mul_span_singleton]

Premises used: Ideal.span_singleton_mul_span_singleton, Ideal.sup_mul, Ideal.span_insert
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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
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₂))}
⊢ 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₂))})

Tactic:
apply congr_arg (_ ∘ _)

Premises used: Function.comp, congr_arg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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 (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))}) =
    span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))}

Tactic:
top_mul (_ : Ideal W.CoordinateRing)

Premises used: Ideal.top_mul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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
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))))
    ⊤
⊢ 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:
convert! top_mul (_ : Ideal W.CoordinateRing)

Premises used: Ideal.top_mul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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
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)
⊢ 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:
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']

Premises used: Ideal.mem_span_singleton', AdjoinRoot.mk_surjective, Set.image_singleton, Ideal.map_span, Ideal.map_sup, Ideal.eq_top_iff_one, WeierstrassCurve.Affine.CoordinateRing.XClass, Ideal.mem_map_iff_of_surjective, Ideal.mem_span_insert', Ideal.span_insert
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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)
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)
⊢ ∃ (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₂
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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₂
⊢ y₁ ≠ W.negY x₂ y₂

Tactic:
have hy : y₁ ≠ W.negY x₂ y₂ := fun h => hxy ⟨hx, h⟩