ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>s : Set α<VAR>a : α<GOAL>f a ∈ f '' s ↔ a ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>hf : Function.Injective f<VAR>h : Set.SurjOn f s t<GOAL>f ⁻¹' t ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<VAR>p : β → Prop<GOAL>(∀ y ∈ f '' s, p y) ↔ ∀ ⦃x : α⦄, x ∈ s → p (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<VAR>p : β → Prop<GOAL>(∃ y ∈ f '' s, p y) ↔ ∃ x ∈ s, p (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<VAR>C : β → Prop<VAR>h : ∀ x ∈ s, C (f x)<VAR>y : β<GOAL>y ∈ f '' s → C y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<VAR>C : β → Prop<VAR>y : β<VAR>h_y : y ∈ f '' s<VAR>h : ∀ x ∈ s, C (f x)<GOAL>C y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : α → β<VAR>s : Set α<VAR>h : ∀ a ∈ s, f a = g a<GOAL>f '' s = g '' s
<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>γ : Type u_3<VAR>f : β → γ<VAR>g : α → β<VAR>a : Set α<GOAL>f ∘ g '' a = f '' (g '' a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>g : β → γ<GOAL>Set.image (g ∘ f) = Set.image g ∘ Set.image f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>g : β → γ<VAR>f : α → β<VAR>s : Set α<GOAL>g '' (f '' s) = (fun x => g (f x)) '' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Set α<VAR>β' : Type u_6<VAR>f : β → γ<VAR>g : α → β<VAR>f' : α → β'<VAR>g' : β' → γ<VAR>h_comm : ∀ (a : α), f (g a) = g' (f' a)<GOAL>f '' (g '' s) = g' '' (f' '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>ga : α → α<VAR>gb : β → β<VAR>h : Function.Semiconj f ga gb<GOAL>Function.Semiconj (Set.image f) (Set.image ga) (Set.image gb)
<VAR>α : Type u_1<VAR>f g : α → α<VAR>h : Function.Commute f g<GOAL>Function.Commute (Set.image f) (Set.image g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a b : Set α<VAR>f : α → β<VAR>h : a ⊆ b<GOAL>f '' a ⊆ f '' b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>Monotone (Set.image f)
<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 : α → β<GOAL>f '' ∅ = ∅
<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 α<VAR>h : ∀ x ∈ t, ∀ y ∈ s, f x = f y → x = y<GOAL>f '' (s ∩ t) = f '' s ∩ f '' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s t : Set α<VAR>H : Function.Injective f<GOAL>f '' (s ∩ t) = f '' s ∩ f '' t
<VAR>β : Type u_2<VAR>ι : Type u_6<VAR>f : ι → β<VAR>H : Function.Surjective f<GOAL>f '' Set.univ = Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>a : α<GOAL>f '' {a} = {f a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>hs : s.Nonempty<VAR>a : β<GOAL>(fun x => a) '' s = {a}
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>f : α → β<VAR>s : Set α<GOAL>f '' s = ∅ ↔ s = ∅
<VAR>α : Type u_1<VAR>BooleanAlgebra α<VAR>S : Set α<GOAL>compl ⁻¹' S = compl '' S
<VAR>α : Type u_1<VAR>BooleanAlgebra α<VAR>t : α<VAR>S : Set α<GOAL>t ∈ compl '' S ↔ tᶜ ∈ S
<VAR>α : Type u_1<VAR>s : Set α<GOAL>(fun x => x) '' s = s
<VAR>α : Type u_1<VAR>s : Set α<GOAL>id '' s = s
<VAR>α : Type u_1<VAR>f : α → α<VAR>n : ℕ<GOAL>Set.image f^[n] = (Set.image f)^[n]
<VAR>α : Type u_1<VAR>BooleanAlgebra α<VAR>S : Set α<GOAL>compl '' (compl '' S) = S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>a : α<VAR>s : Set α<GOAL>f '' insert a s = insert (f a) (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>a b : α<GOAL>f '' {a, b} = {f a, f b}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>g : β → α<VAR>I : Function.LeftInverse g f<VAR>s : Set α<GOAL>f '' s ⊆ g ⁻¹' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>g : β → α<VAR>I : Function.LeftInverse g f<VAR>s : Set β<GOAL>f ⁻¹' s ⊆ g '' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>g : β → α<VAR>h₁ : Function.LeftInverse g f<VAR>h₂ : Function.RightInverse g f<GOAL>Set.image f = Set.preimage g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>g : β → α<VAR>b : β<VAR>s : Set α<VAR>h₁ : Function.LeftInverse g f<VAR>h₂ : Function.RightInverse g f<GOAL>b ∈ f '' s ↔ g b ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<VAR>H : Function.Injective f<GOAL>f '' sᶜ ⊆ (f '' s)ᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<VAR>H : Function.Surjective f<GOAL>(f '' s)ᶜ ⊆ f '' sᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<VAR>H : Function.Bijective f<GOAL>f '' sᶜ = (f '' s)ᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s t : Set α<GOAL>f '' s \ f '' t ⊆ f '' (s \ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s t : Set α<GOAL>symmDiff (f '' s) (f '' t) ⊆ f '' symmDiff s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>s t : Set α<GOAL>f '' (s \ t) = f '' s \ f '' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Injective 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 : Set α<GOAL>s.Nonempty → (f '' s).Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<GOAL>(f '' s).Nonempty → s.Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<GOAL>(f '' s).Nonempty ↔ s.Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set β<VAR>hs : s.Nonempty<VAR>f : α → β<VAR>hf : Function.Surjective f<GOAL>(f ⁻¹' s).Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<GOAL>f '' s ⊆ t ↔ s ⊆ f ⁻¹' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set β<GOAL>f '' (f ⁻¹' s) ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<GOAL>s ⊆ f ⁻¹' (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<VAR>h : Function.Injective f<GOAL>f ⁻¹' (f '' s) = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set β<VAR>h : Function.Surjective f<GOAL>f '' (f ⁻¹' s) = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>hs : s.Nonempty<VAR>t : Set β<VAR>a : β<GOAL>s ⊆ (fun x => a) ⁻¹' t ↔ a ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : β → α<VAR>hf : Function.Surjective f<GOAL>f ⁻¹' s = f ⁻¹' t ↔ s = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<GOAL>f '' (s ∩ f ⁻¹' t) = f '' s ∩ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<GOAL>f '' (f ⁻¹' t ∩ s) = t ∩ f '' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<GOAL>(f '' s ∩ t).Nonempty ↔ (s ∩ f ⁻¹' t).Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<GOAL>f '' (s \ f ⁻¹' t) = f '' s \ t
<VAR>α : Type u_1<GOAL>Set.image compl = Set.preimage compl
<VAR>α : Type u_1<VAR>p : Set α → Prop<GOAL>compl '' {s | p s} = {s | p sᶜ}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<GOAL>s ∩ f ⁻¹' t ⊆ f ⁻¹' (f '' s ∩ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<GOAL>s ∪ f ⁻¹' t ⊆ f ⁻¹' (f '' s ∪ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<GOAL>f '' (s ∪ f ⁻¹' t) ⊆ f '' s ∪ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<GOAL>f ⁻¹' B ⊆ A ↔ ∀ (a : α), f a ∈ B → a ∈ A
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>f '' s = f '' t ↔ s = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<GOAL>t ⊆ f '' s ↔ ∃ u ⊆ s, f '' u = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<VAR>p : Set β → Prop<GOAL>(∃ t ⊆ f '' s, p t) ↔ ∃ t ⊆ s, p (f '' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<VAR>p : Set β → Prop<GOAL>(∀ t ⊆ f '' s, p t) ↔ ∀ t ⊆ s, p (f '' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>f '' s ⊆ f '' t ↔ s ⊆ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Setoid α<VAR>g : Quotient s → β<VAR>h : α → β<VAR>Hh : h = g ∘ Quotient.mk''<VAR>r : Set (β × β)<GOAL>{x | (g x.1, g x.2) ∈ r} = (fun a => (⟦a.1⟧, ⟦a.2⟧)) '' ((fun a => (h a.1, h a.2)) ⁻¹' r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>x : Set α<VAR>P : β → Prop<GOAL>(∃ a, P ↑a) ↔ ∃ a, P (f ↑a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<GOAL>Subtype.val ∘ Set.imageFactorization f s = f ∘ Subtype.val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<GOAL>Function.Surjective (Set.imageFactorization f s)
<VAR>α : Type u_1<VAR>s : Set α<VAR>σ : Equiv.Perm α<VAR>hs : {a | σ a ≠ a} ⊆ s<GOAL>⇑σ '' s = s
<VAR>α : Type u_1<VAR>s : Set α<VAR>a : α<GOAL>𝒫 insert a s = 𝒫 s ∪ insert a '' 𝒫 s
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>f : ι → α<VAR>p : α → Prop<GOAL>(∀ a ∈ Set.range f, p a) ↔ ∀ (i : ι), p (f i)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>f : ι → α<VAR>p : ↑(Set.range f) → Prop<GOAL>(∀ (a : ↑(Set.range f)), p a) ↔ ∀ (i : ι), p ⟨f i, ⋯⟩
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>f : ι → α<VAR>p : α → Prop<GOAL>(∃ a ∈ Set.range f, p a) ↔ ∃ i, p (f i)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>f : ι → α<VAR>p : ↑(Set.range f) → Prop<GOAL>(∃ a, p a) ↔ ∃ i, p ⟨f i, ⋯⟩
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>f : ι → α<GOAL>Set.range f = Set.univ ↔ Function.Surjective f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>h : Function.Surjective f<VAR>s : Set β<GOAL>s ⊆ Set.range f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>f '' Set.univ = Set.range f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set β<GOAL>f ⁻¹' s = Set.univ ↔ Set.range f ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<GOAL>f '' s ⊆ Set.range f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<VAR>x : β<VAR>h : x ∈ f '' s<GOAL>x ∈ Set.range f
<VAR>i : ℕ<GOAL>i ∈ Set.range Nat.succ ↔ 0 < i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set β<VAR>hs : s.Nonempty<VAR>f : α → β<VAR>hf : s ⊆ Set.range f<GOAL>(f ⁻¹' s).Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>g : α → β<VAR>f : ι → α<GOAL>Set.range (g ∘ f) = g '' Set.range f
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>f : ι → α<VAR>s : Set α<GOAL>Set.range f ⊆ s ↔ ∀ (y : ι), f y ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → γ<VAR>g : β → γ<GOAL>Set.range f ⊆ Set.range g ↔ ∃ h, f = g ∘ h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set β<GOAL>Set.range f = s ↔ (∀ (a : α), f a ∈ s) ∧ ∀ b ∈ s, ∃ a, f a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>g : β → γ<GOAL>Set.range (g ∘ f) ⊆ Set.range g
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>f : ι → α<GOAL>(Set.range f).Nonempty ↔ Nonempty ι
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>h : Nonempty ι<VAR>f : ι → α<GOAL>(Set.range f).Nonempty
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>f : ι → α<GOAL>Set.range f = ∅ ↔ IsEmpty ι
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>IsEmpty ι<VAR>f : ι → α<GOAL>Set.range f = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<GOAL>f '' s ∪ f '' sᶜ = Set.range f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>x : α<GOAL>insert (f x) (f '' {x}ᶜ) = Set.range f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>t : Set β<GOAL>f '' (f ⁻¹' t) = Set.range f ∩ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>t : Set β<GOAL>f '' (f ⁻¹' t) = t ∩ Set.range f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set β<VAR>hs : s ⊆ Set.range f<GOAL>f '' (f ⁻¹' s) = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set β<GOAL>f '' (f ⁻¹' s) = s ↔ s ⊆ Set.range f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set β<GOAL>s ⊆ Set.range f ↔ ∃ t, f '' t = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>Set.range (Set.image f) = 𝒫 Set.range f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>p : Set β → Prop<GOAL>(∃ s ⊆ Set.range f, p s) ↔ ∃ s, p (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>p : Set β → Prop<GOAL>(∃ s, ∃ (_ : s ⊆ Set.range f), p s) ↔ ∃ s, p (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>p : Set β → Prop<GOAL>(∀ s ⊆ Set.range f, p s) ↔ ∀ (s : Set α), p (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : β → α<VAR>hs : s ⊆ Set.range f<GOAL>f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : β → α<VAR>hs : s ⊆ Set.range f<VAR>ht : t ⊆ Set.range f<GOAL>f ⁻¹' s = f ⁻¹' t ↔ s = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set β<GOAL>f ⁻¹' (s ∩ Set.range f) = f ⁻¹' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set β<GOAL>f ⁻¹' (Set.range f ∩ s) = f ⁻¹' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set β<GOAL>f ⁻¹' (f '' (f ⁻¹' s)) = f ⁻¹' s
<VAR>α : Type u_1<GOAL>Set.range id = Set.univ
<VAR>α : Type u_1<GOAL>(Set.range fun x => x) = Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Nonempty β<GOAL>Set.range Prod.fst = Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Nonempty α<GOAL>Set.range Prod.snd = Set.univ
<VAR>ι : Sort u_4<VAR>α : ι → Type u_6<VAR>∀ (i : ι), Nonempty (α i)<VAR>i : ι<GOAL>Set.range (Function.eval i) = Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Set.range Sum.inl = {x | x.isLeft = true}
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Set.range Sum.inr = {x | x.isRight = true}
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>IsCompl (Set.range Sum.inl) (Set.range Sum.inr)
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Set.range Sum.inl ∪ Set.range Sum.inr = Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Set.range Sum.inl ∩ Set.range Sum.inr = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Set.range Sum.inr ∪ Set.range Sum.inl = Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Set.range Sum.inr ∩ Set.range Sum.inl = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set β<GOAL>Sum.inl ⁻¹' (Sum.inr '' s) = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<GOAL>Sum.inr ⁻¹' (Sum.inl '' s) = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Sum.inl ⁻¹' Set.range Sum.inr = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Sum.inr ⁻¹' Set.range Sum.inl = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>(Set.range Sum.inl)ᶜ = Set.range Sum.inr
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>(Set.range Sum.inr)ᶜ = Set.range Sum.inl
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set (α ⊕ β)<GOAL>Sum.inl '' (Sum.inl ⁻¹' s) ∪ Sum.inr '' (Sum.inr ⁻¹' s) = s
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>Set.range (Quot.mk r) = Set.univ
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>f : ι → α<VAR>r : ι → ι → Prop<VAR>hf : ∀ (x y : ι), r x y → f x = f y<GOAL>Set.range (Quot.lift f hf) = Set.range f
<VAR>α : Type u_1<VAR>sa : Setoid α<GOAL>(Set.range fun x => ⟦x⟧) = Set.univ
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>f : ι → α<VAR>s : Setoid ι<VAR>hf : ∀ (a b : ι), a ≈ b → f a = f b<GOAL>Set.range (Quotient.lift f hf) = Set.range f
<VAR>α : Type u_1<VAR>s : Setoid α<GOAL>Set.range Quotient.mk' = Set.univ
<VAR>α : Type u_1<VAR>sa : Setoid α<GOAL>Set.range Quotient.mk'' = Set.univ
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>f : ι → α<VAR>s : Setoid ι<VAR>hf : ∀ (a b : ι), Setoid.r a b → f a = f b<GOAL>(Set.range fun x => x.liftOn' f hf) = Set.range f
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>c : α<GOAL>(Set.range fun x => c) ⊆ {c}
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>Nonempty ι<VAR>c : α<GOAL>(Set.range fun x => c) = {c}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α → Prop<VAR>q : β → Prop<VAR>f : α → β<VAR>h : ∀ (x : α), p x → q (f x)<GOAL>Set.range (Subtype.map f h) = Subtype.val ⁻¹' (f '' {x | p x})
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Set.image Prod.swap = Set.preimage Prod.swap
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>y : β<GOAL>(f ⁻¹' {y}).Nonempty ↔ y ∈ Set.range f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>y : β<GOAL>f ⁻¹' {y} = ∅ ↔ y ∉ Set.range f
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>f : ι → α<VAR>x : α<GOAL>Set.range f ⊆ {x} ↔ f = Function.const ι x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set β<GOAL>f '' (f ⁻¹' s)ᶜ = Set.range f \ s
<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>f : ι → β<GOAL>Subtype.val ∘ Set.rangeFactorization f = f
<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>f : ι → β<VAR>a : ι<GOAL>↑(Set.rangeFactorization f a) = f a
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>f : ι → α<GOAL>Function.Surjective (Set.rangeFactorization f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<GOAL>f '' s = Set.range fun x => f ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α ⊕ β → γ<GOAL>Set.range f = Set.range (f ∘ Sum.inl) ∪ Set.range (f ∘ Sum.inr)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → γ<VAR>g : β → γ<GOAL>Set.range (Sum.elim f g) = Set.range f ∪ Set.range g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : Prop<VAR>Decidable p<VAR>f g : α → β<GOAL>Set.range (if p then f else g) ⊆ Set.range f ∪ Set.range g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f g : α → β<GOAL>(Set.range fun x => if p x then f x else g x) ⊆ Set.range f ∪ Set.range g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>f ⁻¹' Set.range f = Set.univ
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>f : ι → α<VAR>h : Unique ι<GOAL>Set.range f = {f default}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<GOAL>Set.range f \ f '' s ⊆ f '' sᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>H : Function.Injective f<VAR>s : Set α<GOAL>Set.range f \ f '' s = f '' sᶜ
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : s ⊆ t<GOAL>Set.range (Set.inclusion h) = {x | ↑x ∈ s}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>Function.LeftInverse (Set.rangeFactorization f) (Set.rangeSplitting f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>Function.Injective (Set.rangeSplitting f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>h : Function.Injective f<GOAL>Function.RightInverse (Set.rangeFactorization f) (Set.rangeSplitting f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>Set.preimage (Set.rangeSplitting f) = Set.image (Set.rangeFactorization f)
<VAR>α : Type u_6<GOAL>IsCompl (Set.range some) {none}
<VAR>α : Type u_6<GOAL>(Set.range some)ᶜ = {none}
<VAR>α : Type u_6<GOAL>Set.range some ∩ {none} = ∅
<VAR>α : Type u_6<GOAL>Set.range some ∪ {none} = Set.univ
<VAR>α : Type u_6<GOAL>insert none (Set.range some) = Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>hs : s.Subsingleton<VAR>f : α → β<GOAL>(f '' s).Subsingleton
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set β<VAR>hs : s.Subsingleton<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>(f ⁻¹' s).Subsingleton
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>s : Set α<VAR>hs : (f '' s).Subsingleton<GOAL>s.Subsingleton
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Surjective f<VAR>s : Set β<VAR>hs : (f ⁻¹' s).Subsingleton<GOAL>s.Subsingleton
<VAR>β : Type u_2<VAR>α : Sort u_6<VAR>Subsingleton α<VAR>f : α → β<GOAL>(Set.range f).Subsingleton
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set β<VAR>hs : s.Nontrivial<VAR>f : α → β<VAR>hf : Function.Surjective f<GOAL>(f ⁻¹' s).Nontrivial
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>hs : s.Nontrivial<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>(f '' s).Nontrivial
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<VAR>hs : (f '' s).Nontrivial<GOAL>s.Nontrivial
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>(f '' s).Nontrivial ↔ s.Nontrivial
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>s : Set β<VAR>hs : (f ⁻¹' s).Nontrivial<GOAL>s.Nontrivial
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Surjective f<GOAL>Function.Injective (Set.preimage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>s : Set α<GOAL>f ⁻¹' (f '' s) = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>Function.Surjective (Set.preimage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>s : Set α<GOAL>(f '' s).Subsingleton ↔ s.Subsingleton
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Surjective f<VAR>s : Set β<GOAL>f '' (f ⁻¹' s) = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Surjective f<GOAL>Function.Surjective (Set.image f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Surjective f<VAR>s : Set β<GOAL>(f ⁻¹' s).Nonempty ↔ s.Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>Function.Injective (Set.image f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s t : Set β<VAR>hf : Function.Surjective f<GOAL>f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t
<VAR>α : Type u_1<VAR>ι : Sort u_3<VAR>ι' : Sort u_4<VAR>f : ι → ι'<VAR>hf : Function.Surjective f<VAR>g : ι' → α<GOAL>Set.range (g ∘ f) = Set.range g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>b : β<GOAL>b ∈ Set.range f ↔ ∃! a, f a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>b : β<VAR>hb : b ∈ Set.range f<GOAL>∃! a, f a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>s : Set α<GOAL>(f '' s)ᶜ = f '' sᶜ ∪ (Set.range f)ᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>g : β → α<VAR>h : Function.LeftInverse g f<VAR>s : Set α<GOAL>g '' (f '' s) = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>g : β → α<VAR>h : Function.LeftInverse g f<VAR>s : Set α<GOAL>f ⁻¹' (g ⁻¹' s) = s
<VAR>α : Type u_1<VAR>f : α → α<VAR>hf : Function.Involutive f<GOAL>Function.Involutive (Set.preimage f)
<VAR>ι : Sort u_1<VAR>ι' : Sort u_2<VAR>E : Type u_3<VAR>EquivLike E ι ι'<VAR>α : Type u_4<VAR>f : ι' → α<VAR>e : E<GOAL>Set.range (f ∘ ⇑e) = Set.range f
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>s : Set (Subtype p)<GOAL>Subtype.val '' s = {x | ∃ (h : p x), ⟨x, h⟩ ∈ s}
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : t ⊆ s<GOAL>Subtype.val '' {x | ↑x ∈ t} = t
<VAR>α : Type u_1<VAR>s : Set α<GOAL>Set.range Subtype.val = s
<VAR>α : Type u_1<VAR>p : α → Prop<GOAL>Set.range Subtype.val = {x | p x}
<VAR>α : Type u_1<VAR>s : Set α<GOAL>Subtype.val ⁻¹' s = Set.univ
<VAR>α : Type u_1<VAR>s : Set α<VAR>t : Set ↑s<GOAL>Subtype.val '' t ⊆ s
<VAR>α : Type u_1<VAR>s : Set α<GOAL>Subtype.val '' Set.univ = s
<VAR>α : Type u_1<VAR>s t : Set α<GOAL>Subtype.val '' (Subtype.val ⁻¹' t) = s ∩ t
<VAR>α : Type u_1<VAR>s t u : Set α<GOAL>Subtype.val ⁻¹' t = Subtype.val ⁻¹' u ↔ s ∩ t = s ∩ u
<VAR>α : Type u_1<VAR>s t : Set α<GOAL>Subtype.val ⁻¹' (s ∩ t) = Subtype.val ⁻¹' t
<VAR>α : Type u_1<VAR>s t : Set α<GOAL>Subtype.val ⁻¹' (t ∩ s) = Subtype.val ⁻¹' t
<VAR>α : Type u_1<VAR>s t u : Set α<GOAL>Subtype.val ⁻¹' t ⊆ Subtype.val ⁻¹' u ↔ s ∩ t ⊆ s ∩ u
<VAR>α : Type u_1<VAR>t : Set α<VAR>p : Set α → Prop<GOAL>(∃ s, p (Subtype.val '' s)) ↔ ∃ s ⊆ t, p s
<VAR>α : Type u_1<VAR>t : Set α<VAR>p : Set α → Prop<GOAL>(∀ (s : Set ↑t), p (Subtype.val '' s)) ↔ ∀ s ⊆ t, p s
<VAR>α : Type u_1<VAR>s t : Set α<GOAL>(Subtype.val ⁻¹' t).Nonempty ↔ (s ∩ t).Nonempty
<VAR>α : Type u_1<VAR>s t : Set α<GOAL>Subtype.val ⁻¹' t = ∅ ↔ s ∩ t = ∅
<VAR>α : Type u_1<VAR>s : Set α<GOAL>Subtype.val ⁻¹' sᶜ = ∅
<VAR>α : Type u_1<VAR>s : Set α<GOAL>(fun x => ↑x) ⁻¹' s = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Option α → β<GOAL>Function.Injective f ↔ Function.Injective (f ∘ some) ∧ f none ∉ Set.range (f ∘ some)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Option α → β<GOAL>Set.range f = insert (f none) (Set.range (f ∘ some))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : WithBot α → β<GOAL>Set.range f = insert (f ⊥) (Set.range (f ∘ WithBot.some))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : WithTop α → β<GOAL>Set.range f = insert (f ⊤) (Set.range (f ∘ WithBot.some))
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<GOAL>Function.Injective (Set.preimage f) ↔ Function.Surjective f
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<GOAL>Function.Surjective (Set.preimage f) ↔ Function.Injective f
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<GOAL>Function.Surjective (Set.image f) ↔ Function.Surjective f
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<GOAL>Function.Injective (Set.image f) ↔ Function.Injective f