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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : ∀ (U : Set X), IsOpen[inst✝] U → U.Nonempty → (U ∩ s).Nonempty
u : Set ↑s
hud : ∀ (U : Set ↑s), IsOpen[instTopologicalSpaceSubtype] U → U.Nonempty → (U ∩ u).Nonempty
v : Set X
hv1 : IsOpen[inst✝] v
hv2 : Subtype.val ⁻¹' v = u
t : Set X
ht : IsOpen[inst✝] t
ht' : t.Nonempty
⊢ (t ∩ v).Nonempty

Tactic:
subst hv2

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : ∀ (U : Set X), IsOpen[inst✝] U → U.Nonempty → (U ∩ s).Nonempty
v : Set X
hv1 : IsOpen[inst✝] v
t : Set X
ht : IsOpen[inst✝] t
ht' : t.Nonempty
hud : ∀ (U : Set ↑s), IsOpen[instTopologicalSpaceSubtype] U → U.Nonempty → (U ∩ Subtype.val ⁻¹' v).Nonempty
⊢ (t ∩ v).Nonempty
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.Compactness.LocallyCompact

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactPair X Y
f : X → Y
K : Set X
U : Set Y
hf : Continuous[inst✝², inst✝¹] f
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hKU : MapsTo f K U
⊢ ∃ L ∈ 𝓝ˢ K, IsCompact L ∧ MapsTo f L U

Tactic:
choose! V hxV hVc hVU using fun x (hx : x ∈ K) ↦
    exists_mem_nhds_isCompact_mapsTo hf (hU.mem_nhds (hKU hx))

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactPair X Y
f : X → Y
K : Set X
U : Set Y
hf : Continuous[inst✝², inst✝¹] f
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hKU : MapsTo f K U
V : X → Set X
hxV : ∀ x ∈ K, V x ∈ 𝓝 x
hVc : ∀ x ∈ K, IsCompact (V x)
hVU : ∀ x ∈ K, MapsTo f (V x) U
⊢ ∃ L ∈ 𝓝ˢ K, IsCompact L ∧ MapsTo f L U
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Nonempty ι
V : ι → Set X
hV : Directed (fun x1 x2 ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst✝¹] (V i)
U : Set X
hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x
⊢ ∃ i, V i ⊆ U

Tactic:
by
  obtain ⟨W, hsubW, W_op, hWU⟩ := exists_open_set_nhds hU
  suffices ∃ i, V i ⊆ W from this.imp fun i hi => hi.trans hWU
  by_contra! H
  replace H : ∀ i, (V i ∩ Wᶜ).Nonempty := fun i => Set.inter_compl_nonempty_iff.mpr (H i)
  have : (⋂ i, V i ∩ Wᶜ).Nonempty := by
    refine
      IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed _ (fun i j => ?_) H
        (fun i => (hV_cpct i).inter_right W_op.isClosed_compl) fun i =>
        (hV_closed i).inter W_op.isClosed_compl
    rcases hV i j with ⟨k, hki, hkj⟩
    refine ⟨k, ⟨fun x => ?_, fun x => ?_⟩⟩ <;> simp only [and_imp, mem_inter_iff, mem_compl_iff] <;>
      tauto
  have : ¬⋂ i : ι, V i ⊆ W := by simpa [← iInter_inter, inter_compl_nonempty_iff]
  contradiction

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

Goal state before:
pp: X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
f : ι → X
x : X
this : TopologicalSpace ι := ⊥
hf : Tendsto f (cocompact ι) (𝓝 x)
h : DiscreteTopology ι
⊢ IsCompact (insert x (range f))

Tactic:
exact hf.isCompact_insert_range_of_cocompact continuous_of_discreteTopology

Goal state after:
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
⊢ Continuous[_, inst✝] (uncurry (lift₂ f hf)) ↔ Continuous[instTopologicalSpaceProd, inst✝] (uncurry f)

Tactic:
simp only [← continuousOn_univ, continuousOn_lift₂, preimage_univ]

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 : IsOpen[inst✝¹] s
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen[inst✝¹] t → t = s
⊢ s.Subsingleton

Tactic:
refine fun x hx y hy => of_not_not fun hxy => ?_
  rcases exists_isOpen_xor_mem hxy with ⟨U, hUo, hU⟩
  wlog h : x ∈ U ∧ y ∉ U
  · exact this hs hmin y hy x hx (Ne.symm hxy) U hUo hU.symm (hU.resolve_left h)
  obtain ⟨hxU, hyU⟩ := h
  have : s ∩ U = s := hmin (s ∩ U) inter_subset_left ⟨x, hx, hxU⟩ (hs.inter hUo)
  exact hyU (this.symm.subset hy).2

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsDiscrete s
hf : ContinuousOn f (f ⁻¹' s)
hf' : Injective f
x : X
hx : x ∈ f ⁻¹' s
⊢ map f (𝓝[f ⁻¹' s] x) ≤ 𝓝[s] f x

Tactic:
← Tendsto

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsDiscrete s
hf : ContinuousOn f (f ⁻¹' s)
hf' : Injective f
x : X
hx : x ∈ f ⁻¹' s
⊢ Tendsto f (𝓝[f ⁻¹' s] x) (𝓝[s] f x)
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
hy : x ≠ y
⊢ 𝓝[≠] x ≤ 𝓝 x

Tactic:
exact nhdsWithin_le_nhds

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ (U : Set X), IsOpen[inst✝] U → (S ∩ U).Nonempty → S ⊆ closure[inst✝] (S ∩ U)
a b : Set X
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
p : X
pS : p ∈ S
pa : p ∈ a
bS : (S ∩ b).Nonempty
h0 : S ∩ (a ∩ b) = ∅
⊢ ∃ x, IsClosed[inst✝] x ∧ S ∩ b ⊆ x ∧ p ∉ x

Tactic:
use aᶜ

Goal state after:
case h
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ (U : Set X), IsOpen[inst✝] U → (S ∩ U).Nonempty → S ⊆ closure[inst✝] (S ∩ U)
a b : Set X
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
p : X
pS : p ∈ S
pa : p ∈ a
bS : (S ∩ b).Nonempty
h0 : S ∩ (a ∩ b) = ∅
⊢ IsClosed[inst✝] aᶜ ∧ S ∩ b ⊆ aᶜ ∧ p ∉ aᶜ
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
⊢ IsOpen[inst✝²] U ↔ ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ ↑F

Tactic:
isOpen_iff_ultrafilter

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s t : Set X
f : X → Y
hf₁ : Continuous[inst✝¹, inst✝] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
W : ↑(irreducibleComponents X)
x : X
hx : x ∈ ↑W
⊢ (f ⁻¹' f '' ↑W).Nonempty

Tactic:
exact ⟨_, x, hx, rfl⟩

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case h.left
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
U s : Set X
hs : Finite ↑s
t : Set X
ht : IsOpen[inst✝¹] t
h₁ts : x ∈ t
h₂ts : t ∩ {x}ᶜ ⊆ U
⊢ IsOpen[inst✝¹] (t \ (s \ {x}))

Tactic:
rw [← isClosed_compl_iff, compl_sdiff]
    exact s.toFinite.sdiff.isClosed.union (isClosed_compl_iff.2 ht)

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsEmbedding f
s : Set X
⊢ s ∈ codiscreteWithin univ ↔ s ∈ codiscrete X

Tactic:
codiscrete

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsEmbedding f
s : Set X
⊢ s ∈ codiscreteWithin univ ↔ s ∈ codiscreteWithin univ
Module: Mathlib.Topology.Clopen

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hab : Disjoint a b
⊢ IsClopen (s ∩ a)

Tactic:
refine ⟨?_, IsOpen.inter h.2 ha⟩
  have : IsClosed (s ∩ bᶜ) := IsClosed.inter h.1 (isClosed_compl_iff.2 hb)
  convert! this using 1
  refine (inter_subset_inter_right s hab.subset_compl_right).antisymm ?_
  rintro x ⟨hx₁, hx₂⟩
  exact ⟨hx₁, by simpa [notMem_of_mem_compl hx₂] using cover hx₁⟩

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
s : ι → Set α
hs : IsPreconnected (⋃ n, s n)
hs' : ∀ (i : ι), IsOpen[inst✝] (s i)
i j : ι
hi : (s i).Nonempty
hj : (s j).Nonempty
hij : ¬TransGen (fun a b ↦ (s a ∩ s b).Nonempty) i j
⊢ False

Tactic:
let S : Set ι := {k | TransGen (fun a b ↦ (s a ∩ s b).Nonempty) i k}

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
s : ι → Set α
hs : IsPreconnected (⋃ n, s n)
hs' : ∀ (i : ι), IsOpen[inst✝] (s i)
i j : ι
hi : (s i).Nonempty
hj : (s j).Nonempty
hij : ¬TransGen (fun a b ↦ (s a ∩ s b).Nonempty) i j
S : Set ι := {k | TransGen (fun a b ↦ (s a ∩ s b).Nonempty) i k}
⊢ False
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: case neg
ι : Type u_1
X : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyConnectedSpace (X i)
hfinite : {i | ¬PreconnectedSpace (X i)}.Finite
x : (i : ι) → X i
U : Set ((i : ι) → X i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htU : J.pi t ⊆ U
K : Set ι := J ∪ {i | ¬PreconnectedSpace (X i)}
i : ι
hi : i ∉ K
⊢ IsPreconnected (K.piecewise (fun i ↦ connectedComponentIn (t i) (x i)) (fun x ↦ univ) i)

Tactic:
piecewise_eq_of_notMem _ _ _ hi

Goal state after:
case neg
ι : Type u_1
X : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyConnectedSpace (X i)
hfinite : {i | ¬PreconnectedSpace (X i)}.Finite
x : (i : ι) → X i
U : Set ((i : ι) → X i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htU : J.pi t ⊆ U
K : Set ι := J ∪ {i | ¬PreconnectedSpace (X i)}
i : ι
hi : i ∉ K
⊢ IsPreconnected univ
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_1
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) × X i)
hs : IsConnected s
⊢ ∃ i t, IsConnected t ∧ s = mk i '' t

Tactic:
obtain ⟨⟨i, x⟩, hx⟩ := hs.nonempty
    have : s ⊆ range (Sigma.mk i) :=
      hs.isPreconnected.subset_isClopen isClopen_range_sigmaMk ⟨⟨i, x⟩, hx, x, rfl⟩
    exact ⟨i, Sigma.mk i ⁻¹' s, hs.preimage_of_isOpenMap sigma_mk_injective isOpenMap_sigmaMk this,
      (Set.image_preimage_eq_of_subset this).symm⟩

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

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β✝ : Type u_3
l✝ : Filter α✝
inst✝² : CountableInterFilter l✝
α : Type u_4
β : Type u_5
l : Filter α
m : Filter β
inst✝¹ : CountableInterFilter l
inst✝ : CountableInterFilter m
⊢ ∀ (S : Set (Set (α × β))), S.Countable → (∀ s ∈ S, s ∈ l.curry m) → ⋂₀ S ∈ l.curry m

Tactic:
intro S Sct hS
  simp_rw [mem_curry_iff, mem_sInter, eventually_countable_ball (p := fun _ _ _ => (_, _) ∈ _) Sct,
    eventually_countable_ball (p := fun _ _ _ => ∀ᶠ (_ : β) in m, _)  Sct, ← mem_curry_iff]
  exact hS

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

Goal state before:
pp: case refine_2.inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
t : Set β
ht : IsConnected t
⊢ IsConnected (inr '' t)

Tactic:
exact ht.image _ continuous_inr.continuousOn

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

Goal state before:
pp: case refine_2.inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
t : Set β
ht : IsPreconnected t
⊢ IsPreconnected (inr '' t)

Tactic:
exact ht.image _ continuous_inr.continuousOn

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

Goal state before:
pp: α : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_open : ∀ (i : ι), IsOpen[inst✝¹] (s i)
h_Union : ⋃ i, s i = univ
i j : ι
⊢ IsOpen[inst✝¹] (s j \ s i)

Tactic:
rcases eq_or_ne i j with rfl | h_ne

Goal state after:
case inl
α : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_open : ∀ (i : ι), IsOpen[inst✝¹] (s i)
h_Union : ⋃ i, s i = univ
i : ι
⊢ IsOpen[inst✝¹] (s i \ s i)

case inr
α : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_open : ∀ (i : ι), IsOpen[inst✝¹] (s i)
h_Union : ⋃ i, s i = univ
i j : ι
h_ne : i ≠ j
⊢ IsOpen[inst✝¹] (s j \ s i)
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
ι : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
inst✝ : Finite ι
h_closed : ∀ (i : ι), IsClosed[inst✝²] (s i)
h_Union : ⋃ i, s i = univ
i j : ι
⊢ IsClosed[inst✝²] (s j \ s i)

Tactic:
rcases eq_or_ne i j with rfl | h_ne

Goal state after:
case inl
α : Type u
ι : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
inst✝ : Finite ι
h_closed : ∀ (i : ι), IsClosed[inst✝²] (s i)
h_Union : ⋃ i, s i = univ
i : ι
⊢ IsClosed[inst✝²] (s i \ s i)

case inr
α : Type u
ι : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
inst✝ : Finite ι
h_closed : ∀ (i : ι), IsClosed[inst✝²] (s i)
h_Union : ⋃ i, s i = univ
i j : ι
h_ne : i ≠ j
⊢ IsClosed[inst✝²] (s j \ s i)
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case refine_1
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
t : Set β
hs : IsPreconnected s
ht : IsPreconnected t
a₁ : α
b₁ : β
ha₁ : (a₁, b₁).1 ∈ s
hb₁ : (a₁, b₁).2 ∈ t
a₂ : α
b₂ : β
ha₂ : (a₂, b₂).1 ∈ s
hb₂ : (a₂, b₂).2 ∈ t
⊢ Prod.mk a₁ '' t ∪ flip Prod.mk b₂ '' s ⊆ s ×ˢ t

pp: case refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
t : Set β
hs : IsPreconnected s
ht : IsPreconnected t
a₁ : α
b₁ : β
ha₁ : (a₁, b₁).1 ∈ s
hb₁ : (a₁, b₁).2 ∈ t
a₂ : α
b₂ : β
ha₂ : (a₂, b₂).1 ∈ s
hb₂ : (a₂, b₂).2 ∈ t
⊢ IsPreconnected (Prod.mk a₁ '' t ∪ flip Prod.mk b₂ '' s)

Tactic:
· rintro _ (⟨y, hy, rfl⟩ | ⟨x, hx, rfl⟩)
    exacts [⟨ha₁, hy⟩, ⟨hx, hb₂⟩]

Goal state after:
case refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
t : Set β
hs : IsPreconnected s
ht : IsPreconnected t
a₁ : α
b₁ : β
ha₁ : (a₁, b₁).1 ∈ s
hb₁ : (a₁, b₁).2 ∈ t
a₂ : α
b₂ : β
ha₂ : (a₂, b₂).1 ∈ s
hb₂ : (a₂, b₂).2 ∈ t
⊢ IsPreconnected (Prod.mk a₁ '' t ∪ flip Prod.mk b₂ '' s)
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : TopologicalSpace Y
f : Y → X
hf : IsInducing f
b : Y
⊢ (𝓝 b).HasBasis (?m.10 b) (?m.11 b)

Tactic:
rw [hf.nhds_eq_comap b]; exact (closed_nhds_basis _).comap _

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 : s ∩ ⋂ i, t i = ∅
U : ι → Set X := ⋯
hUo : ∀ (i : ι), IsOpen[inst✝] (U i)
⊢ Disjoint s (⋂ i, t i)

Tactic:
exact disjoint_iff_inter_eq_empty.mpr hst

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

Goal state before:
pp: X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsLindelof s
hc₁ : ∀ i ∈ b, IsOpen[inst✝] (c i)
hc₂ : s ⊆ ⋃ i ∈ b, c i
⊢ ∃ b' ⊆ b, b'.Countable ∧ s ⊆ ⋃ i ∈ b', c i

Tactic:
simp only [Subtype.forall', biUnion_eq_iUnion] at hc₁ hc₂
  rcases hs.elim_countable_subcover (fun i ↦ c i : b → Set X) hc₁ hc₂ with ⟨d, hd⟩
  refine ⟨Subtype.val '' d, by simp, Countable.image hd.1 Subtype.val, ?_⟩
  rw [biUnion_image]
  exact hd.2

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
⊢ (coclosedLindelof X).HasBasis (fun s ↦ IsClosed[inst✝] s ∧ IsLindelof s) compl

Tactic:
simp only [Filter.coclosedLindelof, iInf_and']

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
⊢ (⨅ s, ⨅ (_ : IsClosed[inst✝] s ∧ IsLindelof s), 𝓟 sᶜ).HasBasis (fun s ↦ IsClosed[inst✝] s ∧ IsLindelof s) compl
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case a
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := ⋯
T₂ : Set β := ⋯
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
⊢ f ⁻¹' T₁ ⊆ f ⁻¹' t ∩ u

Tactic:
rw [← biUnion_preimage_singleton]
      refine iUnion₂_subset fun t' ht' => subset_inter ?_ ht'.2
      rw [hf.preimage_subset_preimage_iff, singleton_subset_iff]
      exact ht'.1

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

Goal state before:
pp: case a
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := ⋯
T₂ : Set β := ⋯
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
⊢ f ⁻¹' T₂ ⊆ f ⁻¹' t ∩ v

Tactic:
rw [← biUnion_preimage_singleton]
      refine iUnion₂_subset fun t' ht' => subset_inter ?_ ht'.2
      rw [hf.preimage_subset_preimage_iff, singleton_subset_iff]
      exact ht'.1

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
⊢ (∀ (x : α), (connectedComponent x).Subsingleton) ↔ ∀ (x : α), connectedComponent x = {x}

Tactic:
refine forall_congr' fun x => ?_

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
x : α
⊢ (connectedComponent x).Subsingleton ↔ connectedComponent x = {x}
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
f : ℕ → Set X
hf : ∀ (n : ℕ), IsOpen[inst✝] (f n)
⊢ IsGδ (⋂ n, f n)

Tactic:
exact .iInter_of_isOpen hf

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

Goal state before:
pp: case inl
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : Infinite (ConnectedComponents α)
n : ℕ
hn : 0 < n
h✝ : IsEmpty α
⊢ ∃ U, (∀ (i : Fin n), IsClopen (U i)) ∧ (∀ (i : Fin n), (U i).Nonempty) ∧ Pairwise (Disjoint on U) ∧ ⋃ i, U i = univ

pp: case inr
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : Infinite (ConnectedComponents α)
n : ℕ
hn : 0 < n
h✝ : Nonempty α
⊢ ∃ U, (∀ (i : Fin n), IsClopen (U i)) ∧ (∀ (i : Fin n), (U i).Nonempty) ∧ Pairwise (Disjoint on U) ∧ ⋃ i, U i = univ

Tactic:
· exact (not_finite (ConnectedComponents α)).elim

Goal state after:
case inr
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : Infinite (ConnectedComponents α)
n : ℕ
hn : 0 < n
h✝ : Nonempty α
⊢ ∃ U, (∀ (i : Fin n), IsClopen (U i)) ∧ (∀ (i : Fin n), (U i).Nonempty) ∧ Pairwise (Disjoint on U) ∧ ⋃ i, U i = univ
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
i : LocallyConnectedSpace Y
h : X ≃ₜ Y
⊢ LocallyConnectedSpace X

Tactic:
have : ∀ x, (𝓝 x).HasBasis (fun s ↦ IsOpen s ∧ h x ∈ s ∧ IsConnected s)
      (h.symm '' ·) := fun x ↦ by
    rw [← h.symm_map_nhds_eq]
    exact (i.1 _).map _

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
i : LocallyConnectedSpace Y
h : X ≃ₜ Y
this : ∀ (x : X), (𝓝 x).HasBasis (fun s ↦ IsOpen[inst✝] s ∧ h x ∈ s ∧ IsConnected s) fun x ↦ ⇑h.symm '' x
⊢ LocallyConnectedSpace X
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
h : ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
⊢ PreconnectedSpace α

Tactic:
refine preconnectedSpace_of_forall_constant fun f hf x y ↦ ?_

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
f : α → Bool
hf : Continuous[inst✝, _] f
x y : α
⊢ f x = f y
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
u₁ u₂ : UniformSpace α
h : 𝓤 α = 𝓤 α
x : α
⊢ 𝓝 x = 𝓝 x

Tactic:
u₁.nhds_eq_comap_uniformity,

Goal state after:
α : Type ua
u₁ u₂ : UniformSpace α
h : 𝓤 α = 𝓤 α
x : α
⊢ comap (Prod.mk x) UniformSpace.uniformity = 𝓝 x
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ i, s i
l : Filter α
⊢ Cauchy l → l ≤ 𝓟 S → ∃ x ∈ S, l ≤ 𝓝 x

Tactic:
hl

Goal state after:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ i, s i
l : Filter α
hl : Cauchy l
⊢ l ≤ 𝓟 S → ∃ x ∈ S, l ≤ 𝓝 x
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
ι : Sort u_2
p : ι → Prop
s : ι → SetRel α α
u : UniformSpace α
h : (𝓤 α).HasBasis p s
⊢ u = ⊥ ↔ ∃ i, p i ∧ Pairwise fun x y ↦ (x, y) ∉ s i

Tactic:
by
  simp [uniformSpace_eq_bot, h.mem_iff, subset_def, Pairwise, not_imp_not]

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 α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
this :
  ∀ᶠ (x : (ι × ι) × α × α) in (p ×ˢ p) ×ˢ p' ×ˢ p',
    (f ((x.1.1, x.2.1), x.1.2, x.2.2).1.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 ((x.1.1, x.2.1), x.1.2, x.2.2).1.2) ∈
        t ∧
      (f ((x.1.1, x.2.1), x.1.2, x.2.2).2.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 ((x.1.1, x.2.1), x.1.2, x.2.2).2.2) ∈
        t
n1 n2 : ι
x : α
⊢ (f x, F n1 x) ∈ t → (f x, F n2 x) ∈ t → (F n1 x, F n2 x) ∈ u

Tactic:
hl

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
this :
  ∀ᶠ (x : (ι × ι) × α × α) in (p ×ˢ p) ×ˢ p' ×ˢ p',
    (f ((x.1.1, x.2.1), x.1.2, x.2.2).1.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 ((x.1.1, x.2.1), x.1.2, x.2.2).1.2) ∈
        t ∧
      (f ((x.1.1, x.2.1), x.1.2, x.2.2).2.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 ((x.1.1, x.2.1), x.1.2, x.2.2).2.2) ∈
        t
n1 n2 : ι
x : α
hl : (f x, F n1 x) ∈ t
⊢ (f x, F n2 x) ∈ t → (F n1 x, F n2 x) ∈ u
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
⊢ IsUniformInducing f ↔ UniformContinuous f ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α

Tactic:
by
  rw [isUniformInducing_iff, UniformContinuous, tendsto_iff_comap, le_antisymm_iff, and_comm]; rfl

Goal state after: