ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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_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_2<VAR>ι : Sort u_4<VAR>Nonempty ι<VAR>s : Set β<GOAL>⋃ x, s = s
<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>Nonempty ι<VAR>s : Set β<GOAL>⋂ x, s = s
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>Nonempty ι<VAR>f : ι → Set α<VAR>s : Set α<VAR>hf : ∀ (i : ι), f i = s<GOAL>⋃ i, f i = s
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>Nonempty ι<VAR>f : ι → Set α<VAR>s : Set α<VAR>hf : ∀ (i : ι), f i = s<GOAL>⋂ i, f i = s
<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>s : ι → Set β<GOAL>(⋃ i, s i)ᶜ = ⋂ i, (s i)ᶜ
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_7<VAR>s : (i : ι) → κ i → Set α<GOAL>(⋃ i, ⋃ j, s i j)ᶜ = ⋂ i, ⋂ j, (s i j)ᶜ
<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>s : ι → Set β<GOAL>(⋂ i, s i)ᶜ = ⋃ i, (s i)ᶜ
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_7<VAR>s : (i : ι) → κ i → Set α<GOAL>(⋂ i, ⋂ j, s i j)ᶜ = ⋃ i, ⋃ j, (s i j)ᶜ
<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>s : ι → Set β<GOAL>⋃ i, s i = (⋂ i, (s i)ᶜ)ᶜ
<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>s : ι → Set β<GOAL>⋂ i, s i = (⋃ i, (s i)ᶜ)ᶜ
<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>s : Set β<VAR>t : ι → Set β<GOAL>s ∩ ⋃ i, t i = ⋃ i, s ∩ t i
<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>s : Set β<VAR>t : ι → Set β<GOAL>(⋃ i, t i) ∩ s = ⋃ i, t i ∩ s
<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>s t : ι → Set β<GOAL>⋃ i, s i ∪ t i = (⋃ i, s i) ∪ ⋃ i, t i
<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>s t : ι → Set β<GOAL>⋂ i, s i ∩ t i = (⋂ i, s i) ∩ ⋂ i, t i
<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>Nonempty ι<VAR>s : Set β<VAR>t : ι → Set β<GOAL>s ∪ ⋃ i, t i = ⋃ i, s ∪ t i
<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>Nonempty ι<VAR>s : Set β<VAR>t : ι → Set β<GOAL>(⋃ i, t i) ∪ s = ⋃ i, t i ∪ s
<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>Nonempty ι<VAR>s : Set β<VAR>t : ι → Set β<GOAL>s ∩ ⋂ i, t i = ⋂ i, s ∩ t i
<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>Nonempty ι<VAR>s : Set β<VAR>t : ι → Set β<GOAL>(⋂ i, t i) ∩ s = ⋂ i, t i ∩ s
<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>s : Set β<VAR>t : ι → Set β<GOAL>s ∪ ⋂ i, t i = ⋂ i, s ∪ t i
<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>s : ι → Set β<VAR>t : Set β<GOAL>(⋂ i, s i) ∪ t = ⋂ i, s i ∪ t
<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>s : Set β<VAR>t : ι → Set β<GOAL>(⋃ i, t i) \ s = ⋃ i, t i \ s
<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>Nonempty ι<VAR>s : Set β<VAR>t : ι → Set β<GOAL>s \ ⋃ i, t i = ⋂ i, s \ t i
<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>s : Set β<VAR>t : ι → Set β<GOAL>s \ ⋂ i, t i = ⋃ i, s \ t i
<VAR>ι : Sort u_11<VAR>α : Type u_12<VAR>s t : ι → Set α<GOAL>⋃ i, s i ∩ t i ⊆ (⋃ i, s i) ∩ ⋃ i, t i
<VAR>ι : Type u_11<VAR>α : Type u_12<VAR>Preorder ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>s t : ι → Set α<VAR>hs : Monotone s<VAR>ht : Monotone t<GOAL>⋃ i, s i ∩ t i = (⋃ i, s i) ∩ ⋃ i, t i
<VAR>ι : Type u_11<VAR>α : Type u_12<VAR>Preorder ι<VAR>IsDirected ι (Function.swap fun x x_1 => x ≤ x_1)<VAR>s t : ι → Set α<VAR>hs : Antitone s<VAR>ht : Antitone t<GOAL>⋃ i, s i ∩ t i = (⋃ i, s i) ∩ ⋃ i, t i
<VAR>ι : Type u_11<VAR>α : Type u_12<VAR>Preorder ι<VAR>IsDirected ι (Function.swap fun x x_1 => x ≤ x_1)<VAR>s t : ι → Set α<VAR>hs : Monotone s<VAR>ht : Monotone t<GOAL>⋂ i, s i ∪ t i = (⋂ i, s i) ∪ ⋂ i, t i
<VAR>ι : Type u_11<VAR>α : Type u_12<VAR>Preorder ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>s t : ι → Set α<VAR>hs : Antitone s<VAR>ht : Antitone t<GOAL>⋂ i, s i ∪ t i = (⋂ i, s i) ∪ ⋂ i, t i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>s : ι → ι' → Set α<GOAL>⋃ j, ⋂ i, s i j ⊆ ⋂ i, ⋃ j, s i j
<VAR>α : Type u_1<VAR>ι : Type u_11<VAR>s : Option ι → Set α<GOAL>⋃ o, s o = s none ∪ ⋃ i, s (some i)
<VAR>α : Type u_1<VAR>ι : Type u_11<VAR>s : Option ι → Set α<GOAL>⋂ o, s o = s none ∩ ⋂ i, s (some i)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>f : (i : ι) → p i → Set α<VAR>g : (i : ι) → ¬p i → Set α<GOAL>(⋃ i, if h : p i then f i h else g i h) = (⋃ i, ⋃ (h : p i), f i h) ∪ ⋃ i, ⋃ (h : ¬p i), g i h
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>f g : ι → Set α<GOAL>(⋃ i, if p i then f i else g i) = (⋃ i, ⋃ (_ : p i), f i) ∪ ⋃ i, ⋃ (_ : ¬p i), g i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>f : (i : ι) → p i → Set α<VAR>g : (i : ι) → ¬p i → Set α<GOAL>(⋂ i, if h : p i then f i h else g i h) = (⋂ i, ⋂ (h : p i), f i h) ∩ ⋂ i, ⋂ (h : ¬p i), g i h
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>f g : ι → Set α<GOAL>(⋂ i, if p i then f i else g i) = (⋂ i, ⋂ (_ : p i), f i) ∩ ⋂ i, ⋂ (_ : ¬p i), g i
<VAR>ι : Type u_11<VAR>α : ι → Type u_12<VAR>v : (i : ι) → Set (α i)<VAR>hv : (Set.univ.pi v).Nonempty<VAR>i : ι<GOAL>(fun x => x i) '' ⋂ k, (fun x => x k) ⁻¹' v k = v i
<VAR>α : Type u_1<VAR>s : False → Set α<GOAL>Set.iInter s = Set.univ
<VAR>α : Type u_1<VAR>s : False → Set α<GOAL>Set.iUnion s = ∅
<VAR>α : Type u_1<VAR>s : True → Set α<GOAL>Set.iInter s = s trivial
<VAR>α : Type u_1<VAR>s : True → Set α<GOAL>Set.iUnion s = s trivial
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>p : ι → Prop<VAR>f : Exists p → Set α<GOAL>⋂ (x : Exists p), f x = ⋂ i, ⋂ (h : p i), f ⋯
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>p : ι → Prop<VAR>f : Exists p → Set α<GOAL>⋃ (x : Exists p), f x = ⋃ i, ⋃ (h : p i), f ⋯
<VAR>α : Type u_1<VAR>ι : Sort u_4<GOAL>⋃ x, ∅ = ∅
<VAR>α : Type u_1<VAR>ι : Sort u_4<GOAL>⋂ x, Set.univ = Set.univ
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>s : ι → Set α<GOAL>⋃ i, s i = ∅ ↔ ∀ (i : ι), s i = ∅
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>s : ι → Set α<GOAL>⋂ i, s i = Set.univ ↔ ∀ (i : ι), s i = Set.univ
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>s : ι → Set α<GOAL>(⋃ i, s i).Nonempty ↔ ∃ i, (s i).Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : Set α<VAR>s : α → Set β<GOAL>(⋃ i ∈ t, s i).Nonempty ↔ ∃ i ∈ t, (s i).Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : s.Nonempty → Set β<GOAL>⋃ (h : s.Nonempty), t h = ⋃ x, ⋃ (h : x ∈ s), t ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>b : β<VAR>s : (x : β) → x = b → Set α<GOAL>⋂ x, ⋂ (h : x = b), s x h = s b ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>b : β<VAR>s : (x : β) → b = x → Set α<GOAL>⋂ x, ⋂ (h : b = x), s x h = s b ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>b : β<VAR>s : (x : β) → x = b → Set α<GOAL>⋃ x, ⋃ (h : x = b), s x h = s b ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>b : β<VAR>s : (x : β) → b = x → Set α<GOAL>⋃ x, ⋃ (h : b = x), s x h = s b ⋯
<VAR>α : Type u_1<VAR>p q : Prop<VAR>s : p ∨ q → Set α<GOAL>⋂ (h : p ∨ q), s h = (⋂ (h : p), s ⋯) ∩ ⋂ (h : q), s ⋯
<VAR>α : Type u_1<VAR>p q : Prop<VAR>s : p ∨ q → Set α<GOAL>⋃ (h : p ∨ q), s h = (⋃ (i : p), s ⋯) ∪ ⋃ (j : q), s ⋯
<VAR>α : Type u_1<VAR>p q : Prop<VAR>s : p ∧ q → Set α<GOAL>⋃ (h : p ∧ q), s h = ⋃ (hp : p), ⋃ (hq : q), s ⋯
<VAR>α : Type u_1<VAR>p q : Prop<VAR>s : p ∧ q → Set α<GOAL>⋂ (h : p ∧ q), s h = ⋂ (hp : p), ⋂ (hq : q), s ⋯
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>s : ι → ι' → Set α<GOAL>⋃ i, ⋃ i', s i i' = ⋃ i', ⋃ i, s i i'
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>s : ι → ι' → Set α<GOAL>⋂ i, ⋂ i', s i i' = ⋂ i', ⋂ i, s i i'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : α → Type u_11<VAR>s : Sigma γ → Set β<GOAL>⋃ ia, s ia = ⋃ i, ⋃ a, s ⟨i, a⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : α → Type u_11<VAR>s : (i : α) → γ i → Set β<GOAL>⋃ i, ⋃ a, s i a = ⋃ ia, s ia.fst ia.snd
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : α → Type u_11<VAR>s : Sigma γ → Set β<GOAL>⋂ ia, s ia = ⋂ i, ⋂ a, s ⟨i, a⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : α → Type u_11<VAR>s : (i : α) → γ i → Set β<GOAL>⋂ i, ⋂ a, s i a = ⋂ ia, s ia.fst ia.snd
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>s : (i₁ : ι) → κ₁ i₁ → (i₂ : ι) → κ₂ i₂ → Set α<GOAL>⋃ i₁, ⋃ j₁, ⋃ i₂, ⋃ j₂, s i₁ j₁ i₂ j₂ = ⋃ i₂, ⋃ j₂, ⋃ i₁, ⋃ j₁, s i₁ j₁ i₂ j₂
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>s : (i₁ : ι) → κ₁ i₁ → (i₂ : ι) → κ₂ i₂ → Set α<GOAL>⋂ i₁, ⋂ j₁, ⋂ i₂, ⋂ j₂, s i₁ j₁ i₂ j₂ = ⋂ i₂, ⋂ j₂, ⋂ i₁, ⋂ j₁, s i₁ j₁ i₂ j₂
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>p : ι → Prop<VAR>q : ι → ι' → Prop<VAR>s : (x : ι) → (y : ι') → p x ∧ q x y → Set α<GOAL>⋃ x, ⋃ y, ⋃ (h : p x ∧ q x y), s x y h = ⋃ x, ⋃ (hx : p x), ⋃ y, ⋃ (hy : q x y), s x y ⋯
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>p : ι' → Prop<VAR>q : ι → ι' → Prop<VAR>s : (x : ι) → (y : ι') → p y ∧ q x y → Set α<GOAL>⋃ x, ⋃ y, ⋃ (h : p y ∧ q x y), s x y h = ⋃ y, ⋃ (hy : p y), ⋃ x, ⋃ (hx : q x y), s x y ⋯
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>p : ι → Prop<VAR>q : ι → ι' → Prop<VAR>s : (x : ι) → (y : ι') → p x ∧ q x y → Set α<GOAL>⋂ x, ⋂ y, ⋂ (h : p x ∧ q x y), s x y h = ⋂ x, ⋂ (hx : p x), ⋂ y, ⋂ (hy : q x y), s x y ⋯
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>p : ι' → Prop<VAR>q : ι → ι' → Prop<VAR>s : (x : ι) → (y : ι') → p y ∧ q x y → Set α<GOAL>⋂ x, ⋂ y, ⋂ (h : p y ∧ q x y), s x y h = ⋂ y, ⋂ (hy : p y), ⋂ x, ⋂ (hx : q x y), s x y ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>b : β<VAR>p : β → Prop<VAR>s : (x : β) → x = b ∨ p x → Set α<GOAL>⋃ x, ⋃ (h : x = b ∨ p x), s x h = s b ⋯ ∪ ⋃ x, ⋃ (h : p x), s x ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>b : β<VAR>p : β → Prop<VAR>s : (x : β) → x = b ∨ p x → Set α<GOAL>⋂ x, ⋂ (h : x = b ∨ p x), s x h = s b ⋯ ∩ ⋂ x, ⋂ (h : p x), s x ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : α → Set β<VAR>x : α<VAR>y : β<VAR>xs : x ∈ s<VAR>ytx : y ∈ t x<GOAL>y ∈ ⋃ x ∈ s, t x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : α → Set β<VAR>y : β<VAR>h : ∀ x ∈ s, y ∈ t x<GOAL>y ∈ ⋂ x ∈ s, t x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>u : α → Set β<VAR>x : α<VAR>xs : x ∈ s<GOAL>u x ⊆ ⋃ x ∈ s, u x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : α → Set β<VAR>x : α<VAR>xs : x ∈ s<GOAL>⋂ x ∈ s, t x ⊆ t x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s s' : Set α<VAR>t : α → Set β<VAR>h : s ⊆ s'<GOAL>⋃ x ∈ s, t x ⊆ ⋃ x ∈ s', t x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s s' : Set α<VAR>t : α → Set β<VAR>h : s' ⊆ s<GOAL>⋂ x ∈ s, t x ⊆ ⋂ x ∈ s', t x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s s' : Set α<VAR>t t' : α → Set β<VAR>hs : s' ⊆ s<VAR>h : ∀ x ∈ s, t x ⊆ t' x<GOAL>⋃ x ∈ s', t x ⊆ ⋃ x ∈ s, t' x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s s' : Set α<VAR>t t' : α → Set β<VAR>hs : s ⊆ s'<VAR>h : ∀ x ∈ s, t x ⊆ t' x<GOAL>⋂ x ∈ s', t x ⊆ ⋂ x ∈ s, t' x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : (x : α) → x ∈ s → Set β<GOAL>⋃ x, ⋃ (h : x ∈ s), t x h = ⋃ x, t ↑x ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : (x : α) → x ∈ s → Set β<GOAL>⋂ x, ⋂ (h : x ∈ s), t x h = ⋂ x, t ↑x ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α → Prop<VAR>s : { x // p x } → Set β<GOAL>⋃ x, s x = ⋃ x, ⋃ (hx : p x), s ⟨x, hx⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α → Prop<VAR>s : { x // p x } → Set β<GOAL>⋂ x, s x = ⋂ x, ⋂ (hx : p x), s ⟨x, hx⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>u : α → Set β<GOAL>⋂ x ∈ ∅, u x = Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>u : α → Set β<GOAL>⋂ x ∈ Set.univ, u x = ⋂ x, u x
<VAR>α : Type u_1<VAR>s : Set α<GOAL>⋃ x ∈ s, s = s
<VAR>α : Type u_1<VAR>s : Set α<GOAL>⋃ (_ : s.Nonempty), s = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>s : α → Set β<GOAL>⋂ x ∈ {a}, s x = s a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>u : α → Set β<GOAL>⋂ x ∈ s ∪ t, u x = (⋂ x ∈ s, u x) ∩ ⋂ x ∈ t, u x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>s : Set α<VAR>t : α → Set β<GOAL>⋂ x ∈ insert a s, t x = t a ∩ ⋂ x ∈ s, t x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a b : α<VAR>s : α → Set β<GOAL>⋂ x ∈ {a, b}, s x = s a ∩ s b
<VAR>ι : Type u_11<VAR>α : Type u_12<VAR>s : Set ι<VAR>hs : s.Nonempty<VAR>f : ι → Set α<VAR>t : Set α<GOAL>⋂ i ∈ s, f i ∩ t = (⋂ i ∈ s, f i) ∩ t
<VAR>ι : Type u_11<VAR>α : Type u_12<VAR>s : Set ι<VAR>hs : s.Nonempty<VAR>f : ι → Set α<VAR>t : Set α<GOAL>⋂ i ∈ s, t ∩ f i = t ∩ ⋂ i ∈ s, f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : α → Set β<GOAL>⋃ x ∈ ∅, s x = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : α → Set β<GOAL>⋃ x ∈ Set.univ, s x = ⋃ x, s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>s : α → Set β<GOAL>⋃ x ∈ {a}, s x = s a
<VAR>α : Type u_1<VAR>s : Set α<GOAL>⋃ x ∈ s, {x} = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>u : α → Set β<GOAL>⋃ x ∈ s ∪ t, u x = (⋃ x ∈ s, u x) ∪ ⋃ x ∈ t, u x
<VAR>α : Type u_11<VAR>β : Type u_12<VAR>s : Set α<VAR>f : ↑s → Set β<GOAL>⋃ i, f i = ⋃ i, ⋃ (h : i ∈ s), f ⟨i, h⟩
<VAR>α : Type u_11<VAR>β : Type u_12<VAR>s : Set α<VAR>f : ↑s → Set β<GOAL>⋂ i, f i = ⋂ i, ⋂ (h : i ∈ s), f ⟨i, h⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>s : Set α<VAR>t : α → Set β<GOAL>⋃ x ∈ insert a s, t x = t a ∪ ⋃ x ∈ s, t x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a b : α<VAR>s : α → Set β<GOAL>⋃ x ∈ {a, b}, s x = s a ∪ s b
<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, s ∩ t i j
<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, s i j ∩ t
<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, s ∪ t i j
<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, s i j ∪ t
<VAR>α : Type u_1<VAR>x : α<VAR>t : Set α<VAR>S : Set (Set α)<VAR>hx : x ∈ t<VAR>ht : t ∈ S<GOAL>x ∈ ⋃₀ S
<VAR>α : Type u_1<VAR>x : α<VAR>t : Set α<VAR>S : Set (Set α)<VAR>hx : x ∉ ⋃₀ S<VAR>ht : t ∈ S<GOAL>x ∉ t
<VAR>α : Type u_1<VAR>S : Set (Set α)<VAR>t : Set α<VAR>tS : t ∈ S<GOAL>⋂₀ S ⊆ t
<VAR>α : Type u_1<VAR>S : Set (Set α)<VAR>t : Set α<VAR>tS : t ∈ S<GOAL>t ⊆ ⋃₀ S
<VAR>α : Type u_1<VAR>s : Set α<VAR>t : Set (Set α)<VAR>u : Set α<VAR>h₁ : s ⊆ u<VAR>h₂ : u ∈ t<GOAL>s ⊆ ⋃₀ t
<VAR>α : Type u_1<VAR>S : Set (Set α)<VAR>t : Set α<VAR>h : ∀ t' ∈ S, t' ⊆ t<GOAL>⋃₀ S ⊆ t
<VAR>α : Type u_1<VAR>s : Set (Set α)<VAR>t : Set α<GOAL>⋃₀ s ⊆ t ↔ ∀ t' ∈ s, t' ⊆ t
<VAR>α : Type u_1<VAR>s : Set (Set α)<VAR>f : Set α → Set α<VAR>hf : ∀ (t : Set α), t ⊆ f t<GOAL>⋃₀ s ⊆ ⋃₀ (f '' s)
<VAR>α : Type u_1<VAR>s : Set (Set α)<VAR>f : Set α → Set α<VAR>hf : ∀ (t : Set α), f t ⊆ t<GOAL>⋃₀ (f '' s) ⊆ ⋃₀ s
<VAR>α : Type u_1<VAR>S : Set (Set α)<VAR>t : Set α<VAR>h : ∀ t' ∈ S, t ⊆ t'<GOAL>t ⊆ ⋂₀ S
<VAR>α : Type u_1<VAR>S : Set (Set α)<VAR>t : Set α<GOAL>t ⊆ ⋂₀ S ↔ ∀ t' ∈ S, t ⊆ t'
<VAR>α : Type u_1<VAR>S T : Set (Set α)<VAR>h : S ⊆ T<GOAL>⋃₀ S ⊆ ⋃₀ T
<VAR>α : Type u_1<VAR>S T : Set (Set α)<VAR>h : S ⊆ T<GOAL>⋂₀ T ⊆ ⋂₀ S
<VAR>α : Type u_1<GOAL>⋃₀ ∅ = ∅
<VAR>α : Type u_1<GOAL>⋂₀ ∅ = Set.univ
<VAR>α : Type u_1<VAR>s : Set α<GOAL>⋃₀ {s} = s
<VAR>α : Type u_1<VAR>s : Set α<GOAL>⋂₀ {s} = s
<VAR>α : Type u_1<VAR>S : Set (Set α)<GOAL>⋃₀ S = ∅ ↔ ∀ s ∈ S, s = ∅
<VAR>α : Type u_1<VAR>S : Set (Set α)<GOAL>⋂₀ S = Set.univ ↔ ∀ s ∈ S, s = Set.univ
<VAR>α : Type u_1<VAR>s : Set (Set α)<VAR>t : Set α<GOAL>s ⊆ 𝒫 t ↔ ⋃₀ s ⊆ t
<VAR>α : Type u_1<GOAL>GaloisConnection (fun x => ⋃₀ x) fun x => 𝒫 x
<VAR>α : Type u_1<VAR>S : Set (Set α)<VAR>h : S ⊆ {∅, Set.univ}<GOAL>⋃₀ S ∈ {∅, Set.univ}
<VAR>α : Type u_1<VAR>S : Set (Set α)<GOAL>(⋃₀ S).Nonempty ↔ ∃ s ∈ S, s.Nonempty
<VAR>α : Type u_1<VAR>s : Set (Set α)<VAR>h : (⋃₀ s).Nonempty<GOAL>s.Nonempty
<VAR>α : Type u_1<VAR>Nonempty α<VAR>s : Set (Set α)<VAR>h : ⋃₀ s = Set.univ<GOAL>s.Nonempty
<VAR>α : Type u_1<VAR>S T : Set (Set α)<GOAL>⋃₀ (S ∪ T) = ⋃₀ S ∪ ⋃₀ T
<VAR>α : Type u_1<VAR>S T : Set (Set α)<GOAL>⋂₀ (S ∪ T) = ⋂₀ S ∩ ⋂₀ T
<VAR>α : Type u_1<VAR>s : Set α<VAR>T : Set (Set α)<GOAL>⋃₀ insert s T = s ∪ ⋃₀ T
<VAR>α : Type u_1<VAR>s : Set α<VAR>T : Set (Set α)<GOAL>⋂₀ insert s T = s ∩ ⋂₀ T
<VAR>α : Type u_1<VAR>s : Set (Set α)<GOAL>⋃₀ (s \ {∅}) = ⋃₀ s
<VAR>α : Type u_1<VAR>s : Set (Set α)<GOAL>⋂₀ (s \ {Set.univ}) = ⋂₀ s
<VAR>α : Type u_1<VAR>s t : Set α<GOAL>⋃₀ {s, t} = s ∪ t
<VAR>α : Type u_1<VAR>s t : Set α<GOAL>⋂₀ {s, t} = s ∩ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → Set β<VAR>s : Set α<GOAL>⋃₀ (f '' s) = ⋃ x ∈ s, f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → Set β<VAR>s : Set α<GOAL>⋂₀ (f '' s) = ⋂ x ∈ s, f x
<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>f : ι → Set β<GOAL>⋃₀ Set.range f = ⋃ x, f x
<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>f : ι → Set β<GOAL>⋂₀ Set.range f = ⋂ x, f x
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>f : ι → Set α<GOAL>⋃ i, f i = Set.univ ↔ ∀ (x : α), ∃ i, x ∈ f i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_7<VAR>s : (i : ι) → κ i → Set α<GOAL>⋃ i, ⋃ j, s i j = Set.univ ↔ ∀ (a : α), ∃ i j, a ∈ s i j
<VAR>α : Type u_1<VAR>c : Set (Set α)<GOAL>⋃₀ c = Set.univ ↔ ∀ (a : α), ∃ b ∈ c, a ∈ b
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>f : ι → Set α<GOAL>⋂ i, f i = ∅ ↔ ∀ (x : α), ∃ i, x ∉ f i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_7<VAR>s : (i : ι) → κ i → Set α<GOAL>⋂ i, ⋂ j, s i j = ∅ ↔ ∀ (a : α), ∃ i j, a ∉ s i j
<VAR>α : Type u_1<VAR>c : Set (Set α)<GOAL>⋂₀ c = ∅ ↔ ∀ (a : α), ∃ b ∈ c, a ∉ b
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>f : ι → Set α<GOAL>(⋂ i, f i).Nonempty ↔ ∃ x, ∀ (i : ι), x ∈ f i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_7<VAR>s : (i : ι) → κ i → Set α<GOAL>(⋂ i, ⋂ j, s i j).Nonempty ↔ ∃ a, ∀ (i : ι) (j : κ i), a ∈ s i j
<VAR>α : Type u_1<VAR>c : Set (Set α)<GOAL>(⋂₀ c).Nonempty ↔ ∃ a, ∀ b ∈ c, a ∈ b
<VAR>α : Type u_1<VAR>S : Set (Set α)<GOAL>(⋃₀ S)ᶜ = ⋂₀ (compl '' S)
<VAR>α : Type u_1<VAR>S : Set (Set α)<GOAL>⋃₀ S = (⋂₀ (compl '' S))ᶜ
<VAR>α : Type u_1<VAR>S : Set (Set α)<GOAL>(⋂₀ S)ᶜ = ⋃₀ (compl '' S)
<VAR>α : Type u_1<VAR>S : Set (Set α)<GOAL>⋂₀ S = (⋃₀ (compl '' S))ᶜ
<VAR>α : Type u_1<VAR>s t : Set α<VAR>S : Set (Set α)<VAR>hs : t ∈ S<VAR>h : s ∩ ⋃₀ S = ∅<GOAL>s ∩ t = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : α → Type u_11<VAR>f : Sigma γ → β<GOAL>Set.range f = ⋃ a, Set.range fun b => f ⟨a, b⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : α → Set β<GOAL>⋃ i, s i = Set.range fun a => ↑a.snd
<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>s : ι → Set β<GOAL>⋃ i, s i = Set.range fun a => ↑a.snd
<VAR>ι : Type u_11<VAR>σ : ι → Type u_12<VAR>s : Set (Sigma σ)<GOAL>⋃ i, Sigma.mk i '' (Sigma.mk i ⁻¹' s) = s
<VAR>α : Type u_1<VAR>X : α → Type u_11<GOAL>Set.univ = ⋃ a, Set.range (Sigma.mk a)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ι₂ : Sort u_6<VAR>s : Set α<VAR>h : ι → ι₂<GOAL>⋃ x, s ⊆ ⋃ x, s
<VAR>α : Type u_11<VAR>β : Type u_12<VAR>f : α → β<GOAL>⋃ x, {f x} = Set.range f
<VAR>α : Type u_11<GOAL>⋃ x, {x} = Set.univ
<VAR>α : Type u_1<VAR>s : Set α<GOAL>⋃ i, {↑i} = s
<VAR>α : Type u_1<VAR>s : Set (Set α)<GOAL>⋃₀ s = ⋃ i ∈ s, i
<VAR>α : Type u_1<VAR>s : Set (Set α)<GOAL>⋂₀ s = ⋂ i ∈ s, i
<VAR>α : Type u_1<VAR>s : Set (Set α)<GOAL>⋃₀ s = ⋃ i, ↑i
<VAR>α : Type u_1<VAR>s : Set (Set α)<GOAL>⋂₀ s = ⋂ i, ↑i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>IsEmpty ι<VAR>s : ι → Set α<GOAL>⋃ i, s i = ∅
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>IsEmpty ι<VAR>s : ι → Set α<GOAL>⋂ i, s i = Set.univ
<VAR>α : Type u_1<VAR>s₁ s₂ : Set α<GOAL>s₁ ∪ s₂ = ⋃ b, bif b then s₁ else s₂
<VAR>α : Type u_1<VAR>s₁ s₂ : Set α<GOAL>s₁ ∩ s₂ = ⋂ b, bif b then s₁ else s₂
<VAR>α : Type u_1<VAR>S T : Set (Set α)<GOAL>⋂₀ S ∪ ⋂₀ T = ⋂ p ∈ S ×ˢ T, p.1 ∪ p.2
<VAR>α : Type u_1<VAR>s t : Set (Set α)<GOAL>⋃₀ s ∩ ⋃₀ t = ⋃ p ∈ s ×ˢ t, p.1 ∩ p.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>s : ι → Set α<VAR>t : α → Set β<GOAL>⋃ x ∈ ⋃ i, s i, t x = ⋃ i, ⋃ x ∈ s i, t x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>s : ι → Set α<VAR>t : α → Set β<GOAL>⋂ x ∈ ⋃ i, s i, t x = ⋂ i, ⋂ x ∈ s i, t x
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>s : ι → Set (Set α)<GOAL>⋃₀ ⋃ i, s i = ⋃ i, ⋃₀ s i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>s : ι → Set (Set α)<GOAL>⋂₀ ⋃ i, s i = ⋂ i, ⋂₀ s i
<VAR>α : Type u_11<VAR>β : Type u_12<VAR>C : Set (Set α)<VAR>f : (s : ↑C) → β → ↑↑s<VAR>hf : ∀ (s : ↑C), Function.Surjective (f s)<GOAL>(⋃ y, Set.range fun s => ↑(f s y)) = ⋃₀ C
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>C : ι → Set α<VAR>f : (x : ι) → β → ↑(C x)<VAR>hf : ∀ (x : ι), Function.Surjective (f x)<GOAL>(⋃ y, Set.range fun x => ↑(f x y)) = ⋃ x, C x
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>s : ι → Set α<VAR>t : Set α<GOAL>t ∪ ⋂ i, s i = ⋂ i, t ∪ s i
<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>β : Type u_2<VAR>S : Set (Set α)<VAR>t : Set β<VAR>f : α → β<GOAL>Set.MapsTo f (⋃₀ S) t ↔ ∀ s ∈ S, Set.MapsTo f s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>s : ι → Set α<VAR>t : Set β<VAR>f : α → β<GOAL>Set.MapsTo f (⋃ i, s i) t ↔ ∀ (i : ι), Set.MapsTo f (s i) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_7<VAR>s : (i : ι) → κ i → Set α<VAR>t : Set β<VAR>f : α → β<GOAL>Set.MapsTo f (⋃ i, ⋃ j, s i j) t ↔ ∀ (i : ι) (j : κ i), Set.MapsTo f (s i j) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>s : ι → Set α<VAR>t : ι → Set β<VAR>f : α → β<VAR>H : ∀ (i : ι), Set.MapsTo f (s i) (t i)<GOAL>Set.MapsTo f (⋃ i, s i) (⋃ i, t i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_7<VAR>s : (i : ι) → κ i → Set α<VAR>t : (i : ι) → κ i → Set β<VAR>f : α → β<VAR>H : ∀ (i : ι) (j : κ i), Set.MapsTo f (s i j) (t i j)<GOAL>Set.MapsTo f (⋃ i, ⋃ j, s i j) (⋃ i, ⋃ j, t i j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>T : Set (Set β)<VAR>f : α → β<GOAL>Set.MapsTo f s (⋂₀ T) ↔ ∀ t ∈ T, Set.MapsTo f s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>s : Set α<VAR>t : ι → Set β<VAR>f : α → β<GOAL>Set.MapsTo f s (⋂ i, t i) ↔ ∀ (i : ι), Set.MapsTo f s (t i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_7<VAR>s : Set α<VAR>t : (i : ι) → κ i → Set β<VAR>f : α → β<GOAL>Set.MapsTo f s (⋂ i, ⋂ j, t i j) ↔ ∀ (i : ι) (j : κ i), Set.MapsTo f s (t i j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>s : ι → Set α<VAR>t : ι → Set β<VAR>f : α → β<VAR>H : ∀ (i : ι), Set.MapsTo f (s i) (t i)<GOAL>Set.MapsTo f (⋂ i, s i) (⋂ i, t i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_7<VAR>s : (i : ι) → κ i → Set α<VAR>t : (i : ι) → κ i → Set β<VAR>f : α → β<VAR>H : ∀ (i : ι) (j : κ i), Set.MapsTo f (s i j) (t i j)<GOAL>Set.MapsTo f (⋂ i, ⋂ j, s i j) (⋂ i, ⋂ j, t i j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>s : ι → Set α<VAR>f : α → β<GOAL>f '' ⋂ i, s i ⊆ ⋂ i, f '' s i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_7<VAR>s : (i : ι) → κ i → Set α<VAR>f : α → β<GOAL>f '' ⋂ i, ⋂ j, s i j ⊆ ⋂ i, ⋂ j, f '' s i j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>S : Set (Set α)<VAR>f : α → β<GOAL>f '' ⋂₀ S ⊆ ⋂ s ∈ S, f '' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>f : α → β<VAR>U : ι → Set β<VAR>hU : Set.iUnion U = Set.univ<GOAL>Function.Injective f ↔ ∀ (i : ι), Function.Injective ((U i).restrictPreimage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>f : α → β<VAR>U : ι → Set β<VAR>hU : Set.iUnion U = Set.univ<GOAL>Function.Surjective f ↔ ∀ (i : ι), Function.Surjective ((U i).restrictPreimage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>f : α → β<VAR>U : ι → Set β<VAR>hU : Set.iUnion U = Set.univ<GOAL>Function.Bijective f ↔ ∀ (i : ι), Function.Bijective ((U i).restrictPreimage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>Nonempty ι<VAR>s : ι → Set α<VAR>f : α → β<VAR>h : Set.InjOn f (⋃ i, s i)<GOAL>f '' ⋂ i, s i = ⋂ i, f '' s i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>p : ι → Prop<VAR>s : (i : ι) → p i → Set α<VAR>hp : ∃ i, p i<VAR>f : α → β<VAR>h : Set.InjOn f (⋃ i, ⋃ (hi : p i), s i hi)<GOAL>f '' ⋂ i, ⋂ (hi : p i), s i hi = ⋂ i, ⋂ (hi : p i), f '' s i hi
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>f : α → β<VAR>hf : Function.Bijective f<VAR>s : ι → Set α<GOAL>f '' ⋂ i, s i = ⋂ i, f '' s i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_7<VAR>f : α → β<VAR>hf : Function.Bijective f<VAR>s : (i : ι) → κ i → Set α<GOAL>f '' ⋂ i, ⋂ j, s i j = ⋂ i, ⋂ j, f '' s i j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>s : ι → Set α<VAR>hs : Directed (fun x x_1 => x ⊆ x_1) s<VAR>f : α → β<VAR>hf : ∀ (i : ι), Set.InjOn f (s i)<GOAL>Set.InjOn f (⋃ i, s i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>T : Set (Set β)<VAR>f : α → β<VAR>H : ∀ t ∈ T, Set.SurjOn f s t<GOAL>Set.SurjOn f s (⋃₀ T)