mathlib-initiative/mathlib-tactics huggingface dataset:
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 : (algebraMap P.Ring (Localization.Away f)) ↑x = 0
⊢ ((TensorProduct.mk S T P.toExtension.Cotangent) 1) (Extension.Cotangent.mk x) = 0

Tactic:
by

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 ι
⊢ Function.Injective
    ⇑(LinearMap.liftBaseChange T (Extension.Cotangent.map ((localizationAway T g).toComp P).toExtensionHom))

Tactic:
by

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 ι
x : ((localizationAway T g).comp P).toExtension.Cotangent
⊢ (cotangentCompAwaySec g P x) (cMulXSubOneCotangent T g) = x

Tactic:
by

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 ι
x : ((localizationAway T g).comp P).toExtension.Cotangent
hx : (Extension.Cotangent.map ((localizationAway T g).ofComp P).toExtensionHom) x = cMulXSubOneCotangent T g
⊢ Extension.Cotangent.map ((localizationAway T g).ofComp P).toExtensionHom ∘ₗ cotangentCompAwaySec g P x = LinearMap.id

Tactic:
by

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 ι
x : ((localizationAway T g).comp P).toExtension.Cotangent
hx : (Extension.Cotangent.map ((localizationAway T g).ofComp P).toExtensionHom) x = cMulXSubOneCotangent T g
⊢ (cotangentCompLocalizationAwayEquiv g P hx).symm (0, cMulXSubOneCotangent T g) = x

Tactic:
by

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 ι
x : ((localizationAway T g).comp P).toExtension.Cotangent
hx : (Extension.Cotangent.map ((localizationAway T g).ofComp P).toExtensionHom) x = cMulXSubOneCotangent T g
a : T ⊗[S] P.toExtension.Cotangent
⊢ (cotangentCompLocalizationAwayEquiv g P hx).symm (a, 0) =
    (LinearMap.liftBaseChange T (Extension.Cotangent.map ((localizationAway T g).toComp P).toExtensionHom)) a

Tactic:
by

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 ι
x : ((localizationAway T g).comp P).toExtension.Cotangent
hx : (Extension.Cotangent.map ((localizationAway T g).ofComp P).toExtensionHom) x = cMulXSubOneCotangent T g
a : ((localizationAway T g).comp P).toExtension.Cotangent
⊢ ((cotangentCompLocalizationAwayEquiv g P hx) a).2 =
    (Extension.Cotangent.map ((localizationAway T g).ofComp P).toExtensionHom) a

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
f : S →ₐ[R] A
hf : Function.Surjective ⇑f
inst✝² : Module.Flat R S
inst✝¹ : IsNoetherianRing S
inst✝ : FormallySmooth R A
⊢ Module.Flat R A

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : IsNoetherianRing R
inst✝ : Smooth R A
⊢ Module.Flat R A

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Smooth R A
⊢ Module.Flat R A

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.Smooth
⊢ f.Flat

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.Etale

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (algebraMap R S).Etale ↔ Algebra.Etale R S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.Etale

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ f.Etale ↔ f.FormallyUnramified ∧ f.Smooth

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.Etale

Goal state before:
pp: ⊢ @Etale = fun R S x x_1 f ↦ f.FormallyUnramified ∧ f.Smooth

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.Etale

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.Etale
⊢ f.FormallyUnramified

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.Etale

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Bijective ⇑f
⊢ f.Etale

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.Etale

Goal state before:
pp: ⊢ IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Etale

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.Etale

Goal state before:
pp: ⊢ PropertyIsLocal fun {R S} [CommRing R] [CommRing S] ↦ Etale

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.Etale

Goal state before:
pp: ⊢ StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Etale

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.Etale

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ f.Etale ↔ f.Flat ∧ f.FormallyUnramified ∧ f.FinitePresentation

Tactic:
by

Goal state after:
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
σ✝ : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ ∀ a ∈ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)), (aeval P.val) a = 0

Tactic:
by

Goal state after:
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
σ✝ : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ IsScalarTower P.Ring D.T S

Tactic:
by

Goal state after:
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
σ✝ : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ D.g ^ 1 • RingHom.ker (algebraMap P.Ring S) ≤ RingHom.ker (algebraMap P.Ring D.T)

Tactic:
by

Goal state after:
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
σ✝ : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
h : (algebraMap P.Ring S) D.g = 1
⊢ IsUnit ((algebraMap P.Ring S) D.g)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
⊢ W'.addX P Q * (P z * Q z) ^ 2 =
    ((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)

Tactic:
by

Goal state after:
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
σ✝ : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ IsLocalization.Away D.gbar S

Tactic:
by

Goal state after:
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.addX P Q =
    ((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

Tactic:
by

Goal state after:
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
σ✝ : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
x : MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b))
⊢ (Ideal.Quotient.mk (Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b))))
      (if x = 0 then 0 else if x = -1 then -1 else Function.surjInv ⋯ x) =
    x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (algebraMap R S).IsStandardSmooth ↔ Algebra.IsStandardSmooth R S

Tactic:
by

Goal state after:
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
⊢ IsStandardSmoothOfRelativeDimension n (algebraMap R S) ↔ Algebra.IsStandardSmoothOfRelativeDimension n R S

Tactic:
by

Goal state after:
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
σ✝ : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
i : ι
⊢ (aeval P.val) (X i) = (algebraMap D.T S) (D.presLeft.val i)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: n : ℕ
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : IsStandardSmoothOfRelativeDimension n f
⊢ f.IsStandardSmooth

Tactic:
by

