awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Idempotents.Biproducts
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
P : Karoubi.{v, u_1} C
⊢ (CategoryStruct.comp (Y := P ⊞ P.complement) (biprod.lift P.decompId_p P.complement.decompId_p)
        (biprod.desc P.decompId_i P.complement.decompId_i)).f =
    Hom.f (𝟙 (Functor.obj (toKaroubi C) P.X))

Tactic:
simp only [toKaroubi_obj_X, biprod.lift_desc, add_def, comp_f, decompId_p_f, decompId_i_f,
      idem, complement_X, complement_p, comp_sub, comp_id, sub_comp, id_comp, sub_self, sub_zero,
      add_sub_cancel, id_f, toKaroubi_obj_p]

Premises used: sub_self, CategoryTheory.Idempotents.add_def, sub_zero, CategoryTheory.Idempotents.Karoubi.id_f, CategoryTheory.Idempotents.Karoubi.comp_f, CategoryTheory.Category.comp_id, CategoryTheory.Idempotents.Karoubi.decompId_i_f, add_sub_cancel, CategoryTheory.Idempotents.Karoubi.complement_p, CategoryTheory.Idempotents.Karoubi.idem, CategoryTheory.Idempotents.Karoubi.decompId_p_f, CategoryTheory.Idempotents.Karoubi.complement_X, CategoryTheory.Idempotents.toKaroubi_obj_X, CategoryTheory.Preadditive.comp_sub, CategoryTheory.Preadditive.sub_comp, CategoryTheory.Limits.biprod.lift_desc, CategoryTheory.Idempotents.toKaroubi_obj_p, CategoryTheory.Category.id_comp
-- 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 : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
X : J
⊢ P.p.app X ≫ P.p.app X = P.p.app X

Tactic:
congr_app P.idem X

Premises used: CategoryTheory.Idempotents.Karoubi.idem, CategoryTheory.congr_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
⊢ P.p.app X ≫ f.f.app X = f.f.app X

Tactic:
congr_app (p_comp f) X

Premises used: CategoryTheory.Idempotents.Karoubi.p_comp, CategoryTheory.congr_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
⊢ f.f.app X ≫ Q.p.app X = f.f.app X

Tactic:
congr_app (comp_p f) X

Premises used: CategoryTheory.Idempotents.Karoubi.comp_p, CategoryTheory.congr_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
⊢ P.p.app X ≫ f.f.app X = f.f.app X ≫ Q.p.app X

Tactic:
congr_app (p_comm f) X

Premises used: CategoryTheory.congr_app, CategoryTheory.Idempotents.Karoubi.p_comm
-- 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
inst_2 : IsIdempotentComplete.{v_2, u_2} C
⊢ IsIdempotentComplete (Functor.{v_1, v_2, u_1, u_2} J C)

Tactic:
⟨fun F p hp => ?_⟩

