case a.h
l : Type ?u.242028
m : Type ?u.242031
n : Type ?u.242034
o : Type u_5
p : Type ?u.242040
q : Type ?u.242043
m' : o → Type u_3
n' : o → Type u_4
p' : o → Type ?u.242058
R✝ : Type ?u.242061
S : Type ?u.242064
α : Type u_2
β : Type ?u.242070
inst✝³ : DecidableEq o
R : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid α
inst✝ : Module R α
x : R
M : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
x✝ : (i : o) × n' i
⊢ blockDiagonal' (x • M) i✝ x✝ = (x • blockDiagonal' M) i✝ x✝
l : Type ?u.242028
m : Type ?u.242031
n : Type ?u.242034
o : Type u_5
p : Type ?u.242040
q : Type ?u.242043
m' : o → Type u_3
n' : o → Type u_4
p' : o → Type ?u.242058
R✝ : Type ?u.242061
S : Type ?u.242064
α : Type u_2
β : Type ?u.242070
inst✝³ : DecidableEq o
R : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid α
inst✝ : Module R α
x : R
M : (i : o) → Matrix (m' i) (n' i) α
⊢ blockDiagonal' (x • M) = x • blockDiagonal' M
ext
case a.h
l : Type ?u.242028
m : Type ?u.242031
n : Type ?u.242034
o : Type u_5
p : Type ?u.242040
q : Type ?u.242043
m' : o → Type u_3
n' : o → Type u_4
p' : o → Type ?u.242058
R✝ : Type ?u.242061
S : Type ?u.242064
α : Type u_2
β : Type ?u.242070
inst✝³ : DecidableEq o
R : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid α
inst✝ : Module R α
x : R
M : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
x✝ : (i : o) × n' i
⊢ (if h : i✝.fst = x✝.fst then x • M i✝.fst i✝.snd (cast (_ : n' x✝.fst = n' i✝.fst) x✝.snd) else 0) =
    x • if h : i✝.fst = x✝.fst then M i✝.fst i✝.snd (cast (_ : n' x✝.fst = n' i✝.fst) x✝.snd) else 0
case a.h
l : Type ?u.242028
m : Type ?u.242031
n : Type ?u.242034
o : Type u_5
p : Type ?u.242040
q : Type ?u.242043
m' : o → Type u_3
n' : o → Type u_4
p' : o → Type ?u.242058
R✝ : Type ?u.242061
S : Type ?u.242064
α : Type u_2
β : Type ?u.242070
inst✝³ : DecidableEq o
R : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid α
inst✝ : Module R α
x : R
M : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
x✝ : (i : o) × n' i
⊢ blockDiagonal' (x • M) i✝ x✝ = (x • blockDiagonal' M) i✝ x✝
simp only [blockDiagonal'_apply, Pi.smul_apply, smul_apply]
no goals
case a.h
l : Type ?u.242028
m : Type ?u.242031
n : Type ?u.242034
o : Type u_5
p : Type ?u.242040
q : Type ?u.242043
m' : o → Type u_3
n' : o → Type u_4
p' : o → Type ?u.242058
R✝ : Type ?u.242061
S : Type ?u.242064
α : Type u_2
β : Type ?u.242070
inst✝³ : DecidableEq o
R : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid α
inst✝ : Module R α
x : R
M : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
x✝ : (i : o) × n' i
⊢ (if h : i✝.fst = x✝.fst then x • M i✝.fst i✝.snd (cast (_ : n' x✝.fst = n' i✝.fst) x✝.snd) else 0) =
    x • if h : i✝.fst = x✝.fst then M i✝.fst i✝.snd (cast (_ : n' x✝.fst = n' i✝.fst) x✝.snd) else 0
split_ifs <;> simp