-- Mathlib/Topology/Instances/Matrix.lean
theorem Matrix.blockDiagonal'_tsum [DecidableEq l] [T2Space R]
    {f : X → ∀ i, Matrix (m' i) (n' i) R} :
    blockDiagonal' (∑' x, f x) = ∑' x, blockDiagonal' (f x)

Proof state:
X : Type u_1
l : Type u_3
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : DecidableEq l
inst✝ : T2Space R
f : X → (i : l) → Matrix (m' i) (n' i) R
⊢ blockDiagonal' (∑' (x : X), f x) = ∑' (x : X), blockDiagonal' (f x)

Tactic:
by_cases hf : Summable f

Result:
case pos
X : Type u_1
l : Type u_3
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : DecidableEq l
inst✝ : T2Space R
f : X → (i : l) → Matrix (m' i) (n' i) R
hf : Summable f
⊢ blockDiagonal' (∑' (x : X), f x) = ∑' (x : X), blockDiagonal' (f x)

case neg
X : Type u_1
l : Type u_3
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : DecidableEq l
inst✝ : T2Space R
f : X → (i : l) → Matrix (m' i) (n' i) R
hf : ¬Summable f
⊢ blockDiagonal' (∑' (x : X), f x) = ∑' (x : X), blockDiagonal' (f x)

Proof state:
case pos
X : Type u_1
l : Type u_3
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : DecidableEq l
inst✝ : T2Space R
f : X → (i : l) → Matrix (m' i) (n' i) R
hf : Summable f
⊢ blockDiagonal' (∑' (x : X), f x) = ∑' (x : X), blockDiagonal' (f x)

Tactic:
exact hf.hasSum.matrix_blockDiagonal'.tsum_eq.symm

Result:
no goals

Proof state:
case neg
X : Type u_1
l : Type u_3
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : DecidableEq l
inst✝ : T2Space R
f : X → (i : l) → Matrix (m' i) (n' i) R
hf : ¬Summable f
hft : ¬Summable fun x => blockDiagonal' (f x)
⊢ blockDiagonal' 0 = 0

Tactic:
exact blockDiagonal'_zero

Result:
no goals

Proof state:
case neg
X : Type u_1
l : Type u_3
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : DecidableEq l
inst✝ : T2Space R
f : X → (i : l) → Matrix (m' i) (n' i) R
hf : ¬Summable f
hft : ¬Summable fun x => blockDiagonal' (f x)
⊢ blockDiagonal' (∑' (x : X), f x) = ∑' (x : X), blockDiagonal' (f x)

Tactic:
rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hft]

Result:
case neg
X : Type u_1
l : Type u_3
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : DecidableEq l
inst✝ : T2Space R
f : X → (i : l) → Matrix (m' i) (n' i) R
hf : ¬Summable f
hft : ¬Summable fun x => blockDiagonal' (f x)
⊢ blockDiagonal' 0 = 0

Proof state:
case neg
X : Type u_1
l : Type u_3
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : DecidableEq l
inst✝ : T2Space R
f : X → (i : l) → Matrix (m' i) (n' i) R
hf : ¬Summable f
⊢ blockDiagonal' (∑' (x : X), f x) = ∑' (x : X), blockDiagonal' (f x)

Tactic:
have hft := summable_matrix_blockDiagonal'.not.mpr hf

Result:
case neg
X : Type u_1
l : Type u_3
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : DecidableEq l
inst✝ : T2Space R
f : X → (i : l) → Matrix (m' i) (n' i) R
hf : ¬Summable f
hft : ¬Summable fun x => blockDiagonal' (f x)
⊢ blockDiagonal' (∑' (x : X), f x) = ∑' (x : X), blockDiagonal' (f x)