case a.h
l : Type ?u.51115
m : Type ?u.51118
n : Type u_1
o : Type ?u.51124
m' : o → Type ?u.51129
n' : o → Type ?u.51134
R : Type ?u.51137
S : Type ?u.51140
α : Type v
β : Type w
γ : Type ?u.51147
inst✝¹ : DecidableEq n
inst✝ : AddZeroClass α
d₁ d₂ : n → α
i j : n
⊢ (diagonal d₁ + diagonal d₂) i j = diagonal (fun i => d₁ i + d₂ i) i j
l : Type ?u.51115
m : Type ?u.51118
n : Type u_1
o : Type ?u.51124
m' : o → Type ?u.51129
n' : o → Type ?u.51134
R : Type ?u.51137
S : Type ?u.51140
α : Type v
β : Type w
γ : Type ?u.51147
inst✝¹ : DecidableEq n
inst✝ : AddZeroClass α
d₁ d₂ : n → α
⊢ diagonal d₁ + diagonal d₂ = diagonal fun i => d₁ i + d₂ i
ext i j
no goals
case a.h
l : Type ?u.51115
m : Type ?u.51118
n : Type u_1
o : Type ?u.51124
m' : o → Type ?u.51129
n' : o → Type ?u.51134
R : Type ?u.51137
S : Type ?u.51140
α : Type v
β : Type w
γ : Type ?u.51147
inst✝¹ : DecidableEq n
inst✝ : AddZeroClass α
d₁ d₂ : n → α
i j : n
⊢ (diagonal d₁ + diagonal d₂) i j = diagonal (fun i => d₁ i + d₂ i) i j
by_cases h : i = j <;>
simp [h]