awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian F
inst_1 : DecidableEq F
point : PointClass F
a : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a)
point_1 : PointClass F
a_1 : Fin 3 → F
hQ : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a_1)
⊢ ({ point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a, nonsingular := hP :
          W.Point } +
        { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a_1,
          nonsingular := hQ : W.Point }).toAffineLift =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a, nonsingular := hP :
          W.Point }.toAffineLift +
      { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a_1,
          nonsingular := hQ : W.Point }.toAffineLift

Tactic:
toAffine_add hP hQ

Premises used: WeierstrassCurve.Jacobian.Point.toAffine_add, WeierstrassCurve.Jacobian.Point.toAffineLift
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian F
inst_1 : DecidableEq F
point : PointClass F
a : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a)
point_1 : PointClass F
a_1 : Fin 3 → F
hQ : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a_1)
⊢ ({ point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a, nonsingular := hP :
          W.Point } +
        { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a_1,
          nonsingular := hQ : W.Point }).toAffineLift =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a, nonsingular := hP :
          W.Point }.toAffineLift +
      { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a_1,
          nonsingular := hQ : W.Point }.toAffineLift

Tactic:
exact toAffine_add hP hQ

Premises used: WeierstrassCurve.Jacobian.Point.toAffine_add
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Jacobian R
W : Jacobian F
inst_6 : DecidableEq F
point : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P)
pos :
  ∀ (hPz : P z = 0),
    fromAffine
        { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P,
            nonsingular := hP : W.Point }.toAffineLift =
      { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P,
        nonsingular := hP }
neg :
  ∀ (hPz : ¬P z = 0),
    fromAffine
        { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P,
            nonsingular := hP : W.Point }.toAffineLift =
      { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P,
        nonsingular := hP }
⊢ fromAffine
      { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P,
          nonsingular := hP : W.Point }.toAffineLift =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P, nonsingular := hP }

Tactic:
by_cases hPz : P z = 0

Premises used: OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Jacobian R
W : Jacobian F
inst_6 : DecidableEq F
point : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P)
hPz : P z = 0
pos :
  Point.point (W' := W) (fromAffine 0) =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P, nonsingular := hP :
        W.Point }.point
⊢ fromAffine
      { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P,
          nonsingular := hP : W.Point }.toAffineLift =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P, nonsingular := hP }

Tactic:
rw [Point.ext_iff, toAffineLift_eq, toAffine_of_Z_eq_zero hPz]

Premises used: WeierstrassCurve.Jacobian.Point.toAffine_of_Z_eq_zero, WeierstrassCurve.Jacobian.Point.ext_iff, WeierstrassCurve.Jacobian.Point.toAffineLift_eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Jacobian R
W : Jacobian F
inst_6 : DecidableEq F
point : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P)
hPz : P z = 0
⊢ Point.point (W' := W) (fromAffine 0) =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P, nonsingular := hP :
        W.Point }.point

Tactic:
Quotient.eq.mpr <| Setoid.symm <| equiv_zero_of_Z_eq_zero hP hPz

Premises used: Iff.mpr, WeierstrassCurve.Jacobian.equiv_zero_of_Z_eq_zero, Setoid.symm, Quotient.eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Jacobian R
W : Jacobian F
inst_6 : DecidableEq F
point : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P)
hPz : P z = 0
⊢ Point.point (W' := W) (fromAffine 0) =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P, nonsingular := hP :
        W.Point }.point

Tactic:
exact Quotient.eq.mpr <| Setoid.symm <| equiv_zero_of_Z_eq_zero hP hPz

Premises used: Iff.mpr, WeierstrassCurve.Jacobian.equiv_zero_of_Z_eq_zero, Setoid.symm, Quotient.eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Jacobian R
W : Jacobian F
inst_6 : DecidableEq F
point : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P)
hPz : ¬P z = 0
neg :
  (fromAffine (Affine.Point.some (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) ⋯)).point =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P, nonsingular := hP :
        W.Point }.point
⊢ fromAffine
      { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P,
          nonsingular := hP : W.Point }.toAffineLift =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P, nonsingular := hP }

Tactic:
rw [Point.ext_iff, toAffineLift_eq, toAffine_of_Z_ne_zero hP hPz]

