Module: Mathlib.CategoryTheory.Sites.CompatiblePlus

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
X : Cᵒᵖ
W : (J.Cover (unop X))ᵒᵖ
⊢ F.map (colimit.ι (J.diagram P (unop X)) W) ≫
      (NatIso.ofComponents
              (fun X ↦
                (isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop X)))).coconePointUniqueUpToIso
                    (colimit.isColimit (J.diagram P (unop X) ⋙ F)) ≪≫
                  HasColimit.isoOfNatIso
                    (NatIso.ofComponents
                      (fun W ↦
                        (isLimitOfPreserves F (limit.isLimit ((unop W).index P).multicospan)).conePointUniqueUpToIso
                            (limit.isLimit (((unop W).index P).multicospan ⋙ F)) ≪≫
                          HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop W)).symm)
                      ⋯))
              ⋯).hom.app
        X =
    (NatIso.ofComponents
              (fun W ↦
                (isLimitOfPreserves F (limit.isLimit ((unop W).index P).multicospan)).conePointUniqueUpToIso
                    (limit.isLimit (((unop W).index P).multicospan ⋙ F)) ≪≫
                  HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop W)).symm)
              ⋯).hom.app
        W ≫
      colimit.ι (J.diagram (P ⋙ F) (unop X)) W

Tactic:
simp only [Iso.trans_hom, NatIso.ofComponents_hom_app, ←
    Category.assoc]

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
X : Cᵒᵖ
W : (J.Cover (unop X))ᵒᵖ
⊢ (F.map (colimit.ι (J.diagram P (unop X)) W) ≫
        ((isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop X)))).coconePointUniqueUpToIso
            (colimit.isColimit (J.diagram P (unop X) ⋙ F))).hom) ≫
      (HasColimit.isoOfNatIso
          (NatIso.ofComponents
            (fun W ↦
              (isLimitOfPreserves F (limit.isLimit ((unop W).index P).multicospan)).conePointUniqueUpToIso
                  (limit.isLimit (((unop W).index P).multicospan ⋙ F)) ≪≫
                HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop W)).symm)
            ⋯)).hom =
    (((isLimitOfPreserves F (limit.isLimit ((unop W).index P).multicospan)).conePointUniqueUpToIso
            (limit.isLimit (((unop W).index P).multicospan ⋙ F))).hom ≫
        (HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop W)).symm).hom) ≫
      colimit.ι (J.diagram (P ⋙ F) (unop X)) W