mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
ι' : Type w₃
σ : Type w₂
σ' : Type w₄
Q : Generators S T ι
P : Generators R S σ
Q' : Generators S T ι'
P' : Generators R S σ'
f : Q'.Hom Q
this : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
y : Q'.toExtension.Ring
hy : y ∈ Q'.toExtension.ker
hx✝ : Extension.Cotangent.mk ⟨y, hy⟩ ∈ Q'.toExtension.cotangentComplex.ker
hx : 1 ⊗ₜ[Q'.Ring] (D S Q'.Ring) y = 0
⊢ (δAux R Q') y = (δAux R Q') y

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
Q : Ideal A
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Ideal.span {p} = RingHom.ker (aeval x).toRingHom
hp₂ : Function.Surjective ⇑(aeval x)
this✝² : FiniteType K A
this✝¹ : Module.Finite K (Localization.AtPrime Q)
this✝ : IsField (Localization.AtPrime Q)
this : Field (Localization.AtPrime Q) := this✝.toField
q : K[X] := minpoly K ((algebraMap A Q.ResidueField) x)
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
W : Generators R T τ
f : W.Hom Q
⊢ Function.Exact ⇑(Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom) ⇑(δ Q P)

Tactic:
]

Goal state after:
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
W : Generators R T τ
f : W.Hom Q
⊢ Function.Exact ⇑(Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom) ⇑(δ Q P)
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
Q : Ideal A
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Ideal.span {p} = RingHom.ker (aeval x).toRingHom
hp₂ : Function.Surjective ⇑(aeval x)
this✝³ : FiniteType K A
this✝² : Module.Finite K (Localization.AtPrime Q)
this✝¹ : IsField (Localization.AtPrime Q)
this✝ : Field (Localization.AtPrime Q) := this✝¹.toField
q : K[X] := minpoly K ((algebraMap A Q.ResidueField) x)
this : (algebraMap A (Localization.AtPrime Q)) ((aeval x) q) = 0
m : K[X]
hm : (aeval x) m ∈ Q.primeCompl
hm' : p ∣ m * q
⊢ ¬q * q ∣ p

Tactic:
]

Goal state after:
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
Q : Ideal A
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Ideal.span {p} = RingHom.ker (aeval x).toRingHom
hp₂ : Function.Surjective ⇑(aeval x)
this✝³ : FiniteType K A
this✝² : Module.Finite K (Localization.AtPrime Q)
this✝¹ : IsField (Localization.AtPrime Q)
this✝ : Field (Localization.AtPrime Q) := this✝¹.toField
q : K[X] := minpoly K ((algebraMap A Q.ResidueField) x)
this : (algebraMap A (Localization.AtPrime Q)) ((aeval x) q) = 0
m : K[X]
hm : (aeval x) m ∈ Q.primeCompl
hm' : p ∣ m * q
⊢ ¬q * q ∣ p
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
⊢ ∀ (y : P.toExtension.H1Cotangent),
    (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom) y ∈
      ↑(Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom).ker

Tactic:
]

Goal state after:
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
⊢ ∀ (y : P.toExtension.H1Cotangent),
    (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom) y ∈
      ↑(Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom).ker
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
Q : Ideal A
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Ideal.span {p} = RingHom.ker (aeval x).toRingHom
hp₂ : Function.Surjective ⇑(aeval x)
this✝⁴ : FiniteType K A
this✝³ : Module.Finite K (Localization.AtPrime Q)
this✝² : IsField (Localization.AtPrime Q)
this✝¹ : Field (Localization.AtPrime Q) := this✝².toField
q : K[X] := minpoly K ((algebraMap A Q.ResidueField) x)
this✝ : (algebraMap A (Localization.AtPrime Q)) ((aeval x) q) = 0
m : K[X]
hm : (aeval x) m ∈ Q.primeCompl
hm' : p ∣ m * q
H : q * q ∣ p
this : (aeval x) m ∈ Q
⊢ False

Tactic:
]

Goal state after:
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
Q : Ideal A
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Ideal.span {p} = RingHom.ker (aeval x).toRingHom
hp₂ : Function.Surjective ⇑(aeval x)
this✝⁴ : FiniteType K A
this✝³ : Module.Finite K (Localization.AtPrime Q)
this✝² : IsField (Localization.AtPrime Q)
this✝¹ : Field (Localization.AtPrime Q) := this✝².toField
q : K[X] := minpoly K ((algebraMap A Q.ResidueField) x)
this✝ : (algebraMap A (Localization.AtPrime Q)) ((aeval x) q) = 0
m : K[X]
hm : (aeval x) m ∈ Q.primeCompl
hm' : p ∣ m * q
H : q * q ∣ p
this : (aeval x) m ∈ Q
⊢ False
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: case tmul.tmul
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
this✝¹ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝ : IsScalarTower P.Ring S T
this : IsScalarTower P.Ring Q.Ring T
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker :=
  LinearEquiv.ofBijective (LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) H
f' : ↥Q.ker →ₗ[Q.Ring] T ⊗[S] P.Cotangent :=
  LinearMap.liftBaseChange Q.Ring (↑P.Ring ((TensorProduct.mk S T P.Cotangent) 1) ∘ₗ Cotangent.mk) ∘ₗ ↑e.symm
a : Q.Ring
b : ↥P.ker
c : Q.Ring
d : ↥P.ker
h₂ : ↑b • Cotangent.mk d = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
this : CotangentSpace.map P.toInfinitesimal = ↑(tensorKaehlerQuotKerSqEquiv R P.Ring S).symm
⊢ Function.Bijective ⇑↑(tensorKaehlerQuotKerSqEquiv R P.Ring S).symm

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
this : CotangentSpace.map P.toInfinitesimal = ↑(tensorKaehlerQuotKerSqEquiv R P.Ring S).symm
⊢ Function.Bijective ⇑↑(tensorKaehlerQuotKerSqEquiv R P.Ring S).symm
Module: Mathlib.RingTheory.Unramified.LocalRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : FormallyUnramified R S
mR : Ideal S := Ideal.map (algebraMap R S) (maximalIdeal R)
hmR : mR ≤ maximalIdeal S
this✝⁷ : Algebra (ResidueField R) (S ⧸ mR) :=
  { smul := Quotient.lift₂ (fun x1 x2 ↦ ⟦x1 • x2⟧) ⋯,
    algebraMap := Ideal.quotientMap (Ideal.map (algebraMap R S) (maximalIdeal R)) (algebraMap R S) ⋯, commutes' := ⋯,
    smul_def' := ⋯ }
this✝⁶ : IsScalarTower R (ResidueField R) (S ⧸ mR)
this✝⁵ : FormallyUnramified (ResidueField R) (S ⧸ mR)
this✝⁴ : EssFiniteType (ResidueField R) (S ⧸ mR)
this✝³ : Module.Finite (ResidueField R) (S ⧸ mR)
this✝² : IsReduced (S ⧸ mR)
this✝¹ : IsArtinianRing (S ⧸ mR)
this✝ : Nontrivial (S ⧸ mR)
this : IsLocalRing (S ⧸ mR)
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case left
R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ ∀ (a : P.Cotangent), (map P.toInfinitesimal) a = 0 → a = 0

Tactic:
]

