-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
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 })
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))))
              ⋯) ∘
          (⇑{
                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 })
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))))
              ⋯) ∘
          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))))
            ⋯)
        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 (α := { p : Ideal B // p ∣ L })
    (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)
              (↑(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))))
                      ⋯ :
                    { p : Ideal A // p ∣ J }) :
                Ideal A))))
        ⋯ :
      { 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 (α := { p : Ideal B // p ∣ L })
    (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)
              (↑(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))))
                      ⋯ :
                    { p : Ideal A // p ∣ J }) :
                Ideal A))))
        ⋯ :
      { p : Ideal B // p ∣ L })
    (({
            toFun := fun (X : { p : Ideal R // p ∣ I }) ↦
              Subtype.mk (p := fun (p : Ideal B) ↦ p ∣ L)
                (comap (F := B →+* B ⧸ L) (Ideal.Quotient.mk L)
                  (map (R := R ⧸ I) (g.comp f) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) (↑X : Ideal R))))
                ⋯,
            monotone' := ⋯ } :
          (a : { p : Ideal R // p ∣ I }) → { p : Ideal B // p ∣ L })
        x :
      { p : Ideal B // p ∣ L })
rw₇ :
  Eq (α := { p : Ideal B // p ∣ L })
    (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)
              (↑(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))))
                      ⋯ :
                    { p : Ideal A // p ∣ J }) :
                Ideal A))))
        ⋯ :
      { p : Ideal B // p ∣ L })
    (Subtype.mk (p := fun (p : Ideal B) ↦ p ∣ L)
        (comap (F := B →+* B ⧸ L) (Ideal.Quotient.mk L)
          (map (R := R ⧸ I) (g.comp f) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) (↑x : Ideal R))))
        ⋯ :
      { p : Ideal B // p ∣ L })
rw₈ :
  Eq (α := Ideal B)
    (comap (F := B →+* B ⧸ L) (Ideal.Quotient.mk L)
      (map (R := A ⧸ J) g
        (map (F := A →+* A ⧸ J) (Ideal.Quotient.mk J)
          (↑(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))))
                  ⋯ :
                { p : Ideal A // p ∣ J }) :
            Ideal A))))
    (comap (F := B →+* B ⧸ L) (Ideal.Quotient.mk L)
      (map (R := R ⧸ I) (g.comp f) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) (↑x : Ideal R))))
rw₉ :
  Eq (α := Ideal B)
    (comap (F := B →+* B ⧸ L) (Ideal.Quotient.mk L)
      (map (R := A ⧸ J) g
        (map (F := A →+* A ⧸ J) (Ideal.Quotient.mk 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)))))))
    (comap (F := B →+* B ⧸ L) (Ideal.Quotient.mk L)
      (map (R := R ⧸ I) (g.comp f) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) (↑x : Ideal R))))
rw₁₀ :
  Eq (α := Ideal B)
    (comap (F := B →+* B ⧸ L) (Ideal.Quotient.mk L)
      (map (R := A ⧸ J) g (map (R := R ⧸ I) f (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) (↑x : Ideal R)))))
    (comap (F := B →+* B ⧸ L) (Ideal.Quotient.mk L)
      (map (R := R ⧸ I) (g.comp f) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) (↑x : Ideal R))))
rw₁₁ rw₁₂ :
  Eq (α := Ideal B)
    (comap (F := B →+* B ⧸ L) (Ideal.Quotient.mk L)
      (map (R := R ⧸ I) (g.comp f) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) (↑x : Ideal R))))
    (comap (F := B →+* B ⧸ L) (Ideal.Quotient.mk L)
      (map (R := R ⧸ I) (g.comp f) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) (↑x : Ideal R))))
⊢ 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 })

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]

Premises used: Subtype.coe_mk, Ideal.Quotient.mk, IsDedekindDomain.idealFactorsFunOfQuotHom, OrderHom.coe_mk, Ideal.Quotient.mk_surjective, Ideal.map_map, OrderHom.comp_coe, Subtype.mk_eq_mk, Function.comp_apply, Ideal.map_comap_of_surjective