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
X Y : Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D
φ : X ⟶ Y
P : Karoubi.{v_1, u_1} C
w :
  (Hom.f (X.map (map (toKaroubi C) P.p)) ≫ Hom.f (φ.app (obj (toKaroubi C) P.X))) ≫ (Y.map P.decompId_p).f =
    (X.map P.decompId_p).f ≫ (φ.app P).f
⊢ Eq (α :=
    ((obj (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C) ⋙ functorExtension₁ C D)
              X).obj
          P).X ⟶
      ((obj (𝟭 (Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D)) Y).obj P).X)
    (Hom.f
      (NatTrans.app
        (map
            (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C) ⋙ functorExtension₁ C D)
            φ ≫
          Iso.hom
            ((fun (G : Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D) ↦
                {
                  hom :=
                    { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_p).f, comm := ⋯ },
                      naturality := ⋯ },
                  inv :=
                    { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_i).f, comm := ⋯ },
                      naturality := ⋯ },
                  hom_inv_id := ⋯, inv_hom_id := ⋯ :
                  obj
                      (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C) ⋙
                        functorExtension₁ C D)
                      G ≅
                    obj (𝟭 (Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D)) G })
              Y))
        P))
    (Hom.f
      (NatTrans.app
        (Iso.hom
            ((fun (G : Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D) ↦
                {
                  hom :=
                    { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_p).f, comm := ⋯ },
                      naturality := ⋯ },
                  inv :=
                    { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_i).f, comm := ⋯ },
                      naturality := ⋯ },
                  hom_inv_id := ⋯, inv_hom_id := ⋯ :
                  obj
                      (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C) ⋙
                        functorExtension₁ C D)
                      G ≅
                    obj (𝟭 (Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D)) G })
              X) ≫
          map (𝟭 (Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D)) φ)
        P))

Tactic:
dsimp
-- 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
X Y : Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D
φ : X ⟶ Y
P : Karoubi.{v_1, u_1} C
w :
  ((X.map (P.decompId_p ≫ P.decompId_i)).f ≫ Hom.f (φ.app (obj (toKaroubi C) P.X))) ≫ (Y.map P.decompId_p).f =
    (X.map P.decompId_p).f ≫ (X.map P.decompId_i ≫ φ.app { X := P.X, p := 𝟙 P.X, idem := ⋯ } ≫ Y.map P.decompId_p).f
⊢ (Hom.f (X.map (map (toKaroubi C) P.p)) ≫ Hom.f (φ.app (obj (toKaroubi C) P.X))) ≫ (Y.map P.decompId_p).f =
    (X.map P.decompId_p).f ≫ (φ.app P).f

Tactic:
rw [natTrans_eq φ P, P.decomp_p]

Premises used: CategoryTheory.Idempotents.Karoubi.decomp_p, CategoryTheory.Idempotents.natTrans_eq
-- 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
X Y : Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D
φ : X ⟶ Y
P : Karoubi.{v_1, u_1} C
w :
  (X.map P.decompId_p).f ≫ (X.map P.decompId_i).f ≫ Hom.f (φ.app (obj (toKaroubi C) P.X)) ≫ (Y.map P.decompId_p).f =
    (X.map P.decompId_p).f ≫
      (X.map P.decompId_i).f ≫ Hom.f (φ.app { X := P.X, p := 𝟙 P.X, idem := ⋯ }) ≫ (Y.map P.decompId_p).f
⊢ ((X.map (P.decompId_p ≫ P.decompId_i)).f ≫ Hom.f (φ.app (obj (toKaroubi C) P.X))) ≫ (Y.map P.decompId_p).f =
    (X.map P.decompId_p).f ≫ (X.map P.decompId_i ≫ φ.app { X := P.X, p := 𝟙 P.X, idem := ⋯ } ≫ Y.map P.decompId_p).f