Goal state after:
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
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ D.fhom.toAlgHom = AlgHom.id R P.Ring

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
e : R ≃+* S
⊢ IsStandardSmoothOfRelativeDimension 0 ↑e

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
T : Type u_1
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : g.IsStandardSmooth
hf : f.IsStandardSmooth
⊢ (g.comp f).IsStandardSmooth

Tactic:
by

Goal state after:
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
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ D.presLeft.ker ≤ P.ker

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: n m : ℕ
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
T : Type u_1
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : IsStandardSmoothOfRelativeDimension n g
hf : IsStandardSmoothOfRelativeDimension m f
⊢ IsStandardSmoothOfRelativeDimension (n + m) (g.comp f)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: ⊢ RespectsIso @IsStandardSmooth

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: n : ℕ
R S T : Type u_2
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : R →+* S
e : S ≃+* T
hf : IsStandardSmoothOfRelativeDimension n f
⊢ IsStandardSmoothOfRelativeDimension n (e.toRingHom.comp f)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: n : ℕ
R S T : Type u_2
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : S →+* T
e : R ≃+* S
hf : IsStandardSmoothOfRelativeDimension n f
⊢ IsStandardSmoothOfRelativeDimension (n + 0) (f.comp e.toRingHom)

Tactic:
exact hf.comp (IsStandardSmoothOfRelativeDimension.equiv e)

Goal state after:
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: n : ℕ
R S T : Type u_2
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : S →+* T
e : R ≃+* S
hf : IsStandardSmoothOfRelativeDimension n f
⊢ IsStandardSmoothOfRelativeDimension n (f.comp e.toRingHom)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : (algebraMap R T).IsStandardSmooth
⊢ Algebra.IsStandardSmooth R T

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmooth R T
this : Algebra.IsStandardSmooth S (S ⊗[R] T)
⊢ (algebraMap S (S ⊗[R] T)).IsStandardSmooth

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: ⊢ IsStableUnderBaseChange @IsStandardSmooth

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : IsStandardSmoothOfRelativeDimension n (algebraMap R T)
⊢ Algebra.IsStandardSmoothOfRelativeDimension n R T

Tactic:
by

Goal state after:
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
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
x : ↥D.presLeft.toExtension.ker
⊢ D.tensorCotangentHom (1 ⊗ₜ[D.T] Extension.Cotangent.mk x) = Extension.Cotangent.mk ⟨↑x, ⋯⟩

Tactic:
by

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

Goal state before:
pp: 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
inst✝¹ : Finite D.vars
inst✝ : Finite D.rels
⊢ (subalgebra R D).FG

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
this : Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)
⊢ IsStandardSmoothOfRelativeDimension n (algebraMap S (S ⊗[R] T))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: n : ℕ
⊢ IsStableUnderBaseChange (@IsStandardSmoothOfRelativeDimension n)

Tactic:
by

Goal state after:
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
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ Submodule.span D.T (Set.range fun i ↦ Extension.Cotangent.mk (D.kerGen i)) = ⊤

Tactic:
by

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

Goal state before:
pp: 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
⊢ D.P.coeffs ⊆ Set.range ⇑(algebraMap (↥(subalgebra R D)) A)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
Rᵣ : Type u_2
inst✝² : CommRing Rᵣ
inst✝¹ : Algebra R Rᵣ
r : R
inst✝ : IsLocalization.Away r Rᵣ
⊢ (algebraMap R Rᵣ).toAlgebra = inst✝¹

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
Rᵣ : Type u_2
inst✝² : CommRing Rᵣ
inst✝¹ : Algebra R Rᵣ
r : R
inst✝ : IsLocalization.Away r Rᵣ
⊢ IsStandardSmoothOfRelativeDimension 0 (algebraMap R Rᵣ)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: ⊢ HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: ⊢ HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmoothOfRelativeDimension 0

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
⊢ W'.addX (u • P) (v • Q) = (u * v) ^ 2 * W'.addX P Q

Tactic:
by

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

Goal state before:
pp: 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
i : D.vars
⊢ ↑(D.h i).coeffs ⊆ Set.range ⇑(algebraMap (↥(subalgebra R D)) A)

Tactic:
by

Goal state after:
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
⊢ Nat.card ↑(Set.range P.map)ᶜ = n

Tactic:
by

Goal state after:
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
σ✝ : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ S ⊗[D.T] D.presLeft.toExtension.Cotangent ≃ₗ[S] P.toExtension.Cotangent

Tactic:
by

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

Goal state before:
pp: 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
i : D.rels
⊢ ↑(D.p i).coeffs ⊆ Set.range ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))

Tactic:
by

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

Goal state before:
pp: 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
i : D.vars
⊢ ↑(D.q i).coeffs ⊆ Set.range ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ W'.addX P P = 0

Tactic:
by

Goal state after:
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
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
⊢ (Extension.Cotangent.map ((localizationAway S D.gbar).ofComp D.presLeft.toGenerators).toExtensionHom)
      (Extension.Cotangent.mk ⟨D.pres.relation (Sum.inl ()), ⋯⟩) =
    cMulXSubOneCotangent S D.gbar

Tactic:
by

Goal state after:
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
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
⊢ D.basis (Sum.inl ()) = D.cotangentEquivProd.symm (cMulXSubOneCotangent S D.gbar, 0)

Tactic:
by

Goal state after:
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
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
i : σ
⊢ D.basis (Sum.inr i) = D.cotangentEquivProd.symm (0, D.basisLeft i)

Tactic:
by

Goal state after: