-- 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)
this✝³ : Module.Finite (ResidueField R) (S ⧸ mR)
this✝² : IsReduced (S ⧸ mR)
this✝¹ : IsArtinianRing (S ⧸ mR)
this✝ : Nontrivial (S ⧸ mR)
this : IsLocalRing (S ⧸ mR)
⊢ IsField (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))

Tactic:
have : maximalIdeal (S ⧸ mR) = ⊥ := by
  rw [← jacobson_eq_maximalIdeal _ bot_ne_top, IsArtinianRing.jacobson_eq_radical,
    ← Ideal.zero_eq_bot, ← nilradical, nilradical_eq_zero]

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)
this✝² : IsArtinianRing (S ⧸ mR)
this✝¹ : Nontrivial (S ⧸ mR)
this✝ : IsLocalRing (S ⧸ mR)
this : maximalIdeal (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)
⊢ IsField (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))

Tactic:
have : EssFiniteType (ResidueField R) (S ⧸ mR) := .of_comp R _ _

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)
⊢ 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))
⊢ IsField (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))

Tactic:
have : IsScalarTower R (ResidueField R) (S ⧸ mR) := inferInstanceAs (IsScalarTower R (R ⧸ _) _)

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)
⊢ 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
⊢ IsField (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))

Tactic:
letI : Algebra (ResidueField R) (S ⧸ mR) := inferInstanceAs (Algebra (R ⧸ _) _)

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))
⊢ 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)
⊢ IsField (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))

Tactic:
have : IsLocalRing (S ⧸ mR) := .of_surjective' _ Ideal.Quotient.mk_surjective

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)
this✝¹ : IsArtinianRing (S ⧸ mR)
this✝ : Nontrivial (S ⧸ mR)
this : IsLocalRing (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)
⊢ IsField (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))

Tactic:
have hmR : mR ≤ maximalIdeal S := ((local_hom_TFAE (algebraMap R S)).out 0 2 rfl rfl).mp ‹_›

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
⊢ IsField (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))