awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 rwa rwa₁ rwa₂ rwa₃ : IsIdempotentComplete.{v_1, u_1} C
⊢ IsIdempotentComplete.{v_1, u_1} Cᵒᵖ

Tactic:
rwa [isIdempotentComplete_iff_opposite]

Premises used: CategoryTheory.Idempotents.isIdempotentComplete_iff_opposite
-- Module: Mathlib.CategoryTheory.Idempotents.Biproducts
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasFiniteBiproducts.{v, u_1} C
J : Type
inst_3 : Finite J
F : J → Karoubi.{v, u_1} C
w :
  ∀ (j j_1 : J),
    Eq.{v + 1} (α := (F j_1).X ⟶ (F j).X)
      (CategoryStruct.comp (Y := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
          (biproduct.ι.{0, v, u_1} (C := C) (fun (j : J) ↦ (F j).X) j_1)
          (CategoryStruct.comp (Y := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
            (CategoryStruct.comp (Y := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
              (biproduct.map fun (j : J) ↦ (F j).p) (biproduct.map fun (j : J) ↦ (F j).p))
            (biproduct.π (fun (j : J) ↦ (F j).X) j)) :
        (F j_1).X ⟶ (F j).X)
      (CategoryStruct.comp (Y := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
          (biproduct.ι.{0, v, u_1} (C := C) (fun (j : J) ↦ (F j).X) j_1)
          (CategoryStruct.comp (Y := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X) (biproduct.map fun (j : J) ↦ (F j).p)
            (biproduct.π (fun (j : J) ↦ (F j).X) j)) :
        (F j_1).X ⟶ (F j).X)
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u_1} (V := C) (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
      (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X))
    (CategoryStruct.comp (Y := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X) (biproduct.map fun (j : J) ↦ (F j).p)
      (biproduct.map fun (j : J) ↦ (F j).p))
    (biproduct.map fun (j : J) ↦ (F j).p)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Idempotents.Biproducts
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasFiniteBiproducts.{v, u_1} C
J : Type
inst_3 : Finite J
F : J → Karoubi.{v, u_1} C
j j_1 : J
⊢ Eq.{v + 1} (α := (F j_1).X ⟶ (F j).X)
    (CategoryStruct.comp (Y := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
        (biproduct.ι.{0, v, u_1} (C := C) (fun (j : J) ↦ (F j).X) j_1)
        (CategoryStruct.comp (Y := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
          (CategoryStruct.comp (Y := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X) (biproduct.map fun (j : J) ↦ (F j).p)
            (biproduct.map fun (j : J) ↦ (F j).p))
          (biproduct.π (fun (j : J) ↦ (F j).X) j)) :
      (F j_1).X ⟶ (F j).X)
    (CategoryStruct.comp (Y := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
        (biproduct.ι.{0, v, u_1} (C := C) (fun (j : J) ↦ (F j).X) j_1)
        (CategoryStruct.comp (Y := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X) (biproduct.map fun (j : J) ↦ (F j).p)
          (biproduct.π (fun (j : J) ↦ (F j).X) j)) :
      (F j_1).X ⟶ (F j).X)

Tactic:
simp only [assoc, biproduct.map_π, biproduct.map_π_assoc, idem]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biproduct.map_π_assoc, CategoryTheory.Limits.biproduct.map_π, CategoryTheory.Idempotents.Karoubi.idem
-- Module: Mathlib.CategoryTheory.Idempotents.Biproducts
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasFiniteBiproducts.{v, u_1} C
J : Type
inst_3 : Finite J
F : J → Karoubi.{v, u_1} C
j : J
⊢ Eq (α :=
    { X := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X,
          p :=
            (biproduct.map fun (j : J) ↦ (F j).p :
              Quiver.Hom.{v, u_1} (V := C) (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
                (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)),
          idem := ⋯ : Karoubi.{v, u_1} C }.X ⟶
      (F j).X)
    ({ X := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X,
            p :=
              (biproduct.map fun (j : J) ↦ (F j).p :
                Quiver.Hom.{v, u_1} (V := C) (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
                  (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)),
            idem := ⋯ : Karoubi.{v, u_1} C }.p ≫
        CategoryStruct.comp (Y := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X) (biproduct.map fun (j : J) ↦ (F j).p)
            (Bicone.π (biproduct.bicone fun (j : J) ↦ (F j).X) j) ≫
          (F j).p :
      { X := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X,
            p :=
              (biproduct.map fun (j : J) ↦ (F j).p :
                Quiver.Hom.{v, u_1} (V := C) (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
                  (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)),
            idem := ⋯ : Karoubi.{v, u_1} C }.X ⟶
        (F j).X)
    (CategoryStruct.comp (Y := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X) (biproduct.map fun (j : J) ↦ (F j).p)
        (Bicone.π (biproduct.bicone fun (j : J) ↦ (F j).X) j) :
      { X := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X,
            p :=
              (biproduct.map fun (j : J) ↦ (F j).p :
                Quiver.Hom.{v, u_1} (V := C) (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
                  (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)),
            idem := ⋯ : Karoubi.{v, u_1} C }.X ⟶
        (F j).X)

Tactic:
simp only [assoc, biproduct.bicone_π, biproduct.map_π, biproduct.map_π_assoc, (F j).idem]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biproduct.map_π_assoc, CategoryTheory.Limits.biproduct.map_π, CategoryTheory.Idempotents.Karoubi.idem, CategoryTheory.Limits.biproduct.bicone_π
-- Module: Mathlib.CategoryTheory.Idempotents.Biproducts
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasFiniteBiproducts.{v, u_1} C
J : Type
inst_3 : Finite J
F : J → Karoubi.{v, u_1} C
j : J
⊢ Eq (α :=
    (F j).X ⟶
      { X := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X,
          p :=
            (biproduct.map fun (j : J) ↦ (F j).p :
              Quiver.Hom.{v, u_1} (V := C) (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
                (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)),
          idem := ⋯ : Karoubi.{v, u_1} C }.X)
    ((F j).p ≫
      CategoryStruct.comp (Y := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
          (biproduct.ι.{0, v, u_1} (C := C) (fun (j : J) ↦ (F j).X) j) (biproduct.map fun (j : J) ↦ (F j).p) ≫
        { X := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X,
            p :=
              (biproduct.map fun (j : J) ↦ (F j).p :
                Quiver.Hom.{v, u_1} (V := C) (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
                  (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)),
            idem := ⋯ : Karoubi.{v, u_1} C }.p)
    (CategoryStruct.comp (Y := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
      (biproduct.ι.{0, v, u_1} (C := C) (fun (j : J) ↦ (F j).X) j) (biproduct.map fun (j : J) ↦ (F j).p))

Tactic:
simp only [biproduct.ι_map, assoc, idem_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Idempotents.Karoubi.idem_assoc, CategoryTheory.Limits.biproduct.ι_map
-- Module: Mathlib.CategoryTheory.Idempotents.Biproducts
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasFiniteBiproducts.{v, u_1} C
J : Type
inst_3 : Finite J
F : J → Karoubi.{v, u_1} C
j : J
⊢ CategoryStruct.comp (Y :=
      { X := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X,
        p :=
          (biproduct.map fun (j : J) ↦ (F j).p :
            Quiver.Hom.{v, u_1} (V := C) (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
              (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)),
        idem := ⋯ })
      ({
          f :=
            CategoryStruct.comp (Y := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
              (biproduct.ι.{0, v, u_1} (C := C) (fun (j : J) ↦ (F j).X) j) (biproduct.map fun (j : J) ↦ (F j).p),
          comm := ⋯ } :
        (F j).Hom
          { X := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X,
            p :=
              (biproduct.map fun (j : J) ↦ (F j).p :
                Quiver.Hom.{v, u_1} (V := C) (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
                  (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)),
            idem := ⋯ })
      ({
          f :=
            CategoryStruct.comp (Y := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X) (biproduct.map fun (j : J) ↦ (F j).p)
              (Bicone.π (biproduct.bicone fun (j : J) ↦ (F j).X) j),
          comm := ⋯ } :
        { X := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X,
              p :=
                (biproduct.map fun (j : J) ↦ (F j).p :
                  Quiver.Hom.{v, u_1} (V := C) (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
                    (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)),
              idem := ⋯ : Karoubi.{v, u_1} C }.Hom
          (F j)) =
    eqToHom ⋯

Tactic:
simp only [biproduct.ι_map, biproduct.bicone_π, biproduct.map_π, eqToHom_refl,
        id_f, hom_ext_iff, comp_f, assoc, bicone_ι_π_self_assoc, idem]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.bicone_ι_π_self_assoc, CategoryTheory.Limits.biproduct.map_π, CategoryTheory.Idempotents.Karoubi.id_f, CategoryTheory.Idempotents.Karoubi.comp_f, CategoryTheory.eqToHom_refl, CategoryTheory.Idempotents.Karoubi.idem, CategoryTheory.Limits.biproduct.bicone_π, CategoryTheory.Limits.biproduct.ι_map, CategoryTheory.Idempotents.Karoubi.hom_ext_iff
-- Module: Mathlib.CategoryTheory.Idempotents.Biproducts
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasFiniteBiproducts.{v, u_1} C
J : Type
inst_3 : Finite J
F : J → Karoubi.{v, u_1} C
j j' : J
h : ¬j = j'
⊢ Eq.{v + 1} (α := F j ⟶ F j')
    (CategoryStruct.comp (Y :=
      { X := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X,
        p :=
          (biproduct.map fun (j : J) ↦ (F j).p :
            Quiver.Hom.{v, u_1} (V := C) (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
              (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)),
        idem := ⋯ })
      ({
          f :=
            CategoryStruct.comp (Y := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
              (biproduct.ι.{0, v, u_1} (C := C) (fun (j : J) ↦ (F j).X) j) (biproduct.map fun (j : J) ↦ (F j).p),
          comm := ⋯ } :
        (F j).Hom
          { X := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X,
            p :=
              (biproduct.map fun (j : J) ↦ (F j).p :
                Quiver.Hom.{v, u_1} (V := C) (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
                  (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)),
            idem := ⋯ })
      ({
          f :=
            CategoryStruct.comp (Y := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X) (biproduct.map fun (j : J) ↦ (F j).p)
              (biproduct.π (fun (j : J) ↦ (F j).X) j'),
          comm := ⋯ } :
        { X := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X,
              p :=
                (biproduct.map fun (j : J) ↦ (F j).p :
                  Quiver.Hom.{v, u_1} (V := C) (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
                    (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)),
              idem := ⋯ : Karoubi.{v, u_1} C }.Hom
          (F j')))
    { f := 0, comm := ⋯ }

Tactic:
simp only [biproduct.ι_map, biproduct.map_π, hom_ext_iff, comp_f,
        assoc, biproduct.ι_π_ne_assoc _ h, zero_comp, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biproduct.map_π, CategoryTheory.Limits.comp_zero, CategoryTheory.Idempotents.Karoubi.comp_f, CategoryTheory.Limits.zero_comp, CategoryTheory.Limits.biproduct.ι_π_ne_assoc, CategoryTheory.Limits.biproduct.ι_map, CategoryTheory.Idempotents.Karoubi.hom_ext_iff
-- Module: Mathlib.CategoryTheory.Idempotents.Biproducts
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasFiniteBiproducts.{v, u_1} C
n : ℕ
F : Fin n → Karoubi.{v, u_1} C
apply :
  Eq.{v + 1} (α := Bicone.pt (Biproducts.bicone F) ⟶ Bicone.pt (Biproducts.bicone F))
    (∑ j : Fin n, Bicone.π (Biproducts.bicone F) j ≫ Bicone.ι (Biproducts.bicone F) j)
    (𝟙 (Bicone.pt (Biproducts.bicone F)))
⊢ HasBiproduct F

Tactic:
apply hasBiproduct_of_total (Biproducts.bicone F)

Premises used: CategoryTheory.Limits.hasBiproduct_of_total, CategoryTheory.Idempotents.Karoubi.Biproducts.bicone
-- Module: Mathlib.CategoryTheory.Idempotents.Biproducts
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasFiniteBiproducts.{v, u_1} C
n : ℕ
F : Fin n → Karoubi.{v, u_1} C
⊢ Eq.{v + 1} (α := Bicone.pt (Biproducts.bicone F) ⟶ Bicone.pt (Biproducts.bicone F))
    (∑ j : Fin n, Bicone.π (Biproducts.bicone F) j ≫ Bicone.ι (Biproducts.bicone F) j)
    (𝟙 (Bicone.pt (Biproducts.bicone F)))

Tactic:
simpa using biproduct.map_eq.symm

Premises used: Eq.symm, CategoryTheory.Limits.biproduct.map_eq
-- Module: Mathlib.CategoryTheory.Idempotents.Biproducts
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
P : Karoubi.{v, u_1} C
⊢ P.decompId_i ≫ P.complement.decompId_p = 0

Tactic:
simp only [zero_def, hom_ext_iff, complement_X, comp_f,
          decompId_i_f, decompId_p_f, complement_p, comp_sub, comp_id, idem, sub_self]

Premises used: sub_self, CategoryTheory.Idempotents.Karoubi.comp_f, CategoryTheory.Idempotents.zero_def, CategoryTheory.Category.comp_id, CategoryTheory.Idempotents.Karoubi.decompId_i_f, CategoryTheory.Idempotents.Karoubi.complement_p, CategoryTheory.Idempotents.Karoubi.idem, CategoryTheory.Idempotents.Karoubi.decompId_p_f, CategoryTheory.Idempotents.Karoubi.complement_X, CategoryTheory.Preadditive.comp_sub, CategoryTheory.Idempotents.Karoubi.hom_ext_iff
-- Module: Mathlib.CategoryTheory.Idempotents.Biproducts
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
P : Karoubi.{v, u_1} C
⊢ P.complement.decompId_i ≫ P.decompId_p = 0

Tactic:
simp only [zero_def, hom_ext_iff, complement_X, comp_f,
          decompId_i_f, complement_p, decompId_p_f, sub_comp, id_comp, idem, sub_self]

Premises used: sub_self, CategoryTheory.Idempotents.Karoubi.comp_f, CategoryTheory.Idempotents.zero_def, CategoryTheory.Idempotents.Karoubi.decompId_i_f, CategoryTheory.Idempotents.Karoubi.complement_p, CategoryTheory.Idempotents.Karoubi.idem, CategoryTheory.Idempotents.Karoubi.decompId_p_f, CategoryTheory.Idempotents.Karoubi.complement_X, CategoryTheory.Preadditive.sub_comp, CategoryTheory.Category.id_comp, CategoryTheory.Idempotents.Karoubi.hom_ext_iff
-- Module: Mathlib.CategoryTheory.Idempotents.Biproducts
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
P : Karoubi.{v, u_1} C
⊢ (HAdd.hAdd (α :=
        BinaryBicone.pt
            { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v, u_1} C }, fst := P.decompId_p,
              snd := P.complement.decompId_p, inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯,
              inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ : BinaryBicone P P.complement } ⟶
          BinaryBicone.pt
            { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v, u_1} C }, fst := P.decompId_p,
              snd := P.complement.decompId_p, inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯,
              inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ : BinaryBicone P P.complement })
        (BinaryBicone.fst
            { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v, u_1} C }, fst := P.decompId_p,
              snd := P.complement.decompId_p, inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯,
              inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ : BinaryBicone P P.complement } ≫
          BinaryBicone.inl
            { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v, u_1} C }, fst := P.decompId_p,
              snd := P.complement.decompId_p, inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯,
              inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ : BinaryBicone P P.complement })
        (BinaryBicone.snd
            { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v, u_1} C }, fst := P.decompId_p,
              snd := P.complement.decompId_p, inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯,
              inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ : BinaryBicone P P.complement } ≫
          BinaryBicone.inr
            { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v, u_1} C }, fst := P.decompId_p,
              snd := P.complement.decompId_p, inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯,
              inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ : BinaryBicone P P.complement })).f =
    Hom.f
      (𝟙
        (BinaryBicone.pt
          { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ }, fst := P.decompId_p, snd := P.complement.decompId_p,
            inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
            inr_snd := ⋯ }))

Tactic:
simp only [complement_X, comp_f, decompId_i_f, decompId_p_f, complement_p, add_def, idem,
        comp_sub, comp_id, sub_comp, id_comp, sub_self, sub_zero, add_sub_cancel, id_f]

Premises used: sub_self, CategoryTheory.Idempotents.add_def, sub_zero, CategoryTheory.Idempotents.Karoubi.id_f, CategoryTheory.Idempotents.Karoubi.comp_f, CategoryTheory.Category.comp_id, CategoryTheory.Idempotents.Karoubi.decompId_i_f, add_sub_cancel, CategoryTheory.Idempotents.Karoubi.complement_p, CategoryTheory.Idempotents.Karoubi.idem, CategoryTheory.Idempotents.Karoubi.decompId_p_f, CategoryTheory.Idempotents.Karoubi.complement_X, CategoryTheory.Preadditive.comp_sub, CategoryTheory.Preadditive.sub_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Idempotents.Biproducts
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
P : Karoubi.{v, u_1} C
h₀ :
  CategoryStruct.comp (Y := P ⊞ P.complement) biprod.inl
      (biprod.desc P.decompId_i P.complement.decompId_i ≫ biprod.lift P.decompId_p P.complement.decompId_p) =
    biprod.inl ≫ 𝟙 (P ⊞ P.complement)
h₁ :
  CategoryStruct.comp (Y := P ⊞ P.complement) biprod.inr
      (biprod.desc P.decompId_i P.complement.decompId_i ≫ biprod.lift P.decompId_p P.complement.decompId_p) =
    biprod.inr ≫ 𝟙 (P ⊞ P.complement)
⊢ biprod.desc P.decompId_i P.complement.decompId_i ≫ biprod.lift P.decompId_p P.complement.decompId_p =
    𝟙 (P ⊞ P.complement)

Tactic:
apply biprod.hom_ext'

Premises used: CategoryTheory.Limits.biprod.hom_ext'
-- Module: Mathlib.CategoryTheory.Idempotents.Biproducts
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
P : Karoubi.{v, u_1} C
h₀ : Eq (α := P ⟶ P ⊞ P.complement) ((P.decompId_i ≫ P.complement.decompId_p) ≫ biprod.inr) 0
⊢ CategoryStruct.comp (Y := P ⊞ P.complement) biprod.inl
      (biprod.desc P.decompId_i P.complement.decompId_i ≫ biprod.lift P.decompId_p P.complement.decompId_p) =
    biprod.inl ≫ 𝟙 (P ⊞ P.complement)

Tactic:
rw [biprod.inl_desc_assoc, comp_id, biprod.lift_eq, comp_add, ← decompId_assoc,
        add_eq_left, ← assoc]

Premises used: CategoryTheory.Limits.biprod.lift_eq, CategoryTheory.Category.assoc, CategoryTheory.Limits.biprod.inl_desc_assoc, CategoryTheory.Category.comp_id, add_eq_left, CategoryTheory.Idempotents.Karoubi.decompId_assoc, CategoryTheory.Preadditive.comp_add
-- Module: Mathlib.CategoryTheory.Idempotents.Biproducts
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
P : Karoubi.{v, u_1} C
⊢ Eq (α := P ⟶ P ⊞ P.complement) ((P.decompId_i ≫ P.complement.decompId_p) ≫ biprod.inr) 0

Tactic:
(?_ =≫ _).trans zero_comp

Premises used: CategoryTheory.eq_whisker, CategoryTheory.Limits.zero_comp, Eq.trans
-- Module: Mathlib.CategoryTheory.Idempotents.Biproducts
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
P : Karoubi.{v, u_1} C
h₀ : P.decompId_i ≫ P.complement.decompId_p = 0
⊢ Eq (α := P ⟶ P ⊞ P.complement) ((P.decompId_i ≫ P.complement.decompId_p) ≫ biprod.inr) 0

Tactic:
refine (?_ =≫ _).trans zero_comp

Premises used: CategoryTheory.eq_whisker, CategoryTheory.Limits.zero_comp, Eq.trans
-- Module: Mathlib.CategoryTheory.Idempotents.Biproducts
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
P : Karoubi.{v, u_1} C
h₀ : (P.decompId_i ≫ P.complement.decompId_p).f = Hom.f 0
⊢ P.decompId_i ≫ P.complement.decompId_p = 0

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Idempotents.Biproducts
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
P : Karoubi.{v, u_1} C
⊢ (P.decompId_i ≫ P.complement.decompId_p).f = Hom.f 0

Tactic:
simp only [comp_f, toKaroubi_obj_X, decompId_i_f, decompId_p_f,
        complement_p, comp_sub, comp_id, idem, sub_self, zero_def]

Premises used: sub_self, CategoryTheory.Idempotents.Karoubi.comp_f, CategoryTheory.Idempotents.zero_def, CategoryTheory.Category.comp_id, CategoryTheory.Idempotents.Karoubi.decompId_i_f, CategoryTheory.Idempotents.Karoubi.complement_p, CategoryTheory.Idempotents.Karoubi.idem, CategoryTheory.Idempotents.Karoubi.decompId_p_f, CategoryTheory.Idempotents.toKaroubi_obj_X, CategoryTheory.Preadditive.comp_sub
-- Module: Mathlib.CategoryTheory.Idempotents.Biproducts
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
P : Karoubi.{v, u_1} C
h₁ : Eq (α := P.complement ⟶ P ⊞ P.complement) ((P.complement.decompId_i ≫ P.decompId_p) ≫ biprod.inl) 0
⊢ CategoryStruct.comp (Y := P ⊞ P.complement) biprod.inr
      (biprod.desc P.decompId_i P.complement.decompId_i ≫ biprod.lift P.decompId_p P.complement.decompId_p) =
    biprod.inr ≫ 𝟙 (P ⊞ P.complement)

Tactic:
rw [biprod.inr_desc_assoc, comp_id, biprod.lift_eq, comp_add, ← decompId_assoc,
        add_eq_right, ← assoc]

Premises used: CategoryTheory.Limits.biprod.lift_eq, CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.Limits.biprod.inr_desc_assoc, add_eq_right, CategoryTheory.Idempotents.Karoubi.decompId_assoc, CategoryTheory.Preadditive.comp_add
-- Module: Mathlib.CategoryTheory.Idempotents.Biproducts
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
P : Karoubi.{v, u_1} C
⊢ Eq (α := P.complement ⟶ P ⊞ P.complement) ((P.complement.decompId_i ≫ P.decompId_p) ≫ biprod.inl) 0

Tactic:
(?_ =≫ _).trans zero_comp

Premises used: CategoryTheory.eq_whisker, CategoryTheory.Limits.zero_comp, Eq.trans
-- Module: Mathlib.CategoryTheory.Idempotents.Biproducts
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
P : Karoubi.{v, u_1} C
h₁ : P.complement.decompId_i ≫ P.decompId_p = 0
⊢ Eq (α := P.complement ⟶ P ⊞ P.complement) ((P.complement.decompId_i ≫ P.decompId_p) ≫ biprod.inl) 0

Tactic:
refine (?_ =≫ _).trans zero_comp

Premises used: CategoryTheory.eq_whisker, CategoryTheory.Limits.zero_comp, Eq.trans
-- Module: Mathlib.CategoryTheory.Idempotents.Biproducts
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
P : Karoubi.{v, u_1} C
h₁ : (P.complement.decompId_i ≫ P.decompId_p).f = Hom.f 0
⊢ P.complement.decompId_i ≫ P.decompId_p = 0

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Idempotents.Biproducts
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
P : Karoubi.{v, u_1} C
⊢ (P.complement.decompId_i ≫ P.decompId_p).f = Hom.f 0

Tactic:
simp only [complement_X, comp_f, decompId_i_f, complement_p,
        decompId_p_f, sub_comp, id_comp, idem, sub_self, zero_def]

Premises used: sub_self, CategoryTheory.Idempotents.Karoubi.comp_f, CategoryTheory.Idempotents.zero_def, CategoryTheory.Idempotents.Karoubi.decompId_i_f, CategoryTheory.Idempotents.Karoubi.complement_p, CategoryTheory.Idempotents.Karoubi.idem, CategoryTheory.Idempotents.Karoubi.decompId_p_f, CategoryTheory.Idempotents.Karoubi.complement_X, CategoryTheory.Preadditive.sub_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Idempotents.Biproducts
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
P : Karoubi.{v, u_1} C
h :
  (CategoryStruct.comp (Y := P ⊞ P.complement) (biprod.lift P.decompId_p P.complement.decompId_p)
        (biprod.desc P.decompId_i P.complement.decompId_i)).f =
    Hom.f (𝟙 (Functor.obj (toKaroubi C) P.X))
⊢ CategoryStruct.comp (Y := P ⊞ P.complement) (biprod.lift P.decompId_p P.complement.decompId_p)
      (biprod.desc P.decompId_i P.complement.decompId_i) =
    𝟙 (Functor.obj (toKaroubi C) P.X)

Tactic:
ext