awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂
hy : y₁ ≠ W.negY x₂ y₂
pos :
  ∀ (h₂ : W.Equation x₁ y₁) (hxy : ¬(x₁ = x₁ ∧ y₁ = W.negY x₁ y₁)) (hy : y₁ ≠ W.negY x₁ y₁),
    ∃ (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:
rcases hx, Y_eq_of_Y_ne h₁ h₂ hx hy with ⟨rfl, rfl⟩

Premises used: WeierstrassCurve.Affine.Y_eq_of_Y_ne, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ y₁ : F
h₁ : W.Equation x₁ y₁
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
h₂ : W.Equation x₁ y₁
hxy : ¬(x₁ = x₁ ∧ y₁ = W.negY x₁ y₁)
hy : y₁ ≠ W.negY x₁ y₁
y : F := HPow.hPow (β := ℕ) (y₁ - W.negY x₁ y₁) 2
⊢ HPow.hPow (β := ℕ) (y₁ - W.negY x₁ y₁) 2 ≠ 0

Tactic:
replace hxy := pow_ne_zero 2 <| sub_ne_zero_of_ne hy
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ y₁ : F
h₁ : W.Equation x₁ y₁
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
h₂ : W.Equation x₁ y₁
hy : y₁ ≠ W.negY x₁ y₁
y : F := HPow.hPow (β := ℕ) (y₁ - W.negY x₁ y₁) 2
hxy : HPow.hPow (β := ℕ) (y₁ - W.negY x₁ y₁) 2 ≠ 0
rw :
  HAdd.hAdd (α := AdjoinRoot (R := F[X]) W.polynomial) (β := AdjoinRoot (R := F[X]) W.polynomial)
      ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial) 1 : AdjoinRoot (R := F[X]) W.polynomial)
      ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial)
          (HMul.hMul (α := F[X][Y]) (β := F[X][Y])
            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (y⁻¹ * 4)) : F[X][Y]) W.polynomial) :
        AdjoinRoot (R := F[X]) W.polynomial) =
    1
rw₁ :
  HAdd.hAdd (α := AdjoinRoot (R := F[X]) W.polynomial) (β := AdjoinRoot (R := F[X]) W.polynomial)
      (1 : AdjoinRoot (R := F[X]) W.polynomial)
      ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial)
          (HMul.hMul (α := F[X][Y]) (β := F[X][Y])
            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (y⁻¹ * 4)) : F[X][Y]) W.polynomial) :
        AdjoinRoot (R := F[X]) W.polynomial) =
    1
rw₂ :
  1 +
      HMul.hMul (α := W.CoordinateRing) (β := W.CoordinateRing)
        ((mk W : (a : F[X][Y]) → W.CoordinateRing) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (y⁻¹ * 4))) :
          W.CoordinateRing)
        ((mk W : (a : F[X][Y]) → W.CoordinateRing) W.polynomial) =
    1
rw₃ :
  1 +
      HMul.hMul (α := W.CoordinateRing) (β := W.CoordinateRing)
        ((mk W : (a : F[X][Y]) → W.CoordinateRing) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (y⁻¹ * 4))) :
          W.CoordinateRing)
        (0 : AdjoinRoot (R := F[X]) W.polynomial) =
    1
rw₄ : HAdd.hAdd (α := AdjoinRoot (R := F[X]) W.polynomial) 1 0 = 1
rw₅ rw₆ : Eq.{u + 1} (α := AdjoinRoot (R := F[X]) W.polynomial) 1 1
⊢ Eq (α := AdjoinRoot (R := F[X]) W.polynomial)
    ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial)
        (1 +
          HMul.hMul (α := F[X][Y]) (β := F[X][Y])
            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (y⁻¹ * 4)) : F[X][Y]) W.polynomial) :
      AdjoinRoot (R := F[X]) W.polynomial)
    (1 : W.CoordinateRing)

Tactic:
rw [map_add, map_one, map_mul <| mk W, AdjoinRoot.mk_self, mul_zero, add_zero]

