-- 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))
i : ι
⊢ ((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) i =
    HMul.hMul (α := Matrix (↑(h ⁻¹' {i}) : Type) (↑(g ⁻¹' {i}) : Type) (End (s i))) (β :=
      Matrix (↑(g ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))
      (((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 i :
        Matrix (↑(h ⁻¹' {i}) : Type) (↑(g ⁻¹' {i}) : Type) (End (s i)))
      (((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 i :
        Matrix (↑(g ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))
have a : ∀ (c : γ) (a : α) (j_property : a ∈ f ⁻¹' {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 sorry)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {h c}) a j_property) =
    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 sorry)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {h c}) a j_property)
Tactic: ext ⟨c, ⟨⟩⟩ ⟨a, j_property⟩
Cleared hypotheses: i