ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : TopCat<VAR>s : Set (Quotient (t2Setoid (PreStoneCech ↑X)))<GOAL>TopologicalSpace.IsOpen s = IsOpen (Quotient.mk' ⁻¹' s)
<VAR>X : TopCat<GOAL>↑(stoneCechObj X).toTop = StoneCech ↑X
<VAR>X : TopCat<GOAL>↑(topToCompHaus.obj X).toTop = StoneCech ↑X
<VAR>X Y : CompHaus<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Epi f ↔ Function.Surjective ⇑f
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>x : ↑(TopCat.of { p // f p.1 = g p.2 })<GOAL>(TopCat.pullbackFst f g) x = (↑x).1
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>x : ↑(TopCat.of { p // f p.1 = g p.2 })<GOAL>(TopCat.pullbackSnd f g) x = (↑x).2
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(TopCat.pullbackIsoProdSubtype f g).inv ≫ CategoryTheory.Limits.pullback.fst f g = TopCat.pullbackFst f g
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>x : { p // f p.1 = g p.2 }<GOAL>(CategoryTheory.Limits.pullback.fst f g) ((TopCat.pullbackIsoProdSubtype f g).inv x) = (↑x).1
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(TopCat.pullbackIsoProdSubtype f g).inv ≫ CategoryTheory.Limits.pullback.snd f g = TopCat.pullbackSnd f g
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>x : { p // f p.1 = g p.2 }<GOAL>(CategoryTheory.Limits.pullback.snd f g) ((TopCat.pullbackIsoProdSubtype f g).inv x) = (↑x).2
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(TopCat.pullbackIsoProdSubtype f g).hom ≫ TopCat.pullbackFst f g = CategoryTheory.Limits.pullback.fst f g
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(TopCat.pullbackIsoProdSubtype f g).hom ≫ TopCat.pullbackSnd f g = CategoryTheory.Limits.pullback.snd f g
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>x : CategoryTheory.ConcreteCategory.forget.obj (CategoryTheory.Limits.pullback f g)<GOAL>(TopCat.pullbackIsoProdSubtype f g).hom x = ⟨((CategoryTheory.Limits.pullback.fst f g) x, (CategoryTheory.Limits.pullback.snd f g) x), ⋯⟩
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.Limits.pullback f g).str = TopologicalSpace.induced (⇑(CategoryTheory.Limits.pullback.fst f g)) X.str ⊓ TopologicalSpace.induced (⇑(CategoryTheory.Limits.pullback.snd f g)) Y.str
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>Set.range ⇑(CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.snd f g)) = {x | (CategoryTheory.Limits.prod.fst ≫ f) x = (CategoryTheory.Limits.prod.snd ≫ g) x}
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>Inducing ⇑(CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.snd f g))
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>Embedding ⇑(CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.snd f g))
<VAR>W X Y Z S T : TopCat<VAR>f₁ : W ⟶ S<VAR>f₂ : X ⟶ S<VAR>g₁ : Y ⟶ T<VAR>g₂ : Z ⟶ T<VAR>i₁ : W ⟶ Y<VAR>i₂ : X ⟶ Z<VAR>i₃ : S ⟶ T<VAR>H₃ : CategoryTheory.Mono i₃<VAR>eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁<VAR>eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂<GOAL>Set.range ⇑(CategoryTheory.Limits.pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) = ⇑(CategoryTheory.Limits.pullback.fst g₁ g₂) ⁻¹' Set.range ⇑i₁ ∩ ⇑(CategoryTheory.Limits.pullback.snd g₁ g₂) ⁻¹' Set.range ⇑i₂
<VAR>X Y S : TopCat<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<GOAL>Set.range ⇑(CategoryTheory.Limits.pullback.fst f g) = {x | ∃ y, f x = g y}
<VAR>X Y S : TopCat<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<GOAL>Set.range ⇑(CategoryTheory.Limits.pullback.snd f g) = {y | ∃ x, f x = g y}
<VAR>W X Y Z S T : TopCat<VAR>f₁ : W ⟶ S<VAR>f₂ : X ⟶ S<VAR>g₁ : Y ⟶ T<VAR>g₂ : Z ⟶ T<VAR>i₁ : W ⟶ Y<VAR>i₂ : X ⟶ Z<VAR>H₁ : Embedding ⇑i₁<VAR>H₂ : Embedding ⇑i₂<VAR>i₃ : S ⟶ T<VAR>eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁<VAR>eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂<GOAL>Embedding ⇑(CategoryTheory.Limits.pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
<VAR>W X Y Z S T : TopCat<VAR>f₁ : W ⟶ S<VAR>f₂ : X ⟶ S<VAR>g₁ : Y ⟶ T<VAR>g₂ : Z ⟶ T<VAR>i₁ : W ⟶ Y<VAR>i₂ : X ⟶ Z<VAR>H₁ : OpenEmbedding ⇑i₁<VAR>H₂ : OpenEmbedding ⇑i₂<VAR>i₃ : S ⟶ T<VAR>H₃ : CategoryTheory.Mono i₃<VAR>eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁<VAR>eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂<GOAL>OpenEmbedding ⇑(CategoryTheory.Limits.pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
<VAR>X Y S : TopCat<VAR>f : X ⟶ S<VAR>H : Embedding ⇑f<VAR>g : Y ⟶ S<GOAL>Embedding ⇑(CategoryTheory.Limits.pullback.snd f g)
<VAR>X Y S : TopCat<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H : Embedding ⇑g<GOAL>Embedding ⇑(CategoryTheory.Limits.pullback.fst f g)
<VAR>X Y S : TopCat<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H₁ : Embedding ⇑f<VAR>H₂ : Embedding ⇑g<GOAL>Embedding ⇑(CategoryTheory.Limits.limit.π (CategoryTheory.Limits.cospan f g) CategoryTheory.Limits.WalkingCospan.one)
<VAR>X Y S : TopCat<VAR>f : X ⟶ S<VAR>H : OpenEmbedding ⇑f<VAR>g : Y ⟶ S<GOAL>OpenEmbedding ⇑(CategoryTheory.Limits.pullback.snd f g)
<VAR>X Y S : TopCat<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H : OpenEmbedding ⇑g<GOAL>OpenEmbedding ⇑(CategoryTheory.Limits.pullback.fst f g)
<VAR>X Y S : TopCat<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H₁ : OpenEmbedding ⇑f<VAR>H₂ : OpenEmbedding ⇑g<GOAL>OpenEmbedding ⇑(CategoryTheory.Limits.limit.π (CategoryTheory.Limits.cospan f g) CategoryTheory.Limits.WalkingCospan.one)
<VAR>X Y S : TopCat<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>hg : Embedding ⇑g<VAR>H : Set.range ⇑f ⊆ Set.range ⇑g<GOAL>CategoryTheory.IsIso (CategoryTheory.Limits.pullback.fst f g)
<VAR>X Y S : TopCat<VAR>f : X ⟶ S<VAR>hf : Embedding ⇑f<VAR>g : Y ⟶ S<VAR>H : Set.range ⇑g ⊆ Set.range ⇑f<GOAL>CategoryTheory.IsIso (CategoryTheory.Limits.pullback.snd f g)
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>U : Set ↑X<GOAL>⇑(CategoryTheory.Limits.pullback.snd f g) '' (⇑(CategoryTheory.Limits.pullback.fst f g) ⁻¹' U) = ⇑g ⁻¹' (⇑f '' U)
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>U : Set ↑Y<GOAL>⇑(CategoryTheory.Limits.pullback.fst f g) '' (⇑(CategoryTheory.Limits.pullback.snd f g) ⁻¹' U) = ⇑f ⁻¹' (⇑g '' U)
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ TopCat<VAR>c : CategoryTheory.Limits.Cocone F<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>c.pt.str = ⨆ j, TopologicalSpace.coinduced (⇑(c.ι.app j)) (F.obj j).str
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ TopCat<GOAL>(CategoryTheory.Limits.colimit F).str = ⨆ j, TopologicalSpace.coinduced (⇑(CategoryTheory.Limits.colimit.ι F j)) (F.obj j).str
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ TopCat<VAR>U : Set ↑(CategoryTheory.Limits.colimit F)<GOAL>IsOpen U ↔ ∀ (j : J), IsOpen (⇑(CategoryTheory.Limits.colimit.ι F j) ⁻¹' U)
<VAR>F : CategoryTheory.Limits.WalkingParallelPair ⥤ TopCat<VAR>U : Set ↑(CategoryTheory.Limits.colimit F)<GOAL>IsOpen U ↔ IsOpen (⇑(CategoryTheory.Limits.colimit.ι F CategoryTheory.Limits.WalkingParallelPair.one) ⁻¹' U)
<VAR>A : FintypeCat<VAR>u : Set ↑A<GOAL>TopologicalSpace.IsOpen u = (u ∈ ⊤)
<GOAL>∀ {X Y : FintypeCat} (f : X ⟶ Y) (a : ↑X), (FintypeCat.toLightProfinite.map f) a = f a
<VAR>A : FintypeCat<GOAL>↑(FintypeCat.toLightProfinite.obj A).toTop = ↑A
<VAR>X Y : LightProfinite<VAR>f : X ⟶ Y<GOAL>IsClosedMap ⇑f
<VAR>X Y : LightProfinite<VAR>f : X ⟶ Y<VAR>bij : Function.Bijective ⇑f<GOAL>CategoryTheory.IsIso f
<VAR>X Y : LightProfinite<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Epi f ↔ Function.Surjective ⇑f
<VAR>X : CategoryTheory.InducedCategory Profinite LightDiagram.toProfinite<VAR>a : ↑(LightDiagram.toProfinite X).toTop<GOAL>(𝟙 X) a = a
<GOAL>∀ {X Y Z : CategoryTheory.InducedCategory Profinite LightDiagram.toProfinite} (f : X ⟶ Y) (g : Y ⟶ Z) (a : ↑(LightDiagram.toProfinite X).toTop), (f ≫ g) a = g (f a)
<GOAL>∀ {X Y : CategoryTheory.InducedCategory Profinite LightDiagram.toProfinite} (f : X ⟶ Y), lightDiagramToProfinite.map f = f
<VAR>S : LightDiagram<GOAL>lightDiagramToProfinite.obj S = S.toProfinite
<VAR>X : LightProfinite<GOAL>lightProfiniteToLightDiagram.obj X = X.toLightDiagram
<GOAL>∀ {X Y : LightProfinite} (f : X ⟶ Y), lightProfiniteToLightDiagram.map f = f
<VAR>X : LightDiagram<GOAL>lightDiagramToLightProfinite.obj X = LightProfinite.of ↑X.cone.pt.toTop
<GOAL>∀ {X Y : LightDiagram} (f : X ⟶ Y), lightDiagramToLightProfinite.map f = f
<VAR>α : Type<VAR>Finite α<VAR>X : α → Stonean<VAR>B : Stonean<VAR>e : (a : α) → X a ⟶ B<VAR>a : α<GOAL>Stonean.finiteCoproduct.ι X a ≫ Stonean.finiteCoproduct.desc X e = e a
<VAR>α : Type<VAR>Finite α<VAR>X : α → Stonean<VAR>B : Stonean<VAR>f g : Stonean.finiteCoproduct X ⟶ B<VAR>h : ∀ (a : α), Stonean.finiteCoproduct.ι X a ≫ f = Stonean.finiteCoproduct.ι X a ≫ g<GOAL>f = g
<VAR>α : Type<VAR>Finite α<VAR>Z : α → Stonean<VAR>a : α<GOAL>OpenEmbedding ⇑(Stonean.finiteCoproduct.ι Z a)
<VAR>α : Type<VAR>Finite α<VAR>Z : α → Stonean<VAR>a : α<GOAL>OpenEmbedding ⇑(CategoryTheory.Limits.Sigma.ι Z a)
<VAR>X Y Z : Stonean<VAR>f : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>hi : OpenEmbedding ⇑i<GOAL>Stonean.pullback.fst f hi ≫ f = Stonean.pullback.snd f hi ≫ i
<VAR>X Y Z : Stonean<VAR>f : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>hi : OpenEmbedding ⇑i<VAR>W : Stonean<VAR>a : W ⟶ X<VAR>b : W ⟶ Y<VAR>w : a ≫ f = b ≫ i<GOAL>Stonean.pullback.lift f hi a b w ≫ Stonean.pullback.fst f hi = a
<VAR>X Y Z W : Stonean<VAR>f : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>hi : OpenEmbedding ⇑i<VAR>a : W ⟶ X<VAR>b : W ⟶ Y<VAR>w : a ≫ f = b ≫ i<GOAL>Stonean.pullback.lift f hi a b w ≫ Stonean.pullback.snd f hi = b
<VAR>X Y Z : Stonean<VAR>f : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>hi : OpenEmbedding ⇑i<GOAL>(Stonean.pullback.cone f hi).π = { app := fun j => Option.rec (Stonean.pullback.fst f hi ≫ f) (fun val => CategoryTheory.Limits.WalkingPair.rec (Stonean.pullback.fst f hi) (Stonean.pullback.snd f hi) val) j, naturality := ⋯ }
<VAR>X Y Z : Stonean<VAR>f : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>hi : OpenEmbedding ⇑i<GOAL>(Stonean.pullback.cone f hi).pt = Stonean.pullback f hi
<VAR>X Y Z W : Stonean<VAR>f : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>hi : OpenEmbedding ⇑i<VAR>a b : W ⟶ (Stonean.pullback.cone f hi).pt<VAR>hfst : a ≫ Stonean.pullback.fst f hi = b ≫ Stonean.pullback.fst f hi<GOAL>a = b
<VAR>X Y Z : Stonean<VAR>f : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>hi : OpenEmbedding ⇑i<GOAL>CategoryTheory.Limits.HasPullback f i
<VAR>X Y Z : Stonean<VAR>f : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>hi : OpenEmbedding ⇑i<GOAL>(Stonean.pullbackIsoPullback f hi).hom = CategoryTheory.Limits.pullback.lift (Stonean.pullback.fst f hi) (Stonean.pullback.snd f hi) ⋯
<VAR>X Y Z : Stonean<VAR>f : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>hi : OpenEmbedding ⇑i<GOAL>(Stonean.pullbackIsoPullback f hi).inv = Stonean.pullback.lift f hi (CategoryTheory.Limits.pullback.fst f i) (CategoryTheory.Limits.pullback.snd f i) ⋯
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>𝕜 : Type u_3<VAR>UniformSpace 𝕜<GOAL>𝓤 (Matrix m n 𝕜) = ⨅ i, ⨅ j, Filter.comap (fun a => (a.1 i j, a.2 i j)) (𝓤 𝕜)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>𝕜 : Type u_3<VAR>UniformSpace 𝕜<VAR>β : Type u_4<VAR>UniformSpace β<VAR>f : β → Matrix m n 𝕜<GOAL>UniformContinuous f ↔ ∀ (i : m) (j : n), UniformContinuous fun x => f x i j
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace E<VAR>TopologicalSpace X<VAR>f : E → X<VAR>x : X<VAR>I : Type u_3<VAR>TopologicalSpace I<VAR>h : IsEvenlyCovered f x I<GOAL>x ∈ h.toTrivialization.baseSet
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace E<VAR>TopologicalSpace X<VAR>f : E → X<VAR>x : E<VAR>I : Type u_3<VAR>TopologicalSpace I<VAR>h : IsEvenlyCovered f (f x) I<GOAL>(↑h.toTrivialization x).2 = ⟨x, ⋯⟩
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace E<VAR>TopologicalSpace X<VAR>f : E → X<VAR>x : E<VAR>I : Type u_3<VAR>TopologicalSpace I<VAR>h : IsEvenlyCovered f (f x) I<GOAL>ContinuousAt f x
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace E<VAR>TopologicalSpace X<VAR>f : E → X<VAR>x : X<VAR>I : Type u_3<VAR>TopologicalSpace I<VAR>h : IsEvenlyCovered f x I<GOAL>IsEvenlyCovered f x ↑(f ⁻¹' {x})
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace E<VAR>TopologicalSpace X<VAR>f : E → X<VAR>s : Set X<VAR>F : X → Type u_3<VAR>(x : X) → TopologicalSpace (F x)<VAR>hF : ∀ (x : X), DiscreteTopology (F x)<VAR>e : (x : X) → x ∈ s → Trivialization (F x) f<VAR>h : ∀ (x : X) (hx : x ∈ s), x ∈ (e x hx).baseSet<GOAL>IsCoveringMapOn f s
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace E<VAR>TopologicalSpace X<VAR>f : E → X<VAR>s : Set X<VAR>hf : IsCoveringMapOn f s<VAR>x : E<VAR>hx : f x ∈ s<GOAL>ContinuousAt f x
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace E<VAR>TopologicalSpace X<VAR>f : E → X<VAR>s : Set X<VAR>hf : IsCoveringMapOn f s<GOAL>ContinuousOn f (f ⁻¹' s)
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace E<VAR>TopologicalSpace X<VAR>f : E → X<VAR>s : Set X<VAR>hf : IsCoveringMapOn f s<GOAL>IsLocalHomeomorphOn f (f ⁻¹' s)
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace E<VAR>TopologicalSpace X<VAR>f : E → X<GOAL>IsCoveringMap f ↔ IsCoveringMapOn f Set.univ
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace E<VAR>TopologicalSpace X<VAR>f : E → X<VAR>hf : IsCoveringMap f<GOAL>IsCoveringMapOn f Set.univ
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace E<VAR>TopologicalSpace X<VAR>f : E → X<VAR>F : X → Type u_3<VAR>(x : X) → TopologicalSpace (F x)<VAR>∀ (x : X), DiscreteTopology (F x)<VAR>e : (x : X) → Trivialization (F x) f<VAR>h : ∀ (x : X), x ∈ (e x).baseSet<GOAL>IsCoveringMap f
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace E<VAR>TopologicalSpace X<VAR>f : E → X<VAR>hf : IsCoveringMap f<GOAL>Continuous f
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace E<VAR>TopologicalSpace X<VAR>f : E → X<VAR>hf : IsCoveringMap f<GOAL>IsLocalHomeomorph f
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace E<VAR>TopologicalSpace X<VAR>f : E → X<VAR>hf : IsCoveringMap f<GOAL>IsOpenMap f
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace E<VAR>TopologicalSpace X<VAR>f : E → X<VAR>hf : IsCoveringMap f<VAR>hf' : Function.Surjective f<GOAL>QuotientMap f
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace E<VAR>TopologicalSpace X<VAR>f : E → X<VAR>hf : IsCoveringMap f<GOAL>IsSeparatedMap f
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace E<VAR>TopologicalSpace X<VAR>f : E → X<VAR>hf : IsCoveringMap f<VAR>A : Type u_3<VAR>TopologicalSpace A<VAR>g₁ g₂ : A → E<VAR>PreconnectedSpace A<VAR>h₁ : Continuous g₁<VAR>h₂ : Continuous g₂<VAR>he : f ∘ g₁ = f ∘ g₂<VAR>a : A<VAR>ha : g₁ a = g₂ a<GOAL>g₁ = g₂
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace E<VAR>TopologicalSpace X<VAR>f : E → X<VAR>hf : IsCoveringMap f<VAR>A : Type u_3<VAR>TopologicalSpace A<VAR>s : Set A<VAR>hs : IsPreconnected s<VAR>g₁ g₂ : A → E<VAR>h₁ : ContinuousOn g₁ s<VAR>h₂ : ContinuousOn g₂ s<VAR>he : Set.EqOn (f ∘ g₁) (f ∘ g₂) s<VAR>a : A<VAR>has : a ∈ s<VAR>ha : g₁ a = g₂ a<GOAL>Set.EqOn g₁ g₂ s
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace E<VAR>TopologicalSpace X<VAR>f : E → X<VAR>hf : IsCoveringMap f<VAR>A : Type u_3<VAR>TopologicalSpace A<VAR>g : A → E<VAR>PreconnectedSpace A<VAR>cont : Continuous g<VAR>he : ∀ (a a' : A), f (g a) = f (g a')<VAR>a a' : A<GOAL>g a = g a'
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace E<VAR>TopologicalSpace X<VAR>f : E → X<VAR>hf : IsCoveringMap f<VAR>A : Type u_3<VAR>TopologicalSpace A<VAR>s : Set A<VAR>hs : IsPreconnected s<VAR>g : A → E<VAR>cont : ContinuousOn g s<VAR>he : ∀ a ∈ s, ∀ a' ∈ s, f (g a) = f (g a')<VAR>a a' : A<VAR>ha : a ∈ s<VAR>ha' : a' ∈ s<GOAL>g a = g a'
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace E<VAR>TopologicalSpace X<VAR>f : E → X<VAR>F : Type u_3<VAR>TopologicalSpace F<VAR>DiscreteTopology F<VAR>hf : ∀ (x : X), ∃ e, x ∈ e.baseSet<GOAL>IsCoveringMap f
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>F : Type u_3<VAR>E : X → Type u_4<VAR>TopologicalSpace F<VAR>DiscreteTopology F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : X) → TopologicalSpace (E x)<VAR>FiberBundle F E<GOAL>IsCoveringMap Bundle.TotalSpace.proj
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>T0Space α<VAR>s : Set α<VAR>h : IsComplete s<GOAL>IsClosed s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>UniformSpace β<VAR>CompleteSpace α<VAR>T0Space β<VAR>f : α → β<VAR>hf : UniformEmbedding f<GOAL>ClosedEmbedding f
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>γ : Type u_4<VAR>UniformSpace γ<VAR>CompleteSpace γ<VAR>T0Space γ<VAR>e : α → β<VAR>f : α → γ<VAR>de : DenseInducing e<VAR>h : ∀ (b : β), Cauchy (Filter.map f (Filter.comap e (𝓝 b)))<GOAL>Continuous (de.extend f)
<VAR>ι : Type u_1<VAR>α : ι → Type u<VAR>U : (i : ι) → UniformSpace (α i)<GOAL>Pi.uniformSpace α = ⨅ i, UniformSpace.comap (Function.eval i) (U i)
<VAR>ι : Type u_1<VAR>α : ι → Type u<VAR>U : (i : ι) → UniformSpace (α i)<GOAL>𝓤 ((i : ι) → α i) = ⨅ i, Filter.comap (fun a => (a.1 i, a.2 i)) (𝓤 (α i))
<VAR>ι : Type u_1<VAR>α : ι → Type u<VAR>U : (i : ι) → UniformSpace (α i)<VAR>β : Type u_4<VAR>UniformSpace β<VAR>f : β → (i : ι) → α i<GOAL>UniformContinuous f ↔ ∀ (i : ι), UniformContinuous fun x => f x i
<VAR>ι : Type u_1<VAR>α : ι → Type u<VAR>U : (i : ι) → UniformSpace (α i)<VAR>i : ι<GOAL>UniformContinuous fun a => a i
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u<VAR>U : (i : ι) → UniformSpace (α i)<VAR>φ : ι' → ι<GOAL>UniformContinuous fun f j => f (φ j)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>β : Type u_3<VAR>UniformSpace β<VAR>φ : ι' → ι<GOAL>UniformContinuous fun x => x ∘ φ
<VAR>ι : Type u_1<VAR>α : ι → Type u<VAR>U : (i : ι) → UniformSpace (α i)<VAR>β : ι → Type u_4<VAR>(i : ι) → UniformSpace (β i)<VAR>g : (i : ι) → α i → β i<VAR>hg : ∀ (i : ι), UniformContinuous (g i)<GOAL>UniformContinuous fun f i => g i (f i)
<VAR>ι : Type u_1<VAR>β : Type u_3<VAR>UniformSpace β<VAR>α : Type u_4<VAR>UniformSpace α<VAR>g : α → β<VAR>hg : UniformContinuous g<GOAL>UniformContinuous fun x => g ∘ x
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u<VAR>U : (i : ι) → UniformSpace (α i)<VAR>φ : ι' → ι<GOAL>UniformSpace.comap (fun g i' => g (φ i')) (Pi.uniformSpace fun i' => α (φ i')) = ⨅ i', UniformSpace.comap (Function.eval (φ i')) (U (φ i'))
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>β : Type u_3<VAR>UniformSpace β<VAR>φ : ι' → ι<GOAL>UniformSpace.comap (fun x => x ∘ φ) (Pi.uniformSpace fun x => β) = ⨅ i', UniformSpace.comap (Function.eval (φ i')) inst✝
<VAR>ι : Type u_1<VAR>α : ι → Type u<VAR>U : (i : ι) → UniformSpace (α i)<VAR>S : Set ι<GOAL>UniformContinuous S.restrict
<VAR>ι : Type u_1<VAR>α : ι → Type u<VAR>U : (i : ι) → UniformSpace (α i)<VAR>S : Set ι<GOAL>UniformSpace.comap S.restrict (Pi.uniformSpace fun i => α ↑i) = ⨅ i ∈ S, UniformSpace.comap (Function.eval i) (U i)
<VAR>ι : Type u_1<VAR>α : ι → Type u<VAR>U : (i : ι) → UniformSpace (α i)<VAR>Nonempty ι<VAR>l : Filter ((i : ι) → α i)<GOAL>Cauchy l ↔ ∀ (i : ι), Cauchy (Filter.map (Function.eval i) l)
<VAR>ι : Type u_1<VAR>α : ι → Type u<VAR>U : (i : ι) → UniformSpace (α i)<VAR>l : Filter ((i : ι) → α i)<VAR>l.NeBot<GOAL>Cauchy l ↔ ∀ (i : ι), Cauchy (Filter.map (Function.eval i) l)
<VAR>ι : Type u_1<VAR>α : ι → Type u<VAR>U : (i : ι) → UniformSpace (α i)<VAR>Nonempty ι<VAR>l : (i : ι) → Filter (α i)<VAR>hl : ∀ (i : ι), Cauchy (l i)<GOAL>Cauchy (Filter.pi l)
<VAR>ι : Type u_1<VAR>α : ι → Type u<VAR>U : (i : ι) → UniformSpace (α i)<VAR>𝔖 : Set (Set ι)<GOAL>UniformSpace.comap (⋃₀ 𝔖).restrict (Pi.uniformSpace fun i => α ↑i) = ⨅ S ∈ 𝔖, UniformSpace.comap S.restrict (Pi.uniformSpace fun i => α ↑i)
<VAR>ι : Type u_4<VAR>X : Type u_5<VAR>u : ι → UniformSpace X<VAR>hu : ∀ (i : ι), CompleteSpace X<VAR>ht : ∃ t, T2Space X ∧ ∀ (i : ι), UniformSpace.toTopologicalSpace ≤ t<GOAL>CompleteSpace X
<VAR>B : Type u_1<VAR>F : Type u_2<VAR>TopologicalSpace B<VAR>TopologicalSpace F<GOAL>Inducing ⇑(Bundle.TotalSpace.toProd B F)
<VAR>B : Type u_1<VAR>F : Type u_2<VAR>TopologicalSpace B<VAR>TopologicalSpace F<GOAL>(Bundle.Trivial.trivialization B F).source = Set.univ
<VAR>B : Type u_1<VAR>F : Type u_2<VAR>TopologicalSpace B<VAR>TopologicalSpace F<GOAL>(Bundle.Trivial.trivialization B F).target = Set.univ
<VAR>B : Type u_1<VAR>F : Type u_2<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>i : MemTrivializationAtlas e<GOAL>e = Bundle.Trivial.trivialization B F
<VAR>B : Type u_1<VAR>F₁ : Type u_2<VAR>E₁ : B → Type u_3<VAR>F₂ : Type u_4<VAR>E₂ : B → Type u_5<VAR>TopologicalSpace (Bundle.TotalSpace F₁ E₁)<VAR>TopologicalSpace (Bundle.TotalSpace F₂ E₂)<GOAL>Inducing fun p => ({ proj := p.proj, snd := p.snd.1 }, { proj := p.proj, snd := p.snd.2 })
<VAR>B : Type u_1<VAR>TopologicalSpace B<VAR>F₁ : Type u_2<VAR>TopologicalSpace F₁<VAR>E₁ : B → Type u_3<VAR>TopologicalSpace (Bundle.TotalSpace F₁ E₁)<VAR>F₂ : Type u_4<VAR>TopologicalSpace F₂<VAR>E₂ : B → Type u_5<VAR>TopologicalSpace (Bundle.TotalSpace F₂ E₂)<VAR>e₁ : Trivialization F₁ Bundle.TotalSpace.proj<VAR>e₂ : Trivialization F₂ Bundle.TotalSpace.proj<GOAL>ContinuousOn (Trivialization.Prod.toFun' e₁ e₂) (Bundle.TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet))
<VAR>B : Type u_1<VAR>TopologicalSpace B<VAR>F₁ : Type u_2<VAR>TopologicalSpace F₁<VAR>E₁ : B → Type u_3<VAR>TopologicalSpace (Bundle.TotalSpace F₁ E₁)<VAR>F₂ : Type u_4<VAR>TopologicalSpace F₂<VAR>E₂ : B → Type u_5<VAR>TopologicalSpace (Bundle.TotalSpace F₂ E₂)<VAR>e₁ : Trivialization F₁ Bundle.TotalSpace.proj<VAR>e₂ : Trivialization F₂ Bundle.TotalSpace.proj<VAR>(x : B) → Zero (E₁ x)<VAR>(x : B) → Zero (E₂ x)<VAR>x : Bundle.TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x<VAR>h : x ∈ Bundle.TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet)<GOAL>Trivialization.Prod.invFun' e₁ e₂ (Trivialization.Prod.toFun' e₁ e₂ x) = x
<VAR>B : Type u_1<VAR>TopologicalSpace B<VAR>F₁ : Type u_2<VAR>TopologicalSpace F₁<VAR>E₁ : B → Type u_3<VAR>TopologicalSpace (Bundle.TotalSpace F₁ E₁)<VAR>F₂ : Type u_4<VAR>TopologicalSpace F₂<VAR>E₂ : B → Type u_5<VAR>TopologicalSpace (Bundle.TotalSpace F₂ E₂)<VAR>e₁ : Trivialization F₁ Bundle.TotalSpace.proj<VAR>e₂ : Trivialization F₂ Bundle.TotalSpace.proj<VAR>(x : B) → Zero (E₁ x)<VAR>(x : B) → Zero (E₂ x)<VAR>x : B × F₁ × F₂<VAR>h : x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ Set.univ<GOAL>Trivialization.Prod.toFun' e₁ e₂ (Trivialization.Prod.invFun' e₁ e₂ x) = x
<VAR>B : Type u_1<VAR>TopologicalSpace B<VAR>F₁ : Type u_2<VAR>TopologicalSpace F₁<VAR>E₁ : B → Type u_3<VAR>TopologicalSpace (Bundle.TotalSpace F₁ E₁)<VAR>F₂ : Type u_4<VAR>TopologicalSpace F₂<VAR>E₂ : B → Type u_5<VAR>TopologicalSpace (Bundle.TotalSpace F₂ E₂)<VAR>e₁ : Trivialization F₁ Bundle.TotalSpace.proj<VAR>e₂ : Trivialization F₂ Bundle.TotalSpace.proj<VAR>(x : B) → Zero (E₁ x)<VAR>(x : B) → Zero (E₂ x)<GOAL>ContinuousOn (Trivialization.Prod.invFun' e₁ e₂) ((e₁.baseSet ∩ e₂.baseSet) ×ˢ Set.univ)
<VAR>B : Type u_1<VAR>TopologicalSpace B<VAR>F₁ : Type u_2<VAR>TopologicalSpace F₁<VAR>E₁ : B → Type u_3<VAR>TopologicalSpace (Bundle.TotalSpace F₁ E₁)<VAR>F₂ : Type u_4<VAR>TopologicalSpace F₂<VAR>E₂ : B → Type u_5<VAR>TopologicalSpace (Bundle.TotalSpace F₂ E₂)<VAR>e₁ : Trivialization F₁ Bundle.TotalSpace.proj<VAR>e₂ : Trivialization F₂ Bundle.TotalSpace.proj<VAR>(x : B) → Zero (E₁ x)<VAR>(x : B) → Zero (E₂ x)<GOAL>(e₁.prod e₂).baseSet = e₁.baseSet ∩ e₂.baseSet
<VAR>B : Type u_1<VAR>TopologicalSpace B<VAR>F₁ : Type u_2<VAR>TopologicalSpace F₁<VAR>E₁ : B → Type u_3<VAR>TopologicalSpace (Bundle.TotalSpace F₁ E₁)<VAR>F₂ : Type u_4<VAR>TopologicalSpace F₂<VAR>E₂ : B → Type u_5<VAR>TopologicalSpace (Bundle.TotalSpace F₂ E₂)<VAR>e₁ : Trivialization F₁ Bundle.TotalSpace.proj<VAR>e₂ : Trivialization F₂ Bundle.TotalSpace.proj<VAR>(x : B) → Zero (E₁ x)<VAR>(x : B) → Zero (E₂ x)<VAR>x : B<VAR>w₁ : F₁<VAR>w₂ : F₂<GOAL>↑(e₁.prod e₂).symm (x, w₁, w₂) = { proj := x, snd := (e₁.symm x w₁, e₂.symm x w₂) }
<VAR>B : Type u_1<VAR>F : Type u_2<VAR>E : B → Type u_3<VAR>B' : Type u_4<VAR>f : B' → B<VAR>TopologicalSpace B'<VAR>TopologicalSpace (Bundle.TotalSpace F E)<GOAL>pullbackTopology F E f = TopologicalSpace.induced Bundle.TotalSpace.proj inst✝ ⊓ TopologicalSpace.induced (Bundle.Pullback.lift f) inst✝¹
<VAR>B : Type u<VAR>F : Type v<VAR>E : B → Type w₁<VAR>B' : Type w₂<VAR>TopologicalSpace B'<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>f : B' → B<GOAL>Continuous Bundle.TotalSpace.proj
<VAR>B : Type u<VAR>F : Type v<VAR>E : B → Type w₁<VAR>B' : Type w₂<VAR>TopologicalSpace B'<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>f : B' → B<GOAL>Continuous (Bundle.Pullback.lift f)
<VAR>B : Type u<VAR>F : Type v<VAR>E : B → Type w₁<VAR>B' : Type w₂<VAR>TopologicalSpace B'<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>f : B' → B<GOAL>Inducing (Bundle.pullbackTotalSpaceEmbedding f)