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

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

State before:
case cons
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: 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 : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: 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 : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: 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 : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: 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 : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: 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 : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: t
h✝ : a = h'
⊢ List.length (List.remove a t) < Nat.succ (List.length t)
Tactic:
apply Nat.lt_succ_of_le
State after:
case cons.inl.a
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: t
h✝ : a = h'
⊢ List.length (List.remove a t) ≤ List.length t

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

State before:
case cons.inr
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: 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 : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: 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 : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: t
h✝ : ¬a = h'
⊢ Nat.succ (List.length (List.remove a t)) < Nat.succ (List.length t)
Tactic:
apply Nat.succ_lt_succ
State after:
case cons.inr.a
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: 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 : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: t
h✝ : ¬a = h'
⊢ List.length (List.remove a t) < List.length t
Tactic:
have in_tail: a ∈ t := by
  have : ¬ a = h' := by assumption
  simp [List.mem_cons, this] at hyp
  assumption
State after:
case cons.inr.a
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: t
h✝ : ¬a = h'
in_tail : a ∈ t
⊢ List.length (List.remove a t) < List.length t

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

State before:
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: t
h✝ : ¬a = h'
⊢ a ∈ t
Tactic:
have : ¬ a = h' := by assumption
State after:
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: t
h✝ this : ¬a = h'
⊢ a ∈ t

State before:
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: t
h✝ this : ¬a = h'
⊢ a ∈ t
Tactic:
simp [List.mem_cons, this] at hyp
State after:
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
h✝ this : ¬a = h'
hyp : a ∈ t
⊢ a ∈ t

State before:
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
h✝ this : ¬a = h'
hyp : a ∈ t
⊢ a ∈ t
Tactic:
assumption
State after:
no goals

State before:
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: t
h✝ : ¬a = h'
⊢ ¬a = h'
Tactic:
assumption
State after:
no goals