-- 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
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))
⊢ 1 ⊗ₜ[S] (KaehlerDifferential.D R S) x = 0

Tactic:
replace hx : x ∈ Ideal.map (algebraMap R S) (maximalIdeal R) := by simpa [H] using hx

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 ∈ Ideal.map (algebraMap R S) (maximalIdeal R)
⊢ 1 ⊗ₜ[S] (KaehlerDifferential.D R S) x = 0

Proof state:
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

Tactic:
simp only [KaehlerDifferential.kerCotangentToTensor_toCotangent]

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))
⊢ 1 ⊗ₜ[S] (KaehlerDifferential.D R S) x = 0

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 : S
hx : x ∈ RingHom.ker (algebraMap S (ResidueField S))
⊢ x ∈ Ideal.map (algebraMap R S) (maximalIdeal R)

Tactic:
simpa [H] using hx

Result:
no goals

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

Tactic:
obtain ⟨x, rfl⟩ := (KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange R S
  (ResidueField S) Ideal.Quotient.mk_surjective x).mp (Subsingleton.elim _ _)

Result:
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

Proof state:
case subsingleton_kaehlerDifferential.intro.intro.mk.add
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✝ x y : S
hx : x ∈ Submodule.span S (⇑(algebraMap R S) '' ↑(maximalIdeal R))
hy : y ∈ Submodule.span S (⇑(algebraMap R S) '' ↑(maximalIdeal R))
a✝¹ : 1 ⊗ₜ[S] (KaehlerDifferential.D R S) x = 0
a✝ : 1 ⊗ₜ[S] (KaehlerDifferential.D R S) y = 0
⊢ 1 ⊗ₜ[S] (KaehlerDifferential.D R S) (x + y) = 0

Tactic:
simp [*, TensorProduct.tmul_add]

Result:
no goals

Proof state:
case subsingleton_kaehlerDifferential.intro.intro.mk.mem
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✝ x : S
h : x ∈ ⇑(algebraMap R S) '' ↑(maximalIdeal R)
⊢ 1 ⊗ₜ[S] (KaehlerDifferential.D R S) x = 0

Tactic:
obtain ⟨x, hx, rfl⟩ := h

Result:
case subsingleton_kaehlerDifferential.intro.intro.mk.mem.intro.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✝ : S
x : R
hx : x ∈ ↑(maximalIdeal R)
⊢ 1 ⊗ₜ[S] (KaehlerDifferential.D R S) ((algebraMap R S) 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
⊢ Subsingleton (Ω[S⁄R])

Tactic:
have : FormallyUnramified (ResidueField R) (ResidueField S) := .of_isSeparable _ _

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)
⊢ Subsingleton (Ω[S⁄R])