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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
y : β
hg : ContinuousWithinAt g t y
hf : ContinuousWithinAt f s x
h : MapsTo f s t
hy : f x = y
⊢ ContinuousWithinAt (g ∘ f) s x

Tactic:
subst hy; exact hg.comp hf h

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
hf : ContinuousWithinAt f s x
hg : ContinuousWithinAt g t (f x)
hs : t ∈ 𝓝[f '' s] f x
⊢ ContinuousWithinAt (g ∘ f) s x

Tactic:
exact hg.comp_of_mem_nhdsWithin_image hf hs

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case h
α : Type u
t✝ : TopologicalSpace α
a : α
s✝ : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
s : Set α
hs₁ : a ∈ s
hs₂ : s ∈ b
t : Set α
ht₁ : a ∈ t
ht₂ : t ∈ b
u : Set α
hu₁ : u ∈ b
hu₂ : a ∈ u
hu₃ : u ⊆ s ∩ t
⊢ ∃ z ∈ {s | a ∈ s ∧ s ∈ b}, (𝓟 ⁻¹'o fun x1 x2 ↦ x1 ≥ x2) s z ∧ (𝓟 ⁻¹'o fun x1 x2 ↦ x1 ≥ x2) t z

Tactic:
exact ⟨u, ⟨hu₂, hu₁⟩, le_principal_iff.2 (hu₃.trans inter_subset_left),
      le_principal_iff.2 (hu₃.trans inter_subset_right)⟩

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s : Set α
t : Set β
hs : IsSeparable s
ht : IsSeparable t
⊢ IsSeparable (s ×ˢ t)

Tactic:
by
  rcases hs with ⟨cs, cs_count, hcs⟩
  rcases ht with ⟨ct, ct_count, hct⟩
  refine ⟨cs ×ˢ ct, cs_count.prod ct_count, ?_⟩
  rw [closure_prod_eq]
  gcongr

Goal state after:
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
f : Filter α
s : Set α
H : ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g
hf : s ∉ f
⊢ False

Tactic:
set g : Filter (sᶜ : Set α) := comap (↑) f

Goal state after:
α : Type u
f : Filter α
s : Set α
H : ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g
hf : s ∉ f
g : Filter ↑sᶜ := comap Subtype.val f
⊢ False
Module: Mathlib.Topology.Ultrafilter

Goal state before:
pp: X : Type u
x : X
s : Set X
inst✝ : TopologicalSpace X
⊢ x ∈ closure[inst✝] s ↔ ∃ u, s ∈ u ∧ ↑u ≤ 𝓝 x

