-- Mathlib/CategoryTheory/Sites/CompatiblePlus.lean
theorem plusCompIso_whiskerRight {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) :
    whiskerRight (J.plusMap η) F ≫ (J.plusCompIso F Q).hom =
      (J.plusCompIso F P).hom ≫ J.plusMap (whiskerRight η F)

Proof state:
case w.h
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
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : Cᵒᵖ
W : (J.Cover (unop X))ᵒᵖ
⊢ (F.map
          (Multiequalizer.lift ((unop W).index Q) (multiequalizer ((unop W).index P))
            (fun x => Multiequalizer.ι ((unop W).index P) x ≫ η.app (op x.Y)) ⋯) ≫
        (J.diagramCompIso F Q (unop X)).hom.app W) ≫
      colimit.ι (J.diagram (Q ⋙ F) (unop X)) W =
    ((J.diagramCompIso F P (unop X)).hom.app W ≫
        Multiequalizer.lift ((unop W).index (Q ⋙ F)) (multiequalizer ((unop W).index (P ⋙ F)))
          (fun x => Multiequalizer.ι ((unop W).index (P ⋙ F)) x ≫ F.map (η.app (op x.Y))) ⋯) ≫
      colimit.ι (J.diagram (Q ⋙ F) (unop X)) W

Tactic:
congr 1

Result:
case w.h.e_a
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
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : Cᵒᵖ
W : (J.Cover (unop X))ᵒᵖ
⊢ F.map
        (Multiequalizer.lift ((unop W).index Q) (multiequalizer ((unop W).index P))
          (fun x => Multiequalizer.ι ((unop W).index P) x ≫ η.app (op x.Y)) ⋯) ≫
      (J.diagramCompIso F Q (unop X)).hom.app W =
    (J.diagramCompIso F P (unop X)).hom.app W ≫
      Multiequalizer.lift ((unop W).index (Q ⋙ F)) (multiequalizer ((unop W).index (P ⋙ F)))
        (fun x => Multiequalizer.ι ((unop W).index (P ⋙ F)) x ≫ F.map (η.app (op x.Y))) ⋯

Proof state:
case w.h
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
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : Cᵒᵖ
⊢ ∀ (j : (J.Cover (unop X))ᵒᵖ),
    (F.mapCocone (colimit.cocone (J.diagram P (unop X)))).ι.app j ≫
        (whiskerRight (J.plusMap η) F ≫ (J.plusCompIso F Q).hom).app X =
      (F.mapCocone (colimit.cocone (J.diagram P (unop X)))).ι.app j ≫
        ((J.plusCompIso F P).hom ≫ J.plusMap (whiskerRight η F)).app X

Tactic:
intro W

Result:
case w.h
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
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : Cᵒᵖ
W : (J.Cover (unop X))ᵒᵖ
⊢ (F.mapCocone (colimit.cocone (J.diagram P (unop X)))).ι.app W ≫
      (whiskerRight (J.plusMap η) F ≫ (J.plusCompIso F Q).hom).app X =
    (F.mapCocone (colimit.cocone (J.diagram P (unop X)))).ι.app W ≫
      ((J.plusCompIso F P).hom ≫ J.plusMap (whiskerRight η F)).app X

Proof state:
case w.h
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
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : Cᵒᵖ
W : (J.Cover (unop X))ᵒᵖ
⊢ F.map (((Cocones.precompose (J.diagramNatTrans η (unop X))).obj (colimit.cocone (J.diagram Q (unop X)))).ι.app W) ≫
      (J.plusCompIso F Q).hom.app X =
    ((J.diagramCompIso F P (unop X)).hom.app W ≫
        Multiequalizer.lift ((unop W).index (Q ⋙ F)) (multiequalizer ((unop W).index (P ⋙ F)))
          (fun x => Multiequalizer.ι ((unop W).index (P ⋙ F)) x ≫ F.map (η.app (op x.Y))) ⋯) ≫
      colimit.ι (J.diagram (Q ⋙ F) (unop X)) W

Tactic:
dsimp [Cocones.precompose]

Result:
case w.h
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
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : Cᵒᵖ
W : (J.Cover (unop X))ᵒᵖ
⊢ F.map
        (Multiequalizer.lift ((unop W).index Q) (multiequalizer ((unop W).index P))
            (fun x => Multiequalizer.ι ((unop W).index P) x ≫ η.app (op x.Y)) ⋯ ≫
          colimit.ι (J.diagram Q (unop X)) W) ≫
      (J.plusCompIso F Q).hom.app X =
    ((J.diagramCompIso F P (unop X)).hom.app W ≫
        Multiequalizer.lift ((unop W).index (Q ⋙ F)) (multiequalizer ((unop W).index (P ⋙ F)))
          (fun x => Multiequalizer.ι ((unop W).index (P ⋙ F)) x ≫ F.map (η.app (op x.Y))) ⋯) ≫
      colimit.ι (J.diagram (Q ⋙ F) (unop X)) W