-- Mathlib/CategoryTheory/Sites/CompatiblePlus.lean
theorem ι_plusCompIso_hom (X) (W) :
    F.map (colimit.ι _ W) ≫ (J.plusCompIso F P).hom.app X =
      (J.diagramCompIso F P X.unop).hom.app W ≫ colimit.ι _ W

Proof state:
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} 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) ≫ (J.plusCompIso F P).hom.app X =
    (J.diagramCompIso F P (unop X)).hom.app W ≫ colimit.ι (J.diagram (P ⋙ F) (unop X)) W

Tactic:
delta diagramCompIso plusCompIso

Result:
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} 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

Proof state:
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} 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))ᵒᵖ
⊢ (colimit.cocone (J.diagram P (unop X) ⋙ F)).ι.app W ≫
      (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

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} 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

Tactic:
erw [(isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop X)))).fac]

Result:
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} 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))ᵒᵖ
⊢ (colimit.cocone (J.diagram P (unop X) ⋙ F)).ι.app W ≫
      (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