case refine'_1
α : Type u_1
m n : ℕ
a : α
t : Vector3 α m
v : Vector3 α n
i : Fin2 (succ n)
e✝ : succ n + m = succ (n + m)
e : succ n + 0 = succ (n + 0)
⊢ insert a ([] +-+ v) (Eq.recOn e (add i 0)) = Eq.recOn e ([] +-+ insert a v i)

case refine'_2
α : Type u_1
m n : ℕ
a : α
t✝ : Vector3 α m
v : Vector3 α n
i : Fin2 (succ n)
e : succ n + m = succ (n + m)
k : ℕ
b : α
t : Vector3 α k
IH : ∀ (x : succ n + k = succ (n + k)), insert a (t +-+ v) (Eq.recOn x (add i k)) = Eq.recOn x (t +-+ insert a v i)
x✝ : succ n + succ k = succ (n + succ k)
⊢ insert a ((b :: t) +-+ v) (Eq.recOn x✝ (add i (succ k))) = Eq.recOn x✝ ((b :: t) +-+ insert a v i)
α : Type u_1
m n : ℕ
a : α
t : Vector3 α m
v : Vector3 α n
i : Fin2 (succ n)
e : succ n + m = succ (n + m)
⊢ insert a (t +-+ v) (Eq.recOn e (add i m)) = Eq.recOn e (t +-+ insert a v i)
refine' Vector3.recOn t (fun e => _) (@fun k b t IH _ => _) e
case refine'_2
α : Type u_1
m n : ℕ
a : α
t✝ : Vector3 α m
v : Vector3 α n
i : Fin2 (succ n)
e : succ n + m = succ (n + m)
k : ℕ
b : α
t : Vector3 α k
IH : ∀ (x : succ n + k = succ (n + k)), insert a (t +-+ v) (Eq.recOn x (add i k)) = Eq.recOn x (t +-+ insert a v i)
x✝ : succ n + succ k = succ (n + succ k)
⊢ insert a ((b :: t) +-+ v) (Eq.recOn x✝ (add i (succ k))) = Eq.recOn x✝ ((b :: t) +-+ insert a v i)
case refine'_1
α : Type u_1
m n : ℕ
a : α
t : Vector3 α m
v : Vector3 α n
i : Fin2 (succ n)
e✝ : succ n + m = succ (n + m)
e : succ n + 0 = succ (n + 0)
⊢ insert a ([] +-+ v) (Eq.recOn e (add i 0)) = Eq.recOn e ([] +-+ insert a v i)

