[GOAL]
α : Type u_1
m n : ℕ
a : α
v : Vector3 α n
i : Fin2 (succ n)
⊢ α
[PROOFSTEP]
refine' i.cases' _ _
[GOAL]
case refine'_1
α : Type u_1
m n : ℕ
a : α
v : Vector3 α n
i : Fin2 (succ n)
⊢ α
case refine'_2 α : Type u_1 m n : ℕ a : α v : Vector3 α n i : Fin2 (succ n) ⊢ Fin2 n → α
[PROOFSTEP]
exact a
[GOAL]
case refine'_2
α : Type u_1
m n : ℕ
a : α
v : Vector3 α n
i : Fin2 (succ n)
⊢ Fin2 n → α
[PROOFSTEP]
exact v
[GOAL]
α : Type u_1
m n : ℕ
C : Vector3 α 0 → Sort u
H : C []
v : Vector3 α 0
⊢ C v
[PROOFSTEP]
rw [eq_nil v]
[GOAL]
α : Type u_1
m n : ℕ
C : Vector3 α 0 → Sort u
H : C []
v : Vector3 α 0
⊢ C []
[PROOFSTEP]
apply H
[GOAL]
α : Type u_1
m n : ℕ
C : Vector3 α (succ n) → Sort u
H : (a : α) → (t : Vector3 α n) → C (a :: t)
v : Vector3 α (succ n)
⊢ C v
[PROOFSTEP]
rw [← cons_head_tail v]
[GOAL]
α : Type u_1
m n : ℕ
C : Vector3 α (succ n) → Sort u
H : (a : α) → (t : Vector3 α n) → C (a :: t)
v : Vector3 α (succ n)
⊢ C (head v :: tail v)
[PROOFSTEP]
apply H
[GOAL]
α : Type u_1
m✝ n✝ m : ℕ
v : Vector3 α (succ m)
n : ℕ
w : Vector3 α n
a : α
_t : Vector3 α m
⊢ ((a :: _t) +-+ w) (left n fz) = (a :: _t) fz
[PROOFSTEP]
simp [*, left]
[GOAL]
α : Type u_1
m✝ n✝ m : ℕ
i : Fin2 m
v : Vector3 α (succ m)
n : ℕ
w : Vector3 α n
_a : α
t : Vector3 α m
⊢ ((_a :: t) +-+ w) (left n (fs i)) = (_a :: t) (fs i)
[PROOFSTEP]
simp [append_left, left]
[GOAL]
α : Type u_1
m✝ n✝ m : ℕ
v : Vector3 α (succ m)
n : ℕ
w : Vector3 α n
i : Fin2 n
_a : α
t : Vector3 α m
⊢ ((_a :: t) +-+ w) (add i (succ m)) = w i
[PROOFSTEP]
simp [append_add, add]
[GOAL]
α : Type u_1
m n : ℕ
a : α
v : Vector3 α n
⊢ insert a v fz = a :: v
[PROOFSTEP]
refine' funext fun j => j.cases' _ _
[GOAL]
case refine'_1
α : Type u_1
m n : ℕ
a : α
v : Vector3 α n
j : Fin2 (succ n)
⊢ insert a v fz fz = (a :: v) fz
[PROOFSTEP]
intros
[GOAL]
case refine'_2
α : Type u_1
m n : ℕ
a : α
v : Vector3 α n
j : Fin2 (succ n)
⊢ ∀ (n_1 : Fin2 n), insert a v fz (fs n_1) = (a :: v) (fs n_1)
[PROOFSTEP]
intros
[GOAL]
case refine'_1
α : Type u_1
m n : ℕ
a : α
v : Vector3 α n
j : Fin2 (succ n)
⊢ insert a v fz fz = (a :: v) fz
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
α : Type u_1
m n : ℕ
a : α
v : Vector3 α n
j : Fin2 (succ n)
n✝ : Fin2 n
⊢ insert a v fz (fs n✝) = (a :: v) (fs n✝)
[PROOFSTEP]
rfl
[GOAL]
α : 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
[PROOFSTEP]
refine' j.cases' _ fun j => _
[GOAL]
case refine'_1
α : 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) fz = (b :: insert a v i) fz
[PROOFSTEP]
simp [insert, insertPerm]
[GOAL]
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)
⊢ insert a (b :: v) (fs i) (fs j) = (b :: insert a v i) (fs j)
[PROOFSTEP]
simp [insert, insertPerm]
[GOAL]
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)
[PROOFSTEP]
refine' Fin2.cases' _ _ (insertPerm i j)
[GOAL]
case refine'_2.refine'_1
α : 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 fz with
      | fz => fz
      | fs k => fs (fs k)) =
    (a :: v) fz
[PROOFSTEP]
simp [insertPerm]
[GOAL]
case refine'_2.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)
⊢ ∀ (n_1 : Fin2 n),
    (a :: b :: v)
        (match fs n_1 with
        | fz => fz
        | fs k => fs (fs k)) =
      (a :: v) (fs n_1)
