awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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})
rw : finrank F (HasQuotient.Quotient W.CoordinateRing (B := Ideal W.CoordinateRing) (span {p})) = 1
⊢ natDegree.{u} (R := F) ((Algebra.norm F[X] : (a : W.CoordinateRing) → F[X]) p) = 1
have rw₁ : finrank F
    (HasQuotient.Quotient W.CoordinateRing (B := Ideal W.CoordinateRing)
      (CoordinateRing.XYIdeal W x ((C : (a : F) → F[X]) y))) =
  1
Tactic: rw [← finrank_quotient_span_eq_natDegree_norm (CoordinateRing.basis W) h0,
        ← (quotientEquivAlgOfEq F hp).toLinearEquiv.finrank_eq,
        (CoordinateRing.quotientXYIdealEquiv h).toLinearEquiv.finrank_eq, Module.finrank_self]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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})
rw : finrank F (HasQuotient.Quotient W.CoordinateRing (B := Ideal W.CoordinateRing) (span {p})) = 1
rw₁ :
  finrank F
      (HasQuotient.Quotient W.CoordinateRing (B := Ideal W.CoordinateRing)
        (CoordinateRing.XYIdeal W x ((C : (a : F) → F[X]) y))) =
    1
⊢ natDegree.{u} (R := F) ((Algebra.norm F[X] : (a : W.CoordinateRing) → F[X]) p) = 1
have rw₂ : finrank F F = 1
Tactic: rw [← finrank_quotient_span_eq_natDegree_norm (CoordinateRing.basis W) h0,
        ← (quotientEquivAlgOfEq F hp).toLinearEquiv.finrank_eq,
        (CoordinateRing.quotientXYIdealEquiv h).toLinearEquiv.finrank_eq, Module.finrank_self]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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})
rw : finrank F (HasQuotient.Quotient W.CoordinateRing (B := Ideal W.CoordinateRing) (span {p})) = 1
rw₁ :
  finrank F
      (HasQuotient.Quotient W.CoordinateRing (B := Ideal W.CoordinateRing)
        (CoordinateRing.XYIdeal W x ((C : (a : F) → F[X]) y))) =
    1
rw₂ : finrank F F = 1
⊢ natDegree.{u} (R := F) ((Algebra.norm F[X] : (a : W.CoordinateRing) → F[X]) p) = 1
have rw₃ : Eq (α := ℕ) 1 1
Tactic: rw [← finrank_quotient_span_eq_natDegree_norm (CoordinateRing.basis W) h0,
        ← (quotientEquivAlgOfEq F hp).toLinearEquiv.finrank_eq,
        (CoordinateRing.quotientXYIdealEquiv h).toLinearEquiv.finrank_eq, Module.finrank_self]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
a₂ : W.Point
hP :
  Eq (α := Additive (ClassGroup W.CoordinateRing))
    ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) zero : Additive (ClassGroup W.CoordinateRing))
    ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) a₂ : Additive (ClassGroup W.CoordinateRing))
⊢ zero = a₂
have zero : HAdd.hAdd (α := Additive (ClassGroup W.CoordinateRing)) (β := Additive (ClassGroup W.CoordinateRing))
    ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) (-zero) :
      Additive (ClassGroup W.CoordinateRing))
    ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) zero : Additive (ClassGroup W.CoordinateRing)) =
  0
Tactic: rw [← neg_inj, ← add_eq_zero, ← toClass_eq_zero, map_add, ← hP]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x y : F
h : W.Nonsingular x y
a₂ : W.Point
hP :
  Eq (α := Additive (ClassGroup W.CoordinateRing))
    ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) (some x y h) :
      Additive (ClassGroup W.CoordinateRing))
    ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) a₂ : Additive (ClassGroup W.CoordinateRing))
⊢ some x y h = a₂
have some : HAdd.hAdd (α := Additive (ClassGroup W.CoordinateRing)) (β := Additive (ClassGroup W.CoordinateRing))
    ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) (-some x y h) :
      Additive (ClassGroup W.CoordinateRing))
    ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) (some x y h) :
      Additive (ClassGroup W.CoordinateRing)) =
  0
