mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Extension.Presentation.Core

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Presentation R S ι σ
R₀ : Type u_5
inst✝⁴ : CommRing R₀
inst✝³ : Algebra R₀ R
inst✝² : Algebra R₀ S
inst✝¹ : IsScalarTower R₀ R S
inst✝ : P.HasCoeffs R₀
h : Function.Surjective ⇑((↑(AlgEquiv.restrictScalars R P.quotientEquiv)).comp (Ideal.Quotient.mkₐ R P.ker))
⊢ (P.tensorModelOfHasCoeffsHom R₀).comp
      ((Ideal.Quotient.liftₐ P.ker
            ((TensorProduct.map (AlgHom.id R R)
                  (Ideal.Quotient.mkₐ R₀ (Ideal.span (Set.range (relationOfHasCoeffs R₀))))).comp
              ↑(MvPolynomial.algebraTensorAlgEquiv R₀ R).symm)
            ⋯).comp
        (Ideal.Quotient.mkₐ R P.ker)) =
    (↑(AlgEquiv.restrictScalars R P.quotientEquiv)).comp (Ideal.Quotient.mkₐ R P.ker)

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Presentation R S ι σ
R₀ : Type u_5
inst✝⁴ : CommRing R₀
inst✝³ : Algebra R₀ R
inst✝² : Algebra R₀ S
inst✝¹ : IsScalarTower R₀ R S
inst✝ : P.HasCoeffs R₀
h : Function.Surjective ⇑((↑(AlgEquiv.restrictScalars R P.quotientEquiv)).comp (Ideal.Quotient.mkₐ R P.ker))
⊢ (P.tensorModelOfHasCoeffsHom R₀).comp
      ((Ideal.Quotient.liftₐ P.ker
            ((TensorProduct.map (AlgHom.id R R)
                  (Ideal.Quotient.mkₐ R₀ (Ideal.span (Set.range (relationOfHasCoeffs R₀))))).comp
              ↑(MvPolynomial.algebraTensorAlgEquiv R₀ R).symm)
            ⋯).comp
        (Ideal.Quotient.mkₐ R P.ker)) =
    (↑(AlgEquiv.restrictScalars R P.quotientEquiv)).comp (Ideal.Quotient.mkₐ R P.ker)
Module: Mathlib.RingTheory.Extension.Presentation.Core

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Finite σ
P : SubmersivePresentation R S ι σ
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
H : ∃ c, ∑ i, c i * P.relation i = P.jacobiMatrix.det * P.σ ↑⋯.unit⁻¹ - 1
⊢ ∃ v, ∑ i, v i * P.relation i = P.jacobiMatrix.det * P.σ ↑⋯.unit⁻¹ - 1

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Finite σ
P : SubmersivePresentation R S ι σ
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
H : ∃ c, ∑ i, c i * P.relation i = P.jacobiMatrix.det * P.σ ↑⋯.unit⁻¹ - 1
⊢ ∃ v, ∑ i, v i * P.relation i = P.jacobiMatrix.det * P.σ ↑⋯.unit⁻¹ - 1
Module: Mathlib.RingTheory.Extension.Presentation.Core

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : Finite σ
P : SubmersivePresentation R S ι σ
R₀ : Type u_5
inst✝⁶ : CommRing R₀
inst✝⁵ : Algebra R₀ R
inst✝⁴ : Algebra R₀ S
inst✝³ : IsScalarTower R₀ R S
inst✝² : P.HasCoeffs R₀
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
⊢ ((MvPolynomial.map (algebraMap R₀ R)).mapMatrix (P.ofHasCoeffs R₀).jacobiMatrix).det = P.jacobiMatrix.det

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : Finite σ
P : SubmersivePresentation R S ι σ
R₀ : Type u_5
inst✝⁶ : CommRing R₀
inst✝⁵ : Algebra R₀ R
inst✝⁴ : Algebra R₀ S
inst✝³ : IsScalarTower R₀ R S
inst✝² : P.HasCoeffs R₀
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
⊢ ((MvPolynomial.map (algebraMap R₀ R)).mapMatrix (P.ofHasCoeffs R₀).jacobiMatrix).det = P.jacobiMatrix.det
Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : PreSubmersivePresentation R S ι σ
x : ↥P.ker
⊢ (∀ (x_1 : σ), P.cotangentComplexAux (Cotangent.mk x) x_1 = 0 x_1) ↔
    ∀ (i : σ), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : PreSubmersivePresentation R S ι σ
