ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>H : StrictAntiOn f s<GOAL>Set.InjOn f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>g : β → γ<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>hg : StrictMonoOn g t<VAR>hf : StrictMonoOn f s<VAR>hs : Set.MapsTo f s t<GOAL>StrictMonoOn (g ∘ f) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>g : β → γ<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>hg : StrictMonoOn g t<VAR>hf : StrictAntiOn f s<VAR>hs : Set.MapsTo f s t<GOAL>StrictAntiOn (g ∘ f) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>g : β → γ<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>hg : StrictAntiOn g t<VAR>hf : StrictAntiOn f s<VAR>hs : Set.MapsTo f s t<GOAL>StrictMonoOn (g ∘ f) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>g : β → γ<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>hg : StrictAntiOn g t<VAR>hf : StrictMonoOn f s<VAR>hs : Set.MapsTo f s t<GOAL>StrictAntiOn (g ∘ f) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<GOAL>StrictMono (s.restrict f) ↔ StrictMonoOn f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : StrictMono f<VAR>s : Set β<VAR>hs : ∀ (x : α), f x ∈ s<GOAL>StrictMono (Set.codRestrict f s hs)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>g : β → γ<VAR>s : Set α<VAR>hg : Function.Injective g<VAR>hf : Set.InjOn f s<GOAL>Set.InjOn (g ∘ f) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Surjective f<VAR>s : Set β<GOAL>Set.SurjOn f Set.univ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>g : β → α<VAR>h : Function.LeftInverse f g<VAR>s : Set β<GOAL>Set.LeftInvOn f g s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>g : β → α<VAR>h : Function.RightInverse f g<VAR>s : Set α<GOAL>Set.RightInvOn f g s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>g : β → α<VAR>h : Function.LeftInverse f g<GOAL>Set.RightInvOn f g (Set.range g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>fa : α → α<VAR>fb : β → β<VAR>f : α → β<VAR>s t : Set α<VAR>h : Function.Semiconj f fa fb<VAR>ha : Set.MapsTo fa s t<GOAL>Set.MapsTo fb (f '' s) (f '' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>fa : α → α<VAR>fb : β → β<VAR>f : α → β<VAR>h : Function.Semiconj f fa fb<GOAL>Set.MapsTo fb (Set.range f) (Set.range f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>fa : α → α<VAR>fb : β → β<VAR>f : α → β<VAR>s t : Set α<VAR>h : Function.Semiconj f fa fb<VAR>ha : Set.SurjOn fa s t<GOAL>Set.SurjOn fb (f '' s) (f '' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>fa : α → α<VAR>fb : β → β<VAR>f : α → β<VAR>h : Function.Semiconj f fa fb<VAR>ha : Function.Surjective fa<GOAL>Set.SurjOn fb (Set.range f) (Set.range f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>fa : α → α<VAR>fb : β → β<VAR>f : α → β<VAR>s : Set α<VAR>h : Function.Semiconj f fa fb<VAR>ha : Set.InjOn fa s<VAR>hf : Set.InjOn f (fa '' s)<GOAL>Set.InjOn fb (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>fa : α → α<VAR>fb : β → β<VAR>f : α → β<VAR>h : Function.Semiconj f fa fb<VAR>ha : Function.Injective fa<VAR>hf : Set.InjOn f (Set.range fa)<GOAL>Set.InjOn fb (Set.range f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>fa : α → α<VAR>fb : β → β<VAR>f : α → β<VAR>s t : Set α<VAR>h : Function.Semiconj f fa fb<VAR>ha : Set.BijOn fa s t<VAR>hf : Set.InjOn f t<GOAL>Set.BijOn fb (f '' s) (f '' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>fa : α → α<VAR>fb : β → β<VAR>f : α → β<VAR>h : Function.Semiconj f fa fb<VAR>ha : Function.Bijective fa<VAR>hf : Function.Injective f<GOAL>Set.BijOn fb (Set.range f) (Set.range f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>fa : α → α<VAR>fb : β → β<VAR>f : α → β<VAR>h : Function.Semiconj f fa fb<VAR>s t : Set β<VAR>hb : Set.MapsTo fb s t<GOAL>Set.MapsTo fa (f ⁻¹' s) (f ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>fa : α → α<VAR>fb : β → β<VAR>f : α → β<VAR>h : Function.Semiconj f fa fb<VAR>s : Set β<VAR>hb : Set.InjOn fb s<VAR>hf : Set.InjOn f (f ⁻¹' s)<GOAL>Set.InjOn fa (f ⁻¹' s)
<VAR>α : Sort u_6<VAR>β : Type u_7<VAR>γ : β → Sort u_8<VAR>DecidableEq β<VAR>g : (b : β) → γ b<VAR>f : α → β<VAR>i : β<VAR>a : γ i<VAR>h : i ∉ Set.range f<GOAL>(fun j => Function.update g i a (f j)) = fun j => g (f j)
<VAR>α : Sort u_6<VAR>β : Type u_7<VAR>γ : Sort u_8<VAR>DecidableEq β<VAR>g : β → γ<VAR>f : α → β<VAR>i : β<VAR>a : γ<VAR>h : i ∉ Set.range f<GOAL>Function.update g i a ∘ f = g ∘ f
<VAR>α : Type u_1<VAR>s : Set α<GOAL>Set.InjOn (fun a => insert a s) sᶜ
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>PartialOrder α<VAR>LinearOrder β<VAR>φ : β → α<VAR>ψ : α → β<VAR>t : Set β<VAR>s : Set α<VAR>hφ : MonotoneOn φ t<VAR>φψs : Set.RightInvOn ψ φ s<VAR>ψts : Set.MapsTo ψ s t<GOAL>MonotoneOn ψ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PartialOrder α<VAR>LinearOrder β<VAR>φ : β → α<VAR>ψ : α → β<VAR>t : Set β<VAR>s : Set α<VAR>hφ : AntitoneOn φ t<VAR>φψs : Set.RightInvOn ψ φ s<VAR>ψts : Set.MapsTo ψ s t<GOAL>AntitoneOn ψ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : β → Prop<VAR>DecidablePred p<VAR>f : α ≃ Subtype p<VAR>g : Equiv.Perm α<VAR>s t : Set α<VAR>h : Set.MapsTo (⇑g) s t<GOAL>Set.MapsTo (⇑(g.extendDomain f)) (Subtype.val ∘ ⇑f '' s) (Subtype.val ∘ ⇑f '' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : β → Prop<VAR>DecidablePred p<VAR>f : α ≃ Subtype p<VAR>g : Equiv.Perm α<VAR>s t : Set α<VAR>h : Set.SurjOn (⇑g) s t<GOAL>Set.SurjOn (⇑(g.extendDomain f)) (Subtype.val ∘ ⇑f '' s) (Subtype.val ∘ ⇑f '' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : β → Prop<VAR>DecidablePred p<VAR>f : α ≃ Subtype p<VAR>g : Equiv.Perm α<VAR>s t : Set α<VAR>h : Set.BijOn (⇑g) s t<GOAL>Set.BijOn (⇑(g.extendDomain f)) (Subtype.val ∘ ⇑f '' s) (Subtype.val ∘ ⇑f '' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : β → Prop<VAR>DecidablePred p<VAR>f : α ≃ Subtype p<VAR>g₁ g₂ : Equiv.Perm α<VAR>s : Set α<VAR>h : Set.LeftInvOn (⇑g₁) (⇑g₂) s<GOAL>Set.LeftInvOn (⇑(g₁.extendDomain f)) (⇑(g₂.extendDomain f)) (Subtype.val ∘ ⇑f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : β → Prop<VAR>DecidablePred p<VAR>f : α ≃ Subtype p<VAR>g₁ g₂ : Equiv.Perm α<VAR>t : Set α<VAR>h : Set.RightInvOn (⇑g₁) (⇑g₂) t<GOAL>Set.RightInvOn (⇑(g₁.extendDomain f)) (⇑(g₂.extendDomain f)) (Subtype.val ∘ ⇑f '' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : β → Prop<VAR>DecidablePred p<VAR>f : α ≃ Subtype p<VAR>g₁ g₂ : Equiv.Perm α<VAR>s t : Set α<VAR>h : Set.InvOn (⇑g₁) (⇑g₂) s t<GOAL>Set.InvOn (⇑(g₁.extendDomain f)) (⇑(g₂.extendDomain f)) (Subtype.val ∘ ⇑f '' s) (Subtype.val ∘ ⇑f '' t)
<VAR>α₁ : Type u_6<VAR>α₂ : Type u_7<VAR>β₁ : Type u_8<VAR>β₂ : Type u_9<VAR>s₁ : Set α₁<VAR>s₂ : Set α₂<VAR>f₁ : α₁ → β₁<VAR>f₂ : α₂ → β₂<VAR>h₁ : Set.InjOn f₁ s₁<VAR>h₂ : Set.InjOn f₂ s₂<GOAL>Set.InjOn (fun x => (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂)
<VAR>α₁ : Type u_6<VAR>α₂ : Type u_7<VAR>β₁ : Type u_8<VAR>β₂ : Type u_9<VAR>s₁ : Set α₁<VAR>s₂ : Set α₂<VAR>t₁ : Set β₁<VAR>t₂ : Set β₂<VAR>f₁ : α₁ → β₁<VAR>f₂ : α₂ → β₂<VAR>h₁ : Set.SurjOn f₁ s₁ t₁<VAR>h₂ : Set.SurjOn f₂ s₂ t₂<GOAL>Set.SurjOn (fun x => (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ t₂)
<VAR>α₁ : Type u_6<VAR>α₂ : Type u_7<VAR>β₁ : Type u_8<VAR>β₂ : Type u_9<VAR>s₁ : Set α₁<VAR>s₂ : Set α₂<VAR>t₁ : Set β₁<VAR>t₂ : Set β₂<VAR>f₁ : α₁ → β₁<VAR>f₂ : α₂ → β₂<VAR>h₁ : Set.MapsTo f₁ s₁ t₁<VAR>h₂ : Set.MapsTo f₂ s₂ t₂<GOAL>Set.MapsTo (fun x => (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ t₂)
<VAR>α₁ : Type u_6<VAR>α₂ : Type u_7<VAR>β₁ : Type u_8<VAR>β₂ : Type u_9<VAR>s₁ : Set α₁<VAR>s₂ : Set α₂<VAR>t₁ : Set β₁<VAR>t₂ : Set β₂<VAR>f₁ : α₁ → β₁<VAR>f₂ : α₂ → β₂<VAR>h₁ : Set.BijOn f₁ s₁ t₁<VAR>h₂ : Set.BijOn f₂ s₂ t₂<GOAL>Set.BijOn (fun x => (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ t₂)
<VAR>α₁ : Type u_6<VAR>α₂ : Type u_7<VAR>β₁ : Type u_8<VAR>β₂ : Type u_9<VAR>s₁ : Set α₁<VAR>s₂ : Set α₂<VAR>f₁ : α₁ → β₁<VAR>f₂ : α₂ → β₂<VAR>g₁ : β₁ → α₁<VAR>g₂ : β₂ → α₂<VAR>h₁ : Set.LeftInvOn g₁ f₁ s₁<VAR>h₂ : Set.LeftInvOn g₂ f₂ s₂<GOAL>Set.LeftInvOn (fun x => (g₁ x.1, g₂ x.2)) (fun x => (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂)
<VAR>α₁ : Type u_6<VAR>α₂ : Type u_7<VAR>β₁ : Type u_8<VAR>β₂ : Type u_9<VAR>t₁ : Set β₁<VAR>t₂ : Set β₂<VAR>f₁ : α₁ → β₁<VAR>f₂ : α₂ → β₂<VAR>g₁ : β₁ → α₁<VAR>g₂ : β₂ → α₂<VAR>h₁ : Set.RightInvOn g₁ f₁ t₁<VAR>h₂ : Set.RightInvOn g₂ f₂ t₂<GOAL>Set.RightInvOn (fun x => (g₁ x.1, g₂ x.2)) (fun x => (f₁ x.1, f₂ x.2)) (t₁ ×ˢ t₂)
<VAR>α₁ : Type u_6<VAR>α₂ : Type u_7<VAR>β₁ : Type u_8<VAR>β₂ : Type u_9<VAR>s₁ : Set α₁<VAR>s₂ : Set α₂<VAR>t₁ : Set β₁<VAR>t₂ : Set β₂<VAR>f₁ : α₁ → β₁<VAR>f₂ : α₂ → β₂<VAR>g₁ : β₁ → α₁<VAR>g₂ : β₂ → α₂<VAR>h₁ : Set.InvOn g₁ f₁ s₁ t₁<VAR>h₂ : Set.InvOn g₂ f₂ s₂ t₂<GOAL>Set.InvOn (fun x => (g₁ x.1, g₂ x.2)) (fun x => (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ t₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>s : Set α<VAR>t : Set β<VAR>h₁ : Set.MapsTo (⇑e) s t<VAR>h₂ : Set.MapsTo (⇑e.symm) t s<GOAL>Set.BijOn (⇑e) s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>s : Set α<VAR>t : Set β<VAR>h : ∀ (a : α), e a ∈ t ↔ a ∈ s<GOAL>Set.BijOn (⇑e) s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>s : Set α<VAR>t : Set β<GOAL>Set.InvOn (⇑e) (⇑e.symm) t s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>s : Set α<GOAL>Set.BijOn (⇑e) s (⇑e '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>s : Set α<GOAL>Set.BijOn (⇑e.symm) (⇑e '' s) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>s : Set α<VAR>t : Set β<GOAL>Set.BijOn (⇑e.symm) t s ↔ Set.BijOn (⇑e) s t
<VAR>α : Type u_1<VAR>s : Set α<VAR>DecidableEq α<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>Set.BijOn (⇑(Equiv.swap a b)) s s
<VAR>ι : Sort u_1<VAR>f : ι → ℕ<GOAL>⨆ i, ↑(f i) = ⊤ ↔ ¬BddAbove (Set.range f)
<VAR>ι : Sort u_1<VAR>f : ι → ℕ<GOAL>⨆ i, ↑(f i) ≠ ⊤ ↔ BddAbove (Set.range f)
<VAR>ι : Sort u_1<VAR>f : ι → ℕ<GOAL>⨆ i, ↑(f i) < ⊤ ↔ BddAbove (Set.range f)
<VAR>ι : Sort u_1<VAR>f : ι → ℕ<GOAL>⨅ i, ↑(f i) = ⊤ ↔ IsEmpty ι
<VAR>ι : Sort u_1<VAR>f : ι → ℕ<GOAL>⨅ i, ↑(f i) ≠ ⊤ ↔ Nonempty ι
<VAR>ι : Sort u_1<VAR>f : ι → ℕ<GOAL>⨅ i, ↑(f i) < ⊤ ↔ Nonempty ι
<VAR>s : Set ℕ<GOAL>BddAbove s → ↑(sSup s) = ⨆ a ∈ s, ↑a
<VAR>s : Set ℕ<VAR>hs : s.Nonempty<GOAL>↑(sInf s) = ⨅ a ∈ s, ↑a
<VAR>ι : Sort u_1<VAR>f : ι → ℕ<GOAL>BddAbove (Set.range f) → ↑(⨆ i, f i) = ⨆ i, ↑(f i)
<VAR>ι : Sort u_1<VAR>f : ι → ℕ<VAR>Nonempty ι<GOAL>↑(⨅ i, f i) = ⨅ i, ↑(f i)
<VAR>ι : Sort u_1<VAR>f : ι → ℕ<VAR>IsEmpty ι<GOAL>⨅ i, ↑(f i) = ⊤
<VAR>ι : Sort u_1<VAR>f : ι → ℕ<GOAL>(⨅ i, ↑(f i)).toNat = ⨅ i, f i
<VAR>ι : Sort u_1<VAR>f : ι → ℕ<GOAL>⨅ i, ↑(f i) = 0 ↔ ∃ i, f i = 0
<VAR>s : Set ℕ∞<GOAL>sSup s = 0 ↔ ∀ a ∈ s, a = 0
<VAR>s : Set ℕ∞<GOAL>sInf s = 0 ↔ 0 ∈ s
<VAR>s : Set ℕ∞<GOAL>sSup s = 0 ↔ s = ∅ ∨ s = {0}
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>self : Ctop α σ<VAR>x : α<GOAL>x ∈ self.f (self.top x)
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>self : Ctop α σ<VAR>a b : σ<VAR>x : α<VAR>h : x ∈ self.f a ∩ self.f b<GOAL>x ∈ self.f (self.inter a b x h)
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>self : Ctop α σ<VAR>a b : σ<VAR>x : α<VAR>h : x ∈ self.f a ∩ self.f b<GOAL>self.f (self.inter a b x h) ⊆ self.f a ∩ self.f b
<VAR>α : Type u_1<VAR>σ : Type u_3<VAR>f : σ → Set α<VAR>T : α → σ<VAR>h₁ : ∀ (x : α), x ∈ f (T x)<VAR>I : (a b : σ) → (x : α) → x ∈ f a ∩ f b → σ<VAR>h₂ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), x ∈ f (I a b x h)<VAR>h₃ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), f (I a b x h) ⊆ f a ∩ f b<VAR>a : σ<GOAL>{ f := f, top := T, top_mem := h₁, inter := I, inter_mem := h₂, inter_sub := h₃ }.f a = f a
<VAR>α : Type u_1<VAR>σ : Type u_3<VAR>τ : Type u_4<VAR>E : σ ≃ τ<VAR>F : Ctop α σ<VAR>a : τ<GOAL>(Ctop.ofEquiv E F).f a = F.f (E.symm a)
<VAR>α : Type u_1<VAR>σ : Type u_3<VAR>F : Ctop α σ<GOAL>TopologicalSpace.IsTopologicalBasis (Set.range F.f)
<VAR>α : Type u_1<VAR>σ : Type u_3<VAR>F : Ctop α σ<VAR>s : Set α<VAR>a : α<GOAL>s ∈ 𝓝 a ↔ ∃ b, a ∈ F.f b ∧ F.f b ⊆ s
<VAR>α : Type u_6<VAR>T : TopologicalSpace α<VAR>self : Ctop.Realizer α<GOAL>self.F.toTopsp = T
<VAR>α : Type u_1<VAR>T : TopologicalSpace α<VAR>F : Ctop.Realizer α<GOAL>TopologicalSpace.IsTopologicalBasis (Set.range F.F.f)
<VAR>α : Type u_1<VAR>T : TopologicalSpace α<VAR>F : Ctop.Realizer α<VAR>s : Set α<VAR>a : α<GOAL>s ∈ 𝓝 a ↔ ∃ b, a ∈ F.F.f b ∧ F.F.f b ⊆ s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>F : Ctop.Realizer α<VAR>s : Set α<GOAL>IsOpen s ↔ ∀ a ∈ s, ∃ b, a ∈ F.F.f b ∧ F.F.f b ⊆ s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>F : Ctop.Realizer α<VAR>s : Set α<GOAL>IsClosed s ↔ ∀ (a : α), (∀ (b : F.σ), a ∈ F.F.f b → ∃ z, z ∈ F.F.f b ∩ s) → a ∈ s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>F : Ctop.Realizer α<VAR>s : Set α<VAR>a : α<GOAL>a ∈ interior s ↔ ∃ b, a ∈ F.F.f b ∧ F.F.f b ⊆ s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>F : Ctop.Realizer α<VAR>s : F.σ<GOAL>IsOpen (F.F.f s)
<VAR>α : Type u_1<VAR>T : TopologicalSpace α<VAR>σ : Type u_5<VAR>F : Ctop α σ<VAR>H : ∀ (a : α) (s : Set α), s ∈ 𝓝 a ↔ ∃ b, a ∈ F.f b ∧ F.f b ⊆ s<GOAL>F.toTopsp = T
<VAR>α : Type u_1<VAR>T : TopologicalSpace α<VAR>σ : Type u_5<VAR>F : Ctop α σ<VAR>H₁ : ∀ (a : σ), IsOpen (F.f a)<VAR>H₂ : ∀ (a : α), ∀ s ∈ 𝓝 a, ∃ b, a ∈ F.f b ∧ F.f b ⊆ s<GOAL>F.toTopsp = T
<VAR>α : Type u_1<VAR>τ : Type u_4<VAR>TopologicalSpace α<VAR>F : Ctop.Realizer α<VAR>E : F.σ ≃ τ<GOAL>(F.ofEquiv E).σ = τ
<VAR>α : Type u_1<VAR>τ : Type u_4<VAR>TopologicalSpace α<VAR>F : Ctop.Realizer α<VAR>E : F.σ ≃ τ<VAR>s : τ<GOAL>(F.ofEquiv E).F.f s = F.F.f (E.symm s)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>F : Ctop.Realizer α<VAR>a : α<GOAL>(F.nhds a).σ = { s // a ∈ F.F.f s }
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>F : Ctop.Realizer α<VAR>a : α<VAR>s : (F.nhds a).σ<GOAL>(F.nhds a).F.f s = F.F.f ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>m : β → α<VAR>f : Filter β<VAR>F : f.Realizer<VAR>R : Ctop.Realizer α<VAR>a : α<GOAL>Filter.Tendsto m f (𝓝 a) ↔ ∀ (t : R.σ), a ∈ R.F.f t → ∃ s, ∀ x ∈ F.F.f s, m x ∈ R.F.f t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>F : Ctop.Realizer α<VAR>f : β → Set α<VAR>R : LocallyFinite.Realizer F f<GOAL>LocallyFinite f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>F : Ctop.Realizer α<VAR>f : β → Set α<GOAL>LocallyFinite f ↔ Nonempty (LocallyFinite.Realizer F f)
<VAR>m n : ℕ<GOAL>↑(m + n) = ↑m + ↑n
<VAR>m : ℕ∞<VAR>hm : m ≠ 0<GOAL>m * ⊤ = ⊤
<VAR>m : ℕ∞<VAR>hm : m ≠ 0<GOAL>⊤ * m = ⊤
<VAR>n : ℕ<VAR>n_pos : 0 < n<GOAL>⊤ ^ n = ⊤
<GOAL>⇑ENat.toNatHom = ENat.toNat
<VAR>n : ℕ<GOAL>ENat.toNatHom ↑n = (↑n).toNat
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>(OfNat.ofNat n).toNat = n
<VAR>n : ℕ∞<GOAL>n.toNat = 0 ↔ n = 0 ∨ n = ⊤
<VAR>C : ℕ∞ → Sort u_1<VAR>d : C ⊤<VAR>f : (a : ℕ) → C ↑a<GOAL>ENat.recTopCoe d f ⊤ = d
<VAR>C : ℕ∞ → Sort u_1<VAR>d : C ⊤<VAR>f : (a : ℕ) → C ↑a<VAR>x : ℕ<GOAL>ENat.recTopCoe d f ↑x = f x
<VAR>C : ℕ∞ → Sort u_1<VAR>d : C ⊤<VAR>f : (a : ℕ) → C ↑a<GOAL>ENat.recTopCoe d f 0 = f 0
<VAR>C : ℕ∞ → Sort u_1<VAR>d : C ⊤<VAR>f : (a : ℕ) → C ↑a<GOAL>ENat.recTopCoe d f 1 = f 1
<VAR>C : ℕ∞ → Sort u_1<VAR>d : C ⊤<VAR>f : (a : ℕ) → C ↑a<VAR>x : ℕ<VAR>x.AtLeastTwo<GOAL>ENat.recTopCoe d f (OfNat.ofNat x) = f (OfNat.ofNat x)
<VAR>a : ℕ<GOAL>⊤ ≠ ↑a
<VAR>a : ℕ<VAR>a.AtLeastTwo<GOAL>⊤ ≠ OfNat.ofNat a
<VAR>a : ℕ<GOAL>↑a ≠ ⊤
<VAR>a : ℕ<VAR>a.AtLeastTwo<GOAL>OfNat.ofNat a ≠ ⊤
<VAR>a : ℕ<GOAL>⊤ - ↑a = ⊤
<VAR>a : ℕ<VAR>a.AtLeastTwo<GOAL>⊤ - OfNat.ofNat a = ⊤
<VAR>a : ℕ∞<GOAL>a - ⊤ = 0
<VAR>n : ℕ∞<GOAL>↑n.toNat = n ↔ n ≠ ⊤
<VAR>n : ℕ∞<GOAL>↑n.toNat ≤ n
<VAR>m n : ℕ∞<VAR>hm : m ≠ ⊤<VAR>hn : n ≠ ⊤<GOAL>(m + n).toNat = m.toNat + n.toNat
<VAR>n : ℕ∞<VAR>hn : n ≠ ⊤<VAR>m : ℕ∞<GOAL>(m - n).toNat = m.toNat - n.toNat
<VAR>m : ℕ∞<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>m.toNat = n ↔ m = ↑n
<VAR>m : ℕ∞<VAR>n : ℕ<VAR>h : m ≤ ↑n<GOAL>m.toNat ≤ n
<VAR>m n : ℕ∞<VAR>h : m ≤ n<VAR>hn : n ≠ ⊤<GOAL>m.toNat ≤ n.toNat
<VAR>m : ℕ∞<GOAL>Order.succ m = m + 1
<VAR>m n : ℕ∞<VAR>h : m < n<GOAL>m + 1 ≤ n
<VAR>m n : ℕ∞<VAR>hm : m ≠ ⊤<GOAL>m + 1 ≤ n ↔ m < n
<VAR>n : ℕ∞<GOAL>1 ≤ n ↔ 0 < n
<VAR>n : ℕ∞<GOAL>1 ≤ n ↔ n ≠ 0
<VAR>n : ℕ∞<GOAL>n < 1 ↔ n = 0
<VAR>m n : ℕ∞<VAR>h : m < n + 1<GOAL>m ≤ n
<VAR>n : ℕ∞<VAR>k : ℕ<GOAL>n ≤ ↑k ↔ ∃ n₀, n = ↑n₀ ∧ n₀ ≤ k
<VAR>P : ℕ∞ → Prop<VAR>a : ℕ∞<VAR>h0 : P 0<VAR>hsuc : ∀ (n : ℕ), P ↑n → P ↑n.succ<VAR>htop : (∀ (n : ℕ), P ↑n) → P ⊤<GOAL>P a
<VAR>n : ℕ<GOAL>↑n = 0 ↔ Even n
<VAR>n : ℕ<GOAL>↑n ≠ 0 ↔ Odd n
<VAR>a : ℤ<VAR>p : ℕ<VAR>pp : Nat.Prime p<VAR>h : a.gcd ↑p = 1<GOAL>↑a ≠ 0
<VAR>a : ℤ<VAR>p : ℕ<VAR>pp : Nat.Prime p<VAR>h : a.gcd ↑p ≠ 1<GOAL>↑a = 0
<VAR>z : ZMod 2<VAR>au : Additive ℤˣ<GOAL>z • au = z.val • au
<VAR>n : ℕ<VAR>au : Additive ℤˣ<GOAL>↑n • au = n • au
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Module R (Additive ℤˣ)<VAR>u : ℤˣ<VAR>r : R<GOAL>Additive.ofMul (u ^ r) = r • Additive.ofMul u
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Module R (Additive ℤˣ)<VAR>u : Additive ℤˣ<VAR>r : R<GOAL>Additive.toMul (r • u) = Additive.toMul u ^ r
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Module R (Additive ℤˣ)<VAR>u : ℤˣ<VAR>n : ℕ<GOAL>u ^ ↑n = u ^ n
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Module R (Additive ℤˣ)<VAR>s : ℤˣ<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>s ^ OfNat.ofNat n = s ^ OfNat.ofNat n
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Module R (Additive ℤˣ)<VAR>x : R<GOAL>1 ^ x = 1
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Module R (Additive ℤˣ)<VAR>s₁ s₂ : ℤˣ<VAR>x : R<GOAL>(s₁ * s₂) ^ x = s₁ ^ x * s₂ ^ x
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Module R (Additive ℤˣ)<VAR>s : ℤˣ<GOAL>s ^ 0 = 1
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Module R (Additive ℤˣ)<VAR>s : ℤˣ<GOAL>s ^ 1 = s
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Module R (Additive ℤˣ)<VAR>s : ℤˣ<VAR>x y : R<GOAL>s ^ (x * y) = (s ^ x) ^ y
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Module R (Additive ℤˣ)<VAR>s : ℤˣ<VAR>x y : R<GOAL>s ^ (x + y) = s ^ x * s ^ y
<VAR>R : Type u_1<VAR>CommRing R<VAR>Module R (Additive ℤˣ)<VAR>s : ℤˣ<VAR>x y : R<GOAL>s ^ (x - y) = s ^ x / s ^ y
<VAR>R : Type u_1<VAR>CommRing R<VAR>Module R (Additive ℤˣ)<VAR>s : ℤˣ<VAR>x : R<GOAL>s ^ (-x) = (s ^ x)⁻¹
<VAR>R : Type u_1<VAR>CommRing R<VAR>Module R (Additive ℤˣ)<VAR>u : ℤˣ<VAR>z : ℤ<GOAL>u ^ ↑z = u ^ z
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>PartialOrder α<VAR>self : CFilter α σ<VAR>a b : σ<GOAL>self.f (self.inf a b) ≤ self.f a
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>PartialOrder α<VAR>self : CFilter α σ<VAR>a b : σ<GOAL>self.f (self.inf a b) ≤ self.f b
<VAR>α : Type u_1<VAR>σ : Type u_3<VAR>PartialOrder α<VAR>f : σ → α<VAR>pt : σ<VAR>inf : σ → σ → σ<VAR>h₁ : ∀ (a b : σ), f (inf a b) ≤ f a<VAR>h₂ : ∀ (a b : σ), f (inf a b) ≤ f b<VAR>a : σ<GOAL>{ f := f, pt := pt, inf := inf, inf_le_left := h₁, inf_le_right := h₂ }.f a = f a
<VAR>α : Type u_1<VAR>σ : Type u_3<VAR>τ : Type u_4<VAR>PartialOrder α<VAR>E : σ ≃ τ<VAR>F : CFilter α σ<VAR>a : τ<GOAL>(CFilter.ofEquiv E F).f a = F.f (E.symm a)
<VAR>α : Type u_1<VAR>σ : Type u_3<VAR>F : CFilter (Set α) σ<VAR>a : Set α<GOAL>a ∈ F.toFilter ↔ ∃ b, F.f b ⊆ a
<VAR>α : Type u_1<VAR>f : Filter α<VAR>self : f.Realizer<GOAL>self.F.toFilter = f
<VAR>α : Type u_1<VAR>f : Filter α<VAR>F : f.Realizer<VAR>a : Set α<GOAL>a ∈ f ↔ ∃ b, F.F.f b ⊆ a
<VAR>α : Type u_1<VAR>τ : Type u_4<VAR>f : Filter α<VAR>F : f.Realizer<VAR>E : F.σ ≃ τ<GOAL>(F.ofEquiv E).σ = τ
<VAR>α : Type u_1<VAR>τ : Type u_4<VAR>f : Filter α<VAR>F : f.Realizer<VAR>E : F.σ ≃ τ<VAR>s : τ<GOAL>(F.ofEquiv E).F.f s = F.F.f (E.symm s)
<VAR>α : Type u_1<VAR>s : Set α<GOAL>(Filter.Realizer.principal s).σ = Unit
<VAR>α : Type u_1<VAR>s : Set α<VAR>u : Unit<GOAL>(Filter.Realizer.principal s).F.f u = s
<VAR>α : Type u_1<GOAL>Filter.Realizer.top.σ = Unit
<VAR>α : Type u_1<VAR>u : Unit<GOAL>Filter.Realizer.top.F.f u = Set.univ
<VAR>α : Type u_1<GOAL>Filter.Realizer.bot.σ = Unit
<VAR>α : Type u_1<VAR>u : Unit<GOAL>Filter.Realizer.bot.F.f u = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : α → β<VAR>f : Filter α<VAR>F : f.Realizer<GOAL>(Filter.Realizer.map m F).σ = F.σ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : α → β<VAR>f : Filter α<VAR>F : f.Realizer<VAR>s : (Filter.Realizer.map m F).σ<GOAL>(Filter.Realizer.map m F).F.f s = m '' F.F.f s
<VAR>α : Type u_1<VAR>f g : Filter α<VAR>F : f.Realizer<VAR>G : g.Realizer<GOAL>f ≤ g ↔ ∀ (b : G.σ), ∃ a, F.F.f a ≤ G.F.f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>l₁ : Filter α<VAR>l₂ : Filter β<VAR>L₁ : l₁.Realizer<VAR>L₂ : l₂.Realizer<GOAL>Filter.Tendsto f l₁ l₂ ↔ ∀ (b : L₂.σ), ∃ a, ∀ x ∈ L₁.F.f a, f x ∈ L₂.F.f b
<VAR>α : Type u_1<VAR>f : Filter α<VAR>F : f.Realizer<GOAL>f ≠ ⊥ ↔ ∀ (a : F.σ), (F.F.f a).Nonempty
<VAR>n : ℕ<VAR>M : Type u_1<VAR>M₁ : Type u_2<VAR>F : Type u_3<VAR>AddCommGroup M<VAR>AddCommGroup M₁<VAR>FunLike F M M₁<VAR>AddMonoidHomClass F M M₁<VAR>Module (ZMod n) M<VAR>Module (ZMod n) M₁<VAR>f : F<VAR>c : ZMod n<VAR>x : M<GOAL>f (c • x) = c • f x
<VAR>n : ℕ<VAR>M : Type u_1<VAR>S : Type u_4<VAR>AddCommGroup M<VAR>Module (ZMod n) M<VAR>SetLike S M<VAR>AddSubgroupClass S M<VAR>x : M<VAR>K : S<VAR>hx : x ∈ K<VAR>c : ZMod n<GOAL>c • x ∈ K
<VAR>n : ℕ<VAR>M : Type u_1<VAR>M₁ : Type u_2<VAR>AddCommGroup M<VAR>AddCommGroup M₁<VAR>Module (ZMod n) M<VAR>Module (ZMod n) M₁<GOAL>Function.Injective (AddMonoidHom.toZModLinearMap n)
<VAR>n : ℕ<VAR>M : Type u_1<VAR>M₁ : Type u_2<VAR>AddCommGroup M<VAR>AddCommGroup M₁<VAR>Module (ZMod n) M<VAR>Module (ZMod n) M₁<VAR>f : M →+ M₁<GOAL>⇑(AddMonoidHom.toZModLinearMap n f) = ⇑f
<VAR>n : ℕ<VAR>M : Type u_1<VAR>AddCommGroup M<VAR>Module (ZMod n) M<GOAL>⇑(AddSubgroup.toZModSubmodule n).symm = Submodule.toAddSubgroup
<VAR>n : ℕ<VAR>M : Type u_1<VAR>AddCommGroup M<VAR>Module (ZMod n) M<VAR>S : AddSubgroup M<GOAL>↑((AddSubgroup.toZModSubmodule n) S) = ↑S
<VAR>n : ℕ<VAR>M : Type u_1<VAR>AddCommGroup M<VAR>Module (ZMod n) M<VAR>S : AddSubgroup M<GOAL>((AddSubgroup.toZModSubmodule n) S).toAddSubgroup = S
<VAR>n : ℕ<VAR>M : Type u_1<VAR>AddCommGroup M<VAR>Module (ZMod n) M<VAR>S : Submodule (ZMod n) M<GOAL>(AddSubgroup.toZModSubmodule n) S.toAddSubgroup = S
<VAR>α : Type u_1<VAR>Add α<VAR>Preorder α<VAR>DecidableEq α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap HAdd.hAdd) LE.le<VAR>LocallyFiniteOrder α<VAR>a b c d : α<GOAL>Finset.Icc a b + Finset.Icc c d ⊆ Finset.Icc (a + c) (b + d)
<VAR>α : Type u_1<VAR>Mul α<VAR>Preorder α<VAR>DecidableEq α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap HMul.hMul) LE.le<VAR>LocallyFiniteOrder α<VAR>a b c d : α<GOAL>Finset.Icc a b * Finset.Icc c d ⊆ Finset.Icc (a * c) (b * d)
<VAR>α : Type u_1<VAR>Mul α<VAR>Preorder α<VAR>DecidableEq α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap HMul.hMul) LE.le<VAR>LocallyFiniteOrderBot α<VAR>a b : α<GOAL>Finset.Iic a * Finset.Iic b ⊆ Finset.Iic (a * b)
<VAR>α : Type u_1<VAR>Add α<VAR>Preorder α<VAR>DecidableEq α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap HAdd.hAdd) LE.le<VAR>LocallyFiniteOrderBot α<VAR>a b : α<GOAL>Finset.Iic a + Finset.Iic b ⊆ Finset.Iic (a + b)
<VAR>α : Type u_1<VAR>Mul α<VAR>Preorder α<VAR>DecidableEq α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap HMul.hMul) LE.le<VAR>LocallyFiniteOrderTop α<VAR>a b : α<GOAL>Finset.Ici a * Finset.Ici b ⊆ Finset.Ici (a * b)
<VAR>α : Type u_1<VAR>Add α<VAR>Preorder α<VAR>DecidableEq α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap HAdd.hAdd) LE.le<VAR>LocallyFiniteOrderTop α<VAR>a b : α<GOAL>Finset.Ici a + Finset.Ici b ⊆ Finset.Ici (a + b)
<VAR>α : Type u_1<VAR>Add α<VAR>PartialOrder α<VAR>DecidableEq α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap HAdd.hAdd) LT.lt<VAR>LocallyFiniteOrder α<VAR>a b c d : α<GOAL>Finset.Icc a b + Finset.Ico c d ⊆ Finset.Ico (a + c) (b + d)
<VAR>α : Type u_1<VAR>Mul α<VAR>PartialOrder α<VAR>DecidableEq α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>LocallyFiniteOrder α<VAR>a b c d : α<GOAL>Finset.Icc a b * Finset.Ico c d ⊆ Finset.Ico (a * c) (b * d)
<VAR>α : Type u_1<VAR>Add α<VAR>PartialOrder α<VAR>DecidableEq α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap HAdd.hAdd) LT.lt<VAR>LocallyFiniteOrder α<VAR>a b c d : α<GOAL>Finset.Ico a b + Finset.Icc c d ⊆ Finset.Ico (a + c) (b + d)