case refine'_1
C : Type u_1
D : Type u_2
E : Type ?u.30040
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
⊢ ∀ (X : C ⥤ Karoubi D),
    (functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj X =
      (𝟭 (C ⥤ Karoubi D)).obj X

case refine'_2
C : Type u_1
D : Type u_2
E : Type ?u.30040
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
⊢ ∀ (X Y : C ⥤ Karoubi D) (f : X ⟶ Y),
    (functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).map f =
      eqToHom (_ : ?m.30774.obj X = ?m.30775.obj X) ≫
        (𝟭 (C ⥤ Karoubi D)).map f ≫
          eqToHom
            (_ :
              (𝟭 (C ⥤ Karoubi D)).obj Y =
                (functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj Y)
C : Type u_1
D : Type u_2
E : Type ?u.30040
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
⊢ functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) = 𝟭 (C ⥤ Karoubi D)
refine' Functor.ext _ _
case refine'_1
C : Type u_1
D : Type u_2
E : Type ?u.30040
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
F : C ⥤ Karoubi D
⊢ (functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj F =
    (𝟭 (C ⥤ Karoubi D)).obj F
case refine'_1
C : Type u_1
D : Type u_2
E : Type ?u.30040
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
⊢ ∀ (X : C ⥤ Karoubi D),
    (functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj X =
      (𝟭 (C ⥤ Karoubi D)).obj X
intro F
case refine'_1.refine'_1
C : Type u_1
D : Type u_2
E : Type ?u.30040
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
F : C ⥤ Karoubi D
⊢ ∀ (X : C),
    ((functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj F).obj X =
      ((𝟭 (C ⥤ Karoubi D)).obj F).obj X

case refine'_1.refine'_2
C : Type u_1
D : Type u_2
E : Type ?u.30040
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
F : C ⥤ Karoubi D
⊢ ∀ (X Y : C) (f : X ⟶ Y),
    ((functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj F).map f =
      eqToHom (_ : ?m.31081.obj X = ?m.31082.obj X) ≫
        ((𝟭 (C ⥤ Karoubi D)).obj F).map f ≫
          eqToHom
            (_ :
              ((𝟭 (C ⥤ Karoubi D)).obj F).obj Y =
                ((functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj F).obj Y)
case refine'_1
C : Type u_1
D : Type u_2
E : Type ?u.30040
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
F : C ⥤ Karoubi D
⊢ (functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj F =
    (𝟭 (C ⥤ Karoubi D)).obj F
refine' Functor.ext _ _
case refine'_1.refine'_1
C : Type u_1
D : Type u_2
E : Type ?u.30040
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
F : C ⥤ Karoubi D
X : C
⊢ ((functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj F).obj X =
    ((𝟭 (C ⥤ Karoubi D)).obj F).obj X
case refine'_1.refine'_1
C : Type u_1
D : Type u_2
E : Type ?u.30040
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
F : C ⥤ Karoubi D
⊢ ∀ (X : C),
    ((functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj F).obj X =
      ((𝟭 (C ⥤ Karoubi D)).obj F).obj X
intro X
case refine'_1.refine'_1.h_p
C : Type u_1
D : Type u_2
E : Type ?u.30040
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
F : C ⥤ Karoubi D
X : C
⊢ (((functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj F).obj X).p ≫
      eqToHom ?refine'_1.refine'_1.h_X =
    eqToHom ?refine'_1.refine'_1.h_X ≫ (((𝟭 (C ⥤ Karoubi D)).obj F).obj X).p

case refine'_1.refine'_1.h_X
C : Type u_1
D : Type u_2
E : Type ?u.30040
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
F : C ⥤ Karoubi D
X : C
⊢ (((functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj F).obj X).X =
    (((𝟭 (C ⥤ Karoubi D)).obj F).obj X).X
case refine'_1.refine'_1
C : Type u_1
D : Type u_2
E : Type ?u.30040
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
F : C ⥤ Karoubi D
X : C
⊢ ((functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj F).obj X =
    ((𝟭 (C ⥤ Karoubi D)).obj F).obj X
ext
case refine'_1.refine'_1.h_X
C : Type u_1
D : Type u_2
E : Type ?u.30040
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
F : C ⥤ Karoubi D
X : C
⊢ (((functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj F).obj X).X =
    (((𝟭 (C ⥤ Karoubi D)).obj F).obj X).X
case refine'_1.refine'_1.h_p
C : Type u_1
D : Type u_2
E : Type ?u.30040
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
F : C ⥤ Karoubi D
X : C
⊢ (((functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj F).obj X).p ≫
      eqToHom ?refine'_1.refine'_1.h_X =
    eqToHom ?refine'_1.refine'_1.h_X ≫ (((𝟭 (C ⥤ Karoubi D)).obj F).obj X).p

case refine'_1.refine'_1.h_X
C : Type u_1
D : Type u_2
E : Type ?u.30040
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
F : C ⥤ Karoubi D
X : C
⊢ (((functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj F).obj X).X =
    (((𝟭 (C ⥤ Karoubi D)).obj F).obj X).X
. simp
no goals
case refine'_1.refine'_1.h_X
C : Type u_1
D : Type u_2
E : Type ?u.30040
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
F : C ⥤ Karoubi D
X : C
⊢ (((functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj F).obj X).X =
    (((𝟭 (C ⥤ Karoubi D)).obj F).obj X).X
. simp
no goals
case refine'_1.refine'_1.h_p
C : Type u_1
D : Type u_2
E : Type ?u.30040
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
F : C ⥤ Karoubi D
X : C
⊢ (((functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj F).obj X).p ≫
      eqToHom ?refine'_1.refine'_1.h_X =
    eqToHom ?refine'_1.refine'_1.h_X ≫ (((𝟭 (C ⥤ Karoubi D)).obj F).obj X).p
simp
no goals
case refine'_1.refine'_1.h_X
C : Type u_1
D : Type u_2
E : Type ?u.30040
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
F : C ⥤ Karoubi D
X : C
⊢ (((functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj F).obj X).X =
    (((𝟭 (C ⥤ Karoubi D)).obj F).obj X).X
simp
no goals
case refine'_1.refine'_2
C : Type u_1
D : Type u_2
E : Type ?u.30040
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
F : C ⥤ Karoubi D
⊢ ∀ (X Y : C) (f : X ⟶ Y),
    ((functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj F).map f =
      eqToHom
          (_ :
            ((functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj F).obj X =
              ((𝟭 (C ⥤ Karoubi D)).obj F).obj X) ≫
        ((𝟭 (C ⥤ Karoubi D)).obj F).map f ≫
          eqToHom
            (_ :
              ((𝟭 (C ⥤ Karoubi D)).obj F).obj Y =
                ((functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj F).obj Y)
aesop_cat
case refine'_2
C : Type u_1
D : Type u_2
E : Type ?u.30040
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
F G : C ⥤ Karoubi D
φ : F ⟶ G
⊢ (functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).map φ =
    eqToHom
        (_ :
          (functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj F =
            (𝟭 (C ⥤ Karoubi D)).obj F) ≫
      (𝟭 (C ⥤ Karoubi D)).map φ ≫
        eqToHom
          (_ :
            (𝟭 (C ⥤ Karoubi D)).obj G =
              (functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj G)
case refine'_2
C : Type u_1
D : Type u_2
E : Type ?u.30040
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
⊢ ∀ (X Y : C ⥤ Karoubi D) (f : X ⟶ Y),
    (functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).map f =
      eqToHom
          (_ :
            (functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj X =
              (𝟭 (C ⥤ Karoubi D)).obj X) ≫
        (𝟭 (C ⥤ Karoubi D)).map f ≫
          eqToHom
            (_ :
              (𝟭 (C ⥤ Karoubi D)).obj Y =
                (functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj Y)
intro F G φ
no goals
case refine'_2
C : Type u_1
D : Type u_2
E : Type ?u.30040
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
F G : C ⥤ Karoubi D
φ : F ⟶ G
⊢ (functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).map φ =
    eqToHom
        (_ :
          (functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj F =
            (𝟭 (C ⥤ Karoubi D)).obj F) ≫
      (𝟭 (C ⥤ Karoubi D)).map φ ≫
        eqToHom
          (_ :
            (𝟭 (C ⥤ Karoubi D)).obj G =
              (functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj G)
aesop_cat