awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x y : F
h : W.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
rw₃ rw₄ : Eq (α := ℕ) 1 1
⊢ natDegree.{u} (R := F) ((Algebra.norm F[X] : (a : W.CoordinateRing) → F[X]) 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]

Premises used: finrank_quotient_span_eq_natDegree_norm, Ideal.quotientEquivAlgOfEq, LinearEquiv.finrank_eq, WeierstrassCurve.Affine.CoordinateRing.basis, AlgEquiv.toLinearEquiv, Module.finrank_self, WeierstrassCurve.Affine.CoordinateRing.quotientXYIdealEquiv
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
P : W.Point
⊢ 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:
congr_arg toClass

Premises used: congr_arg, WeierstrassCurve.Affine.Point.toClass, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
P : W.Point
⊢ 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:
exact congr_arg toClass

Premises used: congr_arg, WeierstrassCurve.Affine.Point.toClass, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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)) Point.zero :
      Additive (ClassGroup W.CoordinateRing))
    ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) a₂ : Additive (ClassGroup W.CoordinateRing))
zero :
  HAdd.hAdd (α := Additive (ClassGroup W.CoordinateRing)) (β := Additive (ClassGroup W.CoordinateRing))
      ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) (-Point.zero) :
        Additive (ClassGroup W.CoordinateRing))
      ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) Point.zero :
        Additive (ClassGroup W.CoordinateRing)) =
    0
⊢ Point.zero = a₂

Tactic:
rw [← neg_inj, ← add_eq_zero, ← toClass_eq_zero, map_add, ← hP]

Premises used: map_add, _private.0.WeierstrassCurve.Affine.Point.add_eq_zero, neg_inj, WeierstrassCurve.Affine.Point.toClass_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x y : F
h : W.Nonsingular x y
a₂ : W.Point
hP :
  Eq (α := Additive (ClassGroup W.CoordinateRing))
    ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) (Point.some x y h) :
      Additive (ClassGroup W.CoordinateRing))
    ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) a₂ : Additive (ClassGroup W.CoordinateRing))
some :
  HAdd.hAdd (α := Additive (ClassGroup W.CoordinateRing)) (β := Additive (ClassGroup W.CoordinateRing))
      ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) (-Point.some x y h) :
        Additive (ClassGroup W.CoordinateRing))
      ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) (Point.some x y h) :
        Additive (ClassGroup W.CoordinateRing)) =
    0
⊢ Point.some x y h = a₂

Tactic:
rw [← neg_inj, ← add_eq_zero, ← toClass_eq_zero, map_add, ← hP]

Premises used: map_add, _private.0.WeierstrassCurve.Affine.Point.add_eq_zero, neg_inj, WeierstrassCurve.Affine.Point.toClass_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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))
⊢ 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:
zero_add 0

Premises used: zero_add, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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))
⊢ 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:
exact zero_add 0

Premises used: zero_add, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x y : F
h : W.Nonsingular x y
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))
⊢ 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:
CoordinateRing.mk_XYIdeal'_neg_mul h

Premises used: Additive, WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_neg_mul, Quotient.map₂, ClassGroup
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x y : F
h : W.Nonsingular x y
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))
⊢ 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:
exact CoordinateRing.mk_XYIdeal'_neg_mul h

Premises used: WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_neg_mul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
inst_6 : Field L
W' : Affine R
W : Affine F
inst_7 : DecidableEq F
inst_8 : DecidableEq K
inst_9 : DecidableEq L
x x_1 x_2 : W.Point
⊢ Eq (α := Additive (ClassGroup W.CoordinateRing))
    ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) (x + x_1 + x_2) :
      Additive (ClassGroup W.CoordinateRing))
    ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) (x + (x_1 + x_2)) :
      Additive (ClassGroup W.CoordinateRing))

Tactic:
simp only [map_add, add_assoc]

Premises used: add_assoc, map_add
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
inst_6 : Field L
W' : Affine R
W : Affine F
inst_7 : DecidableEq F
inst_8 : DecidableEq K
inst_9 : DecidableEq L
x x_1 : W.Point
⊢ Eq (α := Additive (ClassGroup W.CoordinateRing))
    ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) (x + x_1) :
      Additive (ClassGroup W.CoordinateRing))
    ((toClass : (a : W.Point) → Additive (ClassGroup W.CoordinateRing)) (x_1 + x) :
      Additive (ClassGroup W.CoordinateRing))

Tactic:
simp only [map_add, add_comm]

Premises used: map_add, add_comm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
inst_6 : Field L
W' : Affine R
W : Affine F
inst_7 : DecidableEq F
inst_8 : DecidableEq K
inst_9 : DecidableEq L
x : W.Point
rw rw₁ : -x = -x
⊢ -x + x = 0

Tactic:
rw [add_eq_zero]

