awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
x : R[X][Y]
rw :
  eval₂ (AdjoinRoot.of (W'.map f).polynomial) (AdjoinRoot.root (W'.map f).polynomial)
      (Polynomial.map (mapRingHom f) x) =
    (mk (W'.map f) : (a : S[X][Y]) → (W'.map f).CoordinateRing) (Polynomial.map (mapRingHom f) x)
⊢ Eq.{s + 1} (α := (W'.map f).CoordinateRing)
    ((map W' f : (a : W'.CoordinateRing) → (W'.map f).CoordinateRing) ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) x) :
      (W'.map f).CoordinateRing)
    ((mk (W'.map f) : (a : S[X][Y]) → (W'.map f).CoordinateRing) (Polynomial.map (mapRingHom f) x) :
      (W'.map f).CoordinateRing)

Tactic:
rw [map, AdjoinRoot.lift_mk, ← eval₂_map]

Premises used: WeierstrassCurve.Affine.CoordinateRing.map, Polynomial.eval₂_map, AdjoinRoot.lift_mk
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
x : R[X][Y]
⊢ eval₂ (AdjoinRoot.of (W'.map f).polynomial) (AdjoinRoot.root (W'.map f).polynomial)
      (Polynomial.map (mapRingHom f) x) =
    (mk (W'.map f) : (a : S[X][Y]) → (W'.map f).CoordinateRing) (Polynomial.map (mapRingHom f) x)

Tactic:
AdjoinRoot.aeval_eq <| x.map <| mapRingHom f

Premises used: Submodule.Quotient.mk, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, Polynomial.mapRingHom, Polynomial.map, AdjoinRoot.aeval_eq, AdjoinRoot.of
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
x : R[X][Y]
⊢ eval₂ (AdjoinRoot.of (W'.map f).polynomial) (AdjoinRoot.root (W'.map f).polynomial)
      (Polynomial.map (mapRingHom f) x) =
    (mk (W'.map f) : (a : S[X][Y]) → (W'.map f).CoordinateRing) (Polynomial.map (mapRingHom f) x)

Tactic:
exact AdjoinRoot.aeval_eq <| x.map <| mapRingHom f

Premises used: Polynomial.mapRingHom, Polynomial.map, AdjoinRoot.aeval_eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
x : R[X]
y : W'.CoordinateRing
rw :
  HMul.hMul (α := (W'.map f).CoordinateRing) (β := (W'.map f).CoordinateRing)
      ((mk (W'.map f) : (a : S[X][Y]) → (W'.map f).CoordinateRing)
          ((C : (a : S[X]) → S[X][Y]) ((mapRingHom f : (a : R[X]) → S[X]) x)) :
        (W'.map f).CoordinateRing)
      ((map W' f : (a : W'.CoordinateRing) → (W'.map f).CoordinateRing) y : (W'.map f).CoordinateRing) =
    HMul.hMul (α := (W'.map f).CoordinateRing) (β := (W'.map f).CoordinateRing)
      ((mk (W'.map f) : (a : S[X][Y]) → (W'.map f).CoordinateRing) ((C : (a : S[X]) → S[X][Y]) (Polynomial.map f x)) :
        (W'.map f).CoordinateRing)
      ((map W' f : (a : W'.CoordinateRing) → (W'.map f).CoordinateRing) y : (W'.map f).CoordinateRing)
⊢ (map W' f : (a : W'.CoordinateRing) → (W'.map f).CoordinateRing) (x • y) =
    HSMul.hSMul (β := (W'.map f).CoordinateRing) (Polynomial.map f x)
      ((map W' f : (a : W'.CoordinateRing) → (W'.map f).CoordinateRing) y : (W'.map f).CoordinateRing)

Tactic:
rw [smul, map_mul, map_mk, map_C, smul]

Premises used: WeierstrassCurve.Affine.CoordinateRing.smul, WeierstrassCurve.Affine.CoordinateRing.map_mk, map_mul, Polynomial.map_C
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
x : R[X]
y : W'.CoordinateRing
⊢ HMul.hMul (α := (W'.map f).CoordinateRing) (β := (W'.map f).CoordinateRing)
      ((mk (W'.map f) : (a : S[X][Y]) → (W'.map f).CoordinateRing)
          ((C : (a : S[X]) → S[X][Y]) ((mapRingHom f : (a : R[X]) → S[X]) x)) :
        (W'.map f).CoordinateRing)
      ((map W' f : (a : W'.CoordinateRing) → (W'.map f).CoordinateRing) y : (W'.map f).CoordinateRing) =
    HMul.hMul (α := (W'.map f).CoordinateRing) (β := (W'.map f).CoordinateRing)
      ((mk (W'.map f) : (a : S[X][Y]) → (W'.map f).CoordinateRing) ((C : (a : S[X]) → S[X][Y]) (Polynomial.map f x)) :
        (W'.map f).CoordinateRing)
      ((map W' f : (a : W'.CoordinateRing) → (W'.map f).CoordinateRing) y : (W'.map f).CoordinateRing)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
hf : Function.Injective.{r + 1, s + 1} (α := R) (β := S) (⇑f : (a : R) → S)
y : W'.CoordinateRing
hy :
  Eq.{s + 1} (α := (W'.map f).CoordinateRing)
    ((map W' f : (a : W'.CoordinateRing) → (W'.map f).CoordinateRing) y : (W'.map f).CoordinateRing)
    (0 : (W'.map f).CoordinateRing)
obtain :
  ∀ (p q : R[X])
    (hy :
      Eq.{s + 1} (α := (W'.map f).CoordinateRing)
        ((map W' f : (a : W'.CoordinateRing) → (W'.map f).CoordinateRing)
            (HSMul.hSMul (β := W'.CoordinateRing) p 1 +
              HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y)) :
          (W'.map f).CoordinateRing)
        (0 : (W'.map f).CoordinateRing)),
    HSMul.hSMul (β := W'.CoordinateRing) p 1 +
        HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
      0
⊢ y = 0

Tactic:
obtain ⟨p, q, rfl⟩ := exists_smul_basis_eq y

Premises used: WeierstrassCurve.Affine.CoordinateRing.exists_smul_basis_eq, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
hf : Function.Injective.{r + 1, s + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p q : R[X]
hy :
  Eq.{s + 1} (α := (W'.map f).CoordinateRing)
    ((map W' f : (a : W'.CoordinateRing) → (W'.map f).CoordinateRing)
        (HSMul.hSMul (β := W'.CoordinateRing) p 1 +
          HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y)) :
      (W'.map f).CoordinateRing)
    (0 : (W'.map f).CoordinateRing)
⊢ HSMul.hSMul (β := (W'.map f).CoordinateRing) (Polynomial.map f p) 1 +
      HSMul.hSMul (β := (W'.map f).CoordinateRing) (Polynomial.map f q)
        ((mk (W'.map f) : (a : S[X][Y]) → (W'.map f).CoordinateRing) Y) =
    0

Tactic:
simp_rw [map_add, CoordinateRing.map_smul, map_one, map_mk, map_X] at hy

Premises used: map_add, Polynomial.map_X, WeierstrassCurve.Affine.CoordinateRing.map_mk, map_one, WeierstrassCurve.Affine.CoordinateRing.map_smul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
hf : Function.Injective.{r + 1, s + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p q : R[X]
hy :
  HSMul.hSMul (β := (W'.map f).CoordinateRing) (Polynomial.map f p) 1 +
      HSMul.hSMul (β := (W'.map f).CoordinateRing) (Polynomial.map f q)
        ((mk (W'.map f) : (a : S[X][Y]) → (W'.map f).CoordinateRing) Y) =
    0
⊢ Polynomial.map f p = 0

Tactic:
obtain ⟨hp, hq⟩ := smul_basis_eq_zero hy

Premises used: WeierstrassCurve.Affine.CoordinateRing.smul_basis_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
hf : Function.Injective.{r + 1, s + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p q : R[X]
hy :
  HSMul.hSMul (β := (W'.map f).CoordinateRing) (Polynomial.map f p) 1 +
      HSMul.hSMul (β := (W'.map f).CoordinateRing) (Polynomial.map f q)
        ((mk (W'.map f) : (a : S[X][Y]) → (W'.map f).CoordinateRing) Y) =
    0
hp : Polynomial.map f p = 0
⊢ Polynomial.map f q = 0

Tactic:
obtain ⟨hp, hq⟩ := smul_basis_eq_zero hy

Premises used: WeierstrassCurve.Affine.CoordinateRing.smul_basis_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
hf : Function.Injective.{r + 1, s + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p q : R[X]
hy :
  HSMul.hSMul (β := (W'.map f).CoordinateRing) (Polynomial.map f p) 1 +
      HSMul.hSMul (β := (W'.map f).CoordinateRing) (Polynomial.map f q)
        ((mk (W'.map f) : (a : S[X][Y]) → (W'.map f).CoordinateRing) Y) =
    0
hp : Polynomial.map f p = 0
hq : Polynomial.map f q = 0
⊢ p = 0

Tactic:
rw [Polynomial.map_eq_zero_iff hf] at hp hq

Premises used: Polynomial.map_eq_zero_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
hf : Function.Injective.{r + 1, s + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p q : R[X]
hy :
  HSMul.hSMul (β := (W'.map f).CoordinateRing) (Polynomial.map f p) 1 +
      HSMul.hSMul (β := (W'.map f).CoordinateRing) (Polynomial.map f q)
        ((mk (W'.map f) : (a : S[X][Y]) → (W'.map f).CoordinateRing) Y) =
    0
hp : Polynomial.map f p = 0
hq : Polynomial.map f q = 0
hp₁ : p = 0
⊢ q = 0

Tactic:
rw [Polynomial.map_eq_zero_iff hf] at hp hq

Premises used: Polynomial.map_eq_zero_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
hf : Function.Injective.{r + 1, s + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p q : R[X]
hy :
  HSMul.hSMul (β := (W'.map f).CoordinateRing) (Polynomial.map f p) 1 +
      HSMul.hSMul (β := (W'.map f).CoordinateRing) (Polynomial.map f q)
        ((mk (W'.map f) : (a : S[X][Y]) → (W'.map f).CoordinateRing) Y) =
    0
hp : p = 0
hq : q = 0
simp_rw :
  HSMul.hSMul (α := R[X]) (β := W'.CoordinateRing) 0 1 +
      HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
    0
simp_rw₁ :
  HSMul.hSMul (α := R[X]) (β := W'.CoordinateRing) 0 1 +
      HSMul.hSMul (α := R[X]) (β := W'.CoordinateRing) 0 ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
    0
simp_rw₂ : HAdd.hAdd (α := W'.CoordinateRing) 0 0 = 0
⊢ HSMul.hSMul (β := W'.CoordinateRing) p 1 +
      HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
    0

Tactic:
simp_rw [hp, hq, zero_smul, add_zero]

Premises used: zero_smul, add_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
inst_6 : Field L
W' : Affine R
W : Affine F
inst_7 : IsDomain R
⊢ IsDomain.{r} W'.CoordinateRing

Tactic:
have : IsDomain (W'.map <| algebraMap R <| FractionRing R).CoordinateRing :=
    AdjoinRoot.isDomain_of_prime irreducible_polynomial.prime
  (map_injective <| IsFractionRing.injective R <| FractionRing R).isDomain

Premises used: Algebra.algebraMap, WeierstrassCurve.Affine.CoordinateRing.map, WeierstrassCurve.Affine.irreducible_polynomial, IsFractionRing.injective, AdjoinRoot.isDomain_of_prime, Function.Injective.isDomain, FractionRing, WeierstrassCurve.Affine.CoordinateRing.map_injective, Irreducible.prime
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : Nontrivial R
x : R
rw : LT.lt (α := ℕ) 0 2
⊢ natDegree.{r} (R := R[X])
      ((C : (a : R[X]) → R[X][Y]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))) <
    natDegree (R := R[X]) W'.polynomial

Tactic:
rw [natDegree_polynomial, natDegree_C]

Premises used: WeierstrassCurve.Affine.natDegree_polynomial, Polynomial.natDegree_C
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : Nontrivial R
x : R
⊢ LT.lt (α := ℕ) 0 2

Tactic:
norm_num1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : Nontrivial R
y : R[X]
rw : LT.lt (α := ℕ) 1 2
⊢ (HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) y : R[X][Y])).natDegree <
    natDegree (R := R[X]) W'.polynomial

Tactic:
rw [natDegree_polynomial, natDegree_X_sub_C]

Premises used: WeierstrassCurve.Affine.natDegree_polynomial, Polynomial.natDegree_X_sub_C
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : Nontrivial R
y : R[X]
⊢ LT.lt (α := ℕ) 1 2

Tactic:
norm_num1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y ℓ : R
rw :
  HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) (linePolynomial x y ℓ) : R[X][Y]) *
          HSub.hSub (α := R[X][Y]) (β := R[X][Y]) W'.negPolynomial
            ((C : (a : R[X]) → R[X][Y]) (linePolynomial x y ℓ) : R[X][Y]) +
        W'.polynomial -
      HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) (linePolynomial x y ℓ) : R[X][Y]) *
        HSub.hSub (α := R[X][Y]) (β := R[X][Y]) W'.negPolynomial
          ((C : (a : R[X]) → R[X][Y]) (linePolynomial x y ℓ) : R[X][Y]) =
    HMul.hMul (α := R[X][Y]) W'.polynomial 1
rw₁ : W'.polynomial = HMul.hMul (α := R[X][Y]) W'.polynomial 1
rw₂ rw₃ : Eq (α := R[X][Y]) W'.polynomial W'.polynomial
⊢ HSub.hSub (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W'.addPolynomial x y ℓ) : R[X][Y])
      (HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) (linePolynomial x y ℓ) : R[X][Y]) *
        HSub.hSub (α := R[X][Y]) (β := R[X][Y]) W'.negPolynomial
          ((C : (a : R[X]) → R[X][Y]) (linePolynomial x y ℓ) : R[X][Y])) =
    HMul.hMul (α := R[X][Y]) W'.polynomial 1

Tactic:
rw [W'.C_addPolynomial, add_sub_cancel_left, mul_one]

Premises used: WeierstrassCurve.Affine.C_addPolynomial, add_sub_cancel_left, mul_one
-- 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₂)
⊢ (mk W : (a : F[X][Y]) → W.CoordinateRing) ((C : (a : F[X]) → F[X][Y]) (W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) =
    -(HMul.hMul (α := W.CoordinateRing) (XClass W x₁) (XClass W x₂) * XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)))

Tactic:
congr_arg (mk W) <| W.C_addPolynomial_slope h₁ h₂ hxy

Premises used: WeierstrassCurve.Affine.CoordinateRing.mk, Submodule.Quotient.mk, WeierstrassCurve.Affine.C_addPolynomial_slope, congr_arg, Quot.map, Quotient.map', DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
inst_6 : Field L
W' : Affine R
W : Affine F
x : R
y : R[X]
h : eval x (eval y W'.polynomial) = 0
simp :
  Eq (α := Ideal (HasQuotient.Quotient R[X][Y] (B := Ideal R[X][Y]) (span {W'.polynomial})))
    (Ideal.map (R := R[X][Y]) (F := R[X][Y] →+* W'.CoordinateRing) (mk W')
      (span
        (insert (α := R[X][Y])
          ((C : (a : R[X]) → R[X][Y]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) : R[X][Y])
          {HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) y : R[X][Y])})))
    (Ideal.map (R := R[X][Y]) (F :=
      R[X][Y] →ₐ[R] HasQuotient.Quotient R[X][Y] (B := Ideal R[X][Y]) (span {W'.polynomial}))
      (Quotient.mkₐ R (span {W'.polynomial}))
      (span
        (insert (α := R[X][Y])
          ((C : (a : R[X]) → R[X][Y]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) : R[X][Y])
          {HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) y : R[X][Y])})))
⊢ XYIdeal W' x y =
    Ideal.map (R := R[X][Y]) (F :=
      R[X][Y] →ₐ[R] HasQuotient.Quotient R[X][Y] (B := Ideal R[X][Y]) (span {W'.polynomial}))
      (Quotient.mkₐ R (span {W'.polynomial}))
      (span
        (insert (α := R[X][Y])
          ((C : (a : R[X]) → R[X][Y]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) : R[X][Y])
          {HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) y : R[X][Y])}))

Tactic:
simp only [XYIdeal, XClass, YClass, ← Set.image_pair, ← map_span]

Premises used: Set.image_pair, WeierstrassCurve.Affine.CoordinateRing.XYIdeal, Ideal.map_span, WeierstrassCurve.Affine.CoordinateRing.XClass, WeierstrassCurve.Affine.CoordinateRing.YClass
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
inst_6 : Field L
W' : Affine R
W : Affine F
x : R
y : R[X]
h : eval x (eval y W'.polynomial) = 0
⊢ Eq (α := Ideal (HasQuotient.Quotient R[X][Y] (B := Ideal R[X][Y]) (span {W'.polynomial})))
    (Ideal.map (R := R[X][Y]) (F := R[X][Y] →+* W'.CoordinateRing) (mk W')
      (span
        (insert (α := R[X][Y])
          ((C : (a : R[X]) → R[X][Y]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) : R[X][Y])
          {HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) y : R[X][Y])})))
    (Ideal.map (R := R[X][Y]) (F :=
      R[X][Y] →ₐ[R] HasQuotient.Quotient R[X][Y] (B := Ideal R[X][Y]) (span {W'.polynomial}))
      (Quotient.mkₐ R (span {W'.polynomial}))
      (span
        (insert (α := R[X][Y])
          ((C : (a : R[X]) → R[X][Y]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) : R[X][Y])
          {HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) y : R[X][Y])})))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
simp :
  Eq (α := Ideal W'.CoordinateRing)
    (span
      (insert (α := W'.CoordinateRing)
        ((mk W' : (a : R[X][Y]) → W'.CoordinateRing)
            ((C : (a : R[X]) → R[X][Y])
              (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (W'.addX x₁ x₂ ℓ) : R[X]))) :
          W'.CoordinateRing)
        (singleton (α := W'.CoordinateRing)
          ((mk W' : (a : R[X][Y]) → W'.CoordinateRing)
              (HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y
                ((C : (a : R[X]) → R[X][Y])
                    ((C : (a : R) → R[X]) (-(ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) - W'.a₁ * W'.addX x₁ x₂ ℓ - W'.a₃)) :
                  R[X][Y])) :
            W'.CoordinateRing))))
    (span
        (singleton (α := W'.CoordinateRing)
          ((mk W' : (a : R[X][Y]) → W'.CoordinateRing)
              (HSub.hSub (β := R[X][Y])
                (HSub.hSub (α := R[X][Y]) (β := R[X][Y]) (-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]))
                ((C : (a : R[X]) → R[X][Y])
                    (HAdd.hAdd (β := R[X])
                      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ℓ : R[X])
                        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x₁ : R[X])))
                      ((C : (a : R) → R[X]) y₁ : R[X])) :
                  R[X][Y])) :
            W'.CoordinateRing)) ⊔
      span
        (singleton (α := W'.CoordinateRing)
          ((mk W' : (a : R[X][Y]) → W'.CoordinateRing)
              ((C : (a : R[X]) → R[X][Y])
                (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (W'.addX x₁ x₂ ℓ) : R[X]))) :
            W'.CoordinateRing)))
⊢ Eq (α := Ideal W'.CoordinateRing) (XYIdeal W' (W'.addX x₁ x₂ ℓ) ((C : (a : R) → R[X]) (W'.addY x₁ x₂ y₁ ℓ)))
    (span
        (singleton (α := W'.CoordinateRing)
          ((mk W' : (a : R[X][Y]) → W'.CoordinateRing)
              (HSub.hSub (α := R[X][Y]) (β := R[X][Y]) W'.negPolynomial
                ((C : (a : R[X]) → R[X][Y]) (linePolynomial x₁ y₁ ℓ) : R[X][Y])) :
            W'.CoordinateRing)) ⊔
      XIdeal W' (W'.addX x₁ x₂ ℓ))

Tactic:
simp only [XYIdeal, XIdeal, XClass, YClass, addY, negAddY, negY, negPolynomial, linePolynomial]

Premises used: WeierstrassCurve.Affine.CoordinateRing.XYIdeal, WeierstrassCurve.Affine.negY, WeierstrassCurve.Affine.addY, WeierstrassCurve.Affine.CoordinateRing.XClass, WeierstrassCurve.Affine.CoordinateRing.XIdeal, WeierstrassCurve.Affine.negPolynomial, WeierstrassCurve.Affine.negAddY, WeierstrassCurve.Affine.CoordinateRing.YClass, WeierstrassCurve.Affine.linePolynomial
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
e_s :
  Y -
        HSub.hSub (β := R[X][Y])
          (-HAdd.hAdd (β := R[X][Y])
                (HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) ℓ) : R[X][Y])
                  (HSub.hSub (α := R[X][Y]) (β := R[X][Y])
                    ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) (W'.addX x₁ x₂ ℓ)) : R[X][Y])
                    ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) x₁) : R[X][Y])))
                ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) y₁) : 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]) ((C : (a : R) → R[X]) (W'.addX x₁ x₂ ℓ)) : R[X][Y]))
          ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W'.a₃) : R[X][Y]) +
      HSub.hSub (α := R[X][Y]) (β := 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'.addX x₁ x₂ ℓ)) : R[X][Y]) *
        HAdd.hAdd (α := 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]) ((C : (a : R) → R[X]) ℓ) : R[X][Y]) =
    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]) +
        HAdd.hAdd (β := R[X][Y])
          (HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) ℓ) : R[X][Y])
            (HSub.hSub (α := R[X][Y]) (β := 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]) x₁) : R[X][Y])))
          ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) y₁) : R[X][Y]) +
      Y
⊢ HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y
        ((C : (a : R[X]) → R[X][Y])
            ((C : (a : R) → R[X]) (-(ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) - W'.a₁ * W'.addX x₁ x₂ ℓ - W'.a₃)) :
          R[X][Y]) +
      HMul.hMul (α := R[X][Y]) (β := R[X][Y])
        ((C : (a : R[X]) → R[X][Y])
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (W'.addX x₁ x₂ ℓ) : R[X])) :
          R[X][Y])
        ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) (W'.a₁ + ℓ)) : R[X][Y]) =
    HAdd.hAdd (α := 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])
        ((C : (a : R[X]) → R[X][Y])
            (HAdd.hAdd (β := R[X])
              (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ℓ : R[X])
                (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x₁ : R[X])))
              ((C : (a : R) → R[X]) y₁ : R[X])) :
          R[X][Y]) +
      Y

Tactic:
C_simp