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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
⊢ (closure[inst✝] s ∩ u).Nonempty → (closure[inst✝] s ∩ v).Nonempty → (closure[inst✝] s ∩ (u ∩ v)).Nonempty ↔
    (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty

Tactic:
closure_inter_open_nonempty_iff

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
⊢ (s ∩ u).Nonempty → (closure[inst✝] s ∩ v).Nonempty → (closure[inst✝] s ∩ (u ∩ v)).Nonempty ↔
    (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty

X : Type u_1
inst✝ : TopologicalSpace X
s u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
⊢ IsOpen[inst✝] u
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
⊢ (s ∩ u).Nonempty → (closure[inst✝] s ∩ v).Nonempty → (closure[inst✝] s ∩ (u ∩ v)).Nonempty ↔
    (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty

pp: X : Type u_1
inst✝ : TopologicalSpace X
s u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
⊢ IsOpen[inst✝] u

Tactic:
closure_inter_open_nonempty_iff

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
⊢ (s ∩ u).Nonempty → (s ∩ v).Nonempty → (closure[inst✝] s ∩ (u ∩ v)).Nonempty ↔
    (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty

X : Type u_1
inst✝ : TopologicalSpace X
s u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
⊢ IsOpen[inst✝] v

X : Type u_1
inst✝ : TopologicalSpace X
s u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
⊢ IsOpen[inst✝] u
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
⊢ (s ∩ u).Nonempty → (s ∩ v).Nonempty → (closure[inst✝] s ∩ (u ∩ v)).Nonempty ↔
    (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty

pp: X : Type u_1
inst✝ : TopologicalSpace X
s u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
⊢ IsOpen[inst✝] v

pp: X : Type u_1
inst✝ : TopologicalSpace X
s u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
⊢ IsOpen[inst✝] u

Tactic:
closure_inter_open_nonempty_iff

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
⊢ (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty ↔
    (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty

X : Type u_1
inst✝ : TopologicalSpace X
s u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
⊢ IsOpen[inst✝] (u ∩ v)

X : Type u_1
inst✝ : TopologicalSpace X
s u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
⊢ IsOpen[inst✝] v

X : Type u_1
inst✝ : TopologicalSpace X
s u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
⊢ IsOpen[inst✝] u
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case a.inl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, (↑t).Nonempty → IsOpen[inst✝¹] ↑t → ∃ x ∈ ↑t, IsOpen[inst✝¹] {x}
hne : (↑s).Nonempty
ho : IsOpen[inst✝¹] ↑s
t : Finset X
hts : t ⊂ s
htne : t.Nonempty
hto : IsOpen[inst✝¹] ↑t
⊢ ∃ x ∈ ↑s, IsOpen[inst✝¹] {x}

Tactic:
rcases ihs t hts htne hto with ⟨x, hxt, hxo⟩
    exact ⟨x, hts.1 hxt, hxo⟩

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
⊢ IsDiscrete Set.univ

Tactic:
rwa [isDiscrete_univ_iff]

Goal state after:
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✝
X : Type u_3
inst✝ : Infinite X
u v : Set (CofiniteTopology X)
⊢ IsOpen u → IsOpen v → (univ ∩ u).Nonempty → (univ ∩ v).Nonempty → (univ ∩ (u ∩ v)).Nonempty

Tactic:
simp only [CofiniteTopology.isOpen_iff, univ_inter]
    intro hu hv hu' hv'
    simpa only [compl_union, compl_compl] using ((hu hu').union (hv hv')).infinite_compl.nonempty

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case h₂.hU
X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ IsClosed[inst✝] (⋃ i ∈ irreducibleComponents X \ {Z}, i)

Tactic:
exact hX.sdiff.isClosed_biUnion fun W hW ↦ isClosed_of_mem_irreducibleComponents W hW.1

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
t S U✝ : Set X
hU' : IsOpen[inst✝] U✝
h₁ : U✝ ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U✝
ht : IsIrreducible t
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
U : Set X
H : U = U✝ ∨ U = u ∨ U = v
⊢ (t ∩ U).Nonempty

Tactic:
rcases H with (rfl | rfl | rfl)

Goal state after:
case refine_2.inl
X : Type u_1
inst✝ : TopologicalSpace X
t S : Set X
h₂ : S ⊆ t
z : X
ht : IsIrreducible t
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
U : Set X
hU' : IsOpen[inst✝] U
h₁ : U ⊆ S
hz : z ∈ U
⊢ (t ∩ U).Nonempty

case refine_2.inr.inl
X : Type u_1
inst✝ : TopologicalSpace X
t S U✝ : Set X
hU' : IsOpen[inst✝] U✝
h₁ : U✝ ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U✝
ht : IsIrreducible t
v : Set X
hv : IsOpen[inst✝] v
x : X
hx : x ∈ S
y : X
hy : y ∈ S
hy' : y ∈ v
U : Set X
hu : IsOpen[inst✝] U
hx' : x ∈ U
⊢ (t ∩ U).Nonempty

case refine_2.inr.inr
X : Type u_1
inst✝ : TopologicalSpace X
t S U✝ : Set X
hU' : IsOpen[inst✝] U✝
h₁ : U✝ ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U✝
ht : IsIrreducible t
u : Set X
hu : IsOpen[inst✝] u
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
U : Set X
hv : IsOpen[inst✝] U
hy' : y ∈ U
⊢ (t ∩ U).Nonempty
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
⊢ Prod.map f f (x, y) ∈ (diagonal Y)ᶜ

Tactic:
exact inj.ne hx hy hne

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
⊢ (∀ x ∈ 𝓝ˢ t, x ∈ 𝓝ˢ s) → s ⊆ t

Tactic:
intro h x hx

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
s : Set α
a : α
f : α → β
⊢ ContinuousWithinAt f s a ↔ ContinuousWithinAt f (s ∩ Iic a) a ∧ ContinuousWithinAt f (s ∩ Ici a) a

Tactic:
by
  simp only [ContinuousWithinAt, ← tendsto_sup, nhdsWithinLE_sup_nhdsWithinGE]

Goal state after:
Module: Mathlib.Topology.Order.LeftRight

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
s : Set α
a : α
f : α → β
⊢ ContinuousWithinAt f s a ↔ ContinuousWithinAt f (s ∩ Iio a) a ∧ ContinuousWithinAt f (s ∩ Ioi a) a

Tactic:
rw [continuousWithinAt_inter_Ioi_iff_Ici, continuousWithinAt_inter_Iio_iff_Iic,
    continuousWithinAt_iff_continuous_left_right]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K L : Set X
hK : IsCompact K
hL : IsCompact L
h'L : IsClosed[inst✝¹] L
hd : Disjoint K L
x : X
hx : x ∈ K
y : X
hy : y ∈ L
h : Inseparable x y
⊢ False

Tactic:
exact absurd ((h.mem_closed_iff h'L).2 hy) <| disjoint_left.1 hd hx

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x : α
c : Set (Set α)
H1 : ∀ s ∈ c, x ∈ s
H2 : ∀ s ∈ c, IsPreconnected s
⊢ IsPreconnected (⋃₀ c)

Tactic:
by
  apply isPreconnected_of_forall x
  rintro y ⟨s, sc, ys⟩
  exact ⟨s, subset_sUnion_of_mem sc, H1 s sc, ys, H2 s sc⟩

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

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

Tactic:
refine fun x U hU =>
        ⟨connectedComponentIn (interior U) x,
          (connectedComponentIn_subset _ _).trans interior_subset, h _ isOpen_interior x ?_,
          mem_connectedComponentIn ?_, isConnected_connectedComponentIn_iff.mpr ?_⟩ <;>
      exact mem_interior_iff_mem_nhds.mpr hU

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 (α × β))
Sct : S.Countable
⊢ (∀ s ∈ S, s ∈ l.curry m) → ⋂₀ S ∈ l.curry m

Tactic:
hS

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.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)
⊢ S.Countable → (∀ s ∈ S, ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i

Tactic:
hS

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
⊢ (∀ s ∈ S, ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set (Set X)
h : inst✝ = generateFrom s
h' : ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
a : X
t : Set X
ht : IsOpen[generateFrom s] t
ha : a ∈ t
⊢ Disjoint (𝓝ˢ tᶜ) (𝓝 a)

Tactic:
induction ht with
  | basic t ht => exact h' t ht a ha
  | univ => simp
  | inter t₁ t₂ _ _ ih₁ ih₂ => grind [compl_inter, nhdsSet_union, disjoint_sup_left]
  | sUnion S _ ih =>
    obtain ⟨t, ht, ha⟩ := ha
    grw [compl_sUnion, sInter_image, iInter₂_subset t ht]
    exact ih t ht ha

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

Goal state before:
pp: case pos
α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
h✝ : x ∈ F
⊢ IsPreconnected (Subtype.val '' connectedComponent ⟨x, h✝⟩)

pp: case neg
α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
h✝ : x ∉ F
⊢ IsPreconnected ∅

Tactic:
· exact IsInducing.subtypeVal.isPreconnected_image.mpr isPreconnected_connectedComponent

Goal state after:
case neg
α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
h✝ : x ∉ F
⊢ IsPreconnected ∅
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
s : Set (SeparationQuotient X)
hs : IsClosed s
a : X
ha : SeparationQuotient.mk a ∉ s
⊢ Disjoint (comap SeparationQuotient.mk (𝓝ˢ s)) (𝓝 a)

Tactic:
comap_mk_nhdsSet

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
s : Set (SeparationQuotient X)
hs : IsClosed s
a : X
ha : SeparationQuotient.mk a ∉ s
⊢ Disjoint (𝓝ˢ (SeparationQuotient.mk ⁻¹' s)) (𝓝 a)
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set (SeparationQuotient X)
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
⊢ Disjoint (𝓝ˢ (mk ⁻¹' s)) (comap mk (𝓝ˢ t))

Tactic:
comap_mk_nhdsSet

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set (SeparationQuotient X)
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
⊢ Disjoint (𝓝ˢ (mk ⁻¹' s)) (𝓝ˢ (mk ⁻¹' t))
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)
⊢ SeparatedNhds s t

Tactic:
Subtype.preimage_val_subset_preimage_val_iff,

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 : e ∩ closure[inst✝] s ⊆ e ∩ U
V : Set X
hV : IsOpen[inst✝] V
htV : e ∩ closure[inst✝] t ⊆ e ∩ V
hUV : Disjoint (Subtype.val ⁻¹' U) (Subtype.val ⁻¹' V)
⊢ SeparatedNhds s t
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case a.right
α : 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' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
a : α
hat : a ∈ f ⁻¹' t
hau : a ∈ u
h : f ⁻¹' {f a} ⊆ v
⊢ False

Tactic:
exact uv_disj.subset_compl_right hau (h rfl)

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : CompletelyNormalSpace X
inst✝ : R0Space X
s t : Set (SeparationQuotient X)
hd₁ : Disjoint (closure s) t
hd₂ : Disjoint s (closure t)
⊢ Disjoint (𝓝ˢ (SeparationQuotient.mk ⁻¹' s)) (comap SeparationQuotient.mk (𝓝ˢ t))

Tactic:
comap_mk_nhdsSet

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : CompletelyNormalSpace X
inst✝ : R0Space X
s t : Set (SeparationQuotient X)
hd₁ : Disjoint (closure s) t
hd₂ : Disjoint s (closure t)
⊢ Disjoint (𝓝ˢ (SeparationQuotient.mk ⁻¹' s)) (𝓝ˢ (SeparationQuotient.mk ⁻¹' t))
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsEmbedding f
⊢ IsTotallyDisconnected (f '' univ) ↔ IsTotallyDisconnected univ

Tactic:
hf.isTotallyDisconnected_image

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsEmbedding f
⊢ IsTotallyDisconnected univ ↔ IsTotallyDisconnected univ
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsEmbedding f
⊢ IsTotallyDisconnected (range f) ↔ TotallyDisconnectedSpace α

Tactic:
by
  rw [totallyDisconnectedSpace_iff, ← image_univ, hf.isTotallyDisconnected_image]

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

Goal state before:
pp: case inl
α : 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
T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₁ : IsClosed[inst✝] T₁
hT₂ : IsClosed[inst✝] T₂
t' : β
ht' : t' ∈ t
htu : f ⁻¹' {t'} ⊆ u
⊢ t' ∈ T₁

Tactic:
exact ⟨ht', htu⟩

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

Goal state before:
pp: case refine_2
α : Type u_3
inst✝ : TopologicalSpace α
x y : α
x✝¹ : x ≠ y
x✝ : (fun x1 x2 ↦ ∃ U, IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ) x y
U : Set α
hU : IsClopen U
Ux : x ∈ U
Ucy : y ∈ Uᶜ
⊢ ∃ u v, IsOpen[inst✝] u ∧ IsOpen[inst✝] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v

Tactic:
· exact ⟨U, Uᶜ, hU.2, hU.compl.2, Ux, Ucy, (Set.union_compl_self U).ge, disjoint_compl_right⟩

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s : Set X
hG : IsGδ s
hd : Dense s
f : ℕ → Set ↑s
⊢ (∀ (n : ℕ), IsOpen[instTopologicalSpaceSubtype] (f n)) → (∀ (n : ℕ), Dense (f n)) → Dense (⋂ n, f n)

Tactic:
hof

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s : Set X
hG : IsGδ s
hd : Dense s
f : ℕ → Set ↑s
hof : ∀ (n : ℕ), IsOpen[instTopologicalSpaceSubtype] (f n)
⊢ (∀ (n : ℕ), Dense (f n)) → Dense (⋂ n, f n)
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
f : ℕ → Set Y
⊢ (∀ (n : ℕ), IsOpen[inst✝] (f n)) → (∀ (n : ℕ), Dense (f n)) → Dense (⋂ n, f n)

Tactic:
hof

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
Y : Type u_4
inst✝ : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst✝] (f n)
⊢ (∀ (n : ℕ), Dense (f n)) → Dense (⋂ n, f n)
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
⊢ map (⇑h) (coclosedCompact X) = coclosedCompact Y

Tactic:
by
  rw [← h.comap_coclosedCompact, map_comap_of_surjective h.surjective]

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

Goal state before:
pp: α : Type ua
u₁ u₂ : UniformSpace α
h : 𝓤 α = 𝓤 α
this : u₁.toTopologicalSpace = u₂.toTopologicalSpace
⊢ u₁ = u₂

Tactic:
cases u₁

Goal state after:
case mk
α : Type ua
u₂ : UniformSpace α
toTopologicalSpace✝ : TopologicalSpace α
uniformity✝ : Filter (α × α)
symm✝ : Tendsto Prod.swap uniformity✝ uniformity✝
comp✝ : (uniformity✝.lift' fun s ↦ s ○ s) ≤ uniformity✝
nhds_eq_comap_uniformity✝ : ∀ (x : α), 𝓝 x = comap (Prod.mk x) uniformity✝
h : 𝓤 α = 𝓤 α
this :
  { toTopologicalSpace := toTopologicalSpace✝, uniformity := uniformity✝, symm := symm✝, comp := comp✝,
        nhds_eq_comap_uniformity := nhds_eq_comap_uniformity✝ }.toTopologicalSpace =
    u₂.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace✝, uniformity := uniformity✝, symm := symm✝, comp := comp✝,
      nhds_eq_comap_uniformity := nhds_eq_comap_uniformity✝ } =
    u₂
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
⊢ Tendsto (fun p ↦ (u p.1, u p.2)) (atTop ×ˢ atTop) (𝓤 α) ↔ Tendsto (Prod.map u u) atTop (𝓤 α)

Tactic:
simp only [prod_atTop_atTop_eq, Prod.map_def]

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
r : w ○ w ○ w ⊆ t
⊢ closure[instTopologicalSpaceProd] w ⊆ w ○ w ○ w

Tactic:
rw [closure_eq_uniformity]

Goal state after:
α : Type ua
inst✝ : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
r : w ○ w ○ w ⊆ t
⊢ ⋂ V ∈ {V | V ∈ 𝓤 α ∧ SetRel.IsSymm V}, V ○ w ○ V ⊆ w ○ w ○ w
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
β : Type ub
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
ι' : Sort u_2
p : ι → Prop
s : ι → SetRel α α
ha : (𝓤 α).HasBasis p s
q : ι' → Prop
t : ι' → Set (β × β)
hb : (𝓤 β).HasBasis q t
f : α → β
S : Set α
⊢ (∀ (ib : ι'), q ib → ∃ ia, p ia ∧ ∀ (a b : α), (a, b) ∈ s ia ∩ S ×ˢ S → (f a, f b) ∈ t ib) ↔
    ∀ (i : ι'), q i → ∃ j, p j ∧ ∀ x ∈ S, ∀ y ∈ S, (x, y) ∈ s j → (f x, f y) ∈ t i

Tactic:
Set.inter_comm (s _),

Goal state after:
α : Type ua
β : Type ub
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
ι' : Sort u_2
p : ι → Prop
s : ι → SetRel α α
ha : (𝓤 α).HasBasis p s
q : ι' → Prop
t : ι' → Set (β × β)
hb : (𝓤 β).HasBasis q t
f : α → β
S : Set α
⊢ (∀ (ib : ι'), q ib → ∃ ia, p ia ∧ ∀ (a b : α), (a, b) ∈ S ×ˢ S ∩ s ia → (f a, f b) ∈ t ib) ↔
    ∀ (i : ι'), q i → ∃ j, p j ∧ ∀ x ∈ S, ∀ y ∈ S, (x, y) ∈ s j → (f x, f y) ∈ t i
Module: Mathlib.Topology.UniformSpace.Basic

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

Tactic:
intro h x hx

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

Tactic:
intro h x hx

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
⊢ 𝓤 (α × β) = Filter.comap (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 β)

Tactic:
by
  simp_rw [uniformity_prod, prod_eq_inf, Filter.comap_inf, Filter.comap_comap, Function.comp_def]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
x : α
⊢ Filter.comap mk (𝓝 (mk x)) = Filter.comap mk (Filter.comap (Prod.mk (mk x)) (map (Prod.map mk mk) (𝓤 α)))

Tactic:
conv_lhs => rw [comap_mk_nhds_mk, nhds_eq_comap_uniformity, ← comap_map_mk_uniformity]
    simp only [Filter.comap_comap, Function.comp_def, Prod.map_apply]

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
⊢ range s ⊆ ⋃ y ∈ s '' {k | k ≤ n}, {x | (x, y) ∈ a}

Tactic:
rw [range_subset_iff, biUnion_image]

Goal state after:
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
⊢ ∀ (y : ℕ), s y ∈ ⋃ y ∈ {k | k ≤ n}, {x | (x, s y) ∈ a}
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α' : Type u_3
β : Type u_4
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : T2Space α'
inst✝ : TopologicalSpace β
U : Set α'
hU : IsOpen[inst✝³] U
f : ↑U → β
cont : Continuous[instTopologicalSpaceSubtype, inst✝] f
supp : HasCompactMulSupport f
x : α'
h : x ∈ mulTSupport (extend Subtype.val f 1)
⊢ ContinuousAt (extend Subtype.val f 1) x

Tactic:
show x = ↑(⟨x, Subtype.coe_image_subset _ _
      (supp.mulTSupport_extend_one_subset continuous_subtype_val h)⟩ : U) by rfl,

Goal state after:
α' : Type u_3
β : Type u_4
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : T2Space α'
inst✝ : TopologicalSpace β
U : Set α'
hU : IsOpen[inst✝³] U
f : ↑U → β
cont : Continuous[instTopologicalSpaceSubtype, inst✝] f
supp : HasCompactMulSupport f
x : α'
h : x ∈ mulTSupport (extend Subtype.val f 1)
⊢ ContinuousAt (extend Subtype.val f 1) ↑⟨x, ⋯⟩