-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CompatibleSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
F : Functor.{v_1, v_2, u_1, u_2} D E
inst_3 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_4 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_5 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_6 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst_7 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst_8 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ D
rw :
  Eq (α := P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))
    (CategoryStruct.comp (Y := J.plusObj P ⋙ F) (whiskerRight (J.toPlus P) F : P ⋙ F ⟶ J.plusObj P ⋙ F)
        (CategoryStruct.comp (Y := J.plusObj (P ⋙ F))
            (Iso.hom (J.plusCompIso F P) : J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ F))
            (CategoryStruct.comp (Y := J.plusObj (J.plusObj P ⋙ F))
                (J.plusMap (whiskerRight (J.toPlus P) F) : J.plusObj (P ⋙ F) ⟶ J.plusObj (J.plusObj P ⋙ F))
                (J.plusMap (Iso.hom (J.plusCompIso F P)) :
                  J.plusObj (J.plusObj P ⋙ F) ⟶ J.plusObj (J.plusObj (P ⋙ F))) :
              J.plusObj (P ⋙ F) ⟶ J.plusObj (J.plusObj (P ⋙ F))) :
          J.plusObj P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F))) :
      P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))
    (J.toPlus (P ⋙ F) ≫ J.plusMap (J.toPlus (P ⋙ F)) : P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))
rw₁ :
  Eq (α := P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))
    (CategoryStruct.comp (Y := J.plusObj P ⋙ F) (whiskerRight (J.toPlus P) F : P ⋙ F ⟶ J.plusObj P ⋙ F)
        (CategoryStruct.comp (Y := J.plusObj (P ⋙ F))
            (Iso.hom (J.plusCompIso F P) : J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ F))
            (J.plusMap
                (CategoryStruct.comp (Y := J.plusObj P ⋙ F) (whiskerRight (J.toPlus P) F : P ⋙ F ⟶ J.plusObj P ⋙ F)
                  (Iso.hom (J.plusCompIso F P) : J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ F))) :
              J.plusObj (P ⋙ F) ⟶ J.plusObj (J.plusObj (P ⋙ F))) :
          J.plusObj P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F))) :
      P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))
    (J.toPlus (P ⋙ F) ≫ J.plusMap (J.toPlus (P ⋙ F)) : P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))
⊢ Eq (α := P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))
    (CategoryStruct.comp (Y := J.plusObj P ⋙ F) (whiskerRight (J.toPlus P) F : P ⋙ F ⟶ J.plusObj P ⋙ F)
        (CategoryStruct.comp (Y := J.plusObj (J.plusObj P ⋙ F))
            (CategoryStruct.comp (Y := J.plusObj (P ⋙ F))
                (Iso.hom (J.plusCompIso F P) : J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ F))
                (J.plusMap (whiskerRight (J.toPlus P) F) : J.plusObj (P ⋙ F) ⟶ J.plusObj (J.plusObj P ⋙ F)) :
              J.plusObj P ⋙ F ⟶ J.plusObj (J.plusObj P ⋙ F))
            (J.plusMap (Iso.hom (J.plusCompIso F P)) : J.plusObj (J.plusObj P ⋙ F) ⟶ J.plusObj (J.plusObj (P ⋙ F))) :
          J.plusObj P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F))) :
      P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))
    (J.toPlus (P ⋙ F) ≫ J.plusMap (J.toPlus (P ⋙ F)) : P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))
have rw₂ : Eq (α := P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))
  (CategoryStruct.comp (Y := J.plusObj P ⋙ F) (whiskerRight (J.toPlus P) F : P ⋙ F ⟶ J.plusObj P ⋙ F)
      (CategoryStruct.comp (Y := J.plusObj (P ⋙ F)) (Iso.hom (J.plusCompIso F P) : J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ F))
          (J.plusMap (J.toPlus (P ⋙ F)) : J.plusObj (P ⋙ F) ⟶ J.plusObj (J.plusObj (P ⋙ F))) :
        J.plusObj P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F))) :
    P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))
  (J.toPlus (P ⋙ F) ≫ J.plusMap (J.toPlus (P ⋙ F)) : P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))
Tactic: rw [Category.assoc, ← J.plusMap_comp, whiskerRight_toPlus_comp_plusCompIso_hom, ←
    Category.assoc, whiskerRight_toPlus_comp_plusCompIso_hom]