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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace β
s : Set α
f : α → β
⊢ IsClosed[TopologicalSpace.induced f t] s ↔ ∃ t_1, IsClosed[t] t_1 ∧ f ⁻¹' t_1 = s

Tactic:
by
  let := t.induced f
  simp only [← isOpen_compl_iff, isOpen_induced_iff]
  exact compl_surjective.exists.trans (by simp only [preimage_compl, compl_inj_iff])

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace α
b : Set (Set β)
f : α → β
h : ∀ a ∈ b, IsOpen[t] (f ⁻¹' a)
⊢ ∀ a ∈ b, IsOpen[t] (f ⁻¹' a)

Tactic:
exact h

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hf : IsCoinducing f
⊢ IsCoinducing (g ∘ f) ↔ IsCoinducing g

Tactic:
refine ⟨fun hgf ↦ .of_isOpen_preimage_iff_isOpen fun s ↦ ?_, fun hg ↦ hg.comp hf⟩

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hf : IsCoinducing f
hgf : IsCoinducing (g ∘ f)
s : Set Z
⊢ IsOpen[inst✝¹] (g ⁻¹' s) ↔ IsOpen[inst✝] s
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
h : t ∈ 𝓝[s] a
⊢ 𝓝[s ∩ t] a = 𝓝[s] a

Tactic:
rw [inter_comm, nhdsWithin_inter_of_mem h]

Goal state after:
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: case inr.mp.refine_1
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : IsOpen[instTopologicalSpaceProd] (s ×ˢ t)
⊢ IsOpen[inst✝¹] s

pp: case inr.mp.refine_2
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : IsOpen[instTopologicalSpaceProd] (s ×ˢ t)
⊢ IsOpen[inst✝] t

Tactic:
· simpa only [fst_image_prod _ st.2] using isOpenMap_fst _ H

Goal state after:
case inr.mp.refine_2
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : IsOpen[instTopologicalSpaceProd] (s ×ˢ t)
⊢ IsOpen[inst✝] t
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
⊢ frontier (s ×ˢ t) = closure[inst✝¹] s ×ˢ frontier t ∪ frontier s ×ˢ closure[inst✝] t

Tactic:
simp only [frontier, closure_prod_eq, interior_prod_eq, prod_sdiff_prod]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
⊢ ClusterPt a (𝓟 J) ↔ ∃ᶠ (x : α) in 𝓝[t] ↑a, ∃ (h : x ∈ s), ⟨x, h⟩ ∈ J

Tactic:
rw [nhdsWithin_eq_map_subtype_coe (hst a.prop), Filter.frequently_map,
    clusterPt_principal_iff_frequently,
    Topology.IsInducing.subtypeVal.nhds_eq_comap, Filter.frequently_comap,
    Topology.IsInducing.subtypeVal.nhds_eq_comap, Filter.frequently_comap, Subtype.coe_mk]
  apply frequently_congr
  apply Eventually.of_forall
  intro x
  simp only [SetCoe.exists, exists_and_left, exists_eq_left]
  exact ⟨fun ⟨h, hx⟩ => ⟨hst h, h, hx⟩, fun ⟨_, hx⟩ => hx⟩

Goal state after:
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
⊢ IsOpenMap (Sum.elim f g) ↔ IsOpenMap f ∧ IsOpenMap g

Tactic:
simp only [isOpenMap_sum, elim_inl, elim_inr]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
p : X → Prop
x : X
hx : p x
h : ∀ᶠ (x : X) in 𝓝 x, p x
⊢ p ∈ 𝓝 ↑⟨x, hx⟩

Tactic:
exact h

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous[inst✝¹, inst✝] f
s u : Set β
h : u ∈ 𝓝ˢ s
⊢ f ⁻¹' u ∈ 𝓝ˢ (f ⁻¹' s)

Tactic:
by
  simpa [h] using hf.preimage_mem_nhdsSetWithin (s := s) (u := u) (s' := univ)

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case inl
ι : Type u_2
inst✝¹ : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst✝ : (i : ι) → TopologicalSpace (X i)
h : ∀ (i : ι), IsSeparable (s i)
he : univ.pi s = ∅
⊢ IsSeparable (univ.pi s)

pp: case inr
ι : Type u_2
inst✝¹ : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst✝ : (i : ι) → TopologicalSpace (X i)
h : ∀ (i : ι), IsSeparable (s i)
f₀ : (i : ι) → X i
⊢ IsSeparable (univ.pi s)

Tactic:
· rw [he]
    exact countable_empty.isSeparable

Goal state after:
case inr
ι : Type u_2
inst✝¹ : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst✝ : (i : ι) → TopologicalSpace (X i)
h : ∀ (i : ι), IsSeparable (s i)
f₀ : (i : ι) → X i
⊢ IsSeparable (univ.pi s)
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case refine_1
ι : Type u_5
A : ι → Type u_9
g : (a : ι) → Set (Set (A a))
s : (a : ι) → Set (A a)
i : Finset ι
hi : ∀ a ∈ i, s a ∈ g a
this : (a : ι) → TopologicalSpace (A a) := fun a ↦ generateFrom (g a)
⊢ IsOpen[Pi.topologicalSpace] ((↑i).pi s)

Tactic:
exact isOpen_set_pi i.finite_toSet (fun a ha => GenerateOpen.basic _ (hi a ha))

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case mp
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
S : Set β
⊢ (∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i) →
    ∃ U F, (∀ i ∈ F, U i ∈ preimage (f i) '' T i) ∧ S = ⋂ i ∈ F, U i

Tactic:
rintro ⟨U, F, hUT, hSU⟩

Goal state after:
case mp
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
S : Set β
U : (i : ι) → Set (X i)
F : Finset ι
hUT : ∀ i ∈ F, U i ∈ T i
hSU : S = ⋂ i ∈ F, f i ⁻¹' U i
⊢ ∃ U F, (∀ i ∈ F, U i ∈ preimage (f i) '' T i) ∧ S = ⋂ i ∈ F, U i
Module: Mathlib.Topology.Bases

Goal state before:
pp: case mpr
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
S : Set β
⊢ (∃ U F, (∀ i ∈ F, U i ∈ preimage (f i) '' T i) ∧ S = ⋂ i ∈ F, U i) →
    ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i

Tactic:
rintro ⟨U, F, hUT, hSU⟩

Goal state after:
case mpr
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
S : Set β
U : ι → Set β
F : Finset ι
hUT : ∀ i ∈ F, U i ∈ preimage (f i) '' T i
hSU : S = ⋂ i ∈ F, U i
⊢ ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
⊢ map m (ofComapInfPrincipal h) = g

Tactic:
let f := Filter.comap m g ⊓ 𝓟 s
  have : f.NeBot := comap_inf_principal_neBot_of_image_mem h
  apply eq_of_le
  calc
    Filter.map m (of f) ≤ Filter.map m f := map_mono (of_le _)
    _ ≤ (Filter.map m <| Filter.comap m g) ⊓ Filter.map m (𝓟 s) := map_inf_le
    _ = (Filter.map m <| Filter.comap m g) ⊓ (𝓟 <| m '' s) := by rw [map_principal]
    _ ≤ ↑g ⊓ (𝓟 <| m '' s) := inf_le_inf_right _ map_comap_le
    _ = ↑g := inf_of_le_left (le_principal_iff.mpr h)

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case pos
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
b : ℕ → Set α
ht : (range b).Countable ∧ ∅ ∉ range b ∧ IsTopologicalBasis (range b)
hn : (range b).Nonempty
⊢ ∃ b, IsTopologicalBasis (range b)

Tactic:
exact ⟨b, ht.2.2⟩

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t✝] u
A : ∀ x ∈ u, ∃ a ∈ t, x ∈ a ∧ a ⊆ u
⊢ ∃ s ⊆ t, s.Countable ∧ u = ⋃ a ∈ s, a

Tactic:
choose! a hat xa au using A

Goal state after:
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t✝] u
a : α → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
⊢ ∃ s ⊆ t, s.Countable ∧ u = ⋃ a ∈ s, a
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hc : S.Countable
hcomp : ∀ s ∈ S, IsCompact s
⊢ IsSigmaCompact (⋃₀ S)

Tactic:
have : Countable S := countable_coe_iff.mpr hc
  rw [sUnion_eq_iUnion]
  apply isSigmaCompact_iUnion_of_isCompact _ (fun ⟨s, hs⟩ ↦ hcomp s hs)

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

Goal state before:
pp: case mpr.refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ n, L n = f '' s
⊢ ∀ (n : ℕ), IsCompact ((fun n ↦ f ⁻¹' L n ∩ s) n)

Tactic:
intro n
      have : f '' (f ⁻¹' (L n) ∩ s) = L n := by
        rw [image_preimage_inter, inter_eq_left.mpr]
        exact (subset_iUnion _ n).trans hcov.le
      apply hf.isCompact_iff.mpr (this.symm ▸ (hcomp n))

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
t : Set (Set X)
ht : ∀ a ∈ t, IsClosed[inst✝] a
h : ∀ a ⊆ t, a.Finite → (s ∩ ⋂₀ a).Nonempty
⊢ (s ∩ ⋂₀ t).Nonempty

Tactic:
by
  rw [Set.sInter_eq_iInter]
  refine hs.inter_iInter_nonempty _ (fun i ↦ ht _ i.2) fun a ↦ ?_
  simpa using h (Subtype.val '' (a : Set t)) (by simp) (a.finite_toSet.image _)

Goal state after:
Module: Mathlib.Data.Set.Subset

Goal state before:
pp: α : Type u_2
A B : Set α
h : A ⊆ B
⊢ ∀ (a : α) (b : a ∈ A), ⟨a, b⟩ ∈ A ↓∩ B

Tactic:
exact h

Goal state after:
Module: Mathlib.Data.Set.Subset

Goal state before:
pp: α : Type u_2
A B C : Set α
hB : A ∩ B = B
hC : A ∩ C = C
h : B = C
⊢ B = C

Tactic:
exact h

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : Filter X
y : Y
hf : Disjoint f (cocompact X)
⊢ f ×ˢ 𝓝 y ≤ 𝓝ˢ (univ ×ˢ {y})

Tactic:
by
  simpa using prod_nhdsSet_le_of_disjoint_cocompact isCompact_singleton hf

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
t : Set (SeparationQuotient X)
| comap mk (𝓝ˢ t)

Tactic:
← image_preimage_eq t surjective_mk,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
t : Set (SeparationQuotient X)
| comap mk (𝓝ˢ (mk '' mk ⁻¹' t))
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ t ⊆ S, ∃ u, IsOpen[inst✝] u ∧ u ∩ S = t
s : Set X
sS : s ⊆ S
U : Set X
Uo : IsOpen[inst✝] U
Us : U ∩ S = sᶜ ∩ S
⊢ ∃ U, IsClosed[inst✝] U ∧ U ∩ S = s

Tactic:
exact ⟨Uᶜ, isClosed_compl_iff.mpr Uo, by rw [left_eq_inter.mpr sS]; simp_all [Set.ext_iff]⟩

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)
H : ∀ (x : Y), IsDiscrete (f ⁻¹' {x})
x : X
hx : x ∈ f ⁻¹' s
h : 𝓝[f ⁻¹' s] x ≤ pure x
⊢ 𝓝[f ⁻¹' s] x ≤ pure x

Tactic:
exact h

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
inst✝¹ : T1Space X
inst✝ : WeaklyLocallyCompactSpace Y
hf' : Continuous[inst✝³, inst✝²] f
hf : Tendsto f cofinite (cocompact Y)
⊢ DiscreteTopology X

Tactic:
by
  refine discreteTopology_iff_isOpen_singleton.mpr (fun x ↦ ?_)
  obtain ⟨K : Set Y, hK : IsCompact K, hK' : K ∈ 𝓝 (f x)⟩ := exists_compact_mem_nhds (f x)
  obtain ⟨U : Set Y, hU₁ : U ⊆ K, hU₂ : IsOpen U, hU₃ : f x ∈ U⟩ := mem_nhds_iff.mp hK'
  have hU₄ : Set.Finite (f ⁻¹' U) :=
    Finite.subset (tendsto_cofinite_cocompact_iff.mp hf K hK) (preimage_mono hU₁)
  exact isOpen_singleton_of_finite_mem_nhds _ ((hU₂.preimage hf').mem_nhds hU₃) hU₄

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsDiscrete s
hs' : IsPreirreducible s
x : X
hxs : x ∈ s
y : X
⊢ y ∈ s → x = y

Tactic:
hys

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsDiscrete s
hs' : IsPreirreducible s
x : X
hxs : x ∈ s
y : X
hys : y ∈ s
⊢ x = y
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
a : X
p : X → Prop
hs : IsOpen[inst✝] s
⊢ (∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝 y, p x) ↔ ∀ᶠ (x : X) in 𝓝[s] a, p x

Tactic:
by
  nth_rw 2 [← eventually_eventually_nhdsWithin]
  constructor
  · intro h
    filter_upwards [h] with _ hy
    exact eventually_nhdsWithin_of_eventually_nhds hy
  · intro h
    filter_upwards [h, eventually_nhdsWithin_of_forall fun _ a ↦ a] with _ _ _
    simp_all [IsOpen.nhdsWithin_eq]

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 : ι
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}
U : Set α := ⋃ k ∈ S, s k
V : Set α := ⋃ k ∈ Sᶜ, s k
hsplit : ⋃ n, s n = U ∪ V
a : α
ha : a ∈ s i
b : α
hb : b ∈ s j
hi_S : i ∈ S := TransGen.single (Exists.intro a ⟨ha, ha⟩)
hUne : ((⋃ n, s n) ∩ U).Nonempty
hVne : ((⋃ n, s n) ∩ V).Nonempty
x : α
hxU : x ∈ U
hxV : x ∈ V
⊢ False

Tactic:
simp only [mem_iUnion, exists_prop, mem_compl_iff, U, V] at hxU hxV

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 : ι
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}
U : Set α := ⋃ k ∈ S, s k
V : Set α := ⋃ k ∈ Sᶜ, s k
hsplit : ⋃ n, s n = U ∪ V
a : α
ha : a ∈ s i
b : α
hb : b ∈ s j
hi_S : i ∈ S := TransGen.single (Exists.intro a ⟨ha, ha⟩)
hUne : ((⋃ n, s n) ∩ U).Nonempty
hVne : ((⋃ n, s n) ∩ V).Nonempty
x : α
hxU : ∃ i ∈ S, x ∈ s i
hxV : ∃ i ∉ S, x ∈ s i
⊢ False
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_1.inl
ι : Type u_1
X : ι → Type u_2
hι : Nonempty ι
inst✝ : (i : ι) → TopologicalSpace (X i)
hs : IsPreconnected ∅
⊢ ∃ i t, IsPreconnected t ∧ ∅ = mk i '' t

Tactic:
exact ⟨Classical.choice hι, ∅, isPreconnected_empty, (Set.image_empty _).symm⟩

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

Goal state before:
pp: case refine_2.inl
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
he : IsEmpty ((i : ι) → X i)
⊢ LocallyConnectedSpace ((i : ι) → X i)

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 ⟨he.elim⟩

Goal state after:
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)
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_1.insert.refine_2
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hne : s.Nonempty
u : Set α
U : Finset (Set α)
uU : u ∉ U
x✝ :
  s.Nonempty ∧
    ∀ (a : Set α), IsOpen[inst✝] a → ∀ (b : Set α), IsOpen[inst✝] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
h : ∀ (a : Set α), IsOpen[inst✝] a → ∀ (b : Set α), IsOpen[inst✝] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
IH : (∀ a ∈ U, ∀ b ∈ U, (s ∩ (a ∩ b)).Nonempty → a = b) → (∀ u ∈ U, IsOpen[inst✝] u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
hU :
  (∀ x ∈ U, (s ∩ (u ∩ x)).Nonempty → u = x) ∧
    ∀ x ∈ U, ((s ∩ (x ∩ u)).Nonempty → x = u) ∧ ∀ x_1 ∈ U, (s ∩ (x ∩ x_1)).Nonempty → x = x_1
hUo : IsOpen[inst✝] u ∧ ∀ x ∈ U, IsOpen[inst✝] x
hsU : s ⊆ u ∪ ⋃₀ ↑U
⊢ s ⊆ ⋃₀ ↑U → ∃ x ∈ U, s ⊆ x

Tactic:
exact IH (fun u hu => (hU.2 u hu).2) hUo.2

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

Goal state before:
pp: X : Type u_1
ι' : Sort u_4
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι'
f : ι' → Set X
hs : ∀ (i : ι'), IsMeagre (f i)
⊢ (⋃ i, f i)ᶜ ∈ residual X

Tactic:
compl_iUnion

Goal state after:
X : Type u_1
ι' : Sort u_4
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι'
f : ι' → Set X
hs : ∀ (i : ι'), IsMeagre (f i)
⊢ ⋂ i, (f i)ᶜ ∈ residual X
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
a b : X
ne : connectedComponent a ≠ connectedComponent b
h : Disjoint (connectedComponent a) (⋂ s, ↑s)
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ mk a ∈ u ∧ mk b ∈ v ∧ Disjoint u v

Tactic:
disjoint_iff_inter_eq_empty

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
a b : X
ne : connectedComponent a ≠ connectedComponent b
h : connectedComponent a ∩ ⋂ s, ↑s = ∅
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ mk a ∈ u ∧ mk b ∈ v ∧ Disjoint u v
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 α
ι : 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 j : ι
x : ↑(U i)
y : ↑(U j)
hxy : connectedComponent ↑x = connectedComponent ↑y
⊢ i = j

Tactic:
apply hdisj.eq
      rw [Set.not_disjoint_iff]
      exact ⟨x, x.2, (hclopen j).connectedComponent_subset y.2 (hxy ▸ mem_connectedComponent)⟩

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

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

Tactic:
by
    rw [u₁.nhds_eq_comap_uniformity, u₂.nhds_eq_comap_uniformity]
    exact congr_arg (comap _) h

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝ : UniformSpace α
g : SetRel α α → Filter β
f : Filter β
hg : Monotone g
h : ((𝓤 α).lift fun s ↦ g (Prod.swap ⁻¹' s)) ≤ f
⊢ (𝓤 α).lift (g ∘ preimage Prod.swap) ≤ f

Tactic:
exact h

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

Goal state before:
pp: case hh
α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : SetRel α α → Filter β
h : Monotone f
⊢ Monotone f

Tactic:
exact h

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
⊢ ∃ t ∈ 𝓤 α, SetRel.IsSymm t ∧ t ○ t ○ t ⊆ s

Tactic:
rcases comp_symm_mem_uniformity_sets hs with ⟨w, w_in, _, w_sub⟩

Goal state after:
α : Type ua
inst✝ : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SetRel.IsSymm w
w_sub : w ○ w ⊆ s
⊢ ∃ t ∈ 𝓤 α, SetRel.IsSymm t ∧ t ○ t ○ t ⊆ s
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
⊢ interior s ∈ 𝓤 α

Tactic:
by
  rw [uniformity_eq_uniformity_interior]; exact mem_lift' hs

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

Goal state before:
pp: α : Type ua
β : Type ub
f : α → β
U : SetRel β β
x : α
⊢ UniformSpace.ball x (Prod.map f f ⁻¹' U) = f ⁻¹' UniformSpace.ball (f x) U

Tactic:
ext : 1

Goal state after:
α : Type ua
β : Type ub
f : α → β
U : SetRel β β
x x✝ : α
⊢ x✝ ∈ UniformSpace.ball x (Prod.map f f ⁻¹' U) ↔ x✝ ∈ f ⁻¹' UniformSpace.ball (f x) U
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: ι : Sort u_2
α : Type u_3
γ : Type u_4
u : ι → UniformSpace γ
f : α → γ
⊢ comap f (⨅ i, u i) = ⨅ i, comap f (u i)

Tactic:
ext : 1

Goal state after:
ι : Sort u_2
α : Type u_3
γ : Type u_4
u : ι → UniformSpace γ
f : α → γ
⊢ 𝓤 α = 𝓤 α
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
x y : α
h : Inseparable x y
⊢ 𝓝 (x, y) ≤ 𝓤 α

Tactic:
by
  rw [h.prod rfl]
  apply nhds_le_uniformity

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

Goal state before:
pp: α : Type u_1
u : UniformSpace α
inst✝ : IndiscreteTopology α
x : α × α
⊢ x ∈ (𝓤 α).ker ↔ x ∈ univ

Tactic:
rw [← inseparable_iff_ker_uniformity]

Goal state after:
α : Type u_1
u : UniformSpace α
inst✝ : IndiscreteTopology α
x : α × α
⊢ Inseparable x.1 x.2 ↔ x ∈ univ
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case mpr
α : Type u
uniformSpace : UniformSpace α
g : Filter α
d : SetRel α α
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), t.Finite → d.preimage t ∉ g
f : Filter α := ⨅ t, g ⊓ 𝓟 (d.preimage ↑t)ᶜ
hb : Antitone fun t ↦ g ⊓ 𝓟 (d.preimage ↑t)ᶜ
this✝ : f.NeBot
this : f ≤ g
c : Filter α
hcf : c ≤ f
hc : Cauchy c
m : Set α
hm : m ∈ c
hmd : m ×ˢ m ⊆ d
⊢ False

Tactic:
rcases hc.1.nonempty_of_mem hm with ⟨y, hym⟩

Goal state after:
case mpr
α : Type u
uniformSpace : UniformSpace α
g : Filter α
d : SetRel α α
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), t.Finite → d.preimage t ∉ g
f : Filter α := ⨅ t, g ⊓ 𝓟 (d.preimage ↑t)ᶜ
hb : Antitone fun t ↦ g ⊓ 𝓟 (d.preimage ↑t)ᶜ
this✝ : f.NeBot
this : f ≤ g
c : Filter α
hcf : c ≤ f
hc : Cauchy c
m : Set α
hm : m ∈ c
hmd : m ×ˢ m ⊆ d
y : α
hym : y ∈ m
⊢ False
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: case right
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
F : Filter α
hf : IsUniformInducing f
hs : (map f F).TotallyBounded
t : Set (β × β)
ht : t ∈ 𝓤 β
u : Set α
hfin : u.Finite
h : {a | ∃ x ∈ u, (a, f x) ∈ t} ∈ map f F
⊢ SetRel.preimage (Prod.map f f ⁻¹' id t) u ∈ F

Tactic:
exact h

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
⊢ uniformSpace α = ⨅ i, UniformSpace.comap (eval i) (U i)

Tactic:
ext : 1

Goal state after:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
⊢ 𝓤 ((i : ι) → α i) = 𝓤 ((i : ι) → α i)
Module: Mathlib.Topology.Coherent

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
S : Set (Set X)
inst✝ : SequentialSpace X
h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S
t : Set X
ht : ∀ s ∈ S, IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' t)
u : ℕ → X
x : X
hut : ∀ (n : ℕ), u n ∈ t
hux : Tendsto u atTop (𝓝 x)
s : Set X
hsc : IsClosed[inst✝¹] s
hst : Subtype.val ⁻¹' s = Subtype.val ⁻¹' t
⊢ x ∈ t

Tactic:
Subtype.preimage_val_eq_preimage_val_iff,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
S : Set (Set X)
inst✝ : SequentialSpace X
h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S
t : Set X
ht : ∀ s ∈ S, IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' t)
u : ℕ → X
x : X
hut : ∀ (n : ℕ), u n ∈ t
hux : Tendsto u atTop (𝓝 x)
s : Set X
hsc : IsClosed[inst✝¹] s
hst : insert x (range u) ∩ s = insert x (range u) ∩ t
⊢ x ∈ t
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: case hfs
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : UniformSpace γ
g : β → γ
t : Set β
hg : UniformContinuousOn g t
hf : TendstoLocallyUniformlyOn F f p univ
hfs : ∀ (x : α), f x ∈ t
hFs : ∀ᶠ (n : ι) in p, ∀ (x : α), F n x ∈ t
⊢ MapsTo f univ t

Tactic:
simpa [MapsTo]

Goal state after: