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✝ : 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 : ∀ x ∈ ⋃₀ 𝔖, ∃ 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 : ∀ x ∈ ⋃₀ 𝔖, ∃ Q, IsCompact Q ∧ ∀ (i : ι), F i x ∈ Q
this : IsInducing ((⋃₀ 𝔖).domRestrict ∘ F)
⊢ IsCompact (range ((⋃₀ 𝔖).domRestrict ∘ F))
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)
n : ℕ
x✝¹ : True
x : X
hx : x ∈ U n
x✝ : ↑{f | Set.MapsTo (⇑f) (U 0) (V 0)}
f : X →* Y
hf : f ∈ {f | Set.MapsTo (⇑f) (U 0) (V 0)}
⊢ (1, ↑⟨f, hf⟩ x).2 ∈ V n

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)
n : ℕ
x✝¹ : True
x : X
hx : x ∈ U n
x✝ : ↑{f | Set.MapsTo (⇑f) (U 0) (V 0)}
f : X →* Y
hf : f ∈ {f | Set.MapsTo (⇑f) (U 0) (V 0)}
⊢ (1, ↑⟨f, hf⟩ x).2 ∈ V n
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : GrpCat
P : ProfiniteGrp.{u}
f : G ⟶ GrpCat.of ↑P.toProfinite.toTop
X Y : OpenNormalSubgroup ↑P.toProfinite.toTop
g : X ⟶ Y
x :
  (j : FiniteIndexNormalSubgroup ↑G) →
    ↑((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j)
hx :
  x ∈
    {u |
      ∀ {i j : FiniteIndexNormalSubgroup ↑G} (f : i ⟶ j),
        (ConcreteCategory.hom
              ((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).map f))
            (u i) =
          u j}
this :
  (ConcreteCategory.hom
        ((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).map ⋯.hom))
      (x (preimage f X)) =
    x (preimage f Y)
t : ↑G
ht : ↑t = x (preimage f X)
⊢ (ConcreteCategory.hom (quotientMap f Y))
      ((ConcreteCategory.hom
          ((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).map ⋯.hom))
        ↑t) =
    (Hom.hom (P.diagram.map g)) ((ConcreteCategory.hom (quotientMap f X)) ↑t)

Tactic:
]

Goal state after:
G : GrpCat
P : ProfiniteGrp.{u}
f : G ⟶ GrpCat.of ↑P.toProfinite.toTop
X Y : OpenNormalSubgroup ↑P.toProfinite.toTop
g : X ⟶ Y
x :
  (j : FiniteIndexNormalSubgroup ↑G) →
    ↑((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j)
hx :
  x ∈
    {u |
      ∀ {i j : FiniteIndexNormalSubgroup ↑G} (f : i ⟶ j),
        (ConcreteCategory.hom
              ((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).map f))
            (u i) =
          u j}
this :
  (ConcreteCategory.hom
        ((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).map ⋯.hom))
      (x (preimage f X)) =
    x (preimage f Y)
t : ↑G
ht : ↑t = x (preimage f X)
⊢ (ConcreteCategory.hom (quotientMap f Y))
      ((ConcreteCategory.hom
          ((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).map ⋯.hom))
        ↑t) =
    (Hom.hom (P.diagram.map g)) ((ConcreteCategory.hom (quotientMap f X)) ↑t)
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 ι
inst✝ : T2Space α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_clemb : IsClosedEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ F)
s : Set ι
s_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn (F ∘ Subtype.val) K
s_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ i ∈ s, F i x ∈ Q
⊢ CompactSpace ↑(closure[inst✝¹] s)

