awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
P_1 Q_1 : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
f_1 : P_1 ⟶ Q_1
X : J
P Q : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
f : Functor.obj (karoubiFunctorCategoryEmbedding J C) P ⟶ Functor.obj (karoubiFunctorCategoryEmbedding J C) Q
w :
  ∀ (j : J),
    (P.p ≫ { app := fun (j : J) ↦ (f.app j).f, naturality := ⋯ : NatTrans P.X Q.X } ≫ Q.p).app j =
      NatTrans.app { app := fun (j : J) ↦ (f.app j).f, naturality := ⋯ } j
⊢ P.p ≫ { app := fun (j : J) ↦ (f.app j).f, naturality := ⋯ : NatTrans P.X Q.X } ≫ Q.p =
    { app := fun (j : J) ↦ (f.app j).f, naturality := ⋯ }

Tactic:
ext j
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
P_1 Q_1 : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
f_1 : P_1 ⟶ Q_1
X : J
P Q : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
f : Functor.obj (karoubiFunctorCategoryEmbedding J C) P ⟶ Functor.obj (karoubiFunctorCategoryEmbedding J C) Q
j : J
⊢ (P.p ≫ { app := fun (j : J) ↦ (f.app j).f, naturality := ⋯ : NatTrans P.X Q.X } ≫ Q.p).app j =
    NatTrans.app { app := fun (j : J) ↦ (f.app j).f, naturality := ⋯ } j

Tactic:
(f.app j).comm

Premises used: CategoryTheory.Idempotents.Karoubi.Hom.comm, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
P_1 Q_1 : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
f_1 : P_1 ⟶ Q_1
X : J
P Q : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
f : Functor.obj (karoubiFunctorCategoryEmbedding J C) P ⟶ Functor.obj (karoubiFunctorCategoryEmbedding J C) Q
j : J
⊢ (P.p ≫ { app := fun (j : J) ↦ (f.app j).f, naturality := ⋯ : NatTrans P.X Q.X } ≫ Q.p).app j =
    NatTrans.app { app := fun (j : J) ↦ (f.app j).f, naturality := ⋯ } j

Tactic:
exact (f.app j).comm

Premises used: CategoryTheory.Idempotents.Karoubi.Hom.comm, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
P Q : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
f : P ⟶ Q
X : J
X_1 Y : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
a₁ a₂ : X_1 ⟶ Y
h :
  Eq (α := Functor.obj (karoubiFunctorCategoryEmbedding J C) X_1 ⟶ Functor.obj (karoubiFunctorCategoryEmbedding J C) Y)
    (Functor.map (karoubiFunctorCategoryEmbedding J C) a₁) (Functor.map (karoubiFunctorCategoryEmbedding J C) a₂)
h₁ : ∀ (j : J), a₁.f.app j = a₂.f.app j
⊢ a₁ = a₂

Tactic:
ext j
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
P Q : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
f : P ⟶ Q
X : J
X_1 Y : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
a₁ a₂ : X_1 ⟶ Y
h :
  Eq (α := Functor.obj (karoubiFunctorCategoryEmbedding J C) X_1 ⟶ Functor.obj (karoubiFunctorCategoryEmbedding J C) Y)
    (Functor.map (karoubiFunctorCategoryEmbedding J C) a₁) (Functor.map (karoubiFunctorCategoryEmbedding J C) a₂)
j : J
⊢ a₁.f.app j = a₂.f.app j

Tactic:
hom_ext_iff.mp (congr_app h j)

Premises used: Iff.mp, CategoryTheory.congr_app, CategoryTheory.Idempotents.Karoubi.hom_ext_iff
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
P Q : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
f : P ⟶ Q
X : J
X_1 Y : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
a₁ a₂ : X_1 ⟶ Y
h :
  Eq (α := Functor.obj (karoubiFunctorCategoryEmbedding J C) X_1 ⟶ Functor.obj (karoubiFunctorCategoryEmbedding J C) Y)
    (Functor.map (karoubiFunctorCategoryEmbedding J C) a₁) (Functor.map (karoubiFunctorCategoryEmbedding J C) a₂)
j : J
⊢ a₁.f.app j = a₂.f.app j

Tactic:
exact hom_ext_iff.mp (congr_app h j)

Premises used: Iff.mp, CategoryTheory.congr_app, CategoryTheory.Idempotents.Karoubi.hom_ext_iff
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
h_map :
  autoParam
    (∀ (X Y : Functor.{v_1, v_2, u_1, u_2} J C) (f : X ⟶ Y),
      Eq (α :=
        Functor.obj (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) X ⟶
          Functor.obj (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) Y)
        (Functor.map (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) f)
        (CategoryStruct.comp (Y :=
          Functor.obj (Functor.obj (Functor.whiskeringRight J C (Karoubi.{v_2, u_2} C)) (toKaroubi C)) X) (eqToHom ⋯)
          (Functor.map (Functor.obj (Functor.whiskeringRight J C (Karoubi.{v_2, u_2} C)) (toKaroubi C)) f ≫ eqToHom ⋯)))
    Functor.ext._auto_1