Premises used: CategoryTheory.IsIdempotentComplete.mk
-- 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
inst_2 : IsIdempotentComplete.{v_2, u_2} C
refine :
  ∀ (F : Functor.{v_1, v_2, u_1, u_2} J C) (p : F ⟶ F) (hp : p ≫ p = p),
    ∃ (Y : Functor.{v_1, v_2, u_1, u_2} J C) (i : Y ⟶ F) (e : F ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p
⊢ IsIdempotentComplete (Functor.{v_1, v_2, u_1, u_2} J C)

Tactic:
refine ⟨fun F p hp => ?_⟩
-- 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
inst_2 : IsIdempotentComplete.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
p : F ⟶ F
hp : p ≫ p = p
⊢ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p

Tactic:
have hC := (isIdempotentComplete_iff_hasEqualizer_of_id_and_idempotent C).mp inferInstance
-- 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
inst_2 : IsIdempotentComplete.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
p : F ⟶ F
hp : p ≫ p = p
hC : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
⊢ ∀ (j : J), HasEqualizer (𝟙 (F.obj j)) (p.app j)

Tactic:
haveI : ∀ j : J, HasEqualizer (𝟙 _) (p.app j) := fun j => hC _ _ (congr_app hp 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
inst_2 : IsIdempotentComplete.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
p : F ⟶ F
hp : p ≫ p = p
hC : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
this : ∀ (j : J), HasEqualizer (𝟙 (F.obj j)) (p.app j)
j j' : J
φ : j ⟶ j'
rw :
  Eq (α := equalizer (𝟙 (F.obj j)) (p.app j) ⟶ F.obj j') (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ)
    ((equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ≫ p.app j')
rw₁ :
  Eq (α := equalizer (𝟙 (F.obj j)) (p.app j) ⟶ F.obj j') (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ)
    (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ ≫ p.app j')
rw₂ :
  Eq (α := equalizer (𝟙 (F.obj j)) (p.app j) ⟶ F.obj j') (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ)
    (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ p.app j ≫ F.map φ)
rw₃ :
  Eq (α := equalizer (𝟙 (F.obj j)) (p.app j) ⟶ F.obj j') (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ)
    ((equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ p.app j) ≫ F.map φ)
rw₄ :
  Eq (α := equalizer (𝟙 (F.obj j)) (p.app j) ⟶ F.obj j') (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ)
    ((equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ 𝟙 (F.obj j)) ≫ F.map φ)
rw₅ rw₆ :
  Eq (α := equalizer (𝟙 (F.obj j)) (p.app j) ⟶ F.obj j') (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ)
    (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ)
⊢ Eq (α := equalizer (𝟙 (F.obj j)) (p.app j) ⟶ F.obj j')
    ((equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ≫ 𝟙 (F.obj j'))
    ((equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ≫ p.app j')

Tactic:
rw [comp_id, assoc, p.naturality φ, ← assoc, ← Limits.equalizer.condition, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.equalizer.condition, CategoryTheory.Category.comp_id, CategoryTheory.NatTrans.naturality
-- 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
inst_2 : IsIdempotentComplete.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
p : F ⟶ F
hp : p ≫ p = p
hC : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
this : ∀ (j : J), HasEqualizer (𝟙 (F.obj j)) (p.app j)
Y : Functor.{v_1, v_2, u_1, u_2} J C :=
  { obj := fun (j : J) ↦ equalizer (𝟙 (F.obj j)) (p.app j),
    map := fun {j j' : J} (φ : j ⟶ j') ↦ equalizer.lift (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ⋯, map_id := ⋯,
    map_comp := ⋯ }
x x_1 : J
x_2 : x ⟶ x_1
rw rw₁ :
  Eq (α := Y.obj x ⟶ F.obj x_1) (equalizer.ι (𝟙 (F.obj x)) (p.app x) ≫ F.map x_2)
    (equalizer.ι (𝟙 (F.obj x)) (p.app x) ≫ F.map x_2)
⊢ Y.map x_2 ≫ equalizer.ι (𝟙 (F.obj x_1)) (p.app x_1) = equalizer.ι (𝟙 (F.obj x)) (p.app x) ≫ F.map x_2

Tactic:
rw [equalizer.lift_ι]

Premises used: CategoryTheory.Limits.equalizer.lift_ι
-- 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
inst_2 : IsIdempotentComplete.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
p : F ⟶ F
hp : p ≫ p = p
hC : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
this : ∀ (j : J), HasEqualizer (𝟙 (F.obj j)) (p.app j)
Y : Functor.{v_1, v_2, u_1, u_2} J C :=
  { obj := fun (j : J) ↦ equalizer (𝟙 (F.obj j)) (p.app j),
    map := fun {j j' : J} (φ : j ⟶ j') ↦ equalizer.lift (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ⋯, map_id := ⋯,
    map_comp := ⋯ }
i : Y ⟶ F := { app := fun (j : J) ↦ equalizer.ι (𝟙 (F.obj j)) (p.app j), naturality := ⋯ }
j : J
⊢ p.app j ≫ 𝟙 (F.obj j) = p.app j ≫ p.app j

Tactic:
simpa only [comp_id] using (congr_app hp j).symm

Premises used: CategoryTheory.Category.comp_id, Eq.symm, CategoryTheory.congr_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
inst_2 : IsIdempotentComplete.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
p : F ⟶ F
hp : p ≫ p = p
hC : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
this : ∀ (j : J), HasEqualizer (𝟙 (F.obj j)) (p.app j)
Y : Functor.{v_1, v_2, u_1, u_2} J C :=
  { obj := fun (j : J) ↦ equalizer (𝟙 (F.obj j)) (p.app j),
    map := fun {j j' : J} (φ : j ⟶ j') ↦ equalizer.lift (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ⋯, map_id := ⋯,
    map_comp := ⋯ }
i : Y ⟶ F := { app := fun (j : J) ↦ equalizer.ι (𝟙 (F.obj j)) (p.app j), naturality := ⋯ }
j j' : J
φ : j ⟶ j'
⊢ CategoryStruct.comp (Y := equalizer (𝟙 (F.obj j')) (p.app j')) (F.map φ ≫ equalizer.lift (p.app j') ⋯)
      (equalizer.ι (𝟙 (F.obj j')) (p.app j')) =
    (equalizer.lift (p.app j) ⋯ ≫ Y.map φ) ≫ equalizer.ι (𝟙 (F.obj j')) (p.app j')

Tactic:
simp [Y]
-- 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
inst_2 : IsIdempotentComplete.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
p : F ⟶ F
hp : p ≫ p = p
hC : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
this : ∀ (j : J), HasEqualizer (𝟙 (F.obj j)) (p.app j)
Y : Functor.{v_1, v_2, u_1, u_2} J C :=
  { obj := fun (j : J) ↦ equalizer (𝟙 (F.obj j)) (p.app j),
    map := fun {j j' : J} (φ : j ⟶ j') ↦ equalizer.lift (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ⋯, map_id := ⋯,
    map_comp := ⋯ }
i : Y ⟶ F := { app := fun (j : J) ↦ equalizer.ι (𝟙 (F.obj j)) (p.app j), naturality := ⋯ }
e : F ⟶ Y := { app := fun (j : J) ↦ equalizer.lift (p.app j) ⋯, naturality := ⋯ }
h : i ≫ e = 𝟙 Y ∧ e ≫ i = p
⊢ ∃ (Y : Functor.{v_1, v_2, u_1, u_2} J C) (i : Y ⟶ F) (e : F ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p

Tactic:
use Y, i, e
-- 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
inst_2 : IsIdempotentComplete.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
p : F ⟶ F
hp : p ≫ p = p
hC : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
this : ∀ (j : J), HasEqualizer (𝟙 (F.obj j)) (p.app j)
Y : Functor.{v_1, v_2, u_1, u_2} J C :=
  { obj := fun (j : J) ↦ equalizer (𝟙 (F.obj j)) (p.app j),
    map := fun {j j' : J} (φ : j ⟶ j') ↦ equalizer.lift (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ⋯, map_id := ⋯,
    map_comp := ⋯ }
i : Y ⟶ F := { app := fun (j : J) ↦ equalizer.ι (𝟙 (F.obj j)) (p.app j), naturality := ⋯ }
e : F ⟶ Y := { app := fun (j : J) ↦ equalizer.lift (p.app j) ⋯, naturality := ⋯ }
h : i ≫ e = 𝟙 Y
h₁ : e ≫ i = p
⊢ i ≫ e = 𝟙 Y ∧ e ≫ i = p

Tactic:
constructor
-- 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
inst_2 : IsIdempotentComplete.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
p : F ⟶ F
hp : p ≫ p = p
hC : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
this : ∀ (j : J), HasEqualizer (𝟙 (F.obj j)) (p.app j)
Y : Functor.{v_1, v_2, u_1, u_2} J C :=
  { obj := fun (j : J) ↦ equalizer (𝟙 (F.obj j)) (p.app j),
    map := fun {j j' : J} (φ : j ⟶ j') ↦ equalizer.lift (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ⋯, map_id := ⋯,
    map_comp := ⋯ }
i : Y ⟶ F := { app := fun (j : J) ↦ equalizer.ι (𝟙 (F.obj j)) (p.app j), naturality := ⋯ }
e : F ⟶ Y := { app := fun (j : J) ↦ equalizer.lift (p.app j) ⋯, naturality := ⋯ }
h :
  ∀ (j : J),
    (i ≫ e).app j ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j) = NatTrans.app (𝟙 Y) j ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j)
⊢ i ≫ e = 𝟙 Y

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
inst_2 : IsIdempotentComplete.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
p : F ⟶ F
hp : p ≫ p = p
hC : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
this : ∀ (j : J), HasEqualizer (𝟙 (F.obj j)) (p.app j)
Y : Functor.{v_1, v_2, u_1, u_2} J C :=
  { obj := fun (j : J) ↦ equalizer (𝟙 (F.obj j)) (p.app j),
    map := fun {j j' : J} (φ : j ⟶ j') ↦ equalizer.lift (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ⋯, map_id := ⋯,
    map_comp := ⋯ }
i : Y ⟶ F := { app := fun (j : J) ↦ equalizer.ι (𝟙 (F.obj j)) (p.app j), naturality := ⋯ }
e : F ⟶ Y := { app := fun (j : J) ↦ equalizer.lift (p.app j) ⋯, naturality := ⋯ }
j : J
h : (i.app j ≫ e.app j) ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j) = 𝟙 (Y.obj j) ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j)
⊢ (i ≫ e).app j ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j) = NatTrans.app (𝟙 Y) j ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j)

Tactic:
dsimp
-- 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
inst_2 : IsIdempotentComplete.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
p : F ⟶ F
hp : p ≫ p = p
hC : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
this : ∀ (j : J), HasEqualizer (𝟙 (F.obj j)) (p.app j)
Y : Functor.{v_1, v_2, u_1, u_2} J C :=
  { obj := fun (j : J) ↦ equalizer (𝟙 (F.obj j)) (p.app j),
    map := fun {j j' : J} (φ : j ⟶ j') ↦ equalizer.lift (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ⋯, map_id := ⋯,
    map_comp := ⋯ }
i : Y ⟶ F := { app := fun (j : J) ↦ equalizer.ι (𝟙 (F.obj j)) (p.app j), naturality := ⋯ }
e : F ⟶ Y := { app := fun (j : J) ↦ equalizer.lift (p.app j) ⋯, naturality := ⋯ }
j : J
h : i.app j ≫ e.app j ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j) = 𝟙 (Y.obj j) ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j)
h₁ : i.app j ≫ p.app j = 𝟙 (Y.obj j) ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j)
h₂ : equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ 𝟙 (F.obj j) = 𝟙 (Y.obj j) ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j)
h₃ :
  Eq (α := Y.obj j ⟶ F.obj j) (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ 𝟙 (F.obj j)) (equalizer.ι (𝟙 (F.obj j)) (p.app j))
h₄ h₅ : Eq (α := Y.obj j ⟶ F.obj j) (equalizer.ι (𝟙 (F.obj j)) (p.app j)) (equalizer.ι (𝟙 (F.obj j)) (p.app j))
⊢ (i.app j ≫ e.app j) ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j) = 𝟙 (Y.obj j) ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j)

Tactic:
rw [assoc, equalizer.lift_ι, ← equalizer.condition, id_comp, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.equalizer.lift_ι, CategoryTheory.Limits.equalizer.condition, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- 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
inst_2 : IsIdempotentComplete.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
p : F ⟶ F
hp : p ≫ p = p
hC : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
this : ∀ (j : J), HasEqualizer (𝟙 (F.obj j)) (p.app j)
Y : Functor.{v_1, v_2, u_1, u_2} J C :=
  { obj := fun (j : J) ↦ equalizer (𝟙 (F.obj j)) (p.app j),
    map := fun {j j' : J} (φ : j ⟶ j') ↦ equalizer.lift (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ⋯, map_id := ⋯,
    map_comp := ⋯ }
i : Y ⟶ F := { app := fun (j : J) ↦ equalizer.ι (𝟙 (F.obj j)) (p.app j), naturality := ⋯ }
e : F ⟶ Y := { app := fun (j : J) ↦ equalizer.lift (p.app j) ⋯, naturality := ⋯ }
h : ∀ (j : J), (e ≫ i).app j = p.app j
⊢ e ≫ i = p

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
inst_2 : IsIdempotentComplete.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
p : F ⟶ F
hp : p ≫ p = p
hC : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
this : ∀ (j : J), HasEqualizer (𝟙 (F.obj j)) (p.app j)
Y : Functor.{v_1, v_2, u_1, u_2} J C :=
  { obj := fun (j : J) ↦ equalizer (𝟙 (F.obj j)) (p.app j),
    map := fun {j j' : J} (φ : j ⟶ j') ↦ equalizer.lift (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ⋯, map_id := ⋯,
    map_comp := ⋯ }
i : Y ⟶ F := { app := fun (j : J) ↦ equalizer.ι (𝟙 (F.obj j)) (p.app j), naturality := ⋯ }
e : F ⟶ Y := { app := fun (j : J) ↦ equalizer.lift (p.app j) ⋯, naturality := ⋯ }
j : J
⊢ (e ≫ i).app j = p.app j

Tactic:
simp [Y, i, e]
-- 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 : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
f : P_1 ⟶ Q
X : J
P : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
j j' : J
φ : j ⟶ j'
simp : P.p.app j ≫ P.p.app j ≫ P.p.app j ≫ P.X.map φ = P.p.app j ≫ P.X.map φ
⊢ { X := P.X.obj j, p := P.p.app j, idem := ⋯ : Karoubi.{v_2, u_2} C }.p ≫
      (P.p.app j ≫ P.X.map φ) ≫ { X := P.X.obj j', p := P.p.app j', idem := ⋯ : Karoubi.{v_2, u_2} C }.p =
    P.p.app j ≫ P.X.map φ

Tactic:
simp only [NatTrans.naturality, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.NatTrans.naturality
-- 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 : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
f : P_1 ⟶ Q
X : J
P : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
j j' : J
φ : j ⟶ j'
⊢ (P.p ≫ P.p).app j = P.p.app j

Tactic:
have h := congr_app P.idem 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 : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
f : P_1 ⟶ Q
X : J
P : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
j j' : J
φ : j ⟶ j'
h : (P.p ≫ P.p).app j = P.p.app j
⊢ P.p.app j ≫ P.p.app j = P.p.app j

Tactic:
rw [NatTrans.comp_app] at h

Premises used: CategoryTheory.NatTrans.comp_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 : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
f : P_1 ⟶ Q
X : J
P : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
j j' : J
φ : j ⟶ j'
h : P.p.app j ≫ P.p.app j = P.p.app j
rw : P.p.app j ≫ P.p.app j ≫ P.X.map φ = P.p.app j ≫ P.X.map φ
rw₁ rw₂ : P.p.app j ≫ P.X.map φ = P.p.app j ≫ P.X.map φ
⊢ P.p.app j ≫ P.p.app j ≫ P.p.app j ≫ P.X.map φ = P.p.app j ≫ P.X.map φ

Tactic:
rw [reassoc_of% h, reassoc_of% h]
-- 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' : J
φ : j ⟶ j'
rw :
  P.X.map φ ≫ (f.app j').f = (f.app j).f ≫ ((Functor.obj (karoubiFunctorCategoryEmbedding J C) Q).obj j).p ≫ Q.X.map φ
⊢ P.X.map φ ≫ (f.app j').f = (f.app j).f ≫ Q.X.map φ

Tactic:
rw [← Karoubi.comp_p_assoc]

Premises used: CategoryTheory.Idempotents.Karoubi.comp_p_assoc
-- 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' : J
φ : j ⟶ j'
⊢ ((Functor.obj (karoubiFunctorCategoryEmbedding J C) P).map φ ≫ f.app j').f =
    (f.app j ≫ (Functor.obj (karoubiFunctorCategoryEmbedding J C) Q).map φ).f

Tactic:
have h := hom_ext_iff.mp (f.naturality φ)
-- 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' : J
φ : j ⟶ j'
h : (P.p.app j ≫ P.X.map φ) ≫ (f.app j').f = (f.app j).f ≫ Q.p.app j ≫ Q.X.map φ
simp : P.X.map φ ≫ (f.app j').f = P.p.app j ≫ P.X.map φ ≫ (f.app j').f
⊢ P.X.map φ ≫ (f.app j').f = (f.app j).f ≫ ((Functor.obj (karoubiFunctorCategoryEmbedding J C) Q).obj j).p ≫ Q.X.map φ

Tactic:
simp only [assoc, h.symm, karoubiFunctorCategoryEmbedding_obj,
              KaroubiFunctorCategoryEmbedding.obj_obj_p]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Idempotents.karoubiFunctorCategoryEmbedding_obj, CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj_obj_p, Eq.symm
-- 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' : J
φ : j ⟶ j'
h : (P.p.app j ≫ P.X.map φ) ≫ (f.app j').f = (f.app j).f ≫ Q.p.app j ≫ Q.X.map φ
rw : P.X.map φ ≫ (f.app j').f = P.X.map φ ≫ P.p.app j' ≫ (f.app j').f
⊢ P.X.map φ ≫ (f.app j').f = P.p.app j ≫ P.X.map φ ≫ (f.app j').f

Tactic:
rw [← P.p.naturality_assoc]

Premises used: CategoryTheory.Idempotents.Karoubi.p, CategoryTheory.NatTrans.naturality_assoc
-- 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' : J
φ : j ⟶ j'
h : (P.p.app j ≫ P.X.map φ) ≫ (f.app j').f = (f.app j).f ≫ Q.p.app j ≫ Q.X.map φ
⊢ P.X.map φ ≫ (f.app j').f = P.X.map φ ≫ P.p.app j' ≫ (f.app j').f

Tactic:
congrArg _ (p_comp (f.app _)).symm

Premises used: congrArg, CategoryTheory.Idempotents.Karoubi.p_comp, Eq.symm, 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' : J
φ : j ⟶ j'
h : (P.p.app j ≫ P.X.map φ) ≫ (f.app j').f = (f.app j).f ≫ Q.p.app j ≫ Q.X.map φ
⊢ P.X.map φ ≫ (f.app j').f = P.X.map φ ≫ P.p.app j' ≫ (f.app j').f

Tactic:
exact congrArg _ (p_comp (f.app _)).symm

Premises used: congrArg, CategoryTheory.Idempotents.Karoubi.p_comp, Eq.symm, CategoryTheory.NatTrans.app