theorem WithTop.eq_top_iff_forall_le {α : Type u_3} [Preorder α] [NoMaxOrder α] {x : WithTop α} : x = ⊤ ↔ ∀ (a : α), ↑a ≤ x

theorem WithBot.eq_bot_iff_forall_ge {α : Type u_3} [Preorder α] [NoMinOrder α] {x : WithBot α} : x = ⊥ ↔ ∀ (a : α), x ≤ ↑a

@[simp]

theorem ENat.lt_one_iff (n : ℕ∞) : n < 1 ↔ n = 0

theorem biUnion_insert_eq {α : Type u_1} {X : Set α} (hX : X.Nonempty) (Y : Set α) : ⋃ x ∈ X, insert x Y = X ∪ Y

theorem Equiv.exists_bijOn {α : Type u_1} {β : Type u_2} [Nonempty β] {s : Set α} {t : Set β} (e : ↑s ≃ ↑t) : ∃ (f : α → β), Set.BijOn f s t ∧ ∀ (x : ↑s), ↑(e x) = f ↑x

theorem Set.Finite.encard_eq_iff_nonempty_equiv {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (ht : t.Finite) : s.encard = t.encard ↔ Nonempty (↑s ≃ ↑t)

theorem Set.Finite.encard_eq_iff_nonempty_equiv' {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (hs : s.Finite) : s.encard = t.encard ↔ Nonempty (↑s ≃ ↑t)

theorem Equiv.bijOn_swap' {α : Type u_1} {e f : α} [DecidableEq α] {S : Set α} (hef : e ∈ S ↔ f ∈ S) : Set.BijOn (⇑(swap e f)) S S

theorem Equiv.swap_image_eq_self {α : Type u_1} {e f : α} [DecidableEq α] {S : Set α} (hef : e ∈ S ↔ f ∈ S) : ⇑(swap e f) '' S = S

theorem Equiv.swap_image_eq_exchange {α : Type u_1} {e f : α} [DecidableEq α] {S : Set α} (he : e ∈ S) (hf : f ∉ S) : ⇑(swap e f) '' S = insert f (S \ {e})