ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<GOAL>(s.sigma t).Nonempty → s.Nonempty
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<GOAL>(s.sigma t).Nonempty → ∃ i ∈ s, (t i).Nonempty
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<GOAL>(s.sigma t).Nonempty ↔ ∃ i ∈ s, (t i).Nonempty
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<GOAL>s.sigma t = ∅ ↔ ∀ i ∈ s, t i = ∅
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>a : (i : ι) → α i<VAR>ha : ∀ (i : ι), a i ∈ t i<GOAL>(fun i => ⟨i, a i⟩) '' s ⊆ s.sigma t
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>i : ι<VAR>hi : i ∈ s<GOAL>Sigma.mk i '' t i ⊆ s.sigma t
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<GOAL>s.sigma t ⊆ Sigma.fst ⁻¹' s
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<GOAL>Sigma.fst '' s.sigma t ⊆ s
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>t : (i : ι) → Set (α i)<VAR>s : Set ι<VAR>ht : ∀ (i : ι), (t i).Nonempty<GOAL>Sigma.fst '' s.sigma t = s
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>s₁ s₂ : Set ι<VAR>t₁ t₂ : (i : ι) → Set (α i)<GOAL>s₁.sigma t₁ \ s₂.sigma t₂ = s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁
<VAR>α : Type u_3<VAR>self : TwoPointing α<GOAL>self.fst ≠ self.snd
<VAR>α : Type u_1<VAR>p : TwoPointing α<GOAL>p.snd ≠ p.fst
<VAR>α : Type u_1<VAR>p : TwoPointing α<GOAL>p.swap.toProd = (p.snd, p.fst)
<VAR>α : Type u_1<VAR>p : TwoPointing α<GOAL>p.swap.fst = p.snd
<VAR>α : Type u_1<VAR>p : TwoPointing α<GOAL>p.swap.snd = p.fst
<VAR>α : Type u_1<VAR>p : TwoPointing α<GOAL>p.swap.swap = p
<VAR>α : Type u_1<VAR>p : TwoPointing α<GOAL>Nontrivial α
<VAR>α : Type u_1<GOAL>Nonempty (TwoPointing α) ↔ Nontrivial α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>q : TwoPointing β<VAR>Nonempty α<GOAL>(TwoPointing.pi α q).fst = Function.const α q.fst
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>q : TwoPointing β<VAR>Nonempty α<GOAL>(TwoPointing.pi α q).snd = Function.const α q.snd
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : TwoPointing α<VAR>q : TwoPointing β<GOAL>(p.prod q).fst = (p.fst, q.fst)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : TwoPointing α<VAR>q : TwoPointing β<GOAL>(p.prod q).snd = (p.snd, q.snd)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : TwoPointing α<VAR>q : TwoPointing β<GOAL>(p.sum q).fst = Sum.inl p.fst
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : TwoPointing α<VAR>q : TwoPointing β<GOAL>(p.sum q).snd = Sum.inr q.snd
<VAR>α : Type u<GOAL>⊤ = Set.univ
<VAR>α : Type u<GOAL>(fun x x_1 => x ⊔ x_1) = fun x x_1 => x ∪ x_1
<VAR>α : Type u<GOAL>(fun x x_1 => x ⊓ x_1) = fun x x_1 => x ∩ x_1
<VAR>α : Type u<GOAL>(fun x x_1 => x ≤ x_1) = fun x x_1 => x ⊆ x_1
<VAR>α : Type u<GOAL>(fun x x_1 => x < x_1) = fun x x_1 => x ⊂ x_1
<VAR>α : Type u<VAR>s t : Set α<GOAL>s ≤ t ↔ s ⊆ t
<VAR>α : Type u<VAR>s t : Set α<GOAL>s < t ↔ s ⊂ t
<VAR>α : Type u<VAR>s : Set α<GOAL>↑s = { x // x ∈ s }
<VAR>α : Type u<VAR>p : α → Prop<GOAL>↑{x | p x} = { x // p x }
<VAR>α : Type u<VAR>s : Set α<VAR>p : ↑s → Prop<GOAL>(∀ (x : ↑s), p x) ↔ ∀ (x : α) (h : x ∈ s), p ⟨x, h⟩
<VAR>α : Type u<VAR>s : Set α<VAR>p : ↑s → Prop<GOAL>(∃ x, p x) ↔ ∃ x, ∃ (h : x ∈ s), p ⟨x, h⟩
<VAR>α : Type u<VAR>s : Set α<VAR>p : (x : α) → x ∈ s → Prop<GOAL>(∃ x, ∃ (h : x ∈ s), p x h) ↔ ∃ x, p ↑x ⋯
<VAR>α : Type u<VAR>s : Set α<VAR>p : (x : α) → x ∈ s → Prop<GOAL>(∀ (x : α) (h : x ∈ s), p x h) ↔ ∀ (x : ↑s), p ↑x ⋯
<VAR>α : Type u<VAR>s t : Set α<VAR>H' : s = t<VAR>H : ↑s = ↑t<VAR>x : ↑s<GOAL>cast H x = ⟨↑x, ⋯⟩
<VAR>α : Type u<VAR>s : Set α<VAR>a b : ↑s<GOAL>↑a = ↑b → a = b
<VAR>α : Type u<VAR>s : Set α<VAR>a b : ↑s<GOAL>↑a = ↑b ↔ a = b
<VAR>α : Type u_1<VAR>s : Set α<VAR>p : ↑s<GOAL>↑p ∈ s
<VAR>α : Type u_1<VAR>s t : Set α<GOAL>s = t → s ⊆ t
<VAR>α : Type u<VAR>s t : Set α<GOAL>s = t ↔ ∀ (x : α), x ∈ s ↔ x ∈ t
<VAR>α : Type u<VAR>x : α<VAR>s t : Set α<VAR>hx : x ∈ s<VAR>h : s ⊆ t<GOAL>x ∈ t
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>p : α → β → Prop<GOAL>(∀ a ∈ s, ∀ (b : β), p a b) ↔ ∀ (b : β), ∀ a ∈ s, p a b
<VAR>α : Type u<VAR>a : α<VAR>p : α → Prop<GOAL>a ∈ {x | p x} ↔ p a
<VAR>α : Type u<VAR>p : α → Prop<VAR>a : α<VAR>h : a ∈ {x | p x}<GOAL>p a
<VAR>α : Type u<VAR>a : α<VAR>p : α → Prop<GOAL>a ∉ {x | p x} ↔ ¬p a
<VAR>α : Type u<VAR>s : Set α<GOAL>{x | x ∈ s} = s
<VAR>α : Type u<VAR>s : Set α<GOAL>setOf s = s
<VAR>α : Type u<VAR>p : α → Prop<VAR>x : α<GOAL>{x | p x} x ↔ p x
<VAR>α : Type u<VAR>a : α<VAR>s : Set α<GOAL>a ∈ s ↔ s a
<VAR>α : Type u<VAR>p : α → Prop<VAR>s : Set α<GOAL>s ⊆ setOf p ↔ ∀ x ∈ s, p x
<VAR>α : Type u<VAR>p : α → Prop<VAR>s : Set α<GOAL>setOf p ⊆ s ↔ ∀ (x : α), p x → x ∈ s
<VAR>α : Type u<VAR>p q : α → Prop<GOAL>{a | p a} ⊆ {a | q a} ↔ ∀ (a : α), p a → q a
<VAR>α : Type u<VAR>p q : α → Prop<GOAL>{a | p a ∧ q a} = {a | p a} ∩ {a | q a}
<VAR>α : Type u<VAR>p q : α → Prop<GOAL>{a | p a ∨ q a} = {a | p a} ∪ {a | q a}
<VAR>α : Type u<VAR>s t : Set α<GOAL>(s ⊆ t) = ∀ x ∈ s, x ∈ t
<VAR>α : Type u<VAR>s t : Set α<GOAL>(s ⊂ t) = (s ⊆ t ∧ ¬t ⊆ s)
<VAR>α : Type u<VAR>a : Set α<GOAL>a ⊆ a
<VAR>α : Type u<VAR>s : Set α<GOAL>s ⊆ s
<VAR>α : Type u<VAR>a b c : Set α<VAR>ab : a ⊆ b<VAR>bc : b ⊆ c<GOAL>a ⊆ c
<VAR>α : Type u<VAR>x y : α<VAR>s : Set α<VAR>hx : x = y<VAR>h : y ∈ s<GOAL>x ∈ s
<VAR>α : Type u<VAR>a b : Set α<VAR>h₁ : a ⊆ b<VAR>h₂ : b ⊆ a<GOAL>a = b
<VAR>α : Type u<VAR>a b : Set α<GOAL>a = b ↔ a ⊆ b ∧ b ⊆ a
<VAR>α : Type u<VAR>a b : Set α<GOAL>a ⊆ b → b ⊆ a → a = b
<VAR>α : Type u<VAR>s₁ s₂ : Set α<VAR>a : α<VAR>h : s₁ ⊆ s₂<GOAL>a ∈ s₁ → a ∈ s₂
<VAR>α : Type u<VAR>a : α<VAR>s t : Set α<VAR>h : s ⊆ t<GOAL>a ∉ t → a ∉ s
<VAR>α : Type u<VAR>s t : Set α<GOAL>¬s ⊆ t ↔ ∃ a ∈ s, a ∉ t
<VAR>α : Type u<VAR>s t : Set α<VAR>h : ∀ (u : Set α), s ⊆ u ↔ t ⊆ u<GOAL>s = t
<VAR>α : Type u<VAR>s t : Set α<VAR>h : s ⊆ t<GOAL>s = t ∨ s ⊂ t
<VAR>α : Type u<VAR>s t : Set α<VAR>h : s ⊂ t<GOAL>∃ x ∈ t, x ∉ s
<VAR>α : Type u<VAR>s t : Set α<GOAL>s ⊂ t ↔ s ⊆ t ∧ s ≠ t
<VAR>α : Type u<VAR>s t : Set α<VAR>h : s ⊆ t<GOAL>s ⊂ t ↔ ∃ x ∈ t, x ∉ s
<VAR>α : Type u<VAR>s₁ s₂ s₃ : Set α<VAR>hs₁s₂ : s₁ ⊂ s₂<VAR>hs₂s₃ : s₂ ⊆ s₃<GOAL>s₁ ⊂ s₃
<VAR>α : Type u<VAR>s₁ s₂ s₃ : Set α<VAR>hs₁s₂ : s₁ ⊆ s₂<VAR>hs₂s₃ : s₂ ⊂ s₃<GOAL>s₁ ⊂ s₃
<VAR>α : Type u<VAR>x : α<GOAL>x ∉ ∅
<VAR>α : Type u<VAR>a : α<VAR>s : Set α<GOAL>¬a ∉ s ↔ a ∈ s
<VAR>α : Type u<VAR>s : Set α<GOAL>Nonempty ↑s ↔ s.Nonempty
<VAR>α : Type u<VAR>s : Set α<GOAL>s.Nonempty ↔ ∃ x, x ∈ s
<VAR>α : Type u<VAR>s : Set α<VAR>x : α<VAR>h : x ∈ s<GOAL>s.Nonempty
<VAR>α : Type u<VAR>s : Set α<GOAL>s.Nonempty → ¬s ⊆ ∅
<VAR>α : Type u<VAR>s : Set α<VAR>h : s.Nonempty<GOAL>h.some ∈ s
<VAR>α : Type u<VAR>s t : Set α<VAR>ht : s ⊆ t<VAR>hs : s.Nonempty<GOAL>t.Nonempty
<VAR>α : Type u<VAR>s t : Set α<VAR>h : ¬s ⊆ t<GOAL>(s \ t).Nonempty
<VAR>α : Type u<VAR>s t : Set α<VAR>ht : s ⊂ t<GOAL>(t \ s).Nonempty
<VAR>α : Type u<VAR>s t : Set α<VAR>h : (s \ t).Nonempty<GOAL>s.Nonempty
<VAR>α : Type u<VAR>s t : Set α<VAR>ht : s ⊂ t<GOAL>t.Nonempty
<VAR>α : Type u<VAR>s t : Set α<VAR>hs : s.Nonempty<GOAL>(s ∪ t).Nonempty
<VAR>α : Type u<VAR>s t : Set α<VAR>ht : t.Nonempty<GOAL>(s ∪ t).Nonempty
<VAR>α : Type u<VAR>s t : Set α<GOAL>(s ∪ t).Nonempty ↔ s.Nonempty ∨ t.Nonempty
<VAR>α : Type u<VAR>s t : Set α<VAR>h : (s ∩ t).Nonempty<GOAL>s.Nonempty
<VAR>α : Type u<VAR>s t : Set α<VAR>h : (s ∩ t).Nonempty<GOAL>t.Nonempty
<VAR>α : Type u<VAR>s t : Set α<GOAL>(s ∩ t).Nonempty ↔ ∃ x ∈ s, x ∈ t
<VAR>α : Type u<VAR>s t : Set α<GOAL>(s ∩ t).Nonempty ↔ ∃ x ∈ t, x ∈ s
<VAR>α : Type u<GOAL>Nonempty α ↔ Set.univ.Nonempty
<VAR>α : Type u<VAR>Nonempty α<GOAL>Set.univ.Nonempty
<VAR>α : Type u<VAR>s : Set α<GOAL>s.Nonempty → Nonempty ↑s
<VAR>α : Type u<VAR>s : Set α<GOAL>s.Nonempty → Nonempty α
<VAR>α : Type u<VAR>s : Set α<VAR>Nonempty ↑s<GOAL>s.Nonempty
<VAR>α : Type u<GOAL>∅ = {_x | False}
<VAR>α : Type u<VAR>x : α<GOAL>x ∈ ∅ ↔ False
<VAR>α : Type u<GOAL>{_a | False} = ∅
<VAR>α : Type u<GOAL>{_x | ⊥} = ∅
<VAR>α : Type u<VAR>s : Set α<GOAL>∅ ⊆ s
<VAR>α : Type u<VAR>s : Set α<GOAL>s ⊆ ∅ ↔ s = ∅
<VAR>α : Type u<VAR>s : Set α<GOAL>s = ∅ ↔ ∀ (x : α), x ∉ s
<VAR>α : Type u<VAR>s : Set α<VAR>h : ∀ (x : α), x ∉ s<GOAL>s = ∅
<VAR>α : Type u<VAR>s : Set α<GOAL>s ⊆ ∅ → s = ∅
<VAR>α : Type u<VAR>IsEmpty α<VAR>s : Set α<GOAL>s = ∅
<VAR>α : Type u<VAR>s : Set α<GOAL>¬s.Nonempty ↔ s = ∅
<VAR>α : Type u<VAR>s : Set α<GOAL>s.Nonempty ↔ s ≠ ∅
<VAR>α : Type u<VAR>s : Set α<GOAL>¬Nonempty ↑s ↔ s = ∅
<VAR>α : Type u<VAR>s : Set α<GOAL>Nonempty ↑s ↔ s ≠ ∅
<VAR>α : Type u<GOAL>¬∅.Nonempty
<VAR>α : Type u<VAR>s : Set α<GOAL>IsEmpty ↑s ↔ s = ∅
<VAR>α : Type u<VAR>s : Set α<GOAL>s = ∅ ∨ s.Nonempty
<VAR>α : Type u<VAR>s t : Set α<VAR>h : t ⊆ s<VAR>e : s = ∅<GOAL>t = ∅
<VAR>α : Type u<VAR>p : α → Prop<GOAL>(∀ x ∈ ∅, p x) ↔ True
<VAR>α : Type u<VAR>s : Set α<GOAL>∅ ⊂ s ↔ s.Nonempty
<VAR>α : Type u<GOAL>{_x | True} = Set.univ
<VAR>α : Type u<GOAL>{_x | ⊤} = Set.univ
<VAR>α : Type u<GOAL>Set.univ = ∅ ↔ IsEmpty α
<VAR>α : Type u<VAR>Nonempty α<GOAL>∅ ≠ Set.univ
<VAR>α : Type u<VAR>s : Set α<GOAL>s ⊆ Set.univ
<VAR>α : Type u<VAR>s : Set α<GOAL>Set.univ ⊆ s ↔ s = Set.univ
<VAR>α : Type u<VAR>s : Set α<GOAL>s = Set.univ ↔ ∀ (x : α), x ∈ s
<VAR>α : Type u<VAR>s : Set α<GOAL>(∀ (x : α), x ∈ s) → s = Set.univ
<VAR>α : Type u<VAR>s : Set α<VAR>Subsingleton α<GOAL>s.Nonempty → s = Set.univ
<VAR>α : Type u<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>hs : s = Set.univ<GOAL>t = Set.univ
<VAR>α : Type u_1<VAR>Nonempty α<GOAL>∃ x, x ∈ Set.univ
<VAR>α : Type u_1<VAR>s : Set α<GOAL>s ≠ Set.univ ↔ ∃ a, a ∉ s
<VAR>α : Type u_1<VAR>s t : Set α<GOAL>¬s ⊆ t ↔ ∃ x ∈ s, x ∉ t
<VAR>α : Type u<VAR>Unique α<GOAL>Set.univ = {default}
<VAR>α : Type u<VAR>s : Set α<GOAL>s ⊂ Set.univ ↔ s ≠ Set.univ
<VAR>α : Type u<VAR>s₁ s₂ : Set α<GOAL>s₁ ∪ s₂ = {a | a ∈ s₁ ∨ a ∈ s₂}
<VAR>α : Type u<VAR>x : α<VAR>a : Set α<VAR>b : Set α<GOAL>x ∈ a → x ∈ a ∪ b
<VAR>α : Type u<VAR>x : α<VAR>b : Set α<VAR>a : Set α<GOAL>x ∈ b → x ∈ a ∪ b
<VAR>α : Type u<VAR>x : α<VAR>a b : Set α<VAR>H : x ∈ a ∪ b<GOAL>x ∈ a ∨ x ∈ b
<VAR>α : Type u<VAR>x : α<VAR>a b : Set α<VAR>P : Prop<VAR>H₁ : x ∈ a ∪ b<VAR>H₂ : x ∈ a → P<VAR>H₃ : x ∈ b → P<GOAL>P
<VAR>α : Type u<VAR>x : α<VAR>a b : Set α<GOAL>x ∈ a ∪ b ↔ x ∈ a ∨ x ∈ b
<VAR>α : Type u<VAR>a : Set α<GOAL>a ∪ a = a
<VAR>α : Type u<VAR>a : Set α<GOAL>a ∪ ∅ = a
<VAR>α : Type u<VAR>a : Set α<GOAL>∅ ∪ a = a
<VAR>α : Type u<VAR>a b : Set α<GOAL>a ∪ b = b ∪ a
<VAR>α : Type u<VAR>a b c : Set α<GOAL>a ∪ b ∪ c = a ∪ (b ∪ c)
<VAR>α : Type u<VAR>s₁ s₂ s₃ : Set α<GOAL>s₁ ∪ (s₂ ∪ s₃) = s₂ ∪ (s₁ ∪ s₃)
<VAR>α : Type u<VAR>s₁ s₂ s₃ : Set α<GOAL>s₁ ∪ s₂ ∪ s₃ = s₁ ∪ s₃ ∪ s₂
<VAR>α : Type u<VAR>s t : Set α<GOAL>s ∪ t = s ↔ t ⊆ s
<VAR>α : Type u<VAR>s t : Set α<GOAL>s ∪ t = t ↔ s ⊆ t
<VAR>α : Type u<VAR>s t : Set α<VAR>h : s ⊆ t<GOAL>s ∪ t = t
<VAR>α : Type u<VAR>s t : Set α<VAR>h : t ⊆ s<GOAL>s ∪ t = s
<VAR>α : Type u<VAR>s t : Set α<GOAL>s ⊆ s ∪ t
<VAR>α : Type u<VAR>s t : Set α<GOAL>t ⊆ s ∪ t
<VAR>α : Type u<VAR>s t r : Set α<VAR>sr : s ⊆ r<VAR>tr : t ⊆ r<GOAL>s ∪ t ⊆ r
<VAR>α : Type u<VAR>s t u : Set α<GOAL>s ∪ t ⊆ u ↔ s ⊆ u ∧ t ⊆ u
<VAR>α : Type u<VAR>s₁ s₂ t₁ t₂ : Set α<VAR>h₁ : s₁ ⊆ s₂<VAR>h₂ : t₁ ⊆ t₂<GOAL>s₁ ∪ t₁ ⊆ s₂ ∪ t₂
<VAR>α : Type u<VAR>s₁ s₂ : Set α<VAR>t : Set α<VAR>h : s₁ ⊆ s₂<GOAL>s₁ ∪ t ⊆ s₂ ∪ t
<VAR>α : Type u<VAR>s : Set α<VAR>t₁ t₂ : Set α<VAR>h : t₁ ⊆ t₂<GOAL>s ∪ t₁ ⊆ s ∪ t₂
<VAR>α : Type u<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>u : Set α<GOAL>s ⊆ t ∪ u
<VAR>α : Type u<VAR>s u : Set α<VAR>h : s ⊆ u<VAR>t : Set α<GOAL>s ⊆ t ∪ u
<VAR>α : Type u<VAR>s t u : Set α<VAR>ht : t ⊆ s ∪ u<VAR>hu : u ⊆ s ∪ t<GOAL>s ∪ t = s ∪ u
<VAR>α : Type u<VAR>s t u : Set α<VAR>hs : s ⊆ t ∪ u<VAR>ht : t ⊆ s ∪ u<GOAL>s ∪ u = t ∪ u
<VAR>α : Type u<VAR>s t u : Set α<GOAL>s ∪ t = s ∪ u ↔ t ⊆ s ∪ u ∧ u ⊆ s ∪ t
<VAR>α : Type u<VAR>s t u : Set α<GOAL>s ∪ u = t ∪ u ↔ s ⊆ t ∪ u ∧ t ⊆ s ∪ u
<VAR>α : Type u<VAR>s t : Set α<GOAL>s ∪ t = ∅ ↔ s = ∅ ∧ t = ∅
<VAR>α : Type u<VAR>s : Set α<GOAL>s ∪ Set.univ = Set.univ
<VAR>α : Type u<VAR>s : Set α<GOAL>Set.univ ∪ s = Set.univ
<VAR>α : Type u<VAR>s₁ s₂ : Set α<GOAL>s₁ ∩ s₂ = {a | a ∈ s₁ ∧ a ∈ s₂}
<VAR>α : Type u<VAR>x : α<VAR>a b : Set α<GOAL>x ∈ a ∩ b ↔ x ∈ a ∧ x ∈ b
<VAR>α : Type u<VAR>x : α<VAR>a b : Set α<VAR>ha : x ∈ a<VAR>hb : x ∈ b<GOAL>x ∈ a ∩ b
<VAR>α : Type u<VAR>x : α<VAR>a b : Set α<VAR>h : x ∈ a ∩ b<GOAL>x ∈ a
<VAR>α : Type u<VAR>x : α<VAR>a b : Set α<VAR>h : x ∈ a ∩ b<GOAL>x ∈ b
<VAR>α : Type u<VAR>a : Set α<GOAL>a ∩ a = a
<VAR>α : Type u<VAR>a : Set α<GOAL>a ∩ ∅ = ∅
<VAR>α : Type u<VAR>a : Set α<GOAL>∅ ∩ a = ∅
<VAR>α : Type u<VAR>a b : Set α<GOAL>a ∩ b = b ∩ a
<VAR>α : Type u<VAR>a b c : Set α<GOAL>a ∩ b ∩ c = a ∩ (b ∩ c)
<VAR>α : Type u<VAR>s₁ s₂ s₃ : Set α<GOAL>s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃)
<VAR>α : Type u<VAR>s₁ s₂ s₃ : Set α<GOAL>s₁ ∩ s₂ ∩ s₃ = s₁ ∩ s₃ ∩ s₂
<VAR>α : Type u<VAR>s t : Set α<GOAL>s ∩ t ⊆ s
<VAR>α : Type u<VAR>s t : Set α<GOAL>s ∩ t ⊆ t
<VAR>α : Type u<VAR>s t r : Set α<VAR>rs : r ⊆ s<VAR>rt : r ⊆ t<GOAL>r ⊆ s ∩ t
<VAR>α : Type u<VAR>s t r : Set α<GOAL>r ⊆ s ∩ t ↔ r ⊆ s ∧ r ⊆ t
<VAR>α : Type u<VAR>s t : Set α<GOAL>s ∩ t = s ↔ s ⊆ t
<VAR>α : Type u<VAR>s t : Set α<GOAL>s ∩ t = t ↔ t ⊆ s
<VAR>α : Type u<VAR>s t : Set α<GOAL>s = s ∩ t ↔ s ⊆ t
<VAR>α : Type u<VAR>s t : Set α<GOAL>t = s ∩ t ↔ t ⊆ s
<VAR>α : Type u<VAR>s t : Set α<GOAL>s ⊆ t → s ∩ t = s
<VAR>α : Type u<VAR>s t : Set α<GOAL>t ⊆ s → s ∩ t = t
<VAR>α : Type u<VAR>s t u : Set α<VAR>ht : s ∩ u ⊆ t<VAR>hu : s ∩ t ⊆ u<GOAL>s ∩ t = s ∩ u
<VAR>α : Type u<VAR>s t u : Set α<VAR>hs : t ∩ u ⊆ s<VAR>ht : s ∩ u ⊆ t<GOAL>s ∩ u = t ∩ u
<VAR>α : Type u<VAR>s t u : Set α<GOAL>s ∩ t = s ∩ u ↔ s ∩ u ⊆ t ∧ s ∩ t ⊆ u
<VAR>α : Type u<VAR>s t u : Set α<GOAL>s ∩ u = t ∩ u ↔ t ∩ u ⊆ s ∧ s ∩ u ⊆ t
<VAR>α : Type u<VAR>a : Set α<GOAL>a ∩ Set.univ = a
<VAR>α : Type u<VAR>a : Set α<GOAL>Set.univ ∩ a = a
<VAR>α : Type u<VAR>s₁ s₂ t₁ t₂ : Set α<VAR>h₁ : s₁ ⊆ t₁<VAR>h₂ : s₂ ⊆ t₂<GOAL>s₁ ∩ s₂ ⊆ t₁ ∩ t₂
<VAR>α : Type u<VAR>s t : Set α<VAR>u : Set α<VAR>H : s ⊆ t<GOAL>s ∩ u ⊆ t ∩ u
<VAR>α : Type u<VAR>s t : Set α<VAR>u : Set α<VAR>H : s ⊆ t<GOAL>u ∩ s ⊆ u ∩ t
<VAR>α : Type u<VAR>s t : Set α<GOAL>(s ∪ t) ∩ s = s
<VAR>α : Type u<VAR>s t : Set α<GOAL>(s ∪ t) ∩ t = t
<VAR>α : Type u<VAR>s : Set α<VAR>p : α → Prop<GOAL>s ∩ {a | p a} = {a | a ∈ s ∧ p a}
<VAR>α : Type u<VAR>p : α → Prop<VAR>s : Set α<GOAL>{a | p a} ∩ s = {a | a ∈ s ∧ p a}
<VAR>α : Type u<VAR>s t u : Set α<GOAL>s ∩ (t ∪ u) = s ∩ t ∪ s ∩ u
<VAR>α : Type u<VAR>s t u : Set α<GOAL>(s ∪ t) ∩ u = s ∩ u ∪ t ∩ u
<VAR>α : Type u<VAR>s t u : Set α<GOAL>s ∪ t ∩ u = (s ∪ t) ∩ (s ∪ u)
<VAR>α : Type u<VAR>s t u : Set α<GOAL>s ∩ t ∪ u = (s ∪ u) ∩ (t ∪ u)
<VAR>α : Type u<VAR>s t u : Set α<GOAL>s ∪ (t ∪ u) = s ∪ t ∪ (s ∪ u)
<VAR>α : Type u<VAR>s t u : Set α<GOAL>s ∪ t ∪ u = s ∪ u ∪ (t ∪ u)
<VAR>α : Type u<VAR>s t u : Set α<GOAL>s ∩ (t ∩ u) = s ∩ t ∩ (s ∩ u)
<VAR>α : Type u<VAR>s t u : Set α<GOAL>s ∩ t ∩ u = s ∩ u ∩ (t ∩ u)
<VAR>α : Type u<VAR>s t u v : Set α<GOAL>s ∪ t ∪ (u ∪ v) = s ∪ u ∪ (t ∪ v)
<VAR>α : Type u<VAR>s t u v : Set α<GOAL>s ∩ t ∩ (u ∩ v) = s ∩ u ∩ (t ∩ v)
<VAR>α : Type u<VAR>x : α<VAR>s : Set α<GOAL>insert x s = {y | y = x ∨ y ∈ s}
<VAR>α : Type u<VAR>x : α<VAR>s : Set α<GOAL>s ⊆ insert x s
<VAR>α : Type u<VAR>x : α<VAR>s : Set α<GOAL>x ∈ insert x s
<VAR>α : Type u<VAR>x : α<VAR>s : Set α<VAR>y : α<GOAL>x ∈ s → x ∈ insert y s
<VAR>α : Type u<VAR>x a : α<VAR>s : Set α<GOAL>x ∈ insert a s → x = a ∨ x ∈ s
<VAR>α : Type u<VAR>a b : α<VAR>s : Set α<GOAL>b ∈ insert a s → b ≠ a → b ∈ s
<VAR>α : Type u<VAR>a b : α<VAR>s : Set α<GOAL>b ∈ insert a s → b ∉ s → b = a
<VAR>α : Type u<VAR>x a : α<VAR>s : Set α<GOAL>x ∈ insert a s ↔ x = a ∨ x ∈ s
<VAR>α : Type u<VAR>a : α<VAR>s : Set α<VAR>h : a ∈ s<GOAL>insert a s = s
<VAR>α : Type u<VAR>s : Set α<VAR>t : Set α<VAR>a : α<GOAL>a ∉ s → s ≠ insert a t
<VAR>α : Type u<VAR>a : α<VAR>s : Set α<GOAL>insert a s = s ↔ a ∈ s
<VAR>α : Type u<VAR>a : α<VAR>s : Set α<GOAL>insert a s ≠ s ↔ a ∉ s
<VAR>α : Type u<VAR>a : α<VAR>s t : Set α<GOAL>insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t
<VAR>α : Type u<VAR>a : α<VAR>s t : Set α<VAR>ha : a ∈ t<VAR>hs : s ⊆ t<GOAL>insert a s ⊆ t
<VAR>α : Type u<VAR>a : α<VAR>s t : Set α<VAR>h : s ⊆ t<GOAL>insert a s ⊆ insert a t
<VAR>α : Type u<VAR>a : α<VAR>s t : Set α<VAR>ha : a ∉ s<GOAL>insert a s ⊆ insert a t ↔ s ⊆ t
<VAR>α : Type u<VAR>a : α<VAR>s t : Set α<VAR>ha : a ∉ s<GOAL>s ⊆ insert a t ↔ s ⊆ t
<VAR>α : Type u<VAR>s t : Set α<GOAL>s ⊂ t ↔ ∃ a ∉ s, insert a s ⊆ t
<VAR>α : Type u<VAR>s : Set α<VAR>a : α<VAR>h : a ∉ s<GOAL>s ⊂ insert a s
<VAR>α : Type u<VAR>a b : α<VAR>s : Set α<GOAL>insert a (insert b s) = insert b (insert a s)
<VAR>α : Type u<VAR>a : α<VAR>s : Set α<GOAL>insert a (insert a s) = insert a s
<VAR>α : Type u<VAR>a : α<VAR>s t : Set α<GOAL>insert a s ∪ t = insert a (s ∪ t)
<VAR>α : Type u<VAR>a : α<VAR>s t : Set α<GOAL>s ∪ insert a t = insert a (s ∪ t)
<VAR>α : Type u<VAR>a : α<VAR>s : Set α<GOAL>(insert a s).Nonempty
<VAR>α : Type u<VAR>a : α<VAR>s t : Set α<GOAL>insert a (s ∩ t) = insert a s ∩ insert a t
<VAR>α : Type u<VAR>a : α<VAR>s t : Set α<GOAL>insert a (s ∪ t) = insert a s ∪ insert a t
<VAR>α : Type u<VAR>a b : α<VAR>s : Set α<VAR>ha : a ∉ s<GOAL>insert a s = insert b s ↔ a = b
<VAR>α : Type u<VAR>P : α → Prop<VAR>a : α<VAR>s : Set α<VAR>H : ∀ x ∈ insert a s, P x<VAR>x : α<VAR>h : x ∈ s<GOAL>P x
<VAR>α : Type u<VAR>P : α → Prop<VAR>a : α<VAR>s : Set α<VAR>H : ∀ x ∈ s, P x<VAR>ha : P a<VAR>x : α<VAR>h : x ∈ insert a s<GOAL>P x
<VAR>α : Type u<VAR>P : α → Prop<VAR>a : α<VAR>s : Set α<GOAL>(∃ x ∈ insert a s, P x) ↔ P a ∨ ∃ x ∈ s, P x
<VAR>α : Type u<VAR>P : α → Prop<VAR>a : α<VAR>s : Set α<GOAL>(∀ x ∈ insert a s, P x) ↔ P a ∧ ∀ x ∈ s, P x
<VAR>α : Type u<VAR>a : α<GOAL>{a} = insert a ∅
<VAR>α : Type u<VAR>a b : α<GOAL>a ∈ {b} ↔ a = b
<VAR>α : Type u<VAR>a b : α<GOAL>a ∉ {b} ↔ a ≠ b
<VAR>α : Type u<VAR>a : α<GOAL>{n | n = a} = {a}
<VAR>α : Type u<VAR>a : α<GOAL>{x | a = x} = {a}
<VAR>α : Type u<VAR>a : α<GOAL>a ∈ {a}
<VAR>α : Type u<VAR>x y : α<VAR>h : x ∈ {y}<GOAL>x = y
<VAR>α : Type u<VAR>x y : α<GOAL>{x} = {y} ↔ x = y
<VAR>α : Type u<VAR>x y : α<VAR>H : x = y<GOAL>x ∈ {y}
<VAR>α : Type u<VAR>x : α<VAR>s : Set α<GOAL>insert x s = {x} ∪ s
<VAR>α : Type u<VAR>a : α<GOAL>{a}.Nonempty
<VAR>α : Type u<VAR>a : α<GOAL>{a} ≠ ∅
<VAR>α : Type u<VAR>a : α<GOAL>∅ ⊂ {a}
<VAR>α : Type u<VAR>a : α<VAR>s : Set α<GOAL>{a} ⊆ s ↔ a ∈ s
<VAR>α : Type u<VAR>a b : α<GOAL>{a} ⊆ {b} ↔ a = b
<VAR>α : Type u<VAR>a : α<GOAL>{b | b = a} = {a}
<VAR>α : Type u<VAR>a : α<VAR>s : Set α<GOAL>{a} ∪ s = insert a s
<VAR>α : Type u<VAR>a : α<VAR>s : Set α<GOAL>s ∪ {a} = insert a s
<VAR>α : Type u<VAR>a : α<VAR>s : Set α<GOAL>({a} ∩ s).Nonempty ↔ a ∈ s
<VAR>α : Type u<VAR>a : α<VAR>s : Set α<GOAL>(s ∩ {a}).Nonempty ↔ a ∈ s
<VAR>α : Type u<VAR>a : α<VAR>s : Set α<GOAL>{a} ∩ s = ∅ ↔ a ∉ s
<VAR>α : Type u<VAR>a : α<VAR>s : Set α<GOAL>s ∩ {a} = ∅ ↔ a ∉ s
<VAR>α : Type u<VAR>s : Set α<GOAL>s ∉ {∅} ↔ s.Nonempty
<VAR>α : Type u<VAR>a : α<VAR>s : Set α<GOAL>s = {a} ↔ a ∈ s ∧ ∀ x ∈ s, x = a
<VAR>α : Type u<VAR>a : α<VAR>s : Set α<GOAL>s = {a} ↔ s.Nonempty ∧ ∀ x ∈ s, x = a
<VAR>α : Type u<VAR>x : α<GOAL>default = ⟨x, ⋯⟩
<VAR>α : Type u<VAR>s : Set α<VAR>p : α → Prop<VAR>x : α<VAR>xs : x ∈ s<VAR>px : p x<GOAL>x ∈ {x | x ∈ s ∧ p x}
<VAR>α : Type u<VAR>s t : Set α<GOAL>{x | x ∈ s ∧ x ∈ t} = s ∩ t
<VAR>α : Type u<VAR>s : Set α<VAR>p : α → Prop<VAR>x : α<GOAL>x ∈ {x | x ∈ s ∧ p x} ↔ x ∈ s ∧ p x
<VAR>α : Type u<VAR>s : Set α<VAR>p q : α → Prop<GOAL>{x | x ∈ s ∧ p x} = {x | x ∈ s ∧ q x} ↔ ∀ x ∈ s, p x ↔ q x
<VAR>α : Type u<VAR>s t : Set α<VAR>h : s ⊆ t<GOAL>{x | x ∈ t ∧ x ∈ s} = s
<VAR>α : Type u<VAR>s : Set α<VAR>p : α → Prop<GOAL>{x | x ∈ s ∧ p x} ⊆ s
<VAR>α : Type u<VAR>s : Set α<VAR>p : α → Prop<GOAL>{x | x ∈ s ∧ p x} = s ↔ ∀ x ∈ s, p x
<VAR>α : Type u<VAR>s : Set α<VAR>p : α → Prop<GOAL>{x | x ∈ s ∧ p x} = ∅ ↔ ∀ x ∈ s, ¬p x
<VAR>α : Type u<VAR>s : Set α<GOAL>{x | x ∈ s ∧ True} = s
<VAR>α : Type u<VAR>s : Set α<GOAL>{x | x ∈ s ∧ False} = ∅
<VAR>α : Type u<VAR>p : α → Prop<GOAL>{x | x ∈ ∅ ∧ p x} = ∅
<VAR>α : Type u<VAR>p : α → Prop<GOAL>{x | x ∈ Set.univ ∧ p x} = {x | p x}
<VAR>α : Type u<VAR>s t : Set α<VAR>p : α → Prop<GOAL>{x | (x ∈ s ∨ x ∈ t) ∧ p x} = {x | x ∈ s ∧ p x} ∪ {x | x ∈ t ∧ p x}
<VAR>α : Type u<VAR>s t : Set α<VAR>p : α → Prop<GOAL>{x | (x ∈ s ∧ x ∈ t) ∧ p x} = {x | x ∈ s ∧ p x} ∩ {x | x ∈ t ∧ p x}
<VAR>α : Type u<VAR>s : Set α<VAR>p q : α → Prop<GOAL>{x | x ∈ s ∧ p x ∧ q x} = {x | x ∈ s ∧ p x} ∩ {x | x ∈ s ∧ q x}
<VAR>α : Type u<VAR>s : Set α<VAR>p q : α → Prop<GOAL>{x | x ∈ s ∧ (p x ∨ q x)} = {x | x ∈ s ∧ p x} ∪ {x | x ∈ s ∧ q x}
<VAR>α : Type u<VAR>p q : α → Prop<GOAL>{x | x ∈ {y | p y} ∧ q x} = {x | p x ∧ q x}
<VAR>α : Type u_1<VAR>s : Set α<VAR>x : α<GOAL>s ⊆ {x} ↔ ∀ y ∈ s, y = x
<VAR>α : Type u<VAR>s : Set α<VAR>x : α<GOAL>s ⊆ {x} ↔ s = ∅ ∨ s = {x}
<VAR>α : Type u<VAR>a : α<VAR>s : Set α<VAR>h : s.Nonempty<GOAL>s ⊆ {a} ↔ s = {a}
<VAR>α : Type u<VAR>s : Set α<VAR>x : α<GOAL>s ⊂ {x} ↔ s = ∅
<VAR>α : Type u<VAR>s : Set α<VAR>x : α<VAR>hs : s ⊂ {x}<GOAL>s = ∅
<VAR>α : Type u_1<VAR>Subsingleton α<VAR>s t : Set α<VAR>Nonempty ↑s<VAR>Nonempty ↑t<GOAL>s = t
<VAR>α : Type u_1<VAR>Subsingleton α<VAR>s : Set α<VAR>t : Set α<VAR>hs : s.Nonempty<VAR>Nonempty ↑t<GOAL>s = t
<VAR>α : Type u<VAR>Subsingleton α<VAR>Zero α<VAR>s : Set α<VAR>h : s.Nonempty<GOAL>s = {0}
<VAR>α : Type u<VAR>Subsingleton α<VAR>One α<VAR>s : Set α<VAR>h : s.Nonempty<GOAL>s = {1}
<VAR>α : Type u<VAR>s t : Set α<GOAL>Disjoint s t ↔ s ∩ t ⊆ ∅
<VAR>α : Type u<VAR>s t : Set α<GOAL>Disjoint s t ↔ s ∩ t = ∅
<VAR>α : Type u<VAR>s t : Set α<GOAL>Disjoint s t → s ∩ t = ∅
<VAR>α : Type u<VAR>s t : Set α<GOAL>Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → a ∉ t
<VAR>α : Type u<VAR>s t : Set α<GOAL>Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ t → a ∉ s
<VAR>α : Type u<VAR>s t : Set α<GOAL>¬Disjoint s t ↔ ∃ x ∈ s, x ∈ t
<VAR>α : Type u<VAR>s t : Set α<GOAL>¬Disjoint s t ↔ (s ∩ t).Nonempty
<VAR>α : Type u<VAR>s t : Set α<GOAL>Disjoint s t ∨ (s ∩ t).Nonempty
<VAR>α : Type u<VAR>s t : Set α<GOAL>Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ t → a ≠ b
<VAR>α : Type u<VAR>s t u : Set α<VAR>h : s ⊆ u<VAR>d : Disjoint u t<GOAL>Disjoint s t
<VAR>α : Type u<VAR>s t u : Set α<VAR>h : t ⊆ u<VAR>d : Disjoint s u<GOAL>Disjoint s t
<VAR>α : Type u<VAR>s₁ s₂ t₁ t₂ : Set α<VAR>hs : s₁ ⊆ s₂<VAR>ht : t₁ ⊆ t₂<VAR>h : Disjoint s₂ t₂<GOAL>Disjoint s₁ t₁
<VAR>α : Type u<VAR>s t u : Set α<GOAL>Disjoint (s ∪ t) u ↔ Disjoint s u ∧ Disjoint t u
<VAR>α : Type u<VAR>s t u : Set α<GOAL>Disjoint s (t ∪ u) ↔ Disjoint s t ∧ Disjoint s u
<VAR>α : Type u<VAR>s : Set α<GOAL>Disjoint s ∅
<VAR>α : Type u<VAR>s : Set α<GOAL>Disjoint ∅ s
<VAR>α : Type u<VAR>s : Set α<GOAL>Disjoint Set.univ s ↔ s = ∅
<VAR>α : Type u<VAR>s : Set α<GOAL>Disjoint s Set.univ ↔ s = ∅
<VAR>α : Type u<VAR>s t : Set α<GOAL>Disjoint (t \ s) s
<VAR>α : Type u<VAR>s t : Set α<GOAL>Disjoint s (t \ s)
<VAR>α : Type u<VAR>s t : Set α<GOAL>Disjoint (s \ t) (s ∩ t)
<VAR>α : Type u<VAR>s t u : Set α<VAR>hts : t ⊆ s<VAR>hut : u ⊆ t<GOAL>s \ t ∪ t \ u = s \ u
<VAR>α : Type u<VAR>s t u : Set α<VAR>h : u ⊆ s<GOAL>s \ (t \ u) = s \ t ∪ u
<VAR>α : Type u<VAR>a : α<VAR>s : Set α<GOAL>Disjoint {a} s ↔ a ∉ s
<VAR>α : Type u<VAR>a : α<VAR>s : Set α<GOAL>Disjoint s {a} ↔ a ∉ s
<VAR>α : Type u<VAR>a b : α<GOAL>Disjoint {a} {b} ↔ a ≠ b
<VAR>α : Type u<VAR>s t u : Set α<GOAL>s ⊆ t \ u ↔ s ⊆ t ∧ Disjoint s u
<VAR>α : Type u<VAR>s t : Set α<GOAL>s ⊂ t ↔ ∃ a ∈ t, s ⊆ t \ {a}
<VAR>α : Type u<VAR>s t u : Set α<GOAL>s ∩ (t \ u) = (s ∩ t) \ (s ∩ u)
<VAR>α : Type u<VAR>s t u : Set α<GOAL>s \ t ∩ u = (s ∩ u) \ (t ∩ u)
<VAR>α : Type u<VAR>s : Set α<GOAL>sᶜ = {x | x ∉ s}
<VAR>α : Type u<VAR>s : Set α<VAR>x : α<VAR>h : x ∉ s<GOAL>x ∈ sᶜ
<VAR>α : Type u_1<VAR>p : α → Prop<GOAL>{a | p a}ᶜ = {a | ¬p a}
<VAR>α : Type u<VAR>s : Set α<VAR>x : α<VAR>h : x ∈ sᶜ<GOAL>x ∉ s
<VAR>α : Type u<VAR>s : Set α<VAR>x : α<GOAL>x ∉ sᶜ ↔ x ∈ s
<VAR>α : Type u<VAR>s : Set α<GOAL>s ∩ sᶜ = ∅
<VAR>α : Type u<VAR>s : Set α<GOAL>sᶜ ∩ s = ∅
<VAR>α : Type u<GOAL>∅ᶜ = Set.univ
<VAR>α : Type u<VAR>s t : Set α<GOAL>(s ∪ t)ᶜ = sᶜ ∩ tᶜ
<VAR>α : Type u<VAR>s t : Set α<GOAL>(s ∩ t)ᶜ = sᶜ ∪ tᶜ
<VAR>α : Type u<GOAL>Set.univᶜ = ∅
<VAR>α : Type u<VAR>s : Set α<GOAL>sᶜ = ∅ ↔ s = Set.univ
<VAR>α : Type u<VAR>s : Set α<GOAL>sᶜ = Set.univ ↔ s = ∅
<VAR>α : Type u<VAR>s : Set α<GOAL>sᶜ ≠ Set.univ ↔ s.Nonempty
<VAR>α : Type u<VAR>s : Set α<GOAL>sᶜ.Nonempty ↔ s ≠ Set.univ
<VAR>α : Type u<VAR>Nontrivial α<VAR>x : α<GOAL>{x}ᶜ.Nonempty