h_obj :
  ∀ (X : Functor.{v_1, v_2, u_1, u_2} J C),
    Functor.obj (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) X =
      Functor.obj (Functor.obj (Functor.whiskeringRight J C (Karoubi.{v_2, u_2} C)) (toKaroubi C)) X
⊢ Eq (α := Functor.{v_1, v_2, u_1, u_2} J C ⥤ J ⥤ Karoubi.{v_2, u_2} C)
    (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C)
    (Functor.obj (Functor.whiskeringRight J C (Karoubi.{v_2, u_2} C)) (toKaroubi C))

Tactic:
apply Functor.ext

Premises used: CategoryTheory.Functor.ext
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
X Y : Functor.{v_1, v_2, u_1, u_2} J C
f : X ⟶ Y
h_map :
  ∀ (j : J),
    Eq (α :=
      ((Functor.obj (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) X).obj j).X ⟶
        ((Functor.obj (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) Y).obj j).X)
      (Hom.f
        (NatTrans.app
          (Functor.map (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) f) j))
      (Hom.f
        (NatTrans.app
          (CategoryStruct.comp (Y :=
            Functor.obj (Functor.obj (Functor.whiskeringRight J C (Karoubi.{v_2, u_2} C)) (toKaroubi C)) X) (eqToHom ⋯)
            (Functor.map (Functor.obj (Functor.whiskeringRight J C (Karoubi.{v_2, u_2} C)) (toKaroubi C)) f ≫
              eqToHom ⋯))
          j))
⊢ Eq (α :=
    Functor.obj (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) X ⟶
      Functor.obj (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) Y)
    (Functor.map (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) f)
    (CategoryStruct.comp (Y :=
      Functor.obj (Functor.obj (Functor.whiskeringRight J C (Karoubi.{v_2, u_2} C)) (toKaroubi C)) X) (eqToHom ⋯)
      (Functor.map (Functor.obj (Functor.whiskeringRight J C (Karoubi.{v_2, u_2} C)) (toKaroubi C)) f ≫ eqToHom ⋯))

Tactic:
ext j
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
X Y : Functor.{v_1, v_2, u_1, u_2} J C
f : X ⟶ Y
j : J
⊢ Eq (α :=
    ((Functor.obj (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) X).obj j).X ⟶
      ((Functor.obj (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) Y).obj j).X)
    (Hom.f
      (NatTrans.app (Functor.map (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) f)
        j))
    (Hom.f
      (NatTrans.app
        (CategoryStruct.comp (Y :=
          Functor.obj (Functor.obj (Functor.whiskeringRight J C (Karoubi.{v_2, u_2} C)) (toKaroubi C)) X) (eqToHom ⋯)
          (Functor.map (Functor.obj (Functor.whiskeringRight J C (Karoubi.{v_2, u_2} C)) (toKaroubi C)) f ≫ eqToHom ⋯))
        j))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
X : Functor.{v_1, v_2, u_1, u_2} J C
h_obj :
  autoParam
    (∀ (X_1 Y : J) (f : X_1 ⟶ Y),
      (Functor.obj (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) X).map f =
        eqToHom ⋯ ≫
          (Functor.obj (Functor.obj (Functor.whiskeringRight J C (Karoubi.{v_2, u_2} C)) (toKaroubi C)) X).map f ≫
            eqToHom ⋯)
    Functor.ext._auto_1
h_obj₁ :
  ∀ (X_1 : J),
    (Functor.obj (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) X).obj X_1 =
      (Functor.obj (Functor.obj (Functor.whiskeringRight J C (Karoubi.{v_2, u_2} C)) (toKaroubi C)) X).obj X_1
⊢ Functor.obj (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) X =
    Functor.obj (Functor.obj (Functor.whiskeringRight J C (Karoubi.{v_2, u_2} C)) (toKaroubi C)) X

Tactic:
apply Functor.ext

Premises used: CategoryTheory.Functor.ext
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
X : Functor.{v_1, v_2, u_1, u_2} J C
j j' : J
φ : j ⟶ j'
h_obj :
  ((Functor.obj (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) X).map φ).f =
    (eqToHom ⋯ ≫
        (Functor.obj (Functor.obj (Functor.whiskeringRight J C (Karoubi.{v_2, u_2} C)) (toKaroubi C)) X).map φ ≫
          eqToHom ⋯).f
