Theorem: remove_length_le (PnP2023/Lec_03_24/Sampling.lean)

State before:
case nil
α : Type u
inst✝ : DecidableEq α
a : α
⊢ List.length (List.remove a []) ≤ List.length []
Tactic:
simp [List.remove]
State after:
no goals

State before:
case cons
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : List.length (List.remove a t) ≤ List.length t
⊢ List.length (List.remove a (h' :: t)) ≤ List.length (h' :: t)
Tactic:
simp [List.remove]
State after:
case cons
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : List.length (List.remove a t) ≤ List.length t
⊢ List.length (if a = h' then List.remove a t else h' :: List.remove a t) ≤ Nat.succ (List.length t)

State before:
case cons
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : List.length (List.remove a t) ≤ List.length t
⊢ List.length (if a = h' then List.remove a t else h' :: List.remove a t) ≤ Nat.succ (List.length t)
Tactic:
split
State after:
case cons.inl
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : List.length (List.remove a t) ≤ List.length t
h✝ : a = h'
⊢ List.length (List.remove a t) ≤ Nat.succ (List.length t)

case cons.inr
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : List.length (List.remove a t) ≤ List.length t
h✝ : ¬a = h'
⊢ List.length (h' :: List.remove a t) ≤ Nat.succ (List.length t)

State before:
case cons.inl
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : List.length (List.remove a t) ≤ List.length t
h✝ : a = h'
⊢ List.length (List.remove a t) ≤ Nat.succ (List.length t)
Tactic:
apply Nat.le_step
State after:
case cons.inl.h
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : List.length (List.remove a t) ≤ List.length t
h✝ : a = h'
⊢ List.length (List.remove a t) ≤ List.length t

State before:
case cons.inl.h
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : List.length (List.remove a t) ≤ List.length t
h✝ : a = h'
⊢ List.length (List.remove a t) ≤ List.length t
Tactic:
assumption
State after:
no goals

State before:
case cons.inr
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : List.length (List.remove a t) ≤ List.length t
h✝ : ¬a = h'
⊢ List.length (h' :: List.remove a t) ≤ Nat.succ (List.length t)
Tactic:
rw [List.length_cons]
State after:
case cons.inr
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : List.length (List.remove a t) ≤ List.length t
h✝ : ¬a = h'
⊢ Nat.succ (List.length (List.remove a t)) ≤ Nat.succ (List.length t)

State before:
case cons.inr
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : List.length (List.remove a t) ≤ List.length t
h✝ : ¬a = h'
⊢ Nat.succ (List.length (List.remove a t)) ≤ Nat.succ (List.length t)
Tactic:
apply Nat.succ_le_succ
State after:
case cons.inr.a
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : List.length (List.remove a t) ≤ List.length t
h✝ : ¬a = h'
⊢ List.length (List.remove a t) ≤ List.length t

State before:
case cons.inr.a
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : List.length (List.remove a t) ≤ List.length t
h✝ : ¬a = h'
⊢ List.length (List.remove a t) ≤ List.length t
Tactic:
exact ih
State after:
no goals