[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
h_X : P.X = Q.X
h_p : P.p ≫ eqToHom h_X = eqToHom h_X ≫ Q.p
⊢ P = Q
[PROOFSTEP]
cases P
[GOAL]
case mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Q : Karoubi C
X✝ : C
p✝ : X✝ ⟶ X✝
idem✝ : p✝ ≫ p✝ = p✝
h_X : (mk X✝ p✝).X = Q.X
h_p : (mk X✝ p✝).p ≫ eqToHom h_X = eqToHom h_X ≫ Q.p
⊢ mk X✝ p✝ = Q
[PROOFSTEP]
cases Q
[GOAL]
case mk.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X✝¹ : C
p✝¹ : X✝¹ ⟶ X✝¹
idem✝¹ : p✝¹ ≫ p✝¹ = p✝¹
X✝ : C
p✝ : X✝ ⟶ X✝
idem✝ : p✝ ≫ p✝ = p✝
h_X : (mk X✝¹ p✝¹).X = (mk X✝ p✝).X
h_p : (mk X✝¹ p✝¹).p ≫ eqToHom h_X = eqToHom h_X ≫ (mk X✝ p✝).p
⊢ mk X✝¹ p✝¹ = mk X✝ p✝
[PROOFSTEP]
dsimp at h_X h_p 
[GOAL]
case mk.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X✝¹ : C
p✝¹ : X✝¹ ⟶ X✝¹
idem✝¹ : p✝¹ ≫ p✝¹ = p✝¹
X✝ : C
p✝ : X✝ ⟶ X✝
idem✝ : p✝ ≫ p✝ = p✝
h_X : X✝¹ = X✝
h_p : p✝¹ ≫ eqToHom h_X = eqToHom h_X ≫ p✝
⊢ mk X✝¹ p✝¹ = mk X✝ p✝
[PROOFSTEP]
subst h_X
[GOAL]
case mk.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X✝ : C
p✝¹ : X✝ ⟶ X✝
idem✝¹ : p✝¹ ≫ p✝¹ = p✝¹
p✝ : X✝ ⟶ X✝
idem✝ : p✝ ≫ p✝ = p✝
h_p : p✝¹ ≫ eqToHom (_ : X✝ = X✝) = eqToHom (_ : X✝ = X✝) ≫ p✝
⊢ mk X✝ p✝¹ = mk X✝ p✝
[PROOFSTEP]
simpa only [mk.injEq, heq_eq_eq, true_and, eqToHom_refl, comp_id, id_comp] using h_p
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.2814, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
⊢ 0 = P.p ≫ 0 ≫ Q.p
[PROOFSTEP]
rw [zero_comp, comp_zero]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
f : Hom P Q
⊢ P.p ≫ f.f = f.f
[PROOFSTEP]
rw [f.comm, ← assoc, P.idem]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
f : Hom P Q
⊢ f.f ≫ Q.p = f.f
[PROOFSTEP]
rw [f.comm, assoc, assoc, Q.idem]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
f : Hom P Q
⊢ P.p ≫ f.f = f.f ≫ Q.p
[PROOFSTEP]
rw [p_comp, comp_p]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q R : Karoubi C
g : Hom Q R
f : Hom P Q
⊢ f.f ≫ g.f = P.p ≫ (f.f ≫ g.f) ≫ R.p
[PROOFSTEP]
rw [assoc, comp_p, ← assoc, p_comp]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.11320, u_1} C
P : Karoubi C
⊢ P.p = P.p ≫ P.p ≫ P.p
[PROOFSTEP]
repeat' rw [P.idem]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.11320, u_1} C
P : Karoubi C
⊢ P.p = P.p ≫ P.p ≫ P.p
[PROOFSTEP]
rw [P.idem]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.11320, u_1} C
P : Karoubi C
⊢ P.p = P.p ≫ P.p
[PROOFSTEP]
rw [P.idem]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f = g ↔ f.f = g.f
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f = g → f.f = g.f
[PROOFSTEP]
intro h
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
f g : P ⟶ Q
h : f = g
⊢ f.f = g.f
[PROOFSTEP]
rw [h]
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f.f = g.f → f = g
[PROOFSTEP]
apply Hom.ext
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
f g : P ⟶ Q
h : f.f = g.f
⊢ f = g
[PROOFSTEP]
simpa [hom_ext_iff] using h
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q R : Karoubi C
f : P ⟶ Q
g : Q ⟶ R
⊢ (f ≫ g).f = f.f ≫ g.f
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝ : Category.{?u.15241, u_1} C
P : Karoubi C
⊢ P.p = P.p ≫ P.p ≫ P.p
[PROOFSTEP]
repeat' rw [P.idem]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.15241, u_1} C
P : Karoubi C
⊢ P.p = P.p ≫ P.p ≫ P.p
[PROOFSTEP]
rw [P.idem]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.15241, u_1} C
P : Karoubi C
⊢ P.p = P.p ≫ P.p
[PROOFSTEP]
rw [P.idem]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P : Karoubi C
⊢ 𝟙 P = Hom.mk P.p
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝ : Category.{?u.15536, u_1} C
X : C
⊢ 𝟙 X ≫ 𝟙 X = 𝟙 X
[PROOFSTEP]
rw [comp_id]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : C
⊢ (mk X (𝟙 X)).X = X
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : C
⊢ (mk X (𝟙 X)).p = 𝟙 X
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
h : P = Q
⊢ (eqToHom h).f = P.p ≫ eqToHom (_ : P.X = Q.X)
[PROOFSTEP]
subst h
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P : Karoubi C
⊢ (eqToHom (_ : P = P)).f = P.p ≫ eqToHom (_ : P.X = P.X)
[PROOFSTEP]
simp only [eqToHom_refl, Karoubi.id_eq, comp_id]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.17980, u_1} C
X : C
⊢ 𝟙 X ≫ 𝟙 X = 𝟙 X
[PROOFSTEP]
rw [comp_id]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.17980, u_1} C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ f = ((fun X => Karoubi.mk X (𝟙 X)) X✝).p ≫ f ≫ ((fun X => Karoubi.mk X (𝟙 X)) Y✝).p
[PROOFSTEP]
simp only [comp_id, id_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.24958, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f.f + g.f = P.p ≫ (f.f + g.f) ≫ Q.p
[PROOFSTEP]
rw [add_comp, comp_add, ← f.comm, ← g.comm]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.24958, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f g h' : P ⟶ Q
⊢ f + g + h' = f + (g + h')
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{?u.24958, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f g h' : P ⟶ Q
⊢ (f + g + h').f = (f + (g + h')).f
[PROOFSTEP]
apply add_assoc
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.24958, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
⊢ 0 = P.p ≫ 0 ≫ Q.p
[PROOFSTEP]
simp only [comp_zero, zero_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.24958, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f : P ⟶ Q
⊢ 0 + f = f
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{?u.24958, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f : P ⟶ Q
⊢ (0 + f).f = f.f
[PROOFSTEP]
apply zero_add
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.24958, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f : P ⟶ Q
⊢ f + 0 = f
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{?u.24958, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f : P ⟶ Q
⊢ (f + 0).f = f.f
[PROOFSTEP]
apply add_zero
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.24958, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f : P ⟶ Q
⊢ -f.f = P.p ≫ (-f.f) ≫ Q.p
[PROOFSTEP]
simpa only [neg_comp, comp_neg, neg_inj] using f.comm
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.24958, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f : P ⟶ Q
⊢ -f + f = 0
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{?u.24958, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f : P ⟶ Q
⊢ (-f + f).f = 0.f
[PROOFSTEP]
apply add_left_neg
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.24958, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f + g = g + f
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{?u.24958, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f g : P ⟶ Q
⊢ (f + g).f = (g + f).f
[PROOFSTEP]
apply add_comm
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.35550, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
⊢ AddCommGroup (P ⟶ Q)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝ : Category.{?u.38941, u_1} C
⊢ IsIdempotentComplete (Karoubi C)
[PROOFSTEP]
refine' ⟨_⟩
[GOAL]
C : Type u_1
inst✝ : Category.{?u.38941, u_1} C
⊢ ∀ (X : Karoubi C) (p : X ⟶ X), p ≫ p = p → ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
[PROOFSTEP]
intro P p hp
[GOAL]
C : Type u_1
inst✝ : Category.{?u.38941, u_1} C
P : Karoubi C
p : P ⟶ P
hp : p ≫ p = p
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
[PROOFSTEP]
simp only [hom_ext_iff, comp_f] at hp 
[GOAL]
C : Type u_1
inst✝ : Category.{?u.38941, u_1} C
P : Karoubi C
p : P ⟶ P
hp : p.f ≫ p.f = p.f
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
[PROOFSTEP]
use⟨P.X, p.f, hp⟩
[GOAL]
case h
C : Type u_1
inst✝ : Category.{?u.38941, u_1} C
P : Karoubi C
p : P ⟶ P
hp : p.f ≫ p.f = p.f
⊢ ∃ i e, i ≫ e = 𝟙 (Karoubi.mk P.X p.f) ∧ e ≫ i = p
[PROOFSTEP]
use⟨p.f, by rw [comp_p p, hp]⟩
[GOAL]
C : Type u_1
inst✝ : Category.{?u.38941, u_1} C
P : Karoubi C
p : P ⟶ P
hp : p.f ≫ p.f = p.f
⊢ p.f = (Karoubi.mk P.X p.f).p ≫ p.f ≫ P.p
[PROOFSTEP]
rw [comp_p p, hp]
[GOAL]
case h
C : Type u_1
inst✝ : Category.{?u.38941, u_1} C
P : Karoubi C
p : P ⟶ P
hp : p.f ≫ p.f = p.f
⊢ ∃ e, Hom.mk p.f ≫ e = 𝟙 (Karoubi.mk P.X p.f) ∧ e ≫ Hom.mk p.f = p
[PROOFSTEP]
use⟨p.f, by rw [hp, p_comp p]⟩
[GOAL]
C : Type u_1
inst✝ : Category.{?u.38941, u_1} C
P : Karoubi C
p : P ⟶ P
hp : p.f ≫ p.f = p.f
⊢ p.f = P.p ≫ p.f ≫ (Karoubi.mk P.X p.f).p
[PROOFSTEP]
rw [hp, p_comp p]
[GOAL]
case h
C : Type u_1
inst✝ : Category.{?u.38941, u_1} C
P : Karoubi C
p : P ⟶ P
hp : p.f ≫ p.f = p.f
⊢ Hom.mk p.f ≫ Hom.mk p.f = 𝟙 (Karoubi.mk P.X p.f) ∧ Hom.mk p.f ≫ Hom.mk p.f = p
[PROOFSTEP]
simp [hp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.40282, u_1} C
inst✝ : IsIdempotentComplete C
P : Karoubi C
⊢ P ∈ Functor.essImage (toKaroubi C)
[PROOFSTEP]
rcases IsIdempotentComplete.idempotents_split P.X P.p P.idem with ⟨Y, i, e, ⟨h₁, h₂⟩⟩
[GOAL]
case intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{?u.40282, u_1} C
inst✝ : IsIdempotentComplete C
P : Karoubi C
Y : C
i : Y ⟶ P.X
e : P.X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = P.p
⊢ P ∈ Functor.essImage (toKaroubi C)
[PROOFSTEP]
use Y
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{?u.40282, u_1} C
inst✝ : IsIdempotentComplete C
P : Karoubi C
Y : C
i : Y ⟶ P.X
e : P.X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = P.p
⊢ Nonempty ((toKaroubi C).obj Y ≅ P)
[PROOFSTEP]
exact
  Nonempty.intro
    { hom := ⟨i, by erw [id_comp, ← h₂, ← assoc, h₁, id_comp]⟩
      inv := ⟨e, by erw [comp_id, ← h₂, assoc, h₁, comp_id]⟩ }
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.40282, u_1} C
inst✝ : IsIdempotentComplete C
P : Karoubi C
Y : C
i : Y ⟶ P.X
e : P.X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = P.p
⊢ i = ((toKaroubi C).obj Y).p ≫ i ≫ P.p
[PROOFSTEP]
erw [id_comp, ← h₂, ← assoc, h₁, id_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.40282, u_1} C
inst✝ : IsIdempotentComplete C
P : Karoubi C
Y : C
i : Y ⟶ P.X
e : P.X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = P.p
⊢ e = P.p ≫ e ≫ ((toKaroubi C).obj Y).p
[PROOFSTEP]
erw [comp_id, ← h₂, assoc, h₁, comp_id]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.45540, u_1} C
P : Karoubi C
⊢ P.p = P.p ≫ P.p ≫ (mk P.X (𝟙 P.X)).p
[PROOFSTEP]
erw [coe_p, comp_id, P.idem]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.47113, u_1} C
P : Karoubi C
⊢ P.p = (mk P.X (𝟙 P.X)).p ≫ P.p ≫ P.p
[PROOFSTEP]
erw [coe_p, id_comp, P.idem]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P : Karoubi C
⊢ 𝟙 P = decompId_i P ≫ decompId_p P
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P : Karoubi C
⊢ (𝟙 P).f = (decompId_i P ≫ decompId_p P).f
[PROOFSTEP]
simp only [comp_f, id_eq, P.idem, decompId_i, decompId_p]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P : Karoubi C
⊢ (toKaroubi C).map P.p = decompId_p P ≫ decompId_i P
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P : Karoubi C
⊢ ((toKaroubi C).map P.p).f = (decompId_p P ≫ decompId_i P).f
[PROOFSTEP]
simp only [comp_f, decompId_p_f, decompId_i_f, P.idem, toKaroubi_map_f]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : C
⊢ decompId_i ((toKaroubi C).obj X) = 𝟙 ((toKaroubi C).obj X)
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : C
⊢ decompId_p ((toKaroubi C).obj X) = 𝟙 (mk ((toKaroubi C).obj X).X (𝟙 ((toKaroubi C).obj X).X))
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝ : Category.{?u.50209, u_1} C
P Q : Karoubi C
f : P ⟶ Q
⊢ mk P.X (𝟙 P.X) ⟶ mk Q.X (𝟙 Q.X)
[PROOFSTEP]
exact Hom.mk f.f (by simp)
[GOAL]
C : Type u_1
inst✝ : Category.{?u.50209, u_1} C
P Q : Karoubi C
f : P ⟶ Q
⊢ f.f = (mk P.X (𝟙 P.X)).p ≫ f.f ≫ (mk Q.X (𝟙 Q.X)).p
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
f : P ⟶ Q
⊢ f ≫ decompId_i Q = decompId_i P ≫ Hom.mk f.f
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝ : Category.{?u.51254, u_1} C
P Q : Karoubi C
f : P ⟶ Q
⊢ mk P.X (𝟙 P.X) ⟶ mk Q.X (𝟙 Q.X)
[PROOFSTEP]
exact Hom.mk f.f (by simp)
[GOAL]
C : Type u_1
inst✝ : Category.{?u.51254, u_1} C
P Q : Karoubi C
f : P ⟶ Q
⊢ f.f = (mk P.X (𝟙 P.X)).p ≫ f.f ≫ (mk Q.X (𝟙 Q.X)).p
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
f : P ⟶ Q
⊢ decompId_p P ≫ f = Hom.mk f.f ≫ decompId_p Q
[PROOFSTEP]
aesop_cat