Premises used: _private.0.WeierstrassCurve.Affine.Point.add_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
inst_6 : Field L
W' : Affine R
W : Affine F
inst_7 : DecidableEq F
inst_8 : DecidableEq K
inst_9 : DecidableEq L
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
⊢ (match (motive := (W'⁄F).Point → (W'⁄K).Point) HAdd.hAdd (α := (W'⁄F).Point) zero zero 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) zero 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) zero with
        | zero => 0
        | some x y h => some ((f : (a : F) → K) x) ((f : (a : F) → K) y) ⋯ :
        (W'⁄K).Point)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
inst_6 : Field L
W' : Affine R
W : Affine F
inst_7 : DecidableEq F
inst_8 : DecidableEq K
inst_9 : DecidableEq L
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₂
⊢ (match (motive := (W'⁄F).Point → (W'⁄K).Point) zero + 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) zero 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)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
inst_6 : Field L
W' : Affine R
W : Affine F
inst_7 : DecidableEq F
inst_8 : DecidableEq K
inst_9 : DecidableEq L
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₁
⊢ (match (motive := (W'⁄F).Point → (W'⁄K).Point) some x₁ y₁ h₁ + zero 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) zero with
        | zero => 0
        | some x y h => some ((f : (a : F) → K) x) ((f : (a : F) → K) y) ⋯ :
        (W'⁄K).Point)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
inst_6 : Field L
W' : Affine R
W : Affine F
inst_7 : DecidableEq F
inst_8 : DecidableEq K
inst_9 : DecidableEq L
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)
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) ⋯) =
      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)

Tactic:
by_cases hxy : x₁ = x₂ ∧ y₁ = (W'⁄F).negY x₂ y₂

Premises used: WeierstrassCurve.Affine.negY, WeierstrassCurve.Affine.baseChange
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
inst_6 : Field L
W' : Affine R
W : Affine F
inst_7 : DecidableEq F
inst_8 : DecidableEq K
inst_9 : DecidableEq L
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₂)
rw₁ 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)
⊢ (f : (a : F) → K) y₁ = (W'⁄K).negY ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₂)

Tactic:
rw [hxy.right, baseChange_negY]

Premises used: WeierstrassCurve.Affine.baseChange_negY, And.right
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
inst_6 : Field L
W' : Affine R
W : Affine F
inst_7 : DecidableEq F
inst_8 : DecidableEq K
inst_9 : DecidableEq L
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)
pos₁ 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) ⋯ :
      (W'⁄K).Point)
    (0 : (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)

Tactic:
rw [add_of_Y_eq hxy.left hxy.right,
        add_of_Y_eq (congr_arg _ hxy.left) <| by rw [hxy.right, baseChange_negY]]

Premises used: congr_arg, WeierstrassCurve.Affine.Point.add_of_Y_eq, And.right, And.left
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
inst_6 : Field L
W' : Affine R
W : Affine F
inst_7 : DecidableEq F
inst_8 : DecidableEq K
inst_9 : DecidableEq L
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)

Tactic:
simpa only [add_some hxy, ← baseChange_addX, ← baseChange_addY, ← baseChange_slope] using
        (add_some fun h ↦ hxy ⟨f.injective h.1, f.injective (W'.baseChange_negY f .. ▸ h).2⟩).symm

Premises used: RingHom.injective, And.left, AlgHom.toRingHom, WeierstrassCurve.Affine.Point.add_some, And.intro, WeierstrassCurve.Affine.baseChange_slope, WeierstrassCurve.Affine.baseChange_addY, WeierstrassCurve.Affine.baseChange_addX, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
S : Type s
F : Type u
K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field F
inst_3 : Field K
W' : Affine R
inst_4 : DecidableEq F
inst_5 : DecidableEq K
inst_6 : Algebra R S
inst_7 : Algebra R F
inst_8 : Algebra S F
inst_9 : IsScalarTower R S F
inst_10 : Algebra R K
inst_11 : Algebra S K
inst_12 : IsScalarTower R S K
f : F →ₐ[S] K
⊢ Eq.{v + 1} (α := (W'⁄K).Point)
    (((map f : AddMonoidHom.{u, v} (W'⁄F).Point (W'⁄K).Point) : (a : (W'⁄F).Point) → (W'⁄K).Point) 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
S : Type s
F : Type u
K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field F
inst_3 : Field K
W' : Affine R
inst_4 : DecidableEq F
inst_5 : DecidableEq K
inst_6 : Algebra R S
inst_7 : Algebra R F
inst_8 : Algebra S F
inst_9 : IsScalarTower R S F
inst_10 : Algebra R K
inst_11 : Algebra S K
inst_12 : IsScalarTower R S K
f : F →ₐ[S] K
x y : F
h : (W'⁄F).Nonsingular x y
⊢ Eq.{v + 1} (α := (W'⁄K).Point)
    (((map f : AddMonoidHom.{u, v} (W'⁄F).Point (W'⁄K).Point) : (a : (W'⁄F).Point) → (W'⁄K).Point) (some x y h) :
      (W'⁄K).Point)
    (some ((f : (a : F) → K) x) ((f : (a : F) → K) y) ⋯ : (W'⁄K).Point)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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)
some :
  ∀ (x y : F) (h : (W'⁄F).Nonsingular x y),
    (map (Algebra.ofId F F) : (a : (W'⁄F).Point) → (W'⁄F).Point) (Point.some x y h) = Point.some x y h
⊢ (map (Algebra.ofId F F) : (a : (W'⁄F).Point) → (W'⁄F).Point) P = P

Tactic:
cases P