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

Tactic:
let mR := (maximalIdeal R).map (algebraMap R S)

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

Tactic:
have : Nontrivial (S ⧸ mR) := Ideal.Quotient.nontrivial fun e ↦
  (maximalIdeal.isMaximal S).ne_top (top_le_iff.mp <| e.symm.trans_le hmR)

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

Tactic:
have : IsArtinianRing (S ⧸ mR) := isArtinian_of_tower (ResidueField R) inferInstance

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

Tactic:
rwa [← isField_iff_maximalIdeal_eq] at this

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

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