ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>f : α → β<VAR>hi : Set.InjOn f s<GOAL>(f '' s).Finite ↔ s.Finite
<VAR>α : Type u<GOAL>Set.univ.Finite ↔ Nonempty (Fintype α)
<VAR>α : Type u<VAR>a : α<VAR>ha : {a}.Finite := ⋯<GOAL>Set.Finite.toFinset ha = {a}
<VAR>α : Type u<VAR>DecidableEq α<VAR>s : Set α<VAR>a : α<VAR>hs : (insert a s).Finite<GOAL>hs.toFinset = insert a ⋯.toFinset
<VAR>α : Type u<VAR>DecidableEq α<VAR>a : α<VAR>s : Set α<VAR>hs : s.Finite<GOAL>⋯.toFinset = insert a hs.toFinset
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>t : Set β<VAR>hs : s.Finite<VAR>ht : t.Finite<GOAL>hs.toFinset ×ˢ ht.toFinset = ⋯.toFinset
<VAR>α : Type u<VAR>s : Set α<VAR>DecidableEq α<VAR>hs : s.Finite<GOAL>⋯.toFinset = hs.toFinset.offDiag
<VAR>α : Type u<VAR>s : Set α<VAR>h : s.Finite<GOAL>∃ n f, Set.range ⇑f = s
<VAR>α : Type u<VAR>s : Set α<VAR>h : s.Finite<GOAL>∃ n f, Function.Injective f ∧ Set.range f = s
<VAR>α : Type u<VAR>s : Set (Option α)<GOAL>s.Finite ↔ {x | some x ∈ s}.Finite
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set (α × β)<GOAL>(Prod.fst '' s).Finite ∧ (Prod.snd '' s).Finite ↔ s.Finite
<VAR>δ : Type u_1<VAR>Finite δ<VAR>κ : δ → Type u_2<VAR>s : Set ((d : δ) → κ d)<GOAL>(∀ (d : δ), (Function.eval d '' s).Finite) ↔ s.Finite
<VAR>α : Type u<VAR>s : Set α<VAR>hs : s.Finite<VAR>ι : Type u_1<VAR>t : ι → Set α<VAR>h : s ⊆ ⋃ i, t i<GOAL>∃ I, I.Finite ∧ s ⊆ ⋃ i ∈ I, t i
<VAR>α : Type u<VAR>ι : Type u_1<VAR>s : ι → Set α<VAR>t : Set α<VAR>tfin : t.Finite<VAR>h : t ⊆ ⋃ i, s i<GOAL>∃ I, I.Finite ∧ ∃ σ, (∀ (i : ↑{i | i ∈ I}), (σ i).Finite) ∧ (∀ (i : ↑{i | i ∈ I}), σ i ⊆ s ↑i) ∧ t = ⋃ i, σ i
<VAR>α : Type u<VAR>C : Set α → Prop<VAR>s : Set α<VAR>h : s.Finite<VAR>H0 : C ∅<VAR>H1 : ∀ {a : α} {s : Set α}, a ∉ s → s.Finite → C s → C (insert a s)<GOAL>C s
<VAR>α : Type u<VAR>C : Set α → Prop<VAR>S : Set α<VAR>h : S.Finite<VAR>H0 : C ∅<VAR>H1 : ∀ {a : α} {s : Set α}, a ∈ S → s ⊆ S → a ∉ s → C s → C (insert a s)<GOAL>C S
<VAR>α : Type u<VAR>C : (s : Set α) → s.Finite → Prop<VAR>s : Set α<VAR>h : s.Finite<VAR>H0 : C ∅ ⋯<VAR>H1 : ∀ {a : α} {s : Set α}, a ∉ s → ∀ (h : s.Finite), C s h → C (insert a s) ⋯<GOAL>C s h
<VAR>α : Type u<VAR>C : Set α → Prop<VAR>S : Set α<VAR>h : S.Finite<VAR>S0 : Set α<VAR>hS0 : S0 ⊆ S<VAR>H0 : C S0<VAR>H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)<GOAL>C S
<VAR>α : Type u<VAR>Finite α<VAR>C : Set α → Prop<VAR>S0 : Set α<VAR>H0 : C S0<VAR>H1 : ∀ (S : Set α), S ≠ Set.univ → C S → ∃ a ∉ S, C (insert a S)<GOAL>C Set.univ
<VAR>γ : Type u_1<VAR>P : γ → Set γ → Prop<VAR>h : ∀ (t : Set γ), t.Finite → ∃ c, P c t<GOAL>∃ u, ∀ (n : ℕ), P (u n) (u '' Set.Iio n)
<VAR>α : Type u<GOAL>Fintype.card ↑∅ = 0
<VAR>α : Type u<VAR>h : Fintype ↑∅<GOAL>Fintype.card ↑∅ = 0
<VAR>α : Type u<VAR>a : α<VAR>s : Set α<VAR>Fintype ↑s<VAR>h : a ∉ s<GOAL>Fintype.card ↑(insert a s) = Fintype.card ↑s + 1
<VAR>α : Type u<VAR>a : α<VAR>s : Set α<VAR>Fintype ↑s<VAR>h : a ∉ s<VAR>d : Fintype ↑(insert a s)<GOAL>Fintype.card ↑(insert a s) = Fintype.card ↑s + 1
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>Fintype ↑s<VAR>f : α → β<VAR>Fintype ↑(f '' s)<VAR>H : ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y<GOAL>Fintype.card ↑(f '' s) = Fintype.card ↑s
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>Fintype ↑s<VAR>f : α → β<VAR>Fintype ↑(f '' s)<VAR>H : Function.Injective f<GOAL>Fintype.card ↑(f '' s) = Fintype.card ↑s
<VAR>α : Type u<VAR>a : α<GOAL>Fintype.card ↑{a} = 1
<VAR>α : Type u<VAR>s t : Set α<VAR>Fintype ↑s<VAR>Fintype ↑t<VAR>h : s ⊂ t<GOAL>Fintype.card ↑s < Fintype.card ↑t
<VAR>α : Type u<VAR>s t : Set α<VAR>Fintype ↑s<VAR>Fintype ↑t<VAR>hsub : s ⊆ t<GOAL>Fintype.card ↑s ≤ Fintype.card ↑t
<VAR>α : Type u<VAR>s t : Set α<VAR>Fintype ↑s<VAR>Fintype ↑t<VAR>hsub : s ⊆ t<VAR>hcard : Fintype.card ↑t ≤ Fintype.card ↑s<GOAL>s = t
<VAR>α : Type u<VAR>β : Type v<VAR>Fintype α<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>Fintype ↑(Set.range f)<GOAL>Fintype.card ↑(Set.range f) = Fintype.card α
<VAR>α : Type u<VAR>s : Set α<VAR>Fintype ↑s<VAR>h : s.Finite<GOAL>h.toFinset.card = Fintype.card ↑s
<VAR>α : Type u<VAR>Fintype α<VAR>a : α<VAR>Fintype ↑{x | x ≠ a}<GOAL>Fintype.card ↑{x | x ≠ a} = Fintype.card α - 1
<VAR>α : Type u<GOAL>Set.univ.Infinite ↔ Infinite α
<VAR>α : Type u<VAR>h : Infinite α<GOAL>Set.univ.Infinite
<VAR>α : Type u<VAR>s : Set α<GOAL>Infinite ↑s ↔ s.Infinite
<VAR>α : Type u<VAR>s t : Set α<VAR>hs : s.Infinite<VAR>ht : t.Finite<GOAL>∃ a ∈ s, a ∉ t
<VAR>α : Type u<VAR>s : Set α<VAR>hs : s.Infinite<VAR>t : Finset α<GOAL>∃ a ∈ s, a ∉ t
<VAR>α : Type u<VAR>s : Set α<VAR>Infinite α<VAR>hs : s.Finite<GOAL>∃ a, a ∉ s
<VAR>α : Type u<VAR>Infinite α<VAR>s : Finset α<GOAL>∃ a, a ∉ s
<VAR>α : Type u<VAR>s : Set α<VAR>hs : s.Infinite<VAR>n : ℕ<GOAL>∃ t, ↑t ⊆ s ∧ t.card = n
<VAR>α : Type u<VAR>Infinite α<VAR>s : Set α<VAR>hs : sᶜ.Finite<GOAL>s.Infinite
<VAR>α : Type u<VAR>Infinite α<VAR>s : Set α<VAR>hs : s.Finite<GOAL>sᶜ.Infinite
<VAR>α : Type u<VAR>s t : Set α<VAR>hs : s.Infinite<VAR>ht : t.Finite<GOAL>(s \ t).Infinite
<VAR>α : Type u<VAR>s t : Set α<GOAL>(s ∪ t).Infinite ↔ s.Infinite ∨ t.Infinite
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set α<VAR>hs : (f '' s).Infinite<GOAL>s.Infinite
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>f : α → β<VAR>hi : Set.InjOn f s<GOAL>(f '' s).Infinite ↔ s.Infinite
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>hi : Function.Injective f<GOAL>(Set.range f).Infinite ↔ Infinite α
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type x<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>b : β<VAR>hs : s.Infinite<VAR>hb : b ∈ t<VAR>hf : Set.InjOn (fun a => f a b) s<GOAL>(Set.image2 f s t).Infinite
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type x<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>ht : t.Infinite<VAR>ha : a ∈ s<VAR>hf : Set.InjOn (f a) t<GOAL>(Set.image2 f s t).Infinite
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type x<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>hfs : ∀ b ∈ t, Set.InjOn (fun a => f a b) s<VAR>hft : ∀ a ∈ s, Set.InjOn (f a) t<GOAL>(Set.image2 f s t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type x<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>hfs : ∀ b ∈ t, Set.InjOn (fun x => f x b) s<VAR>hft : ∀ a ∈ s, Set.InjOn (f a) t<GOAL>(Set.image2 f s t).Finite ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>hi : Set.InjOn f s<VAR>hm : Set.MapsTo f s t<VAR>hs : s.Infinite<GOAL>t.Infinite
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>hs : s.Infinite<VAR>hf : Set.MapsTo f s t<VAR>ht : t.Finite<GOAL>∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y
<VAR>α : Type u<VAR>β : Type v<VAR>Infinite α<VAR>f : α → β<VAR>hi : Function.Injective f<GOAL>(Set.range f).Infinite
<VAR>α : Type u<VAR>β : Type v<VAR>Infinite α<VAR>s : Set β<VAR>f : α → β<VAR>hi : Function.Injective f<VAR>hf : ∀ (x : α), f x ∈ s<GOAL>s.Infinite
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set α<VAR>h_inf : s.Infinite<VAR>h_fin : (f '' s).Finite<GOAL>¬Set.InjOn f s
<VAR>α : Type u<VAR>Preorder α<VAR>Nonempty α<VAR>s : Set α<VAR>h : ∀ (a : α), ∃ b ∈ s, a < b<GOAL>s.Infinite
<VAR>α : Type u<VAR>Preorder α<VAR>Nonempty α<VAR>s : Set α<VAR>h : ∀ (a : α), ∃ b ∈ s, b < a<GOAL>s.Infinite
<VAR>α : Type u_1<VAR>PartialOrder α<GOAL>{x | IsTop x}.Finite
<VAR>α : Type u_1<VAR>PartialOrder α<GOAL>{x | IsBot x}.Finite
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>hs : s.Infinite<VAR>hf : Set.MapsTo f s t<VAR>ht : t.Finite<GOAL>∃ x ∈ s, ∃ y ∈ s, x < y ∧ f x = f y
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>Infinite α<VAR>t : Set β<VAR>f : α → β<VAR>hf : ∀ (a : α), f a ∈ t<VAR>ht : t.Finite<GOAL>∃ a b, a < b ∧ f a = f b
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder β<VAR>s : Set α<VAR>f : α → β<VAR>h1 : s.Finite<GOAL>s.Nonempty → ∃ a ∈ s, ∀ b ∈ s, f a ≤ f b
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder β<VAR>s : Set α<VAR>f : α → β<VAR>h1 : s.Finite<GOAL>s.Nonempty → ∃ a ∈ s, ∀ b ∈ s, f b ≤ f a
<VAR>α : Type u<VAR>β : Type v<VAR>Nonempty α<VAR>LinearOrder β<VAR>s : Set α<VAR>f : α → β<VAR>h : s.Finite<GOAL>∃ a, ∀ b ∈ s, f a ≤ f b
<VAR>α : Type u<VAR>β : Type v<VAR>Nonempty α<VAR>LinearOrder β<VAR>s : Set α<VAR>f : α → β<VAR>h : s.Finite<GOAL>∃ a, ∀ b ∈ s, f b ≤ f a
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>Preorder ι'<VAR>Nonempty ι'<VAR>IsDirected ι' fun x x_1 => x ≤ x_1<VAR>Order.Frame α<VAR>s : Set ι<VAR>hs : s.Finite<VAR>f : ι → ι' → α<VAR>hf : ∀ i ∈ s, Monotone (f i)<GOAL>⨆ j, ⨅ i ∈ s, f i j = ⨅ i ∈ s, ⨆ j, f i j
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>Preorder ι'<VAR>Nonempty ι'<VAR>IsDirected ι' (Function.swap fun x x_1 => x ≤ x_1)<VAR>Order.Frame α<VAR>s : Set ι<VAR>hs : s.Finite<VAR>f : ι → ι' → α<VAR>hf : ∀ i ∈ s, Antitone (f i)<GOAL>⨆ j, ⨅ i ∈ s, f i j = ⨅ i ∈ s, ⨆ j, f i j
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>Preorder ι'<VAR>Nonempty ι'<VAR>IsDirected ι' (Function.swap fun x x_1 => x ≤ x_1)<VAR>Order.Coframe α<VAR>s : Set ι<VAR>hs : s.Finite<VAR>f : ι → ι' → α<VAR>hf : ∀ i ∈ s, Monotone (f i)<GOAL>⨅ j, ⨆ i ∈ s, f i j = ⨆ i ∈ s, ⨅ j, f i j
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>Preorder ι'<VAR>Nonempty ι'<VAR>IsDirected ι' fun x x_1 => x ≤ x_1<VAR>Order.Coframe α<VAR>s : Set ι<VAR>hs : s.Finite<VAR>f : ι → ι' → α<VAR>hf : ∀ i ∈ s, Antitone (f i)<GOAL>⨅ j, ⨆ i ∈ s, f i j = ⨆ i ∈ s, ⨅ j, f i j
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>Finite ι<VAR>Preorder ι'<VAR>Nonempty ι'<VAR>IsDirected ι' fun x x_1 => x ≤ x_1<VAR>Order.Frame α<VAR>f : ι → ι' → α<VAR>hf : ∀ (i : ι), Monotone (f i)<GOAL>⨆ j, ⨅ i, f i j = ⨅ i, ⨆ j, f i j
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>Finite ι<VAR>Preorder ι'<VAR>Nonempty ι'<VAR>IsDirected ι' (Function.swap fun x x_1 => x ≤ x_1)<VAR>Order.Frame α<VAR>f : ι → ι' → α<VAR>hf : ∀ (i : ι), Antitone (f i)<GOAL>⨆ j, ⨅ i, f i j = ⨅ i, ⨆ j, f i j
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>Finite ι<VAR>Preorder ι'<VAR>Nonempty ι'<VAR>IsDirected ι' (Function.swap fun x x_1 => x ≤ x_1)<VAR>Order.Coframe α<VAR>f : ι → ι' → α<VAR>hf : ∀ (i : ι), Monotone (f i)<GOAL>⨅ j, ⨆ i, f i j = ⨆ i, ⨅ j, f i j
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>Finite ι<VAR>Preorder ι'<VAR>Nonempty ι'<VAR>IsDirected ι' fun x x_1 => x ≤ x_1<VAR>Order.Coframe α<VAR>f : ι → ι' → α<VAR>hf : ∀ (i : ι), Antitone (f i)<GOAL>⨅ j, ⨆ i, f i j = ⨆ i, ⨅ j, f i j
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>Finite ι<VAR>Preorder ι'<VAR>IsDirected ι' fun x x_1 => x ≤ x_1<VAR>Nonempty ι'<VAR>s : ι → ι' → Set α<VAR>hs : ∀ (i : ι), Monotone (s i)<GOAL>⋃ j, ⋂ i, s i j = ⋂ i, ⋃ j, s i j
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>Finite ι<VAR>Preorder ι'<VAR>IsDirected ι' (Function.swap fun x x_1 => x ≤ x_1)<VAR>Nonempty ι'<VAR>s : ι → ι' → Set α<VAR>hs : ∀ (i : ι), Antitone (s i)<GOAL>⋃ j, ⋂ i, s i j = ⋂ i, ⋃ j, s i j
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>Finite ι<VAR>Preorder ι'<VAR>IsDirected ι' (Function.swap fun x x_1 => x ≤ x_1)<VAR>Nonempty ι'<VAR>s : ι → ι' → Set α<VAR>hs : ∀ (i : ι), Monotone (s i)<GOAL>⋂ j, ⋃ i, s i j = ⋃ i, ⋂ j, s i j
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>Finite ι<VAR>Preorder ι'<VAR>IsDirected ι' fun x x_1 => x ≤ x_1<VAR>Nonempty ι'<VAR>s : ι → ι' → Set α<VAR>hs : ∀ (i : ι), Antitone (s i)<GOAL>⋂ j, ⋃ i, s i j = ⋃ i, ⋂ j, s i j
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>LinearOrder ι'<VAR>Nonempty ι'<VAR>α : ι → Type u_3<VAR>I : Set ι<VAR>s : (i : ι) → ι' → Set (α i)<VAR>hI : I.Finite<VAR>hs : ∀ i ∈ I, Monotone (s i)<GOAL>(⋃ j, I.pi fun i => s i j) = I.pi fun i => ⋃ j, s i j
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>LinearOrder ι'<VAR>Nonempty ι'<VAR>Finite ι<VAR>α : ι → Type u_3<VAR>s : (i : ι) → ι' → Set (α i)<VAR>hs : ∀ (i : ι), Monotone (s i)<GOAL>(⋃ j, Set.univ.pi fun i => s i j) = Set.univ.pi fun i => ⋃ j, s i j
<VAR>α : Type u<VAR>P : α → ℕ → Prop<VAR>(x : α) → DecidablePred (P x)<VAR>b : ℕ<GOAL>(Set.range fun x => Nat.findGreatest (P x) b).Finite
<VAR>α : Type u<VAR>β : Type v<VAR>PartialOrder β<VAR>f : α → β<VAR>s : Set α<VAR>h : s.Finite<VAR>hs : s.Nonempty<GOAL>∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'
<VAR>α : Type u<VAR>β : Type v<VAR>PartialOrder β<VAR>f : α → β<VAR>s : Set α<VAR>h : (f '' s).Finite<VAR>hs : s.Nonempty<GOAL>∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'
<VAR>α : Type u<VAR>β : Type v<VAR>PartialOrder β<VAR>f : α → β<VAR>s : Set α<VAR>h : s.Finite<VAR>hs : s.Nonempty<GOAL>∃ a ∈ s, ∀ a' ∈ s, f a' ≤ f a → f a = f a'
<VAR>α : Type u<VAR>β : Type v<VAR>PartialOrder β<VAR>f : α → β<VAR>s : Set α<VAR>h : (f '' s).Finite<VAR>hs : s.Nonempty<GOAL>∃ a ∈ s, ∀ a' ∈ s, f a' ≤ f a → f a = f a'
<VAR>α : Type u<VAR>Preorder α<VAR>IsDirected α fun x x_1 => x ≤ x_1<VAR>Nonempty α<VAR>s : Set α<VAR>hs : s.Finite<GOAL>BddAbove s
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>IsDirected α fun x x_1 => x ≤ x_1<VAR>Nonempty α<VAR>I : Set β<VAR>S : β → Set α<VAR>H : I.Finite<GOAL>BddAbove (⋃ i ∈ I, S i) ↔ ∀ i ∈ I, BddAbove (S i)
<VAR>α : Type u<VAR>Preorder α<VAR>IsDirected α fun x x_1 => x ≤ x_1<VAR>Nonempty α<VAR>s : Set α<GOAL>¬BddAbove s → s.Infinite
<VAR>α : Type u<VAR>Preorder α<VAR>IsDirected α fun x x_1 => x ≥ x_1<VAR>Nonempty α<VAR>s : Set α<VAR>hs : s.Finite<GOAL>BddBelow s
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>IsDirected α fun x x_1 => x ≥ x_1<VAR>Nonempty α<VAR>I : Set β<VAR>S : β → Set α<VAR>H : I.Finite<GOAL>BddBelow (⋃ i ∈ I, S i) ↔ ∀ i ∈ I, BddBelow (S i)
<VAR>α : Type u<VAR>Preorder α<VAR>IsDirected α fun x x_1 => x ≥ x_1<VAR>Nonempty α<VAR>s : Set α<GOAL>¬BddBelow s → s.Infinite
<VAR>α : Type u<VAR>Infinite α<VAR>n : ℕ<GOAL>∃ s, s.card = n
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>Nonempty α<VAR>s : Finset α<GOAL>BddAbove ↑s
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>Nonempty α<VAR>s : Finset α<GOAL>BddBelow ↑s
<VAR>α : Type u<VAR>LinearOrder α<VAR>h : ∀ ⦃x y z : α⦄, x < y → y < z → False<GOAL>Finite α
<VAR>α : Type u<VAR>LinearOrder α<VAR>s : Set α<VAR>h : ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ s, x < y → y < z → False<GOAL>s.Finite
<VAR>α : Type u<VAR>LinearOrder α<VAR>s : Set α<GOAL>(s \ ⋃ x ∈ s, ⋃ y ∈ s, Set.Ioo x y).Finite
<VAR>α : Type u<VAR>LinearOrder α<VAR>s : Set α<GOAL>(s \ ⋃ x, Set.Ioo ↑x.1 ↑x.2).Finite
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>Nonempty ι<VAR>f : ι → Set α<VAR>h : Directed (fun x x_1 => x ⊆ x_1) f<VAR>s : Finset α<VAR>hs : ↑s ⊆ ⋃ i, f i<GOAL>∃ i, ↑s ⊆ f i
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>f : ι → Set α<VAR>c : Set ι<VAR>hn : c.Nonempty<VAR>hc : DirectedOn (fun i j => f i ⊆ f j) c<VAR>s : Finset α<VAR>hs : ↑s ⊆ ⋃ i ∈ c, f i<GOAL>∃ i ∈ c, ↑s ⊆ f i
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>Finset.Icc s t = Finset.map Multiset.equivDFinsupp.symm.toEmbedding (Finset.Icc (Multiset.toDFinsupp s) (Multiset.toDFinsupp t))
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>Finset.uIcc s t = Finset.map Multiset.equivDFinsupp.symm.toEmbedding (Finset.uIcc (Multiset.toDFinsupp s) (Multiset.toDFinsupp t))
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>(Finset.Icc s t).card = ∏ i ∈ s.toFinset ∪ t.toFinset, (Multiset.count i t + 1 - Multiset.count i s)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>(Finset.Ico s t).card = ∏ i ∈ s.toFinset ∪ t.toFinset, (Multiset.count i t + 1 - Multiset.count i s) - 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>(Finset.Ioc s t).card = ∏ i ∈ s.toFinset ∪ t.toFinset, (Multiset.count i t + 1 - Multiset.count i s) - 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>(Finset.Ioo s t).card = ∏ i ∈ s.toFinset ∪ t.toFinset, (Multiset.count i t + 1 - Multiset.count i s) - 2
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>(Finset.uIcc s t).card = ∏ i ∈ s.toFinset ∪ t.toFinset, ((↑(Multiset.count i t) - ↑(Multiset.count i s)).natAbs + 1)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<GOAL>(Finset.Iic s).card = ∏ i ∈ s.toFinset, (Multiset.count i s + 1)
<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_7<VAR>x : γ<VAR>s : (i : ι) → κ i → Set γ<GOAL>x ∈ ⋃ i, ⋃ j, s i j ↔ ∃ i j, x ∈ s i j
<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_7<VAR>x : γ<VAR>s : (i : ι) → κ i → Set γ<GOAL>x ∈ ⋂ i, ⋂ j, s i j ↔ ∀ (i : ι) (j : κ i), x ∈ s i j
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>s : ι → Set α<VAR>a : α<VAR>i : ι<VAR>ha : a ∈ s i<GOAL>a ∈ ⋃ i, s i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_7<VAR>s : (i : ι) → κ i → Set α<VAR>a : α<VAR>i : ι<VAR>j : κ i<VAR>ha : a ∈ s i j<GOAL>a ∈ ⋃ i, ⋃ j, s i j
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>s : ι → Set α<VAR>a : α<VAR>h : ∀ (i : ι), a ∈ s i<GOAL>a ∈ ⋂ i, s i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_7<VAR>s : (i : ι) → κ i → Set α<VAR>a : α<VAR>h : ∀ (i : ι) (j : κ i), a ∈ s i j<GOAL>a ∈ ⋂ i, ⋂ j, s i j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>GaloisConnection (Set.image f) (Set.preimage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>GaloisConnection (Set.preimage f) (Set.kernImage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>Monotone (Set.kernImage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<GOAL>Set.kernImage f s = (f '' sᶜ)ᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<GOAL>Set.kernImage f sᶜ = (f '' s)ᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>Set.kernImage f ∅ = (Set.range f)ᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set β<GOAL>Set.kernImage f (f ⁻¹' s) = s ↔ (Set.range f)ᶜ ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<GOAL>(Set.range f)ᶜ ⊆ Set.kernImage f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<GOAL>Set.kernImage f (s ∪ f ⁻¹' t) = Set.kernImage f s ∪ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<GOAL>Set.kernImage f (f ⁻¹' t ∪ s) = t ∪ Set.kernImage f s
<VAR>α : Type u_1<VAR>p q : Prop<VAR>f₁ : p → Set α<VAR>f₂ : q → Set α<VAR>pq : p ↔ q<VAR>f : ∀ (x : q), f₁ ⋯ = f₂ x<GOAL>Set.iUnion f₁ = Set.iUnion f₂
<VAR>α : Type u_1<VAR>p q : Prop<VAR>f₁ : p → Set α<VAR>f₂ : q → Set α<VAR>pq : p ↔ q<VAR>f : ∀ (x : q), f₁ ⋯ = f₂ x<GOAL>Set.iInter f₁ = Set.iInter f₂
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>f : PLift ι → Set α<GOAL>⋃ i, f { down := i } = ⋃ i, f i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>f : ι → Set α<GOAL>⋃ i, f i.down = ⋃ i, f i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>f : PLift ι → Set α<GOAL>⋂ i, f { down := i } = ⋂ i, f i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>f : ι → Set α<GOAL>⋂ i, f i.down = ⋂ i, f i
<VAR>α : Type u_1<VAR>p : Prop<VAR>Decidable p<VAR>s : Set α<GOAL>⋃ (_ : p), s = if p then s else ∅
<VAR>α : Type u_1<VAR>p : Prop<VAR>Decidable p<VAR>s : p → Set α<GOAL>⋃ (h : p), s h = if h : p then s h else ∅
<VAR>α : Type u_1<VAR>p : Prop<VAR>Decidable p<VAR>s : Set α<GOAL>⋂ (_ : p), s = if p then s else Set.univ
<VAR>α : Type u_1<VAR>p : Prop<VAR>Decidable p<VAR>s : p → Set α<GOAL>⋂ (h : p), s h = if h : p then s h else Set.univ
<VAR>β : Type u_2<VAR>ι : Type u_11<VAR>t : Set ι<VAR>s : ι → Set β<VAR>w : ⋃ i ∈ t, s i = ⊤<VAR>x : β<GOAL>∃ i ∈ t, x ∈ s i
<VAR>α : Type u_1<VAR>ι : Type u_11<VAR>t : Set ι<VAR>s : ι → Set α<VAR>H : Nonempty α<VAR>w : ⋃ i ∈ t, s i = ⊤<GOAL>t.Nonempty
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>s : ι → Set α<VAR>h_Union : (⋃ i, s i).Nonempty<GOAL>Nonempty ι
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>s : ι → Set α<VAR>Nonempty α<VAR>h_Union : ⋃ i, s i = Set.univ<GOAL>Nonempty ι
<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>p : ι → β → Prop<GOAL>{x | ∃ i, p i x} = ⋃ i, {x | p i x}
<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>p : ι → β → Prop<GOAL>{x | ∀ (i : ι), p i x} = ⋂ i, {x | p i x}
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>s : ι → Set α<VAR>t : Set α<VAR>h : ∀ (i : ι), s i ⊆ t<GOAL>⋃ i, s i ⊆ t
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_7<VAR>s : (i : ι) → κ i → Set α<VAR>t : Set α<VAR>h : ∀ (i : ι) (j : κ i), s i j ⊆ t<GOAL>⋃ i, ⋃ j, s i j ⊆ t
<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>t : Set β<VAR>s : ι → Set β<VAR>h : ∀ (i : ι), t ⊆ s i<GOAL>t ⊆ ⋂ i, s i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_7<VAR>s : Set α<VAR>t : (i : ι) → κ i → Set α<VAR>h : ∀ (i : ι) (j : κ i), s ⊆ t i j<GOAL>s ⊆ ⋂ i, ⋂ j, t i j
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>s : ι → Set α<VAR>t : Set α<GOAL>⋃ i, s i ⊆ t ↔ ∀ (i : ι), s i ⊆ t
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_7<VAR>s : (i : ι) → κ i → Set α<VAR>t : Set α<GOAL>⋃ i, ⋃ j, s i j ⊆ t ↔ ∀ (i : ι) (j : κ i), s i j ⊆ t
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>s : Set α<VAR>t : ι → Set α<GOAL>s ⊆ ⋂ i, t i ↔ ∀ (i : ι), s ⊆ t i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_7<VAR>s : Set α<VAR>t : (i : ι) → κ i → Set α<GOAL>s ⊆ ⋂ i, ⋂ j, t i j ↔ ∀ (i : ι) (j : κ i), s ⊆ t i j
<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>s : ι → Set β<VAR>i : ι<GOAL>s i ⊆ ⋃ i, s i
<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>s : ι → Set β<VAR>i : ι<GOAL>⋂ i, s i ⊆ s i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_7<VAR>s : (i : ι) → κ i → Set α<VAR>i : ι<VAR>j : κ i<GOAL>s i j ⊆ ⋃ i', ⋃ j', s i' j'
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_7<VAR>s : (i : ι) → κ i → Set α<VAR>i : ι<VAR>j : κ i<GOAL>⋂ i, ⋂ j, s i j ⊆ s i j
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>s : Set α<VAR>t : ι → Set α<VAR>i : ι<VAR>h : s ⊆ t i<GOAL>s ⊆ ⋃ i, t i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>s : ι → Set α<VAR>t : Set α<VAR>i : ι<VAR>h : s i ⊆ t<GOAL>⋂ i, s i ⊆ t
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_7<VAR>s : Set α<VAR>t : (i : ι) → κ i → Set α<VAR>i : ι<VAR>j : κ i<VAR>h : s ⊆ t i j<GOAL>s ⊆ ⋃ i, ⋃ j, t i j
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_7<VAR>s : (i : ι) → κ i → Set α<VAR>t : Set α<VAR>i : ι<VAR>j : κ i<VAR>h : s i j ⊆ t<GOAL>⋂ i, ⋂ j, s i j ⊆ t
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>s t : ι → Set α<VAR>h : ∀ (i : ι), s i ⊆ t i<GOAL>⋃ i, s i ⊆ ⋃ i, t i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>s t : ι → Set α<VAR>h : ∀ (i : ι), s i ⊆ t i<GOAL>Set.iUnion s ⊆ Set.iUnion t
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_7<VAR>s t : (i : ι) → κ i → Set α<VAR>h : ∀ (i : ι) (j : κ i), s i j ⊆ t i j<GOAL>⋃ i, ⋃ j, s i j ⊆ ⋃ i, ⋃ j, t i j
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>s t : ι → Set α<VAR>h : ∀ (i : ι), s i ⊆ t i<GOAL>⋂ i, s i ⊆ ⋂ i, t i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>s t : ι → Set α<VAR>h : ∀ (i : ι), s i ⊆ t i<GOAL>Set.iInter s ⊆ Set.iInter t
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_7<VAR>s t : (i : ι) → κ i → Set α<VAR>h : ∀ (i : ι) (j : κ i), s i j ⊆ t i j<GOAL>⋂ i, ⋂ j, s i j ⊆ ⋂ i, ⋂ j, t i j
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ι₂ : Sort u_6<VAR>s : ι → Set α<VAR>t : ι₂ → Set α<VAR>h : ∀ (i : ι), ∃ j, s i ⊆ t j<GOAL>⋃ i, s i ⊆ ⋃ i, t i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_10<VAR>s : (i : ι) → κ i → Set α<VAR>t : (i' : ι') → κ' i' → Set α<VAR>h : ∀ (i : ι) (j : κ i), ∃ i' j', s i j ⊆ t i' j'<GOAL>⋃ i, ⋃ j, s i j ⊆ ⋃ i', ⋃ j', t i' j'
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>s : ι → Set α<VAR>t : ι' → Set α<VAR>h : ∀ (j : ι'), ∃ i, s i ⊆ t j<GOAL>⋂ i, s i ⊆ ⋂ j, t j
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_10<VAR>s : (i : ι) → κ i → Set α<VAR>t : (i' : ι') → κ' i' → Set α<VAR>h : ∀ (i' : ι') (j' : κ' i'), ∃ i j, s i j ⊆ t i' j'<GOAL>⋂ i, ⋂ j, s i j ⊆ ⋂ i', ⋂ j', t i' j'
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_11<VAR>s : ι → Set α<GOAL>⋃ i, ⋃ x, s i ⊆ ⋃ i, s i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_11<VAR>s : ι → Set α<GOAL>⋂ i, s i ⊆ ⋂ i, ⋂ x, s i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>P : ι → α → Prop<GOAL>⋃ i, {x | P i x} = {x | ∃ i, P i x}
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>P : ι → α → Prop<GOAL>⋂ i, {x | P i x} = {x | ∀ (i : ι), P i x}
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ι₂ : Sort u_6<VAR>f : ι → Set α<VAR>g : ι₂ → Set α<VAR>h : ι → ι₂<VAR>h1 : Function.Surjective h<VAR>h2 : ∀ (x : ι), g (h x) = f x<GOAL>⋃ x, f x = ⋃ y, g y
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ι₂ : Sort u_6<VAR>f : ι → Set α<VAR>g : ι₂ → Set α<VAR>h : ι → ι₂<VAR>h1 : Function.Surjective h<VAR>h2 : ∀ (x : ι), g (h x) = f x<GOAL>⋂ x, f x = ⋂ y, g y
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>s t : ι → Set α<VAR>h : ∀ (i : ι), s i = t i<GOAL>⋃ i, s i = ⋃ i, t i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>s t : ι → Set α<VAR>h : ∀ (i : ι), s i = t i<GOAL>⋂ i, s i = ⋂ i, t i