Lean4
/-- The counit isomorphism of the equivalence `(C ⥤ Karoubi D) ≌ (Karoubi C ⥤ Karoubi D)`. -/
def counitIso : (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) ⋙ functorExtension₁ C D ≅ 𝟭 _ :=
NatIso.ofComponents
(fun G =>
{ hom :=
{ app := fun P =>
{ f := (G.map (decompId_p P)).f
comm := by
simpa only [hom_ext_iff, G.map_comp, G.map_id] using
G.congr_map (show (toKaroubi C).map P.p ≫ P.decompId_p ≫ 𝟙 _ = P.decompId_p by simp) }
naturality := fun P Q f => by
simpa only [hom_ext_iff, G.map_comp] using (G.congr_map (decompId_p_naturality f)).symm }
inv :=
{ app := fun P =>
{ f := (G.map (decompId_i P)).f
comm := by
simpa only [hom_ext_iff, G.map_comp, G.map_id] using
G.congr_map (show 𝟙 _ ≫ P.decompId_i ≫ (toKaroubi C).map P.p = P.decompId_i by simp) }
naturality := fun P Q f => by
simpa only [hom_ext_iff, G.map_comp] using G.congr_map (decompId_i_naturality f) }
hom_inv_id := by
ext P
simpa only [hom_ext_iff, G.map_comp, G.map_id] using G.congr_map P.decomp_p.symm
inv_hom_id := by
ext P
simpa only [hom_ext_iff, G.map_comp, G.map_id] using G.congr_map P.decompId.symm })
(fun {X Y} φ => by
ext P
dsimp
rw [natTrans_eq φ P, P.decomp_p]
simp only [Functor.map_comp, comp_f, assoc]
rfl)
