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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClopen s ↔ frontier s = ∅

Tactic:
rw [IsClopen, ← closure_eq_iff_isClosed, ← interior_eq_iff_isOpen, frontier, sdiff_eq_empty]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ closure[inst✝] s = s ∧ interior s = s ↔ closure[inst✝] s ⊆ interior s
Module: Mathlib.Topology.Order.OrderClosed

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

Tactic:
[

Goal state after:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
t : OrderClosedTopology α
inst✝ : Preorder β
⊢ IsClosed[Pi.topologicalSpace] {f | Monotone f}
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case inr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
x : α
H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
xv : x ∈ v
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
| inr xv =>

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

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst✝², inst✝¹] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
⊢ SeparatedNhds {f x} (f '' K \ interior s)

Tactic:
[

Goal state after:
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst✝², inst✝¹] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
⊢ SeparatedNhds {f x} (f '' K \ interior s)
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
f : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝 a)
⊢ Tendsto (fun i ↦ max (f i) a) l (𝓝 a)

Tactic:
[

Goal state after:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
f : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝 a)
⊢ Tendsto (fun i ↦ max (f i) a) l (𝓝 a)
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
f : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝[>] a)
⊢ Tendsto (fun i ↦ max (f i) a) l (𝓝[>] a)

Tactic:
[

Goal state after:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
f : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝[>] a)
⊢ Tendsto (fun i ↦ max (f i) a) l (𝓝[>] a)
Module: Mathlib.Topology.Connected.LocallyConnected

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

Tactic:
[

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
⊢ LocallyConnectedSpace α ↔ ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst✝] V ∧ x ∈ V ∧ IsConnected V
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
S : Set (Set α)
hSc : S.Countable
s : (s : Set α) → s ∈ S → Set α
hs : ∀ (s_1 : Set α) (a : s_1 ∈ S), s s_1 a ∈ l₁
t : (s : Set α) → s ∈ S → Set α
ht : ∀ (s : Set α) (a : s ∈ S), t s a ∈ l₂
hst : ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a
⊢ ⋂₀ S ∈ l₁ ⊓ l₂

Tactic:
replace hs : (⋂ i ∈ S, s i ‹_›) ∈ l₁ := (countable_bInter_mem hSc).2 hs

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
S : Set (Set α)
hSc : S.Countable
s t : (s : Set α) → s ∈ S → Set α
ht : ∀ (s : Set α) (a : s ∈ S), t s a ∈ l₂
hst : ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a
hs : ⋂ i, ⋂ (h : i ∈ S), s i h ∈ l₁
⊢ ⋂₀ S ∈ l₁ ⊓ l₂
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 (α × β))
Sct : S.Countable
hS : ∀ s ∈ S, s ∈ l.curry m
⊢ ⋂₀ S ∈ l.curry m

Tactic:
[

Goal state after:
ι : 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 (α × β))
Sct : S.Countable
hS : ∀ s ∈ S, s ∈ l.curry m
⊢ ⋂₀ S ∈ l.curry m
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: case refine_2.inr
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
hloc : ∀ (i : ι), LocallyConnectedSpace (X i)
hfin : {i | ¬PreconnectedSpace (X i)}.Finite
⊢ LocallyConnectedSpace ((i : ι) → X i)

Tactic:
exact locallyConnectedSpace_of_finite_not_preconnectedSpace hfin

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

Goal state before:
pp: α : Type u_2
g : Set (Set α)
f : Filter α
fct : CountableInterFilter f
hf : g ⊆ f.sets
⊢ f ≤ countableGenerate g

Tactic:
@le_countableGenerate_iff_of_countableInterFilter _ _ _ fct

Goal state after:
α : Type u_2
g : Set (Set α)
f : Filter α
fct : CountableInterFilter f
hf : g ⊆ f.sets
⊢ g ⊆ f.sets
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
x y : α
hx : x ∈ s
hy : y ∈ s
Q : ↑s → ↑s → Prop := fun a b ↦ P ↑a ↑b
this : PreconnectedSpace ↑s
⊢ Q ⟨x, hx⟩ ⟨y, hy⟩

