Theorem: List.countP_mono_right (Fifteen/Data/List/Basic.lean)

State before:
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
l l' : List α
hsub : l ⊆ l'
nodup : Nodup l
⊢ countP p l ≤ countP p l'
Tactic:
induction l generalizing l' with
| nil => exact Nat.zero_le _
| cons a l IH =>
  let .cons nodup_head (nodup_tail : l.Nodup) := nodup
  simp only [countP_cons]
  cases hpa : p a <;> simp only [if_pos, if_neg, Nat.add_zero]
  . refine IH (subset_of_cons_subset hsub) nodup_tail
  let l'' := l'.erase a
  have : l ⊆ l'' := fun b h => by
    simp only [List.mem_erase_of_ne (nodup_head b h).symm]
    specialize @hsub b
    simp only [List.mem_cons] at hsub
    exact hsub <| Or.inr h
  specialize IH this nodup_tail
  refine trans (s:=Eq) (Nat.succ_le_succ IH) ?_
  refine Eq.symm <| countP_erase_true ?_ hpa
  exact (cons_subset.mp hsub).1
State after:
no goals

State before:
case nil
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
l' : List α
hsub : [] ⊆ l'
nodup : Nodup []
⊢ countP p [] ≤ countP p l'
Tactic:
exact Nat.zero_le _
State after:
no goals

State before:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
⊢ countP p (a :: l) ≤ countP p l'
Tactic:
let .cons nodup_head (nodup_tail : l.Nodup) := nodup
State after:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
⊢ countP p (a :: l) ≤ countP p l'

State before:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
⊢ countP p (a :: l) ≤ countP p l'
Tactic:
simp only [countP_cons]
State after:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
⊢ (countP p l + if p a = true then 1 else 0) ≤ countP p l'

State before:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
⊢ (countP p l + if p a = true then 1 else 0) ≤ countP p l'
Tactic:
cases hpa : p a <;> simp only [if_pos, if_neg, Nat.add_zero]
State after:
case cons.false
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = false
⊢ countP p l ≤ countP p l'

case cons.true
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
⊢ countP p l + 1 ≤ countP p l'

State before:
case cons.false
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = false
⊢ countP p l ≤ countP p l'

case cons.true
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
⊢ countP p l + 1 ≤ countP p l'
Tactic:
. refine IH (subset_of_cons_subset hsub) nodup_tail
State after:
case cons.true
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
⊢ countP p l + 1 ≤ countP p l'

State before:
case cons.true
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
⊢ countP p l + 1 ≤ countP p l'
Tactic:
let l'' := l'.erase a
State after:
case cons.true
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
l'' : List α := List.erase l' a
⊢ countP p l + 1 ≤ countP p l'

State before:
case cons.true
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
l'' : List α := List.erase l' a
⊢ countP p l + 1 ≤ countP p l'
Tactic:
have : l ⊆ l'' := fun b h => by
  simp only [List.mem_erase_of_ne (nodup_head b h).symm]
  specialize @hsub b
  simp only [List.mem_cons] at hsub
  exact hsub <| Or.inr h
State after:
case cons.true
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
l'' : List α := List.erase l' a
this : l ⊆ l''
⊢ countP p l + 1 ≤ countP p l'

State before:
case cons.true
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
l'' : List α := List.erase l' a
this : l ⊆ l''
⊢ countP p l + 1 ≤ countP p l'
Tactic:
specialize IH this nodup_tail
State after:
case cons.true
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
l'' : List α := List.erase l' a
this : l ⊆ l''
IH : countP p l ≤ countP p l''
⊢ countP p l + 1 ≤ countP p l'

State before:
case cons.true
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
l'' : List α := List.erase l' a
this : l ⊆ l''
IH : countP p l ≤ countP p l''
⊢ countP p l + 1 ≤ countP p l'
Tactic:
refine trans (s:=Eq) (Nat.succ_le_succ IH) ?_
State after:
case cons.true
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
l'' : List α := List.erase l' a
this : l ⊆ l''
IH : countP p l ≤ countP p l''
⊢ Nat.succ (countP p l'') = countP p l'

State before:
case cons.true
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
l'' : List α := List.erase l' a
this : l ⊆ l''
IH : countP p l ≤ countP p l''
⊢ Nat.succ (countP p l'') = countP p l'
Tactic:
refine Eq.symm <| countP_erase_true ?_ hpa
State after:
case cons.true
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
l'' : List α := List.erase l' a
this : l ⊆ l''
IH : countP p l ≤ countP p l''
⊢ a ∈ l'

State before:
case cons.true
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
l'' : List α := List.erase l' a
this : l ⊆ l''
IH : countP p l ≤ countP p l''
⊢ a ∈ l'
Tactic:
exact (cons_subset.mp hsub).1
State after:
no goals

State before:
case cons.false
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = false
⊢ countP p l ≤ countP p l'
Tactic:
refine IH (subset_of_cons_subset hsub) nodup_tail
State after:
no goals

State before:
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
l'' : List α := List.erase l' a
b : α
h : b ∈ l
⊢ b ∈ l''
Tactic:
simp only [List.mem_erase_of_ne (nodup_head b h).symm]
State after:
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
l'' : List α := List.erase l' a
b : α
h : b ∈ l
⊢ b ∈ l'

State before:
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
l'' : List α := List.erase l' a
b : α
h : b ∈ l
⊢ b ∈ l'
Tactic:
specialize @hsub b
State after:
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
l'' : List α := List.erase l' a
b : α
h : b ∈ l
hsub : b ∈ a :: l → b ∈ l'
⊢ b ∈ l'

State before:
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
l'' : List α := List.erase l' a
b : α
h : b ∈ l
hsub : b ∈ a :: l → b ∈ l'
⊢ b ∈ l'
Tactic:
simp only [List.mem_cons] at hsub
State after:
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
l'' : List α := List.erase l' a
b : α
h : b ∈ l
hsub : b = a ∨ b ∈ l → b ∈ l'
⊢ b ∈ l'

State before:
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
l'' : List α := List.erase l' a
b : α
h : b ∈ l
hsub : b = a ∨ b ∈ l → b ∈ l'
⊢ b ∈ l'
Tactic:
exact hsub <| Or.inr h
State after:
no goals