awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : DecidableEq F
inst_8 : DecidableEq K
inst_9 : DecidableEq L
x₂ y₂ : F
h₂ : W.Nonsingular x₂ y₂
⊢ (match (motive := W.Point → Additive (ClassGroup W.CoordinateRing)) zero + some x₂ y₂ h₂ with
    | zero => 0
    | some x y h =>
      (ClassGroup.mk W.FunctionField :
          (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
        (CoordinateRing.XYIdeal' h)) =
    HAdd.hAdd (α := Additive (ClassGroup W.CoordinateRing)) (β := Additive (ClassGroup W.CoordinateRing))
      (match (motive := W.Point → Additive (ClassGroup W.CoordinateRing)) zero with
        | zero => 0
        | some x y h =>
          (ClassGroup.mk W.FunctionField :
              (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
            (CoordinateRing.XYIdeal' h) :
        Additive (ClassGroup W.CoordinateRing))
      (match (motive := W.Point → Additive (ClassGroup W.CoordinateRing)) some x₂ y₂ h₂ with
        | zero => 0
        | some x y h =>
          (ClassGroup.mk W.FunctionField :
              (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
            (CoordinateRing.XYIdeal' h) :
        Additive (ClassGroup W.CoordinateRing))

Tactic:
simp only [← zero_def, zero_add, add_zero]

Premises used: WeierstrassCurve.Affine.Point.zero_def, zero_add, 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 : DecidableEq F
inst_8 : DecidableEq K
inst_9 : DecidableEq L
x₁ y₁ : F
h₁ : W.Nonsingular x₁ y₁
⊢ (match (motive := W.Point → Additive (ClassGroup W.CoordinateRing)) some x₁ y₁ h₁ + zero with
    | zero => 0
    | some x y h =>
      (ClassGroup.mk W.FunctionField :
          (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
        (CoordinateRing.XYIdeal' h)) =
    HAdd.hAdd (α := Additive (ClassGroup W.CoordinateRing)) (β := Additive (ClassGroup W.CoordinateRing))
      (match (motive := W.Point → Additive (ClassGroup W.CoordinateRing)) some x₁ y₁ h₁ with
        | zero => 0
        | some x y h =>
          (ClassGroup.mk W.FunctionField :
              (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
            (CoordinateRing.XYIdeal' h) :
        Additive (ClassGroup W.CoordinateRing))
      (match (motive := W.Point → Additive (ClassGroup W.CoordinateRing)) zero with
        | zero => 0
        | some x y h =>
          (ClassGroup.mk W.FunctionField :
              (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
            (CoordinateRing.XYIdeal' h) :
        Additive (ClassGroup W.CoordinateRing))

Tactic:
simp only [← zero_def, zero_add, add_zero]

Premises used: WeierstrassCurve.Affine.Point.zero_def, zero_add, 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 : DecidableEq F
inst_8 : DecidableEq K
inst_9 : DecidableEq L
x₁ y₁ : F
h₁ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h₂ : W.Nonsingular x₂ y₂
hxy : x₁ = x₂ ∧ y₁ = W.negY x₂ y₂
pos :
  0 =
    HAdd.hAdd (α := Additive (ClassGroup W.CoordinateRing)) (β := Additive (ClassGroup W.CoordinateRing))
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (CoordinateRing.XYIdeal' (y := W.negY x₂ y₂) ⋯) :
        ClassGroup W.CoordinateRing)
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (CoordinateRing.XYIdeal' h₂) :
        ClassGroup W.CoordinateRing)
⊢ (match (motive := W.Point → Additive (ClassGroup W.CoordinateRing)) some x₁ y₁ h₁ + some x₂ y₂ h₂ with
    | zero => 0
    | some x y h =>
      (ClassGroup.mk W.FunctionField :
          (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
        (CoordinateRing.XYIdeal' h)) =
    HAdd.hAdd (α := Additive (ClassGroup W.CoordinateRing)) (β := Additive (ClassGroup W.CoordinateRing))
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (CoordinateRing.XYIdeal' h₁) :
        ClassGroup W.CoordinateRing)
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (CoordinateRing.XYIdeal' h₂) :
        ClassGroup W.CoordinateRing)

Tactic:
simp only [hxy.left, hxy.right, add_of_Y_eq rfl rfl]

Premises used: WeierstrassCurve.Affine.Point.add_of_Y_eq, And.right, And.left, rfl
-- 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 : DecidableEq F
inst_8 : DecidableEq K
inst_9 : DecidableEq L
x₁ y₁ : F
h₁ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h₂ : W.Nonsingular x₂ y₂
hxy : x₁ = x₂ ∧ y₁ = W.negY x₂ y₂
⊢ 0 =
    HAdd.hAdd (α := Additive (ClassGroup W.CoordinateRing)) (β := Additive (ClassGroup W.CoordinateRing))
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (CoordinateRing.XYIdeal' (y := W.negY x₂ y₂) ⋯) :
        ClassGroup W.CoordinateRing)
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (CoordinateRing.XYIdeal' h₂) :
        ClassGroup W.CoordinateRing)

Tactic:
(CoordinateRing.mk_XYIdeal'_neg_mul h₂).symm

Premises used: Additive, WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_neg_mul, Quotient.map₂, ClassGroup, Eq.symm
-- 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 : DecidableEq F
inst_8 : DecidableEq K
inst_9 : DecidableEq L
x₁ y₁ : F
h₁ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h₂ : W.Nonsingular x₂ y₂
hxy : x₁ = x₂ ∧ y₁ = W.negY x₂ y₂
⊢ 0 =
    HAdd.hAdd (α := Additive (ClassGroup W.CoordinateRing)) (β := Additive (ClassGroup W.CoordinateRing))
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (CoordinateRing.XYIdeal' (y := W.negY x₂ y₂) ⋯) :
        ClassGroup W.CoordinateRing)
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (CoordinateRing.XYIdeal' h₂) :
        ClassGroup W.CoordinateRing)

Tactic:
exact (CoordinateRing.mk_XYIdeal'_neg_mul h₂).symm

Premises used: WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_neg_mul, Eq.symm
-- 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 : DecidableEq F
inst_8 : DecidableEq K
inst_9 : DecidableEq L
x₁ y₁ : F
h₁ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
neg :
  (ClassGroup.mk W.FunctionField :
        (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
      (CoordinateRing.XYIdeal' (x := W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) ⋯) =
    HAdd.hAdd (α := Additive (ClassGroup W.CoordinateRing)) (β := Additive (ClassGroup W.CoordinateRing))
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (CoordinateRing.XYIdeal' h₁) :
        ClassGroup W.CoordinateRing)
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (CoordinateRing.XYIdeal' h₂) :
        ClassGroup W.CoordinateRing)
⊢ (match (motive := W.Point → Additive (ClassGroup W.CoordinateRing)) some x₁ y₁ h₁ + some x₂ y₂ h₂ with
    | zero => 0
    | some x y h =>
      (ClassGroup.mk W.FunctionField :
          (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
        (CoordinateRing.XYIdeal' h)) =
    HAdd.hAdd (α := Additive (ClassGroup W.CoordinateRing)) (β := Additive (ClassGroup W.CoordinateRing))
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (CoordinateRing.XYIdeal' h₁) :
        ClassGroup W.CoordinateRing)
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (CoordinateRing.XYIdeal' h₂) :
        ClassGroup W.CoordinateRing)

Tactic:
simp only [add_some hxy]

Premises used: WeierstrassCurve.Affine.Point.add_some
-- 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 : DecidableEq F
inst_8 : DecidableEq K
inst_9 : DecidableEq L
x₁ y₁ : F
h₁ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ (ClassGroup.mk W.FunctionField :
        (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
      (CoordinateRing.XYIdeal' (x := W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) ⋯) =
    HAdd.hAdd (α := Additive (ClassGroup W.CoordinateRing)) (β := Additive (ClassGroup W.CoordinateRing))
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (CoordinateRing.XYIdeal' h₁) :
        ClassGroup W.CoordinateRing)
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (CoordinateRing.XYIdeal' h₂) :
        ClassGroup W.CoordinateRing)

Tactic:
(CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal' h₁ h₂ hxy).symm

Premises used: Additive, Quotient.map₂, WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal', ClassGroup, Eq.symm
-- 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 : DecidableEq F
inst_8 : DecidableEq K
inst_9 : DecidableEq L
x₁ y₁ : F
h₁ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ (ClassGroup.mk W.FunctionField :
        (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
      (CoordinateRing.XYIdeal' (x := W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) ⋯) =
    HAdd.hAdd (α := Additive (ClassGroup W.CoordinateRing)) (β := Additive (ClassGroup W.CoordinateRing))
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (CoordinateRing.XYIdeal' h₁) :
        ClassGroup W.CoordinateRing)
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (CoordinateRing.XYIdeal' h₂) :
        ClassGroup W.CoordinateRing)

Tactic:
exact (CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal' h₁ h₂ hxy).symm

Premises used: WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal', Eq.symm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
⊢ Eq.{u + 1} (α := Additive (ClassGroup W.CoordinateRing))
    ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) 0) 0

Tactic:
rfl

Premises used: 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.Nonsingular x y
⊢ Eq (α := Additive (ClassGroup W.CoordinateRing))
    ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) (some x y h) :
      Additive (ClassGroup W.CoordinateRing))
    ((ClassGroup.mk W.FunctionField :
          (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
        (CoordinateRing.XYIdeal' h) :
      ClassGroup W.CoordinateRing)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
P Q : W.Point
zero : HAdd.hAdd (α := W.Point) Point.zero Point.zero = 0 ↔ Eq.{u + 1} (α := W.Point) Point.zero (-Point.zero)
zero₁ : ∀ (x₂ y₂ : F) (h : W.Nonsingular x₂ y₂), Point.zero + Point.some x₂ y₂ h = 0 ↔ Point.zero = -Point.some x₂ y₂ h
some : ∀ (x₁ y₁ : F) (h : W.Nonsingular x₁ y₁), Point.some x₁ y₁ h + Point.zero = 0 ↔ Point.some x₁ y₁ h = -Point.zero
some₁ :
  ∀ (x₁ y₁ : F) (h : W.Nonsingular x₁ y₁) (x₂ y₂ : F) (h_1 : W.Nonsingular x₂ y₂),
    Point.some x₁ y₁ h + Point.some x₂ y₂ h_1 = 0 ↔ Point.some x₁ y₁ h = -Point.some x₂ y₂ h_1
⊢ P + Q = 0 ↔ P = -Q

Tactic:
rcases P, Q with ⟨_ | ⟨x₁, y₁, _⟩, _ | ⟨x₂, y₂, _⟩⟩
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
⊢ HAdd.hAdd (α := W.Point) zero zero = 0 ↔ Eq.{u + 1} (α := W.Point) zero (-zero)

Tactic:
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.Nonsingular x₁ y₁
⊢ some x₁ y₁ h + zero = 0 ↔ some x₁ y₁ h = -zero

Tactic:
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.Nonsingular x₂ y₂
zero : 0 + some x₂ y₂ h = 0 ↔ 0 = -some x₂ y₂ h
zero₁ : some x₂ y₂ h = 0 ↔ 0 = -some x₂ y₂ h
zero₂ : some x₂ y₂ h = 0 ↔ -some x₂ y₂ h = 0
zero₃ : some x₂ y₂ h = 0 ↔ some x₂ y₂ h = -0
zero₄ zero₅ : some x₂ y₂ h = 0 ↔ some x₂ y₂ h = 0
⊢ Point.zero + some x₂ y₂ h = 0 ↔ Point.zero = -some x₂ y₂ h

Tactic:
rw [← zero_def, zero_add, eq_comm (a := 0), neg_eq_iff_eq_neg, neg_zero]

Premises used: neg_eq_iff_eq_neg, WeierstrassCurve.Affine.Point.zero_def, eq_comm, zero_add, WeierstrassCurve.Affine.Point.neg_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.Nonsingular x₁ y₁
x₂ y₂ : F
h_1 : W.Nonsingular x₂ y₂
some : Point.some x₁ y₁ h + Point.some x₂ y₂ h_1 = 0 ↔ x₁ = x₂ ∧ y₁ = W.negY x₂ y₂
⊢ Point.some x₁ y₁ h + Point.some x₂ y₂ h_1 = 0 ↔ Point.some x₁ y₁ h = -Point.some x₂ y₂ h_1

Tactic:
rw [neg_some, some.injEq]

Premises used: WeierstrassCurve.Affine.Point.neg_some, WeierstrassCurve.Affine.Point.some.injEq
-- 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.Nonsingular x₁ y₁
x₂ y₂ : F
h_1 : W.Nonsingular x₂ y₂
some : Point.some x₁ y₁ h + Point.some x₂ y₂ h_1 = 0 → x₁ = x₂ ∧ y₁ = W.negY x₂ y₂
some₁ : x₁ = x₂ ∧ y₁ = W.negY x₂ y₂ → Point.some x₁ y₁ h + Point.some x₂ y₂ h_1 = 0
⊢ Point.some x₁ y₁ h + Point.some x₂ y₂ h_1 = 0 ↔ x₁ = x₂ ∧ y₁ = W.negY x₂ y₂

Tactic:
constructor
-- 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.Nonsingular x₁ y₁
x₂ y₂ : F
h_1 : W.Nonsingular x₂ y₂
some : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂) → ¬Point.some x₁ y₁ h + Point.some x₂ y₂ h_1 = 0
⊢ Point.some x₁ y₁ h + Point.some x₂ y₂ h_1 = 0 → x₁ = x₂ ∧ y₁ = W.negY x₂ y₂

Tactic:
contrapose
-- 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.Nonsingular x₁ y₁
x₂ y₂ : F
h_1 : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ ¬some x₁ y₁ h + some x₂ y₂ h_1 = 0

Tactic:
simpa only [add_some hxy] using some_ne_zero _

Premises used: WeierstrassCurve.Affine.Point.some_ne_zero, WeierstrassCurve.Affine.Point.add_some
-- 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.Nonsingular x₁ y₁
x₂ y₂ : F
h_1 : W.Nonsingular x₂ y₂
⊢ ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂) → ¬some x₁ y₁ h + some x₂ y₂ h_1 = 0

Tactic:
exact fun hxy => by simpa only [add_some hxy] using some_ne_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.Nonsingular x₁ y₁
x₂ y₂ : F
h_1 : W.Nonsingular x₂ y₂
⊢ x₁ = x₂ ∧ y₁ = W.negY x₂ y₂ → some x₁ y₁ h + some x₂ y₂ h_1 = 0

Tactic:
fun ⟨hx, hy⟩ => add_of_Y_eq hx hy

Premises used: WeierstrassCurve.Affine.Point.add_of_Y_eq, HAdd.hAdd, WeierstrassCurve.Affine.Point.some, OfNat.ofNat, Eq, _private.0.WeierstrassCurve.Affine.Point.add_eq_zero.match_1
-- 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.Nonsingular x₁ y₁
x₂ y₂ : F
h_1 : W.Nonsingular x₂ y₂
⊢ x₁ = x₂ ∧ y₁ = W.negY x₂ y₂ → some x₁ y₁ h + some x₂ y₂ h_1 = 0

Tactic:
exact fun ⟨hx, hy⟩ => add_of_Y_eq hx hy
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
P : W.Point
mp :
  Eq (α := Additive (ClassGroup W.CoordinateRing))
      ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) P : Additive (ClassGroup W.CoordinateRing))
      (0 : Additive (ClassGroup W.CoordinateRing)) →
    P = 0
mpr :
  P = 0 →
    Eq (α := Additive (ClassGroup W.CoordinateRing))
      ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) P : Additive (ClassGroup W.CoordinateRing))
      (0 : Additive (ClassGroup W.CoordinateRing))
⊢ Eq (α := Additive (ClassGroup W.CoordinateRing))
      ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) P : Additive (ClassGroup W.CoordinateRing))
      (0 : Additive (ClassGroup W.CoordinateRing)) ↔
    P = 0

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
P : W.Point
hP :
  Eq (α := Additive (ClassGroup W.CoordinateRing))
    ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) P : Additive (ClassGroup W.CoordinateRing))
    (0 : Additive (ClassGroup W.CoordinateRing))
mp :
  ∀
    (hP :
      Eq.{u + 1} (α := Additive (ClassGroup W.CoordinateRing))
        ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) zero :
          Additive (ClassGroup W.CoordinateRing))
        (0 : Additive (ClassGroup W.CoordinateRing))),
    Eq.{u + 1} (α := W.Point) zero 0
mp₁ :
  ∀ (x y : F) (h : W.Equation x y) (right : evalEval x y W.polynomialX ≠ 0 ∨ evalEval x y W.polynomialY ≠ 0)
    (hP :
      Eq (α := Additive (ClassGroup W.CoordinateRing))
        ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) (some x y ⋯) :
          Additive (ClassGroup W.CoordinateRing))
        (0 : Additive (ClassGroup W.CoordinateRing))),
    some x y ⋯ = 0
⊢ P = 0

Tactic:
rcases P with (_ | ⟨_, _, h, _⟩)
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
hP :
  Eq.{u + 1} (α := Additive (ClassGroup W.CoordinateRing))
    ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) zero : Additive (ClassGroup W.CoordinateRing))
    (0 : Additive (ClassGroup W.CoordinateRing))
⊢ Eq.{u + 1} (α := W.Point) zero 0

Tactic:
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
right : evalEval x y W.polynomialX ≠ 0 ∨ evalEval x y W.polynomialY ≠ 0
hP :
  Eq (α := Additive (ClassGroup W.CoordinateRing))
    ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) (some x y ⋯) :
      Additive (ClassGroup W.CoordinateRing))
    (0 : Additive (ClassGroup W.CoordinateRing))
⊢ (↑(CoordinateRing.XYIdeal' ⋯) : FractionalIdeal W.CoordinateRing⁰ (FractionRing W.CoordinateRing)) =
    (↑(CoordinateRing.XYIdeal W x ((C : (a : F) → F[X]) y)) :
      FractionalIdeal W.CoordinateRing⁰ (FractionRing W.CoordinateRing))

Tactic:
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
right : evalEval x y W.polynomialX ≠ 0 ∨ evalEval x y W.polynomialY ≠ 0
hP :
  Eq (α := Additive (ClassGroup W.CoordinateRing))
    ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) (some x y ⋯) :
      Additive (ClassGroup W.CoordinateRing))
    (0 : Additive (ClassGroup W.CoordinateRing))
mp :
  ∀ (p : W.CoordinateRing) (h0 : p ≠ 0)
    (hp : Eq (α := Ideal W.CoordinateRing) (CoordinateRing.XYIdeal W x ((C : (a : F) → F[X]) y)) (span {p})),
    some x y ⋯ = 0
⊢ some x y ⋯ = 0

Tactic:
rcases (ClassGroup.mk_eq_one_of_coe_ideal <| by rfl).mp hP with ⟨p, h0, hp⟩

Premises used: Iff.mp, ClassGroup.mk_eq_one_of_coe_ideal
-- 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
right : evalEval x y W.polynomialX ≠ 0 ∨ evalEval x y W.polynomialY ≠ 0
hP :
  Eq (α := Additive (ClassGroup W.CoordinateRing))
    ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) (some x y ⋯) :
      Additive (ClassGroup W.CoordinateRing))
    (0 : Additive (ClassGroup W.CoordinateRing))
p : W.CoordinateRing
h0 : p ≠ 0
hp : Eq (α := Ideal W.CoordinateRing) (CoordinateRing.XYIdeal W x ((C : (a : F) → F[X]) y)) (span {p})
apply : natDegree.{u} (R := F) ((Algebra.norm F[X] : (a : W.CoordinateRing) → F[X]) p) = 1
⊢ some x y ⋯ = 0

Tactic:
apply (p.natDegree_norm_ne_one _).elim

Premises used: WeierstrassCurve.Affine.CoordinateRing.natDegree_norm_ne_one, False.elim