ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>a ∈ s → Multiset.card (s.erase a) + 1 = Multiset.card s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>a ∈ s → Multiset.card (s.erase a) < Multiset.card s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>Multiset.card (s.erase a) ≤ Multiset.card s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>Multiset.card (s.erase a) = if a ∈ s then (Multiset.card s).pred else Multiset.card s
<VAR>α : Type u_1<VAR>l : List α<GOAL>↑l.reverse = ↑l
<VAR>α : Type u_1<VAR>β : Type v<VAR>f g : α → β<VAR>s t : Multiset α<GOAL>s = t → (∀ x ∈ t, f x = g x) → Multiset.map f s = Multiset.map g t
<VAR>α : Type u_1<VAR>β β' : Type v<VAR>m : Multiset α<VAR>f : α → β<VAR>f' : α → β'<VAR>h : β = β'<VAR>hf : ∀ a ∈ m, HEq (f a) (f' a)<GOAL>HEq (Multiset.map f m) (Multiset.map f' m)
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β<VAR>p : β → Prop<VAR>s : Multiset α<GOAL>(∀ y ∈ Multiset.map f s, p y) ↔ ∀ x ∈ s, p (f x)
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β<VAR>l : List α<GOAL>Multiset.map f ↑l = ↑(List.map f l)
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β<GOAL>Multiset.map f 0 = 0
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β<VAR>a : α<VAR>s : Multiset α<GOAL>Multiset.map f (a ::ₘ s) = f a ::ₘ Multiset.map f s
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β<VAR>t : α<GOAL>Multiset.map f ∘ Multiset.cons t = Multiset.cons (f t) ∘ Multiset.map f
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β<VAR>a : α<GOAL>Multiset.map f {a} = {f a}
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β<VAR>k : ℕ<VAR>a : α<GOAL>Multiset.map f (Multiset.replicate k a) = Multiset.replicate k (f a)
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β<VAR>s t : Multiset α<GOAL>Multiset.map f (s + t) = Multiset.map f s + Multiset.map f t
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β<GOAL>⇑(Multiset.mapAddMonoidHom f) = Multiset.map f
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β<VAR>n : ℕ<VAR>s : Multiset α<GOAL>Multiset.map f (n • s) = n • Multiset.map f s
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β<VAR>b : β<VAR>s : Multiset α<GOAL>b ∈ Multiset.map f s ↔ ∃ a ∈ s, f a = b
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β<VAR>s : Multiset α<GOAL>Multiset.card (Multiset.map f s) = Multiset.card s
<VAR>α : Type u_1<VAR>β : Type v<VAR>s : Multiset α<VAR>f : α → β<GOAL>Multiset.map f s = 0 ↔ s = 0
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β<VAR>a : α<VAR>s : Multiset α<VAR>h : a ∈ s<GOAL>f a ∈ Multiset.map f s
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β<VAR>s : Multiset α<VAR>b : β<GOAL>Multiset.map f s = {b} ↔ ∃ a, s = {a} ∧ f a = b
<VAR>α : Type u_1<VAR>β : Type v<VAR>DecidableEq α<VAR>f : α → β<VAR>s : Multiset α<VAR>t : Multiset β<VAR>b : β<GOAL>(∃ a ∈ s, f a = b ∧ Multiset.map f (s.erase a) = t) ↔ Multiset.map f s = b ::ₘ t
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β<VAR>H : Function.Injective f<VAR>a : α<VAR>s : Multiset α<GOAL>f a ∈ Multiset.map f s ↔ a ∈ s
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>g : β → γ<VAR>f : α → β<VAR>s : Multiset α<GOAL>Multiset.map g (Multiset.map f s) = Multiset.map (g ∘ f) s
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>Multiset.map id s = s
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>Multiset.map (fun x => x) s = s
<VAR>α : Type u_1<VAR>β : Type v<VAR>s : Multiset α<VAR>b : β<GOAL>Multiset.map (Function.const α b) s = Multiset.replicate (Multiset.card s) b
<VAR>α : Type u_1<VAR>β : Type v<VAR>s : Multiset α<VAR>b : β<GOAL>Multiset.map (fun x => b) s = Multiset.replicate (Multiset.card s) b
<VAR>α : Type u_1<VAR>β : Type v<VAR>b₁ b₂ : β<VAR>l : List α<VAR>h : b₁ ∈ Multiset.map (Function.const α b₂) ↑l<GOAL>b₁ = b₂
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β<VAR>s t : Multiset α<VAR>h : s ≤ t<GOAL>Multiset.map f s ≤ Multiset.map f t
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β<VAR>s t : Multiset α<VAR>h : s < t<GOAL>Multiset.map f s < Multiset.map f t
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β<GOAL>Monotone (Multiset.map f)
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β<GOAL>StrictMono (Multiset.map f)
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β<VAR>s t : Multiset α<VAR>H : s ⊆ t<GOAL>Multiset.map f s ⊆ Multiset.map f t
<VAR>α : Type u_1<VAR>β : Type v<VAR>DecidableEq α<VAR>DecidableEq β<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>x : α<VAR>s : Multiset α<GOAL>Multiset.map f (s.erase x) = (Multiset.map f s).erase (f x)
<VAR>α : Type u_1<VAR>β : Type v<VAR>DecidableEq α<VAR>DecidableEq β<VAR>f : α → β<VAR>s : Multiset α<VAR>x : α<VAR>h : x ∈ s<GOAL>Multiset.map f (s.erase x) = (Multiset.map f s).erase (f x)
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β<VAR>hf : Function.Surjective f<GOAL>Function.Surjective (Multiset.map f)
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : β → α → β<VAR>H : RightCommutative f<VAR>b : β<GOAL>Multiset.foldl f H b 0 = b
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : β → α → β<VAR>H : RightCommutative f<VAR>b : β<VAR>a : α<VAR>s : Multiset α<GOAL>Multiset.foldl f H b (a ::ₘ s) = Multiset.foldl f H (f b a) s
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : β → α → β<VAR>H : RightCommutative f<VAR>b : β<VAR>s t : Multiset α<GOAL>Multiset.foldl f H b (s + t) = Multiset.foldl f H (Multiset.foldl f H b s) t
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β → β<VAR>H : LeftCommutative f<VAR>b : β<GOAL>Multiset.foldr f H b 0 = b
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β → β<VAR>H : LeftCommutative f<VAR>b : β<VAR>a : α<VAR>s : Multiset α<GOAL>Multiset.foldr f H b (a ::ₘ s) = f a (Multiset.foldr f H b s)
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β → β<VAR>H : LeftCommutative f<VAR>b : β<VAR>a : α<GOAL>Multiset.foldr f H b {a} = f a b
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β → β<VAR>H : LeftCommutative f<VAR>b : β<VAR>s t : Multiset α<GOAL>Multiset.foldr f H b (s + t) = Multiset.foldr f H (Multiset.foldr f H b t) s
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β → β<VAR>H : LeftCommutative f<VAR>b : β<VAR>l : List α<GOAL>Multiset.foldr f H b ↑l = List.foldr f b l
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : β → α → β<VAR>H : RightCommutative f<VAR>b : β<VAR>l : List α<GOAL>Multiset.foldl f H b ↑l = List.foldl f b l
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β → β<VAR>H : LeftCommutative f<VAR>b : β<VAR>l : List α<GOAL>Multiset.foldr f H b ↑l = List.foldl (fun x y => f y x) b l
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β → β<VAR>H : LeftCommutative f<VAR>b : β<VAR>s : Multiset α<GOAL>Multiset.foldr f H b s = Multiset.foldl (fun x y => f y x) ⋯ b s
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : β → α → β<VAR>H : RightCommutative f<VAR>b : β<VAR>s : Multiset α<GOAL>Multiset.foldl f H b s = Multiset.foldr (fun x y => f y x) ⋯ b s
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β → β<VAR>H : LeftCommutative f<VAR>x : β<VAR>q : α → Prop<VAR>p : β → Prop<VAR>s : Multiset α<VAR>hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)<VAR>px : p x<VAR>q_s : ∀ a ∈ s, q a<GOAL>p (Multiset.foldr f H x s)
<VAR>α : Type u_1<VAR>f : α → α → α<VAR>H : LeftCommutative f<VAR>x : α<VAR>p : α → Prop<VAR>s : Multiset α<VAR>p_f : ∀ (a b : α), p a → p b → p (f a b)<VAR>px : p x<VAR>p_s : ∀ a ∈ s, p a<GOAL>p (Multiset.foldr f H x s)
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : β → α → β<VAR>H : RightCommutative f<VAR>x : β<VAR>q : α → Prop<VAR>p : β → Prop<VAR>s : Multiset α<VAR>hpqf : ∀ (a : α) (b : β), q a → p b → p (f b a)<VAR>px : p x<VAR>q_s : ∀ a ∈ s, q a<GOAL>p (Multiset.foldl f H x s)
<VAR>α : Type u_1<VAR>f : α → α → α<VAR>H : RightCommutative f<VAR>x : α<VAR>p : α → Prop<VAR>s : Multiset α<VAR>p_f : ∀ (a b : α), p a → p b → p (f b a)<VAR>px : p x<VAR>p_s : ∀ a ∈ s, p a<GOAL>p (Multiset.foldl f H x s)
<VAR>α : Type u_1<VAR>β : Type v<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>l : List α<VAR>H : ∀ a ∈ l, p a<GOAL>Multiset.pmap f (↑l) H = ↑(List.pmap f l H)
<VAR>α : Type u_1<VAR>β : Type v<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>h : ∀ a ∈ 0, p a<GOAL>Multiset.pmap f 0 h = 0
<VAR>α : Type u_1<VAR>β : Type v<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>a : α<VAR>m : Multiset α<VAR>h : ∀ b ∈ a ::ₘ m, p b<GOAL>Multiset.pmap f (a ::ₘ m) h = f a ⋯ ::ₘ Multiset.pmap f m ⋯
<VAR>α : Type u_1<VAR>l : List α<GOAL>(↑l).attach = ↑l.attach
<VAR>α : Type u_1<VAR>SizeOf α<VAR>x : α<VAR>s : Multiset α<VAR>hx : x ∈ s<GOAL>sizeOf x < sizeOf s
<VAR>α : Type u_1<VAR>β : Type v<VAR>p : α → Prop<VAR>f : α → β<VAR>s : Multiset α<VAR>H : ∀ a ∈ s, p a<GOAL>Multiset.pmap (fun a x => f a) s H = Multiset.map f s
<VAR>α : Type u_1<VAR>β : Type v<VAR>p q : α → Prop<VAR>f : (a : α) → p a → β<VAR>g : (a : α) → q a → β<VAR>s : Multiset α<VAR>H₁ : ∀ a ∈ s, p a<VAR>H₂ : ∀ a ∈ s, q a<GOAL>(∀ a ∈ s, ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂) → Multiset.pmap f s H₁ = Multiset.pmap g s H₂
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>p : α → Prop<VAR>g : β → γ<VAR>f : (a : α) → p a → β<VAR>s : Multiset α<VAR>H : ∀ a ∈ s, p a<GOAL>Multiset.map g (Multiset.pmap f s H) = Multiset.pmap (fun a h => g (f a h)) s H
<VAR>α : Type u_1<VAR>β : Type v<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>s : Multiset α<VAR>H : ∀ a ∈ s, p a<GOAL>Multiset.pmap f s H = Multiset.map (fun x => f ↑x ⋯) s.attach
<VAR>α : Type u_1<VAR>β : Type v<VAR>s : Multiset α<VAR>f : α → β<GOAL>Multiset.map (fun i => f ↑i) s.attach = Multiset.map f s
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>Multiset.map Subtype.val s.attach = s
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>x : { x // x ∈ s }<GOAL>x ∈ s.attach
<VAR>α : Type u_1<VAR>β : Type v<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>s : Multiset α<VAR>H : ∀ a ∈ s, p a<VAR>b : β<GOAL>b ∈ Multiset.pmap f s H ↔ ∃ a, ∃ (h : a ∈ s), f a ⋯ = b
<VAR>α : Type u_1<VAR>β : Type v<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>s : Multiset α<VAR>H : ∀ a ∈ s, p a<GOAL>Multiset.card (Multiset.pmap f s H) = Multiset.card s
<VAR>α : Type u_1<VAR>m : Multiset α<GOAL>Multiset.card m.attach = Multiset.card m
<VAR>α : Type u_1<GOAL>Multiset.attach 0 = 0
<VAR>α : Type u_1<VAR>a : α<VAR>m : Multiset α<GOAL>(a ::ₘ m).attach = ⟨a, ⋯⟩ ::ₘ Multiset.map (fun p => ⟨↑p, ⋯⟩) m.attach
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : List α<GOAL>↑s - ↑t = ↑(s.diff t)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<GOAL>s - 0 = s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s t : Multiset α<GOAL>s - a ::ₘ t = s.erase a - t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Multiset α<GOAL>s - t ≤ u ↔ s ≤ u + t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s t : Multiset α<VAR>h : t ≤ s<GOAL>a ::ₘ s - t = a ::ₘ (s - t)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>s - t = Multiset.foldl Multiset.erase ⋯ s t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<VAR>h : t ≤ s<GOAL>Multiset.card (s - t) = Multiset.card s - Multiset.card t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>s ∪ t = s - t + t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>s ≤ s ∪ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>t ≤ s ∪ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>t ≤ s → s ∪ t = s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<VAR>h : s ≤ t<VAR>u : Multiset α<GOAL>s ∪ u ≤ t ∪ u
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Multiset α<VAR>h₁ : s ≤ u<VAR>h₂ : t ≤ u<GOAL>s ∪ t ≤ u
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<VAR>a : α<GOAL>a ∈ s ∪ t ↔ a ∈ s ∨ a ∈ t
<VAR>α : Type u_1<VAR>β : Type v<VAR>DecidableEq α<VAR>DecidableEq β<VAR>f : α → β<VAR>finj : Function.Injective f<VAR>s t : Multiset α<GOAL>Multiset.map f (s ∪ t) = Multiset.map f s ∪ Multiset.map f t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<GOAL>0 ∪ s = s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<GOAL>s ∪ 0 = s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<GOAL>s ∩ 0 = 0
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<GOAL>0 ∩ s = 0
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<VAR>t : Multiset α<GOAL>a ∈ t → (a ::ₘ s) ∩ t = a ::ₘ s ∩ t.erase a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<VAR>t : Multiset α<GOAL>a ∉ t → (a ::ₘ s) ∩ t = s ∩ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>s ∩ t ≤ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>s ∩ t ≤ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Multiset α<VAR>h₁ : s ≤ t<VAR>h₂ : s ≤ u<GOAL>s ≤ t ∩ u
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<VAR>a : α<GOAL>a ∈ s ∩ t ↔ a ∈ s ∧ a ∈ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>s ⊔ t = s ∪ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>s ⊓ t = s ∩ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Multiset α<GOAL>s ≤ t ∩ u ↔ s ≤ t ∧ s ≤ u
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Multiset α<GOAL>s ∪ t ≤ u ↔ s ≤ u ∧ t ≤ u
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>s ∪ t = t ∪ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>s ∩ t = t ∩ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<VAR>h : s ≤ t<GOAL>s ∪ t = t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<VAR>h : s ≤ t<VAR>u : Multiset α<GOAL>u ∪ s ≤ u ∪ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>s ∪ t ≤ s + t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Multiset α<GOAL>s ∪ t + u = s + u ∪ (t + u)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Multiset α<GOAL>s + (t ∪ u) = s + t ∪ (s + u)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s t : Multiset α<GOAL>a ::ₘ (s ∪ t) = a ::ₘ s ∪ a ::ₘ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Multiset α<GOAL>s ∩ t + u = (s + u) ∩ (t + u)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Multiset α<GOAL>s + t ∩ u = (s + t) ∩ (s + u)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s t : Multiset α<GOAL>a ::ₘ s ∩ t = (a ::ₘ s) ∩ (a ::ₘ t)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>s ∪ t + s ∩ t = s + t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>s - t + s ∩ t = s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>s - s ∩ t = s - t
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>l : List α<GOAL>Multiset.filter p ↑l = ↑(List.filter (fun b => decide (p b)) l)
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<GOAL>Multiset.filter p 0 = 0
<VAR>α : Type u_1<VAR>p q : α → Prop<VAR>DecidablePred p<VAR>DecidablePred q<VAR>s : Multiset α<GOAL>(∀ x ∈ s, p x ↔ q x) → Multiset.filter p s = Multiset.filter q s
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s t : Multiset α<GOAL>Multiset.filter p (s + t) = Multiset.filter p s + Multiset.filter p t
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Multiset α<GOAL>Multiset.filter p s ≤ s
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Multiset α<GOAL>Multiset.filter p s ⊆ s
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s t : Multiset α<VAR>h : s ≤ t<GOAL>Multiset.filter p s ≤ Multiset.filter p t
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<GOAL>Monotone (Multiset.filter p)
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>p q : α → Prop<VAR>DecidablePred p<VAR>DecidablePred q<VAR>h : ∀ (b : α), p b → q b<GOAL>Multiset.filter p s ≤ Multiset.filter q s
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>a : α<VAR>s : Multiset α<GOAL>p a → Multiset.filter p (a ::ₘ s) = a ::ₘ Multiset.filter p s
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>a : α<VAR>s : Multiset α<GOAL>¬p a → Multiset.filter p (a ::ₘ s) = Multiset.filter p s
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>a : α<VAR>s : Multiset α<GOAL>a ∈ Multiset.filter p s ↔ a ∈ s ∧ p a
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>a : α<VAR>s : Multiset α<VAR>h : a ∈ Multiset.filter p s<GOAL>p a
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>a : α<VAR>s : Multiset α<VAR>h : a ∈ Multiset.filter p s<GOAL>a ∈ s
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>a : α<VAR>l : Multiset α<VAR>m : a ∈ l<VAR>h : p a<GOAL>a ∈ Multiset.filter p l
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Multiset α<GOAL>Multiset.filter p s = s ↔ ∀ a ∈ s, p a
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Multiset α<GOAL>Multiset.filter p s = 0 ↔ ∀ a ∈ s, ¬p a
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s t : Multiset α<GOAL>s ≤ Multiset.filter p t ↔ s ≤ t ∧ ∀ a ∈ s, p a
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>a : α<VAR>s : Multiset α<GOAL>Multiset.filter p (a ::ₘ s) = (if p a then {a} else 0) + Multiset.filter p s
<VAR>α : Type u_1<VAR>a : α<VAR>p : α → Prop<VAR>DecidablePred p<GOAL>Multiset.filter p {a} = if p a then {a} else ∅
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Multiset α<VAR>n : ℕ<GOAL>Multiset.filter p (n • s) = n • Multiset.filter p s
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>Multiset.filter p (s - t) = Multiset.filter p s - Multiset.filter p t
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>Multiset.filter p (s ∪ t) = Multiset.filter p s ∪ Multiset.filter p t
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>Multiset.filter p (s ∩ t) = Multiset.filter p s ∩ Multiset.filter p t
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>q : α → Prop<VAR>DecidablePred q<VAR>s : Multiset α<GOAL>Multiset.filter p (Multiset.filter q s) = Multiset.filter (fun a => p a ∧ q a) s
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>q : α → Prop<VAR>DecidablePred q<VAR>s : Multiset α<GOAL>Multiset.filter p (Multiset.filter q s) = Multiset.filter q (Multiset.filter p s)
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>q : α → Prop<VAR>DecidablePred q<VAR>s : Multiset α<GOAL>Multiset.filter p s + Multiset.filter q s = Multiset.filter (fun a => p a ∨ q a) s + Multiset.filter (fun a => p a ∧ q a) s
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Multiset α<GOAL>Multiset.filter p s + Multiset.filter (fun a => ¬p a) s = s
<VAR>α : Type u_1<VAR>β : Type v<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f : β → α<VAR>s : Multiset β<GOAL>Multiset.filter p (Multiset.map f s) = Multiset.map f (Multiset.filter (p ∘ f) s)
<VAR>α : Type u_1<VAR>β : Type v<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>s : Multiset α<VAR>DecidablePred fun b => ∃ a, p a ∧ f a = b<GOAL>Multiset.map f (Multiset.filter p s) = Multiset.filter (fun b => ∃ a, p a ∧ f a = b) (Multiset.map f s)
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>P : α → Prop<VAR>DecidablePred P<VAR>n : ℕ<GOAL>Multiset.card (Multiset.filter P s) ≤ n ↔ ∀ s' ≤ s, n < Multiset.card s' → ∃ a ∈ s', ¬P a
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → Option β<VAR>l : List α<GOAL>Multiset.filterMap f ↑l = ↑(List.filterMap f l)
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → Option β<GOAL>Multiset.filterMap f 0 = 0
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → Option β<VAR>a : α<VAR>s : Multiset α<VAR>h : f a = none<GOAL>Multiset.filterMap f (a ::ₘ s) = Multiset.filterMap f s
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → Option β<VAR>a : α<VAR>s : Multiset α<VAR>b : β<VAR>h : f a = some b<GOAL>Multiset.filterMap f (a ::ₘ s) = b ::ₘ Multiset.filterMap f s
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β<GOAL>Multiset.filterMap (some ∘ f) = Multiset.map f
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<GOAL>Multiset.filterMap (Option.guard p) = Multiset.filter p
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>f : α → Option β<VAR>g : β → Option γ<VAR>s : Multiset α<GOAL>Multiset.filterMap g (Multiset.filterMap f s) = Multiset.filterMap (fun x => (f x).bind g) s
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>f : α → Option β<VAR>g : β → γ<VAR>s : Multiset α<GOAL>Multiset.map g (Multiset.filterMap f s) = Multiset.filterMap (fun x => Option.map g (f x)) s
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>f : α → β<VAR>g : β → Option γ<VAR>s : Multiset α<GOAL>Multiset.filterMap g (Multiset.map f s) = Multiset.filterMap (g ∘ f) s
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → Option β<VAR>p : β → Prop<VAR>DecidablePred p<VAR>s : Multiset α<GOAL>Multiset.filter p (Multiset.filterMap f s) = Multiset.filterMap (fun x => Option.filter (fun b => decide (p b)) (f x)) s
<VAR>α : Type u_1<VAR>β : Type v<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f : α → Option β<VAR>s : Multiset α<GOAL>Multiset.filterMap f (Multiset.filter p s) = Multiset.filterMap (fun x => if p x then f x else none) s
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>Multiset.filterMap some s = s
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → Option β<VAR>s : Multiset α<VAR>b : β<GOAL>b ∈ Multiset.filterMap f s ↔ ∃ a ∈ s, f a = some b
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → Option β<VAR>g : β → α<VAR>H : ∀ (x : α), Option.map g (f x) = some x<VAR>s : Multiset α<GOAL>Multiset.map g (Multiset.filterMap f s) = s
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → Option β<VAR>s t : Multiset α<VAR>h : s ≤ t<GOAL>Multiset.filterMap f s ≤ Multiset.filterMap f t
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>l : List α<GOAL>Multiset.countP p ↑l = List.countP (fun b => decide (p b)) l
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<GOAL>Multiset.countP p 0 = 0
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>a : α<VAR>s : Multiset α<GOAL>p a → Multiset.countP p (a ::ₘ s) = Multiset.countP p s + 1
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>a : α<VAR>s : Multiset α<GOAL>¬p a → Multiset.countP p (a ::ₘ s) = Multiset.countP p s
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>b : α<VAR>s : Multiset α<GOAL>Multiset.countP p (b ::ₘ s) = Multiset.countP p s + if p b then 1 else 0
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Multiset α<GOAL>Multiset.countP p s = Multiset.card (Multiset.filter p s)
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Multiset α<GOAL>Multiset.countP p s ≤ Multiset.card s
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s t : Multiset α<GOAL>Multiset.countP p (s + t) = Multiset.countP p s + Multiset.countP p t
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Multiset α<VAR>n : ℕ<GOAL>Multiset.countP p (n • s) = n * Multiset.countP p s
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Multiset α<GOAL>Multiset.card s = Multiset.countP p s + Multiset.countP (fun x => ¬p x) s
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<GOAL>⇑(Multiset.countPAddMonoidHom p) = Multiset.countP p
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>DecidableEq α<VAR>s t : Multiset α<VAR>h : t ≤ s<GOAL>Multiset.countP p (s - t) = Multiset.countP p s - Multiset.countP p t
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s t : Multiset α<VAR>h : s ≤ t<GOAL>Multiset.countP p s ≤ Multiset.countP p t
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>q : α → Prop<VAR>DecidablePred q<VAR>s : Multiset α<GOAL>Multiset.countP p (Multiset.filter q s) = Multiset.countP (fun a => p a ∧ q a) s
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>p q : α → Prop<VAR>DecidablePred p<VAR>DecidablePred q<GOAL>Multiset.countP p s = Multiset.countP p (Multiset.filter q s) + Multiset.countP p (Multiset.filter (fun a => ¬q a) s)
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>Multiset.countP (fun x => True) s = Multiset.card s
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>Multiset.countP (fun x => False) s = 0
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β<VAR>s : Multiset α<VAR>p : β → Prop<VAR>DecidablePred p<GOAL>Multiset.countP p (Multiset.map f s) = Multiset.card (Multiset.filter (fun a => p (f a)) s)
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Multiset α<GOAL>Multiset.countP (fun a => p ↑a) s.attach = Multiset.countP p s
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>p : α → Prop<VAR>DecidablePred p<GOAL>Multiset.filter (fun a => p ↑a) s.attach = Multiset.map (Subtype.map id ⋯) (Multiset.filter p s).attach
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Multiset α<GOAL>0 < Multiset.countP p s ↔ ∃ a ∈ s, p a
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Multiset α<GOAL>Multiset.countP p s = 0 ↔ ∀ a ∈ s, ¬p a
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Multiset α<GOAL>Multiset.countP p s = Multiset.card s ↔ ∀ a ∈ s, p a