-- Mathlib/RingTheory/Unramified/LocalRing.lean
@[stacks 02FM]
lemma FormallyUnramified.of_map_maximalIdeal
    [Algebra.IsSeparable (ResidueField R) (ResidueField S)]
    (H : (maximalIdeal R).map (algebraMap R S) = maximalIdeal S) :
    Algebra.FormallyUnramified R S

Proof state:
case subsingleton_kaehlerDifferential.intro.intro.mk.smul
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
⊢ 1 ⊗ₜ[S] (KaehlerDifferential.D R S) (a • x) = 0

Tactic:
have : residue S x = 0 := by rwa [residue_eq_zero_iff, ← H]

Result:
case subsingleton_kaehlerDifferential.intro.intro.mk.smul
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
this : (residue S) x = 0
⊢ 1 ⊗ₜ[S] (KaehlerDifferential.D R S) (a • x) = 0

Proof state:
case subsingleton_kaehlerDifferential
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 (Ω[S⁄R])

Tactic:
rw [← subsingleton_tensorProduct (R := S)]

Result:
case subsingleton_kaehlerDifferential
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]))

Proof state:
case subsingleton_kaehlerDifferential
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:
refine subsingleton_of_forall_eq 0 fun x ↦ ?_

Result:
case subsingleton_kaehlerDifferential
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 : TensorProduct S (ResidueField S) (Ω[S⁄R])
⊢ x = 0

Proof state:
case subsingleton_kaehlerDifferential.intro
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 : (RingHom.ker (algebraMap S (ResidueField S))).Cotangent
⊢ (KaehlerDifferential.kerCotangentToTensor R S (ResidueField S)) x = 0

Tactic:
obtain ⟨⟨x, hx⟩, rfl⟩ := Ideal.toCotangent_surjective _ x

Result:
case subsingleton_kaehlerDifferential.intro.intro.mk
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 : S
hx : x ∈ RingHom.ker (algebraMap S (ResidueField S))
⊢ (KaehlerDifferential.kerCotangentToTensor R S (ResidueField S))
      ((RingHom.ker (algebraMap S (ResidueField S))).toCotangent ⟨x, hx⟩) =
    0

Proof state:
case subsingleton_kaehlerDifferential.intro.intro.mk.zero
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 : S
⊢ 1 ⊗ₜ[S] (KaehlerDifferential.D R S) 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
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
⊢ (residue S) x = 0

Tactic:
rwa [residue_eq_zero_iff, ← H]

Result:
no goals

Proof state:
case subsingleton_kaehlerDifferential.intro.intro.mk.smul
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
this : (residue S) x = 0
⊢ 1 ⊗ₜ[S] (KaehlerDifferential.D R S) (a • x) = 0

Tactic:
simp [*, TensorProduct.tmul_add, TensorProduct.smul_tmul', ← Algebra.algebraMap_eq_smul_one]

Result:
no goals