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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
t : Finset (Set X)
⊢ (∀ u ∈ t, IsOpen[inst✝] u) → (∀ u ∈ t, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑t).Nonempty ↔
    (∀ x ∈ t, IsClosed[inst✝] xᶜ) → s ⊆ ⋃ a ∈ ↑t, aᶜ → ∃ z, (∃ a ∈ t, aᶜ = z) ∧ s ⊆ z

Tactic:
isClosed_compl_iff,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
t : Finset (Set X)
⊢ (∀ u ∈ t, IsOpen[inst✝] u) → (∀ u ∈ t, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑t).Nonempty ↔
    (∀ u ∈ t, IsOpen[inst✝] u) → s ⊆ ⋃ a ∈ ↑t, aᶜ → ∃ z, (∃ a ∈ t, aᶜ = z) ∧ s ⊆ z
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
U s : Set X
h : sᶜ ∈ codiscreteWithin U
⊢ IsDiscrete (s ∩ U)

Tactic:
by
  rw [(by simp : ((s ∩ U) : Set X) = ((sᶜ ∪ Uᶜ)ᶜ : Set X)), isDiscrete_iff_nhdsNE]
  simp_rw [← Filter.mem_iff_inf_principal_compl]
  simp_all [← Set.compl_sdiff, mem_codiscreteWithin]

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case h₂
X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ Z ⊆ closure[inst✝] (⋃₀ (irreducibleComponents X \ {Z}))ᶜ

Tactic:
← Set.inter_eq_right.mpr h

