Theorem: List.length_filterTR_le (Table/BuiltinExtensions.lean)

State before:
α : Type u_1
g : α → Bool
xs : List α
⊢ ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
Tactic:
induction xs with
| nil =>
  intro rs
  simp only [filter, filterTR.loop]
  rw [List.length_reverse]
  simp only [length, Nat.zero_add]
  apply Nat.le.refl
| cons x xs ih =>
  intro rs
  simp only [filter, filterTR.loop]
  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
State after:
no goals

State before:
case nil
α : Type u_1
g : α → Bool
⊢ ∀ (rs : List α), length (filterTR.loop g [] rs) ≤ length [] + length rs
Tactic:
intro rs
State after:
case nil
α : Type u_1
g : α → Bool
rs : List α
⊢ length (filterTR.loop g [] rs) ≤ length [] + length rs

State before:
case nil
α : Type u_1
g : α → Bool
rs : List α
⊢ length (filterTR.loop g [] rs) ≤ length [] + length rs
Tactic:
simp only [filter, filterTR.loop]
State after:
case nil
α : Type u_1
g : α → Bool
rs : List α
⊢ length (reverse rs) ≤ length [] + length rs

State before:
case nil
α : Type u_1
g : α → Bool
rs : List α
⊢ length (reverse rs) ≤ length [] + length rs
Tactic:
rw [List.length_reverse]
State after:
case nil
α : Type u_1
g : α → Bool
rs : List α
⊢ length rs ≤ length [] + length rs

State before:
case nil
α : Type u_1
g : α → Bool
rs : List α
⊢ length rs ≤ length [] + length rs
Tactic:
simp only [length, Nat.zero_add]
State after:
case nil
α : Type u_1
g : α → Bool
rs : List α
⊢ length rs ≤ length rs

State before:
case nil
α : Type u_1
g : α → Bool
rs : List α
⊢ length rs ≤ length rs
Tactic:
apply Nat.le.refl
State after:
no goals

State before:
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 (filterTR.loop g (x :: xs) rs) ≤ length (x :: xs) + length rs
Tactic:
intro rs
State after:
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 (filterTR.loop g (x :: xs) rs) ≤ length (x :: xs) + length rs

State before:
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 (filterTR.loop g (x :: xs) rs) ≤ length (x :: xs) + length rs
Tactic:
simp only [filter, filterTR.loop]
State after:
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

State before:
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
Tactic:
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
State after:
no goals

State before:
case cons.true
α : 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 true with
      | true => filterTR.loop g xs (x :: rs)
      | false => filterTR.loop g xs rs) ≤
    length (x :: xs) + length rs
Tactic:
simp only
State after:
case cons.true
α : 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 (x :: rs)) ≤ length (x :: xs) + length rs

State before:
case cons.true
α : 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 (x :: rs)) ≤ length (x :: xs) + length rs
Tactic:
apply Nat.le_trans (ih (x::rs))
State after:
case cons.true
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
rs : List α
⊢ length xs + length (x :: rs) ≤ length (x :: xs) + length rs

State before:
case cons.true
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
rs : List α
⊢ length xs + length (x :: rs) ≤ length (x :: xs) + length rs
Tactic:
simp only [length]
State after:
case cons.true
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
rs : List α
⊢ length xs + (length rs + 1) ≤ length xs + 1 + length rs

State before:
case cons.true
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
rs : List α
⊢ length xs + (length rs + 1) ≤ length xs + 1 + length rs
Tactic:
rw [Nat.add_comm (length rs), Nat.add_assoc]
State after:
case cons.true
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
rs : List α
⊢ length xs + (1 + length rs) ≤ length xs + (1 + length rs)

State before:
case cons.true
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
rs : List α
⊢ length xs + (1 + length rs) ≤ length xs + (1 + length rs)
Tactic:
apply Nat.le.refl
State after:
no goals

State before:
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
Tactic:
simp only [length]
State after:
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

State before:
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
Tactic:
apply Nat.le_trans (ih rs)
State after:
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 xs + length rs ≤ length xs + 1 + length rs

State before:
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 xs + length rs ≤ length xs + 1 + length rs
Tactic:
rw [Nat.add_comm (length xs) 1,
    Nat.add_assoc 1,
    Nat.add_comm 1,
    Nat.add_one]
State after:
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 xs + length rs ≤ Nat.succ (length xs + length rs)

State before:
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 xs + length rs ≤ Nat.succ (length xs + length rs)
Tactic:
apply Nat.le.step
State after:
case cons.false.a
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
rs : List α
⊢ Nat.le (length xs + length rs) (length xs + length rs)

State before:
case cons.false.a
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
rs : List α
⊢ Nat.le (length xs + length rs) (length xs + length rs)
Tactic:
apply Nat.le.refl
State after:
no goals