cases (g x) with
| true => simp only
          apply Nat.le_trans (ih (x::rs))
          simp only [length]
          rw [Nat.add_comm (length rs), Nat.add_assoc]
          apply Nat.le.refl
| false => simp only [length]
           apply Nat.le_trans (ih rs)
           rw [Nat.add_comm (length xs) 1,
               Nat.add_assoc 1,
               Nat.add_comm 1,
               Nat.add_one]
           apply Nat.le.step
           apply Nat.le.refl
case cons
α : 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 g x with
      | true => filterTR.loop g xs (x :: rs)
      | false => filterTR.loop g xs rs) ≤
    length (x :: xs) + length rs
no goals