[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.41, u_3} E
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
⊢ NatTrans.app φ P = F.map (decompId_i P) ≫ NatTrans.app φ (Karoubi.mk P.X (𝟙 P.X)) ≫ G.map (decompId_p P)
[PROOFSTEP]
rw [← φ.naturality, ← assoc, ← F.map_comp]
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.41, u_3} E
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
⊢ NatTrans.app φ P = F.map (decompId_i P ≫ decompId_p P) ≫ NatTrans.app φ P
[PROOFSTEP]
conv =>
  lhs
  rw [← id_comp (φ.app P), ← F.map_id]
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.41, u_3} E
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
| NatTrans.app φ P = F.map (decompId_i P ≫ decompId_p P) ≫ NatTrans.app φ P
[PROOFSTEP]
  lhs
  rw [← id_comp (φ.app P), ← F.map_id]
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.41, u_3} E
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
| NatTrans.app φ P = F.map (decompId_i P ≫ decompId_p P) ≫ NatTrans.app φ P
[PROOFSTEP]
  lhs
  rw [← id_comp (φ.app P), ← F.map_id]
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.41, u_3} E
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
| NatTrans.app φ P = F.map (decompId_i P ≫ decompId_p P) ≫ NatTrans.app φ P
[PROOFSTEP]
lhs
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.41, u_3} E
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
| NatTrans.app φ P
[PROOFSTEP]
rw [← id_comp (φ.app P), ← F.map_id]
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.41, u_3} E
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
⊢ F.map (𝟙 P) ≫ NatTrans.app φ P = F.map (decompId_i P ≫ decompId_p P) ≫ NatTrans.app φ P
[PROOFSTEP]
congr
[GOAL]
case e_a.e_a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.41, u_3} E
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
⊢ 𝟙 P = decompId_i P ≫ decompId_p P
[PROOFSTEP]
apply decompId
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.1588, u_1} C
inst✝¹ : Category.{?u.1592, u_2} D
inst✝ : Category.{?u.1596, u_3} E
F : C ⥤ Karoubi D
P : Karoubi C
⊢ (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
[PROOFSTEP]
simpa only [F.map_comp, hom_ext_iff] using F.congr_map P.idem
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.1588, u_1} C
inst✝¹ : Category.{?u.1592, u_2} D
inst✝ : Category.{?u.1596, u_3} E
F : C ⥤ Karoubi D
X✝ Y✝ : Karoubi C
f : X✝ ⟶ Y✝
⊢ (F.map f.f).f =
    ((fun P => Karoubi.mk (F.obj P.X).X (F.map P.p).f) X✝).p ≫
      (F.map f.f).f ≫ ((fun P => Karoubi.mk (F.obj P.X).X (F.map P.p).f) Y✝).p
[PROOFSTEP]
simpa only [F.map_comp, hom_ext_iff] using F.congr_map f.comm
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
P : Karoubi C
⊢ (F.map P.p).f ≫ (NatTrans.app φ P.X).f =
    ((obj F).obj P).p ≫ ((F.map P.p).f ≫ (NatTrans.app φ P.X).f) ≫ ((obj G).obj P).p
[PROOFSTEP]
have h := φ.naturality P.p
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
P : Karoubi C
h : F.map P.p ≫ NatTrans.app φ P.X = NatTrans.app φ P.X ≫ G.map P.p
⊢ (F.map P.p).f ≫ (NatTrans.app φ P.X).f =
    ((obj F).obj P).p ≫ ((F.map P.p).f ≫ (NatTrans.app φ P.X).f) ≫ ((obj G).obj P).p
[PROOFSTEP]
have h' := F.congr_map P.idem
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
P : Karoubi C
h : F.map P.p ≫ NatTrans.app φ P.X = NatTrans.app φ P.X ≫ G.map P.p
h' : F.map (P.p ≫ P.p) = F.map P.p
⊢ (F.map P.p).f ≫ (NatTrans.app φ P.X).f =
    ((obj F).obj P).p ≫ ((F.map P.p).f ≫ (NatTrans.app φ P.X).f) ≫ ((obj G).obj P).p
[PROOFSTEP]
simp only [hom_ext_iff, Karoubi.comp_f, F.map_comp] at h h' 
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
⊢ (F.map P.p).f ≫ (NatTrans.app φ P.X).f =
    ((obj F).obj P).p ≫ ((F.map P.p).f ≫ (NatTrans.app φ P.X).f) ≫ ((obj G).obj P).p
