[GOAL]
α : Type u_1
l✝ : List α
p q : α → Bool
n : ℕ
l : List α
⊢ countp.go p l n = n + countp.go p l 0
[PROOFSTEP]
induction' l with head tail ih generalizing n
[GOAL]
case nil
α : Type u_1
l : List α
p q : α → Bool
n✝ n : ℕ
⊢ countp.go p [] n = n + countp.go p [] 0
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
l : List α
p q : α → Bool
n✝ : ℕ
head : α
tail : List α
ih : ∀ {n : ℕ}, countp.go p tail n = n + countp.go p tail 0
n : ℕ
⊢ countp.go p (head :: tail) n = n + countp.go p (head :: tail) 0
[PROOFSTEP]
unfold countp.go
[GOAL]
case cons
α : Type u_1
l : List α
p q : α → Bool
n✝ : ℕ
head : α
tail : List α
ih : ∀ {n : ℕ}, countp.go p tail n = n + countp.go p tail 0
n : ℕ
⊢ (bif p head then countp.go p tail (n + 1) else countp.go p tail n) =
    n + bif p head then countp.go p tail (0 + 1) else countp.go p tail 0
[PROOFSTEP]
rw [ih (n := n + 1), ih (n := n), ih (n := 1)]
[GOAL]
case cons
α : Type u_1
l : List α
p q : α → Bool
n✝ : ℕ
head : α
tail : List α
ih : ∀ {n : ℕ}, countp.go p tail n = n + countp.go p tail 0
n : ℕ
⊢ (bif p head then n + 1 + countp.go p tail 0 else n + countp.go p tail 0) =
    n + bif p head then 1 + countp.go p tail 0 else countp.go p tail 0
[PROOFSTEP]
by_cases h : p head
[GOAL]
case pos
α : Type u_1
l : List α
p q : α → Bool
n✝ : ℕ
head : α
tail : List α
ih : ∀ {n : ℕ}, countp.go p tail n = n + countp.go p tail 0
n : ℕ
h : p head = true
⊢ (bif p head then n + 1 + countp.go p tail 0 else n + countp.go p tail 0) =
    n + bif p head then 1 + countp.go p tail 0 else countp.go p tail 0