⊢ (Functor.obj (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) X).map φ =
    eqToHom ⋯ ≫
      (Functor.obj (Functor.obj (Functor.whiskeringRight J C (Karoubi.{v_2, u_2} C)) (toKaroubi C)) X).map φ ≫ eqToHom ⋯

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
X : Functor.{v_1, v_2, u_1, u_2} J C
j j' : J
φ : j ⟶ j'
⊢ ((Functor.obj (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) X).map φ).f =
    (eqToHom ⋯ ≫
        (Functor.obj (Functor.obj (Functor.whiskeringRight J C (Karoubi.{v_2, u_2} C)) (toKaroubi C)) X).map φ ≫
          eqToHom ⋯).f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
X : Functor.{v_1, v_2, u_1, u_2} J C
j : J
⊢ (Functor.obj (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) X).obj j =
    (Functor.obj (Functor.obj (Functor.whiskeringRight J C (Karoubi.{v_2, u_2} C)) (toKaroubi C)) X).obj j

Tactic:
rfl
-- 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
F G : Karoubi.{v_1, u_1} C ⥤ D
φ : F ⟶ G
P : Karoubi.{v_1, u_1} C
rw : φ.app P = F.map (P.decompId_i ≫ P.decompId_p) ≫ φ.app P
⊢ φ.app P = F.map P.decompId_i ≫ φ.app { X := P.X, p := 𝟙 P.X, idem := ⋯ } ≫ G.map P.decompId_p

