[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
⊢ count p 0 = 0
[PROOFSTEP]
rw [count, List.range_zero, List.countp, List.countp.go]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ Fintype { i // i < n ∧ p i }
[PROOFSTEP]
apply Fintype.ofFinset ((Finset.range n).filter p)
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ ∀ (x : ℕ), x ∈ filter p (range n) ↔ x ∈ fun x => x < n ∧ p x
[PROOFSTEP]
intro x
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n x : ℕ
⊢ x ∈ filter p (range n) ↔ x ∈ fun x => x < n ∧ p x
[PROOFSTEP]
rw [mem_filter, mem_range]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n x : ℕ
⊢ x < n ∧ p x ↔ x ∈ fun x => x < n ∧ p x
[PROOFSTEP]
rfl
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n = card (filter p (range n))
[PROOFSTEP]
rw [count, List.countp_eq_length_filter]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ List.length (List.filter (fun b => decide (p b)) (List.range n)) = card (filter p (range n))
[PROOFSTEP]
rfl
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n = Fintype.card { k // k < n ∧ p k }
[PROOFSTEP]
rw [count_eq_card_filter_range, ← Fintype.card_ofFinset, ← CountSet.fintype]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ (Fintype.card ↑fun x => x < n ∧ p x) = Fintype.card { k // k < n ∧ p k }
[PROOFSTEP]
rfl
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p (n + 1) = count p n + if p n then 1 else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
h : p n
⊢ count p (n + 1) = count p n + 1
[PROOFSTEP]
simp [count, List.range_succ, h]
[GOAL]
case neg
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
h : ¬p n
⊢ count p (n + 1) = count p n + 0
[PROOFSTEP]
simp [count, List.range_succ, h]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n ≤ count p (n + 1)
[PROOFSTEP]
by_cases h : p n
[GOAL]
case pos
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
h : p n
⊢ count p n ≤ count p (n + 1)
[PROOFSTEP]
simp [count_succ, h]
[GOAL]
case neg
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
h : ¬p n
⊢ count p n ≤ count p (n + 1)
[PROOFSTEP]
simp [count_succ, h]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ count p (a + b) = count p a + count (fun k => p (a + k)) b
[PROOFSTEP]
have : Disjoint ((range a).filter p) (((range b).map <| addLeftEmbedding a).filter p) :=
  by
  apply disjoint_filter_filter
  rw [Finset.disjoint_left]
  simp_rw [mem_map, mem_range, addLeftEmbedding_apply]
  rintro x hx ⟨c, _, rfl⟩
  exact (self_le_add_right _ _).not_lt hx
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ Disjoint (filter p (range a)) (filter p (map (addLeftEmbedding a) (range b)))
[PROOFSTEP]
apply disjoint_filter_filter
[GOAL]
case a
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ Disjoint (range a) (map (addLeftEmbedding a) (range b))
[PROOFSTEP]
rw [Finset.disjoint_left]
[GOAL]
case a
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ ∀ ⦃a_1 : ℕ⦄, a_1 ∈ range a → ¬a_1 ∈ map (addLeftEmbedding a) (range b)
[PROOFSTEP]
simp_rw [mem_map, mem_range, addLeftEmbedding_apply]
[GOAL]
case a
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ ∀ ⦃a_1 : ℕ⦄, a_1 < a → ¬∃ a_3, a_3 < b ∧ a + a_3 = a_1
[PROOFSTEP]
rintro x hx ⟨c, _, rfl⟩
[GOAL]
case a.intro.intro
p : ℕ → Prop
inst✝ : DecidablePred p
a b c : ℕ
left✝ : c < b
hx : a + c < a
⊢ False
[PROOFSTEP]
exact (self_le_add_right _ _).not_lt hx
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
this : Disjoint (filter p (range a)) (filter p (map (addLeftEmbedding a) (range b)))
⊢ count p (a + b) = count p a + count (fun k => p (a + k)) b
[PROOFSTEP]
simp_rw [count_eq_card_filter_range, range_add, filter_union, card_disjoint_union this, filter_map, addLeftEmbedding,
  card_map]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
this : Disjoint (filter p (range a)) (filter p (map (addLeftEmbedding a) (range b)))
⊢ card (filter p (range a)) +
      card
        (filter (p ∘ ↑{ toFun := fun h => a + h, inj' := (_ : Function.Injective ((fun x x_1 => x + x_1) a)) })
          (range b)) =
    card (filter p (range a)) + card (filter (fun k => p (a + k)) (range b))
[PROOFSTEP]
rfl
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ count p (a + b) = count (fun k => p (k + b)) a + count p b
[PROOFSTEP]
rw [add_comm, count_add, add_comm]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ count (fun k => p (b + k)) a + count p b = count (fun k => p (k + b)) a + count p b
[PROOFSTEP]
simp_rw [add_comm b]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
⊢ count p 1 = if p 0 then 1 else 0
[PROOFSTEP]
simp [count_succ]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p (n + 1) = count (fun k => p (k + 1)) n + if p 0 then 1 else 0
[PROOFSTEP]
rw [count_add', count_one]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n < count p (n + 1) ↔ p n
[PROOFSTEP]
by_cases h : p n
[GOAL]
case pos
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
h : p n
⊢ count p n < count p (n + 1) ↔ p n
[PROOFSTEP]
simp [count_succ, h]
[GOAL]
case neg
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
h : ¬p n
⊢ count p n < count p (n + 1) ↔ p n
[PROOFSTEP]
simp [count_succ, h]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p (n + 1) = count p n + 1 ↔ p n
[PROOFSTEP]
by_cases h : p n
[GOAL]
case pos
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
h : p n
⊢ count p (n + 1) = count p n + 1 ↔ p n
[PROOFSTEP]
simp [h, count_succ]
[GOAL]
case neg
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
h : ¬p n
⊢ count p (n + 1) = count p n + 1 ↔ p n
[PROOFSTEP]
simp [h, count_succ]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p (n + 1) = count p n ↔ ¬p n
[PROOFSTEP]
by_cases h : p n
[GOAL]
case pos
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
h : p n
⊢ count p (n + 1) = count p n ↔ ¬p n
[PROOFSTEP]
simp [h, count_succ]
[GOAL]
case neg
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
h : ¬p n
⊢ count p (n + 1) = count p n ↔ ¬p n
[PROOFSTEP]
simp [h, count_succ]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ ↑(count p n) ≤ Cardinal.mk ↑{k | p k}
[PROOFSTEP]
rw [count_eq_card_fintype, ← Cardinal.mk_fintype]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ Cardinal.mk { k // k < n ∧ p k } ≤ Cardinal.mk ↑{k | p k}
[PROOFSTEP]
exact Cardinal.mk_subtype_mono fun x hx ↦ hx.2
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
m n : ℕ
hm : p m
hn : p n
heq : count p m = count p n
⊢ m = n
[PROOFSTEP]
by_contra' h : m ≠ n
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
m n : ℕ
hm : p m
hn : p n
heq : count p m = count p n
h : m ≠ n
⊢ False
[PROOFSTEP]
wlog hmn : m < n
[GOAL]
case inr
p : ℕ → Prop
inst✝ : DecidablePred p
m n : ℕ
hm : p m
hn : p n
heq : count p m = count p n
h : m ≠ n
this : ∀ {p : ℕ → Prop} [inst : DecidablePred p] {m n : ℕ}, p m → p n → count p m = count p n → m ≠ n → m < n → False
hmn : ¬m < n
⊢ False
[PROOFSTEP]
exact this hn hm heq.symm h.symm (h.lt_or_lt.resolve_left hmn)
[GOAL]
p✝ : ℕ → Prop
inst✝¹ : DecidablePred p✝
p : ℕ → Prop
inst✝ : DecidablePred p
m n : ℕ
hm : p m
hn : p n
heq : count p m = count p n
h : m ≠ n
hmn : m < n
⊢ False
[PROOFSTEP]
simpa [heq] using count_strict_mono hm hmn
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
hp : Set.Finite (setOf p)
n : ℕ
⊢ count p n ≤ card (Set.Finite.toFinset hp)
[PROOFSTEP]
rw [count_eq_card_filter_range]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
hp : Set.Finite (setOf p)
n : ℕ
⊢ card (filter p (range n)) ≤ card (Set.Finite.toFinset hp)
[PROOFSTEP]
exact Finset.card_mono fun x hx ↦ hp.mem_toFinset.2 (mem_filter.1 hx).2
[GOAL]
p : ℕ → Prop
inst✝¹ : DecidablePred p
q : ℕ → Prop
inst✝ : DecidablePred q
n : ℕ
hpq : ∀ (k : ℕ), p k → q k
⊢ count p n ≤ count q n
[PROOFSTEP]
simp only [count_eq_card_filter_range]
[GOAL]
p : ℕ → Prop
inst✝¹ : DecidablePred p
q : ℕ → Prop
inst✝ : DecidablePred q
n : ℕ
hpq : ∀ (k : ℕ), p k → q k
⊢ card (filter p (range n)) ≤ card (filter q (range n))
[PROOFSTEP]
exact card_le_of_subset ((range n).monotone_filter_right hpq)
