[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
x : α
u : Fin m → α
i : Fin m
⊢ vecCons x u (Fin.succ i) = u i
[PROOFSTEP]
simp [vecCons]
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
i : ℕ
h : Nat.succ i < Nat.succ m
x : α
u : Fin m → α
⊢ vecCons x u { val := Nat.succ i, isLt := h } = u { val := i, isLt := (_ : i < m) }
[PROOFSTEP]
simp only [vecCons, Fin.cons, Fin.cases_succ']
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
x : α
u : Fin m → α
⊢ vecTail (vecCons x u) = u
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
x : α
u : Fin m → α
x✝ : Fin m
⊢ vecTail (vecCons x u) x✝ = u x✝
[PROOFSTEP]
simp [vecTail]
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
x : α
u : Fin n → α
y : α
⊢ y ∈ Set.range (vecCons x u) ↔ y ∈ {x} ∪ Set.range u
[PROOFSTEP]
simp [Fin.exists_fin_succ, eq_comm]
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
x : α
u : Fin 0 → α
⊢ Set.range (vecCons x u) = {x}
[PROOFSTEP]
rw [range_cons, range_empty, Set.union_empty]
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
x y : α
u : Fin 0 → α
⊢ Set.range (vecCons x (vecCons y u)) = {x, y}
[PROOFSTEP]
rw [range_cons, range_cons_empty, Set.singleton_union]
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
x : α
u : Fin 0 → α
⊢ ∀ (i : Fin 1), vecCons x u i = x
[PROOFSTEP]
rw [Fin.forall_fin_one]
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
x : α
u : Fin 0 → α
⊢ vecCons x u 0 = x
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u
m n o✝ : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
α : Type u_4
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
⊢ vecAppend ho u v = fun i =>
    if h : ↑i < m then u { val := ↑i, isLt := h } else v { val := ↑i - m, isLt := (_ : ↑i - m < n) }
[PROOFSTEP]
ext i
[GOAL]
case h
α✝ : Type u
m n o✝ : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
α : Type u_4
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
⊢ vecAppend ho u v i = if h : ↑i < m then u { val := ↑i, isLt := h } else v { val := ↑i - m, isLt := (_ : ↑i - m < n) }
[PROOFSTEP]
rw [vecAppend, Fin.append, Function.comp_apply, Fin.addCases]
[GOAL]
case h
α✝ : Type u
m n o✝ : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
α : Type u_4
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
⊢ (if hi : ↑(↑(Fin.castIso ho) i) < m then
      (_ : Fin.castAdd n (Fin.castLT (↑(Fin.castIso ho) i) hi) = ↑(Fin.castIso ho) i) ▸
        u (Fin.castLT (↑(Fin.castIso ho) i) hi)
    else
      (_ :
          Fin.natAdd m
              (Fin.subNat m (Fin.cast (_ : m + n = n + m) (↑(Fin.castIso ho) i)) (_ : m ≤ ↑(↑(Fin.castIso ho) i))) =
            ↑(Fin.castIso ho) i) ▸
        v (Fin.subNat m (Fin.cast (_ : m + n = n + m) (↑(Fin.castIso ho) i)) (_ : m ≤ ↑(↑(Fin.castIso ho) i)))) =
    if h : ↑i < m then u { val := ↑i, isLt := h } else v { val := ↑i - m, isLt := (_ : ↑i - m < n) }
[PROOFSTEP]
congr with hi
[GOAL]
case h.e_e.h
α✝ : Type u
m n o✝ : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
α : Type u_4
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
hi : ¬↑(↑(Fin.castIso ho) i) < m
⊢ (_ :
        Fin.natAdd m
            (Fin.subNat m (Fin.cast (_ : m + n = n + m) (↑(Fin.castIso ho) i)) (_ : m ≤ ↑(↑(Fin.castIso ho) i))) =
          ↑(Fin.castIso ho) i) ▸
      v (Fin.subNat m (Fin.cast (_ : m + n = n + m) (↑(Fin.castIso ho) i)) (_ : m ≤ ↑(↑(Fin.castIso ho) i))) =
    v { val := ↑i - m, isLt := (_ : ↑i - m < n) }
[PROOFSTEP]
simp only [eq_rec_constant]
[GOAL]
case h.e_e.h
α✝ : Type u
m n o✝ : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
α : Type u_4
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
hi : ¬↑(↑(Fin.castIso ho) i) < m
⊢ v (Fin.subNat m (Fin.cast (_ : m + n = n + m) (↑(Fin.castIso ho) i)) (_ : m ≤ ↑(↑(Fin.castIso ho) i))) =
    v { val := ↑i - m, isLt := (_ : ↑i - m < n) }
[PROOFSTEP]
rfl
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin n → α
⊢ vecAppend (_ : n = 0 + n) ![] v = v
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin n → α
x✝ : Fin n
⊢ vecAppend (_ : n = 0 + n) ![] v x✝ = v x✝
[PROOFSTEP]
simp [vecAppend_eq_ite]
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
⊢ o = m + n
[PROOFSTEP]
rwa [add_assoc, add_comm 1, ← add_assoc, add_right_cancel_iff] at ho 
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
⊢ vecAppend ho (vecCons x u) v = vecCons x (vecAppend (_ : o = m + n) u v)
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : Fin (o + 1)
⊢ vecAppend ho (vecCons x u) v i = vecCons x (vecAppend (_ : o = m + n) u v) i
[PROOFSTEP]
simp_rw [vecAppend_eq_ite]
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : Fin (o + 1)
⊢ (if h : ↑i < m + 1 then vecCons x u { val := ↑i, isLt := h }
    else v { val := ↑i - (m + 1), isLt := (_ : ↑i - (m + 1) < n) }) =
    vecCons x
      (fun i => if h : ↑i < m then u { val := ↑i, isLt := h } else v { val := ↑i - m, isLt := (_ : ↑i - m < n) }) i
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : Fin (o + 1)
h : ↑i < m + 1
⊢ vecCons x u { val := ↑i, isLt := h } =
    vecCons x
      (fun i => if h : ↑i < m then u { val := ↑i, isLt := h } else v { val := ↑i - m, isLt := (_ : ↑i - m < n) }) i
[PROOFSTEP]
rcases i with ⟨⟨⟩ | i, hi⟩
[GOAL]
case pos.mk.zero
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
hi : Nat.zero < o + 1
h : ↑{ val := Nat.zero, isLt := hi } < m + 1
⊢ vecCons x u { val := ↑{ val := Nat.zero, isLt := hi }, isLt := h } =
    vecCons x
      (fun i => if h : ↑i < m then u { val := ↑i, isLt := h } else v { val := ↑i - m, isLt := (_ : ↑i - m < n) })
      { val := Nat.zero, isLt := hi }
[PROOFSTEP]
simp
[GOAL]
case pos.mk.succ
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : ℕ
hi : Nat.succ i < o + 1
h : ↑{ val := Nat.succ i, isLt := hi } < m + 1
⊢ vecCons x u { val := ↑{ val := Nat.succ i, isLt := hi }, isLt := h } =
    vecCons x
      (fun i => if h : ↑i < m then u { val := ↑i, isLt := h } else v { val := ↑i - m, isLt := (_ : ↑i - m < n) })
      { val := Nat.succ i, isLt := hi }
[PROOFSTEP]
simp only [Nat.succ_eq_add_one, add_lt_add_iff_right, Fin.val_mk] at h 
[GOAL]
case pos.mk.succ
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : ℕ
hi : Nat.succ i < o + 1
h✝ : ↑{ val := Nat.succ i, isLt := hi } < m + 1
h : i < m
⊢ vecCons x u { val := ↑{ val := Nat.succ i, isLt := hi }, isLt := h✝ } =
    vecCons x
      (fun i => if h : ↑i < m then u { val := ↑i, isLt := h } else v { val := ↑i - m, isLt := (_ : ↑i - m < n) })
      { val := Nat.succ i, isLt := hi }
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : Fin (o + 1)
h : ¬↑i < m + 1
⊢ v { val := ↑i - (m + 1), isLt := (_ : ↑i - (m + 1) < n) } =
    vecCons x
      (fun i => if h : ↑i < m then u { val := ↑i, isLt := h } else v { val := ↑i - m, isLt := (_ : ↑i - m < n) }) i
[PROOFSTEP]
rcases i with ⟨⟨⟩ | i, hi⟩
[GOAL]
case neg.mk.zero
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
hi : Nat.zero < o + 1
h : ¬↑{ val := Nat.zero, isLt := hi } < m + 1
⊢ v
      { val := ↑{ val := Nat.zero, isLt := hi } - (m + 1),
        isLt := (_ : ↑{ val := Nat.zero, isLt := hi } - (m + 1) < n) } =
    vecCons x
      (fun i => if h : ↑i < m then u { val := ↑i, isLt := h } else v { val := ↑i - m, isLt := (_ : ↑i - m < n) })
      { val := Nat.zero, isLt := hi }
[PROOFSTEP]
simp at h 
[GOAL]
case neg.mk.succ
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : ℕ
hi : Nat.succ i < o + 1
h : ¬↑{ val := Nat.succ i, isLt := hi } < m + 1
⊢ v
      { val := ↑{ val := Nat.succ i, isLt := hi } - (m + 1),
        isLt := (_ : ↑{ val := Nat.succ i, isLt := hi } - (m + 1) < n) } =
    vecCons x
      (fun i => if h : ↑i < m then u { val := ↑i, isLt := h } else v { val := ↑i - m, isLt := (_ : ↑i - m < n) })
      { val := Nat.succ i, isLt := hi }
[PROOFSTEP]
rw [not_lt, Fin.val_mk, Nat.succ_eq_add_one, add_le_add_iff_right] at h 
[GOAL]
case neg.mk.succ
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : ℕ
hi : Nat.succ i < o + 1
h✝ : ¬↑{ val := Nat.succ i, isLt := hi } < m + 1
h : m ≤ i
⊢ v
      { val := ↑{ val := Nat.succ i, isLt := hi } - (m + 1),
        isLt := (_ : ↑{ val := Nat.succ i, isLt := hi } - (m + 1) < n) } =
    vecCons x
      (fun i => if h : ↑i < m then u { val := ↑i, isLt := h } else v { val := ↑i - m, isLt := (_ : ↑i - m < n) })
      { val := Nat.succ i, isLt := hi }
[PROOFSTEP]
simp [h, not_lt.2 h]
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin n → α
⊢ vecAlt0 (_ : n + n = n + n) (vecAppend (_ : n + n = n + n) v v) = v ∘ bit0
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin n → α
i : Fin n
⊢ vecAlt0 (_ : n + n = n + n) (vecAppend (_ : n + n = n + n) v v) i = (v ∘ bit0) i
[PROOFSTEP]
simp_rw [Function.comp, bit0, vecAlt0, vecAppend_eq_ite]
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin n → α
i : Fin n
⊢ (if h : ↑i + ↑i < n then v { val := ↑i + ↑i, isLt := (_ : ↑{ val := ↑i + ↑i, isLt := (_ : ↑i + ↑i < n + n) } < n) }
    else v { val := ↑i + ↑i - n, isLt := (_ : ↑{ val := ↑i + ↑i, isLt := (_ : ↑i + ↑i < n + n) } - n < n) }) =
    v (i + i)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin n → α
i : Fin n
h : ↑i + ↑i < n
⊢ v { val := ↑i + ↑i, isLt := (_ : ↑{ val := ↑i + ↑i, isLt := (_ : ↑i + ↑i < n + n) } < n) } = v (i + i)
[PROOFSTEP]
congr
[GOAL]
case neg
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin n → α
i : Fin n
h : ¬↑i + ↑i < n
⊢ v { val := ↑i + ↑i - n, isLt := (_ : ↑{ val := ↑i + ↑i, isLt := (_ : ↑i + ↑i < n + n) } - n < n) } = v (i + i)
[PROOFSTEP]
congr
[GOAL]
case pos.e_a.e_val
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin n → α
i : Fin n
h : ↑i + ↑i < n
⊢ ↑i + ↑i = (↑i + ↑i) % n
[PROOFSTEP]
rw [Fin.val_mk] at h 
[GOAL]
case pos.e_a.e_val
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin n → α
i : Fin n
h : ↑i + ↑i < n
⊢ ↑i + ↑i = (↑i + ↑i) % n
[PROOFSTEP]
exact (Nat.mod_eq_of_lt h).symm
[GOAL]
case neg.e_a.e_val
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin n → α
i : Fin n
h : ¬↑i + ↑i < n
⊢ ↑i + ↑i - n = (↑i + ↑i) % n
[PROOFSTEP]
rw [Fin.val_mk, not_lt] at h 
[GOAL]
case neg.e_a.e_val
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin n → α
i : Fin n
h : n ≤ ↑i + ↑i
⊢ ↑i + ↑i - n = (↑i + ↑i) % n
[PROOFSTEP]
simp only [Fin.ext_iff, Fin.val_add, Fin.val_mk, Nat.mod_eq_sub_mod h]
[GOAL]
case neg.e_a.e_val
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin n → α
i : Fin n
h : n ≤ ↑i + ↑i
⊢ ↑i + ↑i - n = (↑i + ↑i - n) % n
[PROOFSTEP]
refine' (Nat.mod_eq_of_lt _).symm
[GOAL]
case neg.e_a.e_val
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin n → α
i : Fin n
h : n ≤ ↑i + ↑i
⊢ ↑i + ↑i - n < n
[PROOFSTEP]
rw [tsub_lt_iff_left h]
[GOAL]
case neg.e_a.e_val
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin n → α
i : Fin n
h : n ≤ ↑i + ↑i
⊢ ↑i + ↑i < n + n
[PROOFSTEP]
exact add_lt_add i.2 i.2
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin (n + 1) → α
⊢ vecAlt1 (_ : n + 1 + (n + 1) = n + 1 + (n + 1)) (vecAppend (_ : n + 1 + (n + 1) = n + 1 + (n + 1)) v v) = v ∘ bit1
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ vecAlt1 (_ : n + 1 + (n + 1) = n + 1 + (n + 1)) (vecAppend (_ : n + 1 + (n + 1) = n + 1 + (n + 1)) v v) i =
    (v ∘ bit1) i
[PROOFSTEP]
simp_rw [Function.comp, vecAlt1, vecAppend_eq_ite]
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ (if h : ↑i + ↑i + 1 < n + 1 then
      v
        { val := ↑i + ↑i + 1,
          isLt := (_ : ↑{ val := ↑i + ↑i + 1, isLt := (_ : ↑i + ↑i + 1 < n + 1 + (n + 1)) } < n + 1) }
    else
      v
        { val := ↑i + ↑i + 1 - (n + 1),
          isLt := (_ : ↑{ val := ↑i + ↑i + 1, isLt := (_ : ↑i + ↑i + 1 < n + 1 + (n + 1)) } - (n + 1) < n + 1) }) =
    v (bit1 i)
[PROOFSTEP]
cases n with
| zero =>
  cases' i with i hi
  simp only [Nat.zero_eq, zero_add, Nat.lt_one_iff] at hi ; subst i; rfl
| succ n =>
  split_ifs with h <;> simp_rw [bit1, bit0] <;> congr
  · rw [Fin.val_mk] at h 
    rw [Nat.mod_eq_of_lt (Nat.lt_of_succ_lt h)]
    erw [Nat.mod_eq_of_lt h]
  · rw [Fin.val_mk, not_lt] at h 
    simp only [Fin.ext_iff, Fin.val_add, Fin.val_mk, Nat.mod_add_mod, Fin.val_one, Nat.mod_eq_sub_mod h,
      show 1 % (n + 2) = 1 from Nat.mod_eq_of_lt (by simp)]
    refine (Nat.mod_eq_of_lt ?_).symm
    rw [tsub_lt_iff_left h]
    exact Nat.add_succ_lt_add i.2 i.2
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ (if h : ↑i + ↑i + 1 < n + 1 then
      v
        { val := ↑i + ↑i + 1,
          isLt := (_ : ↑{ val := ↑i + ↑i + 1, isLt := (_ : ↑i + ↑i + 1 < n + 1 + (n + 1)) } < n + 1) }
    else
      v
        { val := ↑i + ↑i + 1 - (n + 1),
          isLt := (_ : ↑{ val := ↑i + ↑i + 1, isLt := (_ : ↑i + ↑i + 1 < n + 1 + (n + 1)) } - (n + 1) < n + 1) }) =
    v (bit1 i)
[PROOFSTEP]
cases n with
| zero =>
  cases' i with i hi
  simp only [Nat.zero_eq, zero_add, Nat.lt_one_iff] at hi ; subst i; rfl
| succ n =>
  split_ifs with h <;> simp_rw [bit1, bit0] <;> congr
  · rw [Fin.val_mk] at h 
    rw [Nat.mod_eq_of_lt (Nat.lt_of_succ_lt h)]
    erw [Nat.mod_eq_of_lt h]
  · rw [Fin.val_mk, not_lt] at h 
    simp only [Fin.ext_iff, Fin.val_add, Fin.val_mk, Nat.mod_add_mod, Fin.val_one, Nat.mod_eq_sub_mod h,
      show 1 % (n + 2) = 1 from Nat.mod_eq_of_lt (by simp)]
    refine (Nat.mod_eq_of_lt ?_).symm
    rw [tsub_lt_iff_left h]
    exact Nat.add_succ_lt_add i.2 i.2
[GOAL]
case h.zero
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin (Nat.zero + 1) → α
i : Fin (Nat.zero + 1)
⊢ (if h : ↑i + ↑i + 1 < Nat.zero + 1 then
      v
        { val := ↑i + ↑i + 1,
          isLt :=
            (_ : ↑{ val := ↑i + ↑i + 1, isLt := (_ : ↑i + ↑i + 1 < Nat.zero + 1 + (Nat.zero + 1)) } < Nat.zero + 1) }
    else
      v
        { val := ↑i + ↑i + 1 - (Nat.zero + 1),
          isLt :=
            (_ :
              ↑{ val := ↑i + ↑i + 1, isLt := (_ : ↑i + ↑i + 1 < Nat.zero + 1 + (Nat.zero + 1)) } - (Nat.zero + 1) <
                Nat.zero + 1) }) =
    v (bit1 i)
[PROOFSTEP]

| zero =>
  cases' i with i hi
  simp only [Nat.zero_eq, zero_add, Nat.lt_one_iff] at hi ; subst i; rfl
[GOAL]
case h.zero
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin (Nat.zero + 1) → α
i : Fin (Nat.zero + 1)
⊢ (if h : ↑i + ↑i + 1 < Nat.zero + 1 then
      v
        { val := ↑i + ↑i + 1,
          isLt :=
            (_ : ↑{ val := ↑i + ↑i + 1, isLt := (_ : ↑i + ↑i + 1 < Nat.zero + 1 + (Nat.zero + 1)) } < Nat.zero + 1) }
    else
      v
        { val := ↑i + ↑i + 1 - (Nat.zero + 1),
          isLt :=
            (_ :
              ↑{ val := ↑i + ↑i + 1, isLt := (_ : ↑i + ↑i + 1 < Nat.zero + 1 + (Nat.zero + 1)) } - (Nat.zero + 1) <
                Nat.zero + 1) }) =
    v (bit1 i)
[PROOFSTEP]
cases' i with i hi
[GOAL]
case h.zero.mk
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin (Nat.zero + 1) → α
i : ℕ
hi : i < Nat.zero + 1
⊢ (if h : ↑{ val := i, isLt := hi } + ↑{ val := i, isLt := hi } + 1 < Nat.zero + 1 then
      v
        { val := ↑{ val := i, isLt := hi } + ↑{ val := i, isLt := hi } + 1,
          isLt :=
            (_ :
              ↑{ val := ↑{ val := i, isLt := hi } + ↑{ val := i, isLt := hi } + 1,
                    isLt :=
                      (_ :
                        ↑{ val := i, isLt := hi } + ↑{ val := i, isLt := hi } + 1 < Nat.zero + 1 + (Nat.zero + 1)) } <
                Nat.zero + 1) }
    else
      v
        { val := ↑{ val := i, isLt := hi } + ↑{ val := i, isLt := hi } + 1 - (Nat.zero + 1),
          isLt :=
            (_ :
              ↑{ val := ↑{ val := i, isLt := hi } + ↑{ val := i, isLt := hi } + 1,
                      isLt :=
                        (_ :
                          ↑{ val := i, isLt := hi } + ↑{ val := i, isLt := hi } + 1 < Nat.zero + 1 + (Nat.zero + 1)) } -
                  (Nat.zero + 1) <
                Nat.zero + 1) }) =
    v (bit1 { val := i, isLt := hi })
[PROOFSTEP]
simp only [Nat.zero_eq, zero_add, Nat.lt_one_iff] at hi 
[GOAL]
case h.zero.mk
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin (Nat.zero + 1) → α
i : ℕ
hi✝ : i < Nat.zero + 1
hi : i = 0
⊢ (if h : ↑{ val := i, isLt := hi✝ } + ↑{ val := i, isLt := hi✝ } + 1 < Nat.zero + 1 then
      v
        { val := ↑{ val := i, isLt := hi✝ } + ↑{ val := i, isLt := hi✝ } + 1,
          isLt :=
            (_ :
              ↑{ val := ↑{ val := i, isLt := hi✝ } + ↑{ val := i, isLt := hi✝ } + 1,
                    isLt :=
                      (_ :
                        ↑{ val := i, isLt := hi✝ } + ↑{ val := i, isLt := hi✝ } + 1 < Nat.zero + 1 + (Nat.zero + 1)) } <
                Nat.zero + 1) }
    else
      v
        { val := ↑{ val := i, isLt := hi✝ } + ↑{ val := i, isLt := hi✝ } + 1 - (Nat.zero + 1),
          isLt :=
            (_ :
              ↑{ val := ↑{ val := i, isLt := hi✝ } + ↑{ val := i, isLt := hi✝ } + 1,
                      isLt :=
                        (_ :
                          ↑{ val := i, isLt := hi✝ } + ↑{ val := i, isLt := hi✝ } + 1 <
                            Nat.zero + 1 + (Nat.zero + 1)) } -
                  (Nat.zero + 1) <
                Nat.zero + 1) }) =
    v (bit1 { val := i, isLt := hi✝ })
[PROOFSTEP]
subst i
[GOAL]
case h.zero.mk
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin (Nat.zero + 1) → α
hi : 0 < Nat.zero + 1
⊢ (if h : ↑{ val := 0, isLt := hi } + ↑{ val := 0, isLt := hi } + 1 < Nat.zero + 1 then
      v
        { val := ↑{ val := 0, isLt := hi } + ↑{ val := 0, isLt := hi } + 1,
          isLt :=
            (_ :
              ↑{ val := ↑{ val := 0, isLt := hi } + ↑{ val := 0, isLt := hi } + 1,
                    isLt :=
                      (_ :
                        ↑{ val := 0, isLt := hi } + ↑{ val := 0, isLt := hi } + 1 < Nat.zero + 1 + (Nat.zero + 1)) } <
                Nat.zero + 1) }
    else
      v
        { val := ↑{ val := 0, isLt := hi } + ↑{ val := 0, isLt := hi } + 1 - (Nat.zero + 1),
          isLt :=
            (_ :
              ↑{ val := ↑{ val := 0, isLt := hi } + ↑{ val := 0, isLt := hi } + 1,
                      isLt :=
                        (_ :
                          ↑{ val := 0, isLt := hi } + ↑{ val := 0, isLt := hi } + 1 < Nat.zero + 1 + (Nat.zero + 1)) } -
                  (Nat.zero + 1) <
                Nat.zero + 1) }) =
    v (bit1 { val := 0, isLt := hi })
[PROOFSTEP]
rfl
[GOAL]
case h.succ
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
n : ℕ
v : Fin (Nat.succ n + 1) → α
i : Fin (Nat.succ n + 1)
⊢ (if h : ↑i + ↑i + 1 < Nat.succ n + 1 then
      v
        { val := ↑i + ↑i + 1,
          isLt :=
            (_ :
              ↑{ val := ↑i + ↑i + 1, isLt := (_ : ↑i + ↑i + 1 < Nat.succ n + 1 + (Nat.succ n + 1)) } < Nat.succ n + 1) }
    else
      v
        { val := ↑i + ↑i + 1 - (Nat.succ n + 1),
          isLt :=
            (_ :
              ↑{ val := ↑i + ↑i + 1, isLt := (_ : ↑i + ↑i + 1 < Nat.succ n + 1 + (Nat.succ n + 1)) } -
                  (Nat.succ n + 1) <
                Nat.succ n + 1) }) =
    v (bit1 i)
[PROOFSTEP]

| succ n =>
  split_ifs with h <;> simp_rw [bit1, bit0] <;> congr
  · rw [Fin.val_mk] at h 
    rw [Nat.mod_eq_of_lt (Nat.lt_of_succ_lt h)]
    erw [Nat.mod_eq_of_lt h]
  · rw [Fin.val_mk, not_lt] at h 
    simp only [Fin.ext_iff, Fin.val_add, Fin.val_mk, Nat.mod_add_mod, Fin.val_one, Nat.mod_eq_sub_mod h,
      show 1 % (n + 2) = 1 from Nat.mod_eq_of_lt (by simp)]
    refine (Nat.mod_eq_of_lt ?_).symm
    rw [tsub_lt_iff_left h]
    exact Nat.add_succ_lt_add i.2 i.2
[GOAL]
case h.succ
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
n : ℕ
v : Fin (Nat.succ n + 1) → α
i : Fin (Nat.succ n + 1)
⊢ (if h : ↑i + ↑i + 1 < Nat.succ n + 1 then
      v
        { val := ↑i + ↑i + 1,
          isLt :=
            (_ :
              ↑{ val := ↑i + ↑i + 1, isLt := (_ : ↑i + ↑i + 1 < Nat.succ n + 1 + (Nat.succ n + 1)) } < Nat.succ n + 1) }
    else
      v
        { val := ↑i + ↑i + 1 - (Nat.succ n + 1),
          isLt :=
            (_ :
              ↑{ val := ↑i + ↑i + 1, isLt := (_ : ↑i + ↑i + 1 < Nat.succ n + 1 + (Nat.succ n + 1)) } -
                  (Nat.succ n + 1) <
                Nat.succ n + 1) }) =
    v (bit1 i)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
n : ℕ
v : Fin (Nat.succ n + 1) → α
i : Fin (Nat.succ n + 1)
h : ↑i + ↑i + 1 < Nat.succ n + 1
⊢ v
      { val := ↑i + ↑i + 1,
        isLt :=
          (_ :
            ↑{ val := ↑i + ↑i + 1, isLt := (_ : ↑i + ↑i + 1 < Nat.succ n + 1 + (Nat.succ n + 1)) } < Nat.succ n + 1) } =
    v (bit1 i)
[PROOFSTEP]
simp_rw [bit1, bit0]
[GOAL]
case neg
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
n : ℕ
v : Fin (Nat.succ n + 1) → α
i : Fin (Nat.succ n + 1)
h : ¬↑i + ↑i + 1 < Nat.succ n + 1
⊢ v
      { val := ↑i + ↑i + 1 - (Nat.succ n + 1),
        isLt :=
          (_ :
            ↑{ val := ↑i + ↑i + 1, isLt := (_ : ↑i + ↑i + 1 < Nat.succ n + 1 + (Nat.succ n + 1)) } - (Nat.succ n + 1) <
              Nat.succ n + 1) } =
    v (bit1 i)
[PROOFSTEP]
simp_rw [bit1, bit0]
[GOAL]
case pos
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
n : ℕ
v : Fin (Nat.succ n + 1) → α
i : Fin (Nat.succ n + 1)
h : ↑i + ↑i + 1 < Nat.succ n + 1
⊢ v
      { val := ↑i + ↑i + 1,
        isLt :=
          (_ :
            ↑{ val := ↑i + ↑i + 1, isLt := (_ : ↑i + ↑i + 1 < Nat.succ n + 1 + (Nat.succ n + 1)) } < Nat.succ n + 1) } =
    v (i + i + 1)
[PROOFSTEP]
congr
[GOAL]
case neg
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
n : ℕ
v : Fin (Nat.succ n + 1) → α
i : Fin (Nat.succ n + 1)
h : ¬↑i + ↑i + 1 < Nat.succ n + 1
⊢ v
      { val := ↑i + ↑i + 1 - (Nat.succ n + 1),
        isLt :=
          (_ :
            ↑{ val := ↑i + ↑i + 1, isLt := (_ : ↑i + ↑i + 1 < Nat.succ n + 1 + (Nat.succ n + 1)) } - (Nat.succ n + 1) <
              Nat.succ n + 1) } =
    v (i + i + 1)
[PROOFSTEP]
congr
[GOAL]
case pos.e_a.e_val
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
n : ℕ
v : Fin (Nat.succ n + 1) → α
i : Fin (Nat.succ n + 1)
h : ↑i + ↑i + 1 < Nat.succ n + 1
⊢ ↑i + ↑i + 1 = ((↑i + ↑i) % (Nat.succ n + 1) + 1 % (Nat.succ n + 1)) % (Nat.succ n + 1)
[PROOFSTEP]
rw [Fin.val_mk] at h 
[GOAL]
case pos.e_a.e_val
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
n : ℕ
v : Fin (Nat.succ n + 1) → α
i : Fin (Nat.succ n + 1)
h : ↑i + ↑i + 1 < Nat.succ n + 1
⊢ ↑i + ↑i + 1 = ((↑i + ↑i) % (Nat.succ n + 1) + 1 % (Nat.succ n + 1)) % (Nat.succ n + 1)
[PROOFSTEP]
rw [Nat.mod_eq_of_lt (Nat.lt_of_succ_lt h)]
[GOAL]
case pos.e_a.e_val
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
n : ℕ
v : Fin (Nat.succ n + 1) → α
i : Fin (Nat.succ n + 1)
h : ↑i + ↑i + 1 < Nat.succ n + 1
⊢ ↑i + ↑i + 1 = (↑i + ↑i + 1 % (Nat.succ n + 1)) % (Nat.succ n + 1)
[PROOFSTEP]
erw [Nat.mod_eq_of_lt h]
[GOAL]
case neg.e_a.e_val
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
n : ℕ
v : Fin (Nat.succ n + 1) → α
i : Fin (Nat.succ n + 1)
h : ¬↑i + ↑i + 1 < Nat.succ n + 1
⊢ ↑i + ↑i + 1 - (Nat.succ n + 1) = ((↑i + ↑i) % (Nat.succ n + 1) + 1 % (Nat.succ n + 1)) % (Nat.succ n + 1)
[PROOFSTEP]
rw [Fin.val_mk, not_lt] at h 
[GOAL]
case neg.e_a.e_val
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
n : ℕ
v : Fin (Nat.succ n + 1) → α
i : Fin (Nat.succ n + 1)
h : Nat.succ n + 1 ≤ ↑i + ↑i + 1
⊢ ↑i + ↑i + 1 - (Nat.succ n + 1) = ((↑i + ↑i) % (Nat.succ n + 1) + 1 % (Nat.succ n + 1)) % (Nat.succ n + 1)
[PROOFSTEP]
simp only [Fin.ext_iff, Fin.val_add, Fin.val_mk, Nat.mod_add_mod, Fin.val_one, Nat.mod_eq_sub_mod h,
  show 1 % (n + 2) = 1 from Nat.mod_eq_of_lt (by simp)]
[GOAL]
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
n : ℕ
v : Fin (Nat.succ n + 1) → α
i : Fin (Nat.succ n + 1)
h : Nat.succ n + 1 ≤ ↑i + ↑i + 1
⊢ 1 < n + 2
[PROOFSTEP]
simp
[GOAL]
case neg.e_a.e_val
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
n : ℕ
v : Fin (Nat.succ n + 1) → α
i : Fin (Nat.succ n + 1)
h : Nat.succ n + 1 ≤ ↑i + ↑i + 1
⊢ ↑i + ↑i + 1 - (Nat.succ n + 1) = (↑i + ↑i + 1 - (Nat.succ n + 1)) % (Nat.succ n + 1)
[PROOFSTEP]
refine (Nat.mod_eq_of_lt ?_).symm
[GOAL]
case neg.e_a.e_val
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
n : ℕ
v : Fin (Nat.succ n + 1) → α
i : Fin (Nat.succ n + 1)
h : Nat.succ n + 1 ≤ ↑i + ↑i + 1
⊢ ↑i + ↑i + 1 - (Nat.succ n + 1) < Nat.succ n + 1
[PROOFSTEP]
rw [tsub_lt_iff_left h]
[GOAL]
case neg.e_a.e_val
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
n : ℕ
v : Fin (Nat.succ n + 1) → α
i : Fin (Nat.succ n + 1)
h : Nat.succ n + 1 ≤ ↑i + ↑i + 1
⊢ ↑i + ↑i + 1 < Nat.succ n + 1 + (Nat.succ n + 1)
[PROOFSTEP]
exact Nat.add_succ_lt_add i.2 i.2
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
hm : m + 2 = n + 1 + (n + 1)
v : Fin (m + 2) → α
⊢ vecHead (vecAlt1 hm v) = v 1
[PROOFSTEP]
simp [vecHead, vecAlt1]
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
x : α
u : Fin n → α
i : Fin (n + 1)
⊢ vecCons x u (bit0 i) =
    vecAlt0 (_ : Nat.succ n + Nat.succ n = Nat.succ n + Nat.succ n)
      (vecAppend (_ : Nat.succ n + Nat.succ n = Nat.succ n + Nat.succ n) (vecCons x u) (vecCons x u)) i
[PROOFSTEP]
rw [vecAlt0_vecAppend]
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
x : α
u : Fin n → α
i : Fin (n + 1)
⊢ vecCons x u (bit0 i) = (vecCons x u ∘ bit0) i
[PROOFSTEP]
rfl
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
x : α
u : Fin n → α
i : Fin (n + 1)
⊢ vecCons x u (bit1 i) =
    vecAlt1 (_ : Nat.succ n + Nat.succ n = Nat.succ n + Nat.succ n)
      (vecAppend (_ : Nat.succ n + Nat.succ n = Nat.succ n + Nat.succ n) (vecCons x u) (vecCons x u)) i
[PROOFSTEP]
rw [vecAlt1_vecAppend]
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
x : α
u : Fin n → α
i : Fin (n + 1)
⊢ vecCons x u (bit1 i) = (vecCons x u ∘ bit1) i
[PROOFSTEP]
rfl
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
⊢ m = n + n
[PROOFSTEP]
rwa [add_assoc n, add_comm 1, ← add_assoc, ← add_assoc, add_right_cancel_iff, add_right_cancel_iff] at h 
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
⊢ vecAlt0 h (vecCons x (vecCons y u)) = vecCons x (vecAlt0 (_ : m = n + n) u)
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : Fin (n + 1)
⊢ vecAlt0 h (vecCons x (vecCons y u)) i = vecCons x (vecAlt0 (_ : m = n + n) u) i
[PROOFSTEP]
simp_rw [vecAlt0]
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : Fin (n + 1)
⊢ vecCons x (vecCons y u) { val := ↑i + ↑i, isLt := (_ : ↑i + ↑i < m + 1 + 1) } =
    vecCons x (fun k => u { val := ↑k + ↑k, isLt := (_ : ↑k + ↑k < m) }) i
[PROOFSTEP]
rcases i with ⟨⟨⟩ | i, hi⟩
[GOAL]
case h.mk.zero
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
hi : Nat.zero < n + 1
⊢ vecCons x (vecCons y u)
      { val := ↑{ val := Nat.zero, isLt := hi } + ↑{ val := Nat.zero, isLt := hi },
        isLt := (_ : ↑{ val := Nat.zero, isLt := hi } + ↑{ val := Nat.zero, isLt := hi } < m + 1 + 1) } =
    vecCons x (fun k => u { val := ↑k + ↑k, isLt := (_ : ↑k + ↑k < m) }) { val := Nat.zero, isLt := hi }
[PROOFSTEP]
rfl
[GOAL]
case h.mk.succ
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : ℕ
hi : Nat.succ i < n + 1
⊢ vecCons x (vecCons y u)
      { val := ↑{ val := Nat.succ i, isLt := hi } + ↑{ val := Nat.succ i, isLt := hi },
        isLt := (_ : ↑{ val := Nat.succ i, isLt := hi } + ↑{ val := Nat.succ i, isLt := hi } < m + 1 + 1) } =
    vecCons x (fun k => u { val := ↑k + ↑k, isLt := (_ : ↑k + ↑k < m) }) { val := Nat.succ i, isLt := hi }
[PROOFSTEP]
simp [vecAlt0, Nat.add_succ, Nat.succ_add]
[GOAL]
α✝ : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
α : Type u_4
h : 0 = 0 + 0
⊢ vecAlt0 h ![] = ![]
[PROOFSTEP]
simp
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
⊢ m = n + n
[PROOFSTEP]
rwa [add_assoc n, add_comm 1, ← add_assoc, ← add_assoc, add_right_cancel_iff, add_right_cancel_iff] at h 
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
⊢ vecAlt1 h (vecCons x (vecCons y u)) = vecCons y (vecAlt1 (_ : m = n + n) u)
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : Fin (n + 1)
⊢ vecAlt1 h (vecCons x (vecCons y u)) i = vecCons y (vecAlt1 (_ : m = n + n) u) i
[PROOFSTEP]
simp_rw [vecAlt1]
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : Fin (n + 1)
⊢ vecCons x (vecCons y u) { val := ↑i + ↑i + 1, isLt := (_ : ↑i + ↑i + 1 < m + 1 + 1) } =
    vecCons y (fun k => u { val := ↑k + ↑k + 1, isLt := (_ : ↑k + ↑k + 1 < m) }) i
[PROOFSTEP]
rcases i with ⟨⟨⟩ | i, hi⟩
[GOAL]
case h.mk.zero
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
hi : Nat.zero < n + 1
⊢ vecCons x (vecCons y u)
      { val := ↑{ val := Nat.zero, isLt := hi } + ↑{ val := Nat.zero, isLt := hi } + 1,
        isLt := (_ : ↑{ val := Nat.zero, isLt := hi } + ↑{ val := Nat.zero, isLt := hi } + 1 < m + 1 + 1) } =
    vecCons y (fun k => u { val := ↑k + ↑k + 1, isLt := (_ : ↑k + ↑k + 1 < m) }) { val := Nat.zero, isLt := hi }
[PROOFSTEP]
rfl
[GOAL]
case h.mk.succ
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : ℕ
hi : Nat.succ i < n + 1
⊢ vecCons x (vecCons y u)
      { val := ↑{ val := Nat.succ i, isLt := hi } + ↑{ val := Nat.succ i, isLt := hi } + 1,
        isLt := (_ : ↑{ val := Nat.succ i, isLt := hi } + ↑{ val := Nat.succ i, isLt := hi } + 1 < m + 1 + 1) } =
    vecCons y (fun k => u { val := ↑k + ↑k + 1, isLt := (_ : ↑k + ↑k + 1 < m) }) { val := Nat.succ i, isLt := hi }
[PROOFSTEP]
simp [vecAlt1, Nat.add_succ, Nat.succ_add]
[GOAL]
α✝ : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
α : Type u_4
h : 0 = 0 + 0
⊢ vecAlt1 h ![] = ![]
[PROOFSTEP]
simp
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
M : Type u_4
inst✝ : SMul M α
x : M
y : α
v : Fin n → α
⊢ x • vecCons y v = vecCons (x • y) (x • v)
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
M : Type u_4
inst✝ : SMul M α
x : M
y : α
v : Fin n → α
i : Fin (Nat.succ n)
⊢ (x • vecCons y v) i = vecCons (x • y) (x • v) i
[PROOFSTEP]
refine' Fin.cases _ _ i
[GOAL]
case h.refine'_1
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
M : Type u_4
inst✝ : SMul M α
x : M
y : α
v : Fin n → α
i : Fin (Nat.succ n)
⊢ (x • vecCons y v) 0 = vecCons (x • y) (x • v) 0
[PROOFSTEP]
simp
[GOAL]
case h.refine'_2
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
M : Type u_4
inst✝ : SMul M α
x : M
y : α
v : Fin n → α
i : Fin (Nat.succ n)
⊢ ∀ (i : Fin n), (x • vecCons y v) (Fin.succ i) = vecCons (x • y) (x • v) (Fin.succ i)
[PROOFSTEP]
simp
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Add α
x : α
v : Fin n → α
w : Fin (Nat.succ n) → α
⊢ vecCons x v + w = vecCons (x + vecHead w) (v + vecTail w)
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Add α
x : α
v : Fin n → α
w : Fin (Nat.succ n) → α
i : Fin (Nat.succ n)
⊢ (vecCons x v + w) i = vecCons (x + vecHead w) (v + vecTail w) i
[PROOFSTEP]
refine' Fin.cases _ _ i
[GOAL]
case h.refine'_1
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Add α
x : α
v : Fin n → α
w : Fin (Nat.succ n) → α
i : Fin (Nat.succ n)
⊢ (vecCons x v + w) 0 = vecCons (x + vecHead w) (v + vecTail w) 0
[PROOFSTEP]
simp [vecHead, vecTail]
[GOAL]
case h.refine'_2
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Add α
x : α
v : Fin n → α
w : Fin (Nat.succ n) → α
i : Fin (Nat.succ n)
⊢ ∀ (i : Fin n), (vecCons x v + w) (Fin.succ i) = vecCons (x + vecHead w) (v + vecTail w) (Fin.succ i)
[PROOFSTEP]
simp [vecHead, vecTail]
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Add α
v : Fin (Nat.succ n) → α
y : α
w : Fin n → α
⊢ v + vecCons y w = vecCons (vecHead v + y) (vecTail v + w)
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Add α
v : Fin (Nat.succ n) → α
y : α
w : Fin n → α
i : Fin (Nat.succ n)
⊢ (v + vecCons y w) i = vecCons (vecHead v + y) (vecTail v + w) i
[PROOFSTEP]
refine' Fin.cases _ _ i
[GOAL]
case h.refine'_1
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Add α
v : Fin (Nat.succ n) → α
y : α
w : Fin n → α
i : Fin (Nat.succ n)
⊢ (v + vecCons y w) 0 = vecCons (vecHead v + y) (vecTail v + w) 0
[PROOFSTEP]
simp [vecHead, vecTail]
[GOAL]
case h.refine'_2
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Add α
v : Fin (Nat.succ n) → α
y : α
w : Fin n → α
i : Fin (Nat.succ n)
⊢ ∀ (i : Fin n), (v + vecCons y w) (Fin.succ i) = vecCons (vecHead v + y) (vecTail v + w) (Fin.succ i)
[PROOFSTEP]
simp [vecHead, vecTail]
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Add α
x : α
v : Fin n → α
y : α
w : Fin n → α
⊢ vecCons x v + vecCons y w = vecCons (x + y) (v + w)
[PROOFSTEP]
simp
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Sub α
x : α
v : Fin n → α
w : Fin (Nat.succ n) → α
⊢ vecCons x v - w = vecCons (x - vecHead w) (v - vecTail w)
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Sub α
x : α
v : Fin n → α
w : Fin (Nat.succ n) → α
i : Fin (Nat.succ n)
⊢ (vecCons x v - w) i = vecCons (x - vecHead w) (v - vecTail w) i
[PROOFSTEP]
refine' Fin.cases _ _ i
[GOAL]
case h.refine'_1
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Sub α
x : α
v : Fin n → α
w : Fin (Nat.succ n) → α
i : Fin (Nat.succ n)
⊢ (vecCons x v - w) 0 = vecCons (x - vecHead w) (v - vecTail w) 0
[PROOFSTEP]
simp [vecHead, vecTail]
[GOAL]
case h.refine'_2
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Sub α
x : α
v : Fin n → α
w : Fin (Nat.succ n) → α
i : Fin (Nat.succ n)
⊢ ∀ (i : Fin n), (vecCons x v - w) (Fin.succ i) = vecCons (x - vecHead w) (v - vecTail w) (Fin.succ i)
[PROOFSTEP]
simp [vecHead, vecTail]
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Sub α
v : Fin (Nat.succ n) → α
y : α
w : Fin n → α
⊢ v - vecCons y w = vecCons (vecHead v - y) (vecTail v - w)
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Sub α
v : Fin (Nat.succ n) → α
y : α
w : Fin n → α
i : Fin (Nat.succ n)
⊢ (v - vecCons y w) i = vecCons (vecHead v - y) (vecTail v - w) i
[PROOFSTEP]
refine' Fin.cases _ _ i
[GOAL]
case h.refine'_1
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Sub α
v : Fin (Nat.succ n) → α
y : α
w : Fin n → α
i : Fin (Nat.succ n)
⊢ (v - vecCons y w) 0 = vecCons (vecHead v - y) (vecTail v - w) 0
[PROOFSTEP]
simp [vecHead, vecTail]
[GOAL]
case h.refine'_2
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Sub α
v : Fin (Nat.succ n) → α
y : α
w : Fin n → α
i : Fin (Nat.succ n)
⊢ ∀ (i : Fin n), (v - vecCons y w) (Fin.succ i) = vecCons (vecHead v - y) (vecTail v - w) (Fin.succ i)
[PROOFSTEP]
simp [vecHead, vecTail]
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Sub α
x : α
v : Fin n → α
y : α
w : Fin n → α
⊢ vecCons x v - vecCons y w = vecCons (x - y) (v - w)
[PROOFSTEP]
simp
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Zero α
⊢ vecCons 0 0 = 0
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Zero α
i : Fin (Nat.succ n)
⊢ vecCons 0 0 i = OfNat.ofNat 0 i
[PROOFSTEP]
refine' Fin.cases _ _ i
[GOAL]
case h.refine'_1
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Zero α
i : Fin (Nat.succ n)
⊢ vecCons 0 0 0 = OfNat.ofNat 0 0
[PROOFSTEP]
rfl
[GOAL]
case h.refine'_2
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Zero α
i : Fin (Nat.succ n)
⊢ ∀ (i : Fin n), vecCons 0 0 (Fin.succ i) = OfNat.ofNat 0 (Fin.succ i)
[PROOFSTEP]
simp
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Zero α
v : Fin n → α
x : α
h : vecCons x v = 0
⊢ v = 0
[PROOFSTEP]
convert congr_arg vecTail h
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Zero α
v : Fin n → α
x : α
x✝ : x = 0 ∧ v = 0
hx : x = 0
hv : v = 0
⊢ vecCons x v = 0
[PROOFSTEP]
simp [hx, hv]
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Neg α
x : α
v : Fin n → α
⊢ -vecCons x v = vecCons (-x) (-v)
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Neg α
x : α
v : Fin n → α
i : Fin (Nat.succ n)
⊢ (-vecCons x v) i = vecCons (-x) (-v) i
[PROOFSTEP]
refine' Fin.cases _ _ i
[GOAL]
case h.refine'_1
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Neg α
x : α
v : Fin n → α
i : Fin (Nat.succ n)
⊢ (-vecCons x v) 0 = vecCons (-x) (-v) 0
[PROOFSTEP]
simp
[GOAL]
case h.refine'_2
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Neg α
x : α
v : Fin n → α
i : Fin (Nat.succ n)
⊢ ∀ (i : Fin n), (-vecCons x v) (Fin.succ i) = vecCons (-x) (-v) (Fin.succ i)
[PROOFSTEP]
simp