Tactic:
rw [← φ.naturality, ← assoc, ← F.map_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.NatTrans.naturality, 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
F G : Karoubi.{v_1, u_1} C ⥤ D
φ : F ⟶ G
P : Karoubi.{v_1, u_1} C
rw : F.map (𝟙 P) ≫ φ.app P
| φ.app P

Tactic:
rw [← id_comp (φ.app P), ← F.map_id]

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.NatTrans.app, CategoryTheory.Category.id_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
F G : Karoubi.{v_1, u_1} C ⥤ D
φ : F ⟶ G
P : Karoubi.{v_1, u_1} C
conv_lhs : F.map (𝟙 P) ≫ φ.app P = F.map (P.decompId_i ≫ P.decompId_p) ≫ φ.app P
⊢ φ.app P = F.map (P.decompId_i ≫ P.decompId_p) ≫ φ.app P

Tactic:
conv_lhs => rw [← id_comp (φ.app P), ← F.map_id]

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.NatTrans.app, CategoryTheory.Category.id_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
F G : Karoubi.{v_1, u_1} C ⥤ D
φ : F ⟶ G
P : Karoubi.{v_1, u_1} C
e_a : 𝟙 P = P.decompId_i ≫ P.decompId_p
⊢ F.map (𝟙 P) ≫ φ.app P = F.map (P.decompId_i ≫ P.decompId_p) ≫ φ.app P

Tactic:
congr
-- 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
F G : Karoubi.{v_1, u_1} C ⥤ D
φ : F ⟶ G
P : Karoubi.{v_1, u_1} C
⊢ 𝟙 P = P.decompId_i ≫ P.decompId_p

Tactic:
apply decompId

Premises used: CategoryTheory.Idempotents.Karoubi.decompId
-- 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
⊢ (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f

Tactic:
simpa only [F.map_comp, hom_ext_iff] using F.congr_map P.idem

Premises used: CategoryTheory.Idempotents.Karoubi.idem, 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
F : C ⥤ Karoubi.{v_2, u_2} D
X Y : Karoubi.{v_1, u_1} C
f : X ⟶ Y
⊢ { X := (F.obj X.X).X, p := (F.map X.p).f, idem := ⋯ : Karoubi.{v_2, u_2} D }.p ≫
      (F.map f.f).f ≫ { X := (F.obj Y.X).X, p := (F.map Y.p).f, idem := ⋯ : Karoubi.{v_2, u_2} D }.p =
    (F.map f.f).f

Tactic:
simpa only [F.map_comp, hom_ext_iff] using F.congr_map f.comm

Premises used: CategoryTheory.Idempotents.Karoubi.Hom.comm, 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
F G : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
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 : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
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 : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
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, Karoubi.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 : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
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, Karoubi.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 : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
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
simp : (F.map P.p).f ≫ (F.map P.p).f ≫ (F.map P.p).f ≫ Hom.f (φ.app P.X) = (F.map P.p).f ≫ Hom.f (φ.app P.X)
⊢ ((obj F).obj P).p ≫ ((F.map P.p).f ≫ Hom.f (φ.app P.X)) ≫ ((obj G).obj P).p = (F.map P.p).f ≫ Hom.f (φ.app P.X)

Tactic:
simp only [obj_obj_p, assoc, ← h]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Idempotents.FunctorExtension₁.obj_obj_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 : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
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 ≫ (F.map P.p).f

Tactic:
rw [h', 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
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
slice_lhs : (F.map P.p).f ≫ (F.map P.p).f ≫ (F.map P.p).f ≫ Hom.f (φ.app P.X) = (F.map P.p).f ≫ Hom.f (φ.app P.X)
slice_lhs₁ : (F.map P.p).f ≫ Hom.f (φ.app P.X) = (F.map P.p).f ≫ Hom.f (φ.app P.X)
⊢ (F.map P.p).f ≫ (F.map P.p).f ≫ (F.map P.p).f ≫ Hom.f (φ.app P.X) = (F.map P.p).f ≫ Hom.f (φ.app P.X)

Tactic:
slice_lhs 1 3 => rw [h', 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 :
  ((obj F).map f ≫
        { f := (F.map x_1.p).f ≫ Hom.f (φ.app x_1.X), comm := ⋯ : ((obj F).obj x_1).Hom ((obj G).obj x_1) }).f =
    Hom.f ({ f := (F.map x.p).f ≫ Hom.f (φ.app x.X), comm := ⋯ : ((obj F).obj x).Hom ((obj G).obj x) } ≫ (obj G).map f)
⊢ (obj F).map f ≫ { f := (F.map x_1.p).f ≫ Hom.f (φ.app x_1.X), comm := ⋯ : ((obj F).obj x_1).Hom ((obj G).obj x_1) } =
    { f := (F.map x.p).f ≫ Hom.f (φ.app x.X), comm := ⋯ : ((obj F).obj x).Hom ((obj G).obj x) } ≫ (obj G).map f

Tactic:
ext
-- 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 ≫ (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
⊢ ((obj F).map f ≫
        { f := (F.map x_1.p).f ≫ Hom.f (φ.app x_1.X), comm := ⋯ : ((obj F).obj x_1).Hom ((obj G).obj x_1) }).f =
    Hom.f ({ f := (F.map x.p).f ≫ Hom.f (φ.app x.X), comm := ⋯ : ((obj F).obj x).Hom ((obj G).obj x) } ≫ (obj G).map f)

Tactic:
dsimp [obj]

Premises used: CategoryTheory.Idempotents.FunctorExtension₁.obj
-- 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
⊢ F.map f.f ≫ φ.app x_1.X = φ.app x.X ≫ 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 : 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 ≫ φ.app x_1.X = φ.app x.X ≫ G.map f.f
⊢ F.map (f.f ≫ x_1.p) = F.map f.f

Tactic:
have h' := F.congr_map (comp_p 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 : 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 ≫ φ.app x_1.X = φ.app x.X ≫ G.map f.f
h' : F.map (f.f ≫ x_1.p) = F.map f.f
⊢ F.map (x.p ≫ f.f) = F.map f.f

Tactic:
have h'' := F.congr_map (p_comp 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 : 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 ≫ φ.app x_1.X = φ.app x.X ≫ G.map f.f
h' : F.map (f.f ≫ x_1.p) = F.map f.f
h'' : F.map (x.p ≫ f.f) = F.map f.f
⊢ (F.map f.f).f ≫ Hom.f (φ.app x_1.X) = Hom.f (φ.app x.X) ≫ (G.map f.f).f

Tactic:
simp only [hom_ext_iff, Functor.map_comp, comp_f] at h 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 : 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 ≫ φ.app x_1.X = φ.app x.X ≫ G.map f.f
h' : F.map (f.f ≫ x_1.p) = F.map f.f
h'' : F.map (x.p ≫ f.f) = F.map f.f
h₁ : (F.map f.f).f ≫ Hom.f (φ.app x_1.X) = Hom.f (φ.app x.X) ≫ (G.map f.f).f
⊢ (F.map f.f).f ≫ (F.map x_1.p).f = (F.map f.f).f

Tactic:
simp only [hom_ext_iff, Functor.map_comp, comp_f] at h 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 : 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 ≫ φ.app x_1.X = φ.app x.X ≫ G.map f.f
h' : F.map (f.f ≫ x_1.p) = F.map f.f
h'' : F.map (x.p ≫ f.f) = F.map f.f
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
⊢ (F.map x.p).f ≫ (F.map f.f).f = (F.map f.f).f

Tactic:
simp only [hom_ext_iff, Functor.map_comp, comp_f] at h 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 : 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 ≫ Hom.f (φ.app x_1.X)
| Hom.f (φ.app x.X) ≫ (G.map f.f).f

Tactic:
rw [← h]