-- Mathlib/RingTheory/Unramified/LocalRing.lean
lemma FormallyUnramified.isField_quotient_map_maximalIdeal [FormallyUnramified R S] :
    IsField (S ⧸ (maximalIdeal R).map (algebraMap R S))

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✝ : FormallyUnramified R S
mR : Ideal S := Ideal.map (algebraMap R S) (maximalIdeal R)
hmR : mR ≤ maximalIdeal S
this✝² : Algebra (ResidueField R) (S ⧸ mR) := inferInstanceAs (Algebra (R ⧸ maximalIdeal R) (S ⧸ mR))
this✝¹ : IsScalarTower R (ResidueField R) (S ⧸ mR)
this✝ : FormallyUnramified (ResidueField R) (S ⧸ mR)
this : EssFiniteType (ResidueField R) (S ⧸ mR)
⊢ IsField (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))

Tactic:
have : Module.Finite (ResidueField R) (S ⧸ mR) := FormallyUnramified.finite_of_free _ _

Result:
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) := inferInstanceAs (Algebra (R ⧸ maximalIdeal R) (S ⧸ mR))
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)
⊢ IsField (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))

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✝ : FormallyUnramified R S
mR : Ideal S := Ideal.map (algebraMap R S) (maximalIdeal R)
hmR : mR ≤ maximalIdeal S
this✝⁷ : Algebra (ResidueField R) (S ⧸ mR) := inferInstanceAs (Algebra (R ⧸ maximalIdeal R) (S ⧸ mR))
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)
⊢ maximalIdeal (S ⧸ mR) = ⊥

Tactic:
rw [← jacobson_eq_maximalIdeal _ bot_ne_top, IsArtinianRing.jacobson_eq_radical,
  ← Ideal.zero_eq_bot, ← nilradical, nilradical_eq_zero]

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✝ : FormallyUnramified R S
mR : Ideal S := Ideal.map (algebraMap R S) (maximalIdeal R)
hmR : mR ≤ maximalIdeal S
this✝³ : Algebra (ResidueField R) (S ⧸ mR) := inferInstanceAs (Algebra (R ⧸ maximalIdeal R) (S ⧸ mR))
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)
⊢ IsField (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))

Tactic:
have : IsReduced (S ⧸ mR) := FormallyUnramified.isReduced_of_field (ResidueField R) (S ⧸ mR)

Result:
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) := inferInstanceAs (Algebra (R ⧸ maximalIdeal R) (S ⧸ mR))
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)
⊢ IsField (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))