case refine'_2
α : Type u_1
m n : ℕ
a b : α
v : Vector3 α n
i : Fin2 (succ n)
j✝ : Fin2 (succ (succ n))
j : Fin2 (n + 1)
⊢ (a :: b :: v)
      (match insertPerm i j with
      | fz => fz
      | fs k => fs (fs k)) =
    (a :: v) (insertPerm i j)
α : Type u_1
m n : ℕ
a b : α
v : Vector3 α n
i : Fin2 (succ n)
j : Fin2 (succ (succ n))
⊢ insert a (b :: v) (fs i) j = (b :: insert a v i) j
refine' j.cases' _ fun j => _ <;> simp [insert, insertPerm]
no goals
case refine'_2
α : Type u_1
m n : ℕ
a b : α
v : Vector3 α n
i : Fin2 (succ n)
j✝ : Fin2 (succ (succ n))
j : Fin2 (n + 1)
⊢ (a :: b :: v)
      (match insertPerm i j with
      | fz => fz
      | fs k => fs (fs k)) =
    (a :: v) (insertPerm i j)
refine' Fin2.cases' _ _ (insertPerm i j) <;> simp [insertPerm]