/-
Copyright (c) 2014 Parikshit Khanna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro

! This file was ported from Lean 3 source module data.list.count
! leanprover-community/mathlib commit 47adfab39a11a072db552f47594bf8ed2cf8a722
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.List.BigOperators.Basic

/-!
# Counting in lists

This file proves basic properties of `List.countp` and `List.count`, which count the number of
elements of a list satisfying a predicate and equal to a given element respectively. Their
definitions can be found in `Std.Data.List.Basic`.
-/


open Nat

variable {
l: List α
l : 
List: Type ?u.24637 → Type ?u.24637
List 
α: ?m.4
α}

namespace List

section Countp

variable (
p: α → Bool
p 
q: α → Bool
q : 
α: ?m.12
α → 
Bool: Type
Bool)

@[simp]
theorem 
countp_nil: ∀ {α : Type u_1} (p : α → Bool), countp p [] = 0
countp_nil : 
countp: {α : Type ?u.43} → (α → Bool) → List α → ℕ
countp 
p: α → Bool
p 
[]: List ?m.49
[] = 
0: ?m.52
0 := 
rfl: ∀ {α : Sort ?u.77} {a : α}, a = a
rfl
#align list.countp_nil 
List.countp_nil: ∀ {α : Type u_1} (p : α → Bool), countp p [] = 0
List.countp_nil

-- Porting note: added to aid in the following proof.
protected theorem 
countp_go_eq_add: ∀ {n : ℕ} (l : List α), countp.go p l n = n + countp.go p l 0
countp_go_eq_add (
l: unknown metavariable '?_uniq.122'
l) : 
countp.go: {α : Type ?u.140} → (α → Bool) → List α → ℕ → ℕ
countp.go 
p: α → Bool
p 
l: ?m.136
l 
n: ?m.133
n = 
n: ?m.133
n + 
countp.go: {α : Type ?u.148} → (α → Bool) → List α → ℕ → ℕ
countp.go 
p: α → Bool
p 
l: ?m.136
l 
0: ?m.154
0 := by
Goals accomplished! 🐙
  
α: Type u_1

l✝: List α

p, q: α → Bool

n: ℕ

l: List α

countp.go p l n = n + countp.go p l 0induction' 
l: List α
l with 
head: ?m.226
head 
tail: List ?m.226
tail 
ih: ?m.227 tail
ih generalizing 
n: ℕ
n
α: Type u_1

l: List α

p, q: α → Bool

n✝, n: ℕ

nil
countp.go p [] n = n + countp.go p [] 0
α: 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: ℕ

cons
countp.go p (head :: tail) n = n + countp.go p (head :: tail) 0
  
α: Type u_1

l✝: List α

p, q: α → Bool

n: ℕ

l: List α

countp.go p l n = n + countp.go p l 0·
α: Type u_1

l: List α

p, q: α → Bool

n✝, n: ℕ

nil
countp.go p [] n = n + countp.go p [] 0 
α: Type u_1

l: List α

p, q: α → Bool

n✝, n: ℕ

nil
countp.go p [] n = n + countp.go p [] 0
α: 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: ℕ

cons
countp.go p (head :: tail) n = n + countp.go p (head :: tail) 0rfl
Goals accomplished! 🐙
  
α: Type u_1

l✝: List α

p, q: α → Bool

n: ℕ

l: List α

countp.go p l n = n + countp.go p l 0·
α: 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: ℕ

cons
countp.go p (head :: tail) n = n + countp.go p (head :: tail) 0 
α: 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: ℕ

cons
countp.go p (head :: tail) n = n + countp.go p (head :: tail) 0unfold 
countp.go: {α : Type u_1} → (α → Bool) → List α → ℕ → ℕ
countp.go
α: 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: ℕ