Tactic:
simp only [Functor.map_comp, comp_f, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Idempotents.Karoubi.comp_f, CategoryTheory.Functor.map_comp
-- 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
X Y : Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D
φ : X ⟶ Y
P : Karoubi.{v_1, u_1} C
⊢ (X.map P.decompId_p).f ≫ (X.map P.decompId_i).f ≫ Hom.f (φ.app (obj (toKaroubi C) P.X)) ≫ (Y.map P.decompId_p).f =
    (X.map P.decompId_p).f ≫
      (X.map P.decompId_i).f ≫ Hom.f (φ.app { X := P.X, p := 𝟙 P.X, idem := ⋯ }) ≫ (Y.map P.decompId_p).f

Tactic:
rfl
-- 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),
    Hom.f
        (NatTrans.app
          (map (functorExtension₁ C D)
              (NatTrans.app (Iso.hom (Iso.symm (functorExtension₁CompWhiskeringLeftToKaroubiIso C D))) F) ≫
            NatTrans.app (Iso.hom (KaroubiUniversal₁.counitIso C D)) (obj (functorExtension₁ C D) F))
          P) =
      (NatTrans.app (𝟙 (obj (functorExtension₁ C D) F)) P).f
⊢ map (functorExtension₁ C D)
        (NatTrans.app (Iso.hom (Iso.symm (functorExtension₁CompWhiskeringLeftToKaroubiIso C D))) F) ≫
      NatTrans.app (Iso.hom (KaroubiUniversal₁.counitIso C D)) (obj (functorExtension₁ C D) F) =
    𝟙 (obj (functorExtension₁ C D) 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
w : ((F.map P.p).f ≫ (F.obj P.X).p) ≫ (F.map P.p).f = (F.map P.p).f
⊢ Hom.f
      (NatTrans.app
        (map (functorExtension₁ C D)
            (NatTrans.app (Iso.hom (Iso.symm (functorExtension₁CompWhiskeringLeftToKaroubiIso C D))) F) ≫
          NatTrans.app (Iso.hom (KaroubiUniversal₁.counitIso C D)) (obj (functorExtension₁ C D) F))
        P) =
    (NatTrans.app (𝟙 (obj (functorExtension₁ C D) F)) P).f

Tactic:
dsimp
-- 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
w : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
w₁ : (F.map P.p ≫ F.map P.p).f = (F.map P.p).f
w₂ : (F.map (P.p ≫ P.p)).f = (F.map P.p).f
w₃ w₄ : (F.map P.p).f = (F.map P.p).f
⊢ ((F.map P.p).f ≫ (F.obj P.X).p) ≫ (F.map P.p).f = (F.map P.p).f

Tactic:
rw [comp_p, ← comp_f, ← F.map_comp, P.idem]

Premises used: CategoryTheory.Idempotents.Karoubi.comp_p, CategoryTheory.Idempotents.Karoubi.comp_f, CategoryTheory.Idempotents.Karoubi.idem, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : IsIdempotentComplete.{v_2, u_2} D
⊢ Eq (α := Functor.{v_1, v_2, u_1, u_2} C D ⥤ Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D)
    (Equivalence.functor (karoubiUniversal₂ C D)) (functorExtension₂ C D)

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Idempotents.functorExtension₂, CategoryTheory.Idempotents.toKaroubi, rfl
-- 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
inst_3 : IsIdempotentComplete.{v_2, u_2} D
⊢ IsEquivalence (C := Functor.{v_1, v_2, u_1, u_2} C D) (Equivalence.functor (karoubiUniversal₂ C D))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : IsIdempotentComplete.{v_2, u_2} D
⊢ Eq (α := Functor.{v_1, v_2, u_1, u_2} C D ⥤ Karoubi.{v_1, u_1} C ⥤ D) (Equivalence.functor (karoubiUniversal C D))
    (functorExtension C D)

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Idempotents.toKaroubi, CategoryTheory.Functor.inv, CategoryTheory.Idempotents.functorExtension, rfl
-- 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
inst_3 : IsIdempotentComplete.{v_2, u_2} D
⊢ IsEquivalence (C := Functor.{v_1, v_2, u_1, u_2} C D) (Equivalence.functor (karoubiUniversal C D))

Tactic:
infer_instance
-- 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
inst_3 : IsIdempotentComplete.{v_2, u_2} D
change : IsEquivalence (C := Karoubi.{v_1, u_1} C ⥤ D) (Equivalence.inverse (karoubiUniversal C D))
⊢ IsEquivalence (C := Karoubi.{v_1, u_1} C ⥤ D)
    (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C) ⋙
      obj (whiskeringRight C D (Karoubi.{v_2, u_2} D)) (toKaroubi D) ⋙
        obj (whiskeringRight C (Karoubi.{v_2, u_2} D) D) (Functor.inv (toKaroubi D)))

