-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type u_4
inst_3 : CommRing B
inst_4 : IsDedekindDomain B
L : Ideal B
f : RingHom.{u_1, u_2} (R ⧸ I) (A ⧸ J)
g : RingHom.{u_2, u_4} (A ⧸ J) (B ⧸ L)
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := A ⧸ J) (⇑f : (a : R ⧸ I) → A ⧸ J)
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := A ⧸ J) (β := B ⧸ L) (⇑g : (a : A ⧸ J) → B ⧸ L)
x : { p : Ideal R // p ∣ I }
rw :
  Eq.{u_4 + 1} (α := { p : Ideal B // p ∣ L })
    (({
                toFun := fun (X : { p : Ideal A // p ∣ J }) ↦
                  Subtype.mk (p := fun (p : Ideal B) ↦ p ∣ L)
                    (comap (F := B →+* B ⧸ L) (Ideal.Quotient.mk L)
                      (map (R := A ⧸ J) g (map (F := A →+* A ⧸ J) (Ideal.Quotient.mk J) (↑X : Ideal A))))
                    ⋯,
                monotone' := ⋯ : OrderHom.{u_2, u_4} { p : Ideal A // p ∣ J } { p : Ideal B // p ∣ L } }.comp
            (idealFactorsFunOfQuotHom hf) :
          (a : { p : Ideal R // p ∣ I }) → { p : Ideal B // p ∣ L })
        x :
      { p : Ideal B // p ∣ L })
    ((idealFactorsFunOfQuotHom (f := g.comp f) ⋯ : (a : { p : Ideal R // p ∣ I }) → { p : Ideal B // p ∣ L }) x :
      { p : Ideal B // p ∣ L })
rw₁ :
  Eq.{u_4 + 1} (α := { p : Ideal B // p ∣ L })
    (({
                toFun := fun (X : { p : Ideal A // p ∣ J }) ↦
                  Subtype.mk (p := fun (p : Ideal B) ↦ p ∣ L)
                    (comap (F := B →+* B ⧸ L) (Ideal.Quotient.mk L)
                      (map (R := A ⧸ J) g (map (F := A →+* A ⧸ J) (Ideal.Quotient.mk J) (↑X : Ideal A))))
                    ⋯,
                monotone' := ⋯ : OrderHom.{u_2, u_4} { p : Ideal A // p ∣ J } { p : Ideal B // p ∣ L } }.comp
            {
              toFun := fun (X : { p : Ideal R // p ∣ I }) ↦
                Subtype.mk (p := fun (p : Ideal A) ↦ p ∣ J)
                  (comap (F := A →+* A ⧸ J) (Ideal.Quotient.mk J)
                    (map (R := R ⧸ I) f (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) (↑X : Ideal R))))
                  ⋯,
              monotone' := ⋯ : OrderHom.{u_1, u_2} { p : Ideal R // p ∣ I } { p : Ideal A // p ∣ J } } :
          (a : { p : Ideal R // p ∣ I }) → { p : Ideal B // p ∣ L })
        x :
      { p : Ideal B // p ∣ L })
    ((idealFactorsFunOfQuotHom (f := g.comp f) ⋯ : (a : { p : Ideal R // p ∣ I }) → { p : Ideal B // p ∣ L }) x :
      { p : Ideal B // p ∣ L })
rw₂ :
  Eq.{u_4 + 1} (α := { p : Ideal B // p ∣ L })
    (Function.comp.{u_1 + 1, u_2 + 1, u_4 + 1} (β := { p : Ideal A // p ∣ J })
        (⇑{
              toFun := fun (X : { p : Ideal A // p ∣ J }) ↦
                Subtype.mk (p := fun (p : Ideal B) ↦ p ∣ L)
                  (comap (F := B →+* B ⧸ L) (Ideal.Quotient.mk L)
                    (map (R := A ⧸ J) g (map (F := A →+* A ⧸ J) (Ideal.Quotient.mk J) (↑X : Ideal A))))
                  ⋯,
              monotone' := ⋯ : OrderHom.{u_2, u_4} { p : Ideal A // p ∣ J } { p : Ideal B // p ∣ L } } :
          (a : { p : Ideal A // p ∣ J }) → { p : Ideal B // p ∣ L })
        (⇑{
              toFun := fun (X : { p : Ideal R // p ∣ I }) ↦
                Subtype.mk (p := fun (p : Ideal A) ↦ p ∣ J)
                  (comap (F := A →+* A ⧸ J) (Ideal.Quotient.mk J)
                    (map (R := R ⧸ I) f (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) (↑X : Ideal R))))
                  ⋯,
              monotone' := ⋯ : OrderHom.{u_1, u_2} { p : Ideal R // p ∣ I } { p : Ideal A // p ∣ J } } :
          (a : { p : Ideal R // p ∣ I }) → { p : Ideal A // p ∣ J })
        x :
      { p : Ideal B // p ∣ L })
    ((idealFactorsFunOfQuotHom (f := g.comp f) ⋯ : (a : { p : Ideal R // p ∣ I }) → { p : Ideal B // p ∣ L }) x :
      { p : Ideal B // p ∣ L })
⊢ Eq.{u_4 + 1} (α := { p : Ideal B // p ∣ L })
    (((idealFactorsFunOfQuotHom hg).comp (idealFactorsFunOfQuotHom hf) :
          (a : { p : Ideal R // p ∣ I }) → { p : Ideal B // p ∣ L })
        x :
      { p : Ideal B // p ∣ L })
    ((idealFactorsFunOfQuotHom (f := g.comp f) ⋯ : (a : { p : Ideal R // p ∣ I }) → { p : Ideal B // p ∣ L }) x :
      { p : Ideal B // p ∣ L })
have rw₃ : Eq.{u_4 + 1} (α := { p : Ideal B // p ∣ L })
  (((fun (X : { p : Ideal A // p ∣ J }) ↦
          Subtype.mk (p := fun (p : Ideal B) ↦ p ∣ L)
            (comap (F := B →+* B ⧸ L) (Ideal.Quotient.mk L)
              (map (R := A ⧸ J) g (map (F := A →+* A ⧸ J) (Ideal.Quotient.mk J) (↑X : Ideal A))))
            sorry) ∘
        (⇑{
              toFun := fun (X : { p : Ideal R // p ∣ I }) ↦
                Subtype.mk (p := fun (p : Ideal A) ↦ p ∣ J)
                  (comap (F := A →+* A ⧸ J) (Ideal.Quotient.mk J)
                    (map (R := R ⧸ I) f (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) (↑X : Ideal R))))
                  sorry,
              monotone' := sorry : OrderHom.{u_1, u_2} { p : Ideal R // p ∣ I } { p : Ideal A // p ∣ J } } :
          (a : { p : Ideal R // p ∣ I }) → { p : Ideal A // p ∣ J }))
      x :
    { p : Ideal B // p ∣ L })
  ((idealFactorsFunOfQuotHom (f := g.comp f) sorry : (a : { p : Ideal R // p ∣ I }) → { p : Ideal B // p ∣ L }) x :
    { p : Ideal B // p ∣ L })
Tactic: rw [idealFactorsFunOfQuotHom, idealFactorsFunOfQuotHom, OrderHom.comp_coe, OrderHom.coe_mk,
    OrderHom.coe_mk, Function.comp_apply, idealFactorsFunOfQuotHom, OrderHom.coe_mk,
    Subtype.mk_eq_mk, Subtype.coe_mk, map_comap_of_surjective (Ideal.Quotient.mk J)
    Ideal.Quotient.mk_surjective, map_map]