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

Goal state before:
pp: case h_nhds
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : Set α → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
⊢ ∀ (a : α) (u : Set α), a ∈ u → IsOpen[t✝] u → ∃ v ∈ ⋃ u ∈ countableBasis α, s u, a ∈ v ∧ v ⊆ u

Tactic:
· intro x v hx hv
    simp only [mem_iUnion, exists_prop]
    obtain ⟨u, u_mem, xu, uv⟩ : ∃ u ∈ countableBasis α, x ∈ u ∧ u ⊆ v :=
      (isBasis_countableBasis α).isOpen_iff.1 hv _ hx
    have : x ∈ ⋃ a ∈ s u, a := by
      convert! xu
      exact (hs u u_mem).symm
    obtain ⟨w, ws, xw⟩ : ∃ w ∈ s u, x ∈ w := by simpa using this
    refine ⟨w, ⟨u, u_mem, ws⟩, xw, ?_⟩
    apply Subset.trans (Subset.trans _ (hs u u_mem).symm.subset) uv
    exact subset_iUnion₂_of_subset w ws (Subset.refl _)

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure[inst✝¹] (f i), ContinuousWithinAt g (f i) x
⊢ ContinuousOn g (⋃ i, f i)

Tactic:
rintro x -

Goal state after:
ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure[inst✝¹] (f i), ContinuousWithinAt g (f i) x
x : X
⊢ ContinuousWithinAt g (⋃ i, f i) x
Module: Mathlib.Topology.Compactness.LocallyCompact

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen[inst✝¹] U
hZ : IsClosed[inst✝¹] Z
hUZ : range f = U ∩ Z
this : ∀ (x : X), (𝓝 x).HasBasis (fun s ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U) fun s ↦ f ⁻¹' (s ∩ Z)
x : X
s : Set Y
x✝ : (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U
left✝ : s ∈ 𝓝 (f x)
hs : IsCompact s
hsU : s ⊆ U
⊢ s ∩ Z ⊆ U ∩ Z

Tactic:
by gcongr

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

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y
s t : Set X✝
inst✝³ : SigmaCompactSpace X✝
inst✝² : Finite ι
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), SigmaCompactSpace (X i)
⊢ ∀ (i : ι), Monotone (compactCovering (X i))

Tactic:
· exact fun i => compactCovering_subset (X i)

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

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
ι : Type v
inst✝ : Nonempty ι
hs : IsCompact s
t✝ : ι → Set X
htc : ∀ (i : ι), IsClosed[inst✝¹] (t✝ i)
hst : s ∩ ⋂ i, t✝ i = ∅
hdt : Directed (fun x1 x2 ↦ x1 ⊇ x2) t✝
t : ι
ht : s ⊆ (compl ∘ t✝) t
⊢ s ∩ t✝ t = ∅

Tactic:
by
    simpa only [subset_def, not_forall, eq_empty_iff_forall_notMem, mem_iUnion, exists_prop,
      mem_inter_iff, not_and, mem_iInter, mem_compl_iff] using! ht

Goal state after:
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:
← f.symm_symm,

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : UpperSet α
b : β
⊢ b ∈ (map f) s ↔ f.symm b ∈ s

Tactic:
← f.symm_symm,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : UpperSet α
b : β
⊢ b ∈ (map f.symm.symm) s ↔ f.symm.symm.symm b ∈ s
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
h : StableUnderSpecialization (range f)
x : X
y : Y
⊢ flip (fun x1 x2 ↦ x1 ⤳ x2) y (f x) → ∃ a', flip (fun x1 x2 ↦ x1 ⤳ x2) a' x ∧ f a' = y

Tactic:
e

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
h : StableUnderSpecialization (range f)
x : X
y : Y
e : flip (fun x1 x2 ↦ x1 ⤳ x2) y (f x)
⊢ ∃ a', flip (fun x1 x2 ↦ x1 ⤳ x2) a' x ∧ f a' = y
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
h : StableUnderGeneralization (range f)
x : X
y : Y
⊢ (fun x1 x2 ↦ x1 ⤳ x2) y (f x) → ∃ a', (fun x1 x2 ↦ x1 ⤳ x2) a' x ∧ f a' = y

Tactic:
e

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
h : StableUnderGeneralization (range f)
x : X
y : Y
e : y ⤳ f x
⊢ ∃ a', (fun x1 x2 ↦ x1 ⤳ x2) a' x ∧ f a' = y
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
V : Set Y
hV : IsPreirreducible V
f : X → Y
hf' : IsOpenMap f
hf'' : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
⊢ V ⊆ closure[inst✝] (V ∩ {x | IsPreirreducible (f ⁻¹' {x})})

Tactic:
simp [hf'', subset_closure]

Goal state after:
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
cond : ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ ↑F
⊢ ∀ x ∈ U, ∀ (l : Ultrafilter X), ↑l ≤ 𝓝 x → U ∈ l

Tactic:
x

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : Set X
cond : ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ ↑F
x : X
⊢ x ∈ U → ∀ (l : Ultrafilter X), ↑l ≤ 𝓝 x → U ∈ l
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : Y → X
hf : IsOpenEmbedding f
inst✝ : PreirreducibleSpace X
⊢ IsPreirreducible univ

Tactic:
by
    rw [← Set.preimage_univ]
    exact .preimage PreirreducibleSpace.isPreirreducible_univ hf

Goal state after:
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
tfae_5_iff_8 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
tfae_1_to_4 : T1Space X → Continuous[inst✝, _] ⇑CofiniteTopology.of
h : Continuous[inst✝, _] ⇑CofiniteTopology.of
⊢ ∀ (x : X), IsClosed[inst✝] {x}

Tactic:
x

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)
tfae_8_iff_9 : (∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
tfae_1_to_4 : T1Space X → Continuous[inst✝, _] ⇑CofiniteTopology.of
h : Continuous[inst✝, _] ⇑CofiniteTopology.of
x : X
⊢ IsClosed[inst✝] {x}
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: case inr
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⟩
h : i ≠ j
x✝ : TopologicalSpace ι := ⊥
this : DiscreteTopology ι
⊢ ∃ u v,
    IsOpen[instTopologicalSpaceSigma] u ∧ IsOpen[instTopologicalSpaceSigma] v ∧ ⟨i, x⟩ ∈ u ∧ ⟨j, y⟩ ∈ v ∧ Disjoint u v

Tactic:
exact separated_by_continuous (continuous_def.2 fun u _ => isOpen_sigma_fst_preimage u) h

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
U s : Set X
hU : U ∈ 𝓝[≠] x
hs : Finite ↑s
⊢ U \ s ∈ 𝓝[≠] x

Tactic:
by
  rw [mem_nhdsWithin] at hU ⊢
  obtain ⟨t, ht, h₁ts, h₂ts⟩ := hU
  use t \ (s \ {x})
  constructor
  · rw [← isClosed_compl_iff, compl_sdiff]
    exact s.toFinite.sdiff.isClosed.union (isClosed_compl_iff.2 ht)
  · tauto_set

Goal state after:
Module: Mathlib.Order.SuccPred.Relation

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
hnm : n ≤ m
⊢ (∀ i ∈ Ico n m, r i (succ i)) → ReflTransGen r n m

Tactic:
refine Succ.rec ?_ ?_ hnm

Goal state after:
case refine_1
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
hnm : n ≤ m
⊢ (∀ i ∈ Ico n n, r i (succ i)) → ReflTransGen r n n

case refine_2
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
hnm : n ≤ m
⊢ ∀ (n_1 : α),
    n ≤ n_1 →
      ((∀ i ∈ Ico n n_1, r i (succ i)) → ReflTransGen r n n_1) →
        (∀ i ∈ Ico n (succ n_1), r i (succ i)) → ReflTransGen r n (succ n_1)
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
h : ∀ x ∈ 𝓝ˢ t, x ∈ 𝓝ˢ s
⊢ s ⊆ t

Tactic:
x

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
h : ∀ x ∈ 𝓝ˢ t, x ∈ 𝓝ˢ s
x : X
⊢ x ∈ s → x ∈ t
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
S : Set X
h : IsPreirreducible S
⊢ ∀ x ∈ S, S ⊆ closure[inst✝¹] {x}

Tactic:
x

Goal state after:
case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
S : Set X
h : IsPreirreducible S
x : X
⊢ x ∈ S → S ⊆ closure[inst✝¹] {x}
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ (∀ ⦃x y : SeparationQuotient X⦄, x ⤳ y → x = y) ↔ Std.Symm Specializes

Tactic:
refine ⟨fun h ↦ ⟨fun x y xspecy ↦ ?_⟩, ?_⟩

Goal state after:
case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ ⦃x y : SeparationQuotient X⦄, x ⤳ y → x = y
x y : X
xspecy : x ⤳ y
⊢ y ⤳ x

case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
⊢ Std.Symm Specializes → ∀ ⦃x y : SeparationQuotient X⦄, x ⤳ y → x = y
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: α : Type u_2
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
p : α → (i : ι) → i ∈ S → Prop
⊢ (∀ᶠ (x : α) in l, ∀ (i : ι) (hi : i ∈ S), p x i hi) ↔ ∀ (i : ι) (hi : i ∈ S), ∀ᶠ (x : α) in l, p x i hi

Tactic:
simpa only [Filter.Eventually, ofPred_forall] using
    @countable_bInter_mem _ l _ _ _ hS fun i hi => { x | p x i hi }

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

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst✝] V ∧ x ∈ V ∧ IsConnected V
⊢ ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U

Tactic:
x

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst✝] V ∧ x ∈ V ∧ IsConnected V
x : α
⊢ ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst✝] ≤ 𝓝 x
tfae_5_to_6 : (∀ (x : X), (𝓝 x).lift' closure[inst✝] ≤ 𝓝 x) → ∀ (x : X), (𝓝 x).lift' closure[inst✝] = 𝓝 x
H : ∀ (x : X), (𝓝 x).lift' closure[inst✝] = 𝓝 x
a : X
s : Set X
hs : s ∈ 𝓝 a
⊢ ∃ t ∈ 𝓝 a, IsClosed[inst✝] t ∧ t ⊆ s

Tactic:
by
    rw [← H] at hs
    rcases (𝓝 a).basis_sets.lift'_closure.mem_iff.mp hs with ⟨U, hU, hUs⟩
    exact ⟨closure U, mem_of_superset hU subset_closure, isClosed_closure, hUs⟩

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

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : IsPreconnected s
⊢ ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v

pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
⊢ IsPreconnected s

Tactic:
· intro u v hu hv hs huv
    rw [isPreconnected_closed_iff] at h
    specialize h u v hu hv hs
    contrapose! huv
    simp only [not_subset] at huv
    rcases huv with ⟨⟨x, hxs, hxu⟩, ⟨y, hys, hyv⟩⟩
    have hxv : x ∈ v := or_iff_not_imp_left.mp (hs hxs) hxu
    have hyu : y ∈ u := or_iff_not_imp_right.mp (hs hys) hyv
    exact h ⟨y, hys, hyu⟩ ⟨x, hxs, hxv⟩

Goal state after:
case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
⊢ IsPreconnected s
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 : s ∩ ⋂ i, t i = ∅
u : Set ι
left✝ : u.Countable
husub : s ∩ ⋂ i ∈ u, t i = ∅
⊢ ∃ u, u.Countable → s ∩ ⋂ i ∈ u, t i = ∅

Tactic:
exact ⟨u, fun _ ↦ husub⟩

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

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
h : PreconnectedSpace α
⊢ ∀ (x : α), connectedComponent x = univ

Tactic:
x

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
h : PreconnectedSpace α
x : α
⊢ connectedComponent x = univ
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hSt : Disjoint (closure[inst✝] s) t
hsT : Disjoint s (closure[inst✝] t)
e : Set X := (closure[inst✝] s ∩ closure[inst✝] t)ᶜ
h : NormalSpace ↑e
he : IsOpen[inst✝] e
hst : Disjoint (Subtype.val ⁻¹' closure[inst✝] s) (Subtype.val ⁻¹' closure[inst✝] t)
U : Set X
hU : IsOpen[inst✝] U
hsU : Subtype.val ⁻¹' closure[inst✝] s ⊆ Subtype.val ⁻¹' U
V : Set X
hV : IsOpen[inst✝] V
htV : Subtype.val ⁻¹' closure[inst✝] t ⊆ Subtype.val ⁻¹' V
hUV : Disjoint (Subtype.val ⁻¹' U) (Subtype.val ⁻¹' V)
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
rw [← separatedNhds_iff_disjoint]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hSt : Disjoint (closure[inst✝] s) t
hsT : Disjoint s (closure[inst✝] t)
e : Set X := (closure[inst✝] s ∩ closure[inst✝] t)ᶜ
h : NormalSpace ↑e
he : IsOpen[inst✝] e
hst : Disjoint (Subtype.val ⁻¹' closure[inst✝] s) (Subtype.val ⁻¹' closure[inst✝] t)
U : Set X
hU : IsOpen[inst✝] U
hsU : Subtype.val ⁻¹' closure[inst✝] s ⊆ Subtype.val ⁻¹' U
V : Set X
hV : IsOpen[inst✝] V
htV : Subtype.val ⁻¹' closure[inst✝] t ⊆ Subtype.val ⁻¹' V
hUV : Disjoint (Subtype.val ⁻¹' U) (Subtype.val ⁻¹' V)
⊢ SeparatedNhds s t
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
⊢ (coLindelof X).NeBot

Tactic:
refine hasBasis_coLindelof.neBot_iff.2 fun {s} 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 : IsLindelof s
⊢ sᶜ.Nonempty
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: case inl
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝³ : TopologicalSpace α
s t✝ u v : Set α
inst✝² : TopologicalSpace β
inst✝¹ : TotallyDisconnectedSpace α
inst✝ : TotallyDisconnectedSpace β
t : Set α
ht : IsPreconnected t
x✝ : Sum.inl '' t ⊆ univ
hs : IsPreconnected (Sum.inl '' t)
⊢ (Sum.inl '' t).Subsingleton

Tactic:
exact ht.subsingleton.image _

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

Goal state before:
pp: case inr
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝³ : TopologicalSpace α
s t✝ u v : Set α
inst✝² : TopologicalSpace β
inst✝¹ : TotallyDisconnectedSpace α
inst✝ : TotallyDisconnectedSpace β
t : Set β
ht : IsPreconnected t
x✝ : Sum.inr '' t ⊆ univ
hs : IsPreconnected (Sum.inr '' t)
⊢ (Sum.inr '' t).Subsingleton

Tactic:
exact ht.subsingleton.image _

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

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
h : TotallyDisconnectedSpace α
⊢ ∀ (x : α), (connectedComponent x).Subsingleton

Tactic:
x

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
h : TotallyDisconnectedSpace α
x : α
⊢ (connectedComponent x).Subsingleton
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
H : IsTotallySeparated s
t : Set α
hts : t ⊆ s
ht : IsPreconnected t
⊢ t.Subsingleton

Tactic:
x

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
H : IsTotallySeparated s
t : Set α
hts : t ⊆ s
ht : IsPreconnected t
x : α
⊢ x ∈ t → ∀ ⦃y : α⦄, y ∈ t → x = y
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case ht
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : β
⊢ IsClosed[inst✝] (connectedComponent t)

Tactic:
exact isClosed_connectedComponent

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
Y : Type u_4
inst✝ : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
⊢ BaireSpace Y

Tactic:
constructor
  intro f hof hdf
  let s := range p
  let c := fun n : ℕ => p '' f n ∪ (closure s)ᶜ
  have c_open (n : ℕ) : IsOpen (c n) := IsOpen.union (hp.isOpenMap (f n) (hof n))
    isClosed_closure.isOpen_compl
  have c_dense (n : ℕ) : Dense (c n) := by
    rw [dense_iff_closure_eq, subset_antisymm_iff]
    have : univ ⊆ closure (c n) := calc
      _ ⊆ (interior (closure s)) ∪ (interior (closure s))ᶜ := by grind
      _ ⊆ closure s ∪ (interior (closure s))ᶜ := by gcongr; exact interior_subset
      _ ⊆ closure (p '' f n) ∪ (interior (closure s))ᶜ := union_subset_union
          (closure_minimal (hp.continuous.range_subset_closure_image_dense (hdf n))
          isClosed_closure) (subset_refl (interior (closure s))ᶜ)
      _ ⊆ closure (p '' f n) ∪ closure ((closure s)ᶜ) := union_subset_union (by simp) (by simp)
      _ = closure (c n) := closure_union.symm
    grind
  have c_inter_dense : Dense (⋂ n, c n) := dense_iInter_of_isOpen_nat c_open c_dense
  have c_inter_eq : ⋂ n, f n = p ⁻¹' (⋂ n, c n) := by
    ext x
    simp only [mem_iInter, mem_preimage, mem_union, mem_compl_iff, c]
    refine ⟨fun h i => by grind, fun h i => ?_⟩
    exact hp.injective.mem_set_image.mp (imp_iff_or_not.mpr (h i)
      (subset_closure (mem_range_self x)))
  exact c_inter_eq ▸ Dense.preimage c_inter_dense hp.isOpenMap

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_sub : w ○ w ⊆ s
this : SetRel.symmetrize w ⊆ w
⊢ SetRel.symmetrize w ○ SetRel.symmetrize w ⊆ w ○ w

Tactic:
by gcongr

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SetRel.IsSymm w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SetRel.IsSymm t
t_sub : t ○ t ⊆ w
this : t ⊆ t ○ t
⊢ t ○ t ○ t ⊆ w ○ (t ○ t)

Tactic:
by gcongr

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SetRel.IsSymm w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SetRel.IsSymm t
t_sub : t ○ t ⊆ w
this : t ⊆ t ○ t
⊢ w ○ (t ○ t) ⊆ w ○ w

Tactic:
by gcongr

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 : α
⊢ (𝓝 x).HasBasis p fun i ↦ {y | (y, x) ∈ s i}

Tactic:
replace h := h.comap Prod.swap

Goal state after:
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → SetRel α α
x : α
h : (comap Prod.swap (𝓤 α)).HasBasis p fun i ↦ Prod.swap ⁻¹' s i
⊢ (𝓝 x).HasBasis p fun i ↦ {y | (y, x) ∈ s i}
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
s t : Set α
hs : IsComplete s
ht : IsComplete t
⊢ IsComplete (s ∪ t)

Tactic:
by
  simp only [isComplete_iff_ultrafilter', Ultrafilter.union_mem_iff, or_imp] at *
  exact fun l hl =>
    ⟨fun hsl => (hs l hl hsl).imp fun x hx => ⟨Or.inl hx.1, hx.2⟩, fun htl =>
      (ht l hl htl).imp fun x hx => ⟨Or.inr hx.1, hx.2⟩⟩

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
t : SetRel α α
x✝¹ x✝ : Set (α × α)
hV : x✝¹ ⊆ x✝
⊢ x✝¹ ○ t ○ x✝¹ ⊆ x✝ ○ t ○ x✝

Tactic:
by gcongr

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

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

Tactic:
x

Goal state after:
case mp
α : Type ua
inst✝ : UniformSpace α
s : Set α
h : ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s
x : α
⊢ x ∈ s → ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s
Module: Mathlib.Topology.UniformSpace.Basic

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

Tactic:
x

Goal state after:
case mpr
α : Type ua
inst✝ : UniformSpace α
s : Set α
h : ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s
x : α
⊢ x ∈ s → ∃ V ∈ 𝓤 α, ball x V ⊆ s
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)
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
let S (b : Bool) : Set α := b.casesOn (false := s) (true := t)

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
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
p : ι → Prop
U : ι → SetRel α α
H : (𝓤 α).HasBasis p U
f : Filter α
x✝³ x✝² : Set (α × α)
x✝¹ : x✝³ ⊆ x✝²
h : ∃ t, t.Finite ∧ SetRel.preimage x✝³ t ∈ f
x✝ : Set α
ht : x✝.Finite ∧ SetRel.preimage x✝³ x✝ ∈ f
⊢ SetRel.preimage x✝³ x✝ ⊆ SetRel.preimage x✝² x✝

Tactic:
by gcongr

Goal state after: