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

State before:
α : Type u_1
g : α → Bool
xs : List α
⊢ length (filter g xs) ≤ length xs
Tactic:
induction xs with
| nil => simp [length]
| cons x xs ih =>
   simp only [filter]
   cases (g x) with
   | true =>
     simp only
     apply Nat.succ_le_succ
     exact ih
   | false =>
     simp only
     apply Nat.le.step
     exact ih
State after:
no goals

State before:
case nil
α : Type u_1
g : α → Bool
⊢ length (filter g []) ≤ length []
Tactic:
simp [length]
State after:
no goals

State before:
case cons
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : length (filter g xs) ≤ length xs
⊢ length (filter g (x :: xs)) ≤ length (x :: xs)
Tactic:
simp only [filter]
State after:
case cons
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : length (filter g xs) ≤ length xs
⊢ length
      (match g x with
      | true => x :: filter g xs
      | false => filter g xs) ≤
    length (x :: xs)

State before:
case cons
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : length (filter g xs) ≤ length xs
⊢ length
      (match g x with
      | true => x :: filter g xs
      | false => filter g xs) ≤
    length (x :: xs)
Tactic:
cases (g x) with
| true =>
  simp only
  apply Nat.succ_le_succ
  exact ih
| false =>
  simp only
  apply Nat.le.step
  exact ih
State after:
no goals

State before:
case cons.true
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : length (filter g xs) ≤ length xs
⊢ length
      (match true with
      | true => x :: filter g xs
      | false => filter g xs) ≤
    length (x :: xs)
Tactic:
simp only
State after:
case cons.true
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : length (filter g xs) ≤ length xs
⊢ length (x :: filter g xs) ≤ length (x :: xs)

State before:
case cons.true
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : length (filter g xs) ≤ length xs
⊢ length (x :: filter g xs) ≤ length (x :: xs)
Tactic:
apply Nat.succ_le_succ
State after:
case cons.true.a
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : length (filter g xs) ≤ length xs
⊢ length (filter g xs) ≤ length xs

State before:
case cons.true.a
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : length (filter g xs) ≤ length xs
⊢ length (filter g xs) ≤ length xs
Tactic:
exact ih
State after:
no goals

State before:
case cons.false
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : length (filter g xs) ≤ length xs
⊢ length
      (match false with
      | true => x :: filter g xs
      | false => filter g xs) ≤
    length (x :: xs)
Tactic:
simp only
State after:
case cons.false
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : length (filter g xs) ≤ length xs
⊢ length (filter g xs) ≤ length (x :: xs)

State before:
case cons.false
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : length (filter g xs) ≤ length xs
⊢ length (filter g xs) ≤ length (x :: xs)
Tactic:
apply Nat.le.step
State after:
case cons.false.a
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : length (filter g xs) ≤ length xs
⊢ Nat.le (length (filter g xs)) (length xs)

State before:
case cons.false.a
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : length (filter g xs) ≤ length xs
⊢ Nat.le (length (filter g xs)) (length xs)
Tactic:
exact ih
State after:
no goals