Tactic:
change (karoubiUniversal C D).inverse.IsEquivalence

Premises used: CategoryTheory.Functor.IsEquivalence, CategoryTheory.Idempotents.karoubiUniversal, CategoryTheory.Equivalence.inverse
-- 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
inst_3 : IsIdempotentComplete.{v_2, u_2} D
⊢ IsEquivalence (C := Karoubi.{v_1, u_1} C ⥤ D) (Equivalence.inverse (karoubiUniversal C D))

Tactic:
infer_instance
-- 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
inst_3 : IsIdempotentComplete.{v_2, u_2} D
⊢ IsEquivalence (C := Karoubi.{v_1, u_1} C ⥤ D)
    (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C) ⋙
      obj (whiskeringRight C D (Karoubi.{v_2, u_2} D)) (toKaroubi D) ⋙
        obj (whiskeringRight C (Karoubi.{v_2, u_2} D) D) (Functor.inv (toKaroubi D)))

Tactic:
have : ((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))).IsEquivalence := by
    change (karoubiUniversal C D).inverse.IsEquivalence
    infer_instance
-- 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
inst_3 : IsIdempotentComplete.{v_2, u_2} D
this :
  IsEquivalence (C := Karoubi.{v_1, u_1} C ⥤ D)
    (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C) ⋙
      obj (whiskeringRight C D (Karoubi.{v_2, u_2} D)) (toKaroubi D) ⋙
        obj (whiskeringRight C (Karoubi.{v_2, u_2} D) D) (Functor.inv (toKaroubi D)))
⊢ IsEquivalence (C := Karoubi.{v_1, u_1} C ⥤ D) (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C))

Tactic:
Functor.isEquivalence_of_comp_right _
    ((whiskeringRight C _ _).obj (toKaroubi D) ⋙
      (whiskeringRight C (Karoubi D) D).obj (Functor.inv (toKaroubi D)))

Premises used: CategoryTheory.Idempotents.Karoubi, CategoryTheory.Functor.comp, CategoryTheory.Idempotents.toKaroubi, CategoryTheory.Functor.whiskeringRight, CategoryTheory.Functor.inv, CategoryTheory.Functor.obj, CategoryTheory.Functor.isEquivalence_of_comp_right
-- 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
inst_3 : IsIdempotentComplete.{v_2, u_2} D
this :
  IsEquivalence (C := Karoubi.{v_1, u_1} C ⥤ D)
    (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C) ⋙
      obj (whiskeringRight C D (Karoubi.{v_2, u_2} D)) (toKaroubi D) ⋙
        obj (whiskeringRight C (Karoubi.{v_2, u_2} D) D) (Functor.inv (toKaroubi D)))
⊢ IsEquivalence (C := Karoubi.{v_1, u_1} C ⥤ D) (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C))

Tactic:
exact Functor.isEquivalence_of_comp_right _
    ((whiskeringRight C _ _).obj (toKaroubi D) ⋙
      (whiskeringRight C (Karoubi D) D).obj (Functor.inv (toKaroubi D)))

Premises used: CategoryTheory.Idempotents.Karoubi, CategoryTheory.Functor.comp, CategoryTheory.Idempotents.toKaroubi, CategoryTheory.Functor.whiskeringRight, CategoryTheory.Functor.inv, CategoryTheory.Functor.obj, CategoryTheory.Functor.isEquivalence_of_comp_right
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : IsIdempotentComplete.{v_2, u_2} D
F G : Karoubi.{v_1, u_1} C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
P : Karoubi.{v_1, u_1} C
rw :
  F.map P.decompId_i ≫
      NatTrans.app (preimage (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) τ)
          { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v_1, u_1} C } ≫
        G.map P.decompId_p =
    F.map P.decompId_i ≫ τ.app P.X ≫ G.map P.decompId_p
⊢ NatTrans.app (preimage (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) τ) P =
    F.map P.decompId_i ≫ τ.app P.X ≫ G.map P.decompId_p

Tactic:
rw [natTrans_eq]

Premises used: CategoryTheory.Idempotents.natTrans_eq
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : IsIdempotentComplete.{v_2, u_2} D
F G : Karoubi.{v_1, u_1} C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
P : Karoubi.{v_1, u_1} C
e_a :
  Eq (α := F.obj { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v_1, u_1} C } ⟶ G.obj { X := P.X, p := 𝟙 P.X, idem := ⋯ })
    (NatTrans.app (preimage (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) τ)
      { X := P.X, p := 𝟙 P.X, idem := ⋯ })
    (τ.app P.X)
⊢ F.map P.decompId_i ≫
      NatTrans.app (preimage (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) τ)
          { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v_1, u_1} C } ≫
        G.map P.decompId_p =
    F.map P.decompId_i ≫ τ.app P.X ≫ G.map P.decompId_p

Tactic:
congr 2
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : IsIdempotentComplete.{v_2, u_2} D
F G : Karoubi.{v_1, u_1} C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
P : Karoubi.{v_1, u_1} C
e_a :
  Eq.{v_2 + 1} (α :=
    F.obj { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v_1, u_1} C } ⟶ G.obj { X := P.X, p := 𝟙 P.X, idem := ⋯ })
    (NatTrans.app (preimage (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) τ)
      { X := P.X, p := 𝟙 P.X, idem := ⋯ })
    (NatTrans.app
      (map (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C))
        (preimage (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) τ))
      P.X)
⊢ Eq (α := F.obj { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v_1, u_1} C } ⟶ G.obj { X := P.X, p := 𝟙 P.X, idem := ⋯ })
    (NatTrans.app (preimage (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) τ)
      { X := P.X, p := 𝟙 P.X, idem := ⋯ })
    (τ.app P.X)

Tactic:
rw [← congr_app (((whiskeringLeft _ _ _).obj (toKaroubi _)).map_preimage τ) P.X]

Premises used: CategoryTheory.Idempotents.toKaroubi, CategoryTheory.Idempotents.Karoubi.X, CategoryTheory.Functor.whiskeringLeft, CategoryTheory.congr_app, CategoryTheory.Functor.obj, CategoryTheory.Functor.map_preimage
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : IsIdempotentComplete.{v_2, u_2} D
F G : Karoubi.{v_1, u_1} C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
P : Karoubi.{v_1, u_1} C
⊢ Eq.{v_2 + 1} (α :=
    F.obj { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v_1, u_1} C } ⟶ G.obj { X := P.X, p := 𝟙 P.X, idem := ⋯ })
    (NatTrans.app (preimage (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) τ)
      { X := P.X, p := 𝟙 P.X, idem := ⋯ })
    (NatTrans.app (preimage (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) τ) (obj (toKaroubi C) P.X))

Tactic:
congr
-- 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 : Karoubi.{v_1, u_1} C ⥤ D
τ :
  obj (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) F ⟶
    obj (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) G
X Y : Karoubi.{v_1, u_1} C
f : X ⟶ Y
dsimp :
  F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    (F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p) ≫ G.map f
⊢ F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    (F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p) ≫ G.map f

Tactic:
dsimp at τ ⊢
-- 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 : Karoubi.{v_1, u_1} C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
X Y : Karoubi.{v_1, u_1} C
f : X ⟶ Y
⊢ f ≫ Y.decompId_i = X.decompId_i ≫ map (toKaroubi C) f.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
F G : Karoubi.{v_1, u_1} C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
X Y : Karoubi.{v_1, u_1} C
f : X ⟶ Y
⊢ f ≫ Y.decompId_i = X.decompId_i ≫ map (toKaroubi C) f.f

Tactic:
have h₁ : f ≫ Y.decompId_i = X.decompId_i ≫ (toKaroubi C).map f.f := by 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
F G : Karoubi.{v_1, u_1} C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
X Y : Karoubi.{v_1, u_1} C
f : X ⟶ Y
h₁ : f ≫ Y.decompId_i = X.decompId_i ≫ map (toKaroubi C) f.f
⊢ (toKaroubi C ⋙ F).map f.f ≫ τ.app Y.X = τ.app X.X ≫ (toKaroubi C ⋙ G).map f.f