Goal state after:
case left
R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ ∀ (a : P.Cotangent), (map P.toInfinitesimal) a = 0 → a = 0
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : ↥P.ker
hx : P.toInfinitesimal.toRingHom ↑x ∈ ⊥
⊢ ↑x ∈ P.ker ^ 2

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : ↥P.ker
hx : P.toInfinitesimal.toRingHom ↑x ∈ ⊥
⊢ ↑x ∈ P.ker ^ 2
Module: Mathlib.RingTheory.Unramified.LocalRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : FormallyUnramified R S
mR : Ideal S := Ideal.map (algebraMap R S) (maximalIdeal R)
hmR : mR ≤ maximalIdeal S
this✝⁸ : Algebra (ResidueField R) (S ⧸ mR) :=
  { smul := Quotient.lift₂ (fun x1 x2 ↦ ⟦x1 • x2⟧) ⋯,
    algebraMap := Ideal.quotientMap (Ideal.map (algebraMap R S) (maximalIdeal R)) (algebraMap R S) ⋯, commutes' := ⋯,
    smul_def' := ⋯ }
this✝⁷ : IsScalarTower R (ResidueField R) (S ⧸ mR)
this✝⁶ : FormallyUnramified (ResidueField R) (S ⧸ mR)
this✝⁵ : EssFiniteType (ResidueField R) (S ⧸ mR)
this✝⁴ : Module.Finite (ResidueField R) (S ⧸ mR)
this✝³ : IsReduced (S ⧸ mR)
this✝² : IsArtinianRing (S ⧸ mR)
this✝¹ : Nontrivial (S ⧸ mR)
this✝ : IsLocalRing (S ⧸ mR)
this : IsField (S ⧸ mR)
⊢ IsField (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : FormallyUnramified R S
mR : Ideal S := Ideal.map (algebraMap R S) (maximalIdeal R)
hmR : mR ≤ maximalIdeal S
this✝⁸ : Algebra (ResidueField R) (S ⧸ mR) :=
  { smul := Quotient.lift₂ (fun x1 x2 ↦ ⟦x1 • x2⟧) ⋯,
    algebraMap := Ideal.quotientMap (Ideal.map (algebraMap R S) (maximalIdeal R)) (algebraMap R S) ⋯, commutes' := ⋯,
    smul_def' := ⋯ }
this✝⁷ : IsScalarTower R (ResidueField R) (S ⧸ mR)
this✝⁶ : FormallyUnramified (ResidueField R) (S ⧸ mR)
this✝⁵ : EssFiniteType (ResidueField R) (S ⧸ mR)
this✝⁴ : Module.Finite (ResidueField R) (S ⧸ mR)
this✝³ : IsReduced (S ⧸ mR)
this✝² : IsArtinianRing (S ⧸ mR)
this✝¹ : Nontrivial (S ⧸ mR)
this✝ : IsLocalRing (S ⧸ mR)
this : IsField (S ⧸ mR)
⊢ IsField (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))
Module: Mathlib.RingTheory.Unramified.LocalRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : FormallyUnramified R S
⊢ IsField (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : FormallyUnramified R S
⊢ IsField (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : P.Ring
x_in✝ : x ∈ P.toExtension.ker
x_in : x ∈ RingHom.ker (aeval P.val)
property✝ : Extension.Cotangent.mk ⟨x, x_in✝⟩ ∈ P.toExtension.cotangentComplex.ker
⊢ (Q.ofComp P).toAlgHom ((Q.toComp P).toAlgHom x) ∈ Q.toExtension.ker ^ 2

Tactic:
]

Goal state after:
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : P.Ring
x_in✝ : x ∈ P.toExtension.ker
x_in : x ∈ RingHom.ker (aeval P.val)
property✝ : Extension.Cotangent.mk ⟨x, x_in✝⟩ ∈ P.toExtension.cotangentComplex.ker
⊢ (Q.ofComp P).toAlgHom ((Q.toComp P).toAlgHom x) ∈ Q.toExtension.ker ^ 2
Module: Mathlib.RingTheory.Unramified.LocalRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : Algebra.IsSeparable (ResidueField R) (ResidueField S)
H : Ideal.map (algebraMap R S) (maximalIdeal R) = maximalIdeal S
this✝ : FormallyUnramified (ResidueField R) (ResidueField S)
this : FormallyUnramified R (ResidueField S)
⊢ Subsingleton (TensorProduct S (ResidueField S) Ω[S⁄R])

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : Algebra.IsSeparable (ResidueField R) (ResidueField S)
H : Ideal.map (algebraMap R S) (maximalIdeal R) = maximalIdeal S
this✝ : FormallyUnramified (ResidueField R) (ResidueField S)
this : FormallyUnramified R (ResidueField S)
⊢ Subsingleton (TensorProduct S (ResidueField S) Ω[S⁄R])
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: case right
R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : P.Ring
hx✝ : (Ideal.Quotient.mk (P.ker ^ 2)) x ∈ P.infinitesimal.ker
hx : x ∈ P.ker
⊢ ∃ a, (map P.toInfinitesimal) a = mk ⟨(Ideal.Quotient.mk (P.ker ^ 2)) x, hx✝⟩

Tactic:
]

Goal state after:
case right
R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : P.Ring
hx✝ : (Ideal.Quotient.mk (P.ker ^ 2)) x ∈ P.infinitesimal.ker
hx : x ∈ P.ker
⊢ ∃ a, (map P.toInfinitesimal) a = mk ⟨(Ideal.Quotient.mk (P.ker ^ 2)) x, hx✝⟩
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : P.Ring
x_in✝ : x ∈ P.toExtension.ker
x_in : x ∈ RingHom.ker (aeval P.val)
property✝ : Extension.Cotangent.mk ⟨x, x_in✝⟩ ∈ P.toExtension.cotangentComplex.ker
⊢ 0 ∈ Q.toExtension.ker ^ 2

Tactic:
]

Goal state after:
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : P.Ring
x_in✝ : x ∈ P.toExtension.ker
x_in : x ∈ RingHom.ker (aeval P.val)
property✝ : Extension.Cotangent.mk ⟨x, x_in✝⟩ ∈ P.toExtension.cotangentComplex.ker
⊢ 0 ∈ Q.toExtension.ker ^ 2
Module: Mathlib.RingTheory.Unramified.LocalRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : Algebra.IsSeparable (ResidueField R) (ResidueField S)
H : Ideal.map (algebraMap R S) (maximalIdeal R) = maximalIdeal S
this✝ : FormallyUnramified (ResidueField R) (ResidueField S)
this : FormallyUnramified R (ResidueField S)
x✝ a x : S
hx : x ∈ Submodule.span S (⇑(algebraMap R S) '' ↑(maximalIdeal R))
a✝ : 1 ⊗ₜ[S] (KaehlerDifferential.D R S) x = 0
⊢ x ∈ Ideal.map (algebraMap R S) (maximalIdeal R)

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : Algebra.IsSeparable (ResidueField R) (ResidueField S)
H : Ideal.map (algebraMap R S) (maximalIdeal R) = maximalIdeal S
this✝ : FormallyUnramified (ResidueField R) (ResidueField S)
this : FormallyUnramified R (ResidueField S)
x✝ a x : S
hx : x ∈ Submodule.span S (⇑(algebraMap R S) '' ↑(maximalIdeal R))
a✝ : 1 ⊗ₜ[S] (KaehlerDifferential.D R S) x = 0
⊢ x ∈ Ideal.map (algebraMap R S) (maximalIdeal R)
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: S : Type u_1
inst✝⁴ : CommRing S
q : Ideal S
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : q.IsPrime
inst✝ : Module.Finite R S
p : Ideal R := under R q
Sq : Type u_1 := Localization.AtPrime q
⊢ 0 <
    (Module.length (Localization.AtPrime q)
        (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R q))).toNat

Tactic:
]

Goal state after:
S : Type u_1
inst✝⁴ : CommRing S
q : Ideal S
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : q.IsPrime
inst✝ : Module.Finite R S
p : Ideal R := under R q
Sq : Type u_1 := Localization.AtPrime q
⊢ 0 <
    (Module.length (Localization.AtPrime q)
        (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R q))).toNat
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: case hn0
S : Type u_1
inst✝⁴ : CommRing S
q : Ideal S
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : q.IsPrime
inst✝ : Module.Finite R S
p : Ideal R := under R q
Sq : Type u_1 := Localization.AtPrime q
⊢ map (algebraMap S (Localization.AtPrime q)) (map (algebraMap R S) (under R q)) < ⊤

Tactic:
]

Goal state after:
case hn0
S : Type u_1
inst✝⁴ : CommRing S
q : Ideal S
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : q.IsPrime
inst✝ : Module.Finite R S
p : Ideal R := under R q
Sq : Type u_1 := Localization.AtPrime q
⊢ map (algebraMap S (Localization.AtPrime q)) (map (algebraMap R S) (under R q)) < ⊤
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: case hn0
S : Type u_1
inst✝⁴ : CommRing S
q : Ideal S
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : q.IsPrime
inst✝ : Module.Finite R S
p : Ideal R := under R q
Sq : Type u_1 := Localization.AtPrime q
⊢ IsLocalRing.maximalIdeal (Localization q.primeCompl) < ⊤

