awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
x x_1 : Karoubi.{v_1, u_1} C
f : x ⟶ x_1
h : (F.map f.f).f ≫ Hom.f (φ.app x_1.X) = Hom.f (φ.app x.X) ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x_1.p).f = (F.map f.f).f
h'' : (F.map x.p).f ≫ (F.map f.f).f = (F.map f.f).f
h₁ : (F.map f.f).f ≫ (F.map x_1.p).f ≫ Hom.f (φ.app x_1.X) = (F.map x.p).f ≫ (F.map f.f).f ≫ Hom.f (φ.app x_1.X)
⊢ (F.map f.f).f ≫ (F.map x_1.p).f ≫ Hom.f (φ.app x_1.X) = ((F.map x.p).f ≫ Hom.f (φ.app x.X)) ≫ (G.map f.f).f

Tactic:
slice_rhs 2 3 => rw [← h]
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
x x_1 : Karoubi.{v_1, u_1} C
f : x ⟶ x_1
h : (F.map f.f).f ≫ Hom.f (φ.app x_1.X) = Hom.f (φ.app x.X) ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x_1.p).f = (F.map f.f).f
h'' : (F.map x.p).f ≫ (F.map f.f).f = (F.map f.f).f
a : (F.map f.f).f
| (F.map f.f).f ≫ (F.map x_1.p).f

Tactic:
rw [h']
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
x x_1 : Karoubi.{v_1, u_1} C
f : x ⟶ x_1
h : (F.map f.f).f ≫ Hom.f (φ.app x_1.X) = Hom.f (φ.app x.X) ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x_1.p).f = (F.map f.f).f
h'' : (F.map x.p).f ≫ (F.map f.f).f = (F.map f.f).f
h₁ : (F.map f.f).f ≫ Hom.f (φ.app x_1.X) = (F.map x.p).f ≫ (F.map f.f).f ≫ Hom.f (φ.app x_1.X)
⊢ (F.map f.f).f ≫ (F.map x_1.p).f ≫ Hom.f (φ.app x_1.X) = (F.map x.p).f ≫ (F.map f.f).f ≫ Hom.f (φ.app x_1.X)

Tactic:
slice_lhs 1 2 => rw [h']
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
x x_1 : Karoubi.{v_1, u_1} C
f : x ⟶ x_1
h : (F.map f.f).f ≫ Hom.f (φ.app x_1.X) = Hom.f (φ.app x.X) ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x_1.p).f = (F.map f.f).f
h'' : (F.map x.p).f ≫ (F.map f.f).f = (F.map f.f).f
a : (F.map f.f).f
| (F.map x.p).f ≫ (F.map f.f).f

Tactic:
rw [h'']
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
x x_1 : Karoubi.{v_1, u_1} C
f : x ⟶ x_1
h : (F.map f.f).f ≫ Hom.f (φ.app x_1.X) = Hom.f (φ.app x.X) ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x_1.p).f = (F.map f.f).f
h'' : (F.map x.p).f ≫ (F.map f.f).f = (F.map f.f).f
slice_rhs : (F.map f.f).f ≫ Hom.f (φ.app x_1.X) = (F.map x.p).f ≫ (F.map f.f).f ≫ Hom.f (φ.app x_1.X)
h₁ : (F.map f.f).f ≫ Hom.f (φ.app x_1.X) = (F.map f.f).f ≫ Hom.f (φ.app x_1.X)
⊢ (F.map f.f).f ≫ Hom.f (φ.app x_1.X) = (F.map x.p).f ≫ (F.map f.f).f ≫ Hom.f (φ.app x_1.X)

Tactic:
slice_rhs 1 2 => rw [h'']
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : C ⥤ Karoubi.{v_2, u_2} D
w :
  ∀ (P : Karoubi.{v_1, u_1} C),
    ((FunctorExtension₁.map (𝟙 F)).app P).f = (NatTrans.app (𝟙 (FunctorExtension₁.obj F)) P).f
⊢ FunctorExtension₁.map (𝟙 F) = 𝟙 (FunctorExtension₁.obj F)

Tactic:
ext P
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : C ⥤ Karoubi.{v_2, u_2} D
P : Karoubi.{v_1, u_1} C
⊢ ((FunctorExtension₁.map (𝟙 F)).app P).f = (NatTrans.app (𝟙 (FunctorExtension₁.obj F)) P).f

Tactic:
comp_p (F.map P.p)

Premises used: CategoryTheory.Idempotents.Karoubi.comp_p, CategoryTheory.Idempotents.Karoubi.p, CategoryTheory.Functor.map
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : C ⥤ Karoubi.{v_2, u_2} D
P : Karoubi.{v_1, u_1} C
⊢ ((FunctorExtension₁.map (𝟙 F)).app P).f = (NatTrans.app (𝟙 (FunctorExtension₁.obj F)) P).f

