-- Mathlib/Data/Matrix/Block.lean
theorem blockDiagonal'_mul [NonUnitalNonAssocSemiring α] [∀ i, Fintype (n' i)] [Fintype o]
    (M : ∀ i, Matrix (m' i) (n' i) α) (N : ∀ i, Matrix (n' i) (p' i) α) :
    (blockDiagonal' fun k => M k * N k) = blockDiagonal' M * blockDiagonal' N

Proof state:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
j' : o
hj' : j' ≠ k
x✝¹ : n' j'
x✝ : x✝¹ ∈ Finset.univ
⊢ ((if h : k = j' then M k i (cast ⋯ x✝¹) else 0) * if h : j' = k' then N j' x✝¹ (cast ⋯ j) else 0) = 0

Tactic:
rw [dif_neg hj'.symm, zero_mul]

Result:
no goals

Proof state:
case a.mk.mk
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
⊢ ∀ (x : o),
    x ≠ k →
      (∑ x_1 : n' x, (if h : k = x then M k i (cast ⋯ x_1) else 0) * if h : x = k' then N x x_1 (cast ⋯ j) else 0) = 0

Tactic:
intro j' hj'

Result:
case a.mk.mk
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
j' : o
hj' : j' ≠ k
⊢ (∑ x : n' j', (if h : k = j' then M k i (cast ⋯ x) else 0) * if h : j' = k' then N j' x (cast ⋯ j) else 0) = 0

Proof state:
case a.mk.mk
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
⊢ (if h : k = k' then ∑ j_1 : n' k, M k i j_1 * N k j_1 (cast ⋯ j) else 0) =
    ∑ x : n' k, M k i (cast ⋯ x) * if h : k = k' then N k x (cast ⋯ j) else 0

Tactic:
split_ifs <;> simp

Result:
no goals

Proof state:
case a.mk.mk
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
⊢ (if h : k = k' then ∑ j_1 : n' k, M k i j_1 * N k j_1 (cast ⋯ j) else 0) =
    ∑ x : n' k, (if h : k = k then M k i (cast ⋯ x) else 0) * if h : k = k' then N k x (cast ⋯ j) else 0

Tactic:
simp only [if_pos, dif_pos]

Result:
case a.mk.mk
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
⊢ (if h : k = k' then ∑ j_1 : n' k, M k i j_1 * N k j_1 (cast ⋯ j) else 0) =
    ∑ x : n' k, M k i (cast ⋯ x) * if h : k = k' then N k x (cast ⋯ j) else 0

Proof state:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
⊢ (blockDiagonal' fun k => M k * N k) = blockDiagonal' M * blockDiagonal' N

Tactic:
ext ⟨k, i⟩ ⟨k', j⟩

Result:
case a.mk.mk
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
⊢ blockDiagonal' (fun k => M k * N k) ⟨k, i⟩ ⟨k', j⟩ = (blockDiagonal' M * blockDiagonal' N) ⟨k, i⟩ ⟨k', j⟩

Proof state:
case a.mk.mk
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
⊢ (if h : k = k' then ∑ j_1 : n' k, M k i j_1 * N k j_1 (cast ⋯ j) else 0) =
    ∑ x : o, ∑ x_1 : n' x, (if h : k = x then M k i (cast ⋯ x_1) else 0) * if h : x = k' then N x x_1 (cast ⋯ j) else 0

Tactic:
rw [Fintype.sum_eq_single k]

Result:
case a.mk.mk
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
⊢ (if h : k = k' then ∑ j_1 : n' k, M k i j_1 * N k j_1 (cast ⋯ j) else 0) =
    ∑ x : n' k, (if h : k = k then M k i (cast ⋯ x) else 0) * if h : k = k' then N k x (cast ⋯ j) else 0

case a.mk.mk
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
⊢ ∀ (x : o),
    x ≠ k →
      (∑ x_1 : n' x, (if h : k = x then M k i (cast ⋯ x_1) else 0) * if h : x = k' then N x x_1 (cast ⋯ j) else 0) = 0

Proof state:
case a.mk.mk
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
j' : o
hj' : j' ≠ k
⊢ (∑ x : n' j', (if h : k = j' then M k i (cast ⋯ x) else 0) * if h : j' = k' then N j' x (cast ⋯ j) else 0) = 0

Tactic:
exact Finset.sum_eq_zero fun _ _ => by rw [dif_neg hj'.symm, zero_mul]

Result:
no goals

Proof state:
case a.mk.mk
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
⊢ blockDiagonal' (fun k => M k * N k) ⟨k, i⟩ ⟨k', j⟩ = (blockDiagonal' M * blockDiagonal' N) ⟨k, i⟩ ⟨k', j⟩

Tactic:
simp only [blockDiagonal'_apply, mul_apply, ← Finset.univ_sigma_univ, Finset.sum_sigma]

Result:
case a.mk.mk
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
⊢ (if h : k = k' then ∑ j_1 : n' k, M k i j_1 * N k j_1 (cast ⋯ j) else 0) =
    ∑ x : o, ∑ x_1 : n' x, (if h : k = x then M k i (cast ⋯ x_1) else 0) * if h : x = k' then N x x_1 (cast ⋯ j) else 0