Premises used: WeierstrassCurve.Affine.CoordinateRing.mk, map_add, MulZeroClass.mul_zero, map_mul, map_one, AdjoinRoot.mk_self, add_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ y₁ : F
h₁ : W.Equation x₁ y₁
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
h₂ : W.Equation x₁ y₁
hy : y₁ ≠ W.negY x₁ y₁
y : F := HPow.hPow (β := ℕ) (y₁ - W.negY x₁ y₁) 2
hxy : HPow.hPow (β := ℕ) (y₁ - W.negY x₁ y₁) 2 ≠ 0
pos :
  HMul.hMul (α := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) y⁻¹) : F[X][Y])
        (HSub.hSub (α := F[X][Y]) Y W.negPolynomial) *
      HSub.hSub (α := F[X][Y]) Y W.negPolynomial =
    1 +
          HMul.hMul (α := F[X][Y]) (β := F[X][Y])
            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (y⁻¹ * 4)) : F[X][Y]) W.polynomial +
        HMul.hMul (α := F[X][Y]) (β := F[X][Y])
          ((C : (a : F[X]) → F[X][Y])
              (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) y⁻¹ : F[X])
                (HAdd.hAdd (β := F[X])
                  ((C : (a : F) → F[X]) 4 * HPow.hPow (α := F[X]) (β := ℕ) X 2 +
                    HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (4 * x₁ + b₂ W) : F[X]) X)
                  ((C : (a : F) → F[X]) (4 * HPow.hPow (β := ℕ) x₁ 2 + b₂ W * x₁ + 2 * b₄ W) : F[X]))) :
            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]) +
      HMul.hMul (α := F[X][Y]) (β := F[X][Y]) (0 : 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])
⊢ ∃ (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:
refine ⟨1 + C (C <| y⁻¹ * 4) * W.polynomial,
      ⟨C <| C y⁻¹ * (C 4 * X ^ 2 + C (4 * x₁ + W.b₂) * X + C (4 * x₁ ^ 2 + W.b₂ * x₁ + 2 * W.b₄)),
        0, C (C y⁻¹) * (Y - W.negPolynomial), ?_⟩, by
      rw [map_add, map_one, map_mul <| mk W, AdjoinRoot.mk_self, mul_zero, add_zero]⟩
-- 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₂
⊢ x₁ - x₂ ≠ 0

Tactic:
replace hx := sub_ne_zero_of_ne hx
-- 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₂ ≠ 0
⊢ ∃ (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:
⟨_, ⟨⟨C <| C (x₁ - x₂)⁻¹, C <| C <| (x₁ - x₂)⁻¹ * -1, 0, ?_⟩, map_one _⟩⟩

Premises used: Polynomial.C, HMul.hMul, HSub.hSub, Inv.inv, map_one, And.intro, 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₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
hx : x₁ - x₂ ≠ 0
neg :
  0 * HSub.hSub (α := F[X][Y]) Y W.negPolynomial =
    1 +
        HMul.hMul (α := F[X][Y]) (β := F[X][Y])
          ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (x₁ - x₂)⁻¹) : 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]) +
      HMul.hMul (α := F[X][Y]) (β := F[X][Y])
        ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) ((x₁ - x₂)⁻¹ * -1)) : 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])
⊢ ∃ (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:
refine ⟨_, ⟨⟨C <| C (x₁ - x₂)⁻¹, C <| C <| (x₁ - x₂)⁻¹ * -1, 0, ?_⟩, map_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₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
hx : x₁ - x₂ ≠ 0
neg :
  HMul.hMul (α := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (x₁ - x₂)) : F[X][Y])
      (0 * HSub.hSub (α := F[X][Y]) Y W.negPolynomial) =
    HMul.hMul (α := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (x₁ - x₂)) : F[X][Y])
      (1 +
          HMul.hMul (α := F[X][Y]) (β := F[X][Y])
            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (x₁ - x₂)⁻¹) : 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]) +
        HMul.hMul (α := F[X][Y]) (β := F[X][Y])
          ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) ((x₁ - x₂)⁻¹ * -1)) : 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]))
⊢ 0 * HSub.hSub (α := F[X][Y]) Y W.negPolynomial =
    1 +
        HMul.hMul (α := F[X][Y]) (β := F[X][Y])
          ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (x₁ - x₂)⁻¹) : 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]) +
      HMul.hMul (α := F[X][Y]) (β := F[X][Y])
        ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) ((x₁ - x₂)⁻¹ * -1)) : 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])

Tactic:
rw [← mul_right_inj' <| C_ne_zero.mpr <| C_ne_zero.mpr hx]

Premises used: Iff.mpr, mul_right_inj', Polynomial.C_ne_zero
-- 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₂ ≠ 0
neg :
  HMul.hMul (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (x₁ - x₂)) : F[X][Y])
        (0 : F[X][Y]) *
      HSub.hSub (α := F[X][Y]) Y W.negPolynomial =
    HAdd.hAdd (β := F[X][Y])
      (HAdd.hAdd (β := F[X][Y])
        (HMul.hMul (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (x₁ - x₂)) : F[X][Y])
          (1 : F[X][Y]))
        ((C : (a : F[X]) → F[X][Y])
            ((C : (a : F) → F[X]) 1 * HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])) :
          F[X][Y]))
      ((C : (a : F[X]) → F[X][Y])
          (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (HMul.hMul (α := F) 1 (-1)) : F[X])
            (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₂ : F[X]))) :
        F[X][Y])
