-- Mathlib/CategoryTheory/Preadditive/HomOrthogonal.lean
theorem matrixDecomposition_comp (o : HomOrthogonal s) {α β γ : Type} [Finite α] [Fintype β]
    [Finite γ] {f : α → ι} {g : β → ι} {h : γ → ι} (z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b))
    (w : (⨁ fun b => s (g b)) ⟶ ⨁ fun c => s (h c)) (i : ι) :
    o.matrixDecomposition (z ≫ w) i = o.matrixDecomposition w i * o.matrixDecomposition z i

Proof state:
case a.mk.refl.mk.w'
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Finite α
inst✝¹ : Fintype β
inst✝ : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
w : (⨁ fun b => s (g b)) ⟶ ⨁ fun c => s (h c)
c : γ
a : α
j_property✝ : a ∈ f ⁻¹' {h c}
j_property : f a = h c
b : β
nm : ¬g b = h c
⊢ eqToHom ⋯ ≫
      biproduct.ι (fun a => s (f a)) a ≫
        z ≫ biproduct.π (fun b => s (g b)) b ≫ biproduct.ι (fun b => s (g b)) b ≫ w ≫ biproduct.π (fun b => s (h b)) c =
    0

Tactic:
have : biproduct.ι (fun b ↦ s (g b)) b ≫ w ≫ biproduct.π (fun b ↦ s (h b)) c = 0 := by
  apply o.eq_zero nm

Result:
case a.mk.refl.mk.w'
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Finite α
inst✝¹ : Fintype β
inst✝ : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
w : (⨁ fun b => s (g b)) ⟶ ⨁ fun c => s (h c)
c : γ
a : α
j_property✝ : a ∈ f ⁻¹' {h c}
j_property : f a = h c
b : β
nm : ¬g b = h c
this : biproduct.ι (fun b => s (g b)) b ≫ w ≫ biproduct.π (fun b => s (h b)) c = 0
⊢ eqToHom ⋯ ≫
      biproduct.ι (fun a => s (f a)) a ≫
        z ≫ biproduct.π (fun b => s (g b)) b ≫ biproduct.ι (fun b => s (g b)) b ≫ w ≫ biproduct.π (fun b => s (h b)) c =
    0

Proof state:
case a.mk.refl.mk
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Finite α
inst✝¹ : Fintype β
inst✝ : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
w : (⨁ fun b => s (g b)) ⟶ ⨁ fun c => s (h c)
c : γ
a : α
j_property : a ∈ f ⁻¹' {h c}
⊢ o.matrixDecomposition (z ≫ w) (h c) ⟨c, ⋯⟩ ⟨a, j_property⟩ =
    (o.matrixDecomposition w (h c) * o.matrixDecomposition z (h c)) ⟨c, ⋯⟩ ⟨a, j_property⟩

Tactic:
simp only [Set.mem_preimage, Set.mem_singleton_iff] at j_property

Result:
case a.mk.refl.mk
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Finite α
inst✝¹ : Fintype β
inst✝ : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
w : (⨁ fun b => s (g b)) ⟶ ⨁ fun c => s (h c)
c : γ
a : α
j_property✝ : a ∈ f ⁻¹' {h c}
j_property : f a = h c
⊢ o.matrixDecomposition (z ≫ w) (h c) ⟨c, ⋯⟩ ⟨a, j_property✝⟩ =
    (o.matrixDecomposition w (h c) * o.matrixDecomposition z (h c)) ⟨c, ⋯⟩ ⟨a, j_property✝⟩

Proof state:
case a.mk.refl.mk.w'
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Finite α
inst✝¹ : Fintype β
inst✝ : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
w : (⨁ fun b => s (g b)) ⟶ ⨁ fun c => s (h c)
c : γ
a : α
j_property✝ : a ∈ f ⁻¹' {h c}
j_property : f a = h c
⊢ ∀ x ∉ g ⁻¹' {h c},
    eqToHom ⋯ ≫
        biproduct.ι (fun a => s (f a)) a ≫
          z ≫
            ((biproduct.π (fun b => s (g b)) x ≫ biproduct.ι (fun b => s (g b)) x) ≫ w) ≫
              biproduct.π (fun b => s (h b)) c =
      0

Tactic:
intro b nm

Result:
case a.mk.refl.mk.w'
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Finite α
inst✝¹ : Fintype β
inst✝ : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
w : (⨁ fun b => s (g b)) ⟶ ⨁ fun c => s (h c)
c : γ
a : α
j_property✝ : a ∈ f ⁻¹' {h c}
j_property : f a = h c
b : β
nm : b ∉ g ⁻¹' {h c}
⊢ eqToHom ⋯ ≫
      biproduct.ι (fun a => s (f a)) a ≫
        z ≫
          ((biproduct.π (fun b => s (g b)) b ≫ biproduct.ι (fun b => s (g b)) b) ≫ w) ≫
            biproduct.π (fun b => s (h b)) c =
    0

Proof state:
case a.mk.refl.mk.w'
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Finite α
inst✝¹ : Fintype β
inst✝ : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
w : (⨁ fun b => s (g b)) ⟶ ⨁ fun c => s (h c)
c : γ
a : α
j_property✝ : a ∈ f ⁻¹' {h c}
j_property : f a = h c
b : β
nm : ¬g b = h c
this : biproduct.ι (fun b => s (g b)) b ≫ w ≫ biproduct.π (fun b => s (h b)) c = 0
⊢ eqToHom ⋯ ≫
      biproduct.ι (fun a => s (f a)) a ≫
        z ≫ biproduct.π (fun b => s (g b)) b ≫ biproduct.ι (fun b => s (g b)) b ≫ w ≫ biproduct.π (fun b => s (h b)) c =
    0

Tactic:
simp only [this, comp_zero]

Result:
no goals

Proof state:
case a.mk.refl.mk.w'
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Finite α
inst✝¹ : Fintype β
inst✝ : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
w : (⨁ fun b => s (g b)) ⟶ ⨁ fun c => s (h c)
c : γ
a : α
j_property✝ : a ∈ f ⁻¹' {h c}
j_property : f a = h c
b : β
nm : ¬g b = h c
⊢ eqToHom ⋯ ≫
      biproduct.ι (fun a => s (f a)) a ≫
        z ≫
          ((biproduct.π (fun b => s (g b)) b ≫ biproduct.ι (fun b => s (g b)) b) ≫ w) ≫
            biproduct.π (fun b => s (h b)) c =
    0

Tactic:
simp only [Category.assoc]

Result:
case a.mk.refl.mk.w'
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Finite α
inst✝¹ : Fintype β
inst✝ : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
w : (⨁ fun b => s (g b)) ⟶ ⨁ fun c => s (h c)
c : γ
a : α
j_property✝ : a ∈ f ⁻¹' {h c}
j_property : f a = h c
b : β
nm : ¬g b = h c
⊢ eqToHom ⋯ ≫
      biproduct.ι (fun a => s (f a)) a ≫
        z ≫ biproduct.π (fun b => s (g b)) b ≫ biproduct.ι (fun b => s (g b)) b ≫ w ≫ biproduct.π (fun b => s (h b)) c =
    0

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Finite α
inst✝¹ : Fintype β
inst✝ : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
w : (⨁ fun b => s (g b)) ⟶ ⨁ fun c => s (h c)
i : ι
⊢ o.matrixDecomposition (z ≫ w) i = o.matrixDecomposition w i * o.matrixDecomposition z i

Tactic:
ext ⟨c, ⟨⟩⟩ ⟨a, j_property⟩

Result:
case a.mk.refl.mk
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Finite α
inst✝¹ : Fintype β
inst✝ : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
w : (⨁ fun b => s (g b)) ⟶ ⨁ fun c => s (h c)
c : γ
a : α
j_property : a ∈ f ⁻¹' {h c}
⊢ o.matrixDecomposition (z ≫ w) (h c) ⟨c, ⋯⟩ ⟨a, j_property⟩ =
    (o.matrixDecomposition w (h c) * o.matrixDecomposition z (h c)) ⟨c, ⋯⟩ ⟨a, j_property⟩