[PROOFSTEP]
simp only [obj_obj_p, assoc, ← h]
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
⊢ (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (F.map P.p).f ≫ (F.map P.p).f ≫ (F.map P.p).f ≫ (NatTrans.app φ P.X).f
[PROOFSTEP]
slice_rhs 1 3 => rw [h', h']
[GOAL]
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (F.map P.p).f ≫ (F.map P.p).f ≫ (F.map P.p).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (NatTrans.app φ P.X).f
[PROOFSTEP]
rw [h', h']
[GOAL]
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (F.map P.p).f ≫ (F.map P.p).f ≫ (F.map P.p).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (NatTrans.app φ P.X).f
[PROOFSTEP]
rw [h', h']
[GOAL]
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (F.map P.p).f ≫ (F.map P.p).f ≫ (F.map P.p).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (NatTrans.app φ P.X).f
[PROOFSTEP]
rw [h', h']
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
⊢ (obj F).map f ≫ (fun P => Hom.mk ((F.map P.p).f ≫ (NatTrans.app φ P.X).f)) x✝ =
    (fun P => Hom.mk ((F.map P.p).f ≫ (NatTrans.app φ P.X).f)) x✝¹ ≫ (obj G).map f
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
⊢ ((obj F).map f ≫ (fun P => Hom.mk ((F.map P.p).f ≫ (NatTrans.app φ P.X).f)) x✝).f =
    ((fun P => Hom.mk ((F.map P.p).f ≫ (NatTrans.app φ P.X).f)) x✝¹ ≫ (obj G).map f).f
[PROOFSTEP]
dsimp [obj]
[GOAL]
case h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
⊢ (F.map f.f).f ≫ (F.map x✝.p).f ≫ (NatTrans.app φ x✝.X).f =
    ((F.map x✝¹.p).f ≫ (NatTrans.app φ x✝¹.X).f) ≫ (G.map f.f).f
[PROOFSTEP]
have h := φ.naturality f.f
[GOAL]
case h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : F.map f.f ≫ NatTrans.app φ x✝.X = NatTrans.app φ x✝¹.X ≫ G.map f.f
⊢ (F.map f.f).f ≫ (F.map x✝.p).f ≫ (NatTrans.app φ x✝.X).f =
    ((F.map x✝¹.p).f ≫ (NatTrans.app φ x✝¹.X).f) ≫ (G.map f.f).f
[PROOFSTEP]
have h' := F.congr_map (comp_p f)
[GOAL]
case h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : F.map f.f ≫ NatTrans.app φ x✝.X = NatTrans.app φ x✝¹.X ≫ G.map f.f
h' : F.map (f.f ≫ x✝.p) = F.map f.f
⊢ (F.map f.f).f ≫ (F.map x✝.p).f ≫ (NatTrans.app φ x✝.X).f =
    ((F.map x✝¹.p).f ≫ (NatTrans.app φ x✝¹.X).f) ≫ (G.map f.f).f
[PROOFSTEP]
have h'' := F.congr_map (p_comp f)
[GOAL]
case h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : F.map f.f ≫ NatTrans.app φ x✝.X = NatTrans.app φ x✝¹.X ≫ G.map f.f
h' : F.map (f.f ≫ x✝.p) = F.map f.f
h'' : F.map (x✝¹.p ≫ f.f) = F.map f.f
⊢ (F.map f.f).f ≫ (F.map x✝.p).f ≫ (NatTrans.app φ x✝.X).f =
    ((F.map x✝¹.p).f ≫ (NatTrans.app φ x✝¹.X).f) ≫ (G.map f.f).f
[PROOFSTEP]
simp only [hom_ext_iff, Functor.map_comp, comp_f] at h h' h'' ⊢
[GOAL]
case h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
⊢ (F.map f.f).f ≫ (F.map x✝.p).f ≫ (NatTrans.app φ x✝.X).f =
    ((F.map x✝¹.p).f ≫ (NatTrans.app φ x✝¹.X).f) ≫ (G.map f.f).f
[PROOFSTEP]
slice_rhs 2 3 => rw [← h]
[GOAL]
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (F.map x✝¹.p).f
[PROOFSTEP]
rw [← h]
[GOAL]
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (F.map x✝¹.p).f
[PROOFSTEP]
rw [← h]
[GOAL]
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (F.map x✝¹.p).f
[PROOFSTEP]
rw [← h]
[GOAL]
case h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
⊢ (F.map f.f).f ≫ (F.map x✝.p).f ≫ (NatTrans.app φ x✝.X).f = (F.map x✝¹.p).f ≫ (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f
[PROOFSTEP]
slice_lhs 1 2 => rw [h']
[GOAL]
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (F.map f.f).f ≫ (F.map x✝.p).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (NatTrans.app φ x✝.X).f
[PROOFSTEP]
rw [h']
[GOAL]
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (F.map f.f).f ≫ (F.map x✝.p).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (NatTrans.app φ x✝.X).f
[PROOFSTEP]
rw [h']
[GOAL]
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (F.map f.f).f ≫ (F.map x✝.p).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (NatTrans.app φ x✝.X).f
[PROOFSTEP]
rw [h']
[GOAL]
case h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
⊢ (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (F.map x✝¹.p).f ≫ (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f
[PROOFSTEP]
slice_rhs 1 2 => rw [h'']
[GOAL]
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (F.map x✝¹.p).f ≫ (F.map f.f).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (NatTrans.app φ x✝.X).f
[PROOFSTEP]
rw [h'']
[GOAL]
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (F.map x✝¹.p).f ≫ (F.map f.f).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (NatTrans.app φ x✝.X).f
[PROOFSTEP]
rw [h'']
[GOAL]
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (F.map x✝¹.p).f ≫ (F.map f.f).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (NatTrans.app φ x✝.X).f
[PROOFSTEP]
rw [h'']
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F : C ⥤ Karoubi D
⊢ { obj := FunctorExtension₁.obj, map := fun {X Y} => FunctorExtension₁.map }.map (𝟙 F) =
    𝟙 ({ obj := FunctorExtension₁.obj, map := fun {X Y} => FunctorExtension₁.map }.obj F)
[PROOFSTEP]
ext P
[GOAL]
case w.h.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F : C ⥤ Karoubi D
P : Karoubi C
⊢ (NatTrans.app ({ obj := FunctorExtension₁.obj, map := fun {X Y} => FunctorExtension₁.map }.map (𝟙 F)) P).f =
    (NatTrans.app (𝟙 ({ obj := FunctorExtension₁.obj, map := fun {X Y} => FunctorExtension₁.map }.obj F)) P).f
[PROOFSTEP]
exact comp_p (F.map P.p)
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
⊢ { obj := FunctorExtension₁.obj, map := fun {X Y} => FunctorExtension₁.map }.map (φ ≫ φ') =
    { obj := FunctorExtension₁.obj, map := fun {X Y} => FunctorExtension₁.map }.map φ ≫
      { obj := FunctorExtension₁.obj, map := fun {X Y} => FunctorExtension₁.map }.map φ'
[PROOFSTEP]
ext P
[GOAL]
case w.h.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
⊢ (NatTrans.app ({ obj := FunctorExtension₁.obj, map := fun {X Y} => FunctorExtension₁.map }.map (φ ≫ φ')) P).f =
    (NatTrans.app
        ({ obj := FunctorExtension₁.obj, map := fun {X Y} => FunctorExtension₁.map }.map φ ≫
          { obj := FunctorExtension₁.obj, map := fun {X Y} => FunctorExtension₁.map }.map φ')
        P).f
[PROOFSTEP]
simp only [comp_f, FunctorExtension₁.map_app_f, NatTrans.comp_app, assoc]
[GOAL]
case w.h.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
⊢ (F.map P.p).f ≫ (NatTrans.app φ P.X).f ≫ (NatTrans.app φ' P.X).f =
    (F.map P.p).f ≫ (NatTrans.app φ P.X).f ≫ (G.map P.p).f ≫ (NatTrans.app φ' P.X).f
[PROOFSTEP]
have h := φ.naturality P.p
[GOAL]
case w.h.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : F.map P.p ≫ NatTrans.app φ P.X = NatTrans.app φ P.X ≫ G.map P.p
⊢ (F.map P.p).f ≫ (NatTrans.app φ P.X).f ≫ (NatTrans.app φ' P.X).f =
    (F.map P.p).f ≫ (NatTrans.app φ P.X).f ≫ (G.map P.p).f ≫ (NatTrans.app φ' P.X).f
[PROOFSTEP]
have h' := F.congr_map P.idem
[GOAL]
case w.h.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : F.map P.p ≫ NatTrans.app φ P.X = NatTrans.app φ P.X ≫ G.map P.p
h' : F.map (P.p ≫ P.p) = F.map P.p
⊢ (F.map P.p).f ≫ (NatTrans.app φ P.X).f ≫ (NatTrans.app φ' P.X).f =
    (F.map P.p).f ≫ (NatTrans.app φ P.X).f ≫ (G.map P.p).f ≫ (NatTrans.app φ' P.X).f
[PROOFSTEP]
simp only [hom_ext_iff, comp_f, F.map_comp] at h h' 
[GOAL]
case w.h.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
⊢ (F.map P.p).f ≫ (NatTrans.app φ P.X).f ≫ (NatTrans.app φ' P.X).f =
    (F.map P.p).f ≫ (NatTrans.app φ P.X).f ≫ (G.map P.p).f ≫ (NatTrans.app φ' P.X).f
[PROOFSTEP]
slice_rhs 2 3 => rw [← h]
[GOAL]
case a.a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (NatTrans.app φ P.X).f ≫ (G.map P.p).f
case a.a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (NatTrans.app φ' P.X).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (F.map P.p).f
[PROOFSTEP]
rw [← h]
[GOAL]
case a.a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (NatTrans.app φ P.X).f ≫ (G.map P.p).f
case a.a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (NatTrans.app φ' P.X).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (F.map P.p).f
[PROOFSTEP]
rw [← h]
[GOAL]
case a.a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (NatTrans.app φ P.X).f ≫ (G.map P.p).f
case a.a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (NatTrans.app φ' P.X).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (F.map P.p).f
[PROOFSTEP]
rw [← h]
[GOAL]
case w.h.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
⊢ (F.map P.p).f ≫ (NatTrans.app φ P.X).f ≫ (NatTrans.app φ' P.X).f =
    (F.map P.p).f ≫ ((F.map P.p).f ≫ (NatTrans.app φ P.X).f) ≫ (NatTrans.app φ' P.X).f
[PROOFSTEP]
slice_rhs 1 2 => rw [h']
[GOAL]
case a.a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (F.map P.p).f ≫ (F.map P.p).f
case a.a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (NatTrans.app φ P.X).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (NatTrans.app φ' P.X).f
[PROOFSTEP]
rw [h']
[GOAL]
case a.a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (F.map P.p).f ≫ (F.map P.p).f
case a.a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (NatTrans.app φ P.X).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (NatTrans.app φ' P.X).f
[PROOFSTEP]
rw [h']
[GOAL]
case a.a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (F.map P.p).f ≫ (F.map P.p).f
case a.a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (NatTrans.app φ P.X).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (NatTrans.app φ' P.X).f
[PROOFSTEP]
rw [h']
[GOAL]
case w.h.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
⊢ (F.map P.p).f ≫ (NatTrans.app φ P.X).f ≫ (NatTrans.app φ' P.X).f =
    ((F.map P.p).f ≫ (NatTrans.app φ P.X).f) ≫ (NatTrans.app φ' P.X).f
[PROOFSTEP]
simp only [assoc]
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.29797, u_3} E
⊢ functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) = 𝟭 (C ⥤ Karoubi D)
[PROOFSTEP]
refine' Functor.ext _ _
[GOAL]
case refine'_1
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.29797, u_3} E
⊢ ∀ (X : C ⥤ Karoubi D),
    (functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj X =
      (𝟭 (C ⥤ Karoubi D)).obj X
[PROOFSTEP]
intro F
[GOAL]
case refine'_1
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.29797, u_3} E
F : C ⥤ Karoubi D
⊢ (functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj F =
    (𝟭 (C ⥤ Karoubi D)).obj F
[PROOFSTEP]
refine' Functor.ext _ _
[GOAL]
case refine'_1.refine'_1
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.29797, u_3} 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
[PROOFSTEP]
intro X
[GOAL]
case refine'_1.refine'_1
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.29797, u_3} 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
[PROOFSTEP]
ext
[GOAL]
case refine'_1.refine'_1.h_X
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.29797, u_3} 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
[PROOFSTEP]
simp
[GOAL]
case refine'_1.refine'_1.h_p
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.29797, u_3} 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 (_ : (F.obj X).X = (F.obj X).X) =
    eqToHom (_ : (F.obj X).X = (F.obj X).X) ≫ (((𝟭 (C ⥤ Karoubi D)).obj F).obj X).p
[PROOFSTEP]
simp
[GOAL]
case refine'_1.refine'_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.29797, u_3} 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)
[PROOFSTEP]
aesop_cat
[GOAL]
case refine'_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.29797, u_3} 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)
[PROOFSTEP]
intro F G φ
[GOAL]
case refine'_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.29797, u_3} 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)
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.49904, u_1} C
inst✝¹ : Category.{?u.49908, u_2} D
inst✝ : Category.{?u.49912, u_3} E
G : Karoubi C ⥤ Karoubi D
P : Karoubi C
⊢ (G.map (decompId_p P)).f =
    ((((whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) ⋙ functorExtension₁ C D).obj G).obj P).p ≫
      (G.map (decompId_p P)).f ≫ (((𝟭 (Karoubi C ⥤ Karoubi D)).obj G).obj P).p
[PROOFSTEP]
simpa only [hom_ext_iff, G.map_comp, G.map_id] using
  G.congr_map (show P.decompId_p = (toKaroubi C).map P.p ≫ P.decompId_p ≫ 𝟙 _ by simp)
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.49904, u_1} C
inst✝¹ : Category.{?u.49908, u_2} D
inst✝ : Category.{?u.49912, u_3} E
G : Karoubi C ⥤ Karoubi D
P : Karoubi C
⊢ decompId_p P = (toKaroubi C).map P.p ≫ decompId_p P ≫ 𝟙 P
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.49904, u_1} C
inst✝¹ : Category.{?u.49908, u_2} D
inst✝ : Category.{?u.49912, u_3} E
G : Karoubi C ⥤ Karoubi D
P Q : Karoubi C
f : P ⟶ Q
⊢ (((whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) ⋙ functorExtension₁ C D).obj G).map f ≫
      (fun P => Hom.mk (G.map (decompId_p P)).f) Q =
    (fun P => Hom.mk (G.map (decompId_p P)).f) P ≫ ((𝟭 (Karoubi C ⥤ Karoubi D)).obj G).map f
[PROOFSTEP]
simpa only [hom_ext_iff, G.map_comp] using (G.congr_map (decompId_p_naturality f)).symm
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.49904, u_1} C
inst✝¹ : Category.{?u.49908, u_2} D
inst✝ : Category.{?u.49912, u_3} E
G : Karoubi C ⥤ Karoubi D
P : Karoubi C
⊢ (G.map (decompId_i P)).f =
    (((𝟭 (Karoubi C ⥤ Karoubi D)).obj G).obj P).p ≫
      (G.map (decompId_i P)).f ≫
        ((((whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) ⋙ functorExtension₁ C D).obj G).obj P).p
[PROOFSTEP]
simpa only [hom_ext_iff, G.map_comp, G.map_id] using
  G.congr_map (show P.decompId_i = 𝟙 _ ≫ P.decompId_i ≫ (toKaroubi C).map P.p by simp)
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.49904, u_1} C
inst✝¹ : Category.{?u.49908, u_2} D
inst✝ : Category.{?u.49912, u_3} E
G : Karoubi C ⥤ Karoubi D
P : Karoubi C
⊢ decompId_i P = 𝟙 P ≫ decompId_i P ≫ (toKaroubi C).map P.p
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.49904, u_1} C
inst✝¹ : Category.{?u.49908, u_2} D
inst✝ : Category.{?u.49912, u_3} E
G : Karoubi C ⥤ Karoubi D
P Q : Karoubi C
f : P ⟶ Q
⊢ ((𝟭 (Karoubi C ⥤ Karoubi D)).obj G).map f ≫ (fun P => Hom.mk (G.map (decompId_i P)).f) Q =
    (fun P => Hom.mk (G.map (decompId_i P)).f) P ≫
      (((whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) ⋙ functorExtension₁ C D).obj G).map f
[PROOFSTEP]
simpa only [hom_ext_iff, G.map_comp] using G.congr_map (decompId_i_naturality f)
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.49904, u_1} C
inst✝¹ : Category.{?u.49908, u_2} D
inst✝ : Category.{?u.49912, u_3} E
G : Karoubi C ⥤ Karoubi D
⊢ ((NatTrans.mk fun P => Hom.mk (G.map (decompId_p P)).f) ≫ NatTrans.mk fun P => Hom.mk (G.map (decompId_i P)).f) =
    𝟙 (((whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) ⋙ functorExtension₁ C D).obj G)
[PROOFSTEP]
ext P
[GOAL]
case w.h.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.49904, u_1} C
inst✝¹ : Category.{?u.49908, u_2} D
inst✝ : Category.{?u.49912, u_3} E
G : Karoubi C ⥤ Karoubi D
P : Karoubi C
⊢ (NatTrans.app
        ((NatTrans.mk fun P => Hom.mk (G.map (decompId_p P)).f) ≫ NatTrans.mk fun P => Hom.mk (G.map (decompId_i P)).f)
        P).f =
    (NatTrans.app (𝟙 (((whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) ⋙ functorExtension₁ C D).obj G))
        P).f
[PROOFSTEP]
simpa only [hom_ext_iff, G.map_comp, G.map_id] using G.congr_map P.decomp_p.symm
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.49904, u_1} C
inst✝¹ : Category.{?u.49908, u_2} D
inst✝ : Category.{?u.49912, u_3} E
G : Karoubi C ⥤ Karoubi D
⊢ ((NatTrans.mk fun P => Hom.mk (G.map (decompId_i P)).f) ≫ NatTrans.mk fun P => Hom.mk (G.map (decompId_p P)).f) =
    𝟙 ((𝟭 (Karoubi C ⥤ Karoubi D)).obj G)
[PROOFSTEP]
ext P
[GOAL]
case w.h.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.49904, u_1} C
inst✝¹ : Category.{?u.49908, u_2} D
inst✝ : Category.{?u.49912, u_3} E
G : Karoubi C ⥤ Karoubi D
P : Karoubi C
⊢ (NatTrans.app
        ((NatTrans.mk fun P => Hom.mk (G.map (decompId_i P)).f) ≫ NatTrans.mk fun P => Hom.mk (G.map (decompId_p P)).f)
        P).f =
    (NatTrans.app (𝟙 ((𝟭 (Karoubi C ⥤ Karoubi D)).obj G)) P).f
[PROOFSTEP]
simpa only [hom_ext_iff, G.map_comp, G.map_id] using G.congr_map P.decompId.symm
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.49904, u_1} C
inst✝¹ : Category.{?u.49908, u_2} D
inst✝ : Category.{?u.49912, u_3} E
X Y : Karoubi C ⥤ Karoubi D
φ : X ⟶ Y
⊢ ((whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) ⋙ functorExtension₁ C D).map φ ≫
      ((fun G =>
            Iso.mk (NatTrans.mk fun P => Hom.mk (G.map (decompId_p P)).f)
              (NatTrans.mk fun P => Hom.mk (G.map (decompId_i P)).f))
          Y).hom =
    ((fun G =>
            Iso.mk (NatTrans.mk fun P => Hom.mk (G.map (decompId_p P)).f)
              (NatTrans.mk fun P => Hom.mk (G.map (decompId_i P)).f))
          X).hom ≫
      (𝟭 (Karoubi C ⥤ Karoubi D)).map φ
[PROOFSTEP]
ext P
[GOAL]
case w.h.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.49904, u_1} C
inst✝¹ : Category.{?u.49908, u_2} D
inst✝ : Category.{?u.49912, u_3} E
X Y : Karoubi C ⥤ Karoubi D
φ : X ⟶ Y
P : Karoubi C
⊢ (NatTrans.app
        (((whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) ⋙ functorExtension₁ C D).map φ ≫
          ((fun G =>
                Iso.mk (NatTrans.mk fun P => Hom.mk (G.map (decompId_p P)).f)
                  (NatTrans.mk fun P => Hom.mk (G.map (decompId_i P)).f))
              Y).hom)
        P).f =
    (NatTrans.app
        (((fun G =>
                Iso.mk (NatTrans.mk fun P => Hom.mk (G.map (decompId_p P)).f)
                  (NatTrans.mk fun P => Hom.mk (G.map (decompId_i P)).f))
              X).hom ≫
          (𝟭 (Karoubi C ⥤ Karoubi D)).map φ)
        P).f
[PROOFSTEP]
dsimp
[GOAL]
case w.h.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.49904, u_1} C
inst✝¹ : Category.{?u.49908, u_2} D
inst✝ : Category.{?u.49912, u_3} E
X Y : Karoubi C ⥤ Karoubi D
φ : X ⟶ Y
P : Karoubi C
⊢ ((X.map ((toKaroubi C).map P.p)).f ≫ (NatTrans.app φ ((toKaroubi C).obj P.X)).f) ≫ (Y.map (decompId_p P)).f =
    (X.map (decompId_p P)).f ≫ (NatTrans.app φ P).f
[PROOFSTEP]
rw [natTrans_eq φ P, P.decomp_p]
[GOAL]
case w.h.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.49904, u_1} C
inst✝¹ : Category.{?u.49908, u_2} D
inst✝ : Category.{?u.49912, u_3} E
X Y : Karoubi C ⥤ Karoubi D
φ : X ⟶ Y
P : Karoubi C
⊢ ((X.map (decompId_p P ≫ decompId_i P)).f ≫ (NatTrans.app φ ((toKaroubi C).obj P.X)).f) ≫ (Y.map (decompId_p P)).f =
    (X.map (decompId_p P)).f ≫ (X.map (decompId_i P) ≫ NatTrans.app φ (Karoubi.mk P.X (𝟙 P.X)) ≫ Y.map (decompId_p P)).f
[PROOFSTEP]
simp only [Functor.map_comp, comp_f, assoc]
[GOAL]
case w.h.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.49904, u_1} C
inst✝¹ : Category.{?u.49908, u_2} D
inst✝ : Category.{?u.49912, u_3} E
X Y : Karoubi C ⥤ Karoubi D
φ : X ⟶ Y
P : Karoubi C
⊢ (X.map (decompId_p P)).f ≫
      (X.map (decompId_i P)).f ≫ (NatTrans.app φ ((toKaroubi C).obj P.X)).f ≫ (Y.map (decompId_p P)).f =
    (X.map (decompId_p P)).f ≫
      (X.map (decompId_i P)).f ≫ (NatTrans.app φ (Karoubi.mk P.X (𝟙 P.X))).f ≫ (Y.map (decompId_p P)).f
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.61683, u_1} C
inst✝¹ : Category.{?u.61687, u_2} D
inst✝ : Category.{?u.61691, u_3} E
F : C ⥤ Karoubi D
⊢ (functorExtension₁ C D).map (NatTrans.app (functorExtension₁_comp_whiskeringLeft_toKaroubi_iso C D).symm.hom F) ≫
      NatTrans.app (KaroubiUniversal₁.counitIso C D).hom ((functorExtension₁ C D).obj F) =
    𝟙 ((functorExtension₁ C D).obj F)
[PROOFSTEP]
ext P
[GOAL]
case w.h.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.61683, u_1} C
inst✝¹ : Category.{?u.61687, u_2} D
inst✝ : Category.{?u.61691, u_3} E
F : C ⥤ Karoubi D
P : Karoubi C
⊢ (NatTrans.app
        ((functorExtension₁ C D).map
            (NatTrans.app (functorExtension₁_comp_whiskeringLeft_toKaroubi_iso C D).symm.hom F) ≫
          NatTrans.app (KaroubiUniversal₁.counitIso C D).hom ((functorExtension₁ C D).obj F))
        P).f =
    (NatTrans.app (𝟙 ((functorExtension₁ C D).obj F)) P).f
[PROOFSTEP]
dsimp [FunctorExtension₁.map, KaroubiUniversal₁.counitIso]
[GOAL]
case w.h.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.61683, u_1} C
inst✝¹ : Category.{?u.61687, u_2} D
inst✝ : Category.{?u.61691, u_3} E
F : C ⥤ Karoubi D
P : Karoubi C
⊢ ((F.map P.p).f ≫
        (NatTrans.app
            (NatTrans.app
              (eqToHom
                (_ :
                  𝟭 (C ⥤ Karoubi D) =
                    functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)))
              F)
            P.X).f) ≫
      (F.map P.p).f =
    (F.map P.p).f
[PROOFSTEP]
simp only [eqToHom_app, Functor.id_obj, Functor.comp_obj, functorExtension₁_obj, whiskeringLeft_obj_obj, eqToHom_f,
  FunctorExtension₁.obj_obj_X, toKaroubi_obj_X, eqToHom_refl, comp_id, comp_p, ← comp_f, ← F.map_comp, P.idem]
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{u_6, u_3} 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
[PROOFSTEP]
refine' Functor.ext _ _
[GOAL]
case refine'_1
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{u_6, u_3} 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
[PROOFSTEP]
aesop_cat
[GOAL]
case refine'_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{u_6, u_3} 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)
[PROOFSTEP]
intro X Y f
[GOAL]
case refine'_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{u_6, u_3} 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)
[PROOFSTEP]
ext
[GOAL]
case refine'_2.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{u_6, u_3} 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
[PROOFSTEP]
simp only [eqToHom_refl, id_comp, comp_id]
[GOAL]
case refine'_2.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{u_6, u_3} 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
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.72126, u_3} E
⊢ functorExtension₂ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) =
    (whiskeringRight C D (Karoubi D)).obj (toKaroubi D)
[PROOFSTEP]
simp only [functorExtension₂, Functor.assoc, functorExtension₁_comp_whiskeringLeft_toKaroubi, Functor.comp_id]
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝³ : Category.{?u.76565, u_1} C
inst✝² : Category.{?u.76569, u_2} D
inst✝¹ : Category.{?u.76573, u_3} E
inst✝ : IsIdempotentComplete D
⊢ IsEquivalence (functorExtension₂ C D)
[PROOFSTEP]
rw [← karoubiUniversal₂_functor_eq]
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝³ : Category.{?u.76565, u_1} C
inst✝² : Category.{?u.76569, u_2} D
inst✝¹ : Category.{?u.76573, u_3} E
inst✝ : IsIdempotentComplete D
⊢ IsEquivalence (karoubiUniversal₂ C D).functor
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝³ : Category.{?u.81595, u_1} C
inst✝² : Category.{?u.81599, u_2} D
inst✝¹ : Category.{?u.81603, u_3} E
inst✝ : IsIdempotentComplete D
⊢ IsEquivalence (functorExtension C D)
[PROOFSTEP]
rw [← karoubiUniversal_functor_eq]
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝³ : Category.{?u.81595, u_1} C
inst✝² : Category.{?u.81599, u_2} D
inst✝¹ : Category.{?u.81603, u_3} E
inst✝ : IsIdempotentComplete D
⊢ IsEquivalence (karoubiUniversal C D).functor
[PROOFSTEP]
infer_instance
  -- porting note: added to avoid a timeout in the following definition
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_5, u_2} D
inst✝¹ : Category.{?u.82137, u_3} E
inst✝ : IsIdempotentComplete D
⊢ (whiskeringLeft C (Karoubi C) D).obj (toKaroubi C) ⋙
      (whiskeringRight C D (Karoubi D)).obj (toKaroubi D) ⋙
        (whiskeringRight C (Karoubi D) D).obj (Functor.inv (toKaroubi D)) =
    (karoubiUniversal C D).inverse
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝³ : Category.{?u.84023, u_1} C
inst✝² : Category.{?u.84027, u_2} D
inst✝¹ : Category.{?u.84031, u_3} E
inst✝ : IsIdempotentComplete D
⊢ IsEquivalence
    ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C) ⋙
      (whiskeringRight C D (Karoubi D)).obj (toKaroubi D) ⋙
        (whiskeringRight C (Karoubi D) D).obj (Functor.inv (toKaroubi D)))
[PROOFSTEP]
rw [isEquivalence_whiskeringLeft_obj_toKaroubi_aux]
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝³ : Category.{?u.84023, u_1} C
inst✝² : Category.{?u.84027, u_2} D
inst✝¹ : Category.{?u.84031, u_3} E
inst✝ : IsIdempotentComplete D
⊢ IsEquivalence (karoubiUniversal C D).inverse
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_5, u_2} D
inst✝¹ : Category.{?u.87671, u_3} E
inst✝ : IsIdempotentComplete D
F G : Karoubi C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
P : Karoubi C
⊢ NatTrans.app (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ) P =
    F.map (decompId_i P) ≫ NatTrans.app τ P.X ≫ G.map (decompId_p P)
[PROOFSTEP]
rw [natTrans_eq]
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_5, u_2} D
inst✝¹ : Category.{?u.87671, u_3} E
inst✝ : IsIdempotentComplete D
F G : Karoubi C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
P : Karoubi C
⊢ F.map (decompId_i P) ≫
      NatTrans.app (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ) (Karoubi.mk P.X (𝟙 P.X)) ≫
        G.map (decompId_p P) =
    F.map (decompId_i P) ≫ NatTrans.app τ P.X ≫ G.map (decompId_p P)
[PROOFSTEP]
congr 2
[GOAL]
case e_a.e_a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_5, u_2} D
inst✝¹ : Category.{?u.87671, u_3} E
inst✝ : IsIdempotentComplete D
F G : Karoubi C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
P : Karoubi C
⊢ NatTrans.app (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ) (Karoubi.mk P.X (𝟙 P.X)) =
    NatTrans.app τ P.X
[PROOFSTEP]
rw [← congr_app (((whiskeringLeft _ _ _).obj (toKaroubi _)).image_preimage τ) P.X]
[GOAL]
case e_a.e_a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_5, u_2} D
inst✝¹ : Category.{?u.87671, u_3} E
inst✝ : IsIdempotentComplete D
F G : Karoubi C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
P : Karoubi C
⊢ NatTrans.app (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ) (Karoubi.mk P.X (𝟙 P.X)) =
    NatTrans.app
      (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).map
        (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ))
      P.X
[PROOFSTEP]
dsimp
[GOAL]
case e_a.e_a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_5, u_2} D
inst✝¹ : Category.{?u.87671, u_3} E
inst✝ : IsIdempotentComplete D
F G : Karoubi C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
P : Karoubi C
⊢ NatTrans.app (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ) (Karoubi.mk P.X (𝟙 P.X)) =
    NatTrans.app (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ) ((toKaroubi C).obj P.X)
[PROOFSTEP]
congr