Goal state after:
case h₂
X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ Z ⊆ closure[inst✝] (Z ∩ (⋃₀ (irreducibleComponents X \ {Z}))ᶜ)
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
V : Set Y
hV : IsPreirreducible V
f : X → Y
hf' : IsOpenMap f
hf'' : V ⊆ closure[inst✝] (V ∩ {x | IsPreirreducible (f ⁻¹' {x})})
U₁ U₂ : Set X
hU₁ : IsOpen[inst✝¹] U₁
hU₂ : IsOpen[inst✝¹] U₂
x : X
hxV : x ∈ f ⁻¹' V
hxU₁ : x ∈ U₁
y : X
hyV : y ∈ f ⁻¹' V
hyU₂ : y ∈ U₂
z : Y
hzV : z ∈ V
hz₁ : z ∈ f '' U₁
hz₂ : z ∈ f '' U₂
⊢ (f ⁻¹' V ∩ (U₁ ∩ U₂)).Nonempty

Tactic:
obtain ⟨z, ⟨⟨z₁, hz₁, e₁⟩, ⟨z₂, hz₂, e₂⟩⟩, hzV, hz⟩ :=
    mem_closure_iff.mp (hf'' hzV) _ ((hf' _ hU₁).inter (hf' _ hU₂)) ⟨hz₁, hz₂⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
V : Set Y
hV : IsPreirreducible V
f : X → Y
hf' : IsOpenMap f
hf'' : V ⊆ closure[inst✝] (V ∩ {x | IsPreirreducible (f ⁻¹' {x})})
U₁ U₂ : Set X
hU₁ : IsOpen[inst✝¹] U₁
hU₂ : IsOpen[inst✝¹] U₂
x : X
hxV : x ∈ f ⁻¹' V
hxU₁ : x ∈ U₁
y : X
hyV : y ∈ f ⁻¹' V
hyU₂ : y ∈ U₂
z✝ : Y
hzV✝ : z✝ ∈ V
hz₁✝ : z✝ ∈ f '' U₁
hz₂✝ : z✝ ∈ f '' U₂
z : Y
z₁ : X
hz₁ : z₁ ∈ U₁
e₁ : f z₁ = z
z₂ : X
hz₂ : z₂ ∈ U₂
e₂ : f z₂ = z
hzV : z ∈ V
hz : z ∈ {x | IsPreirreducible (f ⁻¹' {x})}
⊢ (f ⁻¹' V ∩ (U₁ ∩ U₂)).Nonempty
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
s t : Set X
H1 : IsClosed[inst✝¹] s
H2 : IsCompact (closure[inst✝¹] sᶜ)
H3 : IsClosed[inst✝¹] t
H4 : Disjoint s t
ht : IsCompact t
⊢ SeparatedNhds (closure[inst✝¹] s ∩ closure[inst✝¹] sᶜ) t

Tactic:
H1.closure_eq

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
s t : Set X
H1 : IsClosed[inst✝¹] s
H2 : IsCompact (closure[inst✝¹] sᶜ)
H3 : IsClosed[inst✝¹] t
H4 : Disjoint s t
ht : IsCompact t
⊢ SeparatedNhds (s ∩ closure[inst✝¹] sᶜ) t
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: case mpr
ι : Type u_4
X : ι → Type u_5
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), T2Space (X i)
s : Set ((i : ι) → X i)
H : IsClosed[topologicalSpace] s ∧ ∀ (i : ι), IsCompact (eval i '' s)
⊢ IsCompact s

Tactic:
· exact IsCompact.of_isClosed_subset (isCompact_univ_pi H.2) H.1 (subset_pi_eval_image univ s)

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
x y : X
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ insert x s =ᶠ[𝓝 x] insert x t

Tactic:
simp_rw [eventuallyEq_set] at h ⊢

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
x y : X
h : ∀ᶠ (x : X) in 𝓝[{y}ᶜ] x, x ∈ s ↔ x ∈ t
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, x_1 ∈ insert x s ↔ x_1 ∈ insert x t
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Sort u_3
inst✝ : Finite ι
s : ι → Set X
hs : ∀ (i : ι), IsDiscrete (s i)
hsc : ∀ (i : ι), IsClosed[inst✝¹] (s i)
⊢ (⋃ i, s i)ᶜ ∈ codiscrete X

Tactic:
simp [compl_mem_codiscrete_iff, *]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K L : Set X
hK : IsCompact K
hL : IsCompact L
h'L : IsClosed[inst✝¹] L
hd : Disjoint K L
⊢ ∀ x ∈ K, ∀ x_1 ∈ L, Disjoint (𝓝 x) (𝓝 x_1)

Tactic:
disjoint_nhds_nhds_iff_not_inseparable

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K L : Set X
hK : IsCompact K
hL : IsCompact L
h'L : IsClosed[inst✝¹] L
hd : Disjoint K L
⊢ ∀ x ∈ K, ∀ x_1 ∈ L, ¬Inseparable x x_1
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hV : IsOpen[inst✝¹] V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure[inst✝¹] K)
this : SeparatedNhds (closure[inst✝¹] K \ U) (closure[inst✝¹] K \ V)
O₁ O₂ : Set X
h1O₁ : IsOpen[inst✝¹] O₁
h1O₂ : IsOpen[inst✝¹] O₂
h2O₁ : K \ U ⊆ O₁
h2O₂ : K \ V ⊆ O₂
hO : Disjoint O₁ O₂
⊢ K = K \ O₁ ∪ K \ O₂

Tactic:
rw [← sdiff_inter, hO.inter_eq, sdiff_empty]

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

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst✝², inst✝¹] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
⊢ ∀ x_1 ∈ f '' K \ interior s, Disjoint (𝓝 (f x)) (𝓝 x_1)

Tactic:
disjoint_nhds_nhds_iff_not_inseparable

Goal state after:
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst✝², inst✝¹] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
⊢ ∀ x_1 ∈ f '' K \ interior s, ¬Inseparable (f x) x_1
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyConnectedSpace (X i)
hfinite : {i | ¬PreconnectedSpace (X i)}.Finite
⊢ LocallyConnectedSpace ((i : ι) → X i)

Tactic:
refine locallyConnectedSpace_iff_connected_subsets.2 fun x U hU ↦ ?_
  rw [nhds_pi, Filter.mem_pi] at hU
  obtain ⟨J, hJ, t, ht, htU⟩ := hU
  let K := J ∪ {i | ¬PreconnectedSpace (X i)}
  refine ⟨K.pi fun i ↦ connectedComponentIn (t i) (x i),
    set_pi_mem_nhds (hJ.union hfinite) fun i _ ↦ connectedComponentIn_mem_nhds (ht i), ?_,
    fun f hf ↦ htU fun i hiJ ↦ connectedComponentIn_subset _ _ (hf i (mem_union_left _ hiJ))⟩
  classical
  rw [← univ_pi_piecewise_univ]
  refine isPreconnected_univ_pi fun i ↦ ?_
  by_cases hi : i ∈ K
  · rw [piecewise_eq_of_mem _ _ _ hi]
    exact isPreconnected_connectedComponentIn
  · rw [piecewise_eq_of_notMem _ _ _ hi]
    have : PreconnectedSpace (X i) := not_not.mp (not_or.1 hi).2
    exact isPreconnected_univ

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

Goal state before:
pp: case refine_2.inr
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
hloc : ∀ (i : ι), LocallyConnectedSpace (X i)
hfin : {i | ¬PreconnectedSpace (X i)}.Finite
⊢ LocallyConnectedSpace ((i : ι) → X i)

Tactic:
· exact locallyConnectedSpace_of_finite_not_preconnectedSpace hfin

Goal state after:
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
⊢ IsPreconnected (f '' s)

Tactic:
by
  -- Unfold/destruct definitions in hypotheses
  rintro u v hu hv huv ⟨_, ⟨x, xs, rfl⟩, xu⟩ ⟨_, ⟨y, ys, rfl⟩, yv⟩
  rcases continuousOn_iff'.1 hf u hu with ⟨u', hu', u'_eq⟩
  rcases continuousOn_iff'.1 hf v hv with ⟨v', hv', v'_eq⟩
  -- Reformulate `huv : f '' s ⊆ u ∪ v` in terms of `u'` and `v'`
  replace huv : s ⊆ u' ∪ v' := by
    rw [image_subset_iff, preimage_union] at huv
    replace huv := subset_inter huv Subset.rfl
    rw [union_inter_distrib_right, u'_eq, v'_eq, ← union_inter_distrib_right] at huv
    exact (subset_inter_iff.1 huv).1
  -- Now `s ⊆ u' ∪ v'`, so we can apply `‹IsPreconnected s›`
  obtain ⟨z, hz⟩ : (s ∩ (u' ∩ v')).Nonempty := by
    refine H u' v' hu' hv' huv ⟨x, ?_⟩ ⟨y, ?_⟩ <;> rw [inter_comm]
    exacts [u'_eq ▸ ⟨xu, xs⟩, v'_eq ▸ ⟨yv, ys⟩]
  rw [← inter_self s, inter_assoc, inter_left_comm s u', ← inter_assoc, inter_comm s, inter_comm s,
    ← u'_eq, ← v'_eq] at hz
  exact ⟨f z, ⟨z, hz.1.2, rfl⟩, hz.1.1, hz.2.1⟩

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsLindelof s
hf : ContinuousOn f s
⊢ IsLindelof (f '' s)

Tactic:
intro l lne _ ls

Goal state after:
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsLindelof s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
inst✝ : CountableInterFilter l
ls : l ≤ 𝓟 (f '' s)
⊢ ∃ x ∈ f '' s, ClusterPt x l
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
huv : (∃ a ∈ s, a ∉ u) ∧ ∃ a ∈ s, a ∉ v
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
rcases huv with ⟨⟨x, hxs, hxu⟩, ⟨y, hys, hyv⟩⟩

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
x : α
hxs : x ∈ s
hxu : x ∉ u
y : α
hys : y ∈ s
hyv : y ∉ v
⊢ (s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set (Set X)
h : inst✝ = generateFrom s
h' : ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
a : X
t : Set X
ht : IsClosed[inst✝] tᶜ
ha : a ∉ tᶜ
⊢ Disjoint (𝓝ˢ tᶜ) (𝓝 a)

Tactic:
isClosed_compl_iff,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (Set X)
h : inst✝ = generateFrom s
h' : ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
a : X
t : Set X
ht : IsOpen[inst✝] t
ha : a ∉ tᶜ
⊢ Disjoint (𝓝ˢ tᶜ) (𝓝 a)
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hs : s ⊆ u ∪ v
huv : (∃ a ∈ s, a ∉ u) ∧ ∃ a ∈ s, a ∉ v
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
rcases huv with ⟨⟨x, hxs, hxu⟩, ⟨y, hys, hyv⟩⟩

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hs : s ⊆ u ∪ v
x : α
hxs : x ∈ s
hxu : x ∉ u
y : α
hys : y ∈ s
hyv : y ∉ v
⊢ (s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ sᶜ ∈ residual X ↔ ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S

Tactic:
mem_residual_iff,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ S, (∀ t ∈ S, IsOpen[inst✝] t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ⋂₀ S ⊆ sᶜ) ↔
    ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: case isNowhereDense
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
T : Set (Set X)
isNowhereDense : ∀ t ∈ T, IsNowhereDense t
countable : T.Countable
cover : s ⊆ ⋃₀ T
⊢ ∀ t ∈ image f '' T, IsNowhereDense t

pp: case cover
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
T : Set (Set X)
isNowhereDense : ∀ t ∈ T, IsNowhereDense t
countable : T.Countable
cover : s ⊆ ⋃₀ T
⊢ f '' s ⊆ ⋃₀ (image f '' T)

Tactic:
case isNowhereDense =>
    intro u ⟨t, tT, tu⟩
    rw [← tu]
    apply hf.isNowhereDense_image (isNowhereDense t tT)

Goal state after:
case cover
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
T : Set (Set X)
isNowhereDense : ∀ t ∈ T, IsNowhereDense t
countable : T.Countable
cover : s ⊆ ⋃₀ T
⊢ f '' s ⊆ ⋃₀ (image f '' T)
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
V : SetRel α α
h : V ∈ 𝓤 α
⊢ V.inv ∈ (comap Prod.swap (𝓤 α)).sets

Tactic:
exact preimage_mem_comap h

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
t : SetRel α α
ht : IsOpen[instTopologicalSpaceProd] t
hst : s ⊆ t
ht_comp : t ⊆ {p | ∃ x y, (p.1, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.2) ∈ s}
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d

Tactic:
have : s ⊆ interior d :=
        calc
          s ⊆ t := hst
          _ ⊆ interior d :=
            ht.subset_interior_iff.mpr fun x (hx : x ∈ t) =>
              let ⟨x, y, h₁, h₂, h₃⟩ := ht_comp hx
              hs_comp ⟨x, h₁, y, h₂, h₃⟩

Goal state after:
α : Type ua
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
t : SetRel α α
ht : IsOpen[instTopologicalSpaceProd] t
hst : s ⊆ t
ht_comp : t ⊆ {p | ∃ x y, (p.1, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.2) ∈ s}
this : s ⊆ interior d
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d
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 α
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
q : Filter ι'
q' : Filter α'
h : TendstoUniformlyOnFilter F f p p'
h' : TendstoUniformlyOnFilter F' f' q q'
⊢ TendstoUniformlyOnFilter (fun i ↦ Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ q) (p' ×ˢ q')

Tactic:
by
  rw [tendstoUniformlyOnFilter_iff_tendsto] at h h' ⊢
  rw [uniformity_prod_eq_comap_prod, tendsto_comap_iff, ← map_swap4_prod, tendsto_map'_iff]
  simpa using! h.prodMap h'

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
t : SetRel α α
ht : IsOpen[instTopologicalSpaceProd] t
hst : s ⊆ t
ht_comp : t ⊆ {p | ∃ x y, (p.1, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.2) ∈ s}
this : s ⊆ interior d
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d

Tactic:
have : interior d ∈ 𝓤 α := by filter_upwards [hs] using this

Goal state after:
α : Type ua
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
t : SetRel α α
ht : IsOpen[instTopologicalSpaceProd] t
hst : s ⊆ t
ht_comp : t ⊆ {p | ∃ x y, (p.1, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.2) ∈ s}
this✝ : s ⊆ interior d
this : interior d ∈ 𝓤 α
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
u : Set (β × β)
x✝ : u ∈ 𝓤 β
⊢ (fun q ↦ (f q.2, F q.1 q.2)) ⁻¹' u ∈ p ×ˢ 𝓟 {x} ↔ (fun x_1 ↦ (f x, F x_1 x)) ⁻¹' u ∈ p

Tactic:
by simp [preimage]

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

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : Subsingleton α
u : UniformSpace α
⊢ SetRel.id ∈ (fun u ↦ 𝓤 α) u

Tactic:
rw [SetRel.id, ← diagonal, diagonal_eq_univ]; exact univ_mem

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h : TendstoLocallyUniformlyOn F f p s
hc : ∃ᶠ (n : ι) in p, ContinuousOn (F n) s
⊢ ContinuousOn f s

Tactic:
by
  refine continuousOn_of_locally_uniform_approx_of_continuousWithinAt fun x hx u hu => ?_
  rcases h u hu x hx with ⟨t, ht, H⟩
  rcases (hc.and_eventually H).exists with ⟨n, hFc, hF⟩
  exact ⟨t, ht, ⟨F n, hFc.continuousWithinAt hx, hF⟩⟩

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

Goal state before:
pp: case hunion.inl
α : Type u_4
β : Type u_5
E : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
t t' : Set β
v : Set α
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u
v' : Set α
v'_mem : v' ∈ 𝓝[s] q
hv' : ∀ p ∈ v', ∀ x ∈ t', (f p x, f q x) ∈ u
p : α
hp : p ∈ v ∩ v'
x : β
h'x : x ∈ t
⊢ (f p x, f q x) ∈ u

Tactic:
exact hv p hp.1 x h'x

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:
simp_rw [UniformOnFun.uniformSpace, UniformFun.iInf_eq, UniformSpace.comap_iInf]
  rw [iInf_comm]
  exact iInf_congr fun s => iInf_comm

Goal state after:
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝¹ : Monoid α
inst✝ : MulAction α β
a b : α
f : Filter β
⊢ (a * b) • f = a • b • f

Tactic:
simp only [← Filter.map_smul, map_map, Function.comp_def, ← mul_smul]

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

Goal state before:
pp: case refine_1
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
⊢ ∃ V ∈ 𝓝 0, ∅ * V ⊆ U

Tactic:
exact ⟨univ, by 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
inst✝ : T1Space Y
⊢ (Continuous[inst✝², inst✝¹] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})) ↔
    Continuous[inst✝², inst✝¹] f ∧ IsClosedMap f ∧ ∀ (x : Y), (f ⁻¹' {x})ᶜ ∈ cocompact X

Tactic:
refine and_congr_right fun f_cont ↦ and_congr_right fun _ ↦
    ⟨fun H y ↦ (H y).compl_mem_cocompact, fun H y ↦ ?_⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : T1Space Y
f_cont : Continuous[inst✝², inst✝¹] f
x✝ : IsClosedMap f
H : ∀ (x : Y), (f ⁻¹' {x})ᶜ ∈ cocompact X
y : Y
⊢ IsCompact (f ⁻¹' {y})
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U ∈ 𝓝 1, x ∉ U
x y : G
hspec : x ⤳ y
hne : ¬x = y
U : Set G
hU₁ : U ∈ 𝓝 1
hU : x * y⁻¹ ∉ U
⊢ U ∈ 𝓝 (y * y⁻¹)

Tactic:
rwa [mul_inv_cancel]

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

Goal state before:
pp: G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
N : Subgroup G
inst✝ : N.Normal
n : G
hn : n ∈ N.topologicalClosure
g : G
⊢ MapsTo (fun h ↦ g * h * g⁻¹) ↑N ↑N

Tactic:
exact fun m hm => Subgroup.Normal.conj_mem inferInstance m hm g

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

Goal state before:
pp: G : Type w
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
x : G
⊢ comap (fun x_1 ↦ x_1 / x) (𝓝 1) = 𝓝 x

Tactic:
simpa only [div_eq_mul_inv] using nhds_translation_mul_inv x

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

Goal state before:
pp: case refine_1
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
⊢ ∃ V ∈ 𝓝 1, ∅ * V ⊆ U

Tactic:
exact ⟨univ, by simp⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
h : Tendsto f l atBot
⊢ Tendsto (fun x ↦ f x * r) l atBot ↔ 0 < r

Tactic:
by
  simp only [mul_comm _ r, tendsto_const_mul_atBot_iff_pos h]

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
V : Set Gᵐᵒᵖ
hV : V ∈ 𝓝 (op 1)
hV' : op '' K * V ⊆ op '' U
⊢ op ⁻¹' V * K ⊆ U

Tactic:
← image_preimage_eq V op_surjective,

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
V : Set Gᵐᵒᵖ
hV : V ∈ 𝓝 (op 1)
hV' : op '' K * op '' op ⁻¹' V ⊆ op '' U
⊢ op ⁻¹' V * K ⊆ U
Module: Mathlib.Topology.Algebra.Field

Goal state before:
pp: case inr
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : ContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : 2 * g y = 0
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ 2 * g x = 0

pp: α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : ContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : (-g) y = g y
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ x ∈ S

pp: α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : ContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : f y = g y
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ y ∈ S

Tactic:
mul_eq_zero,

Goal state after:
case inr
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : ContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : 2 = 0 ∨ g y = 0
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ 2 = 0 ∨ g x = 0

α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : ContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : (-g) y = g y
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ x ∈ S

α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : ContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : f y = g y
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ y ∈ S