awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
W : Projective F
K : Type v
inst_1 : Field K
f : F →+* K
Q : Fin 3 → F
hQ : W.Nonsingular Q
u : Fˣ
hP : W.Nonsingular ((fun (m : Fˣ) ↦ m • Q) u)
⊢ HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K)
    (Function.comp.{1, u + 1, v + 1} (β := F) (⇑f : (a : F) → K) ((fun (m : Fˣ) ↦ m • Q) u)) ((⇑f : (a : F) → K) ∘ Q)

Tactic:
⟨Units.map f u, (comp_smul ..).symm⟩

Premises used: Set.Mem, setOf, MulAction.orbit, Exists.intro, Set.range, DFunLike.coe, Units.map
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
W : Projective F
K : Type v
inst_1 : Field K
f : F →+* K
Q : Fin 3 → F
hQ : W.Nonsingular Q
u : Fˣ
hP : W.Nonsingular ((fun (m : Fˣ) ↦ m • Q) u)
⊢ HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K)
    (Function.comp.{1, u + 1, v + 1} (β := F) (⇑f : (a : F) → K) ((fun (m : Fˣ) ↦ m • Q) u)) ((⇑f : (a : F) → K) ∘ Q)

Tactic:
exact ⟨Units.map f u, (comp_smul ..).symm⟩
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ W'.NonsingularLift ⟦P⟧ ↔ W'.Nonsingular P

Tactic:
Iff.rfl

Premises used: Iff.rfl, WeierstrassCurve.Projective.NonsingularLift
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : Nontrivial R
⊢ W'.NonsingularLift ⟦![0, 1, 0]⟧

Tactic:
nonsingular_zero

Premises used: WeierstrassCurve.Projective.nonsingular_zero, WeierstrassCurve.Projective.NonsingularLift
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
a b : R
⊢ W'.NonsingularLift ⟦![a, b, 1]⟧ ↔ W'.toAffine.Nonsingular a b

Tactic:
nonsingular_some a b

Premises used: WeierstrassCurve.Projective.nonsingular_some, WeierstrassCurve.Projective.NonsingularLift
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
f : R →+* S
⊢ HPow.hPow (α := MvPolynomial (Fin 3) S) (β := ℕ) («X» y) 2 * «X» z +
          HMul.hMul (α := MvPolynomial (Fin 3) S) (β := MvPolynomial (Fin 3) S)
                ((C : (a : S) → MvPolynomial (Fin 3) S) (W'.map f).a₁ : MvPolynomial (Fin 3) S) («X» x) *
              «X» y *
            «X» z +
        HMul.hMul (α := MvPolynomial (Fin 3) S) (β := MvPolynomial (Fin 3) S)
            ((C : (a : S) → MvPolynomial (Fin 3) S) (W'.map f).a₃ : MvPolynomial (Fin 3) S) («X» y) *
          HPow.hPow (α := MvPolynomial (Fin 3) S) (β := ℕ) («X» z) 2 -
      (HPow.hPow (α := MvPolynomial (Fin 3) S) (β := ℕ) («X» x) 3 +
            HMul.hMul (α := MvPolynomial (Fin 3) S)
                ((C : (a : S) → MvPolynomial (Fin 3) S) (W'.map f).a₂ : MvPolynomial (Fin 3) S)
                (HPow.hPow (α := MvPolynomial (Fin 3) S) (β := ℕ) («X» x) 2) *
              «X» z +
          HMul.hMul (α := MvPolynomial (Fin 3) S) (β := MvPolynomial (Fin 3) S)
              ((C : (a : S) → MvPolynomial (Fin 3) S) (W'.map f).a₄ : MvPolynomial (Fin 3) S) («X» x) *
            HPow.hPow (α := MvPolynomial (Fin 3) S) (β := ℕ) («X» z) 2 +
        HMul.hMul (α := MvPolynomial (Fin 3) S)
          ((C : (a : S) → MvPolynomial (Fin 3) S) (W'.map f).a₆ : MvPolynomial (Fin 3) S)
          (HPow.hPow (α := MvPolynomial (Fin 3) S) (β := ℕ) («X» z) 3)) =
    ((MvPolynomial.map f : RingHom.{r, s} (MvPolynomial (Fin 3) R) (MvPolynomial (Fin 3) S)) :
        (a : MvPolynomial (Fin 3) R) → MvPolynomial (Fin 3) S)
      (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Y 2 * Z +
            HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
                  ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₁ : MvPolynomial (Fin 3) R) X *
                Y *
              Z +
          HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
              ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₃ : MvPolynomial (Fin 3) R) Y *
            HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 2 -
        (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) X 3 +
              HMul.hMul (α := MvPolynomial (Fin 3) R)
                  ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₂ : MvPolynomial (Fin 3) R)
                  (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) X 2) *
                Z +
            HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
                ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₄ : MvPolynomial (Fin 3) R) X *
              HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 2 +
          HMul.hMul (α := MvPolynomial (Fin 3) R)
            ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₆ : MvPolynomial (Fin 3) R)
            (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 3)))

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
f : R →+* S
P : Fin 3 → R
h : W'.Equation P
rw : Eq (α := S) ((eval ((⇑f : (a : R) → S) ∘ P) : (a : MvPolynomial (Fin 3) S) → S) (W'.map f).polynomial : S) (0 : S)
rw₁ :
  Eq.{s + 1} (α := S)
    ((eval ((⇑f : (a : R) → S) ∘ P) : (a : MvPolynomial (Fin 3) S) → S)
        (((MvPolynomial.map f : RingHom.{r, s} (MvPolynomial (Fin 3) R) (MvPolynomial (Fin 3) S)) :
              (a : MvPolynomial (Fin 3) R) → MvPolynomial (Fin 3) S)
            W'.polynomial :
          MvPolynomial (Fin 3) S) :
      S)
    (0 : S)
rw₂ : eval₂ f ((⇑f : (a : R) → S) ∘ P) W'.polynomial = 0
rw₃ :
  Eq.{s + 1} (α := S) ((f : (a : R) → S) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomial : R) : S) (0 : S)
rw₄ : Eq.{s + 1} (α := S) ((f : (a : R) → S) 0 : S) (0 : S)
rw₅ rw₆ : Eq.{s + 1} (α := S) 0 0
⊢ (W'.map f).Equation ((⇑f : (a : R) → S) ∘ P)

Tactic:
rw [Equation, map_polynomial, eval_map, ← eval₂_comp, h, map_zero]

Premises used: WeierstrassCurve.Projective.Equation, MvPolynomial.eval_map, map_zero, MvPolynomial.eval₂_comp, WeierstrassCurve.Projective.map_polynomial
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
f : R →+* S
hf : Function.Injective.{r + 1, s + 1} (α := R) (β := S) (⇑f : (a : R) → S)
P : Fin 3 → R
⊢ (W'.map f).Equation ((⇑f : (a : R) → S) ∘ P) ↔ W'.Equation P

Tactic:
simp only [Equation, map_polynomial, eval_map, ← eval₂_comp, map_eq_zero_iff f hf]

Premises used: WeierstrassCurve.Projective.Equation, MvPolynomial.eval_map, map_eq_zero_iff, MvPolynomial.eval₂_comp, WeierstrassCurve.Projective.map_polynomial
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
f : R →+* S
⊢ Eq (α := MvPolynomial (Fin 3) S) (W'.map f).polynomialX
    (((MvPolynomial.map f : RingHom.{r, s} (MvPolynomial (Fin 3) R) (MvPolynomial (Fin 3) S)) :
        (a : MvPolynomial (Fin 3) R) → MvPolynomial (Fin 3) S)
      W'.polynomialX)

Tactic:
simp only [polynomialX, map_polynomial, pderiv_map]

Premises used: MvPolynomial.pderiv_map, WeierstrassCurve.Projective.polynomialX, WeierstrassCurve.Projective.map_polynomial
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
f : R →+* S
⊢ Eq (α := MvPolynomial (Fin 3) S) (W'.map f).polynomialY
    (((MvPolynomial.map f : RingHom.{r, s} (MvPolynomial (Fin 3) R) (MvPolynomial (Fin 3) S)) :
        (a : MvPolynomial (Fin 3) R) → MvPolynomial (Fin 3) S)
      W'.polynomialY)

Tactic:
simp only [polynomialY, map_polynomial, pderiv_map]

Premises used: WeierstrassCurve.Projective.polynomialY, MvPolynomial.pderiv_map, WeierstrassCurve.Projective.map_polynomial
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
f : R →+* S
⊢ Eq (α := MvPolynomial (Fin 3) S) (W'.map f).polynomialZ
    (((MvPolynomial.map f : RingHom.{r, s} (MvPolynomial (Fin 3) R) (MvPolynomial (Fin 3) S)) :
        (a : MvPolynomial (Fin 3) R) → MvPolynomial (Fin 3) S)
      W'.polynomialZ)

Tactic:
simp only [polynomialZ, map_polynomial, pderiv_map]

Premises used: WeierstrassCurve.Projective.polynomialZ, MvPolynomial.pderiv_map, WeierstrassCurve.Projective.map_polynomial
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
f : R →+* S
hf : Function.Injective.{r + 1, s + 1} (α := R) (β := S) (⇑f : (a : R) → S)
P : Fin 3 → R
⊢ (W'.map f).Nonsingular ((⇑f : (a : R) → S) ∘ P) ↔ W'.Nonsingular P

Tactic:
simp only [Nonsingular, W'.map_equation hf, map_polynomialX, map_polynomialY, map_polynomialZ,
    eval_map, ← eval₂_comp, map_ne_zero_iff f hf]

Premises used: WeierstrassCurve.Projective.Nonsingular, MvPolynomial.eval_map, WeierstrassCurve.Projective.map_polynomialX, WeierstrassCurve.Projective.map_equation, WeierstrassCurve.Projective.map_polynomialZ, MvPolynomial.eval₂_comp, map_ne_zero_iff, WeierstrassCurve.Projective.map_polynomialY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
⊢ (W'⁄A).map (↑f : A →+* B) = W'⁄B

Tactic:
WeierstrassCurve.map_baseChange W' f

Premises used: WeierstrassCurve.map_baseChange
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
rw : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomial ((W'⁄A).map (↑f : A →+* B)).polynomial
rw₁ rw₂ : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomial (W'⁄B).polynomial
⊢ Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomial
    (((MvPolynomial.map (↑f : A →+* B) : RingHom.{u, v} (MvPolynomial (Fin 3) A) (MvPolynomial (Fin 3) B)) :
        (a : MvPolynomial (Fin 3) A) → MvPolynomial (Fin 3) B)
      (W'⁄A).polynomial)

Tactic:
rw [← map_polynomial, map_baseChange]

Premises used: WeierstrassCurve.Projective.map_baseChange, WeierstrassCurve.Projective.map_polynomial
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
P : Fin 3 → A
h : (W'⁄A).Equation P
⊢ ((W'⁄A).map f.toRingHom).Equation ((⇑f.toRingHom : (a : A) → B) ∘ P)

Tactic:
Equation.map f.toRingHom h

Premises used: AlgHom.toRingHom, WeierstrassCurve.Projective.Equation.map
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
P : Fin 3 → A
h : (W'⁄A).Equation P
h₁ : W'⁄B = (W'⁄A).map f.toRingHom
⊢ (W'⁄B).Equation ((⇑f : (a : A) → B) ∘ P)

Tactic:
convert! Equation.map f.toRingHom h using 1

Premises used: AlgHom.toRingHom, WeierstrassCurve.Projective.Equation.map
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
P : Fin 3 → A
h : (W'⁄A).Equation P
h₁ : W'⁄B = (W'⁄A).map (↑f : A →+* B)
h₂ h₃ : W'⁄B = W'⁄B
⊢ W'⁄B = (W'⁄A).map f.toRingHom

Tactic:
rw [AlgHom.toRingHom_eq_coe, map_baseChange]

Premises used: AlgHom.toRingHom_eq_coe, WeierstrassCurve.Projective.map_baseChange
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
hf : Function.Injective.{u + 1, v + 1} (α := A) (β := B) (⇑f : (a : A) → B)
P : Fin 3 → A
rw : (W'⁄B).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔ (W'⁄A).Equation P
rw₁ :
  (W'⁄B).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔
    ((W'⁄A).map f.toRingHom).Equation ((⇑f.toRingHom : (a : A) → B) ∘ P)
rw₂ :
  (W'⁄B).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔
    ((W'⁄A).map (↑f : A →+* B)).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
rw₃ rw₄ : (W'⁄B).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔ (W'⁄B).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
⊢ (W'⁄B).Equation ((⇑f : (a : A) → B) ∘ P) ↔ (W'⁄A).Equation P

Tactic:
rw [← RingHom.coe_coe, ← map_equation _ hf, AlgHom.toRingHom_eq_coe, map_baseChange]

Premises used: RingHom.coe_coe, WeierstrassCurve.Projective.map_equation, AlgHom.toRingHom_eq_coe, WeierstrassCurve.Projective.map_baseChange
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
rw : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialX ((W'⁄A).map (↑f : A →+* B)).polynomialX
rw₁ rw₂ : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialX (W'⁄B).polynomialX
⊢ Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialX
    (((MvPolynomial.map (↑f : A →+* B) : RingHom.{u, v} (MvPolynomial (Fin 3) A) (MvPolynomial (Fin 3) B)) :
        (a : MvPolynomial (Fin 3) A) → MvPolynomial (Fin 3) B)
      (W'⁄A).polynomialX)

Tactic:
rw [← map_polynomialX, map_baseChange]

Premises used: WeierstrassCurve.Projective.map_polynomialX, WeierstrassCurve.Projective.map_baseChange
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
rw : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialY ((W'⁄A).map (↑f : A →+* B)).polynomialY
rw₁ rw₂ : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialY (W'⁄B).polynomialY
⊢ Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialY
    (((MvPolynomial.map (↑f : A →+* B) : RingHom.{u, v} (MvPolynomial (Fin 3) A) (MvPolynomial (Fin 3) B)) :
        (a : MvPolynomial (Fin 3) A) → MvPolynomial (Fin 3) B)
      (W'⁄A).polynomialY)

Tactic:
rw [← map_polynomialY, map_baseChange]

Premises used: WeierstrassCurve.Projective.map_baseChange, WeierstrassCurve.Projective.map_polynomialY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
rw : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialZ ((W'⁄A).map (↑f : A →+* B)).polynomialZ
rw₁ rw₂ : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialZ (W'⁄B).polynomialZ
⊢ Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialZ
    (((MvPolynomial.map (↑f : A →+* B) : RingHom.{u, v} (MvPolynomial (Fin 3) A) (MvPolynomial (Fin 3) B)) :
        (a : MvPolynomial (Fin 3) A) → MvPolynomial (Fin 3) B)
      (W'⁄A).polynomialZ)

Tactic:
rw [← map_polynomialZ, map_baseChange]

Premises used: WeierstrassCurve.Projective.map_polynomialZ, WeierstrassCurve.Projective.map_baseChange
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
hf : Function.Injective.{u + 1, v + 1} (α := A) (β := B) (⇑f : (a : A) → B)
P : Fin 3 → A
rw : (W'⁄B).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔ (W'⁄A).Nonsingular P
rw₁ :
  (W'⁄B).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔
    ((W'⁄A).map f.toRingHom).Nonsingular ((⇑f.toRingHom : (a : A) → B) ∘ P)
rw₂ :
  (W'⁄B).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔
    ((W'⁄A).map (↑f : A →+* B)).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
rw₃ rw₄ :
  (W'⁄B).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔ (W'⁄B).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
⊢ (W'⁄B).Nonsingular ((⇑f : (a : A) → B) ∘ P) ↔ (W'⁄A).Nonsingular P

Tactic:
rw [← RingHom.coe_coe, ← map_nonsingular _ hf, AlgHom.toRingHom_eq_coe, map_baseChange]

Premises used: RingHom.coe_coe, AlgHom.toRingHom_eq_coe, WeierstrassCurve.Projective.map_baseChange, WeierstrassCurve.Projective.map_nonsingular
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
X Y Z : R
⊢ W'.negY ![X, Y, Z] = -Y - W'.a₁ * X - W'.a₃ * Z

Tactic:
rfl

Premises used: WeierstrassCurve.Projective.negY, Eq.mpr, Fin.cons, Fin.induction.go, Fin.induction, Fin.cases, Matrix.vecCons, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
simp : -(u * P y) - W'.a₁ * (u * P x) - W'.a₃ * (u * P z) = u * (-P y - W'.a₁ * P x - W'.a₃ * P z)
⊢ W'.negY (u • P) = u * W'.negY P

Tactic:
simp only [negY, smul_fin3_ext]

Premises used: WeierstrassCurve.Projective.negY, WeierstrassCurve.Projective.smul_fin3_ext
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
⊢ -(u * P y) - W'.a₁ * (u * P x) - W'.a₃ * (u * P z) = u * (-P y - W'.a₁ * P x - W'.a₃ * P z)

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
rw : -P y - W'.a₁ * P x - W'.a₃ * P z = -P y
rw₁ : -P y - W'.a₁ * P x - W'.a₃ * 0 = -P y
rw₂ : -P y - W'.a₁ * 0 - W'.a₃ * 0 = -P y
rw₃ : -P y - 0 - W'.a₃ * 0 = -P y
rw₄ : -P y - W'.a₃ * 0 = -P y
rw₅ : -P y - 0 = -P y
rw₆ rw₇ : -P y = -P y
⊢ W'.negY P = -P y

Tactic:
rw [negY, hPz, X_eq_zero_of_Z_eq_zero hP hPz, mul_zero, sub_zero, mul_zero, sub_zero]

Premises used: WeierstrassCurve.Projective.negY, sub_zero, MulZeroClass.mul_zero, WeierstrassCurve.Projective.X_eq_zero_of_Z_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
a :
  (-P y - W.a₁ * P x - W.a₃ * P z) / P z + -W.a₃ * 1 -
      (-(P y / P z) - W.toAffine.a₁ * (P x / P z) - W.toAffine.a₃ + -W.a₃ * (P z / P z)) =
    0
⊢ W.negY P / P z + -W.a₃ * 1 - (W.toAffine.negY (P x / P z) (P y / P z) + -W.a₃ * (P z / P z)) = 0

Tactic:
rw [negY, Affine.negY]

Premises used: WeierstrassCurve.Projective.negY, WeierstrassCurve.Affine.negY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (-P y - W.a₁ * P x - W.a₃ * P z) / P z + -W.a₃ * 1 -
      (-(P y / P z) - W.toAffine.a₁ * (P x / P z) - W.toAffine.a₃ + -W.a₃ * (P z / P z)) =
    0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
a : W.negY P / P z + -W.a₃ * 1 - (W.toAffine.negY (P x / P z) (P y / P z) + -W.a₃ * (P z / P z)) = 0
⊢ W.negY P / P z = W.toAffine.negY (P x / P z) (P y / P z)

Tactic:
linear_combination (norm := (rw [negY, Affine.negY]; ring1)) -W.a₃ * div_self hPz

Premises used: WeierstrassCurve.Projective.negY, WeierstrassCurve.a₃, WeierstrassCurve.Affine.negY, div_self
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z = Q x * P z
⊢ P z * Q z * (P y * Q z - Q y * P z) * (P y * Q z - (-Q y - W'.a₁ * Q x - W'.a₃ * Q z) * P z) +
        (HPow.hPow (β := ℕ) (Q z) 3 * 0 +
            HPow.hPow (β := ℕ) (P z) 3 *
              (HPow.hPow (β := ℕ) (Q y) 2 * Q z + W'.a₁ * Q x * Q y * Q z + W'.a₃ * Q y * HPow.hPow (β := ℕ) (Q z) 2 -
                (HPow.hPow (β := ℕ) (Q x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (Q x) 2 * Q z +
                    W'.a₄ * Q x * HPow.hPow (β := ℕ) (Q z) 2 +
                  W'.a₆ * HPow.hPow (β := ℕ) (Q z) 3)) +
          (HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (Q z) 2 + P x * Q x * P z * Q z +
                      HPow.hPow (β := ℕ) (Q x) 2 * HPow.hPow (β := ℕ) (P z) 2 -
                    W'.a₁ * P y * P z * HPow.hPow (β := ℕ) (Q z) 2 +
                  W'.a₂ * P x * HPow.hPow (β := ℕ) (Q z) 2 * P z +
                W'.a₂ * Q x * HPow.hPow (β := ℕ) (P z) 2 * Q z +
              W'.a₄ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (Q z) 2) *
            (Q x * P z)) -
      (0 +
        (HPow.hPow (β := ℕ) (Q z) 3 *
              (HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
                (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
                    W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
                  W'.a₆ * HPow.hPow (β := ℕ) (P z) 3)) +
            HPow.hPow (β := ℕ) (P z) 3 * 0 +
          (HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (Q z) 2 + P x * Q x * P z * Q z +
                      HPow.hPow (β := ℕ) (Q x) 2 * HPow.hPow (β := ℕ) (P z) 2 -
                    W'.a₁ * P y * P z * HPow.hPow (β := ℕ) (Q z) 2 +
                  W'.a₂ * P x * HPow.hPow (β := ℕ) (Q z) 2 * P z +
                W'.a₂ * Q x * HPow.hPow (β := ℕ) (P z) 2 * Q z +
              W'.a₄ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (Q z) 2) *
            (P x * Q z))) =
    0

Tactic:
ring1