ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s t : Set α<GOAL>lowerClosure (s ⊼ t) = lowerClosure s ⊓ lowerClosure t
<VAR>n : ℕ<GOAL>↑(List.range n) = Multiset.range n
<VAR>n : ℕ<GOAL>Multiset.range n.succ = n ::ₘ Multiset.range n
<VAR>n : ℕ<GOAL>Multiset.card (Multiset.range n) = n
<VAR>m n : ℕ<GOAL>Multiset.range m ⊆ Multiset.range n ↔ m ≤ n
<VAR>m n : ℕ<GOAL>m ∈ Multiset.range n ↔ m < n
<VAR>n : ℕ<GOAL>n ∉ Multiset.range n
<VAR>n : ℕ<GOAL>n ∈ Multiset.range (n + 1)
<VAR>a b : ℕ<GOAL>Multiset.range (a + b) = Multiset.range a + Multiset.map (fun x => a + x) (Multiset.range b)
<VAR>a : ℕ<VAR>m : Multiset ℕ<GOAL>(Multiset.range a).Disjoint (Multiset.map (fun x => a + x) m)
<VAR>a b : ℕ<GOAL>Multiset.range (a + b) = Multiset.range a ∪ Multiset.map (fun x => a + x) (Multiset.range b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>hs : s.Subsingleton<VAR>ht : t.Subsingleton<GOAL>(s ×ˢ t).Subsingleton
<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₁ ×ˢ t₁ ⊆ s₂ ×ˢ t₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s₁ s₂ : Set α<VAR>t : Set β<VAR>hs : s₁ ⊆ s₂<GOAL>s₁ ×ˢ t ⊆ s₂ ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t₁ t₂ : Set β<VAR>ht : t₁ ⊆ t₂<GOAL>s ×ˢ t₁ ⊆ s ×ˢ t₂
<VAR>α : Type u_1<VAR>s₁ s₂ : Set α<GOAL>s₁ ×ˢ s₁ ⊆ s₂ ×ˢ s₂ ↔ s₁ ⊆ s₂
<VAR>α : Type u_1<VAR>s₁ s₂ : Set α<GOAL>s₁ ×ˢ s₁ ⊂ s₂ ×ˢ s₂ ↔ s₁ ⊂ s₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>P : Set (α × β)<GOAL>s ×ˢ t ⊆ P ↔ ∀ x ∈ s, ∀ y ∈ t, (x, y) ∈ P
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>p : α × β → Prop<GOAL>(∀ x ∈ s ×ˢ t, p x) ↔ ∀ x ∈ s, ∀ y ∈ t, p (x, y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>p : α × β → Prop<GOAL>(∃ x ∈ s ×ˢ t, p x) ↔ ∃ x ∈ s, ∃ y ∈ t, p (x, y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<GOAL>s ×ˢ ∅ = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : Set β<GOAL>∅ ×ˢ t = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Set.univ ×ˢ Set.univ = Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : Set β<GOAL>Set.univ ×ˢ t = Prod.snd ⁻¹' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<GOAL>s ×ˢ Set.univ = Prod.fst ⁻¹' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>Nonempty α<VAR>Nonempty β<GOAL>s ×ˢ t = Set.univ ↔ s = Set.univ ∧ t = Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : Set β<VAR>a : α<GOAL>{a} ×ˢ t = Prod.mk a '' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>b : β<GOAL>s ×ˢ {b} = (fun a => (a, b)) '' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<GOAL>{a} ×ˢ {b} = {(a, b)}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s₁ s₂ : Set α<VAR>t : Set β<GOAL>(s₁ ∪ s₂) ×ˢ t = s₁ ×ˢ t ∪ s₂ ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t₁ t₂ : Set β<GOAL>s ×ˢ (t₁ ∪ t₂) = s ×ˢ t₁ ∪ s ×ˢ t₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s₁ s₂ : Set α<VAR>t : Set β<GOAL>(s₁ ∩ s₂) ×ˢ t = s₁ ×ˢ t ∩ s₂ ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t₁ t₂ : Set β<GOAL>s ×ˢ (t₁ ∩ t₂) = s ×ˢ t₁ ∩ s ×ˢ t₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s₁ s₂ : Set α<VAR>t₁ t₂ : Set β<GOAL>s₁ ×ˢ t₁ ∩ s₂ ×ˢ t₂ = (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂)
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>s : Set α<VAR>t : Set β<GOAL>(s ×ˢ t)ᶜ = sᶜ ×ˢ Set.univ ∪ Set.univ ×ˢ tᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s₁ s₂ : Set α<VAR>t₁ t₂ : Set β<GOAL>Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ t₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s₁ s₂ : Set α<VAR>hs : Disjoint s₁ s₂<VAR>t₁ t₂ : Set β<GOAL>Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t₁ t₂ : Set β<VAR>ht : Disjoint t₁ t₂<VAR>s₁ s₂ : Set α<GOAL>Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>a : α<GOAL>insert a s ×ˢ t = Prod.mk a '' t ∪ s ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>b : β<GOAL>s ×ˢ insert b t = (fun a => (a, b)) '' s ∪ s ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s : Set α<VAR>t : Set β<VAR>f : γ → α<VAR>g : δ → β<GOAL>(f ⁻¹' s) ×ˢ (g ⁻¹' t) = (fun p => (f p.1, g p.2)) ⁻¹' s ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Set α<VAR>t : Set β<VAR>f : γ → α<GOAL>(f ⁻¹' s) ×ˢ t = (fun p => (f p.1, p.2)) ⁻¹' s ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_4<VAR>s : Set α<VAR>t : Set β<VAR>g : δ → β<GOAL>s ×ˢ (g ⁻¹' t) = (fun p => (p.1, g p.2)) ⁻¹' s ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α → β<VAR>g : γ → δ<VAR>s : Set β<VAR>t : Set δ<GOAL>Prod.map f g ⁻¹' s ×ˢ t = (f ⁻¹' s) ×ˢ (g ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Set α<VAR>t : Set β<VAR>f : γ → α<VAR>g : γ → β<GOAL>(fun x => (f x, g x)) ⁻¹' s ×ˢ t = f ⁻¹' s ∩ g ⁻¹' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>b : β<VAR>hb : b ∈ t<GOAL>(fun a => (a, b)) ⁻¹' s ×ˢ t = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>ha : a ∈ s<GOAL>Prod.mk a ⁻¹' s ×ˢ t = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>b : β<VAR>hb : b ∉ t<GOAL>(fun a => (a, b)) ⁻¹' s ×ˢ t = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>ha : a ∉ s<GOAL>Prod.mk a ⁻¹' s ×ˢ t = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>b : β<VAR>DecidablePred fun x => x ∈ t<GOAL>(fun a => (a, b)) ⁻¹' s ×ˢ t = if b ∈ t then s else ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>DecidablePred fun x => x ∈ s<GOAL>Prod.mk a ⁻¹' s ×ˢ t = if a ∈ s then t else ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Set α<VAR>t : Set β<VAR>b : β<VAR>DecidablePred fun x => x ∈ t<VAR>f : γ → α<GOAL>(fun a => (f a, b)) ⁻¹' s ×ˢ t = if b ∈ t then f ⁻¹' s else ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_4<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>DecidablePred fun x => x ∈ s<VAR>g : δ → β<GOAL>(fun b => (a, g b)) ⁻¹' s ×ˢ t = if a ∈ s then g ⁻¹' t else ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<GOAL>Prod.swap ⁻¹' s ×ˢ t = t ×ˢ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<GOAL>Prod.swap '' s ×ˢ t = t ×ˢ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s : Set α<VAR>t : Set β<VAR>m₁ : α → γ<VAR>m₂ : β → δ<GOAL>(m₁ '' s) ×ˢ (m₂ '' t) = (fun p => (m₁ p.1, m₂ p.2)) '' s ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m₁ : α → γ<VAR>m₂ : β → δ<GOAL>Set.range m₁ ×ˢ Set.range m₂ = Set.range fun p => (m₁ p.1, m₂ p.2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m₁ : α → γ<VAR>m₂ : β → δ<GOAL>Set.range (Prod.map m₁ m₂) = Set.range m₁ ×ˢ Set.range m₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>m₁ : α → γ<GOAL>Set.range m₁ ×ˢ Set.univ = Set.range fun p => (m₁ p.1, p.2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_4<VAR>m₂ : β → δ<GOAL>Set.univ ×ˢ Set.range m₂ = Set.range fun p => (p.1, m₂ p.2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>g : α → γ<GOAL>(Set.range fun x => (f x, g x)) ⊆ Set.range f ×ˢ Set.range g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<GOAL>s.Nonempty → t.Nonempty → (s ×ˢ t).Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<GOAL>(s ×ˢ t).Nonempty → s.Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<GOAL>(s ×ˢ t).Nonempty → t.Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<GOAL>(s ×ˢ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<GOAL>s ×ˢ t = ∅ ↔ s = ∅ ∨ t = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Set α<VAR>t : Set β<VAR>W : Set γ<VAR>f : α × β → γ<GOAL>s ×ˢ t ⊆ f ⁻¹' W ↔ ∀ (a : α) (b : β), a ∈ s → b ∈ t → f (a, b) ∈ W
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>g : α → γ<VAR>s : Set α<GOAL>(fun x => (f x, g x)) '' s ⊆ (f '' s) ×ˢ (g '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>b : β<VAR>hb : b ∈ t<GOAL>(fun a => (a, b)) '' s ⊆ s ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>ha : a ∈ s<GOAL>Prod.mk a '' t ⊆ s ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<GOAL>s ×ˢ t ⊆ Prod.fst ⁻¹' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<GOAL>Prod.fst '' s ×ˢ t ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set β<VAR>t : Set α<VAR>ht : t.Nonempty<GOAL>Prod.fst '' s ×ˢ t = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<GOAL>s ×ˢ t ⊆ Prod.snd ⁻¹' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<GOAL>Prod.snd '' s ×ˢ t ⊆ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>hs : s.Nonempty<VAR>t : Set β<GOAL>Prod.snd '' s ×ˢ t = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s s₁ : Set α<VAR>t t₁ : Set β<GOAL>s ×ˢ t \ s₁ ×ˢ t₁ = s ×ˢ (t \ t₁) ∪ (s \ s₁) ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s s₁ : Set α<VAR>t t₁ : Set β<GOAL>s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s s₁ : Set α<VAR>t t₁ : Set β<VAR>h : (s ×ˢ t).Nonempty<GOAL>s ×ˢ t = s₁ ×ˢ t₁ ↔ s = s₁ ∧ t = t₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s s₁ : Set α<VAR>t t₁ : Set β<GOAL>s ×ˢ t = s₁ ×ˢ t₁ ↔ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s s₁ : Set α<VAR>t : Set β<VAR>ht : t.Nonempty<GOAL>s ×ˢ t = s₁ ×ˢ t ↔ s = s₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Preorder α<VAR>f : α → Set β<VAR>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>γ : Type u_3<VAR>Preorder α<VAR>f : α → Set β<VAR>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>γ : Type u_3<VAR>s : Set α<VAR>Preorder α<VAR>f : α → Set β<VAR>g : α → 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>γ : Type u_3<VAR>s : Set α<VAR>Preorder α<VAR>f : α → Set β<VAR>g : α → 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>Nonempty α<GOAL>(Set.diagonal α).Nonempty
<VAR>α : Type u_1<VAR>s : Set α<GOAL>(Prod.map (fun x => ↑x) fun x => ↑x) ⁻¹' Set.diagonal α = Set.diagonal ↑s
<VAR>α : Type u_1<GOAL>(Set.range fun x => (x, x)) = Set.diagonal α
<VAR>α : Type u_1<VAR>s : Set (α × α)<GOAL>Set.diagonal α ⊆ s ↔ ∀ (x : α), (x, x) ∈ s
<VAR>α : Type u_1<VAR>s t : Set α<GOAL>s ×ˢ t ⊆ (Set.diagonal α)ᶜ ↔ Disjoint s t
<VAR>α : Type u_1<VAR>s t : Set α<GOAL>(fun x => (x, x)) ⁻¹' s ×ˢ t = s ∩ t
<VAR>α : Type u_1<VAR>s : Set α<GOAL>(fun x => (x, x)) ⁻¹' s ×ˢ s = s
<VAR>α : Type u_1<VAR>s : Set α<GOAL>(fun x => (x, x)) '' s = Set.diagonal α ∩ s ×ˢ s
<VAR>α : Type u_1<GOAL>Set.diagonal α = Set.univ ↔ Subsingleton α
<VAR>α : Type u_1<VAR>Subsingleton α<GOAL>Set.diagonal α = Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>hβ : Nonempty β<GOAL>Set.range (Function.const α) = {f | ∀ (x y : α), f x = f y}
<VAR>X : Type u_2<VAR>Y : Sort u_3<VAR>Z : Type u_1<VAR>f : X → Y<VAR>g : Z → Y<GOAL>f ∘ Function.Pullback.fst = g ∘ Function.Pullback.snd
<VAR>X : Type u_2<VAR>Y : Sort u_3<VAR>Z : Type u_1<VAR>f : X → Y<VAR>g : Z → Y<GOAL>Function.PullbackSelf.map_fst ⁻¹' Function.pullbackDiagonal f = Function.pullbackDiagonal Function.Pullback.snd
<VAR>X : Type u_2<VAR>Y : Sort u_3<VAR>Z : Type u_1<VAR>f : X → Y<VAR>g : Z → X<VAR>inj : Function.Injective g<GOAL>Function.mapPullback g id g ⋯ ⋯ ⁻¹' Function.pullbackDiagonal f = Function.pullbackDiagonal (f ∘ g)
<VAR>X : Type u_1<VAR>Y : Sort u_2<VAR>f : X → Y<VAR>s : Set X<GOAL>toPullbackDiag f '' s = Function.pullbackDiagonal f ∩ Subtype.val ⁻¹' s ×ˢ s
<VAR>X : Type u_1<VAR>Y : Sort u_2<VAR>f : X → Y<GOAL>Set.range (toPullbackDiag f) = Function.pullbackDiagonal f
<VAR>X : Type u_1<VAR>Y : Sort u_2<VAR>f : X → Y<GOAL>Function.Injective (toPullbackDiag f)
<VAR>α : Type u_1<GOAL>Monotone Set.offDiag
<VAR>α : Type u_1<VAR>s : Set α<GOAL>s.offDiag.Nonempty ↔ s.Nontrivial
<VAR>α : Type u_1<VAR>s : Set α<GOAL>s.offDiag = ∅ ↔ s.Subsingleton
<VAR>α : Type u_1<VAR>s : Set α<GOAL>s.offDiag ⊆ s ×ˢ s
<VAR>α : Type u_1<VAR>s : Set α<GOAL>s.offDiag = {x | x ∈ s ×ˢ s ∧ x.1 ≠ x.2}
<VAR>α : Type u_1<GOAL>∅.offDiag = ∅
<VAR>α : Type u_1<VAR>a : α<GOAL>{a}.offDiag = ∅
<VAR>α : Type u_1<GOAL>Set.univ.offDiag = (Set.diagonal α)ᶜ
<VAR>α : Type u_1<VAR>s : Set α<GOAL>s ×ˢ s \ Set.diagonal α = s.offDiag
<VAR>α : Type u_1<VAR>s : Set α<GOAL>Disjoint (Set.diagonal α) s.offDiag
<VAR>α : Type u_1<VAR>s t : Set α<GOAL>(s ∩ t).offDiag = s.offDiag ∩ t.offDiag
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : Disjoint s t<GOAL>(s ∪ t).offDiag = s.offDiag ∪ t.offDiag ∪ s ×ˢ t ∪ t ×ˢ s
<VAR>α : Type u_1<VAR>s : Set α<VAR>a : α<VAR>ha : a ∉ s<GOAL>(insert a s).offDiag = s.offDiag ∪ {a} ×ˢ s ∪ s ×ˢ {a}
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : (i : ι) → Set (α i)<GOAL>∅.pi s = Set.univ
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>t : (i : ι) → Set (α i)<VAR>ht : ∀ (i : ι), (t i).Subsingleton<GOAL>(Set.univ.pi t).Subsingleton
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Set ι<GOAL>(s.pi fun i => Set.univ) = Set.univ
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Set ι<VAR>DecidablePred fun x => x ∈ s<VAR>t : (i : ι) → Set (α i)<GOAL>(Set.univ.pi fun i => if i ∈ s then t i else Set.univ) = s.pi t
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Set ι<VAR>t₁ t₂ : (i : ι) → Set (α i)<VAR>h : ∀ i ∈ s, t₁ i ⊆ t₂ i<GOAL>s.pi t₁ ⊆ s.pi t₂
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Set ι<VAR>t t₁ : (i : ι) → Set (α i)<GOAL>(s.pi fun i => t i ∩ t₁ i) = s.pi t ∩ s.pi t₁
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s₁ s₂ : Set ι<VAR>t₁ t₂ : (i : ι) → Set (α i)<VAR>h : s₁ = s₂<VAR>h' : ∀ i ∈ s₁, t₁ i = t₂ i<GOAL>s₁.pi t₁ = s₂.pi t₂
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>i : ι<VAR>hs : i ∈ s<VAR>ht : t i = ∅<GOAL>s.pi t = ∅
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>t : (i : ι) → Set (α i)<VAR>i : ι<VAR>ht : t i = ∅<GOAL>Set.univ.pi t = ∅
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<GOAL>(s.pi t).Nonempty ↔ ∀ (i : ι), ∃ x, i ∈ s → x ∈ t i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>t : (i : ι) → Set (α i)<GOAL>(Set.univ.pi t).Nonempty ↔ ∀ (i : ι), (t i).Nonempty
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<GOAL>s.pi t = ∅ ↔ ∃ i, IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>t : (i : ι) → Set (α i)<GOAL>Set.univ.pi t = ∅ ↔ ∃ i, t i = ∅
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>h : Nonempty ι<GOAL>(Set.univ.pi fun x => ∅) = ∅
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>t₁ t₂ : (i : ι) → Set (α i)<GOAL>Disjoint (Set.univ.pi t₁) (Set.univ.pi t₂) ↔ ∃ i, Disjoint (t₁ i) (t₂ i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Set ι<VAR>t₁ t₂ : (i : ι) → Set (α i)<VAR>i : ι<VAR>hi : i ∈ s<VAR>ht : Disjoint (t₁ i) (t₂ i)<GOAL>Disjoint (s.pi t₁) (s.pi t₂)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>Unique ι<VAR>t : (i : ι) → Set (α i)<GOAL>uniqueElim ⁻¹' Set.univ.pi t = t default
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>∀ (i : ι), Nonempty (α i)<GOAL>s.pi t = ∅ ↔ ∃ i ∈ s, t i = ∅
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Set ι<VAR>t₁ t₂ : (i : ι) → Set (α i)<VAR>∀ (i : ι), Nonempty (α i)<GOAL>Disjoint (s.pi t₁) (s.pi t₂) ↔ ∃ i ∈ s, Disjoint (t₁ i) (t₂ i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>f : (i : ι) → α i → β i<GOAL>(Set.range fun g i => f i (g i)) = Set.univ.pi fun i => Set.range (f i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>i : ι<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<GOAL>(insert i s).pi t = Function.eval i ⁻¹' t i ∩ s.pi t
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>i : ι<VAR>t : (i : ι) → Set (α i)<GOAL>{i}.pi t = Function.eval i ⁻¹' t i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>i : ι<VAR>t : (i : ι) → Set (α i)<GOAL>{i}.pi t = {x | x i ∈ t i}
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f : (i : ι) → α i<GOAL>(Set.univ.pi fun i => {f i}) = {f}
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s : Set ι<VAR>t : (i : ι) → Set (β i)<VAR>f : (i : ι) → α i → β i<GOAL>(fun g i => f i (g i)) ⁻¹' s.pi t = s.pi fun i => f i ⁻¹' t i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>p : ι → Prop<VAR>h : DecidablePred p<VAR>s : Set ι<VAR>t₁ t₂ : (i : ι) → Set (α i)<GOAL>(s.pi fun i => if p i then t₁ i else t₂ i) = {i | i ∈ s ∧ p i}.pi t₁ ∩ {i | i ∈ s ∧ ¬p i}.pi t₂
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s₁ s₂ : Set ι<VAR>t : (i : ι) → Set (α i)<GOAL>(s₁ ∪ s₂).pi t = s₁.pi t ∩ s₂.pi t
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s₁ s₂ : Set ι<VAR>t₁ t₂ : (i : ι) → Set (α i)<VAR>ht₁ : ∀ i ∉ s₁, t₁ i = Set.univ<VAR>ht₂ : ∀ i ∉ s₂, t₂ i = Set.univ<GOAL>((s₁ ∪ s₂).pi fun i => t₁ i ∩ t₂ i) = s₁.pi t₁ ∩ s₂.pi t₂
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>t : (i : ι) → Set (α i)<VAR>s : Set ι<GOAL>s.pi t ∩ sᶜ.pi t = Set.univ.pi t
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s : Set ι<VAR>i : ι<VAR>DecidableEq ι<VAR>hi : i ∉ s<VAR>f : (j : ι) → α j<VAR>a : α i<VAR>t : (j : ι) → α j → Set (β j)<GOAL>(s.pi fun j => t j (Function.update f i a j)) = s.pi fun j => t j (f j)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s : Set ι<VAR>i : ι<VAR>DecidableEq ι<VAR>hi : i ∈ s<VAR>f : (j : ι) → α j<VAR>a : α i<VAR>t : (j : ι) → α j → Set (β j)<GOAL>(s.pi fun j => t j (Function.update f i a j)) = {x | x i ∈ t i a} ∩ (s \ {i}).pi fun j => t j (f j)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>β : ι → Type u_4<VAR>i : ι<VAR>f : (j : ι) → α j<VAR>a : α i<VAR>t : (j : ι) → α j → Set (β j)<GOAL>(Set.univ.pi fun j => t j (Function.update f i a j)) = {x | x i ∈ t i a} ∩ {i}ᶜ.pi fun j => t j (f j)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>i : ι<VAR>s : Set (α i)<GOAL>Set.univ.pi (Function.update (fun j => Set.univ) i s) = Function.eval i ⁻¹' s
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>i : ι<VAR>hs : i ∈ s<GOAL>Function.eval i '' s.pi t ⊆ t i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>t : (i : ι) → Set (α i)<VAR>i : ι<GOAL>Function.eval i '' Set.univ.pi t ⊆ t i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>ht : (s.pi t).Nonempty<VAR>i : ι<GOAL>t i ⊆ Function.eval i '' s.pi t
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>i : ι<VAR>hs : i ∈ s<VAR>ht : (s.pi t).Nonempty<GOAL>Function.eval i '' s.pi t = t i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>i : ι<VAR>Decidable (s.pi t).Nonempty<VAR>hi : i ∉ s<GOAL>Function.eval i '' s.pi t = if (s.pi t).Nonempty then Set.univ else ∅
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>t : (i : ι) → Set (α i)<VAR>i : ι<VAR>ht : (Set.univ.pi t).Nonempty<GOAL>(fun f => f i) '' Set.univ.pi t = t i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Set ι<VAR>t₁ t₂ : (i : ι) → Set (α i)<GOAL>s.pi t₁ ⊆ s.pi t₂ ↔ (∀ i ∈ s, t₁ i ⊆ t₂ i) ∨ s.pi t₁ = ∅
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>t₁ t₂ : (i : ι) → Set (α i)<GOAL>Set.univ.pi t₁ ⊆ Set.univ.pi t₂ ↔ (∀ (i : ι), t₁ i ⊆ t₂ i) ∨ ∃ i, t₁ i = ∅
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>i : ι<VAR>DecidableEq ι<VAR>s : Set (α i)<GOAL>Function.eval i ⁻¹' s = Set.univ.pi (Function.update (fun i => Set.univ) i s)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>i : ι<VAR>DecidableEq ι<VAR>s : Set (α i)<GOAL>Function.eval i ⁻¹' s = {i}.pi (Function.update (fun i => Set.univ) i s)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>i : ι<VAR>DecidableEq ι<VAR>f : (i : ι) → α i<VAR>hi : i ∈ s<VAR>hf : ∀ j ∈ s, j ≠ i → f j ∈ t j<GOAL>Function.update f i ⁻¹' s.pi t = t i
<VAR>ι : Type u_1<VAR>β : ι → Type u_3<VAR>DecidableEq ι<VAR>x : (i : ι) → β i<VAR>i : ι<VAR>s : Set (β i)<GOAL>Function.update x i '' s = Set.univ.pi (Function.update (fun j => {x j}) i s)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>t : (i : ι) → Set (α i)<VAR>i : ι<VAR>DecidableEq ι<VAR>f : (i : ι) → α i<VAR>hf : ∀ (j : ι), j ≠ i → f j ∈ t j<GOAL>Function.update f i ⁻¹' Set.univ.pi t = t i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Set ι<VAR>u : Set ((i : ι) → α i)<GOAL>u ⊆ s.pi fun i => Function.eval i '' u
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>f : ι' ≃ ι<VAR>s : Set ι'<VAR>t : (i : ι) → Set (α i)<GOAL>(⇑(Equiv.piCongrLeft α f).symm ⁻¹' s.pi fun i' => t (f i')) = (⇑f '' s).pi t
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>f : ι' ≃ ι<VAR>t : (i : ι) → Set (α i)<GOAL>(⇑(Equiv.piCongrLeft α f).symm ⁻¹' Set.univ.pi fun i' => t (f i')) = Set.univ.pi t
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>f : ι' ≃ ι<VAR>s : Set ι'<VAR>t : (i : ι) → Set (α i)<GOAL>⇑(Equiv.piCongrLeft α f) ⁻¹' (⇑f '' s).pi t = s.pi fun i => t (f i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>f : ι' ≃ ι<VAR>t : (i : ι) → Set (α i)<GOAL>⇑(Equiv.piCongrLeft α f) ⁻¹' Set.univ.pi t = Set.univ.pi fun i => t (f i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>π : ι ⊕ ι' → Type u_4<VAR>t : (i : ι ⊕ ι') → Set (π i)<GOAL>⇑(Equiv.sumPiEquivProdPi π).symm ⁻¹' Set.univ.pi t = (Set.univ.pi fun i => t (Sum.inl i)) ×ˢ Set.univ.pi fun i => t (Sum.inr i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>f ⁻¹' ∅ = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : α → β<VAR>s : Set β<VAR>h : ∀ (x : α), f x = g x<GOAL>f ⁻¹' s = g ⁻¹' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s t : Set β<VAR>h : s ⊆ t<GOAL>f ⁻¹' s ⊆ f ⁻¹' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>f ⁻¹' Set.univ = Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<GOAL>s ⊆ f ⁻¹' Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s t : Set β<GOAL>f ⁻¹' (s ∩ t) = f ⁻¹' s ∩ f ⁻¹' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s t : Set β<GOAL>f ⁻¹' (s ∪ t) = f ⁻¹' s ∪ f ⁻¹' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set β<GOAL>f ⁻¹' sᶜ = (f ⁻¹' s)ᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s t : Set β<GOAL>f ⁻¹' (s \ t) = f ⁻¹' s \ f ⁻¹' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s t : Set β<GOAL>f ⁻¹' symmDiff s t = symmDiff (f ⁻¹' s) (f ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s t₁ t₂ : Set β<GOAL>f ⁻¹' s.ite t₁ t₂ = (f ⁻¹' s).ite (f ⁻¹' t₁) (f ⁻¹' t₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α → Prop<VAR>f : β → α<GOAL>f ⁻¹' {a | p a} = {a | p (f a)}
<VAR>α : Type u_1<GOAL>Set.preimage id = id
<VAR>α : Type u_1<VAR>s : Set α<GOAL>id ⁻¹' s = s
<VAR>α : Type u_1<VAR>s : Set α<GOAL>(fun x => x) ⁻¹' s = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>b : β<VAR>s : Set β<VAR>h : b ∈ s<GOAL>(fun x => b) ⁻¹' s = Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>b : β<VAR>s : Set β<VAR>h : b ∉ s<GOAL>(fun x => b) ⁻¹' s = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>b : β<VAR>s : Set β<VAR>Decidable (b ∈ s)<GOAL>(fun x => b) ⁻¹' s = if b ∈ s then Set.univ else ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Nonempty β<VAR>f : α → β<VAR>hf : ∀ (b : β), f ⁻¹' {b} = ∅ ∨ f ⁻¹' {b} = Set.univ<GOAL>∃ b, f = Function.const α b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>g : β → γ<VAR>s : Set γ<GOAL>g ∘ f ⁻¹' s = f ⁻¹' (g ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>g : β → γ<GOAL>Set.preimage (g ∘ f) = Set.preimage f ∘ Set.preimage g
<VAR>α : Type u_1<VAR>f : α → α<VAR>n : ℕ<GOAL>Set.preimage f^[n] = (Set.preimage f)^[n]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>g : β → γ<VAR>f : α → β<VAR>s : Set γ<GOAL>f ⁻¹' (g ⁻¹' s) = (fun x => g (f x)) ⁻¹' s
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>s : Set (Subtype p)<VAR>t : Set α<GOAL>s = Subtype.val ⁻¹' t ↔ ∀ (x : α) (h : p x), ⟨x, h⟩ ∈ s ↔ x ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set β<VAR>f : α → β<VAR>hf : (f ⁻¹' s).Nonempty<GOAL>s.Nonempty
<VAR>α : Type u_1<VAR>p : α → Prop<GOAL>p ⁻¹' {True} = {a | p a}
<VAR>α : Type u_1<VAR>p : α → Prop<GOAL>p ⁻¹' {False} = {a | ¬p a}
<VAR>α : Type u_1<VAR>s u v : Set α<VAR>hsuv : s ⊆ u ∪ v<VAR>H : s ∩ (u ∩ v) = ∅<GOAL>Subtype.val ⁻¹' u = (Subtype.val ⁻¹' v)ᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<VAR>y : β<GOAL>y ∈ f '' s ↔ ∃ x, ∃ (_ : x ∈ s), f x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<GOAL>f '' s = (fun x => f x) '' s