awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 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:
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
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:
rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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)
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)
            (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)
          (Point.some x y h) :
        (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)

Tactic:
cases P
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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
⊢ 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:
rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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
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:
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_1 : (W'⁄F).Nonsingular x y
h :
  Eq.{v + 1} (α := (W'⁄K).Point)
    (((map f : AddMonoidHom.{u, v} (W'⁄F).Point (W'⁄K).Point) : (a : (W'⁄F).Point) → (W'⁄K).Point) zero : (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_1) :
      (W'⁄K).Point)
⊢ zero = some x y h_1

Tactic:
contradiction
-- 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_1 : (W'⁄F).Nonsingular x y
h :
  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_1) :
      (W'⁄K).Point)
    (((map f : AddMonoidHom.{u, v} (W'⁄F).Point (W'⁄K).Point) : (a : (W'⁄F).Point) → (W'⁄K).Point) zero : (W'⁄K).Point)
⊢ some x y h_1 = zero

Tactic:
contradiction
-- 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
h :
  Eq.{v + 1} (α := (W'⁄K).Point)
    (((map f : AddMonoidHom.{u, v} (W'⁄F).Point (W'⁄K).Point) : (a : (W'⁄F).Point) → (W'⁄K).Point) zero : (W'⁄K).Point)
    (((map f : AddMonoidHom.{u, v} (W'⁄F).Point (W'⁄K).Point) : (a : (W'⁄F).Point) → (W'⁄K).Point) zero : (W'⁄K).Point)
⊢ Eq.{u + 1} (α := (W'⁄F).Point) zero zero

Tactic:
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_1 : (W'⁄F).Nonsingular x y
x_1 y_1 : F
h_2 : (W'⁄F).Nonsingular x_1 y_1
h :
  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_1) :
      (W'⁄K).Point)
    (((map f : AddMonoidHom.{u, v} (W'⁄F).Point (W'⁄K).Point) : (a : (W'⁄F).Point) → (W'⁄K).Point) (some x_1 y_1 h_2) :
      (W'⁄K).Point)
⊢ some x y h_1 = some x_1 y_1 h_2

Tactic:
simpa only [some.injEq] using ⟨f.injective (some.inj h).left, f.injective (some.inj h).right⟩

Premises used: WeierstrassCurve.Affine.Point.some.injEq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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
⊢ Subsingleton (F →ₐ[F] L)

Tactic:
have : Subsingleton (F →ₐ[F] L) := inferInstance
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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
this : Subsingleton (F →ₐ[F] L)
⊢ Eq.{w + 1} (α := (W'⁄L).Point)
    (((map f : AddMonoidHom.{v, w} (W'⁄K).Point (W'⁄L).Point) : (a : (W'⁄K).Point) → (W'⁄L).Point)
        (((map (Algebra.ofId F K) : AddMonoidHom.{u, v} (W'⁄F).Point (W'⁄K).Point) : (a : (W'⁄F).Point) → (W'⁄K).Point)
          P) :
      (W'⁄L).Point)
    (((map (f.comp (Algebra.ofId F K)) : AddMonoidHom.{u, w} (W'⁄F).Point (W'⁄L).Point) :
          (a : (W'⁄F).Point) → (W'⁄L).Point)
        P :
      (W'⁄L).Point)

Tactic:
map_map (Algebra.ofId F K) f P

Premises used: Algebra.ofId, WeierstrassCurve.Affine.Point.map_map
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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
this : Subsingleton (F →ₐ[F] L)
⊢ 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)

Tactic:
convert! map_map (Algebra.ofId F K) f P

Premises used: Algebra.ofId, WeierstrassCurve.Affine.Point.map_map
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
⊢ Eq.{r + 1} (α := Fin 2 → R) (xRep (W' := W') 0) ![1, 0]

Tactic:
rfl

Premises used: WeierstrassCurve.Affine.Point.xRep, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y : R
h : W'.Nonsingular x y
⊢ (some x y h).xRep = ![x, 1]

Tactic:
rfl

Premises used: WeierstrassCurve.Affine.Point.xRep, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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
some : ∀ (x y : R) (h : W'.Nonsingular x y), (Point.some x y h).xRep ≠ 0
⊢ P.xRep ≠ 0

Tactic:
cases P
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : Nontrivial R
⊢ Ne.{r + 1} (α := Fin 2 → R) (xRep (W' := W') zero) 0

Tactic:
simp [xRep]

Premises used: WeierstrassCurve.Affine.Point.xRep
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : Nontrivial R
x y : R
h : W'.Nonsingular x y
⊢ (some x y h).xRep ≠ 0

Tactic:
simp [xRep]

Premises used: WeierstrassCurve.Affine.Point.xRep
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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)
some : ∀ (x y : R) (h : W'.Nonsingular x y), (-Point.some x y h).xRep = (Point.some x y h).xRep
⊢ (-P).xRep = P.xRep

Tactic:
cases P
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
⊢ Eq.{r + 1} (α := Fin 2 → R) (xRep (W' := W') (-zero)) (xRep (W' := W') zero)

Tactic:
simp [← zero_def]

Premises used: WeierstrassCurve.Affine.Point.zero_def
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y : R
h : W'.Nonsingular x y
⊢ (-some x y h).xRep = (some x y h).xRep

Tactic:
simp [← zero_def]

Premises used: WeierstrassCurve.Affine.Point.zero_def
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
P Q : W.Point
h : Eq.{u + 1} (α := Fin 2 → F) (xRep (W' := W) 0) (xRep (W' := W) 0)
⊢ Eq.{u + 1} (α := W.Point) 0 0 ∨ Eq.{u + 1} (α := W.Point) 0 (-0)

Tactic:
.inl rfl

Premises used: Or.inl, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
P Q : W.Point
h : Eq.{u + 1} (α := Fin 2 → F) (xRep (W' := W) 0) (xRep (W' := W) 0)
⊢ Eq.{u + 1} (α := W.Point) 0 0 ∨ Eq.{u + 1} (α := W.Point) 0 (-0)

Tactic:
exact .inl rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
P Q : W.Point
x y : F
h_1 : W.Nonsingular x y
h : xRep (W' := W) 0 = (some x y h_1).xRep
⊢ 0 = some x y h_1 ∨ 0 = -some x y h_1

Tactic:
simp [xRep] at h

Premises used: WeierstrassCurve.Affine.Point.xRep
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
P Q : W.Point
x y : F
h_1 : W.Nonsingular x y
h : (some x y h_1).xRep = xRep (W' := W) 0
⊢ some x y h_1 = 0 ∨ some x y h_1 = -0

Tactic:
simp [xRep] at h

Premises used: WeierstrassCurve.Affine.Point.xRep
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
P Q : W.Point
x₁ y : F
h_1 : W.Nonsingular x₁ y
x₂ y_1 : F
h_2 : W.Nonsingular x₂ y_1
h : (some x₁ y h_1).xRep = (some x₂ y_1 h_2).xRep
⊢ x₁ = x₂

Tactic:
simp only [xRep, Matrix.vecCons_inj, and_true] at h

Premises used: and_true, Matrix.vecCons_inj, WeierstrassCurve.Affine.Point.xRep
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
P Q : W.Point
x₁ y : F
h_1 : W.Nonsingular x₁ y
x₂ y_1 : F
h_2 : W.Nonsingular x₂ y_1
h : x₁ = x₂
⊢ some x₁ y h_1 = some x₂ y_1 h_2 ∨ some x₁ y h_1 = -some x₂ y_1 h_2

Tactic:
X_eq_iff.mp h

Premises used: Iff.mp, WeierstrassCurve.Affine.Point.X_eq_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
P Q : W.Point
x₁ y : F
h_1 : W.Nonsingular x₁ y
x₂ y_1 : F
h_2 : W.Nonsingular x₂ y_1
h : x₁ = x₂
⊢ some x₁ y h_1 = some x₂ y_1 h_2 ∨ some x₁ y h_1 = -some x₂ y_1 h_2

Tactic:
exact X_eq_iff.mp h

Premises used: Iff.mp, WeierstrassCurve.Affine.Point.X_eq_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
P Q : W.Point
h : P.xRep = Q.xRep
⊢ P = Q ∨ P = -Q

Tactic:
match P, Q with
  | 0, 0 => exact .inl rfl
  | 0, some .. => simp [xRep] at h
  | some .., 0 => simp [xRep] at h
  | some x₁ .., some x₂ .. =>
    simp only [xRep, Matrix.vecCons_inj, and_true] at h
    exact X_eq_iff.mp h
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
P Q : W.Point
⊢ P.xRep = Q.xRep ↔ P = Q ∨ P = -Q

Tactic:
⟨eq_or_eq_neg_of_xRep_eq_xRep, fun H ↦ ?_⟩

Premises used: Iff.intro, WeierstrassCurve.Affine.Point.eq_or_eq_neg_of_xRep_eq_xRep
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
P Q : W.Point
refine : ∀ (H : P = Q ∨ P = -Q), P.xRep = Q.xRep
⊢ P.xRep = Q.xRep ↔ P = Q ∨ P = -Q

Tactic:
refine ⟨eq_or_eq_neg_of_xRep_eq_xRep, fun H ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
P Q : W.Point
H : P = Q ∨ P = -Q
inl : P.xRep = P.xRep
inr : (-Q).xRep = Q.xRep
⊢ P.xRep = Q.xRep

Tactic:
rcases H with rfl | rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
P : W.Point
⊢ P.xRep = P.xRep

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
Q : W.Point
⊢ (-Q).xRep = Q.xRep

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
rw :
  (C : (a : R[X]) → R[X][Y])
      (HAdd.hAdd (β := R[X])
        ((C : (a : R) → R[X]) 4 * HPow.hPow (α := R[X]) (β := ℕ) X 3 +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂) : R[X])
              (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (2 * (2 * W.a₄ + W.a₁ * W.a₃)) : R[X]) X)
        ((C : (a : R) → R[X]) (HPow.hPow (β := ℕ) W.a₃ 2 + 4 * W.a₆) : R[X])) =
    HPow.hPow (β := ℕ)
        (HAdd.hAdd (β := R[X][Y])
          (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) 2) : R[X][Y]) Y)
          ((C : (a : R[X]) → R[X][Y])
              (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W.toAffine.a₁ : R[X]) X)
                ((C : (a : R) → R[X]) W.toAffine.a₃ : R[X])) :
            R[X][Y]))
        2 -
      4 *
        HSub.hSub (β := R[X][Y])
          (HPow.hPow (α := R[X][Y]) (β := ℕ) Y 2 +
            HMul.hMul (α := R[X][Y]) (β := R[X][Y])
              ((C : (a : R[X]) → R[X][Y])
                  (HAdd.hAdd (β := R[X])
                    (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W.toAffine.a₁ : R[X]) X)
                    ((C : (a : R) → R[X]) W.toAffine.a₃ : R[X])) :
                R[X][Y])
              Y)
          ((C : (a : R[X]) → R[X][Y])
              (HAdd.hAdd (β := R[X])
                (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
                    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W.toAffine.a₂ : R[X])
                      (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
                  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W.toAffine.a₄ : R[X]) X)
                ((C : (a : R) → R[X]) W.toAffine.a₆ : R[X])) :
            R[X][Y])
⊢ (C : (a : R[X]) → R[X][Y]) W.Ψ₂Sq =
    HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 2 - HMul.hMul (α := R[X][Y]) 4 W.toAffine.polynomial

Tactic:
rw [Ψ₂Sq, ψ₂, b₂, b₄, b₆, Affine.polynomialY, Affine.polynomial]

Premises used: WeierstrassCurve.Ψ₂Sq, WeierstrassCurve.b₂, WeierstrassCurve.b₄, WeierstrassCurve.Affine.polynomial, WeierstrassCurve.Affine.polynomialY, WeierstrassCurve.ψ₂, WeierstrassCurve.b₆
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ 4 * HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) 3 +
          (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.a₁) : R[X][Y]) 2 +
              HMul.hMul (α := R[X][Y]) (β := R[X][Y]) (4 : R[X][Y])
                ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.a₂) : R[X][Y])) *
            HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) 2 +
        HMul.hMul (β := R[X][Y])
          (2 *
            (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) (2 : R[X][Y])
                ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.a₄) : R[X][Y]) +
              HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.a₁) : R[X][Y])
                ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.a₃) : R[X][Y])))
          ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) +
      (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.a₃) : R[X][Y]) 2 +
        HMul.hMul (α := R[X][Y]) (β := R[X][Y]) (4 : R[X][Y])
          ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.a₆) : R[X][Y])) =
    HPow.hPow (β := ℕ)
        (HMul.hMul (α := R[X][Y]) 2 Y +
          HAdd.hAdd (β := R[X][Y])
            (HMul.hMul (α := R[X][Y]) (β := R[X][Y])
              ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.toAffine.a₁) : R[X][Y])
              ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]))
            ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.toAffine.a₃) : R[X][Y]))
        2 -
      4 *
        (HPow.hPow (α := R[X][Y]) (β := ℕ) Y 2 +
            HAdd.hAdd (β := R[X][Y])
                (HMul.hMul (α := R[X][Y]) (β := R[X][Y])
                  ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.toAffine.a₁) : R[X][Y])
                  ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]))
                ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.toAffine.a₃) : R[X][Y]) *
              Y -
          HAdd.hAdd (β := R[X][Y])
            (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) 3 +
                HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.toAffine.a₂) : R[X][Y])
                  (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) 2) +
              HMul.hMul (α := R[X][Y]) (β := R[X][Y])
                ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.toAffine.a₄) : R[X][Y])
                ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]))
            ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.toAffine.a₆) : R[X][Y]))

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 2 =
    HAdd.hAdd (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) W.Ψ₂Sq : R[X][Y])
      (HMul.hMul (α := R[X][Y]) 4 W.toAffine.polynomial)

