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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst✝] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst✝] {x}) ↔ ∀ (x : X), IsOpen[inst✝] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst✝] {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:
tfae_have 5 ↔ 6 := by
    simp only [← subset_compl_singleton_iff, exists_mem_subset_iff]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst✝] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst✝] {x}) ↔ ∀ (x : X), IsOpen[inst✝] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst✝] {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
⊢ [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
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsCompact s
ht : IsCompact t
⊢ ⨆ x ∈ s, ⨆ x_2 ∈ t, 𝓝 x ⊓ 𝓝 x_2 ≤ ⨆ a ∈ s ∩ t, 𝓝 a

Tactic:
refine iSup₂_le fun x hxs ↦ iSup₂_le fun y hyt ↦ ?_

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsCompact s
ht : IsCompact t
x : X
hxs : x ∈ s
y : X
hyt : y ∈ t
⊢ 𝓝 x ⊓ 𝓝 y ≤ ⨆ a ∈ s ∩ t, 𝓝 a
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : Set X
⊢ IsOpen[inst✝²] U ↔ ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ ↑F

Tactic:
by
  rw [isOpen_iff_ultrafilter]
  refine ⟨fun h F hF => h F.lim hF F F.le_nhds_lim, ?_⟩
  intro cond x hx f h
  rw [← Ultrafilter.lim_eq_iff_le_nhds.2 h] at hx
  exact cond _ hx

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

Goal state before:
pp: case inl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
hs : ∅.Subsingleton
⊢ IsClosed[inst✝¹] ∅

pp: case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
hs : {x}.Subsingleton
⊢ IsClosed[inst✝¹] {x}

Tactic:
· exact isClosed_empty

Goal state after:
case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
hs : {x}.Subsingleton
⊢ IsClosed[inst✝¹] {x}
Module: Mathlib.Topology.Separation.Hausdorff

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

Tactic:
by
  constructor <;> intro H
  · exact ⟨H.isClosed, fun i ↦ H.image <| continuous_apply i⟩
  · 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
ι : Sort u_3
p : ι → Prop
s : ι → Set X
x : X
h : (𝓝 x).HasBasis p s
⊢ ⋂ i, ⋂ (_ : p i), s i = {x}

Tactic:
← h.ker,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
ι : Sort u_3
p : ι → Prop
s : ι → Set X
x : X
h : (𝓝 x).HasBasis p s
⊢ (𝓝 x).ker = {x}
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case insert
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
a✝¹ : X
s✝ : Finset X
a✝ : a✝¹ ∉ s✝
ih : Dense (s \ ↑s✝)
⊢ Dense (s \ ↑(insert a✝¹ s✝))

Tactic:
rw [Finset.coe_insert, ← union_singleton, ← sdiff_sdiff]
    exact ih.sdiff_singleton _

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

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

Tactic:
have := hI.to_subtype

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
ι : Type u_3
I : Set ι
s : ι → Set X
hI : I.Finite
hs : ∀ i ∈ I, IsDiscrete (s i)
hsc : ∀ i ∈ I, IsClosed[inst✝] (s i)
this : Finite ↑I
⊢ IsDiscrete (⋃ i ∈ I, s i)
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K : Set X
hK : IsCompact K
⊢ closure[inst✝¹] K = ⋃ x ∈ K, closure[inst✝¹] {x}

Tactic:
by
  simp only [hK.closure_eq_biUnion_inseparable, ← specializes_iff_inseparable,
    specializes_iff_mem_closure, ofPred_mem_eq]

Goal state after:
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
f : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝[>] a)
⊢ Tendsto (fun i ↦ max (f i) a) l (𝓝[>] a)

Tactic:
simp_rw [max_comm _ a]
  exact Filter.tendsto_nhds_max_right h

Goal state after:
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 : ι
hi : (s i).Nonempty
hj : (s j).Nonempty
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
⊢ False

Tactic:
let V : Set α := ⋃ k ∈ Sᶜ, s k

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 : ι
hi : (s i).Nonempty
hj : (s j).Nonempty
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
⊢ False
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝¹ : CountableInterFilter l✝
l : Filter β
inst✝ : CountableInterFilter l
f : α → β
⊢ CountableInterFilter (comap f l)

Tactic:
refine ⟨fun S hSc hS => ?_⟩

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝¹ : CountableInterFilter l✝
l : Filter β
inst✝ : CountableInterFilter l
f : α → β
S : Set (Set α)
hSc : S.Countable
hS : ∀ s ∈ S, s ∈ comap f l
⊢ ⋂₀ S ∈ comap f l
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝¹ : CountableInterFilter l✝
l : Filter α
inst✝ : CountableInterFilter l
f : α → β
⊢ CountableInterFilter (map f l)

Tactic:
refine ⟨fun S hSc hS => ?_⟩

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝¹ : CountableInterFilter l✝
l : Filter α
inst✝ : CountableInterFilter l
f : α → β
S : Set (Set β)
hSc : S.Countable
hS : ∀ s ∈ S, s ∈ map f l
⊢ ⋂₀ S ∈ map f l
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
⊢ CountableInterFilter (l₁ ⊓ l₂)

Tactic:
refine ⟨fun S hSc hS => ?_⟩

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
S : Set (Set α)
hSc : S.Countable
hS : ∀ s ∈ S, s ∈ l₁ ⊓ l₂
⊢ ⋂₀ S ∈ l₁ ⊓ l₂
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_1.inr.refine_1
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : β
hx : inr x ∈ s
h : s ⊆ range inr
⊢ IsConnected (inr ⁻¹' s)

pp: case refine_1.inr.refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : β
hx : inr x ∈ s
h : s ⊆ range inr
⊢ s = inr '' inr ⁻¹' s

Tactic:
· exact hs.preimage_of_isOpenMap Sum.inr_injective isOpenMap_inr h

Goal state after:
case refine_1.inr.refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : β
hx : inr x ∈ s
h : s ⊆ range inr
⊢ s = inr '' inr ⁻¹' s
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_1
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
⊢ (∃ t, IsConnected t ∧ s = inl '' t) ∨ ∃ t, IsConnected t ∧ s = inr '' t

Tactic:
obtain ⟨x | x, hx⟩ := hs.nonempty
    · have h : s ⊆ range Sum.inl :=
        hs.isPreconnected.subset_isClopen isClopen_range_inl ⟨.inl x, hx, x, rfl⟩
      refine Or.inl ⟨Sum.inl ⁻¹' s, ?_, ?_⟩
      · exact hs.preimage_of_isOpenMap Sum.inl_injective isOpenMap_inl h
      · exact (image_preimage_eq_of_subset h).symm
    · have h : s ⊆ range Sum.inr :=
        hs.isPreconnected.subset_isClopen isClopen_range_inr ⟨.inr x, hx, x, rfl⟩
      refine Or.inr ⟨Sum.inr ⁻¹' s, ?_, ?_⟩
      · exact hs.preimage_of_isOpenMap Sum.inr_injective isOpenMap_inr h
      · exact (image_preimage_eq_of_subset h).symm

Goal state after:
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 → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Set ↑s
htc : t.Countable
htsub : s ⊆ ⋃ x ∈ t, U ↑x
⊢ s ⊆ ⋃ x ∈ Subtype.val '' t, U x

Tactic:
have : ⋃ x ∈ t, U ↑x = ⋃ x ∈ Subtype.val '' t, U x := biUnion_image.symm
    rwa [← this]

Goal state after:
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 : IsOpen[generateFrom s] t
ha : a ∉ tᶜ
⊢ Disjoint (𝓝ˢ tᶜ) (𝓝 a)

Tactic:
Set.notMem_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[generateFrom s] t
ha : a ∈ t
⊢ Disjoint (𝓝ˢ tᶜ) (𝓝 a)
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case pos
α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
h✝ : x ∈ F
⊢ (Subtype.val '' connectedComponent ⟨x, h✝⟩).Nonempty ↔ x ∈ F

Tactic:
simp [connectedComponent_nonempty, *]

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

Goal state before:
pp: case neg
α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
h✝ : x ∉ F
⊢ ∅.Nonempty ↔ x ∈ F

Tactic:
simp [connectedComponent_nonempty, *]

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

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompletelyNormalSpace Y
e : X → Y
he : IsInducing e
s t : Set X
hd₁ : Disjoint (closure[inst✝²] s) t
hd₂ : Disjoint s (closure[inst✝²] t)
⊢ t ⊆ e ⁻¹' (closure[inst✝¹] (e '' s))ᶜ

Tactic:
preimage_compl,

Goal state after:
case refine_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompletelyNormalSpace Y
e : X → Y
he : IsInducing e
s t : Set X
hd₁ : Disjoint (closure[inst✝²] s) t
hd₂ : Disjoint s (closure[inst✝²] t)
⊢ t ⊆ (e ⁻¹' closure[inst✝¹] (e '' s))ᶜ
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompletelyNormalSpace Y
e : X → Y
he : IsInducing e
s t : Set X
hd₁ : Disjoint (closure[inst✝²] s) t
hd₂ : Disjoint s (closure[inst✝²] t)
⊢ s ⊆ e ⁻¹' (closure[inst✝¹] (e '' t))ᶜ

Tactic:
preimage_compl,

Goal state after:
case refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompletelyNormalSpace Y
e : X → Y
he : IsInducing e
s t : Set X
hd₁ : Disjoint (closure[inst✝²] s) t
hd₂ : Disjoint s (closure[inst✝²] t)
⊢ s ⊆ (e ⁻¹' closure[inst✝¹] (e '' t))ᶜ
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
i : α → β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
f : α → γ
di : IsDenseInducing i
hf : ∀ (b : β), ∃ c, Tendsto f (comap i (𝓝 b)) (𝓝 c)
a : α
b : γ
hb : Tendsto f (comap i (𝓝 (i a))) (𝓝 b)
⊢ di.extend f (i a) = f a

Tactic:
refine di.extend_eq_at' b ?_

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
i : α → β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
f : α → γ
di : IsDenseInducing i
hf : ∀ (b : β), ∃ c, Tendsto f (comap i (𝓝 b)) (𝓝 c)
a : α
b : γ
hb : Tendsto f (comap i (𝓝 (i a))) (𝓝 b)
⊢ Tendsto f (𝓝 a) (𝓝 b)
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
i : α → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := di.extend f
this : ∀ (b : β), (comap i (𝓝 b)).NeBot
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed[inst✝¹] V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
x : β
c : γ
hc : Tendsto f (comap i (𝓝 x)) (𝓝 c)
⊢ x ∈ V₁

Tactic:
← di.extend_eq_of_tendsto hc

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
i : α → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := di.extend f
this : ∀ (b : β), (comap i (𝓝 b)).NeBot
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed[inst✝¹] V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
x : β
c : γ
hc : Tendsto f (comap i (𝓝 x)) (𝓝 (di.extend f x))
⊢ x ∈ V₁
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
Sopen : ∀ t ∈ S, IsOpen[inst✝] t
Scount : S.Countable
T : Set (Set X)
Topen : ∀ t ∈ T, IsOpen[inst✝] t
Tcount : T.Countable
a b : Set X
ha : (a, b).1 ∈ S
hb : (a, b).2 ∈ T
⊢ IsOpen[inst✝] ((a, b).1 ∪ (a, b).2)

Tactic:
exact (Sopen a ha).union (Topen b hb)

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ S ⊆ {t | IsOpen[inst✝] t ∧ Dense t}, S.Countable ∧ ⋂₀ S ⊆ s) ↔
    ∃ S, (∀ t ∈ S, IsOpen[inst✝] t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ⋂₀ S ⊆ s

Tactic:
subset_def,

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed[inst✝] s ∧ interior s = ∅ ↔ IsOpen[inst✝] sᶜ ∧ Dense sᶜ

Tactic:
isOpen_compl_iff,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed[inst✝] s ∧ interior s = ∅ ↔ IsClosed[inst✝] s ∧ Dense sᶜ
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
F' : ι → α → β
hF : ∀ᶠ (x : ι) in p, ∀ (y : α), Inseparable (F x y) (F' x y)
⊢ TendstoUniformly F f p ↔ TendstoUniformly F' f p

Tactic:
by
  rw [← tendstoUniformlyOn_univ, ← tendstoUniformlyOn_univ]
  exact ⟨fun h => h.congr_inseparable (hF.mono fun _ hx y _ => hx y),
    fun h => h.congr_inseparable (hF.mono fun _ hx y _ => (hx y).symm)⟩

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

Goal state before:
pp: α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → SetRel α α
h : (𝓤 α).HasBasis p s
x : α
⊢ (comap (Prod.mk x) (𝓤 α)).HasBasis p fun i ↦ ball x (s i)

Tactic:
exact h.comap (Prod.mk x)

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

Goal state before:
pp: case succ
β : Type ub
inst✝ : UniformSpace β
T : β → β
h : UniformContinuous T
n : ℕ
hn : UniformContinuous T^[n]
⊢ UniformContinuous T^[n + 1]

Tactic:
| succ n hn =>

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

Goal state before:
pp: α : Type u
inst✝¹ : UniformSpace α
ι : Type u_1
inst✝ : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst✝¹.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst✝¹.toTopologicalSpace] t)
S : Bool → Set α := fun b ↦ Bool.casesOn b s t
U : (b : Bool) → ↑(S b) → ι
hU : ∀ (b : Bool) (x : ↑(S b)), Disjoint (ball (↑x) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
b : Bool
⊢ ⋃ x, ball (↑x) (B (U b x)) ∈ 𝓝ˢ (S b)

Tactic:
rw [mem_nhdsSet_iff_forall]

Goal state after:
α : Type u
inst✝¹ : UniformSpace α
ι : Type u_1
inst✝ : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst✝¹.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst✝¹.toTopologicalSpace] t)
S : Bool → Set α := fun b ↦ Bool.casesOn b s t
U : (b : Bool) → ↑(S b) → ι
hU : ∀ (b : Bool) (x : ↑(S b)), Disjoint (ball (↑x) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
b : Bool
⊢ ∀ x ∈ S b, ⋃ x, ball (↑x) (B (U b x)) ∈ 𝓝 x
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
⊢ (∀ (x y : α), (∀ r ∈ 𝓤 α, (x, y) ∈ r) → x = y) ↔ (𝓤 α).ker ⊆ diagonal α ∧ ∀ (x : α), (x, x) ∈ (𝓤 α).ker

Tactic:
subset_def,

Goal state after:
α : Type u
inst✝ : UniformSpace α
⊢ (∀ (x y : α), (∀ r ∈ 𝓤 α, (x, y) ∈ r) → x = y) ↔ (∀ x ∈ (𝓤 α).ker, x ∈ diagonal α) ∧ ∀ (x : α), (x, x) ∈ (𝓤 α).ker
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
ι : Type u_1
I : Set ι
hI : I.Finite
f : ι → Filter α
⊢ (⨆ i ∈ I, f i).TotallyBounded ↔ ∀ i ∈ I, (f i).TotallyBounded

Tactic:
have := hI.to_subtype

Goal state after:
α : Type u
uniformSpace : UniformSpace α
ι : Type u_1
I : Set ι
hI : I.Finite
f : ι → Filter α
this : Finite ↑I
⊢ (⨆ i ∈ I, f i).TotallyBounded ↔ ∀ i ∈ I, (f i).TotallyBounded
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
ι : Type u_1
I : Set ι
hI : I.Finite
s : ι → Set α
⊢ TotallyBounded (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, TotallyBounded (s i)

Tactic:
have := hI.to_subtype

Goal state after:
α : Type u
uniformSpace : UniformSpace α
ι : Type u_1
I : Set ι
hI : I.Finite
s : ι → Set α
this : Finite ↑I
⊢ TotallyBounded (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, TotallyBounded (s i)
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
x : α
p : Filter ι
hp : p.NeBot
hf : UniformCauchySeqOn F p s
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ (fun p ↦ (F p.1 x, F p.2 x)) ⁻¹' u ∈ p ×ˢ p

Tactic:
filter_upwards [hf u hu] with p hp using hp x hx

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

Goal state before:
pp: α : Type u_2
α' : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace α'
inst✝ : One β
f : α → β
hf : HasCompactMulSupport f
g : α' → α
hg : IsClosedEmbedding g
⊢ HasCompactMulSupport (f ∘ g)

Tactic:
rw [hasCompactMulSupport_def, Function.mulSupport_comp_eq_preimage]

Goal state after:
α : Type u_2
α' : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace α'
inst✝ : One β
f : α → β
hf : HasCompactMulSupport f
g : α' → α
hg : IsClosedEmbedding g
⊢ IsCompact (closure[inst✝¹] (g ⁻¹' mulSupport f))
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case refine_2
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
x : α
V : Set α
hxV : x ∈ V
hVo : IsOpen[uniformSpace.toTopologicalSpace] V
U : Set (α × α)
hU : U ∈ 𝓤 α
hUV : ball x U ⊆ V
⊢ ∃ v, (∃ i ∈ s, ∃ y, ball i (t y) = v) ∧ x ∈ v ∧ v ⊆ V

Tactic:
rcases comp_symm_of_uniformity hU with ⟨U', hU', _, hUU'⟩

Goal state after:
case refine_2
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
x : α
V : Set α
hxV : x ∈ V
hVo : IsOpen[uniformSpace.toTopologicalSpace] V
U : Set (α × α)
hU : U ∈ 𝓤 α
hUV : ball x U ⊆ V
U' : Set (α × α)
hU' : U' ∈ 𝓤 α
left✝ : ∀ {a b : α}, (a, b) ∈ U' → (b, a) ∈ U'
hUU' : U' ○ U' ⊆ U
⊢ ∃ v, (∃ i ∈ s, ∃ y, ball i (t y) = v) ∧ x ∈ v ∧ v ⊆ V
Module: Mathlib.Algebra.Order.Group.MinMax

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
⊢ max a⁻¹ 1 = a⁻¹ * max a 1

Tactic:
by
  rw [eq_inv_mul_iff_mul_eq, ← eq_div_iff_mul_eq', max_one_div_max_inv_one_eq_self]

Goal state after:
Module: Mathlib.Algebra.Order.Group.MinMax

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ max a b - max c d ≤ max |a - c| |b - d|

Tactic:
exact (max_sub_max_le_max _ _ _ _).trans (max_le_max (le_abs_self _) (le_abs_self _))

Goal state after:
Module: Mathlib.Algebra.Order.Group.MinMax

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ max c d - max a b ≤ max |c - a| |d - b|

Tactic:
exact (max_sub_max_le_max _ _ _ _).trans (max_le_max (le_abs_self _) (le_abs_self _))

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

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

Tactic:
change
      comap (Prod.map (Equiv.arrowProdEquivProdArrow _ _ _) (Equiv.arrowProdEquivProdArrow _ _ _))
          _ = _

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ comap
      (Prod.map ⇑(Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ)
        ⇑(Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ))
      (𝓤 ((α →ᵤ β) × (α →ᵤ γ))) =
    𝓤 (α →ᵤ β × γ)
Module: Mathlib.Topology.UniformSpace.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✝ : CompleteSpace β
⊢ CompleteSpace (α →ᵤ[𝔖] β)

Tactic:
rcases isEmpty_or_nonempty β

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : CompleteSpace β
h✝ : IsEmpty β
⊢ CompleteSpace (α →ᵤ[𝔖] β)

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : CompleteSpace β
h✝ : Nonempty β
⊢ CompleteSpace (α →ᵤ[𝔖] β)