case a.h
l : Type ?u.131023
m : Type u_1
n : Type u_2
o : Type u_4
p : Type ?u.131035
q : Type ?u.131038
m' : o → Type ?u.131043
n' : o → Type ?u.131048
p' : o → Type ?u.131053
R : Type ?u.131056
S : Type ?u.131059
α : Type u_3
β : Type ?u.131065
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
i✝ : n × o
x✝ : m × o
⊢ (blockDiagonal M)ᵀ i✝ x✝ = blockDiagonal (fun k => (M k)ᵀ) i✝ x✝
l : Type ?u.131023
m : Type u_1
n : Type u_2
o : Type u_4
p : Type ?u.131035
q : Type ?u.131038
m' : o → Type ?u.131043
n' : o → Type ?u.131048
p' : o → Type ?u.131053
R : Type ?u.131056
S : Type ?u.131059
α : Type u_3
β : Type ?u.131065
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
⊢ (blockDiagonal M)ᵀ = blockDiagonal fun k => (M k)ᵀ
ext
case a.h
l : Type ?u.131023
m : Type u_1
n : Type u_2
o : Type u_4
p : Type ?u.131035
q : Type ?u.131038
m' : o → Type ?u.131043
n' : o → Type ?u.131048
p' : o → Type ?u.131053
R : Type ?u.131056
S : Type ?u.131059
α : Type u_3
β : Type ?u.131065
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
i✝ : n × o
x✝ : m × o
⊢ (if i✝.snd = x✝.snd then M i✝.snd x✝.fst i✝.fst else 0) = if i✝.snd = x✝.snd then M x✝.snd x✝.fst i✝.fst else 0
case a.h
l : Type ?u.131023
m : Type u_1
n : Type u_2
o : Type u_4
p : Type ?u.131035
q : Type ?u.131038
m' : o → Type ?u.131043
n' : o → Type ?u.131048
p' : o → Type ?u.131053
R : Type ?u.131056
S : Type ?u.131059
α : Type u_3
β : Type ?u.131065
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
i✝ : n × o
x✝ : m × o
⊢ (blockDiagonal M)ᵀ i✝ x✝ = blockDiagonal (fun k => (M k)ᵀ) i✝ x✝
simp only [transpose_apply, blockDiagonal_apply, eq_comm]
case a.h.inl
l : Type ?u.131023
m : Type u_1
n : Type u_2
o : Type u_4
p : Type ?u.131035
q : Type ?u.131038
m' : o → Type ?u.131043
n' : o → Type ?u.131048
p' : o → Type ?u.131053
R : Type ?u.131056
S : Type ?u.131059
α : Type u_3
β : Type ?u.131065
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
i✝ : n × o
x✝ : m × o
h : i✝.snd = x✝.snd
⊢ M i✝.snd x✝.fst i✝.fst = M x✝.snd x✝.fst i✝.fst

case a.h.inr
l : Type ?u.131023
m : Type u_1
n : Type u_2
o : Type u_4
p : Type ?u.131035
q : Type ?u.131038
m' : o → Type ?u.131043
n' : o → Type ?u.131048
p' : o → Type ?u.131053
R : Type ?u.131056
S : Type ?u.131059
α : Type u_3
β : Type ?u.131065
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
i✝ : n × o
x✝ : m × o
h : ¬i✝.snd = x✝.snd
⊢ 0 = 0
case a.h
l : Type ?u.131023
m : Type u_1
n : Type u_2
o : Type u_4
p : Type ?u.131035
q : Type ?u.131038
m' : o → Type ?u.131043
n' : o → Type ?u.131048
p' : o → Type ?u.131053
R : Type ?u.131056
S : Type ?u.131059
α : Type u_3
β : Type ?u.131065
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
i✝ : n × o
x✝ : m × o
⊢ (if i✝.snd = x✝.snd then M i✝.snd x✝.fst i✝.fst else 0) = if i✝.snd = x✝.snd then M x✝.snd x✝.fst i✝.fst else 0
split_ifs with h
no goals
case a.h.inl
l : Type ?u.131023
m : Type u_1
n : Type u_2
o : Type u_4
p : Type ?u.131035
q : Type ?u.131038
m' : o → Type ?u.131043
n' : o → Type ?u.131048
p' : o → Type ?u.131053
R : Type ?u.131056
S : Type ?u.131059
α : Type u_3
β : Type ?u.131065
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
i✝ : n × o
x✝ : m × o
h : i✝.snd = x✝.snd
⊢ M i✝.snd x✝.fst i✝.fst = M x✝.snd x✝.fst i✝.fst
rw [h]
no goals
case a.h.inr
l : Type ?u.131023
m : Type u_1
n : Type u_2
o : Type u_4
p : Type ?u.131035
q : Type ?u.131038
m' : o → Type ?u.131043
n' : o → Type ?u.131048
p' : o → Type ?u.131053
R : Type ?u.131056
S : Type ?u.131059
α : Type u_3
β : Type ?u.131065
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
i✝ : n × o
x✝ : m × o
h : ¬i✝.snd = x✝.snd
⊢ 0 = 0
rfl