case refine'_2
α : Type u_1
m n : ℕ
a : α
t✝ : Vector3 α m
v : Vector3 α n
i : Fin2 (succ n)
e : succ n + m = succ (n + m)
k : ℕ
b : α
t : Vector3 α k
IH : ∀ (x : succ n + k = succ (n + k)), insert a (t +-+ v) (Eq.recOn x (add i k)) = Eq.recOn x (t +-+ insert a v i)
x✝ : succ n + succ k = succ (n + succ k)
⊢ insert a ((b :: t) +-+ v) (Eq.recOn x✝ (add i (succ k))) = Eq.recOn x✝ ((b :: t) +-+ insert a v i)
rfl
case refine'_2
α : Type u_1
m n : ℕ
a : α
t✝ : Vector3 α m
v : Vector3 α n
i : Fin2 (succ n)
e : succ n + m = succ (n + m)
k : ℕ
b : α
t : Vector3 α k
IH : ∀ (x : succ n + k = succ (n + k)), insert a (t +-+ v) (Eq.recOn x (add i k)) = Eq.recOn x (t +-+ insert a v i)
x✝ : succ n + succ k = succ (n + succ k)
e' : succ n + k = succ (n + k)
⊢ insert a ((b :: t) +-+ v) (Eq.recOn x✝ (add i (succ k))) = Eq.recOn x✝ ((b :: t) +-+ insert a v i)
case refine'_2
α : Type u_1
m n : ℕ
a : α
t✝ : Vector3 α m
v : Vector3 α n
i : Fin2 (succ n)
e : succ n + m = succ (n + m)
k : ℕ
b : α
t : Vector3 α k
IH : ∀ (x : succ n + k = succ (n + k)), insert a (t +-+ v) (Eq.recOn x (add i k)) = Eq.recOn x (t +-+ insert a v i)
x✝ : succ n + succ k = succ (n + succ k)
⊢ insert a ((b :: t) +-+ v) (Eq.recOn x✝ (add i (succ k))) = Eq.recOn x✝ ((b :: t) +-+ insert a v i)
have e' := succ_add n k
case refine'_2
α : Type u_1
m n : ℕ
a : α
t✝ : Vector3 α m
v : Vector3 α n
i : Fin2 (succ n)
e : succ n + m = succ (n + m)
k : ℕ
b : α
t : Vector3 α k
IH : ∀ (x : succ n + k = succ (n + k)), insert a (t +-+ v) (Eq.recOn x (add i k)) = Eq.recOn x (t +-+ insert a v i)
x✝ : succ n + succ k = succ (n + succ k)
e' : succ n + k = succ (n + k)
⊢ insert a (b :: t +-+ v) (Eq.recOn (_ : succ (succ n + k) = succ (succ (n + k))) (fs (add i k))) =
    Eq.recOn (_ : succ (succ n + k) = succ (succ (n + k))) (b :: t +-+ insert a v i)