Tactic:
by
  simp [closure_eq_cluster_pts, ClusterPt, ← exists_ultrafilter_iff, and_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter β
f : α → β
⊢ (comap f l).smallSets = comap (image f) l.smallSets

Tactic:
by
  refine (gc_map_comap _).u_comm_of_l_comm (gc_map_comap _) bind_smallSets_gc bind_smallSets_gc ?_
  simp [Function.comp_def, map_bind, bind_map]

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

Goal state before:
pp: X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
s : Set X
f : ι → Set X
hs : IsCompact s
U : X → Set X
hxU : ∀ (x : X), U x ∈ nhds x
hUf : ∀ (x : X), {i | (f i ∩ U x).Nonempty}.Finite
t : Finset X
hsU : s ⊆ ⋃ x ∈ t, U x
i : ι
x : X
hx : x ∈ f i ∩ s
⊢ i ∈ ⋃ i ∈ ↑t, {i_1 | (f i_1 ∩ U i).Nonempty}

Tactic:
rcases mem_iUnion₂.1 (hsU hx.2) with ⟨c, hct, hcx⟩

Goal state after:
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
s : Set X
f : ι → Set X
hs : IsCompact s
U : X → Set X
hxU : ∀ (x : X), U x ∈ nhds x
hUf : ∀ (x : X), {i | (f i ∩ U x).Nonempty}.Finite
t : Finset X
hsU : s ⊆ ⋃ x ∈ t, U x
i : ι
x : X
hx : x ∈ f i ∩ s
c : X
hct : c ∈ t
hcx : x ∈ U c
⊢ i ∈ ⋃ i ∈ ↑t, {i_1 | (f i_1 ∩ U i).Nonempty}
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
x : X
⊢ x ∈ K (K.find x)

Tactic:
exact Nat.find_spec (K.exists_mem x)

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
⊢ ∃ t, (∀ x ∈ t, x ∈ s) ∧ ⋃ x ∈ t, U x ∈ 𝓝ˢ s

Tactic:
by
  let ⟨t, ht⟩ := hs.elim_nhds_subcover_nhdsSet' (fun x _ => U x) hU
  classical
  exact ⟨t.image (↑), fun x hx =>
    let ⟨y, _, hyx⟩ := Finset.mem_image.1 hx
    hyx ▸ y.2,
    by rwa [Finset.set_biUnion_finset_image]⟩

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed[inst✝] (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, s ∩ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝] (U i)
hsU : s ⊆ ⋃ i, U i
⊢ ∃ t, s ⊆ ⋃ i ∈ t, U i

Tactic:
← disjoint_compl_right_iff_subset,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed[inst✝] (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, s ∩ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝] (U i)
hsU : Disjoint s (⋃ i, U i)ᶜ
⊢ ∃ t, s ⊆ ⋃ i ∈ t, U i
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed[inst✝] (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, s ∩ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝] (U i)
hsU : s ⊓ ⋂ i, (U i)ᶜ = ⊥
t : Finset ι✝
ht : s ∩ ⋂ i ∈ t, (U i)ᶜ = ∅
⊢ s ⊆ ⋃ i ∈ t, U i

Tactic:
← disjoint_compl_right_iff_subset,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed[inst✝] (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, s ∩ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝] (U i)
hsU : s ⊓ ⋂ i, (U i)ᶜ = ⊥
t : Finset ι✝
ht : s ∩ ⋂ i ∈ t, (U i)ᶜ = ∅
⊢ Disjoint s (⋃ i ∈ t, U i)ᶜ
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
s : Set X
h : ∀ P ⊆ S, s ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ s ⊆ ⋃₀ Q
F : Ultrafilter X
⊢ s ∈ F → ∃ x ∈ s, ↑F ≤ 𝓝 x

Tactic:
hsF

Goal state after:
X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
s : Set X
h : ∀ P ⊆ S, s ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ s ⊆ ⋃₀ Q
F : Ultrafilter X
hsF : s ∈ F
⊢ ∃ x ∈ s, ↑F ≤ 𝓝 x
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α ≃o β
⊢ upperClosure (⇑f '' s) = (UpperSet.map f) (upperClosure s)

Tactic:
rw [← f.symm_symm, ← UpperSet.symm_map, f.symm_symm]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α ≃o β
⊢ upperClosure (⇑f '' s) = (UpperSet.map f.symm).symm (upperClosure s)
Module: Mathlib.Order.UpperLower.CompleteLattice

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : LE α
a : α
f : ι → UpperSet α
⊢ a ∈ ⋂ i, ↑(f i) ↔ ∀ (i : ι), a ∈ f i

Tactic:
exact mem_iInter

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s s' : Set X
hs : IsCompact s
t : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : n ∈ 𝓝ˢ[s' ×ˢ t] (s ×ˢ t)
⊢ ∃ u ∈ 𝓝ˢ[s'] s, u ×ˢ t ⊆ n

Tactic:
rw [hs.nhdsSetWithin_prod_eq ht, nhdsSetWithin_self, Filter.mem_prod_principal] at hn
  exact ⟨_, hn, fun x hx ↦ hx.1 _ hx.2⟩

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

Goal state before:
pp: X : Type u
Y : Type v
ι : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s t : Set X
f : X → Y
inst✝ : NoncompactSpace X
i✝ : Set X
hs : i✝ = univ
⊢ ¬IsCompact i✝

Tactic:
rw [hs]

Goal state after:
X : Type u
Y : Type v
ι : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s t : Set X
f : X → Y
inst✝ : NoncompactSpace X
i✝ : Set X
hs : i✝ = univ
⊢ ¬IsCompact univ
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
ι : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
s t : Set X
f : X → Y
inst✝¹ : CompactSpace X
inst✝ : CompactSpace Y
⊢ IsCompact univ

Tactic:
rw [← univ_prod_univ]; exact isCompact_univ.prod isCompact_univ

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : X → Y
h : ∀ (x : X), f x ~ᵢ g x
⊢ Continuous[inst✝¹, inst✝] f ↔ Continuous[inst✝¹, inst✝] g

Tactic:
simp_rw [SeparationQuotient.isInducing_mk.continuous_iff (Y := Y)]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : X → Y
h : ∀ (x : X), f x ~ᵢ g x
⊢ Continuous[inst✝¹, _] (SeparationQuotient.mk ∘ f) ↔ Continuous[inst✝¹, _] (SeparationQuotient.mk ∘ g)
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_3
inst✝ : TopologicalSpace X
⊢ irreducibleComponents X = {s | Maximal (fun x ↦ IsClosed[inst✝] x ∧ IsIrreducible x) s}

Tactic:
ext s
  constructor
  · intro H
    exact ⟨⟨isClosed_of_mem_irreducibleComponents _ H, H.1⟩, fun x h e => H.2 h.2 e⟩
  · intro H
    refine ⟨H.1.2, fun x h e => ?_⟩
    have : closure x ≤ s := H.2 ⟨isClosed_closure, h.closure⟩ (e.trans subset_closure)
    exact le_trans subset_closure this

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case mpr
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
H : Disjoint (𝓝[≠] x) (𝓟 S)
⊢ (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S))

Tactic:
refine ⟨fun hx ↦ ?_, fun _ ↦ H⟩
    simpa [disjoint_iff, nhdsWithin, inf_assoc, hx] using H

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
h : t.Subsingleton
⊢ s ∈ codiscreteWithin t

Tactic:
by
  rw [codiscreteWithin_iff_locallyEmptyComplementWithin]
  intro z hz
  use univ \ t, nhdsNE_of_nhdsNE_sdiff_finite univ_mem h.finite, by aesop

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
⊢ TransGen (fun a b ↦ (s a ∩ s b).Nonempty) i j

Tactic:
by_contra hij
  let S : Set ι := {k | TransGen (fun a b ↦ (s a ∩ s b).Nonempty) i k}
  let U : Set α := ⋃ k ∈ S, s k
  let V : Set α := ⋃ k ∈ Sᶜ, s k
  have hsplit : (⋃ n, s n) = U ∪ V := iSup_split s (· ∈ S)
  obtain ⟨a, ha⟩ := hi
  obtain ⟨b, hb⟩ := hj
  let hi_S : i ∈ S := Relation.TransGen.single ⟨a, ha, ha⟩
  have hUne : ((⋃ n, s n) ∩ U).Nonempty := ⟨a, mem_iUnion_of_mem i ha, mem_iUnion₂_of_mem hi_S ha⟩
  have hVne : ((⋃ n, s n) ∩ V).Nonempty := ⟨b, mem_iUnion_of_mem j hb, mem_iUnion₂_of_mem hij hb⟩
  obtain ⟨x, -, hxU, hxV⟩ := hs U V (isOpen_biUnion fun i a ↦ hs' i)
    (isOpen_biUnion fun i a ↦ hs' i) hsplit.le hUne hVne
  simp only [mem_iUnion, exists_prop, mem_compl_iff, U, V] at hxU hxV
  obtain ⟨k, hk, hxk⟩ := hxU
  obtain ⟨l, hl, hxl⟩ := hxV
  exact hl (hk.tail ⟨x, hxk, hxl⟩)

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

Goal state before:
pp: case h
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
x✝ y : α
hx✝ : x✝ ∈ s
hy : y ∈ s
Q : ↑s → ↑s → Prop := fun a b ↦ P ↑a ↑b
this : PreconnectedSpace ↑s
x : α
hx : x ∈ s
Z : ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
⊢ ∀ᶠ (y : { x // x ∈ s }) in 𝓝 ⟨x, hx⟩, Q ⟨x, hx⟩ y ∧ Q y ⟨x, hx⟩

Tactic:
nhdsWithin_eq_map_subtype_coe

Goal state after:
case h
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
x✝ y : α
hx✝ : x✝ ∈ s
hy : y ∈ s
Q : ↑s → ↑s → Prop := fun a b ↦ P ↑a ↑b
this : PreconnectedSpace ↑s
x : α
hx : x ∈ s
Z✝ : ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
Z : ∀ᶠ (y : α) in Filter.map Subtype.val (𝓝 ⟨x, ?h✝⟩), P x y ∧ P y x
⊢ ∀ᶠ (y : { x // x ∈ s }) in 𝓝 ⟨x, hx⟩, Q ⟨x, hx⟩ y ∧ Q y ⟨x, hx⟩

case h
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
x✝ y : α
hx✝ : x✝ ∈ s
hy : y ∈ s
Q : ↑s → ↑s → Prop := fun a b ↦ P ↑a ↑b
this : PreconnectedSpace ↑s
x : α
hx : x ∈ s
Z : ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
⊢ x ∈ s
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h :
  ∀ {ι : Type u} (t : ι → Set X),
    (∀ (i : ι), IsClosed[inst✝] (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝] (U i)
hsU : s ⊆ ⋃ i, U i
⊢ ∃ t, t.Countable ∧ s ⊆ ⋃ i ∈ t, U i

Tactic:
← disjoint_compl_right_iff_subset,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h :
  ∀ {ι : Type u} (t : ι → Set X),
    (∀ (i : ι), IsClosed[inst✝] (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝] (U i)
hsU : Disjoint s (⋃ i, U i)ᶜ
⊢ ∃ t, t.Countable ∧ s ⊆ ⋃ i ∈ t, U i
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h :
  ∀ {ι : Type u} (t : ι → Set X),
    (∀ (i : ι), IsClosed[inst✝] (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝] (U i)
hsU : s ⊓ ⋂ i, (U i)ᶜ = ⊥
t : Set ι✝
ht : t.Countable ∧ s ∩ ⋂ i ∈ t, (U i)ᶜ = ∅
⊢ t.Countable ∧ s ⊆ ⋃ i ∈ t, U i

Tactic:
← disjoint_compl_right_iff_subset,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h :
  ∀ {ι : Type u} (t : ι → Set X),
    (∀ (i : ι), IsClosed[inst✝] (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝] (U i)
hsU : s ⊓ ⋂ i, (U i)ᶜ = ⊥
t : Set ι✝
ht : t.Countable ∧ s ∩ ⋂ i ∈ t, (U i)ᶜ = ∅
⊢ t.Countable ∧ Disjoint s (⋃ i ∈ t, U i)ᶜ
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompletelyNormalSpace Y
e : X → Y
he : IsInducing e
⊢ CompletelyNormalSpace X

Tactic:
refine ⟨fun s t hd₁ hd₂ => ?_⟩
  simp only [he.nhdsSet_eq_comap]
  refine disjoint_comap (completely_normal ?_ ?_)
  · rwa [← subset_compl_iff_disjoint_left, image_subset_iff, preimage_compl,
      ← he.closure_eq_preimage_closure_image, subset_compl_iff_disjoint_left]
  · rwa [← subset_compl_iff_disjoint_right, image_subset_iff, preimage_compl,
      ← he.closure_eq_preimage_closure_image, subset_compl_iff_disjoint_right]

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 γ
inst✝ : T2Space γ
b : β
f : α → γ
g : β → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : α) in comap i (𝓝 b), g (i x) = f x
hg : ContinuousAt g b
⊢ di.extend f b = g b

Tactic:
by
  refine di.extend_eq_of_tendsto fun s hs => mem_map.2 ?_
  suffices ∀ᶠ x : α in comap i (𝓝 b), g (i x) ∈ s from
    hf.mp (this.mono fun x hgx hfx => hfx ▸ hgx)
  clear hf f
  refine eventually_comap.2 ((hg.eventually hs).mono ?_)
  rintro _ hxs x rfl
  exact hxs

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

Goal state before:
pp: X : Type u
Y : Type v
ι : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s✝ t : Set X
inst✝ : NonLindelofSpace X
s : Set X
hs : s = univ
⊢ ¬IsLindelof s

Tactic:
rw [hs]

Goal state after:
X : Type u
Y : Type v
ι : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s✝ t : Set X
inst✝ : NonLindelofSpace X
s : Set X
hs : s = univ
⊢ ¬IsLindelof univ
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
H : ∀ (s : Set X), IsOpen[inst✝] s → IsLindelof s
s : Set X
x✝ : s ⊆ univ
ι✝ : Type u
U : ι✝ → Set X
U_open : ∀ (i : ι✝), IsOpen[inst✝] (U i)
hU : s ⊆ ⋃ i, U i
t : Set ι✝
t_count : t.Countable
ht : ⋃ i, U i ⊆ ⋃ i ∈ t, U i
⊢ ∃ t, t.Countable ∧ s ⊆ ⋃ i ∈ t, U i

Tactic:
exact ⟨t, t_count, hU.trans ht⟩

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

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

Tactic:
rw [totallyDisconnectedSpace_iff, ← image_univ, hf.isTotallyDisconnected_image]

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
ho : IsGδ s
hd : Dense s
⊢ s ∈ residual X

Tactic:
by
  rcases ho with ⟨T, To, Tct, rfl⟩
  exact
    (countable_sInter_mem Tct).mpr fun t tT =>
      residual_of_dense_open (To t tT) (hd.mono (sInter_subset_of_mem tT))

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
ht : t ⊆ s
hs : IsNowhereDense s
⊢ interior (closure[inst✝] s) ⊆ ∅

Tactic:
rw [hs]

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ univ ∈ residual X

Tactic:
exact Filter.univ_mem

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

Goal state before:
pp: X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed[inst✝²] (f i)
hU : s ⊆ ⋃ i, f i
g : ι → Set X := fun i ↦ (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen[inst✝²] (g i)
⊢ Dense (⋃ i, interior (f i))

Tactic:
have hgd : Dense (⋂ i, g i) := by
    refine dense_iInter_of_isOpen hgo fun i x => ?_
    rw [closure_compl, interior_frontier (hc _)]
    exact id

Goal state after:
X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed[inst✝²] (f i)
hU : s ⊆ ⋃ i, f i
g : ι → Set X := fun i ↦ (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen[inst✝²] (g i)
hgd : Dense (⋂ i, g i)
⊢ Dense (⋃ i, interior (f i))
Module: Mathlib.Data.Rel.Cover

Goal state before:
pp: X : Type u_1
U : SetRel X X
s : Set X
⊢ U.IsCover s ∅ ↔ s = ∅

Tactic:
by
  simp [IsCover, eq_empty_iff_forall_notMem]

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

Goal state before:
pp: case mpr
β : Type ub
V W M : SetRel β β
inst✝ : W.IsSymm
x y w z : β
hwz : (w, z) ∈ M
w_in : (w, z).1 ∈ ball (x, y).1 V
z_in : (x, y).2 ∈ ball (w, z).2 W
⊢ (x, y) ∈ V ○ M ○ W

Tactic:
exact ⟨z, ⟨w, w_in, hwz⟩, z_in⟩

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
d s : SetRel α α
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
x✝ : α × α
x y : α
hp : (x, y) ∈ s
⊢ cl_d ∈ 𝓝 (x, y)

Tactic:
rw [nhds_eq_uniformity_prod, mem_lift'_sets]

Goal state after:
α : Type ua
inst✝ : UniformSpace α
d s : SetRel α α
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
x✝ : α × α
x y : α
hp : (x, y) ∈ s
⊢ ∃ t ∈ 𝓤 α, {y | (y, x) ∈ t} ×ˢ {y_1 | (y, y_1) ∈ t} ⊆ cl_d

case hh
α : Type ua
inst✝ : UniformSpace α
d s : SetRel α α
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
x✝ : α × α
x y : α
hp : (x, y) ∈ s
⊢ Monotone fun s ↦ {y | (y, x) ∈ s} ×ˢ {y_1 | (y, y_1) ∈ s}
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d

Tactic:
by
      let ⟨s, hs, hs_comp⟩ := comp3_mem_uniformity hd
      let ⟨t, ht, hst, ht_comp⟩ := nhdset_of_mem_uniformity s hs
      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₃⟩
      have : interior d ∈ 𝓤 α := by filter_upwards [hs] using this
      simp [this]

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

Goal state before:
pp: α : Type ua
β : Type ub
f : α → β
u₁ : Set (UniformSpace α)
u₂ : UniformSpace β
u : UniformSpace α
h₁ : u ∈ u₁
hf : UniformContinuous f
⊢ Tendsto (fun x ↦ (f x.1, f x.2)) (⨅ i, 𝓤 α) (𝓤 β)

Tactic:
exact tendsto_iInf' ⟨u, h₁⟩ hf

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
⊢ 𝓤 (α × β) = Filter.comap (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 β)

Tactic:
uniformity_prod,

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
⊢ Filter.comap (fun p ↦ (p.1.1, p.2.1)) (𝓤 α) ⊓ Filter.comap (fun p ↦ (p.1.2, p.2.2)) (𝓤 β) =
    Filter.comap (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 β)
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
hs : TotallyBounded s
hf : UniformContinuous f
⊢ TotallyBounded (f '' s)

Tactic:
simp only [← Filter.totallyBounded_principal_iff, ← Filter.map_principal] at hs ⊢

Goal state after:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
hf : UniformContinuous f
hs : (𝓟 s).TotallyBounded
⊢ (map f (𝓟 s)).TotallyBounded
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
uas : Set (UniformSpace α)
ubs : Set (UniformSpace β)
ua : UniformSpace α
ub : UniformSpace β
uc : UniformSpace γ
ha✝ : ua ∈ uas
hb✝ : ub ∈ ubs
hf : UniformContinuous fun p ↦ f p.1 p.2
ha : UniformContinuous id
hb : UniformContinuous id
⊢ UniformContinuous fun p ↦ f p.1 p.2

Tactic:
have h_unif_cont_id := @UniformContinuous.prodMap _ _ _ _ (sInf uas) (sInf ubs) ua ub _ _ ha hb

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
uas : Set (UniformSpace α)
ubs : Set (UniformSpace β)
ua : UniformSpace α
ub : UniformSpace β
uc : UniformSpace γ
ha✝ : ua ∈ uas
hb✝ : ub ∈ ubs
hf : UniformContinuous fun p ↦ f p.1 p.2
ha : UniformContinuous id
hb : UniformContinuous id
h_unif_cont_id : UniformContinuous (Prod.map id id)
⊢ UniformContinuous fun p ↦ f p.1 p.2
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: β : Type v
inst✝ : UniformSpace β
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y ↦ (f x, f y) ∉ s
⊢ comap (Prod.map f f) (𝓤 β) = 𝓟 SetRel.id

Tactic:
refine le_antisymm ?_ (@refl_le_uniformity α (UniformSpace.comap f _))

Goal state after:
β : Type v
inst✝ : UniformSpace β
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y ↦ (f x, f y) ∉ s
⊢ comap (Prod.map f f) (𝓤 β) ≤ 𝓟 SetRel.id
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: X : Type u_1
α : Type u_2
inst✝¹ : One α
inst✝ : TopologicalSpace X
⊢ mulTSupport 1 = ∅

Tactic:
rw [mulTSupport, mulSupport_one, closure_empty]

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

Goal state before:
pp: case refine_2
α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Tendsto u atTop (𝓝 a)
U' : ℕ → Set (α × α)
hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ i, U' i ⊆ s
Hmem : ∀ (n : ℕ), U n ∩ U' n ∈ 𝓤 α
f✝ : Filter α
hf : Cauchy f✝
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∃ n, U n ∩ U' n ⊆ s

Tactic:
· rcases hU'.1 hs with ⟨N, hN⟩
    exact ⟨N, Subset.trans inter_subset_right hN⟩

Goal state after: