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

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

Tactic:
rw [Set.sUnion_eq_biUnion, isOpen_compl_iff]

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

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space Y
y : Y
s : Set X
x✝ : IsClosed[inst✝²] s
h2s : s.Nonempty
⊢ IsClosed[inst✝¹] ((fun a ↦ y) '' s)

Tactic:
h2s.image_const,

Goal state after:
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space Y
y : Y
s : Set X
x✝ : IsClosed[inst✝²] s
h2s : s.Nonempty
⊢ IsClosed[inst✝¹] {y}
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
s : Set X
hxy : x ≠ y
t : Set X
ht : t ∈ 𝓝[s] x
⊢ t ∈ 𝓝[insert y s] x

Tactic:
obtain ⟨o, ho, hxo, host⟩ := mem_nhdsWithin.mp ht

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
s : Set X
hxy : x ≠ y
t : Set X
ht : t ∈ 𝓝[s] x
o : Set X
ho : IsOpen[inst✝¹] o
hxo : x ∈ o
host : o ∩ s ⊆ t
⊢ t ∈ 𝓝[insert y s] x
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
⊢ cofinite ≤ codiscrete X

Tactic:
by
  simpa using! isCompact_univ.cofinite_inf_le_codiscreteWithin

Goal state after:
Module: Mathlib.Topology.Clopen

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hab : Disjoint a b
this : IsClosed[inst✝] (s ∩ bᶜ)
⊢ s ∩ a = s ∩ bᶜ

Tactic:
refine (inter_subset_inter_right s hab.subset_compl_right).antisymm ?_

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hab : Disjoint a b
this : IsClosed[inst✝] (s ∩ bᶜ)
⊢ s ∩ bᶜ ⊆ s ∩ a
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
x : (i : ι) → X i
U : Set ((i : ι) → X i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htU : J.pi t ⊆ U
K : Set ι := J ∪ {i | ¬PreconnectedSpace (X i)}
⊢ IsPreconnected (K.pi fun i ↦ connectedComponentIn (t i) (x i))

Tactic:
← univ_pi_piecewise_univ

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyConnectedSpace (X i)
hfinite : {i | ¬PreconnectedSpace (X i)}.Finite
x : (i : ι) → X i
U : Set ((i : ι) → X i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htU : J.pi t ⊆ U
K : Set ι := J ∪ {i | ¬PreconnectedSpace (X i)}
⊢ IsPreconnected (univ.pi (K.piecewise (fun i ↦ connectedComponentIn (t i) (x i)) fun x ↦ univ))
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
s : ι → Set α
hs : IsPreconnected (⋃ n, s n)
hs' : ∀ (i : ι), IsOpen[inst✝] (s i)
i j : ι
hij : ¬TransGen (fun a b ↦ (s a ∩ s b).Nonempty) i j
S : Set ι := {k | TransGen (fun a b ↦ (s a ∩ s b).Nonempty) i k}
U : Set α := ⋃ k ∈ S, s k
V : Set α := ⋃ k ∈ Sᶜ, s k
hsplit : ⋃ n, s n = U ∪ V
a : α
ha : a ∈ s i
b : α
hb : b ∈ s j
hi_S : i ∈ S := TransGen.single (Exists.intro a ⟨ha, ha⟩)
hUne : ((⋃ n, s n) ∩ U).Nonempty
hVne : ((⋃ n, s n) ∩ V).Nonempty
x : α
hxV : ∃ i ∉ S, x ∈ s i
k : ι
hk : k ∈ S
hxk : x ∈ s k
⊢ False

Tactic:
obtain ⟨l, hl, hxl⟩ := hxV

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
s : ι → Set α
hs : IsPreconnected (⋃ n, s n)
hs' : ∀ (i : ι), IsOpen[inst✝] (s i)
i j : ι
hij : ¬TransGen (fun a b ↦ (s a ∩ s b).Nonempty) i j
S : Set ι := {k | TransGen (fun a b ↦ (s a ∩ s b).Nonempty) i k}
U : Set α := ⋃ k ∈ S, s k
V : Set α := ⋃ k ∈ Sᶜ, s k
hsplit : ⋃ n, s n = U ∪ V
a : α
ha : a ∈ s i
b : α
hb : b ∈ s j
hi_S : i ∈ S := TransGen.single (Exists.intro a ⟨ha, ha⟩)
hUne : ((⋃ n, s n) ∩ U).Nonempty
hVne : ((⋃ n, s n) ∩ V).Nonempty
x : α
k : ι
hk : k ∈ S
hxk : x ∈ s k
l : ι
hl : l ∉ S
hxl : x ∈ s l
⊢ False
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
⊢ IsPreconnected s →
    ∀ (t t' : Set α),
      IsClosed[inst✝] t →
        IsClosed[inst✝] t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty

Tactic:
rintro h t t' ht ht' htt' ⟨x, xs, xt⟩ ⟨y, ys, yt'⟩
      rw [← not_disjoint_iff_nonempty_inter, ← subset_compl_iff_disjoint_right, compl_inter]
      intro h'
      have xt' : x ∉ t' := (h' xs).resolve_left (absurd xt)
      have yt : y ∉ t := (h' ys).resolve_right (absurd yt')
      have := h _ _ ht.isOpen_compl ht'.isOpen_compl h' ⟨y, ys, yt⟩ ⟨x, xs, xt'⟩
      rw [← compl_union] at this
      exact this.ne_empty htt'.disjoint_compl_right.inter_eq

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
l : Filter Y
lne : l.NeBot
inst✝ : CountableInterFilter l
ls : l ≤ 𝓟 (f '' s)
this✝ : (comap f l ⊓ 𝓟 s).NeBot
x : X
hxs : x ∈ s
hx : ClusterPt x (comap f l ⊓ 𝓟 s)
this : (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot
⊢ Tendsto f (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)) (𝓝 (f x) ⊓ l)

Tactic:
convert! (hf x hxs).inf (@tendsto_comap _ _ f l) using 1

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)
this✝ : (comap f l ⊓ 𝓟 s).NeBot
x : X
hxs : x ∈ s
hx : ClusterPt x (comap f l ⊓ 𝓟 s)
this : (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot
⊢ 𝓝 x ⊓ (comap f l ⊓ 𝓟 s) = 𝓝[s] x ⊓ comap f l
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: case right
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs✝ : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
r : Set ↑s
hr : r.Countable
hs : s ⊆ ⋃ i ∈ r, interior (U ↑i ⋯)
i : ↑s
hi : i ∈ r
⊢ interior (U ↑i ⋯) ⊆ ⋃ x ∈ r, U ↑x ⋯

Tactic:
apply Subset.trans interior_subset

Goal state after:
case right
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs✝ : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
r : Set ↑s
hr : r.Countable
hs : s ⊆ ⋃ i ∈ r, interior (U ↑i ⋯)
i : ↑s
hi : i ∈ r
⊢ U ↑i ⋯ ⊆ ⋃ x ∈ r, U ↑x ⋯
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
s : Set α
a : α
di : IsDenseInducing i
hs : ∃ i_1, (i a ∈ i_1 ∧ IsOpen[inst✝] i_1) ∧ i ⁻¹' i_1 ⊆ s
⊢ closure[inst✝] (i '' s) ∈ 𝓝 (i a)

Tactic:
rcases hs with ⟨U, ⟨haU, hUo⟩, sub : i ⁻¹' U ⊆ s⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
s : Set α
a : α
di : IsDenseInducing i
U : Set β
sub : i ⁻¹' U ⊆ s
haU : i a ∈ U
hUo : IsOpen[inst✝] U
⊢ closure[inst✝] (i '' s) ∈ 𝓝 (i a)
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsSigmaCompact s
⊢ IsLindelof s

Tactic:
IsSigmaCompact

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : ∃ K, (∀ (n : ℕ), IsCompact (K n)) ∧ ⋃ n, K n = s
⊢ IsLindelof s
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : HereditarilyLindelofSpace X
ι : Type u_2
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst✝¹] (C i)
t : Set ι
| ⋂ i ∈ t, C i = ⋂ i, C i

Tactic:
rw [← compl_inj_iff]; simp

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : HereditarilyLindelofSpace X
ι : Type u_2
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst✝¹] (C i)
t : Set ι
| ⋃ i ∈ t, (C i)ᶜ = ⋃ i, (C i)ᶜ
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : HereditarilyLindelofSpace X
ι : Type u_2
inst✝ : Nonempty ι
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst✝²] (C i)
k : ℕ → ι
| ⋂ n, C (k n) = ⋂ i, C i

Tactic:
rw [← compl_inj_iff]; simp

Goal state after:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : HereditarilyLindelofSpace X
ι : Type u_2
inst✝ : Nonempty ι
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst✝²] (C i)
k : ℕ → ι
| ⋃ i, (C (k i))ᶜ = ⋃ i, (C i)ᶜ
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
⊢ IsGδ (s ∩ t)

Tactic:
inter_eq_iInter

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
⊢ IsGδ (⋂ b, bif b then s else t)
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
h : IsMeagre s
⊢ IsMeagre (f '' s)

Tactic:
rw [isMeagre_iff_countable_union_isNowhereDense] at *
  obtain ⟨T, isNowhereDense, countable, cover⟩ := h
  refine ⟨(Set.image f) '' T, ?isNowhereDense, countable.image _, ?cover⟩
  case isNowhereDense =>
    intro u ⟨t, tT, tu⟩
    rw [← tu]
    apply hf.isNowhereDense_image (isNowhereDense t tT)
  case cover =>
    rw [← Set.image_sUnion]
    grw [cover]

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
Y : Type u_4
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsOpenQuotientMap f
⊢ ∀ (f : ℕ → Set Y), (∀ (n : ℕ), IsOpen[inst✝] (f n)) → (∀ (n : ℕ), Dense (f n)) → Dense (⋂ n, f n)

Tactic:
intro u hou hdu

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
Y : Type u_4
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsOpenQuotientMap f
u : ℕ → Set Y
hou : ∀ (n : ℕ), IsOpen[inst✝] (u n)
hdu : ∀ (n : ℕ), Dense (u n)
⊢ Dense (⋂ n, u n)
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
hsc : Dense s
htc : Dense t
⊢ Dense (s ∩ t)

Tactic:
inter_eq_iInter

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
hsc : Dense s
htc : Dense t
⊢ Dense (⋂ b, bif b then s else t)
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
⊢ map (⇑h) (cocompact X) = cocompact Y

Tactic:
← h.comap_cocompact,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
⊢ map (⇑h) (comap (⇑h) (cocompact Y)) = cocompact Y
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
f : Filter α
m : α → β
hf : Cauchy f
s : Set α
hm : UniformContinuousOn m s
hfs : f ≤ 𝓟 s
⊢ Cauchy (map m f)

Tactic:
by
  suffices Cauchy (comap (Subtype.val : s → α) f) by
    simpa [Set.domRestrict_def, ← Function.comp_def, ← map_map,
      subtype_coe_map_comap, inf_eq_left.mpr hfs] using this.map hm.restrict
  exact hf.comap' (fun _ x ↦ x) (comap_coe_neBot_of_le_principal (h := hf.1) hfs)

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
n : ℕ
⊢ ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun x ↦ t ○ x)^[n] t ⊆ s

Tactic:
induction n generalizing s with
  | zero => simpa
  | succ _ ihn =>
    rcases comp_mem_uniformity_sets hs with ⟨t, htU, hts⟩
    refine (ihn htU).mono fun U hU => ?_
    rw [Function.iterate_succ_apply']
    have := isRefl_of_mem_uniformity htU
    exact ⟨hU.1.trans <| SetRel.left_subset_comp.trans hts,
     (SetRel.comp_subset_comp hU.1 hU.2).trans hts⟩

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
s : Set α
x : α
⊢ x ∈ closure[inst✝.toTopologicalSpace] s ↔ ∀ {V : Set (α × α)}, V ∈ 𝓤 α → SetRel.IsSymm V → (s ∩ ball x V).Nonempty

Tactic:
by
  simp [mem_closure_iff_nhds_basis (hasBasis_nhds x), Set.Nonempty]

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
a b : α
⊢ 𝓝 a ×ˢ 𝓝 b = (𝓤 α).lift fun s ↦ (𝓤 α).lift' fun t ↦ {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t}

Tactic:
by
  rw [nhds_eq_uniformity', nhds_eq_uniformity, prod_lift'_lift']
  exacts [rfl, monotone_preimage, monotone_preimage]

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
⊢ (𝓤 α).HasBasis (fun V ↦ V ∈ 𝓤 α ∧ IsClosed[instTopologicalSpaceProd] V) id

Tactic:
by
  refine Filter.hasBasis_self.2 fun t h => ?_
  rcases comp_comp_symm_mem_uniformity_sets h with ⟨w, w_in, w_symm, r⟩
  refine ⟨closure w, mem_of_superset w_in subset_closure, isClosed_closure, ?_⟩
  refine Subset.trans ?_ r
  rw [closure_eq_uniformity]
  apply iInter_subset_of_subset
  apply iInter_subset
  exact ⟨w_in, w_symm⟩

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

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : DiscreteUniformity α
f : Filter α
hf : Cauchy f
⊢ ∃ x, f ≤ 𝓝 x

Tactic:
obtain ⟨x, rfl⟩ := eq_pure_of_cauchy hf
    exact ⟨x, pure_le_nhds x⟩

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
⊢ Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (s ×ˢ s)) (𝓤 β) ↔
    Tendsto (fun x ↦ (s.domRestrict f x.1, s.domRestrict f x.2)) (𝓤 ↑s) (𝓤 β)

Tactic:
rw [← map_uniformity_set_coe, tendsto_map'_iff]

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
⊢ Tendsto ((fun x ↦ (f x.1, f x.2)) ∘ Prod.map Subtype.val Subtype.val) (𝓤 ↑s) (𝓤 β) ↔
    Tendsto (fun x ↦ (s.domRestrict f x.1, s.domRestrict f x.2)) (𝓤 ↑s) (𝓤 β)
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
⊢ ∃ x, f ≤ 𝓝 x

Tactic:
have := hf.1
    simp_rw [cauchy_pi_iff', cauchy_iff_exists_le_nhds] at hf
    choose x hx using hf
    use x
    rwa [nhds_pi, le_pi]

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
hs : ∀ U ∈ 𝓤 α, ∃ t, t.Countable ∧ ⋃ x ∈ t, ball x U = univ
⊢ SecondCountableTopology α

Tactic:
suffices SeparableSpace α from UniformSpace.secondCountable_of_separable α
  have : ∀ U ∈ 𝓤 α, ∃ t : Set α, Set.Countable t ∧ univ ⊆ ⋃ x ∈ t, ball x U := by
    simpa only [univ_subset_iff] using hs
  rcases subset_countable_closure_of_almost_dense_set (univ : Set α) this with ⟨t, -, htc, ht⟩
  exact ⟨⟨t, htc, fun x => ht (mem_univ x)⟩⟩

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

Goal state before:
pp: α : Type u_1
γ : Type u_3
u₁ u₂ : UniformSpace γ
i : Bool
⊢ uniformSpace α γ = bif i then uniformSpace α γ else uniformSpace α γ

Tactic:
cases i <;> rfl

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝² : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
t : ι → Set α
V : ι → Set (β × β)
ht : ∀ (n : ι), t n ∈ 𝔖
hmono : Monotone t
hex : ∀ s ∈ 𝔖, ∃ n, s ⊆ t n
hb : (𝓤 β).HasAntitoneBasis V
this : Nonempty ι
⊢ Antitone fun n ↦ UniformOnFun.gen 𝔖 (t n) (V n)

Tactic:
· exact fun k l h ↦ UniformOnFun.gen_mono (hmono h) (hb.2 h)

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 α
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set X
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → X → α
S : Set X
x₀ : X
hX : (𝓝[S] x₀).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ EquicontinuousWithinAt F S x₀ ↔ ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂

Tactic:
rw [equicontinuousWithinAt_iff_continuousWithinAt, ContinuousWithinAt,
    hX.tendsto_iff (UniformFun.hasBasis_nhds_of_basis ι α _ hα)]
  rfl

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (α × α)
F : ι → β → α
hα : (𝓤 α).HasBasis p s
⊢ UniformEquicontinuous F ↔ ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β, ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k

Tactic:
by
  rw [uniformEquicontinuous_iff_uniformContinuous, UniformContinuous,
    (UniformFun.hasBasis_uniformity_of_basis ι α hα).tendsto_right_iff]
  rfl

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

Goal state before:
pp: α : Type u_1
γ : Type u_3
𝔖 : Set (Set α)
u₁ u₂ : UniformSpace γ
i : Bool
⊢ uniformSpace α γ 𝔖 = bif i then uniformSpace α γ 𝔖 else uniformSpace α γ 𝔖

Tactic:
cases i <;> rfl

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
hb : a ≠ 0
U V : Set α
hU : U ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}
hV : V = (fun x ↦ a * x) ⁻¹' U
⊢ V ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}

Tactic:
obtain ⟨aU, (haU | haU)⟩ := hU <;>
  simp only [hV, haU, mem_ofPred_eq] <;>
  use a⁻¹ * aU <;>
  rcases lt_or_gt_of_ne hb with (hb | hb)

Goal state after:
case h.inl
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
hb✝ : a ≠ 0
U V : Set α
hV : V = (fun x ↦ a * x) ⁻¹' U
aU : α
haU : U = Ioi aU
hb : a < 0
⊢ (fun x ↦ a * x) ⁻¹' Ioi aU = Ioi (a⁻¹ * aU) ∨ (fun x ↦ a * x) ⁻¹' Ioi aU = Iio (a⁻¹ * aU)

case h.inr
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
hb✝ : a ≠ 0
U V : Set α
hV : V = (fun x ↦ a * x) ⁻¹' U
aU : α
haU : U = Ioi aU
hb : 0 < a
⊢ (fun x ↦ a * x) ⁻¹' Ioi aU = Ioi (a⁻¹ * aU) ∨ (fun x ↦ a * x) ⁻¹' Ioi aU = Iio (a⁻¹ * aU)

case h.inl
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
hb✝ : a ≠ 0
U V : Set α
hV : V = (fun x ↦ a * x) ⁻¹' U
aU : α
haU : U = Iio aU
hb : a < 0
⊢ (fun x ↦ a * x) ⁻¹' Iio aU = Ioi (a⁻¹ * aU) ∨ (fun x ↦ a * x) ⁻¹' Iio aU = Iio (a⁻¹ * aU)

case h.inr
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
hb✝ : a ≠ 0
U V : Set α
hV : V = (fun x ↦ a * x) ⁻¹' U
aU : α
haU : U = Iio aU
hb : 0 < a
⊢ (fun x ↦ a * x) ⁻¹' Iio aU = Ioi (a⁻¹ * aU) ∨ (fun x ↦ a * x) ⁻¹' Iio aU = Iio (a⁻¹ * aU)
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
X : Type u_5
inst✝¹ : TopologicalSpace X
M : Type u_6
inst✝ : One M
f : ι → X → M
hf : LocallyFinite fun i ↦ mulSupport (f i)
x₀ : X
U : Set X
hxU : U ∈ 𝓝 x₀
hUf : {i | ((fun i ↦ mulSupport (f i)) i ∩ U).Nonempty}.Finite
y : X
hy : y ∈ U
i : ι
hi : i ∈ mulSupport fun i ↦ f i y
⊢ i ∈ ↑hUf.toFinset

Tactic:
hUf.coe_toFinset

Goal state after:
ι : Type u_1
X : Type u_5
inst✝¹ : TopologicalSpace X
M : Type u_6
inst✝ : One M
f : ι → X → M
hf : LocallyFinite fun i ↦ mulSupport (f i)
x₀ : X
U : Set X
hxU : U ∈ 𝓝 x₀
hUf : {i | ((fun i ↦ mulSupport (f i)) i ∩ U).Nonempty}.Finite
y : X
hy : y ∈ U
i : ι
hi : i ∈ mulSupport fun i ↦ f i y
⊢ i ∈ {i | ((fun i ↦ mulSupport (f i)) i ∩ U).Nonempty}
Module: Mathlib.Topology.Algebra.Group.Quotient

Goal state before:
pp: G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
H : Subgroup G
hH : IsCompact ↑H
⊢ IsClosedMap mk

Tactic:
intro t ht
  rw [← (isQuotientMap_mk H).isClosed_preimage, preimage_image_mk_eq_mul]
  exact ht.mul_right_of_isCompact hH

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
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : (𝓝 1).HasBasis (fun x ↦ True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
n j k : ℕ
h : ∀ (a b : G), a ∈ u j → b ∈ u k → a * b ∈ u n
m : ℕ
hm : m ∈ Ici (max j k)
⊢ u m * u m ⊆ u n

Tactic:
rintro - ⟨a, ha, b, hb, rfl⟩

Goal state after:
G : Type w
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : (𝓝 1).HasBasis (fun x ↦ True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
n j k : ℕ
h : ∀ (a b : G), a ∈ u j → b ∈ u k → a * b ∈ u n
m : ℕ
hm : m ∈ Ici (max j k)
a : G
ha : a ∈ u m
b : G
hb : b ∈ u m
⊢ (fun x1 x2 ↦ x1 * x2) a b ∈ u n
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 : α
hr : r < 0
⊢ Tendsto (fun x ↦ r * f x) l atBot ↔ Tendsto f l atTop

Tactic:
simpa only [neg_mul, tendsto_neg_atTop_iff] using tendsto_const_mul_atTop_of_pos (neg_pos.2 hr)

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 atTop ↔ r < 0

Tactic:
simp only [mul_comm _ r, tendsto_const_mul_atTop_iff_neg h]

Goal state after:
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
hxa : x ≤ a
hay : a ≤ y
ha' : ∃ x, ¬(x' x < a x ∧ a x < y' x)
⊢ a ∈ (⋃ i, Icc x (update y i (x' i))) ∪ ⋃ i, Icc (update x i (y' i)) y

Tactic:
simp only [le_update_iff, update_le_iff, mem_union, mem_iUnion, mem_Icc,
    hxa, hay _, hxa _, hay, ← exists_or]

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
hxa : x ≤ a
hay : a ≤ y
ha' : ∃ x, ¬(x' x < a x ∧ a x < y' x)
⊢ ∃ x, (True ∧ a x ≤ x' x ∧ ∀ (j : ι), j ≠ x → True) ∨ (y' x ≤ a x ∧ ∀ (j : ι), j ≠ x → True) ∧ True
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst✝ : Preorder α
t : OrderTopology α
⊢ OrderTopology αᵒᵈ

Tactic:
by
  constructor
  rcases t.topology_eq_generate_intervals with rfl
  simp_rw [Preorder.topology, or_comm]
  rfl

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : β
⊢ ↑e.symm x = ↑e'.symm x

Tactic:
apply h.symm'.2

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : β
⊢ x ∈ e.symm.source
Module: Mathlib.Algebra.Category.Grp.Images

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
this : Mono F'.m
⊢ (ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x ↦ (Hom.hom f) x = ↑0) ⋯) = 0

Tactic:
apply injective_of_mono F'.m

Goal state after:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
this : Mono F'.m
⊢ (ConcreteCategory.hom F'.m)
      ((ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x ↦ (Hom.hom f) x = ↑0) ⋯)) =
    (ConcreteCategory.hom F'.m) 0