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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
⊢ [T1Space X, ∀ (x : X), IsClosed[inst✝] {x}, ∀ (x : X), IsOpen[inst✝] {x}ᶜ, Continuous[inst✝, _] ⇑CofiniteTopology.of,
      ∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x, ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s,
      ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ y ∉ U, ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : X⦄, x ⤳ y → x = y, T0Space X ∧ R0Space X].TFAE

Tactic:
by
  tfae_have 1 ↔ 2 := ⟨fun h => h.1, fun h => ⟨h⟩⟩
  tfae_have 2 ↔ 3 := by
    simp only [isOpen_compl_iff]
  tfae_have 5 ↔ 3 := by
    refine forall_comm.trans ?_
    simp only [isOpen_iff_mem_nhds, mem_compl_iff, mem_singleton_iff]
  tfae_have 5 ↔ 6 := by
    simp only [← subset_compl_singleton_iff, exists_mem_subset_iff]
  tfae_have 5 ↔ 7 := by
    simp only [(nhds_basis_opens _).mem_iff, subset_compl_singleton_iff, and_assoc,
      and_left_comm]
  tfae_have 5 ↔ 8 := by
    simp only [← principal_singleton, disjoint_principal_right]
  tfae_have 8 ↔ 9 := forall_comm.trans (by simp only [disjoint_comm, ne_comm])
  tfae_have 1 → 4 := by
    simp only [continuous_def, CofiniteTopology.isOpen_iff']
    rintro H s (rfl | hs)
    · exact isOpen_empty
    · rw [← compl_compl s, preimage_compl]
      exact hs.preimage (Equiv.injective _).injOn |>.isClosed.isOpen_compl
  tfae_have 4 → 2 := by
    intro h x
    rw [← CofiniteTopology.of.preimage_image {x}]
    exact (Set.Finite.isClosed <| by simp) |>.preimage h
  tfae_have 2 ↔ 10 := by
    simp only [← closure_subset_iff_isClosed, specializes_iff_mem_closure, subset_def,
      mem_singleton_iff, eq_comm]
  tfae_have 10 ↔ 11 :=
    ⟨fun h => ⟨⟨fun _ _ h₂ => h h₂.specializes⟩, ⟨⟨fun _ _ h₂ => specializes_of_eq (h h₂).symm⟩⟩⟩,
      fun ⟨_, _⟩ _ _ h => (h.antisymm h.symm).eq⟩
  tfae_finish

Goal state after:
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : s.Finite
ht : t.Finite
h : Disjoint s t
⊢ SeparatedNhds (↑hs.toFinset) t

Tactic:
← ht.coe_toFinset

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : s.Finite
ht : t.Finite
h : Disjoint s t
⊢ SeparatedNhds ↑hs.toFinset ↑ht.toFinset
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
inst✝ : (𝓝[≠] x).NeBot
⊢ f =ᶠ[𝓝[≠] x] g ↔ f =ᶠ[𝓝 x] g

Tactic:
by
  constructor <;> intro hfg
  · apply eventuallyEq_nhds_of_eventuallyEq_nhdsNE hfg
    by_contra hCon
    obtain ⟨a, ha⟩ : {x | f x ≠ g x ∧ f x = g x}.Nonempty := by
      have h₁ := (eventually_nhdsWithin_of_eventually_nhds
        ((hf.ne_iff_eventually_ne hg).1 hCon)).and hfg
      have h₂ : ∅ ∉ 𝓝[≠] x := by exact empty_notMem (𝓝[≠] x)
      simp_all
    simp at ha
  · exact hfg.filter_mono nhdsWithin_le_nhds

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

Goal state before:
pp: case pos
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x✝ : TopologicalSpace X := sInf T
x y : X
hTd : ∃ t ∈ T, Disjoint (𝓝 x) (𝓝 y)
⊢ ⨅ t ∈ T, 𝓝 x ≤ ⨅ t ∈ T, 𝓝 y ∨ Disjoint (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)

Tactic:
rcases hTd with ⟨t, htT, htd⟩
    exact .inr <| htd.mono (iInf₂_le t htT) (iInf₂_le t htT)

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : R1Space X
inst✝ : WeaklyLocallyCompactSpace X
K : Set X
hK : IsCompact K
⊢ ∃ V, IsOpen[inst✝²] V ∧ K ⊆ V ∧ IsCompact (closure[inst✝²] V)

Tactic:
rcases exists_compact_superset hK with ⟨K', hK', hKK'⟩

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : R1Space X
inst✝ : WeaklyLocallyCompactSpace X
K : Set X
hK : IsCompact K
K' : Set X
hK' : IsCompact K'
hKK' : K ⊆ interior K'
⊢ ∃ V, IsOpen[inst✝²] V ∧ K ⊆ V ∧ IsCompact (closure[inst✝²] V)
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
x : α
⊢ IsOpen[inst✝¹] (connectedComponent x)

Tactic:
rw [← connectedComponentIn_univ]

Goal state after:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
x : α
⊢ IsOpen[inst✝¹] (connectedComponentIn univ x)
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : TopologicalSpace Y
f : Y → X
hf : IsInducing f
b : Y
s : Set X
hs : s ∈ 𝓝 (f b) ∧ IsClosed[inst✝²] s
⊢ IsClosed[inst✝] (f ⁻¹' id s)

Tactic:
exact hs.2.preimage hf.continuous

Goal state after:
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst✝] (t i)
hst : s ∩ ⋂ i, t i = ∅
⊢ ∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅

Tactic:
let U := tᶜ

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst✝] (t i)
hst : s ∩ ⋂ i, t i = ∅
U : ι → Set X := tᶜ
⊢ ∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : CountableInterFilter f
fsub : f ≤ 𝓟 s
U : ↑s → Set X
hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen[inst✝] (U x)
hUf : ∀ (x : ↑s), (U x)ᶜ ∈ f
t : Set ↑s
ht : t.Countable
h : s ⊆ ⋃ i ∈ t, U i
uinf : ⋃ i ∈ t, U i ∈ f.sets
uninf✝ : (⋃ i ∈ t, U i)ᶜ ∈ f
uninf : (⋃ i ∈ t, U i)ᶜᶜ ∉ f
⊢ False

