mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst✝¹] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
huv : s ⊆ u' ∪ v'
z : α
hz : z ∈ s ∩ s ∩ (u' ∩ v')
⊢ (f '' s ∩ (u ∩ v)).Nonempty

Tactic:
inter_assoc,

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst✝¹] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
huv : s ⊆ u' ∪ v'
z : α
hz : z ∈ s ∩ (s ∩ (u' ∩ v'))
⊢ (f '' s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
hs : IsPreconnected s
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen[inst✝¹] u
hv : IsOpen[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (s ∩ f '' u).Nonempty

pp: case refine_3
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
hs : IsPreconnected s
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen[inst✝¹] u
hv : IsOpen[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (s ∩ f '' v).Nonempty

Tactic:
· simpa only [image_preimage_inter] using hsu.image f

Goal state after:
case refine_3
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
hs : IsPreconnected s
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen[inst✝¹] u
hv : IsOpen[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (s ∩ f '' v).Nonempty
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (s ∩ f '' u).Nonempty

pp: case refine_3
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (s ∩ f '' v).Nonempty

Tactic:
· simpa only [image_preimage_inter] using hsu.image f

Goal state after:
case refine_3
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (s ∩ f '' v).Nonempty
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst✝] (U i)
hsU : s ⊆ ⋃ i, U i
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → (∃ r, r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
hcountable_union :
  ∀ (S : Set (Set X)),
    S.Countable → (∀ s ∈ S, ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i
x : X
hx : x ∈ s
i : ι
hi : x ∈ U i
⊢ ∃ t ∈ 𝓝[s] x, ∃ r, r.Countable ∧ t ⊆ ⋃ i ∈ r, U i

Tactic:
refine ⟨U i, mem_nhdsWithin_of_mem_nhds ((hUo i).mem_nhds hi), {i}, by simp, ?_⟩

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst✝] (U i)
hsU : s ⊆ ⋃ i, U i
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → (∃ r, r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
hcountable_union :
  ∀ (S : Set (Set X)),
    S.Countable → (∀ s ∈ S, ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i
x : X
hx : x ∈ s
i : ι
hi : x ∈ U i
⊢ U i ⊆ ⋃ i_1 ∈ {i}, U i_1
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
K : Set X
hK : IsCompact K
U : Set X
hU : IsOpen[inst✝²] U
h_KU : K ⊆ U
⊢ ∃ r ∈ 𝓝ˢ K, (IsCompact r ∧ IsClosed[inst✝²] r) ∧ r ⊆ U

Tactic:
obtain ⟨L, hL, hL', hKL, hLU⟩ := exists_compact_closed_between hK hU h_KU

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
K : Set X
hK : IsCompact K
U : Set X
hU : IsOpen[inst✝²] U
h_KU : K ⊆ U
L : Set X
hL : IsCompact L
hL' : IsClosed[inst✝²] L
hKL : K ⊆ interior L
hLU : L ⊆ U
⊢ ∃ r ∈ 𝓝ˢ K, (IsCompact r ∧ IsClosed[inst✝²] r) ∧ r ⊆ U
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed[inst✝¹] s
ht : IsOpen[inst✝¹] t
hst : s ⊆ t
this : Disjoint s tᶜ
s' t' : Set X
hs' : IsOpen[inst✝¹] s'
ht' : IsOpen[inst✝¹] t'
hss' : s ⊆ s'
htt' : tᶜ ⊆ t'
hs't' : Disjoint s' t'
⊢ ∃ u, IsOpen[inst✝¹] u ∧ s ⊆ u ∧ closure[inst✝¹] u ⊆ t

Tactic:
refine ⟨s', hs', hss', Subset.trans (closure_minimal ?_ (isClosed_compl_iff.2 ht'))
    (compl_subset_comm.1 htt')⟩

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed[inst✝¹] s
ht : IsOpen[inst✝¹] t
hst : s ⊆ t
this : Disjoint s tᶜ
s' t' : Set X
hs' : IsOpen[inst✝¹] s'
ht' : IsOpen[inst✝¹] t'
hss' : s ⊆ s'
htt' : tᶜ ⊆ t'
hs't' : Disjoint s' t'
⊢ s' ⊆ t'ᶜ
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_2.a
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed[inst✝] s
H : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
H1 : IsClosed[inst✝] (u ∩ s) → IsClosed[inst✝] (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∨ s ⊆ v
⊢ Disjoint (u ∩ s) (v ∩ s)

Tactic:
rwa [disjoint_iff_inter_eq_empty, ← inter_inter_distrib_right, inter_comm]

Goal state after:
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), connectedComponent x = univ
hα : IsEmpty α
⊢ IsPreconnected univ

Tactic:
rw [univ_eq_empty_iff.mpr hα]; exact isPreconnected_empty

Goal state after:
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : IsDenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
T' : Set β
hT₁ : T' ∈ 𝓝 (f x)
hT₂ : IsClosed[inst✝¹] T'
hT₃ : T' ⊆ T
hT₄ : f ⁻¹' T' ∈ 𝓝 x
i : ι
hi : p i
hi' : s i ⊆ f ⁻¹' T'
⊢ ∃ i, p i ∧ closure[inst✝¹] (f '' s i) ⊆ T

Tactic:
exact
      ⟨i, hi,
        (closure_mono (image_mono hi')).trans
          (Subset.trans (closure_minimal (image_preimage_subset _ _) hT₂) hT₃)⟩

Goal state after:
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : IsEmbedding f
⊢ IsTotallyDisconnected (f '' s) ↔ IsTotallyDisconnected s

Tactic:
refine ⟨hf.isTotallyDisconnected, fun hs u hus hu ↦ ?_⟩
  obtain ⟨v, hvs, rfl⟩ : ∃ v, v ⊆ s ∧ f '' v = u :=
    ⟨f ⁻¹' u ∩ s, inter_subset_right, by rwa [image_preimage_inter, inter_eq_left]⟩
  rw [hf.isInducing.isPreconnected_image] at hu
  exact (hs v hvs hu).image _

Goal state after:
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed[inst✝] s
⊢ IsNowhereDense s ↔ interior s = ∅

Tactic:
by
  rw [IsNowhereDense, IsClosed.closure_eq hs]

Goal state after:
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : T2Space Y
f : X ≃ Y
hf : Continuous[inst✝³, inst✝²] ⇑f
⊢ Continuous[inst✝², inst✝³] ⇑f.symm

Tactic:
continuous_iff_isClosed

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : T2Space Y
f : X ≃ Y
hf : Continuous[inst✝³, inst✝²] ⇑f
⊢ ∀ (s : Set X), IsClosed[inst✝³] s → IsClosed[inst✝²] (⇑f.symm ⁻¹' s)
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ ∃ V ∈ 𝓤 α, ball x V ⊆ s

Tactic:
rw [nhds_eq_comap_uniformity, mem_comap]
  simp_rw [ball]

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

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
⊢ Tendsto Prod.swap (𝓟 SetRel.id) (𝓟 SetRel.id)

Tactic:
by simp [Tendsto, SetRel.id]

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
s : Set α
hs : (𝓟 s).TotallyBounded
U : SetRel α α
hU : U ∈ 𝓤 α
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U}

Tactic:
← SetRel.preimage_eq_biUnion

Goal state after:
α : Type u
uniformSpace : UniformSpace α
s : Set α
hs : (𝓟 s).TotallyBounded
U : SetRel α α
hU : U ∈ 𝓤 α
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ U.preimage t
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous fun p ↦ f p.1 p.2
ha : UniformContinuous id
hb : UniformContinuous id
⊢ UniformContinuous fun p ↦ f p.1 p.2

Tactic:
have h_unif_cont_id :=
    @UniformContinuous.prodMap _ _ _ _ (ua1 ⊓ ua2) (ub1 ⊓ ub2) ua2 ub2 _ _ ha hb

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous fun p ↦ f p.1 p.2
ha : UniformContinuous id
hb : UniformContinuous id
h_unif_cont_id : UniformContinuous (Prod.map id id)
⊢ UniformContinuous fun p ↦ f p.1 p.2
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
h : ∀ (s : Set (α × α)), s ∈ 𝓤 α ↔ ∃ t ∈ 𝓤 β, ∀ (x y : α), (f x, f y) ∈ t → (x, y) ∈ s
⊢ comap (fun x ↦ (f x.1, f x.2)) (𝓤 β) = 𝓤 α

Tactic:
simp [eq_comm, Filter.ext_iff, subset_def, h]

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

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
x : α ⊕ β
⊢ 𝓝 x = comap (Prod.mk x) (map (fun p ↦ (inl p.1, inl p.2)) (𝓤 α) ⊔ map (fun p ↦ (inr p.1, inr p.2)) (𝓤 β))

Tactic:
ext
    cases x <;> simp [mem_comap', -mem_comap, nhds_inl, nhds_inr, nhds_eq_comap_uniformity,
      Prod.ext_iff]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
ι : Sort u_1
ι' : Sort u_2
p : ι → Prop
p' : ι' → Prop
s : ι → Set (α × α)
s' : ι' → Set (β × β)
h : (𝓤 α).HasBasis p s
h' : (𝓤 β).HasBasis p' s'
f : α → β
⊢ IsUniformEmbedding f ↔
    Injective f ∧ UniformContinuous f ∧ ∀ (j : ι), p j → ∃ i, p' i ∧ ∀ (x y : α), (f x, f y) ∈ s' i → (x, y) ∈ s j

Tactic:
by
  simp only [h.isUniformEmbedding_iff' h', h.uniformContinuous_iff h']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst✝ : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
⊢ ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s

Tactic:
obtain ⟨t, ht, hts⟩ := comp3_mem_uniformity hs

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst✝ : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : SetRel.comp t (SetRel.comp t t) ⊆ s
⊢ ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
γ : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : One γ
f : α → γ
inst✝ : TopologicalSpace γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
⊢ (mulTSupport f)ᶜ ⊆ f ⁻¹' N

Tactic:
intro v hv

Goal state after:
α : Type u_2
γ : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : One γ
f : α → γ
inst✝ : TopologicalSpace γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
v : α
hv : v ∈ (mulTSupport f)ᶜ
⊢ v ∈ f ⁻¹' N
Module: Mathlib.Topology.UniformSpace.Pi

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

Tactic:
simp +unfoldPartialApp
    [← iInf_subtype'', ← uniformSpace_comap_precomp' _ ((↑) : S → ι), Set.domRestrict]

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 → α
S : Set X
x₀ : X
hx₀ : x₀ ∈ S
⊢ EquicontinuousWithinAt F S x₀ ↔ ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
constructor <;> intro H U hU

Goal state after:
case mp
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
x₀ : X
hx₀ : x₀ ∈ S
H : EquicontinuousWithinAt F S x₀
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U

case mpr
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
x₀ : X
hx₀ : x₀ ∈ S
H : ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ∀ᶠ (x : X) in 𝓝[S] x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
κ : Type u_2
X' : Type u_4
α : Type u_6
uα : UniformSpace α
t : κ → TopologicalSpace X'
F : ι → X' → α
S : Set X'
x₀ : X'
k : κ
hk : EquicontinuousWithinAt F S x₀
⊢ EquicontinuousWithinAt F S x₀

Tactic:
simp only [equicontinuousWithinAt_iff_continuousWithinAt (tX := _)] at hk ⊢

Goal state after:
ι : Type u_1
κ : Type u_2
X' : Type u_4
α : Type u_6
uα : UniformSpace α
t : κ → TopologicalSpace X'
F : ι → X' → α
S : Set X'
x₀ : X'
k : κ
hk : ContinuousWithinAt (⇑ofFun ∘ swap F) S x₀
⊢ ContinuousWithinAt (⇑ofFun ∘ swap F) S x₀
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
⊢ 𝓤 (α →ᵤ β) = ⨅ i, 𝓤 (α →ᵤ β)

Tactic:
uniformity_comap

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
⊢ 𝓤 (α →ᵤ β) =
    ⨅ i, comap (Prod.map (⇑ofFun ∘ (fun x ↦ x ∘ φ i) ∘ ⇑toFun) (⇑ofFun ∘ (fun x ↦ x ∘ φ i) ∘ ⇑toFun)) (𝓤 (δ i →ᵤ β))
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 ↦
    Prod.map (S.domRestrict ∘ ⇑UniformFun.toFun) (S.domRestrict ∘ ⇑UniformFun.toFun) ⁻¹' UniformFun.gen (↑S) β (s i)

Tactic:
uniformity_comap

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 α
⊢ (comap (Prod.map S.domRestrict S.domRestrict) (𝓤 (↑S → β))).HasBasis p fun i ↦
    Prod.map (S.domRestrict ∘ ⇑UniformFun.toFun) (S.domRestrict ∘ ⇑UniformFun.toFun) ⁻¹' UniformFun.gen (↑S) β (s i)
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
⊢ (map₂ m f g).NeBot ↔ f.NeBot ∧ g.NeBot

Tactic:
simp [neBot_iff, not_or]

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

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set (β × β)
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → β → α
hβ : (𝓤 β).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ UniformEquicontinuous F ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂

Tactic:
rw [uniformEquicontinuous_iff_uniformContinuous, UniformContinuous,
    hβ.tendsto_iff (UniformFun.hasBasis_uniformity_of_basis ι α hα)]

Goal state after:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set (β × β)
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → β → α
hβ : (𝓤 β).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ (∀ (ib : κ₂),
      p₂ ib →
        ∃ ia, p₁ ia ∧ ∀ x ∈ s₁ ia, ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2) ∈ (UniformFun.gen ι α ∘ s₂) ib) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂
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 α)
inst✝ : UniformSpace γ
H : 𝓤 (α →ᵤ[𝔖] β × γ) = 𝓤 (α →ᵤ[𝔖] β × γ)
⊢ comap
        ((fun p ↦ (p.1.1, p.2.1)) ∘ fun x ↦
          (((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.1,
            ((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.2))
        (𝓤 (α →ᵤ[𝔖] β)) ⊓
      comap
        ((fun p ↦ (p.1.2, p.2.2)) ∘ fun x ↦
          (((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.1,
            ((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.2))
        (𝓤 (α →ᵤ[𝔖] γ)) =
    comap (Prod.map (fun x ↦ Prod.fst ∘ x) fun x ↦ Prod.fst ∘ x) (𝓤 (α → β)) ⊓ 𝓤 (α →ᵤ[𝔖] β × γ)

Tactic:
uniformity_comap

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
H : 𝓤 (α →ᵤ[𝔖] β × γ) = 𝓤 (α →ᵤ[𝔖] β × γ)
⊢ comap
        ((fun p ↦ (p.1.1, p.2.1)) ∘ fun x ↦
          (((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.1,
            ((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.2))
        (𝓤 (α →ᵤ[𝔖] β)) ⊓
      comap
        ((fun p ↦ (p.1.2, p.2.2)) ∘ fun x ↦
          (((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.1,
            ((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.2))
        (𝓤 (α →ᵤ[𝔖] γ)) =
    comap (Prod.map (fun x ↦ Prod.fst ∘ x) fun x ↦ Prod.fst ∘ x) (𝓤 (α → β)) ⊓
      comap (Prod.map (fun x ↦ Prod.snd ∘ x) fun x ↦ Prod.snd ∘ x) (𝓤 (α → γ))
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
φ : (i : ι) → δ i → α
𝔗 : (i : ι) → Set (Set (δ i))
h_image : ∀ (i : ι), MapsTo (fun x ↦ φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x ↦ φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
ψ : (S : Set α) → (i : ι) → ↑(φ i ⁻¹' S) → ↑S := fun S i ↦ S.restrictPreimage (φ i)
this :
  ∀ S ∈ 𝔖,
    UniformFun.uniformSpace (↑S) β =
      ⨅ i, UniformSpace.comap (fun x ↦ x ∘ ψ S i) (UniformFun.uniformSpace (↑(φ i ⁻¹' S)) β)
S : Set α
hS : S ∈ 𝔖
⊢ ⨅ i,
      ⨅ i_1 ∈ 𝔗 i,
        UniformSpace.comap
          ((⇑UniformFun.ofFun ∘ i_1.domRestrict ∘ ⇑(toFun (𝔗 i))) ∘ ⇑(ofFun (𝔗 i)) ∘ (fun x ↦ x ∘ φ i) ∘ ⇑(toFun 𝔖))
          (UniformFun.uniformSpace (↑i_1) β) ≤
    ⨅ i,
      UniformSpace.comap ((fun x ↦ x ∘ ψ S i) ∘ ⇑UniformFun.ofFun ∘ S.domRestrict ∘ ⇑(toFun 𝔖))
        (UniformFun.uniformSpace (↑(φ i ⁻¹' S)) β)

Tactic:
exact iInf_mono fun i ↦ iInf₂_le_of_le _ (h_preimage i hS) le_rfl

Goal state after:
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : SMul M α
inst✝ : ContinuousConstSMul M α
s : Set M
t : Set α
⊢ s • closure[inst✝²] t ⊆ closure[inst✝²] (s • t)

Tactic:
simp only [← iUnion_smul_set]

Goal state after:
M : Type u_1
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : SMul M α
inst✝ : ContinuousConstSMul M α
s : Set M
t : Set α
⊢ ⋃ a ∈ s, a • closure[inst✝²] t ⊆ closure[inst✝²] (⋃ a ∈ s, a • t)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
hg : UniformContinuousOn g s
h : TendstoUniformly F f p
s' : Set ι
hs' : s' ∈ p
hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s
F' : ι → α → β := fun i x ↦ if i ∈ s' then F i x else f x
⊢ ∃ s ∈ p, EqOn F F' s

Tactic:
refine ⟨s', hs', fun y hy => by grind⟩

Goal state after:
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace M
inst✝⁶ : Mul M
inst✝⁵ : ContinuousMul M
inst✝⁴ : TopologicalSpace N
inst✝³ : Monoid N
inst✝² : ContinuousMul N
inst✝¹ : T2Space N
f : ι → Nˣ
r₁ r₂ : N
l : Filter ι
inst✝ : l.NeBot
h₁ : Tendsto (fun x ↦ ↑(f x)) l (𝓝 r₁)
h₂ : Tendsto (fun x ↦ ↑(f x)⁻¹) l (𝓝 r₂)
⊢ 1 = r₁ * r₂

Tactic:
simpa using h₁.mul h₂

Goal state after:
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
⊢ ContinuousMul M

Tactic:
by
  apply ContinuousMul.of_nhds_one hmul hleft
  intro x₀
  simp_rw [mul_comm, hleft x₀]

Goal state after: