case a.h
l : Type ?u.49070
m : Type ?u.49073
n : Type u_1
o : Type ?u.49079
m' : o → Type ?u.49084
n' : o → Type ?u.49089
R : Type ?u.49092
S : Type ?u.49095
α : Type v
β : Type w
γ : Type ?u.49102
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i j : n
⊢ (diagonal v)ᵀ i j = diagonal v i j
l : Type ?u.49070
m : Type ?u.49073
n : Type u_1
o : Type ?u.49079
m' : o → Type ?u.49084
n' : o → Type ?u.49089
R : Type ?u.49092
S : Type ?u.49095
α : Type v
β : Type w
γ : Type ?u.49102
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
⊢ (diagonal v)ᵀ = diagonal v
ext i j
case pos
l : Type ?u.49070
m : Type ?u.49073
n : Type u_1
o : Type ?u.49079
m' : o → Type ?u.49084
n' : o → Type ?u.49089
R : Type ?u.49092
S : Type ?u.49095
α : Type v
β : Type w
γ : Type ?u.49102
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i j : n
h : i = j
⊢ (diagonal v)ᵀ i j = diagonal v i j

case neg
l : Type ?u.49070
m : Type ?u.49073
n : Type u_1
o : Type ?u.49079
m' : o → Type ?u.49084
n' : o → Type ?u.49089
R : Type ?u.49092
S : Type ?u.49095
α : Type v
β : Type w
γ : Type ?u.49102
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i j : n
h : ¬i = j
⊢ (diagonal v)ᵀ i j = diagonal v i j
case a.h
l : Type ?u.49070
m : Type ?u.49073
n : Type u_1
o : Type ?u.49079
m' : o → Type ?u.49084
n' : o → Type ?u.49089
R : Type ?u.49092
S : Type ?u.49095
α : Type v
β : Type w
γ : Type ?u.49102
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i j : n
⊢ (diagonal v)ᵀ i j = diagonal v i j
by_cases h : i = j
no goals
case pos
l : Type ?u.49070
m : Type ?u.49073
n : Type u_1
o : Type ?u.49079
m' : o → Type ?u.49084
n' : o → Type ?u.49089
R : Type ?u.49092
S : Type ?u.49095
α : Type v
β : Type w
γ : Type ?u.49102
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i j : n
h : i = j
⊢ (diagonal v)ᵀ i j = diagonal v i j
simp [h, transpose]
no goals
case neg
l : Type ?u.49070
m : Type ?u.49073
n : Type u_1
o : Type ?u.49079
m' : o → Type ?u.49084
n' : o → Type ?u.49089
R : Type ?u.49092
S : Type ?u.49095
α : Type v
β : Type w
γ : Type ?u.49102
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i j : n
h : ¬i = j
⊢ (diagonal v)ᵀ i j = diagonal v i j
simp [h, transpose, diagonal_apply_ne' _ h]