[PROOFSTEP]
simp [insertPerm]
[GOAL]
α : 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)
[PROOFSTEP]
refine' Vector3.recOn t (fun e => _) (@fun k b t IH _ => _) e
[GOAL]
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)
[PROOFSTEP]
rfl
[GOAL]
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)
[PROOFSTEP]
have e' := succ_add n k
[GOAL]
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)
[PROOFSTEP]
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)
[GOAL]
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)
[PROOFSTEP]
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)))]
[GOAL]
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)
[PROOFSTEP]
simp
[GOAL]
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
[PROOFSTEP]
rw [IH]
[GOAL]
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
[PROOFSTEP]
exact Eq.recOn e' rfl
[GOAL]
α : Type u_1
m n : ℕ
f : Vector3 α 0 → Prop
x✝ : Exists f
v : Vector3 α 0
fv : f v
⊢ f []
[PROOFSTEP]
rw [← eq_nil v]
[GOAL]
α : Type u_1
m n : ℕ
f : Vector3 α 0 → Prop
x✝ : Exists f
v : Vector3 α 0
fv : f v
⊢ f v
[PROOFSTEP]
exact fv
[GOAL]
α : Type u_1
m n : ℕ
f : Vector3 α (succ n) → Prop
x✝ : Exists f
v : Vector3 α (succ n)
fv : f v
⊢ f (?m.40396 f x✝ v fv :: ?m.40397 f x✝ v fv)
[PROOFSTEP]
rw [cons_head_tail v]
[GOAL]
α : Type u_1
m n : ℕ
f : Vector3 α (succ n) → Prop
x✝ : Exists f
v : Vector3 α (succ n)
fv : f v
⊢ f v
[PROOFSTEP]
exact fv
[GOAL]
α : Type u_1
m n : ℕ
p : α → Prop
v : Vector3 α n
⊢ VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
[PROOFSTEP]
refine' v.recOn _ _
[GOAL]
case refine'_1
α : Type u_1
m n : ℕ
p : α → Prop
v : Vector3 α n
⊢ VectorAllP p [] ↔ ∀ (i : Fin2 0), p []
[PROOFSTEP]
exact ⟨fun _ => Fin2.elim0, fun _ => trivial⟩
[GOAL]
case refine'_2
α : Type u_1
m n : ℕ
p : α → Prop
v : Vector3 α n
⊢ ∀ {n : ℕ} (a : α) (w : Vector3 α n),
    (VectorAllP p w ↔ ∀ (i : Fin2 n), p (w i)) → (VectorAllP p (a :: w) ↔ ∀ (i : Fin2 (succ n)), p ((a :: w) i))
[PROOFSTEP]
simp only [vectorAllP_cons]
[GOAL]
case refine'_2
α : Type u_1
m n : ℕ
p : α → Prop
v : Vector3 α n
⊢ ∀ {n : ℕ} (a : α) (w : Vector3 α n),
    (VectorAllP p w ↔ ∀ (i : Fin2 n), p (w i)) → (p a ∧ VectorAllP p w ↔ ∀ (i : Fin2 (succ n)), p ((a :: w) i))
[PROOFSTEP]
refine' fun {n} a v IH =>
  (and_congr_right fun _ => IH).trans
    ⟨fun ⟨pa, h⟩ i => by
      refine' i.cases' _ _
      exacts [pa, h], fun h => ⟨_, fun i => _⟩⟩
[GOAL]
α : Type u_1
m n✝ : ℕ
p : α → Prop
v✝ : Vector3 α n✝
n : ℕ
a : α
v : Vector3 α n
IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
x✝ : p a ∧ ∀ (i : Fin2 n), p (v i)
i : Fin2 (succ n)
pa : p a
h : ∀ (i : Fin2 n), p (v i)
⊢ p ((a :: v) i)
[PROOFSTEP]
refine' i.cases' _ _
[GOAL]
case refine'_1
α : Type u_1
m n✝ : ℕ
p : α → Prop
v✝ : Vector3 α n✝
n : ℕ
a : α
v : Vector3 α n
IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
x✝ : p a ∧ ∀ (i : Fin2 n), p (v i)
i : Fin2 (succ n)
pa : p a
h : ∀ (i : Fin2 n), p (v i)
⊢ p ((a :: v) fz)
case refine'_2
α : Type u_1
m n✝ : ℕ
p : α → Prop
v✝ : Vector3 α n✝
n : ℕ
a : α
v : Vector3 α n
IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
x✝ : p a ∧ ∀ (i : Fin2 n), p (v i)
i : Fin2 (succ n)
pa : p a
h : ∀ (i : Fin2 n), p (v i)
⊢ ∀ (n_1 : Fin2 n), p ((a :: v) (fs n_1))
[PROOFSTEP]
exacts [pa, h]
[GOAL]
case refine'_2.refine'_1
α : Type u_1
m n✝ : ℕ
p : α → Prop
v✝ : Vector3 α n✝
n : ℕ
a : α
v : Vector3 α n
IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
h : ∀ (i : Fin2 (succ n)), p ((a :: v) i)
⊢ p a
[PROOFSTEP]
simpa using h fz
[GOAL]
case refine'_2.refine'_2
α : Type u_1
m n✝ : ℕ
p : α → Prop
v✝ : Vector3 α n✝
n : ℕ
a : α
v : Vector3 α n
IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
h : ∀ (i : Fin2 (succ n)), p ((a :: v) i)
i : Fin2 n
⊢ p (v i)
[PROOFSTEP]
simpa using h (fs i)
