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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
X : α → β
s : Set β
t : Set α
a : { x // x ∈ t }
hs : (fun x ↦ X ↑x) ⁻¹' s ∈ 𝓝 a
⊢ X ⁻¹' s ∈ 𝓝[t] ↑a

Tactic:
← map_nhds_subtype_val,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
X : α → β
s : Set β
t : Set α
a : { x // x ∈ t }
hs : (fun x ↦ X ↑x) ⁻¹' s ∈ 𝓝 a
⊢ X ⁻¹' s ∈ map Subtype.val (𝓝 a)
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
a : ↑s
t : Set ↑s
⊢ t ∈ 𝓝 a ↔ Subtype.val '' t ∈ 𝓝[s] ↑a

Tactic:
← map_nhds_subtype_val,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
a : ↑s
t : Set ↑s
⊢ t ∈ 𝓝 a ↔ Subtype.val '' t ∈ map Subtype.val (𝓝 a)
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
a : ↑s
⊢ Subtype.val ⁻¹' t ∈ 𝓝 a ↔ t ∈ 𝓝[s] ↑a

Tactic:
← map_nhds_subtype_val,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
a : ↑s
⊢ Subtype.val ⁻¹' t ∈ 𝓝 a ↔ t ∈ map Subtype.val (𝓝 a)
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ IsClosed[instTopologicalSpaceSum] (range inl)

Tactic:
rw [← isOpen_compl_iff, compl_range_inl]
  exact isOpen_range_inr

Goal state after:
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
z : β
x x' : α
⊢ x' ≤ x ∧ z ∈ s x' → ∃ i, z ∈ s i

Tactic:
⟨_, hz⟩

Goal state after:
case h₁
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
z : β
x x' : α
left✝ : x' ≤ x
hz : z ∈ s x'
⊢ ∃ i, z ∈ s i
Module: Mathlib.Topology.Bornology.Basic

Goal state before:
pp: α : Type u_2
x✝ : Bornology α
⊢ IsBounded ∅

Tactic:
by
  rw [isBounded_def, compl_empty]
  exact univ_mem

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), SeparableSpace (X i)
inst✝ : Countable ι
⊢ SeparableSpace ((i : ι) → X i)

Tactic:
by
  choose t htc htd using (exists_countable_dense <| X ·)
  have := fun i ↦ (htc i).to_subtype
  nontriviality ∀ i, X i; inhabit ∀ i, X i
  classical
    set f : (Σ I : Finset ι, ∀ i : I, t i) → ∀ i, X i := fun ⟨I, g⟩ i ↦
      if hi : i ∈ I then g ⟨i, hi⟩ else (default : ∀ i, X i) i
    refine ⟨⟨range f, countable_range f, dense_iff_inter_open.2 fun U hU ⟨g, hg⟩ ↦ ?_⟩⟩
    rcases isOpen_pi_iff.1 hU g hg with ⟨I, u, huo, huU⟩
    have : ∀ i : I, ∃ y ∈ t i, y ∈ u i := fun i ↦
      (htd i).exists_mem_open (huo i i.2).1 ⟨_, (huo i i.2).2⟩
    choose y hyt hyu using this
    lift y to ∀ i : I, t i using hyt
    refine ⟨f ⟨I, y⟩, huU fun i (hi : i ∈ I) ↦ ?_, mem_range_self (f := f) ⟨I, y⟩⟩
    simp only [f, dif_pos hi]
    exact hyu ⟨i, _⟩

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case inr
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsOpen[inst✝ i] s
j : ι
hne : j ≠ i
⊢ IsOpen[inst✝ j] (Sigma.mk j ⁻¹' Sigma.mk i '' s)

Tactic:
· rw [preimage_image_sigmaMk_of_ne hne]
    exact isOpen_empty

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: X : Type u_4
inst✝ : TopologicalSpace X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : X → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), {i | ((fun n ↦ {x | f (n + 1) x ≠ f n x}) i ∩ U x).Nonempty}.Finite
N : X → ℕ
hN : ∀ (x : X), ∀ n ≥ N x + 1, ∀ y ∈ U x, f n y = f (N x + 1) y
x : X
⊢ ∀ᶠ (p : ℕ × X) in atTop ×ˢ 𝓝 x, f p.1 p.2 = (fun x ↦ f (N x + 1) x) p.2

Tactic:
filter_upwards [Filter.prod_mem_prod (eventually_gt_atTop (N x)) (hUx x)]

Goal state after:
X : Type u_4
inst✝ : TopologicalSpace X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : X → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), {i | ((fun n ↦ {x | f (n + 1) x ≠ f n x}) i ∩ U x).Nonempty}.Finite
N : X → ℕ
hN : ∀ (x : X), ∀ n ≥ N x + 1, ∀ y ∈ U x, f n y = f (N x + 1) y
x : X
⊢ ∀ a ∈ {x_1 | N x < x_1} ×ˢ U x, f a.1 a.2 = f (N a.2 + 1) a.2
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : SecondCountableTopology β
hf : IsInducing f
⊢ SecondCountableTopology α

