[GOAL]
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
F : J → Karoubi C
⊢ ((biproduct.map fun j => (F j).p) ≫ biproduct.map fun j => (F j).p) = biproduct.map fun j => (F j).p
[PROOFSTEP]
ext
[GOAL]
case w.w
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
F : J → Karoubi C
j✝¹ j✝ : J
⊢ biproduct.ι (fun j => (F j).X) j✝ ≫
      ((biproduct.map fun j => (F j).p) ≫ biproduct.map fun j => (F j).p) ≫ biproduct.π (fun j => (F j).X) j✝¹ =
    biproduct.ι (fun j => (F j).X) j✝ ≫ (biproduct.map fun j => (F j).p) ≫ biproduct.π (fun j => (F j).X) j✝¹
[PROOFSTEP]
simp only [assoc, biproduct.map_π, biproduct.map_π_assoc, idem]
[GOAL]
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
F : J → Karoubi C
j : J
⊢ (biproduct.map fun j => (F j).p) ≫ Bicone.π (biproduct.bicone fun j => (F j).X) j =
    (mk (⨁ fun j => (F j).X) (biproduct.map fun j => (F j).p)).p ≫
      ((biproduct.map fun j => (F j).p) ≫ Bicone.π (biproduct.bicone fun j => (F j).X) j) ≫ (F j).p
[PROOFSTEP]
simp only [assoc, biproduct.bicone_π, biproduct.map_π, biproduct.map_π_assoc, (F j).idem]
[GOAL]
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
F : J → Karoubi C
j : J
⊢ (biproduct.ι (fun j => (F j).X) j ≫ biproduct.map fun j => (F j).p) =
    (F j).p ≫
      (biproduct.ι (fun j => (F j).X) j ≫ biproduct.map fun j => (F j).p) ≫
        (mk (⨁ fun j => (F j).X) (biproduct.map fun j => (F j).p)).p
[PROOFSTEP]
simp only [biproduct.ι_map, assoc, idem_assoc]
[GOAL]
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
F : J → Karoubi C
j j' : J
⊢ (fun j => Hom.mk (biproduct.ι (fun j => (F j).X) j ≫ biproduct.map fun j => (F j).p)) j ≫
      (fun j => Hom.mk ((biproduct.map fun j => (F j).p) ≫ Bicone.π (biproduct.bicone fun j => (F j).X) j)) j' =
    if h : j = j' then eqToHom (_ : F j = F j') else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
