-- 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 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
ι : Type u_3
f : ι → Type u_2
g : (i : ι) → f i → C
inst_6 : ∀ (i : ι), HasBiproduct.{u_2, v, u} (g i)
inst_7 : HasBiproduct.{u_3, v, u} (C := C) fun (i : ι) ↦ biproduct.{u_2, v, u} (g i)
x_1 x_2 : (i : ι) × f i
j : ι
x : f j
j' : ι
y : f j'
⊢ Eq.{v + 1} (α :=
    g ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i))
        ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).snd (β := fun (i : ι) ↦ f i)) ⟶
      g ((Sigma.mk (β := fun (i : ι) ↦ f i) j' y).fst (β := fun (i : ι) ↦ f i))
        ((Sigma.mk (β := fun (i : ι) ↦ f i) j' y).snd (β := fun (i : ι) ↦ f i)))
    (CategoryStruct.comp (Y := biproduct.{u_3, v, u} fun (i : ι) ↦ biproduct.{u_2, v, u} (g i))
      (CategoryStruct.comp (Y :=
        biproduct.{u_2, v, u} (J := f ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i)))
          (g ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i))))
        (biproduct.ι (g ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i)))
          ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).snd (β := fun (i : ι) ↦ f i)))
        (biproduct.ι.{u_3, v, u} (C := C) (fun (i : ι) ↦ biproduct.{u_2, v, u} (g i))
          ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i))))
      (biproduct.π (fun (i : ι) ↦ biproduct.{u_2, v, u} (g i))
          ((Sigma.mk (β := fun (i : ι) ↦ f i) j' y).fst (β := fun (i : ι) ↦ f i)) ≫
        biproduct.π (g ((Sigma.mk (β := fun (i : ι) ↦ f i) j' y).fst (β := fun (i : ι) ↦ f i)))
          ((Sigma.mk (β := fun (i : ι) ↦ f i) j' y).snd (β := fun (i : ι) ↦ f i))))
    (if h : Sigma.mk (β := fun (i : ι) ↦ f i) j x = Sigma.mk (β := fun (i : ι) ↦ f i) j' y then eqToHom ⋯ else 0)
have pos : ∀ (h : Sigma.mk (β := fun (i : ι) ↦ f i) j x = Sigma.mk (β := fun (i : ι) ↦ f i) j' y),
  Eq.{v + 1} (α :=
    g ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i))
        ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).snd (β := fun (i : ι) ↦ f i)) ⟶
      g ((Sigma.mk (β := fun (i : ι) ↦ f i) j' y).fst (β := fun (i : ι) ↦ f i))
        ((Sigma.mk (β := fun (i : ι) ↦ f i) j' y).snd (β := fun (i : ι) ↦ f i)))
    (CategoryStruct.comp (Y := biproduct.{u_3, v, u} fun (i : ι) ↦ biproduct.{u_2, v, u} (g i))
      (CategoryStruct.comp (Y :=
        biproduct.{u_2, v, u} (J := f ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i)))
          (g ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i))))
        (biproduct.ι (g ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i)))
          ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).snd (β := fun (i : ι) ↦ f i)))
        (biproduct.ι.{u_3, v, u} (C := C) (fun (i : ι) ↦ biproduct.{u_2, v, u} (g i))
          ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i))))
      (biproduct.π (fun (i : ι) ↦ biproduct.{u_2, v, u} (g i))
          ((Sigma.mk (β := fun (i : ι) ↦ f i) j' y).fst (β := fun (i : ι) ↦ f i)) ≫
        biproduct.π (g ((Sigma.mk (β := fun (i : ι) ↦ f i) j' y).fst (β := fun (i : ι) ↦ f i)))
          ((Sigma.mk (β := fun (i : ι) ↦ f i) j' y).snd (β := fun (i : ι) ↦ f i))))
    (eqToHom sorry)
Tactic: split_ifs with h