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

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
ι : Type u_1
I : Set ι
s : ι → Set α
H : ∀ i ∈ I, IsOpen[t] (s i)
⊢ ∃ s_1, (Subtype.val '' s_1).Countable ∧ ⋃ y ∈ s_1, s ↑y = ⋃ i ∈ I, s i

Tactic:
rcases isOpen_iUnion_countable (fun i : I ↦ s i) fun i ↦ H i i.2 with ⟨T, hTc, hU⟩

Goal state after:
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
ι : Type u_1
I : Set ι
s : ι → Set α
H : ∀ i ∈ I, IsOpen[t] (s i)
T : Set ↑I
hTc : T.Countable
hU : ⋃ i ∈ T, s ↑i = ⋃ i, s ↑i
⊢ ∃ s_1, (Subtype.val '' s_1).Countable ∧ ⋃ y ∈ s_1, s ↑y = ⋃ i ∈ I, s i
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
t : Set ↑s
ht : IsClosed[instTopologicalSpaceSubtype] t
hs : IsClosed[inst✝] s
⊢ IsClosed[inst✝] (Subtype.val '' t)

Tactic:
rcases isClosed_induced_iff.mp ht with ⟨s', hs', rfl⟩

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed[inst✝] s
s' : Set X
hs' : IsClosed[inst✝] s'
ht : IsClosed[instTopologicalSpaceSubtype] (s ↓∩ s')
⊢ IsClosed[inst✝] (Subtype.val '' s ↓∩ s')
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_4
l : Filter α
p : Set α → Prop
hp : ∀ ⦃s t : Set α⦄, s ⊆ t → p s → p t
⊢ (∃ᶠ (s : Set α) in l.smallSets, p s) ↔ ∀ t ∈ l, p t

Tactic:
convert! not_iff_not.mpr <| l.eventually_smallSets' (p := (¬p ·)) (by tauto)

Goal state after:
case e'_2
α : Type u_4
l : Filter α
p : Set α → Prop
hp : ∀ ⦃s t : Set α⦄, s ⊆ t → p s → p t
⊢ (∀ t ∈ l, p t) ↔ ¬∃ s ∈ l, ¬p s
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
⊢ IsCompact (f ⁻¹' (s ∩ Z))

Tactic:
hf.isCompact_preimage_iff

Goal state after:
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
⊢ IsCompact (s ∩ Z)

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 ⊆ range f
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : IsCompact s
ht : IsCompact t
⊢ 𝓝ˢ (s ×ˢ t) = 𝓝ˢ s ×ˢ 𝓝ˢ t

Tactic:
simp_rw [hs.nhdsSet_prod_eq_biSup, ht.prod_nhdsSet_eq_biSup, nhdsSet, sSup_image, biSup_prod,
    nhds_prod_eq]

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case hg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure[inst✝²] {a | p a})
hg : ContinuousOn g (s ∩ closure[inst✝²] {a | ¬p a})
⊢ ContinuousOn g (s ∩ {a | ¬p a})

Tactic:
exact hg.mono (inter_subset_inter_right s subset_closure)

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: α : 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 (t.piecewise f g) (t.ite s s')

Tactic:
apply ContinuousOn.piecewise
  · rwa [ite_inter_of_inter_eq _ H]
  · rwa [ite_inter_closure_eq_of_inter_frontier_eq H]
  · rwa [ite_inter_closure_compl_eq_of_inter_frontier_eq H]

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case refine_1.empty
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsIrreducible s
hu : ∀ u ∈ ∅, IsOpen[inst✝] u
hU : ∀ u ∈ ∅, (s ∩ u).Nonempty
⊢ (s ∩ ⋂₀ ↑∅).Nonempty

Tactic:
| empty =>

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
hs : s.Finite
⊢ IsClosed[inst✝¹] (⋃ x ∈ s, {x})

Tactic:
exact hs.isClosed_biUnion fun i _ => isClosed_singleton

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

Goal state before:
pp: case inr
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
x✝¹ : X × X
x y : X
x✝ : (x, y) ∈ s ×ˢ s
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ s
hne : x ≠ y
⊢ ∀ᶠ (z : X × X) in 𝓝 (x, y), f z.1 ≠ f z.2

Tactic:
refine (fc x hx).prodMap' (fc y hy) <| isClosed_diagonal.isOpen_compl.mem_nhds ?_

Goal state after:
case inr
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
x✝¹ : X × X
x y : X
x✝ : (x, y) ∈ s ×ˢ s
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ s
hne : x ≠ y
⊢ Prod.map f f (x, y) ∈ (diagonal Y)ᶜ
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
⊢ T2Space (T2Quotient X)

Tactic:
t2Space_iff

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
⊢ Pairwise fun x y ↦ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
Module: Mathlib.Order.SuccPred.Relation

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

Tactic:
revert h

Goal state after:
α : 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
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
⊢ [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 4 → 2 := by
    intro h x
    rw [← CofiniteTopology.of.preimage_image {x}]
    exact (Set.Finite.isClosed <| by simp) |>.preimage h

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
tfae_4_to_2 : Continuous[inst✝, _] ⇑CofiniteTopology.of → ∀ (x : X), IsClosed[inst✝] {x}
⊢ [T1Space X, ∀ (x : X), IsClosed[inst✝] {x}, ∀ (x : X), IsOpen[inst✝] {x}ᶜ, Continuous[inst✝, _] ⇑CofiniteTopology.of,
      ∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x, ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s,
      ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ y ∉ U, ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : X⦄, x ⤳ y → x = y, T0Space X ∧ R0Space X].TFAE
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
⊢ (𝓝 x).ker = {x}

Tactic:
simp [ker_nhds_eq_specializes]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
⊢ 𝓝ˢ s ≤ 𝓝ˢ t → s ⊆ t

Tactic:
simp_rw [Filter.le_def]

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

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

Tactic:
| empty =>

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case a
X : Type u_1
inst✝ : TopologicalSpace X
p : X
s : Set X
hs : Disjoint (𝓝[s] p) cofinite
⊢ 𝓟 ({x | x ⤳ p} ∩ s) ≤ 𝓝[s] p

Tactic:
rw [← inf_principal, nhdsWithin]
    gcongr
    rw [Filter.principal_le_iff]
    exact fun s hs x hx ↦ mem_of_mem_nhds (hx hs)

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

Goal state before:
pp: case empty
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
ι : Type u_3
s : Set X
hs : IsCompact s
U : ι → Set X
hU : ∀ i ∈ ∅, IsOpen[inst✝¹] (U i)
hsC : s ⊆ ⋃ i ∈ ∅, U i
⊢ ∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ ∅, K i

Tactic:
| empty =>

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:
by
  simp only [isClosed_iff_clusterPt, clusterPt_principal_iff_frequently]
  exact fun g hg => monotoneOn_of_frequently_monotoneOn_of_tendsto hg
    fun x _ ↦ continuousAt_apply x g

Goal state after:
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
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
this : Encodable ↑S
⊢ ⋃ x, s ↑x ⋯ ≤ᶠ[l] ⋃ x, t ↑x ⋯

Tactic:
exact EventuallyLE.countable_iUnion fun i => h i i.2

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

Goal state before:
pp: case refine_1.inr
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h : LocallyConnectedSpace ((i : ι) → X i)
x : (i : ι) → X i
this : ∀ (i : ι), Nonempty (X i)
hVn : ∃ I, I.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ 𝓝 (x i)) ∧ I.pi t ⊆ connectedComponent x
⊢ {i | ¬PreconnectedSpace (X i)}.Finite

Tactic:
obtain ⟨J, hJ, t, ht, htV⟩ := hVn

Goal state after:
case refine_1.inr
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h : LocallyConnectedSpace ((i : ι) → X i)
x : (i : ι) → X i
this : ∀ (i : ι), Nonempty (X i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htV : J.pi t ⊆ connectedComponent x
⊢ {i | ¬PreconnectedSpace (X i)}.Finite
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: α : Type u_2
g : Set (Set α)
⊢ IsGreatest {f | CountableInterFilter f ∧ g ⊆ f.sets} (countableGenerate g)

Tactic:
refine ⟨⟨inferInstance, fun s => CountableGenerateSets.basic⟩, ?_⟩

Goal state after:
α : Type u_2
g : Set (Set α)
⊢ countableGenerate g ∈ upperBounds {f | CountableInterFilter f ∧ g ⊆ f.sets}
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_1.empty
α : Type u
inst✝ : TopologicalSpace α
s : Set α
x✝ : s.Nonempty ∧ ∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
hne : s.Nonempty
h : ∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
hU : ∀ (u v : Set α), u ∈ ∅ → v ∈ ∅ → (s ∩ (u ∩ v)).Nonempty → u = v
hUo : ∀ u ∈ ∅, IsOpen[inst✝] u
hsU : s ⊆ ⋃₀ ↑∅
⊢ ∃ u ∈ ∅, s ⊆ u

Tactic:
| empty =>

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

Goal state before:
pp: case empty
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : univ.pi s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ univ.pi s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ univ.pi s
hgv : g ∈ v
hI : ∅.piecewise f g ∈ u
⊢ (univ.pi s ∩ (u ∩ v)).Nonempty

Tactic:
| empty =>

Goal state after:
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
s t : Set X
hd₁ : Disjoint (closure[inst✝²] s) t
hd₂ : Disjoint s (closure[inst✝²] t)
⊢ Disjoint (comap e (𝓝ˢ (e '' s))) (comap e (𝓝ˢ (e '' t)))

Tactic:
refine disjoint_comap (completely_normal ?_ ?_)

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

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

Goal state before:
pp: case mp.refine_1
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : Y → ι
h₁ : IsLindelof (⋃ i, (b ∘ f') i)
h₂ : IsOpen[inst✝] (⋃ i, (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ ⋃ i, (b ∘ f') i ⊆ ⋃ i ∈ t, (b ∘ f') i
⊢ ⋃ i ∈ t, (b ∘ f') i ⊆ ⋃ i ∈ f' '' t, b i

Tactic:
simp only [Set.iUnion_subset_iff]

Goal state after:
case mp.refine_1
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : Y → ι
h₁ : IsLindelof (⋃ i, (b ∘ f') i)
h₂ : IsOpen[inst✝] (⋃ i, (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ ⋃ i, (b ∘ f') i ⊆ ⋃ i ∈ t, (b ∘ f') i
⊢ ∀ i ∈ t, (b ∘ f') i ⊆ ⋃ i ∈ f' '' t, b i
Module: Mathlib.Topology.Connected.Basic

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

Tactic:
· exact ⟨by rw [← h (Classical.choice hα)]; exact isPreconnected_connectedComponent⟩

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
⊢ IsLindelof s ↔ IsLindelof (f '' s)

Tactic:
by
  refine ⟨fun hs => hs.image hf.continuous, fun hs F F_ne_bot _ F_le => ?_⟩
  obtain ⟨_, ⟨x, x_in : x ∈ s, rfl⟩, hx : ClusterPt (f x) (map f F)⟩ :=
    hs ((map_mono F_le).trans_eq map_principal)
  exact ⟨x, x_in, hf.mapClusterPt_iff.1 hx⟩

Goal state after:
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
f : α → β
hf : IsDenseInducing f
T : Set β
i : ι
hi : p i
hi' : closure[inst✝¹] (f '' s i) ⊆ T
h : s i ∈ 𝓝 x
⊢ closure[inst✝¹] (f '' s i) ∈ 𝓝 (f x)

Tactic:
exact hf.closure_image_mem_nhds h

Goal state after:
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : (𝓝 x).HasBasis p s
f : α → β
hf : IsDenseInducing f
⊢ (𝓝 (f x)).HasBasis p fun i ↦ closure[inst✝¹] (f '' s i)

Tactic:
rw [Filter.hasBasis_iff] at h ⊢
  intro T
  refine ⟨fun hT => ?_, fun hT => ?_⟩
  · obtain ⟨T', hT₁, hT₂, hT₃⟩ := exists_mem_nhds_isClosed_subset hT
    have hT₄ : f ⁻¹' T' ∈ 𝓝 x := by
      rw [hf.isInducing.nhds_eq_comap x]
      exact ⟨T', hT₁, Subset.rfl⟩
    obtain ⟨i, hi, hi'⟩ := (h _).mp hT₄
    exact
      ⟨i, hi,
        (closure_mono (image_mono hi')).trans
          (Subset.trans (closure_minimal (image_preimage_subset _ _) hT₂) hT₃)⟩
  · obtain ⟨i, hi, hi'⟩ := hT
    suffices closure (f '' s i) ∈ 𝓝 (f x) by filter_upwards [this] using hi'
    replace h := (h (s i)).mpr ⟨i, hi, Subset.rfl⟩
    exact hf.closure_image_mem_nhds h

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x : α
⊢ x ∈ connectedComponent x

Tactic:
exact mem_connectedComponent

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

Goal state before:
pp: case empty
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
h : ∀ s ∈ ∅, IsGδ s
⊢ IsGδ (⋃₀ ∅)

Tactic:
| empty =>

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

Goal state before:
pp: case empty
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (Set X)
ho : ∀ t ∈ ∅, IsOpen[inst✝] t
hd : ∀ t ∈ ∅, Dense t
⊢ Dense (⋂₀ ∅)

Tactic:
| empty =>

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Nonempty X
s : Set X
hs : IsGδ s
hd : Dense s
h : IsMeagre s
t : Set X
hts : t ⊆ sᶜ
htG : IsGδ t
hd' : Dense t
⊢ False

Tactic:
rcases (hd.inter_of_Gδ hs htG hd').nonempty with ⟨x, hx₁, hx₂⟩

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Nonempty X
s : Set X
hs : IsGδ s
hd : Dense s
h : IsMeagre s
t : Set X
hts : t ⊆ sᶜ
htG : IsGδ t
hd' : Dense t
x : X
hx₁ : x ∈ s
hx₂ : x ∈ t
⊢ False
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : Infinite (ConnectedComponents α)
h✝ : Nonempty α
n : ℕ
U : Fin (n + 1) → Set α
h₁ : ∀ (i : Fin (n + 1)), IsClopen (U i)
h₂ : ∀ (i : Fin (n + 1)), (U i).Nonempty
h₃ : Pairwise (Disjoint on U)
h₄ : ⋃ i, U i = univ
⊢ ∃ i, ¬IsConnected (U i)

Tactic:
simp_rw [isConnected_iff_connectedSpace, ← not_forall]
      exact fun _ ↦ not_finite_iff_infinite.mpr ‹_› (.of_equiv _ (equivOfIsClopen h₁ h₃ h₄).symm)

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

Goal state before:
pp: β : Type v
ι : Sort u_1
inst✝ : Nonempty ι
u : ι → UniformSpace β
l : Filter β
⊢ Cauchy l ↔ ∀ (i : ι), Cauchy l

Tactic:
unfold Cauchy
  rw [iInf_uniformity, le_iInf_iff, forall_and, forall_const]

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

Goal state before:
pp: case mp
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h : ∀ V ∈ 𝓤 α, ∃ N, ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
V : Set (α × α)
mV : V ∈ 𝓤 α
⊢ ∃ N, ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V

Tactic:
obtain ⟨N, h⟩ := h V mV

Goal state after:
case mp
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h✝ : ∀ V ∈ 𝓤 α, ∃ N, ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
V : Set (α × α)
mV : V ∈ 𝓤 α
N : ℕ
h : ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
⊢ ∃ N, ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
g : α → β
hf :
  ∀ (i : SetRel β β),
    i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, (f x.2, F x.1 x.2) ∈ id i
hfg : ∀ x ∈ s, Inseparable (f x) (g x)
⊢ ∀ (i : SetRel β β),
    i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, (g x.2, F x.1 x.2) ∈ id i

Tactic:
refine forall₂_imp (fun i hi hf => ?_) hf

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
g : α → β
hf✝ :
  ∀ (i : SetRel β β),
    i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, (f x.2, F x.1 x.2) ∈ id i
hfg : ∀ x ∈ s, Inseparable (f x) (g x)
i : SetRel β β
hi : i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i
hf : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, (f x.2, F x.1 x.2) ∈ id i
⊢ ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, (g x.2, F x.1 x.2) ∈ id i
Module: Mathlib.Topology.UniformSpace.Separation

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

Tactic:
obtain ⟨U, hUu, hU⟩ := UniformSpace.mem_nhds_iff.1 (nhds_le_nhdsSet x.2 hST)

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
b : Bool
x : ↑(S b)
hST : (S !b)ᶜ ∈ 𝓝ˢ (S b)
U : Set (α × α)
hUu : U ∈ 𝓤 α
hU : ball (↑x) U ⊆ (S !b)ᶜ
⊢ ∃ i, Disjoint (ball (↑x) ((B i).comp (B i).inv)) (S !b)
Module: Mathlib.Topology.UniformSpace.Compact

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : SetRel α β
hs : IsClosed s
t : Set β
ht : IsCompact t
⊢ IsClosed (s.preimage t)

Tactic:
rw [← isOpen_compl_iff, isOpen_iff_eventually] at hs ⊢

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : SetRel α β
hs : ∀ x ∈ sᶜ, ∀ᶠ (y : α × β) in nhds x, y ∈ sᶜ
t : Set β
ht : IsCompact t
⊢ ∀ x ∈ (s.preimage t)ᶜ, ∀ᶠ (y : α) in nhds x, y ∈ (s.preimage t)ᶜ
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : One β
f : α → β
inst✝ : TopologicalSpace β
K : Set β
h'f : HasCompactMulSupport f
hf : Continuous[inst✝², inst✝] f
hk : IsClosed[inst✝] K
h'k : 1 ∉ K
⊢ IsCompact (f ⁻¹' K)

Tactic:
by
  apply IsCompact.of_isClosed_subset h'f (hk.preimage hf) (fun x hx ↦ ?_)
  apply subset_mulTSupport
  aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
hs : IsCompact s
⊢ TendstoLocallyUniformlyOn F f p s ↔ TendstoUniformlyOn F f p s

Tactic:
have : CompactSpace s := isCompact_iff_compactSpace.mp hs

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
hs : IsCompact s
this : CompactSpace ↑s
⊢ TendstoLocallyUniformlyOn F f p s ↔ TendstoUniformlyOn F f p s