F : J → Karoubi C
j j' : J
h : j = j'
⊢ (fun j => Hom.mk (biproduct.ι (fun j => (F j).X) j ≫ biproduct.map fun j => (F j).p)) j ≫
      (fun j => Hom.mk ((biproduct.map fun j => (F j).p) ≫ Bicone.π (biproduct.bicone fun j => (F j).X) j)) j' =
    eqToHom (_ : F j = F j')
[PROOFSTEP]
subst h
[GOAL]
case pos
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
F : J → Karoubi C
j : J
⊢ (fun j => Hom.mk (biproduct.ι (fun j => (F j).X) j ≫ biproduct.map fun j => (F j).p)) j ≫
      (fun j => Hom.mk ((biproduct.map fun j => (F j).p) ≫ Bicone.π (biproduct.bicone fun j => (F j).X) j)) j =
    eqToHom (_ : F j = F j)
[PROOFSTEP]
simp only [biproduct.ι_map, biproduct.bicone_π, biproduct.map_π, eqToHom_refl, id_eq, hom_ext_iff, comp_f, assoc,
  bicone_ι_π_self_assoc, idem]
[GOAL]
case neg
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
F : J → Karoubi C
j j' : J
h : ¬j = j'
⊢ (fun j => Hom.mk (biproduct.ι (fun j => (F j).X) j ≫ biproduct.map fun j => (F j).p)) j ≫
      (fun j => Hom.mk ((biproduct.map fun j => (F j).p) ≫ Bicone.π (biproduct.bicone fun j => (F j).X) j)) j' =
    0
[PROOFSTEP]
dsimp
[GOAL]
case neg
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
F : J → Karoubi C
j j' : J
h : ¬j = j'
⊢ Hom.mk (biproduct.ι (fun j => (F j).X) j ≫ biproduct.map fun j => (F j).p) ≫
      Hom.mk ((biproduct.map fun j => (F j).p) ≫ biproduct.π (fun j => (F j).X) j') =
    Hom.mk 0
[PROOFSTEP]
simp only [hom_ext_iff, biproduct.ι_map, biproduct.map_π, comp_f, assoc, ne_eq, biproduct.ι_π_ne_assoc _ h, comp_zero,
  zero_comp]
[GOAL]
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteBiproducts C
n : ℕ
F : Fin n → Karoubi C
⊢ HasBiproduct F
[PROOFSTEP]
apply hasBiproduct_of_total (Biproducts.bicone F)
[GOAL]
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteBiproducts C
n : ℕ
F : Fin n → Karoubi C
⊢ (Finset.sum Finset.univ fun j => Bicone.π (Biproducts.bicone F) j ≫ Bicone.ι (Biproducts.bicone F) j) =
    𝟙 (Biproducts.bicone F).pt
[PROOFSTEP]
simp only [hom_ext_iff]
[GOAL]
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteBiproducts C
n : ℕ
F : Fin n → Karoubi C
⊢ (Finset.sum Finset.univ fun j => Bicone.π (Biproducts.bicone F) j ≫ Bicone.ι (Biproducts.bicone F) j).f =
    (𝟙 (Biproducts.bicone F).pt).f
[PROOFSTEP]
refine' biproduct.hom_ext' _ _ (fun j => _)
[GOAL]
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteBiproducts C
n : ℕ
F : Fin n → Karoubi C
j : Fin n
⊢ biproduct.ι (fun j => (F j).X) j ≫
      (Finset.sum Finset.univ fun j => Bicone.π (Biproducts.bicone F) j ≫ Bicone.ι (Biproducts.bicone F) j).f =
    biproduct.ι (fun j => (F j).X) j ≫ (𝟙 (Biproducts.bicone F).pt).f
[PROOFSTEP]
simp only [Biproducts.bicone_pt_X, sum_hom, comp_f, Biproducts.bicone_π_f, biproduct.bicone_π, biproduct.map_π,
  Biproducts.bicone_ι_f, biproduct.ι_map, assoc, idem_assoc, id_eq, Biproducts.bicone_pt_p, comp_sum]
[GOAL]
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteBiproducts C
n : ℕ
F : Fin n → Karoubi C
j : Fin n
⊢ (Finset.sum Finset.univ fun j_1 =>
      biproduct.ι (fun j => (F j).X) j ≫
        biproduct.π (fun b => (F b).X) j_1 ≫ (F j_1).p ≫ biproduct.ι (fun j => (F j).X) j_1) =
    (F j).p ≫ biproduct.ι (fun j => (F j).X) j
[PROOFSTEP]
rw [Finset.sum_eq_single j]
[GOAL]
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteBiproducts C
n : ℕ
F : Fin n → Karoubi C
j : Fin n
⊢ biproduct.ι (fun j => (F j).X) j ≫ biproduct.π (fun b => (F b).X) j ≫ (F j).p ≫ biproduct.ι (fun j => (F j).X) j =
    (F j).p ≫ biproduct.ι (fun j => (F j).X) j
[PROOFSTEP]
simp only [bicone_ι_π_self_assoc]
[GOAL]
case h₀
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteBiproducts C
n : ℕ
F : Fin n → Karoubi C
j : Fin n
⊢ ∀ (b : Fin n),
    b ∈ Finset.univ →
      b ≠ j →
        biproduct.ι (fun j => (F j).X) j ≫
            biproduct.π (fun b => (F b).X) b ≫ (F b).p ≫ biproduct.ι (fun j => (F j).X) b =
          0
[PROOFSTEP]
intro b _ hb
[GOAL]
case h₀
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteBiproducts C
n : ℕ
F : Fin n → Karoubi C
j b : Fin n
a✝ : b ∈ Finset.univ
hb : b ≠ j
⊢ biproduct.ι (fun j => (F j).X) j ≫ biproduct.π (fun b => (F b).X) b ≫ (F b).p ≫ biproduct.ι (fun j => (F j).X) b = 0
[PROOFSTEP]
simp only [biproduct.ι_π_ne_assoc _ hb.symm, zero_comp]
[GOAL]
case h₁
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteBiproducts C
n : ℕ
F : Fin n → Karoubi C
j : Fin n
⊢ ¬j ∈ Finset.univ →
    biproduct.ι (fun j => (F j).X) j ≫ biproduct.π (fun b => (F b).X) j ≫ (F j).p ≫ biproduct.ι (fun j => (F j).X) j = 0
[PROOFSTEP]
intro hj
[GOAL]
case h₁
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteBiproducts C
n : ℕ
F : Fin n → Karoubi C
j : Fin n
hj : ¬j ∈ Finset.univ
⊢ biproduct.ι (fun j => (F j).X) j ≫ biproduct.π (fun b => (F b).X) j ≫ (F j).p ≫ biproduct.ι (fun j => (F j).X) j = 0
[PROOFSTEP]
simp only [Finset.mem_univ, not_true] at hj 
[GOAL]
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ decompId_i P ≫ decompId_p (complement P) = 0
[PROOFSTEP]
simp only [instAddCommGroupHom_zero, hom_ext_iff, complement_X, comp_f, decompId_i_f, decompId_p_f, complement_p,
  comp_sub, comp_id, idem, sub_self]
[GOAL]
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ decompId_i (complement P) ≫ decompId_p P = 0
[PROOFSTEP]
simp only [instAddCommGroupHom_zero, hom_ext_iff, complement_X, comp_f, decompId_i_f, complement_p, decompId_p_f,
  sub_comp, id_comp, idem, sub_self]
[GOAL]
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ (BinaryBicone.mk (mk P.X (𝟙 P.X)) (decompId_p P) (decompId_p (complement P)) (decompId_i P)
            (decompId_i (complement P))).fst ≫
        (BinaryBicone.mk (mk P.X (𝟙 P.X)) (decompId_p P) (decompId_p (complement P)) (decompId_i P)
            (decompId_i (complement P))).inl +
      (BinaryBicone.mk (mk P.X (𝟙 P.X)) (decompId_p P) (decompId_p (complement P)) (decompId_i P)
            (decompId_i (complement P))).snd ≫
        (BinaryBicone.mk (mk P.X (𝟙 P.X)) (decompId_p P) (decompId_p (complement P)) (decompId_i P)
            (decompId_i (complement P))).inr =
    𝟙
      (BinaryBicone.mk (mk P.X (𝟙 P.X)) (decompId_p P) (decompId_p (complement P)) (decompId_i P)
          (decompId_i (complement P))).pt
[PROOFSTEP]
simp only [id_eq, complement_X, comp_f, decompId_i_f, decompId_p_f, complement_p, instAddCommGroupHom_add, idem,
  comp_sub, comp_id, sub_comp, id_comp, sub_self, sub_zero, add_sub_cancel'_right]
[GOAL]
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ biprod.desc (decompId_i P) (decompId_i (complement P)) ≫ biprod.lift (decompId_p P) (decompId_p (complement P)) =
    𝟙 (P ⊞ complement P)
[PROOFSTEP]
apply biprod.hom_ext'
[GOAL]
case h₀
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ biprod.inl ≫
      biprod.desc (decompId_i P) (decompId_i (complement P)) ≫ biprod.lift (decompId_p P) (decompId_p (complement P)) =
    biprod.inl ≫ 𝟙 (P ⊞ complement P)
[PROOFSTEP]
rw [biprod.inl_desc_assoc, comp_id, biprod.lift_eq, comp_add, ← decompId_assoc, add_right_eq_self, ← assoc]
[GOAL]
case h₀
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ (decompId_i P ≫ decompId_p (complement P)) ≫ biprod.inr = 0
[PROOFSTEP]
refine' (_ =≫ _).trans zero_comp
[GOAL]
case h₀
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ decompId_i P ≫ decompId_p (complement P) = 0
[PROOFSTEP]
ext
[GOAL]
case h₀.h
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ (decompId_i P ≫ decompId_p (complement P)).f = 0.f
[PROOFSTEP]
simp only [comp_f, toKaroubi_obj_X, decompId_i_f, decompId_p_f, complement_p, comp_sub, comp_id, idem, sub_self,
  instAddCommGroupHom_zero]
[GOAL]
case h₁
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ biprod.inr ≫
      biprod.desc (decompId_i P) (decompId_i (complement P)) ≫ biprod.lift (decompId_p P) (decompId_p (complement P)) =
    biprod.inr ≫ 𝟙 (P ⊞ complement P)
[PROOFSTEP]
rw [biprod.inr_desc_assoc, comp_id, biprod.lift_eq, comp_add, ← decompId_assoc, add_left_eq_self, ← assoc]
[GOAL]
case h₁
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ (decompId_i (complement P) ≫ decompId_p P) ≫ biprod.inl = 0
[PROOFSTEP]
refine' (_ =≫ _).trans zero_comp
[GOAL]
case h₁
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ decompId_i (complement P) ≫ decompId_p P = 0
[PROOFSTEP]
ext
[GOAL]
case h₁.h
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ (decompId_i (complement P) ≫ decompId_p P).f = 0.f
[PROOFSTEP]
simp only [complement_X, comp_f, decompId_i_f, complement_p, decompId_p_f, sub_comp, id_comp, idem, sub_self,
  instAddCommGroupHom_zero]
[GOAL]
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ biprod.lift (decompId_p P) (decompId_p (complement P)) ≫ biprod.desc (decompId_i P) (decompId_i (complement P)) =
    𝟙 ((toKaroubi C).obj P.X)
[PROOFSTEP]
simp only [biprod.lift_desc, instAddCommGroupHom_add, toKaroubi_obj_X, 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'_right, id_eq,
  toKaroubi_obj_p]
