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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ n, u n
u_props : ∀ (n : ℕ), IsOpen[inst✝] (u n) ∧ Disjoint (closure[inst✝] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ n, v n
v_props : ∀ (n : ℕ), IsOpen[inst✝] (v n) ∧ Disjoint (closure[inst✝] (v n)) s
open_lemma : ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst✝] (u₀ n)) → IsOpen[inst✝] (⋃ n, u₀ n \ closure[inst✝] (a n))
h₀ : Set X
u₀ v₀ : ℕ → Set X
h₀_cov : h₀ ⊆ ⋃ n, u₀ n
dis : ∀ (n : ℕ), Disjoint (closure[inst✝] (v₀ n)) h₀
x : X
xinh : x ∈ h₀
n : ℕ
xinun : x ∈ (fun n ↦ u₀ n) n
⊢ ∃ i, x ∈ u₀ i \ closure[inst✝] (⋃ m, ⋃ (_ : m ≤ i), v₀ m)

Tactic:
refine ⟨n, xinun, ?_⟩

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ n, u n
u_props : ∀ (n : ℕ), IsOpen[inst✝] (u n) ∧ Disjoint (closure[inst✝] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ n, v n
v_props : ∀ (n : ℕ), IsOpen[inst✝] (v n) ∧ Disjoint (closure[inst✝] (v n)) s
open_lemma : ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst✝] (u₀ n)) → IsOpen[inst✝] (⋃ n, u₀ n \ closure[inst✝] (a n))
h₀ : Set X
u₀ v₀ : ℕ → Set X
h₀_cov : h₀ ⊆ ⋃ n, u₀ n
dis : ∀ (n : ℕ), Disjoint (closure[inst✝] (v₀ n)) h₀
x : X
xinh : x ∈ h₀
n : ℕ
xinun : x ∈ (fun n ↦ u₀ n) n
⊢ x ∉ closure[inst✝] (⋃ m, ⋃ (_ : m ≤ n), v₀ m)
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
t : TopologicalSpace α
⊢ NontrivialTopology (WithTopology α t) ↔ t ≠ ⊤

Tactic:
simp_rw [nontrivialTopology_iff, topology_eq_induced, ne_eq, not_iff_not]
  constructor
  · intro h
    simpa [induced_compose, comp_def, induced_fun_id] using congr(induced (toTopology t) $h)
  · simp +contextual

Goal state after:
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
hf : IsCoinducing f
hf' : Injective f
s : Set X
hs : IsOpen[inst✝¹] s
⊢ IsOpen[inst✝] (f '' s)

Tactic:
rwa [← hf.isOpen_preimage, preimage_image_eq _ hf']

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
hg : IsOpenEmbedding g
⊢ IsOpenEmbedding (g ∘ f) ↔ IsOpenEmbedding f

Tactic:
by
  simp only [isOpenEmbedding_iff_continuous_injective_isOpenMap, ← hg.isOpenMap_iff, ←
    hg.1.continuous_iff, hg.injective.of_comp_iff]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x : α
s t : Set α
hs : s ∈ 𝓝[t] x
t' : Set α
⊢ s \ t' ∈ 𝓝[t \ t'] x

Tactic:
by
  rw [nhdsWithin, sdiff_eq, sdiff_eq, ← inf_principal, ← inf_assoc]
  exact inter_mem_inf hs (mem_principal_self _)

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
x : α
⊢ s ∩ t =ᶠ[𝓝 x] s ∩ t ∩ t

Tactic:
simp [inter_assoc]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
⊢ ContinuousOn f s ↔ Continuous[instTopologicalSpaceSubtype, inst✝] (s.domRestrict f)

Tactic:
ContinuousOn,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
⊢ (∀ x ∈ s, ContinuousWithinAt f s x) ↔ Continuous[instTopologicalSpaceSubtype, inst✝] (s.domRestrict f)
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
h : t ⊆ s
⊢ 𝓝ˢ[t] s = 𝓟 t

Tactic:
by
  simp [nhdsSetWithin, (principal_mono.2 h).trans principal_le_nhdsSet]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
x : α
⊢ ContinuousWithinAt f (s ∪ t) x ↔ ContinuousWithinAt f s x ∧ ContinuousWithinAt f t x

Tactic:
simp only [ContinuousWithinAt, nhdsWithin_union, tendsto_sup]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
Y : Type u_5
p : X → Prop
l : Filter Y
f : Y → Subtype p
a : X
ha : p a
⊢ Tendsto f l (𝓝 ⟨a, ha⟩) ↔ Tendsto (fun x ↦ ↑(f x)) l (𝓝 ↑⟨a, ha⟩)

Tactic:
rw [nhds_subtype_eq_comap, tendsto_comap_iff]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
Y : Type u_5
p : X → Prop
l : Filter Y
f : Y → Subtype p
a : X
ha : p a
⊢ Tendsto (Subtype.val ∘ f) l (𝓝 a) ↔ Tendsto (fun x ↦ ↑(f x)) l (𝓝 ↑⟨a, ha⟩)
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
h : MapsTo f s t
hg : ContinuousWithinAt g t (f x)
⊢ ContinuousWithinAt (g ∘ f) s x

Tactic:
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 γ
inst✝ : DiscreteTopology α
f : α × β → γ
s : Set (α × β)
⊢ ContinuousOn f s ↔ ∀ (a : α), ContinuousOn (fun x ↦ f (a, x)) {b | (a, b) ∈ s}

Tactic:
ContinuousOn,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
s : Set (α × β)
⊢ (∀ x ∈ s, ContinuousWithinAt f s x) ↔
    ∀ (a : α), ∀ x ∈ {b | (a, b) ∈ s}, ContinuousWithinAt (fun x ↦ f (a, x)) {b | (a, b) ∈ s} x
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
s : Set (α × β)
⊢ ContinuousOn f s ↔ ∀ (b : β), ContinuousOn (fun x ↦ f (x, b)) {a | (a, b) ∈ s}

Tactic:
ContinuousOn,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
s : Set (α × β)
⊢ (∀ x ∈ s, ContinuousWithinAt f s x) ↔
    ∀ (b : β), ∀ x ∈ {a | (a, b) ∈ s}, ContinuousWithinAt (fun x ↦ f (x, b)) {a | (a, b) ∈ s} x
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_2
α : Type u
t : TopologicalSpace α
ι : Sort u_2
U : ι → Set α
Uo : ∀ (i : ι), IsOpen[t] (U i)
Uc : ⋃ i, U i = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
⊢ ∀ (a : α) (u : Set α), a ∈ u → IsOpen[t] u → ∃ v ∈ ⋃ i, image Subtype.val '' b i, a ∈ v ∧ v ⊆ u

Tactic:
· intro a u ha uo
    rcases iUnion_eq_univ_iff.1 Uc a with ⟨i, hi⟩
    lift a to ↥(U i) using hi
    rcases (hb i).exists_subset_of_mem_open ha (uo.preimage continuous_subtype_val) with
      ⟨v, hvb, hav, hvu⟩
    exact ⟨(↑) '' v, mem_iUnion.2 ⟨i, mem_image_of_mem _ hvb⟩, mem_image_of_mem _ hav,
      image_subset_iff.2 hvu⟩

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 : α → β
g : β → γ
hg : IsInducing g
s : Set α
⊢ ContinuousOn f s ↔ ContinuousOn (g ∘ f) s

Tactic:
ContinuousOn,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : β → γ
hg : IsInducing g
s : Set α
⊢ (∀ x ∈ s, ContinuousWithinAt f s x) ↔ ∀ x ∈ s, ContinuousWithinAt (g ∘ f) s x
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: β : Type u_2
s : ℕ → Set β
n : ℕ
⊢ accumulate s n = ⋃ k, ⋃ (_ : k < n + 1), s k

Tactic:
by
  simp_rw [Nat.lt_add_one_iff, accumulate]

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

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B
union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B
sUnion_univ : ∀ (a : α), ∃ b ∈ B, a ∈ b
x : α
s : Set α
hs : s ∈ B
hxs : x ∈ s
⊢ {x} ∈ B

Tactic:
exact subset_mem s hs {x} (singleton_subset_iff.mpr hxs)

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

Goal state before:
pp: α : Type u_2
inst✝ : Bornology α
⊢ cobounded α = ⊥ ↔ BoundedSpace α

Tactic:
rw [← isBounded_univ, isBounded_def, compl_univ, empty_mem_iff_bot]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case refine_2
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : TopologicalSpace X
f : Sigma σ → X
x✝¹ : (∀ (i : ι), IsInducing (f ∘ Sigma.mk i)) ∧ ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
h₁ : ∀ (i : ι), IsInducing (f ∘ Sigma.mk i)
h₂ : ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
x✝ : Sigma σ
i : ι
x : σ i
⊢ map (Sigma.mk i) (comap (Sigma.mk i) (comap f (𝓝 (f ⟨i, x⟩)))) = comap f (𝓝 (f ⟨i, x⟩))

Tactic:
map_comap_of_mem

Goal state after:
case refine_2
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : TopologicalSpace X
f : Sigma σ → X
x✝¹ : (∀ (i : ι), IsInducing (f ∘ Sigma.mk i)) ∧ ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
h₁ : ∀ (i : ι), IsInducing (f ∘ Sigma.mk i)
h₂ : ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
x✝ : Sigma σ
i : ι
x : σ i
⊢ comap f (𝓝 (f ⟨i, x⟩)) = comap f (𝓝 (f ⟨i, x⟩))

case refine_2
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : TopologicalSpace X
f : Sigma σ → X
x✝¹ : (∀ (i : ι), IsInducing (f ∘ Sigma.mk i)) ∧ ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
h₁ : ∀ (i : ι), IsInducing (f ∘ Sigma.mk i)
h₂ : ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
x✝ : Sigma σ
i : ι
x : σ i
⊢ range (Sigma.mk i) ∈ comap f (𝓝 (f ⟨i, x⟩))
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_2.a
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := ⋯
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
⊢ ⋃ u ∈ s', f u ⊆ {s | IsOpen[ts] s}

Tactic:
simp only [iUnion_subset_iff]

Goal state after:
case refine_2.a
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
⊢ ∀ i ∈ s', f i ⊆ {s | IsOpen[ts] s}
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed[inst✝] (f i)
x : X
⊢ IsClosed[inst✝] (⋃ i, f ↑i)

Tactic:
exact (hf.comp_injective Subtype.val_injective).isClosed_iUnion fun i => hc _

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : X → Set X
hf : ∀ (x : X), f x ∈ 𝓝 x
⊢ ∃ s, s.Countable ∧ ⋃ x ∈ s, f x = univ

Tactic:
by
  simp only [← nhdsWithin_univ] at hf
  rcases countable_cover_nhdsWithin_of_sigmaCompact isClosed_univ fun x _ => hf x with
    ⟨s, -, hsc, hsU⟩
  exact ⟨s, hsc, univ_subset_iff.1 hsU⟩

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
l : Filter X
s' : Set X
hmem : s ∈ l
h : ∀ x ∈ s, ClusterPt x l → x ∈ s'
⊢ l ≤ 𝓝ˢ s'

Tactic:
refine le_iff_ultrafilter.2 fun f hf ↦ ?_

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
l : Filter X
s' : Set X
hmem : s ∈ l
h : ∀ x ∈ s, ClusterPt x l → x ∈ s'
f : Ultrafilter X
hf : ↑f ≤ l
⊢ ↑f ≤ 𝓝ˢ s'
Module: Mathlib.Data.Set.Subset

Goal state before:
pp: α : Type u_2
A : Set α
D : Set ↑A
⊢ Subtype.val '' Dᶜ = A \ Subtype.val '' D

Tactic:
by
  rw [compl_eq_univ_sdiff, image_val_sdiff, image_univ, Subtype.range_coe_subtype, ofPred_mem_eq]

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
tfae_2_to_3 : pure x ≤ 𝓝 y → ∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s
tfae_3_to_4 : (∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s) → ∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s
tfae_4_to_5 : (∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s) → y ∈ closure[inst✝] {x}
tfae_6_iff_5 : closure[inst✝] {y} ⊆ closure[inst✝] {x} ↔ y ∈ closure[inst✝] {x}
⊢ y ∈ closure[inst✝] {x} ↔ ClusterPt y (pure x)

Tactic:
mem_closure_iff_clusterPt,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
tfae_2_to_3 : pure x ≤ 𝓝 y → ∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s
tfae_3_to_4 : (∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s) → ∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s
tfae_4_to_5 : (∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s) → y ∈ closure[inst✝] {x}
tfae_6_iff_5 : closure[inst✝] {y} ⊆ closure[inst✝] {x} ↔ y ∈ closure[inst✝] {x}
⊢ ClusterPt y (𝓟 {x}) ↔ ClusterPt y (pure x)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
g : X → Y
f : Filter X
hg : Continuous[inst✝¹, inst✝] g
hf : Disjoint f (cocompact X)
⊢ Disjoint f (comap g (cocompact Y))

Tactic:
disjoint_iff_inf_le

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
g : X → Y
f : Filter X
hg : Continuous[inst✝¹, inst✝] g
hf : Disjoint f (cocompact X)
⊢ f ⊓ comap g (cocompact Y) ≤ ⊥
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case neg.inr.ht
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : x ∉ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}ᶜ
⊢ ContinuousWithinAt (fun a ↦ if p a then f a else g a) (s ∩ {a | p a}ᶜ) x

Tactic:
exact (hg x hx).congr (fun y hy => if_neg hy.2) (if_neg hx.2)

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ StableUnderGeneralization s ↔ ∃ S, (∀ s ∈ S, IsOpen[inst✝] s) ∧ ⋂₀ S = s

Tactic:
by
  refine ⟨?_, fun ⟨S, hS, e⟩ ↦ e ▸
    stableUnderGeneralization_sInter S (fun x hx ↦ (hS x hx).stableUnderGeneralization)⟩
  rw [← stableUnderSpecialization_compl_iff, stableUnderSpecialization_iff_exists_sUnion_eq]
  exact fun ⟨S, h₁, h₂⟩ ↦ ⟨(·ᶜ) '' S, fun s ⟨t, ht, e⟩ ↦ e ▸ (h₁ t ht).isOpen_compl,
    compl_injective ((sUnion_eq_compl_sInter_compl S).symm.trans h₂)⟩

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Set X
hs : IsClosed[inst✝¹] s
hmin : ∀ t ⊆ s, t.Nonempty → IsClosed[inst✝¹] t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen[inst✝¹] U
hU : Xor (x ∈ U) (y ∈ U)
⊢ False

Tactic:
wlog h : x ∈ U ∧ y ∉ U

Goal state after:
case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Set X
hs : IsClosed[inst✝¹] s
hmin : ∀ t ⊆ s, t.Nonempty → IsClosed[inst✝¹] t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen[inst✝¹] U
hU : Xor (x ∈ U) (y ∈ U)
this :
  ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X] {s : Set X},
    IsClosed s →
      (∀ t ⊆ s, t.Nonempty → IsClosed t → t = s) →
        ∀ x ∈ s, ∀ y ∈ s, ¬x = y → ∀ (U : Set X), IsOpen U → Xor (x ∈ U) (y ∈ U) → x ∈ U ∧ y ∉ U → False
h : ¬(x ∈ U ∧ y ∉ U)
⊢ False

X✝ : Type u_1
inst✝² : TopologicalSpace X✝
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Set X
hs : IsClosed[inst✝¹] s
hmin : ∀ t ⊆ s, t.Nonempty → IsClosed[inst✝¹] t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen[inst✝¹] U
hU : Xor (x ∈ U) (y ∈ U)
h : x ∈ U ∧ y ∉ U
⊢ False
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y → Z
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
s : Set (SeparationQuotient X × SeparationQuotient Y)
⊢ ContinuousOn (uncurry (lift₂ f hf)) s ↔ ContinuousOn (uncurry f) (Prod.map mk mk ⁻¹' s)

Tactic:
ContinuousOn,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y → Z
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
s : Set (SeparationQuotient X × SeparationQuotient Y)
⊢ (∀ x ∈ s, ContinuousWithinAt (uncurry (lift₂ f hf)) s x) ↔
    ∀ x ∈ Prod.map mk mk ⁻¹' s, ContinuousWithinAt (uncurry f) (Prod.map mk mk ⁻¹' s) x
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case hg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s s' t : Set α
inst✝ : (x : α) → Decidable (x ∈ t)
h : ContinuousOn f (s ∩ closure[inst✝²] t)
h' : ContinuousOn g (s' ∩ closure[inst✝²] tᶜ)
H : s ∩ frontier t = s' ∩ frontier t
Heq : EqOn f g (s ∩ frontier t)
⊢ ContinuousOn g (t.ite s s' ∩ closure[inst✝²] tᶜ)

Tactic:
ite_inter_closure_compl_eq_of_inter_frontier_eq H

Goal state after:
case hg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s s' t : Set α
inst✝ : (x : α) → Decidable (x ∈ t)
h : ContinuousOn f (s ∩ closure[inst✝²] t)
h' : ContinuousOn g (s' ∩ closure[inst✝²] tᶜ)
H : s ∩ frontier t = s' ∩ frontier t
Heq : EqOn f g (s ∩ frontier t)
⊢ ContinuousOn g (s' ∩ closure[inst✝²] tᶜ)
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Set X
hs : IsOpen[inst✝¹] s
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen[inst✝¹] t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen[inst✝¹] U
hU : Xor (x ∈ U) (y ∈ U)
⊢ False

Tactic:
wlog h : x ∈ U ∧ y ∉ U

Goal state after:
case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Set X
hs : IsOpen[inst✝¹] s
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen[inst✝¹] t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen[inst✝¹] U
hU : Xor (x ∈ U) (y ∈ U)
this :
  ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X] {s : Set X},
    IsOpen s →
      (∀ t ⊆ s, t.Nonempty → IsOpen t → t = s) →
        ∀ x ∈ s, ∀ y ∈ s, ¬x = y → ∀ (U : Set X), IsOpen U → Xor (x ∈ U) (y ∈ U) → x ∈ U ∧ y ∉ U → False
h : ¬(x ∈ U ∧ y ∉ U)
⊢ False

X✝ : Type u_1
inst✝² : TopologicalSpace X✝
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Set X
hs : IsOpen[inst✝¹] s
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen[inst✝¹] t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen[inst✝¹] U
hU : Xor (x ∈ U) (y ∈ U)
h : x ∈ U ∧ y ∉ U
⊢ False
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case refine_1.insert
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsIrreducible s
u : Set X
U : Finset (Set X)
a✝ : u ∉ U
IH : (∀ u ∈ U, IsOpen[inst✝] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty
hu : ∀ u_1 ∈ insert u U, IsOpen[inst✝] u_1
hU : ∀ u_1 ∈ insert u U, (s ∩ u_1).Nonempty
⊢ (s ∩ ⋂₀ ↑(insert u U)).Nonempty

Tactic:
rw [Finset.coe_insert, sInter_insert]
      rw [Finset.forall_mem_insert] at hu hU
      exact h.2 _ _ hu.1 (U.finite_toSet.isOpen_sInter hu.2) hU.1 (IH hu.2 hU.2)

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

Goal state before:
pp: case htcl
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝¹] S
hne : S.Nonempty
opens : Set (Set X) := ⋯
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty { U // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
⊢ ∀ (i : { U // U ∈ c }), IsClosed[inst✝¹] (↑i)ᶜ

Tactic:
· exact fun U => (hc U.2).2.1.isClosed_compl

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
s t : Set X
f g : X → Y
h : EqOn f g s
hf : ContinuousOn f t
hg : ContinuousOn g t
hst : s ⊆ t
hts : t ⊆ closure[inst✝²] s
x : X
hx : x ∈ t
this : (𝓝[s] x).NeBot
⊢ f x = g x

Tactic:
exact
    tendsto_nhds_unique_of_eventuallyEq ((hf x hx).mono_left <| nhdsWithin_mono _ hst)
      ((hg x hx).mono_left <| nhdsWithin_mono _ hst) (h.eventuallyEq_of_mem self_mem_nhdsWithin)

Goal state after:
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
⊢ ContinuousOn (update f x y) s ↔ ContinuousOn f (s \ {x}) ∧ (x ∈ s → Tendsto f (𝓝[s \ {x}] x) (𝓝 y))

Tactic:
ContinuousOn,

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
⊢ (∀ x_1 ∈ s, ContinuousWithinAt (update f x y) s x_1) ↔
    ContinuousOn f (s \ {x}) ∧ (x ∈ s → Tendsto f (𝓝[s \ {x}] x) (𝓝 y))
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
ι : Type u_3
p : ι → Prop
t : ι → Set X
s : Set X
hs : IsDiscrete s
x : X
hb : (𝓝 x).HasBasis p t
hx : x ∈ s
⊢ ∃ i, p i ∧ t i ∩ s = {x}

Tactic:
rcases (nhdsWithin_hasBasis hb s).mem_iff.1 (singleton_mem_nhdsWithin_of_mem_discrete hs hx) with
    ⟨i, hi, hix⟩

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
ι : Type u_3
p : ι → Prop
t : ι → Set X
s : Set X
hs : IsDiscrete s
x : X
hb : (𝓝 x).HasBasis p t
hx : x ∈ s
i : ι
hi : p i
hix : t i ∩ s ⊆ {x}
⊢ ∃ i, p i ∧ t i ∩ s = {x}
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s K : Set X
hK : IsCompact K
hs : (K \ s).Infinite
⊢ ∃ x ∈ K, AccPt x (𝓟 (K \ s))

Tactic:
exact Set.Infinite.exists_accPt_of_subset_isCompact hs hK (sep_subset _ _)

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x : α
s t : Set α
H1 : x ∈ s
H2 : x ∈ t
H3 : IsPreconnected s
H4 : IsPreconnected t
⊢ ∀ s_1 ∈ {s, t}, x ∈ s_1

Tactic:
rintro r (rfl | rfl | h)

Goal state after:
case inl
α : Type u
inst✝ : TopologicalSpace α
x : α
t : Set α
H2 : x ∈ t
H4 : IsPreconnected t
r : Set α
H1 : x ∈ r
H3 : IsPreconnected r
⊢ x ∈ r

case inr
α : Type u
inst✝ : TopologicalSpace α
x : α
s t : Set α
H1 : x ∈ s
H2 : x ∈ t
H3 : IsPreconnected s
H4 : IsPreconnected t
⊢ x ∈ t
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x : α
s t : Set α
H1 : x ∈ s
H2 : x ∈ t
H3 : IsPreconnected s
H4 : IsPreconnected t
⊢ ∀ s_1 ∈ {s, t}, IsPreconnected s_1

Tactic:
rintro r (rfl | rfl | h)

Goal state after:
case inl
α : Type u
inst✝ : TopologicalSpace α
x : α
t : Set α
H2 : x ∈ t
H4 : IsPreconnected t
r : Set α
H1 : x ∈ r
H3 : IsPreconnected r
⊢ IsPreconnected r

case inr
α : Type u
inst✝ : TopologicalSpace α
x : α
s t : Set α
H1 : x ∈ s
H2 : x ∈ t
H3 : IsPreconnected s
H4 : IsPreconnected t
⊢ IsPreconnected t
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
hF : IsOpen[inst✝¹] F
y : α
hy : y ∈ connectedComponentIn F x
⊢ connectedComponentIn F x ∈ 𝓝 y

Tactic:
connectedComponentIn_eq hy

Goal state after:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
hF : IsOpen[inst✝¹] F
y : α
hy : y ∈ connectedComponentIn F x
⊢ connectedComponentIn F y ∈ 𝓝 y