Tactic:
by
  rw [hf.1]
  exact secondCountableTopology_induced α β f

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : f ≤ 𝓟 s
h : ∀ x ∈ s, ¬ClusterPt x f
⊢ ∃ ι U, (∀ (i : ι), IsOpen[inst✝] (U i)) ∧ s ⊆ ⋃ i, U i ∧ ∀ (t : Finset ι), ¬s ⊆ ⋃ i ∈ t, U i

Tactic:
simp only [ClusterPt, not_neBot, ← disjoint_iff, SetCoe.forall',
    (nhds_basis_opens _).disjoint_iff_left] at h

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : f ≤ 𝓟 s
h : ∀ (x : ↑s), ∃ i, (↑x ∈ i ∧ IsOpen[inst✝] i) ∧ iᶜ ∈ f
⊢ ∃ ι U, (∀ (i : ι), IsOpen[inst✝] (U i)) ∧ s ⊆ ⋃ i, U i ∧ ∀ (t : Finset ι), ¬s ⊆ ⋃ i ∈ t, U i
Module: Mathlib.Data.Set.Subset

Goal state before:
pp: α : Type u_2
A : Set α
T : Set (Set ↑A)
hT : T.Nonempty
⊢ Subtype.val '' ⋂₀ T = ⋂₀ {x | ∃ B ∈ T, Subtype.val '' B = x}

Tactic:
by
  rw [← Set.image, sInter_image, sInter_eq_biInter, Subtype.val_injective.injOn.image_biInter_eq hT]

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

Goal state before:
pp: X : Type u
T : TopologicalSpace X
𝔅 : Set (Set X)
hT : T = generateFrom 𝔅
h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅
h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
P : Set (Set X)
hP𝔅 : P ⊆ 𝔅
hP : ∀ Q ⊆ P, Q.Finite → (⋂₀ (compl '' Q)).Nonempty
Q : Set (Set X)
hQP : Q ⊆ compl '' P
hQ : Q.Finite
⊢ Q ⊆ compl '' P → (compl '' Q).Finite → (⋂₀ Q).Nonempty

Tactic:
simpa [← compl_involutive.image_eq_preimage_symm] using hP (compl '' Q)

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₁ x₂ : X
y₁ y₂ : Y
⊢ (x₁, y₁) ⤳ (x₂, y₂) ↔ x₁ ⤳ x₂ ∧ y₁ ⤳ y₂

Tactic:
by
  simp only [Specializes, nhds_prod_eq, prod_le_prod]

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
hts : t ⊆ s
h : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
⊢ IsCompact t

Tactic:
by
  intro f _ hf
  obtain ⟨x, hxs, hxf⟩ := hs <| hf.trans <| Filter.monotone_principal hts
  obtain ⟨y, hyt, hxy⟩ := h x hxs
  exact ⟨y, hyt, hxy.clusterPt hxf⟩

Goal state after:
Module: Mathlib.Topology.Piecewise

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

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

Tactic:
· exact hf.mono (inter_subset_inter_right s subset_closure)

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

Goal state before:
pp: X✝ : Type u
Y : Type v
ι : Type u_1
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s t : Set X✝
f : X✝ → Y
X : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), CompactSpace (X i)
⊢ CompactSpace ((i : ι) × X i)

