C : Type u_1
inst✝² : Category 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
C : Type u_1
inst✝² : Category C
inst✝¹ : Preadditive C
inst✝ : HasFiniteBiproducts C
n : ℕ
F : Fin n → Karoubi C
⊢ HasBiproduct F
apply hasBiproduct_of_total (Biproducts.bicone F)
C : Type u_1
inst✝² : Category 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
C : Type u_1
inst✝² : Category 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
simp only [hom_ext_iff]
C : Type u_1
inst✝² : Category 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
C : Type u_1
inst✝² : Category 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
refine' biproduct.hom_ext' _ _ (fun j => _)
C : Type u_1
inst✝² : Category 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
C : Type u_1
inst✝² : Category 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
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]
C : Type u_1
inst✝² : Category 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

case h₀
C : Type u_1
inst✝² : Category 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

case h₁
C : Type u_1
inst✝² : Category 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
C : Type u_1
inst✝² : Category 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
rw [Finset.sum_eq_single j]
case h₀
C : Type u_1
inst✝² : Category 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

case h₁
C : Type u_1
inst✝² : Category 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
C : Type u_1
inst✝² : Category 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

case h₀
C : Type u_1
inst✝² : Category 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

case h₁
C : Type u_1
inst✝² : Category 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
. simp only [bicone_ι_π_self_assoc]
case h₁
C : Type u_1
inst✝² : Category 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
case h₀
C : Type u_1
inst✝² : Category 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

case h₁
C : Type u_1
inst✝² : Category 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
. intro b _ hb
  simp only [biproduct.ι_π_ne_assoc _ hb.symm, zero_comp]
no goals
case h₁
C : Type u_1
inst✝² : Category 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
. intro hj
  simp only [Finset.mem_univ, not_true] at hj
no goals
C : Type u_1
inst✝² : Category 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
simp only [bicone_ι_π_self_assoc]
case h₀
C : Type u_1
inst✝² : Category 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
case h₀
C : Type u_1
inst✝² : Category 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
intro b _ hb
no goals
case h₀
C : Type u_1
inst✝² : Category 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
simp only [biproduct.ι_π_ne_assoc _ hb.symm, zero_comp]
case h₁
C : Type u_1
inst✝² : Category 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
case h₁
C : Type u_1
inst✝² : Category 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
intro hj
no goals
case h₁
C : Type u_1
inst✝² : Category 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
simp only [Finset.mem_univ, not_true] at hj