-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_8 : Localization.AtPrime.IsLiesOverAlgebra p q
this : EssFiniteType.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
a :
  Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime q))
    (Ideal.map (R := Localization.AtPrime p) (F := RingHom.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
      (Localization.localRingHom p q (algebraMap R S) ⋯) (maximalIdeal (Localization.AtPrime p)))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p)
a₁ :
  Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime q))
    (Ideal.map (R := Localization.AtPrime p) (F := RingHom.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
      (Localization.localRingHom p q (algebraMap R S) ⋯)
      (Ideal.map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p)
a₂ :
  Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime q))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q))
      (RingHom.comp (β := Localization.AtPrime p) (Localization.localRingHom p q (algebraMap R S) ⋯)
        (algebraMap R (Localization.AtPrime p)))
      p)
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p)
a₃ :
  Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime q))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q))
      (@RingHom.comp _ (Localization.AtPrime p) _ _ Semiring.toNonAssocSemiring _
        (IsLocalization.map (M := p.primeCompl) (T := q.primeCompl) (Localization.AtPrime q) (algebraMap R S) ⋯)
        (algebraMap R (Localization.AtPrime p)))
      p)
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p)
a₄ :
  Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime q))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q))
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S (Localization.AtPrime q)) (algebraMap R S)) p)
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p)
⊢ Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime q))
    (Ideal.map (R := Localization.AtPrime p) (F := RingHom.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
      (algebraMap (Localization.AtPrime p) (Localization.AtPrime q)) (maximalIdeal (Localization.AtPrime p)))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p)
have a₅ : Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime q))
  (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p)
  (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p)
Tactic: rw [Localization.AtPrime.IsLiesOverAlgebra.algebraMap_eq,
    ← Localization.AtPrime.map_eq_maximalIdeal, Ideal.map_map, Localization.localRingHom,
    IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]