mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : UniformSpace ι
𝔖 : Set (Set X)
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
φ : (↑(⋃₀ 𝔖) → α) ≃ᵤ (X → α) := UniformEquiv.piCongrLeft (Equiv.subtypeUnivEquiv 𝔖_covers)
⊢ IsUniformInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ IsUniformInducing F

Tactic:
rw [EquicontinuousOn.isUniformInducing_uniformOnFun_iff_pi' 𝔖_compact F_eqcont,
      show domRestrict (⋃₀ 𝔖) ∘ F = φ.symm ∘ F by rfl]

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : UniformSpace ι
𝔖 : Set (Set X)
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
φ : (↑(⋃₀ 𝔖) → α) ≃ᵤ (X → α) := UniformEquiv.piCongrLeft (Equiv.subtypeUnivEquiv 𝔖_covers)
⊢ IsUniformInducing (⇑φ.symm ∘ F) ↔ IsUniformInducing F
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : TopologicalSpace ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ inst✝ = TopologicalSpace.induced (⇑(UniformOnFun.ofFun 𝔖) ∘ F) (UniformOnFun.topologicalSpace X α 𝔖) ↔
    inst✝ = TopologicalSpace.induced ((⋃₀ 𝔖).domRestrict ∘ F) Pi.topologicalSpace

Tactic:
]

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : TopologicalSpace ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ inst✝ = TopologicalSpace.induced (⇑(UniformOnFun.ofFun 𝔖) ∘ F) (UniformOnFun.topologicalSpace X α 𝔖) ↔
    inst✝ = TopologicalSpace.induced ((⋃₀ 𝔖).domRestrict ∘ F) Pi.topologicalSpace
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case h₀
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
hperm : map Sigma.fst (List.toFinmap' (xs₀.zip xs₁)) ~ map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))
hnodup : (map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))).Nodup
⊢ (map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))).Nodup

Tactic:
]

Goal state after:
case h₀
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
hperm : map Sigma.fst (List.toFinmap' (xs₀.zip xs₁)) ~ map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))
hnodup : (map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))).Nodup
⊢ (map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))).Nodup
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : GrpCat
⊢ (∀ (a : ↑G), (ConcreteCategory.hom (eta G)) a = 1 → a = 1) ↔
    ∀ (g : ↑G), (∀ (H : FiniteIndexNormalSubgroup ↑G), g ∈ H) → g = 1

Tactic:
]

Goal state after:
G : GrpCat
⊢ (∀ (a : ↑G), (ConcreteCategory.hom (eta G)) a = 1 → a = 1) ↔
    ∀ (g : ↑G), (∀ (H : FiniteIndexNormalSubgroup ↑G), g ∈ H) → g = 1
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : TopologicalSpace ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ inst✝ = (UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖)).toTopologicalSpace ↔
    inst✝ = (UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖)).toTopologicalSpace

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : GrpCat
g : ↑G
⊢ (∀ (x : FiniteIndexNormalSubgroup ↑G), ↑((ConcreteCategory.hom (eta G)) g) x = ↑1 x) ↔
    ∀ (H : FiniteIndexNormalSubgroup ↑G), g ∈ H

Tactic:
]

Goal state after:
G : GrpCat
g : ↑G
⊢ (∀ (x : FiniteIndexNormalSubgroup ↑G), ↑((ConcreteCategory.hom (eta G)) g) x = ↑1 x) ↔
    ∀ (H : FiniteIndexNormalSubgroup ↑G), g ∈ H
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : TopologicalSpace ι
𝔖 : Set (Set X)
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ IsInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ IsInducing F

Tactic:
]

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : TopologicalSpace ι
𝔖 : Set (Set X)
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ IsInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ IsInducing F
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : GrpCat
U : Set ↑(completion G).toProfinite.toTop
s : Set ((j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc : (j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux (diagram G)
uDefaultSpec : ↑⟨spc, hspc⟩ ∈ s
⊢ (U ∩ Set.range (etaFn G)).Nonempty

Tactic:
]

Goal state after:
G : GrpCat
U : Set ↑(completion G).toProfinite.toTop
s : Set ((j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc : (j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux (diagram G)
uDefaultSpec : ↑⟨spc, hspc⟩ ∈ s
⊢ (U ∩ Set.range (etaFn G)).Nonempty
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case h₁
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
hperm : xs₀ ~ xs₁
hnodup : (map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))).Nodup
⊢ xs₀ ~ xs₁

Tactic:
]

Goal state after:
case h₁
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
hperm : xs₀ ~ xs₁
hnodup : (map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))).Nodup
⊢ xs₀ ~ xs₁
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : TopologicalSpace ι
𝔖 : Set (Set X)
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
φ : (↑(⋃₀ 𝔖) → α) ≃ₜ (X → α) := Homeomorph.piCongrLeft (Equiv.subtypeUnivEquiv 𝔖_covers)
⊢ IsInducing (⇑φ.symm ∘ F) ↔ IsInducing F

Tactic:
]

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : TopologicalSpace ι
𝔖 : Set (Set X)
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
φ : (↑(⋃₀ 𝔖) → α) ≃ₜ (X → α) := Homeomorph.piCongrLeft (Equiv.subtypeUnivEquiv 𝔖_covers)
⊢ IsInducing (⇑φ.symm ∘ F) ↔ IsInducing F
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
⊢ Tendsto (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ (𝓝 ((UniformOnFun.ofFun 𝔖) f)) ↔ Tendsto F ℱ (𝓝 f)

Tactic:
]

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
⊢ Tendsto (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ (𝓝 ((UniformOnFun.ofFun 𝔖) f)) ↔ Tendsto F ℱ (𝓝 f)
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: case h
G : GrpCat
U : Set ↑(completion G).toProfinite.toTop
s : Set ((j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc : (j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux (diagram G)
uDefaultSpec : ↑⟨spc, hspc⟩ ∈ s
J : Finset (FiniteIndexNormalSubgroup ↑G)
fJ : (a : FiniteIndexNormalSubgroup ↑G) → Set ↑((diagram G).obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ ↑⟨spc, hspc⟩ a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑G := ⨅ j, (↑j).toSubgroup
hM : M.Normal
hMFinite : M.FiniteIndex
m : FiniteIndexNormalSubgroup ↑G := { toSubgroup := M, isNormal' := ⋯, isFiniteIndex' := ⋯ }
origin : ↑G
horigin : (QuotientGroup.mk' M) origin = spc m
⊢ etaFn G origin ∈ Subtype.val ⁻¹' s

Tactic:
]

Goal state after:
case h
G : GrpCat
U : Set ↑(completion G).toProfinite.toTop
s : Set ((j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc : (j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux (diagram G)
uDefaultSpec : ↑⟨spc, hspc⟩ ∈ s
J : Finset (FiniteIndexNormalSubgroup ↑G)
fJ : (a : FiniteIndexNormalSubgroup ↑G) → Set ↑((diagram G).obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ ↑⟨spc, hspc⟩ a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑G := ⨅ j, (↑j).toSubgroup
hM : M.Normal
hMFinite : M.FiniteIndex
m : FiniteIndexNormalSubgroup ↑G := { toSubgroup := M, isNormal' := ⋯, isFiniteIndex' := ⋯ }
origin : ↑G
horigin : (QuotientGroup.mk' M) origin = spc m
⊢ etaFn G origin ∈ Subtype.val ⁻¹' s
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
K : Set X
hK : K ∈ 𝔖
this : CompactSpace ↑K
⊢ Tendsto ((⇑UniformFun.ofFun ∘ K.domRestrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ∘ ⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ
      (𝓝 ((⇑UniformFun.ofFun ∘ K.domRestrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ((UniformOnFun.ofFun 𝔖) f))) ↔
    Tendsto (⇑UniformFun.ofFun ∘ K.domRestrict ∘ F) ℱ (𝓝 (UniformFun.ofFun (K.domRestrict f)))

Tactic:
]

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
K : Set X
hK : K ∈ 𝔖
this : CompactSpace ↑K
⊢ Tendsto ((⇑UniformFun.ofFun ∘ K.domRestrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ∘ ⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ
      (𝓝 ((⇑UniformFun.ofFun ∘ K.domRestrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ((UniformOnFun.ofFun 𝔖) f))) ↔
    Tendsto (⇑UniformFun.ofFun ∘ K.domRestrict ∘ F) ℱ (𝓝 (UniformFun.ofFun (K.domRestrict f)))
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
⊢ Tendsto (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ (𝓝 ((UniformOnFun.ofFun 𝔖) f)) ↔ Tendsto F ℱ (𝓝 f)

Tactic:
]

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
⊢ Tendsto (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ (𝓝 ((UniformOnFun.ofFun 𝔖) f)) ↔ Tendsto F ℱ (𝓝 f)
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: case h
G : GrpCat
U : Set ↑(completion G).toProfinite.toTop
s : Set ((j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc : (j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux (diagram G)
uDefaultSpec : ↑⟨spc, hspc⟩ ∈ s
J : Finset (FiniteIndexNormalSubgroup ↑G)
fJ : (a : FiniteIndexNormalSubgroup ↑G) → Set ↑((diagram G).obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ ↑⟨spc, hspc⟩ a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑G := ⨅ j, (↑j).toSubgroup
hM : M.Normal
hMFinite : M.FiniteIndex
m : FiniteIndexNormalSubgroup ↑G := { toSubgroup := M, isNormal' := ⋯, isFiniteIndex' := ⋯ }
origin : ↑G
horigin : (QuotientGroup.mk' M) origin = spc m
⊢ etaFn G origin ∈ Subtype.val ⁻¹' s

Tactic:
apply hJ2

Goal state after:
case h
G : GrpCat
U : Set ↑(completion G).toProfinite.toTop
s : Set ((j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc : (j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux (diagram G)
uDefaultSpec : ↑⟨spc, hspc⟩ ∈ s
J : Finset (FiniteIndexNormalSubgroup ↑G)
fJ : (a : FiniteIndexNormalSubgroup ↑G) → Set ↑((diagram G).obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ ↑⟨spc, hspc⟩ a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑G := ⋯
hM : M.Normal
hMFinite : M.FiniteIndex
m : FiniteIndexNormalSubgroup ↑G := ⋯
origin : ↑G
horigin : (QuotientGroup.mk' M) origin = spc m
⊢ ↑(etaFn G origin) ∈ (↑J).pi fJ
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
φ : (↑(⋃₀ 𝔖) → α) ≃ₜ (X → α) := Homeomorph.piCongrLeft (Equiv.subtypeUnivEquiv 𝔖_covers)
⊢ Tendsto (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ (𝓝 ((UniformOnFun.ofFun 𝔖) f)) ↔ Tendsto F ℱ (𝓝 f)

Tactic:
EquicontinuousOn.tendsto_uniformOnFun_iff_pi' 𝔖_compact F_eqcont,

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
φ : (↑(⋃₀ 𝔖) → α) ≃ₜ (X → α) := Homeomorph.piCongrLeft (Equiv.subtypeUnivEquiv 𝔖_covers)
⊢ Tendsto ((⋃₀ 𝔖).domRestrict ∘ F) ℱ (𝓝 ((⋃₀ 𝔖).domRestrict f)) ↔ Tendsto F ℱ (𝓝 f)
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
φ : (↑(⋃₀ 𝔖) → α) ≃ₜ (X → α) := Homeomorph.piCongrLeft (Equiv.subtypeUnivEquiv 𝔖_covers)
⊢ Tendsto (⇑φ.symm ∘ F) ℱ (𝓝 (φ.symm f)) ↔ Tendsto (⇑φ.symm ∘ F) ℱ (𝓝 (φ.symm f))

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: case h
G : GrpCat
U : Set ↑(completion G).toProfinite.toTop
s : Set ((j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc : (j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux (diagram G)
uDefaultSpec : ↑⟨spc, hspc⟩ ∈ s
J : Finset (FiniteIndexNormalSubgroup ↑G)
fJ : (a : FiniteIndexNormalSubgroup ↑G) → Set ↑((diagram G).obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ ↑⟨spc, hspc⟩ a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑G := ⨅ j, (↑j).toSubgroup
hM : M.Normal
hMFinite : M.FiniteIndex
m : FiniteIndexNormalSubgroup ↑G := { toSubgroup := M, isNormal' := ⋯, isFiniteIndex' := ⋯ }
origin : ↑G
horigin : (QuotientGroup.mk' M) origin = spc m
a : FiniteIndexNormalSubgroup ↑G
a_in_J : a ∈ ↑J
M_to_Na : m ⟶ a := ⋯.hom
⊢ (Hom.hom ((diagram G).map M_to_Na)) (↑(etaFn G origin) m) ∈ fJ a

Tactic:
]

Goal state after:
case h
G : GrpCat
U : Set ↑(completion G).toProfinite.toTop
s : Set ((j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc : (j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux (diagram G)
uDefaultSpec : ↑⟨spc, hspc⟩ ∈ s
J : Finset (FiniteIndexNormalSubgroup ↑G)
fJ : (a : FiniteIndexNormalSubgroup ↑G) → Set ↑((diagram G).obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ ↑⟨spc, hspc⟩ a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑G := ⨅ j, (↑j).toSubgroup
hM : M.Normal
hMFinite : M.FiniteIndex
m : FiniteIndexNormalSubgroup ↑G := { toSubgroup := M, isNormal' := ⋯, isFiniteIndex' := ⋯ }
origin : ↑G
horigin : (QuotientGroup.mk' M) origin = spc m
a : FiniteIndexNormalSubgroup ↑G
a_in_J : a ∈ ↑J
M_to_Na : m ⟶ a := ⋯.hom
⊢ (Hom.hom ((diagram G).map M_to_Na)) (↑(etaFn G origin) m) ∈ fJ a
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: case h
G : GrpCat
U : Set ↑(completion G).toProfinite.toTop
s : Set ((j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc : (j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux (diagram G)
uDefaultSpec : ↑⟨spc, hspc⟩ ∈ s
J : Finset (FiniteIndexNormalSubgroup ↑G)
fJ : (a : FiniteIndexNormalSubgroup ↑G) → Set ↑((diagram G).obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ ↑⟨spc, hspc⟩ a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑G := ⨅ j, (↑j).toSubgroup
hM : M.Normal
hMFinite : M.FiniteIndex
m : FiniteIndexNormalSubgroup ↑G := { toSubgroup := M, isNormal' := ⋯, isFiniteIndex' := ⋯ }
origin : ↑G
horigin : ↑origin = spc m
a : FiniteIndexNormalSubgroup ↑G
a_in_J : a ∈ ↑J
M_to_Na : m ⟶ a := ⋯.hom
⊢ (Hom.hom ((diagram G).map M_to_Na)) (spc m) ∈ fJ a

Tactic:
]

Goal state after:
case h
G : GrpCat
U : Set ↑(completion G).toProfinite.toTop
s : Set ((j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc : (j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux (diagram G)
uDefaultSpec : ↑⟨spc, hspc⟩ ∈ s
J : Finset (FiniteIndexNormalSubgroup ↑G)
fJ : (a : FiniteIndexNormalSubgroup ↑G) → Set ↑((diagram G).obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ ↑⟨spc, hspc⟩ a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑G := ⨅ j, (↑j).toSubgroup
hM : M.Normal
hMFinite : M.FiniteIndex
m : FiniteIndexNormalSubgroup ↑G := { toSubgroup := M, isNormal' := ⋯, isFiniteIndex' := ⋯ }
origin : ↑G
horigin : ↑origin = spc m
a : FiniteIndexNormalSubgroup ↑G
a_in_J : a ∈ ↑J
M_to_Na : m ⟶ a := ⋯.hom
⊢ (Hom.hom ((diagram G).map M_to_Na)) (spc m) ∈ fJ a
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : TopologicalSpace ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_ind : IsInducing ((⋃₀ 𝔖).domRestrict ∘ F)
F_cl : IsClosed[UniformOnFun.topologicalSpace X α 𝔖] (range (⇑(UniformOnFun.ofFun 𝔖) ∘ F))
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
F_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ (i : ι), F i x ∈ Q
⊢ IsInducing ((⋃₀ 𝔖).domRestrict ∘ F)

Tactic:
]

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : TopologicalSpace ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_ind : IsInducing ((⋃₀ 𝔖).domRestrict ∘ F)
F_cl : IsClosed[UniformOnFun.topologicalSpace X α 𝔖] (range (⇑(UniformOnFun.ofFun 𝔖) ∘ F))
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
F_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ (i : ι), F i x ∈ Q
⊢ IsInducing ((⋃₀ 𝔖).domRestrict ∘ F)
Module: Mathlib.Topology.Algebra.Group.OpenMapping

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
U : Set G
hU : U ∈ 𝓝 1
x : X
V : Set G
V_mem : V ∈ 𝓝 1
V_closed : IsClosed[inst✝⁹] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : ⋃ g ∈ s, g • V = univ
K : ℕ → Set G := compactCovering G
F : ℕ × ↑s → Set X := fun p ↦ (K p.1 ∩ ↑p.2 • V) • {x}
n : ℕ
g : G
hg : g ∈ s
hi : (interior (F (n, ⟨g, hg⟩))).Nonempty
I : (g • interior (V • {x})).Nonempty
⊢ (interior (V • {x})).Nonempty

Tactic:
]

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
U : Set G
hU : U ∈ 𝓝 1
x : X
V : Set G
V_mem : V ∈ 𝓝 1
V_closed : IsClosed[inst✝⁹] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : ⋃ g ∈ s, g • V = univ
K : ℕ → Set G := compactCovering G
F : ℕ × ↑s → Set X := fun p ↦ (K p.1 ∩ ↑p.2 • V) • {x}
n : ℕ
g : G
hg : g ∈ s
hi : (interior (F (n, ⟨g, hg⟩))).Nonempty
I : (g • interior (V • {x})).Nonempty
⊢ (interior (V • {x})).Nonempty
Module: Mathlib.Topology.Algebra.Group.CompactOpen

Goal state before:
pp: X : Type u_7
Y : Type u_8
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group X
inst✝⁶ : IsTopologicalGroup X
inst✝⁵ : UniformSpace Y
inst✝⁴ : CommGroup Y
inst✝³ : IsUniformGroup Y
inst✝² : T0Space Y
inst✝¹ : CompactSpace Y
inst✝ : LocallyCompactSpace X
V : ℕ → Set Y
hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)
hVo : (𝓝 1).HasBasis (fun x ↦ True) V
U0 : Set X
hU0c : IsCompact U0
hU0o : U0 ∈ 𝓝 1
U_aux : ℕ → ↑{S | S ∈ 𝓝 1} :=
  fun t ↦
    Nat.rec ⟨U0, hU0o⟩
      (fun x S ↦
        let h := ⋯;
        ⟨Classical.choose h, ⋯⟩)
      t
U : ℕ → Set X := fun n ↦ ↑(U_aux n)
hU1 : ∀ (n : ℕ), U n ∈ 𝓝 1
hU2 : ∀ (n : ℕ), U (n + 1) * U (n + 1) ⊆ U n
hU3 : ∀ (n : ℕ), U (n + 1) ⊆ U n
hU4 : ∀ (f : X →* Y), Set.MapsTo (⇑f) (U 0) (V 0) → ∀ (n : ℕ), Set.MapsTo (⇑f) (U n) (V n)
⊢ ∀ (k : ℕ), True → ∀ᶠ (x : X) in 𝓝 1, ∀ (i : ↑{f | Set.MapsTo (⇑f) (U 0) (V 0)}), (↑i 1, ↑i x) ∈ {x | x.2 / x.1 ∈ V k}

Tactic:
]

Goal state after:
X : Type u_7
Y : Type u_8
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group X
inst✝⁶ : IsTopologicalGroup X
inst✝⁵ : UniformSpace Y
inst✝⁴ : CommGroup Y
inst✝³ : IsUniformGroup Y
inst✝² : T0Space Y
inst✝¹ : CompactSpace Y
inst✝ : LocallyCompactSpace X
V : ℕ → Set Y
hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)
hVo : (𝓝 1).HasBasis (fun x ↦ True) V
U0 : Set X
hU0c : IsCompact U0
hU0o : U0 ∈ 𝓝 1
U_aux : ℕ → ↑{S | S ∈ 𝓝 1} :=
  fun t ↦
    Nat.rec ⟨U0, hU0o⟩
      (fun x S ↦
        let h := ⋯;
        ⟨Classical.choose h, ⋯⟩)
      t
U : ℕ → Set X := fun n ↦ ↑(U_aux n)
hU1 : ∀ (n : ℕ), U n ∈ 𝓝 1
hU2 : ∀ (n : ℕ), U (n + 1) * U (n + 1) ⊆ U n
hU3 : ∀ (n : ℕ), U (n + 1) ⊆ U n
hU4 : ∀ (f : X →* Y), Set.MapsTo (⇑f) (U 0) (V 0) → ∀ (n : ℕ), Set.MapsTo (⇑f) (U n) (V n)
⊢ ∀ (k : ℕ), True → ∀ᶠ (x : X) in 𝓝 1, ∀ (i : ↑{f | Set.MapsTo (⇑f) (U 0) (V 0)}), (↑i 1, ↑i x) ∈ {x | x.2 / x.1 ∈ V k}
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : TopologicalSpace ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_ind : IsInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F)
F_cl : IsClosed[UniformOnFun.topologicalSpace X α 𝔖] (range (⇑(UniformOnFun.ofFun 𝔖) ∘ F))
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
F_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ (i : ι), F i x ∈ Q
this : IsInducing ((⋃₀ 𝔖).domRestrict ∘ F)
⊢ IsCompact (range ((⋃₀ 𝔖).domRestrict ∘ F))

Tactic:
]

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : TopologicalSpace ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_ind : IsInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F)
F_cl : IsClosed[UniformOnFun.topologicalSpace X α 𝔖] (range (⇑(UniformOnFun.ofFun 𝔖) ∘ F))
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
F_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ (i : ι), F i x ∈ Q
this : IsInducing ((⋃₀ 𝔖).domRestrict ∘ F)
⊢ IsCompact (range ((⋃₀ 𝔖).domRestrict ∘ F))