x : ↥P.ker
⊢ (∀ (x_1 : σ), P.cotangentComplexAux (Cotangent.mk x) x_1 = 0 x_1) ↔
    ∀ (i : σ), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
Module: Mathlib.RingTheory.Extension.Presentation.Core

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Finite σ
P : SubmersivePresentation R S ι σ
R₀ : Type u_5
inst✝⁴ : CommRing R₀
inst✝³ : Algebra R₀ R
inst✝² : Algebra R₀ S
inst✝¹ : IsScalarTower R₀ R S
inst✝ : P.HasCoeffs R₀
this : Fintype σ := Fintype.ofFinite σ
⊢ (MvPolynomial.aeval P.val) P.jacobiMatrix.det = (MvPolynomial.aeval P.val) P.jacobiMatrix.det

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
⊢ P.cotangentComplexAux.ker ≤ ⊥

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
⊢ P.cotangentComplexAux.ker ≤ ⊥
Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx : Cotangent.mk x ∈ P.cotangentComplexAux.ker
⊢ ↑x ∈ P.toExtension.ker ^ 2

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx : Cotangent.mk x ∈ P.cotangentComplexAux.ker
⊢ ↑x ∈ P.toExtension.ker ^ 2
Module: Mathlib.RingTheory.Extension.Presentation.Core

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P✝ : Presentation R S ι σ
inst✝⁶ : Finite σ
P : SubmersivePresentation R S ι σ
R₀ : Type u_5
inst✝⁵ : CommRing R₀
inst✝⁴ : Algebra R₀ R
inst✝³ : Algebra R₀ S
inst✝² : IsScalarTower R₀ R S
inst✝¹ : P.HasCoeffs R₀
inst✝ : FaithfulSMul R₀ R
this✝ : Fintype σ := Fintype.ofFinite σ
this :
  (Ideal.Quotient.mk (Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀)))) (P.jacobianOfHasCoeffs R₀) *
      (Ideal.Quotient.mk (Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀)))) (P.invJacobianOfHasCoeffs R₀) =
    1
⊢ (algebraMap (P.ofHasCoeffs R₀).Ring (Presentation.ModelOfHasCoeffs R₀)) (P.ofHasCoeffs R₀).jacobiMatrix.det =
    (Ideal.Quotient.mk (Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀)))) (P.jacobianOfHasCoeffs R₀)

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P✝ : Presentation R S ι σ
inst✝⁶ : Finite σ
P : SubmersivePresentation R S ι σ
R₀ : Type u_5
inst✝⁵ : CommRing R₀
inst✝⁴ : Algebra R₀ R
inst✝³ : Algebra R₀ S
inst✝² : IsScalarTower R₀ R S
inst✝¹ : P.HasCoeffs R₀
inst✝ : FaithfulSMul R₀ R
this✝ : Fintype σ := Fintype.ofFinite σ
this :
  (Ideal.Quotient.mk (Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀)))) (P.jacobianOfHasCoeffs R₀) *
      (Ideal.Quotient.mk (Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀)))) (P.invJacobianOfHasCoeffs R₀) =
    1
⊢ (algebraMap (P.ofHasCoeffs R₀).Ring (Presentation.ModelOfHasCoeffs R₀)) (P.ofHasCoeffs R₀).jacobiMatrix.det =
    (Ideal.Quotient.mk (Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀)))) (P.jacobianOfHasCoeffs R₀)
Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx : ∀ (i : σ), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
⊢ ↑x ∈ P.toExtension.ker ^ 2

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx : ∀ (i : σ), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
⊢ ↑x ∈ P.toExtension.ker ^ 2
Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx : ∀ (i : σ), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
⊢ ↑x ∈ P.ker

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx : ∀ (i : σ), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
⊢ ↑x ∈ P.ker
Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx : ∀ (i : σ), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
this : ↑x ∈ Ideal.span (Set.range P.relation)
c : σ →₀ P.Ring
hc : (c.sum fun i a ↦ a * P.relation i) = ↑x
i : σ
⊢ (aeval P.val) ((pderiv (P.map i)) ↑x) = 0

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx : ∀ (i : σ), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
this : ↑x ∈ Ideal.span (Set.range P.relation)
c : σ →₀ P.Ring
hc : (c.sum fun i a ↦ a * P.relation i) = ↑x
i : σ
⊢ (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx : ∀ (i : σ), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
this✝ : ↑x ∈ Ideal.span (Set.range P.relation)
c : σ →₀ P.Ring
hc : (c.sum fun i a ↦ a * P.relation i) = ↑x
heq : ∀ (i : σ), ∑ x ∈ c.support, (aeval P.val) (c x) * (aeval P.val) ((pderiv (P.map i)) (P.relation x)) = 0
heq2 : (∑ i ∈ c.support, (aeval P.val) (c i) • fun j ↦ (aeval P.val) ((pderiv (P.map j)) (P.relation i))) = 0
i : σ
this :
  ∀ (s : Finset σ) (g : σ → S),
    (∀ i ∉ s, g i = 0) →
      (∑ i ∈ s, g i • fun j ↦ (aeval P.val) ((pderiv (P.map j)) (P.relation i))) = 0 → ∀ (i : σ), g i = 0
⊢ (aeval P.val) (c i) = 0

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx : ∀ (i : σ), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
this✝ : ↑x ∈ Ideal.span (Set.range P.relation)
c : σ →₀ P.Ring
hc : (c.sum fun i a ↦ a * P.relation i) = ↑x
heq : ∀ (i : σ), ∑ x ∈ c.support, (aeval P.val) (c x) * (aeval P.val) ((pderiv (P.map i)) (P.relation x)) = 0
heq2 : (∑ i ∈ c.support, (aeval P.val) (c i) • fun j ↦ (aeval P.val) ((pderiv (P.map j)) (P.relation i))) = 0
i : σ
this :
  ∀ (s : Finset σ) (g : σ → S),
    (∀ i ∉ s, g i = 0) →
      (∑ i ∈ s, g i • fun j ↦ (aeval P.val) ((pderiv (P.map j)) (P.relation i))) = 0 → ∀ (i : σ), g i = 0
⊢ (aeval P.val) (c i) = 0
Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx : ∀ (i : σ), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
this✝ : ↑x ∈ Ideal.span (Set.range P.relation)
c : σ →₀ P.Ring
hc : (c.sum fun i a ↦ a * P.relation i) = ↑x
heq : ∀ (i : σ), ∑ x ∈ c.support, (aeval P.val) (c x) * (aeval P.val) ((pderiv (P.map i)) (P.relation x)) = 0
heq2 : (∑ i ∈ c.support, (aeval P.val) (c i) • fun j ↦ (aeval P.val) ((pderiv (P.map j)) (P.relation i))) = 0
this : ∀ (i : σ), (aeval P.val) (c i) = 0
⊢ (c.sum fun i a ↦ a * P.relation i) ∈ P.ker ^ 2

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx : ∀ (i : σ), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
this✝ : ↑x ∈ Ideal.span (Set.range P.relation)
c : σ →₀ P.Ring
hc : (c.sum fun i a ↦ a * P.relation i) = ↑x
heq : ∀ (i : σ), ∑ x ∈ c.support, (aeval P.val) (c x) * (aeval P.val) ((pderiv (P.map i)) (P.relation x)) = 0
heq2 : (∑ i ∈ c.support, (aeval P.val) (c i) • fun j ↦ (aeval P.val) ((pderiv (P.map j)) (P.relation i))) = 0
this : ∀ (i : σ), (aeval P.val) (c i) = 0
⊢ (c.sum fun i a ↦ a * P.relation i) ∈ P.ker ^ 2
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
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ -(eval P) W'.polynomialX *
        ((eval P) W'.polynomialX ^ 2 - W'.a₁ * (eval P) W'.polynomialX * P z * (W'.negY P - W'.negY P) -
              W'.a₂ * P z ^ 2 * (W'.negY P - W'.negY P) ^ 2 -
            2 * P x * P z * (W'.negY P - W'.negY P) ^ 2 -
          P x * P z * (W'.negY P - W'.negY P) ^ 2) +
      W'.negY P * P z ^ 2 * (W'.negY P - W'.negY P) ^ 3 =
    -(eval P) W'.polynomialX ^ 3

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
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ -(eval P) W'.polynomialX *
        ((eval P) W'.polynomialX ^ 2 - W'.a₁ * (eval P) W'.polynomialX * P z * (W'.negY P - W'.negY P) -
              W'.a₂ * P z ^ 2 * (W'.negY P - W'.negY P) ^ 2 -
            2 * P x * P z * (W'.negY P - W'.negY P) ^ 2 -
          P x * P z * (W'.negY P - W'.negY P) ^ 2) +
      W'.negY P * P z ^ 2 * (W'.negY P - W'.negY P) ^ 3 =
    -(eval P) W'.polynomialX ^ 3
Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx : ∀ (i : σ), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
this✝ : ↑x ∈ Ideal.span (Set.range P.relation)
c : σ →₀ P.Ring
hc : (c.sum fun i a ↦ a * P.relation i) = ↑x
heq : ∀ (i : σ), ∑ x ∈ c.support, (aeval P.val) (c x) * (aeval P.val) ((pderiv (P.map i)) (P.relation x)) = 0
heq2 : (∑ i ∈ c.support, (aeval P.val) (c i) • fun j ↦ (aeval P.val) ((pderiv (P.map j)) (P.relation i))) = 0
this : ∀ (i : σ), (aeval P.val) (c i) = 0
i : σ
hi : i ∈ c.support
⊢ (fun i a ↦ a * P.relation i) i (c i) ∈ P.ker * P.ker

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx : ∀ (i : σ), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
this✝ : ↑x ∈ Ideal.span (Set.range P.relation)
c : σ →₀ P.Ring
hc : (c.sum fun i a ↦ a * P.relation i) = ↑x
heq : ∀ (i : σ), ∑ x ∈ c.support, (aeval P.val) (c x) * (aeval P.val) ((pderiv (P.map i)) (P.relation x)) = 0
heq2 : (∑ i ∈ c.support, (aeval P.val) (c i) • fun j ↦ (aeval P.val) ((pderiv (P.map j)) (P.relation i))) = 0
this : ∀ (i : σ), (aeval P.val) (c i) = 0
i : σ
hi : i ∈ c.support
⊢ (fun i a ↦ a * P.relation i) i (c i) ∈ P.ker * P.ker
Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent

Goal state before:
pp: case hr
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx : ∀ (i : σ), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
this✝ : ↑x ∈ Ideal.span (Set.range P.relation)
c : σ →₀ P.Ring
hc : (c.sum fun i a ↦ a * P.relation i) = ↑x
heq : ∀ (i : σ), ∑ x ∈ c.support, (aeval P.val) (c x) * (aeval P.val) ((pderiv (P.map i)) (P.relation x)) = 0
heq2 : (∑ i ∈ c.support, (aeval P.val) (c i) • fun j ↦ (aeval P.val) ((pderiv (P.map j)) (P.relation i))) = 0
this : ∀ (i : σ), (aeval P.val) (c i) = 0
i : σ
hi : i ∈ c.support
⊢ c i ∈ RingHom.ker (aeval P.val)

Tactic:
]

Goal state after:
case hr
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx : ∀ (i : σ), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
this✝ : ↑x ∈ Ideal.span (Set.range P.relation)
c : σ →₀ P.Ring
hc : (c.sum fun i a ↦ a * P.relation i) = ↑x
heq : ∀ (i : σ), ∑ x ∈ c.support, (aeval P.val) (c x) * (aeval P.val) ((pderiv (P.map i)) (P.relation x)) = 0
heq2 : (∑ i ∈ c.support, (aeval P.val) (c i) • fun j ↦ (aeval P.val) ((pderiv (P.map j)) (P.relation i))) = 0
this : ∀ (i : σ), (aeval P.val) (c i) = 0
i : σ
hi : i ∈ c.support
⊢ c i ∈ RingHom.ker (aeval P.val)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W.negY Q * P z
⊢ W.negDblY P = W.negDblY P

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
⊢ Set.range ⇑P.basisDeriv ⊆ ↑P.cotangentComplexAux.range

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
⊢ Set.range ⇑P.basisDeriv ⊆ ↑P.cotangentComplexAux.range
Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
i j : σ
⊢ (aeval P.val) ((pderiv (P.map j)) ↑⟨P.relation i, ⋯⟩) = P.basisDeriv i j

Tactic:
]

Goal state after:
case h
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
i j : σ
⊢ (aeval P.val) ((pderiv (P.map j)) ↑⟨P.relation i, ⋯⟩) = P.basisDeriv i j
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
⊢ -n / P z / d *
        ((n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * P z * d ^ 2) * d / P z / (P z * d ^ 3) -
          P x / P z) +
      P y / P z =
    (-n * (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * P z * d ^ 2 - P x * P z * d ^ 2) +
          P y * P z ^ 2 * d ^ 3) /
        P z ^ 2 /
      (P z * d ^ 3)

Tactic:
]

Goal state after:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
⊢ -n / P z / d *
        ((n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * P z * d ^ 2) * d / P z / (P z * d ^ 3) -
          P x / P z) +
      P y / P z =
    (-n * (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * P z * d ^ 2 - P x * P z * d ^ 2) +
          P y * P z ^ 2 * d ^ 3) /
        P z ^ 2 /
      (P z * d ^ 3)
Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
⊢ Function.Injective ⇑P.toExtension.cotangentComplex

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
⊢ Function.Injective ⇑P.toExtension.cotangentComplex
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
⊢ W.toAffine.negAddY (P x / P z) (P x / P z) (P y / P z) (-n / P z / d) =
    (-n * (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * P z * d ^ 2 - P x * P z * d ^ 2) +
          P y * P z ^ 2 * d ^ 3) /
        P z ^ 2 /
      (P z * d ^ 3)

Tactic:
by
  rw [Affine.negAddY, toAffine_addX_of_eq hPz hd]
  simp [field]

Goal state after:
Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
x : P.toExtension.CotangentSpace
y : P.toExtension.Cotangent
⊢ (∀ (x_1 : σ),
      (Finsupp.linearEquivFunOnFinite S S σ) ((Finsupp.lcomapDomain P.map ⋯) (P.cotangentSpaceBasis.repr x)) x_1 =
        P.cotangentEquiv y x_1) ↔
    ∀ (i : σ), (P.cotangentSpaceBasis.repr x) (P.map i) = P.cotangentComplexAux y i

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
x : P.toExtension.CotangentSpace
y : P.toExtension.Cotangent
⊢ (∀ (x_1 : σ),
      (Finsupp.linearEquivFunOnFinite S S σ) ((Finsupp.lcomapDomain P.map ⋯) (P.cotangentSpaceBasis.repr x)) x_1 =
        P.cotangentEquiv y x_1) ↔
    ∀ (i : σ), (P.cotangentSpaceBasis.repr x) (P.map i) = P.cotangentComplexAux y i
Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
x✝ : P.toExtension.Cotangent
⊢ ∀ (i : σ), (P.cotangentSpaceBasis.repr (P.toExtension.cotangentComplex x✝)) (P.map i) = P.cotangentComplexAux x✝ i

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
x✝ : P.toExtension.Cotangent
⊢ ∀ (i : σ), (P.cotangentSpaceBasis.repr (P.toExtension.cotangentComplex x✝)) (P.map i) = P.cotangentComplexAux x✝ i
Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
i : ι
hi : ¬∀ (i_1 : σ), (P.cotangentSpaceBasis.repr (P.cotangentSpaceBasis i)) (P.map i_1) = P.cotangentComplexAux 0 i_1
⊢ i ∈ Set.range P.map

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
i : ι
hi : ¬∀ (i_1 : σ), (P.cotangentSpaceBasis.repr (P.cotangentSpaceBasis i)) (P.map i_1) = P.cotangentComplexAux 0 i_1
⊢ i ∈ Set.range P.map