no goals
l : Type ?u.82029
m : Type ?u.82032
n : Type u_1
o : Type ?u.82038
m' : o → Type ?u.82043
n' : o → Type ?u.82048
R : Type ?u.82051
S : Type ?u.82054
α : Type v
β : Type w
γ : Type ?u.82061
inst✝² : DecidableEq n
inst✝¹ : AddZeroClass α
inst✝ : One α
M : Matrix n n α
i : n
⊢ bit1 M i i = bit1 (M i i)
simp [bit1_apply]