awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
inst_1 : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy :
  ¬(P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2 ∧
      P y * HPow.hPow (β := ℕ) (Q z) 3 = W.negY Q * HPow.hPow (β := ℕ) (P z) 3)
this :
  toAffine W
      ![W.toAffine.addX (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
          (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
            (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3)),
        W.toAffine.addY (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
          (P y / HPow.hPow (β := ℕ) (P z) 3)
          (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
            (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3)),
        1] =
    HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
hx : ¬P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
⊢ toAffine W (W.add P Q) = HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
have neg : toAffine W
    (addZ P Q •
      ![W.toAffine.addX (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
          (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
            (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3)),
        W.toAffine.addY (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
          (P y / HPow.hPow (β := ℕ) (P z) 3)
          (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
            (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3)),
        1]) =
  HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
Tactic: rwa [add_of_X_ne hP.left hQ.left hPz hQz hx, toAffine_smul _ <| isUnit_addZ_of_X_ne hx]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : W.Point
⊢ (-P).toAffineLift = -P.toAffineLift
have mk : ∀ {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 := 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,
          nonsingular := hP }.toAffineLift
Tactic: rcases P with @⟨⟨_⟩, hP⟩
Cleared hypotheses: P
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
inst_1 : DecidableEq F
P Q : W.Point
⊢ (P + Q).toAffineLift = P.toAffineLift + Q.toAffineLift
have mk : ∀ {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 : 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: rcases P, Q with ⟨@⟨⟨_⟩, hP⟩, @⟨⟨_⟩, hQ⟩⟩
Cleared hypotheses: P, Q
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
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)
⊢ 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 }
have 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 }
Tactic: by_cases hPz : P z = 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
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 }
⊢ 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 }
have 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 }
Tactic: by_cases hPz : P z = 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
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
      { 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 }
have 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
Tactic: rw [Point.ext_iff, toAffineLift_eq, toAffine_of_Z_eq_zero hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
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
      { 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 }
have neg : (fromAffine (Affine.Point.some (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) sorry)).point =
  { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P, nonsingular := hP :
      W.Point }.point
Tactic: rw [Point.ext_iff, toAffineLift_eq, toAffine_of_Z_ne_zero hP hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
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
⊢ Eq.{u + 1} (α := W.toAffine.Point) (toAffineLift (fromAffine Affine.Point.zero)) Affine.Point.zero
have zero : Eq.{u + 1} (α := W.toAffine.Point) (toAffineLift (fromAffine 0)) 0
Tactic: rw [← Affine.Point.zero_def, fromAffine_zero, toAffineLift_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
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
⊢ Eq.{u + 1} (α := W.toAffine.Point) (toAffineLift (fromAffine Affine.Point.zero)) Affine.Point.zero
have zero₁ : Eq.{u + 1} (α := W.toAffine.Point) (toAffineLift 0) 0
Tactic: rw [← Affine.Point.zero_def, fromAffine_zero, toAffineLift_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
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
⊢ Eq.{u + 1} (α := W.toAffine.Point) (toAffineLift (fromAffine Affine.Point.zero)) Affine.Point.zero
have zero₂ : Eq.{u + 1} (α := W.toAffine.Point) 0 0
Tactic: rw [← Affine.Point.zero_def, fromAffine_zero, toAffineLift_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
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»
⊢ (fromAffine (Affine.Point.some «x» «y» h)).toAffineLift = Affine.Point.some «x» «y» h
have some : { point := ⟦![«x», «y», 1]⟧, nonsingular := sorry : W.Point }.toAffineLift = Affine.Point.some «x» «y» h
Tactic: rw [fromAffine_some, toAffineLift_some]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
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
⊢ (fromAffine (Affine.Point.some «x» «y» h)).toAffineLift = Affine.Point.some «x» «y» h
have some₁ : Affine.Point.some «x» «y» sorry = Affine.Point.some «x» «y» h
Tactic: rw [fromAffine_some, toAffineLift_some]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
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
⊢ «x» + x_1 + x_2 = «x» + (x_1 + x_2)
have 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)
Tactic: apply (toAffineAddEquiv W).injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
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
⊢ «x» + x_1 + x_2 = «x» + (x_1 + x_2)
have 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)
Tactic: classical
    apply (toAffineAddEquiv W).injective
    simp only [map_add, add_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
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
⊢ 0 + «x» = «x»
have 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)
Tactic: apply (toAffineAddEquiv W).injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
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
⊢ 0 + «x» = «x»
have 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)
Tactic: classical
    apply (toAffineAddEquiv W).injective
    simp only [map_add, toAffineAddEquiv_apply, toAffineLift_zero, zero_add]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
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
⊢ «x» + 0 = «x»
have 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)
Tactic: apply (toAffineAddEquiv W).injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
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
⊢ «x» + 0 = «x»
have 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)
Tactic: classical
    apply (toAffineAddEquiv W).injective
    simp only [map_add, toAffineAddEquiv_apply, toAffineLift_zero, add_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
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
⊢ -P + P = 0
have 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)
Tactic: apply (toAffineAddEquiv W).injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
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
⊢ -P + P = 0
have 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)
Tactic: classical
    apply (toAffineAddEquiv W).injective
    simp only [map_add, toAffineAddEquiv_apply, toAffineLift_neg, neg_add_cancel, toAffineLift_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
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
⊢ «x» + x_1 = x_1 + «x»
have 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)
Tactic: apply (toAffineAddEquiv W).injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
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
⊢ «x» + x_1 = x_1 + «x»
have 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)
Tactic: classical
    apply (toAffineAddEquiv W).injective
    simp only [map_add, add_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Jacobian R
f : R →+* S
P : Fin 3 → R
⊢ (W'.map f).neg ((⇑f : (a : R) → S) ∘ P) = (⇑f : (a : R) → S) ∘ W'.neg P
have 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)
Tactic: simp only [neg, map_negY, comp_fin3]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
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
⊢ (W.map f).add ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ W.add P Q
have 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
Tactic: by_cases h : P ≈ Q
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
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
⊢ (W.map f).add ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ W.add P Q
have 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
Tactic: by_cases h : P ≈ Q
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
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
⊢ (W.map f).add ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ W.add P Q
have pos : (W.map f).dblXYZ ((⇑f : (a : F) → K) ∘ P) = (⇑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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
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
⊢ (W.map f).add ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ W.add P Q
have pos₁ : (W.map f).dblXYZ ((⇑f : (a : F) → K) ∘ P) = (⇑f : (a : F) → K) ∘ W.dblXYZ P
Tactic: rw [add_of_equiv <| (comp_equiv_comp f hP hQ).mpr h, add_of_equiv h, map_dblXYZ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
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
⊢ (W.map f).add ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ W.add P Q
have pos₂ : Eq.{v + 1} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ W.dblXYZ P) ((⇑f : (a : F) → K) ∘ W.dblXYZ P)
Tactic: rw [add_of_equiv <| (comp_equiv_comp f hP hQ).mpr h, add_of_equiv h, map_dblXYZ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
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
⊢ (W.map f).add ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ W.add P Q
have neg : (W.map f).addXYZ ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ W.add P Q
Tactic: rw [add_of_not_equiv <| h.comp (comp_equiv_comp f hP hQ).mp, add_of_not_equiv h, map_addXYZ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
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
neg : (W.map f).addXYZ ((⇑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
have neg₁ : (W.map f).addXYZ ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ W.addXYZ P Q
Tactic: rw [add_of_not_equiv <| h.comp (comp_equiv_comp f hP hQ).mp, add_of_not_equiv h, map_addXYZ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
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
neg : (W.map f).addXYZ ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ W.add P Q
neg₁ : (W.map f).addXYZ ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ W.addXYZ P Q
⊢ (W.map f).add ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ W.add P Q
have neg₂ : Eq.{v + 1} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ W.addXYZ P Q) ((⇑f : (a : F) → K) ∘ W.addXYZ P Q)
Tactic: rw [add_of_not_equiv <| h.comp (comp_equiv_comp f hP hQ).mp, add_of_not_equiv h, map_addXYZ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (W'⁄B).neg ((⇑f : (a : A) → B) ∘ P) = (⇑f : (a : A) → B) ∘ (W'⁄A).neg P
have rw : (W'⁄B).neg ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = (⇑(↑f : A →+* B) : (a : A) → B) ∘ (W'⁄A).neg P
Tactic: rw [← RingHom.coe_coe, ← WeierstrassCurve.Jacobian.map_neg, map_baseChange]