mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: case refine_1
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i ↦ mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := {i ∈ hnf.toFinset | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset | x ∉ U j}
⊢ ⋂ j ∈ js, (mulTSupport (f j))ᶜ ∈ 𝓝 x

pp: case refine_2
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i ↦ mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := {i ∈ hnf.toFinset | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset | x ∉ U j}
⊢ ⋂ i ∈ is, U i ∈ 𝓝 x

pp: case refine_3
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i ↦ mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := {i ∈ hnf.toFinset | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset | x ∉ U j}
z : X
hz : z ∈ (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i
⊢ (mulSupport fun i ↦ f i z) ⊆ ↑is

Tactic:
· exact (biInter_finset_mem js).mpr fun j hj => IsClosed.compl_mem_nhds (isClosed_mulTSupport _)
        (Set.notMem_subset (hso j) (Finset.mem_filter.mp hj).2)

Goal state after:
case refine_2
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i ↦ mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := {i ∈ hnf.toFinset | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset | x ∉ U j}
⊢ ⋂ i ∈ is, U i ∈ 𝓝 x

case refine_3
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i ↦ mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := {i ∈ hnf.toFinset | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset | x ∉ U j}
z : X
hz : z ∈ (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i
⊢ (mulSupport fun i ↦ f i z) ⊆ ↑is
Module: Mathlib.Topology.UniformSpace.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst✝ : Nonempty ι
l : Filter ((i : ι) → α i)
⊢ Cauchy l ↔ ∀ (i : ι), Cauchy (map (eval i) l)

Tactic:
[

Goal state after:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst✝ : Nonempty ι
l : Filter ((i : ι) → α i)
⊢ Cauchy l ↔ ∀ (i : ι), Cauchy (map (eval i) l)
Module: Mathlib.Topology.UniformSpace.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
l : Filter ((i : ι) → α i)
inst✝ : l.NeBot
⊢ Cauchy l ↔ ∀ (i : ι), Cauchy (map (eval i) l)

Tactic:
[

Goal state after:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
l : Filter ((i : ι) → α i)
inst✝ : l.NeBot
⊢ Cauchy l ↔ ∀ (i : ι), Cauchy (map (eval i) l)
Module: Mathlib.Topology.UniformSpace.Pi

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
β : Type u_3
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst✝¹ : UniformSpace β
inst✝ : ∀ (i : ι), CompleteSpace (α i)
f : Filter ((i : ι) → α i)
hf : Cauchy f
this : f.NeBot
⊢ ∃ x, f ≤ 𝓝 x

Tactic:
[

Goal state after:
ι : Type u_1
ι' : Type u_2
β : Type u_3
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst✝¹ : UniformSpace β
inst✝ : ∀ (i : ι), CompleteSpace (α i)
f : Filter ((i : ι) → α i)
hf : Cauchy f
this : f.NeBot
⊢ ∃ x, f ≤ 𝓝 x
Module: Mathlib.Topology.UniformSpace.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
𝔖 : Set (Set ι)
⊢ UniformSpace.comap (⋃₀ 𝔖).domRestrict (uniformSpace fun i ↦ α ↑i) =
    ⨅ S ∈ 𝔖, UniformSpace.comap S.domRestrict (uniformSpace fun i ↦ α ↑i)

Tactic:
[

Goal state after:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
𝔖 : Set (Set ι)
⊢ UniformSpace.comap (⋃₀ 𝔖).domRestrict (uniformSpace fun i ↦ α ↑i) =
    ⨅ S ∈ 𝔖, UniformSpace.comap S.domRestrict (uniformSpace fun i ↦ α ↑i)
Module: Mathlib.Topology.UniformSpace.Pi

Goal state before:
pp: ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
a✝ : Nontrivial X
t : TopologicalSpace X
ht : T2Space X
hut : ∀ (i : ι), (u i).toTopologicalSpace ≤ t
⊢ IsUniformInducing (const ι)

Tactic:
[

Goal state after:
ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
a✝ : Nontrivial X
t : TopologicalSpace X
ht : T2Space X
hut : ∀ (i : ι), (u i).toTopologicalSpace ≤ t
⊢ IsUniformInducing (const ι)
Module: Mathlib.Topology.UniformSpace.Pi

Goal state before:
pp: ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
a✝ : Nontrivial X
t : TopologicalSpace X
ht : T2Space X
hut : ∀ (i : ι), (u i).toTopologicalSpace ≤ t
this : IsUniformInducing (const ι)
⊢ CompleteSpace X

Tactic:
[

Goal state after:
ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
a✝ : Nontrivial X
t : TopologicalSpace X
ht : T2Space X
hut : ∀ (i : ι), (u i).toTopologicalSpace ≤ t
this : IsUniformInducing (const ι)
⊢ CompleteSpace X
Module: Mathlib.Topology.UniformSpace.Pi

Goal state before:
pp: ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
ht : ∃ t, T2Space X ∧ ∀ (i : ι), (u i).toTopologicalSpace ≤ t
⊢ CompleteSpace X

Tactic:
by
  -- We can assume `X` is nonempty.
  nontriviality X
  rcases ht with ⟨t, ht, hut⟩
  -- The diagonal map `(X, ⨅ i, u i) → ∀ i, (X, u i)` is a uniform embedding.
  have : @IsUniformInducing X (ι → X) (⨅ i, u i) (Pi.uniformSpace (U := u)) (const ι) := by
    simp_rw [isUniformInducing_iff, iInf_uniformity, Pi.uniformity, Filter.comap_iInf,
      Filter.comap_comap, comp_def, const, Prod.eta, comap_id']
  -- Hence, it suffices to show that its range, the diagonal, is closed in `Π i, (X, u i)`.
  simp_rw [@completeSpace_iff_isComplete_range _ _ (_) (_) _ this, range_const_eq_diagonal,
    ofPred_forall]
  -- The separation of `t` ensures that this is the case in `Π i, (X, t)`, hence the result
  -- since the topology associated to each `u i` is finer than `t`.
  have : Pi.topologicalSpace (t₂ := fun i ↦ (u i).toTopologicalSpace) ≤
         Pi.topologicalSpace (t₂ := fun _ ↦ t) :=
    iInf_mono fun i ↦ induced_mono <| hut i
  refine IsClosed.isComplete <| .mono ?_ this
  exact isClosed_iInter fun i ↦ isClosed_iInter fun j ↦
    isClosed_eq (continuous_apply _) (continuous_apply _)

Goal state after:
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
x✝³ : α
x✝² : x✝³ ∈ s
x✝¹ : Set (β × β)
x✝ : x✝¹ ∈ 𝓤 β
⊢ (∃ t ∈ 𝓝[s] x✝³, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ x✝¹) ↔
    x✝¹ ∈ map (fun y ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x✝³)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
x✝³ : α
x✝² : x✝³ ∈ s
x✝¹ : Set (β × β)
x✝ : x✝¹ ∈ 𝓤 β
⊢ (∃ t ∈ 𝓝[s] x✝³, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ x✝¹) ↔
    x✝¹ ∈ map (fun y ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x✝³)
Module: Mathlib.Topology.UniformSpace.Equiv

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
hf : IsUniformInducing Equiv.ulift.toFun
⊢ UniformContinuous Equiv.ulift.invFun

Tactic:
[

Goal state after:
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
hf : IsUniformInducing Equiv.ulift.toFun
⊢ UniformContinuous Equiv.ulift.invFun
Module: Mathlib.Topology.UniformSpace.UniformApproximation

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
h : ∀ u ∈ 𝓤 β, ∃ F, UniformContinuousOn F s ∧ ∀ y ∈ s, (f y, F y) ∈ u
⊢ UniformContinuousOn f s

Tactic:
[

Goal state after:
α : Type u_4
β : Type u_5
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
h : ∀ u ∈ 𝓤 β, ∃ F, UniformContinuousOn F s ∧ ∀ y ∈ s, (f y, F y) ∈ u
⊢ UniformContinuousOn f s
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : TopologicalSpace γ
h : TendstoLocallyUniformlyOn F f p univ
g : γ → α
cg : ContinuousOn g univ
⊢ TendstoLocallyUniformlyOn (fun n ↦ F n ∘ g) (f ∘ g) p univ

Tactic:
exact h.comp _ (mapsTo_univ _ _) cg

Goal state after:
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
x₀ : X
⊢ EquicontinuousAt F x₀ ↔ ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
[

Goal state after:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
x₀ : X
⊢ EquicontinuousAt F x₀ ↔ ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
⊢ Equicontinuous F ↔ Continuous[tX, topologicalSpace ι α] (⇑ofFun ∘ swap F)

Tactic:
[

Goal state after:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
⊢ Equicontinuous F ↔ Continuous[tX, topologicalSpace ι α] (⇑ofFun ∘ swap F)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ comap
      (Prod.map ⇑(Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ)
        ⇑(Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ))
      (𝓤 ((α →ᵤ β) × (α →ᵤ γ))) =
    𝓤 (α →ᵤ β × γ)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ comap
      (Prod.map ⇑(Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ)
        ⇑(Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ))
      (𝓤 ((α →ᵤ β) × (α →ᵤ γ))) =
    𝓤 (α →ᵤ β × γ)
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
⊢ EquicontinuousOn F S ↔ ContinuousOn (⇑ofFun ∘ swap F) S

Tactic:
[

Goal state after:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
⊢ EquicontinuousOn F S ↔ ContinuousOn (⇑ofFun ∘ swap F) S
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
κ : Type u_2
X : Type u_3
α' : Type u_7
tX : TopologicalSpace X
u : κ → UniformSpace α'
F : ι → X → α'
⊢ Equicontinuous F ↔ ∀ (k : κ), Equicontinuous F

Tactic:
[

Goal state after:
ι : Type u_1
κ : Type u_2
X : Type u_3
α' : Type u_7
tX : TopologicalSpace X
u : κ → UniformSpace α'
F : ι → X → α'
⊢ Equicontinuous F ↔ ∀ (k : κ), Equicontinuous F
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
κ : Type u_2
X : Type u_3
α' : Type u_7
tX : TopologicalSpace X
u : κ → UniformSpace α'
F : ι → X → α'
S : Set X
⊢ EquicontinuousOn F S ↔ ∀ (k : κ), EquicontinuousOn F S

Tactic:
[

Goal state after:
ι : Type u_1
κ : Type u_2
X : Type u_3
α' : Type u_7
tX : TopologicalSpace X
u : κ → UniformSpace α'
F : ι → X → α'
S : Set X
⊢ EquicontinuousOn F S ↔ ∀ (k : κ), EquicontinuousOn F S
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α' : Type u_7
β : Type u_8
uβ : UniformSpace β
u : κ → UniformSpace α'
F : ι → β → α'
⊢ UniformEquicontinuous F ↔ ∀ (k : κ), UniformEquicontinuous F

Tactic:
[

Goal state after:
ι : Type u_1
κ : Type u_2
α' : Type u_7
β : Type u_8
uβ : UniformSpace β
u : κ → UniformSpace α'
F : ι → β → α'
⊢ UniformEquicontinuous F ↔ ∀ (k : κ), UniformEquicontinuous F
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α' : Type u_7
β : Type u_8
uβ : UniformSpace β
u : κ → UniformSpace α'
F : ι → β → α'
S : Set β
⊢ UniformEquicontinuousOn F S ↔ ∀ (k : κ), UniformEquicontinuousOn F S

Tactic:
[

Goal state after:
ι : Type u_1
κ : Type u_2
α' : Type u_7
β : Type u_8
uβ : UniformSpace β
u : κ → UniformSpace α'
F : ι → β → α'
S : Set β
⊢ UniformEquicontinuousOn F S ↔ ∀ (k : κ), UniformEquicontinuousOn F S
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_6
β' : Type u_9
uα : UniformSpace α
u : κ → UniformSpace β'
F : ι → β' → α
k : κ
hk : UniformEquicontinuous F
⊢ UniformEquicontinuous F

Tactic:
[

Goal state after:
ι : Type u_1
κ : Type u_2
α : Type u_6
β' : Type u_9
uα : UniformSpace α
u : κ → UniformSpace β'
F : ι → β' → α
k : κ
hk : UniformEquicontinuous F
⊢ UniformEquicontinuous F
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_6
β' : Type u_9
uα : UniformSpace α
u : κ → UniformSpace β'
F : ι → β' → α
S : Set β'
k : κ
hk : UniformEquicontinuousOn F S
⊢ UniformEquicontinuousOn F S

Tactic:
[

Goal state after:
ι : Type u_1
κ : Type u_2
α : Type u_6
β' : Type u_9
uα : UniformSpace α
u : κ → UniformSpace β'
F : ι → β' → α
S : Set β'
k : κ
hk : UniformEquicontinuousOn F S
⊢ UniformEquicontinuousOn F S
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
h_cover : ∃ I, I.Finite ∧ ⋃ i ∈ I, range (φ i) = univ
⊢ 𝓤 (α →ᵤ β) = 𝓤 (α →ᵤ β)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
h_cover : ∃ I, I.Finite ∧ ⋃ i ∈ I, range (φ i) = univ
⊢ 𝓤 (α →ᵤ β) = 𝓤 (α →ᵤ β)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
𝔖 : Set (Set α)
p : ι → Prop
s : ι → Set (β × β)
hb : (𝓤 β).HasBasis p s
S : Set α
⊢ (𝓤 (α →ᵤ[𝔖] β)).HasBasis p fun i ↦ UniformOnFun.gen 𝔖 S (s i)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
𝔖 : Set (Set α)
p : ι → Prop
s : ι → Set (β × β)
hb : (𝓤 β).HasBasis p s
S : Set α
⊢ (𝓤 (α →ᵤ[𝔖] β)).HasBasis p fun i ↦ UniformOnFun.gen 𝔖 S (s i)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
⊢ comap (fun x ↦ ((toFun {s | s.Finite}) x.1, (toFun {s | s.Finite}) x.2)) (𝓤 (α → β)) = 𝓤 (α →ᵤ[{s | s.Finite}] β)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
⊢ comap (fun x ↦ ((toFun {s | s.Finite}) x.1, (toFun {s | s.Finite}) x.2)) (𝓤 (α → β)) = 𝓤 (α →ᵤ[{s | s.Finite}] β)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
⊢ comap (fun x ↦ ((toFun {s | s.Finite}) x.1, (toFun {s | s.Finite}) x.2)) (⨅ i, comap (fun a ↦ (a.1 i, a.2 i)) (𝓤 β)) =
    𝓤 (α →ᵤ[{s | s.Finite}] β)

Tactic:
comap_iInf,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
⊢ ⨅ i, comap (fun x ↦ ((toFun {s | s.Finite}) x.1, (toFun {s | s.Finite}) x.2)) (comap (fun a ↦ (a.1 i, a.2 i)) (𝓤 β)) =
    𝓤 (α →ᵤ[{s | s.Finite}] β)
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f₁ f₂ : Filter α
g : Filter β
⊢ map₂ m (f₁ ⊔ f₂) g = map₂ m f₁ g ⊔ map₂ m f₂ g

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f₁ f₂ : Filter α
g : Filter β
⊢ map₂ m (f₁ ⊔ f₂) g = map₂ m f₁ g ⊔ map₂ m f₂ g
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
ι : Sort u_5
p : ι → Prop
V : ι → Set (β × β)
h : (𝓤 β).HasBasis p V
⊢ 𝓤 (α →ᵤ[𝔖] β) = ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i))

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
ι : Sort u_5
p : ι → Prop
V : ι → Set (β × β)
h : (𝓤 β).HasBasis p V
⊢ 𝓤 (α →ᵤ[𝔖] β) = ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i))
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g₁ g₂ : Filter β
⊢ map₂ m f (g₁ ⊔ g₂) = map₂ m f g₁ ⊔ map₂ m f g₂

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g₁ g₂ : Filter β
⊢ map₂ m f (g₁ ⊔ g₂) = map₂ m f g₁ ⊔ map₂ m f g₂
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
ι : Sort u_5
p : ι → Prop
V : ι → Set (β × β)
h : (𝓤 β).HasBasis p V
⊢ ⨅ i ∈ 𝔖,
      comap (Prod.map (⇑UniformFun.ofFun ∘ i.domRestrict ∘ ⇑(toFun 𝔖)) (⇑UniformFun.ofFun ∘ i.domRestrict ∘ ⇑(toFun 𝔖)))
        (⨅ i_1, ⨅ (_ : p i_1), 𝓟 ((UniformFun.gen (↑i) β ∘ V) i_1)) =
    ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i))

Tactic:
comap_iInf,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
ι : Sort u_5
p : ι → Prop
V : ι → Set (β × β)
h : (𝓤 β).HasBasis p V
⊢ ⨅ i ∈ 𝔖,
      ⨅ i_1,
        ⨅ (_ : p i_1),
          comap
            (Prod.map (⇑UniformFun.ofFun ∘ i.domRestrict ∘ ⇑(toFun 𝔖)) (⇑UniformFun.ofFun ∘ i.domRestrict ∘ ⇑(toFun 𝔖)))
            (𝓟 ((UniformFun.gen (↑i) β ∘ V) i_1)) =
    ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i))
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
ι : Sort u_5
p : ι → Prop
V : ι → Set (β × β)
h : (𝓤 β).HasBasis p V
f : α →ᵤ[𝔖] β
⊢ 𝓝 f = ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 {g | ∀ x ∈ s, ((toFun 𝔖) f x, (toFun 𝔖) g x) ∈ V i}

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
ι : Sort u_5
p : ι → Prop
V : ι → Set (β × β)
h : (𝓤 β).HasBasis p V
f : α →ᵤ[𝔖] β
⊢ 𝓝 f = ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 {g | ∀ x ∈ s, ((toFun 𝔖) f x, (toFun 𝔖) g x) ∈ V i}
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
n : β → α → γ
h_comm : ∀ (a : α) (b : β), m a b = n b a
⊢ map₂ (fun a b ↦ m b a) g f = map₂ n g f

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
n : β → α → γ
h_comm : ∀ (a : α) (b : β), m a b = n b a
⊢ map₂ (fun a b ↦ m b a) g f = map₂ n g f
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
ι : Sort u_5
p : ι → Prop
V : ι → Set (β × β)
h : (𝓤 β).HasBasis p V
f : α →ᵤ[𝔖] β
⊢ comap (Prod.mk f) (⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i))) =
    ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 {g | ∀ x ∈ s, ((toFun 𝔖) f x, (toFun 𝔖) g x) ∈ V i}

Tactic:
comap_iInf,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
ι : Sort u_5
p : ι → Prop
V : ι → Set (β × β)
h : (𝓤 β).HasBasis p V
f : α →ᵤ[𝔖] β
⊢ ⨅ i ∈ 𝔖, ⨅ i_1, ⨅ (_ : p i_1), comap (Prod.mk f) (𝓟 (UniformOnFun.gen 𝔖 i (V i_1))) =
    ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 {g | ∀ x ∈ s, ((toFun 𝔖) f x, (toFun 𝔖) g x) ∈ V i}
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
m : α → β → γ
f : Filter α
g : Filter β
n : γ → δ
m' : α' → β' → δ
n₁ : α → α'
n₂ : β → β'
h_distrib : ∀ (a : α) (b : β), n (m a b) = m' (n₁ a) (n₂ b)
⊢ map n (map₂ m f g) = map₂ m' (map n₁ f) (map n₂ g)

Tactic:
[

Goal state after:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
m : α → β → γ
f : Filter α
g : Filter β
n : γ → δ
m' : α' → β' → δ
n₁ : α → α'
n₂ : β → β'
h_distrib : ∀ (a : α) (b : β), n (m a b) = m' (n₁ a) (n₂ b)
⊢ map n (map₂ m f g) = map₂ m' (map n₁ f) (map n₂ g)
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : α → δ → ε
n : β → γ → δ
m₁ : α → β → β'
m₂ : α → γ → γ'
n' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)
s : Set ε
t₁ : Set β'
u₁ : Set α
hu₁ : u₁ ∈ f
v : Set β
hv : v ∈ g
ht₁ : image2 m₁ u₁ v ⊆ t₁
t₂ : Set γ'
hs : image2 n' t₁ t₂ ⊆ s
u₂ : Set α
hu₂ : u₂ ∈ f
w : Set γ
hw : w ∈ h
ht₂ : image2 m₂ u₂ w ⊆ t₂
⊢ image2 m₂ (u₁ ∩ u₂) w ⊆ t₂

Tactic:
exact (image2_subset_right inter_subset_right).trans ht₂

Goal state after:
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
γ : Type u_3
ι : Type u_4
𝔖 : Set (Set α)
u : ι → UniformSpace γ
⊢ uniformSpace α γ 𝔖 = ⨅ i, uniformSpace α γ 𝔖

Tactic:
[

Goal state after:
α : Type u_1
γ : Type u_3
ι : Type u_4
𝔖 : Set (Set α)
u : ι → UniformSpace γ
⊢ uniformSpace α γ 𝔖 = ⨅ i, uniformSpace α γ 𝔖
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : UniformSpace β
𝔖 : Set (Set α)
f : γ → β
⊢ uniformSpace α γ 𝔖 = UniformSpace.comap (fun x ↦ f ∘ x) (uniformSpace α β 𝔖)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : UniformSpace β
𝔖 : Set (Set α)
f : γ → β
⊢ uniformSpace α γ 𝔖 = UniformSpace.comap (fun x ↦ f ∘ x) (uniformSpace α β 𝔖)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : MapsTo (fun x ↦ f '' x) 𝔗 𝔖
⊢ UniformContinuous fun g ↦ (ofFun 𝔗) ((toFun 𝔖) g ∘ f)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : MapsTo (fun x ↦ f '' x) 𝔗 𝔖
⊢ UniformContinuous fun g ↦ (ofFun 𝔗) ((toFun 𝔖) g ∘ f)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s✝ : Set α
p : Filter ι
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
e : γ ≃ α
he : 𝔗 ⊆ image ⇑e ⁻¹' 𝔖
he' : 𝔖 ⊆ preimage ⇑e ⁻¹' 𝔗
s : Set α
hs : s ∈ 𝔖
⊢ ⇑e.symm '' s ∈ 𝔗

Tactic:
rw [Equiv.image_symm_eq_preimage]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s✝ : Set α
p : Filter ι
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
e : γ ≃ α
he : 𝔗 ⊆ image ⇑e ⁻¹' 𝔖
he' : 𝔖 ⊆ preimage ⇑e ⁻¹' 𝔗
s : Set α
hs : s ∈ 𝔖
⊢ ⇑e ⁻¹' s ∈ 𝔗
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
⊢ IsUniformInducing fun f s ↦ UniformFun.ofFun ((↑s).domRestrict ((toFun 𝔖) f))

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
⊢ IsUniformInducing fun f s ↦ UniformFun.ofFun ((↑s).domRestrict ((toFun 𝔖) f))