Tactic:
exact comp_p (F.map P.p)

Premises used: CategoryTheory.Idempotents.Karoubi.comp_p, CategoryTheory.Idempotents.Karoubi.p, CategoryTheory.Functor.map
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G H : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
φ' : G ⟶ H
w :
  ∀ (P : Karoubi.{v_1, u_1} C),
    ((FunctorExtension₁.map (φ ≫ φ')).app P).f = ((FunctorExtension₁.map φ ≫ FunctorExtension₁.map φ').app P).f
⊢ FunctorExtension₁.map (φ ≫ φ') = FunctorExtension₁.map φ ≫ FunctorExtension₁.map φ'

Tactic:
ext P
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G H : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi.{v_1, u_1} C
w :
  (F.map P.p).f ≫ Hom.f (φ.app P.X) ≫ Hom.f (φ'.app P.X) =
    (F.map P.p).f ≫ Hom.f (φ.app P.X) ≫ (G.map P.p).f ≫ Hom.f (φ'.app P.X)
⊢ ((FunctorExtension₁.map (φ ≫ φ')).app P).f = ((FunctorExtension₁.map φ ≫ FunctorExtension₁.map φ').app P).f

Tactic:
simp only [comp_f, FunctorExtension₁.map_app_f, NatTrans.comp_app, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Idempotents.Karoubi.comp_f, CategoryTheory.NatTrans.comp_app, CategoryTheory.Idempotents.FunctorExtension₁.map_app_f
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G H : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi.{v_1, u_1} C
⊢ F.map P.p ≫ φ.app P.X = φ.app P.X ≫ G.map P.p

Tactic:
have h := φ.naturality P.p
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G H : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi.{v_1, u_1} C
h : F.map P.p ≫ φ.app P.X = φ.app P.X ≫ G.map P.p
⊢ F.map (P.p ≫ P.p) = F.map P.p

Tactic:
have h' := F.congr_map P.idem
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G H : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi.{v_1, u_1} C
h : F.map P.p ≫ φ.app P.X = φ.app P.X ≫ G.map P.p
h' : F.map (P.p ≫ P.p) = F.map P.p
⊢ (F.map P.p).f ≫ Hom.f (φ.app P.X) = Hom.f (φ.app P.X) ≫ (G.map P.p).f

Tactic:
simp only [hom_ext_iff, comp_f, F.map_comp] at h h'

Premises used: CategoryTheory.Idempotents.Karoubi.comp_f, CategoryTheory.Functor.map_comp, CategoryTheory.Idempotents.Karoubi.hom_ext_iff
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G H : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi.{v_1, u_1} C
h : F.map P.p ≫ φ.app P.X = φ.app P.X ≫ G.map P.p
h' : F.map (P.p ≫ P.p) = F.map P.p
h₁ : (F.map P.p).f ≫ Hom.f (φ.app P.X) = Hom.f (φ.app P.X) ≫ (G.map P.p).f
⊢ (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f

Tactic:
simp only [hom_ext_iff, comp_f, F.map_comp] at h h'

Premises used: CategoryTheory.Idempotents.Karoubi.comp_f, CategoryTheory.Functor.map_comp, CategoryTheory.Idempotents.Karoubi.hom_ext_iff
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G H : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi.{v_1, u_1} C
h : (F.map P.p).f ≫ Hom.f (φ.app P.X) = Hom.f (φ.app P.X) ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
a : (F.map P.p).f ≫ Hom.f (φ.app P.X)
| Hom.f (φ.app P.X) ≫ (G.map P.p).f

Tactic:
rw [← h]
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G H : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi.{v_1, u_1} C
h : (F.map P.p).f ≫ Hom.f (φ.app P.X) = Hom.f (φ.app P.X) ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
w :
  (F.map P.p).f ≫ Hom.f (φ.app P.X) ≫ Hom.f (φ'.app P.X) =
    (F.map P.p).f ≫ ((F.map P.p).f ≫ Hom.f (φ.app P.X)) ≫ Hom.f (φ'.app P.X)
⊢ (F.map P.p).f ≫ Hom.f (φ.app P.X) ≫ Hom.f (φ'.app P.X) =
    (F.map P.p).f ≫ Hom.f (φ.app P.X) ≫ (G.map P.p).f ≫ Hom.f (φ'.app P.X)

Tactic:
slice_rhs 2 3 => rw [← h]
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G H : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi.{v_1, u_1} C
h : (F.map P.p).f ≫ Hom.f (φ.app P.X) = Hom.f (φ.app P.X) ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
a : (F.map P.p).f
| (F.map P.p).f ≫ (F.map P.p).f

Tactic:
rw [h']
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G H : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi.{v_1, u_1} C
h : (F.map P.p).f ≫ Hom.f (φ.app P.X) = Hom.f (φ.app P.X) ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
w : (F.map P.p).f ≫ Hom.f (φ.app P.X) ≫ Hom.f (φ'.app P.X) = ((F.map P.p).f ≫ Hom.f (φ.app P.X)) ≫ Hom.f (φ'.app P.X)
⊢ (F.map P.p).f ≫ Hom.f (φ.app P.X) ≫ Hom.f (φ'.app P.X) =
    (F.map P.p).f ≫ ((F.map P.p).f ≫ Hom.f (φ.app P.X)) ≫ Hom.f (φ'.app P.X)

Tactic:
slice_rhs 1 2 => rw [h']
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G H : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi.{v_1, u_1} C
h : (F.map P.p).f ≫ Hom.f (φ.app P.X) = Hom.f (φ.app P.X) ≫ (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 ≫ Hom.f (φ.app P.X) ≫ Hom.f (φ'.app P.X) = ((F.map P.p).f ≫ Hom.f (φ.app P.X)) ≫ Hom.f (φ'.app P.X)

Tactic:
simp only [assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : C ⥤ Karoubi.{v_2, u_2} D
X Y : C
f : X ⟶ Y
⊢ (obj (functorExtension₁ C D ⋙ obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C))
            F).map
        f ≫
      Iso.hom
        ((fun (X : C) ↦
            { hom := { f := (F.obj X).p, comm := ⋯ }, inv := { f := (F.obj X).p, comm := ⋯ }, hom_inv_id := ⋯,
              inv_hom_id := ⋯ :
              (obj
                      (functorExtension₁ C D ⋙
                        obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C))
                      F).obj
                  X ≅
                (obj (𝟭 (C ⥤ Karoubi.{v_2, u_2} D)) F).obj X })
          Y) =
    Iso.hom
        ((fun (X : C) ↦
            {
              hom :=
                { f := (F.obj X).p, comm := ⋯ :
                  ((obj
                            (functorExtension₁ C D ⋙
                              obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C))
                            F).obj
                        X).Hom
                    ((obj (𝟭 (C ⥤ Karoubi.{v_2, u_2} D)) F).obj X) },
              inv :=
                { f := (F.obj X).p, comm := ⋯ :
                  ((obj (𝟭 (C ⥤ Karoubi.{v_2, u_2} D)) F).obj X).Hom
                    ((obj
                          (functorExtension₁ C D ⋙
                            obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C))
                          F).obj
                      X) },
              hom_inv_id := ⋯, inv_hom_id := ⋯ :
              (obj
                      (functorExtension₁ C D ⋙
                        obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C))
                      F).obj
                  X ≅
                (obj (𝟭 (C ⥤ Karoubi.{v_2, u_2} D)) F).obj X })
          X) ≫
      (obj (𝟭 (C ⥤ Karoubi.{v_2, u_2} D)) F).map f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
G : Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D
P : Karoubi.{v_1, u_1} C
⊢ map (toKaroubi C) P.p ≫ P.decompId_p ≫ 𝟙 P = P.decompId_p

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
G : Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D
P : Karoubi.{v_1, u_1} C
⊢ ((obj (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C) ⋙ functorExtension₁ C D)
              G).obj
          P).p ≫
      (G.map P.decompId_p).f ≫ ((obj (𝟭 (Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D)) G).obj P).p =
    (G.map P.decompId_p).f

Tactic:
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)

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.congr_map, CategoryTheory.Idempotents.Karoubi.hom_ext_iff
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
G : Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D
P Q : Karoubi.{v_1, u_1} C
f : P ⟶ Q
⊢ (obj (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C) ⋙ functorExtension₁ C D)
            G).map
        f ≫
      { f := (G.map Q.decompId_p).f, comm := ⋯ :
        ((obj
                  (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C) ⋙
                    functorExtension₁ C D)
                  G).obj
              Q).Hom
          ((obj (𝟭 (Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D)) G).obj Q) } =
    { f := (G.map P.decompId_p).f, comm := ⋯ :
        ((obj
                  (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C) ⋙
                    functorExtension₁ C D)
                  G).obj
              P).Hom
          ((obj (𝟭 (Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D)) G).obj P) } ≫
      (obj (𝟭 (Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D)) G).map f

Tactic:
simpa only [hom_ext_iff, G.map_comp]
                using (G.congr_map (decompId_p_naturality f)).symm

Premises used: CategoryTheory.Idempotents.Karoubi.decompId_p_naturality, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.congr_map, Eq.symm, CategoryTheory.Idempotents.Karoubi.hom_ext_iff
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
G : Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D
P : Karoubi.{v_1, u_1} C
⊢ 𝟙 P ≫ P.decompId_i ≫ map (toKaroubi C) P.p = P.decompId_i

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
G : Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D
P : Karoubi.{v_1, u_1} C
⊢ ((obj (𝟭 (Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D)) G).obj P).p ≫
      (G.map P.decompId_i).f ≫
        ((obj
                (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C) ⋙
                  functorExtension₁ C D)
                G).obj
            P).p =
    (G.map P.decompId_i).f

Tactic:
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)

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.congr_map, CategoryTheory.Idempotents.Karoubi.hom_ext_iff
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
G : Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D
P Q : Karoubi.{v_1, u_1} C
f : P ⟶ Q
⊢ (obj (𝟭 (Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D)) G).map f ≫
      { f := (G.map Q.decompId_i).f, comm := ⋯ :
        ((obj (𝟭 (Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D)) G).obj Q).Hom
          ((obj
                (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C) ⋙
                  functorExtension₁ C D)
                G).obj
            Q) } =
    { f := (G.map P.decompId_i).f, comm := ⋯ :
        ((obj (𝟭 (Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D)) G).obj P).Hom
          ((obj
                (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C) ⋙
                  functorExtension₁ C D)
                G).obj
            P) } ≫
      (obj (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C) ⋙ functorExtension₁ C D)
            G).map
        f

Tactic:
simpa only [hom_ext_iff, G.map_comp] using G.congr_map (decompId_i_naturality f)

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Functor.congr_map, CategoryTheory.Idempotents.Karoubi.decompId_i_naturality, CategoryTheory.Idempotents.Karoubi.hom_ext_iff
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
G : Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D
w :
  ∀ (P : Karoubi.{v_1, u_1} C),
    Hom.f
        (NatTrans.app
          (CategoryStruct.comp (Y := obj (𝟭 (Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D)) G)
            { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_p).f, comm := ⋯ }, naturality := ⋯ }
            { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_i).f, comm := ⋯ }, naturality := ⋯ })
          P) =
      (NatTrans.app
          (𝟙
            (obj
              (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C) ⋙
                functorExtension₁ C D)
              G))
          P).f