⊢ HMul.hMul (α := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (x₁ - x₂)) : F[X][Y])
      (0 * HSub.hSub (α := F[X][Y]) Y W.negPolynomial) =
    HMul.hMul (α := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (x₁ - x₂)) : F[X][Y])
      (1 +
          HMul.hMul (α := F[X][Y]) (β := F[X][Y])
            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (x₁ - x₂)⁻¹) : 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]) +
        HMul.hMul (α := F[X][Y]) (β := F[X][Y])
          ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) ((x₁ - x₂)⁻¹ * -1)) : 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]))

Tactic:
simp only [← mul_assoc, mul_add, ← C_mul, mul_inv_cancel₀ hx]

Premises used: mul_inv_cancel₀, mul_assoc, Polynomial.C_mul, mul_add
-- 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₂ ≠ 0
neg :
  HSub.hSub (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x₁) : F[X][Y])
          ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x₂) : F[X][Y]) *
        0 *
      HSub.hSub (α := F[X][Y]) Y W.negPolynomial =
    HSub.hSub (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x₁) : F[X][Y])
            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x₂) : F[X][Y]) *
          1 +
        1 *
          HSub.hSub (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) X : F[X][Y])
            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x₁) : F[X][Y]) +
      HMul.hMul (α := F[X][Y]) 1 (-1) *
        HSub.hSub (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) X : F[X][Y])
          ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x₂) : F[X][Y])
⊢ HMul.hMul (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (x₁ - x₂)) : F[X][Y])
        (0 : F[X][Y]) *
      HSub.hSub (α := F[X][Y]) Y W.negPolynomial =
    HAdd.hAdd (β := F[X][Y])
      (HAdd.hAdd (β := F[X][Y])
        (HMul.hMul (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (x₁ - x₂)) : F[X][Y])
          (1 : F[X][Y]))
        ((C : (a : F[X]) → F[X][Y])
            ((C : (a : F) → F[X]) 1 * HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])) :
          F[X][Y]))
      ((C : (a : F[X]) → F[X][Y])
          (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (HMul.hMul (α := F) 1 (-1)) : F[X])
            (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₂ : F[X]))) :
        F[X][Y])

Tactic:
C_simp
-- 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₂ ≠ 0
⊢ HSub.hSub (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x₁) : F[X][Y])
          ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x₂) : F[X][Y]) *
        0 *
      HSub.hSub (α := F[X][Y]) Y W.negPolynomial =
    HSub.hSub (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x₁) : F[X][Y])
            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x₂) : F[X][Y]) *
          1 +
        1 *
          HSub.hSub (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) X : F[X][Y])
            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x₁) : F[X][Y]) +
      HMul.hMul (α := F[X][Y]) 1 (-1) *
        HSub.hSub (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) X : F[X][Y])
          ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x₂) : F[X][Y])

Tactic:
ring1
-- 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 y : F
h : W.Nonsingular x y
rw :
  HMul.hMul (α := FractionalIdeal (R := W.CoordinateRing) W.CoordinateRing⁰ W.FunctionField)
        (↑(XYIdeal W x ((C : (a : F) → F[X]) y)) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)
        (↑(XYIdeal W x ((C : (a : F) → F[X]) (W.negY x y))) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField) *
      (↑(XIdeal W x) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)⁻¹ =
    1
rw₁ :
  HMul.hMul (α := FractionalIdeal (R := W.CoordinateRing) W.CoordinateRing⁰ W.FunctionField)
      (↑(HMul.hMul (α := Ideal W.CoordinateRing) (XYIdeal W x ((C : (a : F) → F[X]) y))
            (XYIdeal W x ((C : (a : F) → F[X]) (W.negY x y)))) :
        FractionalIdeal W.CoordinateRing⁰ W.FunctionField)
      (↑(XIdeal W x) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)⁻¹ =
    1
rw₂ :
  HMul.hMul (α := FractionalIdeal (R := W.CoordinateRing) W.CoordinateRing⁰ W.FunctionField)
      (↑(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))) :
        FractionalIdeal W.CoordinateRing⁰ W.FunctionField)
      (↑(XIdeal W x) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)⁻¹ =
    1
