ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>a x : α<GOAL>x ∈ {a}ᶜ ↔ x ≠ a
<VAR>α : Type u<VAR>a : α<GOAL>{a}ᶜ = {x | x ≠ a}
<VAR>α : Type u<VAR>a : α<GOAL>{x | x ≠ a}ᶜ = {a}
<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 ∪ sᶜ = Set.univ
<VAR>α : Type u<VAR>s : Set α<GOAL>sᶜ ∪ s = Set.univ
<VAR>α : Type u<VAR>s t : Set α<GOAL>sᶜ ⊆ t ↔ tᶜ ⊆ s
<VAR>α : Type u<VAR>s t : Set α<GOAL>s ⊆ tᶜ ↔ t ⊆ sᶜ
<VAR>α : Type u<VAR>s t : Set α<GOAL>sᶜ ⊆ tᶜ ↔ t ⊆ s
<VAR>α : Type u<VAR>s t : Set α<VAR>h : t ⊆ s<GOAL>sᶜ ⊆ tᶜ
<VAR>α : Type u<VAR>s t : Set α<GOAL>s ⊆ tᶜ ↔ Disjoint t s
<VAR>α : Type u<VAR>s t : Set α<GOAL>s ⊆ tᶜ ↔ Disjoint s t
<VAR>α : Type u<VAR>s t : Set α<GOAL>Disjoint sᶜ t ↔ t ⊆ s
<VAR>α : Type u<VAR>s t : Set α<GOAL>Disjoint s tᶜ ↔ s ⊆ t
<VAR>α : Type u<VAR>s t u : Set α<GOAL>s ⊆ t ∪ uᶜ ↔ s ∩ u ⊆ t
<VAR>α : Type u<VAR>s t : Set α<GOAL>sᶜ ⊆ t ↔ s ∪ t = Set.univ
<VAR>α : Type u<VAR>a : α<VAR>s : Set α<GOAL>s ⊆ {a}ᶜ ↔ a ∉ s
<VAR>α : Type u<VAR>a b c : Set α<GOAL>a ∩ b ⊆ c ↔ a ⊆ bᶜ ∪ c
<VAR>α : Type u<VAR>s t : Set α<GOAL>(s ∩ tᶜ).Nonempty ↔ ¬s ⊆ t
<VAR>α : Type u<VAR>s t : Set α<VAR>x : α<VAR>hx : x ∈ t<GOAL>x ∉ s \ t
<VAR>α : Type u<VAR>s t : Set α<VAR>x : α<VAR>h : x ∈ s \ t<GOAL>x ∈ s
<VAR>α : Type u<VAR>s t : Set α<VAR>x : α<VAR>h : x ∈ s \ t<GOAL>x ∉ t
<VAR>α : Type u<VAR>s t : Set α<GOAL>s \ t = tᶜ ∩ s
<VAR>α : Type u<VAR>s t : Set α<GOAL>(s \ t).Nonempty ↔ ¬s ⊆ t
<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 u : Set α<VAR>h₁ : s ⊆ t<VAR>h₂ : t ⊆ u<GOAL>t ∪ u \ s = u
<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>(s ∪ t) \ s = t
<VAR>α : Type u<VAR>s t : Set α<VAR>h : s ∩ t ⊆ ∅<GOAL>(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>(s ∪ t) \ t = s \ t
<VAR>α : Type u<VAR>s t u : Set α<GOAL>(s ∪ t) \ u = s \ u ∪ t \ u
<VAR>α : Type u<VAR>a b c : Set α<GOAL>(a ∩ b) \ c = a ∩ (b \ c)
<VAR>α : Type u<VAR>a b : Set α<GOAL>a ∩ (b \ a) = ∅
<VAR>α : Type u<VAR>s t : Set α<GOAL>s ∩ t ∪ s \ t = s
<VAR>α : Type u<VAR>s t : Set α<GOAL>s \ t ∪ s ∩ t = s
<VAR>α : Type u<VAR>s t : Set α<GOAL>s ∩ t ∪ s ∩ tᶜ = s
<VAR>α : Type u<VAR>s₁ s₂ t₁ t₂ : Set α<GOAL>s₁ ⊆ s₂ → t₂ ⊆ t₁ → s₁ \ t₁ ⊆ s₂ \ t₂
<VAR>α : Type u<VAR>s₁ s₂ t : Set α<VAR>h : s₁ ⊆ s₂<GOAL>s₁ \ t ⊆ s₂ \ t
<VAR>α : Type u<VAR>s t u : Set α<VAR>h : t ⊆ u<GOAL>s \ u ⊆ s \ t
<VAR>α : Type u<VAR>s : Set α<GOAL>sᶜ = Set.univ \ s
<VAR>α : Type u<VAR>s : Set α<GOAL>∅ \ s = ∅
<VAR>α : Type u<VAR>s t : Set α<GOAL>s \ t = ∅ ↔ s ⊆ t
<VAR>α : Type u<VAR>s : Set α<GOAL>s \ ∅ = s
<VAR>α : Type u<VAR>s : Set α<GOAL>s \ Set.univ = ∅
<VAR>α : Type u<VAR>s t u : Set α<GOAL>(s \ t) \ u = s \ (t ∪ u)
<VAR>α : Type u<VAR>s t u : Set α<GOAL>(s \ t) \ u = (s \ u) \ t
<VAR>α : Type u<VAR>s t u : Set α<GOAL>s \ t ⊆ u ↔ s ⊆ t ∪ u
<VAR>α : Type u<VAR>s t : Set α<GOAL>s ⊆ s \ t ∪ t
<VAR>α : Type u<VAR>s t : Set α<VAR>h : t ⊆ s<GOAL>s \ t ∪ t = s
<VAR>α : Type u<VAR>x : α<VAR>s t : Set α<GOAL>s \ {x} ⊆ t ↔ s ⊆ insert x t
<VAR>α : Type u<VAR>x : α<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>hx : x ∉ s<GOAL>s ⊆ t \ {x}
<VAR>α : Type u<VAR>x : α<VAR>s : Set α<GOAL>s ⊆ insert x (s \ {x})
<VAR>α : Type u<VAR>s t u : Set α<GOAL>s \ t ⊆ u ↔ s \ u ⊆ t
<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 ∩ (s \ u) = s \ (t ∪ u)
<VAR>α : Type u<VAR>s t : Set α<GOAL>s \ tᶜ = s ∩ t
<VAR>α : Type u<VAR>s t u : Set α<GOAL>s \ (t \ u) = s \ t ∪ s ∩ u
<VAR>α : Type u<VAR>a : α<VAR>t : Set α<VAR>s : Set α<VAR>h : a ∈ t<GOAL>insert a s \ t = s \ t
<VAR>α : Type u<VAR>a : α<VAR>t : Set α<VAR>s : Set α<VAR>h : a ∉ t<GOAL>insert a s \ t = insert a (s \ t)
<VAR>α : Type u<VAR>a : α<VAR>s : Set α<VAR>h : a ∉ s<GOAL>insert a s \ {a} = s
<VAR>α : Type u<VAR>a : α<VAR>s : Set α<VAR>h : a ∉ s<GOAL>insert a s \ s = {a}
<VAR>α : Type u<VAR>a : α<VAR>s t : Set α<VAR>h : a ∈ s<GOAL>s ∩ insert a t = insert a (s ∩ t)
<VAR>α : Type u<VAR>a : α<VAR>s t : Set α<VAR>h : a ∈ t<GOAL>insert a s ∩ t = insert a (s ∩ t)
<VAR>α : Type u<VAR>a : α<VAR>s t : Set α<VAR>h : a ∉ s<GOAL>s ∩ insert a t = s ∩ t
<VAR>α : Type u<VAR>a : α<VAR>s t : Set α<VAR>h : a ∉ t<GOAL>insert a s ∩ t = s ∩ 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 = s ∪ t
<VAR>α : Type u<VAR>a b : Set α<GOAL>b \ a ∩ a = ∅
<VAR>α : Type u<VAR>s t : Set α<GOAL>s \ (t ∩ s) = s \ t
<VAR>α : Type u<VAR>s t : Set α<GOAL>s \ (s ∩ t) = s \ t
<VAR>α : Type u<VAR>a : α<VAR>s : Set α<VAR>h : a ∉ s<GOAL>s \ {a} = s
<VAR>α : Type u<VAR>s : Set α<VAR>a : α<GOAL>s \ {a} ⊂ s ↔ a ∈ s
<VAR>α : Type u<VAR>a : α<VAR>s : Set α<GOAL>insert a (s \ {a}) = insert a s
<VAR>α : Type u<VAR>a b : α<VAR>hab : a ≠ b<VAR>s : Set α<GOAL>insert a (s \ {b}) = insert a s \ {b}
<VAR>α : Type u<VAR>s : Set α<GOAL>s \ s = ∅
<VAR>α : Type u<VAR>s t : Set α<GOAL>s \ (s \ t) = s ∩ t
<VAR>α : Type u<VAR>s t : Set α<VAR>h : s ⊆ t<GOAL>t \ (t \ s) = s
<VAR>α : Type u<VAR>x y : α<VAR>s : Set α<GOAL>x ∈ s \ {y} ↔ x ∈ s ∧ x ≠ y
<VAR>α : Type u<VAR>s : Set α<VAR>t : Set (Set α)<GOAL>s ∈ t \ {∅} ↔ s ∈ t ∧ s.Nonempty
<VAR>α : Type u<VAR>s t : Set α<VAR>x : α<GOAL>s ⊆ insert x t ↔ s ⊆ t ∨ x ∈ s ∧ s \ {x} ⊆ t
<VAR>α : Type u<VAR>s t : Set α<GOAL>s ∪ t = s \ t ∪ t \ s ∪ s ∩ t
<VAR>α : Type u<VAR>a : α<GOAL>{a, a} = {a}
<VAR>α : Type u<VAR>a b : α<GOAL>{a, b} = {b, a}
<VAR>α : Type u<VAR>x y z w : α<GOAL>{x, y} = {z, w} ↔ x = z ∧ y = w ∨ x = w ∧ y = z
<VAR>α : Type u<VAR>a b : α<VAR>hne : a ≠ b<GOAL>{a, b} \ {a} = {b}
<VAR>α : Type u<VAR>a b : α<VAR>hne : a ≠ b<GOAL>{a, b} \ {b} = {a}
<VAR>α : Type u<VAR>a b : α<VAR>s : Set α<GOAL>{a, b} ⊆ s ↔ a ∈ s ∧ b ∈ s
<VAR>α : Type u<VAR>a b : α<VAR>s : Set α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>{a, b} ⊆ s
<VAR>α : Type u<VAR>a b : α<VAR>s : Set α<GOAL>s ⊆ {a, b} ↔ ∀ x ∈ s, x = a ∨ x = b
<VAR>α : Type u<VAR>s : Set α<VAR>x y : α<GOAL>s ⊆ {x, y} ↔ s = ∅ ∨ s = {x} ∨ s = {y} ∨ s = {x, y}
<VAR>α : Type u<VAR>a b : α<VAR>s : Set α<VAR>hs : s.Nonempty<GOAL>s ⊆ {a, b} ↔ s = {a} ∨ s = {b} ∨ s = {a, b}
<VAR>α : Type u<VAR>a : α<VAR>s t : Set α<GOAL>a ∈ symmDiff s t ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s
<VAR>α : Type u<VAR>s t : Set α<GOAL>symmDiff s t = s \ t ∪ t \ s
<VAR>α : Type u<VAR>s t : Set α<GOAL>symmDiff s t ⊆ s ∪ t
<VAR>α : Type u<VAR>s t : Set α<GOAL>symmDiff s t = ∅ ↔ s = t
<VAR>α : Type u<VAR>s t : Set α<GOAL>(symmDiff s t).Nonempty ↔ s ≠ t
<VAR>α : Type u<VAR>s t u : Set α<GOAL>s ∩ symmDiff t u = symmDiff (s ∩ t) (s ∩ u)
<VAR>α : Type u<VAR>s t u : Set α<GOAL>symmDiff s t ∩ u = symmDiff (s ∩ u) (t ∩ u)
<VAR>α : Type u<VAR>s t u : Set α<VAR>h : Disjoint s t<GOAL>u ⊆ symmDiff s u ∪ symmDiff t u
<VAR>α : Type u<VAR>s t u : Set α<VAR>h : Disjoint t u<GOAL>s ⊆ symmDiff s t ∪ symmDiff s u
<VAR>α : Type u<VAR>x s : Set α<VAR>h : x ⊆ s<GOAL>x ∈ 𝒫 s
<VAR>α : Type u<VAR>x s : Set α<VAR>h : x ∈ 𝒫 s<GOAL>x ⊆ s
<VAR>α : Type u<VAR>x s : Set α<GOAL>x ∈ 𝒫 s ↔ x ⊆ s
<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).Nonempty
<VAR>α : Type u<GOAL>𝒫∅ = {∅}
<VAR>α : Type u<GOAL>𝒫 Set.univ = Set.univ
<VAR>α : Type u<VAR>x : α<GOAL>𝒫{x} = {∅, {x}}
<VAR>α : Type u<VAR>p : Prop<VAR>Decidable p<VAR>s : p → Set α<VAR>t : ¬p → Set α<VAR>x : α<GOAL>(x ∈ if h : p then s h else t h) ↔ (∀ (h : p), x ∈ s h) ∧ ∀ (h : ¬p), x ∈ t h
<VAR>α : Type u<VAR>p : Prop<VAR>Decidable p<VAR>t : p → Set α<VAR>x : α<GOAL>(x ∈ if h : p then t h else Set.univ) ↔ ∀ (h : p), x ∈ t h
<VAR>α : Type u<VAR>p : Prop<VAR>Decidable p<VAR>t : Set α<VAR>x : α<GOAL>(x ∈ if p then t else Set.univ) ↔ p → x ∈ t
<VAR>α : Type u<VAR>p : Prop<VAR>Decidable p<VAR>t : ¬p → Set α<VAR>x : α<GOAL>(x ∈ if h : p then Set.univ else t h) ↔ ∀ (h : ¬p), x ∈ t h
<VAR>α : Type u<VAR>p : Prop<VAR>Decidable p<VAR>t : Set α<VAR>x : α<GOAL>(x ∈ if p then Set.univ else t) ↔ ¬p → x ∈ t
<VAR>α : Type u<VAR>p : Prop<VAR>Decidable p<VAR>t : p → Set α<VAR>x : α<GOAL>(x ∈ if h : p then t h else ∅) ↔ ∃ (h : p), x ∈ t h
<VAR>α : Type u<VAR>p : Prop<VAR>Decidable p<VAR>t : Set α<VAR>x : α<GOAL>(x ∈ if p then t else ∅) ↔ p ∧ x ∈ t
<VAR>α : Type u<VAR>p : Prop<VAR>Decidable p<VAR>t : ¬p → Set α<VAR>x : α<GOAL>(x ∈ if h : p then ∅ else t h) ↔ ∃ (h : ¬p), x ∈ t h
<VAR>α : Type u<VAR>p : Prop<VAR>Decidable p<VAR>t : Set α<VAR>x : α<GOAL>(x ∈ if p then ∅ else t) ↔ ¬p ∧ x ∈ t
<VAR>α : Type u<VAR>t s s' : Set α<GOAL>t.ite s s' ∩ t = s ∩ t
<VAR>α : Type u<VAR>t s s' : Set α<GOAL>tᶜ.ite s s' = t.ite s' s
<VAR>α : Type u<VAR>t s s' : Set α<GOAL>t.ite s s' ∩ tᶜ = s' ∩ tᶜ
<VAR>α : Type u<VAR>t s s' : Set α<GOAL>t.ite s s' \ t = s' \ t
<VAR>α : Type u<VAR>t s : Set α<GOAL>t.ite s s = s
<VAR>α : Type u<VAR>s t : Set α<GOAL>s.ite s t = s ∪ t
<VAR>α : Type u<VAR>s t : Set α<GOAL>s.ite t s = t ∩ s
<VAR>α : Type u<VAR>s s' : Set α<GOAL>∅.ite s s' = s'
<VAR>α : Type u<VAR>s s' : Set α<GOAL>Set.univ.ite s s' = s
<VAR>α : Type u<VAR>t s : Set α<GOAL>t.ite ∅ s = s \ t
<VAR>α : Type u<VAR>t s : Set α<GOAL>t.ite s ∅ = s ∩ t
<VAR>α : Type u<VAR>t : Set α<VAR>s₁ s₁' s₂ s₂' : Set α<VAR>h : s₁ ⊆ s₂<VAR>h' : s₁' ⊆ s₂'<GOAL>t.ite s₁ s₁' ⊆ t.ite s₂ s₂'
<VAR>α : Type u<VAR>t s s' : Set α<GOAL>t.ite s s' ⊆ s ∪ s'
<VAR>α : Type u<VAR>t s s' : Set α<GOAL>s ∩ s' ⊆ t.ite s s'
<VAR>α : Type u<VAR>t s₁ s₂ s₁' s₂' : Set α<GOAL>t.ite (s₁ ∩ s₂) (s₁' ∩ s₂') = t.ite s₁ s₁' ∩ t.ite s₂ s₂'
<VAR>α : Type u<VAR>t s₁ s₂ s : Set α<GOAL>t.ite (s₁ ∩ s) (s₂ ∩ s) = t.ite s₁ s₂ ∩ s
<VAR>α : Type u<VAR>t : Set α<VAR>s₁ s₂ s : Set α<VAR>h : s₁ ∩ s = s₂ ∩ s<GOAL>t.ite s₁ s₂ ∩ s = s₁ ∩ s
<VAR>α : Type u<VAR>t s s' u : Set α<GOAL>u ⊆ t.ite s s' ↔ u ∩ t ⊆ s ∧ u \ t ⊆ s'
<VAR>α : Type u<VAR>t : Set α<VAR>s₁ s₂ : Set α<VAR>h : s₁ ⊆ s₂<GOAL>t.ite s₁ s₂ = s₁ ∪ s₂ \ t
<VAR>α : Type u<VAR>t : Set α<VAR>s₁ s₂ : Set α<VAR>h : s₂ ⊆ s₁<GOAL>t.ite s₁ s₂ = s₁ ∩ t ∪ s₂
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<GOAL>MonotoneOn f s ↔ Monotone fun a => f ↑a
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<GOAL>AntitoneOn f s ↔ Antitone fun a => f ↑a
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<GOAL>StrictMonoOn f s ↔ StrictMono fun a => f ↑a
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<GOAL>StrictAntiOn f s ↔ StrictAnti fun a => f ↑a
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>LinearOrder α<VAR>LinearOrder β<VAR>f : α → β<GOAL>¬MonotoneOn f s ∧ ¬AntitoneOn f s ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>LinearOrder α<VAR>LinearOrder β<VAR>f : α → β<GOAL>¬MonotoneOn f s ∧ ¬AntitoneOn f s ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a < b ∧ b < c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f : Set α → Set β<VAR>hf : Function.Injective f<VAR>h2 : f ∅ = ∅<VAR>s : Set α<GOAL>(f s).Nonempty ↔ s.Nonempty
<VAR>α : Type u_1<VAR>s : Set α<VAR>x : ↑s<GOAL>Set.inclusion ⋯ x = x
<VAR>α : Type u_1<VAR>s : Set α<VAR>h : s ⊆ s<GOAL>Set.inclusion h = id
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>a : α<VAR>ha : a ∈ s<GOAL>Set.inclusion h ⟨a, ha⟩ = ⟨a, ⋯⟩
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>x : ↑t<VAR>m : ↑x ∈ s<GOAL>Set.inclusion h ⟨↑x, m⟩ = x
<VAR>α : Type u_1<VAR>s t u : Set α<VAR>hst : s ⊆ t<VAR>htu : t ⊆ u<VAR>x : ↑s<GOAL>Set.inclusion htu (Set.inclusion hst x) = Set.inclusion ⋯ x
<VAR>α : Type u_2<VAR>s t u : Set α<VAR>hst : s ⊆ t<VAR>htu : t ⊆ u<GOAL>Set.inclusion htu ∘ Set.inclusion hst = Set.inclusion ⋯
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>x : ↑s<GOAL>↑(Set.inclusion h x) = ↑x
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : s ⊆ t<GOAL>Subtype.val ∘ Set.inclusion h = Subtype.val
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : s ⊆ t<GOAL>Function.Injective (Set.inclusion h)
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>x y : ↑s<GOAL>Set.inclusion h x = Set.inclusion h y ↔ x = y
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>h_surj : Function.Surjective (Set.inclusion h)<GOAL>s = t
<VAR>α : Type u_1<VAR>Preorder α<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>x y : ↑s<GOAL>Set.inclusion h x ≤ Set.inclusion h y ↔ x ≤ y
<VAR>α : Type u_1<VAR>Preorder α<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>x y : ↑s<GOAL>Set.inclusion h x < Set.inclusion h y ↔ x < y
<VAR>α : Type u_1<VAR>Subsingleton α<VAR>s : Set α<GOAL>s.Nonempty → s = Set.univ
<VAR>α : Type u_1<VAR>Subsingleton α<VAR>p : Set α → Prop<VAR>h0 : p ∅<VAR>h1 : p Set.univ<VAR>s : Set α<GOAL>p s
<VAR>α : Type u_2<VAR>Subsingleton α<VAR>s : Set α<VAR>x : α<GOAL>x ∈ s ↔ s.Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>f g : β → Set α<VAR>hf : Monotone f<VAR>hg : Monotone g<GOAL>Monotone fun x => f x ∩ g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>f g : β → Set α<VAR>s : Set β<VAR>hf : MonotoneOn f s<VAR>hg : MonotoneOn g s<GOAL>MonotoneOn (fun x => f x ∩ g x) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>f g : β → Set α<VAR>hf : Antitone f<VAR>hg : Antitone g<GOAL>Antitone fun x => f x ∩ g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>f g : β → Set α<VAR>s : Set β<VAR>hf : AntitoneOn f s<VAR>hg : AntitoneOn g s<GOAL>AntitoneOn (fun x => f x ∩ g x) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>f g : β → Set α<VAR>hf : Monotone f<VAR>hg : Monotone g<GOAL>Monotone fun x => f x ∪ g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>f g : β → Set α<VAR>s : Set β<VAR>hf : MonotoneOn f s<VAR>hg : MonotoneOn g s<GOAL>MonotoneOn (fun x => f x ∪ g x) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>f g : β → Set α<VAR>hf : Antitone f<VAR>hg : Antitone g<GOAL>Antitone fun x => f x ∪ g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>f g : β → Set α<VAR>s : Set β<VAR>hf : AntitoneOn f s<VAR>hg : AntitoneOn g s<GOAL>AntitoneOn (fun x => f x ∪ g x) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>p : α → β → Prop<VAR>hp : ∀ (b : β), Monotone fun a => p a b<GOAL>Monotone fun a => {b | p a b}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>p : α → β → Prop<VAR>hp : ∀ (b : β), Antitone fun a => p a b<GOAL>Antitone fun a => {b | p a b}
<VAR>α : Type u_1<VAR>P : α → Prop<GOAL>Antitone fun s => ∀ x ∈ s, P x
<VAR>α : Type u_1<VAR>s t u : Set α<VAR>hs : Disjoint s u<VAR>ht : Disjoint t u<GOAL>Disjoint (s ∪ t) u
<VAR>α : Type u_1<VAR>s t u : Set α<VAR>ht : Disjoint s t<VAR>hu : Disjoint s u<GOAL>Disjoint s (t ∪ u)
<VAR>α : Type u_1<VAR>s t : Set α<VAR>u : Set α<VAR>h : Disjoint s t<GOAL>Disjoint (s ∩ u) t
<VAR>α : Type u_1<VAR>s t : Set α<VAR>u : Set α<VAR>h : Disjoint s t<GOAL>Disjoint (u ∩ s) t
<VAR>α : Type u_1<VAR>s t : Set α<VAR>u : Set α<VAR>h : Disjoint s t<GOAL>Disjoint s (t ∩ u)
<VAR>α : Type u_1<VAR>s t : Set α<VAR>u : Set α<VAR>h : Disjoint s t<GOAL>Disjoint s (u ∩ t)
<VAR>α : Type u_1<VAR>s t u : Set α<VAR>h : s ⊆ t ∪ u<VAR>hac : Disjoint s u<GOAL>s ⊆ t
<VAR>α : Type u_1<VAR>s t u : Set α<VAR>h : s ⊆ t ∪ u<VAR>hab : Disjoint s t<GOAL>s ⊆ u
<VAR>p : Prop<GOAL>{p}ᶜ = {¬p}
<VAR>α : Type u_1<VAR>s : Set α<VAR>f : α → ℚ≥0<VAR>a : α<GOAL>↑(s.indicator f a) = s.indicator (fun x => ↑(f x)) a
<VAR>q : ℚ<GOAL>q⁻¹.toNNRat = q.toNNRat⁻¹
<VAR>q : ℚ≥0<GOAL>↑q.num / ↑q.den = q
<VAR>l : List ℚ≥0<GOAL>↑l.sum = (List.map NNRat.cast l).sum
<VAR>l : List ℚ≥0<GOAL>↑l.prod = (List.map NNRat.cast l).prod
<VAR>s : Multiset ℚ≥0<GOAL>↑s.sum = (Multiset.map NNRat.cast s).sum
<VAR>s : Multiset ℚ≥0<GOAL>↑s.prod = (Multiset.map NNRat.cast s).prod
<VAR>α : Type u_2<VAR>s : Finset α<VAR>f : α → ℚ≥0<GOAL>↑(∑ a ∈ s, f a) = ∑ a ∈ s, ↑(f a)
<VAR>α : Type u_2<VAR>s : Finset α<VAR>f : α → ℚ<VAR>hf : ∀ a ∈ s, 0 ≤ f a<GOAL>(∑ a ∈ s, f a).toNNRat = ∑ a ∈ s, (f a).toNNRat
<VAR>α : Type u_2<VAR>s : Finset α<VAR>f : α → ℚ≥0<GOAL>↑(∏ a ∈ s, f a) = ∏ a ∈ s, ↑(f a)
<VAR>α : Type u_2<VAR>s : Finset α<VAR>f : α → ℚ<VAR>hf : ∀ a ∈ s, 0 ≤ f a<GOAL>(∏ a ∈ s, f a).toNNRat = ∏ a ∈ s, (f a).toNNRat
<VAR>c : Prop<VAR>Decidable c<VAR>a b : Ordering<GOAL>((if c then a else b) = Ordering.lt) = if c then a = Ordering.lt else b = Ordering.lt
<VAR>c : Prop<VAR>Decidable c<VAR>a b : Ordering<GOAL>((if c then a else b) = Ordering.eq) = if c then a = Ordering.eq else b = Ordering.eq
<VAR>c : Prop<VAR>Decidable c<VAR>a b : Ordering<GOAL>((if c then a else b) = Ordering.gt) = if c then a = Ordering.gt else b = Ordering.gt
<VAR>α : Type u<VAR>lt : α → α → Prop<VAR>DecidableRel lt<VAR>a b : α<GOAL>(cmpUsing lt a b = Ordering.lt) = lt a b
<VAR>α : Type u<VAR>lt : α → α → Prop<VAR>DecidableRel lt<VAR>IsStrictOrder α lt<VAR>a b : α<GOAL>cmpUsing lt a b = Ordering.gt ↔ lt b a
<VAR>α : Type u<VAR>lt : α → α → Prop<VAR>DecidableRel lt<VAR>a b : α<GOAL>cmpUsing lt a b = Ordering.eq ↔ ¬lt a b ∧ ¬lt b a
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s t : Set α<VAR>c : α<GOAL>c ∈ s ⊻ t ↔ ∃ a ∈ s, ∃ b ∈ t, a ⊔ b = c
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s t : Set α<VAR>a b : α<GOAL>a ∈ s → b ∈ t → a ⊔ b ∈ s ⊻ t
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s₁ s₂ t₁ t₂ : Set α<GOAL>s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ ⊻ t₁ ⊆ s₂ ⊻ t₂
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s t₁ t₂ : Set α<GOAL>t₁ ⊆ t₂ → s ⊻ t₁ ⊆ s ⊻ t₂
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s₁ s₂ t : Set α<GOAL>s₁ ⊆ s₂ → s₁ ⊻ t ⊆ s₂ ⊻ t
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s t : Set α<VAR>b : α<GOAL>b ∈ t → (fun a => a ⊔ b) '' s ⊆ s ⊻ t
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s t : Set α<VAR>a : α<GOAL>a ∈ s → (fun x x_1 => x ⊔ x_1) a '' t ⊆ s ⊻ t
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s t : Set α<VAR>p : α → Prop<GOAL>(∀ c ∈ s ⊻ t, p c) ↔ ∀ a ∈ s, ∀ b ∈ t, p (a ⊔ b)
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s t u : Set α<GOAL>s ⊻ t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a ⊔ b ∈ u
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s t : Set α<GOAL>(s ⊻ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s t : Set α<GOAL>s.Nonempty → t.Nonempty → (s ⊻ t).Nonempty
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s t : Set α<GOAL>(s ⊻ t).Nonempty → s.Nonempty
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s t : Set α<GOAL>(s ⊻ t).Nonempty → t.Nonempty
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>t : Set α<GOAL>∅ ⊻ t = ∅
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s : Set α<GOAL>s ⊻ ∅ = ∅
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s t : Set α<GOAL>s ⊻ t = ∅ ↔ s = ∅ ∨ t = ∅
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>t : Set α<VAR>a : α<GOAL>{a} ⊻ t = (fun b => a ⊔ b) '' t
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s : Set α<VAR>b : α<GOAL>s ⊻ {b} = (fun a => a ⊔ b) '' s
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>a b : α<GOAL>{a} ⊻ {b} = {a ⊔ b}
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s₁ s₂ t : Set α<GOAL>(s₁ ∪ s₂) ⊻ t = s₁ ⊻ t ∪ s₂ ⊻ t
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s t₁ t₂ : Set α<GOAL>s ⊻ (t₁ ∪ t₂) = s ⊻ t₁ ∪ s ⊻ t₂
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s₁ s₂ t : Set α<GOAL>(s₁ ∩ s₂) ⊻ t ⊆ s₁ ⊻ t ∩ s₂ ⊻ t
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s t₁ t₂ : Set α<GOAL>s ⊻ (t₁ ∩ t₂) ⊆ s ⊻ t₁ ∩ s ⊻ t₂
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>SemilatticeSup β<VAR>FunLike F α β<VAR>SupHomClass F α β<VAR>f : F<VAR>s t : Set α<GOAL>⇑f '' (s ⊻ t) = ⇑f '' s ⊻ ⇑f '' t
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s : Set α<GOAL>s ⊆ s ⊻ s
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s : Set α<GOAL>s ⊻ s ⊆ s ↔ SupClosed s
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s : Set α<GOAL>s ⊻ s = s ↔ SupClosed s
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s t : Set α<VAR>a : α<GOAL>{b | b ∈ s ⊻ t ∧ b ≤ a} = {b | b ∈ s ∧ b ≤ a} ⊻ {b | b ∈ t ∧ b ≤ a}
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s t : Set α<GOAL>⋃ a ∈ s, (fun x x_1 => x ⊔ x_1) a '' t = s ⊻ t
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s t : Set α<GOAL>⋃ b ∈ t, (fun x => x ⊔ b) '' s = s ⊻ t
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s t : Set α<GOAL>Set.image2 (fun x x_1 => x ⊔ x_1) s t = s ⊻ t
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s t u : Set α<GOAL>s ⊻ t ⊻ u = s ⊻ (t ⊻ u)
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s t : Set α<GOAL>s ⊻ t = t ⊻ s
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s t u : Set α<GOAL>s ⊻ (t ⊻ u) = t ⊻ (s ⊻ u)
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s t u : Set α<GOAL>s ⊻ t ⊻ u = s ⊻ u ⊻ t
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s t u v : Set α<GOAL>s ⊻ t ⊻ (u ⊻ v) = s ⊻ u ⊻ (t ⊻ v)
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s t : Set α<VAR>c : α<GOAL>c ∈ s ⊼ t ↔ ∃ a ∈ s, ∃ b ∈ t, a ⊓ b = c
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s t : Set α<VAR>a b : α<GOAL>a ∈ s → b ∈ t → a ⊓ b ∈ s ⊼ t
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s₁ s₂ t₁ t₂ : Set α<GOAL>s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ ⊼ t₁ ⊆ s₂ ⊼ t₂
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s t₁ t₂ : Set α<GOAL>t₁ ⊆ t₂ → s ⊼ t₁ ⊆ s ⊼ t₂
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s₁ s₂ t : Set α<GOAL>s₁ ⊆ s₂ → s₁ ⊼ t ⊆ s₂ ⊼ t
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s t : Set α<VAR>b : α<GOAL>b ∈ t → (fun a => a ⊓ b) '' s ⊆ s ⊼ t
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s t : Set α<VAR>a : α<GOAL>a ∈ s → (fun x => a ⊓ x) '' t ⊆ s ⊼ t
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s t : Set α<VAR>p : α → Prop<GOAL>(∀ c ∈ s ⊼ t, p c) ↔ ∀ a ∈ s, ∀ b ∈ t, p (a ⊓ b)
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s t u : Set α<GOAL>s ⊼ t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a ⊓ b ∈ u
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s t : Set α<GOAL>(s ⊼ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s t : Set α<GOAL>s.Nonempty → t.Nonempty → (s ⊼ t).Nonempty
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s t : Set α<GOAL>(s ⊼ t).Nonempty → s.Nonempty
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s t : Set α<GOAL>(s ⊼ t).Nonempty → t.Nonempty
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>t : Set α<GOAL>∅ ⊼ t = ∅
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s : Set α<GOAL>s ⊼ ∅ = ∅
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s t : Set α<GOAL>s ⊼ t = ∅ ↔ s = ∅ ∨ t = ∅
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>t : Set α<VAR>a : α<GOAL>{a} ⊼ t = (fun b => a ⊓ b) '' t
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s : Set α<VAR>b : α<GOAL>s ⊼ {b} = (fun a => a ⊓ b) '' s
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>a b : α<GOAL>{a} ⊼ {b} = {a ⊓ b}
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s₁ s₂ t : Set α<GOAL>(s₁ ∪ s₂) ⊼ t = s₁ ⊼ t ∪ s₂ ⊼ t
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s t₁ t₂ : Set α<GOAL>s ⊼ (t₁ ∪ t₂) = s ⊼ t₁ ∪ s ⊼ t₂
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s₁ s₂ t : Set α<GOAL>(s₁ ∩ s₂) ⊼ t ⊆ s₁ ⊼ t ∩ s₂ ⊼ t
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s t₁ t₂ : Set α<GOAL>s ⊼ (t₁ ∩ t₂) ⊆ s ⊼ t₁ ∩ s ⊼ t₂
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>SemilatticeInf β<VAR>FunLike F α β<VAR>InfHomClass F α β<VAR>f : F<VAR>s t : Set α<GOAL>⇑f '' (s ⊼ t) = ⇑f '' s ⊼ ⇑f '' t
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s : Set α<GOAL>s ⊆ s ⊼ s
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s : Set α<GOAL>s ⊼ s ⊆ s ↔ InfClosed s
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s : Set α<GOAL>s ⊼ s = s ↔ InfClosed s
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s t : Set α<VAR>a : α<GOAL>{b | b ∈ s ⊼ t ∧ a ≤ b} = {b | b ∈ s ∧ a ≤ b} ⊼ {b | b ∈ t ∧ a ≤ b}
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s t : Set α<GOAL>⋃ a ∈ s, (fun x => a ⊓ x) '' t = s ⊼ t
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s t : Set α<GOAL>⋃ b ∈ t, (fun x => x ⊓ b) '' s = s ⊼ t
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s t : Set α<GOAL>Set.image2 (fun x x_1 => x ⊓ x_1) s t = s ⊼ t
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s t u : Set α<GOAL>s ⊼ t ⊼ u = s ⊼ (t ⊼ u)
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s t : Set α<GOAL>s ⊼ t = t ⊼ s
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s t u : Set α<GOAL>s ⊼ (t ⊼ u) = t ⊼ (s ⊼ u)
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s t u : Set α<GOAL>s ⊼ t ⊼ u = s ⊼ u ⊼ t
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s t u v : Set α<GOAL>s ⊼ t ⊼ (u ⊼ v) = s ⊼ u ⊼ (t ⊼ v)
<VAR>α : Type u_2<VAR>DistribLattice α<VAR>s t u : Set α<GOAL>s ⊻ t ⊼ u ⊆ (s ⊻ t) ⊼ (s ⊻ u)
<VAR>α : Type u_2<VAR>DistribLattice α<VAR>s t u : Set α<GOAL>t ⊼ u ⊻ s ⊆ (t ⊻ s) ⊼ (u ⊻ s)
<VAR>α : Type u_2<VAR>DistribLattice α<VAR>s t u : Set α<GOAL>s ⊼ (t ⊻ u) ⊆ s ⊼ t ⊻ s ⊼ u
<VAR>α : Type u_2<VAR>DistribLattice α<VAR>s t u : Set α<GOAL>(t ⊻ u) ⊼ s ⊆ t ⊼ s ⊻ u ⊼ s
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s t : Set α<GOAL>upperClosure (s ⊻ t) = upperClosure s ⊔ upperClosure t