ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Multiset α<VAR>a : α<VAR>h : a ∈ s<VAR>pa : p a<GOAL>0 < Multiset.countP p s
<VAR>α : Type u_1<VAR>s s' : Multiset α<VAR>hs : s = s'<VAR>p p' : α → Prop<VAR>DecidablePred p<VAR>DecidablePred p'<VAR>hp : ∀ x ∈ s, p x = p' x<GOAL>Multiset.countP p s = Multiset.countP p' s'
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<GOAL>Multiset.count a ↑l = List.count a l
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<GOAL>Multiset.count a 0 = 0
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>Multiset.count a (a ::ₘ s) = Multiset.count a s + 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : α<VAR>h : a ≠ b<VAR>s : Multiset α<GOAL>Multiset.count a (b ::ₘ s) = Multiset.count a s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>Multiset.count a s ≤ Multiset.card s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s t : Multiset α<GOAL>s ≤ t → Multiset.count a s ≤ Multiset.count a t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : α<VAR>s : Multiset α<GOAL>Multiset.count a s ≤ Multiset.count a (b ::ₘ s)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : α<VAR>s : Multiset α<GOAL>Multiset.count a (b ::ₘ s) = Multiset.count a s + if a = b then 1 else 0
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<GOAL>Multiset.count a {a} = 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : α<GOAL>Multiset.count a {b} = if a = b then 1 else 0
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s t : Multiset α<GOAL>Multiset.count a (s + t) = Multiset.count a s + Multiset.count a t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<GOAL>⇑(Multiset.countAddMonoidHom a) = Multiset.count a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>n : ℕ<VAR>s : Multiset α<GOAL>Multiset.count a (n • s) = n * Multiset.count a s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<VAR>a : { x // x ∈ s }<GOAL>Multiset.count a s.attach = Multiset.count (↑a) s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>0 < Multiset.count a s ↔ a ∈ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>1 ≤ Multiset.count a s ↔ a ∈ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<VAR>h : a ∉ s<GOAL>Multiset.count a s = 0
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<VAR>a : α<GOAL>Multiset.count a s ≠ 0 ↔ a ∈ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<VAR>a : α<GOAL>Multiset.count a s = 0 ↔ a ∉ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>Multiset.count a s = Multiset.card s ↔ ∀ x ∈ s, a = x
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>n : ℕ<GOAL>Multiset.count a (Multiset.replicate n a) = n
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : α<VAR>n : ℕ<GOAL>Multiset.count a (Multiset.replicate n b) = if a = b then n else 0
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>Multiset.count a (s.erase a) = Multiset.count a s - 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : α<VAR>ab : a ≠ b<VAR>s : Multiset α<GOAL>Multiset.count a (s.erase b) = Multiset.count a s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s t : Multiset α<GOAL>Multiset.count a (s - t) = Multiset.count a s - Multiset.count a t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s t : Multiset α<GOAL>Multiset.count a (s ∪ t) = max (Multiset.count a s) (Multiset.count a t)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s t : Multiset α<GOAL>Multiset.count a (s ∩ t) = min (Multiset.count a s) (Multiset.count a t)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<VAR>n : ℕ<GOAL>n ≤ Multiset.count a s ↔ Multiset.replicate n a ≤ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>a : α<VAR>s : Multiset α<VAR>h : p a<GOAL>Multiset.count a (Multiset.filter p s) = Multiset.count a s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>a : α<VAR>s : Multiset α<VAR>h : ¬p a<GOAL>Multiset.count a (Multiset.filter p s) = 0
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>a : α<VAR>s : Multiset α<GOAL>Multiset.count a (Multiset.filter p s) = if p a then Multiset.count a s else 0
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>s = t ↔ ∀ (a : α), Multiset.count a s = Multiset.count a t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>(∀ (a : α), Multiset.count a s = Multiset.count a t) → s = t
<VAR>α : Type u_1<VAR>DecidableEq α<GOAL>Function.Injective fun s a => Multiset.count a s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : List α<GOAL>↑s ∩ ↑t = ↑(s.bagInter t)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>s ≤ t ↔ ∀ (a : α), Multiset.count a s ≤ Multiset.count a t
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>f : α → β<VAR>s : Multiset α<VAR>DecidableEq β<VAR>b : β<GOAL>Multiset.count b (Multiset.map f s) = Multiset.card (Multiset.filter (fun a => b = f a) s)
<VAR>α : Type u_1<VAR>β : Type v<VAR>DecidableEq α<VAR>DecidableEq β<VAR>f : α → β<VAR>s : Multiset α<VAR>hf : Set.InjOn f {x | x ∈ s}<VAR>x : α<VAR>H : x ∈ s<GOAL>Multiset.count (f x) (Multiset.map f s) = Multiset.count x s
<VAR>α : Type u_1<VAR>β : Type v<VAR>DecidableEq α<VAR>DecidableEq β<VAR>f : α → β<VAR>s : Multiset α<VAR>hf : Function.Injective f<VAR>x : α<GOAL>Multiset.count (f x) (Multiset.map f s) = Multiset.count x s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Multiset α<GOAL>s - Multiset.filter p s = Multiset.filter (fun a => ¬p a) s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<VAR>b : α<GOAL>Multiset.filter (fun x => x = b) s = Multiset.replicate (Multiset.count b s) b
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<VAR>b : α<GOAL>Multiset.filter (Eq b) s = Multiset.replicate (Multiset.count b s) b
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>n : ℕ<VAR>x : α<VAR>s : Multiset α<GOAL>Multiset.replicate n x ∩ s = Multiset.replicate (min n (Multiset.count x s)) x
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<VAR>n : ℕ<VAR>x : α<GOAL>s ∩ Multiset.replicate n x = Multiset.replicate (min (Multiset.count x s) n) x
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<VAR>x : { x // x ∈ s }<GOAL>Multiset.map Subtype.val (s.attach.erase x) = s.erase ↑x
<VAR>α : Type u_1<VAR>β : Type v<VAR>DecidableEq α<VAR>s : Multiset α<VAR>f : α → β<VAR>x : { x // x ∈ s }<GOAL>Multiset.map (fun j => f ↑j) (s.attach.erase x) = Multiset.map f (s.erase ↑x)
<VAR>α : Type u_1<VAR>β : Type v<VAR>AddZeroClass β<VAR>f g : Multiset α →+ β<VAR>h : ∀ (x : α), f {x} = g {x}<GOAL>f = g
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>s t : Multiset α<GOAL>Multiset.map f s ≤ Multiset.map f t ↔ s ≤ t
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α ↪ β<VAR>s : Multiset α<GOAL>(Multiset.mapEmbedding f) s = Multiset.map (⇑f) s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<VAR>a : α<GOAL>Multiset.count a s = Multiset.card (Multiset.filter (fun x => a = x) s)
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>p : α → Prop<VAR>DecidablePred p<GOAL>Multiset.count True (Multiset.map p s) = Multiset.card (Multiset.filter p s)
<VAR>α : Type u_1<VAR>β : Type v<VAR>r : α → β → Prop<GOAL>∀ (a : Multiset α) (a_1 : Multiset β), Multiset.Rel r a a_1 ↔ a = 0 ∧ a_1 = 0 ∨ ∃ a_2 b as bs, r a_2 b ∧ Multiset.Rel r as bs ∧ a = a_2 ::ₘ as ∧ a_1 = b ::ₘ bs
<VAR>α : Type u_1<VAR>β : Type v<VAR>r : α → β → Prop<VAR>s : Multiset α<VAR>t : Multiset β<VAR>h : Multiset.Rel r s t<GOAL>Multiset.Rel (flip r) t s
<VAR>α : Type u_1<VAR>β : Type v<VAR>r : α → β → Prop<VAR>s : Multiset β<VAR>t : Multiset α<GOAL>Multiset.Rel (flip r) s t ↔ Multiset.Rel r t s
<VAR>α : Type u_1<VAR>m : Multiset α<VAR>r : α → α → Prop<GOAL>(∀ x ∈ m, r x x) → Multiset.Rel r m m
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>Multiset.Rel (fun x x_1 => x = x_1) s s
<VAR>α : Type u_1<VAR>s t : Multiset α<GOAL>Multiset.Rel (fun x x_1 => x = x_1) s t ↔ s = t
<VAR>α : Type u_1<VAR>β : Type v<VAR>r p : α → β → Prop<VAR>s : Multiset α<VAR>t : Multiset β<VAR>hst : Multiset.Rel r s t<VAR>h : ∀ a ∈ s, ∀ b ∈ t, r a b → p a b<GOAL>Multiset.Rel p s t
<VAR>α : Type u_1<VAR>β : Type v<VAR>r : α → β → Prop<VAR>s : Multiset α<VAR>t : Multiset β<VAR>u : Multiset α<VAR>v : Multiset β<VAR>hst : Multiset.Rel r s t<VAR>huv : Multiset.Rel r u v<GOAL>Multiset.Rel r (s + u) (t + v)
<VAR>α : Type u_1<VAR>s t : Multiset α<GOAL>Multiset.Rel (fun a b => b = a) s t ↔ s = t
<VAR>α : Type u_1<VAR>β : Type v<VAR>r : α → β → Prop<VAR>b : Multiset β<GOAL>Multiset.Rel r 0 b ↔ b = 0
<VAR>α : Type u_1<VAR>β : Type v<VAR>r : α → β → Prop<VAR>a : Multiset α<GOAL>Multiset.Rel r a 0 ↔ a = 0
<VAR>α : Type u_1<VAR>β : Type v<VAR>r : α → β → Prop<VAR>a : α<VAR>as : Multiset α<VAR>bs : Multiset β<GOAL>Multiset.Rel r (a ::ₘ as) bs ↔ ∃ b bs', r a b ∧ Multiset.Rel r as bs' ∧ bs = b ::ₘ bs'
<VAR>α : Type u_1<VAR>β : Type v<VAR>r : α → β → Prop<VAR>as : Multiset α<VAR>b : β<VAR>bs : Multiset β<GOAL>Multiset.Rel r as (b ::ₘ bs) ↔ ∃ a as', r a b ∧ Multiset.Rel r as' bs ∧ as = a ::ₘ as'
<VAR>α : Type u_1<VAR>β : Type v<VAR>r : α → β → Prop<VAR>as₀ as₁ : Multiset α<VAR>bs : Multiset β<GOAL>Multiset.Rel r (as₀ + as₁) bs ↔ ∃ bs₀ bs₁, Multiset.Rel r as₀ bs₀ ∧ Multiset.Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
<VAR>α : Type u_1<VAR>β : Type v<VAR>r : α → β → Prop<VAR>as : Multiset α<VAR>bs₀ bs₁ : Multiset β<GOAL>Multiset.Rel r as (bs₀ + bs₁) ↔ ∃ as₀ as₁, Multiset.Rel r as₀ bs₀ ∧ Multiset.Rel r as₁ bs₁ ∧ as = as₀ + as₁
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>r : α → β → Prop<VAR>s : Multiset γ<VAR>f : γ → α<VAR>t : Multiset β<GOAL>Multiset.Rel r (Multiset.map f s) t ↔ Multiset.Rel (fun a b => r (f a) b) s t
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>r : α → β → Prop<VAR>s : Multiset α<VAR>t : Multiset γ<VAR>f : γ → β<GOAL>Multiset.Rel r s (Multiset.map f t) ↔ Multiset.Rel (fun a b => r a (f b)) s t
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>p : γ → δ → Prop<VAR>s : Multiset α<VAR>t : Multiset β<VAR>f : α → γ<VAR>g : β → δ<GOAL>Multiset.Rel p (Multiset.map f s) (Multiset.map g t) ↔ Multiset.Rel (fun a b => p (f a) (g b)) s t
<VAR>α : Type u_1<VAR>β : Type v<VAR>r : α → β → Prop<VAR>s : Multiset α<VAR>t : Multiset β<VAR>h : Multiset.Rel r s t<GOAL>Multiset.card s = Multiset.card t
<VAR>α : Type u_1<VAR>β : Type v<VAR>r : α → β → Prop<VAR>s : Multiset α<VAR>t : Multiset β<VAR>h : Multiset.Rel r s t<VAR>a : α<GOAL>a ∈ s → ∃ b ∈ t, r a b
<VAR>α : Type u_1<VAR>m1 m2 : Multiset α<VAR>r : α → α → Prop<VAR>h : ∀ (a b : α), a ∈ m1 → b ∈ m2 → r a b<VAR>hc : Multiset.card m1 = Multiset.card m2<GOAL>Multiset.Rel r m1 m2
<VAR>α : Type u_1<VAR>m : Multiset α<VAR>a : α<VAR>r : α → α → Prop<VAR>n : ℕ<GOAL>Multiset.Rel r (Multiset.replicate n a) m ↔ Multiset.card m = n ∧ ∀ x ∈ m, r a x
<VAR>α : Type u_1<VAR>m : Multiset α<VAR>a : α<VAR>r : α → α → Prop<VAR>n : ℕ<GOAL>Multiset.Rel r m (Multiset.replicate n a) ↔ Multiset.card m = n ∧ ∀ x ∈ m, r x a
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsTrans α r<VAR>s t u : Multiset α<VAR>r1 : Multiset.Rel r s t<VAR>r2 : Multiset.Rel r t u<GOAL>Multiset.Rel r s u
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsTrans α r<VAR>IsSymm α r<VAR>s t : Multiset α<VAR>x : α<VAR>DecidablePred (r x)<VAR>h : Multiset.Rel r s t<GOAL>Multiset.countP (r x) s = Multiset.countP (r x) t
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>s t : Multiset α<GOAL>Multiset.map f s = Multiset.map f t ↔ s = t
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>Function.Injective (Multiset.map f)
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>p : { a // a ∈ s } → Prop<VAR>DecidableEq α<VAR>DecidablePred p<GOAL>Multiset.filter p s.attach = Multiset.map (Subtype.map id ⋯) (Multiset.filter (fun x => ∃ (h : x ∈ s), p ⟨x, h⟩) s).attach
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Multiset α<VAR>hst : Multiset.Rel r s t<GOAL>Multiset.map (Quot.mk r) s = Multiset.map (Quot.mk r) t
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Multiset (Quot r)<GOAL>∃ t, s = Multiset.map (Quot.mk r) t
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>p : Multiset (Quot r) → Prop<VAR>s : Multiset (Quot r)<GOAL>(∀ (s : Multiset α), p (Multiset.map (Quot.mk r) s)) → p s
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<GOAL>(↑l₁).Disjoint ↑l₂ ↔ l₁.Disjoint l₂
<VAR>α : Type u_1<VAR>s t : Multiset α<VAR>d : s.Disjoint t<GOAL>t.Disjoint s
<VAR>α : Type u_1<VAR>s t : Multiset α<GOAL>s.Disjoint t ↔ t.Disjoint s
<VAR>α : Type u_1<VAR>s t : Multiset α<GOAL>s.Disjoint t ↔ ∀ {a : α}, a ∈ s → a ∉ t
<VAR>α : Type u_1<VAR>s t : Multiset α<GOAL>s.Disjoint t ↔ ∀ {a : α}, a ∈ t → a ∉ s
<VAR>α : Type u_1<VAR>s t : Multiset α<GOAL>s.Disjoint t ↔ ∀ a ∈ s, ∀ b ∈ t, a ≠ b
<VAR>α : Type u_1<VAR>s t u : Multiset α<VAR>h : s ⊆ u<VAR>d : u.Disjoint t<GOAL>s.Disjoint t
<VAR>α : Type u_1<VAR>s t u : Multiset α<VAR>h : t ⊆ u<VAR>d : s.Disjoint u<GOAL>s.Disjoint t
<VAR>α : Type u_1<VAR>s t u : Multiset α<VAR>h : s ≤ u<GOAL>u.Disjoint t → s.Disjoint t
<VAR>α : Type u_1<VAR>s t u : Multiset α<VAR>h : t ≤ u<GOAL>s.Disjoint u → s.Disjoint t
<VAR>α : Type u_1<VAR>l : Multiset α<GOAL>Multiset.Disjoint 0 l
<VAR>α : Type u_1<VAR>l : Multiset α<VAR>a : α<GOAL>{a}.Disjoint l ↔ a ∉ l
<VAR>α : Type u_1<VAR>l : Multiset α<VAR>a : α<GOAL>l.Disjoint {a} ↔ a ∉ l
<VAR>α : Type u_1<VAR>s t u : Multiset α<GOAL>(s + t).Disjoint u ↔ s.Disjoint u ∧ t.Disjoint u
<VAR>α : Type u_1<VAR>s t u : Multiset α<GOAL>s.Disjoint (t + u) ↔ s.Disjoint t ∧ s.Disjoint u
<VAR>α : Type u_1<VAR>a : α<VAR>s t : Multiset α<GOAL>(a ::ₘ s).Disjoint t ↔ a ∉ t ∧ s.Disjoint t
<VAR>α : Type u_1<VAR>a : α<VAR>s t : Multiset α<GOAL>s.Disjoint (a ::ₘ t) ↔ a ∉ s ∧ s.Disjoint t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>s ∩ t = 0 ↔ s.Disjoint t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Multiset α<GOAL>(s ∪ t).Disjoint u ↔ s.Disjoint u ∧ t.Disjoint u
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Multiset α<GOAL>s.Disjoint (t ∪ u) ↔ s.Disjoint t ∧ s.Disjoint u
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>s + t = s ∪ t ↔ s.Disjoint t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Multiset α<VAR>h : t ≤ s<GOAL>u + s = u ∪ t ↔ u.Disjoint s ∧ s = t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>x y z : Multiset α<VAR>h : z ≤ y<GOAL>x + y = x ∪ z ↔ y = z ∧ x.Disjoint y
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>f : α → γ<VAR>g : β → γ<VAR>s : Multiset α<VAR>t : Multiset β<GOAL>(Multiset.map f s).Disjoint (Multiset.map g t) ↔ ∀ a ∈ s, ∀ b ∈ t, f a ≠ g b
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>Multiset.Pairwise r 0
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>l : List α<GOAL>Multiset.Pairwise r ↑l ↔ ∃ l', l ~ l' ∧ List.Pairwise r l'
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>hr : Symmetric r<VAR>l : List α<GOAL>Multiset.Pairwise r ↑l ↔ List.Pairwise r l
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β<VAR>r : β → β → Prop<VAR>m : Multiset α<VAR>h : {a | a ∈ m}.Pairwise fun a₁ a₂ => r (f a₁) (f a₂)<GOAL>{b | b ∈ Multiset.map f m}.Pairwise r
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>l : Multiset α<VAR>hp : ∃! a, a ∈ l ∧ p a<GOAL>Multiset.choose p l hp ∈ l ∧ p (Multiset.choose p l hp)
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>l : Multiset α<VAR>hp : ∃! a, a ∈ l ∧ p a<GOAL>Multiset.choose p l hp ∈ l
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>l : Multiset α<VAR>hp : ∃! a, a ∈ l ∧ p a<GOAL>p (Multiset.choose p l hp)
<VAR>α : Type u_1<VAR>Subsingleton α<GOAL>⇑(Multiset.subsingletonEquiv α) = Multiset.ofList
<VAR>n : ℕ<VAR>NeZero n<VAR>a : ZMod n<GOAL>a.val < n
<VAR>n : ℕ<VAR>NeZero n<VAR>a : ZMod n<GOAL>a.val ≤ n
<VAR>n : ℕ<GOAL>ZMod.val 0 = 0
<VAR>n : ZMod 0<GOAL>(-n).val = n.val
<VAR>m n : ZMod 0<GOAL>(m * n).val = m.val * n.val
<VAR>n : ℕ<VAR>a : ℕ<GOAL>(↑a).val = a % n
<VAR>n : ZMod 0<GOAL>IsUnit n ↔ n.val = 1
<VAR>n : ℕ<GOAL>addOrderOf 1 = n
<VAR>a : ℕ<VAR>n : ℕ<VAR>n0 : n ≠ 0<GOAL>addOrderOf ↑a = n / n.gcd a
<VAR>a : ℕ<VAR>n : ℕ<VAR>a0 : a ≠ 0<GOAL>addOrderOf ↑a = n / n.gcd a
<VAR>n : ℕ<VAR>R : Type u_1<VAR>AddGroupWithOne R<GOAL>ZMod.cast 0 = 0
<VAR>n : ℕ<VAR>R : Type u_1<VAR>AddGroupWithOne R<VAR>NeZero n<VAR>a : ZMod n<GOAL>a.cast = ↑a.val
<VAR>n : ℕ<VAR>R : Type u_1<VAR>AddGroupWithOne R<VAR>S : Type u_2<VAR>AddGroupWithOne S<VAR>a : ZMod n<GOAL>a.cast.1 = a.cast
<VAR>n : ℕ<VAR>R : Type u_1<VAR>AddGroupWithOne R<VAR>S : Type u_2<VAR>AddGroupWithOne S<VAR>a : ZMod n<GOAL>a.cast.2 = a.cast
<VAR>n : ℕ<VAR>NeZero n<VAR>a : ZMod n<GOAL>↑a.val = a
<VAR>n : ℕ<VAR>NeZero n<GOAL>Function.RightInverse ZMod.val Nat.cast
<VAR>n : ℕ<VAR>NeZero n<GOAL>Function.Surjective Nat.cast
<VAR>n : ℕ<VAR>a : ZMod n<GOAL>↑a.cast = a
<VAR>n : ℕ<GOAL>Function.RightInverse ZMod.cast Int.cast
<VAR>n : ℕ<GOAL>Function.Surjective Int.cast
<VAR>n : ℕ<VAR>i : ZMod n<GOAL>i.cast = i
<VAR>n : ℕ<GOAL>ZMod.cast = id
<VAR>n : ℕ<VAR>R : Type u_1<VAR>Ring R<VAR>NeZero n<GOAL>Nat.cast ∘ ZMod.val = ZMod.cast
<VAR>n : ℕ<VAR>R : Type u_1<VAR>Ring R<GOAL>Int.cast ∘ ZMod.cast = ZMod.cast
<VAR>n : ℕ<VAR>R : Type u_1<VAR>Ring R<VAR>NeZero n<VAR>i : ZMod n<GOAL>↑i.val = i.cast
<VAR>n : ℕ<VAR>R : Type u_1<VAR>Ring R<VAR>i : ZMod n<GOAL>↑i.cast = i.cast
<VAR>n : ℕ<VAR>a b : ZMod n<GOAL>(a + b).cast = if ↑n ≤ a.cast + b.cast then a.cast + b.cast - ↑n else a.cast + b.cast
<VAR>n : ℕ<VAR>R : Type u_1<VAR>Ring R<VAR>m : ℕ<VAR>CharP R m<VAR>h : m ∣ n<GOAL>ZMod.cast 1 = 1
<VAR>n : ℕ<VAR>R : Type u_1<VAR>Ring R<VAR>m : ℕ<VAR>CharP R m<VAR>h : m ∣ n<VAR>a b : ZMod n<GOAL>(a + b).cast = a.cast + b.cast
<VAR>n : ℕ<VAR>R : Type u_1<VAR>Ring R<VAR>m : ℕ<VAR>CharP R m<VAR>h : m ∣ n<VAR>a b : ZMod n<GOAL>(a * b).cast = a.cast * b.cast
<VAR>n : ℕ<VAR>R : Type u_1<VAR>Ring R<VAR>m : ℕ<VAR>CharP R m<VAR>h : m ∣ n<VAR>i : ZMod n<GOAL>(ZMod.castHom h R) i = i.cast
<VAR>n : ℕ<VAR>R : Type u_1<VAR>Ring R<VAR>m : ℕ<VAR>CharP R m<VAR>h : m ∣ n<VAR>a b : ZMod n<GOAL>(a - b).cast = a.cast - b.cast
<VAR>n : ℕ<VAR>R : Type u_1<VAR>Ring R<VAR>m : ℕ<VAR>CharP R m<VAR>h : m ∣ n<VAR>a : ZMod n<GOAL>(-a).cast = -a.cast
<VAR>n : ℕ<VAR>R : Type u_1<VAR>Ring R<VAR>m : ℕ<VAR>CharP R m<VAR>h : m ∣ n<VAR>a : ZMod n<VAR>k : ℕ<GOAL>(a ^ k).cast = a.cast ^ k
<VAR>n : ℕ<VAR>R : Type u_1<VAR>Ring R<VAR>m : ℕ<VAR>CharP R m<VAR>h : m ∣ n<VAR>k : ℕ<GOAL>(↑k).cast = ↑k
<VAR>n : ℕ<VAR>R : Type u_1<VAR>Ring R<VAR>m : ℕ<VAR>CharP R m<VAR>h : m ∣ n<VAR>k : ℤ<GOAL>(↑k).cast = ↑k
<VAR>n : ℕ<VAR>R : Type u_1<VAR>Ring R<VAR>CharP R n<GOAL>ZMod.cast 1 = 1
<VAR>n : ℕ<VAR>R : Type u_1<VAR>Ring R<VAR>CharP R n<VAR>a b : ZMod n<GOAL>(a + b).cast = a.cast + b.cast
<VAR>n : ℕ<VAR>R : Type u_1<VAR>Ring R<VAR>CharP R n<VAR>a b : ZMod n<GOAL>(a * b).cast = a.cast * b.cast
<VAR>n : ℕ<VAR>R : Type u_1<VAR>Ring R<VAR>CharP R n<VAR>a b : ZMod n<GOAL>(a - b).cast = a.cast - b.cast
<VAR>n : ℕ<VAR>R : Type u_1<VAR>Ring R<VAR>CharP R n<VAR>a : ZMod n<VAR>k : ℕ<GOAL>(a ^ k).cast = a.cast ^ k
<VAR>n : ℕ<VAR>R : Type u_1<VAR>Ring R<VAR>CharP R n<VAR>k : ℕ<GOAL>(↑k).cast = ↑k
<VAR>n : ℕ<VAR>R : Type u_1<VAR>Ring R<VAR>CharP R n<VAR>k : ℤ<GOAL>(↑k).cast = ↑k
<VAR>n : ℕ<VAR>R : Type u_1<VAR>Ring R<VAR>CharP R n<GOAL>Function.Injective ⇑(ZMod.castHom ⋯ R)
<VAR>n : ℕ<VAR>R : Type u_1<VAR>Ring R<VAR>CharP R n<VAR>Fintype R<VAR>h : Fintype.card R = n<GOAL>Function.Bijective ⇑(ZMod.castHom ⋯ R)
<VAR>R : Type u_1<VAR>Ring R<VAR>Fintype R<VAR>p : ℕ<VAR>CharP R p<VAR>hp : Nat.Prime p<VAR>hR : Fintype.card R = p<GOAL>ZMod.ringEquivOfPrime R hp hR = ZMod.ringEquiv R hR
<VAR>a : ℕ<GOAL>ZMod.ringEquivCongr ⋯ = RingEquiv.refl (ZMod a)
<VAR>a : ℕ<VAR>x : ZMod a<GOAL>(ZMod.ringEquivCongr ⋯) x = x
<VAR>a b : ℕ<VAR>hab : a = b<GOAL>(ZMod.ringEquivCongr hab).symm = ZMod.ringEquivCongr ⋯
<VAR>a b c : ℕ<VAR>hab : a = b<VAR>hbc : b = c<GOAL>(ZMod.ringEquivCongr hab).trans (ZMod.ringEquivCongr hbc) = ZMod.ringEquivCongr ⋯
<VAR>a b c : ℕ<VAR>hab : a = b<VAR>hbc : b = c<VAR>x : ZMod a<GOAL>(ZMod.ringEquivCongr hbc) ((ZMod.ringEquivCongr hab) x) = (ZMod.ringEquivCongr ⋯) x
<VAR>a b : ℕ<VAR>h : a = b<VAR>x : ZMod a<GOAL>((ZMod.ringEquivCongr h) x).val = x.val
<VAR>a b : ℕ<VAR>h : a = b<VAR>z : ℤ<GOAL>(ZMod.ringEquivCongr h) ↑z = ↑z
<VAR>a b : ℤ<VAR>c : ℕ<GOAL>↑a = ↑b ↔ a ≡ b [ZMOD ↑c]
<VAR>a b : ℤ<VAR>c : ℕ<GOAL>↑a = ↑b ↔ a % ↑c = b % ↑c
<VAR>a b c : ℕ<GOAL>↑a = ↑b ↔ a ≡ b [MOD c]
<VAR>a b c : ℕ<GOAL>↑a = ↑b ↔ a % c = b % c
<VAR>a : ℤ<VAR>b : ℕ<GOAL>↑a = 0 ↔ ↑b ∣ a
<VAR>a b : ℤ<VAR>c : ℕ<GOAL>↑a = ↑b ↔ ↑c ∣ b - a
<VAR>a b : ℕ<GOAL>↑a = 0 ↔ b ∣ a
<VAR>n : ℕ<VAR>a : ℤ<VAR>NeZero n<GOAL>↑(↑a).val = a % ↑n
<VAR>n : ℕ<VAR>a : ℤ<GOAL>(↑a).cast = a % ↑n
<VAR>n : ℕ<VAR>x y : ZMod n<GOAL>(x + y).cast = (x.cast + y.cast) % ↑n
<VAR>n : ℕ<VAR>x y : ZMod n<GOAL>(x * y).cast = x.cast * y.cast % ↑n
<VAR>n : ℕ<VAR>x y : ZMod n<GOAL>(x - y).cast = (x.cast - y.cast) % ↑n
<VAR>n : ℕ<VAR>x : ZMod n<GOAL>(-x).cast = -x.cast % ↑n
<VAR>R : Type u_1<VAR>Ring R<VAR>n : ℕ<GOAL>(-1).cast = ↑n - 1
<VAR>R : Type u_1<VAR>Ring R<VAR>n : ℕ<VAR>k : ZMod n<GOAL>(k - 1).cast = (if k = 0 then ↑n else k.cast) - 1
<VAR>p n : ℕ<VAR>z : ZMod p<VAR>NeZero p<GOAL>↑n = z ↔ ∃ k, n = z.val + p * k
<VAR>p : ℕ<VAR>n : ℤ<VAR>z : ZMod p<VAR>NeZero p<GOAL>↑n = z ↔ ∃ k, n = ↑z.val + ↑p * k
<VAR>a : ℤ<VAR>b : ℕ<GOAL>↑(a % ↑b) = ↑a
<VAR>n : ℕ<GOAL>(Int.castAddHom (ZMod n)).ker = AddSubgroup.zmultiples ↑n
<VAR>m n : ℕ<VAR>nzm : NeZero m<VAR>h : m ≤ n<GOAL>Function.Injective ZMod.cast
<VAR>m n : ℕ<VAR>NeZero m<VAR>h : m ≤ n<VAR>a : ZMod m<GOAL>a.cast = 0 ↔ a = 0
<VAR>p : ℕ<VAR>z : ℤ<VAR>_h : 0 ≤ z<GOAL>↑z.toNat = ↑z
<VAR>n : ℕ<VAR>NeZero n<GOAL>Function.Injective ZMod.val
<VAR>n : ℕ<GOAL>ZMod.val 1 = 1 % n
<VAR>n : ℕ<VAR>Fact (1 < n)<GOAL>ZMod.val 1 = 1
<VAR>n : ℕ<GOAL>n ≠ 1 → ZMod.val 1 = 1
<VAR>n : ℕ<VAR>NeZero n<VAR>a b : ZMod n<GOAL>(a + b).val = (a.val + b.val) % n
<VAR>n : ℕ<VAR>a b : ZMod n<VAR>h : a.val + b.val < n<GOAL>(a + b).val = a.val + b.val
<VAR>n : ℕ<VAR>NeZero n<VAR>a b : ZMod n<VAR>h : n ≤ a.val + b.val<GOAL>a.val + b.val = (a + b).val + n
<VAR>n : ℕ<VAR>NeZero n<VAR>a b : ZMod n<VAR>h : n ≤ a.val + b.val<GOAL>(a + b).val = a.val + b.val - n
<VAR>n : ℕ<VAR>a b : ZMod n<GOAL>(a + b).val ≤ a.val + b.val
<VAR>n : ℕ<VAR>a b : ZMod n<GOAL>(a * b).val = a.val * b.val % n
<VAR>n : ℕ<VAR>a b : ZMod n<GOAL>(a * b).val ≤ a.val * b.val
<VAR>n : ℕ<VAR>a b : ZMod n<VAR>h : a.val * b.val < n<GOAL>(a * b).val = a.val * b.val
<VAR>n : ℕ<GOAL>0⁻¹ = 0
<VAR>n : ℕ<VAR>a : ZMod n<GOAL>a * a⁻¹ = ↑(a.val.gcd n)
<VAR>n : ℕ<GOAL>1⁻¹ = 1
<VAR>a n : ℕ<GOAL>↑(a % n) = ↑a
<VAR>n : ℕ<VAR>a b : ℕ<GOAL>↑a = ↑b ↔ a ≡ b [MOD n]
<VAR>n : ℕ<VAR>x : ℕ<VAR>h : x.Coprime n<GOAL>↑x * (↑x)⁻¹ = 1
<VAR>n : ℕ<VAR>x : ℕ<VAR>h : x.Coprime n<GOAL>↑(ZMod.unitOfCoprime x h) = ↑x
<VAR>n : ℕ<VAR>u : (ZMod n)ˣ<GOAL>(↑u).val.Coprime n
<VAR>m n : ℕ<GOAL>IsUnit ↑m ↔ m.Coprime n
<VAR>n p : ℕ<VAR>hp : Nat.Prime p<GOAL>IsUnit ↑p ↔ ¬p ∣ n
<VAR>n p : ℕ<VAR>hp : Nat.Prime p<VAR>h : ¬p ∣ n<GOAL>IsUnit ↑p
<VAR>n : ℕ<VAR>u : (ZMod n)ˣ<GOAL>(↑u)⁻¹ = ↑u⁻¹
<VAR>n : ℕ<VAR>a : ZMod n<VAR>h : IsUnit a<GOAL>a * a⁻¹ = 1
<VAR>n : ℕ<VAR>a : ZMod n<VAR>h : IsUnit a<GOAL>a⁻¹ * a = 1
<VAR>n : ℕ<VAR>a b : ZMod n<VAR>h : a * b = 1<GOAL>a⁻¹ = b
<VAR>n : ℕ<GOAL>Subsingleton (ZMod n) ↔ n = 1
<VAR>n : ℕ<GOAL>Nontrivial (ZMod n) ↔ n ≠ 1
<VAR>n : ℕ<VAR>hn : Odd n<VAR>a : ZMod n<GOAL>a + a = 0 ↔ a = 0
<VAR>n : ℕ<VAR>hn : Odd n<VAR>a : ZMod n<VAR>ha : a ≠ 0<GOAL>a ≠ -a
<VAR>n : ℕ<VAR>Fact (2 < n)<GOAL>-1 ≠ 1
<VAR>a : ℤ<GOAL>↑a.natAbs = ↑a
<VAR>n : ℕ<VAR>a : ZMod n<GOAL>a.val = 0 ↔ a = 0
<VAR>n : ℕ<VAR>a : ZMod n<GOAL>a.val ≠ 0 ↔ a ≠ 0
<VAR>n : ℕ<VAR>a : ZMod n<GOAL>-a = a ↔ a = 0 ∨ 2 * a.val = n
<VAR>n : ℕ<VAR>NeZero n<VAR>a : ZMod n<GOAL>(-a).val = (n - a.val) % n
<VAR>n : ℕ<VAR>NeZero n<VAR>a : ZMod n<GOAL>(-a).val = if a = 0 then 0 else n - a.val
<VAR>n : ℕ<VAR>nz : NeZero n<VAR>a : ZMod n<VAR>na : NeZero a<GOAL>(-a).val = n - a.val
<VAR>n : ℕ<VAR>NeZero n<VAR>a b : ZMod n<VAR>h : b.val ≤ a.val<GOAL>(a - b).val = a.val - b.val
<VAR>m n : ℕ<VAR>nzm : NeZero m<VAR>a : ZMod m<VAR>h : a.val < n<GOAL>a.cast.val = a.val
<VAR>m n : ℕ<VAR>hm : NeZero m<VAR>h : m ≤ n<VAR>a : ZMod m<GOAL>a.cast.cast = a
<VAR>x : ZMod 0<GOAL>x.valMinAbs = x
<VAR>n : ℕ<VAR>NeZero n<VAR>x : ZMod n<GOAL>x.valMinAbs = if x.val ≤ n / 2 then ↑x.val else ↑x.val - ↑n
<VAR>n : ℕ<VAR>x : ZMod n<GOAL>↑x.valMinAbs = x
<VAR>n : ℕ<GOAL>Function.Injective ZMod.valMinAbs
<VAR>n m : ℕ<GOAL>m ≤ n / 2 ↔ ↑m * 2 ≤ ↑n
<VAR>n : ℕ<VAR>NeZero n<VAR>x : ZMod n<GOAL>0 ≤ x.valMinAbs ↔ x.val ≤ n / 2
<VAR>n : ℕ<VAR>a : ZMod n<GOAL>a.valMinAbs * 2 = ↑n ↔ 2 * a.val = n