case refine'_1
C : Type u_3
D : Type u_4
E : Type u_6
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
F : C ⥤ Karoubi D
G : D ⥤ Karoubi E
⊢ ∀ (X : Karoubi C),
    ((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).obj X =
      ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).obj X

case refine'_2
C : Type u_3
D : Type u_4
E : Type u_6
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
F : C ⥤ Karoubi D
G : D ⥤ Karoubi E
⊢ ∀ (X Y : Karoubi C) (f : X ⟶ Y),
    ((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).map f =
      eqToHom (_ : ?m.64538.obj X = ?m.64539.obj X) ≫
        ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).map f ≫
          eqToHom
            (_ :
              ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).obj Y =
                ((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).obj Y)
C : Type u_3
D : Type u_4
E : Type u_6
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
F : C ⥤ Karoubi D
G : D ⥤ Karoubi E
⊢ (functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G) =
    (functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G
refine' Functor.ext _ _
case refine'_2
C : Type u_3
D : Type u_4
E : Type u_6
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
F : C ⥤ Karoubi D
G : D ⥤ Karoubi E
⊢ ∀ (X Y : Karoubi C) (f : X ⟶ Y),
    ((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).map f =
      eqToHom
          (_ :
            ((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).obj X =
              ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).obj X) ≫
        ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).map f ≫
          eqToHom
            (_ :
              ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).obj Y =
                ((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).obj Y)
case refine'_1
C : Type u_3
D : Type u_4
E : Type u_6
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
F : C ⥤ Karoubi D
G : D ⥤ Karoubi E
⊢ ∀ (X : Karoubi C),
    ((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).obj X =
      ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).obj X

case refine'_2
C : Type u_3
D : Type u_4
E : Type u_6
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
F : C ⥤ Karoubi D
G : D ⥤ Karoubi E
⊢ ∀ (X Y : Karoubi C) (f : X ⟶ Y),
    ((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).map f =
      eqToHom (_ : ?m.64538.obj X = ?m.64539.obj X) ≫
        ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).map f ≫
          eqToHom
            (_ :
              ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).obj Y =
                ((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).obj Y)
. aesop_cat
no goals
case refine'_2
C : Type u_3
D : Type u_4
E : Type u_6
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
F : C ⥤ Karoubi D
G : D ⥤ Karoubi E
⊢ ∀ (X Y : Karoubi C) (f : X ⟶ Y),
    ((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).map f =
      eqToHom
          (_ :
            ((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).obj X =
              ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).obj X) ≫
        ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).map f ≫
          eqToHom
            (_ :
              ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).obj Y =
                ((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).obj Y)
. intro X Y f
  ext
  simp only [eqToHom_refl, id_comp, comp_id]
  rfl
no goals
case refine'_1
C : Type u_3
D : Type u_4
E : Type u_6
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
F : C ⥤ Karoubi D
G : D ⥤ Karoubi E
⊢ ∀ (X : Karoubi C),
    ((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).obj X =
      ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).obj X
aesop_cat
case refine'_2
C : Type u_3
D : Type u_4
E : Type u_6
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
F : C ⥤ Karoubi D
G : D ⥤ Karoubi E
X Y : Karoubi C
f : X ⟶ Y
⊢ ((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).map f =
    eqToHom
        (_ :
          ((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).obj X =
            ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).obj X) ≫
      ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).map f ≫
        eqToHom
          (_ :
            ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).obj Y =
              ((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).obj Y)
case refine'_2
C : Type u_3
D : Type u_4
E : Type u_6
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
F : C ⥤ Karoubi D
G : D ⥤ Karoubi E
⊢ ∀ (X Y : Karoubi C) (f : X ⟶ Y),
    ((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).map f =
      eqToHom
          (_ :
            ((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).obj X =
              ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).obj X) ≫
        ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).map f ≫
          eqToHom
            (_ :
              ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).obj Y =
                ((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).obj Y)
intro X Y f
case refine'_2.h
C : Type u_3
D : Type u_4
E : Type u_6
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
F : C ⥤ Karoubi D
G : D ⥤ Karoubi E
X Y : Karoubi C
f : X ⟶ Y
⊢ (((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).map f).f =
    (eqToHom
          (_ :
            ((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).obj X =
              ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).obj X) ≫
        ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).map f ≫
          eqToHom
            (_ :
              ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).obj Y =
                ((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).obj Y)).f
case refine'_2
C : Type u_3
D : Type u_4
E : Type u_6
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
F : C ⥤ Karoubi D
G : D ⥤ Karoubi E
X Y : Karoubi C
f : X ⟶ Y
⊢ ((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).map f =
    eqToHom
        (_ :
          ((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).obj X =
            ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).obj X) ≫
      ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).map f ≫
        eqToHom
          (_ :
            ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).obj Y =
              ((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).obj Y)
ext
case refine'_2.h
C : Type u_3
D : Type u_4
E : Type u_6
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
F : C ⥤ Karoubi D
G : D ⥤ Karoubi E
X Y : Karoubi C
f : X ⟶ Y
⊢ (((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).map f).f =
    (((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).map f).f
case refine'_2.h
C : Type u_3
D : Type u_4
E : Type u_6
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
F : C ⥤ Karoubi D
G : D ⥤ Karoubi E
X Y : Karoubi C
f : X ⟶ Y
⊢ (((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).map f).f =
    (eqToHom
          (_ :
            ((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).obj X =
              ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).obj X) ≫
        ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).map f ≫
          eqToHom
            (_ :
              ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).obj Y =
                ((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).obj Y)).f
simp only [eqToHom_refl, id_comp, comp_id]
no goals
case refine'_2.h
C : Type u_3
D : Type u_4
E : Type u_6
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
F : C ⥤ Karoubi D
G : D ⥤ Karoubi E
X Y : Karoubi C
f : X ⟶ Y
⊢ (((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).map f).f =
    (((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).map f).f
rfl