-- Mathlib/CategoryTheory/Idempotents/Biproducts.lean
theorem karoubi_hasFiniteBiproducts [HasFiniteBiproducts C] : HasFiniteBiproducts (Karoubi C) :=
  { out := fun n =>
      { has_biproduct := fun F => by
          apply hasBiproduct_of_total (Biproducts.bicone F)
          simp only [hom_ext_iff]
          refine biproduct.hom_ext' _ _ (fun j => ?_)
          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_f, Biproducts.bicone_pt_p, comp_sum]
          rw [Finset.sum_eq_single j]
          · simp only [bicone_ι_π_self_assoc]
          · intro b _ hb
            simp only [biproduct.ι_π_ne_assoc _ hb.symm, zero_comp]
          · intro hj
            simp only [Finset.mem_univ, not_true] at hj } }

Proof state:
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, (Biproducts.bicone F).π j ≫ (Biproducts.bicone F).ι j = 𝟙 (Biproducts.bicone F).pt

Tactic:
simp only [hom_ext_iff]

Result:
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, (Biproducts.bicone F).π j ≫ (Biproducts.bicone F).ι j).f = (𝟙 (Biproducts.bicone F).pt).f

Proof state:
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 ∈ Finset.univ,
    b ≠ j →
      biproduct.ι (fun j => (F j).X) j ≫ biproduct.π (fun j => (F j).X) b ≫ (F b).p ≫ biproduct.ι (fun j => (F j).X) b =
        0

Tactic:
intro b _ hb

Result:
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 j => (F j).X) b ≫ (F b).p ≫ biproduct.ι (fun j => (F j).X) b = 0

Proof state:
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_1 : Fin n,
      biproduct.ι (fun j => (F j).X) j ≫
        biproduct.π (fun j => (F j).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

Tactic:
rw [Finset.sum_eq_single j]

Result:
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 j => (F j).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.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteBiproducts C
n : ℕ
F : Fin n → Karoubi C
j : Fin n
⊢ ∀ b ∈ Finset.univ,
    b ≠ j →
      biproduct.ι (fun j => (F j).X) j ≫ biproduct.π (fun j => (F j).X) b ≫ (F b).p ≫ biproduct.ι (fun j => (F j).X) b =
        0

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 j => (F j).X) j ≫ (F j).p ≫ biproduct.ι (fun j => (F j).X) j = 0

Proof state:
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 j => (F j).X) j ≫ (F j).p ≫ biproduct.ι (fun j => (F j).X) j = 0

Tactic:
simp only [Finset.mem_univ, not_true] at hj

Result:
no goals

Proof state:
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, (Biproducts.bicone F).π j ≫ (Biproducts.bicone F).ι j).f = (𝟙 (Biproducts.bicone F).pt).f

Tactic:
refine biproduct.hom_ext' _ _ (fun j => ?_)

Result:
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 ≫ (∑ j : Fin n, (Biproducts.bicone F).π j ≫ (Biproducts.bicone F).ι j).f =
    biproduct.ι (fun j => (F j).X) j ≫ (𝟙 (Biproducts.bicone F).pt).f

Proof state:
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteBiproducts C
n : ℕ
F : Fin n → Karoubi C
⊢ HasBiproduct F

Tactic:
apply hasBiproduct_of_total (Biproducts.bicone F)

Result:
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, (Biproducts.bicone F).π j ≫ (Biproducts.bicone F).ι j = 𝟙 (Biproducts.bicone F).pt

Proof state:
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 j => (F j).X) j ≫ (F j).p ≫ biproduct.ι (fun j => (F j).X) j =
    (F j).p ≫ biproduct.ι (fun j => (F j).X) j

Tactic:
simp only [bicone_ι_π_self_assoc]

Result:
no goals

Proof state:
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 j => (F j).X) b ≫ (F b).p ≫ biproduct.ι (fun j => (F j).X) b = 0

Tactic:
simp only [biproduct.ι_π_ne_assoc _ hb.symm, zero_comp]

Result:
no goals

Proof state:
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 ≫ (∑ j : Fin n, (Biproducts.bicone F).π j ≫ (Biproducts.bicone F).ι j).f =
    biproduct.ι (fun j => (F j).X) j ≫ (𝟙 (Biproducts.bicone F).pt).f

Tactic:
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_f, Biproducts.bicone_pt_p, comp_sum]

Result:
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_1 : Fin n,
      biproduct.ι (fun j => (F j).X) j ≫
        biproduct.π (fun j => (F j).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

Proof state:
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 j => (F j).X) j ≫ (F j).p ≫ biproduct.ι (fun j => (F j).X) j = 0

Tactic:
intro hj

Result:
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 j => (F j).X) j ≫ (F j).p ≫ biproduct.ι (fun j => (F j).X) j = 0