Tactic:
]

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : UniformSpace α
F : ι → X → α
inst✝¹ : TopologicalSpace ι
inst✝ : T2Space α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_clemb : IsClosedEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ F)
s : Set ι
s_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn (F ∘ Subtype.val) K
s_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ i ∈ s, F i x ∈ Q
⊢ CompactSpace ↑(closure[inst✝¹] s)
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 : (interior ((g • V) • {x})).Nonempty
g' : G
hg' : g' ∈ V
hy : g' • x ∈ interior (V • {x})
⊢ g' • x ∈ interior (V • {x})

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 : (interior ((g • V) • {x})).Nonempty
g' : G
hg' : g' ∈ V
hy : g' • x ∈ interior (V • {x})
⊢ g' • x ∈ interior (V • {x})
Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x : G
m : ℤ
y : G
hy : MapClusterPt y atTop fun x_1 ↦ x ^ x_1
⊢ MapClusterPt (x ^ m) atTop fun x_1 ↦ x ^ x_1

Tactic:
]

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x : G
m : ℤ
y : G
hy : MapClusterPt y atTop fun x_1 ↦ x ^ x_1
⊢ MapClusterPt (x ^ m) atTop fun x_1 ↦ x ^ x_1
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 : (interior ((g • V) • {x})).Nonempty
g' : G
hg' : g' ∈ V
hy : g' • x ∈ interior (V • {x})
J : (g'⁻¹ • V) • {x} ∈ 𝓝 x
⊢ V • V ⊆ U

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 : (interior ((g • V) • {x})).Nonempty
g' : G
hg' : g' ∈ V
hy : g' • x ∈ interior (V • {x})
J : (g'⁻¹ • V) • {x} ∈ 𝓝 x
⊢ V • V ⊆ U
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : GrpCat
P : ProfiniteGrp.{u}
f : G ⟶ GrpCat.of ↑P.toProfinite.toTop
e : P ≅ limit P.diagram := P.isoLimittoFiniteQuotientFunctor
⊢ (eta G ≫ (forget₂ ProfiniteGrp.{u} GrpCat).map (lift f)) ≫ ((forget₂ ProfiniteGrp.{u} GrpCat).mapIso e).hom =
    f ≫ ((forget₂ ProfiniteGrp.{u} GrpCat).mapIso e).hom

Tactic:
]

Goal state after:
G : GrpCat
P : ProfiniteGrp.{u}
f : G ⟶ GrpCat.of ↑P.toProfinite.toTop
e : P ≅ limit P.diagram := P.isoLimittoFiniteQuotientFunctor
⊢ (eta G ≫ (forget₂ ProfiniteGrp.{u} GrpCat).map (lift f)) ≫ ((forget₂ ProfiniteGrp.{u} GrpCat).mapIso e).hom =
    f ≫ ((forget₂ ProfiniteGrp.{u} GrpCat).mapIso e).hom
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : CompactSpace ↑(ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x ↦ ⇑↑x
h : IsInducing ⇑(Equiv.Set.image DFunLike.coe S ⋯)
⊢ CompactSpace ↑S

Tactic:
]

Goal state after:
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : CompactSpace ↑(ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x ↦ ⇑↑x
h : IsInducing ⇑(Equiv.Set.image DFunLike.coe S ⋯)
⊢ CompactSpace ↑S
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : GrpCat
P : ProfiniteGrp.{u}
f : G ⟶ GrpCat.of ↑P.toProfinite.toTop
e : P ≅ limit P.diagram := P.isoLimittoFiniteQuotientFunctor
⊢ eta G ≫ (forget₂ ProfiniteGrp.{u} GrpCat).map (lift f ≫ e.hom) = f ≫ (forget₂ ProfiniteGrp.{u} GrpCat).map e.hom

Tactic:
]

Goal state after:
G : GrpCat
P : ProfiniteGrp.{u}
f : G ⟶ GrpCat.of ↑P.toProfinite.toTop
e : P ≅ limit P.diagram := P.isoLimittoFiniteQuotientFunctor
⊢ eta G ≫ (forget₂ ProfiniteGrp.{u} GrpCat).map (lift f ≫ e.hom) = f ≫ (forget₂ ProfiniteGrp.{u} GrpCat).map e.hom
Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x y : G
tfae_2_iff_1 : (MapClusterPt x atTop fun x ↦ y ^ x) ↔ MapClusterPt x atTop fun x ↦ y ^ x
tfae_3_to_4 : x ∈ closure[inst✝²] (range fun x ↦ y ^ x) → x ∈ closure[inst✝²] (range fun x ↦ y ^ x)
tfae_4_to_1 : x ∈ closure[inst✝²] (range fun x ↦ y ^ x) → MapClusterPt x atTop fun x ↦ y ^ x
⊢ (MapClusterPt x atTop fun x ↦ y ^ x) → ClusterPt x (𝓟 (range fun x ↦ y ^ x))

Tactic:
]

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x y : G
tfae_2_iff_1 : (MapClusterPt x atTop fun x ↦ y ^ x) ↔ MapClusterPt x atTop fun x ↦ y ^ x
tfae_3_to_4 : x ∈ closure[inst✝²] (range fun x ↦ y ^ x) → x ∈ closure[inst✝²] (range fun x ↦ y ^ x)
tfae_4_to_1 : x ∈ closure[inst✝²] (range fun x ↦ y ^ x) → MapClusterPt x atTop fun x ↦ y ^ x
⊢ (MapClusterPt x atTop fun x ↦ y ^ x) → ClusterPt x (𝓟 (range fun x ↦ y ^ x))
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x ↦ ⇑↑x
⊢ IsInducing (⇑(UniformOnFun.ofFun ?m.83) ∘ Subtype.val ∘ ⇑(Equiv.Set.image DFunLike.coe S ⋯))