cons
(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
    
α: 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: ℕ

cons
countp.go p (head :: tail) n = n + countp.go p (head :: tail) 0rw [
α: 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: ℕ

cons
(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
ih: ?m.227 tail
ih (n := 
n: ℕ
n + 
1: ?m.1047
1),
α: 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: ℕ

cons
(bif p head then n + 1 + countp.go p tail 0 else countp.go p tail n) =   n + bif p head then countp.go p tail (0 + 1) else countp.go p tail 0 
α: 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: ℕ

cons
(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
ih: ?m.227 tail
ih (n := 
n: ℕ
n),
α: 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: ℕ

cons
(bif p head then n + 1 + countp.go p tail 0 else n + countp.go p tail 0) =   n + bif p head then countp.go p tail (0 + 1) else countp.go p tail 0 
α: 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: ℕ

cons
(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
ih: ?m.227 tail
ih (n := 
1: ?m.1120
1)
α: 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: ℕ

cons
(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]
α: 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: ℕ

cons
(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
    
α: 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: ℕ

cons
countp.go p (head :: tail) n = n + countp.go p (head :: tail) 0by_cases 
h: ?m.1236
h : 
p: α → Bool
p 
head: ?m.226
head
α: 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

pos
(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
α: 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

neg
(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
    
α: 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: ℕ

cons
countp.go p (head :: tail) n = n + countp.go p (head :: tail) 0·
α: 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

pos
(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 
α: 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

pos
(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
α: 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

neg
(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 0simp [
h: ?m.1236
h, 
add_assoc: ∀ {G : Type ?u.1251} [inst : AddSemigroup G] (a b c : G), a + b + c = a + (b + c)
add_assoc]
Goals accomplished! 🐙
    
α: 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: ℕ

cons
countp.go p (head :: tail) n = n + countp.go p (head :: tail) 0·
α: 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

neg
(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 
α: 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

neg
(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 0simp [
h: ?m.1243
h]
Goals accomplished! 🐙

@[simp]
theorem 
countp_cons_of_pos: ∀ {α : Type u_1} (p : α → Bool) {a : α} (l : List α), p a = true → countp p (a :: l) = countp p l + 1
countp_cons_of_pos {
a: α
a : 
α: ?m.1478
α} (
l: List α
l) (
pa: p a = true
pa : 
p: α → Bool
p 
a: α
a) : 
countp: {α : Type ?u.1511} → (α → Bool) → List α → ℕ
countp 
p: α → Bool
p (
a: α
a :: 
l: ?m.1494
l) = 
countp: {α : Type ?u.1522} → (α → Bool) → List α → ℕ
countp 
p: α → Bool
p 
l: ?m.1494
l + 
1: ?m.1528
1 := by
Goals accomplished! 🐙
  
α: Type u_1

l✝: List α

p, q: α → Bool

a: α

l: List α

pa: p a = true

countp p (a :: l) = countp p l + 1have : 
countp.go: {α : Type ?u.1596} → (α → Bool) → List α → ℕ → ℕ
countp.go 
p: α → Bool
p (
a: α
a :: 
l: List α
l) 
0: ?m.1605
0 = 
countp.go: {α : Type ?u.1611} → (α → Bool) → List α → ℕ → ℕ
countp.go 
p: α → Bool
p 
l: List α
l 
1: ?m.1617
1
α: 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
α: 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
  
α: Type u_1

l✝: List α

p, q: α → Bool

a: α

l: List α

pa: p a = true

countp p (a :: l) = countp p l + 1·
α: 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 
α: 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
α: 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 + 1change (bif 
_: Bool
_ then 
_: ?m.1628
_ else 
_: ?m.1628
_) = 
countp.go: {α : Type ?u.1632} → (α → Bool) → List α → ℕ → ℕ
countp.go 
_: ?m.1633 → Bool
_ 
_: List ?m.1633
_ 
_: ℕ
_
α: Type u_1

l✝: List α

p, q: α → Bool

a: α

l: List α

pa: p a = true

this
(bif p a then countp.go p l (0 + 1) else countp.go p l 0) = countp.go p l 1
    
α: 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 1rw [
α: Type u_1

l✝: List α

p, q: α → Bool

a: α

l: List α

pa: p a = true

this
(bif p a then countp.go p l (0 + 1) else countp.go p l 0) = countp.go p l 1
pa: p a = true
pa
α: Type u_1

l✝: List α

p, q: α → Bool

a: α

l: List α

pa: p a = true

this
(bif true then countp.go p l (0 + 1) else countp.go p l 0) = countp.go p l 1]
α: Type u_1

l✝: List α

p, q: α → Bool

a: α

l: List α

pa: p a = true

this
(bif true then countp.go p l (0 + 1) else countp.go p l 0) = countp.go p l 1
    
α: 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 1rfl
Goals accomplished! 🐙
  
α: Type u_1

l✝: List α

p, q: α → Bool

a: α

l: List α

pa: p a = true

countp p (a :: l) = countp p l + 1unfold 
countp: {α : Type u_1} → (α → Bool) → List α → ℕ
countp
α: 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
  
α: Type u_1

l✝: List α

p, q: α → Bool

a: α

l: List α

pa: p a = true

countp p (a :: l) = countp p l + 1rw [
α: 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
this: countp.go p (a :: l) 0 = countp.go p l 1
this,
α: 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 l 1 = countp.go p l 0 + 1 
α: 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
add_comm: ∀ {G : Type ?u.1722} [inst : AddCommSemigroup G] (a b : G), a + b = b + a
add_comm,
α: 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 l 1 = 1 + countp.go p l 0 
α: 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
List.countp_go_eq_add: ∀ {α : Type ?u.1757} (p : α → Bool) {n : ℕ} (l : List α), countp.go p l n = n + countp.go p l 0
List.countp_go_eq_add
α: 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

1 + countp.go p l 0 = 1 + countp.go p l 0]
Goals accomplished! 🐙
#align list.countp_cons_of_pos 
List.countp_cons_of_pos: ∀ {α : Type u_1} (p : α → Bool) {a : α} (l : List α), p a = true → countp p (a :: l) = countp p l + 1
List.countp_cons_of_pos

@[simp]
theorem 
countp_cons_of_neg: ∀ {α : Type u_1} (p : α → Bool) {a : α} (l : List α), ¬p a = true → countp p (a :: l) = countp p l
countp_cons_of_neg {
a: α
a : 
α: ?m.1804
α} (
l: List α
l) (
pa: ¬p a = true
pa : ¬
p: α → Bool
p 
a: α
a) : 
countp: {α : Type ?u.1905} → (α → Bool) → List α → ℕ
countp 
p: α → Bool
p (
a: α
a :: 
l: ?m.1820
l) = 
countp: {α : Type ?u.1913} → (α → Bool) → List α → ℕ
countp 
p: α → Bool
p 
l: ?m.1820
l := by
Goals accomplished! 🐙
  
α: Type u_1

l✝: List α

p, q: α → Bool

a: α

l: List α

pa: ¬p a = true

countp p (a :: l) = countp p lchange (bif 
_: Bool
_ then 
_: ?m.1928
_ else 
_: ?m.1928
_) = 
countp.go: {α : Type ?u.1932} → (α → Bool) → List α → ℕ → ℕ
countp.go 
_: ?m.1933 → Bool
_ 
_: List ?m.1933
_ 
_: ℕ
_
α: 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
  
α: Type u_1

l✝: List α

p, q: α → Bool

a: α

l: List α

pa: ¬p a = true

countp p (a :: l) = countp p lrw [
α: 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
Bool.of_not_eq_true: ∀ {b : Bool}, ¬b = true → b = false
Bool.of_not_eq_true 
pa: ¬p a = true
pa
α: 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]
α: 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
  
α: Type u_1

l✝: List α

p, q: α → Bool

a: α

l: List α

pa: ¬p a = true

countp p (a :: l) = countp p lrfl
Goals accomplished! 🐙
#align list.countp_cons_of_neg 
List.countp_cons_of_neg: ∀ {α : Type u_1} (p : α → Bool) {a : α} (l : List α), ¬p a = true → countp p (a :: l) = countp p l
List.countp_cons_of_neg

theorem 
countp_cons: ∀ {α : Type u_1} (p : α → Bool) (a : α) (l : List α), countp p (a :: l) = countp p l + if p a = true then 1 else 0
countp_cons (
a: α
a : 
α: ?m.2092
α) (
l: List α
l) : 
countp: {α : Type ?u.2112} → (α → Bool) → List α → ℕ
countp 
p: α → Bool
p (
a: α
a :: 
l: ?m.2108
l) = 
countp: {α : Type ?u.2123} → (α → Bool) → List α → ℕ
countp 
p: α → Bool
p 
l: ?m.2108
l + if 
p: α → Bool
p 
a: α
a then 
1: ?m.2212
1 else 
0: ?m.2223
0 := by
Goals accomplished! 🐙
  
α: 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 0by_cases 
h: ?m.2397
h : 
p: α → Bool
p 
a: α
a
α: Type u_1

l✝: List α

p, q: α → Bool

a: α

l: List α

h: p a = true

pos
countp p (a :: l) = countp p l + if p a = true then 1 else 0
α: Type u_1

l✝: List α

p, q: α → Bool

a: α

l: List α

h: ¬p a = true

neg
countp p (a :: l) = countp p l + if p a = true then 1 else 0 
α: 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<;>
α: Type u_1

l✝: List α

p, q: α → Bool

a: α

l: List α

h: p a = true

pos
countp p (a :: l) = countp p l + if p a = true then 1 else 0
α: Type u_1

l✝: List α

p, q: α → Bool

a: α

l: List α

h: ¬p a = true

neg
countp p (a :: l) = countp p l + if p a = true then 1 else 0 
α: 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 0simp [
h: ?m.2404
h]
Goals accomplished! 🐙
#align list.countp_cons 
List.countp_cons: ∀ {α : Type u_1} (p : α → Bool) (a : α) (l : List α), countp p (a :: l) = countp p l + if p a = true then 1 else 0
List.countp_cons

theorem 
length_eq_countp_add_countp: ∀ (l : List α), length l = countp p l + countp (fun a => decide ¬p a = true) l
length_eq_countp_add_countp (
l: ?m.2765
l) : 
length: {α : Type ?u.2769} → List α → ℕ
length 
l: ?m.2765
l = 
countp: {α : Type ?u.2776} → (α → Bool) → List α → ℕ
countp 
p: α → Bool
p 
l: ?m.2765
l + 
countp: {α : Type ?u.2782} → (α → Bool) → List α → ℕ
countp (fun 
a: ?m.2785
a => ¬
p: α → Bool
p 
a: ?m.2785
a) 
l: ?m.2765
l := by
Goals accomplished! 🐙
  
α: Type u_1

l✝: List α

p, q: α → Bool

l: List α

length l = countp p l + countp (fun a => decide ¬p a = true) linduction' 
l: List α
l with 
x: ?m.2960
x 
h: List ?m.2960
h 
ih: ?m.2961 h
ih
α: Type u_1

l: List α

p, q: α → Bool

nil
length [] = countp p [] + countp (fun a => decide ¬p a = true) []
α: 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

cons
length (x :: h) = countp p (x :: h) + countp (fun a => decide ¬p a = true) (x :: h)
  
α: Type u_1

l✝: List α

p, q: α → Bool

l: List α

length l = countp p l + countp (fun a => decide ¬p a = true) l·
α: Type u_1

l: List α

p, q: α → Bool

nil
length [] = countp p [] + countp (fun a => decide ¬p a = true) [] 
α: Type u_1

l: List α

p, q: α → Bool

nil
length [] = countp p [] + countp (fun a => decide ¬p a = true) []
α: 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

cons
length (x :: h) = countp p (x :: h) + countp (fun a => decide ¬p a = true) (x :: h)rfl
Goals accomplished! 🐙
  
α: Type u_1

l✝: List α

p, q: α → Bool

l: List α

length l = countp p l + countp (fun a => decide ¬p a = true) lby_cases 
h: ?m.3097
h : 
p: α → Bool
p 
x: ?m.2960
x
α: 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

pos
length (x :: h✝) = countp p (x :: h✝) + countp (fun a => decide ¬p a = true) (x :: h✝)
α: 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

neg
length (x :: h✝) = countp p (x :: h✝) + countp (fun a => decide ¬p a = true) (x :: h✝)
  
α: Type u_1

l✝: List α

p, q: α → Bool

l: List α

length l = countp p l + countp (fun a => decide ¬p a = true) l·
α: 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

pos
length (x :: h✝) = countp p (x :: h✝) + countp (fun a => decide ¬p a = true) (x :: h✝) 
α: 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

pos
length (x :: h✝) = countp p (x :: h✝) + countp (fun a => decide ¬p a = true) (x :: h✝)
α: 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

neg
length (x :: h✝) = countp p (x :: h✝) + countp (fun a => decide ¬p a = true) (x :: h✝)rw [
α: 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

pos
length (x :: h✝) = countp p (x :: h✝) + countp (fun a => decide ¬p a = true) (x :: h✝)
countp_cons_of_pos: ∀ {α : Type ?u.3110} (p : α → Bool) {a : α} (l : List α), p a = true → countp p (a :: l) = countp p l + 1
countp_cons_of_pos 
_: ?m.3111 → Bool
_ 
_: List ?m.3111
_ 
h: ?m.3097
h,
α: 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

pos
length (x :: h✝) = countp p h✝ + 1 + countp (fun a => decide ¬p a = true) (x :: h✝) 
α: 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

pos
length (x :: h✝) = countp p (x :: h✝) + countp (fun a => decide ¬p a = true) (x :: h✝)
countp_cons_of_neg: ∀ {α : Type ?u.3134} (p : α → Bool) {a : α} (l : List α), ¬p a = true → countp p (a :: l) = countp p l
countp_cons_of_neg 
_: ?m.3135 → Bool
_ 
_: List ?m.3135
_ 
_: ¬?m.3136 ?m.3137 = true
_,
α: 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

pos
length (x :: h✝) = countp p h✝ + 1 + countp (fun a => decide ¬p a = true) h✝
α: 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 
α: 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

pos
length (x :: h✝) = countp p (x :: h✝) + countp (fun a => decide ¬p a = true) (x :: h✝)
length: {α : Type ?u.3414} → List α → ℕ
length,
α: 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

pos
length h✝ + 1 = countp p h✝ + 1 + countp (fun a => decide ¬p a = true) h✝
α: 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 
α: 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

pos
length (x :: h✝) = countp p (x :: h✝) + countp (fun a => decide ¬p a = true) (x :: h✝)
ih: ?m.2961 h✝
ih
α: 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

pos
countp p h✝ + countp (fun a => decide ¬p a = true) h✝ + 1 = countp p h✝ + 1 + countp (fun a => decide ¬p a = true) h✝
α: 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]
α: 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

pos
countp p h✝ + countp (fun a => decide ¬p a = true) h✝ + 1 = countp p h✝ + 1 + countp (fun a => decide ¬p a = true) h✝
α: 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
    
α: 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

pos
length (x :: h✝) = countp p (x :: h✝) + countp (fun a => decide ¬p a = true) (x :: h✝)·
α: 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

pos
countp p h✝ + countp (fun a => decide ¬p a = true) h✝ + 1 = countp p h✝ + 1 + countp (fun a => decide ¬p a = true) h✝ 
α: 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

pos
countp p h✝ + countp (fun a => decide ¬p a = true) h✝ + 1 = countp p h✝ + 1 + countp (fun a => decide ¬p a = true) h✝
α: 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) = trueac_rfl
Goals accomplished! 🐙
    
α: 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

pos
length (x :: h✝) = countp p (x :: h✝) + countp (fun a => decide ¬p a = true) (x :: h✝)·
α: 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 
α: 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) = truesimp only [
h: ?m.3097
h]
Goals accomplished! 🐙
  
α: Type u_1

l✝: List α

p, q: α → Bool

l: List α

length l = countp p l + countp (fun a => decide ¬p a = true) l·
α: 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

neg
length (x :: h✝) = countp p (x :: h✝) + countp (fun a => decide ¬p a = true) (x :: h✝) 
α: 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

neg
length (x :: h✝) = countp p (x :: h✝) + countp (fun a => decide ¬p a = true) (x :: h✝)rw [
α: 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

neg
length (x :: h✝) = countp p (x :: h✝) + countp (fun a => decide ¬p a = true) (x :: h✝)
countp_cons_of_pos: ∀ {α : Type ?u.3844} (p : α → Bool) {a : α} (l : List α), p a = true → countp p (a :: l) = countp p l + 1
countp_cons_of_pos (fun 
a: ?m.3847
a => ¬
p: α → Bool
p 
a: ?m.3847
a) 
_: List ?m.3845
_ 
_: (fun a => decide ¬p a = true) ?m.3955 = true
_,
α: 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

neg
length (x :: h✝) = countp p (x :: h✝) + (countp (fun a => decide ¬p a = true) h✝ + 1)
α: 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 
α: 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

neg
length (x :: h✝) = countp p (x :: h✝) + countp (fun a => decide ¬p a = true) (x :: h✝)
countp_cons_of_neg: ∀ {α : Type ?u.3963} (p : α → Bool) {a : α} (l : List α), ¬p a = true → countp p (a :: l) = countp p l
countp_cons_of_neg 
_: ?m.3964 → Bool
_ 
_: List ?m.3964
_ 
h: ?m.3104
h,
α: 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

neg
length (x :: h✝) = countp p h✝ + (countp (fun a => decide ¬p a = true) h✝ + 1)
α: 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 
α: 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

neg
length (x :: h✝) = countp p (x :: h✝) + countp (fun a => decide ¬p a = true) (x :: h✝)
length: {α : Type ?u.3988} → List α → ℕ
length,
α: 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

neg
length h✝ + 1 = countp p h✝ + (countp (fun a => decide ¬p a = true) h✝ + 1)
α: 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 
α: 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

neg
length (x :: h✝) = countp p (x :: h✝) + countp (fun a => decide ¬p a = true) (x :: h✝)
ih: ?m.2961 h✝
ih
α: 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

neg
countp p h✝ + countp (fun a => decide ¬p a = true) h✝ + 1 = countp p h✝ + (countp (fun a => decide ¬p a = true) h✝ + 1)
α: 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]
α: 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

neg
countp p h✝ + countp (fun a => decide ¬p a = true) h✝ + 1 = countp p h✝ + (countp (fun a => decide ¬p a = true) h✝ + 1)
α: 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
    
α: 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

neg
length (x :: h✝) = countp p (x :: h✝) + countp (fun a => decide ¬p a = true) (x :: h✝)·
α: 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

neg
countp p h✝ + countp (fun a => decide ¬p a = true) h✝ + 1 = countp p h✝ + (countp (fun a => decide ¬p a = true) h✝ + 1) 
α: 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

neg
countp p h✝ + countp (fun a => decide ¬p a = true) h✝ + 1 = countp p h✝ + (countp (fun a => decide ¬p a = true) h✝ + 1)
α: 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 = trueac_rfl
Goals accomplished! 🐙
    
α: 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

neg
length (x :: h✝) = countp p (x :: h✝) + countp (fun a => decide ¬p a = true) (x :: h✝)·
α: 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 
α: 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 = truesimp only [
h: ?m.3104
h]
Goals accomplished! 🐙
#align list.length_eq_countp_add_countp 
List.length_eq_countp_add_countp: ∀ {α : Type u_1} (p : α → Bool) (l : List α), length l = countp p l + countp (fun a => decide ¬p a = true) l
List.length_eq_countp_add_countp

theorem 
countp_eq_length_filter: ∀ (l : List α), countp p l = length (filter p l)
countp_eq_length_filter (
l: ?m.4236
l) : 
countp: {α : Type ?u.4240} → (α → Bool) → List α → ℕ
countp 
p: α → Bool
p 
l: ?m.4236
l = 
length: {α : Type ?u.4246} → List α → ℕ
length (
filter: {α : Type ?u.4248} → (α → Bool) → List α → List α
filter 
p: α → Bool
p 
l: ?m.4236
l) := by
Goals accomplished! 🐙
  
α: Type u_1

l✝: List α

p, q: α → Bool

l: List α

countp p l = length (filter p l)induction' 
l: List α
l with 
x: ?m.4277
x 
l: List ?m.4277
l 
ih: ?m.4278 l
ih
α: Type u_1

l: List α

p, q: α → Bool

nil
countp p [] = length (filter p [])
α: Type u_1

l✝: List α

p, q: α → Bool

x: α

l: List α

ih: countp p l = length (filter p l)

cons
countp p (x :: l) = length (filter p (x :: l))
  
α: Type u_1

l✝: List α

p, q: α → Bool

l: List α

countp p l = length (filter p l)·
α: Type u_1

l: List α

p, q: α → Bool

nil
countp p [] = length (filter p []) 
α: Type u_1

l: List α

p, q: α → Bool

nil
countp p [] = length (filter p [])
α: Type u_1

l✝: List α

p, q: α → Bool

x: α

l: List α

ih: countp p l = length (filter p l)

cons
countp p (x :: l) = length (filter p (x :: l))rfl
Goals accomplished! 🐙
  
α: Type u_1

l✝: List α

p, q: α → Bool

l: List α

countp p l = length (filter p l)by_cases 
h: ?m.4412
h : 
p: α → Bool
p 
x: ?m.4277
x
α: Type u_1

l✝: List α

p, q: α → Bool

x: α

l: List α

ih: countp p l = length (filter p l)

h: p x = true

pos
countp p (x :: l) = length (filter p (x :: l))
α: Type u_1

l✝: List α

p, q: α → Bool

x: α

l: List α

ih: countp p l = length (filter p l)

h: ¬p x = true

neg
countp p (x :: l) = length (filter p (x :: l))
  
α: Type u_1

l✝: List α

p, q: α → Bool

l: List α

countp p l = length (filter p l)·
α: Type u_1

l✝: List α

p, q: α → Bool

x: α

l: List α

ih: countp p l = length (filter p l)

h: p x = true

pos
countp p (x :: l) = length (filter p (x :: l)) 
α: Type u_1

l✝: List α

p, q: α → Bool

x: α

l: List α

ih: countp p l = length (filter p l)

h: p x = true

pos
countp p (x :: l) = length (filter p (x :: l))
α: Type u_1

l✝: List α

p, q: α → Bool

x: α

l: List α

ih: countp p l = length (filter p l)

h: ¬p x = true

neg
countp p (x :: l) = length (filter p (x :: l))rw [
α: Type u_1

l✝: List α

p, q: α → Bool

x: α

l: List α

ih: countp p l = length (filter p l)

h: p x = true

pos
countp p (x :: l) = length (filter p (x :: l))
countp_cons_of_pos: ∀ {α : Type ?u.4425} (p : α → Bool) {a : α} (l : List α), p a = true → countp p (a :: l) = countp p l + 1
countp_cons_of_pos 
p: α → Bool
p 
l: List ?m.4277
l 
h: ?m.4412
h,
α: Type u_1

l✝: List α

p, q: α → Bool

x: α

l: List α

ih: countp p l = length (filter p l)

h: p x = true

pos
countp p l + 1 = length (filter p (x :: l)) 
α: Type u_1

l✝: List α

p, q: α → Bool

x: α

l: List α

ih: countp p l = length (filter p l)

h: p x = true

pos
countp p (x :: l) = length (filter p (x :: l))
ih: ?m.4278 l
ih,
α: Type u_1

l✝: List α

p, q: α → Bool

x: α

l: List α

ih: countp p l = length (filter p l)

h: p x = true

pos
length (filter p l) + 1 = length (filter p (x :: l)) 
α: Type u_1

l✝: List α

p, q: α → Bool

x: α

l: List α

ih: countp p l = length (filter p l)

h: p x = true

pos
countp p (x :: l) = length (filter p (x :: l))
filter_cons_of_pos: ∀ {α : Type ?u.4443} {p : α → Bool} {a : α} (l : List α), p a = true → filter p (a :: l) = a :: filter p l
filter_cons_of_pos 
l: List ?m.4277
l 
h: ?m.4412
h,
α: Type u_1

l✝: List α

p, q: α → Bool

x: α

l: List α

ih: countp p l = length (filter p l)

h: p x = true

pos
length (filter p l) + 1 = length (x :: filter p l) 
α: Type u_1

l✝: List α

p, q: α → Bool

x: α

l: List α

ih: countp p l = length (filter p l)

h: p x = true

pos
countp p (x :: l) = length (filter p (x :: l))
length: {α : Type ?u.4472} → List α → ℕ
length
α: Type u_1

l✝: List α

p, q: α → Bool

x: α

l: List α

ih: countp p l = length (filter p l)

h: p x = true

pos
length (filter p l) + 1 = length (filter p l) + 1]
Goals accomplished! 🐙
  
α: Type u_1

l✝: List α

p, q: α → Bool

l: List α

countp p l = length (filter p l)·
α: Type u_1

l✝: List α

p, q: α → Bool

x: α

l: List α

ih: countp p l = length (filter p l)

h: ¬p x = true

neg
countp p (x :: l) = length (filter p (x :: l)) 
α: Type u_1

l✝: List α

p, q: α → Bool

x: α

l: List α

ih: countp p l = length (filter p l)

h: ¬p x = true

neg
countp p (x :: l) = length (filter p (x :: l))rw [
α: Type u_1

l✝: List α

p, q: α → Bool

x: α

l: List α

ih: countp p l = length (filter p l)

h: ¬p x = true

neg
countp p (x :: l) = length (filter p (x :: l))
countp_cons_of_neg: ∀ {α : Type ?u.4477} (p : α → Bool) {a : α} (l : List α), ¬p a = true → countp p (a :: l) = countp p l
countp_cons_of_neg 
p: α → Bool
p 
l: List ?m.4277
l 
h: ?m.4419
h,
α: Type u_1

l✝: List α

p, q: α → Bool

x: α

l: List α

ih: countp p l = length (filter p l)

h: ¬p x = true

neg
countp p l = length (filter p (x :: l)) 
α: Type u_1

l✝: List α

p, q: α → Bool

x: α

l: List α

ih: countp p l = length (filter p l)

h: ¬p x = true

neg
countp p (x :: l) = length (filter p (x :: l))
ih: ?m.4278 l
ih,
α: Type u_1

l✝: List α

p, q: α → Bool

x: α

l: List α

ih: countp p l = length (filter p l)

h: ¬p x = true

neg
length (filter p l) = length (filter p (x :: l)) 
α: Type u_1

l✝: List α

p, q: α → Bool

x: α

l: List α

ih: countp p l = length (filter p l)

h: ¬p x = true

neg
countp p (x :: l) = length (filter p (x :: l))
filter_cons_of_neg: ∀ {α : Type ?u.4490} {p : α → Bool} {a : α} (l : List α), ¬p a = true → filter p (a :: l) = filter p l
filter_cons_of_neg 
l: List ?m.4277
l 
h: ?m.4419
h
α: Type u_1

l✝: List α

p, q: α → Bool

x: α

l: List α

ih: countp p l = length (filter p l)

h: ¬p x = true

neg
length (filter p l) = length (filter p l)]
Goals accomplished! 🐙
#align list.countp_eq_length_filter 
List.countp_eq_length_filter: ∀ {α : Type u_1} (p : α → Bool) (l : List α), countp p l = length (filter p l)
List.countp_eq_length_filter

theorem 
countp_le_length: countp p l ≤ length l
countp_le_length : 
countp: {α : Type ?u.4538} → (α → Bool) → List α → ℕ
countp 
p: α → Bool
p 
l: List α
l ≤ 
l: List α
l.
length: {α : Type ?u.4544} → List α → ℕ
length := by
Goals accomplished! 🐙
  
α: Type u_1

l: List α

p, q: α → Bool

countp p l ≤ length lsimpa only [
countp_eq_length_filter: ∀ {α : Type ?u.4566} (p : α → Bool) (l : List α), countp p l = length (filter p l)
countp_eq_length_filter] using 
length_filter_le: ∀ {α : Type ?u.4629} (p : α → Bool) (l : List α), length (filter p l) ≤ length l
length_filter_le 
_: ?m.4630 → Bool
_ 
_: List ?m.4630
_
Goals accomplished! 🐙
#align list.countp_le_length 
List.countp_le_length: ∀ {α : Type u_1} {l : List α} (p : α → Bool), countp p l ≤ length l
List.countp_le_length

@[simp]
theorem 
countp_append: ∀ {α : Type u_1} (p : α → Bool) (l₁ l₂ : List α), countp p (l₁ ++ l₂) = countp p l₁ + countp p l₂
countp_append (
l₁: ?m.4684
l₁ 
l₂: List α
l₂) : 
countp: {α : Type ?u.4691} → (α → Bool) → List α → ℕ
countp 
p: α → Bool
p (
l₁: ?m.4684
l₁ ++ 
l₂: ?m.4687
l₂) = 
countp: {α : Type ?u.4739} → (α → Bool) → List α → ℕ
countp 
p: α → Bool
p 
l₁: ?m.4684
l₁ + 
countp: {α : Type ?u.4744} → (α → Bool) → List α → ℕ
countp 
p: α → Bool
p 
l₂: ?m.4687
l₂ := by
Goals accomplished! 🐙
  
α: Type u_1

l: List α

p, q: α → Bool

l₁, l₂: List α

countp p (l₁ ++ l₂) = countp p l₁ + countp p l₂simp only [
countp_eq_length_filter: ∀ {α : Type ?u.4803} (p : α → Bool) (l : List α), countp p l = length (filter p l)
countp_eq_length_filter, 
filter_append: ∀ {α : Type ?u.4815} {p : α → Bool} (l₁ l₂ : List α), filter p (l₁ ++ l₂) = filter p l₁ ++ filter p l₂
filter_append, 
length_append: ∀ {α : Type ?u.4836} (as bs : List α), length (as ++ bs) = length as + length bs
length_append]
Goals accomplished! 🐙
#align list.countp_append 
List.countp_append: ∀ {α : Type u_1} (p : α → Bool) (l₁ l₂ : List α), countp p (l₁ ++ l₂) = countp p l₁ + countp p l₂
List.countp_append

theorem 
countp_join: ∀ {α : Type u_1} (p : α → Bool) (l : List (List α)), countp p (join l) = sum (map (countp p) l)
countp_join : ∀ 
l: List (List α)
l : 
List: Type ?u.5029 → Type ?u.5029
List (
List: Type ?u.5030 → Type ?u.5030
List 
α: ?m.5014
α), 
countp: {α : Type ?u.5034} → (α → Bool) → List α → ℕ
countp 
p: α → Bool
p 
l: List (List α)
l.
join: {α : Type ?u.5039} → List (List α) → List α
join = (
l: List (List α)
l.
map: {α : Type ?u.5045} → {β : Type ?u.5044} → (α → β) → List α → List β
map (
countp: {α : Type ?u.5052} → (α → Bool) → List α → ℕ
countp 
p: α → Bool
p)).
sum: {α : Type ?u.5062} → [inst : Add α] → [inst : Zero α] → List α → α
sum
  | [] => 
rfl: ∀ {α : Sort ?u.5111} {a : α}, a = a
rfl
  | 
a: List α
a :: 
l: List (List α)
l => by
Goals accomplished! 🐙 
α: Type u_1

l✝: List α

p, q: α → Bool

a: List α

l: List (List α)

countp p (join (a :: l)) = sum (map (countp p) (a :: l))rw [
α: Type u_1

l✝: List α

p, q: α → Bool

a: List α

l: List (List α)

countp p (join (a :: l)) = sum (map (countp p) (a :: l))
join: {α : Type ?u.5522} → List (List α) → List α
join,
α: Type u_1

l✝: List α

p, q: α → Bool

a: List α

l: List (List α)

countp p (a ++ join l) = sum (map (countp p) (a :: l)) 
α: Type u_1

l✝: List α

p, q: α → Bool

a: List α

l: List (List α)

countp p (join (a :: l)) = sum (map (countp p) (a :: l))
countp_append: ∀ {α : Type ?u.5523} (p : α → Bool) (l₁ l₂ : List α), countp p (l₁ ++ l₂) = countp p l₁ + countp p l₂
countp_append,
α: Type u_1

l✝: List α

p, q: α → Bool

a: List α

l: List (List α)

countp p a + countp p (join l) = sum (map (countp p) (a :: l)) 
α: Type u_1

l✝: List α

p, q: α → Bool

a: List α

l: List (List α)

countp p (join (a :: l)) = sum (map (countp p) (a :: l))
map_cons: ∀ {α : Type ?u.5545} {β : Type ?u.5546} (f : α → β) (a : α) (l : List α), map f (a :: l) = f a :: map f l
map_cons,
α: Type u_1

l✝: List α

p, q: α → Bool

a: List α

l: List (List α)

countp p a + countp p (join l) = sum (countp p a :: map (countp p) l) 
α: Type u_1

l✝: List α

p, q: α → Bool

a: List α

l: List (List α)

countp p (join (a :: l)) = sum (map (countp p) (a :: l))
sum_cons: ∀ {M : Type ?u.5565} [inst : AddMonoid M] {l : List M} {a : M}, sum (a :: l) = a + sum l
sum_cons,
α: Type u_1

l✝: List α

p, q: α → Bool

a: List α

l: List (List α)

countp p a + countp p (join l) = countp p a + sum (map (countp p) l) 
α: Type u_1

l✝: List α

p, q: α → Bool

a: List α

l: List (List α)

countp p (join (a :: l)) = sum (map (countp p) (a :: l))
countp_join: ∀ (l : List (List α)), countp p (join l) = sum (map (countp p) l)
countp_join 
l: List (List α)
l
α: Type u_1

l✝: List α

p, q: α → Bool

a: List α

l: List (List α)

countp p a + sum (map (countp p) l) = countp p a + sum (map (countp p) l)]
Goals accomplished! 🐙
#align list.countp_join 
List.countp_join: ∀ {α : Type u_1} (p : α → Bool) (l : List (List α)), countp p (join l) = sum (map (countp p) l)
List.countp_join

theorem 
countp_pos: ∀ {α : Type u_1} {l : List α} (p : α → Bool), 0 < countp p l ↔ ∃ a, a ∈ l ∧ p a = true
countp_pos : 
0: ?m.5714
0 < 
countp: {α : Type ?u.5729} → (α → Bool) → List α → ℕ
countp 
p: α → Bool
p 
l: List α
l ↔ ∃ 
a: ?m.5756
a ∈ 
l: List α
l, 
p: α → Bool
p 
a: ?m.5756
a := by
Goals accomplished! 🐙
  
α: Type u_1

l: List α

p, q: α → Bool

0 < countp p l ↔ ∃ a, a ∈ l ∧ p a = truesimp only [
countp_eq_length_filter: ∀ {α : Type ?u.5868} (p : α → Bool) (l : List α), countp p l = length (filter p l)
countp_eq_length_filter, 
length_pos_iff_exists_mem: ∀ {α : Type ?u.5880} {l : List α}, 0 < length l ↔ ∃ a, a ∈ l
length_pos_iff_exists_mem, 
mem_filter: ∀ {α : Type ?u.5899} {x : α} {p : α → Bool} {as : List α}, x ∈ filter p as ↔ x ∈ as ∧ p x = true
mem_filter, 
exists_prop: ∀ {b a : Prop}, (∃ _h, b) ↔ a ∧ b
exists_prop]
Goals accomplished! 🐙
#align list.countp_pos 
List.countp_pos: ∀ {α : Type u_1} {l : List α} (p : α → Bool), 0 < countp p l ↔ ∃ a, a ∈ l ∧ p a = true
List.countp_pos

@[simp]
theorem 
countp_eq_zero: ∀ {α : Type u_1} {l : List α} (p : α → Bool), countp p l = 0 ↔ ∀ (a : α), a ∈ l → ¬p a = true
countp_eq_zero : 
countp: {α : Type ?u.6177} → (α → Bool) → List α → ℕ
countp 
p: α → Bool
p 
l: List α
l = 
0: ?m.6184
0 ↔ ∀ 
a: ?m.6209
a ∈ 
l: List α
l, ¬
p: α → Bool
p 
a: ?m.6209
a := by
Goals accomplished! 🐙
  
α: Type u_1

l: List α

p, q: α → Bool

countp p l = 0 ↔ ∀ (a : α), a ∈ l → ¬p a = truerw [
α: Type u_1

l: List α

p, q: α → Bool

countp p l = 0 ↔ ∀ (a : α), a ∈ l → ¬p a = true← 
not_iff_not: ∀ {a b : Prop}, (¬a ↔ ¬b) ↔ (a ↔ b)
not_iff_not,
α: Type u_1

l: List α

p, q: α → Bool

¬countp p l = 0 ↔ ¬∀ (a : α), a ∈ l → ¬p a = true 
α: Type u_1

l: List α

p, q: α → Bool

countp p l = 0 ↔ ∀ (a : α), a ∈ l → ¬p a = true← 
Ne.def: ∀ {α : Sort ?u.6334} (a b : α), (a ≠ b) = ¬a = b
Ne.def,
α: Type u_1

l: List α

p, q: α → Bool

countp p l ≠ 0 ↔ ¬∀ (a : α), a ∈ l → ¬p a = true 
α: Type u_1

l: List α

p, q: α → Bool

countp p l = 0 ↔ ∀ (a : α), a ∈ l → ¬p a = true← 
pos_iff_ne_zero: ∀ {α : Type ?u.6357} [inst : CanonicallyOrderedAddMonoid α] {a : α}, 0 < a ↔ a ≠ 0
pos_iff_ne_zero,
α: Type u_1

l: List α

p, q: α → Bool

0 < countp p l ↔ ¬∀ (a : α), a ∈ l → ¬p a = true 
α: Type u_1

l: List α

p, q: α → Bool

countp p l = 0 ↔ ∀ (a : α), a ∈ l → ¬p a = true
countp_pos: ∀ {α : Type ?u.6396} {l : List α} (p : α → Bool), 0 < countp p l ↔ ∃ a, a ∈ l ∧ p a = true
countp_pos
α: Type u_1

l: List α

p, q: α → Bool

(∃ a, a ∈ l ∧ p a = true) ↔ ¬∀ (a : α), a ∈ l → ¬p a = true]
α: Type u_1

l: List α

p, q: α → Bool

(∃ a, a ∈ l ∧ p a = true) ↔ ¬∀ (a : α), a ∈ l → ¬p a = true
  
α: Type u_1

l: List α

p, q: α → Bool

countp p l = 0 ↔ ∀ (a : α), a ∈ l → ¬p a = truesimp
Goals accomplished! 🐙
#align list.countp_eq_zero 
List.countp_eq_zero: ∀ {α : Type u_1} {l : List α} (p : α → Bool), countp p l = 0 ↔ ∀ (a : α), a ∈ l → ¬p a = true
List.countp_eq_zero

@[simp]
theorem 
countp_eq_length: ∀ {α : Type u_1} {l : List α} (p : α → Bool), countp p l = length l ↔ ∀ (a : α), a ∈ l → p a = true
countp_eq_length : 
countp: {α : Type ?u.10489} → (α → Bool) → List α → ℕ
countp 
p: α → Bool
p 
l: List α
l = 
l: List α
l.
length: {α : Type ?u.10495} → List α → ℕ
length ↔ ∀ 
a: ?m.10501
a ∈ 
l: List α
l, 
p: α → Bool
p 
a: ?m.10501
a := by
Goals accomplished! 🐙
  
α: Type u_1

l: List α

p, q: α → Bool

countp p l = length l ↔ ∀ (a : α), a ∈ l → p a = truerw [
α: Type u_1

l: List α

p, q: α → Bool

countp p l = length l ↔ ∀ (a : α), a ∈ l → p a = true
countp_eq_length_filter: ∀ {α : Type ?u.10547} (p : α → Bool) (l : List α), countp p l = length (filter p l)
countp_eq_length_filter,
α: Type u_1

l: List α

p, q: α → Bool

length (filter p l) = length l ↔ ∀ (a : α), a ∈ l → p a = true 
α: Type u_1

l: List α

p, q: α → Bool

countp p l = length l ↔ ∀ (a : α), a ∈ l → p a = true
filter_length_eq_length: ∀ {α : Type ?u.10566} {p : α → Bool} {l : List α}, length (filter p l) = length l ↔ ∀ (a : α), a ∈ l → p a = true
filter_length_eq_length
α: Type u_1

l: List α

p, q: α → Bool

(∀ (a : α), a ∈ l → p a = true) ↔ ∀ (a : α), a ∈ l → p a = true]
Goals accomplished! 🐙
#align list.countp_eq_length 
List.countp_eq_length: ∀ {α : Type u_1} {l : List α} (p : α → Bool), countp p l = length l ↔ ∀ (a : α), a ∈ l → p a = true
List.countp_eq_length

theorem 
length_filter_lt_length_iff_exists: ∀ {α : Type u_1} (p : α → Bool) (l : List α), length (filter p l) < length l ↔ ∃ x, x ∈ l ∧ ¬p x = true
length_filter_lt_length_iff_exists (
l: List α
l) :
    
length: {α : Type ?u.10648} → List α → ℕ
length (
filter: {α : Type ?u.10650} → (α → Bool) → List α → List α
filter 
p: α → Bool
p 
l: ?m.10644
l) < 
length: {α : Type ?u.10657} → List α → ℕ
length 
l: ?m.10644
l ↔ ∃ 
x: ?m.10668
x ∈ 
l: ?m.10644
l, ¬
p: α → Bool
p 
x: ?m.10668
x := by
Goals accomplished! 🐙
  
α: Type u_1

l✝: List α

p, q: α → Bool

l: List α

length (filter p l) < length l ↔ ∃ x, x ∈ l ∧ ¬p x = truesimpa [
length_eq_countp_add_countp: ∀ {α : Type ?u.10772} (p : α → Bool) (l : List α), length l = countp p l + countp (fun a => decide ¬p a = true) l
length_eq_countp_add_countp 
p: α → Bool
p 
l: List α
l, 
countp_eq_length_filter: ∀ {α : Type ?u.10780} (p : α → Bool) (l : List α), countp p l = length (filter p l)
countp_eq_length_filter] using
  
countp_pos: ∀ {α : Type ?u.14239} {l : List α} (p : α → Bool), 0 < countp p l ↔ ∃ a, a ∈ l ∧ p a = true
countp_pos (fun 
x: ?m.14243
x => ¬
p: α → Bool
p 
x: ?m.14243
x) (l := 
l: List α
l)
Goals accomplished! 🐙
#align list.length_filter_lt_length_iff_exists 
List.length_filter_lt_length_iff_exists: ∀ {α : Type u_1} (p : α → Bool) (l : List α), length (filter p l) < length l ↔ ∃ x, x ∈ l ∧ ¬p x = true
List.length_filter_lt_length_iff_exists

theorem 
Sublist.countp_le: ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → countp p l₁ ≤ countp p l₂
Sublist.countp_le (
s: l₁ <+ l₂
s : 
l₁: ?m.17378
l₁ <+ 
l₂: ?m.17386
l₂) : 
countp: {α : Type ?u.17396} → (α → Bool) → List α → ℕ
countp 
p: α → Bool
p 
l₁: ?m.17378
l₁ ≤ 
countp: {α : Type ?u.17402} → (α → Bool) → List α → ℕ
countp 
p: α → Bool
p 
l₂: ?m.17386
l₂ := by
Goals accomplished! 🐙
  
α: Type u_1

l: List α

p, q: α → Bool

l₁, l₂: List α

s: l₁ <+ l₂

countp p l₁ ≤ countp p l₂simpa only [
countp_eq_length_filter: ∀ {α : Type ?u.17432} (p : α → Bool) (l : List α), countp p l = length (List.filter p l)
countp_eq_length_filter] using 
length_le_of_sublist: ∀ {α : Type ?u.17503} {l₁ l₂ : List α}, l₁ <+ l₂ → length l₁ ≤ length l₂
length_le_of_sublist (
s: l₁ <+ l₂
s.
filter: ∀ {α : Type ?u.17507} (p : α → Bool) {l₁ l₂ : List α}, l₁ <+ l₂ → List.filter p l₁ <+ List.filter p l₂
filter 
p: α → Bool
p)
Goals accomplished! 🐙
#align list.sublist.countp_le 
List.Sublist.countp_le: ∀ {α : Type u_1} (p : α → Bool) {l₁ l₂ : List α}, l₁ <+ l₂ → countp p l₁ ≤ countp p l₂
List.Sublist.countp_le

@[simp]
theorem 
countp_filter: ∀ {α : Type u_1} (p q : α → Bool) (l : List α),
  countp p (filter q l) = countp (fun a => decide (p a = true ∧ q a = true)) l
countp_filter (
l: List α
l : 
List: Type ?u.17554 → Type ?u.17554
List 
α: ?m.17540
α) : 
countp: {α : Type ?u.17558} → (α → Bool) → List α → ℕ
countp 
p: α → Bool
p (
filter: {α : Type ?u.17563} → (α → Bool) → List α → List α
filter 
q: α → Bool
q 
l: List α
l) = 
countp: {α : Type ?u.17569} → (α → Bool) → List α → ℕ
countp (fun 
a: ?m.17572
a => 
p: α → Bool
p 
a: ?m.17572
a ∧ 
q: α → Bool
q 
a: ?m.17572
a) 
l: List α
l := by
Goals accomplished! 🐙
  
α: 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)) lsimp only [
countp_eq_length_filter: ∀ {α : Type ?u.17766} (p : α → Bool) (l : List α), countp p l = length (filter p l)
countp_eq_length_filter, 
filter_filter: ∀ {α : Type ?u.17778} {p : α → Bool} (q : α → Bool) (l : List α),
  filter p (filter q l) = filter (fun a => decide (p a = true ∧ q a = true)) l
filter_filter]
Goals accomplished! 🐙
#align list.countp_filter 
List.countp_filter: ∀ {α : Type u_1} (p q : α → Bool) (l : List α),
  countp p (filter q l) = countp (fun a => decide (p a = true ∧ q a = true)) l
List.countp_filter

@[simp]
theorem 
countp_true: ∀ {α : Type u_1} {l : List α}, countp (fun x => true) l = length l
countp_true : (
l: List α
l.
countp: {α : Type ?u.17956} → (α → Bool) → List α → ℕ
countp fun 
_: ?m.17962
_ => 
true: Bool
true) = 
l: List α
l.
length: {α : Type ?u.17966} → List α → ℕ
length := by
Goals accomplished! 🐙 
α: Type u_1

l: List α

p, q: α → Bool

countp (fun x => true) l = length lsimp
Goals accomplished! 🐙
#align list.countp_true 
List.countp_true: ∀ {α : Type u_1} {l : List α}, countp (fun x => true) l = length l
List.countp_true

@[simp]
theorem 
countp_false: ∀ {α : Type u_1} {l : List α}, countp (fun x => false) l = 0
countp_false : (
l: List α
l.
countp: {α : Type ?u.19913} → (α → Bool) → List α → ℕ
countp fun 
_: ?m.19919
_ => 
false: Bool
false) = 
0: ?m.19924
0 := by
Goals accomplished! 🐙 
α: Type u_1

l: List α

p, q: α → Bool

countp (fun x => false) l = 0simp
Goals accomplished! 🐙
#align list.countp_false 
List.countp_false: ∀ {α : Type u_1} {l : List α}, countp (fun x => false) l = 0
List.countp_false

@[simp]
theorem 
countp_map: ∀ {β : Type u_1} (p : β → Bool) (f : α → β) (l : List α), countp p (map f l) = countp (p ∘ f) l
countp_map (
p: β → Bool
p : 
β: ?m.21906
β → 
Bool: Type
Bool) (
f: α → β
f : 
α: ?m.21890
α → 
β: ?m.21906
β) :
    ∀ 
l: ?m.21918
l, 
countp: {α : Type ?u.21922} → (α → Bool) → List α → ℕ
countp 
p: β → Bool
p (
map: {α : Type ?u.21928} → {β : Type ?u.21927} → (α → β) → List α → List β
map 
f: α → β
f 
l: ?m.21918
l) = 
countp: {α : Type ?u.21936} → (α → Bool) → List α → ℕ
countp (
p: β → Bool
p ∘ 
f: α → β
f) 
l: ?m.21918
l
  | [] => 
rfl: ∀ {α : Sort ?u.21974} {a : α}, a = a
rfl
  | 
a: α
a :: 
l: List α
l => by
Goals accomplished! 🐙 
α: 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)rw [
α: 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)
map_cons: ∀ {α : Type ?u.22125} {β : Type ?u.22126} (f : α → β) (a : α) (l : List α), map f (a :: l) = f a :: map f l
map_cons,
α: Type u_2

l✝: List α

p✝, q: α → Bool

β: Type u_1

p: β → Bool

f: α → β

a: α

l: List α

countp p (f a :: map f l) = countp (p ∘ f) (a :: l) 
α: 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)
countp_cons: ∀ {α : Type ?u.22149} (p : α → Bool) (a : α) (l : List α), countp p (a :: l) = countp p l + if p a = true then 1 else 0
countp_cons,
α: Type u_2

l✝: List α

p✝, q: α → Bool

β: Type u_1

p: β → Bool

f: α → β

a: α

l: List α

(countp p (map f l) + if p (f a) = true then 1 else 0) = countp (p ∘ f) (a :: l) 
α: 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)
countp_cons: ∀ {α : Type ?u.22173} (p : α → Bool) (a : α) (l : List α), countp p (a :: l) = countp p l + if p a = true then 1 else 0
countp_cons,
α: Type u_2

l✝: List α

p✝, q: α → Bool

β: Type u_1

p: β → Bool

f: α → β

a: α

l: List α

(countp p (map f l) + if p (f a) = true then 1 else 0) = countp (p ∘ f) l + if (p ∘ f) a = true then 1 else 0 
α: 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)
countp_map: ∀ {β : Type u_1} (p : β → Bool) (f : α → β) (l : List α), countp p (map f l) = countp (p ∘ f) l
countp_map 
p: β → Bool
p 
f: α → β
f 
l: List α
l
α: 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]
α: 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;
α: 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 
α: 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)rfl
Goals accomplished! 🐙
#align list.countp_map 
List.countp_map: ∀ {α : Type u_2} {β : Type u_1} (p : β → Bool) (f : α → β) (l : List α), countp p (map f l) = countp (p ∘ f) l
List.countp_map

variable {
p: ?m.22344
p 
q: ?m.22347
q}

theorem 
countp_mono_left: ∀ {α : Type u_1} {l : List α} {p q : α → Bool}, (∀ (x : α), x ∈ l → p x = true → q x = true) → countp p l ≤ countp q l
countp_mono_left (
h: ∀ (x : α), x ∈ l → p x = true → q x = true
h : ∀ 
x: ?m.22367
x ∈ 
l: List α
l, 
p: α → Bool
p 
x: ?m.22367
x → 
q: α → Bool
q 
x: ?m.22367
x) : 
countp: {α : Type ?u.22423} → (α → Bool) → List α → ℕ
countp 
p: α → Bool
p 
l: List α
l ≤ 
countp: {α : Type ?u.22429} → (α → Bool) → List α → ℕ
countp 
q: α → Bool
q 
l: List α
l := by
Goals accomplished! 🐙
  
α: Type u_1

l: List α

p, q: α → Bool

h: ∀ (x : α), x ∈ l → p x = true → q x = true

countp p l ≤ countp q linduction' 
l: List α
l with 
a: ?m.22463
a 
l: List ?m.22463
l 
ihl: ?m.22464 l
ihl
α: 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

nil
countp p [] ≤ countp q []
α: 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

cons
countp p (a :: l) ≤ countp q (a :: l)
  
α: Type u_1

l: List α

p, q: α → Bool

h: ∀ (x : α), x ∈ l → p x = true → q x = true

countp p l ≤ countp q l·
α: 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

nil
countp p [] ≤ countp q [] 
α: 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

nil
countp p [] ≤ countp q []
α: 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

cons
countp p (a :: l) ≤ countp q (a :: l)rfl
Goals accomplished! 🐙
  
α: Type u_1

l: List α

p, q: α → Bool

h: ∀ (x : α), x ∈ l → p x = true → q x = true

countp p l ≤ countp q lrw [
α: 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

cons
countp p (a :: l) ≤ countp q (a :: l)
forall_mem_cons: ∀ {α : Type ?u.22569} {p : α → Prop} {a : α} {l : List α}, (∀ (x : α), x ∈ a :: l → p x) ↔ p a ∧ ∀ (x : α), x ∈ l → p x
forall_mem_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

cons
countp p (a :: l) ≤ countp q (a :: l)]
α: 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

cons
countp p (a :: l) ≤ countp q (a :: l) at 
h: ∀ (x : α), x ∈ a :: l → p x = true → q x = true
h
α: 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

cons
countp p (a :: l) ≤ countp q (a :: l)
  
α: Type u_1

l: List α

p, q: α → Bool

h: ∀ (x : α), x ∈ l → p x = true → q x = true

countp p l ≤ countp q lcases' 
h: (p a = true → q a = true) ∧ ∀ (x : α), x ∈ l → p x = true → q x = true
h with 
ha: ?m.22682
ha 
hl: ?m.22683
hl
α: 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

cons.intro
countp p (a :: l) ≤ countp q (a :: l)
  
α: Type u_1

l: List α

p, q: α → Bool

h: ∀ (x : α), x ∈ l → p x = true → q x = true

countp p l ≤ countp q lrw [
α: 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

cons.intro
countp p (a :: l) ≤ countp q (a :: l)
countp_cons: ∀ {α : Type ?u.22711} (p : α → Bool) (a : α) (l : List α), countp p (a :: l) = countp p l + if p a = true then 1 else 0
countp_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

ha: p a = true → q a = true

hl: ∀ (x : α), x ∈ l → p x = true → q x = true

cons.intro
(countp p l + if p a = true then 1 else 0) ≤ countp q (a :: l) 
α: 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

cons.intro
countp p (a :: l) ≤ countp q (a :: l)
countp_cons: ∀ {α : Type ?u.22723} (p : α → Bool) (a : α) (l : List α), countp p (a :: l) = countp p l + if p a = true then 1 else 0
countp_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

ha: p a = true → q a = true

hl: ∀ (x : α), x ∈ l → p x = true → q x = true

cons.intro
(countp p l + if p a = true then 1 else 0) ≤ countp q l + if q a = true then 1 else 0]
α: 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

cons.intro
(countp p l + if p a = true then 1 else 0) ≤ countp q l + if q a = true then 1 else 0
  
α: Type u_1

l: List α

p, q: α → Bool

h: ∀ (x : α), x ∈ l → p x = true → q x = true

countp p l ≤ countp q lrefine' 
_root_.add_le_add: ∀ {α : Type ?u.22791} [inst : Add α] [inst_1 : Preorder α]
  [inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
  [inst_3 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b c d : α},
  a ≤ b → c ≤ d → a + c ≤ b + d
_root_.add_le_add (
ihl: ?m.22464 l
ihl 
hl: ?m.22683
hl) 
_: ?m.22799 ≤ ?m.22800
_
α: 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

cons.intro
(if p a = true then 1 else 0) ≤ if q a = true then 1 else 0
  
α: Type u_1

l: List α

p, q: α → Bool

h: ∀ (x : α), x ∈ l → p x = true → q x = true

countp p l ≤ countp q lsplit_ifs
α: 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

cons.intro.inl.inl
1 ≤ 1
α: 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

cons.intro.inl.inr
1 ≤ 0
α: 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

cons.intro.inr.inl
0 ≤ 1
α: 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

cons.intro.inr.inr
0 ≤ 0 
α: 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 =