Tactic:
simp only [compl_compl] at uninf

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : CountableInterFilter f
fsub : f ≤ 𝓟 s
U : ↑s → Set X
hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen[inst✝] (U x)
hUf : ∀ (x : ↑s), (U x)ᶜ ∈ f
t : Set ↑s
ht : t.Countable
h : s ⊆ ⋃ i ∈ t, U i
uinf : ⋃ i ∈ t, U i ∈ f.sets
uninf✝ : (⋃ i ∈ t, U i)ᶜ ∈ f
uninf : ⋃ i ∈ t, U i ∉ f
⊢ False
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
a b : Set α
ha : IsClopen a
hb : IsClopen b
ha' : a.Nonempty
hb' : b.Nonempty
hab : Disjoint a b
hs : IsClopen (a ∪ b)
H : IsPreconnected (a ∪ b)
⊢ ((a ∪ b) ∩ a).Nonempty

Tactic:
by rwa [union_inter_cancel_left]

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
a b : Set α
ha : IsClopen a
hb : IsClopen b
ha' : a.Nonempty
hb' : b.Nonempty
hab : Disjoint a b
hs : IsClopen (a ∪ b)
H : IsPreconnected (a ∪ b)
⊢ ((a ∪ b) ∩ b).Nonempty

Tactic:
rwa [union_inter_cancel_right]

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

Goal state before:
pp: case refine_2
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClopen s
H : ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b
a b : Set α
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hsab : s ⊆ a ∪ b
hsa : (s ∩ a).Nonempty
hsb : (s ∩ b).Nonempty
⊢ (s ∩ (a ∩ b)).Nonempty