Tactic:
]

Goal state after:
case hn0
S : Type u_1
inst✝⁴ : CommRing S
q : Ideal S
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : q.IsPrime
inst✝ : Module.Finite R S
p : Ideal R := under R q
Sq : Type u_1 := Localization.AtPrime q
⊢ IsLocalRing.maximalIdeal (Localization q.primeCompl) < ⊤
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: S : Type u_1
inst✝⁴ : CommRing S
q : Ideal S
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : q.IsPrime
inst✝ : Module.Finite R S
p : Ideal R := under R q
Sq : Type u_1 := Localization.AtPrime q
r : PrimeSpectrum (p.Fiber S) := (PrimeSpectrum.primesOverOrderIsoFiber R S p) (primesOver.mk p q)
⊢ q = ↑(primesOver.mk p q)

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Unramified.LocalRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : EssFiniteType R S
p : Ideal R
inst✝⁴ : p.IsPrime
q : Ideal S
inst✝³ : q.IsPrime
inst✝² : q.LiesOver p
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p q
this : EssFiniteType (Localization.AtPrime p) (Localization.AtPrime q)
⊢ Algebra.IsSeparable (ResidueField (Localization.AtPrime p)) (ResidueField (Localization.AtPrime q)) ∧
      Ideal.map (algebraMap (Localization.AtPrime p) (Localization.AtPrime q)) (maximalIdeal (Localization.AtPrime p)) =
        maximalIdeal (Localization.AtPrime q) ↔
    Algebra.IsSeparable p.ResidueField q.ResidueField ∧
      Ideal.map (algebraMap R (Localization.AtPrime q)) p = maximalIdeal (Localization.AtPrime q)

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : EssFiniteType R S
p : Ideal R
inst✝⁴ : p.IsPrime
q : Ideal S
inst✝³ : q.IsPrime
inst✝² : q.LiesOver p
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p q
this : EssFiniteType (Localization.AtPrime p) (Localization.AtPrime q)
⊢ Algebra.IsSeparable (ResidueField (Localization.AtPrime p)) (ResidueField (Localization.AtPrime q)) ∧
      Ideal.map (algebraMap (Localization.AtPrime p) (Localization.AtPrime q)) (maximalIdeal (Localization.AtPrime p)) =
        maximalIdeal (Localization.AtPrime q) ↔
    Algebra.IsSeparable p.ResidueField q.ResidueField ∧
      Ideal.map (algebraMap R (Localization.AtPrime q)) p = maximalIdeal (Localization.AtPrime q)
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
T : Type u₃
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
inst✝ : Flat S T
⊢ (Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom).ker =
    (liftBaseChange T (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)).range

Tactic:
]

Goal state after:
R : Type u₁
S : Type u₂
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
T : Type u₃
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
inst✝ : Flat S T
⊢ (Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom).ker =
    (liftBaseChange T (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)).range
Module: Mathlib.RingTheory.Unramified.LocalRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : EssFiniteType R S
p : Ideal R
inst✝⁴ : p.IsPrime
q : Ideal S
inst✝³ : q.IsPrime
inst✝² : q.LiesOver p
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p q
this : EssFiniteType (Localization.AtPrime p) (Localization.AtPrime q)
⊢ Ideal.map (algebraMap R (Localization.AtPrime q)) p = Ideal.map (algebraMap R (Localization.AtPrime q)) p

Tactic:
]

Goal state after: