Theorem: List.sizeOf_filter (LeanSAT/Upstream/ToStd.lean)

State before:
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
L : List α
⊢ sizeOf (filter f L) ≤ sizeOf L
Tactic:
induction L <;> simp [filter]
State after:
case cons
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : sizeOf (filter f tail✝) ≤ sizeOf tail✝
⊢ sizeOf
      (match f head✝ with
      | true => head✝ :: filter f tail✝
      | false => filter f tail✝) ≤
    1 + sizeOf head✝ + sizeOf tail✝

State before:
case cons
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : sizeOf (filter f tail✝) ≤ sizeOf tail✝
⊢ sizeOf
      (match f head✝ with
      | true => head✝ :: filter f tail✝
      | false => filter f tail✝) ≤
    1 + sizeOf head✝ + sizeOf tail✝
Tactic:
split
State after:
case cons.h_1
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : sizeOf (filter f tail✝) ≤ sizeOf tail✝
x✝ : Bool
heq✝ : f head✝ = true
⊢ sizeOf (head✝ :: filter f tail✝) ≤ 1 + sizeOf head✝ + sizeOf tail✝

case cons.h_2
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : sizeOf (filter f tail✝) ≤ sizeOf tail✝
x✝ : Bool
heq✝ : f head✝ = false
⊢ sizeOf (filter f tail✝) ≤ 1 + sizeOf head✝ + sizeOf tail✝

State before:
case cons.h_1
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : sizeOf (filter f tail✝) ≤ sizeOf tail✝
x✝ : Bool
heq✝ : f head✝ = true
⊢ sizeOf (head✝ :: filter f tail✝) ≤ 1 + sizeOf head✝ + sizeOf tail✝

case cons.h_2
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : sizeOf (filter f tail✝) ≤ sizeOf tail✝
x✝ : Bool
heq✝ : f head✝ = false
⊢ sizeOf (filter f tail✝) ≤ 1 + sizeOf head✝ + sizeOf tail✝
Tactic:
. simp
  apply Nat.add_le_add_left
  assumption
State after:
case cons.h_2
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : sizeOf (filter f tail✝) ≤ sizeOf tail✝
x✝ : Bool
heq✝ : f head✝ = false
⊢ sizeOf (filter f tail✝) ≤ 1 + sizeOf head✝ + sizeOf tail✝

State before:
case cons.h_2
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : sizeOf (filter f tail✝) ≤ sizeOf tail✝
x✝ : Bool
heq✝ : f head✝ = false
⊢ sizeOf (filter f tail✝) ≤ 1 + sizeOf head✝ + sizeOf tail✝
Tactic:
. apply Nat.le_trans ?_ (Nat.le_add_left _ _)
  assumption
State after:
no goals

State before:
case cons.h_1
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : sizeOf (filter f tail✝) ≤ sizeOf tail✝
x✝ : Bool
heq✝ : f head✝ = true
⊢ sizeOf (head✝ :: filter f tail✝) ≤ 1 + sizeOf head✝ + sizeOf tail✝
Tactic:
simp
State after:
case cons.h_1
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : sizeOf (filter f tail✝) ≤ sizeOf tail✝
x✝ : Bool
heq✝ : f head✝ = true
⊢ 1 + sizeOf head✝ + sizeOf (filter f tail✝) ≤ 1 + sizeOf head✝ + sizeOf tail✝

State before:
case cons.h_1
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : sizeOf (filter f tail✝) ≤ sizeOf tail✝
x✝ : Bool
heq✝ : f head✝ = true
⊢ 1 + sizeOf head✝ + sizeOf (filter f tail✝) ≤ 1 + sizeOf head✝ + sizeOf tail✝
Tactic:
apply Nat.add_le_add_left
State after:
case cons.h_1.h
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : sizeOf (filter f tail✝) ≤ sizeOf tail✝
x✝ : Bool
heq✝ : f head✝ = true
⊢ sizeOf (filter f tail✝) ≤ sizeOf tail✝

State before:
case cons.h_1.h
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : sizeOf (filter f tail✝) ≤ sizeOf tail✝
x✝ : Bool
heq✝ : f head✝ = true
⊢ sizeOf (filter f tail✝) ≤ sizeOf tail✝
Tactic:
assumption
State after:
no goals

State before:
case cons.h_2
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : sizeOf (filter f tail✝) ≤ sizeOf tail✝
x✝ : Bool
heq✝ : f head✝ = false
⊢ sizeOf (filter f tail✝) ≤ 1 + sizeOf head✝ + sizeOf tail✝
Tactic:
apply Nat.le_trans ?_ (Nat.le_add_left _ _)
State after:
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : sizeOf (filter f tail✝) ≤ sizeOf tail✝
x✝ : Bool
heq✝ : f head✝ = false
⊢ sizeOf (filter f tail✝) ≤ sizeOf tail✝

State before:
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : sizeOf (filter f tail✝) ≤ sizeOf tail✝
x✝ : Bool
heq✝ : f head✝ = false
⊢ sizeOf (filter f tail✝) ≤ sizeOf tail✝
Tactic:
assumption
State after:
no goals