Tactic:
rw [nonempty_iff_ne_empty]
    intro h
    exact H (s ∩ a) (s ∩ b)
      (isClopen_inter_of_disjoint_cover_clopen' hs hsab ha hb (by grind))
      (isClopen_inter_of_disjoint_cover_clopen' hs (by grind) hb ha (by grind))
      hsa hsb (by grind [Set.disjoint_iff_inter_eq_empty]) (by grind)

Goal state after:
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
inst✝ : TopologicalSpace γ
di : IsDenseInducing i
f : α → γ
a : α
hf : ContinuousAt f a
⊢ Tendsto f (𝓝 a) (𝓝 (di.extend f (i a)))

Tactic:
IsDenseInducing.extend,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
inst✝ : TopologicalSpace γ
di : IsDenseInducing i
f : α → γ
a : α
hf : ContinuousAt f a
⊢ Tendsto f (𝓝 a) (𝓝 ((comap i (𝓝 (i a))).limUnder f))
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: case h
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
S : Set (Set X)
hS : ∀ t ∈ S, IsNowhereDense t
hc : S.Countable
hsub : s ⊆ ⋃₀ S
⊢ (∀ ⦃x : Set X⦄, x ∈ closure[inst✝] '' S → IsClosed[inst✝] x ∧ IsNowhereDense x) ∧
    (compl '' closure[inst✝] '' S).Countable ∧ s ⊆ ⋃₀ (closure[inst✝] '' S)

Tactic:
rw [forall_mem_image]

Goal state after:
case h
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
S : Set (Set X)
hS : ∀ t ∈ S, IsNowhereDense t
hc : S.Countable
hsub : s ⊆ ⋃₀ S
⊢ (∀ ⦃x : Set X⦄, x ∈ S → IsClosed[inst✝] (closure[inst✝] x) ∧ IsNowhereDense (closure[inst✝] x)) ∧
    (compl '' closure[inst✝] '' S).Countable ∧ s ⊆ ⋃₀ (closure[inst✝] '' S)
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : IsQuotientMap f ∧ Injective f
s : Set X
hs : IsOpen[inst✝¹] s
⊢ IsOpen[inst✝¹] (f ⁻¹' f '' s)

Tactic:
Set.preimage_image_eq _ h.2

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : IsQuotientMap f ∧ Injective f
s : Set X
hs : IsOpen[inst✝¹] s
⊢ IsOpen[inst✝¹] s
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
V : SetRel α α
h : V ∈ 𝓤 α
⊢ V.symmetrize ∈ 𝓤 α

Tactic:
apply (𝓤 α).inter_sets h

Goal state after:
α : Type ua
inst✝ : UniformSpace α
V : SetRel α α
h : V ∈ 𝓤 α
⊢ V.inv ∈ (𝓤 α).sets
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
F : Filter (α × β)
⊢ Cauchy F ↔ Cauchy (map Prod.fst F) ∧ Cauchy (map Prod.snd F)

Tactic:
instUniformSpaceProd,

Goal state after:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
F : Filter (α × β)
⊢ Cauchy F ↔ Cauchy (map Prod.fst F) ∧ Cauchy (map Prod.snd F)
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: case mpr
β : Type ub
V W M : SetRel β β
inst✝ : W.IsSymm
x y : β
⊢ (ball (x, y).1 V ×ˢ ball (x, y).2 W ∩ M).Nonempty → (x, y) ∈ V ○ M ○ W

Tactic:
rintro ⟨⟨w, z⟩, ⟨w_in, z_in⟩, hwz⟩
    rw [mem_ball_symmetry] at z_in
    exact ⟨z, ⟨w, w_in, hwz⟩, z_in⟩

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

Goal state before:
pp: α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → SetRel α α
x : α
h : (𝓤 α).HasBasis p fun i ↦ Prod.swap ⁻¹' s i
⊢ (𝓝 x).HasBasis p fun i ↦ {y | (y, x) ∈ s i}

Tactic:
exact nhds_basis_uniformity' h

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ i, s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
⊢ ∃ x ∈ S, l ≤ 𝓝 x

Tactic:
obtain ⟨hl_ne, hl'⟩ := cauchy_iff.1 hl

Goal state after:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ i, s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
⊢ ∃ x ∈ S, l ≤ 𝓝 x
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ i, s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
i : ι
hi : t ⊆ s i
x : α
hxs : x ∈ s i
hlx : l ≤ 𝓝 x
⊢ ∃ x ∈ S, l ≤ 𝓝 x

Tactic:
exact ⟨x, mem_iUnion.2 ⟨i, hxs⟩, hlx⟩

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

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : CompleteSpace α
inst✝ : CompleteSpace β
f✝ : Filter (α × β)
hf : Cauchy f✝
x1 : α
hx1 : map (fun p ↦ p.1) f✝ ≤ 𝓝 x1
x2 : β
hx2 : map (fun p ↦ p.2) f✝ ≤ 𝓝 x2
⊢ f✝ ≤ 𝓝 (x1, x2)

Tactic:
rw [nhds_prod_eq, le_prod]

Goal state after:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : CompleteSpace α
inst✝ : CompleteSpace β
f✝ : Filter (α × β)
hf : Cauchy f✝
x1 : α
hx1 : map (fun p ↦ p.1) f✝ ≤ 𝓝 x1
x2 : β
hx2 : map (fun p ↦ p.2) f✝ ≤ 𝓝 x2
⊢ Tendsto Prod.fst f✝ (𝓝 x1) ∧ Tendsto Prod.snd f✝ (𝓝 x2)
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u : UniformSpace β
⊢ Tendsto Prod.swap (Filter.comap (fun p ↦ (f p.1, f p.2)) (𝓤 β)) (Filter.comap (fun p ↦ (f p.1, f p.2)) (𝓤 β))

Tactic:
by
    simp only [tendsto_comap_iff]
    exact tendsto_swap_uniformity.comp tendsto_comap

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

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f₁ : α → β
f₂ : α → γ
h₁ : UniformContinuous f₁
h₂ : UniformContinuous f₂
⊢ UniformContinuous fun a ↦ (f₁ a, f₂ a)

Tactic:
rw [UniformContinuous, uniformity_prod]
  exact tendsto_inf.2 ⟨tendsto_comap_iff.2 h₁, tendsto_comap_iff.2 h₂⟩

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

Goal state before:
pp: X : Type u_1
α : Type u_2
inst✝² : One α
inst✝¹ : TopologicalSpace X
Y : Type u_9
inst✝ : TopologicalSpace Y
g : Y → α
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
⊢ closure[inst✝¹] (f ⁻¹' mulSupport g) ⊆ f ⁻¹' closure[inst✝] (mulSupport g)

Tactic:
exact hf.closure_preimage_subset _

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
s : Set α
h : TotallyBounded s
⊢ IsSeparable s

Tactic:
by
  obtain ⟨t, -, htc, hts⟩ := subset_countable_closure_of_almost_dense_set s fun U hU => by
    obtain ⟨t, ht, hst⟩ := h (SetRel.inv U)
      (mem_of_superset (symmetrize_mem_uniformity hU) SetRel.symmetrize_subset_inv)
    exact ⟨t, ht.countable, hst⟩
  exact ⟨t, htc, hts⟩

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₀ ↔ ContinuousAt (⇑ofFun ∘ swap F) x₀

Tactic:
rw [ContinuousAt, (UniformFun.hasBasis_nhds ι α _).tendsto_right_iff]
  rfl

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

Goal state before:
pp: Y : Type u_5
α : Type u_6
β : Type u_8
tY : TopologicalSpace Y
uα : UniformSpace α
uβ : UniformSpace β
A : Set Y
u : Y → β → α
S : Set β
hA : UniformEquicontinuousOn (u ∘ Subtype.val) S
hu : Continuous[tY, Pi.topologicalSpace] (S.domRestrict ∘ u)
⊢ UniformEquicontinuousOn (u ∘ Subtype.val) S

Tactic:
intro U hU
  rcases mem_uniformity_isClosed hU with ⟨V, hV, hVclosed, hVU⟩
  filter_upwards [hA V hV, mem_inf_of_right (mem_principal_self _)]
  rintro ⟨x, y⟩ hxy ⟨hxS, hyS⟩
  rw [SetCoe.forall] at *
  change A ⊆ (fun f => (u f x, u f y)) ⁻¹' V at hxy
  refine (closure_minimal hxy <| hVclosed.preimage <| .prodMk ?_ ?_).trans (preimage_mono hVU)
  · exact (continuous_apply ⟨x, hxS⟩).comp hu
  · exact (continuous_apply ⟨y, hyS⟩).comp hu

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: G₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a : G₀
ha : 0 < a
⊢ (fun x ↦ a * x) '' Ioi 0 = Ioi 0

Tactic:
rw [image_mul_left_Ioi ha, mul_zero]

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

Goal state before:
pp: G : Type u_4
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousConstSMul G G
g : G
s : Set G
⊢ g • s ∈ 𝓝 g ↔ s ∈ 𝓝 1

Tactic:
by
  rw [← smul_mem_nhds_smul_iff g⁻¹]; simp

Goal state after:
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : IsProperMap f
⊢ IsClosedMap f

Tactic:
isClosedMap_iff_clusterPt

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : IsProperMap f
⊢ ∀ (s : Set X) (y : Y), MapClusterPt y (𝓟 s) f → ∃ x, f x = y ∧ ClusterPt x (𝓟 s)
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: case right
X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : Continuous[inst✝³, inst✝²] f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
hg : Continuous[inst✝¹, inst✝] g ∧ ∀ ⦃𝒰 : Ultrafilter Z⦄ ⦃y : W⦄, Tendsto g (↑𝒰) (𝓝 y) → ∃ x, g x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (X × Z)
y : Y
w : W
hyw : Tendsto (fun n ↦ (Prod.map f g n).1) (↑𝒰) (𝓝 y) ∧ Tendsto (fun n ↦ (Prod.map f g n).2) (↑𝒰) (𝓝 w)
x : X
hxy : f x = y
hx : ↑(Ultrafilter.map fst 𝒰) ≤ 𝓝 x
z : Z
hzw : g z = w
hz : ↑(Ultrafilter.map snd 𝒰) ≤ 𝓝 z
⊢ ↑𝒰 ≤ 𝓝 (x, z)

Tactic:
rw [nhds_prod_eq, le_prod]

Goal state after:
case right
X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : Continuous[inst✝³, inst✝²] f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
hg : Continuous[inst✝¹, inst✝] g ∧ ∀ ⦃𝒰 : Ultrafilter Z⦄ ⦃y : W⦄, Tendsto g (↑𝒰) (𝓝 y) → ∃ x, g x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (X × Z)
y : Y
w : W
hyw : Tendsto (fun n ↦ (Prod.map f g n).1) (↑𝒰) (𝓝 y) ∧ Tendsto (fun n ↦ (Prod.map f g n).2) (↑𝒰) (𝓝 w)
x : X
hxy : f x = y
hx : ↑(Ultrafilter.map fst 𝒰) ≤ 𝓝 x
z : Z
hzw : g z = w
hz : ↑(Ultrafilter.map snd 𝒰) ≤ 𝓝 z
⊢ Tendsto fst (↑𝒰) (𝓝 x) ∧ Tendsto snd (↑𝒰) (𝓝 z)
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul αᵐᵒᵖ α
s t : Set α
hs : IsOpen[inst✝²] s
⊢ IsOpen[inst✝²] (op '' t • s)

Tactic:
exact hs.smul_left

Goal state after:
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: α : Type u_3
inst✝¹ : UniformSpace α
inst✝ : Group α
h₁ : UniformContinuous fun p ↦ p.1 * p.2
h₂ : UniformContinuous fun p ↦ p⁻¹
⊢ UniformContinuous fun p ↦ p.1 / p.2

Tactic:
simpa only [div_eq_mul_inv] using!
    h₁.comp (uniformContinuous_fst.prodMk (h₂.comp uniformContinuous_snd))

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
x : G
s : Set G
⊢ (∀ i ∈ 𝓝 1, ∃ y ∈ s, y ∈ {y | y / x ∈ id i}) ↔ ∀ U ∈ 𝓝 1, ∃ y ∈ s, y / x ∈ U

Tactic:
Set.mem_ofPred,

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
x : G
s : Set G
⊢ (∀ i ∈ 𝓝 1, ∃ y ∈ s, y / x ∈ id i) ↔ ∀ U ∈ 𝓝 1, ∃ y ∈ s, y / x ∈ U
Module: Mathlib.Order.Filter.AtTopBot.Monoid

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
hfg : Tendsto (fun x ↦ f x * g x) l atTop
C : M
hC : ∀ᶠ (x : M) in map f l, (fun x1 x2 ↦ x1 ≤ x2) x C
x✝¹ : α
x✝ : (fun x1 x2 ↦ x1 ≤ x2) (f x✝¹) C
⊢ (fun x ↦ f x * g x) x✝¹ ≤ (fun x ↦ C * g x) x✝¹

Tactic:
by dsimp; gcongr

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Monoid

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
h : Tendsto (fun x ↦ f x * g x) l atTop
C : M
hC : ∀ᶠ (x : M) in map g l, (fun x1 x2 ↦ x1 ≤ x2) x C
x✝¹ : α
x✝ : (fun x1 x2 ↦ x1 ≤ x2) (g x✝¹) C
⊢ (fun x ↦ f x * g x) x✝¹ ≤ (fun x ↦ f x * C) x✝¹

Tactic:
by dsimp; gcongr

Goal state after:
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: case refine_2
β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁
φ_ψ_conj : φ = g * ψ * g⁻¹
⊢ Tendsto (fun x ↦ x.2.2⁻¹ * x.2.1) (𝓤 β ×ˢ 𝓤 β) (𝓝 1)

Tactic:
uniformity_eq_comap_inv_mul_nhds_one_swapped

Goal state after:
case refine_2
β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁
φ_ψ_conj : φ = g * ψ * g⁻¹
⊢ Tendsto (fun x ↦ x.2.2⁻¹ * x.2.1) (comap (fun x ↦ x.2⁻¹ * x.1) (𝓝 1) ×ˢ comap (fun x ↦ x.2⁻¹ * x.1) (𝓝 1)) (𝓝 1)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : (𝓝 1).HasBasis p U
⊢ (𝓤 α).HasBasis p fun i ↦ {x | x.2⁻¹ * x.1 ∈ U i}

Tactic:
uniformity_eq_comap_inv_mul_nhds_one_swapped

Goal state after:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : (𝓝 1).HasBasis p U
⊢ (Filter.comap (fun x ↦ x.2⁻¹ * x.1) (𝓝 1)).HasBasis p fun i ↦ {x | x.2⁻¹ * x.1 ∈ U i}
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
c a : G
⊢ map (fun x ↦ x / c) (𝓝[≠] a) = 𝓝[≠] (a / c)

Tactic:
by
  convert! (Homeomorph.divRight c).isEmbedding.map_nhdsWithin_eq .. using 2
  simp [div_eq_mul_inv]

Goal state after:
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: G : Type u_2
u : UniformSpace G
inst✝¹ : Group G
inst✝ : IsUniformGroup G
⊢ IsTopologicalGroup.rightUniformSpace G = u

Tactic:
by
  ext : 1
  rw [uniformity_eq_comap_nhds_one' G, uniformity_eq_comap_mul_inv_nhds_one]

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

Goal state before:
pp: A : Type u_2
E : Type u_6
inst✝⁴ : Monoid A
inst✝³ : TopologicalSpace A
inst✝² : CommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousMul E
f : A →ₜ* E
n : ℕ
a : A
⊢ (f ^ n) a = f a ^ n

Tactic:
induction n
  case zero => rw [pow_zero, pow_zero, one_toFun]
  case succ n ih => rw [pow_succ, pow_succ, ContinuousMonoidHom.mul_apply, ih]

Goal state after:
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
hom : Type u_3
inst✝⁶ : TopologicalSpace α
inst✝⁵ : Group α
inst✝⁴ : IsTopologicalGroup α
inst✝³ : TopologicalSpace β
inst✝² : Group β
inst✝¹ : FunLike hom β α
inst✝ : MonoidHomClass hom β α
e : hom
de : IsDenseInducing ⇑e
x₀ : α
comm : ((fun x ↦ x.2 / x.1) ∘ fun t ↦ (e t.1, e t.2)) = ⇑e ∘ fun t ↦ t.2 / t.1
lim : Tendsto (fun x ↦ x.2 / x.1) (𝓝 (x₀, x₀)) (𝓝 (e 1))
⊢ Tendsto (fun t ↦ t.2 / t.1) (comap (fun p ↦ (e p.1, e p.2)) (𝓝 (x₀, x₀))) (𝓝 1)

Tactic:
simpa using! de.tendsto_comap_nhds_nhds lim comm

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

Goal state before:
pp: G : Type u
inst✝⁷ : TopologicalSpace G
H : Type v
inst✝⁶ : TopologicalSpace H
M : Type u_1
N : Type u_2
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace N
inst✝³ : Mul M
inst✝² : Mul N
L : Type u_3
inst✝¹ : Mul L
inst✝ : TopologicalSpace L
cme1 : M ≃ₜ* N
cme2 : N ≃ₜ* L
⊢ Continuous (cme1.trans cme2.toMulEquiv).invFun

Tactic:
by convert! Continuous.comp cme1.continuous_invFun cme2.continuous_invFun

Goal state after: