simp only [length]
case cons.false
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
rs : List α
⊢ length
      (match false with
      | true => filterTR.loop g xs (x :: rs)
      | false => filterTR.loop g xs rs) ≤
    length (x :: xs) + length rs
case cons.false
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
rs : List α
⊢ length (filterTR.loop g xs rs) ≤ length xs + 1 + length rs