Tactic:
by
  refine ⟨?_⟩
  rw [Sigma.univ]
  exact isCompact_iUnion fun i => isCompact_range continuous_sigmaMk

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst✝] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst✝] {x}) ↔ ∀ (x : X), IsOpen[inst✝] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst✝] {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ y ∉ U
tfae_5_iff_8 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
⊢ T1Space X → Continuous[inst✝, _] ⇑CofiniteTopology.of

Tactic:
simp only [continuous_def, CofiniteTopology.isOpen_iff']

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst✝] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst✝] {x}) ↔ ∀ (x : X), IsOpen[inst✝] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst✝] {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ y ∉ U
tfae_5_iff_8 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
⊢ T1Space X → ∀ (s : Set (CofiniteTopology X)), s = ∅ ∨ sᶜ.Finite → IsOpen[inst✝] (⇑CofiniteTopology.of ⁻¹' s)
Module: Mathlib.Topology.Irreducible

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

Tactic:
(isClosed_of_mem_irreducibleComponents Z hZ).closure_subset_iff

Goal state after:
case h₁
X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
Module: Mathlib.Order.SuccPred.Relation

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

Tactic:
by
  revert h; refine Succ.rec ?_ ?_ hnm
  · intro _
    exact ReflTransGen.refl
  · intro m hnm ih h
    have : ReflTransGen r n m := ih fun i hi => h i ⟨hi.1, hi.2.trans_le <| le_succ m⟩
    rcases (le_succ m).eq_or_lt with hm | hm
    · rwa [← hm]
    exact this.tail (h m ⟨hnm, hm⟩)

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 : X
h : {x}ᶜ ∈ 𝓝ˢ t → {x}ᶜ ∈ 𝓝ˢ s
hx : x ∈ s
⊢ x ∈ t

Tactic:
simp_rw [compl_singleton_mem_nhdsSet_iff] at h

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
x : X
hx : x ∈ s
h : x ∉ t → x ∉ s
⊢ x ∈ t
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
⊢ Std.Symm Specializes → ∀ ⦃x y : SeparationQuotient X⦄, x ⤳ y → x = y

Tactic:
rintro h ⟨x⟩ ⟨y⟩ sxspecsy
    change mk _ = mk _
    have xspecy : x ⤳ y := isInducing_mk.specializes_iff.mp sxspecsy
    have yspecx : y ⤳ x := h.symm x y xspecy
    rw [mk_eq_mk, inseparable_iff_specializes_and]
    exact ⟨xspecy, yspecx⟩

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 ?_⟩

Goal state after:
case mpr.refine_1
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (F : Set α), IsOpen[inst✝] F → ∀ x ∈ F, IsOpen[inst✝] (connectedComponentIn F x)
x : α
U : Set α
hU : U ∈ 𝓝 x
⊢ x ∈ interior U

case mpr.refine_2
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (F : Set α), IsOpen[inst✝] F → ∀ x ∈ F, IsOpen[inst✝] (connectedComponentIn F x)
x : α
U : Set α
hU : U ∈ 𝓝 x
⊢ x ∈ interior U

case mpr.refine_3
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (F : Set α), IsOpen[inst✝] F → ∀ x ∈ F, IsOpen[inst✝] (connectedComponentIn F x)
x : α
U : Set α
hU : U ∈ 𝓝 x
⊢ x ∈ interior U
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝¹ : CountableInterFilter l✝
l : Filter α
inst✝ : CountableInterFilter l
f : α → β
⊢ CountableInterFilter (map f l)

Tactic:
refine ⟨fun S hSc hS => ?_⟩
  simp only [mem_map, sInter_eq_biInter, preimage_iInter₂] at hS ⊢
  exact (countable_bInter_mem hSc).2 hS

Goal state after:
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
hs : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
hsu : (s ∩ u).Nonempty
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
replace hs := mt (hs hsu)
    simp_rw [Set.not_nonempty_iff_eq_empty, ← Set.disjoint_iff_inter_eq_empty,
      disjoint_iff_inter_eq_empty.1 huv] at hs
    exact Or.inl ((hs s.disjoint_empty).subset_left_of_subset_union hsuv)

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 : ∀ (u : Set ι), u.Countable ∧ (s ∩ ⋂ i ∈ u, t i).Nonempty
⊢ (s ∩ ⋂ i, t i).Nonempty

Tactic:
contrapose! hst
  rcases hs.elim_countable_subfamily_closed t htc hst with ⟨u, ⟨_, husub⟩⟩
  exact ⟨u, fun _ ↦ husub⟩

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : CountableInterFilter f
h : f ≤ 𝓟 s ∧ ∀ x ∈ s, ¬ClusterPt x f
⊢ ∃ ι U, (∀ (i : ι), IsOpen[inst✝] (U i)) ∧ s ⊆ ⋃ i, U i ∧ ∀ (t : Set ι), t.Countable → ¬s ⊆ ⋃ i ∈ t, U i

Tactic:
simp only [ClusterPt, not_neBot, ← disjoint_iff, SetCoe.forall',
    (nhds_basis_opens _).disjoint_iff_left] at h

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : CountableInterFilter f
h : f ≤ 𝓟 s ∧ ∀ (x : ↑s), ∃ i, (↑x ∈ i ∧ IsOpen[inst✝] i) ∧ iᶜ ∈ f
⊢ ∃ ι U, (∀ (i : ι), IsOpen[inst✝] (U i)) ∧ s ⊆ ⋃ i, U i ∧ ∀ (t : Set ι), t.Countable → ¬s ⊆ ⋃ i ∈ t, U i
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 : Subtype.val '' v ↓∩ u = Subtype.val '' ⋃ x ∈ v ↓∩ u, connectedComponent x
⊢ u = ⋃ x ∈ u, connectedComponentIn v x

Tactic:
simp only [Subtype.image_preimage_coe, mem_preimage, iUnion_coe_set, image_val_iUnion,
    inter_eq_right.mpr huv₁] at 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, ⋯⟩
⊢ u = ⋃ x ∈ u, connectedComponentIn v x
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)
a b : Set X
ha : IsClosed[inst✝²] a
hb : IsClosed[inst✝²] b
hab : ⋂ s, ↑s ⊆ a ∪ b
ab_disj : Disjoint a b
u v : Set X
hu : IsOpen[inst✝²] u
hv : IsOpen[inst✝²] v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
H1 : Disjoint (u ∪ v)ᶜ (⋂ i, ↑i) → ∃ x_1, ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ x_1, ↑i).Nonempty
⊢ ∃ s, IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v

