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

State before:
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
L : List α
h : filter f L ≠ L
⊢ sizeOf (filter f L) < sizeOf L
Tactic:
induction L <;> simp [filter] at *
State after:
case cons
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : ¬filter f tail✝ = tail✝ → sizeOf (filter f tail✝) < sizeOf tail✝
h :
  ¬(match f head✝ with
      | true => head✝ :: filter f tail✝
      | false => filter f tail✝) =
      head✝ :: 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✝ : ¬filter f tail✝ = tail✝ → sizeOf (filter f tail✝) < sizeOf tail✝
h :
  ¬(match f head✝ with
      | true => head✝ :: filter f tail✝
      | false => filter f tail✝) =
      head✝ :: tail✝
⊢ sizeOf
      (match f head✝ with
      | true => head✝ :: filter f tail✝
      | false => filter f tail✝) <
    1 + sizeOf head✝ + sizeOf tail✝
Tactic:
next hd tl ih =>
split
next hHd =>
  simp [hHd] at h
  simp [_sizeOf_1]
  apply Nat.add_lt_add_left
  apply ih
  assumption
next hHd =>
  clear h hHd
  apply Nat.lt_of_le_of_lt (sizeOf_filter _ _)
  rw [Nat.add_comm, Nat.add_comm 1, Nat.add_one, Nat.add_succ]
  apply Nat.succ_le_succ
  apply Nat.le_add_right
State after:
no goals

State before:
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
h :
  ¬(match f hd with
      | true => hd :: filter f tl
      | false => filter f tl) =
      hd :: tl
⊢ sizeOf
      (match f hd with
      | true => hd :: filter f tl
      | false => filter f tl) <
    1 + sizeOf hd + sizeOf tl
Tactic:
split
State after:
case h_1
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
h :
  ¬(match f hd with
      | true => hd :: filter f tl
      | false => filter f tl) =
      hd :: tl
x✝ : Bool
heq✝ : f hd = true
⊢ sizeOf (hd :: filter f tl) < 1 + sizeOf hd + sizeOf tl

case h_2
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
h :
  ¬(match f hd with
      | true => hd :: filter f tl
      | false => filter f tl) =
      hd :: tl
x✝ : Bool
heq✝ : f hd = false
⊢ sizeOf (filter f tl) < 1 + sizeOf hd + sizeOf tl

State before:
case h_1
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
h :
  ¬(match f hd with
      | true => hd :: filter f tl
      | false => filter f tl) =
      hd :: tl
x✝ : Bool
heq✝ : f hd = true
⊢ sizeOf (hd :: filter f tl) < 1 + sizeOf hd + sizeOf tl

case h_2
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
h :
  ¬(match f hd with
      | true => hd :: filter f tl
      | false => filter f tl) =
      hd :: tl
x✝ : Bool
heq✝ : f hd = false
⊢ sizeOf (filter f tl) < 1 + sizeOf hd + sizeOf tl
Tactic:
next hHd =>
  simp [hHd] at h
  simp [_sizeOf_1]
  apply Nat.add_lt_add_left
  apply ih
  assumption
State after:
case h_2
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
h :
  ¬(match f hd with
      | true => hd :: filter f tl
      | false => filter f tl) =
      hd :: tl
x✝ : Bool
heq✝ : f hd = false
⊢ sizeOf (filter f tl) < 1 + sizeOf hd + sizeOf tl

State before:
case h_2
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
h :
  ¬(match f hd with
      | true => hd :: filter f tl
      | false => filter f tl) =
      hd :: tl
x✝ : Bool
heq✝ : f hd = false
⊢ sizeOf (filter f tl) < 1 + sizeOf hd + sizeOf tl
Tactic:
next hHd =>
  clear h hHd
  apply Nat.lt_of_le_of_lt (sizeOf_filter _ _)
  rw [Nat.add_comm, Nat.add_comm 1, Nat.add_one, Nat.add_succ]
  apply Nat.succ_le_succ
  apply Nat.le_add_right
State after:
no goals

State before:
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
h :
  ¬(match f hd with
      | true => hd :: filter f tl
      | false => filter f tl) =
      hd :: tl
x✝ : Bool
hHd : f hd = true
⊢ sizeOf (hd :: filter f tl) < 1 + sizeOf hd + sizeOf tl
Tactic:
simp [hHd] at h
State after:
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
x✝ : Bool
hHd : f hd = true
h : ¬filter f tl = tl
⊢ sizeOf (hd :: filter f tl) < 1 + sizeOf hd + sizeOf tl

State before:
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
x✝ : Bool
hHd : f hd = true
h : ¬filter f tl = tl
⊢ sizeOf (hd :: filter f tl) < 1 + sizeOf hd + sizeOf tl
Tactic:
simp [_sizeOf_1]
State after:
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
x✝ : Bool
hHd : f hd = true
h : ¬filter f tl = tl
⊢ 1 + sizeOf hd + sizeOf (filter f tl) < 1 + sizeOf hd + sizeOf tl

State before:
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
x✝ : Bool
hHd : f hd = true
h : ¬filter f tl = tl
⊢ 1 + sizeOf hd + sizeOf (filter f tl) < 1 + sizeOf hd + sizeOf tl
Tactic:
apply Nat.add_lt_add_left
State after:
case h
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
x✝ : Bool
hHd : f hd = true
h : ¬filter f tl = tl
⊢ sizeOf (filter f tl) < sizeOf tl

State before:
case h
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
x✝ : Bool
hHd : f hd = true
h : ¬filter f tl = tl
⊢ sizeOf (filter f tl) < sizeOf tl
Tactic:
apply ih
State after:
case h
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
x✝ : Bool
hHd : f hd = true
h : ¬filter f tl = tl
⊢ ¬filter f tl = tl

State before:
case h
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
x✝ : Bool
hHd : f hd = true
h : ¬filter f tl = tl
⊢ ¬filter f tl = tl
Tactic:
assumption
State after:
no goals

State before:
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
h :
  ¬(match f hd with
      | true => hd :: filter f tl
      | false => filter f tl) =
      hd :: tl
x✝ : Bool
hHd : f hd = false
⊢ sizeOf (filter f tl) < 1 + sizeOf hd + sizeOf tl
Tactic:
clear h hHd
State after:
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
x✝ : Bool
⊢ sizeOf (filter f tl) < 1 + sizeOf hd + sizeOf tl

State before:
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
x✝ : Bool
⊢ sizeOf (filter f tl) < 1 + sizeOf hd + sizeOf tl
Tactic:
apply Nat.lt_of_le_of_lt (sizeOf_filter _ _)
State after:
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
x✝ : Bool
⊢ sizeOf tl < 1 + sizeOf hd + sizeOf tl

State before:
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
x✝ : Bool
⊢ sizeOf tl < 1 + sizeOf hd + sizeOf tl
Tactic:
rw [Nat.add_comm, Nat.add_comm 1, Nat.add_one, Nat.add_succ]
State after:
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
x✝ : Bool
⊢ sizeOf tl < Nat.succ (sizeOf tl + sizeOf hd)

State before:
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
x✝ : Bool
⊢ sizeOf tl < Nat.succ (sizeOf tl + sizeOf hd)
Tactic:
apply Nat.succ_le_succ
State after:
case a
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
x✝ : Bool
⊢ sizeOf tl ≤ sizeOf tl + sizeOf hd

State before:
case a
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
x✝ : Bool
⊢ sizeOf tl ≤ sizeOf tl + sizeOf hd
Tactic:
apply Nat.le_add_right
State after:
no goals