no goals
α : Type ?u.18045
a : Array α
i : Fin (size a)
j : Nat
hj : j < size a
v : α
⊢ j < size (set a i v)
simp [*]
no goals
α : Type u_1
a : Array α
i : Fin (size a)
j : Nat
hj : j < size a
v : α
⊢ (set a i v)[j] = if i.val = j then v else a[j]
if h : i.1 = j then subst j; simp [*] else simp [*]
α : Type u_1
a : Array α
i : Fin (size a)
v : α
hj : i.val < size a
⊢ (set a i v)[i.val] = if i.val = i.val then v else a[i.val]
α : Type u_1
a : Array α
i : Fin (size a)
j : Nat
hj : j < size a
v : α
h : i.val = j
⊢ (set a i v)[j] = if i.val = j then v else a[j]
subst j
no goals
α : Type u_1
a : Array α
i : Fin (size a)
v : α
hj : i.val < size a
⊢ (set a i v)[i.val] = if i.val = i.val then v else a[i.val]
simp [*]
no goals
α : Type u_1
a : Array α
i : Fin (size a)
j : Nat
hj : j < size a
v : α
h : ¬i.val = j
⊢ (set a i v)[j] = if i.val = j then v else a[j]
simp [*]