ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>m : Multiset α<GOAL>m.dedup.dedup = m.dedup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<GOAL>s.dedup = 0 ↔ s = 0
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<GOAL>{a}.dedup = {a}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>s ≤ t.dedup ↔ s ≤ t ∧ s.Nodup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<GOAL>s ≤ s.dedup ↔ s.Nodup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>s.dedup = t.dedup ↔ ∀ (a : α), a ∈ s ↔ a ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq α<VAR>DecidableEq β<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>s : Multiset α<GOAL>(Multiset.map f s).dedup = Multiset.map f s.dedup
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq α<VAR>DecidableEq β<VAR>f : α → β<VAR>s : Multiset α<GOAL>(Multiset.map f s.dedup).dedup = (Multiset.map f s).dedup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<VAR>n : ℕ<VAR>h0 : n ≠ 0<GOAL>(n • s).dedup = s.dedup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<VAR>hno : s.Nodup<GOAL>s ≤ t.dedup ↔ s ≤ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<VAR>h : s ⊆ t<GOAL>(s + t).dedup = t.dedup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<VAR>h : t ⊆ s<GOAL>(s + t).dedup = s.dedup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<VAR>h : s.Disjoint t<GOAL>(s + t).dedup = s.dedup + t.dedup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : List α<VAR>h : t ⊆ s<GOAL>(s ++ t).dedup.Perm s.dedup
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<GOAL>s.restrict f = f ∘ Subtype.val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<VAR>x : ↑s<GOAL>s.restrict f x = f ↑x
<VAR>α : Type u_1<VAR>π : α → Type u_5<VAR>f : (a : α) → π a<VAR>s : Set α<VAR>g : (a : ↑s) → π ↑a<GOAL>s.restrict f = g ↔ ∀ (a : α) (ha : a ∈ s), f a = g ⟨a, ha⟩
<VAR>α : Type u_1<VAR>π : α → Type u_5<VAR>s : Set α<VAR>f : (a : ↑s) → π ↑a<VAR>g : (a : α) → π a<GOAL>f = s.restrict g ↔ ∀ (a : α) (ha : a ∈ s), f ⟨a, ha⟩ = g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<GOAL>Set.range (s.restrict f) = f '' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s t : Set α<GOAL>s.restrict f '' (Subtype.val ⁻¹' t) = f '' (t ∩ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>(x : α) → Decidable (x ∈ s)<VAR>f : (a : α) → a ∈ s → β<VAR>g : (a : α) → a ∉ s → β<GOAL>(s.restrict fun a => if h : a ∈ s then f a h else g a h) = fun a => f ↑a ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>(x : α) → Decidable (x ∈ s)<VAR>f : (a : α) → a ∈ s → β<VAR>g : (a : α) → a ∉ s → β<GOAL>(sᶜ.restrict fun a => if h : a ∈ s then f a h else g a h) = fun a => g ↑a ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : α → β<VAR>s : Set α<VAR>(x : α) → Decidable (x ∈ s)<GOAL>(s.restrict fun a => if a ∈ s then f a else g a) = s.restrict f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : α → β<VAR>s : Set α<VAR>(x : α) → Decidable (x ∈ s)<GOAL>(sᶜ.restrict fun a => if a ∈ s then f a else g a) = sᶜ.restrict g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : α → β<VAR>s : Set α<VAR>(x : α) → Decidable (x ∈ s)<GOAL>s.restrict (s.piecewise f g) = s.restrict f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : α → β<VAR>s : Set α<VAR>(x : α) → Decidable (x ∈ s)<GOAL>sᶜ.restrict (s.piecewise f g) = sᶜ.restrict g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>g : α → γ<VAR>g' : β → γ<GOAL>(Set.range f).restrict (Function.extend f g g') = fun x => g (Exists.choose ⋯)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>g : α → γ<VAR>g' : β → γ<GOAL>(Set.range f)ᶜ.restrict (Function.extend f g g') = g' ∘ Subtype.val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>g : α → γ<VAR>g' : β → γ<GOAL>Set.range (Function.extend f g g') ⊆ Set.range g ∪ g' '' (Set.range f)ᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>g : α → γ<VAR>g' : β → γ<GOAL>Set.range (Function.extend f g g') = Set.range g ∪ g' '' (Set.range f)ᶜ
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>f : ι → α<VAR>s : Set α<VAR>h : ∀ (x : ι), f x ∈ s<VAR>x : ι<GOAL>↑(Set.codRestrict f s h x) = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>f : ι → α<VAR>g : α → β<VAR>b : Set α<VAR>h : ∀ (x : ι), f x ∈ b<GOAL>b.restrict g ∘ Set.codRestrict f b h = g ∘ f
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>f : ι → α<VAR>s : Set α<VAR>h : ∀ (x : ι), f x ∈ s<GOAL>Function.Injective (Set.codRestrict f s h) ↔ Function.Injective f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f₁ f₂ : α → β<GOAL>Set.EqOn f₁ f₂ ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f₁ f₂ : α → β<VAR>a : α<GOAL>Set.EqOn f₁ f₂ {a} ↔ f₁ a = f₂ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f₁ f₂ : α → β<GOAL>Set.EqOn f₁ f₂ Set.univ ↔ f₁ = f₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f₁ f₂ : α → β<GOAL>s.restrict f₁ = s.restrict f₂ ↔ Set.EqOn f₁ f₂ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f₁ f₂ : α → β<VAR>h : Set.EqOn f₁ f₂ s<GOAL>Set.EqOn f₂ f₁ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f₁ f₂ : α → β<GOAL>Set.EqOn f₁ f₂ s ↔ Set.EqOn f₂ f₁ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<GOAL>Set.EqOn f f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f₁ f₂ f₃ : α → β<VAR>h₁ : Set.EqOn f₁ f₂ s<VAR>h₂ : Set.EqOn f₂ f₃ s<GOAL>Set.EqOn f₁ f₃ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f₁ f₂ : α → β<VAR>heq : Set.EqOn f₁ f₂ s<GOAL>f₁ '' s = f₂ '' s
<VAR>α : Type u_1<VAR>s : Set α<VAR>f : α → α<VAR>h : Set.EqOn f id s<GOAL>f '' s = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f₁ f₂ : α → β<VAR>heq : Set.EqOn f₁ f₂ s<VAR>t : Set β<GOAL>s ∩ f₁ ⁻¹' t = s ∩ f₂ ⁻¹' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s₁ s₂ : Set α<VAR>f₁ f₂ : α → β<VAR>hs : s₁ ⊆ s₂<VAR>hf : Set.EqOn f₁ f₂ s₂<GOAL>Set.EqOn f₁ f₂ s₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s₁ s₂ : Set α<VAR>f₁ f₂ : α → β<GOAL>Set.EqOn f₁ f₂ (s₁ ∪ s₂) ↔ Set.EqOn f₁ f₂ s₁ ∧ Set.EqOn f₁ f₂ s₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s₁ s₂ : Set α<VAR>f₁ f₂ : α → β<VAR>h₁ : Set.EqOn f₁ f₂ s₁<VAR>h₂ : Set.EqOn f₁ f₂ s₂<GOAL>Set.EqOn f₁ f₂ (s₁ ∪ s₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Set α<VAR>f₁ f₂ : α → β<VAR>g : β → γ<VAR>h : Set.EqOn f₁ f₂ s<GOAL>Set.EqOn (g ∘ f₁) (g ∘ f₂) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_6<VAR>f : ι → α<VAR>g₁ g₂ : α → β<GOAL>Set.EqOn g₁ g₂ (Set.range f) ↔ g₁ ∘ f = g₂ ∘ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f₁ f₂ : α → β<VAR>Preorder α<VAR>Preorder β<VAR>h₁ : MonotoneOn f₁ s<VAR>h : Set.EqOn f₁ f₂ s<GOAL>MonotoneOn f₂ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f₁ f₂ : α → β<VAR>Preorder α<VAR>Preorder β<VAR>h₁ : AntitoneOn f₁ s<VAR>h : Set.EqOn f₁ f₂ s<GOAL>AntitoneOn f₂ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f₁ f₂ : α → β<VAR>Preorder α<VAR>Preorder β<VAR>h₁ : StrictMonoOn f₁ s<VAR>h : Set.EqOn f₁ f₂ s<GOAL>StrictMonoOn f₂ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f₁ f₂ : α → β<VAR>Preorder α<VAR>Preorder β<VAR>h₁ : StrictAntiOn f₁ s<VAR>h : Set.EqOn f₁ f₂ s<GOAL>StrictAntiOn f₂ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f₁ f₂ : α → β<VAR>Preorder α<VAR>Preorder β<VAR>h : Set.EqOn f₁ f₂ s<GOAL>MonotoneOn f₁ s ↔ MonotoneOn f₂ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f₁ f₂ : α → β<VAR>Preorder α<VAR>Preorder β<VAR>h : Set.EqOn f₁ f₂ s<GOAL>AntitoneOn f₁ s ↔ AntitoneOn f₂ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f₁ f₂ : α → β<VAR>Preorder α<VAR>Preorder β<VAR>h : Set.EqOn f₁ f₂ s<GOAL>StrictMonoOn f₁ s ↔ StrictMonoOn f₂ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f₁ f₂ : α → β<VAR>Preorder α<VAR>Preorder β<VAR>h : Set.EqOn f₁ f₂ s<GOAL>StrictAntiOn f₁ s ↔ StrictAntiOn f₂ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s s₂ : Set α<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>h : MonotoneOn f s<VAR>h' : s₂ ⊆ s<GOAL>MonotoneOn f s₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s s₂ : Set α<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>h : AntitoneOn f s<VAR>h' : s₂ ⊆ s<GOAL>AntitoneOn f s₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s s₂ : Set α<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>h : StrictMonoOn f s<VAR>h' : s₂ ⊆ s<GOAL>StrictMonoOn f s₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s s₂ : Set α<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>h : StrictAntiOn f s<VAR>h' : s₂ ⊆ s<GOAL>StrictAntiOn f s₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>h : MonotoneOn f s<GOAL>Monotone (f ∘ Subtype.val)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>h : AntitoneOn f s<GOAL>Antitone (f ∘ Subtype.val)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>h : StrictMonoOn f s<GOAL>StrictMono (f ∘ Subtype.val)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>h : StrictAntiOn f s<GOAL>StrictAnti (f ∘ Subtype.val)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>h : Set.MapsTo f s t<GOAL>Subtype.val ∘ Set.MapsTo.restrict f s t h = f ∘ Subtype.val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>h : Set.MapsTo f s t<VAR>x : ↑s<GOAL>↑(Set.MapsTo.restrict f s t h x) = f ↑x
<VAR>α : Type u_1<VAR>s : Set α<VAR>f : α → α<VAR>h : Set.MapsTo f s s<VAR>x : ↑s<VAR>k : ℕ<GOAL>↑((Set.MapsTo.restrict f s s h)^[k] x) = f^[k] ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>h : ∀ (x : ↑s), f ↑x ∈ t<GOAL>Set.codRestrict (s.restrict f) t h = Set.MapsTo.restrict f s t ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>h : Set.MapsTo f s t<GOAL>Set.MapsTo.restrict f s t h = Set.codRestrict (s.restrict f) t ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>h : Set.MapsTo f s t<GOAL>Subtype.val ∘ Set.MapsTo.restrict f s t h = s.restrict f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>h : Set.MapsTo f s t<GOAL>Set.range (Set.MapsTo.restrict f s t h) = Subtype.val ⁻¹' (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<GOAL>Set.MapsTo f s t ↔ ∃ g, ∀ (x : ↑s), f ↑x = ↑(g x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<GOAL>Set.MapsTo f s t ↔ f '' s ⊆ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>Set.MapsTo (Prod.map f f) (Set.diagonal α) (Set.diagonal β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>hf : Set.MapsTo f s t<GOAL>s ⊆ f ⁻¹' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : Set β<VAR>f : α → β<VAR>x : α<GOAL>Set.MapsTo f {x} t ↔ f x ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>t : Set β<GOAL>Set.MapsTo f ∅ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<GOAL>Set.MapsTo f s ∅ ↔ s = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>h : Set.MapsTo f s t<VAR>hs : s.Nonempty<GOAL>t.Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>h : Set.MapsTo f s t<GOAL>f '' s ⊆ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f₁ f₂ : α → β<VAR>h₁ : Set.MapsTo f₁ s t<VAR>h : Set.EqOn f₁ f₂ s<GOAL>Set.MapsTo f₂ s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>g₁ g₂ : β → γ<VAR>hg : Set.EqOn g₁ g₂ t<VAR>hf : Set.MapsTo f s t<GOAL>Set.EqOn (g₁ ∘ f) (g₂ ∘ f) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f₁ f₂ : α → β<VAR>H : Set.EqOn f₁ f₂ s<GOAL>Set.MapsTo f₁ s t ↔ Set.MapsTo f₂ s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Set α<VAR>t : Set β<VAR>p : Set γ<VAR>f : α → β<VAR>g : β → γ<VAR>h₁ : Set.MapsTo g t p<VAR>h₂ : Set.MapsTo f s t<GOAL>Set.MapsTo (g ∘ f) s p
<VAR>α : Type u_1<VAR>s : Set α<GOAL>Set.MapsTo id s s
<VAR>α : Type u_1<VAR>f : α → α<VAR>s : Set α<VAR>h : Set.MapsTo f s s<VAR>n : ℕ<GOAL>Set.MapsTo f^[n] s s
<VAR>α : Type u_1<VAR>f : α → α<VAR>s : Set α<VAR>h : Set.MapsTo f s s<VAR>n : ℕ<GOAL>(Set.MapsTo.restrict f s s h)^[n] = Set.MapsTo.restrict f^[n] s s ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>Subsingleton β<VAR>f : α → β<VAR>h : s.Nonempty → t.Nonempty<GOAL>Set.MapsTo f s t
<VAR>α : Type u_1<VAR>Subsingleton α<VAR>f : α → α<VAR>s : Set α<GOAL>Set.MapsTo f s s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s₁ s₂ : Set α<VAR>t₁ t₂ : Set β<VAR>f : α → β<VAR>hf : Set.MapsTo f s₁ t₁<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₁ ⊆ t₂<GOAL>Set.MapsTo f s₂ t₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s₁ s₂ : Set α<VAR>t : Set β<VAR>f : α → β<VAR>hf : Set.MapsTo f s₁ t<VAR>hs : s₂ ⊆ s₁<GOAL>Set.MapsTo f s₂ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t₁ t₂ : Set β<VAR>f : α → β<VAR>hf : Set.MapsTo f s t₁<VAR>ht : t₁ ⊆ t₂<GOAL>Set.MapsTo f s t₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s₁ s₂ : Set α<VAR>t₁ t₂ : Set β<VAR>f : α → β<VAR>h₁ : Set.MapsTo f s₁ t₁<VAR>h₂ : Set.MapsTo f s₂ t₂<GOAL>Set.MapsTo f (s₁ ∪ s₂) (t₁ ∪ t₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s₁ s₂ : Set α<VAR>t : Set β<VAR>f : α → β<VAR>h₁ : Set.MapsTo f s₁ t<VAR>h₂ : Set.MapsTo f s₂ t<GOAL>Set.MapsTo f (s₁ ∪ s₂) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s₁ s₂ : Set α<VAR>t : Set β<VAR>f : α → β<GOAL>Set.MapsTo f (s₁ ∪ s₂) t ↔ Set.MapsTo f s₁ t ∧ Set.MapsTo f s₂ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t₁ t₂ : Set β<VAR>f : α → β<VAR>h₁ : Set.MapsTo f s t₁<VAR>h₂ : Set.MapsTo f s t₂<GOAL>Set.MapsTo f s (t₁ ∩ t₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s₁ s₂ : Set α<VAR>t₁ t₂ : Set β<VAR>f : α → β<VAR>h₁ : Set.MapsTo f s₁ t₁<VAR>h₂ : Set.MapsTo f s₂ t₂<GOAL>Set.MapsTo f (s₁ ∩ s₂) (t₁ ∩ t₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t₁ t₂ : Set β<VAR>f : α → β<GOAL>Set.MapsTo f s (t₁ ∩ t₂) ↔ Set.MapsTo f s t₁ ∧ Set.MapsTo f s t₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<GOAL>Set.MapsTo f s Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<GOAL>Set.MapsTo f s (Set.range f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>g : γ → α<VAR>s : Set γ<VAR>t : Set β<GOAL>Set.MapsTo f (g '' s) t ↔ Set.MapsTo (f ∘ g) s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>g : β → γ<VAR>hf : Set.MapsTo f s t<GOAL>Set.MapsTo (g ∘ f) s (g '' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>g : β → γ<VAR>s : Set β<VAR>t : Set γ<VAR>hg : Set.MapsTo g s t<VAR>f : α → β<GOAL>Set.MapsTo (g ∘ f) (f ⁻¹' s) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : Set β<VAR>f : α → β<GOAL>Set.MapsTo f Set.univ t ↔ ∀ (x : α), f x ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set β<GOAL>Set.MapsTo f Set.univ s ↔ ∀ (a : α), f a ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>t : Set β<VAR>f : α → β<VAR>g : ι → α<GOAL>Set.MapsTo f (Set.range g) t ↔ ∀ (i : ι), f (g i) ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>g : γ → α<VAR>s : Set β<GOAL>Set.MapsTo f (Set.range g) s ↔ Set.MapsTo (f ∘ g) Set.univ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<GOAL>Function.Surjective (Set.MapsTo.restrict f s (f '' s) ⋯)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>h : Set.MapsTo f s t<VAR>hc : Set.MapsTo f sᶜ tᶜ<VAR>x : α<GOAL>f x ∈ t ↔ x ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<GOAL>t.restrictPreimage f '' (Subtype.val ⁻¹' s) = Subtype.val ⁻¹' (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : Set β<VAR>f : α → β<GOAL>Set.range (t.restrictPreimage f) = Subtype.val ⁻¹' Set.range f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : Set β<VAR>f : α → β<VAR>a : α<VAR>h : a ∈ f ⁻¹' t<GOAL>t.restrictPreimage f ⟨a, h⟩ = ⟨f a, h⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : Set β<VAR>f : α → β<VAR>u : Set ↑t<GOAL>Subtype.val '' (t.restrictPreimage f ⁻¹' u) = f ⁻¹' (Subtype.val '' u)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : Set β<VAR>f : α → β<VAR>u : Set ↑t<GOAL>t.restrictPreimage f ⁻¹' u = (fun a => f ↑a) ⁻¹' (Subtype.val '' u)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : Set β<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>Function.Injective (t.restrictPreimage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : Set β<VAR>f : α → β<VAR>hf : Function.Surjective f<GOAL>Function.Surjective (t.restrictPreimage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : Set β<VAR>f : α → β<VAR>hf : Function.Bijective f<GOAL>Function.Bijective (t.restrictPreimage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>hs : s.Subsingleton<VAR>f : α → β<GOAL>Set.InjOn f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>Set.InjOn f ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>a : α<GOAL>Set.InjOn f {a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>a b : α<GOAL>Set.InjOn f {a, b} ↔ f a = f b → a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<VAR>x y : α<VAR>h : Set.InjOn f s<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>f x = f y ↔ x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<VAR>x y : α<VAR>h : Set.InjOn f s<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>f x ≠ f y ↔ x ≠ y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f₁ f₂ : α → β<VAR>h₁ : Set.InjOn f₁ s<VAR>h : Set.EqOn f₁ f₂ s<GOAL>Set.InjOn f₂ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f₁ f₂ : α → β<VAR>H : Set.EqOn f₁ f₂ s<GOAL>Set.InjOn f₁ s ↔ Set.InjOn f₂ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s₁ s₂ : Set α<VAR>f : α → β<VAR>h : s₁ ⊆ s₂<VAR>ht : Set.InjOn f s₂<GOAL>Set.InjOn f s₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s₁ s₂ : Set α<VAR>f : α → β<VAR>h : Disjoint s₁ s₂<GOAL>Set.InjOn f (s₁ ∪ s₂) ↔ Set.InjOn f s₁ ∧ Set.InjOn f s₂ ∧ ∀ x ∈ s₁, ∀ y ∈ s₂, f x ≠ f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>has : a ∉ s<GOAL>Set.InjOn f (insert a s) ↔ Set.InjOn f s ∧ f a ∉ f '' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>Function.Injective f ↔ Set.InjOn f Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>h : Function.Injective f<VAR>s : Set α<GOAL>Set.InjOn f s
<VAR>γ : Type u_3<VAR>p : Set γ<VAR>s : Set { x // p x }<GOAL>Set.InjOn Subtype.val s
<VAR>α : Type u_1<VAR>s : Set α<GOAL>Set.InjOn id s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>g : β → γ<VAR>hg : Set.InjOn g t<VAR>hf : Set.InjOn f s<VAR>h : Set.MapsTo f s t<GOAL>Set.InjOn (g ∘ f) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Set α<VAR>f : α → β<VAR>g : β → γ<VAR>h : Set.InjOn (g ∘ f) s<GOAL>Set.InjOn g (f '' s)
<VAR>α : Type u_1<VAR>f : α → α<VAR>s : Set α<VAR>h : Set.InjOn f s<VAR>hf : Set.MapsTo f s s<VAR>n : ℕ<GOAL>Set.InjOn f^[n] s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Subsingleton α<VAR>f : α → β<VAR>s : Set α<GOAL>Set.InjOn f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>g : β → γ<VAR>h : Function.Injective (g ∘ f)<GOAL>Set.InjOn g (Set.range f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<GOAL>Set.InjOn f s ↔ Function.Injective (s.restrict f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>h : Set.MapsTo f s t<GOAL>Function.Injective (Set.MapsTo.restrict f s t h) ↔ Set.InjOn f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>Nonempty β<GOAL>(∃ f, Set.InjOn f s) ↔ ∃ f, Function.Injective f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>B : Set (Set β)<VAR>hB : B ⊆ 𝒫 Set.range f<GOAL>Set.InjOn (Set.preimage f) B
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s s₁ : Set α<VAR>f : α → β<VAR>x : α<VAR>hf : Set.InjOn f s<VAR>hs : s₁ ⊆ s<VAR>h : x ∈ s<VAR>h₁ : f x ∈ f '' s₁<GOAL>x ∈ s₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s s₁ : Set α<VAR>f : α → β<VAR>x : α<VAR>hf : Set.InjOn f s<VAR>hs : s₁ ⊆ s<VAR>hx : x ∈ s<GOAL>f x ∈ f '' s₁ ↔ x ∈ s₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s s₁ : Set α<VAR>f : α → β<VAR>hf : Set.InjOn f s<VAR>hs : s₁ ⊆ s<GOAL>f ⁻¹' (f '' s₁) ∩ s = s₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Set α<VAR>t : Set β<VAR>f₁ f₂ : α → β<VAR>g : β → γ<VAR>h : Set.EqOn (g ∘ f₁) (g ∘ f₂) s<VAR>hg : Set.InjOn g t<VAR>hf₁ : Set.MapsTo f₁ s t<VAR>hf₂ : Set.MapsTo f₂ s t<GOAL>Set.EqOn f₁ f₂ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Set α<VAR>t : Set β<VAR>f₁ f₂ : α → β<VAR>g : β → γ<VAR>hg : Set.InjOn g t<VAR>hf₁ : Set.MapsTo f₁ s t<VAR>hf₂ : Set.MapsTo f₂ s t<GOAL>Set.EqOn (g ∘ f₁) (g ∘ f₂) s ↔ Set.EqOn f₁ f₂ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s t u : Set α<VAR>hf : Set.InjOn f u<VAR>hs : s ⊆ u<VAR>ht : t ⊆ u<GOAL>f '' (s ∩ t) = f '' s ∩ f '' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<VAR>h : Set.InjOn f s<GOAL>Set.InjOn (Set.image f) (𝒫 s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s s₁ s₂ : Set α<VAR>f : α → β<VAR>h : Set.InjOn f s<VAR>h₁ : s₁ ⊆ s<VAR>h₂ : s₂ ⊆ s<GOAL>f '' s₁ = f '' s₂ ↔ s₁ = s₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s s₁ s₂ : Set α<VAR>f : α → β<VAR>h : Set.InjOn f s<VAR>h₁ : s₁ ⊆ s<VAR>h₂ : s₂ ⊆ s<GOAL>f '' s₁ ⊆ f '' s₂ ↔ s₁ ⊆ s₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s s₁ s₂ : Set α<VAR>f : α → β<VAR>h : Set.InjOn f s<VAR>h₁ : s₁ ⊆ s<VAR>h₂ : s₂ ⊆ s<GOAL>f '' s₁ ⊂ f '' s₂ ↔ s₁ ⊂ s₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t u : Set α<VAR>f : α → β<VAR>h : Disjoint s t<VAR>hf : Set.InjOn f u<VAR>hs : s ⊆ u<VAR>ht : t ⊆ u<GOAL>Disjoint (f '' s) (f '' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<VAR>t : Set α<VAR>h : Set.InjOn f s<GOAL>f '' (s \ t) = f '' s \ f '' (s ∩ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<VAR>t : Set α<VAR>h : Set.InjOn f s<VAR>hst : t ⊆ s<GOAL>f '' (s \ t) = f '' s \ f '' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<VAR>h : Set.InjOn f s<GOAL>Function.Injective (Set.imageFactorization f s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<GOAL>Function.Injective (Set.imageFactorization f s) ↔ Set.InjOn f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>Set.graphOn f ∅ = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s t : Set α<GOAL>Set.graphOn f (s ∪ t) = Set.graphOn f s ∪ Set.graphOn f t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>x : α<GOAL>Set.graphOn f {x} = {(x, f x)}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>x : α<VAR>s : Set α<GOAL>Set.graphOn f (insert x s) = insert (x, f x) (Set.graphOn f s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<GOAL>Prod.fst '' Set.graphOn f s = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Nonempty β<VAR>s : Set (α × β)<GOAL>(∃ f, s = Set.graphOn f (Prod.fst '' s)) ↔ Set.InjOn Prod.fst s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Nonempty β<VAR>s : Set (α × β)<GOAL>(∃ f t, s = Set.graphOn f t) ↔ Set.InjOn Prod.fst s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>h : Set.SurjOn f s t<GOAL>t ⊆ Set.range f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<GOAL>Set.SurjOn f s t ↔ ∃ t' g, t ⊆ t' ∧ Function.Surjective g ∧ ∀ (x : ↑s), f ↑x = ↑(g x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<GOAL>Set.SurjOn f s ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : Set β<VAR>f : α → β<GOAL>Set.SurjOn f ∅ t ↔ t = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<VAR>b : β<GOAL>Set.SurjOn f s {b} ↔ b ∈ f '' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<GOAL>Set.SurjOn f s (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>h : Set.SurjOn f s t<VAR>ht : t.Nonempty<GOAL>s.Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f₁ f₂ : α → β<VAR>h : Set.SurjOn f₁ s t<VAR>H : Set.EqOn f₁ f₂ s<GOAL>Set.SurjOn f₂ s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f₁ f₂ : α → β<VAR>h : Set.EqOn f₁ f₂ s<GOAL>Set.SurjOn f₁ s t ↔ Set.SurjOn f₂ s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s₁ s₂ : Set α<VAR>t₁ t₂ : Set β<VAR>f : α → β<VAR>hs : s₁ ⊆ s₂<VAR>ht : t₁ ⊆ t₂<VAR>hf : Set.SurjOn f s₁ t₂<GOAL>Set.SurjOn f s₂ t₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t₁ t₂ : Set β<VAR>f : α → β<VAR>h₁ : Set.SurjOn f s t₁<VAR>h₂ : Set.SurjOn f s t₂<GOAL>Set.SurjOn f s (t₁ ∪ t₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s₁ s₂ : Set α<VAR>t₁ t₂ : Set β<VAR>f : α → β<VAR>h₁ : Set.SurjOn f s₁ t₁<VAR>h₂ : Set.SurjOn f s₂ t₂<GOAL>Set.SurjOn f (s₁ ∪ s₂) (t₁ ∪ t₂)