-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem countP_mono_left (h : ∀ x ∈ l, p x → q x) : countP p l ≤ countP q l

Proof state:
case cons.false
α : Type u_1
p q : α → Bool
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
ha : p a = true → q a = true
hl : ∀ (x : α), x ∈ l → p x = true → q x = true
h : p a = false
⊢ countP p l ≤ countP q l + if q a = true then 1 else 0

Tactic:
apply Nat.le_trans ?_ (Nat.le_add_right _ _)

Result:
α : Type u_1
p q : α → Bool
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
ha : p a = true → q a = true
hl : ∀ (x : α), x ∈ l → p x = true → q x = true
h : p a = false
⊢ countP p l ≤ countP q l

Proof state:
case cons
α : Type u_1
p q : α → Bool
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)

Tactic:
rw [forall_mem_cons] at h

Result:
case cons
α : Type u_1
p q : α → Bool
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)

Proof state:
case cons.true
α : Type u_1
p q : α → Bool
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
ha : p a = true → q a = true
hl : ∀ (x : α), x ∈ l → p x = true → q x = true
h : p a = true
⊢ countP p l ≤ countP q l

Tactic:
apply ihl hl

Result:
no goals

Proof state:
case cons.false
α : Type u_1
p q : α → Bool
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
ha : p a = true → q a = true
hl : ∀ (x : α), x ∈ l → p x = true → q x = true
h : p a = false
⊢ (countP p l + if false = true then 1 else 0) ≤ countP q l + if q a = true then 1 else 0

Tactic:
simp only [Bool.false_eq_true, ↓reduceIte, Nat.add_zero]

Result:
case cons.false
α : Type u_1
p q : α → Bool
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
ha : p a = true → q a = true
hl : ∀ (x : α), x ∈ l → p x = true → q x = true
h : p a = false
⊢ countP p l ≤ countP q l + if q a = true then 1 else 0

Proof state:
case cons.true
α : Type u_1
p q : α → Bool
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
ha : p a = true → q a = true
hl : ∀ (x : α), x ∈ l → p x = true → q x = true
h : p a = true
⊢ (countP p l + if true = true then 1 else 0) ≤ countP q l + if q a = true then 1 else 0

Tactic:
simp only [↓reduceIte, ha h, succ_le_succ_iff]

Result:
case cons.true
α : Type u_1
p q : α → Bool
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
ha : p a = true → q a = true
hl : ∀ (x : α), x ∈ l → p x = true → q x = true
h : p a = true
⊢ countP p l ≤ countP q l

Proof state:
case nil
α : Type u_1
p q : α → Bool
h : ∀ (x : α), x ∈ [] → p x = true → q x = true
⊢ countP p [] ≤ countP q []

Tactic:
apply Nat.le_refl

Result:
no goals

Proof state:
α : Type u_1
p q : α → Bool
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
ha : p a = true → q a = true
hl : ∀ (x : α), x ∈ l → p x = true → q x = true
h : p a = false
⊢ countP p l ≤ countP q l

Tactic:
apply ihl hl

Result:
no goals

Proof state:
case cons
α : Type u_1
p q : α → Bool
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)

Tactic:
have ⟨ha, hl⟩ := h

Result:
case cons
α : Type u_1
p q : α → Bool
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
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)

Proof state:
case cons
α : Type u_1
p q : α → Bool
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
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

Tactic:
cases h : p a

Result:
case cons.false
α : Type u_1
p q : α → Bool
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
ha : p a = true → q a = true
hl : ∀ (x : α), x ∈ l → p x = true → q x = true
h : p a = false
⊢ (countP p l + if false = true then 1 else 0) ≤ countP q l + if q a = true then 1 else 0

case cons.true
α : Type u_1
p q : α → Bool
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
ha : p a = true → q a = true
hl : ∀ (x : α), x ∈ l → p x = true → q x = true
h : p a = true
⊢ (countP p l + if true = true then 1 else 0) ≤ countP q l + if q a = true then 1 else 0

Proof state:
case cons
α : Type u_1
p q : α → Bool
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
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)

Tactic:
simp [countP_cons]

Result:
case cons
α : Type u_1
p q : α → Bool
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
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