Premises used: WeierstrassCurve.Jacobian.Point.toAffine_of_Z_ne_zero, WeierstrassCurve.Jacobian.Point.ext_iff, WeierstrassCurve.Jacobian.Point.toAffineLift_eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Jacobian R
W : Jacobian F
inst_6 : DecidableEq F
point : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P)
hPz : ¬P z = 0
⊢ (fromAffine (Affine.Point.some (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) ⋯)).point =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P, nonsingular := hP :
        W.Point }.point

Tactic:
Quotient.eq.mpr <| Setoid.symm <| equiv_some_of_Z_ne_zero hPz

Premises used: Iff.mpr, Setoid.symm, WeierstrassCurve.Jacobian.equiv_some_of_Z_ne_zero, Quotient.eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Jacobian R
W : Jacobian F
inst_6 : DecidableEq F
point : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P)
hPz : ¬P z = 0
⊢ (fromAffine (Affine.Point.some (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) ⋯)).point =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P, nonsingular := hP :
        W.Point }.point

Tactic:
exact Quotient.eq.mpr <| Setoid.symm <| equiv_some_of_Z_ne_zero hPz

Premises used: Iff.mpr, Setoid.symm, WeierstrassCurve.Jacobian.equiv_some_of_Z_ne_zero, Quotient.eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Jacobian R
W : Jacobian F
inst_6 : DecidableEq F
zero : Eq.{u + 1} (α := W.toAffine.Point) (toAffineLift (fromAffine 0)) 0
zero₁ : Eq.{u + 1} (α := W.toAffine.Point) (toAffineLift 0) 0
zero₂ zero₃ : Eq.{u + 1} (α := W.toAffine.Point) 0 0
⊢ Eq.{u + 1} (α := W.toAffine.Point) (toAffineLift (fromAffine Affine.Point.zero)) Affine.Point.zero

Tactic:
rw [← Affine.Point.zero_def, fromAffine_zero, toAffineLift_zero]

Premises used: WeierstrassCurve.Affine.Point.zero_def, WeierstrassCurve.Jacobian.Point.toAffineLift_zero, WeierstrassCurve.Jacobian.Point.fromAffine_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Jacobian R
W : Jacobian F
inst_6 : DecidableEq F
x y : F
h : W.toAffine.Nonsingular «x» «y»
some : { point := ⟦![«x», «y», 1]⟧, nonsingular := ⋯ : W.Point }.toAffineLift = Affine.Point.some «x» «y» h
some₁ some₂ : Affine.Point.some «x» «y» ⋯ = Affine.Point.some «x» «y» h
⊢ (fromAffine (Affine.Point.some «x» «y» h)).toAffineLift = Affine.Point.some «x» «y» h

Tactic:
rw [fromAffine_some, toAffineLift_some]

Premises used: WeierstrassCurve.Jacobian.Point.toAffineLift_some, WeierstrassCurve.Jacobian.Point.fromAffine_some
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Jacobian R
W : Jacobian F
x x_1 x_2 : W.Point
a :
  Eq (α := W.toAffine.Point)
    ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) («x» + x_1 + x_2) : W.toAffine.Point)
    ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) («x» + (x_1 + x_2)) : W.toAffine.Point)
⊢ «x» + x_1 + x_2 = «x» + (x_1 + x_2)

Tactic:
apply (toAffineAddEquiv W).injective

Premises used: WeierstrassCurve.Jacobian.Point.toAffineAddEquiv, AddEquiv.injective
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Jacobian R
W : Jacobian F
x x_1 x_2 : W.Point
⊢ Eq (α := W.toAffine.Point)
    ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) («x» + x_1 + x_2) : W.toAffine.Point)
    ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) («x» + (x_1 + x_2)) : W.toAffine.Point)

Tactic:
simp only [map_add, add_assoc]

Premises used: add_assoc, map_add
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Jacobian R
W : Jacobian F
x x_1 x_2 : W.Point
a :
  Eq (α := W.toAffine.Point)
    ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) («x» + x_1 + x_2) : W.toAffine.Point)
    ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) («x» + (x_1 + x_2)) : W.toAffine.Point)
⊢ «x» + x_1 + x_2 = «x» + (x_1 + x_2)

Tactic:
classical
    apply (toAffineAddEquiv W).injective
    simp only [map_add, add_assoc]

Premises used: add_assoc, map_add
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Jacobian R
W : Jacobian F
x : W.Point
a :
  Eq (α := W.toAffine.Point) ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) (0 + «x») : W.toAffine.Point)
    ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) «x» : W.toAffine.Point)
⊢ 0 + «x» = «x»

Tactic:
apply (toAffineAddEquiv W).injective

Premises used: WeierstrassCurve.Jacobian.Point.toAffineAddEquiv, AddEquiv.injective
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Jacobian R
W : Jacobian F
x : W.Point
⊢ Eq (α := W.toAffine.Point) ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) (0 + «x») : W.toAffine.Point)
    ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) «x» : W.toAffine.Point)

Tactic:
simp only [map_add, toAffineAddEquiv_apply, toAffineLift_zero, zero_add]

Premises used: map_add, zero_add, WeierstrassCurve.Jacobian.Point.toAffineAddEquiv_apply, WeierstrassCurve.Jacobian.Point.toAffineLift_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Jacobian R
W : Jacobian F
x : W.Point
a :
  Eq (α := W.toAffine.Point) ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) (0 + «x») : W.toAffine.Point)
    ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) «x» : W.toAffine.Point)
⊢ 0 + «x» = «x»

Tactic:
classical
    apply (toAffineAddEquiv W).injective
    simp only [map_add, toAffineAddEquiv_apply, toAffineLift_zero, zero_add]

Premises used: map_add, zero_add, WeierstrassCurve.Jacobian.Point.toAffineAddEquiv_apply, WeierstrassCurve.Jacobian.Point.toAffineLift_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Jacobian R
W : Jacobian F
x : W.Point
a :
  Eq (α := W.toAffine.Point) ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) («x» + 0) : W.toAffine.Point)
    ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) «x» : W.toAffine.Point)
⊢ «x» + 0 = «x»

Tactic:
apply (toAffineAddEquiv W).injective

Premises used: WeierstrassCurve.Jacobian.Point.toAffineAddEquiv, AddEquiv.injective
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Jacobian R
W : Jacobian F
x : W.Point
⊢ Eq (α := W.toAffine.Point) ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) («x» + 0) : W.toAffine.Point)
    ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) «x» : W.toAffine.Point)

Tactic:
simp only [map_add, toAffineAddEquiv_apply, toAffineLift_zero, add_zero]

Premises used: map_add, WeierstrassCurve.Jacobian.Point.toAffineAddEquiv_apply, WeierstrassCurve.Jacobian.Point.toAffineLift_zero, add_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Jacobian R
W : Jacobian F
x : W.Point
a :
  Eq (α := W.toAffine.Point) ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) («x» + 0) : W.toAffine.Point)
    ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) «x» : W.toAffine.Point)
⊢ «x» + 0 = «x»

Tactic:
classical
    apply (toAffineAddEquiv W).injective
    simp only [map_add, toAffineAddEquiv_apply, toAffineLift_zero, add_zero]

Premises used: map_add, WeierstrassCurve.Jacobian.Point.toAffineAddEquiv_apply, WeierstrassCurve.Jacobian.Point.toAffineLift_zero, add_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Jacobian R
W : Jacobian F
P : W.Point
a :
  Eq (α := W.toAffine.Point) ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) (-P + P) : W.toAffine.Point)
    ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) 0 : W.toAffine.Point)
⊢ -P + P = 0

Tactic:
apply (toAffineAddEquiv W).injective

Premises used: WeierstrassCurve.Jacobian.Point.toAffineAddEquiv, AddEquiv.injective
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Jacobian R
W : Jacobian F
P : W.Point
⊢ Eq (α := W.toAffine.Point) ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) (-P + P) : W.toAffine.Point)
    ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) 0 : W.toAffine.Point)

Tactic:
simp only [map_add, toAffineAddEquiv_apply, toAffineLift_neg, neg_add_cancel, toAffineLift_zero]

Premises used: WeierstrassCurve.Jacobian.Point.toAffineLift_neg, map_add, WeierstrassCurve.Jacobian.Point.toAffineAddEquiv_apply, neg_add_cancel, WeierstrassCurve.Jacobian.Point.toAffineLift_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Jacobian R
W : Jacobian F
P : W.Point
a :
  Eq (α := W.toAffine.Point) ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) (-P + P) : W.toAffine.Point)
    ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) 0 : W.toAffine.Point)
⊢ -P + P = 0

Tactic:
classical
    apply (toAffineAddEquiv W).injective
    simp only [map_add, toAffineAddEquiv_apply, toAffineLift_neg, neg_add_cancel, toAffineLift_zero]