case refine'_2
α : Type u_1
m n : ℕ
a : α
t✝ : Vector3 α m
v : Vector3 α n
i : Fin2 (succ n)
e : succ n + m = succ (n + m)
k : ℕ
b : α
t : Vector3 α k
IH : ∀ (x : succ n + k = succ (n + k)), insert a (t +-+ v) (Eq.recOn x (add i k)) = Eq.recOn x (t +-+ insert a v i)
x✝ : succ n + succ k = succ (n + succ k)
e' : succ n + k = succ (n + k)
⊢ insert a ((b :: t) +-+ v) (Eq.recOn x✝ (add i (succ k))) = Eq.recOn x✝ ((b :: t) +-+ insert a v i)
change
  insert a (b :: t +-+ v) (Eq.recOn (congr_arg succ e') (fs (add i k))) =
    Eq.recOn (congr_arg succ e') (b :: t +-+ insert a v i)
case refine'_2
α : Type u_1
m n : ℕ
a : α
t✝ : Vector3 α m
v : Vector3 α n
i : Fin2 (succ n)
e : succ n + m = succ (n + m)
k : ℕ
b : α
t : Vector3 α k
IH : ∀ (x : succ n + k = succ (n + k)), insert a (t +-+ v) (Eq.recOn x (add i k)) = Eq.recOn x (t +-+ insert a v i)
x✝ : succ n + succ k = succ (n + succ k)
e' : succ n + k = succ (n + k)
⊢ insert a (b :: t +-+ v) (fs (Eq.recOn e' (add i k))) =
    Eq.recOn (_ : succ (succ n + k) = succ (succ (n + k))) (b :: t +-+ insert a v i)
case refine'_2
α : Type u_1
m n : ℕ
a : α
t✝ : Vector3 α m
v : Vector3 α n
i : Fin2 (succ n)
e : succ n + m = succ (n + m)
k : ℕ
b : α
t : Vector3 α k
IH : ∀ (x : succ n + k = succ (n + k)), insert a (t +-+ v) (Eq.recOn x (add i k)) = Eq.recOn x (t +-+ insert a v i)
x✝ : succ n + succ k = succ (n + succ k)
e' : succ n + k = succ (n + k)
⊢ insert a (b :: t +-+ v) (Eq.recOn (_ : succ (succ n + k) = succ (succ (n + k))) (fs (add i k))) =
    Eq.recOn (_ : succ (succ n + k) = succ (succ (n + k))) (b :: t +-+ insert a v i)
rw [←
  (Eq.recOn e' rfl :
    fs (Eq.recOn e' (i.add k) : Fin2 (succ (n + k))) =
      Eq.recOn (congr_arg succ e') (fs (i.add k)))]
case refine'_2
α : Type u_1
m n : ℕ
a : α
t✝ : Vector3 α m
v : Vector3 α n
i : Fin2 (succ n)
e : succ n + m = succ (n + m)
k : ℕ
b : α
t : Vector3 α k
IH : ∀ (x : succ n + k = succ (n + k)), insert a (t +-+ v) (Eq.recOn x (add i k)) = Eq.recOn x (t +-+ insert a v i)
x✝ : succ n + succ k = succ (n + succ k)
e' : succ n + k = succ (n + k)
⊢ (b :: insert a (t +-+ v) (e' ▸ add i k)) = (_ : succ (succ n + k) = succ (succ (n + k))) ▸ b :: t +-+ insert a v i
case refine'_2
α : Type u_1
m n : ℕ
a : α
t✝ : Vector3 α m
v : Vector3 α n
i : Fin2 (succ n)
e : succ n + m = succ (n + m)
k : ℕ
b : α
t : Vector3 α k
IH : ∀ (x : succ n + k = succ (n + k)), insert a (t +-+ v) (Eq.recOn x (add i k)) = Eq.recOn x (t +-+ insert a v i)
x✝ : succ n + succ k = succ (n + succ k)
e' : succ n + k = succ (n + k)
⊢ insert a (b :: t +-+ v) (fs (Eq.recOn e' (add i k))) =
    Eq.recOn (_ : succ (succ n + k) = succ (succ (n + k))) (b :: t +-+ insert a v i)
simp
case refine'_2
α : Type u_1
m n : ℕ
a : α
t✝ : Vector3 α m
v : Vector3 α n
i : Fin2 (succ n)
e : succ n + m = succ (n + m)
k : ℕ
b : α
t : Vector3 α k
IH : ∀ (x : succ n + k = succ (n + k)), insert a (t +-+ v) (Eq.recOn x (add i k)) = Eq.recOn x (t +-+ insert a v i)
x✝ : succ n + succ k = succ (n + succ k)
e' : succ n + k = succ (n + k)
⊢ (b :: Eq.recOn e' (t +-+ insert a v i)) = (_ : succ (succ n + k) = succ (succ (n + k))) ▸ b :: t +-+ insert a v i
case refine'_2
α : Type u_1
m n : ℕ
a : α
t✝ : Vector3 α m
v : Vector3 α n
i : Fin2 (succ n)
e : succ n + m = succ (n + m)
k : ℕ
b : α
t : Vector3 α k
IH : ∀ (x : succ n + k = succ (n + k)), insert a (t +-+ v) (Eq.recOn x (add i k)) = Eq.recOn x (t +-+ insert a v i)
x✝ : succ n + succ k = succ (n + succ k)
e' : succ n + k = succ (n + k)
⊢ (b :: insert a (t +-+ v) (e' ▸ add i k)) = (_ : succ (succ n + k) = succ (succ (n + k))) ▸ b :: t +-+ insert a v i
rw [IH]
no goals
case refine'_2
α : Type u_1
m n : ℕ
a : α
t✝ : Vector3 α m
v : Vector3 α n
i : Fin2 (succ n)
e : succ n + m = succ (n + m)
k : ℕ
b : α
t : Vector3 α k
IH : ∀ (x : succ n + k = succ (n + k)), insert a (t +-+ v) (Eq.recOn x (add i k)) = Eq.recOn x (t +-+ insert a v i)
x✝ : succ n + succ k = succ (n + succ k)
e' : succ n + k = succ (n + k)
⊢ (b :: Eq.recOn e' (t +-+ insert a v i)) = (_ : succ (succ n + k) = succ (succ (n + k))) ▸ b :: t +-+ insert a v i
exact Eq.recOn e' rfl