mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
i : D.rels
⊢ (aeval p) (Presentation.relationOfHasCoeffs (↥(subalgebra R D)) i) ∈
    Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))) ^ 2

Tactic:
]

Goal state after:
case refine_1
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
i : D.rels
⊢ (aeval p) (Presentation.relationOfHasCoeffs (↥(subalgebra R D)) i) ∈
    Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))) ^ 2
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
i : D.rels
hinj : Function.Injective ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
⊢ ∃ p_1,
    p_1.IsHomogeneous 2 ∧
      (eval (Presentation.relationOfHasCoeffs ↥(subalgebra R D))) p_1 =
        (aeval p) (Presentation.relationOfHasCoeffs (↥(subalgebra R D)) i)

Tactic:
]

Goal state after:
case refine_1
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
i : D.rels
hinj : Function.Injective ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
⊢ ∃ p_1,
    p_1.IsHomogeneous 2 ∧
      (eval (Presentation.relationOfHasCoeffs ↥(subalgebra R D))) p_1 =
        (aeval p) (Presentation.relationOfHasCoeffs (↥(subalgebra R D)) i)
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: case refine_1.refine_1
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
i : D.rels
hinj : Function.Injective ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
q : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))
hq : (MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))) q = D.p i
⊢ (D.p i).IsHomogeneous 2

Tactic:
]

Goal state after:
case refine_1.refine_1
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
i : D.rels
hinj : Function.Injective ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
q : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))
hq : (MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))) q = D.p i
⊢ (D.p i).IsHomogeneous 2
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: case e_6.h1
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
this : Nontrivial (MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))
⊢ (if -1 = 0 then 0 else if -1 = -1 then -1 else Function.surjInv ⋯ (-1)) = -1

Tactic:
]

Goal state after:
case e_6.h1
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
this : Nontrivial (MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))
⊢ (if -1 = 0 then 0 else if -1 = -1 then -1 else Function.surjInv ⋯ (-1)) = -1
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: case e_6.h0
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
this : Nontrivial (MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))
⊢ (if 0 = 0 then 0 else if 0 = -1 then -1 else Function.surjInv ⋯ 0) = 0

Tactic:
]

Goal state after:
case e_6.h0
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
this : Nontrivial (MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))
⊢ (if 0 = 0 then 0 else if 0 = -1 then -1 else Function.surjInv ⋯ 0) = 0
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
hf₀ :
  Function.Surjective
    ⇑(Ideal.Quotient.mkₐ (↥(subalgebra R D))
        (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D)))))
⊢ ((Ideal.Quotient.mkₐ (↥(subalgebra R D))
                (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))).kerSquareLift.comp
          (Ideal.Quotient.liftₐ (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))
            ((Ideal.Quotient.mkₐ (↥(subalgebra R D))
                  (RingHom.ker
                      (Ideal.Quotient.mkₐ (↥(subalgebra R D))
                        (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))) ^
                    2)).comp
              (aeval p))
            ⋯)).comp
      (Ideal.Quotient.mkₐ (↥(subalgebra R D))
        (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))) =
    (AlgHom.id (↥(subalgebra R D)) (Presentation.ModelOfHasCoeffs ↥(subalgebra R D))).comp
      (Ideal.Quotient.mkₐ (↥(subalgebra R D))
        (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D)))))

Tactic:
]

Goal state after:
case refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
hf₀ :
  Function.Surjective
    ⇑(Ideal.Quotient.mkₐ (↥(subalgebra R D))
        (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D)))))
⊢ ((Ideal.Quotient.mkₐ (↥(subalgebra R D))
                (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))).kerSquareLift.comp
          (Ideal.Quotient.liftₐ (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))
            ((Ideal.Quotient.mkₐ (↥(subalgebra R D))
                  (RingHom.ker
                      (Ideal.Quotient.mkₐ (↥(subalgebra R D))
                        (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))) ^
                    2)).comp
              (aeval p))
            ⋯)).comp
      (Ideal.Quotient.mkₐ (↥(subalgebra R D))
        (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))) =
    (AlgHom.id (↥(subalgebra R D)) (Presentation.ModelOfHasCoeffs ↥(subalgebra R D))).comp
      (Ideal.Quotient.mkₐ (↥(subalgebra R D))
        (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D)))))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -0 * Q y ^ 2 * 0 + Q x * P y ^ 2 * Q z - 2 * 0 * P y * Q y * Q z + 2 * Q x * P y * Q y * 0 -
                            W'.a₁ * 0 ^ 2 * Q y * Q z +
                          W'.a₁ * Q x ^ 2 * P y * 0 +
                        W'.a₂ * 0 ^ 2 * Q x * Q z -
                      W'.a₂ * 0 * Q x ^ 2 * 0 -
                    W'.a₃ * 0 * P y * Q z ^ 2 +
                  W'.a₃ * Q x * Q y * 0 ^ 2 -
                2 * W'.a₃ * 0 * Q y * 0 * Q z +
              2 * W'.a₃ * Q x * P y * 0 * Q z +
            W'.a₄ * 0 ^ 2 * Q z ^ 2 -
          W'.a₄ * Q x ^ 2 * 0 ^ 2 +
        3 * W'.a₆ * 0 * 0 * Q z ^ 2 -
      3 * W'.a₆ * Q x * 0 ^ 2 * Q z =
    P y ^ 2 * Q z * Q x

Tactic:
]

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -0 * Q y ^ 2 * 0 + Q x * P y ^ 2 * Q z - 2 * 0 * P y * Q y * Q z + 2 * Q x * P y * Q y * 0 -
                            W'.a₁ * 0 ^ 2 * Q y * Q z +
                          W'.a₁ * Q x ^ 2 * P y * 0 +
                        W'.a₂ * 0 ^ 2 * Q x * Q z -
                      W'.a₂ * 0 * Q x ^ 2 * 0 -
                    W'.a₃ * 0 * P y * Q z ^ 2 +
                  W'.a₃ * Q x * Q y * 0 ^ 2 -
                2 * W'.a₃ * 0 * Q y * 0 * Q z +
              2 * W'.a₃ * Q x * P y * 0 * Q z +
            W'.a₄ * 0 ^ 2 * Q z ^ 2 -
          W'.a₄ * Q x ^ 2 * 0 ^ 2 +
        3 * W'.a₆ * 0 * 0 * Q z ^ 2 -
      3 * W'.a₆ * Q x * 0 ^ 2 * Q z =
    P y ^ 2 * Q z * Q x
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
r : Unit
⊢ (cotangentCompLocalizationAwayEquiv D.gbar D.presLeft.toGenerators ⋯).symm (0, cMulXSubOneCotangent S D.gbar) =
    Extension.Cotangent.mk ⟨D.pres.relation (Sum.inl r), ⋯⟩

Tactic:
]

Goal state after:
case inl
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
r : Unit
⊢ (cotangentCompLocalizationAwayEquiv D.gbar D.presLeft.toGenerators ⋯).symm (0, cMulXSubOneCotangent S D.gbar) =
    Extension.Cotangent.mk ⟨D.pres.relation (Sum.inl r), ⋯⟩
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: case refine_2.refine_1
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
hf₀ :
  Function.Surjective
    ⇑(Ideal.Quotient.mkₐ (↥(subalgebra R D))
        (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D)))))
i : D.vars
hinj : Function.Injective ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
t : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))
ht : (MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))) t = D.q i
⊢ (D.q i).IsHomogeneous 1

Tactic:
]

Goal state after:
case refine_2.refine_1
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
hf₀ :
  Function.Surjective
    ⇑(Ideal.Quotient.mkₐ (↥(subalgebra R D))
        (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D)))))
i : D.vars
hinj : Function.Injective ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
t : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))
ht : (MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))) t = D.q i
⊢ (D.q i).IsHomogeneous 1
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
r : σ
⊢ Extension.Cotangent.mk
      ⟨((localizationAway S D.gbar).toComp D.presLeft.toGenerators).toExtensionHom.toAlgHom ↑(D.kerGen r), ⋯⟩ =
    Extension.Cotangent.mk ⟨D.pres.relation (Sum.inr r), ⋯⟩

Tactic:
]

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
r : σ
⊢ Extension.Cotangent.mk
      ⟨((localizationAway S D.gbar).toComp D.presLeft.toGenerators).toExtensionHom.toAlgHom ↑(D.kerGen r), ⋯⟩ =
    Extension.Cotangent.mk ⟨D.pres.relation (Sum.inr r), ⋯⟩
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -P x * Q y ^ 2 * P z + 0 * P y ^ 2 * 0 - 2 * P x * P y * Q y * 0 + 2 * 0 * P y * Q y * P z -
                            W'.a₁ * P x ^ 2 * Q y * 0 +
                          W'.a₁ * 0 ^ 2 * P y * P z +
                        W'.a₂ * P x ^ 2 * 0 * 0 -
                      W'.a₂ * P x * 0 ^ 2 * P z -
                    W'.a₃ * P x * P y * 0 ^ 2 +
                  W'.a₃ * 0 * Q y * P z ^ 2 -
                2 * W'.a₃ * P x * Q y * P z * 0 +
              2 * W'.a₃ * 0 * P y * P z * 0 +
            W'.a₄ * P x ^ 2 * 0 ^ 2 -
          W'.a₄ * 0 ^ 2 * P z ^ 2 +
        3 * W'.a₆ * P x * P z * 0 ^ 2 -
      3 * W'.a₆ * 0 * P z ^ 2 * 0 =
    -(Q y ^ 2 * P z) * P x

Tactic:
]

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -P x * Q y ^ 2 * P z + 0 * P y ^ 2 * 0 - 2 * P x * P y * Q y * 0 + 2 * 0 * P y * Q y * P z -
                            W'.a₁ * P x ^ 2 * Q y * 0 +
                          W'.a₁ * 0 ^ 2 * P y * P z +
                        W'.a₂ * P x ^ 2 * 0 * 0 -
                      W'.a₂ * P x * 0 ^ 2 * P z -
                    W'.a₃ * P x * P y * 0 ^ 2 +
                  W'.a₃ * 0 * Q y * P z ^ 2 -
                2 * W'.a₃ * P x * Q y * P z * 0 +
              2 * W'.a₃ * 0 * P y * P z * 0 +
            W'.a₄ * P x ^ 2 * 0 ^ 2 -
          W'.a₄ * 0 ^ 2 * P z ^ 2 +
        3 * W'.a₆ * P x * P z * 0 ^ 2 -
      3 * W'.a₆ * 0 * P z ^ 2 * 0 =
    -(Q y ^ 2 * P z) * P x
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: n : ℕ
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsStandardSmoothOfRelativeDimension n R S
this✝¹ : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w✝¹ : _root_.Finite σ
w✝ : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e✝ : P.dimension = n
e₀ : σ ⊕ Fin n ≃ ι :=
  ((Equiv.ofInjective P.map ⋯).sumCongr (Finite.equivFinOfCardEq ⋯).symm).trans (Equiv.Set.sumCompl (Set.range P.map))
e : MvPolynomial σ (MvPolynomial (Fin n) R) ≃ₐ[R] P.Ring :=
  (MvPolynomial.sumAlgEquiv R σ (Fin n)).symm.trans (MvPolynomial.renameEquiv R e₀)
φ : MvPolynomial (Fin n) R →ₐ[R] P.Ring :=
  (↑e).comp (IsScalarTower.toAlgHom R (MvPolynomial (Fin n) R) (MvPolynomial σ (MvPolynomial (Fin n) R)))
algInst✝¹ : Algebra (MvPolynomial (Fin n) R) P.Ring := φ.toAlgebra
algInst✝ : Algebra (MvPolynomial (Fin n) R) S := ((algebraMap P.Ring S).comp φ.toRingHom).toAlgebra
scalarTowerInst✝ : IsScalarTower (MvPolynomial (Fin n) R) P.Ring S :=
  IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap (MvPolynomial (Fin n) R) S))
this✝ : IsScalarTower R (MvPolynomial (Fin n) R) P.Ring
this : IsScalarTower R (MvPolynomial (Fin n) R) S
H :
  (MvPolynomial.aeval fun x ↦ (algebraMap P.Ring S) (e (MvPolynomial.X x))).toRingHom =
    (algebraMap P.Ring S).comp e.toRingEquiv.toRingHom
⊢ Ideal.comap e.toRingEquiv P.ker =
    (Algebra.Generators.ofSurjective (fun x ↦ (algebraMap P.Ring S) (e (MvPolynomial.X x))) ⋯).ker

Tactic:
]

Goal state after:
n : ℕ
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsStandardSmoothOfRelativeDimension n R S
this✝¹ : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w✝¹ : _root_.Finite σ
w✝ : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e✝ : P.dimension = n
e₀ : σ ⊕ Fin n ≃ ι :=
  ((Equiv.ofInjective P.map ⋯).sumCongr (Finite.equivFinOfCardEq ⋯).symm).trans (Equiv.Set.sumCompl (Set.range P.map))
e : MvPolynomial σ (MvPolynomial (Fin n) R) ≃ₐ[R] P.Ring :=
  (MvPolynomial.sumAlgEquiv R σ (Fin n)).symm.trans (MvPolynomial.renameEquiv R e₀)
φ : MvPolynomial (Fin n) R →ₐ[R] P.Ring :=
  (↑e).comp (IsScalarTower.toAlgHom R (MvPolynomial (Fin n) R) (MvPolynomial σ (MvPolynomial (Fin n) R)))
algInst✝¹ : Algebra (MvPolynomial (Fin n) R) P.Ring := φ.toAlgebra
algInst✝ : Algebra (MvPolynomial (Fin n) R) S := ((algebraMap P.Ring S).comp φ.toRingHom).toAlgebra
scalarTowerInst✝ : IsScalarTower (MvPolynomial (Fin n) R) P.Ring S :=
  IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap (MvPolynomial (Fin n) R) S))
this✝ : IsScalarTower R (MvPolynomial (Fin n) R) P.Ring
this : IsScalarTower R (MvPolynomial (Fin n) R) S
H :
  (MvPolynomial.aeval fun x ↦ (algebraMap P.Ring S) (e (MvPolynomial.X x))).toRingHom =
    (algebraMap P.Ring S).comp e.toRingEquiv.toRingHom
⊢ Ideal.comap e.toRingEquiv P.ker =
    (Algebra.Generators.ofSurjective (fun x ↦ (algebraMap P.Ring S) (e (MvPolynomial.X x))) ⋯).ker
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ ((P y * Q z - Q y * P z) ^ 2 * P z * Q z + W'.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (Q x * P z - Q x * P z) -
            W'.a₂ * P z * Q z * (Q x * P z - Q x * P z) ^ 2 -
          Q x * P z * (Q x * P z - Q x * P z) ^ 2 -
        Q x * P z * (Q x * P z - Q x * P z) ^ 2) *
      (Q x * P z - Q x * P z) =
    0

Tactic:
]

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ ((P y * Q z - Q y * P z) ^ 2 * P z * Q z + W'.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (Q x * P z - Q x * P z) -
            W'.a₂ * P z * Q z * (Q x * P z - Q x * P z) ^ 2 -
          Q x * P z * (Q x * P z - Q x * P z) ^ 2 -
        Q x * P z * (Q x * P z - Q x * P z) ^ 2) *
      (Q x * P z - Q x * P z) =
    0
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝ : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
h✝ : Nontrivial S
f : P.toExtension.Cotangent → ↥P.toExtension.ker
hf : ∀ (b : P.toExtension.Cotangent), Extension.Cotangent.mk (f b) = b
v : σ → ↥P.ker := fun i ↦ f (b₀ i)
J : Ideal P.Ring := Ideal.span (Set.range (Subtype.val ∘ v))
⊢ (RingHom.ker (aeval P.val)).FG

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝ : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
h✝ : Nontrivial S
f : P.toExtension.Cotangent → ↥P.toExtension.ker
hf : ∀ (b : P.toExtension.Cotangent), Extension.Cotangent.mk (f b) = b
v : σ → ↥P.ker := fun i ↦ f (b₀ i)
J : Ideal P.Ring := Ideal.span (Set.range (Subtype.val ∘ v))
⊢ (RingHom.ker (aeval P.val)).FG
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ≠ Q x * P z
⊢ ((P y * Q z - Q y * P z) ^ 2 * P z * Q z + W.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (P x * Q z - Q x * P z) -
                W.a₂ * P z * Q z * (P x * Q z - Q x * P z) ^ 2 -
              P x * Q z * (P x * Q z - Q x * P z) ^ 2 -
            Q x * P z * (P x * Q z - Q x * P z) ^ 2) *
          (P x * Q z - Q x * P z) /
        (P z * Q z) ^ 2 /
      ((P x * Q z - Q x * P z) ^ 3 / (P z * Q z)) =
    ((P y * Q z - Q y * P z) ^ 2 * P z * Q z + W.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (P x * Q z - Q x * P z) -
                W.a₂ * P z * Q z * (P x * Q z - Q x * P z) ^ 2 -
              P x * Q z * (P x * Q z - Q x * P z) ^ 2 -
            Q x * P z * (P x * Q z - Q x * P z) ^ 2) *
          (P x * Q z - Q x * P z) /
        (P z * Q z) ^ 2 /
      ((P x * Q z - Q x * P z) ^ 3 / (P z * Q z))

Tactic:
]

Goal state after: