ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>s : Set α<VAR>t : ι → Set β<VAR>f : α → β<VAR>H : ∀ (i : ι), Set.SurjOn f s (t i)<GOAL>Set.SurjOn f s (⋃ i, t i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>s : ι → Set α<VAR>t : ι → Set β<VAR>f : α → β<VAR>H : ∀ (i : ι), Set.SurjOn f (s i) (t i)<GOAL>Set.SurjOn 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 : Set α<VAR>t : (i : ι) → κ i → Set β<VAR>f : α → β<VAR>H : ∀ (i : ι) (j : κ i), Set.SurjOn f s (t i j)<GOAL>Set.SurjOn f s (⋃ i, ⋃ j, t i j)
<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.SurjOn f (s i j) (t i j)<GOAL>Set.SurjOn f (⋃ i, ⋃ j, s i j) (⋃ i, ⋃ j, t i j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>Nonempty ι<VAR>s : ι → Set α<VAR>t : Set β<VAR>f : α → β<VAR>H : ∀ (i : ι), Set.SurjOn f (s i) t<VAR>Hinj : Set.InjOn f (⋃ i, s i)<GOAL>Set.SurjOn f (⋂ i, s i) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>Nonempty ι<VAR>s : ι → Set α<VAR>t : ι → Set β<VAR>f : α → β<VAR>H : ∀ (i : ι), Set.SurjOn f (s i) (t i)<VAR>Hinj : Set.InjOn f (⋃ i, s i)<GOAL>Set.SurjOn f (⋂ i, s i) (⋂ i, t i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>s : ι → Set α<VAR>t : ι → Set β<VAR>f : α → β<VAR>H : ∀ (i : ι), Set.BijOn f (s i) (t i)<VAR>Hinj : Set.InjOn f (⋃ i, s i)<GOAL>Set.BijOn f (⋃ i, s i) (⋃ i, t i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>hi : Nonempty ι<VAR>s : ι → Set α<VAR>t : ι → Set β<VAR>f : α → β<VAR>H : ∀ (i : ι), Set.BijOn f (s i) (t i)<VAR>Hinj : Set.InjOn f (⋃ i, s i)<GOAL>Set.BijOn f (⋂ i, s i) (⋂ i, t i)
<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>t : ι → Set β<VAR>f : α → β<VAR>H : ∀ (i : ι), Set.BijOn f (s i) (t i)<GOAL>Set.BijOn f (⋃ i, s i) (⋃ i, t i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>Nonempty ι<VAR>s : ι → Set α<VAR>hs : Directed (fun x x_1 => x ⊆ x_1) s<VAR>t : ι → Set β<VAR>f : α → β<VAR>H : ∀ (i : ι), Set.BijOn f (s i) (t i)<GOAL>Set.BijOn f (⋂ i, s i) (⋂ i, t i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>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>s : (i : ι) → κ i → Set α<GOAL>f '' ⋃ i, ⋃ j, s i j = ⋃ i, ⋃ j, f '' s i j
<VAR>α : Type u_1<VAR>p : α → Prop<GOAL>Set.univ = ⋃ x, ⋃ (h : p x), {⟨x, h⟩}
<VAR>α : Type u_1<VAR>ι : Sort u_11<VAR>f : ι → α<GOAL>Set.range f = ⋃ i, {f i}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<GOAL>f '' s = ⋃ i ∈ s, {f i}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>f : ι → α<VAR>g : α → Set β<GOAL>⋃ x ∈ Set.range f, g x = ⋃ y, g (f y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>f : ι → α<VAR>g : α → Set β<GOAL>⋃ x, ⋃ y, ⋃ (_ : f y = x), g x = ⋃ y, g (f y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>f : ι → α<VAR>g : α → Set β<GOAL>⋂ x ∈ Set.range f, g x = ⋂ y, g (f y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>f : ι → α<VAR>g : α → Set β<GOAL>⋂ x, ⋂ y, ⋂ (_ : f y = x), g x = ⋂ y, g (f y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Set γ<VAR>f : γ → α<VAR>g : α → Set β<GOAL>⋃ x ∈ f '' s, g x = ⋃ y ∈ s, g (f y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Set γ<VAR>f : γ → α<VAR>g : α → Set β<GOAL>⋂ x ∈ f '' s, g x = ⋂ y ∈ s, g (f y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>Monotone (Set.preimage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>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>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>f : α → β<VAR>s : Set (Set α)<GOAL>f '' ⋃₀ s = ⋃₀ (Set.image f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set (Set β)<GOAL>f ⁻¹' ⋃₀ s = ⋃ t ∈ s, f ⁻¹' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>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>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>f : α → β<VAR>s : Set (Set β)<GOAL>f ⁻¹' ⋂₀ s = ⋂ t ∈ s, f ⁻¹' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set β<GOAL>⋃ y ∈ s, f ⁻¹' {y} = f ⁻¹' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>⋃ y ∈ Set.range f, f ⁻¹' {y} = Set.univ
<VAR>α : Type u_1<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_1<VAR>β : Type u_2<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>β : Type u_2<VAR>s : Set α<VAR>C : Set (Set β)<GOAL>s ×ˢ ⋃₀ C = ⋃₀ ((fun t => s ×ˢ t) '' C)
<VAR>α : Type u_1<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_1<VAR>β : Type u_2<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>β : Type u_2<VAR>C : Set (Set α)<VAR>t : Set β<GOAL>⋃₀ C ×ˢ t = ⋃₀ ((fun s => s ×ˢ t) '' C)
<VAR>ι : Type u_11<VAR>ι' : Type u_12<VAR>α : Type u_13<VAR>β : Type u_14<VAR>s : ι → Set α<VAR>t : ι' → Set β<GOAL>⋃ x, s x.1 ×ˢ t x.2 = (⋃ i, s i) ×ˢ ⋃ i, t i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : β × γ → Set α<GOAL>⋃ x, f x = ⋃ i, ⋃ j, f (i, j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>SemilatticeSup α<VAR>s : α → Set β<VAR>t : α → Set γ<VAR>hs : Monotone s<VAR>ht : Monotone t<GOAL>⋃ x, s x ×ˢ t x = (⋃ x, s x) ×ˢ ⋃ x, t x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>S : Set (Set α)<VAR>T : Set (Set β)<GOAL>⋂₀ S ×ˢ ⋂₀ T ⊆ ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>S : Set (Set α)<VAR>T : Set (Set β)<VAR>hS : S.Nonempty<VAR>hT : T.Nonempty<GOAL>⋂₀ S ×ˢ ⋂₀ T = ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>S : Set (Set α)<VAR>hS : S.Nonempty<VAR>t : Set β<GOAL>⋂₀ S ×ˢ t = ⋂ s ∈ S, s ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>T : Set (Set β)<VAR>hT : T.Nonempty<VAR>s : Set α<GOAL>s ×ˢ ⋂₀ T = ⋂ t ∈ T, s ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>s : Set α<VAR>t : ι → Set β<VAR>hι : Nonempty ι<GOAL>s ×ˢ ⋂ i, t i = ⋂ i, s ×ˢ t i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<GOAL>Set.image2 f s t = ⋃ i ∈ s, ⋃ j ∈ t, {f i j}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<GOAL>⋃ a ∈ s, f a '' t = Set.image2 f s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<GOAL>⋃ b ∈ t, (fun x => f x b) '' s = Set.image2 f s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f : α → β → γ<VAR>s : ι → Set α<VAR>t : Set β<GOAL>Set.image2 f (⋃ i, s i) t = ⋃ i, Set.image2 f (s i) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : ι → Set β<GOAL>Set.image2 f s (⋃ i, t i) = ⋃ i, Set.image2 f s (t i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_7<VAR>f : α → β → γ<VAR>s : (i : ι) → κ i → Set α<VAR>t : Set β<GOAL>Set.image2 f (⋃ i, ⋃ j, s i j) t = ⋃ i, ⋃ j, Set.image2 f (s i j) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_7<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : (i : ι) → κ i → Set β<GOAL>Set.image2 f s (⋃ i, ⋃ j, t i j) = ⋃ i, ⋃ j, Set.image2 f s (t i j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f : α → β → γ<VAR>s : ι → Set α<VAR>t : Set β<GOAL>Set.image2 f (⋂ i, s i) t ⊆ ⋂ i, Set.image2 f (s i) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : ι → Set β<GOAL>Set.image2 f s (⋂ i, t i) ⊆ ⋂ i, Set.image2 f s (t i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_7<VAR>f : α → β → γ<VAR>s : (i : ι) → κ i → Set α<VAR>t : Set β<GOAL>Set.image2 f (⋂ i, ⋂ j, s i j) t ⊆ ⋂ i, ⋂ j, Set.image2 f (s i j) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_7<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : (i : ι) → κ i → Set β<GOAL>Set.image2 f s (⋂ i, ⋂ j, t i j) ⊆ ⋂ i, ⋂ j, Set.image2 f s (t i j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<GOAL>s ×ˢ t = ⋃ a ∈ s, (fun b => (a, b)) '' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<GOAL>s ×ˢ t = ⋃ b ∈ t, (fun a => (a, b)) '' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set (α → β)<VAR>t : Set α<GOAL>s.seq t = ⋃ f ∈ s, f '' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set (α → β)<VAR>t : Set α<VAR>u : Set β<GOAL>s.seq t ⊆ u ↔ ∀ f ∈ s, ∀ a ∈ t, f a ∈ u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s₀ s₁ : Set (α → β)<VAR>t₀ t₁ : Set α<VAR>hs : s₀ ⊆ s₁<VAR>ht : t₀ ⊆ t₁<GOAL>s₀.seq t₀ ⊆ s₁.seq t₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>t : Set α<GOAL>{f}.seq t = f '' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set (α → β)<VAR>a : α<GOAL>s.seq {a} = (fun f => f a) '' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Set (β → γ)<VAR>t : Set (α → β)<VAR>u : Set α<GOAL>s.seq (t.seq u) = (((fun x x_1 => x ∘ x_1) '' s).seq t).seq u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : β → γ<VAR>s : Set (α → β)<VAR>t : Set α<GOAL>f '' s.seq t = ((fun x => f ∘ x) '' s).seq t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<GOAL>s ×ˢ t = (Prod.mk '' s).seq t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<GOAL>(Prod.mk '' s).seq t = ((fun b a => (a, b)) '' t).seq s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<GOAL>Set.image2 f s t = (f '' s).seq t
<VAR>α : Type u_1<VAR>π : α → Type u_11<VAR>i : Set α<VAR>s : (a : α) → Set (π a)<GOAL>i.pi s = ⋂ a ∈ i, Function.eval a ⁻¹' s a
<VAR>α : Type u_1<VAR>π : α → Type u_11<VAR>t : (i : α) → Set (π i)<GOAL>Set.univ.pi t = ⋂ i, Function.eval i ⁻¹' t i
<VAR>α : Type u_1<VAR>π : α → Type u_11<VAR>i : Set α<VAR>s t : (a : α) → Set (π a)<GOAL>i.pi s \ i.pi t ⊆ ⋃ a ∈ i, Function.eval a ⁻¹' (s a \ t a)
<VAR>α : Type u_1<VAR>π : α → Type u_11<VAR>ι : α → Type u_12<VAR>t : (a : α) → ι a → Set (π a)<GOAL>(⋃ x, Set.univ.pi fun a => t a (x a)) = Set.univ.pi fun a => ⋃ j, t a j
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>r : α → α → Prop<VAR>f : ι → Set α<VAR>hd : Directed (fun x x_1 => x ⊆ x_1) f<VAR>h : ∀ (x : ι), DirectedOn r (f x)<GOAL>DirectedOn r (⋃ x, f x)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>S : Set (Set α)<VAR>hd : DirectedOn (fun x x_1 => x ⊆ x_1) S<VAR>h : ∀ x ∈ S, DirectedOn r x<GOAL>DirectedOn r (⋃₀ S)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ι₂ : Sort u_6<VAR>f : ι → ι₂<VAR>hf : Function.Surjective f<VAR>g : ι₂ → Set α<GOAL>⋃ x, g (f x) = ⋃ y, g y
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ι₂ : Sort u_6<VAR>f : ι → ι₂<VAR>hf : Function.Surjective f<VAR>g : ι₂ → Set α<GOAL>⋂ x, g (f x) = ⋂ y, g y
<VAR>α : Type u_1<VAR>t : Set α<VAR>ι : Sort u_11<VAR>s : ι → Set α<GOAL>Disjoint (⋃ i, s i) t ↔ ∀ (i : ι), Disjoint (s i) t
<VAR>α : Type u_1<VAR>t : Set α<VAR>ι : Sort u_11<VAR>s : ι → Set α<GOAL>Disjoint t (⋃ i, s i) ↔ ∀ (i : ι), Disjoint t (s i)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_7<VAR>s : (i : ι) → κ i → Set α<VAR>t : Set α<GOAL>Disjoint (⋃ i, ⋃ j, s i j) t ↔ ∀ (i : ι) (j : κ i), Disjoint (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>Disjoint s (⋃ i, ⋃ j, t i j) ↔ ∀ (i : ι) (j : κ i), Disjoint s (t i j)
<VAR>α : Type u_1<VAR>S : Set (Set α)<VAR>t : Set α<GOAL>Disjoint (⋃₀ S) t ↔ ∀ s ∈ S, Disjoint s t
<VAR>α : Type u_1<VAR>s : Set α<VAR>S : Set (Set α)<GOAL>Disjoint s (⋃₀ S) ↔ ∀ t ∈ S, Disjoint s t
<VAR>α : Type u_1<VAR>ι : Type u_11<VAR>Es : ι → Set α<VAR>Es_union : ⋃ i, Es i = Set.univ<VAR>Es_disj : Pairwise fun i j => Disjoint (Es i) (Es j)<VAR>I : Set ι<GOAL>(⋃ i ∈ I, Es i)ᶜ = ⋃ i ∈ Iᶜ, Es i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>Preorder α<VAR>f : ι → α<GOAL>(⋂ i, Set.Iic (f i)).Nonempty ↔ BddBelow (Set.range f)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>Preorder α<VAR>f : ι → α<GOAL>(⋂ i, Set.Ici (f i)).Nonempty ↔ BddAbove (Set.range f)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>CompleteLattice α<VAR>f : ι → α<GOAL>Set.Ici (⨆ i, f i) = ⋂ i, Set.Ici (f i)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>CompleteLattice α<VAR>f : ι → α<GOAL>Set.Iic (⨅ i, f i) = ⋂ i, Set.Iic (f i)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_7<VAR>CompleteLattice α<VAR>f : (i : ι) → κ i → α<GOAL>Set.Ici (⨆ i, ⨆ j, f i j) = ⋂ i, ⋂ j, Set.Ici (f i j)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_7<VAR>CompleteLattice α<VAR>f : (i : ι) → κ i → α<GOAL>Set.Iic (⨅ i, ⨅ j, f i j) = ⋂ i, ⋂ j, Set.Iic (f i j)
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>s : Set α<GOAL>Set.Ici (sSup s) = ⋂ a ∈ s, Set.Ici a
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>s : Set α<GOAL>Set.Iic (sInf s) = ⋂ a ∈ s, Set.Iic a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : α → Set β<VAR>s₁ s₂ : Set α<GOAL>(⋃ x ∈ s₁, t x) \ ⋃ x ∈ s₂, t x ⊆ ⋃ x ∈ s₁ \ s₂, t x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : α → Set β<GOAL>Function.Surjective (Set.sigmaToiUnion t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : α → Set β<VAR>h : Pairwise fun i j => Disjoint (t i) (t j)<GOAL>Function.Injective (Set.sigmaToiUnion t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : α → Set β<VAR>h : Pairwise fun i j => Disjoint (t i) (t j)<GOAL>Function.Bijective (Set.sigmaToiUnion t)
<VAR>α : Type u_1<VAR>u : ℕ → Set α<VAR>n : ℕ<GOAL>⋃ i, ⋃ (_ : i ≥ n), u i = ⋃ i, u (i + n)
<VAR>α : Type u_1<VAR>u : ℕ → Set α<VAR>n : ℕ<GOAL>⋂ i, ⋂ (_ : i ≥ n), u i = ⋂ i, u (i + n)
<VAR>α : Type u_1<VAR>f : ℕ → Set α<VAR>hf : Monotone f<VAR>k : ℕ<GOAL>⋃ n, f (n + k) = ⋃ n, f n
<VAR>α : Type u_1<VAR>f : ℕ → Set α<VAR>hf : Antitone f<VAR>k : ℕ<GOAL>⋂ n, f (n + k) = ⋂ n, f n
<VAR>α : Type u_1<VAR>f : ℕ → Set α<VAR>k : ℕ<GOAL>⋃ n, ⋂ i, ⋂ (_ : i ≥ n), f (i + k) = ⋃ n, ⋂ i, ⋂ (_ : i ≥ n), f i
<VAR>α : Type u_1<VAR>u : ℕ → Set α<GOAL>u 0 ∪ ⋃ i, u (i + 1) = ⋃ i, u i
<VAR>α : Type u_1<VAR>u : ℕ → Set α<GOAL>u 0 ∩ ⋂ i, u (i + 1) = ⋂ i, u i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>CompleteLattice β<VAR>s : ι → Set α<VAR>f : α → β<GOAL>⨆ a ∈ ⋃ i, s i, f a = ⨆ i, ⨆ a ∈ s i, f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>CompleteLattice β<VAR>s : ι → Set α<VAR>f : α → β<GOAL>⨅ a ∈ ⋃ i, s i, f a = ⨅ i, ⨅ a ∈ s i, f a
<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>CompleteLattice β<VAR>t : ι → Set β<GOAL>sSup (⋃ i, t i) = ⨆ i, sSup (t i)
<VAR>β : Type u_2<VAR>CompleteLattice β<VAR>s : Set (Set β)<GOAL>sSup (⋃₀ s) = ⨆ t ∈ s, sSup t
<VAR>β : Type u_2<VAR>CompleteLattice β<VAR>s : Set (Set β)<GOAL>sInf (⋃₀ s) = ⨅ t ∈ s, sInf t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice β<VAR>S : Set (Set α)<VAR>f : α → β<GOAL>⨆ x ∈ ⋃₀ S, f x = ⨆ s ∈ S, ⨆ x ∈ s, f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice β<VAR>S : Set (Set α)<VAR>f : α → β<GOAL>⨅ x ∈ ⋃₀ S, f x = ⨅ s ∈ S, ⨅ x ∈ s, f x
<VAR>α : Type u_1<VAR>S : Set (Set α)<VAR>p : α → Prop<GOAL>(∀ x ∈ ⋃₀ S, p x) ↔ ∀ s ∈ S, ∀ x ∈ s, p x
<VAR>α : Type u_1<VAR>S : Set (Set α)<VAR>p : α → Prop<GOAL>(∃ x ∈ ⋃₀ S, p x) ↔ ∃ s ∈ S, ∃ x ∈ s, p x
<VAR>α : Type u_1<VAR>L : List (List α)<GOAL>(↑(List.map Multiset.ofList L)).join = ↑L.join
<VAR>α : Type u_1<GOAL>Multiset.join 0 = 0
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>S : Multiset (Multiset α)<GOAL>(s ::ₘ S).join = s + S.join
<VAR>α : Type u_1<VAR>S T : Multiset (Multiset α)<GOAL>(S + T).join = S.join + T.join
<VAR>α : Type u_1<VAR>a : Multiset α<GOAL>{a}.join = a
<VAR>α : Type u_1<VAR>a : α<VAR>S : Multiset (Multiset α)<GOAL>a ∈ S.join ↔ ∃ s ∈ S, a ∈ s
<VAR>α : Type u_1<VAR>S : Multiset (Multiset α)<GOAL>Multiset.card S.join = (Multiset.map (⇑Multiset.card) S).sum
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → β<VAR>S : Multiset (Multiset α)<GOAL>Multiset.map f S.join = (Multiset.map (Multiset.map f) S).join
<VAR>α : Type u_1<VAR>AddCommMonoid α<VAR>S : Multiset (Multiset α)<GOAL>S.join.sum = (Multiset.map Multiset.sum S).sum
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>S : Multiset (Multiset α)<GOAL>S.join.prod = (Multiset.map Multiset.prod S).prod
<VAR>α : Type u_1<VAR>β : Type v<VAR>r : α → β → Prop<VAR>s : Multiset (Multiset α)<VAR>t : Multiset (Multiset β)<VAR>h : Multiset.Rel (Multiset.Rel r) s t<GOAL>Multiset.Rel r s.join t.join
<VAR>α : Type u_1<VAR>β : Type v<VAR>l : List α<VAR>f : α → List β<GOAL>((↑l).bind fun a => ↑(f a)) = ↑(l.bind f)
<VAR>α : Type u_1<VAR>β : Type v<VAR>f : α → Multiset β<GOAL>Multiset.bind 0 f = 0
<VAR>α : Type u_1<VAR>β : Type v<VAR>a : α<VAR>s : Multiset α<VAR>f : α → Multiset β<GOAL>(a ::ₘ s).bind f = f a + s.bind f
<VAR>α : Type u_1<VAR>β : Type v<VAR>a : α<VAR>f : α → Multiset β<GOAL>{a}.bind f = f a
<VAR>α : Type u_1<VAR>β : Type v<VAR>s t : Multiset α<VAR>f : α → Multiset β<GOAL>(s + t).bind f = s.bind f + t.bind f
<VAR>α : Type u_1<VAR>β : Type v<VAR>s : Multiset α<GOAL>(s.bind fun x => 0) = 0
<VAR>α : Type u_1<VAR>β : Type v<VAR>s : Multiset α<VAR>f g : α → Multiset β<GOAL>(s.bind fun a => f a + g a) = s.bind f + s.bind g
<VAR>α : Type u_1<VAR>β : Type v<VAR>s : Multiset α<VAR>f : α → β<VAR>g : α → Multiset β<GOAL>(s.bind fun a => f a ::ₘ g a) = Multiset.map f s + s.bind g
<VAR>α : Type u_1<VAR>β : Type v<VAR>s : Multiset α<VAR>f : α → β<GOAL>(s.bind fun x => {f x}) = Multiset.map f s
<VAR>α : Type u_1<VAR>β : Type v<VAR>b : β<VAR>s : Multiset α<VAR>f : α → Multiset β<GOAL>b ∈ s.bind f ↔ ∃ a ∈ s, b ∈ f a
<VAR>α : Type u_1<VAR>β : Type v<VAR>s : Multiset α<VAR>f : α → Multiset β<GOAL>Multiset.card (s.bind f) = (Multiset.map (⇑Multiset.card ∘ f) s).sum
<VAR>α : Type u_1<VAR>β : Type v<VAR>f g : α → Multiset β<VAR>m : Multiset α<GOAL>(∀ a ∈ m, f a = g a) → m.bind f = m.bind g
<VAR>α : Type u_1<VAR>β β' : Type v<VAR>m : Multiset α<VAR>f : α → Multiset β<VAR>f' : α → Multiset β'<VAR>h : β = β'<VAR>hf : ∀ a ∈ m, HEq (f a) (f' a)<GOAL>HEq (m.bind f) (m.bind f')
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>m : Multiset α<VAR>n : α → Multiset β<VAR>f : β → γ<GOAL>Multiset.map f (m.bind n) = m.bind fun a => Multiset.map f (n a)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>m : Multiset α<VAR>n : β → Multiset γ<VAR>f : α → β<GOAL>(Multiset.map f m).bind n = m.bind fun a => n (f a)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>s : Multiset α<VAR>f : α → Multiset β<VAR>g : β → Multiset γ<GOAL>(s.bind f).bind g = s.bind fun a => (f a).bind g
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>m : Multiset α<VAR>n : Multiset β<VAR>f : α → β → Multiset γ<GOAL>(m.bind fun a => n.bind fun b => f a b) = n.bind fun b => m.bind fun a => f a b
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>m : Multiset α<VAR>n : Multiset β<VAR>f : α → β → γ<GOAL>(m.bind fun a => Multiset.map (fun b => f a b) n) = n.bind fun b => Multiset.map (fun a => f a b) m
<VAR>α : Type u_1<VAR>β : Type v<VAR>AddCommMonoid β<VAR>s : Multiset α<VAR>t : α → Multiset β<GOAL>(s.bind t).sum = (Multiset.map (fun a => (t a).sum) s).sum
<VAR>α : Type u_1<VAR>β : Type v<VAR>CommMonoid β<VAR>s : Multiset α<VAR>t : α → Multiset β<GOAL>(s.bind t).prod = (Multiset.map (fun a => (t a).prod) s).prod
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>r : α → β → Prop<VAR>p : γ → δ → Prop<VAR>s : Multiset α<VAR>t : Multiset β<VAR>f : α → Multiset γ<VAR>g : β → Multiset δ<VAR>h : (r ⇒ Multiset.Rel p) f g<VAR>hst : Multiset.Rel r s t<GOAL>Multiset.Rel p (s.bind f) (t.bind g)
<VAR>α : Type u_1<VAR>β : Type v<VAR>DecidableEq α<VAR>m : Multiset β<VAR>f : β → Multiset α<VAR>a : α<GOAL>Multiset.count a (Multiset.map f m).sum = (Multiset.map (fun b => Multiset.count a (f b)) m).sum
<VAR>α : Type u_1<VAR>β : Type v<VAR>DecidableEq α<VAR>m : Multiset β<VAR>f : β → Multiset α<VAR>a : α<GOAL>Multiset.count a (m.bind f) = (Multiset.map (fun b => Multiset.count a (f b)) m).sum
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>f : α → Multiset β<VAR>S : Multiset α<VAR>x : α<VAR>hx : x ∈ S<GOAL>f x ≤ S.bind f
<VAR>α : Type u_1<VAR>β : Type v<VAR>s : Multiset α<VAR>f : α → Multiset β<GOAL>(s.attach.bind fun i => f ↑i) = s.bind f
<VAR>α : Type u_1<VAR>β : Type v<VAR>s : Multiset α<VAR>f : α → Multiset β<GOAL>(s.bind f).Nodup ↔ (∀ a ∈ s, (f a).Nodup) ∧ Multiset.Pairwise (fun a b => (f a).Disjoint (f b)) s
<VAR>α : Type u_1<VAR>β : Type v<VAR>DecidableEq α<VAR>DecidableEq β<VAR>s : Multiset α<VAR>f : α → Multiset β<GOAL>(s.dedup.bind f).dedup = (s.bind f).dedup
<VAR>α : Type u_1<VAR>β : Type v<VAR>l₁ : List α<VAR>l₂ : List β<GOAL>↑l₁ ×ˢ ↑l₂ = ↑(l₁ ×ˢ l₂)
<VAR>α : Type u_1<VAR>β : Type v<VAR>t : Multiset β<GOAL>0 ×ˢ t = 0
<VAR>α : Type u_1<VAR>β : Type v<VAR>a : α<VAR>s : Multiset α<VAR>t : Multiset β<GOAL>(a ::ₘ s) ×ˢ t = Multiset.map (Prod.mk a) t + s ×ˢ t
<VAR>α : Type u_1<VAR>β : Type v<VAR>s : Multiset α<GOAL>s ×ˢ 0 = 0
<VAR>α : Type u_1<VAR>β : Type v<VAR>b : β<VAR>s : Multiset α<VAR>t : Multiset β<GOAL>s ×ˢ (b ::ₘ t) = Multiset.map (fun a => (a, b)) s + s ×ˢ t
<VAR>α : Type u_1<VAR>β : Type v<VAR>a : α<VAR>b : β<GOAL>{a} ×ˢ {b} = {(a, b)}
<VAR>α : Type u_1<VAR>β : Type v<VAR>s t : Multiset α<VAR>u : Multiset β<GOAL>(s + t) ×ˢ u = s ×ˢ u + t ×ˢ u
<VAR>α : Type u_1<VAR>β : Type v<VAR>s : Multiset α<VAR>t u : Multiset β<GOAL>s ×ˢ (t + u) = s ×ˢ t + s ×ˢ u
<VAR>α : Type u_1<VAR>β : Type v<VAR>s : Multiset α<VAR>t : Multiset β<GOAL>Multiset.card (s ×ˢ t) = Multiset.card s * Multiset.card t
<VAR>α : Type u_1<VAR>β : Type v<VAR>s : Multiset α<VAR>t : Multiset β<VAR>p : α × β<GOAL>p ∈ s.product t ↔ p.1 ∈ s ∧ p.2 ∈ t
<VAR>α : Type u_1<VAR>β : Type v<VAR>s : Multiset α<VAR>t : Multiset β<GOAL>s.Nodup → t.Nodup → (s ×ˢ t).Nodup
<VAR>α : Type u_1<VAR>σ : α → Type u_4<VAR>l₁ : List α<VAR>l₂ : (a : α) → List (σ a)<GOAL>((↑l₁).sigma fun a => ↑(l₂ a)) = ↑(l₁.sigma l₂)
<VAR>α : Type u_1<VAR>σ : α → Type u_4<VAR>t : (a : α) → Multiset (σ a)<GOAL>Multiset.sigma 0 t = 0
<VAR>α : Type u_1<VAR>σ : α → Type u_4<VAR>a : α<VAR>s : Multiset α<VAR>t : (a : α) → Multiset (σ a)<GOAL>(a ::ₘ s).sigma t = Multiset.map (Sigma.mk a) (t a) + s.sigma t
<VAR>α : Type u_1<VAR>β : Type v<VAR>a : α<VAR>b : α → β<GOAL>({a}.sigma fun a => {b a}) = {⟨a, b a⟩}
<VAR>α : Type u_1<VAR>σ : α → Type u_4<VAR>s t : Multiset α<VAR>u : (a : α) → Multiset (σ a)<GOAL>(s + t).sigma u = s.sigma u + t.sigma u
<VAR>α : Type u_1<VAR>σ : α → Type u_4<VAR>s : Multiset α<VAR>t u : (a : α) → Multiset (σ a)<GOAL>(s.sigma fun a => t a + u a) = s.sigma t + s.sigma u
<VAR>α : Type u_1<VAR>σ : α → Type u_4<VAR>s : Multiset α<VAR>t : (a : α) → Multiset (σ a)<GOAL>Multiset.card (s.sigma t) = (Multiset.map (fun a => Multiset.card (t a)) s).sum
<VAR>α : Type u_1<VAR>σ : α → Type u_4<VAR>s : Multiset α<VAR>t : (a : α) → Multiset (σ a)<VAR>p : (a : α) × σ a<GOAL>p ∈ s.sigma t ↔ p.fst ∈ s ∧ p.snd ∈ t p.fst
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>σ : α → Type u_5<VAR>t : (a : α) → Multiset (σ a)<GOAL>s.Nodup → (∀ (a : α), (t a).Nodup) → (s.sigma t).Nodup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<GOAL>(↑l).dedup = ↑l.dedup
<VAR>α : Type u_1<VAR>DecidableEq α<GOAL>Multiset.dedup 0 = 0
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>a ∈ s.dedup ↔ a ∈ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>a ∈ s → (a ::ₘ s).dedup = s.dedup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>a ∉ s → (a ::ₘ s).dedup = a ::ₘ s.dedup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<GOAL>s.dedup ≤ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<GOAL>s.dedup ⊆ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<GOAL>s ⊆ s.dedup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>s.dedup ⊆ t ↔ s ⊆ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>s ⊆ t.dedup ↔ s ⊆ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<GOAL>s.dedup.Nodup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<GOAL>s.dedup = s ↔ s.Nodup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>m : Multiset α<VAR>a : α<GOAL>Multiset.count a m.dedup = if a ∈ m then 1 else 0