Tactic:
obtain ⟨si, H2⟩ :=
      H1 (disjoint_compl_left_iff_subset.2 <| hab.trans <| union_subset_union hau hbv)

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed[inst✝²] (⋂ s, ↑s)
a b : Set X
ha : IsClosed[inst✝²] a
hb : IsClosed[inst✝²] b
hab : ⋂ s, ↑s ⊆ a ∪ b
ab_disj : Disjoint a b
u v : Set X
hu : IsOpen[inst✝²] u
hv : IsOpen[inst✝²] v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
H1 : Disjoint (u ∪ v)ᶜ (⋂ i, ↑i) → ∃ x_1, ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ x_1, ↑i).Nonempty
si : Finset { s // IsClopen s ∧ x ∈ s }
H2 : ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ si, ↑i).Nonempty
⊢ ∃ s, IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
ht : t ⊆ s
hs : IsNowhereDense s
⊢ interior (closure[inst✝] t) ⊆ ∅

Tactic:
by grw [ht]; rw [hs]

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

Goal state before:
pp: case inr.succ.succ.cons.refine_4
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : Infinite (ConnectedComponents α)
h✝ : Nonempty α
n : ℕ
i : Fin (n + 1)
U : Fin n → Set α
a b : Set α
ha : IsClopen a
hb : IsClopen b
ha' : a.Nonempty
hb' : b.Nonempty
hab : Disjoint a b
h₃ : Pairwise (Disjoint on (Equiv.piCongrLeft (fun x ↦ Set α) (Equiv.swap 0 i)).symm (Fin.cons (a ∪ b) U))
h₁ : ∀ (i_1 : Fin (n + 1)), IsClopen (Fin.cons (a ∪ b) U ((Equiv.swap 0 i) i_1))
h₂ : ∀ (i_1 : Fin (n + 1)), (Fin.cons (a ∪ b) U ((Equiv.swap 0 i) i_1)).Nonempty
h₄ : ⋃ i_1, Fin.cons (a ∪ b) U ((Equiv.swap 0 i) i_1) = univ
hi : ¬IsConnected (a ∪ b)
⊢ ⋃ i, Fin.cons a (Fin.cons b U) i = univ

Tactic:
· simpa [← union_assoc, (Equiv.surjective _).iUnion_comp] using h₄

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x : α
⊢ ConnectedComponents.mk ⁻¹' {ConnectedComponents.mk x} = connectedComponent x

Tactic:
by
  ext y
  rw [mem_preimage, mem_singleton_iff, ConnectedComponents.coe_eq_coe']

Goal state after:
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}}
⊢ ⋂ y, {p | p.2 = y → p.1 ∈ {y}} ∈ uniformity Y

Tactic:
Filter.iInter_mem,

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}}
⊢ ∀ (i : Y), {p | p.2 = i → p.1 ∈ {i}} ∈ uniformity Y
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
l : Filter β
f : β → α
⊢ Cauchy (map f l) ↔ l.NeBot ∧ Tendsto (fun p ↦ (f p.1, f p.2)) (l ×ˢ l) (𝓤 α)

Tactic:
by
  rw [Cauchy, map_neBot_iff, prod_map_map_eq, Tendsto]

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ {p | p.2 = x → p.1 ∈ s} ∈ map Prod.swap (𝓤 α)

