case a.h
l : Type ?u.169372
m : Type u_3
n : Type u_4
o : Type u_5
p : Type ?u.169384
q : Type ?u.169387
m' : o → Type ?u.169392
n' : o → Type ?u.169397
p' : o → Type ?u.169402
R✝ : Type ?u.169405
S : Type ?u.169408
α : Type u_2
β : Type ?u.169414
inst✝³ : DecidableEq o
R : Type u_1
inst✝² : Monoid R
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction R α
x : R
M : o → Matrix m n α
i✝ : m × o
x✝ : n × o
⊢ blockDiagonal (x • M) i✝ x✝ = (x • blockDiagonal M) i✝ x✝
l : Type ?u.169372
m : Type u_3
n : Type u_4
o : Type u_5
p : Type ?u.169384
q : Type ?u.169387
m' : o → Type ?u.169392
n' : o → Type ?u.169397
p' : o → Type ?u.169402
R✝ : Type ?u.169405
S : Type ?u.169408
α : Type u_2
β : Type ?u.169414
inst✝³ : DecidableEq o
R : Type u_1
inst✝² : Monoid R
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction R α
x : R
M : o → Matrix m n α
⊢ blockDiagonal (x • M) = x • blockDiagonal M
ext
case a.h
l : Type ?u.169372
m : Type u_3
n : Type u_4
o : Type u_5
p : Type ?u.169384
q : Type ?u.169387
m' : o → Type ?u.169392
n' : o → Type ?u.169397
p' : o → Type ?u.169402
R✝ : Type ?u.169405
S : Type ?u.169408
α : Type u_2
β : Type ?u.169414
inst✝³ : DecidableEq o
R : Type u_1
inst✝² : Monoid R
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction R α
x : R
M : o → Matrix m n α
i✝ : m × o
x✝ : n × o
⊢ (if i✝.snd = x✝.snd then x • M i✝.snd i✝.fst x✝.fst else 0) =
    x • if i✝.snd = x✝.snd then M i✝.snd i✝.fst x✝.fst else 0
case a.h
l : Type ?u.169372
m : Type u_3
n : Type u_4
o : Type u_5
p : Type ?u.169384
q : Type ?u.169387
m' : o → Type ?u.169392
n' : o → Type ?u.169397
p' : o → Type ?u.169402
R✝ : Type ?u.169405
S : Type ?u.169408
α : Type u_2
β : Type ?u.169414
inst✝³ : DecidableEq o
R : Type u_1
inst✝² : Monoid R
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction R α
x : R
M : o → Matrix m n α
i✝ : m × o
x✝ : n × o
⊢ 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.169372
m : Type u_3
n : Type u_4
o : Type u_5
p : Type ?u.169384
q : Type ?u.169387
m' : o → Type ?u.169392
n' : o → Type ?u.169397
p' : o → Type ?u.169402
R✝ : Type ?u.169405
S : Type ?u.169408
α : Type u_2
β : Type ?u.169414
inst✝³ : DecidableEq o
R : Type u_1
inst✝² : Monoid R
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction R α
x : R
M : o → Matrix m n α
i✝ : m × o
x✝ : n × o
⊢ (if i✝.snd = x✝.snd then x • M i✝.snd i✝.fst x✝.fst else 0) =
    x • if i✝.snd = x✝.snd then M i✝.snd i✝.fst x✝.fst else 0
split_ifs <;> simp