pp: case 𝔖_covers
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x ↦ ⇑↑x
⊢ ⋃₀ ?m.83 = univ

pp: case 𝔖_compact
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x ↦ ⇑↑x
⊢ ∀ K ∈ ?m.83, IsCompact K

pp: case F_eqcont
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x ↦ ⇑↑x
⊢ ∀ K ∈ ?m.83, EquicontinuousOn (Subtype.val ∘ ⇑(Equiv.Set.image DFunLike.coe S ⋯)) K

pp: X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x ↦ ⇑↑x
⊢ Set (Set X)

Tactic:
]

Goal state after:
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x ↦ ⇑↑x
⊢ IsInducing (⇑(UniformOnFun.ofFun ?m.83) ∘ Subtype.val ∘ ⇑(Equiv.Set.image DFunLike.coe S ⋯))

case 𝔖_covers
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x ↦ ⇑↑x
⊢ ⋃₀ ?m.83 = univ

case 𝔖_compact
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x ↦ ⇑↑x
⊢ ∀ K ∈ ?m.83, IsCompact K

case F_eqcont
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x ↦ ⇑↑x
⊢ ∀ K ∈ ?m.83, EquicontinuousOn (Subtype.val ∘ ⇑(Equiv.Set.image DFunLike.coe S ⋯)) K

X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x ↦ ⇑↑x
⊢ Set (Set X)
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
x : X
g : G
U : Set G
hU : U ∈ 𝓝 g
this : (fun x_1 ↦ x_1 • x) = (fun x_1 ↦ x_1 • g • x) ∘ fun x ↦ x * g⁻¹
⊢ (fun x ↦ x * g⁻¹) '' U • {g • x} ∈ 𝓝 (g • x)

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
x : X
g : G
U : Set G
hU : U ∈ 𝓝 g
this : (fun x_1 ↦ x_1 • x) = (fun x_1 ↦ x_1 • g • x) ∘ fun x ↦ x * g⁻¹
⊢ (fun x ↦ x * g⁻¹) '' U • {g • x} ∈ 𝓝 (g • x)
Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
s : Set G
⊢ s ∪ s⁻¹ ⊆ ↑(Submonoid.closure s).topologicalClosure

Tactic:
]

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
s : Set G
⊢ s ∪ s⁻¹ ⊆ ↑(Submonoid.closure s).topologicalClosure
Module: Mathlib.Topology.Algebra.Group.OpenMapping

