no goals
n : ℕ
α : Type u_1
β : Type ?u.60181
γ : Type ?u.60184
v : Vector α n
i j : Fin n
a : α
⊢ get (set v i a) j = if i = j then a else get v j
split_ifs <;> try simp [*] <;> try rw [get_set_of_ne] ; assumption
no goals
case inr
n : ℕ
α : Type u_1
β : Type ?u.60181
γ : Type ?u.60184
v : Vector α n
i j : Fin n
a : α
h✝ : ¬i = j
⊢ get (set v i a) j = get v j
simp [*] <;> try rw [get_set_of_ne] ; assumption
case inr.h
n : ℕ
α : Type u_1
β : Type ?u.60181
γ : Type ?u.60184
v : Vector α n
i j : Fin n
a : α
h✝ : ¬i = j
⊢ i ≠ j
case inr
n : ℕ
α : Type u_1
β : Type ?u.60181
γ : Type ?u.60184
v : Vector α n
i j : Fin n
a : α
h✝ : ¬i = j
⊢ get (set v i a) j = get v j
rw [get_set_of_ne]
no goals
case inr.h
n : ℕ
α : Type u_1
β : Type ?u.60181
γ : Type ?u.60184
v : Vector α n
i j : Fin n
a : α
h✝ : ¬i = j
⊢ i ≠ j
assumption