-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
o : HomOrthogonal.{v, u, u_1} s
α β γ : Type
inst_3 : Finite α
inst_4 : Fintype β
inst_5 : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
w : Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (b : β) ↦ s (g b)) (biproduct.{0, v, u} fun (c : γ) ↦ s (h c))
c : γ
a : α
j_property_1 : a ∈ f ⁻¹' {h c}
j_property : f a = h c
⊢ ((o.matrixDecomposition :
          Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a))
              (biproduct.{0, v, u} fun (b : γ) ↦ s (h b)) ≃
            ((i : ι) → Matrix (↑(h ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))) :
        (a : (⨁ fun (a : α) ↦ s (f a)) ⟶ ⨁ fun (b : γ) ↦ s (h b)) →
          (i : ι) → Matrix (↑(h ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))
      (z ≫ w) (h c) (Subtype.mk (p := fun (x : γ) ↦ x ∈ h ⁻¹' {h c}) c ⋯)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {h c}) a j_property_1) =
    HMul.hMul (α := Matrix (↑(h ⁻¹' {h c}) : Type) (↑(g ⁻¹' {h c}) : Type) (End (s (h c)))) (β :=
      Matrix (↑(g ⁻¹' {h c}) : Type) (↑(f ⁻¹' {h c}) : Type) (End (s (h c))))
      (((o.matrixDecomposition :
              Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : β) ↦ s (g a))
                  (biproduct.{0, v, u} fun (b : γ) ↦ s (h b)) ≃
                ((i : ι) → Matrix (↑(h ⁻¹' {i}) : Type) (↑(g ⁻¹' {i}) : Type) (End (s i)))) :
            (a : (⨁ fun (a : β) ↦ s (g a)) ⟶ ⨁ fun (b : γ) ↦ s (h b)) →
              (i : ι) → Matrix (↑(h ⁻¹' {i}) : Type) (↑(g ⁻¹' {i}) : Type) (End (s i)))
          w (h c) :
        Matrix (↑(h ⁻¹' {h c}) : Type) (↑(g ⁻¹' {h c}) : Type) (End (s (h c))))
      (((o.matrixDecomposition :
              Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a))
                  (biproduct.{0, v, u} fun (b : β) ↦ s (g b)) ≃
                ((i : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))) :
            (a : (⨁ fun (a : α) ↦ s (f a)) ⟶ ⨁ fun (b : β) ↦ s (g b)) →
              (i : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))
          z (h c) :
        Matrix (↑(g ⁻¹' {h c}) : Type) (↑(f ⁻¹' {h c}) : Type) (End (s (h c))))
      (Subtype.mk (p := fun (x : γ) ↦ x ∈ h ⁻¹' {h c}) c ⋯)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {h c}) a j_property_1)
have a₁ : eqToHom sorry ≫ biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a ≫ z ≫ w ≫ biproduct.π (fun (b : γ) ↦ s (h b)) c =
  ∑ x : (↑(g ⁻¹' {h c}) : Type),
    eqToHom sorry ≫
      biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a ≫
        z ≫
          biproduct.π (fun (b : β) ↦ s (g b)) (↑x : β) ≫
            biproduct.ι.{0, v, u} (C := C) (fun (a : β) ↦ s (g a)) (↑x : β) ≫ w ≫ biproduct.π (fun (b : γ) ↦ s (h b)) c
Tactic: simp only [Matrix.mul_apply, Limits.biproduct.components,
    HomOrthogonal.matrixDecomposition_apply, Category.comp_id, Category.id_comp, Category.assoc,
    End.mul_def, eqToHom_refl, eqToHom_trans_assoc]