[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.4050, u_1} J
inst✝¹ : Category.{?u.4054, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
inst✝ : IsIdempotentComplete C
⊢ IsIdempotentComplete (J ⥤ C)
[PROOFSTEP]
refine' ⟨fun F p hp => _⟩
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.4050, u_1} J
inst✝¹ : Category.{?u.4054, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
inst✝ : IsIdempotentComplete C
F : J ⥤ C
p : F ⟶ F
hp : p ≫ p = p
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
[PROOFSTEP]
have hC := (isIdempotentComplete_iff_hasEqualizer_of_id_and_idempotent C).mp inferInstance
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.4050, u_1} J
inst✝¹ : Category.{?u.4054, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
inst✝ : IsIdempotentComplete C
F : J ⥤ C
p : F ⟶ F
hp : p ≫ p = p
hC : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
[PROOFSTEP]
haveI : ∀ j : J, HasEqualizer (𝟙 _) (p.app j) := fun j =>
  hC _ _
    (congr_app hp j)
      /- We construct the direct factor `Y` associated to `p : F ⟶ F` by computing
            the equalizer of the identity and `p.app j` on each object `(j : J)`.  -/
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.4050, u_1} J
inst✝¹ : Category.{?u.4054, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
inst✝ : IsIdempotentComplete C
F : 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)) (NatTrans.app p j)
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
[PROOFSTEP]
let Y : J ⥤ C :=
  { obj := fun j => Limits.equalizer (𝟙 _) (p.app j)
    map := fun {j j'} φ =>
      equalizer.lift (Limits.equalizer.ι (𝟙 _) (p.app j) ≫ F.map φ)
        (by rw [comp_id, assoc, p.naturality φ, ← assoc, ← Limits.equalizer.condition, comp_id]) }
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.4050, u_1} J
inst✝¹ : Category.{?u.4054, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
inst✝ : IsIdempotentComplete C
F : 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)) (NatTrans.app p j)
j j' : J
φ : j ⟶ j'
⊢ (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ) ≫ 𝟙 (F.obj j') =
    (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ) ≫ NatTrans.app p j'
[PROOFSTEP]
rw [comp_id, assoc, p.naturality φ, ← assoc, ← Limits.equalizer.condition, comp_id]
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.4050, u_1} J
inst✝¹ : Category.{?u.4054, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
inst✝ : IsIdempotentComplete C
F : 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)) (NatTrans.app p j)
Y : J ⥤ C :=
  Functor.mk
    { obj := fun j => equalizer (𝟙 (F.obj j)) (NatTrans.app p j),
      map := fun {j j'} φ =>
        equalizer.lift (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ)
          (_ :
            (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ) ≫ 𝟙 (F.obj j') =
              (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ) ≫ NatTrans.app p j') }
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
[PROOFSTEP]
let i : Y ⟶ F :=
  { app := fun j => equalizer.ι _ _
    naturality := fun _ _ _ => by rw [equalizer.lift_ι] }
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.4050, u_1} J
inst✝¹ : Category.{?u.4054, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
inst✝ : IsIdempotentComplete C
F : 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)) (NatTrans.app p j)
Y : J ⥤ C :=
  Functor.mk
    { obj := fun j => equalizer (𝟙 (F.obj j)) (NatTrans.app p j),
      map := fun {j j'} φ =>
        equalizer.lift (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ)
          (_ :
            (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ) ≫ 𝟙 (F.obj j') =
              (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ) ≫ NatTrans.app p j') }
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ Y.map x✝ ≫ (fun j => equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j)) x✝¹ =
    (fun j => equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j)) x✝² ≫ F.map x✝
[PROOFSTEP]
rw [equalizer.lift_ι]
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.4050, u_1} J
inst✝¹ : Category.{?u.4054, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
inst✝ : IsIdempotentComplete C
F : 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)) (NatTrans.app p j)
Y : J ⥤ C :=
  Functor.mk
    { obj := fun j => equalizer (𝟙 (F.obj j)) (NatTrans.app p j),
      map := fun {j j'} φ =>
        equalizer.lift (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ)
          (_ :
            (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ) ≫ 𝟙 (F.obj j') =
              (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ) ≫ NatTrans.app p j') }
i : Y ⟶ F := NatTrans.mk fun j => equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j)
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
[PROOFSTEP]
let e : F ⟶ Y :=
  { app := fun j => equalizer.lift (p.app j) (by simpa only [comp_id] using (congr_app hp j).symm)
    naturality := fun j j' φ => equalizer.hom_ext (by simp) }
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.4050, u_1} J
inst✝¹ : Category.{?u.4054, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
inst✝ : IsIdempotentComplete C
F : 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)) (NatTrans.app p j)
Y : J ⥤ C :=
  Functor.mk
    { obj := fun j => equalizer (𝟙 (F.obj j)) (NatTrans.app p j),
      map := fun {j j'} φ =>
        equalizer.lift (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ)
          (_ :
            (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ) ≫ 𝟙 (F.obj j') =
              (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ) ≫ NatTrans.app p j') }
i : Y ⟶ F := NatTrans.mk fun j => equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j)
j : J
⊢ NatTrans.app p j ≫ 𝟙 (F.obj j) = NatTrans.app p j ≫ NatTrans.app p j
[PROOFSTEP]
simpa only [comp_id] using (congr_app hp j).symm
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.4050, u_1} J
inst✝¹ : Category.{?u.4054, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
inst✝ : IsIdempotentComplete C
F : 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)) (NatTrans.app p j)
Y : J ⥤ C :=
  Functor.mk
    { obj := fun j => equalizer (𝟙 (F.obj j)) (NatTrans.app p j),
      map := fun {j j'} φ =>
        equalizer.lift (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ)
          (_ :
            (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ) ≫ 𝟙 (F.obj j') =
              (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ) ≫ NatTrans.app p j') }
i : Y ⟶ F := NatTrans.mk fun j => equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j)
j j' : J
φ : j ⟶ j'
⊢ (F.map φ ≫
        (fun j =>
            equalizer.lift (NatTrans.app p j)
              (_ : NatTrans.app p j ≫ 𝟙 (F.obj j) = NatTrans.app p j ≫ NatTrans.app p j))
          j') ≫
      equalizer.ι (𝟙 (F.obj j')) (NatTrans.app p j') =
    ((fun j =>
            equalizer.lift (NatTrans.app p j)
              (_ : NatTrans.app p j ≫ 𝟙 (F.obj j) = NatTrans.app p j ≫ NatTrans.app p j))
          j ≫
        Y.map φ) ≫
      equalizer.ι (𝟙 (F.obj j')) (NatTrans.app p j')
[PROOFSTEP]
simp
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.4050, u_1} J
inst✝¹ : Category.{?u.4054, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
inst✝ : IsIdempotentComplete C
F : 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)) (NatTrans.app p j)
Y : J ⥤ C :=
  Functor.mk
    { obj := fun j => equalizer (𝟙 (F.obj j)) (NatTrans.app p j),
      map := fun {j j'} φ =>
        equalizer.lift (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ)
          (_ :
            (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ) ≫ 𝟙 (F.obj j') =
              (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ) ≫ NatTrans.app p j') }
i : Y ⟶ F := NatTrans.mk fun j => equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j)
e : F ⟶ Y :=
  NatTrans.mk fun j =>
    equalizer.lift (NatTrans.app p j) (_ : NatTrans.app p j ≫ 𝟙 (F.obj j) = NatTrans.app p j ≫ NatTrans.app p j)
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
[PROOFSTEP]
use Y, i, e
[GOAL]
case h
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.4050, u_1} J
inst✝¹ : Category.{?u.4054, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
inst✝ : IsIdempotentComplete C
F : 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)) (NatTrans.app p j)
Y : J ⥤ C :=
  Functor.mk
    { obj := fun j => equalizer (𝟙 (F.obj j)) (NatTrans.app p j),
      map := fun {j j'} φ =>
        equalizer.lift (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ)
          (_ :
            (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ) ≫ 𝟙 (F.obj j') =
              (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ) ≫ NatTrans.app p j') }
i : Y ⟶ F := NatTrans.mk fun j => equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j)
e : F ⟶ Y :=
  NatTrans.mk fun j =>
    equalizer.lift (NatTrans.app p j) (_ : NatTrans.app p j ≫ 𝟙 (F.obj j) = NatTrans.app p j ≫ NatTrans.app p j)
⊢ i ≫ e = 𝟙 Y ∧ e ≫ i = p
[PROOFSTEP]
constructor
[GOAL]
case h.left
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.4050, u_1} J
inst✝¹ : Category.{?u.4054, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
inst✝ : IsIdempotentComplete C
F : 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)) (NatTrans.app p j)
Y : J ⥤ C :=
  Functor.mk
    { obj := fun j => equalizer (𝟙 (F.obj j)) (NatTrans.app p j),
      map := fun {j j'} φ =>
        equalizer.lift (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ)
          (_ :
            (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ) ≫ 𝟙 (F.obj j') =
              (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ) ≫ NatTrans.app p j') }
i : Y ⟶ F := NatTrans.mk fun j => equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j)
e : F ⟶ Y :=
  NatTrans.mk fun j =>
    equalizer.lift (NatTrans.app p j) (_ : NatTrans.app p j ≫ 𝟙 (F.obj j) = NatTrans.app p j ≫ NatTrans.app p j)
⊢ i ≫ e = 𝟙 Y
[PROOFSTEP]
ext j
[GOAL]
case h.left.w.h
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.4050, u_1} J
inst✝¹ : Category.{?u.4054, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
inst✝ : IsIdempotentComplete C
F : 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)) (NatTrans.app p j)
Y : J ⥤ C :=
  Functor.mk
    { obj := fun j => equalizer (𝟙 (F.obj j)) (NatTrans.app p j),
      map := fun {j j'} φ =>
        equalizer.lift (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ)
          (_ :
            (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ) ≫ 𝟙 (F.obj j') =
              (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ) ≫ NatTrans.app p j') }
i : Y ⟶ F := NatTrans.mk fun j => equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j)
e : F ⟶ Y :=
  NatTrans.mk fun j =>
    equalizer.lift (NatTrans.app p j) (_ : NatTrans.app p j ≫ 𝟙 (F.obj j) = NatTrans.app p j ≫ NatTrans.app p j)
j : J
⊢ NatTrans.app (i ≫ e) j = NatTrans.app (𝟙 Y) j
[PROOFSTEP]
apply equalizer.hom_ext
[GOAL]
case h.left.w.h.h
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.4050, u_1} J
inst✝¹ : Category.{?u.4054, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
inst✝ : IsIdempotentComplete C
F : 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)) (NatTrans.app p j)
Y : J ⥤ C :=
  Functor.mk
    { obj := fun j => equalizer (𝟙 (F.obj j)) (NatTrans.app p j),
      map := fun {j j'} φ =>
        equalizer.lift (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ)
          (_ :
            (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ) ≫ 𝟙 (F.obj j') =
              (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ) ≫ NatTrans.app p j') }
i : Y ⟶ F := NatTrans.mk fun j => equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j)
e : F ⟶ Y :=
  NatTrans.mk fun j =>
    equalizer.lift (NatTrans.app p j) (_ : NatTrans.app p j ≫ 𝟙 (F.obj j) = NatTrans.app p j ≫ NatTrans.app p j)
j : J
⊢ NatTrans.app (i ≫ e) j ≫ equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) =
    NatTrans.app (𝟙 Y) j ≫ equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j)
[PROOFSTEP]
dsimp
[GOAL]
case h.left.w.h.h
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.4050, u_1} J
inst✝¹ : Category.{?u.4054, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
inst✝ : IsIdempotentComplete C
F : 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)) (NatTrans.app p j)
Y : J ⥤ C :=
  Functor.mk
    { obj := fun j => equalizer (𝟙 (F.obj j)) (NatTrans.app p j),
      map := fun {j j'} φ =>
        equalizer.lift (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ)
          (_ :
            (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ) ≫ 𝟙 (F.obj j') =
              (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ) ≫ NatTrans.app p j') }
i : Y ⟶ F := NatTrans.mk fun j => equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j)
e : F ⟶ Y :=
  NatTrans.mk fun j =>
    equalizer.lift (NatTrans.app p j) (_ : NatTrans.app p j ≫ 𝟙 (F.obj j) = NatTrans.app p j ≫ NatTrans.app p j)
j : J
⊢ (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫
        equalizer.lift (NatTrans.app p j) (_ : NatTrans.app p j ≫ 𝟙 (F.obj j) = NatTrans.app p j ≫ NatTrans.app p j)) ≫
      equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) =
    𝟙 (equalizer (𝟙 (F.obj j)) (NatTrans.app p j)) ≫ equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j)
[PROOFSTEP]
rw [assoc, equalizer.lift_ι, ← equalizer.condition, id_comp, comp_id]
[GOAL]
case h.right
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.4050, u_1} J
inst✝¹ : Category.{?u.4054, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
inst✝ : IsIdempotentComplete C
F : 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)) (NatTrans.app p j)
Y : J ⥤ C :=
  Functor.mk
    { obj := fun j => equalizer (𝟙 (F.obj j)) (NatTrans.app p j),
      map := fun {j j'} φ =>
        equalizer.lift (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ)
          (_ :
            (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ) ≫ 𝟙 (F.obj j') =
              (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ) ≫ NatTrans.app p j') }
i : Y ⟶ F := NatTrans.mk fun j => equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j)
e : F ⟶ Y :=
  NatTrans.mk fun j =>
    equalizer.lift (NatTrans.app p j) (_ : NatTrans.app p j ≫ 𝟙 (F.obj j) = NatTrans.app p j ≫ NatTrans.app p j)
⊢ e ≫ i = p
[PROOFSTEP]
ext j
[GOAL]
case h.right.w.h
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.4050, u_1} J
inst✝¹ : Category.{?u.4054, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
inst✝ : IsIdempotentComplete C
F : 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)) (NatTrans.app p j)
Y : J ⥤ C :=
  Functor.mk
    { obj := fun j => equalizer (𝟙 (F.obj j)) (NatTrans.app p j),
      map := fun {j j'} φ =>
        equalizer.lift (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ)
          (_ :
            (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ) ≫ 𝟙 (F.obj j') =
              (equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j) ≫ F.map φ) ≫ NatTrans.app p j') }
i : Y ⟶ F := NatTrans.mk fun j => equalizer.ι (𝟙 (F.obj j)) (NatTrans.app p j)
e : F ⟶ Y :=
  NatTrans.mk fun j =>
    equalizer.lift (NatTrans.app p j) (_ : NatTrans.app p j ≫ 𝟙 (F.obj j) = NatTrans.app p j ≫ NatTrans.app p j)
j : J
⊢ NatTrans.app (e ≫ i) j = NatTrans.app p j
[PROOFSTEP]
simp
[GOAL]
J : Type u_1
C : Type u_2
inst✝¹ : Category.{?u.51695, u_1} J
inst✝ : Category.{?u.51699, u_2} C
P✝ Q : Karoubi (J ⥤ C)
f : P✝ ⟶ Q
X : J
P : Karoubi (J ⥤ C)
j j' : J
φ : j ⟶ j'
⊢ NatTrans.app P.p j ≫ P.X.map φ =
    ((fun j => Karoubi.mk (P.X.obj j) (NatTrans.app P.p j)) j).p ≫
      (NatTrans.app P.p j ≫ P.X.map φ) ≫ ((fun j => Karoubi.mk (P.X.obj j) (NatTrans.app P.p j)) j').p
[PROOFSTEP]
simp only [NatTrans.naturality, assoc]
[GOAL]
J : Type u_1
C : Type u_2
inst✝¹ : Category.{?u.51695, u_1} J
inst✝ : Category.{?u.51699, u_2} C
P✝ Q : Karoubi (J ⥤ C)
f : P✝ ⟶ Q
X : J
P : Karoubi (J ⥤ C)
j j' : J
φ : j ⟶ j'
⊢ NatTrans.app P.p j ≫ P.X.map φ = NatTrans.app P.p j ≫ NatTrans.app P.p j ≫ NatTrans.app P.p j ≫ P.X.map φ
[PROOFSTEP]
have h := congr_app P.idem j
[GOAL]
J : Type u_1
C : Type u_2
inst✝¹ : Category.{?u.51695, u_1} J
inst✝ : Category.{?u.51699, u_2} C
P✝ Q : Karoubi (J ⥤ C)
f : P✝ ⟶ Q
X : J
P : Karoubi (J ⥤ C)
j j' : J
φ : j ⟶ j'
h : NatTrans.app (P.p ≫ P.p) j = NatTrans.app P.p j
⊢ NatTrans.app P.p j ≫ P.X.map φ = NatTrans.app P.p j ≫ NatTrans.app P.p j ≫ NatTrans.app P.p j ≫ P.X.map φ
[PROOFSTEP]
rw [NatTrans.comp_app] at h 
[GOAL]
J : Type u_1
C : Type u_2
inst✝¹ : Category.{?u.51695, u_1} J
inst✝ : Category.{?u.51699, u_2} C
P✝ Q : Karoubi (J ⥤ C)
f : P✝ ⟶ Q
X : J
P : Karoubi (J ⥤ C)
j j' : J
φ : j ⟶ j'
h : NatTrans.app P.p j ≫ NatTrans.app P.p j = NatTrans.app P.p j
⊢ NatTrans.app P.p j ≫ P.X.map φ = NatTrans.app P.p j ≫ NatTrans.app P.p j ≫ NatTrans.app P.p j ≫ P.X.map φ
[PROOFSTEP]
erw [reassoc_of% h, reassoc_of% h]
[GOAL]
J : Type u_1
C : Type u_2
inst✝¹ : Category.{?u.62947, u_1} J
inst✝ : Category.{?u.62951, u_2} C
P✝ Q✝ : Karoubi (J ⥤ C)
f✝ : P✝ ⟶ Q✝
X : J
P Q : Karoubi (J ⥤ C)
f : (karoubiFunctorCategoryEmbedding J C).obj P ⟶ (karoubiFunctorCategoryEmbedding J C).obj Q
j j' : J
φ : j ⟶ j'
⊢ P.X.map φ ≫ (fun j => (NatTrans.app f j).f) j' = (fun j => (NatTrans.app f j).f) j ≫ Q.X.map φ
[PROOFSTEP]
rw [← Karoubi.comp_p_assoc]
[GOAL]
J : Type u_1
C : Type u_2
inst✝¹ : Category.{?u.62947, u_1} J
inst✝ : Category.{?u.62951, u_2} C
P✝ Q✝ : Karoubi (J ⥤ C)
f✝ : P✝ ⟶ Q✝
X : J
P Q : Karoubi (J ⥤ C)
f : (karoubiFunctorCategoryEmbedding J C).obj P ⟶ (karoubiFunctorCategoryEmbedding J C).obj Q
j j' : J
φ : j ⟶ j'
⊢ P.X.map φ ≫ (fun j => (NatTrans.app f j).f) j' =
    (NatTrans.app f j).f ≫ (((karoubiFunctorCategoryEmbedding J C).obj Q).obj j).p ≫ Q.X.map φ
[PROOFSTEP]
have h := hom_ext_iff.mp (f.naturality φ)
[GOAL]
J : Type u_1
C : Type u_2
inst✝¹ : Category.{?u.62947, u_1} J
inst✝ : Category.{?u.62951, u_2} C
P✝ Q✝ : Karoubi (J ⥤ C)
f✝ : P✝ ⟶ Q✝
X : J
P Q : Karoubi (J ⥤ C)
f : (karoubiFunctorCategoryEmbedding J C).obj P ⟶ (karoubiFunctorCategoryEmbedding J C).obj Q
j j' : J
φ : j ⟶ j'
h :
  (((karoubiFunctorCategoryEmbedding J C).obj P).map φ ≫ NatTrans.app f j').f =
    (NatTrans.app f j ≫ ((karoubiFunctorCategoryEmbedding J C).obj Q).map φ).f
⊢ P.X.map φ ≫ (fun j => (NatTrans.app f j).f) j' =
    (NatTrans.app f j).f ≫ (((karoubiFunctorCategoryEmbedding J C).obj Q).obj j).p ≫ Q.X.map φ
[PROOFSTEP]
simp only [comp_f] at h 
[GOAL]
J : Type u_1
C : Type u_2
inst✝¹ : Category.{?u.62947, u_1} J
inst✝ : Category.{?u.62951, u_2} C
P✝ Q✝ : Karoubi (J ⥤ C)
f✝ : P✝ ⟶ Q✝
X : J
P Q : Karoubi (J ⥤ C)
f : (karoubiFunctorCategoryEmbedding J C).obj P ⟶ (karoubiFunctorCategoryEmbedding J C).obj Q
j j' : J
φ : j ⟶ j'
h :
  (((karoubiFunctorCategoryEmbedding J C).obj P).map φ).f ≫ (NatTrans.app f j').f =
    (NatTrans.app f j).f ≫ (((karoubiFunctorCategoryEmbedding J C).obj Q).map φ).f
⊢ P.X.map φ ≫ (fun j => (NatTrans.app f j).f) j' =
    (NatTrans.app f j).f ≫ (((karoubiFunctorCategoryEmbedding J C).obj Q).obj j).p ≫ Q.X.map φ
[PROOFSTEP]
dsimp [karoubiFunctorCategoryEmbedding] at h 
[GOAL]
J : Type u_1
C : Type u_2
inst✝¹ : Category.{?u.62947, u_1} J
inst✝ : Category.{?u.62951, u_2} C
P✝ Q✝ : Karoubi (J ⥤ C)
f✝ : P✝ ⟶ Q✝
X : J
P Q : Karoubi (J ⥤ C)
f : (karoubiFunctorCategoryEmbedding J C).obj P ⟶ (karoubiFunctorCategoryEmbedding J C).obj Q
j j' : J
φ : j ⟶ j'
h : (NatTrans.app P.p j ≫ P.X.map φ) ≫ (NatTrans.app f j').f = (NatTrans.app f j).f ≫ NatTrans.app Q.p j ≫ Q.X.map φ
⊢ P.X.map φ ≫ (fun j => (NatTrans.app f j).f) j' =
    (NatTrans.app f j).f ≫ (((karoubiFunctorCategoryEmbedding J C).obj Q).obj j).p ≫ Q.X.map φ
[PROOFSTEP]
erw [← h, assoc, ← P.p.naturality_assoc φ, p_comp (f.app j')]
[GOAL]
J : Type u_1
C : Type u_2
inst✝¹ : Category.{?u.62947, u_1} J
inst✝ : Category.{?u.62951, u_2} C
P✝ Q✝ : Karoubi (J ⥤ C)
f✝ : P✝ ⟶ Q✝
X : J
P Q : Karoubi (J ⥤ C)
f : (karoubiFunctorCategoryEmbedding J C).obj P ⟶ (karoubiFunctorCategoryEmbedding J C).obj Q
⊢ (NatTrans.mk fun j => (NatTrans.app f j).f) = P.p ≫ (NatTrans.mk fun j => (NatTrans.app f j).f) ≫ Q.p
[PROOFSTEP]
ext j
[GOAL]
case w.h
J : Type u_1
C : Type u_2
inst✝¹ : Category.{?u.62947, u_1} J
inst✝ : Category.{?u.62951, u_2} C
P✝ Q✝ : Karoubi (J ⥤ C)
f✝ : P✝ ⟶ Q✝
X : J
P Q : Karoubi (J ⥤ C)
f : (karoubiFunctorCategoryEmbedding J C).obj P ⟶ (karoubiFunctorCategoryEmbedding J C).obj Q
j : J
⊢ NatTrans.app (NatTrans.mk fun j => (NatTrans.app f j).f) j =
    NatTrans.app (P.p ≫ (NatTrans.mk fun j => (NatTrans.app f j).f) ≫ Q.p) j
[PROOFSTEP]
exact (f.app j).comm
[GOAL]
J : Type u_1
C : Type u_2
inst✝¹ : Category.{?u.66385, u_1} J
inst✝ : Category.{?u.66389, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
X✝ Y✝ : Karoubi (J ⥤ C)
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : (karoubiFunctorCategoryEmbedding J C).map a₁✝ = (karoubiFunctorCategoryEmbedding J C).map a₂✝
⊢ a₁✝ = a₂✝
[PROOFSTEP]
ext j
[GOAL]
case h.w.h
J : Type u_1
C : Type u_2
inst✝¹ : Category.{?u.66385, u_1} J
inst✝ : Category.{?u.66389, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
X✝ Y✝ : Karoubi (J ⥤ C)
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : (karoubiFunctorCategoryEmbedding J C).map a₁✝ = (karoubiFunctorCategoryEmbedding J C).map a₂✝
j : J
⊢ NatTrans.app a₁✝.f j = NatTrans.app a₂✝.f j
[PROOFSTEP]
exact hom_ext_iff.mp (congr_app h j)
[GOAL]
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
⊢ toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C = (whiskeringRight J C (Karoubi C)).obj (toKaroubi C)
[PROOFSTEP]
apply Functor.ext
[GOAL]
case h_map
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
⊢ autoParam
    (∀ (X Y : J ⥤ C) (f : X ⟶ Y),
      (toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).map f =
        eqToHom (_ : ?F.obj X = ?G.obj X) ≫
          ((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).map f ≫
            eqToHom
              (_ :
                ((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj Y =
                  (toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj Y))
    _auto✝
[PROOFSTEP]
intro X Y f
[GOAL]
case h_map
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
P Q : Karoubi (J ⥤ C)
f✝ : P ⟶ Q
X✝ : J
X Y : J ⥤ C
f : X ⟶ Y
⊢ (toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).map f =
    eqToHom (_ : ?F.obj X = ?G.obj X) ≫
      ((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).map f ≫
        eqToHom
          (_ :
            ((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj Y =
              (toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj Y)
[PROOFSTEP]
ext j
[GOAL]
case h_map.w.h.h
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
P Q : Karoubi (J ⥤ C)
f✝ : P ⟶ Q
X✝ : J
X Y : J ⥤ C
f : X ⟶ Y
j : J
⊢ (NatTrans.app ((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).map f) j).f =
    (NatTrans.app
        (eqToHom (_ : ?F.obj X = ?G.obj X) ≫
          ((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).map f ≫
            eqToHom
              (_ :
                ((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj Y =
                  (toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj Y))
        j).f
[PROOFSTEP]
dsimp [toKaroubi]
[GOAL]
case h_map.w.h.h
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
P Q : Karoubi (J ⥤ C)
f✝ : P ⟶ Q
X✝ : J
X Y : J ⥤ C
f : X ⟶ Y
j : J
⊢ NatTrans.app f j =
    (NatTrans.app (eqToHom (_ : ?F.obj X = ?G.obj X)) j).f ≫
      NatTrans.app f j ≫
        (NatTrans.app
            (eqToHom
              (_ :
                Y ⋙ Functor.mk { obj := fun X => Karoubi.mk X (𝟙 X), map := fun {X Y} f => Hom.mk f } =
                  KaroubiFunctorCategoryEmbedding.obj (Karoubi.mk Y (𝟙 Y))))
            j).f
[PROOFSTEP]
simp only [eqToHom_app, eqToHom_refl]
[GOAL]
case h_map.w.h.h
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
P Q : Karoubi (J ⥤ C)
f✝ : P ⟶ Q
X✝ : J
X Y : J ⥤ C
f : X ⟶ Y
j : J
⊢ NatTrans.app f j =
    (𝟙 ((KaroubiFunctorCategoryEmbedding.obj (Karoubi.mk X (𝟙 X))).obj j)).f ≫
      NatTrans.app f j ≫
        (𝟙 ((Y ⋙ Functor.mk { obj := fun X => Karoubi.mk X (𝟙 X), map := fun {X Y} f => Hom.mk f }).obj j)).f
[PROOFSTEP]
erw [comp_id, id_comp]
[GOAL]
case h_obj
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
⊢ ∀ (X : J ⥤ C),
    (toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X =
      ((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X
[PROOFSTEP]
intro X
[GOAL]
case h_obj
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X✝ : J
X : J ⥤ C
⊢ (toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X =
    ((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X
[PROOFSTEP]
apply Functor.ext
[GOAL]
case h_obj.h_map
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X✝ : J
X : J ⥤ C
⊢ autoParam
    (∀ (X_1 Y : J) (f : X_1 ⟶ Y),
      ((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).map f =
        eqToHom (_ : ?F.obj X_1 = ?G.obj X_1) ≫
          (((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).map f ≫
            eqToHom
              (_ :
                (((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).obj Y =
                  ((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).obj Y))
    _auto✝
[PROOFSTEP]
intro j j' φ
[GOAL]
case h_obj.h_map
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X✝ : J
X : J ⥤ C
j j' : J
φ : j ⟶ j'
⊢ ((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).map φ =
    eqToHom (_ : ?F.obj j = ?G.obj j) ≫
      (((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).map φ ≫
        eqToHom
          (_ :
            (((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).obj j' =
              ((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).obj j')
[PROOFSTEP]
ext
[GOAL]
case h_obj.h_map.h
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X✝ : J
X : J ⥤ C
j j' : J
φ : j ⟶ j'
⊢ (((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).map φ).f =
    (eqToHom (_ : ?F.obj j = ?G.obj j) ≫
        (((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).map φ ≫
          eqToHom
            (_ :
              (((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).obj j' =
                ((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).obj j')).f
[PROOFSTEP]
dsimp
[GOAL]
case h_obj.h_map.h
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X✝ : J
X : J ⥤ C
j j' : J
φ : j ⟶ j'
⊢ 𝟙 (X.obj j) ≫ X.map φ = 𝟙 (X.obj j) ≫ X.map φ ≫ 𝟙 (X.obj j')
[PROOFSTEP]
simp
[GOAL]
case h_obj.h_obj
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X✝ : J
X : J ⥤ C
⊢ ∀ (X_1 : J),
    ((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).obj X_1 =
      (((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).obj X_1
[PROOFSTEP]
intro j
[GOAL]
case h_obj.h_obj
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X✝ : J
X : J ⥤ C
j : J
⊢ ((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).obj j =
    (((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).obj j
[PROOFSTEP]
rfl
