case h
α✝ : Type u
m n o✝ : ℕ
m' : Type ?u.24888
n' : Type ?u.24891
o' : Type ?u.24894
α : Type u_1
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) }
α✝ : Type u
m n o✝ : ℕ
m' : Type ?u.24888
n' : Type ?u.24891
o' : Type ?u.24894
α : Type u_1
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) }
ext i
case h
α✝ : Type u
m n o✝ : ℕ
m' : Type ?u.24888
n' : Type ?u.24891
o' : Type ?u.24894
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
⊢ (if hi : ↑(↑(Fin.cast ho) i) < m then
      (_ : ↑(Fin.castAdd n) (Fin.castLT (↑(Fin.cast ho) i) hi) = ↑(Fin.cast ho) i) ▸
        u (Fin.castLT (↑(Fin.cast ho) i) hi)
    else
      (_ :
          ↑(Fin.natAdd m)
              (Fin.subNat m (↑(Fin.cast (_ : m + n = n + m)) (↑(Fin.cast ho) i)) (_ : m ≤ ↑(↑(Fin.cast ho) i))) =
            ↑(Fin.cast ho) i) ▸
        v (Fin.subNat m (↑(Fin.cast (_ : m + n = n + m)) (↑(Fin.cast ho) i)) (_ : m ≤ ↑(↑(Fin.cast ho) i)))) =
    if h : ↑i < m then u { val := ↑i, isLt := h } else v { val := ↑i - m, isLt := (_ : ↑i - m < n) }
case h
α✝ : Type u
m n o✝ : ℕ
m' : Type ?u.24888
n' : Type ?u.24891
o' : Type ?u.24894
α : Type u_1
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) }
rw [vecAppend, Fin.append, Function.comp_apply, Fin.addCases]
case h.e_e.h
α✝ : Type u
m n o✝ : ℕ
m' : Type ?u.24888
n' : Type ?u.24891
o' : Type ?u.24894
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
hi : ¬↑(↑(Fin.cast ho) i) < m
⊢ (_ :
        ↑(Fin.natAdd m)
            (Fin.subNat m (↑(Fin.cast (_ : m + n = n + m)) (↑(Fin.cast ho) i)) (_ : m ≤ ↑(↑(Fin.cast ho) i))) =
          ↑(Fin.cast ho) i) ▸
      v (Fin.subNat m (↑(Fin.cast (_ : m + n = n + m)) (↑(Fin.cast ho) i)) (_ : m ≤ ↑(↑(Fin.cast ho) i))) =
    v { val := ↑i - m, isLt := (_ : ↑i - m < n) }
case h
α✝ : Type u
m n o✝ : ℕ
m' : Type ?u.24888
n' : Type ?u.24891
o' : Type ?u.24894
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
⊢ (if hi : ↑(↑(Fin.cast ho) i) < m then
      (_ : ↑(Fin.castAdd n) (Fin.castLT (↑(Fin.cast ho) i) hi) = ↑(Fin.cast ho) i) ▸
        u (Fin.castLT (↑(Fin.cast ho) i) hi)
    else
      (_ :
          ↑(Fin.natAdd m)
              (Fin.subNat m (↑(Fin.cast (_ : m + n = n + m)) (↑(Fin.cast ho) i)) (_ : m ≤ ↑(↑(Fin.cast ho) i))) =
            ↑(Fin.cast ho) i) ▸
        v (Fin.subNat m (↑(Fin.cast (_ : m + n = n + m)) (↑(Fin.cast ho) i)) (_ : m ≤ ↑(↑(Fin.cast ho) i)))) =
    if h : ↑i < m then u { val := ↑i, isLt := h } else v { val := ↑i - m, isLt := (_ : ↑i - m < n) }
congr with hi
case h.e_e.h
α✝ : Type u
m n o✝ : ℕ
m' : Type ?u.24888
n' : Type ?u.24891
o' : Type ?u.24894
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
hi : ¬↑(↑(Fin.cast ho) i) < m
⊢ v (Fin.subNat m (↑(Fin.cast (_ : m + n = n + m)) (↑(Fin.cast ho) i)) (_ : m ≤ ↑(↑(Fin.cast ho) i))) =
    v { val := ↑i - m, isLt := (_ : ↑i - m < n) }
case h.e_e.h
α✝ : Type u
m n o✝ : ℕ
m' : Type ?u.24888
n' : Type ?u.24891
o' : Type ?u.24894
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
hi : ¬↑(↑(Fin.cast ho) i) < m
⊢ (_ :
        ↑(Fin.natAdd m)
            (Fin.subNat m (↑(Fin.cast (_ : m + n = n + m)) (↑(Fin.cast ho) i)) (_ : m ≤ ↑(↑(Fin.cast ho) i))) =
          ↑(Fin.cast ho) i) ▸
      v (Fin.subNat m (↑(Fin.cast (_ : m + n = n + m)) (↑(Fin.cast ho) i)) (_ : m ≤ ↑(↑(Fin.cast ho) i))) =
    v { val := ↑i - m, isLt := (_ : ↑i - m < n) }
simp only [eq_rec_constant]
no goals
case h.e_e.h
α✝ : Type u
m n o✝ : ℕ
m' : Type ?u.24888
n' : Type ?u.24891
o' : Type ?u.24894
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
hi : ¬↑(↑(Fin.cast ho) i) < m
⊢ v (Fin.subNat m (↑(Fin.cast (_ : m + n = n + m)) (↑(Fin.cast ho) i)) (_ : m ≤ ↑(↑(Fin.cast ho) i))) =
    v { val := ↑i - m, isLt := (_ : ↑i - m < n) }
rfl