Goal state before:
pp: G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SigmaCompactSpace G
H : Type u_3
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : BaireSpace H
inst✝¹ : T2Space H
inst✝ : ContinuousMul H
f : G →* H
hf : Surjective ⇑f
h'f : Continuous[inst✝⁸, inst✝³] ⇑f
A : MulAction G H := MulAction.compHom H f
this✝¹ : ContinuousSMul G H
this✝ : IsPretransitive G H
this : ⇑f = fun g ↦ g • 1
⊢ IsOpenMap fun g ↦ g • 1

Tactic:
]

Goal state after:
G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SigmaCompactSpace G
H : Type u_3
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : BaireSpace H
inst✝¹ : T2Space H
inst✝ : ContinuousMul H
f : G →* H
hf : Surjective ⇑f
h'f : Continuous[inst✝⁸, inst✝³] ⇑f
A : MulAction G H := MulAction.compHom H f
this✝¹ : ContinuousSMul G H
this✝ : IsPretransitive G H
this : ⇑f = fun g ↦ g • 1
⊢ IsOpenMap fun g ↦ g • 1
Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
s : Set G
x : G
hx : x ∈ s⁻¹
⊢ x⁻¹ ∈ (Subgroup.zpowers x⁻¹).topologicalClosure

Tactic:
]

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
s : Set G
x : G
hx : x ∈ s⁻¹
⊢ x⁻¹ ∈ (Subgroup.zpowers x⁻¹).topologicalClosure
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
x : M
ab : M × M
⊢ ab ∈ mulFiber x ↔ ab.1 * ab.2 = x

Tactic:
simp [mulFiber]

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
⊢ (1, 1) ∈ mulFiber 1

Tactic:
simp [mulFiber]

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
F : Type u_6
inst✝⁶ : Monoid M
inst✝⁵ : CommSemiring S
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid F
inst✝² : Module S E
inst✝¹ : Module S F
inst✝ : TopologicalSpace F
L : E →ₗ[S] F →ₗ[S] F
e : E
f : M → F
hL : ∀ (y : F), (L e) y = y
x : M
⊢ (L (if (↑⟨(1, x), ⋯⟩).1 ∈ {1} then e else 0)) (f (↑⟨(1, x), ⋯⟩).2) = f x

Tactic:
]

Goal state after:
M : Type u_1
S : Type u_2
E : Type u_3
F : Type u_6
inst✝⁶ : Monoid M
inst✝⁵ : CommSemiring S
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid F
inst✝² : Module S E
inst✝¹ : Module S F
inst✝ : TopologicalSpace F
L : E →ₗ[S] F →ₗ[S] F
e : E
f : M → F
hL : ∀ (y : F), (L e) y = y
x : M
⊢ (L (if (↑⟨(1, x), ⋯⟩).1 ∈ {1} then e else 0)) (f (↑⟨(1, x), ⋯⟩).2) = f x
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
F : Type u_6
inst✝⁶ : Monoid M
inst✝⁵ : CommSemiring S
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid F
inst✝² : Module S E
inst✝¹ : Module S F
inst✝ : TopologicalSpace F
L : F →ₗ[S] E →ₗ[S] F
f : M → F
e : E
hL : ∀ (y : F), (L y) e = y
x : M
⊢ (L (f (↑⟨(x, 1), ⋯⟩).1)) (if (↑⟨(x, 1), ⋯⟩).2 ∈ {1} then e else 0) = f x

Tactic:
]

Goal state after:
M : Type u_1
S : Type u_2
E : Type u_3
F : Type u_6
inst✝⁶ : Monoid M
inst✝⁵ : CommSemiring S
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid F
inst✝² : Module S E
inst✝¹ : Module S F
inst✝ : TopologicalSpace F
L : F →ₗ[S] E →ₗ[S] F
f : M → F
e : E
hL : ∀ (y : F), (L y) e = y
x : M
⊢ (L (f (↑⟨(x, 1), ⋯⟩).1)) (if (↑⟨(x, 1), ⋯⟩).2 ∈ {1} then e else 0) = f x
Module: Mathlib.Topology.Algebra.Module.EmbeddingOfLocal

