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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ ClusterPt x (𝓟 s) ↔ ∃ᶠ (y : X) in 𝓝 x, y ∈ s

Tactic:
simp only [clusterPt_principal_iff, frequently_iff, Set.Nonempty, mem_inter_iff]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
t : TopologicalSpace X
s : Set (Set Y)
h : ∀ t_1 ∈ s, IsOpen[t] (f ⁻¹' t_1)
⊢ IsOpen[t] (f ⁻¹' ⋃₀ s)

Tactic:
simpa only [preimage_sUnion] using isOpen_biUnion h

Goal state after:
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
⊢ 𝓟 univ = ⊤

Tactic:
principal_univ

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
⊢ ⊤ = ⊤
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hpure : ∀ (a : α) (i : ι a), p a i → a ∈ s a i
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
⊢ 𝓝 a = n a

Tactic:
let t : TopologicalSpace α := .mkOfNhds n

Goal state after:
α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hpure : ∀ (a : α) (i : ι a), p a i → a ∈ s a i
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := TopologicalSpace.mkOfNhds n
⊢ 𝓝 a = n a
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ IsClosedMap f ↔ ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})

Tactic:
rw [isClosedMap_iff_comap_nhdsSet_le]

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ (∀ {s : Set Y}, comap f (𝓝ˢ s) ≤ 𝓝ˢ (f ⁻¹' s)) ↔ ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝 a ⊓ 𝓟 (s ∪ t) = 𝓝 a ⊓ (𝓟 s ⊔ 𝓟 t)

Tactic:
sup_principal

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝 a ⊓ 𝓟 (s ∪ t) = 𝓝 a ⊓ 𝓟 (s ∪ t)
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
f : X → Bool
b : Bool
⊢ IsOpen[inst✝] (f ⁻¹' {b}) ∧ IsOpen[inst✝] (f ⁻¹' {!b}) ↔ IsOpen[inst✝] (f ⁻¹' {!b}) ∧ IsOpen[inst✝] (f ⁻¹' {b})

Tactic:
and_comm

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
f : X → Bool
b : Bool
⊢ IsOpen[inst✝] (f ⁻¹' {!b}) ∧ IsOpen[inst✝] (f ⁻¹' {b}) ↔ IsOpen[inst✝] (f ⁻¹' {!b}) ∧ IsOpen[inst✝] (f ⁻¹' {b})
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
a : (i : ι) → A i
⊢ 𝓝 a = Filter.pi fun i ↦ 𝓝 (a i)

Tactic:
simp only [nhds_iInf, nhds_induced, Filter.pi]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (A i)
⊢ interior (I.pi s) = I.pi fun i ↦ interior (s i)

Tactic:
by
  ext a
  simp only [Set.mem_pi, mem_interior_iff_mem_nhds, set_pi_mem_nhds_iff hI]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case intro.refine_2
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
⊢ ∀ s ∈ {t | ∃ s i, (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s},
    IsOpen[generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}] s

Tactic:
rintro s ⟨t, i, ht, rfl⟩
    let := generateFrom { t | ∃ s : ∀ a, Set (X a), (∀ a, s a ∈ g a) ∧ t = pi univ s }
    refine isOpen_iff_forall_mem_open.2 fun f hf => ?_
    choose c hcg hfc using fun a => sUnion_eq_univ_iff.1 (hg a) (f a)
    refine ⟨pi i t ∩ pi ((↑i)ᶜ : Set ι) c, inter_subset_left, ?_, ⟨hf, fun a _ => hfc a⟩⟩
    classical
    rw [← univ_pi_piecewise]
    refine GenerateOpen.basic _ ⟨_, fun a => ?_, rfl⟩
    by_cases a ∈ i <;> simp [*]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case pos
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
i : ι
U : (i : ι) → Set (X i)
s : Finset ι
hU : ∀ i ∈ s, U i ∈ {U | IsOpen[inst✝ i] U}
h : ((↑s).pi U).Nonempty
hi : i ∈ s
⊢ IsOpen[inst✝ i] (eval i '' (↑s).pi U)

Tactic:
rw [eval_image_pi (mod_cast hi) h]

Goal state after:
case pos
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
i : ι
U : (i : ι) → Set (X i)
s : Finset ι
hU : ∀ i ∈ s, U i ∈ {U | IsOpen[inst✝ i] U}
h : ((↑s).pi U).Nonempty
hi : i ∈ s
⊢ IsOpen[inst✝ i] (U i)
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_1
⊢ 𝓟 univ = ⊤

Tactic:
principal_univ

Goal state after:
α : Type u_1
⊢ ⊤ = ⊤
Module: Mathlib.Topology.Bases

Goal state before:
pp: case h_open.inr
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
w : Set β
hw : w ∈ t
⊢ IsOpen[instTopologicalSpaceSum] ((fun u ↦ Sum.inr '' u) w)

Tactic:
· exact IsOpenEmbedding.inr.isOpenMap w (ht.isOpen hw)

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case h_nhds
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
y : Y
U : Set Y
y_in_U : y ∈ U
⊢ IsOpen[inst✝] U → ∃ v ∈ image π '' V, y ∈ v ∧ v ⊆ U

Tactic:
U_open

Goal state after:
case h_nhds
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
y : Y
U : Set Y
y_in_U : y ∈ U
U_open : IsOpen[inst✝] U
⊢ ∃ v ∈ image π '' V, y ∈ v ∧ v ⊆ U
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case refine_2
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (∀ (f : Ultrafilter X), ↑f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x ↑f) ↔ ∀ (f : Ultrafilter X), ↑f ≤ 𝓟 s → ∃ x ∈ s, ↑f ≤ 𝓝 x

Tactic:
· simp only [Ultrafilter.clusterPt_iff]

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ {ι : Type u} (U : ι → Set X), (∀ (i : ι), IsOpen[inst✝] (U i)) → s ⊆ ⋃ i, U i → ∃ t, s ⊆ ⋃ i ∈ t, U i
f : Filter X
hf : f.NeBot
hfs : f ≤ 𝓟 s
⊢ ∃ x ∈ s, ClusterPt x f

Tactic:
contrapose! h
  simp only [ClusterPt, not_neBot, ← disjoint_iff, SetCoe.forall',
    (nhds_basis_opens _).disjoint_iff_left] at h
  choose U hU hUf using h
  refine ⟨s, U, fun x => (hU x).2, fun x hx => mem_iUnion.2 ⟨⟨x, hx⟩, (hU _).1⟩, fun t ht => ?_⟩
  refine compl_notMem (le_principal_iff.1 hfs) ?_
  refine mem_of_superset ((biInter_finset_mem t).2 fun x _ => hUf x) ?_
  rw [subset_compl_comm, compl_iInter₂]
  simpa only [compl_compl]

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: case inr
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
a : α
ha : a ∈ (⇑toDual ∘ SetLike.coe) s
hat : a ∉ t
⊢ a ∉ ↑(lowerClosure t)

Tactic:
rintro ⟨b, hb, hab⟩

Goal state after:
case inr
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
a : α
ha : a ∈ (⇑toDual ∘ SetLike.coe) s
hat : a ∉ t
b : α
hb : b ∈ t
hab : a ≤ b
⊢ False
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous[inst✝¹, inst✝] f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y (range f))
s : Set Y
hsy : s ∈ 𝓝 y
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
⊢ ∃ x ∈ insert y (range f), ClusterPt x l

Tactic:
have : f '' K ∈ l := by
    filter_upwards [htl, le_principal_iff.1 hle] with y hyt hyf
    rcases hyf with (rfl | ⟨x, rfl⟩)
    exacts [(hd.le_bot ⟨mem_of_mem_nhds hsy, hyt⟩).elim,
      mem_image_of_mem _ (not_not.1 fun hxK => hd.le_bot ⟨hKs hxK, hyt⟩)]

Goal state after:
case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous[inst✝¹, inst✝] f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y (range f))
s : Set Y
hsy : s ∈ 𝓝 y
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
this : f '' K ∈ l
⊢ ∃ x ∈ insert y (range f), ClusterPt x l
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen[inst✝] s
⊢ IsOpen[inst✝] (mk ⁻¹' mk '' s)

Tactic:
preimage_image_mk_open hs

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen[inst✝] s
⊢ IsOpen[inst✝] s
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s z₁ z₂ : Set X
x✝¹ : IsClosed[inst✝] z₁
x✝ : IsClosed[inst✝] z₂
⊢ ¬(s ⊆ z₁ ∨ s ⊆ z₂) → ¬s ⊆ z₁ ∪ z₂ ↔ s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂

Tactic:
not_imp_not

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s z₁ z₂ : Set X
x✝¹ : IsClosed[inst✝] z₁
x✝ : IsClosed[inst✝] z₂
⊢ s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂ ↔ s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
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}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ y ∉ U
⊢ [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 ↔ 8 := by
    simp only [← principal_singleton, disjoint_principal_right]

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
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ y ∉ U
tfae_5_iff_8 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
⊢ [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.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
t S U : Set X
ht : IsPreirreducible t
hU : U.Nonempty
hU' : IsOpen[inst✝] U
h₁ : U ⊆ S
h₂ : S ⊆ t
⊢ IsIrreducible S

Tactic:
obtain ⟨z, hz⟩ := hU

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
t S U : Set X
ht : IsPreirreducible t
hU' : IsOpen[inst✝] U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
⊢ IsIrreducible S
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
t : Set X
ht : IsIrreducible t
f : Y → X
hf₂ : IsOpenMap f
hf₃ : ∀ (x : X), IsPreirreducible (f ⁻¹' {x})
x : Y
hx : f x ∈ t
⊢ (f ⁻¹' t).Nonempty

Tactic:
exact ⟨x, hx⟩

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

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
ι : Type u_4
X : ι → Type u_3
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (a : ι), T2Space (X a)
⊢ Pairwise fun x y ↦
    ∃ u v, IsOpen[instTopologicalSpaceSigma] u ∧ IsOpen[instTopologicalSpaceSigma] v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v

Tactic:
rintro ⟨i, x⟩ ⟨j, y⟩ ne

Goal state after:
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
ι : Type u_4
X : ι → Type u_3
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (a : ι), T2Space (X a)
i : ι
x : X i
j : ι
y : X j
ne : ⟨i, x⟩ ≠ ⟨j, y⟩
⊢ ∃ u v,
    IsOpen[instTopologicalSpaceSigma] u ∧ IsOpen[instTopologicalSpaceSigma] v ∧ ⟨i, x⟩ ∈ u ∧ ⟨j, y⟩ ∈ v ∧ Disjoint u v
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : T1Space X
inst✝¹ : DecidableEq X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
x : X
y : Y
⊢ ((x ∈ s → ContinuousWithinAt (update f x y) s x) ∧ ∀ (b : X), b ≠ x → b ∈ s → ContinuousWithinAt (update f x y) s b) ↔
    ContinuousOn f (s \ {x}) ∧ (x ∈ s → Tendsto f (𝓝[s \ {x}] x) (𝓝 y))

Tactic:
and_comm

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : T1Space X
inst✝¹ : DecidableEq X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
x : X
y : Y
⊢ (∀ (b : X), b ≠ x → b ∈ s → ContinuousWithinAt (update f x y) s b) ∧ (x ∈ s → ContinuousWithinAt (update f x y) s x) ↔
    ContinuousOn f (s \ {x}) ∧ (x ∈ s → Tendsto f (𝓝[s \ {x}] x) (𝓝 y))
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
s t : Set X
hu : t ⊆ insert y s
h : x ≠ y
⊢ insert x s ∈ 𝓝[s] x

Tactic:
exact mem_of_superset self_mem_nhdsWithin (subset_insert x s)

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
S : Set X
x : X
h : AccPt x (𝓟 S)
⊢ S.Infinite

Tactic:
by
  intro hs
  have := hs.compl_mem_codiscrete
  rw [mem_codiscrete_accPt, compl_compl] at this
  exact this _ h

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
t : OrderClosedTopology α
inst✝ : Preorder β
s : Set β
⊢ IsClosed[Pi.topologicalSpace] {f | MonotoneOn f s}

Tactic:
simp only [isClosed_iff_clusterPt, clusterPt_principal_iff_frequently]

Goal state after:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
t : OrderClosedTopology α
inst✝ : Preorder β
s : Set β
⊢ ∀ (a : β → α), (∃ᶠ (y : β → α) in 𝓝 a, y ∈ {f | MonotoneOn f s}) → a ∈ {f | MonotoneOn f s}
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α✝ : Type u
β : Type v
γ : Type w
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), OrderClosedTopology (α i)
⊢ IsClosed[instTopologicalSpaceProd] (⋂ i, {x | x.1 i ≤ x.2 i})

Tactic:
exact isClosed_iInter fun i => isClosed_le (continuous_apply i).fst' (continuous_apply i).snd'

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

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

Tactic:
apply isPreconnected_of_forall_pair
  rintro ⟨a₁, b₁⟩ ⟨ha₁, hb₁⟩ ⟨a₂, b₂⟩ ⟨ha₂, hb₂⟩
  refine ⟨Prod.mk a₁ '' t ∪ flip Prod.mk b₂ '' s, ?_, .inl ⟨b₁, hb₁, rfl⟩, .inr ⟨a₂, ha₂, rfl⟩, ?_⟩
  · rintro _ (⟨y, hy, rfl⟩ | ⟨x, hx, rfl⟩)
    exacts [⟨ha₁, hy⟩, ⟨hx, hb₂⟩]
  · exact (ht.image _ (by fun_prop)).union (a₁, b₂) ⟨b₂, hb₂, rfl⟩
      ⟨a₁, ha₁, rfl⟩ (hs.image _ (Continuous.prodMk_left _).continuousOn)

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

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

Tactic:
by
  contrapose! hst
  rcases hs.elim_countable_subfamily_closed t htc hst with ⟨u, ⟨_, husub⟩⟩
  exact ⟨u, fun _ ↦ husub⟩

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

Goal state before:
pp: case neg
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (coLindelof X) (𝓝 y)
hfc : Continuous[inst✝², inst✝¹] f
l : Filter Y
hne : l.NeBot
inst✝ : CountableInterFilter l
hle : l ≤ 𝓟 (insert y (range f))
s : Set Y
hsy : s ∈ 𝓝 y
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsLindelof K
hKs : Kᶜ ⊆ f ⁻¹' s
⊢ ∃ x ∈ insert y (range f), ClusterPt x l

Tactic:
have : f '' K ∈ l := by
    filter_upwards [htl, le_principal_iff.1 hle] with y hyt hyf
    rcases hyf with (rfl | ⟨x, rfl⟩)
    exacts [(hd.le_bot ⟨mem_of_mem_nhds hsy, hyt⟩).elim,
      mem_image_of_mem _ (not_not.1 fun hxK => hd.le_bot ⟨hKs hxK, hyt⟩)]

Goal state after:
case neg
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (coLindelof X) (𝓝 y)
hfc : Continuous[inst✝², inst✝¹] f
l : Filter Y
hne : l.NeBot
inst✝ : CountableInterFilter l
hle : l ≤ 𝓟 (insert y (range f))
s : Set Y
hsy : s ∈ 𝓝 y
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsLindelof K
hKs : Kᶜ ⊆ f ⁻¹' s
this : f '' K ∈ l
⊢ ∃ x ∈ insert y (range f), ClusterPt x l
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : HereditarilyLindelofSpace X
s : Set X
⊢ IsLindelof s

Tactic:
by
  apply HereditarilyLindelofSpace.isHereditarilyLindelof_univ
  exact subset_univ s

Goal state after:
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
e : α → β
de : IsDenseEmbedding e
p : α → Prop
x✝ : { x // p x }
x : α
hx : p x
⊢ 𝓝 ⟨x, hx⟩ = comap (subtypeEmb p e) (𝓝 (subtypeEmb p e ⟨x, hx⟩))

Tactic:
simp [subtypeEmb, nhds_subtype_eq_comap, de.isInducing.nhds_eq_comap, comap_comap,
        Function.comp_def]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : IsEmbedding f
hs : IsTotallyDisconnected s
u : Set β
hus : u ⊆ f '' s
hu : IsPreconnected u
⊢ u.Subsingleton

Tactic:
obtain ⟨v, hvs, rfl⟩ : ∃ v, v ⊆ s ∧ f '' v = u :=
    ⟨f ⁻¹' u ∩ s, inter_subset_right, by rwa [image_preimage_inter, inter_eq_left]⟩

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : IsEmbedding f
hs : IsTotallyDisconnected s
v : Set α
hvs : v ⊆ s
hus : f '' v ⊆ f '' s
hu : IsPreconnected (f '' v)
⊢ (f '' v).Subsingleton
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
I : Set ι
c : I.Countable
f : ι → Set X
h : ∀ i ∈ I, IsMeagre (f i)
⊢ IsMeagre (⋃ i ∈ I, f i)

Tactic:
suffices IsMeagre (⋃ i : I, f i) by simpa

Goal state after:
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
I : Set ι
c : I.Countable
f : ι → Set X
h : ∀ i ∈ I, IsMeagre (f i)
⊢ IsMeagre (⋃ i, f ↑i)
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
S : Set α
hS : IsPreconnected S
h : IsDiscrete S
this✝ : DiscreteTopology ↑S
this : PreconnectedSpace ↑S
⊢ S.Subsingleton

Tactic:
have : Subsingleton S := subsingleton_of_preconnected_totallyDisconnected

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
S : Set α
hS : IsPreconnected S
h : IsDiscrete S
this✝¹ : DiscreteTopology ↑S
this✝ : PreconnectedSpace ↑S
this : Subsingleton ↑S
⊢ S.Subsingleton
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 (⋂ b, bif b then s else t)

Tactic:
apply dense_iInter_of_Gδ <;> simp [Bool.forall_bool, *]

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

Goal state before:
pp: X : Type u_2
inst✝ : UniformSpace X
⊢ DiscreteUniformity X ↔ uniformity X = 𝓟 SetRel.id

Tactic:
by
  rw [discreteUniformity_iff_eq_bot, UniformSpace.ext_iff, Filter.ext_iff, bot_uniformity]

Goal state after:
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:
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

Goal state after:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
f : Filter α
m : α → β
hf : Cauchy f
s : Set α
hm : UniformContinuousOn m s
hfs : f ≤ 𝓟 s
⊢ Cauchy (Filter.comap Subtype.val f)
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
⊢ TendstoUniformlyOnFilter F f p (𝓟 univ) ↔ TendstoUniformlyOnFilter F f p ⊤

Tactic:
principal_univ

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
⊢ TendstoUniformlyOnFilter F f p ⊤ ↔ TendstoUniformlyOnFilter F f p ⊤
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
h : TendstoUniformlyOnFilter F f p p'
g : γ → α
⊢ TendstoUniformlyOnFilter (fun n ↦ F n ∘ g) (f ∘ g) p (comap g p')

Tactic:
tendstoUniformlyOnFilter_iff_tendsto

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
h : Tendsto (fun q ↦ (f q.2, F q.1 q.2)) (p ×ˢ p') (𝓤 β)
g : γ → α
⊢ Tendsto (fun q ↦ ((f ∘ g) q.2, (F q.1 ∘ g) q.2)) (p ×ˢ comap g p') (𝓤 β)
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
U : SetRel α α
hU : U ∈ 𝓤 α
s : Set α
⊢ closure[inst✝.toTopologicalSpace] s ⊆ U.preimage s

Tactic:
by
  intro x hx
  obtain ⟨y, hxy, hy⟩ := mem_closure_iff_ball.mp hx hU
  exact ⟨y, hy, hxy⟩

Goal state after:
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:
tendstoUniformlyOnFilter_iff_tendsto

Goal state after:
α : 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 : Tendsto (fun q ↦ (f q.2, F q.1 q.2)) (p ×ˢ p') (𝓤 β)
h' : Tendsto (fun q ↦ (f' q.2, F' q.1 q.2)) (q ×ˢ q') (𝓤 β')
⊢ Tendsto (fun q ↦ (Prod.map f f' q.2, Prod.map (F q.1.1) (F' q.1.2) q.2)) ((p ×ˢ q) ×ˢ p' ×ˢ q') (𝓤 (β × β'))
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:
exact Function.iterate_succ _ _ ▸ UniformContinuous.comp hn h

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
s : Set α
⊢ IsOpen[inst✝.toTopologicalSpace] s ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s

Tactic:
rw [isOpen_iff_ball_subset]

Goal state after:
α : Type ua
inst✝ : UniformSpace α
s : Set α
⊢ (∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s) ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s