Theorem: List.isInfix_count_le (One.lean)

State before:
α : Type u_1
inst✝ : BEq α
a : α
l₁ l₂ : List α
h : l₁ <:+: l₂
⊢ count a l₁ ≤ count a l₂
Tactic:
unfold count
State after:
α : Type u_1
inst✝ : BEq α
a : α
l₁ l₂ : List α
h : l₁ <:+: l₂
⊢ countp (fun x => x == a) l₁ ≤ countp (fun x => x == a) l₂

State before:
α : Type u_1
inst✝ : BEq α
a : α
l₁ l₂ : List α
h : l₁ <:+: l₂
⊢ countp (fun x => x == a) l₁ ≤ countp (fun x => x == a) l₂
Tactic:
apply List.isInfix_countp_le h
State after:
no goals