Tactic:
simp [C_Ψ₂Sq]

Premises used: WeierstrassCurve.C_Ψ₂Sq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ HPow.hPow (α := CoordinateRing W) (β := ℕ) ((mk W : (a : R[X][Y]) → CoordinateRing W) W.ψ₂) 2 =
    (mk W : (a : R[X][Y]) → CoordinateRing W) ((C : (a : R[X]) → R[X][Y]) W.Ψ₂Sq)

Tactic:
simp [C_Ψ₂Sq]

Premises used: WeierstrassCurve.C_Ψ₂Sq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ Eq (α := R[X]) W.Ψ₂Sq W.twoTorsionPolynomial.toPoly

Tactic:
rfl

Premises used: WeierstrassCurve.b₂, Cubic.toPoly, rfl, WeierstrassCurve.b₆
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ Eq (α := R[X]) (W.preΨ' 0) 0

Tactic:
preNormEDS'_zero ..

Premises used: WeierstrassCurve.preΨ', preNormEDS'_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ Eq (α := R[X]) (W.preΨ' 1) 1

Tactic:
preNormEDS'_one ..

Premises used: WeierstrassCurve.preΨ', preNormEDS'_one
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ Eq (α := R[X]) (W.preΨ' 2) 1

Tactic:
preNormEDS'_two ..

Premises used: preNormEDS'_two, WeierstrassCurve.preΨ'
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ Eq (α := R[X]) (W.preΨ' 3) W.Ψ₃

Tactic:
preNormEDS'_three ..

Premises used: WeierstrassCurve.preΨ', preNormEDS'_three
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ Eq (α := R[X]) (W.preΨ' 4) W.preΨ₄

Tactic:
preNormEDS'_four ..

Premises used: preNormEDS'_four, WeierstrassCurve.preΨ'