-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
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
a₁ :
  eqToHom ⋯ ≫ 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 ⋯ ≫
        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
⊢ ((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)

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]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.End.mul_def, Matrix.mul_apply, CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, CategoryTheory.HomOrthogonal.matrixDecomposition_apply, CategoryTheory.eqToHom_trans_assoc, CategoryTheory.Limits.biproduct.components, CategoryTheory.Category.id_comp