-- 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
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)
⊢ FormallyUnramified (Localization.AtPrime p) (Localization.AtPrime q) ↔
    Algebra.IsSeparable p.ResidueField q.ResidueField ∧
      Ideal.map (algebraMap R (Localization.AtPrime q)) p = maximalIdeal (Localization.AtPrime q)

Tactic:
rw [FormallyUnramified.iff_map_maximalIdeal_eq]

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
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)

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)
⊢ IsUnramifiedAt R q ↔
    Algebra.IsSeparable p.ResidueField q.ResidueField ∧
      Ideal.map (algebraMap R (Localization.AtPrime q)) p = maximalIdeal (Localization.AtPrime q)

Tactic:
trans Algebra.FormallyUnramified (Localization.AtPrime p) (Localization.AtPrime q)

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
this : EssFiniteType (Localization.AtPrime p) (Localization.AtPrime q)
⊢ IsUnramifiedAt R q ↔ FormallyUnramified (Localization.AtPrime p) (Localization.AtPrime q)

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)
⊢ FormallyUnramified (Localization.AtPrime p) (Localization.AtPrime 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
⊢ IsUnramifiedAt R q ↔
    Algebra.IsSeparable p.ResidueField q.ResidueField ∧
      Ideal.map (algebraMap R (Localization.AtPrime q)) p = maximalIdeal (Localization.AtPrime q)

Tactic:
have : EssFiniteType (Localization.AtPrime p) (Localization.AtPrime q) := .of_comp R _ _

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
this : EssFiniteType (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)
⊢ IsUnramifiedAt R q ↔ FormallyUnramified (Localization.AtPrime p) (Localization.AtPrime q)

Tactic:
exact ⟨fun _ ↦ .of_comp R _ _, fun _ ↦ .comp _ (Localization.AtPrime p) _⟩

Result:
no goals