ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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₂<VAR>h : Set.InjOn f (s₁ ∪ s₂)<GOAL>Set.SurjOn 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.SurjOn f s₁ t<VAR>h₂ : Set.SurjOn f s₂ t<VAR>h : Set.InjOn f (s₁ ∪ s₂)<GOAL>Set.SurjOn f (s₁ ∩ s₂) t
<VAR>α : Type u_1<VAR>s : Set α<GOAL>Set.SurjOn id s s
<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>hg : Set.SurjOn g t p<VAR>hf : Set.SurjOn f s t<GOAL>Set.SurjOn (g ∘ f) s p
<VAR>α : Type u_1<VAR>f : α → α<VAR>s : Set α<VAR>h : Set.SurjOn f s s<VAR>n : ℕ<GOAL>Set.SurjOn f^[n] s s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>hf : Set.SurjOn f s t<VAR>g : β → γ<GOAL>Set.SurjOn (g ∘ f) s (g '' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>g : β → γ<VAR>s : Set β<VAR>t : Set γ<VAR>hf : Function.Surjective f<VAR>hg : Set.SurjOn g s t<GOAL>Set.SurjOn (g ∘ f) (f ⁻¹' s) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>Subsingleton β<VAR>f : α → β<VAR>h : t.Nonempty → s.Nonempty<GOAL>Set.SurjOn f s t
<VAR>α : Type u_1<VAR>Subsingleton α<VAR>f : α → α<VAR>s : Set α<GOAL>Set.SurjOn f s s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>Function.Surjective f ↔ Set.SurjOn f Set.univ Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<GOAL>Set.SurjOn f s Set.univ ↔ Function.Surjective (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.Surjective (Set.MapsTo.restrict f s t h) ↔ Set.SurjOn f s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>h₁ : Set.SurjOn f s t<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 : α → β<GOAL>f '' s = t ↔ Set.SurjOn 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.SurjOn f s t<VAR>ht : t₁ ⊆ t<GOAL>f '' (f ⁻¹' t₁) = t₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>h : Set.SurjOn f s t<VAR>h' : Function.Injective f<GOAL>Set.MapsTo 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<VAR>h' : Function.Surjective f<GOAL>Set.SurjOn 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>hf : Set.EqOn (g₁ ∘ f) (g₂ ∘ f) s<VAR>hf' : Set.SurjOn f s t<GOAL>Set.EqOn g₁ g₂ 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>hf : Set.SurjOn f s t<VAR>hf' : Set.MapsTo f s t<GOAL>Set.EqOn (g₁ ∘ f) (g₂ ∘ f) s ↔ Set.EqOn g₁ g₂ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Set α<VAR>f : α → β<VAR>g₁ g₂ : β → γ<GOAL>Set.EqOn (g₁ ∘ f) (g₂ ∘ f) s ↔ Set.EqOn g₁ g₂ (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>p : β → Prop<VAR>hf : Set.SurjOn f s t<VAR>hf' : Set.MapsTo f s t<GOAL>(∀ y ∈ t, p y) ↔ ∀ x ∈ s, p (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>h : Set.BijOn f s t<GOAL>Set.MapsTo f s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>h : Set.BijOn f s t<GOAL>Set.InjOn f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>h : Set.BijOn f s t<GOAL>Set.SurjOn 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<VAR>h₂ : Set.InjOn f s<VAR>h₃ : Set.SurjOn f s t<GOAL>Set.BijOn f s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>Set.BijOn f ∅ ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<GOAL>Set.BijOn f s ∅ ↔ s = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : Set β<VAR>f : α → β<GOAL>Set.BijOn f ∅ t ↔ t = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>a : α<VAR>b : β<GOAL>Set.BijOn f {a} {b} ↔ f a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s₁ s₂ : Set α<VAR>t₁ t₂ : Set β<VAR>f : α → β<VAR>h₁ : Set.BijOn f s₁ t₁<VAR>h₂ : Set.MapsTo f s₂ t₂<VAR>h₃ : s₁ ∩ f ⁻¹' t₂ ⊆ s₂<GOAL>Set.BijOn f (s₁ ∩ 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.BijOn f s₂ t₂<VAR>h₃ : s₂ ∩ f ⁻¹' t₁ ⊆ s₁<GOAL>Set.BijOn f (s₁ ∩ s₂) (t₁ ∩ t₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s₁ s₂ : Set α<VAR>t₁ t₂ : Set β<VAR>f : α → β<VAR>h₁ : Set.BijOn f s₁ t₁<VAR>h₂ : Set.BijOn f s₂ t₂<VAR>h : Set.InjOn f (s₁ ∪ s₂)<GOAL>Set.BijOn f (s₁ ∩ s₂) (t₁ ∩ t₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s₁ s₂ : Set α<VAR>t₁ t₂ : Set β<VAR>f : α → β<VAR>h₁ : Set.BijOn f s₁ t₁<VAR>h₂ : Set.BijOn f s₂ t₂<VAR>h : Set.InjOn f (s₁ ∪ s₂)<GOAL>Set.BijOn f (s₁ ∪ s₂) (t₁ ∪ t₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>h : Set.BijOn f s t<GOAL>t ⊆ Set.range f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<VAR>h : Set.InjOn f s<GOAL>Set.BijOn f s (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f₁ f₂ : α → β<VAR>h₁ : Set.BijOn f₁ s t<VAR>h : Set.EqOn f₁ f₂ s<GOAL>Set.BijOn 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.BijOn f₁ s t ↔ Set.BijOn f₂ s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>h : Set.BijOn f s t<GOAL>f '' s = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>p : β → Prop<VAR>hf : Set.BijOn f s t<GOAL>(∀ b ∈ t, p b) ↔ ∀ a ∈ s, p (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>p : β → Prop<VAR>hf : Set.BijOn f s t<GOAL>(∃ b ∈ t, p b) ↔ ∃ a ∈ s, p (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>e : α ≃ β<GOAL>⇑e '' s = t ↔ Set.BijOn (⇑e) s t
<VAR>α : Type u_1<VAR>s : Set α<GOAL>Set.BijOn id s s
<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>hg : Set.BijOn g t p<VAR>hf : Set.BijOn f s t<GOAL>Set.BijOn (g ∘ f) s p
<VAR>α : Type u_1<VAR>f : α → α<VAR>s : Set α<VAR>h : Set.BijOn f s s<VAR>n : ℕ<GOAL>Set.BijOn f^[n] s s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>Subsingleton α<VAR>Subsingleton β<VAR>f : α → β<VAR>h : s.Nonempty ↔ t.Nonempty<GOAL>Set.BijOn f s t
<VAR>α : Type u_1<VAR>Subsingleton α<VAR>f : α → α<VAR>s : Set α<GOAL>Set.BijOn f s s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>h : Set.BijOn f s t<GOAL>Function.Bijective (Set.MapsTo.restrict f s t ⋯)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>Function.Bijective f ↔ Set.BijOn f Set.univ Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>hst : Set.BijOn f s t<VAR>hf : Function.Bijective f<GOAL>Set.BijOn f sᶜ tᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>r : Set β<VAR>hf : Set.BijOn f s t<VAR>hrt : r ⊆ t<GOAL>Set.BijOn f (s ∩ f ⁻¹' r) r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>r : Set α<VAR>hf : Set.BijOn f s t<VAR>hrs : r ⊆ s<GOAL>Set.BijOn f r (f '' r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<VAR>f' : β → α<VAR>h : Set.LeftInvOn f' f s<GOAL>Set.EqOn (f' ∘ f) id s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<VAR>f' : β → α<VAR>h : Set.LeftInvOn f' f s<VAR>x : α<VAR>hx : x ∈ s<GOAL>f' (f x) = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<VAR>f₁' f₂' : β → α<VAR>h₁ : Set.LeftInvOn f₁' f s<VAR>t : Set β<VAR>h₁' : Set.MapsTo f s t<VAR>heq : Set.EqOn f₁' f₂' t<GOAL>Set.LeftInvOn f₂' f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f₁ f₂ : α → β<VAR>f₁' : β → α<VAR>h₁ : Set.LeftInvOn f₁' f₁ s<VAR>heq : Set.EqOn f₁ f₂ s<GOAL>Set.LeftInvOn f₁' f₂ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<VAR>f₁' : β → α<VAR>h : Set.LeftInvOn f₁' f s<GOAL>Set.InjOn f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>f' : β → α<VAR>h : Set.LeftInvOn f' f s<VAR>hf : Set.MapsTo f s t<GOAL>Set.SurjOn f' t s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>f' : β → α<VAR>h : Set.LeftInvOn f' f s<VAR>hf : Set.SurjOn f s t<GOAL>Set.MapsTo f' t s
<VAR>α : Type u_1<VAR>s : Set α<GOAL>Set.LeftInvOn id 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>f' : β → α<VAR>g' : γ → β<VAR>hf' : Set.LeftInvOn f' f s<VAR>hg' : Set.LeftInvOn g' g t<VAR>hf : Set.MapsTo f s t<GOAL>Set.LeftInvOn (f' ∘ g') (g ∘ f) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s s₁ : Set α<VAR>f : α → β<VAR>f' : β → α<VAR>hf : Set.LeftInvOn f' f s<VAR>ht : s₁ ⊆ s<GOAL>Set.LeftInvOn f' f s₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s s₁ : Set α<VAR>f : α → β<VAR>f' : β → α<VAR>hf : Set.LeftInvOn f' f s<GOAL>f '' (s₁ ∩ s) = f' ⁻¹' s₁ ∩ f '' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s s₁ : Set α<VAR>f : α → β<VAR>f' : β → α<VAR>hf : Set.LeftInvOn f' f s<GOAL>f '' (s₁ ∩ s) = f' ⁻¹' (s₁ ∩ s) ∩ f '' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<VAR>f' : β → α<VAR>hf : Set.LeftInvOn f' f s<GOAL>f' '' (f '' s) = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s s₁ : Set α<VAR>f : α → β<VAR>f' : β → α<VAR>hf : Set.LeftInvOn f' f s<VAR>hs : s₁ ⊆ s<GOAL>f' '' (f '' s₁) = s₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : Set β<VAR>f : α → β<VAR>f' : β → α<VAR>h : Set.RightInvOn f' f t<GOAL>Set.EqOn (f ∘ f') id t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : Set β<VAR>f : α → β<VAR>f' : β → α<VAR>h : Set.RightInvOn f' f t<VAR>y : β<VAR>hy : y ∈ t<GOAL>f (f' y) = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<VAR>f' : β → α<VAR>h : Set.LeftInvOn f' f s<GOAL>Set.RightInvOn f' f (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : Set β<VAR>f : α → β<VAR>f₁' f₂' : β → α<VAR>h₁ : Set.RightInvOn f₁' f t<VAR>heq : Set.EqOn f₁' f₂' t<GOAL>Set.RightInvOn f₂' f t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f₁ f₂ : α → β<VAR>f' : β → α<VAR>h₁ : Set.RightInvOn f' f₁ t<VAR>hg : Set.MapsTo f' t s<VAR>heq : Set.EqOn f₁ f₂ s<GOAL>Set.RightInvOn f' f₂ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>f' : β → α<VAR>hf : Set.RightInvOn f' f t<VAR>hf' : Set.MapsTo f' t s<GOAL>Set.SurjOn f s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>f' : β → α<VAR>h : Set.RightInvOn f' f t<VAR>hf : Set.SurjOn f' t s<GOAL>Set.MapsTo f s t
<VAR>α : Type u_1<VAR>s : Set α<GOAL>Set.RightInvOn id id s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Set β<VAR>p : Set γ<VAR>f : α → β<VAR>g : β → γ<VAR>f' : β → α<VAR>g' : γ → β<VAR>hf : Set.RightInvOn f' f t<VAR>hg : Set.RightInvOn g' g p<VAR>g'pt : Set.MapsTo g' p t<GOAL>Set.RightInvOn (f' ∘ g') (g ∘ f) p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t t₁ : Set β<VAR>f : α → β<VAR>f' : β → α<VAR>hf : Set.RightInvOn f' f t<VAR>ht : t₁ ⊆ t<GOAL>Set.RightInvOn f' f t₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>f' : β → α<VAR>hf : Set.InjOn f s<VAR>hf' : Set.LeftInvOn f f' t<VAR>h₁ : Set.MapsTo f s t<VAR>h₂ : Set.MapsTo f' t s<GOAL>Set.RightInvOn f f' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>f₁' f₂' : β → α<VAR>h₁ : Set.LeftInvOn f₁' f s<VAR>h₂ : Set.RightInvOn f₂' f t<VAR>h : Set.MapsTo f₂' t s<GOAL>Set.EqOn f₁' f₂' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>f' : β → α<VAR>hf : Set.SurjOn f s t<VAR>hf' : Set.RightInvOn f f' s<GOAL>Set.LeftInvOn f f' t
<VAR>α : Type u_1<VAR>s : Set α<GOAL>Set.InvOn id id s s
<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>f' : β → α<VAR>g' : γ → β<VAR>hf : Set.InvOn f' f s t<VAR>hg : Set.InvOn g' g t p<VAR>fst : Set.MapsTo f s t<VAR>g'pt : Set.MapsTo g' p t<GOAL>Set.InvOn (f' ∘ g') (g ∘ f) s p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>f' : β → α<VAR>h : Set.InvOn f' f s t<GOAL>Set.InvOn f f' t s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s s₁ : Set α<VAR>t t₁ : Set β<VAR>f : α → β<VAR>f' : β → α<VAR>h : Set.InvOn f' f s t<VAR>hs : s₁ ⊆ s<VAR>ht : t₁ ⊆ t<GOAL>Set.InvOn f' f s₁ t₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>f' : β → α<VAR>h : Set.InvOn f' f s t<VAR>hf : Set.MapsTo f s t<VAR>hf' : Set.MapsTo f' t s<GOAL>Set.BijOn f s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Nonempty α<VAR>s : Set α<VAR>f : α → β<VAR>b : β<VAR>h : ∃ a ∈ s, f a = b<GOAL>Function.invFunOn f s b ∈ s ∧ f (Function.invFunOn f s b) = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Nonempty α<VAR>s : Set α<VAR>f : α → β<VAR>b : β<VAR>h : ∃ a ∈ s, f a = b<GOAL>Function.invFunOn f s b ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Nonempty α<VAR>s : Set α<VAR>f : α → β<VAR>b : β<VAR>h : ∃ a ∈ s, f a = b<GOAL>f (Function.invFunOn f s b) = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Nonempty α<VAR>s : Set α<VAR>f : α → β<VAR>b : β<VAR>h : ¬∃ a ∈ s, f a = b<GOAL>Function.invFunOn f s b = Classical.choice inst✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Nonempty α<VAR>s : Set α<VAR>f : α → β<VAR>a : α<VAR>h : a ∈ s<GOAL>Function.invFunOn f s (f a) ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Nonempty α<VAR>s : Set α<VAR>f : α → β<VAR>a : α<VAR>h : a ∈ s<GOAL>f (Function.invFunOn f s (f a)) = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<VAR>Nonempty α<VAR>h : Set.InjOn f s<GOAL>Set.LeftInvOn (Function.invFunOn f s) f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s₁ s₂ : Set α<VAR>f : α → β<VAR>Nonempty α<VAR>h : Set.InjOn f s₂<VAR>ht : s₁ ⊆ s₂<GOAL>Function.invFunOn f s₂ '' (f '' s₁) = s₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<VAR>Nonempty α<VAR>h : s ⊆ Function.invFunOn f s '' (f '' s)<GOAL>Set.LeftInvOn (Function.invFunOn f s) f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<VAR>Nonempty α<GOAL>Set.InjOn f s ↔ Function.invFunOn f s '' (f '' s) = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Nonempty α<VAR>f : α → β<VAR>s : Set α<GOAL>Set.InjOn (Function.invFunOn f s) (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Nonempty α<VAR>f : α → β<VAR>s : Set α<GOAL>Function.invFunOn f s '' (f '' s) ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>Nonempty α<VAR>h : Set.SurjOn f s t<GOAL>Set.RightInvOn (Function.invFunOn f s) f t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>Nonempty α<VAR>h : Set.BijOn f s t<GOAL>Set.InvOn (Function.invFunOn f s) f s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>Nonempty α<VAR>h : Set.SurjOn f s t<GOAL>Set.InvOn (Function.invFunOn f s) f (Function.invFunOn f s '' t) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>Nonempty α<VAR>h : Set.SurjOn f s t<GOAL>Set.MapsTo (Function.invFunOn f s) t s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>Nonempty α<VAR>r : Set β<VAR>hf : Set.SurjOn f s t<VAR>hrt : r ⊆ t<GOAL>f '' (Function.invFunOn f s '' r) = r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>Nonempty α<VAR>hf : Set.SurjOn f s t<GOAL>f '' (Function.invFunOn f s '' t) = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>Nonempty α<VAR>h : Set.SurjOn f s t<GOAL>Set.BijOn f (Function.invFunOn f s '' t) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<GOAL>Set.SurjOn f s t ↔ ∃ s' ⊆ s, Set.BijOn f s' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<GOAL>∃ s' ⊆ s, Set.BijOn f s' (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<GOAL>∃ u, f '' u = f '' s ∧ Set.InjOn f u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : Set β<VAR>f : α → β<VAR>ht : t ⊆ Set.range f<GOAL>∃ s, f '' s = t ∧ Set.InjOn f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s s₁ : Set α<VAR>t : Set β<VAR>f : α → β<VAR>t' : Set β<VAR>h : Set.BijOn f s t<VAR>hss₁ : s ⊆ s₁<VAR>htt' : t ⊆ t'<VAR>ht' : Set.SurjOn f s₁ t'<GOAL>∃ s', s ⊆ s' ∧ s' ⊆ s₁ ∧ Set.BijOn f s' t'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>t' : Set β<VAR>h : Set.BijOn f s t<VAR>htt' : t ⊆ t'<VAR>ht' : t' ⊆ Set.range f<GOAL>∃ s', s ⊆ s' ∧ Set.BijOn f s' t'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<VAR>r : Set α<VAR>hinj : Set.InjOn f r<VAR>hrs : r ⊆ s<GOAL>∃ u, r ⊆ u ∧ u ⊆ s ∧ f '' u = f '' s ∧ Set.InjOn f u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : Nonempty α<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>s : Set α<VAR>h : Classical.choice n ∈ s<GOAL>Function.invFun f ⁻¹' s = f '' s ∪ (Set.range f)ᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : Nonempty α<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>s : Set α<VAR>h : Classical.choice n ∉ s<GOAL>Function.invFun f ⁻¹' s = f '' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>g : β → α<VAR>h : Set.InvOn f g t s<VAR>hf : Set.BijOn f s t<GOAL>Set.BijOn g t s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>g : β → α<VAR>h : Set.InvOn f g t s<GOAL>Set.BijOn f s t ↔ Set.BijOn g t s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>h : Monotone f<VAR>s : Set α<GOAL>Monotone (s.restrict f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>h : Monotone f<VAR>s : Set β<VAR>hs : ∀ (x : α), f x ∈ s<GOAL>Monotone (Set.codRestrict f s hs)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>h : Monotone f<GOAL>Monotone (Set.rangeFactorization f)
<VAR>α : Type u_1<VAR>δ : α → Sort u_6<VAR>f g : (i : α) → δ i<VAR>(i : α) → Decidable (i ∈ ∅)<GOAL>∅.piecewise f g = g
<VAR>α : Type u_1<VAR>δ : α → Sort u_6<VAR>f g : (i : α) → δ i<VAR>(i : α) → Decidable (i ∈ Set.univ)<GOAL>Set.univ.piecewise f g = f
<VAR>α : Type u_1<VAR>δ : α → Sort u_6<VAR>s : Set α<VAR>f g : (i : α) → δ i<VAR>j : α<VAR>(i : α) → Decidable (i ∈ insert j s)<GOAL>(insert j s).piecewise f g j = f j
<VAR>α : Type u_1<VAR>δ : α → Sort u_6<VAR>s : Set α<VAR>f g : (i : α) → δ i<VAR>(j : α) → Decidable (j ∈ s)<VAR>DecidableEq α<VAR>j : α<VAR>(i : α) → Decidable (i ∈ insert j s)<GOAL>(insert j s).piecewise f g = Function.update (s.piecewise f g) j (f j)
<VAR>α : Type u_1<VAR>δ : α → Sort u_6<VAR>s : Set α<VAR>f g : (i : α) → δ i<VAR>(j : α) → Decidable (j ∈ s)<VAR>i : α<VAR>hi : i ∈ s<GOAL>s.piecewise f g i = f i
<VAR>α : Type u_1<VAR>δ : α → Sort u_6<VAR>s : Set α<VAR>f g : (i : α) → δ i<VAR>(j : α) → Decidable (j ∈ s)<VAR>i : α<VAR>hi : i ∉ s<GOAL>s.piecewise f g i = g i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α<VAR>(y : α) → Decidable (y ∈ {x})<VAR>DecidableEq α<VAR>f g : α → β<GOAL>{x}.piecewise f g = Function.update g x (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>(j : α) → Decidable (j ∈ s)<VAR>f g : α → β<GOAL>Set.EqOn (s.piecewise f g) f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>(j : α) → Decidable (j ∈ s)<VAR>f g : α → β<GOAL>Set.EqOn (s.piecewise f g) g sᶜ
<VAR>α : Type u_1<VAR>δ : α → Type u_7<VAR>(i : α) → Preorder (δ i)<VAR>s : Set α<VAR>(j : α) → Decidable (j ∈ s)<VAR>f₁ f₂ g : (i : α) → δ i<VAR>h₁ : ∀ i ∈ s, f₁ i ≤ g i<VAR>h₂ : ∀ i ∉ s, f₂ i ≤ g i<GOAL>s.piecewise f₁ f₂ ≤ g
<VAR>α : Type u_1<VAR>δ : α → Type u_7<VAR>(i : α) → Preorder (δ i)<VAR>s : Set α<VAR>(j : α) → Decidable (j ∈ s)<VAR>f₁ f₂ g : (i : α) → δ i<VAR>h₁ : ∀ i ∈ s, g i ≤ f₁ i<VAR>h₂ : ∀ i ∉ s, g i ≤ f₂ i<GOAL>g ≤ s.piecewise f₁ f₂
<VAR>α : Type u_1<VAR>δ : α → Type u_7<VAR>(i : α) → Preorder (δ i)<VAR>s : Set α<VAR>(j : α) → Decidable (j ∈ s)<VAR>f₁ f₂ g₁ g₂ : (i : α) → δ i<VAR>h₁ : ∀ i ∈ s, f₁ i ≤ g₁ i<VAR>h₂ : ∀ i ∉ s, f₂ i ≤ g₂ i<GOAL>s.piecewise f₁ f₂ ≤ s.piecewise g₁ g₂
<VAR>α : Type u_1<VAR>δ : α → Sort u_6<VAR>s : Set α<VAR>f g : (i : α) → δ i<VAR>(j : α) → Decidable (j ∈ s)<VAR>i j : α<VAR>h : i ≠ j<VAR>(i : α) → Decidable (i ∈ insert j s)<GOAL>(insert j s).piecewise f g i = s.piecewise f g i
<VAR>α : Type u_1<VAR>δ : α → Sort u_6<VAR>s : Set α<VAR>f g : (i : α) → δ i<VAR>(j : α) → Decidable (j ∈ s)<VAR>(i : α) → Decidable (i ∈ sᶜ)<GOAL>sᶜ.piecewise f g = s.piecewise g f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_7<VAR>f : ι → α<VAR>(j : α) → Decidable (j ∈ Set.range f)<VAR>g₁ g₂ : α → β<GOAL>(Set.range f).piecewise g₁ g₂ ∘ f = g₁ ∘ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>f₁ f₂ : α → β<VAR>(i : α) → Decidable (i ∈ s)<VAR>h₁ : Set.MapsTo f₁ (s₁ ∩ s) (t₁ ∩ t)<VAR>h₂ : Set.MapsTo f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ)<GOAL>Set.MapsTo (s.piecewise f₁ f₂) (s.ite s₁ s₂) (t.ite t₁ t₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>(j : α) → Decidable (j ∈ s)<VAR>f f' g : α → β<VAR>t : Set α<GOAL>Set.EqOn (s.piecewise f f') g t ↔ Set.EqOn f g (t ∩ s) ∧ Set.EqOn f' g (t ∩ sᶜ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>(j : α) → Decidable (j ∈ s)<VAR>f f' g : α → β<VAR>t t' : Set α<VAR>h : Set.EqOn f g (t ∩ s)<VAR>h' : Set.EqOn f' g (t' ∩ sᶜ)<GOAL>Set.EqOn (s.piecewise f f') g (s.ite t t')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>(j : α) → Decidable (j ∈ s)<VAR>f f' g : α → β<VAR>t t' : Set α<VAR>h : Set.EqOn f g t<VAR>h' : Set.EqOn f' g t'<GOAL>Set.EqOn (s.piecewise f f') g (s.ite t t')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>(j : α) → Decidable (j ∈ s)<VAR>f g : α → β<VAR>t : Set β<GOAL>s.piecewise f g ⁻¹' t = s.ite (f ⁻¹' t) (g ⁻¹' t)
<VAR>α : Type u_1<VAR>δ : α → Sort u_6<VAR>s : Set α<VAR>f g : (i : α) → δ i<VAR>(j : α) → Decidable (j ∈ s)<VAR>δ' : α → Sort u_7<VAR>h : (i : α) → δ i → δ' i<VAR>x : α<GOAL>h x (s.piecewise f g x) = s.piecewise (fun x => h x (f x)) (fun x => h x (g x)) x
<VAR>α : Type u_1<VAR>δ : α → Sort u_6<VAR>s : Set α<VAR>f g : (i : α) → δ i<VAR>(j : α) → Decidable (j ∈ s)<VAR>δ' : α → Sort u_7<VAR>δ'' : α → Sort u_8<VAR>f' g' : (i : α) → δ' i<VAR>h : (i : α) → δ i → δ' i → δ'' i<VAR>x : α<GOAL>h x (s.piecewise f g x) (s.piecewise f' g' x) = s.piecewise (fun x => h x (f x) (f' x)) (fun x => h x (g x) (g' x)) x
<VAR>α : Type u_1<VAR>δ : α → Sort u_6<VAR>s : Set α<VAR>f g : (i : α) → δ i<VAR>(j : α) → Decidable (j ∈ s)<VAR>δ' : α → Sort u_7<VAR>h : (i : α) → δ i → δ' i<GOAL>(s.piecewise (fun x => h x (f x)) fun x => h x (g x)) = fun x => h x (s.piecewise f g x)
<VAR>α : Type u_1<VAR>δ : α → Sort u_6<VAR>s : Set α<VAR>f g : (i : α) → δ i<VAR>(j : α) → Decidable (j ∈ s)<VAR>δ' : α → Sort u_7<VAR>δ'' : α → Sort u_8<VAR>f' g' : (i : α) → δ' i<VAR>h : (i : α) → δ i → δ' i → δ'' i<GOAL>(s.piecewise (fun x => h x (f x) (f' x)) fun x => h x (g x) (g' x)) = fun x => h x (s.piecewise f g x) (s.piecewise f' g' x)
<VAR>α : Type u_1<VAR>δ : α → Sort u_6<VAR>s : Set α<VAR>f : (i : α) → δ i<VAR>(j : α) → Decidable (j ∈ s)<GOAL>s.piecewise f f = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>(j : α) → Decidable (j ∈ s)<VAR>f g : α → β<GOAL>Set.range (s.piecewise f g) = f '' s ∪ g '' sᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>(j : α) → Decidable (j ∈ s)<VAR>f g : α → β<GOAL>Function.Injective (s.piecewise f g) ↔ Set.InjOn f s ∧ Set.InjOn g sᶜ ∧ ∀ x ∈ s, ∀ y ∉ s, f x ≠ g y
<VAR>α : Type u_1<VAR>s : Set α<VAR>(j : α) → Decidable (j ∈ s)<VAR>δ : α → Type u_7<VAR>t : Set α<VAR>t' : (i : α) → Set (δ i)<VAR>f g : (i : α) → δ i<VAR>hf : f ∈ t.pi t'<VAR>hg : g ∈ t.pi t'<GOAL>s.piecewise f g ∈ t.pi t'
<VAR>ι : Type u_7<VAR>α : ι → Type u_8<VAR>s s' : Set ι<VAR>t t' : (i : ι) → Set (α i)<VAR>(x : ι) → Decidable (x ∈ s')<GOAL>s.pi (s'.piecewise t t') = (s ∩ s').pi t ∩ (s \ s').pi t'
<VAR>ι : Type u_7<VAR>α : ι → Type u_8<VAR>s : Set ι<VAR>t t' : (i : ι) → Set (α i)<VAR>(x : ι) → Decidable (x ∈ s)<GOAL>Set.univ.pi (s.piecewise t t') = s.pi t ∩ sᶜ.pi t'
<VAR>ι : Type u_7<VAR>α : ι → Type u_8<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>(x : ι) → Decidable (x ∈ s)<GOAL>Set.univ.pi (s.piecewise t fun x => Set.univ) = s.pi t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>H : StrictMonoOn f s<GOAL>Set.InjOn f s