awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : IsDomain R
p q : R[X]
none : max (HSMul.hSMul (α := ℕ) (β := WithBot ℕ) 2 Option.none) (HSMul.hSMul (α := ℕ) (β := WithBot ℕ) 2 ⊥ + 3) ≠ 1
⊢ max (HSMul.hSMul (α := ℕ) (β := WithBot ℕ) 2 Option.none) (HSMul.hSMul (α := ℕ) 2 q.degree + 3) ≠ 1
have none₁ : ∀ (a : ℕ), max (HSMul.hSMul (α := ℕ) (β := WithBot ℕ) 2 Option.none) (HSMul.hSMul (α := ℕ) 2 (↑a : WithBot ℕ) + 3) ≠ 1
Tactic: cases q.degree
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : IsDomain R
p q : R[X]
⊢ max (HSMul.hSMul (α := ℕ) (β := WithBot ℕ) 2 (some 0)) (HSMul.hSMul (α := ℕ) 2 q.degree + 3) ≠ 1
have some : max (HSMul.hSMul (α := ℕ) (β := WithBot ℕ) 2 (some 0)) (HSMul.hSMul (α := ℕ) (β := WithBot ℕ) 2 ⊥ + 3) ≠ 1
Tactic: cases q.degree
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : IsDomain R
p q : R[X]
some : max (HSMul.hSMul (α := ℕ) (β := WithBot ℕ) 2 (Option.some 0)) (HSMul.hSMul (α := ℕ) (β := WithBot ℕ) 2 ⊥ + 3) ≠ 1
⊢ max (HSMul.hSMul (α := ℕ) (β := WithBot ℕ) 2 (Option.some 0)) (HSMul.hSMul (α := ℕ) 2 q.degree + 3) ≠ 1
have some₁ : ∀ (a : ℕ),
  max (HSMul.hSMul (α := ℕ) (β := WithBot ℕ) 2 (Option.some 0)) (HSMul.hSMul (α := ℕ) 2 (↑a : WithBot ℕ) + 3) ≠ 1
Tactic: cases q.degree
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : IsDomain R
p q : R[X]
⊢ max (HSMul.hSMul (α := ℕ) 2 (some (HAdd.hAdd (α := ℕ) 0 1))) (HSMul.hSMul (α := ℕ) 2 q.degree + 3) ≠ 1
have some : max (HSMul.hSMul (α := ℕ) 2 (some (HAdd.hAdd (α := ℕ) 0 1))) (HSMul.hSMul (α := ℕ) (β := WithBot ℕ) 2 ⊥ + 3) ≠ 1
Tactic: cases q.degree
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : IsDomain R
p q : R[X]
some :
  max (HSMul.hSMul (α := ℕ) 2 (Option.some (HAdd.hAdd (α := ℕ) 0 1))) (HSMul.hSMul (α := ℕ) (β := WithBot ℕ) 2 ⊥ + 3) ≠
    1
⊢ max (HSMul.hSMul (α := ℕ) 2 (Option.some (HAdd.hAdd (α := ℕ) 0 1))) (HSMul.hSMul (α := ℕ) 2 q.degree + 3) ≠ 1
have some₁ : ∀ (a : ℕ),
  max (HSMul.hSMul (α := ℕ) 2 (Option.some (HAdd.hAdd (α := ℕ) 0 1))) (HSMul.hSMul (α := ℕ) 2 (↑a : WithBot ℕ) + 3) ≠ 1
Tactic: cases q.degree
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : IsDomain R
p q : R[X]
n : ℕ
⊢ max (HSMul.hSMul (α := ℕ) 2 (some (n + 1 + 1))) (HSMul.hSMul (α := ℕ) 2 q.degree + 3) ≠ 1
have some : max (HSMul.hSMul (α := ℕ) 2 (some (n + 1 + 1))) (HSMul.hSMul (α := ℕ) (β := WithBot ℕ) 2 ⊥ + 3) ≠ 1
Tactic: cases q.degree
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : IsDomain R
p q : R[X]
n : ℕ
some : max (HSMul.hSMul (α := ℕ) 2 (Option.some (n + 1 + 1))) (HSMul.hSMul (α := ℕ) (β := WithBot ℕ) 2 ⊥ + 3) ≠ 1
⊢ max (HSMul.hSMul (α := ℕ) 2 (Option.some (n + 1 + 1))) (HSMul.hSMul (α := ℕ) 2 q.degree + 3) ≠ 1
have some₁ : ∀ (a : ℕ), max (HSMul.hSMul (α := ℕ) 2 (Option.some (n + 1 + 1))) (HSMul.hSMul (α := ℕ) 2 (↑a : WithBot ℕ) + 3) ≠ 1
Tactic: cases q.degree
-- 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 : Nontrivial R
inst_8 : WeierstrassCurve.IsElliptic W'
p : W'.Point → Prop
p0 : p Point.zero
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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₂
⊢ x₁ = x₂ ↔ some x₁ y₁ h₁ = some x₂ y₂ h₂ ∨ some x₁ y₁ h₁ = -some x₂ y₂ h₂
have refine : ∀ (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]⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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₂
⊢ some x₁ y₁ h₁ = some x₂ y₂ h₂ ∨ some x₁ y₁ h₁ = -some x₂ y₂ h₂
have simp_rw : x₁ = x₂ ∧ (y₁ = y₂ ∨ y₁ = W.negY x₂ y₂)
Tactic: simp_rw [neg_some, some.injEq, ← and_or_left]
-- 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₁ y₁ : F
h₁ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h₂ : W.Nonsingular x₂ y₂
⊢ (match (motive := W.Point → Additive (ClassGroup W.CoordinateRing)) some x₁ y₁ h₁ + some x₂ y₂ h₂ with
    | zero => 0
    | some x y h =>
      (ClassGroup.mk W.FunctionField :
          (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
        (CoordinateRing.XYIdeal' h)) =
    HAdd.hAdd (α := Additive (ClassGroup W.CoordinateRing)) (β := Additive (ClassGroup W.CoordinateRing))
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (CoordinateRing.XYIdeal' h₁) :
        ClassGroup W.CoordinateRing)
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (CoordinateRing.XYIdeal' h₂) :
        ClassGroup W.CoordinateRing)
have pos : ∀ (hxy : x₁ = x₂ ∧ y₁ = W.negY x₂ y₂),
  (match (motive := W.Point → Additive (ClassGroup W.CoordinateRing)) some x₁ y₁ h₁ + some x₂ y₂ h₂ with
    | zero => 0
    | some x y h =>
      (ClassGroup.mk W.FunctionField :
          (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
        (CoordinateRing.XYIdeal' h)) =
    HAdd.hAdd (α := Additive (ClassGroup W.CoordinateRing)) (β := Additive (ClassGroup W.CoordinateRing))
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (CoordinateRing.XYIdeal' h₁) :
        ClassGroup W.CoordinateRing)
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (CoordinateRing.XYIdeal' h₂) :
        ClassGroup W.CoordinateRing)
Tactic: by_cases hxy : x₁ = x₂ ∧ y₁ = W.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
x₁ y₁ : F
h₁ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h₂ : W.Nonsingular x₂ y₂
hxy : x₁ = x₂ ∧ y₁ = W.negY x₂ y₂
⊢ (match (motive := W.Point → Additive (ClassGroup W.CoordinateRing)) some x₁ y₁ h₁ + some x₂ y₂ h₂ with
    | zero => 0
    | some x y h =>
      (ClassGroup.mk W.FunctionField :
          (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
        (CoordinateRing.XYIdeal' h)) =
    HAdd.hAdd (α := Additive (ClassGroup W.CoordinateRing)) (β := Additive (ClassGroup W.CoordinateRing))
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (CoordinateRing.XYIdeal' h₁) :
        ClassGroup W.CoordinateRing)
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (CoordinateRing.XYIdeal' h₂) :
        ClassGroup W.CoordinateRing)
have pos : 0 =
  HAdd.hAdd (α := Additive (ClassGroup W.CoordinateRing)) (β := Additive (ClassGroup W.CoordinateRing))
    ((ClassGroup.mk W.FunctionField :
          (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
        (CoordinateRing.XYIdeal' (y := W.negY x₂ y₂) sorry) :
      ClassGroup W.CoordinateRing)
    ((ClassGroup.mk W.FunctionField :
          (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
        (CoordinateRing.XYIdeal' h₂) :
      ClassGroup W.CoordinateRing)
Tactic: simp only [hxy.left, hxy.right, add_of_Y_eq rfl rfl]
-- 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₁ y₁ : F
h₁ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ (match (motive := W.Point → Additive (ClassGroup W.CoordinateRing)) some x₁ y₁ h₁ + some x₂ y₂ h₂ with
    | zero => 0
    | some x y h =>
      (ClassGroup.mk W.FunctionField :
          (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
        (CoordinateRing.XYIdeal' h)) =
    HAdd.hAdd (α := Additive (ClassGroup W.CoordinateRing)) (β := Additive (ClassGroup W.CoordinateRing))
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (CoordinateRing.XYIdeal' h₁) :
        ClassGroup W.CoordinateRing)
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (CoordinateRing.XYIdeal' h₂) :
        ClassGroup W.CoordinateRing)
have neg : (ClassGroup.mk W.FunctionField :
      (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
    (CoordinateRing.XYIdeal' (x := W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) sorry) =
  HAdd.hAdd (α := Additive (ClassGroup W.CoordinateRing)) (β := Additive (ClassGroup W.CoordinateRing))
    ((ClassGroup.mk W.FunctionField :
          (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
        (CoordinateRing.XYIdeal' h₁) :
      ClassGroup W.CoordinateRing)
    ((ClassGroup.mk W.FunctionField :
          (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
        (CoordinateRing.XYIdeal' h₂) :
      ClassGroup W.CoordinateRing)
Tactic: simp only [add_some hxy]
-- 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
P Q : W.Point
⊢ P + Q = 0 ↔ P = -Q
have zero : HAdd.hAdd (α := W.Point) zero zero = 0 ↔ Eq.{u + 1} (α := W.Point) zero (-zero)
Tactic: rcases P, Q with ⟨_ | ⟨x₁, y₁, _⟩, _ | ⟨x₂, y₂, _⟩⟩
Cleared hypotheses: P, Q
-- 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
P Q : W.Point
zero : HAdd.hAdd (α := W.Point) Point.zero Point.zero = 0 ↔ Eq.{u + 1} (α := W.Point) Point.zero (-Point.zero)
⊢ P + Q = 0 ↔ P = -Q
have zero₁ : ∀ (x₂ y₂ : F) (h : W.Nonsingular x₂ y₂), Point.zero + some x₂ y₂ h = 0 ↔ Point.zero = -some x₂ y₂ h
Tactic: rcases P, Q with ⟨_ | ⟨x₁, y₁, _⟩, _ | ⟨x₂, y₂, _⟩⟩
Cleared hypotheses: P, Q
-- 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
P Q : W.Point
zero : HAdd.hAdd (α := W.Point) Point.zero Point.zero = 0 ↔ Eq.{u + 1} (α := W.Point) Point.zero (-Point.zero)
zero₁ : ∀ (x₂ y₂ : F) (h : W.Nonsingular x₂ y₂), Point.zero + some x₂ y₂ h = 0 ↔ Point.zero = -some x₂ y₂ h
⊢ P + Q = 0 ↔ P = -Q
have some : ∀ (x₁ y₁ : F) (h : W.Nonsingular x₁ y₁), some x₁ y₁ h + Point.zero = 0 ↔ some x₁ y₁ h = -Point.zero
Tactic: rcases P, Q with ⟨_ | ⟨x₁, y₁, _⟩, _ | ⟨x₂, y₂, _⟩⟩
Cleared hypotheses: P, Q
-- 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
P Q : W.Point
zero : HAdd.hAdd (α := W.Point) Point.zero Point.zero = 0 ↔ Eq.{u + 1} (α := W.Point) Point.zero (-Point.zero)
zero₁ : ∀ (x₂ y₂ : F) (h : W.Nonsingular x₂ y₂), Point.zero + Point.some x₂ y₂ h = 0 ↔ Point.zero = -Point.some x₂ y₂ h
some : ∀ (x₁ y₁ : F) (h : W.Nonsingular x₁ y₁), Point.some x₁ y₁ h + Point.zero = 0 ↔ Point.some x₁ y₁ h = -Point.zero
⊢ P + Q = 0 ↔ P = -Q
have some₁ : ∀ (x₁ y₁ : F) (h : W.Nonsingular x₁ y₁) (x₂ y₂ : F) (h_1 : W.Nonsingular x₂ y₂),
  Point.some x₁ y₁ h + Point.some x₂ y₂ h_1 = 0 ↔ Point.some x₁ y₁ h = -Point.some x₂ y₂ h_1
Tactic: rcases P, Q with ⟨_ | ⟨x₁, y₁, _⟩, _ | ⟨x₂, y₂, _⟩⟩
Cleared hypotheses: P, Q
-- 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₂
⊢ zero + some x₂ y₂ h = 0 ↔ zero = -some x₂ y₂ h
have zero : 0 + some x₂ y₂ h = 0 ↔ 0 = -some x₂ y₂ h
Tactic: rw [← zero_def, zero_add, eq_comm (a := 0), neg_eq_iff_eq_neg, neg_zero]
-- 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₂
zero : 0 + some x₂ y₂ h = 0 ↔ 0 = -some x₂ y₂ h
⊢ Point.zero + some x₂ y₂ h = 0 ↔ Point.zero = -some x₂ y₂ h
have zero₁ : some x₂ y₂ h = 0 ↔ 0 = -some x₂ y₂ h
Tactic: rw [← zero_def, zero_add, eq_comm (a := 0), neg_eq_iff_eq_neg, neg_zero]
-- 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₂
zero : 0 + some x₂ y₂ h = 0 ↔ 0 = -some x₂ y₂ h
zero₁ : some x₂ y₂ h = 0 ↔ 0 = -some x₂ y₂ h
⊢ Point.zero + some x₂ y₂ h = 0 ↔ Point.zero = -some x₂ y₂ h
have zero₂ : some x₂ y₂ h = 0 ↔ -some x₂ y₂ h = 0
Tactic: rw [← zero_def, zero_add, eq_comm (a := 0), neg_eq_iff_eq_neg, neg_zero]
-- 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₂
zero : 0 + some x₂ y₂ h = 0 ↔ 0 = -some x₂ y₂ h
zero₁ : some x₂ y₂ h = 0 ↔ 0 = -some x₂ y₂ h
zero₂ : some x₂ y₂ h = 0 ↔ -some x₂ y₂ h = 0
⊢ Point.zero + some x₂ y₂ h = 0 ↔ Point.zero = -some x₂ y₂ h
have zero₃ : some x₂ y₂ h = 0 ↔ some x₂ y₂ h = -0
Tactic: rw [← zero_def, zero_add, eq_comm (a := 0), neg_eq_iff_eq_neg, neg_zero]
-- 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₂
zero : 0 + some x₂ y₂ h = 0 ↔ 0 = -some x₂ y₂ h
zero₁ : some x₂ y₂ h = 0 ↔ 0 = -some x₂ y₂ h
zero₂ : some x₂ y₂ h = 0 ↔ -some x₂ y₂ h = 0
zero₃ : some x₂ y₂ h = 0 ↔ some x₂ y₂ h = -0
⊢ Point.zero + some x₂ y₂ h = 0 ↔ Point.zero = -some x₂ y₂ h
have zero₄ : some x₂ y₂ h = 0 ↔ some x₂ y₂ h = 0
Tactic: rw [← zero_def, zero_add, eq_comm (a := 0), neg_eq_iff_eq_neg, neg_zero]
-- 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₁
x₂ y₂ : F
h_1 : W.Nonsingular x₂ y₂
⊢ some x₁ y₁ h + some x₂ y₂ h_1 = 0 ↔ some x₁ y₁ h = -some x₂ y₂ h_1
have some : some x₁ y₁ h + some x₂ y₂ h_1 = 0 ↔ x₁ = x₂ ∧ y₁ = W.negY x₂ y₂
Tactic: rw [neg_some, some.injEq]
-- 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₁
x₂ y₂ : F
h_1 : W.Nonsingular x₂ y₂
⊢ some x₁ y₁ h + some x₂ y₂ h_1 = 0 ↔ x₁ = x₂ ∧ y₁ = W.negY x₂ y₂
have some : some x₁ y₁ h + some x₂ y₂ h_1 = 0 → x₁ = x₂ ∧ y₁ = W.negY x₂ y₂
Tactic: constructor
-- 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₁
x₂ y₂ : F
h_1 : W.Nonsingular x₂ y₂
some : Point.some x₁ y₁ h + Point.some x₂ y₂ h_1 = 0 → x₁ = x₂ ∧ y₁ = W.negY x₂ y₂
⊢ Point.some x₁ y₁ h + Point.some x₂ y₂ h_1 = 0 ↔ x₁ = x₂ ∧ y₁ = W.negY x₂ y₂
have some₁ : x₁ = x₂ ∧ y₁ = W.negY x₂ y₂ → Point.some x₁ y₁ h + Point.some x₂ y₂ h_1 = 0
Tactic: constructor
-- 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₁
x₂ y₂ : F
h_1 : W.Nonsingular x₂ y₂
⊢ some x₁ y₁ h + some x₂ y₂ h_1 = 0 → x₁ = x₂ ∧ y₁ = W.negY x₂ y₂
have some : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂) → ¬some x₁ y₁ h + some x₂ y₂ h_1 = 0
Tactic: contrapose
-- 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
P : W.Point
⊢ Eq (α := Additive (ClassGroup W.CoordinateRing))
      ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) P : Additive (ClassGroup W.CoordinateRing))
      (0 : Additive (ClassGroup W.CoordinateRing)) ↔
    P = 0
have mp : Eq (α := Additive (ClassGroup W.CoordinateRing))
    ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) P : Additive (ClassGroup W.CoordinateRing))
    (0 : Additive (ClassGroup W.CoordinateRing)) →
  P = 0
Tactic: constructor
-- 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
P : W.Point
mp :
  Eq (α := Additive (ClassGroup W.CoordinateRing))
      ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) P : Additive (ClassGroup W.CoordinateRing))
      (0 : Additive (ClassGroup W.CoordinateRing)) →
    P = 0
⊢ Eq (α := Additive (ClassGroup W.CoordinateRing))
      ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) P : Additive (ClassGroup W.CoordinateRing))
      (0 : Additive (ClassGroup W.CoordinateRing)) ↔
    P = 0
have mpr : P = 0 →
  Eq (α := Additive (ClassGroup W.CoordinateRing))
    ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) P : Additive (ClassGroup W.CoordinateRing))
    (0 : Additive (ClassGroup W.CoordinateRing))
Tactic: constructor
-- 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
P : W.Point
hP :
  Eq (α := Additive (ClassGroup W.CoordinateRing))
    ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) P : Additive (ClassGroup W.CoordinateRing))
    (0 : Additive (ClassGroup W.CoordinateRing))
⊢ P = 0
have mp : ∀
  (hP :
    Eq.{u + 1} (α := Additive (ClassGroup W.CoordinateRing))
      ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) zero : Additive (ClassGroup W.CoordinateRing))
      (0 : Additive (ClassGroup W.CoordinateRing))),
  Eq.{u + 1} (α := W.Point) zero 0
Tactic: rcases P with (_ | ⟨_, _, h, _⟩)
Cleared hypotheses: P, 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
P : W.Point
hP :
  Eq (α := Additive (ClassGroup W.CoordinateRing))
    ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) P : Additive (ClassGroup W.CoordinateRing))
    (0 : Additive (ClassGroup W.CoordinateRing))
mp :
  ∀
    (hP :
      Eq.{u + 1} (α := Additive (ClassGroup W.CoordinateRing))
        ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) zero :
          Additive (ClassGroup W.CoordinateRing))
        (0 : Additive (ClassGroup W.CoordinateRing))),
    Eq.{u + 1} (α := W.Point) zero 0
⊢ P = 0
have mp₁ : ∀ (x y : F) (h : W.Equation x y) (right : evalEval x y W.polynomialX ≠ 0 ∨ evalEval x y W.polynomialY ≠ 0)
  (hP :
    Eq (α := Additive (ClassGroup W.CoordinateRing))
      ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) (some x y sorry) :
        Additive (ClassGroup W.CoordinateRing))
      (0 : Additive (ClassGroup W.CoordinateRing))),
  some x y sorry = 0
Tactic: rcases P with (_ | ⟨_, _, h, _⟩)
Cleared hypotheses: P, 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.Equation x y
right : evalEval x y W.polynomialX ≠ 0 ∨ evalEval x y W.polynomialY ≠ 0
hP :
  Eq (α := Additive (ClassGroup W.CoordinateRing))
    ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) (some x y ⋯) :
      Additive (ClassGroup W.CoordinateRing))
    (0 : Additive (ClassGroup W.CoordinateRing))
⊢ some x y ⋯ = 0
have mp : ∀ (p : W.CoordinateRing) (h0 : p ≠ 0)
  (hp : Eq (α := Ideal W.CoordinateRing) (CoordinateRing.XYIdeal W x ((C : (a : F) → F[X]) y)) (span {p})),
  some x y sorry = 0
Tactic: rcases (ClassGroup.mk_eq_one_of_coe_ideal <| by rfl).mp hP with ⟨p, h0, 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.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})
⊢ some x y ⋯ = 0
have apply : natDegree.{u} (R := F) ((Algebra.norm F[X] : (a : W.CoordinateRing) → F[X]) p) = 1
Tactic: apply (p.natDegree_norm_ne_one _).elim
-- 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})
⊢ 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) (span {p})) = 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]