-- Mathlib/Data/Matrix/Block.lean
theorem blockDiagonal'_diagonal [∀ i, DecidableEq (m' i)] (d : ∀ i, m' i → α) :
    (blockDiagonal' fun k => diagonal (d k)) = diagonal fun ik => d ik.1 ik.2

Proof state:
case a.mk.mk.inl
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
i : o
k k' : m' i
⊢ (if h : i = i then of (fun i_1 j => if i_1 = j then d i i_1 else 0) k (cast ⋯ k') else 0) =
    of (fun i j => if i = j then d i.fst i.snd else 0) ⟨i, k⟩ ⟨i, k'⟩

Tactic:
simp

Result:
no goals

Proof state:
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
⊢ (blockDiagonal' fun k => diagonal (d k)) = diagonal fun ik => d ik.fst ik.snd

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

Result:
case a.mk.mk
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
i : o
k : m' i
j : o
k' : m' j
⊢ blockDiagonal' (fun k => diagonal (d k)) ⟨i, k⟩ ⟨j, k'⟩ = diagonal (fun ik => d ik.fst ik.snd) ⟨i, k⟩ ⟨j, k'⟩

Proof state:
case a.mk.mk
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
i : o
k : m' i
j : o
k' : m' j
⊢ blockDiagonal' (fun k => diagonal (d k)) ⟨i, k⟩ ⟨j, k'⟩ = diagonal (fun ik => d ik.fst ik.snd) ⟨i, k⟩ ⟨j, k'⟩

Tactic:
simp only [blockDiagonal'_apply, diagonal]

Result:
case a.mk.mk
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
i : o
k : m' i
j : o
k' : m' j
⊢ (if h : i = j then of (fun i_1 j => if i_1 = j then d i i_1 else 0) k (cast ⋯ k') else 0) =
    of (fun i j => if i = j then d i.fst i.snd else 0) ⟨i, k⟩ ⟨j, k'⟩

Proof state:
case a.mk.mk
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
i : o
k : m' i
j : o
k' : m' j
⊢ (if h : i = j then of (fun i_1 j => if i_1 = j then d i i_1 else 0) k (cast ⋯ k') else 0) =
    of (fun i j => if i = j then d i.fst i.snd else 0) ⟨i, k⟩ ⟨j, k'⟩

Tactic:
obtain rfl | hij := Decidable.eq_or_ne i j

Result:
case a.mk.mk.inl
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
i : o
k k' : m' i
⊢ (if h : i = i then of (fun i_1 j => if i_1 = j then d i i_1 else 0) k (cast ⋯ k') else 0) =
    of (fun i j => if i = j then d i.fst i.snd else 0) ⟨i, k⟩ ⟨i, k'⟩

case a.mk.mk.inr
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
i : o
k : m' i
j : o
k' : m' j
hij : i ≠ j
⊢ (if h : i = j then of (fun i_1 j => if i_1 = j then d i i_1 else 0) k (cast ⋯ k') else 0) =
    of (fun i j => if i = j then d i.fst i.snd else 0) ⟨i, k⟩ ⟨j, k'⟩

Proof state:
case a.mk.mk.inr
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
i : o
k : m' i
j : o
k' : m' j
hij : i ≠ j
⊢ (if h : i = j then of (fun i_1 j => if i_1 = j then d i i_1 else 0) k (cast ⋯ k') else 0) =
    of (fun i j => if i = j then d i.fst i.snd else 0) ⟨i, k⟩ ⟨j, k'⟩

Tactic:
simp [hij]

Result:
no goals