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 []

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)
α : Type u_1
l : List α
p q : α → Bool
h : ∀ (x : α), x ∈ l → p x = true → q x = true
⊢ countp p l ≤ countp q l
induction' l with a l ihl
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)
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)
rw [forall_mem_cons] at h
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)
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)
cases' h with ha hl
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
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)
rw [countp_cons, countp_cons]
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
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
refine' _root_.add_le_add (ihl hl) _
case cons.intro.inl.inr
α : 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
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
split_ifs <;> simp only [le_rfl, _root_.zero_le]
no goals
case cons.intro.inl.inr
α : 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
exact absurd (ha ‹_›) ‹_›
no goals
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 []
rfl