Tactic:
have h₂ := τ.naturality f.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 : Karoubi.{v_1, u_1} C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
X Y : Karoubi.{v_1, u_1} C
f : X ⟶ Y
h₁ : f ≫ Y.decompId_i = X.decompId_i ≫ map (toKaroubi C) f.f
h₂ : (toKaroubi C ⋙ F).map f.f ≫ τ.app Y.X = τ.app X.X ≫ (toKaroubi C ⋙ G).map f.f
⊢ X.decompId_p ≫ f = map (toKaroubi C) f.f ≫ Y.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
F G : Karoubi.{v_1, u_1} C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
X Y : Karoubi.{v_1, u_1} C
f : X ⟶ Y
h₁ : f ≫ Y.decompId_i = X.decompId_i ≫ map (toKaroubi C) f.f
h₂ : (toKaroubi C ⋙ F).map f.f ≫ τ.app Y.X = τ.app X.X ≫ (toKaroubi C ⋙ G).map f.f
⊢ X.decompId_p ≫ f = map (toKaroubi C) f.f ≫ Y.decompId_p

Tactic:
have h₃ : X.decompId_p ≫ f = (toKaroubi C).map f.f ≫ Y.decompId_p := by 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
F G : Karoubi.{v_1, u_1} C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
X Y : Karoubi.{v_1, u_1} C
f : X ⟶ Y
h₁ : f ≫ Y.decompId_i = X.decompId_i ≫ map (toKaroubi C) f.f
h₂ : F.map (map (toKaroubi C) f.f) ≫ τ.app Y.X = τ.app X.X ≫ G.map (map (toKaroubi C) f.f)
h₃ : X.decompId_p ≫ f = map (toKaroubi C) f.f ≫ Y.decompId_p
rw :
  F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ (τ.app X.X ≫ G.map X.decompId_p) ≫ G.map f
rw₁ :
  F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
rw₂ :
  F.map (f ≫ Y.decompId_i) ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
rw₃ :
  F.map (X.decompId_i ≫ map (toKaroubi C) f.f) ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
rw₄ :
  F.map X.decompId_i ≫ F.map (map (toKaroubi C) f.f) ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
rw₅ :
  F.map X.decompId_i ≫ τ.app X.X ≫ G.map (map (toKaroubi C) f.f) ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
rw₆ :
  F.map X.decompId_i ≫ τ.app X.X ≫ G.map (map (toKaroubi C) f.f ≫ Y.decompId_p) =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
rw₇ :
  F.map X.decompId_i ≫ τ.app X.X ≫ G.map (X.decompId_p ≫ f) =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
rw₈ rw₉ :
  F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
⊢ F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    (F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p) ≫ G.map f

Tactic:
rw [Category.assoc, Category.assoc, ← F.map_comp_assoc,
          h₁, F.map_comp_assoc, reassoc_of% h₂, ← G.map_comp, ← h₃, G.map_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_comp
-- 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 : Karoubi.{v_1, u_1} C ⥤ D
τ :
  obj (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) F ⟶
    obj (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) G
w :
  ∀ (X : C),
    NatTrans.app
        (map (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C))
          { app := fun (P : Karoubi.{v_1, u_1} C) ↦ F.map P.decompId_i ≫ τ.app P.X ≫ G.map P.decompId_p,
            naturality := ⋯ })
        X =
      τ.app X
⊢ map (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C))
      { app := fun (P : Karoubi.{v_1, u_1} C) ↦ F.map P.decompId_i ≫ τ.app P.X ≫ G.map P.decompId_p, naturality := ⋯ } =
    τ

Tactic:
ext X

Premises used: CategoryTheory.Idempotents.Karoubi.X
-- 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 : Karoubi.{v_1, u_1} C ⥤ D
τ :
  obj (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) F ⟶
    obj (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) G
X : C
w : F.map (decompId_i (obj (toKaroubi C) X)) ≫ τ.app X ≫ G.map (decompId_p (obj (toKaroubi C) X)) = τ.app X
⊢ NatTrans.app
      (map (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C))
        { app := fun (P : Karoubi.{v_1, u_1} C) ↦ F.map P.decompId_i ≫ τ.app P.X ≫ G.map P.decompId_p,
          naturality := ⋯ })
      X =
    τ.app X

Tactic:
dsimp