Tactic: rw [← neg_inj, ← add_eq_zero, ← toClass_eq_zero, map_add, ← hP]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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 : W.Point
⊢ -x + x = 0
have rw : -x = -x
Tactic: rw [add_eq_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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
inst_10 : Algebra R S
inst_11 : Algebra R F
inst_12 : Algebra S F
inst_13 : IsScalarTower R S F
inst_14 : Algebra R K
inst_15 : Algebra S K
inst_16 : IsScalarTower R S K
inst_17 : Algebra R L
inst_18 : Algebra S L
inst_19 : IsScalarTower R S L
f : F →ₐ[S] K
g : K →ₐ[S] L
x₁ y₁ : F
h₁ : (W'⁄F).Nonsingular x₁ y₁
x₂ y₂ : F
h₂ : (W'⁄F).Nonsingular x₂ y₂
⊢ (match (motive := (W'⁄F).Point → (W'⁄K).Point) some x₁ y₁ h₁ + some x₂ y₂ h₂ with
    | zero => 0
    | some x y h => some ((f : (a : F) → K) x) ((f : (a : F) → K) y) ⋯) =
    HAdd.hAdd (α := (W'⁄K).Point) (β := (W'⁄K).Point)
      (match (motive := (W'⁄F).Point → (W'⁄K).Point) some x₁ y₁ h₁ with
        | zero => 0
        | some x y h => some ((f : (a : F) → K) x) ((f : (a : F) → K) y) ⋯ :
        (W'⁄K).Point)
      (match (motive := (W'⁄F).Point → (W'⁄K).Point) some x₂ y₂ h₂ with
        | zero => 0
        | some x y h => some ((f : (a : F) → K) x) ((f : (a : F) → K) y) ⋯ :
        (W'⁄K).Point)
have pos : ∀ (hxy : x₁ = x₂ ∧ y₁ = (W'⁄F).negY x₂ y₂),
  (match (motive := (W'⁄F).Point → (W'⁄K).Point) some x₁ y₁ h₁ + some x₂ y₂ h₂ with
    | zero => 0
    | some x y h => some ((f : (a : F) → K) x) ((f : (a : F) → K) y) sorry) =
    HAdd.hAdd (α := (W'⁄K).Point) (β := (W'⁄K).Point)
      (match (motive := (W'⁄F).Point → (W'⁄K).Point) some x₁ y₁ h₁ with
        | zero => 0
        | some x y h => some ((f : (a : F) → K) x) ((f : (a : F) → K) y) sorry :
        (W'⁄K).Point)
      (match (motive := (W'⁄F).Point → (W'⁄K).Point) some x₂ y₂ h₂ with
        | zero => 0
        | some x y h => some ((f : (a : F) → K) x) ((f : (a : F) → K) y) sorry :
        (W'⁄K).Point)
Tactic: by_cases hxy : x₁ = x₂ ∧ y₁ = (W'⁄F).negY x₂ y₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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
inst_10 : Algebra R S
inst_11 : Algebra R F
inst_12 : Algebra S F
inst_13 : IsScalarTower R S F
inst_14 : Algebra R K
inst_15 : Algebra S K
inst_16 : IsScalarTower R S K
inst_17 : Algebra R L
inst_18 : Algebra S L
inst_19 : IsScalarTower R S L
f : F →ₐ[S] K
g : K →ₐ[S] L
x₁ y₁ : F
h₁ : (W'⁄F).Nonsingular x₁ y₁
x₂ y₂ : F
h₂ : (W'⁄F).Nonsingular x₂ y₂
pos :
  ∀ (hxy : x₁ = x₂ ∧ y₁ = (W'⁄F).negY x₂ y₂),
    (match (motive := (W'⁄F).Point → (W'⁄K).Point) some x₁ y₁ h₁ + some x₂ y₂ h₂ with
      | zero => 0
      | some x y h => some ((f : (a : F) → K) x) ((f : (a : F) → K) y) ⋯) =
      HAdd.hAdd (α := (W'⁄K).Point) (β := (W'⁄K).Point)
        (match (motive := (W'⁄F).Point → (W'⁄K).Point) some x₁ y₁ h₁ with
          | zero => 0
          | some x y h => some ((f : (a : F) → K) x) ((f : (a : F) → K) y) ⋯ :
          (W'⁄K).Point)
        (match (motive := (W'⁄F).Point → (W'⁄K).Point) some x₂ y₂ h₂ with
          | zero => 0
          | some x y h => some ((f : (a : F) → K) x) ((f : (a : F) → K) y) ⋯ :
          (W'⁄K).Point)
⊢ (match (motive := (W'⁄F).Point → (W'⁄K).Point) some x₁ y₁ h₁ + some x₂ y₂ h₂ with
    | zero => 0
    | some x y h => some ((f : (a : F) → K) x) ((f : (a : F) → K) y) ⋯) =
    HAdd.hAdd (α := (W'⁄K).Point) (β := (W'⁄K).Point)
      (match (motive := (W'⁄F).Point → (W'⁄K).Point) some x₁ y₁ h₁ with
        | zero => 0
        | some x y h => some ((f : (a : F) → K) x) ((f : (a : F) → K) y) ⋯ :
        (W'⁄K).Point)
      (match (motive := (W'⁄F).Point → (W'⁄K).Point) some x₂ y₂ h₂ with
        | zero => 0
        | some x y h => some ((f : (a : F) → K) x) ((f : (a : F) → K) y) ⋯ :
        (W'⁄K).Point)
have neg : ∀ (hxy : ¬(x₁ = x₂ ∧ y₁ = (W'⁄F).negY x₂ y₂)),
  (match (motive := (W'⁄F).Point → (W'⁄K).Point) some x₁ y₁ h₁ + some x₂ y₂ h₂ with
    | zero => 0
    | some x y h => some ((f : (a : F) → K) x) ((f : (a : F) → K) y) sorry) =
    HAdd.hAdd (α := (W'⁄K).Point) (β := (W'⁄K).Point)
      (match (motive := (W'⁄F).Point → (W'⁄K).Point) some x₁ y₁ h₁ with
        | zero => 0
        | some x y h => some ((f : (a : F) → K) x) ((f : (a : F) → K) y) sorry :
        (W'⁄K).Point)
      (match (motive := (W'⁄F).Point → (W'⁄K).Point) some x₂ y₂ h₂ with
        | zero => 0
        | some x y h => some ((f : (a : F) → K) x) ((f : (a : F) → K) y) sorry :
        (W'⁄K).Point)
Tactic: by_cases hxy : x₁ = x₂ ∧ y₁ = (W'⁄F).negY x₂ y₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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
inst_10 : Algebra R S
inst_11 : Algebra R F
inst_12 : Algebra S F
inst_13 : IsScalarTower R S F
inst_14 : Algebra R K
inst_15 : Algebra S K
inst_16 : IsScalarTower R S K
inst_17 : Algebra R L
inst_18 : Algebra S L
inst_19 : IsScalarTower R S L
f : F →ₐ[S] K
g : K →ₐ[S] L
x₁ y₁ : F
h₁ : (W'⁄F).Nonsingular x₁ y₁
x₂ y₂ : F
h₂ : (W'⁄F).Nonsingular x₂ y₂
hxy : x₁ = x₂ ∧ y₁ = (W'⁄F).negY x₂ y₂
⊢ (f : (a : F) → K) y₁ = (W'⁄K).negY ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₂)
have rw : (f : (a : F) → K) ((W'⁄F).negY x₂ y₂) = (W'⁄K).negY ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₂)
Tactic: rw [hxy.right, baseChange_negY]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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
inst_10 : Algebra R S
inst_11 : Algebra R F
inst_12 : Algebra S F
inst_13 : IsScalarTower R S F
inst_14 : Algebra R K
inst_15 : Algebra S K
inst_16 : IsScalarTower R S K
inst_17 : Algebra R L
inst_18 : Algebra S L
inst_19 : IsScalarTower R S L
f : F →ₐ[S] K
g : K →ₐ[S] L
x₁ y₁ : F
h₁ : (W'⁄F).Nonsingular x₁ y₁
x₂ y₂ : F
h₂ : (W'⁄F).Nonsingular x₂ y₂
hxy : x₁ = x₂ ∧ y₁ = (W'⁄F).negY x₂ y₂
rw : (f : (a : F) → K) ((W'⁄F).negY x₂ y₂) = (W'⁄K).negY ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₂)
⊢ (f : (a : F) → K) y₁ = (W'⁄K).negY ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₂)
have rw₁ : Eq.{v + 1} (α := K) ((f : (a : F) → K) ((W'⁄F).negY x₂ y₂) : K) ((f : (a : F) → K) ((W'⁄F).negY x₂ y₂) : K)
Tactic: rw [hxy.right, baseChange_negY]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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
inst_10 : Algebra R S
inst_11 : Algebra R F
inst_12 : Algebra S F
inst_13 : IsScalarTower R S F
inst_14 : Algebra R K
inst_15 : Algebra S K
inst_16 : IsScalarTower R S K
inst_17 : Algebra R L
inst_18 : Algebra S L
inst_19 : IsScalarTower R S L
f : F →ₐ[S] K
g : K →ₐ[S] L
x₁ y₁ : F
h₁ : (W'⁄F).Nonsingular x₁ y₁
x₂ y₂ : F
h₂ : (W'⁄F).Nonsingular x₂ y₂
hxy : x₁ = x₂ ∧ y₁ = (W'⁄F).negY x₂ y₂
⊢ (match (motive := (W'⁄F).Point → (W'⁄K).Point) some x₁ y₁ h₁ + some x₂ y₂ h₂ with
    | zero => 0
    | some x y h => some ((f : (a : F) → K) x) ((f : (a : F) → K) y) ⋯) =
    HAdd.hAdd (α := (W'⁄K).Point) (β := (W'⁄K).Point)
      (match (motive := (W'⁄F).Point → (W'⁄K).Point) some x₁ y₁ h₁ with
        | zero => 0
        | some x y h => some ((f : (a : F) → K) x) ((f : (a : F) → K) y) ⋯ :
        (W'⁄K).Point)
      (match (motive := (W'⁄F).Point → (W'⁄K).Point) some x₂ y₂ h₂ with
        | zero => 0
        | some x y h => some ((f : (a : F) → K) x) ((f : (a : F) → K) y) ⋯ :
        (W'⁄K).Point)
have pos : (match (motive := (W'⁄F).Point → (W'⁄K).Point) 0 with
  | zero => 0
  | some x y h => some ((f : (a : F) → K) x) ((f : (a : F) → K) y) sorry) =
  HAdd.hAdd (α := (W'⁄K).Point) (β := (W'⁄K).Point)
    (match (motive := (W'⁄F).Point → (W'⁄K).Point) some x₁ y₁ h₁ with
      | zero => 0
      | some x y h => some ((f : (a : F) → K) x) ((f : (a : F) → K) y) sorry :
      (W'⁄K).Point)
    (match (motive := (W'⁄F).Point → (W'⁄K).Point) some x₂ y₂ h₂ with
      | zero => 0
      | some x y h => some ((f : (a : F) → K) x) ((f : (a : F) → K) y) sorry :
      (W'⁄K).Point)
Tactic: rw [add_of_Y_eq hxy.left hxy.right,
        add_of_Y_eq (congr_arg _ hxy.left) <| by rw [hxy.right, baseChange_negY]]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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
inst_10 : Algebra R S
inst_11 : Algebra R F
inst_12 : Algebra S F
inst_13 : IsScalarTower R S F
inst_14 : Algebra R K
inst_15 : Algebra S K
inst_16 : IsScalarTower R S K
inst_17 : Algebra R L
inst_18 : Algebra S L
inst_19 : IsScalarTower R S L
f : F →ₐ[S] K
g : K →ₐ[S] L
x₁ y₁ : F
h₁ : (W'⁄F).Nonsingular x₁ y₁
x₂ y₂ : F
h₂ : (W'⁄F).Nonsingular x₂ y₂
hxy : x₁ = x₂ ∧ y₁ = (W'⁄F).negY x₂ y₂
pos :
  (match (motive := (W'⁄F).Point → (W'⁄K).Point) 0 with
    | zero => 0
    | some x y h => some ((f : (a : F) → K) x) ((f : (a : F) → K) y) ⋯) =
    HAdd.hAdd (α := (W'⁄K).Point) (β := (W'⁄K).Point)
      (match (motive := (W'⁄F).Point → (W'⁄K).Point) some x₁ y₁ h₁ with
        | zero => 0
        | some x y h => some ((f : (a : F) → K) x) ((f : (a : F) → K) y) ⋯ :
        (W'⁄K).Point)
      (match (motive := (W'⁄F).Point → (W'⁄K).Point) some x₂ y₂ h₂ with
        | zero => 0
        | some x y h => some ((f : (a : F) → K) x) ((f : (a : F) → K) y) ⋯ :
        (W'⁄K).Point)
⊢ (match (motive := (W'⁄F).Point → (W'⁄K).Point) some x₁ y₁ h₁ + some x₂ y₂ h₂ with
    | zero => 0
    | some x y h => some ((f : (a : F) → K) x) ((f : (a : F) → K) y) ⋯) =
    HAdd.hAdd (α := (W'⁄K).Point) (β := (W'⁄K).Point)
      (match (motive := (W'⁄F).Point → (W'⁄K).Point) some x₁ y₁ h₁ with
        | zero => 0
        | some x y h => some ((f : (a : F) → K) x) ((f : (a : F) → K) y) ⋯ :
        (W'⁄K).Point)
      (match (motive := (W'⁄F).Point → (W'⁄K).Point) some x₂ y₂ h₂ with
        | zero => 0
        | some x y h => some ((f : (a : F) → K) x) ((f : (a : F) → K) y) ⋯ :
        (W'⁄K).Point)
have pos₁ : Eq.{v + 1} (α := (W'⁄K).Point)
  (match (motive := (W'⁄F).Point → (W'⁄K).Point) 0 with
    | zero => 0
    | some x y h => some ((f : (a : F) → K) x) ((f : (a : F) → K) y) sorry :
    (W'⁄K).Point)
  (0 : (W'⁄K).Point)
Tactic: rw [add_of_Y_eq hxy.left hxy.right,
        add_of_Y_eq (congr_arg _ hxy.left) <| by rw [hxy.right, baseChange_negY]]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
F : Type u
inst : CommRing R
inst_1 : Field F
W' : Affine R
inst_2 : DecidableEq F
inst_3 : Algebra R F
P : (W'⁄F).Point
⊢ (map (Algebra.ofId F F) : (a : (W'⁄F).Point) → (W'⁄F).Point) P = P
have zero : Eq (α := (W'⁄F).Point) ((map (Algebra.ofId F F) : (a : (W'⁄F).Point) → (W'⁄F).Point) zero : (W'⁄F).Point)
  (zero : (W'⁄F).Point)
Tactic: cases P
Cleared hypotheses: P
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
F : Type u
inst : CommRing R
inst_1 : Field F
W' : Affine R
inst_2 : DecidableEq F
inst_3 : Algebra R F
P : (W'⁄F).Point
zero :
  Eq (α := (W'⁄F).Point) ((map (Algebra.ofId F F) : (a : (W'⁄F).Point) → (W'⁄F).Point) Point.zero : (W'⁄F).Point)
    (Point.zero : (W'⁄F).Point)
⊢ (map (Algebra.ofId F F) : (a : (W'⁄F).Point) → (W'⁄F).Point) P = P
have some : ∀ (x y : F) (h : (W'⁄F).Nonsingular x y),
  (map (Algebra.ofId F F) : (a : (W'⁄F).Point) → (W'⁄F).Point) (some x y h) = some x y h
Tactic: cases P
Cleared hypotheses: P
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
S : Type s
F : Type u
K : Type v
L : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field F
inst_3 : Field K
inst_4 : Field L
W' : Affine R
inst_5 : DecidableEq F
inst_6 : DecidableEq K
inst_7 : DecidableEq L
inst_8 : Algebra R S
inst_9 : Algebra R F
inst_10 : Algebra S F
inst_11 : IsScalarTower R S F
inst_12 : Algebra R K
inst_13 : Algebra S K
inst_14 : IsScalarTower R S K
inst_15 : Algebra R L
inst_16 : Algebra S L
inst_17 : IsScalarTower R S L
f : F →ₐ[S] K
g : K →ₐ[S] L
P : (W'⁄F).Point
⊢ Eq.{w + 1} (α := (W'⁄L).Point)
    (((map g : AddMonoidHom.{v, w} (W'⁄K).Point (W'⁄L).Point) : (a : (W'⁄K).Point) → (W'⁄L).Point)
        (((map f : AddMonoidHom.{u, v} (W'⁄F).Point (W'⁄K).Point) : (a : (W'⁄F).Point) → (W'⁄K).Point) P) :
      (W'⁄L).Point)
    (((map (g.comp f) : AddMonoidHom.{u, w} (W'⁄F).Point (W'⁄L).Point) : (a : (W'⁄F).Point) → (W'⁄L).Point) P :
      (W'⁄L).Point)
have zero : Eq.{w + 1} (α := (W'⁄L).Point)
  (((map g : AddMonoidHom.{v, w} (W'⁄K).Point (W'⁄L).Point) : (a : (W'⁄K).Point) → (W'⁄L).Point)
      (((map f : AddMonoidHom.{u, v} (W'⁄F).Point (W'⁄K).Point) : (a : (W'⁄F).Point) → (W'⁄K).Point) zero) :
    (W'⁄L).Point)
  (((map (g.comp f) : AddMonoidHom.{u, w} (W'⁄F).Point (W'⁄L).Point) : (a : (W'⁄F).Point) → (W'⁄L).Point) zero :
    (W'⁄L).Point)
Tactic: cases P
Cleared hypotheses: P
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
S : Type s
F : Type u
K : Type v
L : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field F
inst_3 : Field K
inst_4 : Field L
W' : Affine R
inst_5 : DecidableEq F
inst_6 : DecidableEq K
inst_7 : DecidableEq L
inst_8 : Algebra R S
inst_9 : Algebra R F
inst_10 : Algebra S F
inst_11 : IsScalarTower R S F
inst_12 : Algebra R K
inst_13 : Algebra S K
inst_14 : IsScalarTower R S K
inst_15 : Algebra R L
inst_16 : Algebra S L
inst_17 : IsScalarTower R S L
f : F →ₐ[S] K
g : K →ₐ[S] L
P : (W'⁄F).Point
zero :
  Eq.{w + 1} (α := (W'⁄L).Point)
    (((map g : AddMonoidHom.{v, w} (W'⁄K).Point (W'⁄L).Point) : (a : (W'⁄K).Point) → (W'⁄L).Point)
        (((map f : AddMonoidHom.{u, v} (W'⁄F).Point (W'⁄K).Point) : (a : (W'⁄F).Point) → (W'⁄K).Point) Point.zero) :
      (W'⁄L).Point)
    (((map (g.comp f) : AddMonoidHom.{u, w} (W'⁄F).Point (W'⁄L).Point) : (a : (W'⁄F).Point) → (W'⁄L).Point) Point.zero :
      (W'⁄L).Point)
⊢ Eq.{w + 1} (α := (W'⁄L).Point)
    (((map g : AddMonoidHom.{v, w} (W'⁄K).Point (W'⁄L).Point) : (a : (W'⁄K).Point) → (W'⁄L).Point)
        (((map f : AddMonoidHom.{u, v} (W'⁄F).Point (W'⁄K).Point) : (a : (W'⁄F).Point) → (W'⁄K).Point) P) :
      (W'⁄L).Point)
    (((map (g.comp f) : AddMonoidHom.{u, w} (W'⁄F).Point (W'⁄L).Point) : (a : (W'⁄F).Point) → (W'⁄L).Point) P :
      (W'⁄L).Point)
have some : ∀ (x y : F) (h : (W'⁄F).Nonsingular x y),
  Eq.{w + 1} (α := (W'⁄L).Point)
    (((map g : AddMonoidHom.{v, w} (W'⁄K).Point (W'⁄L).Point) : (a : (W'⁄K).Point) → (W'⁄L).Point)
        (((map f : AddMonoidHom.{u, v} (W'⁄F).Point (W'⁄K).Point) : (a : (W'⁄F).Point) → (W'⁄K).Point) (some x y h)) :
      (W'⁄L).Point)
    (((map (g.comp f) : AddMonoidHom.{u, w} (W'⁄F).Point (W'⁄L).Point) : (a : (W'⁄F).Point) → (W'⁄L).Point)
        (some x y h) :
      (W'⁄L).Point)
Tactic: cases P
Cleared hypotheses: P
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (hypothesis)
Goal:
R : Type r
F : Type u
K : Type v
L : Type w
inst : CommRing R
inst_1 : Field F
inst_2 : Field K
inst_3 : Field L
W' : Affine R
inst_4 : DecidableEq F
inst_5 : DecidableEq K
inst_6 : DecidableEq L
inst_7 : Algebra R F
inst_8 : Algebra R K
inst_9 : Algebra R L
inst_10 : Algebra F K
inst_11 : IsScalarTower R F K
inst_12 : Algebra F L
inst_13 : IsScalarTower R F L
f : K →ₐ[F] L
P : (W'⁄F).Point
⊢ Eq.{w + 1} (α := (W'⁄L).Point)
    (((map f : AddMonoidHom.{v, w} (W'⁄K).Point (W'⁄L).Point) : (a : (W'⁄K).Point) → (W'⁄L).Point)
        (((baseChange F K : AddMonoidHom.{u, v} (W'⁄F).Point (W'⁄K).Point) : (a : (W'⁄F).Point) → (W'⁄K).Point) P) :
      (W'⁄L).Point)
    (((baseChange F L : AddMonoidHom.{u, w} (W'⁄F).Point (W'⁄L).Point) : (a : (W'⁄F).Point) → (W'⁄L).Point) P :
      (W'⁄L).Point)
have this : Subsingleton (F →ₐ[F] L)
Tactic: have : Subsingleton (F →ₐ[F] L) := inferInstance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : Nontrivial R
P : W'.Point
⊢ P.xRep ≠ 0
have zero : Ne.{r + 1} (α := Fin 2 → R) (xRep (W' := W') zero) 0
Tactic: cases P
Cleared hypotheses: P
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : Nontrivial R
P : W'.Point
zero : Ne.{r + 1} (α := Fin 2 → R) (xRep (W' := W') Point.zero) 0
⊢ P.xRep ≠ 0
have some : ∀ (x y : R) (h : W'.Nonsingular x y), (some x y h).xRep ≠ 0
Tactic: cases P
Cleared hypotheses: P
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
P : W'.Point
⊢ (-P).xRep = P.xRep
have zero : Eq.{r + 1} (α := Fin 2 → R) (xRep (W' := W') (-zero)) (xRep (W' := W') zero)
Tactic: cases P
Cleared hypotheses: P
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
P : W'.Point
zero : Eq.{r + 1} (α := Fin 2 → R) (xRep (W' := W') (-Point.zero)) (xRep (W' := W') Point.zero)
⊢ (-P).xRep = P.xRep
have some : ∀ (x y : R) (h : W'.Nonsingular x y), (-some x y h).xRep = (some x y h).xRep
Tactic: cases P
Cleared hypotheses: P