ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>m : Multiset α<VAR>p : m.ToType → Prop<GOAL>(∀ (x : m.ToType), p x) ↔ ∀ (x : α) (i : Fin (Multiset.count x m)), p ⟨x, i⟩
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>m : Multiset α<VAR>p : m.ToType → Prop<GOAL>(∃ x, p x) ↔ ∃ x i, p ⟨x, i⟩
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>m : Multiset α<VAR>p : α × ℕ<GOAL>p ∈ m.toEnumFinset ↔ p.2 < Multiset.count p.1 m
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>m : Multiset α<VAR>p : α × ℕ<VAR>h : p ∈ m.toEnumFinset<GOAL>p.1 ∈ m
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>m : Multiset α<VAR>a : α<GOAL>Finset.filter (fun x => x.1 = a) m.toEnumFinset = {a} ×ˢ Finset.range (Multiset.count a m)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>m : Multiset α<GOAL>Multiset.map Prod.fst m.toEnumFinset.val = m
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>m : Multiset α<GOAL>Finset.image Prod.fst m.toEnumFinset = m.toFinset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>m : Multiset α<VAR>s : Finset (α × ℕ)<VAR>hsm : s ⊆ m.toEnumFinset<GOAL>Multiset.map Prod.fst s.val ≤ m
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>m₁ m₂ : Multiset α<VAR>h : m₁ ≤ m₂<GOAL>m₁.toEnumFinset ⊆ m₂.toEnumFinset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>m₁ m₂ : Multiset α<GOAL>m₁.toEnumFinset ⊆ m₂.toEnumFinset ↔ m₁ ≤ m₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>m : Multiset α<VAR>x : m.ToType<GOAL>m.coeEmbedding x = (x.fst, ↑x.snd)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>m : Multiset α<VAR>x : { x // x ∈ m.toEnumFinset }<GOAL>↑(m.coeEquiv.symm x).snd = (↑x).2
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>m : Multiset α<VAR>x : m.ToType<GOAL>↑(m.coeEquiv x) = m.coeEmbedding x
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>m : Multiset α<VAR>x : { x // x ∈ m.toEnumFinset }<GOAL>(m.coeEquiv.symm x).fst = (↑x).1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>m : Multiset α<GOAL>m.coeEquiv.toEmbedding.trans (Function.Embedding.subtype fun x => x ∈ m.toEnumFinset) = m.coeEmbedding
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>m : Multiset α<GOAL>Finset.map m.coeEmbedding Finset.univ = m.toEnumFinset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>m : Multiset α<GOAL>Multiset.map (fun x => x.fst) Finset.univ.val = m
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>β : Type u_2<VAR>m : Multiset α<VAR>f : α → β<GOAL>Multiset.map (fun x => f x.fst) Finset.univ.val = Multiset.map f m
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>m : Multiset α<GOAL>m.toEnumFinset.card = Multiset.card m
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>m : Multiset α<GOAL>Fintype.card m.ToType = Multiset.card m
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>CommMonoid α<VAR>m : Multiset α<GOAL>m.prod = ∏ x : m.ToType, x.fst
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>AddCommMonoid α<VAR>m : Multiset α<GOAL>m.sum = ∑ x : m.ToType, x.fst
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>AddCommMonoid α<VAR>m : Multiset α<GOAL>m.sum = ∑ x ∈ m.toEnumFinset, x.1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>CommMonoid α<VAR>m : Multiset α<GOAL>m.prod = ∏ x ∈ m.toEnumFinset, x.1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>β : Type u_2<VAR>CommMonoid β<VAR>m : Multiset α<VAR>f : α → ℕ → β<GOAL>∏ x ∈ m.toEnumFinset, f x.1 x.2 = ∏ x : m.ToType, f x.fst ↑x.snd
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>β : Type u_2<VAR>AddCommMonoid β<VAR>m : Multiset α<VAR>f : α → ℕ → β<GOAL>∑ x ∈ m.toEnumFinset, f x.1 x.2 = ∑ x : m.ToType, f x.fst ↑x.snd
<VAR>α' β' : Type u_1<VAR>s : Multiset α'<VAR>f : α' → β'<GOAL>f <$> s = Multiset.map f s
<VAR>α β : Type u_1<GOAL>(fun x x_1 => x >>= x_1) = Multiset.bind
<VAR>α β : Type u_1<VAR>h : α → β<GOAL>Functor.map h ∘ Coe.coe = Coe.coe ∘ Functor.map h
<VAR>α : Type u_1<VAR>x : Multiset α<GOAL>Multiset.traverse pure x = x
<VAR>G H : Type u_1 → Type u_1<VAR>Applicative G<VAR>Applicative H<VAR>CommApplicative G<VAR>CommApplicative H<VAR>α β γ : Type u_1<VAR>g : α → G β<VAR>h : β → H γ<VAR>x : Multiset α<GOAL>Multiset.traverse (Functor.Comp.mk ∘ Functor.map h ∘ g) x = Functor.Comp.mk (Multiset.traverse h <$> Multiset.traverse g x)
<VAR>G : Type u_1 → Type u_1<VAR>Applicative G<VAR>CommApplicative G<VAR>α β γ : Type u_1<VAR>g : α → G β<VAR>h : β → γ<VAR>x : Multiset α<GOAL>Functor.map h <$> Multiset.traverse g x = Multiset.traverse (Functor.map h ∘ g) x
<VAR>G : Type u_1 → Type u_1<VAR>Applicative G<VAR>CommApplicative G<VAR>α β γ : Type u_1<VAR>g : α → β<VAR>h : β → G γ<VAR>x : Multiset α<GOAL>Multiset.traverse h (Multiset.map g x) = Multiset.traverse (h ∘ g) x
<VAR>G H : Type u_1 → Type u_1<VAR>Applicative G<VAR>Applicative H<VAR>CommApplicative G<VAR>CommApplicative H<VAR>eta : ApplicativeTransformation G H<VAR>α β : Type u_1<VAR>f : α → G β<VAR>x : Multiset α<GOAL>(fun {α} => eta.app α) (Multiset.traverse f x) = Multiset.traverse ((fun {α} => eta.app α) ∘ f) x
<VAR>α : Type u_1<VAR>l : List α<GOAL>Multiset.powersetAux l = List.map Multiset.ofList l.sublists
<VAR>α : Type u_1<VAR>l : List α<VAR>s : Multiset α<GOAL>s ∈ Multiset.powersetAux l ↔ s ≤ ↑l
<VAR>α : Type u_1<VAR>l : List α<GOAL>(Multiset.powersetAux l).Perm (Multiset.powersetAux' l)
<VAR>α : Type u_1<GOAL>Multiset.powersetAux' [] = [0]
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<GOAL>Multiset.powersetAux' (a :: l) = Multiset.powersetAux' l ++ List.map (Multiset.cons a) (Multiset.powersetAux' l)
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>p : l₁.Perm l₂<GOAL>(Multiset.powersetAux' l₁).Perm (Multiset.powersetAux' l₂)
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>p : l₁.Perm l₂<GOAL>(Multiset.powersetAux l₁).Perm (Multiset.powersetAux l₂)
<VAR>α : Type u_1<VAR>l : List α<GOAL>(↑l).powerset = ↑(List.map Multiset.ofList l.sublists)
<VAR>α : Type u_1<VAR>l : List α<GOAL>(↑l).powerset = ↑(List.map Multiset.ofList l.sublists')
<VAR>α : Type u_1<GOAL>Multiset.powerset 0 = {0}
<VAR>α : Type u_1<VAR>a : α<VAR>s : Multiset α<GOAL>(a ::ₘ s).powerset = s.powerset + Multiset.map (Multiset.cons a) s.powerset
<VAR>α : Type u_1<VAR>s t : Multiset α<GOAL>s ∈ t.powerset ↔ s ≤ t
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>Multiset.map singleton s ≤ s.powerset
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>Multiset.card s.powerset = 2 ^ Multiset.card s
<VAR>α : Type u_1<VAR>l : List α<VAR>x : Multiset α × Multiset α<VAR>h : x ∈ (Multiset.powersetAux l).revzip<GOAL>x.1 + x.2 = ↑l
<VAR>α : Type u_1<VAR>l : List α<VAR>x : Multiset α × Multiset α<VAR>h : x ∈ (Multiset.powersetAux' l).revzip<GOAL>x.1 + x.2 = ↑l
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>l : List α<VAR>l' : List (Multiset α)<VAR>H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l<GOAL>l'.revzip = List.map (fun x => (x, ↑l - x)) l'
<VAR>α : Type u_1<VAR>l : List α<GOAL>(Multiset.powersetAux l).revzip.Perm (Multiset.powersetAux' l).revzip
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>p : l₁.Perm l₂<GOAL>(Multiset.powersetAux l₁).revzip.Perm (Multiset.powersetAux l₂).revzip
<VAR>α : Type u_1<VAR>n : ℕ<VAR>l : List α<GOAL>Multiset.powersetCardAux n l = List.map Multiset.ofList (List.sublistsLen n l)
<VAR>α : Type u_1<VAR>n : ℕ<VAR>l : List α<VAR>s : Multiset α<GOAL>s ∈ Multiset.powersetCardAux n l ↔ s ≤ ↑l ∧ Multiset.card s = n
<VAR>α : Type u_1<VAR>l : List α<GOAL>Multiset.powersetCardAux 0 l = [0]
<VAR>α : Type u_1<VAR>n : ℕ<GOAL>Multiset.powersetCardAux (n + 1) [] = []
<VAR>α : Type u_1<VAR>n : ℕ<VAR>a : α<VAR>l : List α<GOAL>Multiset.powersetCardAux (n + 1) (a :: l) = Multiset.powersetCardAux (n + 1) l ++ List.map (Multiset.cons a) (Multiset.powersetCardAux n l)
<VAR>α : Type u_1<VAR>n : ℕ<VAR>l₁ l₂ : List α<VAR>p : l₁.Perm l₂<GOAL>(Multiset.powersetCardAux n l₁).Perm (Multiset.powersetCardAux n l₂)
<VAR>α : Type u_1<VAR>n : ℕ<VAR>l : List α<GOAL>Multiset.powersetCard n ↑l = ↑(Multiset.powersetCardAux n l)
<VAR>α : Type u_1<VAR>n : ℕ<VAR>l : List α<GOAL>Multiset.powersetCard n ↑l = ↑(List.map Multiset.ofList (List.sublistsLen n l))
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>Multiset.powersetCard 0 s = {0}
<VAR>α : Type u_1<VAR>n : ℕ<GOAL>Multiset.powersetCard (n + 1) 0 = 0
<VAR>α : Type u_1<VAR>n : ℕ<VAR>a : α<VAR>s : Multiset α<GOAL>Multiset.powersetCard (n + 1) (a ::ₘ s) = Multiset.powersetCard (n + 1) s + Multiset.map (Multiset.cons a) (Multiset.powersetCard n s)
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>Multiset.powersetCard 1 s = Multiset.map singleton s
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s t : Multiset α<GOAL>s ∈ Multiset.powersetCard n t ↔ s ≤ t ∧ Multiset.card s = n
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s : Multiset α<GOAL>Multiset.card (Multiset.powersetCard n s) = (Multiset.card s).choose n
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s : Multiset α<GOAL>Multiset.powersetCard n s ≤ s.powerset
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s t : Multiset α<VAR>h : s ≤ t<GOAL>Multiset.powersetCard n s ≤ Multiset.powersetCard n t
<VAR>α : Type u_2<VAR>n : ℕ<VAR>s : Multiset α<VAR>h : Multiset.card s < n<GOAL>Multiset.powersetCard n s = 0
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>i : ℕ<VAR>hi : 0 < i<GOAL>Multiset.powersetCard (Multiset.card s + i) s = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>n : ℕ<VAR>s : Multiset α<GOAL>Multiset.powersetCard n (Multiset.map f s) = Multiset.map (Multiset.map f) (Multiset.powersetCard n s)
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>Pairwise fun i j => (Multiset.powersetCard i s).Disjoint (Multiset.powersetCard j s)
<VAR>α : Type u_2<VAR>S : Multiset α<GOAL>((Multiset.range (Multiset.card S + 1)).bind fun k => Multiset.powersetCard k S) = S.powerset
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>s.powerset.Nodup ↔ s.Nodup
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s : Multiset α<VAR>h : s.Nodup<GOAL>(Multiset.powersetCard n s).Nodup
<VAR>α : Type u_1<VAR>xs : List α<GOAL>(↑xs).sym2 = ↑xs.sym2
<VAR>α : Type u_1<VAR>m : Multiset α<GOAL>m.sym2 = 0 ↔ m = 0
<VAR>α : Type u_1<GOAL>Multiset.sym2 0 = 0
<VAR>α : Type u_1<VAR>a : α<VAR>m : Multiset α<GOAL>(a ::ₘ m).sym2 = Multiset.map (fun b => s(a, b)) (a ::ₘ m) + m.sym2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>m : Multiset α<GOAL>(Multiset.map f m).sym2 = Multiset.map (Sym2.map f) m.sym2
<VAR>α : Type u_1<VAR>m : Multiset α<VAR>a b : α<GOAL>s(a, b) ∈ m.sym2 ↔ a ∈ m ∧ b ∈ m
<VAR>α : Type u_1<VAR>m : Multiset α<VAR>z : Sym2 α<GOAL>z ∈ m.sym2 ↔ ∀ y ∈ z, y ∈ m
<VAR>α : Type u_1<VAR>m : Multiset α<VAR>h : m.Nodup<GOAL>m.sym2.Nodup
<VAR>α : Type u_1<VAR>m m' : Multiset α<VAR>h : m ≤ m'<GOAL>m.sym2 ≤ m'.sym2
<VAR>α : Type u_1<GOAL>Monotone Multiset.sym2
<VAR>α : Type u_1<VAR>m : Multiset α<GOAL>Multiset.card m.sym2 = (Multiset.card m + 1).choose 2
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>m : Multiset α<GOAL>m.sym2.dedup = m.dedup.sym2
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>δ : α → Sort u_2<VAR>m : Multiset α<VAR>a : α<VAR>b : δ a<VAR>f : (a : α) → a ∈ m → δ a<VAR>h : a ∈ a ::ₘ m<GOAL>Multiset.Pi.cons m a b f a h = b
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>δ : α → Sort u_2<VAR>m : Multiset α<VAR>a a' : α<VAR>b : δ a<VAR>f : (a : α) → a ∈ m → δ a<VAR>h' : a' ∈ a ::ₘ m<VAR>h : a' ≠ a<GOAL>Multiset.Pi.cons m a b f a' h' = f a' ⋯
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>δ : α → Sort u_2<VAR>a a' : α<VAR>b : δ a<VAR>b' : δ a'<VAR>m : Multiset α<VAR>f : (a : α) → a ∈ m → δ a<VAR>h : a ≠ a'<GOAL>HEq (Multiset.Pi.cons (a' ::ₘ m) a b (Multiset.Pi.cons m a' b' f)) (Multiset.Pi.cons (a ::ₘ m) a' b' (Multiset.Pi.cons m a b f))
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>δ : α → Sort u_2<VAR>m : Multiset α<VAR>a : α<VAR>f : (a' : α) → a' ∈ a ::ₘ m → δ a'<GOAL>(Multiset.Pi.cons m a (f a ⋯) fun a' ha' => f a' ⋯) = f
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>δ : α → Sort u_2<VAR>m : Multiset α<VAR>a : α<VAR>b : δ a<VAR>f : (a' : α) → a' ∈ m → δ a'<VAR>δ' : α → Sort u_3<VAR>φ : ⦃a' : α⦄ → δ a' → δ' a'<GOAL>(Multiset.Pi.cons m a (φ b) fun a' ha' => φ (f a' ha')) = fun a' ha' => φ (Multiset.Pi.cons m a b f a' ha')
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>δ : α → Sort u_2<VAR>m : Multiset α<VAR>a : α<VAR>r : ⦃a : α⦄ → δ a → δ a → Prop<VAR>b₁ b₂ : δ a<VAR>f₁ f₂ : (a' : α) → a' ∈ m → δ a'<VAR>hb : r b₁ b₂<VAR>hf : ∀ (a : α) (ha : a ∈ m), r (f₁ a ha) (f₂ a ha)<GOAL>∀ (a_1 : α) (ha : a_1 ∈ a ::ₘ m), r (Multiset.Pi.cons m a b₁ f₁ a_1 ha) (Multiset.Pi.cons m a b₂ f₂ a_1 ha)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>δ : α → Sort u_2<VAR>a : α<VAR>b : δ a<VAR>s : Multiset α<VAR>hs : a ∉ s<GOAL>Function.Injective (Multiset.Pi.cons s a b)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>β : α → Type u_2<VAR>t : (a : α) → Multiset (β a)<GOAL>Multiset.pi 0 t = {Multiset.Pi.empty β}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>β : α → Type u_2<VAR>m : Multiset α<VAR>t : (a : α) → Multiset (β a)<VAR>a : α<GOAL>(a ::ₘ m).pi t = (t a).bind fun b => Multiset.map (Multiset.Pi.cons m a b) (m.pi t)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>β : α → Type u_2<VAR>m : Multiset α<VAR>t : (a : α) → Multiset (β a)<GOAL>Multiset.card (m.pi t) = (Multiset.map (fun a => Multiset.card (t a)) m).prod
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>β : α → Type u_2<VAR>s : Multiset α<VAR>t : (a : α) → Multiset (β a)<GOAL>s.Nodup → (∀ a ∈ s, (t a).Nodup) → (s.pi t).Nodup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>β : α → Type u_2<VAR>m : Multiset α<VAR>t : (a : α) → Multiset (β a)<VAR>f : (a : α) → a ∈ m → β a<GOAL>f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
<VAR>α : Type u<VAR>s : Set α<GOAL>s.Finite ↔ Nonempty (Fintype ↑s)
<VAR>α : Type u<VAR>s : Set α<GOAL>Finite ↑s ↔ s.Finite
<VAR>α : Type u<VAR>s : Set α<VAR>Finite ↑s<GOAL>s.Finite
<VAR>α : Type u<VAR>p : Set α<VAR>s : Finset α<VAR>H : ∀ (x : α), x ∈ s ↔ x ∈ p<GOAL>p.Finite
<VAR>α : Type u<VAR>s : Set α<VAR>h : s.Finite<GOAL>Finite ↑s
<VAR>α : Type u<VAR>s : Set α<VAR>Fintype ↑s<VAR>h : s.Finite<GOAL>h.toFinset = s.toFinset
<VAR>α : Type u<VAR>s : Set α<VAR>Fintype ↑s<GOAL>⋯.toFinset = s.toFinset
<VAR>α : Type u<VAR>s : Set α<VAR>h : s.Finite<GOAL>∃ s', ∀ (a : α), a ∈ s' ↔ a ∈ s
<VAR>α : Type u<VAR>s : Set α<VAR>h : s.Finite<GOAL>∃ s', ↑s' = s
<VAR>α : Type u<VAR>s : Set α<GOAL>¬s.Infinite ↔ s.Finite
<VAR>α : Type u<VAR>s : Set α<GOAL>s.Finite ∨ s.Infinite
<VAR>α : Type u<VAR>s : Set α<GOAL>s.Infinite ∨ s.Finite
<VAR>α : Type u<VAR>s : Set α<VAR>a : α<VAR>hs : s.Finite<GOAL>a ∈ hs.toFinset ↔ a ∈ s
<VAR>α : Type u<VAR>s : Set α<VAR>hs : s.Finite<GOAL>↑hs.toFinset = s
<VAR>α : Type u<VAR>s : Set α<VAR>hs : s.Finite<GOAL>hs.toFinset.Nonempty ↔ s.Nonempty
<VAR>α : Type u<VAR>s : Set α<VAR>hs : s.Finite<GOAL>{ x // x ∈ hs.toFinset } = ↑s
<VAR>α : Type u<VAR>s : Set α<VAR>hs : s.Finite<VAR>a : { a // (fun x => x ∈ s) a }<GOAL>↑(hs.subtypeEquivToFinset a) = ↑a
<VAR>α : Type u<VAR>s : Set α<VAR>hs : s.Finite<VAR>b : { b // (fun x => x ∈ hs.toFinset) b }<GOAL>↑(hs.subtypeEquivToFinset.symm b) = ↑b
<VAR>α : Type u<VAR>s t : Set α<VAR>hs : s.Finite<VAR>ht : t.Finite<GOAL>hs.toFinset = ht.toFinset ↔ s = t
<VAR>α : Type u<VAR>s : Set α<VAR>hs : s.Finite<VAR>t : Finset α<GOAL>hs.toFinset ⊆ t ↔ s ⊆ ↑t
<VAR>α : Type u<VAR>s : Set α<VAR>hs : s.Finite<VAR>t : Finset α<GOAL>hs.toFinset ⊂ t ↔ s ⊂ ↑t
<VAR>α : Type u<VAR>t : Set α<VAR>ht : t.Finite<VAR>s : Finset α<GOAL>s ⊆ ht.toFinset ↔ ↑s ⊆ t
<VAR>α : Type u<VAR>t : Set α<VAR>ht : t.Finite<VAR>s : Finset α<GOAL>s ⊂ ht.toFinset ↔ ↑s ⊂ t
<VAR>α : Type u<VAR>s t : Set α<VAR>hs : s.Finite<VAR>ht : t.Finite<GOAL>hs.toFinset ⊆ ht.toFinset ↔ s ⊆ t
<VAR>α : Type u<VAR>s t : Set α<VAR>hs : s.Finite<VAR>ht : t.Finite<GOAL>hs.toFinset ⊂ ht.toFinset ↔ s ⊂ t
<VAR>α : Type u<VAR>Fintype α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>h : {x | p x}.Finite<GOAL>h.toFinset = Finset.filter p Finset.univ
<VAR>α : Type u<VAR>s t : Set α<VAR>hs : s.Finite<VAR>ht : t.Finite<GOAL>Disjoint hs.toFinset ht.toFinset ↔ Disjoint s t
<VAR>α : Type u<VAR>s t : Set α<VAR>DecidableEq α<VAR>hs : s.Finite<VAR>ht : t.Finite<VAR>h : (s ∩ t).Finite<GOAL>h.toFinset = hs.toFinset ∩ ht.toFinset
<VAR>α : Type u<VAR>s t : Set α<VAR>DecidableEq α<VAR>hs : s.Finite<VAR>ht : t.Finite<VAR>h : (s ∪ t).Finite<GOAL>h.toFinset = hs.toFinset ∪ ht.toFinset
<VAR>α : Type u<VAR>s t : Set α<VAR>DecidableEq α<VAR>hs : s.Finite<VAR>ht : t.Finite<VAR>h : (s \ t).Finite<GOAL>h.toFinset = hs.toFinset \ ht.toFinset
<VAR>α : Type u<VAR>s t : Set α<VAR>DecidableEq α<VAR>hs : s.Finite<VAR>ht : t.Finite<VAR>h : (symmDiff s t).Finite<GOAL>h.toFinset = symmDiff hs.toFinset ht.toFinset
<VAR>α : Type u<VAR>s : Set α<VAR>DecidableEq α<VAR>Fintype α<VAR>hs : s.Finite<VAR>h : sᶜ.Finite<GOAL>h.toFinset = hs.toFinsetᶜ
<VAR>α : Type u<VAR>Fintype α<VAR>h : Set.univ.Finite<GOAL>h.toFinset = Finset.univ
<VAR>α : Type u<VAR>s : Set α<VAR>h : s.Finite<GOAL>h.toFinset = ∅ ↔ s = ∅
<VAR>α : Type u<VAR>h : ∅.Finite<GOAL>h.toFinset = ∅
<VAR>α : Type u<VAR>s : Set α<VAR>Fintype α<VAR>h : s.Finite<GOAL>h.toFinset = Finset.univ ↔ s = Set.univ
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>DecidableEq β<VAR>f : α → β<VAR>hs : s.Finite<VAR>h : (f '' s).Finite<GOAL>h.toFinset = Finset.image f hs.toFinset
<VAR>α : Type u<VAR>β : Type v<VAR>DecidableEq α<VAR>Fintype β<VAR>f : β → α<VAR>h : (Set.range f).Finite<GOAL>h.toFinset = Finset.image f Finset.univ
<VAR>α : Type u<VAR>β : Type v<VAR>Fintype β<VAR>DecidableEq α<VAR>f : β → Set α<VAR>(w : β) → Fintype ↑(f w)<GOAL>(⋃ x, f x).toFinset = Finset.univ.biUnion fun x => (f x).toFinset
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>t : Set β<VAR>hst : ↑s ≃ ↑t<GOAL>s.Finite ↔ t.Finite
<VAR>α : Type u<VAR>s : Finset α<GOAL>(↑s).Finite
<VAR>α : Type u<VAR>s : Finset α<GOAL>⋯.toFinset = s
<VAR>α : Type u<VAR>s : Multiset α<GOAL>{x | x ∈ s}.Finite
<VAR>α : Type u<VAR>DecidableEq α<VAR>s : Multiset α<GOAL>⋯.toFinset = s.toFinset
<VAR>α : Type u<VAR>l : List α<GOAL>{x | x ∈ l}.Finite
<VAR>α : Type u<VAR>s : Set α<VAR>t : Set α<VAR>Finite ↑s<VAR>h : t ⊆ s<GOAL>Finite ↑t
<VAR>α : Type u<VAR>ι : Type u_1<VAR>s : Set ι<VAR>Finite ↑s<VAR>t : ι → Set α<VAR>H : ∀ i ∈ s, Finite ↑(t i)<GOAL>Finite ↑(⋃ x ∈ s, t x)
<VAR>α : Type u<VAR>Subsingleton α<VAR>s : Set α<GOAL>s.Finite
<VAR>α : Type u<VAR>Finite α<GOAL>Set.univ.Finite
<VAR>α : Type u<GOAL>Set.univ.Finite ↔ Finite α
<VAR>α : Type u<VAR>s : Set α<VAR>hs : s.Finite<VAR>t : Set α<VAR>ht : t ⊆ s<GOAL>t.Finite
<VAR>α : Type u<VAR>s t : Set α<VAR>hs : s.Finite<VAR>ht : t.Finite<GOAL>(s ∪ t).Finite
<VAR>α : Type u<VAR>s : Set α<VAR>hs : s.Finite<VAR>hsc : sᶜ.Finite<GOAL>Finite α
<VAR>α : Type u<VAR>s t : Set α<GOAL>s.Finite → t.Finite → (s ⊔ t).Finite
<VAR>α : Type u<VAR>s : Set α<VAR>hs : s.Finite<VAR>p : α → Prop<GOAL>{a | a ∈ s ∧ p a}.Finite
<VAR>α : Type u<VAR>s : Set α<VAR>hs : s.Finite<VAR>t : Set α<GOAL>(s ∩ t).Finite
<VAR>α : Type u<VAR>s : Set α<VAR>hs : s.Finite<VAR>t : Set α<GOAL>(t ∩ s).Finite
<VAR>α : Type u<VAR>s : Set α<VAR>h : s.Finite<VAR>t : Set α<GOAL>(s ⊓ t).Finite
<VAR>α : Type u<VAR>s : Set α<VAR>h : s.Finite<VAR>t : Set α<GOAL>(t ⊓ s).Finite
<VAR>α : Type u<VAR>s t : Set α<VAR>h : s ⊆ t<GOAL>s.Infinite → t.Infinite
<VAR>α : Type u<VAR>s : Set α<VAR>hs : s.Finite<VAR>t : Set α<GOAL>(s \ t).Finite
<VAR>α : Type u<VAR>s t : Set α<VAR>hd : (s \ t).Finite<VAR>ht : t.Finite<GOAL>s.Finite
<VAR>α : Type u<VAR>ι : Sort w<VAR>Finite ι<VAR>f : ι → Set α<VAR>H : ∀ (i : ι), (f i).Finite<GOAL>(⋃ i, f i).Finite
<VAR>α : Type u<VAR>ι : Type u_1<VAR>s : Set ι<VAR>hs : s.Finite<VAR>t : (i : ι) → i ∈ s → Set α<VAR>ht : ∀ (i : ι) (hi : i ∈ s), (t i hi).Finite<GOAL>(⋃ i, ⋃ (h : i ∈ s), t i h).Finite
<VAR>α : Type u<VAR>ι : Type u_1<VAR>s : Set ι<VAR>hs : s.Finite<VAR>t : ι → Set α<VAR>ht : ∀ i ∈ s, (t i).Finite<GOAL>(⋃ i ∈ s, t i).Finite
<VAR>α : Type u<VAR>s : Set (Set α)<VAR>hs : s.Finite<VAR>H : ∀ t ∈ s, t.Finite<GOAL>(⋃₀ s).Finite
<VAR>α : Type u_1<VAR>s : Set (Set α)<VAR>t : Set α<VAR>ht : t ∈ s<VAR>hf : t.Finite<GOAL>(⋂₀ s).Finite
<VAR>α : Type u<VAR>ι : Type u_1<VAR>s : ι → Set α<VAR>t : Set ι<VAR>ht : t.Finite<VAR>hs : ∀ i ∈ t, (s i).Finite<VAR>he : ∀ i ∉ t, s i = ∅<GOAL>(⋃ i, s i).Finite
<VAR>α β : Type u_1<VAR>s : Set α<VAR>f : α → Set β<VAR>h : s.Finite<VAR>hf : ∀ a ∈ s, (f a).Finite<GOAL>(s >>= f).Finite
<VAR>α : Type u<VAR>s : Set α<VAR>h : s.Infinite<GOAL>s.Nonempty
<VAR>α : Type u<VAR>a : α<GOAL>{a}.Finite
<VAR>α : Type u<VAR>a : α<GOAL>(pure a).Finite
<VAR>α : Type u<VAR>a : α<VAR>s : Set α<VAR>hs : s.Finite<GOAL>(insert a s).Finite
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>f : α → β<VAR>hs : s.Finite<GOAL>(f '' s).Finite
<VAR>α : Type u<VAR>ι : Sort w<VAR>f : ι → α<VAR>Finite ι<GOAL>(Set.range f).Finite
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>hf : Set.SurjOn f s t<VAR>hs : s.Finite<GOAL>t.Finite
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>hs : s.Finite<VAR>F : (i : α) → i ∈ s → β<GOAL>{y | ∃ x, ∃ (hx : x ∈ s), F x hx = y}.Finite
<VAR>α β : Type u_1<VAR>s : Set α<VAR>f : α → β<GOAL>s.Finite → (f <$> s).Finite
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>f : α → β<VAR>h : (f '' s).Finite<VAR>hi : Set.InjOn f s<GOAL>s.Finite
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set β<VAR>h : (f ⁻¹' s).Finite<VAR>hs : s ⊆ Set.range f<GOAL>s.Finite
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set β<VAR>h : (f ⁻¹' s).Finite<VAR>hf : Function.Surjective f<GOAL>s.Finite
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set β<VAR>I : Set.InjOn f (f ⁻¹' s)<VAR>h : s.Finite<GOAL>(f ⁻¹' s).Finite
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set β<VAR>h : s.Finite<VAR>hf : ∀ b ∈ s, (f ⁻¹' {b}).Finite<GOAL>(f ⁻¹' s).Finite
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set β<VAR>hs : s.Infinite<VAR>hf : s ⊆ Set.range f<GOAL>(f ⁻¹' s).Infinite
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set β<VAR>hs : (s ∩ Set.range f).Infinite<GOAL>(f ⁻¹' s).Infinite
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set β<VAR>f : α ↪ β<VAR>h : s.Finite<GOAL>(⇑f ⁻¹' s).Finite
<VAR>n : ℕ<GOAL>{i | i < n}.Finite
<VAR>n : ℕ<GOAL>{i | i ≤ n}.Finite
<VAR>α : Type u<VAR>s : Set α<VAR>f : α → α<VAR>hs : s.Finite<VAR>hm : Set.MapsTo f s s<GOAL>Set.SurjOn f s s ↔ Set.BijOn f s s
<VAR>α : Type u<VAR>s : Set α<VAR>f : α → α<VAR>hs : s.Finite<VAR>hm : Set.MapsTo f s s<GOAL>Set.InjOn f s ↔ Set.BijOn f s s
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>t : Set β<VAR>hs : s.Finite<VAR>ht : t.Finite<GOAL>(s ×ˢ t).Finite
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>t : Set β<VAR>h : (s ×ˢ t).Finite<GOAL>t.Nonempty → s.Finite
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>t : Set β<VAR>h : (s ×ˢ t).Finite<GOAL>s.Nonempty → t.Finite
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>t : Set β<VAR>hs : s.Infinite<VAR>ht : t.Nonempty<GOAL>(s ×ˢ t).Infinite
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>t : Set β<VAR>ht : t.Infinite<VAR>hs : s.Nonempty<GOAL>(s ×ˢ t).Infinite
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>t : Set β<GOAL>(s ×ˢ t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>t : Set β<GOAL>(s ×ˢ t).Finite ↔ (s.Finite ∨ t = ∅) ∧ (t.Finite ∨ s = ∅)
<VAR>α : Type u<VAR>s : Set α<VAR>hs : s.Finite<GOAL>s.offDiag.Finite
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type x<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β → γ<VAR>hs : s.Finite<VAR>ht : t.Finite<GOAL>(Set.image2 f s t).Finite
<VAR>α : Type u<VAR>β : Type v<VAR>f : Set (α → β)<VAR>s : Set α<VAR>hf : f.Finite<VAR>hs : s.Finite<GOAL>(f.seq s).Finite
<VAR>α β : Type u<VAR>f : Set (α → β)<VAR>s : Set α<VAR>hf : f.Finite<VAR>hs : s.Finite<GOAL>(Seq.seq f fun x => s).Finite
<VAR>α : Type u<VAR>s : Finset α<GOAL>{a | a ∈ s}.Finite
<VAR>α : Type u<VAR>s : Set α<VAR>h : s.Subsingleton<GOAL>s.Finite
<VAR>α : Type u<VAR>s : Set α<VAR>hs : s.Infinite<GOAL>s.Nontrivial
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set (α ⊕ β)<GOAL>(Sum.inl ⁻¹' s).Finite ∧ (Sum.inr ⁻¹' s).Finite ↔ s.Finite
<VAR>α : Type u<VAR>p : Set α → Prop<GOAL>(∃ s, s.Finite ∧ p s) ↔ ∃ s, p ↑s
<VAR>α : Type u<VAR>a : Set α<VAR>h : a.Finite<GOAL>{b | b ⊆ a}.Finite
<VAR>α : Type u<VAR>s : Set α<VAR>h : s.Finite<GOAL>(𝒫 s).Finite
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set α<VAR>p : Set β → Prop<GOAL>(∃ t ⊆ f '' s, t.Finite ∧ p t) ↔ ∃ t ⊆ s, t.Finite ∧ p (f '' t)
<VAR>ι : Type u_1<VAR>Finite ι<VAR>κ : ι → Type u_2<VAR>t : (i : ι) → Set (κ i)<VAR>ht : ∀ (i : ι), (t i).Finite<GOAL>(Set.univ.pi t).Finite
<VAR>ι : Type u_1<VAR>Finite ι<VAR>κ : ι → Type u_2<VAR>t : (i : ι) → Set (κ i)<VAR>ht : ∀ (i : ι), (t i).Finite<GOAL>{f | ∀ (i : ι), f i ∈ t i}.Finite
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → Finset β<VAR>h : (Set.range f).Finite<GOAL>(⋃ a, ↑(f a)).Finite
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f g : α → β<VAR>hf : (Set.range f).Finite<VAR>hg : (Set.range g).Finite<GOAL>(Set.range fun x => if p x then f x else g x).Finite
<VAR>α : Type u<VAR>β : Type v<VAR>c : β<GOAL>(Set.range fun x => c).Finite
<VAR>α : Type u<VAR>s t : Set α<GOAL>(s ∪ t).Finite ↔ s.Finite ∧ t.Finite