C : Type u_3
D : Type u_4
E : Type ?u.84970
inst✝³ : Category C
inst✝² : Category D
inst✝¹ : Category E
inst✝ : IsIdempotentComplete D
F G : Karoubi C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
P : Karoubi C
⊢ F.map (decompId_i P) ≫
      (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ).app (Karoubi.mk P.X (𝟙 P.X)) ≫
        G.map (decompId_p P) =
    F.map (decompId_i P) ≫ τ.app P.X ≫ G.map (decompId_p P)
C : Type u_3
D : Type u_4
E : Type ?u.84970
inst✝³ : Category C
inst✝² : Category D
inst✝¹ : Category E
inst✝ : IsIdempotentComplete D
F G : Karoubi C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
P : Karoubi C
⊢ (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ).app P =
    F.map (decompId_i P) ≫ τ.app P.X ≫ G.map (decompId_p P)
rw [natTrans_eq]
case e_a.e_a
C : Type u_3
D : Type u_4
E : Type ?u.84970
inst✝³ : Category C
inst✝² : Category D
inst✝¹ : Category E
inst✝ : IsIdempotentComplete D
F G : Karoubi C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
P : Karoubi C
⊢ (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ).app (Karoubi.mk P.X (𝟙 P.X)) = τ.app P.X
C : Type u_3
D : Type u_4
E : Type ?u.84970
inst✝³ : Category C
inst✝² : Category D
inst✝¹ : Category E
inst✝ : IsIdempotentComplete D
F G : Karoubi C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
P : Karoubi C
⊢ F.map (decompId_i P) ≫
      (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ).app (Karoubi.mk P.X (𝟙 P.X)) ≫
        G.map (decompId_p P) =
    F.map (decompId_i P) ≫ τ.app P.X ≫ G.map (decompId_p P)
congr 2
case e_a.e_a
C : Type u_3
D : Type u_4
E : Type ?u.84970
inst✝³ : Category C
inst✝² : Category D
inst✝¹ : Category E
inst✝ : IsIdempotentComplete D
F G : Karoubi C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
P : Karoubi C
⊢ (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ).app (Karoubi.mk P.X (𝟙 P.X)) =
    (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).map
          (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ)).app
      P.X
case e_a.e_a
C : Type u_3
D : Type u_4
E : Type ?u.84970
inst✝³ : Category C
inst✝² : Category D
inst✝¹ : Category E
inst✝ : IsIdempotentComplete D
F G : Karoubi C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
P : Karoubi C
⊢ (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ).app (Karoubi.mk P.X (𝟙 P.X)) = τ.app P.X
rw [← congr_app (((whiskeringLeft _ _ _).obj (toKaroubi _)).image_preimage τ) P.X]
case e_a.e_a
C : Type u_3
D : Type u_4
E : Type ?u.84970
inst✝³ : Category C
inst✝² : Category D
inst✝¹ : Category E
inst✝ : IsIdempotentComplete D
F G : Karoubi C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
P : Karoubi C
⊢ (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ).app (Karoubi.mk P.X (𝟙 P.X)) =
    (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ).app ((toKaroubi C).obj P.X)
case e_a.e_a
C : Type u_3
D : Type u_4
E : Type ?u.84970
inst✝³ : Category C
inst✝² : Category D
inst✝¹ : Category E
inst✝ : IsIdempotentComplete D
F G : Karoubi C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
P : Karoubi C
⊢ (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ).app (Karoubi.mk P.X (𝟙 P.X)) =
    (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).map
          (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ)).app
      P.X
dsimp
no goals
case e_a.e_a
C : Type u_3
D : Type u_4
E : Type ?u.84970
inst✝³ : Category C
inst✝² : Category D
inst✝¹ : Category E
inst✝ : IsIdempotentComplete D
F G : Karoubi C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
P : Karoubi C
⊢ (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ).app (Karoubi.mk P.X (𝟙 P.X)) =
    (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ).app ((toKaroubi C).obj P.X)
congr