Premises used: WeierstrassCurve.Jacobian.Point.toAffineLift_neg, map_add, WeierstrassCurve.Jacobian.Point.toAffineAddEquiv_apply, neg_add_cancel, WeierstrassCurve.Jacobian.Point.toAffineLift_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Jacobian R
W : Jacobian F
x x_1 : W.Point
a :
  Eq (α := W.toAffine.Point) ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) («x» + x_1) : W.toAffine.Point)
    ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) (x_1 + «x») : W.toAffine.Point)
⊢ «x» + x_1 = x_1 + «x»

Tactic:
apply (toAffineAddEquiv W).injective

Premises used: WeierstrassCurve.Jacobian.Point.toAffineAddEquiv, AddEquiv.injective
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Jacobian R
W : Jacobian F
x x_1 : W.Point
⊢ Eq (α := W.toAffine.Point) ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) («x» + x_1) : W.toAffine.Point)
    ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) (x_1 + «x») : W.toAffine.Point)

Tactic:
simp only [map_add, add_comm]

Premises used: map_add, add_comm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Jacobian R
W : Jacobian F
x x_1 : W.Point
a :
  Eq (α := W.toAffine.Point) ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) («x» + x_1) : W.toAffine.Point)
    ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) (x_1 + «x») : W.toAffine.Point)
⊢ «x» + x_1 = x_1 + «x»

Tactic:
classical
    apply (toAffineAddEquiv W).injective
    simp only [map_add, add_comm]

Premises used: map_add, add_comm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Jacobian R
f : R →+* S
P : Fin 3 → R
simp :
  Eq.{s + 1} (α := Fin 3 → S)
    (![((⇑f : (a : R) → S) ∘ P) x, (f : (a : R) → S) (W'.negY P), ((⇑f : (a : R) → S) ∘ P) z] : Fin (Nat.succ 2) → S)
    (![(f : (a : R) → S) (P x), (f : (a : R) → S) (W'.negY P), (f : (a : R) → S) (P z)] :
      Fin (Nat.succ 0).succ.succ → S)
⊢ (W'.map f).neg ((⇑f : (a : R) → S) ∘ P) = (⇑f : (a : R) → S) ∘ W'.neg P

Tactic:
simp only [neg, map_negY, comp_fin3]

Premises used: WeierstrassCurve.Jacobian.map_negY, WeierstrassCurve.Jacobian.neg, WeierstrassCurve.Jacobian.comp_fin3
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Jacobian R
f : R →+* S
P : Fin 3 → R
⊢ Eq.{s + 1} (α := Fin 3 → S)
    (![((⇑f : (a : R) → S) ∘ P) x, (f : (a : R) → S) (W'.negY P), ((⇑f : (a : R) → S) ∘ P) z] : Fin (Nat.succ 2) → S)
    (![(f : (a : R) → S) (P x), (f : (a : R) → S) (W'.negY P), (f : (a : R) → S) (P z)] :
      Fin (Nat.succ 0).succ.succ → S)

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
W : Jacobian F
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
pos : ∀ (h : P ≈ Q), (W.map f).add ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ W.add P Q
neg : ∀ (h : ¬P ≈ Q), (W.map f).add ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ W.add P Q
⊢ (W.map f).add ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ W.add P Q

Tactic:
by_cases h : P ≈ Q
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
W : Jacobian F
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : P ≈ Q
pos : (W.map f).dblXYZ ((⇑f : (a : F) → K) ∘ P) = (⇑f : (a : F) → K) ∘ W.add P Q
pos₁ : (W.map f).dblXYZ ((⇑f : (a : F) → K) ∘ P) = (⇑f : (a : F) → K) ∘ W.dblXYZ P
pos₂ pos₃ : Eq.{v + 1} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ W.dblXYZ P) ((⇑f : (a : F) → K) ∘ W.dblXYZ P)
⊢ (W.map f).add ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ W.add P Q

Tactic:
rw [add_of_equiv <| (comp_equiv_comp f hP hQ).mpr h, add_of_equiv h, map_dblXYZ]

Premises used: Iff.mpr, WeierstrassCurve.Jacobian.comp_equiv_comp, WeierstrassCurve.Jacobian.map_dblXYZ, WeierstrassCurve.Jacobian.add_of_equiv