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
p : W'.Point → Prop
p0 : p Point.zero
val : { xy : R × R // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) }
⊢ (fun (x : { P : W'.Point // p P }) ↦
        (match (motive :=
            { P : W'.Point // p P } →
              WithZero { xy : R × R // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) })
            x with
          | ⟨Point.zero, property⟩ => none
          | ⟨Point.some x y h, ph⟩ =>
            some
              (Subtype.mk (p := fun (xy : R × R) ↦ ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h)) (x, y)
                ⋯) :
          WithZero { xy : R × R // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) }))
      ((fun (P : WithZero { xy : R × R // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) }) ↦
          (Option.casesOn (motive :=
              fun (x : WithZero { xy : R × R // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) }) ↦
              { P : W'.Point // p P }) P (Subtype.mk (p := fun (P : W'.Point) ↦ p P) Point.zero p0)
              fun (xy : { xy : R × R // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) }) ↦
              Subtype.mk (p := fun (P : W'.Point) ↦ p P) (Point.some (↑xy : R × R).1 (↑xy : R × R).2 ⋯) ⋯ :
            { P : W'.Point // p P }))
        (some val)) =
    some val

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
p : W'.Point → Prop
p0 : p Point.zero
⊢ Eq (α := WithZero { xy : R × R // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) })
    ((nonsingularPointEquivSubtype (p := p) p0 :
          (a : { P : W'.Point // p P }) →
            WithZero { xy : R × R // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) })
        (Subtype.mk (p := fun (P : W'.Point) ↦ p P) Point.zero p0) :
      WithZero { xy : R × R // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) })
    (none : Option { xy : R × R // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) })

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y : R
h : W'.Nonsingular x y
p : W'.Point → Prop
p0 : p Point.zero
ph : p (Point.some x y h)
⊢ Eq (α := WithZero { xy : R × R // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) })
    ((nonsingularPointEquivSubtype (p := p) p0 :
          (a : { P : W'.Point // p P }) →
            WithZero { xy : R × R // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) })
        (Subtype.mk (p := fun (P : W'.Point) ↦ p P) (Point.some x y h) ph) :
      WithZero { xy : R × R // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) })
    (some (Subtype.mk (p := fun (xy : R × R) ↦ ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h)) (x, y) ⋯) :
      Option { xy : R × R // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) })

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
p : W'.Point → Prop
p0 : p Point.zero
⊢ ((nonsingularPointEquivSubtype (p := p) p0).symm :
        (a : WithZero { xy : R × R // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) }) →
          { P : W'.Point // p P })
      none =
    Subtype.mk (p := fun (P : W'.Point) ↦ p P) Point.zero p0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y : R
h : W'.Nonsingular x y
p : W'.Point → Prop
p0 : p Point.zero
ph : p (Point.some x y h)
⊢ ((nonsingularPointEquivSubtype (p := p) p0).symm :
        (a : WithZero { xy : R × R // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) }) →
          { P : W'.Point // p P })
      (some
        (Subtype.mk (p := fun (xy : R × R) ↦ ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h)) (x, y) ⋯)) =
    Subtype.mk (p := fun (P : W'.Point) ↦ p P) (Point.some x y h) ph

Tactic:
rfl

Premises used: 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
⊢ Eq.{max 1 (r + 1)} (α := R × R → Prop)
    (fun (xy : R × R) ↦
      ∃ (h : W'.Nonsingular xy.1 xy.2), Membership.mem (γ := Set W'.Point) Set.univ (Point.some xy.1 xy.2 h))
    fun (xy : R × R) ↦ W'.Nonsingular xy.1 xy.2

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
⊢ Eq (α := WithZero { xy : R × R // W'.Nonsingular xy.1 xy.2 })
    ((W'.nonsingularPointEquiv : (a : W'.Point) → WithZero { xy : R × R // W'.Nonsingular xy.1 xy.2 }) Point.zero :
      WithZero { xy : R × R // W'.Nonsingular xy.1 xy.2 })
    (none : Option { xy : R × R // W'.Nonsingular xy.1 xy.2 })

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y : R
h : W'.Nonsingular x y
⊢ Eq (α := WithZero { xy : R × R // W'.Nonsingular xy.1 xy.2 })
    ((W'.nonsingularPointEquiv : (a : W'.Point) → WithZero { xy : R × R // W'.Nonsingular xy.1 xy.2 })
        (Point.some x y h) :
      WithZero { xy : R × R // W'.Nonsingular xy.1 xy.2 })
    (some (Subtype.mk (p := fun (xy : R × R) ↦ W'.Nonsingular xy.1 xy.2) (x, y) h) :
      Option { xy : R × R // W'.Nonsingular xy.1 xy.2 })

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
⊢ Eq (α := W'.Point)
    ((Equiv.symm W'.nonsingularPointEquiv : (a : WithZero { xy : R × R // W'.Nonsingular xy.1 xy.2 }) → W'.Point) none :
      W'.Point)
    (Point.zero : W'.Point)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y : R
h : W'.Nonsingular x y
⊢ (Equiv.symm W'.nonsingularPointEquiv : (a : WithZero { xy : R × R // W'.Nonsingular xy.1 xy.2 }) → W'.Point)
      (some (Subtype.mk (p := fun (xy : R × R) ↦ W'.Nonsingular xy.1 xy.2) (x, y) h)) =
    Point.some x y h

Tactic:
rfl

Premises used: 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 : Nontrivial R
inst_8 : WeierstrassCurve.IsElliptic W'
p : W'.Point → Prop
p0 : p Point.zero
h :
  ∀ (x : R × R),
    (∃ (h : W'.Nonsingular x.1 x.2), p (Point.some x.1 x.2 h)) ↔ ∃ (h : W'.Equation x.1 x.2), p (Point.mk h)
⊢ Eq.{max 1 (r + 1)} (α := R × R → Prop)
    (fun (xy : R × R) ↦ ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h)) fun (xy : R × R) ↦
    ∃ (h : W'.Equation xy.1 xy.2), p (Point.mk h)

Tactic:
ext
-- 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 : Nontrivial R
inst_8 : WeierstrassCurve.IsElliptic W'
p : W'.Point → Prop
p0 : p Point.zero
x : R × R
⊢ (∃ (h : W'.Nonsingular x.1 x.2), p (Point.some x.1 x.2 h)) ↔ ∃ (h : W'.Equation x.1 x.2), p (Point.mk h)

Tactic:
simp [equation_iff_nonsingular, Point.mk]

Premises used: WeierstrassCurve.Affine.equation_iff_nonsingular, WeierstrassCurve.Affine.Point.mk
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : Nontrivial R
inst_2 : WeierstrassCurve.IsElliptic W'
p : W'.Point → Prop
p0 : p Point.zero
⊢ Eq (α := WithZero { xy : R × R // ∃ (h : W'.Equation xy.1 xy.2), p (Point.mk h) })
    ((pointEquivSubtype (p := p) p0 :
          (a : { P : W'.Point // p P }) → WithZero { xy : R × R // ∃ (h : W'.Equation xy.1 xy.2), p (Point.mk h) })
        (Subtype.mk (p := fun (P : W'.Point) ↦ p P) Point.zero p0) :
      WithZero { xy : R × R // ∃ (h : W'.Equation xy.1 xy.2), p (Point.mk h) })
    (none : Option { xy : R × R // ∃ (h : W'.Equation xy.1 xy.2), p (Point.mk h) })

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : Nontrivial R
inst_2 : WeierstrassCurve.IsElliptic W'
x y : R
h : W'.Equation x y
p : W'.Point → Prop
p0 : p Point.zero
ph : p (Point.mk h)
⊢ Eq (α := WithZero { xy : R × R // ∃ (h : W'.Equation xy.1 xy.2), p (Point.mk h) })
    ((pointEquivSubtype (p := p) p0 :
          (a : { P : W'.Point // p P }) → WithZero { xy : R × R // ∃ (h : W'.Equation xy.1 xy.2), p (Point.mk h) })
        (Subtype.mk (p := fun (P : W'.Point) ↦ p P) (Point.mk h) ph) :
      WithZero { xy : R × R // ∃ (h : W'.Equation xy.1 xy.2), p (Point.mk h) })
    (some (Subtype.mk (p := fun (xy : R × R) ↦ ∃ (h : W'.Equation xy.1 xy.2), p (Point.mk h)) (x, y) ⋯) :
      Option { xy : R × R // ∃ (h : W'.Equation xy.1 xy.2), p (Point.mk h) })

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : Nontrivial R
inst_2 : WeierstrassCurve.IsElliptic W'
p : W'.Point → Prop
p0 : p Point.zero
⊢ (Equiv.symm (pointEquivSubtype (p := p) p0) :
        (a : WithZero { xy : R × R // ∃ (h : W'.Equation xy.1 xy.2), p (Point.mk h) }) → { P : W'.Point // p P })
      none =
    Subtype.mk (p := fun (P : W'.Point) ↦ p P) Point.zero p0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : Nontrivial R
inst_2 : WeierstrassCurve.IsElliptic W'
x y : R
h : W'.Equation x y
p : W'.Point → Prop
p0 : p Point.zero
ph : p (Point.mk h)
⊢ (Equiv.symm (pointEquivSubtype (p := p) p0) :
        (a : WithZero { xy : R × R // ∃ (h : W'.Equation xy.1 xy.2), p (Point.mk h) }) → { P : W'.Point // p P })
      (some (Subtype.mk (p := fun (xy : R × R) ↦ ∃ (h : W'.Equation xy.1 xy.2), p (Point.mk h)) (x, y) ⋯)) =
    Subtype.mk (p := fun (P : W'.Point) ↦ p P) (Point.mk h) ph

Tactic:
rfl

Premises used: WeierstrassCurve.Affine.Point.mk, 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 : Nontrivial R
inst_8 : WeierstrassCurve.IsElliptic W'
⊢ Eq.{max 1 (r + 1)} (α := R × R → Prop)
    (fun (xy : R × R) ↦ ∃ (h : W'.Equation xy.1 xy.2), Membership.mem (γ := Set W'.Point) Set.univ (Point.mk h))
    fun (xy : R × R) ↦ W'.Equation xy.1 xy.2

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : Nontrivial R
inst_2 : WeierstrassCurve.IsElliptic W'
⊢ Eq (α := WithZero { xy : R × R // W'.Equation xy.1 xy.2 })
    ((W'.pointEquiv : (a : W'.Point) → WithZero { xy : R × R // W'.Equation xy.1 xy.2 }) Point.zero :
      WithZero { xy : R × R // W'.Equation xy.1 xy.2 })
    (none : Option { xy : R × R // W'.Equation xy.1 xy.2 })

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : Nontrivial R
inst_2 : WeierstrassCurve.IsElliptic W'
x y : R
h : W'.Equation x y
⊢ Eq (α := WithZero { xy : R × R // W'.Equation xy.1 xy.2 })
    ((W'.pointEquiv : (a : W'.Point) → WithZero { xy : R × R // W'.Equation xy.1 xy.2 }) (Point.mk h) :
      WithZero { xy : R × R // W'.Equation xy.1 xy.2 })
    (some (Subtype.mk (p := fun (xy : R × R) ↦ W'.Equation xy.1 xy.2) (x, y) h) :
      Option { xy : R × R // W'.Equation xy.1 xy.2 })

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : Nontrivial R
inst_2 : WeierstrassCurve.IsElliptic W'
⊢ Eq (α := W'.Point)
    ((Equiv.symm W'.pointEquiv : (a : WithZero { xy : R × R // W'.Equation xy.1 xy.2 }) → W'.Point) none : W'.Point)
    (Point.zero : W'.Point)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : Nontrivial R
inst_2 : WeierstrassCurve.IsElliptic W'
x y : R
h : W'.Equation x y
⊢ (Equiv.symm W'.pointEquiv : (a : WithZero { xy : R × R // W'.Equation xy.1 xy.2 }) → W'.Point)
      (some (Subtype.mk (p := fun (xy : R × R) ↦ W'.Equation xy.1 xy.2) (x, y) h)) =
    Point.mk h

Tactic:
rfl

Premises used: WeierstrassCurve.Affine.Point.mk, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
⊢ Eq.{r + 1} (α := W'.Point) 0 zero

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
P : W'.Point
⊢ -P = P.neg

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
⊢ Eq.{r + 1} (α := W'.Point) (-0) 0

Tactic:
rfl

Premises used: WeierstrassCurve.Affine.Point.neg, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y : R
h : W'.Nonsingular x y
⊢ -some x y h = some x (W'.negY x y) ⋯

Tactic:
rfl

Premises used: WeierstrassCurve.Affine.Point.neg, 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
⊢ Eq.{r + 1} (α := W'.Point) (- -zero) zero

Tactic:
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
x y : R
h : W'.Nonsingular x y
⊢ - -some x y h = some x y h

Tactic:
simp only [neg_some, negY_negY]

Premises used: WeierstrassCurve.Affine.Point.neg_some, WeierstrassCurve.Affine.negY_negY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
x₁ y₁ x₂ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
H : some x₁ y₁ h₁ = some x₂ y₂ h₂ ∨ some x₁ y₁ h₁ = -some x₂ y₂ h₂
⊢ x₁ = x₂

Tactic:
grind [neg_some]

Premises used: WeierstrassCurve.Affine.Point.neg_some
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
x₁ y₁ x₂ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
refine : ∀ (H : x₁ = x₂), some x₁ y₁ h₁ = some x₂ y₂ h₂ ∨ some x₁ y₁ h₁ = -some x₂ y₂ h₂
⊢ x₁ = x₂ ↔ some x₁ y₁ h₁ = some x₂ y₂ h₂ ∨ some x₁ y₁ h₁ = -some x₂ y₂ h₂

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ by grind [neg_some]⟩
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
x₁ y₁ x₂ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
H : x₁ = x₂
simp_rw : x₁ = x₂ ∧ (y₁ = y₂ ∨ y₁ = W.negY x₂ y₂)
⊢ some x₁ y₁ h₁ = some x₂ y₂ h₂ ∨ some x₁ y₁ h₁ = -some x₂ y₂ h₂

Tactic:
simp_rw [neg_some, some.injEq, ← and_or_left]

Premises used: and_or_left, 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
x₁ y₁ x₂ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
H : x₁ = x₂
⊢ x₁ = x₂ ∧ (y₁ = y₂ ∨ y₁ = W.negY x₂ y₂)

Tactic:
⟨H, Y_eq_of_X_eq h₁.1 h₂.1 H⟩

Premises used: WeierstrassCurve.Affine.Y_eq_of_X_eq, And.left, And.intro
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
x₁ y₁ x₂ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
H : x₁ = x₂
⊢ x₁ = x₂ ∧ (y₁ = y₂ ∨ y₁ = W.negY x₂ y₂)

Tactic:
exact ⟨H, Y_eq_of_X_eq h₁.1 h₂.1 H⟩
-- 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
⊢ HAdd.hAdd (α := W.Point) 0 zero = zero

Tactic:
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
⊢ 0 + some x y h = some x y h

Tactic:
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
⊢ HAdd.hAdd (α := W.Point) zero 0 = zero

Tactic:
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
⊢ some x y h + 0 = some x y h

Tactic:
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
⊢ P + Q = P.add Q

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₁ x₂ y₁ y₂ : F
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
⊢ some x₁ y₁ h₁ + some x₂ y₂ h₂ = some (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂)) ⋯

Tactic:
simp only [add_def, add, dif_neg hxy]

Premises used: WeierstrassCurve.Affine.Point.add_def, dif_neg, WeierstrassCurve.Affine.Point.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.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hx : x₁ = x₂
hy : y₁ = W.negY x₂ y₂
⊢ some x₁ y₁ h₁ + some x₂ y₂ h₂ = 0

Tactic:
simpa only [add_def, add] using dif_pos ⟨hx, hy⟩

Premises used: dif_pos, WeierstrassCurve.Affine.Point.add_def, WeierstrassCurve.Affine.Point.add
-- 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₁
hy : y₁ = W.negY x₁ y₁
⊢ some x₁ y₁ h₁ + some x₁ y₁ h₁ = 0

Tactic:
add_of_Y_eq rfl hy

Premises used: WeierstrassCurve.Affine.Point.add_of_Y_eq, rfl
-- 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.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hy : y₁ ≠ W.negY x₂ y₂
⊢ some x₁ y₁ h₁ + some x₂ y₂ h₂ = some (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂)) ⋯

Tactic:
add_some fun hxy => hy hxy.right

Premises used: And.right, 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₁ x₂ y₁ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hy : y₁ ≠ W.negY x₂ y₂
⊢ some x₁ y₁ h₁ + some x₂ y₂ h₂ =
    -some (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂)) ⋯

Tactic:
add_of_Y_ne hy

Premises used: WeierstrassCurve.Affine.Point.neg, WeierstrassCurve.Affine.Point.add_of_Y_ne, WeierstrassCurve.Affine.addY
-- 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₁
hy : y₁ ≠ W.negY x₁ y₁
⊢ some x₁ y₁ h₁ + some x₁ y₁ h₁ = some (W.addX x₁ x₁ (W.slope x₁ x₁ y₁ y₁)) (W.addY x₁ x₁ y₁ (W.slope x₁ x₁ y₁ y₁)) ⋯

Tactic:
add_of_Y_ne hy

Premises used: WeierstrassCurve.Affine.Point.add_of_Y_ne
-- 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₁
hy : y₁ ≠ W.negY x₁ y₁
⊢ some x₁ y₁ h₁ + some x₁ y₁ h₁ =
    -some (W.addX x₁ x₁ (W.slope x₁ x₁ y₁ y₁)) (W.negAddY x₁ x₁ y₁ (W.slope x₁ x₁ y₁ y₁)) ⋯

Tactic:
add_of_Y_ne hy

Premises used: WeierstrassCurve.Affine.Point.neg, WeierstrassCurve.Affine.Point.add_of_Y_ne, WeierstrassCurve.Affine.addY
-- 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.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hx : x₁ ≠ x₂
⊢ some x₁ y₁ h₁ + some x₂ y₂ h₂ = some (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂)) ⋯

Tactic:
add_some fun hxy => hx hxy.left

Premises used: And.left, 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₁ x₂ y₁ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hx : x₁ ≠ x₂
⊢ some x₁ y₁ h₁ + some x₂ y₂ h₂ =
    -some (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂)) ⋯

Tactic:
add_of_X_ne hx

Premises used: WeierstrassCurve.Affine.Point.add_of_X_ne, WeierstrassCurve.Affine.Point.neg, WeierstrassCurve.Affine.addY
-- 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
⊢ (match (motive := W.Point → Additive (ClassGroup W.CoordinateRing)) HAdd.hAdd (α := W.Point) zero 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)) 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)) 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