-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
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' : W' ⟶ biproduct.{0, v, u} f)
    (w :
      Eq (α := W' ⟶ biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f)) (g' ≫ biproduct.toSubtype f p)
        0),
    CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f))
        ((fun {x : C} (g : x ⟶ biproduct.{0, v, u} f)
              (x_1 :
                Eq (α := x ⟶ biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f))
                  (g ≫ biproduct.toSubtype f p) 0) ↦
            (g ≫ biproduct.toSubtype f pᶜ : x ⟶ biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f)))
          g' w)
        (biproduct.fromSubtype f pᶜ) =
      g'
w :
  ∀ {W' : C} (g' : W' ⟶ biproduct.{0, v, u} f)
    (w :
      Eq (α := W' ⟶ biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f)) (g' ≫ biproduct.toSubtype f p) 0)
    (j : K),
    CategoryStruct.comp (Y := biproduct.{0, v, u} f)
        (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f))
          ((fun {x : C} (g : x ⟶ biproduct.{0, v, u} f)
                (x_1 :
                  Eq (α := x ⟶ biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f))
                    (g ≫ biproduct.toSubtype f p) 0) ↦
              (g ≫ biproduct.toSubtype f pᶜ : x ⟶ biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f)))
            g' w)
          (biproduct.fromSubtype f pᶜ))
        (biproduct.π f j) =
      g' ≫ biproduct.π f j
w₁ :
  ∀ {W' : C} (g' : W' ⟶ biproduct.{0, v, u} f)
    (w :
      Eq (α := W' ⟶ biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f)) (g' ≫ biproduct.toSubtype f p) 0)
    (j : K), (g' ≫ biproduct.π f j ≫ if (p j)ᶜ then 𝟙 (f j) else 0) = g' ≫ biproduct.π f j
pos :
  ∀ {W' : C} (g' : W' ⟶ biproduct.{0, v, u} f)
    (w :
      Eq (α := W' ⟶ biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f)) (g' ≫ biproduct.toSubtype f p) 0)
    (j : K) (h : (p j)ᶜ), g' ≫ biproduct.π f j ≫ 𝟙 (f j) = g' ≫ biproduct.π f j
⊢ ∀ {W' : C} (g' : W' ⟶ biproduct.{0, v, u} f)
    (eq' :
      Eq (α := W' ⟶ biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f)) (g' ≫ biproduct.toSubtype f p)
        0),
    CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f))
        ((fun {x : C} (g : x ⟶ biproduct.{0, v, u} f)
              (x_1 :
                Eq (α := x ⟶ biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f))
                  (g ≫ biproduct.toSubtype f p) 0) ↦
            (g ≫ biproduct.toSubtype f pᶜ : x ⟶ biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f)))
          g' eq')
        (biproduct.fromSubtype f pᶜ) =
      g'
have neg : ∀ {W' : C} (g' : W' ⟶ biproduct.{0, v, u} f)
  (w :
    Eq (α := W' ⟶ biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f)) (g' ≫ biproduct.toSubtype f p) 0)
  (j : K) (h : ¬(p j)ᶜ), g' ≫ biproduct.π f j ≫ 0 = g' ≫ biproduct.π f j
Tactic: classical
        intro W' g' w
        ext j
        simp only [Category.assoc, biproduct.toSubtype_fromSubtype, Pi.compl_apply,
          biproduct.map_π]
        split_ifs with h
        · simp
        · replace w := w =≫ biproduct.π _ ⟨j, not_not.mp h⟩
          simpa using w.symm