Tactic:
apply PreconnectedSpace.induction₂'

Goal state after:
case h
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
x y : α
hx : x ∈ s
hy : y ∈ s
Q : ↑s → ↑s → Prop := ⋯
this : PreconnectedSpace ↑s
⊢ ∀ (x : { x // x ∈ s }), ∀ᶠ (y : { x // x ∈ s }) in 𝓝 x, Q x y ∧ Q y x

case h'
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
x y : α
hx : x ∈ s
hy : y ∈ s
Q : ↑s → ↑s → Prop := ⋯
this : PreconnectedSpace ↑s
⊢ IsTrans { x // x ∈ s } Q
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case mpr.inl
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ u
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
rcases hsv with ⟨x, hxs, hxv⟩
      exact ⟨x, hxs, ⟨h hxs, hxv⟩⟩

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
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst✝] (U i)
hsU : s ⊆ ⋃ i, U i
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → (∃ r, r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
S : Set (Set X)
hS : S.Countable
hsr : ∀ s ∈ S, ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
⊢ ∃ r, r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i

Tactic:
choose! r hr using hsr

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst✝] (U i)
hsU : s ⊆ ⋃ i, U i
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → (∃ r, r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
S : Set (Set X)
hS : S.Countable
r : Set X → Set ι
hr : ∀ s ∈ S, (r s).Countable ∧ s ⊆ ⋃ i ∈ r s, U i
⊢ ∃ r, r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case inr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hs : ¬(s ∩ (u ∩ v)).Nonempty → ¬(s ∩ v).Nonempty
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
[

Goal state after:
case inr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hs : ¬(s ∩ (u ∩ v)).Nonempty → ¬(s ∩ v).Nonempty
⊢ s ⊆ u ∨ s ⊆ v
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case mpr.inl
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ u
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
rcases hsv with ⟨x, hxs, hxv⟩
      exact ⟨x, hxs, ⟨h hxs, hxv⟩⟩

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
⊢ IsConnected (connectedComponentIn F x) ↔ x ∈ F

Tactic:
[

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
⊢ IsConnected (connectedComponentIn F x) ↔ x ∈ F
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x y : α
F : Set α
h : y ∈ connectedComponentIn F x
hx : x ∈ F
⊢ connectedComponentIn F x = connectedComponentIn F y

Tactic:
[

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
x y : α
F : Set α
h : y ∈ connectedComponentIn F x
hx : x ∈ F
⊢ connectedComponentIn F x = connectedComponentIn F y
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
hx : x ∈ F
y : α
hy : y ∈ F
h2y : ⟨y, hy⟩ ∈ connectedComponent ⟨x, hx⟩
⊢ Subtype.val '' connectedComponent ⟨x, hx⟩ = connectedComponentIn F y

Tactic:
[

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
hx : x ∈ F
y : α
hy : y ∈ F
h2y : ⟨y, hy⟩ ∈ connectedComponent ⟨x, hx⟩
⊢ Subtype.val '' connectedComponent ⟨x, hx⟩ = connectedComponentIn F y
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: X : Type u_3
inst✝ : TopologicalSpace X
u v : Set X
hu : IsClopen (v ↓∩ u)
huv₁ : u ⊆ v
this : u = ⋃ i, ⋃ (x : i ∈ v), ⋃ (_ : i ∈ u), Subtype.val '' connectedComponent ⟨i, ⋯⟩
⊢ u = ⋃ x ∈ u, connectedComponentIn v x

Tactic:
this

Goal state after:
X : Type u_3
inst✝ : TopologicalSpace X
u v : Set X
hu : IsClopen (v ↓∩ u)
huv₁ : u ⊆ v
this : u = ⋃ i, ⋃ (x : i ∈ v), ⋃ (_ : i ∈ u), Subtype.val '' connectedComponent ⟨i, ⋯⟩
⊢ ⋃ i, ⋃ (x : i ∈ v), ⋃ (_ : i ∈ u), Subtype.val '' connectedComponent ⟨i, ⋯⟩ = ⋃ x ∈ u, connectedComponentIn v x
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: case inl
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : HereditarilyLindelofSpace X
ι : Type u_2
inst✝ : Nonempty ι
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst✝²] (U i)
htc : ∅.Countable
htu : ⋃ i ∈ ∅, U i = ⋃ i, U i
⊢ ∃ k, ⋃ n, U (k n) = ⋃ i, U i

Tactic:
[

Goal state after:
case inl
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : HereditarilyLindelofSpace X
ι : Type u_2
inst✝ : Nonempty ι
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst✝²] (U i)
htc : ∅.Countable
htu : ⋃ i ∈ ∅, U i = ⋃ i, U i
⊢ ∃ k, ⋃ n, U (k n) = ⋃ i, U i
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed[inst✝²] (⋂ s, ↑s)
⊢ IsPreconnected (⋂ Z, ↑Z)

Tactic:
rw [isPreconnected_iff_subset_of_fully_disjoint_closed hs]

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed[inst✝²] (⋂ s, ↑s)
⊢ ∀ (u v : Set X), IsClosed[inst✝²] u → IsClosed[inst✝²] v → ⋂ s, ↑s ⊆ u ∪ v → Disjoint u v → ⋂ s, ↑s ⊆ u ∨ ⋂ s, ↑s ⊆ v
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:
by
  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.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : HereditarilyLindelofSpace X
ι : Type u_2
inst✝ : Nonempty ι
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst✝²] (C i)
⊢ ∃ k, ⋂ n, C (k n) = ⋂ i, C i

Tactic:
conv in _ = _ => rw [← compl_inj_iff]; simp
  exact eq_open_union_nat (fun i ↦ (C i)ᶜ) (fun i ↦ (h i).isOpen_compl)

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ S ⊆ {t | IsOpen[inst✝] t ∧ Dense t}, S.Countable ∧ ⋂₀ S ⊆ s) ↔
    ∃ S, (∀ t ∈ S, IsOpen[inst✝] t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ⋂₀ S ⊆ s

Tactic:
[

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ S ⊆ {t | IsOpen[inst✝] t ∧ Dense t}, S.Countable ∧ ⋂₀ S ⊆ s) ↔
    ∃ S, (∀ t ∈ S, IsOpen[inst✝] t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ⋂₀ S ⊆ s
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
h : ∀ x ∈ s, closure[inst✝¹] s ∉ 𝓝 x
⊢ ∀ ⦃x : X⦄, x ∈ s → closure[inst✝] (f '' s) ∉ 𝓝 (f x)

Tactic:
[

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
h : ∀ x ∈ s, closure[inst✝¹] s ∉ 𝓝 x
⊢ ∀ ⦃x : X⦄, x ∈ s → closure[inst✝] (f '' s) ∉ 𝓝 (f x)
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ x,
      (∀ t ∈ compl '' x, IsOpen[inst✝] t) ∧
        (∀ t ∈ compl '' x, Dense t) ∧ (compl '' x).Countable ∧ ⋂₀ (compl '' x) ⊆ sᶜ) ↔
    ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S

Tactic:
[

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ x,
      (∀ t ∈ compl '' x, IsOpen[inst✝] t) ∧
        (∀ t ∈ compl '' x, Dense t) ∧ (compl '' x).Countable ∧ ⋂₀ (compl '' x) ⊆ sᶜ) ↔
    ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝¹ : TopologicalSpace α
s t u v : Set α
inst✝ : PreconnectedSpace α
x y : α
⊢ mk x = mk y

Tactic:
[

Goal state after:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝¹ : TopologicalSpace α
s t u v : Set α
inst✝ : PreconnectedSpace α
x y : α
⊢ mk x = mk y
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_1
α : Type u
β : Type v
ι✝ : Type u_1
X : ι✝ → Type u_2
inst✝ : TopologicalSpace α
s t u v : Set α
ι : Type u_3
U : ι → Set α
hclopen : ∀ (i : ι), IsClopen (U i)
hdisj : Pairwise (Disjoint on U)
hunion : ⋃ i, U i = univ
hconn : ∀ (i : ι), IsPreconnected (U i)
heq : ∀ {x : α} {i : ι} (hx : x ∈ U i), Subtype.val '' connectedComponent ⟨x, hx⟩ = connectedComponent x
x✝¹ x✝ : (i : ι) × ConnectedComponents ↑(U i)
i : ι
x y : ↑(U i)
hxy : connectedComponent ↑x = connectedComponent ↑y
⊢ ⟨i, mk x⟩ = ⟨i, mk y⟩

Tactic:
simp [← Set.image_val_inj, heq, hxy]

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

Goal state after:
α : 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)
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
x : X
⊢ (𝓝 x).HasBasis (fun s ↦ IsOpen[inst✝] s ∧ h x ∈ s ∧ IsConnected s) fun x ↦ ⇑h.symm '' x

Tactic:
← h.symm_map_nhds_eq

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsHomeomorph f ↔ IsQuotientMap f ∧ Injective f

Tactic:
refine ⟨fun h ↦ ⟨h.isQuotientMap, h.injective⟩,
    fun h ↦ ⟨h.1.continuous, fun s hs ↦ ?_, h.2, h.1.surjective⟩⟩
  rwa [← h.1.isOpen_preimage, Set.preimage_image_eq _ h.2]

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

Goal state before:
pp: ι : Type u_6
κ : Type u_7
X : ι → Type u_8
Y : κ → Type u_9
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : κ) → TopologicalSpace (Y i)
f : ι → κ
hf : Bijective f
g : (i : ι) → X i → Y (f i)
hg : ∀ (i : ι), IsHomeomorph (g i)
⊢ IsHomeomorph (Sigma.map f g)

Tactic:
[

Goal state after:
ι : Type u_6
κ : Type u_7
X : ι → Type u_8
Y : κ → Type u_9
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : κ) → TopologicalSpace (Y i)
f : ι → κ
hf : Bijective f
g : (i : ι) → X i → Y (f i)
hg : ∀ (i : ι), IsHomeomorph (g i)
⊢ IsHomeomorph (Sigma.map f g)
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
⊢ DiscreteTopology (ConnectedComponents α) ↔ ∀ (x : α), IsOpen[inst✝] (connectedComponent x)

Tactic:
[

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
⊢ DiscreteTopology (ConnectedComponents α) ↔ ∀ (x : α), IsOpen[inst✝] (connectedComponent x)
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y
u v : Set α
u_op : IsOpen[inst✝] u
v_op : IsOpen[inst✝] v
hsuv : s ⊆ u ∪ v
x : α
x_in_s : x ∈ s
x_in_u : x ∈ u
H : s ∩ (u ∩ v) = ∅
y : α
y_in_s : y ∈ s
y_in_v : y ∈ v
⊢ False

Tactic:
have hy : y ∉ u := fun y_in_u => eq_empty_iff_forall_notMem.mp H y ⟨y_in_s, ⟨y_in_u, y_in_v⟩⟩

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y
u v : Set α
u_op : IsOpen[inst✝] u
v_op : IsOpen[inst✝] v
hsuv : s ⊆ u ∪ v
x : α
x_in_s : x ∈ s
x_in_u : x ∈ u
H : s ∩ (u ∩ v) = ∅
y : α
y_in_s : y ∈ s
y_in_v : y ∈ v
hy : y ∉ u
⊢ False
Module: Mathlib.Topology.UniformSpace.DiscreteUniformity

Goal state before:
pp: X : Type u_1
u : UniformSpace X
inst✝³ : DiscreteUniformity X
Y : Type u_2
inst✝² : Finite Y
inst✝¹ : UniformSpace Y
inst✝ : DiscreteTopology Y
h : SetRel.id = ⋂ y, {p | p.2 = y → p.1 ∈ {y}}
⊢ DiscreteUniformity Y

Tactic:
[

Goal state after:
X : Type u_1
u : UniformSpace X
inst✝³ : DiscreteUniformity X
Y : Type u_2
inst✝² : Finite Y
inst✝¹ : UniformSpace Y
inst✝ : DiscreteTopology Y
h : SetRel.id = ⋂ y, {p | p.2 = y → p.1 ∈ {y}}
⊢ DiscreteUniformity Y
Module: Mathlib.Topology.UniformSpace.Cauchy

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

Tactic:
[

Goal state after:
β : Type v
ι : Sort u_1
u : ι → UniformSpace β
l : Filter β
inst✝ : l.NeBot
⊢ Cauchy l ↔ ∀ (i : ι), Cauchy l
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
F : Filter (α × β)
⊢ Cauchy F ↔ Cauchy (map Prod.fst F) ∧ Cauchy (map Prod.snd F)

Tactic:
[

Goal state after:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
F : Filter (α × β)
⊢ Cauchy F ↔ Cauchy (map Prod.fst F) ∧ Cauchy (map Prod.snd F)
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: case hg
α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : SetRel α α → Filter β
h : Monotone f
⊢ Monotone fun s ↦ s ○ s

Tactic:
exact monotone_id.relComp monotone_id

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
β : Type u_1
inst✝ : SemilatticeSup β
u : β → α
h : CauchySeq u
V : SetRel α α
hV : V ∈ 𝓤 α
this : Nonempty β
⊢ ∃ k₀, ∀ (i j : β), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V

Tactic:
have := h.tendsto_uniformity

Goal state after:
α : Type u
uniformSpace : UniformSpace α
β : Type u_1
inst✝ : SemilatticeSup β
u : β → α
h : CauchySeq u
V : SetRel α α
hV : V ∈ 𝓤 α
this✝ : Nonempty β
this : Tendsto (Prod.map u u) atTop (𝓤 α)
⊢ ∃ k₀, ∀ (i j : β), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : SetRel α β
hs : IsOpen[instTopologicalSpaceProd] s
t : Set α
⊢ IsOpen[inst✝] (s.image t)

Tactic:
[

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : SetRel α β
hs : IsOpen[instTopologicalSpaceProd] s
t : Set α
⊢ IsOpen[inst✝] (s.image t)
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 ι
⊢ ∀ a ∈ 𝓤 β, (∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ a) ↔ ∀ᶠ (n : ι × α) in p ×ˢ 𝓟 s, (f n.2, F n.1 n.2) ∈ a

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
⊢ ∀ a ∈ 𝓤 β, (∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ a) ↔ ∀ᶠ (n : ι × α) in p ×ˢ 𝓟 s, (f n.2, F n.1 n.2) ∈ a
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : SetRel α β
hs : IsClosed[instTopologicalSpaceProd] s
t : Set α
ht : t.Finite
⊢ IsClosed[inst✝] (s.image t)

Tactic:
[

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : SetRel α β
hs : IsClosed[instTopologicalSpaceProd] s
t : Set α
ht : t.Finite
⊢ IsClosed[inst✝] (s.image t)
Module: Mathlib.Topology.UniformSpace.Defs

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

Tactic:
[

Goal state after:
α : Type ua
inst✝ : UniformSpace α
s : Set α
⊢ IsOpen[inst✝.toTopologicalSpace] s ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ (∃ t ∈ 𝓤 α, Prod.mk x ⁻¹' t ⊆ s) ↔ ∃ V ∈ 𝓤 α, ball x V ⊆ s

Tactic:
[

Goal state after:
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ (∃ t ∈ 𝓤 α, Prod.mk x ⁻¹' t ⊆ s) ↔ ∃ V ∈ 𝓤 α, ball x V ⊆ s
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
x : α
⊢ 𝓝 (x, x) ≤ 𝓤 α

Tactic:
intro V V_in
  rcases comp_symm_mem_uniformity_sets V_in with ⟨w, w_in, w_symm, w_sub⟩
  have : ball x w ×ˢ ball x w ∈ 𝓝 (x, x) := by
    rw [nhds_prod_eq]
    exact prod_mem_prod (ball_mem_nhds x w_in) (ball_mem_nhds x w_in)
  apply mem_of_superset this
  rintro ⟨u, v⟩ ⟨u_in, v_in⟩
  exact w_sub (mem_comp_of_mem_ball u_in v_in)

Goal state after: