mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hPz : P z = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
hsple :
  ∀ {x : ((localizationAway T g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
⊢ ∀ r ∈ Ideal.map ((localizationAway T g).toComp P).toAlgHom P.ker,
    ∀ s ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1},
      r * s ∈ RingHom.ker (compLocalizationAwayAlgHom T g P)

Tactic:
]

Goal state after:
case a
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
hsple :
  ∀ {x : ((localizationAway T g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
⊢ ∀ r ∈ Ideal.map ((localizationAway T g).toComp P).toAlgHom P.ker,
    ∀ s ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1},
      r * s ∈ RingHom.ker (compLocalizationAwayAlgHom T g P)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hQz : Q z = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Etale R S
a✝ : Nontrivial S
⊢ Subsingleton (H1Cotangent R S) ∧ ∃ I b, Set.range ⇑b ⊆ Set.range ⇑(D R S)

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Etale R S
a✝ : Nontrivial S
⊢ Subsingleton (H1Cotangent R S) ∧ ∃ I b, Set.range ⇑b ⊆ Set.range ⇑(D R S)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

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

Tactic:
]

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

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
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
this :
  ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
    [FinitePresentation R S] (p : Ideal S) [inst_4 : p.IsPrime] [IsSmoothAt R p],
    Smooth R S → ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)
h : ¬Smooth R S
g : S
hg : g ∉ p
hsm : Smooth R (Localization.Away g)
⊢ g ∉ p

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
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
this :
  ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
    [FinitePresentation R S] (p : Ideal S) [inst_4 : p.IsPrime] [IsSmoothAt R p],
    Smooth R S → ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)
h : ¬Smooth R S
g : S
hg : g ∉ p
hsm : Smooth R (Localization.Away g)
⊢ g ∉ p
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: case a.a
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
hsple :
  ∀ {x : ((localizationAway T g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
⊢ ∀ r ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1},
    ∀ s ∈ Ideal.map ((localizationAway T g).toComp P).toAlgHom P.ker,
      r * s ∈ RingHom.ker (compLocalizationAwayAlgHom T g P)

Tactic:
]

Goal state after:
case a.a
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
hsple :
  ∀ {x : ((localizationAway T g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
⊢ ∀ r ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1},
    ∀ s ∈ Ideal.map ((localizationAway T g).toComp P).toAlgHom P.ker,
      r * s ∈ RingHom.ker (compLocalizationAwayAlgHom T g P)
Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FinitePresentation R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
this✝ :
  ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
    [FinitePresentation R S] (p : Ideal S) [inst_4 : p.IsPrime] [IsSmoothAt R p],
    Smooth R S → ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)
h : ¬Smooth R S
g : S
hg : g ∉ p
hsm : Smooth R (Localization.Away g)
x✝ : (Ideal.map (algebraMap S (Localization.Away g)) p).IsPrime
g' : Localization.Away g
hg' : g' ∉ Ideal.map (algebraMap S (Localization.Away g)) p
hstd : IsStandardSmooth R (Localization.Away g')
this : IsLocalization.Away (g * (IsLocalization.Away.sec g g').1) (Localization.Away g')
e : Localization.Away (g * (IsLocalization.Away.sec g g').1) ≃ₐ[S] Localization.Away g' :=
  Localization.algEquiv (Submonoid.powers (g * (IsLocalization.Away.sec g g').1)) (Localization.Away g')
⊢ g * (IsLocalization.Away.sec g g').1 ∉ p

Tactic:
refine Ideal.IsPrime.mul_notMem ‹_› hg fun hmem ↦ hg' ?_

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FinitePresentation R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
this✝ :
  ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
    [FinitePresentation R S] (p : Ideal S) [inst_4 : p.IsPrime] [IsSmoothAt R p],
    Smooth R S → ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)
h : ¬Smooth R S
g : S
hg : g ∉ p
hsm : Smooth R (Localization.Away g)
x✝ : (Ideal.map (algebraMap S (Localization.Away g)) p).IsPrime
g' : Localization.Away g
hg' : g' ∉ Ideal.map (algebraMap S (Localization.Away g)) p
hstd : IsStandardSmooth R (Localization.Away g')
this : IsLocalization.Away (g * (IsLocalization.Away.sec g g').1) (Localization.Away g')
e : Localization.Away (g * (IsLocalization.Away.sec g g').1) ≃ₐ[S] Localization.Away g' :=
  Localization.algEquiv (Submonoid.powers (g * (IsLocalization.Away.sec g g').1)) (Localization.Away g')
hmem : (IsLocalization.Away.sec g g').1 ∈ p
⊢ g' ∈ Ideal.map (algebraMap S (Localization.Away g)) p
Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FinitePresentation R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
this✝ :
  ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
    [FinitePresentation R S] (p : Ideal S) [inst_4 : p.IsPrime] [IsSmoothAt R p],
    Smooth R S → ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)
h : ¬Smooth R S
g : S
hg : g ∉ p
hsm : Smooth R (Localization.Away g)
x✝ : (Ideal.map (algebraMap S (Localization.Away g)) p).IsPrime
g' : Localization.Away g
hg' : g' ∉ Ideal.map (algebraMap S (Localization.Away g)) p
hstd : IsStandardSmooth R (Localization.Away g')
this : IsLocalization.Away (g * (IsLocalization.Away.sec g g').1) (Localization.Away g')
e : Localization.Away (g * (IsLocalization.Away.sec g g').1) ≃ₐ[S] Localization.Away g' :=
  Localization.algEquiv (Submonoid.powers (g * (IsLocalization.Away.sec g g').1)) (Localization.Away g')
hmem : (IsLocalization.Away.sec g g').1 ∈ p
⊢ (algebraMap S (Localization.Away g)) (IsLocalization.Away.sec g g').1 ∈
    Ideal.map (algebraMap S (Localization.Away g)) p

Tactic:
]

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FinitePresentation R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
this✝ :
  ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
    [FinitePresentation R S] (p : Ideal S) [inst_4 : p.IsPrime] [IsSmoothAt R p],
    Smooth R S → ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)
h : ¬Smooth R S
g : S
hg : g ∉ p
hsm : Smooth R (Localization.Away g)
x✝ : (Ideal.map (algebraMap S (Localization.Away g)) p).IsPrime
g' : Localization.Away g
hg' : g' ∉ Ideal.map (algebraMap S (Localization.Away g)) p
hstd : IsStandardSmooth R (Localization.Away g')
this : IsLocalization.Away (g * (IsLocalization.Away.sec g g').1) (Localization.Away g')
e : Localization.Away (g * (IsLocalization.Away.sec g g').1) ≃ₐ[S] Localization.Away g' :=
  Localization.algEquiv (Submonoid.powers (g * (IsLocalization.Away.sec g g').1)) (Localization.Away g')
hmem : (IsLocalization.Away.sec g g').1 ∈ p
⊢ (algebraMap S (Localization.Away g)) (IsLocalization.Away.sec g g').1 ∈
    Ideal.map (algebraMap S (Localization.Away g)) p
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
hsple :
  ∀ {x : ((localizationAway T g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
⊢ ∀ r ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1},
    ∀ s ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1},
      r * s ∈ RingHom.ker (compLocalizationAwayAlgHom T g P)

Tactic:
]

Goal state after:
case a
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
hsple :
  ∀ {x : ((localizationAway T g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
⊢ ∀ r ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1},
    ∀ s ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1},
      r * s ∈ RingHom.ker (compLocalizationAwayAlgHom T g P)
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
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
⊢ W.addZ P Q = W.addZ P Q

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
Q : Generators S T Unit := localizationAway T g
algInst✝ : Algebra P.Ring ((localizationAway T g).comp P).Ring := ((localizationAway T g).toComp P).toAlgHom.toAlgebra
f : P.Ring ⧸ P.ker ^ 2 := (Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)
π : ((localizationAway T g).comp P).Ring →ₐ[R] Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)) :=
  compLocalizationAwayAlgHom T g P
x : ↥P.toExtension.ker
hx :
  (lift
        (↑S
          (↑(LinearMap.ringLmapEquivSelf T T (P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent)).symm
            (Extension.Cotangent.map (Q.toComp P).toExtensionHom))))
      (((TensorProduct.mk S T P.toExtension.Cotangent) 1) (Extension.Cotangent.mk x)) =
    0
h : ∃ m, ↑m * (algebraMap P.Ring (P.Ring ⧸ P.ker ^ 2)) ↑x = 0
⊢ ((TensorProduct.mk S T P.toExtension.Cotangent) 1) (Extension.Cotangent.mk x) = 0

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
Q : Generators S T Unit := localizationAway T g
algInst✝ : Algebra P.Ring ((localizationAway T g).comp P).Ring := ((localizationAway T g).toComp P).toAlgHom.toAlgebra
f : P.Ring ⧸ P.ker ^ 2 := (Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)
π : ((localizationAway T g).comp P).Ring →ₐ[R] Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)) :=
  compLocalizationAwayAlgHom T g P
x : ↥P.toExtension.ker
hx :
  (lift
        (↑S
          (↑(LinearMap.ringLmapEquivSelf T T (P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent)).symm
            (Extension.Cotangent.map (Q.toComp P).toExtensionHom))))
      (((TensorProduct.mk S T P.toExtension.Cotangent) 1) (Extension.Cotangent.mk x)) =
    0
h : ∃ m, ↑m * (algebraMap P.Ring (P.Ring ⧸ P.ker ^ 2)) ↑x = 0
⊢ ((TensorProduct.mk S T P.toExtension.Cotangent) 1) (Extension.Cotangent.mk x) = 0
Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
inst✝⁸ : CommRing R✝
inst✝⁷ : CommRing S✝
inst✝⁶ : Algebra R✝ S✝
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FinitePresentation R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
h✝ : Smooth R S
κ : Type u_2
a : κ → S
b : Module.Basis κ (Localization.AtPrime p) Ω[Localization.AtPrime p⁄R]
hb : ∀ (i : κ), b i = (⇑(map R R S (Localization.AtPrime p)) ∘ ⇑(D R S)) (a i)
e : (κ →₀ S) →ₗ[S] Ω[S⁄R] := Finsupp.linearCombination S fun i ↦ (D R S) (a i)
l₁ : (κ →₀ S) →ₗ[S] κ →₀ Localization.AtPrime p :=
  Finsupp.mapRange.linearMap (Algebra.linearMap S (Localization.AtPrime p))
l₂ : Ω[S⁄R] →ₗ[S] Ω[Localization.AtPrime p⁄R] := map R R S (Localization.AtPrime p)
eₚ : (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R] :=
  (IsLocalizedModule.mapExtendScalars p.primeCompl l₁ l₂ (Localization.AtPrime p)) e
this✝ : eₚ = ↑b.repr.symm
heₚ : Function.Bijective ⇑eₚ
this : Finite κ
g : S
hg : g ∉ p
l₁ₜ : (κ →₀ S) →ₗ[S] κ →₀ Localization.Away g := Finsupp.mapRange.linearMap (Algebra.linearMap S (Localization.Away g))
l₂ₜ : Ω[S⁄R] →ₗ[S] Ω[Localization.Away g⁄R] := map R R S (Localization.Away g)
h : Function.Bijective ⇑((IsLocalizedModule.map (Submonoid.powers g) l₁ₜ l₂ₜ) e)
⊢ ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)

Tactic:
]

Goal state after:
R✝ : Type u_1
S✝ : Type u_2
inst✝⁸ : CommRing R✝
inst✝⁷ : CommRing S✝
inst✝⁶ : Algebra R✝ S✝
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FinitePresentation R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
h✝ : Smooth R S
κ : Type u_2
a : κ → S
b : Module.Basis κ (Localization.AtPrime p) Ω[Localization.AtPrime p⁄R]
hb : ∀ (i : κ), b i = (⇑(map R R S (Localization.AtPrime p)) ∘ ⇑(D R S)) (a i)
e : (κ →₀ S) →ₗ[S] Ω[S⁄R] := Finsupp.linearCombination S fun i ↦ (D R S) (a i)
l₁ : (κ →₀ S) →ₗ[S] κ →₀ Localization.AtPrime p :=
  Finsupp.mapRange.linearMap (Algebra.linearMap S (Localization.AtPrime p))
l₂ : Ω[S⁄R] →ₗ[S] Ω[Localization.AtPrime p⁄R] := map R R S (Localization.AtPrime p)
eₚ : (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R] :=
  (IsLocalizedModule.mapExtendScalars p.primeCompl l₁ l₂ (Localization.AtPrime p)) e
this✝ : eₚ = ↑b.repr.symm
heₚ : Function.Bijective ⇑eₚ
this : Finite κ
g : S
hg : g ∉ p
l₁ₜ : (κ →₀ S) →ₗ[S] κ →₀ Localization.Away g := Finsupp.mapRange.linearMap (Algebra.linearMap S (Localization.Away g))
l₂ₜ : Ω[S⁄R] →ₗ[S] Ω[Localization.Away g⁄R] := map R R S (Localization.Away g)
h : Function.Bijective ⇑((IsLocalizedModule.map (Submonoid.powers g) l₁ₜ l₂ₜ) e)
⊢ ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

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

Tactic:
]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
Q : Generators S T Unit := localizationAway T g
algInst✝ : Algebra P.Ring ((localizationAway T g).comp P).Ring := ((localizationAway T g).toComp P).toAlgHom.toAlgebra
f : P.Ring ⧸ P.ker ^ 2 := (Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)
π : ((localizationAway T g).comp P).Ring →ₐ[R] Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)) :=
  compLocalizationAwayAlgHom T g P
x : ↥P.toExtension.ker
hx :
  (lift
        (↑S
          (↑(LinearMap.ringLmapEquivSelf T T (P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent)).symm
            (Extension.Cotangent.map (Q.toComp P).toExtensionHom))))
      (((TensorProduct.mk S T P.toExtension.Cotangent) 1) (Extension.Cotangent.mk x)) =
    0
n : ℕ
hm : ↑⟨(fun x ↦ f ^ x) n, ⋯⟩ * (algebraMap P.Ring (P.Ring ⧸ P.ker ^ 2)) ↑x = 0
⊢ ∃ s', s' • Extension.Cotangent.mk x = 0

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
Q : Generators S T Unit := localizationAway T g
algInst✝ : Algebra P.Ring ((localizationAway T g).comp P).Ring := ((localizationAway T g).toComp P).toAlgHom.toAlgebra
f : P.Ring ⧸ P.ker ^ 2 := (Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)
π : ((localizationAway T g).comp P).Ring →ₐ[R] Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)) :=
  compLocalizationAwayAlgHom T g P
x : ↥P.toExtension.ker
hx :
  (lift
        (↑S
          (↑(LinearMap.ringLmapEquivSelf T T (P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent)).symm
            (Extension.Cotangent.map (Q.toComp P).toExtensionHom))))
      (((TensorProduct.mk S T P.toExtension.Cotangent) 1) (Extension.Cotangent.mk x)) =
    0
n : ℕ
hm : ↑⟨(fun x ↦ f ^ x) n, ⋯⟩ * (algebraMap P.Ring (P.Ring ⧸ P.ker ^ 2)) ↑x = 0
⊢ ∃ s', s' • Extension.Cotangent.mk x = 0
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
⊢ -3 * 0 ^ 2 * Q x * Q z + 3 * 0 * Q x ^ 2 * 0 + P y ^ 2 * Q z ^ 2 - Q y ^ 2 * 0 ^ 2 + W'.a₁ * 0 * P y * Q z ^ 2 -
                  W'.a₁ * Q x * Q y * 0 ^ 2 -
                W'.a₂ * 0 ^ 2 * Q z ^ 2 +
              W'.a₂ * Q x ^ 2 * 0 ^ 2 +
            W'.a₃ * P y * 0 * Q z ^ 2 -
          W'.a₃ * Q y * 0 ^ 2 * Q z -
        W'.a₄ * 0 * 0 * Q z ^ 2 +
      W'.a₄ * Q x * 0 ^ 2 * Q z =
    P y ^ 2 * Q z * Q z

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
⊢ -3 * 0 ^ 2 * Q x * Q z + 3 * 0 * Q x ^ 2 * 0 + P y ^ 2 * Q z ^ 2 - Q y ^ 2 * 0 ^ 2 + W'.a₁ * 0 * P y * Q z ^ 2 -
                  W'.a₁ * Q x * Q y * 0 ^ 2 -
                W'.a₂ * 0 ^ 2 * Q z ^ 2 +
              W'.a₂ * Q x ^ 2 * 0 ^ 2 +
            W'.a₃ * P y * 0 * Q z ^ 2 -
          W'.a₃ * Q y * 0 ^ 2 * Q z -
        W'.a₄ * 0 * 0 * Q z ^ 2 +
      W'.a₄ * Q x * 0 ^ 2 * Q z =
    P y ^ 2 * Q z * Q z