ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>x : X<VAR>DecidableEq N<VAR>i : N<GOAL>EckmannHilton.IsUnital Mul.mul ⟦GenLoop.const⟧
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>x : X<VAR>DecidableEq N<VAR>i j : N<GOAL>HomotopyGroup.auxGroup i = HomotopyGroup.auxGroup j
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>x : X<VAR>DecidableEq N<VAR>i : N<VAR>j : N<VAR>f g : ↑(Ω^ N X x)<GOAL>⟦GenLoop.transAt i f g⟧ = ⟦GenLoop.transAt j f g⟧
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>x : X<VAR>DecidableEq N<VAR>i : N<VAR>j : N<VAR>f : ↑(Ω^ N X x)<GOAL>⟦GenLoop.symmAt i f⟧ = ⟦GenLoop.symmAt j f⟧
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>x : X<VAR>DecidableEq N<VAR>Nonempty N<GOAL>1 = ⟦GenLoop.const⟧
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>x : X<VAR>DecidableEq N<VAR>Nonempty N<VAR>i : N<VAR>p q : ↑(Ω^ N X x)<GOAL>(fun x_1 x_2 => x_1 * x_2) ⟦p⟧ ⟦q⟧ = ⟦GenLoop.transAt i q p⟧
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>x : X<VAR>DecidableEq N<VAR>Nonempty N<VAR>i : N<VAR>p : ↑(Ω^ N X x)<GOAL>(⟦p⟧)⁻¹ = ⟦GenLoop.symmAt i p⟧
<VAR>B X : Stonean<VAR>π : X ⟶ B<GOAL>[CategoryTheory.EffectiveEpi π, CategoryTheory.Epi π, Function.Surjective ⇑π].TFAE
<VAR>α : Type<VAR>Finite α<VAR>B : Stonean<VAR>X : α → Stonean<VAR>π : (a : α) → X a ⟶ B<GOAL>[CategoryTheory.EffectiveEpiFamily X π, CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc π), ∀ (b : ↑B.toTop), ∃ a x, (π a) x = b].TFAE
<VAR>α : Type<VAR>Finite α<VAR>B : Stonean<VAR>X : α → Stonean<VAR>π : (a : α) → X a ⟶ B<VAR>surj : ∀ (b : ↑B.toTop), ∃ a x, (π a) x = b<GOAL>CategoryTheory.EffectiveEpiFamily X π
<VAR>X Y : LightProfinite<VAR>f : X ⟶ Y<GOAL>CategoryTheory.EffectiveEpi f ↔ Function.Surjective ⇑f
<VAR>Y : Type v<VAR>TopologicalSpace Y<VAR>self : TietzeExtension Y<VAR>X : Type u<VAR>TopologicalSpace X<VAR>NormalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>f : C(↑s, Y)<GOAL>∃ g, ContinuousMap.restrict s g = f
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>NormalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>Y : Type v<VAR>TopologicalSpace Y<VAR>TietzeExtension Y<VAR>f : C(↑s, Y)<GOAL>∃ g, ContinuousMap.restrict s g = f
<VAR>X₁ : Type u₁<VAR>TopologicalSpace X₁<VAR>X : Type u<VAR>TopologicalSpace X<VAR>NormalSpace X<VAR>e : X₁ → X<VAR>he : ClosedEmbedding e<VAR>Y : Type v<VAR>TopologicalSpace Y<VAR>TietzeExtension Y<VAR>f : C(X₁, Y)<GOAL>∃ g, g.comp { toFun := e, continuous_toFun := ⋯ } = f
<VAR>X₁ : Type u₁<VAR>TopologicalSpace X₁<VAR>X : Type u<VAR>TopologicalSpace X<VAR>NormalSpace X<VAR>e : X₁ → X<VAR>he : ClosedEmbedding e<VAR>Y : Type v<VAR>TopologicalSpace Y<VAR>TietzeExtension Y<VAR>f : C(X₁, Y)<GOAL>∃ g, ⇑g ∘ e = ⇑f
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>NormalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>Y : Type v<VAR>TopologicalSpace Y<VAR>f : C(↑s, Y)<VAR>t : Set Y<VAR>hf : ∀ (x : ↑s), f x ∈ t<VAR>ht : TietzeExtension ↑t<GOAL>∃ g, (∀ (x : X), g x ∈ t) ∧ ContinuousMap.restrict s g = f
<VAR>X₁ : Type u₁<VAR>TopologicalSpace X₁<VAR>X : Type u<VAR>TopologicalSpace X<VAR>NormalSpace X<VAR>e : X₁ → X<VAR>he : ClosedEmbedding e<VAR>Y : Type v<VAR>TopologicalSpace Y<VAR>f : C(X₁, Y)<VAR>t : Set Y<VAR>hf : ∀ (x : X₁), f x ∈ t<VAR>ht : TietzeExtension ↑t<GOAL>∃ g, (∀ (x : X), g x ∈ t) ∧ g.comp { toFun := e, continuous_toFun := ⋯ } = f
<VAR>Y : Type v<VAR>Z : Type w<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>TietzeExtension Z<VAR>ι : C(Y, Z)<VAR>r : C(Z, Y)<VAR>h : r.comp ι = ContinuousMap.id Y<GOAL>TietzeExtension Y
<VAR>Y : Type v<VAR>Z : Type w<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>TietzeExtension Z<VAR>e : Y ≃ₜ Z<GOAL>TietzeExtension Y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>NormalSpace Y<VAR>f : X →ᵇ ℝ<VAR>e : C(X, Y)<VAR>he : ClosedEmbedding ⇑e<GOAL>∃ g, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>NormalSpace Y<VAR>f : X →ᵇ ℝ<VAR>e : C(X, Y)<VAR>he : ClosedEmbedding ⇑e<GOAL>∃ g, ‖g‖ = ‖f‖ ∧ g.compContinuous e = f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>NormalSpace Y<VAR>f : X →ᵇ ℝ<VAR>e : X → Y<VAR>he : ClosedEmbedding e<GOAL>∃ g, ‖g‖ = ‖f‖ ∧ ⇑g ∘ e = ⇑f
<VAR>Y : Type u_2<VAR>TopologicalSpace Y<VAR>NormalSpace Y<VAR>s : Set Y<VAR>f : ↑s →ᵇ ℝ<VAR>hs : IsClosed s<GOAL>∃ g, ‖g‖ = ‖f‖ ∧ g.restrict s = f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>NormalSpace Y<VAR>f : X →ᵇ ℝ<VAR>a b : ℝ<VAR>e : X → Y<VAR>hf : ∀ (x : X), f x ∈ Set.Icc a b<VAR>hle : a ≤ b<VAR>he : ClosedEmbedding e<GOAL>∃ g, (∀ (y : Y), g y ∈ Set.Icc a b) ∧ ⇑g ∘ e = ⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>NormalSpace Y<VAR>Nonempty X<VAR>f : X →ᵇ ℝ<VAR>e : X → Y<VAR>he : ClosedEmbedding e<GOAL>∃ g, (∀ (y : Y), ∃ x₁ x₂, g y ∈ Set.Icc (f x₁) (f x₂)) ∧ ⇑g ∘ e = ⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>NormalSpace Y<VAR>f : X →ᵇ ℝ<VAR>t : Set ℝ<VAR>e : X → Y<VAR>hs : t.OrdConnected<VAR>hf : ∀ (x : X), f x ∈ t<VAR>hne : t.Nonempty<VAR>he : ClosedEmbedding e<GOAL>∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f
<VAR>Y : Type u_2<VAR>TopologicalSpace Y<VAR>NormalSpace Y<VAR>s : Set Y<VAR>f : ↑s →ᵇ ℝ<VAR>hs : IsClosed s<VAR>t : Set ℝ<VAR>t.OrdConnected<VAR>hf : ∀ (x : ↑s), f x ∈ t<VAR>hne : t.Nonempty<GOAL>∃ g, (∀ (y : Y), g y ∈ t) ∧ g.restrict s = f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>NormalSpace Y<VAR>f : C(X, ℝ)<VAR>t : Set ℝ<VAR>e : X → Y<VAR>hs : t.OrdConnected<VAR>hf : ∀ (x : X), f x ∈ t<VAR>hne : t.Nonempty<VAR>he : ClosedEmbedding e<GOAL>∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f
<VAR>Y : Type u_2<VAR>TopologicalSpace Y<VAR>NormalSpace Y<VAR>s : Set Y<VAR>f : C(↑s, ℝ)<VAR>t : Set ℝ<VAR>t.OrdConnected<VAR>ht : ∀ (x : ↑s), f x ∈ t<VAR>hne : t.Nonempty<VAR>hs : IsClosed s<GOAL>∃ g, (∀ (y : Y), g y ∈ t) ∧ ContinuousMap.restrict s g = f
<VAR>ι : Type u<VAR>X : ι → Type<VAR>(i : ι) → TopologicalSpace (X i)<VAR>C : Set ((i : ι) → X i)<VAR>J : ι → Prop<GOAL>Function.Surjective ⇑(Profinite.IndexFunctor.π_app C J)
<VAR>ι : Type u<VAR>X : ι → Type<VAR>(i : ι) → TopologicalSpace (X i)<VAR>C : Set ((i : ι) → X i)<VAR>J K : ι → Prop<VAR>h : ∀ (i : ι), J i → K i<GOAL>⇑(Profinite.IndexFunctor.map C h) ∘ ⇑(Profinite.IndexFunctor.π_app C K) = ⇑(Profinite.IndexFunctor.π_app C J)
<VAR>ι : Type u<VAR>X : ι → Type<VAR>(i : ι) → TopologicalSpace (X i)<VAR>C : Set ((i : ι) → X i)<VAR>a b : ↑C<VAR>h : ∀ (J : Finset ι), (Profinite.IndexFunctor.π_app C fun x => x ∈ J) a = (Profinite.IndexFunctor.π_app C fun x => x ∈ J) b<GOAL>a = b
<VAR>X Y B : Profinite<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<GOAL>CategoryTheory.CategoryStruct.comp (Profinite.pullback.fst f g) f = CategoryTheory.CategoryStruct.comp (Profinite.pullback.snd f g) g
<VAR>X Y B : Profinite<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<VAR>Z : Profinite<VAR>a : Z ⟶ X<VAR>b : Z ⟶ Y<VAR>w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g<GOAL>CategoryTheory.CategoryStruct.comp (Profinite.pullback.lift f g a b w) (Profinite.pullback.fst f g) = a
<VAR>X Y B : Profinite<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<VAR>Z : Profinite<VAR>a : Z ⟶ X<VAR>b : Z ⟶ Y<VAR>w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g<GOAL>CategoryTheory.CategoryStruct.comp (Profinite.pullback.lift f g a b w) (Profinite.pullback.snd f g) = b
<VAR>X Y B : Profinite<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<VAR>Z : Profinite<VAR>a b : Z ⟶ Profinite.pullback f g<VAR>hfst : CategoryTheory.CategoryStruct.comp a (Profinite.pullback.fst f g) = CategoryTheory.CategoryStruct.comp b (Profinite.pullback.fst f g)<VAR>hsnd : CategoryTheory.CategoryStruct.comp a (Profinite.pullback.snd f g) = CategoryTheory.CategoryStruct.comp b (Profinite.pullback.snd f g)<GOAL>a = b
<VAR>X Y B : Profinite<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<GOAL>(Profinite.pullback.cone f g).pt = Profinite.pullback f g
<VAR>X Y B : Profinite<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<GOAL>(Profinite.pullback.cone f g).π = { app := fun j => Option.rec (CategoryTheory.CategoryStruct.comp (Profinite.pullback.fst f g) f) (fun val => CategoryTheory.Limits.WalkingPair.rec (Profinite.pullback.fst f g) (Profinite.pullback.snd f g) val) j, naturality := ⋯ }
<VAR>X Y B : Profinite<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<VAR>s : CategoryTheory.Limits.PullbackCone f g<GOAL>(Profinite.pullback.isLimit f g).lift s = Profinite.pullback.lift f g s.fst s.snd ⋯
<VAR>X Y B : Profinite<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<GOAL>Profinite.pullback.fst f g = CategoryTheory.CategoryStruct.comp (Profinite.pullbackIsoPullback f g).hom (CategoryTheory.Limits.pullback.fst f g)
<VAR>X Y B : Profinite<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<GOAL>Profinite.pullback.snd f g = CategoryTheory.CategoryStruct.comp (Profinite.pullbackIsoPullback f g).hom (CategoryTheory.Limits.pullback.snd f g)
<VAR>α : Type w<VAR>Finite α<VAR>X : α → Profinite<VAR>B : Profinite<VAR>e : (a : α) → X a ⟶ B<VAR>a : α<GOAL>CategoryTheory.CategoryStruct.comp (Profinite.finiteCoproduct.ι X a) (Profinite.finiteCoproduct.desc X e) = e a
<VAR>α : Type w<VAR>Finite α<VAR>X : α → Profinite<VAR>B : Profinite<VAR>f g : Profinite.finiteCoproduct X ⟶ B<VAR>h : ∀ (a : α), CategoryTheory.CategoryStruct.comp (Profinite.finiteCoproduct.ι X a) f = CategoryTheory.CategoryStruct.comp (Profinite.finiteCoproduct.ι X a) g<GOAL>f = g
<VAR>α : Type w<VAR>Finite α<VAR>X : α → Profinite<VAR>a : α<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι X a) (Profinite.coproductIsoCoproduct X).inv = Profinite.finiteCoproduct.ι X a
<VAR>α : Type w<VAR>Finite α<VAR>X : α → Profinite<VAR>a : α<GOAL>Function.Injective ⇑(Profinite.finiteCoproduct.ι X a)
<VAR>α : Type w<VAR>Finite α<VAR>X : α → Profinite<VAR>R : ↑(Profinite.finiteCoproduct X).toTop<GOAL>∃ a r, R = (Profinite.finiteCoproduct.ι X a) r
<VAR>α : Type w<VAR>Finite α<VAR>X : α → Profinite<VAR>B : Profinite<VAR>π : (a : α) → X a ⟶ B<VAR>a : α<VAR>x : (CategoryTheory.forget Profinite).obj (X a)<GOAL>(Profinite.finiteCoproduct.desc X π) ((Profinite.finiteCoproduct.ι X a) x) = (π a) x
<VAR>X : CompHaus<GOAL>↑(CompHaus.toProfinite.obj X).toTop = ConnectedComponents ↑X.toTop
<VAR>A : FintypeCat<GOAL>DiscreteTopology ↑A
<VAR>A : FintypeCat<GOAL>FintypeCat.toProfinite.obj A = Profinite.of ↑A
<GOAL>∀ {X Y : FintypeCat} (f : X ⟶ Y) (a : ↑X), (FintypeCat.toProfinite.map f) a = f a
<VAR>X Y : Profinite<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Epi f ↔ Function.Surjective ⇑f
<GOAL>ClosedEmbedding ⇑LightProfinite.natUnionInftyEmbedding
<VAR>Y : Type u_1<VAR>TopologicalSpace Y<VAR>f : ↑LightProfinite.NatUnionInfty.toTop → Y<GOAL>Continuous f ↔ Filter.Tendsto (fun x => f (some x)) Filter.atTop (nhds (f ∞))
<VAR>X : Type u<VAR>Fintype X<VAR>TopologicalSpace X<GOAL>↑(FinTopCat.of X).toTop = X
<VAR>P : TopCat → Prop<VAR>CompHausLike.HasExplicitPullbacks P<VAR>hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑f<GOAL>CategoryTheory.Preregular (CompHausLike P)
<VAR>X : CompHaus<VAR>CategoryTheory.Projective X<GOAL>X.toStonean.toTop = X.toTop
<VAR>X Y : Stonean<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Epi f ↔ Function.Surjective ⇑f
<VAR>X Y : CompHaus<VAR>Z : Stonean<VAR>e : Z.compHaus ⟶ Y<VAR>f : X ⟶ Y<VAR>CategoryTheory.Epi f<GOAL>CompHaus.lift e f ≫ f = e
<VAR>X : CompHaus<GOAL>CategoryTheory.Projective X ↔ ExtremallyDisconnected ↑X.toTop
<VAR>X Y : Profinite<VAR>Z : Stonean<VAR>e : Stonean.toProfinite.obj Z ⟶ Y<VAR>f : X ⟶ Y<VAR>CategoryTheory.Epi f<GOAL>Profinite.lift e f ≫ f = e
<VAR>X : Profinite<VAR>hX : ExtremallyDisconnected ↑X.toTop<GOAL>CategoryTheory.Projective X
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.IsCofiltered J<VAR>F : J ⥤ TopCat<VAR>C : CategoryTheory.Limits.Cone F<VAR>hC : CategoryTheory.Limits.IsLimit C<VAR>T : (j : J) → Set (Set ↑(F.obj j))<VAR>hT : ∀ (j : J), TopologicalSpace.IsTopologicalBasis (T j)<VAR>univ : ∀ (i : J), Set.univ ∈ T i<VAR>inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i<VAR>compat : ∀ (i j : J) (f : i ⟶ j), ∀ V ∈ T j, ⇑(F.map f) ⁻¹' V ∈ T i<GOAL>TopologicalSpace.IsTopologicalBasis {U | ∃ j, ∃ V ∈ T j, U = ⇑(C.π.app j) ⁻¹' V}
<VAR>X : TopCat<VAR>U V : TopologicalSpace.Opens ↑X<VAR>x : ↥(U ⊓ V)<GOAL>(fun x => ⟨↑x, ⋯⟩) x = ⟨↑x, ⋯⟩
<VAR>X : TopCat<VAR>U V : TopologicalSpace.Opens ↑X<VAR>x : ↑X<VAR>m : x ∈ U ⊓ V<GOAL>(fun x => ⟨↑x, ⋯⟩) ⟨x, m⟩ = ⟨x, ⋯⟩
<VAR>X : TopCat<VAR>ι : Type u_1<VAR>U : ι → TopologicalSpace.Opens ↑X<VAR>i : ι<VAR>x : ↑X<VAR>m : x ∈ U i<GOAL>(fun x => ⟨↑x, ⋯⟩) ⟨x, m⟩ = ⟨x, ⋯⟩
<VAR>X : TopCat<VAR>U V : TopologicalSpace.Opens ↑X<VAR>f : U ⟶ V<VAR>x : ↑X<VAR>h : x ∈ U<GOAL>((TopologicalSpace.Opens.toTopCat X).map f) ⟨x, h⟩ = ⟨x, ⋯⟩
<VAR>X : TopCat<VAR>U : TopologicalSpace.Opens ↑X<GOAL>⇑U.inclusion = Subtype.val
<VAR>X : TopCat<VAR>U : TopologicalSpace.Opens ↑X<GOAL>OpenEmbedding ⇑U.inclusion
<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>U : TopologicalSpace.Opens ↑Y<GOAL>↑((TopologicalSpace.Opens.map f).obj U) = ⇑f ⁻¹' ↑U
<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>U : Set ↑Y<VAR>p : IsOpen U<GOAL>(TopologicalSpace.Opens.map f).obj { carrier := U, is_open' := p } = { carrier := ⇑f ⁻¹' U, is_open' := ⋯ }
<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>U V : TopologicalSpace.Opens ↑Y<VAR>e : U ≤ V<GOAL>(TopologicalSpace.Opens.map f).map (CategoryTheory.homOfLE e) = CategoryTheory.homOfLE ⋯
<VAR>X : TopCat<VAR>U : TopologicalSpace.Opens ↑X<GOAL>(TopologicalSpace.Opens.map (𝟙 X)).obj U = U
<VAR>X : TopCat<VAR>U : Set ↑X<VAR>p : IsOpen U<GOAL>(TopologicalSpace.Opens.map (𝟙 X)).obj { carrier := U, is_open' := p } = { carrier := U, is_open' := p }
<VAR>X : TopCat<VAR>U : (TopologicalSpace.Opens ↑X)ᵒᵖ<GOAL>(TopologicalSpace.Opens.map (𝟙 X)).obj (Opposite.unop U) = Opposite.unop U
<VAR>X : TopCat<VAR>U : (TopologicalSpace.Opens ↑X)ᵒᵖ<GOAL>(TopologicalSpace.Opens.map (𝟙 X)).op.obj U = U
<VAR>X Y : TopCat<VAR>f : X ⟶ Y<GOAL>(TopologicalSpace.Opens.map f).obj ⊤ = ⊤
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>U : TopologicalSpace.Opens ↑Z<GOAL>(TopologicalSpace.Opens.map (f ≫ g)).obj U = (TopologicalSpace.Opens.map f).obj ((TopologicalSpace.Opens.map g).obj U)
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>U : Set ↑Z<VAR>p : IsOpen U<GOAL>(TopologicalSpace.Opens.map (f ≫ g)).obj { carrier := U, is_open' := p } = (TopologicalSpace.Opens.map f).obj ((TopologicalSpace.Opens.map g).obj { carrier := U, is_open' := p })
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>U V : TopologicalSpace.Opens ↑Z<VAR>i : U ⟶ V<GOAL>(TopologicalSpace.Opens.map (f ≫ g)).map i = (TopologicalSpace.Opens.map f).map ((TopologicalSpace.Opens.map g).map i)
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>U : (TopologicalSpace.Opens ↑Z)ᵒᵖ<GOAL>(TopologicalSpace.Opens.map (f ≫ g)).obj (Opposite.unop U) = (TopologicalSpace.Opens.map f).obj ((TopologicalSpace.Opens.map g).obj (Opposite.unop U))
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>U : (TopologicalSpace.Opens ↑Z)ᵒᵖ<GOAL>(TopologicalSpace.Opens.map (f ≫ g)).op.obj U = (TopologicalSpace.Opens.map f).op.obj ((TopologicalSpace.Opens.map g).op.obj U)
<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>ι : Type u_1<VAR>U : ι → TopologicalSpace.Opens ↑Y<GOAL>(TopologicalSpace.Opens.map f).obj (iSup U) = iSup ((TopologicalSpace.Opens.map f).obj ∘ U)
<VAR>X : TopCat<VAR>U : TopologicalSpace.Opens ↑X<GOAL>(TopologicalSpace.Opens.mapId X).inv.app U = CategoryTheory.eqToHom ⋯
<VAR>X : TopCat<VAR>U : TopologicalSpace.Opens ↑X<GOAL>(TopologicalSpace.Opens.mapId X).hom.app U = CategoryTheory.eqToHom ⋯
<VAR>X : TopCat<GOAL>TopologicalSpace.Opens.map (𝟙 X) = 𝟭 (TopologicalSpace.Opens ↑X)
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>U : TopologicalSpace.Opens ↑Z<GOAL>(TopologicalSpace.Opens.mapComp f g).inv.app U = CategoryTheory.eqToHom ⋯
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>U : TopologicalSpace.Opens ↑Z<GOAL>(TopologicalSpace.Opens.mapComp f g).hom.app U = CategoryTheory.eqToHom ⋯
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>TopologicalSpace.Opens.map (f ≫ g) = TopologicalSpace.Opens.map g ⋙ TopologicalSpace.Opens.map f
<VAR>X Y : TopCat<VAR>f g : X ⟶ Y<VAR>h : f = g<GOAL>TopologicalSpace.Opens.map f = TopologicalSpace.Opens.map g
<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>h : f = f<GOAL>TopologicalSpace.Opens.mapIso f f h = CategoryTheory.Iso.refl (TopologicalSpace.Opens.map f)
<VAR>X Y : TopCat<VAR>f g : X ⟶ Y<VAR>h : f = g<VAR>U : TopologicalSpace.Opens ↑Y<GOAL>(TopologicalSpace.Opens.mapIso f g h).hom.app U = CategoryTheory.eqToHom ⋯
<VAR>X Y : TopCat<VAR>f g : X ⟶ Y<VAR>h : f = g<VAR>U : TopologicalSpace.Opens ↑Y<GOAL>(TopologicalSpace.Opens.mapIso f g h).inv.app U = CategoryTheory.eqToHom ⋯
<VAR>X Y : TopCat<VAR>H : X ≅ Y<GOAL>(TopologicalSpace.Opens.mapMapIso H).functor = TopologicalSpace.Opens.map H.hom
<VAR>X Y : TopCat<VAR>H : X ≅ Y<GOAL>(TopologicalSpace.Opens.mapMapIso H).inverse = TopologicalSpace.Opens.map H.inv
<VAR>X Y : TopCat<VAR>H : X ≅ Y<GOAL>(TopologicalSpace.Opens.mapMapIso H).unitIso = CategoryTheory.NatIso.ofComponents (fun U => CategoryTheory.eqToIso ⋯) ⋯
<VAR>X Y : TopCat<VAR>H : X ≅ Y<GOAL>(TopologicalSpace.Opens.mapMapIso H).counitIso = CategoryTheory.NatIso.ofComponents (fun U => CategoryTheory.eqToIso ⋯) ⋯
<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>hf : IsOpenMap ⇑f<VAR>U : TopologicalSpace.Opens ↑X<GOAL>↑(hf.functor.obj U) = ⇑f '' ↑U
<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>hf : OpenEmbedding ⇑f<GOAL>Function.Injective ⋯.functor.obj
<VAR>X : TopCat<VAR>U : TopologicalSpace.Opens ↑X<GOAL>⋯.functor.obj ⊤ = U
<VAR>X : TopCat<VAR>U : TopologicalSpace.Opens ↑X<GOAL>(TopologicalSpace.Opens.map U.inclusion).obj U = ⊤
<VAR>X : TopCat<VAR>U : TopologicalSpace.Opens ↑X<GOAL>⋯.adjunction.counit.app U = CategoryTheory.eqToHom ⋯
<VAR>X : TopCat<GOAL>⋯.functor = TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusionTopIso X).inv
<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>hf : IsOpenMap ⇑f<VAR>U : TopologicalSpace.Opens ↑Y<GOAL>hf.functor.obj ((TopologicalSpace.Opens.map f).obj U) = hf.functor.obj ⊤ ⊓ U
<VAR>X : TopCat<VAR>U : TopologicalSpace.Opens ↑X<GOAL>Set.range ((CategoryTheory.forget TopCat).map U.inclusion) = ↑U
<VAR>X : TopCat<VAR>U V : TopologicalSpace.Opens ↑X<GOAL>⋯.functor.obj ((TopologicalSpace.Opens.map U.inclusion).obj V) = V ⊓ U
<VAR>X U : TopCat<VAR>f : U ⟶ X<VAR>hf : OpenEmbedding ⇑f<VAR>V : TopologicalSpace.Opens ↑U<GOAL>(TopologicalSpace.Opens.map f).obj (⋯.functor.obj V) = V
<VAR>X : TopCat<VAR>U : TopologicalSpace.Opens ↑X<VAR>V : TopologicalSpace.Opens ↥U<GOAL>(TopologicalSpace.Opens.map U.inclusion).obj (⋯.functor.obj V) = V
<VAR>X : TopCat<VAR>U : TopologicalSpace.Opens ↑X<VAR>V : TopologicalSpace.Opens ↥U<GOAL>⋯.adjunction.counit.app (⋯.functor.obj V) = CategoryTheory.eqToHom ⋯
<VAR>P : TopCat → Prop<VAR>self : CompHausLike P<GOAL>CompactSpace ↑self.toTop
<VAR>P : TopCat → Prop<VAR>self : CompHausLike P<GOAL>P self.toTop
<VAR>P : TopCat → Prop<VAR>self : CompHausLike P<GOAL>T2Space ↑self.toTop
<VAR>P : TopCat → Prop<VAR>X : Type u<VAR>TopologicalSpace X<VAR>self : CompHausLike.HasProp P X<GOAL>P (TopCat.of X)
<VAR>P : TopCat → Prop<VAR>X : Type u<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>T2Space X<VAR>CompHausLike.HasProp P X<GOAL>↑(CompHausLike.of P X).toTop = X
<VAR>P : TopCat → Prop<VAR>X : CompHausLike P<GOAL>𝟙 ((CategoryTheory.forget (CompHausLike P)).obj X) = id
<VAR>P : TopCat → Prop<VAR>X Y Z : CompHausLike P<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.forget (CompHausLike P)).map f ≫ (CategoryTheory.forget (CompHausLike P)).map g = ⇑g ∘ ⇑f
<VAR>P P' : TopCat → Prop<VAR>h : ∀ (X : CompHausLike P), P X.toTop → P' X.toTop<GOAL>∀ {X Y : CompHausLike P} (f : X ⟶ Y), (CompHausLike.toCompHausLike h).map f = f
<VAR>P P' : TopCat → Prop<VAR>h : ∀ (X : CompHausLike P), P X.toTop → P' X.toTop<VAR>X : CompHausLike P<GOAL>(CompHausLike.toCompHausLike h).obj X = let_fun this := ⋯; CompHausLike.of P' ↑X.toTop
<VAR>P : TopCat → Prop<GOAL>∀ {X Y : CategoryTheory.InducedCategory TopCat CompHausLike.toTop} (f : X ⟶ Y), (CompHausLike.compHausLikeToTop P).map f = f
<VAR>P : TopCat → Prop<VAR>self : CompHausLike P<GOAL>(CompHausLike.compHausLikeToTop P).obj self = self.toTop
<VAR>P : TopCat → Prop<VAR>X Y : CompHausLike P<VAR>f : X ⟶ Y<VAR>hf : Function.Surjective ⇑f<GOAL>CategoryTheory.Epi f
<VAR>P : TopCat → Prop<VAR>X Y : CompHausLike P<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Mono f ↔ Function.Injective ⇑f
<VAR>P : TopCat → Prop<VAR>X Y : CompHausLike P<VAR>f : X ⟶ Y<GOAL>IsClosedMap ⇑f
<VAR>P : TopCat → Prop<VAR>X Y : CompHausLike P<VAR>f : X ⟶ Y<VAR>bij : Function.Bijective ⇑f<GOAL>CategoryTheory.IsIso f
<VAR>P : TopCat → Prop<VAR>X Y : CompHausLike P<VAR>f : ↑X.toTop ≃ₜ ↑Y.toTop<VAR>a : ↑((CompHausLike.compHausLikeToTop P).obj X)<GOAL>(CompHausLike.isoOfHomeo f).hom a = f a
<VAR>P : TopCat → Prop<VAR>X Y : CompHausLike P<VAR>f : ↑X.toTop ≃ₜ ↑Y.toTop<VAR>a : ↑((CompHausLike.compHausLikeToTop P).obj Y)<GOAL>(CompHausLike.isoOfHomeo f).inv a = f.symm a
<VAR>P : TopCat → Prop<VAR>X Y : CompHausLike P<VAR>f : X ≅ Y<VAR>a : ↑Y.toTop<GOAL>(CompHausLike.homeoOfIso f).symm a = f.inv a
<VAR>P : TopCat → Prop<VAR>X Y : CompHausLike P<VAR>f : X ≅ Y<VAR>a : ↑X.toTop<GOAL>(CompHausLike.homeoOfIso f) a = f.hom a
<VAR>P : TopCat → Prop<VAR>X Y : CompHausLike P<VAR>f : ↑X.toTop ≃ₜ ↑Y.toTop<GOAL>CompHausLike.isoEquivHomeo.symm f = CompHausLike.isoOfHomeo f
<VAR>P : TopCat → Prop<VAR>X Y : CompHausLike P<VAR>f : X ≅ Y<GOAL>CompHausLike.isoEquivHomeo f = CompHausLike.homeoOfIso f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>J : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} J<VAR>K : J ⥤ C<VAR>F : C ⥤ D<VAR>CategoryTheory.CreatesLimit K F<VAR>c : CategoryTheory.Limits.Cone (K ⋙ F)<VAR>t : CategoryTheory.Limits.IsLimit c<VAR>n : J<GOAL>(CategoryTheory.liftedLimitMapsToOriginal t).inv.hom ≫ F.map ((CategoryTheory.liftLimit t).π.app n) = c.π.app n
<VAR>S : LightProfinite<VAR>n : ℕ<GOAL>lightToProfinite.map (S.proj n) = (lightToProfinite.obj S).asLimitCone.π.app ((CategoryTheory.Limits.sequentialFunctor (DiscreteQuotient ↑(lightToProfinite.obj S).toTop)).obj (Opposite.op n))
<VAR>S : LightProfinite<VAR>n : ℕ<GOAL>Function.Surjective ⇑(S.proj n)
<VAR>S : LightProfinite<VAR>n : ℕ<GOAL>S.proj (n + 1) ≫ S.diagram.map (Opposite.op (CategoryTheory.homOfLE ⋯)) = S.proj n
<VAR>S : LightProfinite<VAR>n m : ℕ<VAR>h : n ≤ m<GOAL>S.proj m ≫ S.diagram.map (Opposite.op (CategoryTheory.homOfLE h)) = S.proj n
<VAR>X Y B : LightProfinite<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<GOAL>CategoryTheory.CategoryStruct.comp (LightProfinite.pullback.fst f g) f = CategoryTheory.CategoryStruct.comp (LightProfinite.pullback.snd f g) g
<VAR>X Y B : LightProfinite<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<VAR>Z : LightProfinite<VAR>a : Z ⟶ X<VAR>b : Z ⟶ Y<VAR>w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g<GOAL>CategoryTheory.CategoryStruct.comp (LightProfinite.pullback.lift f g a b w) (LightProfinite.pullback.fst f g) = a
<VAR>X Y B : LightProfinite<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<VAR>Z : LightProfinite<VAR>a : Z ⟶ X<VAR>b : Z ⟶ Y<VAR>w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g<GOAL>CategoryTheory.CategoryStruct.comp (LightProfinite.pullback.lift f g a b w) (LightProfinite.pullback.snd f g) = b
<VAR>X Y B : LightProfinite<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<VAR>Z : LightProfinite<VAR>a b : Z ⟶ LightProfinite.pullback f g<VAR>hfst : CategoryTheory.CategoryStruct.comp a (LightProfinite.pullback.fst f g) = CategoryTheory.CategoryStruct.comp b (LightProfinite.pullback.fst f g)<VAR>hsnd : CategoryTheory.CategoryStruct.comp a (LightProfinite.pullback.snd f g) = CategoryTheory.CategoryStruct.comp b (LightProfinite.pullback.snd f g)<GOAL>a = b
<VAR>X Y B : LightProfinite<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<GOAL>(LightProfinite.pullback.cone f g).pt = LightProfinite.pullback f g
<VAR>X Y B : LightProfinite<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<GOAL>(LightProfinite.pullback.cone f g).π = { app := fun j => Option.rec (CategoryTheory.CategoryStruct.comp (LightProfinite.pullback.fst f g) f) (fun val => CategoryTheory.Limits.WalkingPair.rec (LightProfinite.pullback.fst f g) (LightProfinite.pullback.snd f g) val) j, naturality := ⋯ }