[PROOFSTEP]
simp [h, add_assoc]
[GOAL]
case neg
α : Type u_1
l : List α
p q : α → Bool
n✝ : ℕ
head : α
tail : List α
ih : ∀ {n : ℕ}, countp.go p tail n = n + countp.go p tail 0
n : ℕ
h : ¬p head = true
⊢ (bif p head then n + 1 + countp.go p tail 0 else n + countp.go p tail 0) =
    n + bif p head then 1 + countp.go p tail 0 else countp.go p tail 0
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
pa : p a = true
⊢ countp p (a :: l) = countp p l + 1
[PROOFSTEP]
have : countp.go p (a :: l) 0 = countp.go p l 1
[GOAL]
case this
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
pa : p a = true
⊢ countp.go p (a :: l) 0 = countp.go p l 1
[PROOFSTEP]
change (bif _ then _ else _) = countp.go _ _ _
[GOAL]
case this
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
pa : p a = true
⊢ (bif p a then countp.go p l (0 + 1) else countp.go p l 0) = countp.go p l 1
[PROOFSTEP]
rw [pa]
[GOAL]
case this
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
pa : p a = true
⊢ (bif true then countp.go p l (0 + 1) else countp.go p l 0) = countp.go p l 1
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
pa : p a = true
this : countp.go p (a :: l) 0 = countp.go p l 1
⊢ countp p (a :: l) = countp p l + 1
[PROOFSTEP]
unfold countp
[GOAL]
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
pa : p a = true
this : countp.go p (a :: l) 0 = countp.go p l 1
⊢ countp.go p (a :: l) 0 = countp.go p l 0 + 1
[PROOFSTEP]
rw [this, add_comm, List.countp_go_eq_add]
[GOAL]
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
pa : ¬p a = true
⊢ countp p (a :: l) = countp p l
[PROOFSTEP]
change (bif _ then _ else _) = countp.go _ _ _
[GOAL]
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
pa : ¬p a = true
⊢ (bif p a then countp.go p l (0 + 1) else countp.go p l 0) = countp.go p l 0
[PROOFSTEP]
rw [Bool.of_not_eq_true pa]
[GOAL]
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
pa : ¬p a = true
⊢ (bif false then countp.go p l (0 + 1) else countp.go p l 0) = countp.go p l 0
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
⊢ countp p (a :: l) = countp p l + if p a = true then 1 else 0
[PROOFSTEP]
by_cases h : p a
[GOAL]
case pos
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
h : p a = true
⊢ countp p (a :: l) = countp p l + if p a = true then 1 else 0
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
h : ¬p a = true
⊢ countp p (a :: l) = countp p l + if p a = true then 1 else 0
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
l✝ : List α
p q : α → Bool
l : List α
⊢ length l = countp p l + countp (fun a => decide ¬p a = true) l
[PROOFSTEP]
induction' l with x h ih
[GOAL]
case nil
α : Type u_1
l : List α
p q : α → Bool
⊢ length [] = countp p [] + countp (fun a => decide ¬p a = true) []
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
l : List α
p q : α → Bool
x : α
h : List α
ih : length h = countp p h + countp (fun a => decide ¬p a = true) h
⊢ length (x :: h) = countp p (x :: h) + countp (fun a => decide ¬p a = true) (x :: h)
[PROOFSTEP]
by_cases h : p x
[GOAL]
case pos
α : Type u_1
l : List α
p q : α → Bool
x : α
h✝ : List α
ih : length h✝ = countp p h✝ + countp (fun a => decide ¬p a = true) h✝
h : p x = true
⊢ length (x :: h✝) = countp p (x :: h✝) + countp (fun a => decide ¬p a = true) (x :: h✝)
[PROOFSTEP]
rw [countp_cons_of_pos _ _ h, countp_cons_of_neg _ _ _, length, ih]
[GOAL]
case pos
α : Type u_1
l : List α
p q : α → Bool
x : α
h✝ : List α
ih : length h✝ = countp p h✝ + countp (fun a => decide ¬p a = true) h✝
h : p x = true
⊢ countp p h✝ + countp (fun a => decide ¬p a = true) h✝ + 1 = countp p h✝ + 1 + countp (fun a => decide ¬p a = true) h✝
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u_1
l : List α
p q : α → Bool
x : α
h✝ : List α
ih : length h✝ = countp p h✝ + countp (fun a => decide ¬p a = true) h✝
h : p x = true
⊢ ¬(decide ¬p x = true) = true
[PROOFSTEP]
simp only [h]
[GOAL]
case neg
α : Type u_1
l : List α
p q : α → Bool
x : α
h✝ : List α
ih : length h✝ = countp p h✝ + countp (fun a => decide ¬p a = true) h✝
h : ¬p x = true
⊢ length (x :: h✝) = countp p (x :: h✝) + countp (fun a => decide ¬p a = true) (x :: h✝)
[PROOFSTEP]
rw [countp_cons_of_pos (fun a => ¬p a) _ _, countp_cons_of_neg _ _ h, length, ih]
[GOAL]
case neg
α : Type u_1
l : List α
p q : α → Bool
x : α
h✝ : List α
ih : length h✝ = countp p h✝ + countp (fun a => decide ¬p a = true) h✝
h : ¬p x = true
⊢ countp p h✝ + countp (fun a => decide ¬p a = true) h✝ + 1 =
    countp p h✝ + (countp (fun a => decide ¬p a = true) h✝ + 1)
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u_1
l : List α
p q : α → Bool
x : α
h✝ : List α
ih : length h✝ = countp p h✝ + countp (fun a => decide ¬p a = true) h✝
h : ¬p x = true
⊢ (fun a => decide ¬p a = true) x = true
[PROOFSTEP]
simp only [h]
[GOAL]
α : Type u_1
l✝ : List α
p q : α → Bool
l : List α
⊢ countp p l = length (filter p l)
[PROOFSTEP]
induction' l with x l ih
[GOAL]
case nil
α : Type u_1
l : List α
p q : α → Bool
⊢ countp p [] = length (filter p [])
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
l✝ : List α
p q : α → Bool
x : α
l : List α
ih : countp p l = length (filter p l)
⊢ countp p (x :: l) = length (filter p (x :: l))
[PROOFSTEP]
by_cases h : p x
[GOAL]
case pos
α : Type u_1
l✝ : List α
p q : α → Bool
x : α
l : List α
ih : countp p l = length (filter p l)
h : p x = true
⊢ countp p (x :: l) = length (filter p (x :: l))
[PROOFSTEP]
rw [countp_cons_of_pos p l h, ih, filter_cons_of_pos l h, length]
[GOAL]
case neg
α : Type u_1
l✝ : List α
p q : α → Bool
x : α
l : List α
ih : countp p l = length (filter p l)
h : ¬p x = true
⊢ countp p (x :: l) = length (filter p (x :: l))
[PROOFSTEP]
rw [countp_cons_of_neg p l h, ih, filter_cons_of_neg l h]
[GOAL]
α : Type u_1
l : List α
p q : α → Bool
⊢ countp p l ≤ length l
[PROOFSTEP]
simpa only [countp_eq_length_filter] using length_filter_le _ _
[GOAL]
α : Type u_1
l : List α
p q : α → Bool
l₁ l₂ : List α
⊢ countp p (l₁ ++ l₂) = countp p l₁ + countp p l₂
[PROOFSTEP]
simp only [countp_eq_length_filter, filter_append, length_append]
[GOAL]
α : Type u_1
l✝ : List α
p q : α → Bool
a : List α
l : List (List α)
⊢ countp p (join (a :: l)) = sum (map (countp p) (a :: l))
[PROOFSTEP]
rw [join, countp_append, map_cons, sum_cons, countp_join l]
[GOAL]
α : Type u_1
l : List α
p q : α → Bool
⊢ 0 < countp p l ↔ ∃ a, a ∈ l ∧ p a = true
[PROOFSTEP]
simp only [countp_eq_length_filter, length_pos_iff_exists_mem, mem_filter, exists_prop]
[GOAL]
α : Type u_1
l : List α
p q : α → Bool
⊢ countp p l = 0 ↔ ∀ (a : α), a ∈ l → ¬p a = true
[PROOFSTEP]
rw [← not_iff_not, ← Ne.def, ← pos_iff_ne_zero, countp_pos]
[GOAL]
α : Type u_1
l : List α
p q : α → Bool
⊢ (∃ a, a ∈ l ∧ p a = true) ↔ ¬∀ (a : α), a ∈ l → ¬p a = true
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
l : List α
p q : α → Bool
⊢ countp p l = length l ↔ ∀ (a : α), a ∈ l → p a = true
[PROOFSTEP]
rw [countp_eq_length_filter, filter_length_eq_length]
[GOAL]
α : Type u_1
l✝ : List α
p q : α → Bool
l : List α
⊢ length (filter p l) < length l ↔ ∃ x, x ∈ l ∧ ¬p x = true
[PROOFSTEP]
simpa [length_eq_countp_add_countp p l, countp_eq_length_filter] using countp_pos (fun x => ¬p x) (l := l)
[GOAL]
α : Type u_1
l : List α
p q : α → Bool
l₁ l₂ : List α
s : l₁ <+ l₂
⊢ countp p l₁ ≤ countp p l₂
[PROOFSTEP]
simpa only [countp_eq_length_filter] using length_le_of_sublist (s.filter p)
[GOAL]
α : Type u_1
l✝ : List α
p q : α → Bool
l : List α
⊢ countp p (filter q l) = countp (fun a => decide (p a = true ∧ q a = true)) l
[PROOFSTEP]
simp only [countp_eq_length_filter, filter_filter]
[GOAL]
α : Type u_1
l : List α
p q : α → Bool
⊢ countp (fun x => true) l = length l
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
l : List α
p q : α → Bool
⊢ countp (fun x => false) l = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_2
l✝ : List α
p✝ q : α → Bool
β : Type u_1
p : β → Bool
f : α → β
a : α
l : List α
⊢ countp p (map f (a :: l)) = countp (p ∘ f) (a :: l)
[PROOFSTEP]
rw [map_cons, countp_cons, countp_cons, countp_map p f l]
[GOAL]
α : Type u_2
l✝ : List α
p✝ q : α → Bool
β : Type u_1
p : β → Bool
f : α → β
a : α
l : List α
⊢ (countp (p ∘ f) l + if p (f a) = true then 1 else 0) = countp (p ∘ f) l + if (p ∘ f) a = true then 1 else 0
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
l : List α
p q : α → Bool
h : ∀ (x : α), x ∈ l → p x = true → q x = true
⊢ countp p l ≤ countp q l
[PROOFSTEP]
induction' l with a l ihl
[GOAL]
case nil
α : Type u_1
l : List α
p q : α → Bool
h✝ : ∀ (x : α), x ∈ l → p x = true → q x = true
h : ∀ (x : α), x ∈ [] → p x = true → q x = true
⊢ countp p [] ≤ countp q []
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
l✝ : List α
p q : α → Bool
h✝ : ∀ (x : α), x ∈ l✝ → p x = true → q x = true
a : α
l : List α
ihl : (∀ (x : α), x ∈ l → p x = true → q x = true) → countp p l ≤ countp q l
h : ∀ (x : α), x ∈ a :: l → p x = true → q x = true
⊢ countp p (a :: l) ≤ countp q (a :: l)
[PROOFSTEP]
rw [forall_mem_cons] at h 
[GOAL]
case cons
α : Type u_1
l✝ : List α
p q : α → Bool
h✝ : ∀ (x : α), x ∈ l✝ → p x = true → q x = true
a : α
l : List α
ihl : (∀ (x : α), x ∈ l → p x = true → q x = true) → countp p l ≤ countp q l
h : (p a = true → q a = true) ∧ ∀ (x : α), x ∈ l → p x = true → q x = true
⊢ countp p (a :: l) ≤ countp q (a :: l)
[PROOFSTEP]
cases' h with ha hl
[GOAL]
case cons.intro
α : Type u_1
l✝ : List α
p q : α → Bool
h : ∀ (x : α), x ∈ l✝ → p x = true → q x = true
a : α
l : List α
ihl : (∀ (x : α), x ∈ l → p x = true → q x = true) → countp p l ≤ countp q l
ha : p a = true → q a = true
hl : ∀ (x : α), x ∈ l → p x = true → q x = true
⊢ countp p (a :: l) ≤ countp q (a :: l)
[PROOFSTEP]
rw [countp_cons, countp_cons]
[GOAL]
case cons.intro
α : Type u_1
l✝ : List α
p q : α → Bool
h : ∀ (x : α), x ∈ l✝ → p x = true → q x = true
a : α
l : List α
ihl : (∀ (x : α), x ∈ l → p x = true → q x = true) → countp p l ≤ countp q l
ha : p a = true → q a = true
hl : ∀ (x : α), x ∈ l → p x = true → q x = true
⊢ (countp p l + if p a = true then 1 else 0) ≤ countp q l + if q a = true then 1 else 0
[PROOFSTEP]
refine' _root_.add_le_add (ihl hl) _
[GOAL]
case cons.intro
α : Type u_1
l✝ : List α
p q : α → Bool
h : ∀ (x : α), x ∈ l✝ → p x = true → q x = true
a : α
l : List α
ihl : (∀ (x : α), x ∈ l → p x = true → q x = true) → countp p l ≤ countp q l
ha : p a = true → q a = true
hl : ∀ (x : α), x ∈ l → p x = true → q x = true
⊢ (if p a = true then 1 else 0) ≤ if q a = true then 1 else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
l✝ : List α
p q : α → Bool
h : ∀ (x : α), x ∈ l✝ → p x = true → q x = true
a : α
l : List α
ihl : (∀ (x : α), x ∈ l → p x = true → q x = true) → countp p l ≤ countp q l
ha : p a = true → q a = true
hl : ∀ (x : α), x ∈ l → p x = true → q x = true
h✝¹ : p a = true
h✝ : q a = true
⊢ 1 ≤ 1
[PROOFSTEP]
simp only [le_rfl, _root_.zero_le]
[GOAL]
case neg
α : Type u_1
l✝ : List α
p q : α → Bool
h : ∀ (x : α), x ∈ l✝ → p x = true → q x = true
a : α
l : List α
ihl : (∀ (x : α), x ∈ l → p x = true → q x = true) → countp p l ≤ countp q l
ha : p a = true → q a = true
hl : ∀ (x : α), x ∈ l → p x = true → q x = true
h✝¹ : p a = true
h✝ : ¬q a = true
⊢ 1 ≤ 0
[PROOFSTEP]
simp only [le_rfl, _root_.zero_le]
[GOAL]
case pos
α : Type u_1
l✝ : List α
p q : α → Bool
h : ∀ (x : α), x ∈ l✝ → p x = true → q x = true
a : α
l : List α
ihl : (∀ (x : α), x ∈ l → p x = true → q x = true) → countp p l ≤ countp q l
ha : p a = true → q a = true
hl : ∀ (x : α), x ∈ l → p x = true → q x = true
h✝¹ : ¬p a = true
h✝ : q a = true
⊢ 0 ≤ 1
[PROOFSTEP]
simp only [le_rfl, _root_.zero_le]
[GOAL]
case neg
α : Type u_1
l✝ : List α
p q : α → Bool
h : ∀ (x : α), x ∈ l✝ → p x = true → q x = true
a : α
l : List α
ihl : (∀ (x : α), x ∈ l → p x = true → q x = true) → countp p l ≤ countp q l
ha : p a = true → q a = true
hl : ∀ (x : α), x ∈ l → p x = true → q x = true
h✝¹ : ¬p a = true
h✝ : ¬q a = true
⊢ 0 ≤ 0
[PROOFSTEP]
simp only [le_rfl, _root_.zero_le]
[GOAL]
case neg
α : Type u_1
l✝ : List α
p q : α → Bool
h : ∀ (x : α), x ∈ l✝ → p x = true → q x = true
a : α
l : List α
ihl : (∀ (x : α), x ∈ l → p x = true → q x = true) → countp p l ≤ countp q l
ha : p a = true → q a = true
hl : ∀ (x : α), x ∈ l → p x = true → q x = true
h✝¹ : p a = true
h✝ : ¬q a = true
⊢ False
[PROOFSTEP]
exact absurd (ha ‹_›) ‹_›
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b : α
l : List α
⊢ count a (b :: l) = count a l + if a = b then 1 else 0
[PROOFSTEP]
conv =>
  simp [count, countp_cons]
  lhs
  simp only [eq_comm]
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b : α
l : List α
| count a (b :: l) = count a l + if a = b then 1 else 0
[PROOFSTEP]
  simp [count, countp_cons]
  lhs
  simp only [eq_comm]
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b : α
l : List α
| count a (b :: l) = count a l + if a = b then 1 else 0
[PROOFSTEP]
  simp [count, countp_cons]
  lhs
  simp only [eq_comm]
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b : α
l : List α
| count a (b :: l) = count a l + if a = b then 1 else 0
[PROOFSTEP]
simp [count, countp_cons]
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b : α
l : List α
| (if b = a then 1 else 0) = if a = b then 1 else 0
[PROOFSTEP]
lhs
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b : α
l : List α
| if b = a then 1 else 0
[PROOFSTEP]
simp only [eq_comm]
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b : α
l : List α
⊢ count a (b :: l) = if a = b then succ (count a l) else count a l
[PROOFSTEP]
simp [count_cons']
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b : α
l : List α
⊢ (count a l + if a = b then 1 else 0) = if a = b then succ (count a l) else count a l
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b : α
l : List α
h✝ : a = b
⊢ count a l + 1 = succ (count a l)
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b : α
l : List α
h✝ : ¬a = b
⊢ count a l + 0 = count a l
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a : α
l : List α
⊢ count a (a :: l) = count a l + 1
[PROOFSTEP]
simp [count_cons']
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
l : List α
⊢ count a (b :: l) = count a l
[PROOFSTEP]
simp [count_cons']
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
l : List α
⊢ a = b → False
[PROOFSTEP]
exact h
[GOAL]
α : Type u_1
l : List α
inst✝ : DecidableEq α
head : α
tail : List α
a : α
h : 0 < length (head :: tail)
⊢ count a (List.tail (head :: tail)) =
    count a (head :: tail) - if a = get (head :: tail) { val := 0, isLt := h } then 1 else 0
[PROOFSTEP]
rw [count_cons']
[GOAL]
α : Type u_1
l : List α
inst✝ : DecidableEq α
head : α
tail : List α
a : α
h : 0 < length (head :: tail)
⊢ count a (List.tail (head :: tail)) =
    (count a tail + if a = head then 1 else 0) - if a = get (head :: tail) { val := 0, isLt := h } then 1 else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
l : List α
inst✝ : DecidableEq α
head : α
tail : List α
a : α
h : 0 < length (head :: tail)
h✝¹ : a = head
h✝ : a = get (head :: tail) { val := 0, isLt := h }
⊢ count a (List.tail (head :: tail)) = count a tail + 1 - 1
[PROOFSTEP]
simp at *
[GOAL]
case neg
α : Type u_1
l : List α
inst✝ : DecidableEq α
head : α
tail : List α
a : α
h : 0 < length (head :: tail)
h✝¹ : a = head
h✝ : ¬a = get (head :: tail) { val := 0, isLt := h }
⊢ count a (List.tail (head :: tail)) = count a tail + 1 - 0
[PROOFSTEP]
simp at *
[GOAL]
case pos
α : Type u_1
l : List α
inst✝ : DecidableEq α
head : α
tail : List α
a : α
h : 0 < length (head :: tail)
h✝¹ : ¬a = head
h✝ : a = get (head :: tail) { val := 0, isLt := h }
⊢ count a (List.tail (head :: tail)) = count a tail + 0 - 1
[PROOFSTEP]
simp at *
[GOAL]
case neg
α : Type u_1
l : List α
inst✝ : DecidableEq α
head : α
tail : List α
a : α
h : 0 < length (head :: tail)
h✝¹ : ¬a = head
h✝ : ¬a = get (head :: tail) { val := 0, isLt := h }
⊢ count a (List.tail (head :: tail)) = count a tail + 0 - 0
[PROOFSTEP]
simp at *
[GOAL]
case neg
α : Type u_1
l : List α
inst✝ : DecidableEq α
head : α
tail : List α
a : α
h : 0 < length (head :: tail)
h✝¹ : a = head
h✝ : ¬a = head
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case pos
α : Type u_1
l : List α
inst✝ : DecidableEq α
head : α
tail : List α
a : α
h : 0 < length (head :: tail)
h✝¹ : ¬a = head
h✝ : a = head
⊢ count a tail = count a tail - 1
[PROOFSTEP]
contradiction
[GOAL]
α : Type u_1
l : List α
inst✝ : DecidableEq α
a : α
⊢ count a [a] = 1
[PROOFSTEP]
rw [count_cons]
[GOAL]
α : Type u_1
l : List α
inst✝ : DecidableEq α
a : α
⊢ (if a = a then succ (count a []) else count a []) = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
l : List α
inst✝ : DecidableEq α
a b : α
⊢ count a [b] = if a = b then 1 else 0
[PROOFSTEP]
rw [count_cons]
[GOAL]
α : Type u_1
l : List α
inst✝ : DecidableEq α
a b : α
⊢ (if a = b then succ (count a []) else count a []) = if a = b then 1 else 0
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a : α
l : List α
⊢ count a (concat l a) = succ (count a l)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a : α
l : List α
⊢ 0 < count a l ↔ a ∈ l
[PROOFSTEP]
simp only [count, countp_pos, beq_iff_eq, exists_eq_right]
[GOAL]
α : Type u_1
l : List α
inst✝ : DecidableEq α
a : α
⊢ count a l = length l ↔ ∀ (b : α), b ∈ l → a = b
[PROOFSTEP]
simp_rw [count, countp_eq_length, beq_iff_eq, eq_comm]
[GOAL]
α : Type u_1
l : List α
inst✝ : DecidableEq α
a b : α
n : ℕ
⊢ count a (replicate n b) = if a = b then n else 0
[PROOFSTEP]
split
[GOAL]
case inl
α : Type u_1
l : List α
inst✝ : DecidableEq α
a b : α
n : ℕ
h✝ : a = b
⊢ count a (replicate n b) = n
case inr α : Type u_1 l : List α inst✝ : DecidableEq α a b : α n : ℕ h✝ : ¬a = b ⊢ count a (replicate n b) = 0
[PROOFSTEP]
exacts [‹a = b› ▸ count_replicate_self _ _, count_eq_zero.2 <| mt eq_of_mem_replicate ‹a ≠ b›]
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
l : List α
a : α
⊢ filter (fun x => x == a) l = replicate (count a l) a
[PROOFSTEP]
simp only [count, countp_eq_length_filter, eq_replicate, mem_filter, beq_iff_eq]
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
l : List α
a : α
⊢ True ∧ ∀ (b : α), b ∈ l ∧ b = a → b = a
[PROOFSTEP]
exact ⟨trivial, fun _ h => h.2⟩
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
l : List α
a : α
⊢ filter (fun x => decide (a = x)) l = replicate (count a l) a
[PROOFSTEP]
simpa only [eq_comm] using filter_eq' l a
[GOAL]
α : Type u_1
l : List α
inst✝ : DecidableEq α
n : ℕ
a : α
h : replicate n a <+ l
⊢ n ≤ count a l
[PROOFSTEP]
simpa only [count_replicate_self] using h.count_le a
[GOAL]
α : Type u_1
l : List α
inst✝ : DecidableEq α
p : α → Bool
a : α
h : p a = true
⊢ count a (filter p l) = count a l
[PROOFSTEP]
rw [count, countp_filter]
[GOAL]
α : Type u_1
l : List α
inst✝ : DecidableEq α
p : α → Bool
a : α
h : p a = true
⊢ countp (fun a_1 => decide ((a_1 == a) = true ∧ p a_1 = true)) l = countp (fun x => x == a) l
[PROOFSTEP]
congr
[GOAL]
case e_p
α : Type u_1
l : List α
inst✝ : DecidableEq α
p : α → Bool
a : α
h : p a = true
⊢ (fun a_1 => decide ((a_1 == a) = true ∧ p a_1 = true)) = fun x => x == a
[PROOFSTEP]
funext b
[GOAL]
case e_p.h
α : Type u_1
l : List α
inst✝ : DecidableEq α
p : α → Bool
a : α
h : p a = true
b : α
⊢ decide ((b == a) = true ∧ p b = true) = (b == a)
[PROOFSTEP]
rw [Bool.beq_eq_decide_eq]
[GOAL]
case e_p.h
α : Type u_1
l : List α
inst✝ : DecidableEq α
p : α → Bool
a : α
h : p a = true
b : α
⊢ decide (decide (b = a) = true ∧ p b = true) = decide (b = a)
[PROOFSTEP]
by_cases hb : b = a
[GOAL]
case pos
α : Type u_1
l : List α
inst✝ : DecidableEq α
p : α → Bool
a : α
h : p a = true
b : α
hb : b = a
⊢ decide (decide (b = a) = true ∧ p b = true) = decide (b = a)
[PROOFSTEP]
simp [hb, h]
[GOAL]
case neg
α : Type u_1
l : List α
inst✝ : DecidableEq α
p : α → Bool
a : α
h : p a = true
b : α
hb : ¬b = a
⊢ decide (decide (b = a) = true ∧ p b = true) = decide (b = a)
[PROOFSTEP]
simp [hb]
[GOAL]
α✝ : Type ?u.43925
l✝ : List α✝
inst✝¹ : DecidableEq α✝
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
l : List α
f : α → List β
x : β
⊢ count x (List.bind l f) = sum (map (count x ∘ f) l)
[PROOFSTEP]
rw [List.bind, count_join, map_map]
[GOAL]
α✝ : Type ?u.44336
l✝ : List α✝
inst✝² : DecidableEq α✝
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
l : List α
f : α → β
hf : Function.Injective f
x : α
⊢ count (f x) (map f l) = count x l
[PROOFSTEP]
simp only [count, countp_map, (· ∘ ·), hf.beq_eq]
[GOAL]
α : Type u_2
l✝ : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
l : List α
f : α → β
x : α
⊢ count x l ≤ count (f x) (map f l)
[PROOFSTEP]
rw [count, count, countp_map]
[GOAL]
α : Type u_2
l✝ : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
l : List α
f : α → β
x : α
⊢ countp (fun x_1 => x_1 == x) l ≤ countp ((fun x_1 => x_1 == f x) ∘ f) l
[PROOFSTEP]
exact countp_mono_left <| by simp (config := { contextual := true })
[GOAL]
α : Type u_2
l✝ : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
l : List α
f : α → β
x : α
⊢ ∀ (x_1 : α), x_1 ∈ l → (x_1 == x) = true → ((fun x_2 => x_2 == f x) ∘ f) x_1 = true
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
α : Type u_1
l : List α
inst✝ : DecidableEq α
a b : α
⊢ count a (List.erase [] b) = count a [] - if a = b then 1 else 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b c : α
l : List α
⊢ count a (List.erase (c :: l) b) = count a (c :: l) - if a = b then 1 else 0
[PROOFSTEP]
rw [erase_cons]
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b c : α
l : List α
⊢ count a (if c = b then l else c :: List.erase l b) = count a (c :: l) - if a = b then 1 else 0
[PROOFSTEP]
by_cases hc : c = b
[GOAL]
case pos
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b c : α
l : List α
hc : c = b
⊢ count a (if c = b then l else c :: List.erase l b) = count a (c :: l) - if a = b then 1 else 0
[PROOFSTEP]
rw [if_pos hc, hc, count_cons', Nat.add_sub_cancel]
[GOAL]
case neg
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b c : α
l : List α
hc : ¬c = b
⊢ count a (if c = b then l else c :: List.erase l b) = count a (c :: l) - if a = b then 1 else 0
[PROOFSTEP]
rw [if_neg hc, count_cons', count_cons', count_erase a b l]
[GOAL]
case neg
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b c : α
l : List α
hc : ¬c = b
⊢ ((count a l - if a = b then 1 else 0) + if a = c then 1 else 0) =
    (count a l + if a = c then 1 else 0) - if a = b then 1 else 0
[PROOFSTEP]
by_cases ha : a = b
[GOAL]
case pos
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b c : α
l : List α
hc : ¬c = b
ha : a = b
⊢ ((count a l - if a = b then 1 else 0) + if a = c then 1 else 0) =
    (count a l + if a = c then 1 else 0) - if a = b then 1 else 0
[PROOFSTEP]
rw [← ha, eq_comm] at hc 
[GOAL]
case pos
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b c : α
l : List α
hc : ¬a = c
ha : a = b
⊢ ((count a l - if a = b then 1 else 0) + if a = c then 1 else 0) =
    (count a l + if a = c then 1 else 0) - if a = b then 1 else 0
[PROOFSTEP]
rw [if_pos ha, if_neg hc, add_zero, add_zero]
[GOAL]
case neg
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b c : α
l : List α
hc : ¬c = b
ha : ¬a = b
⊢ ((count a l - if a = b then 1 else 0) + if a = c then 1 else 0) =
    (count a l + if a = c then 1 else 0) - if a = b then 1 else 0
[PROOFSTEP]
rw [if_neg ha, tsub_zero, tsub_zero]
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a : α
l : List α
⊢ count a (List.erase l a) = count a l - 1
[PROOFSTEP]
rw [count_erase, if_pos rfl]
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
l : List α
⊢ count a (List.erase l b) = count a l
[PROOFSTEP]
rw [count_erase, if_neg ab, tsub_zero]
[GOAL]
α : Type u_2
l : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : Monoid β
a : α
f : α → β
hf : ∀ (a' : α), a' ≠ a → a' ∈ l → f a' = 1
⊢ prod (map f l) = f a ^ count a l
[PROOFSTEP]
induction' l with a' as h generalizing a
[GOAL]
case nil
α : Type u_2
l : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : Monoid β
a✝ : α
f : α → β
hf✝ : ∀ (a' : α), a' ≠ a✝ → a' ∈ l → f a' = 1
a : α
hf : ∀ (a' : α), a' ≠ a → a' ∈ [] → f a' = 1
⊢ prod (map f []) = f a ^ count a []
[PROOFSTEP]
rw [map_nil, prod_nil, count_nil, _root_.pow_zero]
[GOAL]
case cons
α : Type u_2
l : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : Monoid β
a✝ : α
f : α → β
hf✝ : ∀ (a' : α), a' ≠ a✝ → a' ∈ l → f a' = 1
a' : α
as : List α
h : ∀ (a : α), (∀ (a' : α), a' ≠ a → a' ∈ as → f a' = 1) → prod (map f as) = f a ^ count a as
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
⊢ prod (map f (a' :: as)) = f a ^ count a (a' :: as)
[PROOFSTEP]
specialize h a fun a' ha' hfa' => hf a' ha' (mem_cons_of_mem _ hfa')
[GOAL]
case cons
α : Type u_2
l : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : Monoid β
a✝ : α
f : α → β
hf✝ : ∀ (a' : α), a' ≠ a✝ → a' ∈ l → f a' = 1
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : prod (map f as) = f a ^ count a as
⊢ prod (map f (a' :: as)) = f a ^ count a (a' :: as)
[PROOFSTEP]
rw [List.map_cons, List.prod_cons, count_cons, h]
[GOAL]
case cons
α : Type u_2
l : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : Monoid β
a✝ : α
f : α → β
hf✝ : ∀ (a' : α), a' ≠ a✝ → a' ∈ l → f a' = 1
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : prod (map f as) = f a ^ count a as
⊢ f a' * f a ^ count a as = f a ^ if a = a' then succ (count a as) else count a as
[PROOFSTEP]
split_ifs with ha'
[GOAL]
case pos
α : Type u_2
l : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : Monoid β
a✝ : α
f : α → β
hf✝ : ∀ (a' : α), a' ≠ a✝ → a' ∈ l → f a' = 1
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : prod (map f as) = f a ^ count a as
ha' : a = a'
⊢ f a' * f a ^ count a as = f a ^ succ (count a as)
[PROOFSTEP]
rw [ha', _root_.pow_succ]
[GOAL]
case neg
α : Type u_2
l : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : Monoid β
a✝ : α
f : α → β
hf✝ : ∀ (a' : α), a' ≠ a✝ → a' ∈ l → f a' = 1
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : prod (map f as) = f a ^ count a as
ha' : ¬a = a'
⊢ f a' * f a ^ count a as = f a ^ count a as
[PROOFSTEP]
rw [hf a' (Ne.symm ha') (List.mem_cons_self a' as), one_mul]
[GOAL]
α : Type u_1
l : List α
inst✝¹ : DecidableEq α
inst✝ : Monoid α
a : α
h : ∀ (a' : α), a' ≠ a → a' ∈ l → a' = 1
⊢ prod l = prod (map id l)
[PROOFSTEP]
rw [map_id]