Tactic:
mem_nhds_uniformity_iff_right

Goal state after:
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ {p | p.1 = x → p.2 ∈ s} ∈ 𝓤 α ↔ {p | p.2 = x → p.1 ∈ s} ∈ map Prod.swap (𝓤 α)
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
⊢ closure[instTopologicalSpaceProd] s = ⋂ V ∈ {V | V ∈ 𝓤 α ∧ SetRel.IsSymm V}, V ○ s ○ V

Tactic:
ext ⟨x, y⟩
  simp +contextual only
    [mem_closure_iff_nhds_basis (UniformSpace.hasBasis_nhds_prod x y), mem_iInter, mem_ofPred_eq,
      and_imp, mem_comp_comp, ← mem_inter_iff, inter_comm, Set.Nonempty]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
⊢ comap (fun x ↦ (f x.1, f x.2)) (𝓤 β) = 𝓤 α ↔ ∀ (s : Set (α × α)), s ∈ 𝓤 α ↔ s ∈ 𝓤 α

Tactic:
Filter.ext_iff

Goal state after:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
⊢ (∀ (s : Set (α × α)), s ∈ comap (fun x ↦ (f x.1, f x.2)) (𝓤 β) ↔ s ∈ 𝓤 α) ↔ ∀ (s : Set (α × α)), s ∈ 𝓤 α ↔ s ∈ 𝓤 α
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 | ∃ b ∈ f '' u, (a, b) ∈ t} ∈ map f F
⊢ SetRel.preimage (Prod.map f f ⁻¹' id t) u ∈ F

Tactic:
exists_mem_image

Goal state after:
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
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
⊢ TendstoLocallyUniformlyOn F f p s ↔ ∀ x ∈ s, TendstoUniformlyOnFilter F f p (𝓝[s] x)

Tactic:
simp only [TendstoUniformlyOnFilter, eventually_prod_iff]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
⊢ TendstoLocallyUniformlyOn F f p s ↔
    ∀ x ∈ s,
      ∀ u ∈ 𝓤 β,
        ∃ pa,
          (∀ᶠ (x : ι) in p, pa x) ∧
            ∃ pb, (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
inst✝ : Finite ι
F : ι → β → α
S : Set β
⊢ UniformEquicontinuousOn F S ↔ ∀ (i : ι), UniformContinuousOn (F i) S

Tactic:
simp only [UniformEquicontinuousOn, eventually_all, @forall_comm _ ι]; rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
h_cover : ∃ I, I.Finite ∧ ⋃ i ∈ I, range (φ i) = univ
⊢ 𝓤 (α →ᵤ β) =
    ⨅ i, comap (Prod.map (⇑ofFun ∘ (fun x ↦ x ∘ φ i) ∘ ⇑toFun) (⇑ofFun ∘ (fun x ↦ x ∘ φ i) ∘ ⇑toFun)) (𝓤 (δ i →ᵤ β))

Tactic:
refine le_antisymm (le_iInf fun i ↦ tendsto_iff_comap.mp UniformFun.precomp_uniformContinuous) ?_

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
h_cover : ∃ I, I.Finite ∧ ⋃ i ∈ I, range (φ i) = univ
⊢ ⨅ i, comap (Prod.map (⇑ofFun ∘ (fun x ↦ x ∘ φ i) ∘ ⇑toFun) (⇑ofFun ∘ (fun x ↦ x ∘ φ i) ∘ ⇑toFun)) (𝓤 (δ i →ᵤ β)) ≤
    𝓤 (α →ᵤ β)
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
F : ι → β → α
f : β → α
S : Set β
h₁ : ∀ x ∈ S, Tendsto (fun x_1 ↦ F x_1 x) l (𝓝 (f x))
h₂ : UniformEquicontinuousOn F S
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
⊢ (fun x ↦ (f x.1, f x.2)) ⁻¹' U ∈ 𝓤 β ⊓ 𝓟 (S ×ˢ S)

Tactic:
filter_upwards [h₂ V hV, mem_inf_of_right (mem_principal_self _)]

Goal state after:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
F : ι → β → α
f : β → α
S : Set β
h₁ : ∀ x ∈ S, Tendsto (fun x_1 ↦ F x_1 x) l (𝓝 (f x))
h₂ : UniformEquicontinuousOn F S
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
⊢ ∀ (a : β × β), (∀ (i : ι), (F i a.1, F i a.2) ∈ V) → a ∈ S ×ˢ S → a ∈ (fun x ↦ (f x.1, f x.2)) ⁻¹' U