awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Affine R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
x₁ y₁ x₂ ℓ : A
rw :
  (W'⁄B).negAddY (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂)
      (((↑f : A →+* B) : (a : A) → B) y₁) (((↑f : A →+* B) : (a : A) → B) ℓ) =
    ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).negAddY x₁ x₂ y₁ ℓ)
rw₁ :
  (W'⁄B).negAddY (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂)
      (((↑f : A →+* B) : (a : A) → B) y₁) (((↑f : A →+* B) : (a : A) → B) ℓ) =
    ((W'⁄A).map (↑f : A →+* B)).negAddY (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂)
      (((↑f : A →+* B) : (a : A) → B) y₁) (((↑f : A →+* B) : (a : A) → B) ℓ)
rw₂ rw₃ :
  (W'⁄B).negAddY (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂)
      (((↑f : A →+* B) : (a : A) → B) y₁) (((↑f : A →+* B) : (a : A) → B) ℓ) =
    (W'⁄B).negAddY (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂)
      (((↑f : A →+* B) : (a : A) → B) y₁) (((↑f : A →+* B) : (a : A) → B) ℓ)
⊢ (W'⁄B).negAddY ((f : (a : A) → B) x₁) ((f : (a : A) → B) x₂) ((f : (a : A) → B) y₁) ((f : (a : A) → B) ℓ) =
    (f : (a : A) → B) ((W'⁄A).negAddY x₁ x₂ y₁ ℓ)

Tactic:
rw [← RingHom.coe_coe, ← map_negAddY, map_baseChange]

Premises used: RingHom.coe_coe, WeierstrassCurve.Affine.map_baseChange, WeierstrassCurve.Affine.map_negAddY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Affine R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
x₁ y₁ x₂ ℓ : A
rw :
  (W'⁄B).addY (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂)
      (((↑f : A →+* B) : (a : A) → B) y₁) (((↑f : A →+* B) : (a : A) → B) ℓ) =
    ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).addY x₁ x₂ y₁ ℓ)
rw₁ :
  (W'⁄B).addY (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂)
      (((↑f : A →+* B) : (a : A) → B) y₁) (((↑f : A →+* B) : (a : A) → B) ℓ) =
    ((W'⁄A).map (↑f : A →+* B)).addY (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂)
      (((↑f : A →+* B) : (a : A) → B) y₁) (((↑f : A →+* B) : (a : A) → B) ℓ)
rw₂ rw₃ :
  (W'⁄B).addY (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂)
      (((↑f : A →+* B) : (a : A) → B) y₁) (((↑f : A →+* B) : (a : A) → B) ℓ) =
    (W'⁄B).addY (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂)
      (((↑f : A →+* B) : (a : A) → B) y₁) (((↑f : A →+* B) : (a : A) → B) ℓ)
⊢ (W'⁄B).addY ((f : (a : A) → B) x₁) ((f : (a : A) → B) x₂) ((f : (a : A) → B) y₁) ((f : (a : A) → B) ℓ) =
    (f : (a : A) → B) ((W'⁄A).addY x₁ x₂ y₁ ℓ)

Tactic:
rw [← RingHom.coe_coe, ← map_addY, map_baseChange]

Premises used: WeierstrassCurve.Affine.map_addY, RingHom.coe_coe, WeierstrassCurve.Affine.map_baseChange
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
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 : Algebra R S
inst_5 : DecidableEq F
inst_6 : DecidableEq K
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₁ x₂ y₁ y₂ : F
rw :
  (W'⁄K).slope (((↑f : F →+* K) : (a : F) → K) x₁) (((↑f : F →+* K) : (a : F) → K) x₂)
      (((↑f : F →+* K) : (a : F) → K) y₁) (((↑f : F →+* K) : (a : F) → K) y₂) =
    ((↑f : F →+* K) : (a : F) → K) ((W'⁄F).slope x₁ x₂ y₁ y₂)
rw₁ :
  (W'⁄K).slope (((↑f : F →+* K) : (a : F) → K) x₁) (((↑f : F →+* K) : (a : F) → K) x₂)
      (((↑f : F →+* K) : (a : F) → K) y₁) (((↑f : F →+* K) : (a : F) → K) y₂) =
    ((W'⁄F).map (↑f : F →+* K)).slope (((↑f : F →+* K) : (a : F) → K) x₁) (((↑f : F →+* K) : (a : F) → K) x₂)
      (((↑f : F →+* K) : (a : F) → K) y₁) (((↑f : F →+* K) : (a : F) → K) y₂)
rw₂ rw₃ :
  (W'⁄K).slope (((↑f : F →+* K) : (a : F) → K) x₁) (((↑f : F →+* K) : (a : F) → K) x₂)
      (((↑f : F →+* K) : (a : F) → K) y₁) (((↑f : F →+* K) : (a : F) → K) y₂) =
    (W'⁄K).slope (((↑f : F →+* K) : (a : F) → K) x₁) (((↑f : F →+* K) : (a : F) → K) x₂)
      (((↑f : F →+* K) : (a : F) → K) y₁) (((↑f : F →+* K) : (a : F) → K) y₂)
⊢ (W'⁄K).slope ((f : (a : F) → K) x₁) ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₁) ((f : (a : F) → K) y₂) =
    (f : (a : F) → K) ((W'⁄F).slope x₁ x₂ y₁ y₂)

Tactic:
rw [← RingHom.coe_coe, ← map_slope, map_baseChange]

Premises used: RingHom.coe_coe, WeierstrassCurve.Affine.map_baseChange, WeierstrassCurve.Affine.map_slope
-- 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
⊢ IsScalarTower R R[X] W'.CoordinateRing

Tactic:
inferInstance

Premises used: inferInstance
-- 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 : Subsingleton R
⊢ Subsingleton.{r + 1} W'.CoordinateRing

Tactic:
Module.subsingleton R[X] _

Premises used: Polynomial, Module.subsingleton
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
n : Fin 2
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
n : Fin 2
nontriviality :
  Subsingleton R →
    (CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) n =
      HPow.hPow (α := AdjoinRoot (R := R[X]) W'.polynomial) (PowerBasis.gen (AdjoinRoot.powerBasis' ⋯)) (↑n : ℕ)
nontriviality₁ :
  Nontrivial R →
    (CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) n =
      HPow.hPow (α := AdjoinRoot (R := R[X]) W'.polynomial) (PowerBasis.gen (AdjoinRoot.powerBasis' ⋯)) (↑n : ℕ)
⊢ (CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) n =
    HPow.hPow (α := AdjoinRoot (R := R[X]) W'.polynomial) (PowerBasis.gen (AdjoinRoot.powerBasis' ⋯)) (↑n : ℕ)

Tactic:
classical
  nontriviality R
  rw [CoordinateRing.basis, Or.by_cases, dif_neg <| not_subsingleton R, Basis.reindex_apply,
    PowerBasis.basis_eq_pow, finCongr_symm_apply, Fin.val_cast]

Premises used: dif_neg, PowerBasis.basis_eq_pow, WeierstrassCurve.Affine.CoordinateRing.basis, Or.by_cases, finCongr_symm_apply, Fin.val_cast, Module.Basis.reindex_apply
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
⊢ Eq (α := W'.CoordinateRing) ((CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) 0 : W'.CoordinateRing)
    (1 : W'.CoordinateRing)

Tactic:
simpa only [basis_apply] using pow_zero _

Premises used: pow_zero, WeierstrassCurve.Affine.CoordinateRing.basis_apply
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
⊢ Eq (α := W'.CoordinateRing) ((CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) 1 : W'.CoordinateRing)
    ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y : W'.CoordinateRing)

Tactic:
simpa only [basis_apply] using pow_one _

Premises used: pow_one, WeierstrassCurve.Affine.CoordinateRing.basis_apply
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
h :
  ∀ (n : Fin 2),
    Eq (α := W'.CoordinateRing) ((CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) n : W'.CoordinateRing)
      (![1, (mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y] n : W'.CoordinateRing)
⊢ Eq (α := (a : Fin 2) → W'.CoordinateRing) (⇑(CoordinateRing.basis W') : (a : Fin 2) → W'.CoordinateRing)
    ![1, (mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y]

Tactic:
ext n
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
n : Fin 2
h :
  Eq (α := W'.CoordinateRing)
    ((CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : W'.CoordinateRing)
    (![1, (mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : W'.CoordinateRing)
h₁ :
  Eq (α := W'.CoordinateRing)
    ((CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : W'.CoordinateRing)
    (![1, (mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : W'.CoordinateRing)
⊢ Eq (α := W'.CoordinateRing) ((CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) n : W'.CoordinateRing)
    (![1, (mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y] n : W'.CoordinateRing)

Tactic:
fin_cases n
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
⊢ Eq (α := W'.CoordinateRing)
    ((CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : W'.CoordinateRing)
    (![1, (mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : W'.CoordinateRing)

Tactic:
basis_zero

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, Fin.ofNat, Fin.induction, WeierstrassCurve.Affine.CoordinateRing.basis_zero, Fin.cases, Matrix.vecCons
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
⊢ Eq (α := W'.CoordinateRing)
    ((CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : W'.CoordinateRing)
    (![1, (mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : W'.CoordinateRing)

Tactic:
basis_one

Premises used: Eq.mpr, WeierstrassCurve.Affine.CoordinateRing.basis_one, Fin.cons, Fin.induction.go, Fin.ofNat, Fin.induction, Fin.cases, Matrix.vecCons
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
⊢ Eq (α := W'.CoordinateRing)
    ((CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : W'.CoordinateRing)
    (![1, (mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : W'.CoordinateRing)

Tactic:
exacts [basis_zero, basis_one]

Premises used: WeierstrassCurve.Affine.CoordinateRing.basis_one, WeierstrassCurve.Affine.CoordinateRing.basis_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x : R[X]
y : W'.CoordinateRing
⊢ x • y =
    HMul.hMul (α := W'.CoordinateRing)
      ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) ((C : (a : R[X]) → R[X][Y]) x) : W'.CoordinateRing) y

Tactic:
(algebraMap_smul W'.CoordinateRing x y).symm

Premises used: Submodule.Quotient.mk, algebraMap_smul, WeierstrassCurve.Affine.CoordinateRing, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
p q : R[X]
hpq :
  HSMul.hSMul (β := W'.CoordinateRing) p 1 +
      HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
    0
⊢ Eq.{r + 1} (α := W'.CoordinateRing)
      (∑ i : Fin 2,
        HSMul.hSMul (β := W'.CoordinateRing) (![p, q] i)
          ((CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) i : W'.CoordinateRing))
      0 →
    ∀ (i : Fin 2), ![p, q] i = 0

Tactic:
have h := Fintype.linearIndependent_iff.mp (CoordinateRing.basis W').linearIndependent ![p, q]
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
p q : R[X]
hpq :
  HSMul.hSMul (β := W'.CoordinateRing) p 1 +
      HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
    0
h :
  Eq.{r + 1} (α := W'.CoordinateRing)
      (∑ i : Fin 2,
        HSMul.hSMul (β := W'.CoordinateRing) (![p, q] i)
          ((CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) i : W'.CoordinateRing))
      0 →
    ∀ (i : Fin 2), ![p, q] i = 0
⊢ HSMul.hSMul (β := W'.CoordinateRing) (![p, q] 0) 1 +
        HSMul.hSMul (β := W'.CoordinateRing) (![p, q] 1) ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
      0 →
    ∀ (i : Fin 2), ![p, q] i = 0

Tactic:
rw [Fin.sum_univ_succ, basis_zero, Fin.sum_univ_one, Fin.succ_zero_eq_one, basis_one] at h

Premises used: WeierstrassCurve.Affine.CoordinateRing.basis_one, Fin.sum_univ_one, Fin.succ_zero_eq_one, WeierstrassCurve.Affine.CoordinateRing.basis_zero, Fin.sum_univ_succ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
p q : R[X]
hpq :
  HSMul.hSMul (β := W'.CoordinateRing) p 1 +
      HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
    0
h :
  HSMul.hSMul (β := W'.CoordinateRing) (![p, q] 0) 1 +
        HSMul.hSMul (β := W'.CoordinateRing) (![p, q] 1) ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
      0 →
    ∀ (i : Fin 2), ![p, q] i = 0
⊢ p = 0 ∧ q = 0

Tactic:
⟨h hpq 0, h hpq 1⟩

Premises used: And.intro, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
p q : R[X]
hpq :
  HSMul.hSMul (β := W'.CoordinateRing) p 1 +
      HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
    0
h :
  HSMul.hSMul (β := W'.CoordinateRing) (![p, q] 0) 1 +
        HSMul.hSMul (β := W'.CoordinateRing) (![p, q] 1) ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
      0 →
    ∀ (i : Fin 2), ![p, q] i = 0
⊢ p = 0 ∧ q = 0

Tactic:
exact ⟨h hpq 0, h hpq 1⟩
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x : W'.CoordinateRing
⊢ ∑ i : Fin 2,
      HSMul.hSMul (α := R[X]) (β := W'.CoordinateRing)
        ((Basis.equivFun (CoordinateRing.basis W') : (a : W'.CoordinateRing) → Fin 2 → R[X]) x i : R[X])
        ((CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) i : W'.CoordinateRing) =
    x

Tactic:
have h := (CoordinateRing.basis W').sum_equivFun x
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x : W'.CoordinateRing
h :
  ∑ i : Fin 2,
      HSMul.hSMul (α := R[X]) (β := W'.CoordinateRing)
        ((Basis.equivFun (CoordinateRing.basis W') : (a : W'.CoordinateRing) → Fin 2 → R[X]) x i : R[X])
        ((CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) i : W'.CoordinateRing) =
    x
⊢ HSMul.hSMul (α := R[X]) (β := W'.CoordinateRing)
        ((Basis.equivFun (CoordinateRing.basis W') : (a : W'.CoordinateRing) → Fin 2 → R[X]) x 0 : R[X]) 1 +
      HSMul.hSMul (α := R[X]) (β := W'.CoordinateRing)
        ((Basis.equivFun (CoordinateRing.basis W') : (a : W'.CoordinateRing) → Fin 2 → R[X]) x 1 : R[X])
        ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
    x

Tactic:
rw [Fin.sum_univ_succ, Fin.sum_univ_one, basis_zero, Fin.succ_zero_eq_one, basis_one] at h

Premises used: WeierstrassCurve.Affine.CoordinateRing.basis_one, Fin.sum_univ_one, Fin.succ_zero_eq_one, WeierstrassCurve.Affine.CoordinateRing.basis_zero, Fin.sum_univ_succ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x : W'.CoordinateRing
h :
  HSMul.hSMul (α := R[X]) (β := W'.CoordinateRing)
        ((Basis.equivFun (CoordinateRing.basis W') : (a : W'.CoordinateRing) → Fin 2 → R[X]) x 0 : R[X]) 1 +
      HSMul.hSMul (α := R[X]) (β := W'.CoordinateRing)
        ((Basis.equivFun (CoordinateRing.basis W') : (a : W'.CoordinateRing) → Fin 2 → R[X]) x 1 : R[X])
        ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
    x
⊢ ∃ (p : R[X]) (q : R[X]),
    HSMul.hSMul (β := W'.CoordinateRing) p 1 +
        HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
      x

Tactic:
⟨_, _, h⟩

Premises used: Exists.intro
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x : W'.CoordinateRing
h :
  HSMul.hSMul (α := R[X]) (β := W'.CoordinateRing)
        ((Basis.equivFun (CoordinateRing.basis W') : (a : W'.CoordinateRing) → Fin 2 → R[X]) x 0 : R[X]) 1 +
      HSMul.hSMul (α := R[X]) (β := W'.CoordinateRing)
        ((Basis.equivFun (CoordinateRing.basis W') : (a : W'.CoordinateRing) → Fin 2 → R[X]) x 1 : R[X])
        ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
    x
⊢ ∃ (p : R[X]) (q : R[X]),
    HSMul.hSMul (β := W'.CoordinateRing) p 1 +
        HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
      x

Tactic:
exact ⟨_, _, h⟩
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
y p q : R[X]
simp :
  HMul.hMul (β := W'.CoordinateRing)
      (HMul.hMul (α := W'.CoordinateRing) (β := W'.CoordinateRing)
          ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) ((C : (a : R[X]) → R[X][Y]) p) : W'.CoordinateRing)
          (1 : W'.CoordinateRing) +
        HMul.hMul (α := W'.CoordinateRing) (β := W'.CoordinateRing)
          ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) ((C : (a : R[X]) → R[X][Y]) q) : W'.CoordinateRing)
          ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y))
      ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) ((C : (a : R[X]) → R[X][Y]) y) : W'.CoordinateRing) =
    HMul.hMul (α := W'.CoordinateRing) (β := W'.CoordinateRing)
          ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) ((C : (a : R[X]) → R[X][Y]) p) : W'.CoordinateRing)
          ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) ((C : (a : R[X]) → R[X][Y]) y) : W'.CoordinateRing) *
        1 +
      HMul.hMul (α := W'.CoordinateRing) (β := W'.CoordinateRing)
          ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) ((C : (a : R[X]) → R[X][Y]) q) : W'.CoordinateRing)
          ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) ((C : (a : R[X]) → R[X][Y]) y) : W'.CoordinateRing) *
        (mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y
⊢ HMul.hMul (β := W'.CoordinateRing)
      (HSMul.hSMul (β := W'.CoordinateRing) p 1 +
        HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y))
      ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) ((C : (a : R[X]) → R[X][Y]) y) : W'.CoordinateRing) =
    HSMul.hSMul (β := W'.CoordinateRing) (p * y) 1 +
      HSMul.hSMul (β := W'.CoordinateRing) (q * y) ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y)

Tactic:
simp only [smul, map_mul]

Premises used: WeierstrassCurve.Affine.CoordinateRing.smul, map_mul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
y p q : R[X]
⊢ HMul.hMul (β := W'.CoordinateRing)
      (HMul.hMul (α := W'.CoordinateRing) (β := W'.CoordinateRing)
          ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) ((C : (a : R[X]) → R[X][Y]) p) : W'.CoordinateRing)
          (1 : W'.CoordinateRing) +
        HMul.hMul (α := W'.CoordinateRing) (β := W'.CoordinateRing)
          ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) ((C : (a : R[X]) → R[X][Y]) q) : W'.CoordinateRing)
          ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y))
      ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) ((C : (a : R[X]) → R[X][Y]) y) : W'.CoordinateRing) =
    HMul.hMul (α := W'.CoordinateRing) (β := W'.CoordinateRing)
          ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) ((C : (a : R[X]) → R[X][Y]) p) : W'.CoordinateRing)
          ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) ((C : (a : R[X]) → R[X][Y]) y) : W'.CoordinateRing) *
        1 +
      HMul.hMul (α := W'.CoordinateRing) (β := W'.CoordinateRing)
          ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) ((C : (a : R[X]) → R[X][Y]) q) : W'.CoordinateRing)
          ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) ((C : (a : R[X]) → R[X][Y]) y) : W'.CoordinateRing) *
        (mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
p q : R[X]
⊢ (fun (x : R[X][Y]) ↦ HPow.hPow (β := ℕ) x 2) Y -
      HSub.hSub (α := R[X][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'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
                HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
              ((C : (a : R) → R[X]) W'.a₆ : R[X])) :
          R[X][Y])
        (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'.a₁ : R[X]) X)
                ((C : (a : R) → R[X]) W'.a₃ : R[X])) :
            R[X][Y])
          Y) =
    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'.a₁ : R[X]) X)
                  ((C : (a : R) → R[X]) W'.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'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
                HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
              ((C : (a : R) → R[X]) W'.a₆ : R[X])) :
          R[X][Y]) *
      1

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
p q : R[X]
⊢ HPow.hPow (α := W'.CoordinateRing) (β := ℕ) ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) 2 =
    (mk W' : (a : R[X][Y]) → W'.CoordinateRing)
      (HSub.hSub (α := R[X][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'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
                HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
              ((C : (a : R) → R[X]) W'.a₆ : R[X])) :
          R[X][Y])
        (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'.a₁ : R[X]) X)
                ((C : (a : R) → R[X]) W'.a₃ : R[X])) :
            R[X][Y])
          Y))

Tactic:
have Y_sq : mk W' Y ^ 2 = mk W' (C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆) -
      C (C W'.a₁ * X + C W'.a₃) * Y) := AdjoinRoot.mk_eq_mk.mpr ⟨1, by rw [polynomial]; ring1⟩
-- 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
f : R →+* S
rw :
  Eq (α := (W'.map f).CoordinateRing)
    (eval₂ (AdjoinRoot.of (W'.map f).polynomial) (AdjoinRoot.root (W'.map f).polynomial)
      (Polynomial.map (mapRingHom f) W'.polynomial))
    0
rw₁ :
  Eq (α := (W'.map f).CoordinateRing)
    (eval₂ (AdjoinRoot.of (W'.map f).polynomial) (AdjoinRoot.root (W'.map f).polynomial) (W'.map f).polynomial) 0
rw₂ rw₃ : Eq.{s + 1} (α := (W'.map f).CoordinateRing) 0 0
⊢ Eq (α := (W'.map f).CoordinateRing)
    (eval₂ (RingHom.comp (AdjoinRoot.of (W'.map f).polynomial) (mapRingHom f)) (AdjoinRoot.root (W'.map f).polynomial)
      W'.polynomial)
    0

Tactic:
rw [← eval₂_map, ← map_polynomial, AdjoinRoot.eval₂_root]

Premises used: Polynomial.eval₂_map, WeierstrassCurve.Affine.map_polynomial, AdjoinRoot.eval₂_root