-- Mathlib/RingTheory/Unramified/LocalRing.lean
/-- Let `A` be an essentially of finite type `R`-algebra, `q` be a prime over `p`.
Then `A` is unramified at `p` if and only if `κ(q)/κ(p)` is separable, and `pS_q = qS_q`. -/
lemma isUnramifiedAt_iff_map_eq [EssFiniteType R S]
    (p : Ideal R) [p.IsPrime] (q : Ideal S) [q.IsPrime] [q.LiesOver p] :
    Algebra.IsUnramifiedAt R q ↔
      Algebra.IsSeparable p.ResidueField q.ResidueField ∧
      p.map (algebraMap R (Localization.AtPrime q)) = maximalIdeal _

Proof state:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : EssFiniteType R S
p : Ideal R
inst✝² : p.IsPrime
q : Ideal S
inst✝¹ : q.IsPrime
inst✝ : q.LiesOver p
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) :=
  (Localization.localRingHom p q (algebraMap R S) ⋯).toAlgebra
⊢ IsUnramifiedAt R q ↔
    Algebra.IsSeparable p.ResidueField q.ResidueField ∧
      Ideal.map (algebraMap R (Localization.AtPrime q)) p = maximalIdeal (Localization.AtPrime q)

Tactic:
have : IsScalarTower R (Localization.AtPrime p) (Localization.AtPrime q) := .of_algebraMap_eq
  fun x ↦ (Localization.localRingHom_to_map p q (algebraMap R S) Ideal.LiesOver.over x).symm

Result:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : EssFiniteType R S
p : Ideal R
inst✝² : p.IsPrime
q : Ideal S
inst✝¹ : q.IsPrime
inst✝ : q.LiesOver p
this✝ : Algebra (Localization.AtPrime p) (Localization.AtPrime q) :=
  (Localization.localRingHom p q (algebraMap R S) ⋯).toAlgebra
this : IsScalarTower R (Localization.AtPrime p) (Localization.AtPrime q)
⊢ IsUnramifiedAt R q ↔
    Algebra.IsSeparable p.ResidueField q.ResidueField ∧
      Ideal.map (algebraMap R (Localization.AtPrime q)) p = maximalIdeal (Localization.AtPrime q)

Proof state:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : EssFiniteType R S
p : Ideal R
inst✝² : p.IsPrime
q : Ideal S
inst✝¹ : q.IsPrime
inst✝ : q.LiesOver p
this✝² : Algebra (Localization.AtPrime p) (Localization.AtPrime q) :=
  (Localization.localRingHom p q (algebraMap R S) ⋯).toAlgebra
this✝¹ : IsScalarTower R (Localization.AtPrime p) (Localization.AtPrime q)
this✝ : IsLocalHom (algebraMap (Localization.AtPrime p) (Localization.AtPrime q)) :=
  Localization.isLocalHom_localRingHom p q (algebraMap R S) Ideal.LiesOver.over
this : EssFiniteType (Localization.AtPrime p) (Localization.AtPrime q)
⊢ Algebra.IsSeparable (ResidueField (Localization.AtPrime p)) (ResidueField (Localization.AtPrime q)) ∧
      Ideal.map (algebraMap (Localization.AtPrime p) (Localization.AtPrime q)) (maximalIdeal (Localization.AtPrime p)) =
        maximalIdeal (Localization.AtPrime q) ↔
    Algebra.IsSeparable p.ResidueField q.ResidueField ∧
      Ideal.map (algebraMap R (Localization.AtPrime q)) p = maximalIdeal (Localization.AtPrime q)

Tactic:
congr!

Result:
case a.h.e'_2.h.e'_2
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : EssFiniteType R S
p : Ideal R
inst✝² : p.IsPrime
q : Ideal S
inst✝¹ : q.IsPrime
inst✝ : q.LiesOver p
this✝² : Algebra (Localization.AtPrime p) (Localization.AtPrime q) :=
  (Localization.localRingHom p q (algebraMap R S) ⋯).toAlgebra
this✝¹ : IsScalarTower R (Localization.AtPrime p) (Localization.AtPrime q)
this✝ : IsLocalHom (algebraMap (Localization.AtPrime p) (Localization.AtPrime q)) :=
  Localization.isLocalHom_localRingHom p q (algebraMap R S) Ideal.LiesOver.over
this : EssFiniteType (Localization.AtPrime p) (Localization.AtPrime q)
⊢ Ideal.map (algebraMap (Localization.AtPrime p) (Localization.AtPrime q)) (maximalIdeal (Localization.AtPrime p)) =
    Ideal.map (algebraMap R (Localization.AtPrime q)) p

Proof state:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : EssFiniteType R S
p : Ideal R
inst✝² : p.IsPrime
q : Ideal S
inst✝¹ : q.IsPrime
inst✝ : q.LiesOver p
this✝ : Algebra (Localization.AtPrime p) (Localization.AtPrime q) :=
  (Localization.localRingHom p q (algebraMap R S) ⋯).toAlgebra
this : IsScalarTower R (Localization.AtPrime p) (Localization.AtPrime q)
⊢ IsUnramifiedAt R q ↔
    Algebra.IsSeparable p.ResidueField q.ResidueField ∧
      Ideal.map (algebraMap R (Localization.AtPrime q)) p = maximalIdeal (Localization.AtPrime q)

Tactic:
letI : IsLocalHom (algebraMap (Localization.AtPrime p) (Localization.AtPrime q)) :=
  Localization.isLocalHom_localRingHom _ _ _ Ideal.LiesOver.over

Result:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : EssFiniteType R S
p : Ideal R
inst✝² : p.IsPrime
q : Ideal S
inst✝¹ : q.IsPrime
inst✝ : q.LiesOver p
this✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q) :=
  (Localization.localRingHom p q (algebraMap R S) ⋯).toAlgebra
this✝ : IsScalarTower R (Localization.AtPrime p) (Localization.AtPrime q)
this : IsLocalHom (algebraMap (Localization.AtPrime p) (Localization.AtPrime q)) :=
  Localization.isLocalHom_localRingHom p q (algebraMap R S) Ideal.LiesOver.over
⊢ IsUnramifiedAt R q ↔
    Algebra.IsSeparable p.ResidueField q.ResidueField ∧
      Ideal.map (algebraMap R (Localization.AtPrime q)) p = maximalIdeal (Localization.AtPrime q)

Proof state:
case a.h.e'_2.h.e'_2
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : EssFiniteType R S
p : Ideal R
inst✝² : p.IsPrime
q : Ideal S
inst✝¹ : q.IsPrime
inst✝ : q.LiesOver p
this✝² : Algebra (Localization.AtPrime p) (Localization.AtPrime q) :=
  (Localization.localRingHom p q (algebraMap R S) ⋯).toAlgebra
this✝¹ : IsScalarTower R (Localization.AtPrime p) (Localization.AtPrime q)
this✝ : IsLocalHom (algebraMap (Localization.AtPrime p) (Localization.AtPrime q)) :=
  Localization.isLocalHom_localRingHom p q (algebraMap R S) Ideal.LiesOver.over
this : EssFiniteType (Localization.AtPrime p) (Localization.AtPrime q)
⊢ Ideal.map (algebraMap (Localization.AtPrime p) (Localization.AtPrime q)) (maximalIdeal (Localization.AtPrime p)) =
    Ideal.map (algebraMap R (Localization.AtPrime q)) p

Tactic:
rw [RingHom.algebraMap_toAlgebra, ← Localization.AtPrime.map_eq_maximalIdeal,
  Ideal.map_map, Localization.localRingHom,
  IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]

Result:
no goals