⊢ CategoryStruct.comp (Y := obj (𝟭 (Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D)) G)
      { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_p).f, comm := ⋯ }, naturality := ⋯ }
      { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_i).f, comm := ⋯ }, naturality := ⋯ } =
    𝟙
      (obj (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C) ⋙ functorExtension₁ C D)
        G)

Tactic:
ext P
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
G : Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D
P : Karoubi.{v_1, u_1} C
⊢ Hom.f
      (NatTrans.app
        (CategoryStruct.comp (Y := obj (𝟭 (Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D)) G)
          { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_p).f, comm := ⋯ }, naturality := ⋯ }
          { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_i).f, comm := ⋯ }, naturality := ⋯ })
        P) =
    (NatTrans.app
        (𝟙
          (obj
            (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C) ⋙ functorExtension₁ C D)
            G))
        P).f

Tactic:
simpa only [hom_ext_iff, G.map_comp, G.map_id] using G.congr_map P.decomp_p.symm

Premises used: CategoryTheory.Idempotents.Karoubi.decomp_p, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.congr_map, Eq.symm, CategoryTheory.Idempotents.Karoubi.hom_ext_iff
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
G : Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D
w :
  ∀ (P : Karoubi.{v_1, u_1} C),
    Hom.f
        (NatTrans.app
          (CategoryStruct.comp (Y :=
            obj
              (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C) ⋙
                functorExtension₁ C D)
              G)
            { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_i).f, comm := ⋯ }, naturality := ⋯ }
            { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_p).f, comm := ⋯ }, naturality := ⋯ })
          P) =
      (NatTrans.app (𝟙 (obj (𝟭 (Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D)) G)) P).f
⊢ CategoryStruct.comp (Y :=
      obj (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C) ⋙ functorExtension₁ C D)
        G)
      { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_i).f, comm := ⋯ }, naturality := ⋯ }
      { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_p).f, comm := ⋯ }, naturality := ⋯ } =
    𝟙 (obj (𝟭 (Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D)) G)

Tactic:
ext P
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
G : Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D
P : Karoubi.{v_1, u_1} C
⊢ Hom.f
      (NatTrans.app
        (CategoryStruct.comp (Y :=
          obj
            (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C) ⋙ functorExtension₁ C D)
            G)
          { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_i).f, comm := ⋯ }, naturality := ⋯ }
          { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_p).f, comm := ⋯ }, naturality := ⋯ })
        P) =
    (NatTrans.app (𝟙 (obj (𝟭 (Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D)) G)) P).f

Tactic:
simpa only [hom_ext_iff, G.map_comp, G.map_id] using G.congr_map P.decompId.symm

Premises used: CategoryTheory.Idempotents.Karoubi.decompId, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.congr_map, Eq.symm, CategoryTheory.Idempotents.Karoubi.hom_ext_iff