rw₃ :
  HMul.hMul (α := FractionalIdeal (R := W.CoordinateRing) W.CoordinateRing⁰ W.FunctionField)
      (↑(XIdeal W x) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)
      (↑(XIdeal W x) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)⁻¹ =
    1
rw₄ :
  HMul.hMul (α := FractionalIdeal (R := W.CoordinateRing) W.CoordinateRing⁰ W.FunctionField)
      (↑(span {XClass W x}) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)
      (↑(span {XClass W x}) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)⁻¹ =
    1
rw₅ rw₆ : Eq.{u + 1} (α := FractionalIdeal (R := W.CoordinateRing) W.CoordinateRing⁰ W.FunctionField) 1 1
⊢ (↑(XYIdeal W x ((C : (a : F) → F[X]) y)) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField) *
      HMul.hMul (α := FractionalIdeal (R := W.CoordinateRing) W.CoordinateRing⁰ W.FunctionField)
        (↑(XYIdeal W x ((C : (a : F) → F[X]) (W.negY x y))) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)
        (↑(XIdeal W x) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)⁻¹ =
    1

Tactic:
rw [← mul_assoc, ← coeIdeal_mul, mul_comm <| XYIdeal W .., XYIdeal_neg_mul h, XIdeal,
      FractionalIdeal.coe_ideal_span_singleton_mul_inv W.FunctionField <| XClass_ne_zero x]

Premises used: mul_assoc, WeierstrassCurve.Affine.CoordinateRing.XYIdeal, FractionalIdeal.coeIdeal_mul, WeierstrassCurve.Affine.CoordinateRing.XYIdeal_neg_mul, WeierstrassCurve.Affine.CoordinateRing.XClass_ne_zero, WeierstrassCurve.Affine.CoordinateRing.XIdeal, mul_comm, FractionalIdeal.coe_ideal_span_singleton_mul_inv, WeierstrassCurve.Affine.FunctionField
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
⊢ (↑(XYIdeal' h) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField) =
    (↑(XYIdeal W x ((C : (a : F) → F[X]) y)) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)

Tactic:
rfl

Premises used: FractionalIdeal.coeIdeal, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
rw :
  Eq (α := ClassGroup W.CoordinateRing)
    ((ClassGroup.mk W.FunctionField :
          (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
        (XYIdeal' ⋯ * XYIdeal' h) :
      ClassGroup W.CoordinateRing)
    (1 : ClassGroup W.CoordinateRing)
⊢ HMul.hMul (α := ClassGroup W.CoordinateRing) (β := ClassGroup W.CoordinateRing)
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (XYIdeal' ⋯) :
        ClassGroup W.CoordinateRing)
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (XYIdeal' h) :
        ClassGroup W.CoordinateRing) =
    1

Tactic:
rw [← map_mul]

Premises used: map_mul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
⊢ Eq (α := ClassGroup W.CoordinateRing)
    ((ClassGroup.mk W.FunctionField :
          (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
        (XYIdeal' ⋯ * XYIdeal' h) :
      ClassGroup W.CoordinateRing)
    (1 : ClassGroup W.CoordinateRing)

Tactic:
(ClassGroup.mk_eq_one_of_coe_ideal <| (coeIdeal_mul ..).symm.trans <|
    FractionalIdeal.coeIdeal_inj.mpr <| XYIdeal_neg_mul h).mpr ⟨_, XClass_ne_zero x, rfl⟩

Premises used: Iff.mpr, WeierstrassCurve.Affine.CoordinateRing.XClass_ne_zero, And.intro, Exists.intro, ClassGroup.mk_eq_one_of_coe_ideal, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
⊢ Eq (α := ClassGroup W.CoordinateRing)
    ((ClassGroup.mk W.FunctionField :
          (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
        (XYIdeal' ⋯ * XYIdeal' h) :
      ClassGroup W.CoordinateRing)
    (1 : ClassGroup W.CoordinateRing)

Tactic:
exact (ClassGroup.mk_eq_one_of_coe_ideal <| (coeIdeal_mul ..).symm.trans <|
    FractionalIdeal.coeIdeal_inj.mpr <| XYIdeal_neg_mul h).mpr ⟨_, XClass_ne_zero x, rfl⟩

Premises used: Iff.mpr, WeierstrassCurve.Affine.CoordinateRing.XClass_ne_zero, And.intro, Exists.intro, ClassGroup.mk_eq_one_of_coe_ideal, rfl