-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K_1 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
K : Type
inst_6 : Finite K
inst_7 : HasFiniteBiproducts.{v, u} C
f : K → C
p : K → Prop
intro intro₁ intro₂ :
  ∀ {W : C} (g' : biproduct.{0, v, u} f ⟶ W)
    (w :
      Eq (α := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f) ⟶ W) (biproduct.fromSubtype f p ≫ g')
        0),
    CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f))
        (biproduct.toSubtype f pᶜ)
        ((fun {x : C} (g : biproduct.{0, v, u} f ⟶ x)
              (x_1 :
                Eq (α := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f) ⟶ x)
                  (biproduct.fromSubtype f p ≫ g) 0) ↦
            (biproduct.fromSubtype f pᶜ ≫ g : biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f) ⟶ x))
          g' w) =
      g'
w :
  ∀ {W : C} (g' : biproduct.{0, v, u} f ⟶ W)
    (w :
      Eq (α := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f) ⟶ W) (biproduct.fromSubtype f p ≫ g')
        0)
    (j : K),
    CategoryStruct.comp (Y := biproduct.{0, v, u} f) (biproduct.ι f j)
        (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f))
          (biproduct.toSubtype f pᶜ)
          ((fun {x : C} (g : biproduct.{0, v, u} f ⟶ x)
                (x_1 :
                  Eq (α := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f) ⟶ x)
                    (biproduct.fromSubtype f p ≫ g) 0) ↦
              (biproduct.fromSubtype f pᶜ ≫ g : biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f) ⟶ x))
            g' w)) =
      biproduct.ι f j ≫ g'
w₁ :
  ∀ {W : C} (g' : biproduct.{0, v, u} f ⟶ W)
    (w :
      Eq (α := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f) ⟶ W) (biproduct.fromSubtype f p ≫ g')
        0)
    (j : K), (if (p j)ᶜ then 𝟙 (f j) else 0) ≫ biproduct.ι f j ≫ g' = biproduct.ι f j ≫ g'
pos :
  ∀ {W : C} (g' : biproduct.{0, v, u} f ⟶ W)
    (w :
      Eq (α := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f) ⟶ W) (biproduct.fromSubtype f p ≫ g')
        0)
    (j : K) (h : (p j)ᶜ), 𝟙 (f j) ≫ biproduct.ι f j ≫ g' = biproduct.ι f j ≫ g'
neg neg₁ :
  ∀ {W : C} (g' : biproduct.{0, v, u} f ⟶ W)
    (w :
      Eq (α := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f) ⟶ W) (biproduct.fromSubtype f p ≫ g')
        0)
    (j : K) (h : ¬(p j)ᶜ), 0 ≫ biproduct.ι f j ≫ g' = biproduct.ι f j ≫ g'
⊢ ∀ {Z' : C} (g' : biproduct.{0, v, u} f ⟶ Z')
    (eq' :
      Eq (α := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f) ⟶ Z') (biproduct.fromSubtype f p ≫ g')
        0),
    CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f))
        (biproduct.toSubtype f pᶜ)
        ((fun {x : C} (g : biproduct.{0, v, u} f ⟶ x)
              (x_1 :
                Eq (α := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f) ⟶ x)
                  (biproduct.fromSubtype f p ≫ g) 0) ↦
            (biproduct.fromSubtype f pᶜ ≫ g : biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f) ⟶ x))
          g' eq') =
      g'

Tactic:
classical
        intro W g' w
        ext j
        simp only [biproduct.toSubtype_fromSubtype_assoc, Pi.compl_apply, biproduct.ι_map_assoc]
        split_ifs with h
        · simp
        · replace w := biproduct.ι _ (⟨j, not_not.mp h⟩ : Subtype p) ≫= w
          simpa using w.symm

Premises used: CategoryTheory.Limits.biproduct.ι_map_assoc, CategoryTheory.Limits.biproduct.toSubtype_fromSubtype_assoc, Pi.compl_apply