Goal state before:
pp: 𝕜₁ : Type u_1
E : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜₁
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜₁ E
t₁ t₂ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜₁ E
inst✝ : ContinuousSMul 𝕜₁ E
V : Set E
𝓕₁ : Filter E := 𝓝 0
V_mem : V ∈ 𝓕₁
𝓕₂ : Filter E := 𝓝 0
H : 𝓕₁ = 𝓕₂ ⊓ 𝓟 V
this : 𝓕₁ = 𝓕₂
⊢ 𝓝 0 = 𝓝 0

pp: case tg
𝕜₁ : Type u_1
E : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜₁
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜₁ E
t₁ t₂ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜₁ E
inst✝ : ContinuousSMul 𝕜₁ E
V : Set E
𝓕₁ : Filter E := 𝓝 0
V_mem : V ∈ 𝓕₁
𝓕₂ : Filter E := 𝓝 0
H : 𝓕₁ = 𝓕₂ ⊓ 𝓟 V
this : 𝓕₁ = 𝓕₂
⊢ IsTopologicalAddGroup E

pp: case tg'
𝕜₁ : Type u_1
E : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜₁
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜₁ E
t₁ t₂ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜₁ E
inst✝ : ContinuousSMul 𝕜₁ E
V : Set E
𝓕₁ : Filter E := 𝓝 0
V_mem : V ∈ 𝓕₁
𝓕₂ : Filter E := 𝓝 0
H : 𝓕₁ = 𝓕₂ ⊓ 𝓟 V
this : 𝓕₁ = 𝓕₂
⊢ IsTopologicalAddGroup E

Tactic:
]

Goal state after:
𝕜₁ : Type u_1
E : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜₁
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜₁ E
t₁ t₂ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜₁ E
inst✝ : ContinuousSMul 𝕜₁ E
V : Set E
𝓕₁ : Filter E := 𝓝 0
V_mem : V ∈ 𝓕₁
𝓕₂ : Filter E := 𝓝 0
H : 𝓕₁ = 𝓕₂ ⊓ 𝓟 V
this : 𝓕₁ = 𝓕₂
⊢ 𝓝 0 = 𝓝 0

case tg
𝕜₁ : Type u_1
E : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜₁
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜₁ E
t₁ t₂ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜₁ E
inst✝ : ContinuousSMul 𝕜₁ E
V : Set E
𝓕₁ : Filter E := 𝓝 0
V_mem : V ∈ 𝓕₁
𝓕₂ : Filter E := 𝓝 0
H : 𝓕₁ = 𝓕₂ ⊓ 𝓟 V
this : 𝓕₁ = 𝓕₂
⊢ IsTopologicalAddGroup E

case tg'
𝕜₁ : Type u_1
E : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜₁
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜₁ E
t₁ t₂ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜₁ E
inst✝ : ContinuousSMul 𝕜₁ E
V : Set E
𝓕₁ : Filter E := 𝓝 0
V_mem : V ∈ 𝓕₁
𝓕₂ : Filter E := 𝓝 0
H : 𝓕₁ = 𝓕₂ ⊓ 𝓟 V
this : 𝓕₁ = 𝓕₂
⊢ IsTopologicalAddGroup E
Module: Mathlib.Topology.Algebra.Module.IsWeak

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : CommSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
inst : TopologicalSpace E
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
α : Type u_7
l : Filter α
f : α → E
x : E
hB_inj : Function.Injective ⇑B
⊢ Tendsto (fun x x2 ↦ (B (f x)) x2) l (𝓝 fun x2 ↦ (B x) x2) ↔ Tendsto (fun i ↦ ⇑(B (f i))) l (𝓝 ⇑(B x))

Tactic:
]

Goal state after: