-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Instances (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
rw :
  Eq (α := RingHom.{u_1, u_2} R L)
    (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ L) (algebraMap R Rₚ))
    (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ L)
      (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ Sₚ) (algebraMap R Rₚ)))
rw₁ :
  Eq (α := RingHom.{u_1, u_2} R L)
    (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ L) (algebraMap R Rₚ))
    (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ L) (algebraMap R Sₚ))
rw₂ :
  Eq (α := RingHom.{u_1, u_2} R L)
    (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ L) (algebraMap R Rₚ))
    (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ L)
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S Sₚ) (algebraMap R S)))
rw₃ :
  Eq (α := RingHom.{u_1, u_2} R L)
    (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ L) (algebraMap R Rₚ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ L) (algebraMap S Sₚ)) (algebraMap R S))
rw₄ :
  Eq (α := RingHom.{u_1, u_2} R L)
    (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ L) (algebraMap R Rₚ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S))
rw₅ :
  Eq (α := RingHom.{u_1, u_2} R L)
    (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ K _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap Rₚ K)) (algebraMap R Rₚ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S))
rw₆ :
  Eq (α := RingHom.{u_1, u_2} R L)
    (@RingHom.comp _ K _ _ Semiring.toNonAssocSemiring _ (algebraMap K L)
      (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ K) (algebraMap R Rₚ)))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S))
rw₇ :
  Eq (α := RingHom.{u_1, u_2} R L)
    (@RingHom.comp _ K _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap R K))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S))
rw₈ :
  Eq (α := RingHom.{u_1, u_2} R L) (algebraMap R L)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S))
⊢ Eq (α := RingHom.{u_1, u_2} R L)
    (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ L) (algebraMap R Rₚ))
    (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ L) (algebraMap Rₚ Sₚ)) (algebraMap R Rₚ))
have rw₉ : Eq (α := RingHom.{u_1, u_2} R L) (algebraMap R L) (algebraMap R L)
Tactic: rw [RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq R Rₚ Sₚ, IsScalarTower.algebraMap_eq R S Sₚ,
    ← RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq S Sₚ L, IsScalarTower.algebraMap_eq Rₚ K L,
    RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq,
    ← IsScalarTower.algebraMap_eq]