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

Goal state before:
pp: case a.inr
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
ht : ¬∃ t ⊂ s, t.Nonempty ∧ IsOpen[inst✝¹] ↑t
⊢ ∃ x ∈ ↑s, IsOpen[inst✝¹] {x}

Tactic:
(Mathlib.Tactic.rsuffices
 "rsuffices"
 [(Tactic.rcasesPatMed
   [(Tactic.rcasesPat.tuple
     "⟨"
     [(Tactic.rcasesPatLo (Tactic.rcasesPatMed [(Tactic.rcasesPat.one `x)]) [])
      ","
      (Tactic.rcasesPatLo (Tactic.rcasesPatMed [(Tactic.rcasesPat.one `hx)]) [])]
     "⟩")])]
 [":"
  («term∃_,_»
   "∃"
   (Lean.explicitBinders (Lean.unbracketedExplicitBinders [(Lean.binderIdent `x)] []))
   ","
   («term_=_»
    (Term.typeAscription (Term.hygienicLParen "(" (hygieneInfo `[anonymous])) `s ":" [(Term.app `Set [`X])] ")")
    "="
    (choice
     («term{_}» "{" [`x] "}")
     (Term.structInst
      "{"
      []
      (Term.structInstFields [(Term.structInstField (Term.structInstLVal `x []) [])])
      (Term.optEllipsis [])
      []
      "}"))))]
 [])

Goal state after:
case a.inr
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
ht : ¬∃ t ⊂ s, t.Nonempty ∧ IsOpen[inst✝¹] ↑t
x : X
hx : ↑s = {x}
⊢ ∃ x ∈ ↑s, IsOpen[inst✝¹] {x}

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
ht : ¬∃ t ⊂ s, t.Nonempty ∧ IsOpen[inst✝¹] ↑t
⊢ ∃ x, ↑s = {x}
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case h.refine_3
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝¹] S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen[inst✝¹] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty { U // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
⊢ (⋃₀ c)ᶜ.Nonempty

Tactic:
convert_to (⋂ U : { U // U ∈ c }, U.1ᶜ).Nonempty
          · ext
            simp only [not_exists, not_and, Set.mem_iInter, Subtype.forall,
              mem_compl_iff, mem_sUnion]
          apply IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
          · rintro ⟨U, hU⟩ ⟨U', hU'⟩
            obtain ⟨V, hVc, hVU, hVU'⟩ := hz.directedOn U hU U' hU'
            exact ⟨⟨V, hVc⟩, Set.compl_subset_compl.mpr hVU, Set.compl_subset_compl.mpr hVU'⟩
          · exact fun U => (hc U.2).2.2
          · exact fun U => (hc U.2).2.1.isClosed_compl.isCompact
          · exact fun U => (hc U.2).2.1.isClosed_compl

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ T2Space (SeparationQuotient X) ↔ R1Space X

Tactic:
simp only [t2Space_iff_disjoint_nhds, Pairwise, surjective_mk.forall₂, ne_eq, mk_eq_mk,
    r1Space_iff_inseparable_or_disjoint_nhds, ← disjoint_comap_iff surjective_mk, comap_mk_nhds_mk,
    ← or_iff_not_imp_left]

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ T2Space X ↔ ∀ {x y : X}, (𝓝 x ⊓ 𝓝 y).NeBot → x = y

Tactic:
by
  simp only [t2Space_iff_disjoint_nhds, disjoint_iff, neBot_iff, Ne, not_imp_comm, Pairwise]

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

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
f : X → Y
hf : Continuous[inst✝², inst✝¹] f
⊢ ∀ (a b : X), a ≈ b → f a = f b

Tactic:
change t2Setoid X ≤ Setoid.ker f

Goal state after:
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
f : X → Y
hf : Continuous[inst✝², inst✝¹] f
⊢ t2Setoid X ≤ Setoid.ker f
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
z : X
h₁z : z ∈ U
t : Set X
h₁t : t ∈ 𝓝[≠] z
h₂t : t ∩ (U \ s) = ∅
hz : z ∉ U \ s
⊢ (insert z t ∩ (U \ s)).Finite

Tactic:
· rw [inter_comm, inter_insert_of_notMem hz, inter_comm, h₂t]
      simp

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

Goal state before:
pp: X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
hx : (𝓝[≠] x).NeBot
s : Set X
hs : s ∈ 𝓝 x
⊢ s.Infinite

Tactic:
refine fun hsf => hx.1 ?_
  rw [← isOpen_singleton_iff_punctured_nhds]
  exact isOpen_singleton_of_finite_mem_nhds x hs hsf

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

Goal state before:
pp: case refine_2.mk.mk
X : Type u_1
inst✝ : TopologicalSpace X
h : Std.Symm Specializes
x✝ : SeparationQuotient X
x : X
y✝ : SeparationQuotient X
y : X
sxspecsy : Quot.mk (⇑(inseparableSetoid X)) x ⤳ Quot.mk (⇑(inseparableSetoid X)) y
xspecy : x ⤳ y
yspecx : y ⤳ x
⊢ mk x = mk y

Tactic:
rw [mk_eq_mk, inseparable_iff_specializes_and]

Goal state after:
case refine_2.mk.mk
X : Type u_1
inst✝ : TopologicalSpace X
h : Std.Symm Specializes
x✝ : SeparationQuotient X
x : X
y✝ : SeparationQuotient X
y : X
sxspecsy : Quot.mk (⇑(inseparableSetoid X)) x ⤳ Quot.mk (⇑(inseparableSetoid X)) y
xspecy : x ⤳ y
yspecx : y ⤳ x
⊢ x ⤳ y ∧ y ⤳ x
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
K : Set X
inst✝ : T1Space X
hK : IsCompact K
⊢ codiscreteWithin K = cofinite ⊓ 𝓟 K

Tactic:
refine le_antisymm ?_ hK.cofinite_inf_le_codiscreteWithin
  grw [← codiscrete_le_cofinite]
  exact codiscreteWithin_le_codiscrete_inf_principal K

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
x y : X
⊢ Disjoint (𝓝 x) (𝓝 y) ↔ ¬Inseparable x y

Tactic:
disjoint_nhds_nhds_iff_not_specializes,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
x y : X
⊢ ¬x ⤳ y ↔ ¬Inseparable x y
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsDiscrete s
ht✝ : IsDiscrete t
hsc : IsClosed[inst✝] s
ht : IsClosed[inst✝] t
⊢ IsDiscrete (s ∪ t)

Tactic:
by
  rw [union_eq_iUnion]
  exact .iUnion (by simp [*]) (by simp [*])

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

Goal state before:
pp: case insert.refine_2.inl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
ι : Type u_3
t : Finset ι
ih :
  ∀ {s : Set X},
    IsCompact s →
      ∀ (U : ι → Set X),
        (∀ i ∈ t, IsOpen[inst✝¹] (U i)) →
          s ⊆ ⋃ i ∈ t, U i → ∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
s : Set X
hs : IsCompact s
U : ι → Set X
hU' : ∀ i ∈ t, IsOpen[inst✝¹] (U i)
K₁ K₂ : Set X
h1K₁ : IsCompact K₁
h1K₂ : IsCompact K₂
h2K₂ : K₂ ⊆ ⋃ i ∈ ↑t, U i
hK : s = K₁ ∪ K₂
K : ι → Set X
h1K : ∀ (i : ι), IsCompact (K i)
h2K : ∀ (i : ι), K i ⊆ U i
h3K : K₂ = ⋃ i ∈ t, K i
i : ι
hx : i ∉ t
hsC : s ⊆ U i ∪ ⋃ x ∈ t, U x
hU : IsOpen[inst✝¹] (U i) ∧ ∀ x ∈ t, IsOpen[inst✝¹] (U x)
h2K₁ : K₁ ⊆ U i
⊢ update K i K₁ i ⊆ U i

pp: case insert.refine_2.inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
ι : Type u_3
x : ι
t : Finset ι
hx : x ∉ t
ih :
  ∀ {s : Set X},
    IsCompact s →
      ∀ (U : ι → Set X),
        (∀ i ∈ t, IsOpen[inst✝¹] (U i)) →
          s ⊆ ⋃ i ∈ t, U i → ∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
s : Set X
hs : IsCompact s
U : ι → Set X
hsC : s ⊆ U x ∪ ⋃ x ∈ t, U x
hU : IsOpen[inst✝¹] (U x) ∧ ∀ x ∈ t, IsOpen[inst✝¹] (U x)
hU' : ∀ i ∈ t, IsOpen[inst✝¹] (U i)
K₁ K₂ : Set X
h1K₁ : IsCompact K₁
h1K₂ : IsCompact K₂
h2K₁ : K₁ ⊆ U x
h2K₂ : K₂ ⊆ ⋃ i ∈ ↑t, U i
hK : s = K₁ ∪ K₂
K : ι → Set X
h1K : ∀ (i : ι), IsCompact (K i)
h2K : ∀ (i : ι), K i ⊆ U i
h3K : K₂ = ⋃ i ∈ t, K i
i : ι
hi : i ≠ x
⊢ update K x K₁ i ⊆ U i

Tactic:
· simp only [update_self, h2K₁]

Goal state after:
case insert.refine_2.inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
ι : Type u_3
x : ι
t : Finset ι
hx : x ∉ t
ih :
  ∀ {s : Set X},
    IsCompact s →
      ∀ (U : ι → Set X),
        (∀ i ∈ t, IsOpen[inst✝¹] (U i)) →
          s ⊆ ⋃ i ∈ t, U i → ∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
s : Set X
hs : IsCompact s
U : ι → Set X
hsC : s ⊆ U x ∪ ⋃ x ∈ t, U x
hU : IsOpen[inst✝¹] (U x) ∧ ∀ x ∈ t, IsOpen[inst✝¹] (U x)
hU' : ∀ i ∈ t, IsOpen[inst✝¹] (U i)
K₁ K₂ : Set X
h1K₁ : IsCompact K₁
h1K₂ : IsCompact K₂
h2K₁ : K₁ ⊆ U x
h2K₂ : K₂ ⊆ ⋃ i ∈ ↑t, U i
hK : s = K₁ ∪ K₂
K : ι → Set X
h1K : ∀ (i : ι), IsCompact (K i)
h2K : ∀ (i : ι), K i ⊆ U i
h3K : K₂ = ⋃ i ∈ t, K i
i : ι
hi : i ≠ x
⊢ update K x K₁ i ⊆ U i
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: α : Type u_2
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s : (i : ι) → i ∈ S → Set α
this : Encodable ↑S
⊢ ⋂ x, s ↑x ⋯ ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l

Tactic:
exact countable_iInter_mem.trans Subtype.forall

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

Goal state before:
pp: α : Type u
ι : Type u_1
X : ι → Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : ConnectedSpace α
inst✝ : (i : ι) → TopologicalSpace (X i)
f : α → (i : ι) × X i
hf : Continuous[inst✝², instTopologicalSpaceSigma] f
⊢ ∃ i g, Continuous[inst✝², inst✝ i] g ∧ f = Sigma.mk i ∘ g

Tactic:
by
  obtain ⟨i, hi⟩ : ∃ i, range f ⊆ range (.mk i) := by
    rcases Sigma.isConnected_iff.1 (isConnected_range hf) with ⟨i, s, -, hs⟩
    exact ⟨i, hs.trans_subset (image_subset_range _ _)⟩
  rcases range_subset_range_iff_exists_comp.1 hi with ⟨g, rfl⟩
  refine ⟨i, g, ?_, rfl⟩
  rwa [← IsEmbedding.sigmaMk.continuous_iff] at hf

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsClosed[inst✝] t
⊢ IsLindelof (s ∩ t)

Tactic:
intro f hnf _ hstf

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsClosed[inst✝¹] t
f : Filter X
hnf : f.NeBot
inst✝ : CountableInterFilter f
hstf : f ≤ 𝓟 (s ∩ t)
⊢ ∃ x ∈ s ∩ t, ClusterPt x f
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst✝] ≤ 𝓝 x
tfae_5_to_6 : (∀ (x : X), (𝓝 x).lift' closure[inst✝] ≤ 𝓝 x) → ∀ (x : X), (𝓝 x).lift' closure[inst✝] = 𝓝 x
tfae_6_to_4 : (∀ (x : X), (𝓝 x).lift' closure[inst✝] = 𝓝 x) → ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst✝] t ∧ t ⊆ s
H : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst✝] t ∧ t ⊆ s
s : Set X
a : X
ha : a ∉ closure[inst✝] s
⊢ sᶜ ∈ 𝓝 a

Tactic:
rwa [← mem_interior_iff_mem_nhds, interior_compl]

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
⊢ ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, U ↑x ⋯

Tactic:
have := hs.elim_countable_subcover (fun x : s ↦ interior (U x x.2)) (fun _ ↦ isOpen_interior)
    fun x hx ↦
      mem_iUnion.2 ⟨⟨x, hx⟩, mem_interior_iff_mem_nhds.2 <| hU _ _⟩

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
this : ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, interior (U ↑i ⋯)
⊢ ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, U ↑x ⋯
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: case h.right.h
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
i : Type u
U : i → Set X
hU : ∀ (i : i), IsOpen[inst✝] (U i)
hUcover : ⋃ i ∈ s, f i ⊆ ⋃ i, U i
hiU : ∀ i_1 ∈ s, f i_1 ⊆ ⋃ i, U i
r : ι → Set i
hr : ∀ i_1 ∈ s, (r i_1).Countable ∧ f i_1 ⊆ ⋃ i_2 ∈ r i_1, U i_2
⊢ ∀ i_1 ∈ s, f i_1 ⊆ ⋃ i_2 ∈ ⋃ i_3 ∈ s, r i_3, U i_2

Tactic:
intro i is

Goal state after:
case h.right.h
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
i✝ : Type u
U : i✝ → Set X
hU : ∀ (i : i✝), IsOpen[inst✝] (U i)
hUcover : ⋃ i ∈ s, f i ⊆ ⋃ i, U i
hiU : ∀ i ∈ s, f i ⊆ ⋃ i, U i
r : ι → Set i✝
hr : ∀ i ∈ s, (r i).Countable ∧ f i ⊆ ⋃ i_1 ∈ r i, U i_1
i : ι
is : i ∈ s
⊢ f i ⊆ ⋃ i ∈ ⋃ i ∈ s, r i, U i
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : 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
⊢ f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v

Tactic:
let T₁ := { t' ∈ t | f ⁻¹' {t'} ⊆ u }

Goal state after:
α : 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}
⊢ f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
di : IsDenseInducing i
b : β
s : Set β
hs : s ∈ 𝓝 b
⊢ ∃ a, i a ∈ s

Tactic:
rcases mem_closure_iff_nhds.1 (di.dense b) s hs with ⟨_, ⟨ha, a, rfl⟩⟩
    exact ⟨a, ha⟩

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
⊢ IsLindelof s ↔ IsLindelof (f '' s)

Tactic:
refine ⟨fun hs => hs.image hf.continuous, fun hs F F_ne_bot _ F_le => ?_⟩
  obtain ⟨_, ⟨x, x_in : x ∈ s, rfl⟩, hx : ClusterPt (f x) (map f F)⟩ :=
    hs ((map_mono F_le).trans_eq map_principal)
  exact ⟨x, x_in, hf.mapClusterPt_iff.1 hx⟩

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

Goal state before:
pp: X : Type u
Y : Type v
ι : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
s t : Set X
inst✝¹ : LindelofSpace X
inst✝ : LindelofSpace Y
⊢ IsLindelof (range Sum.inl ∪ range Sum.inr)

Tactic:
exact (isLindelof_range continuous_inl).union (isLindelof_range continuous_inr)

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

Goal state before:
pp: X : Type u
Y : Type v
ι : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s t✝ : Set X
inst✝ : SecondCountableTopology X
t : Set X
x✝¹ : t ⊆ univ
x✝ : Filter X
⊢ ∀ {ι : Type u} (U : ι → Set X),
    (∀ (i : ι), IsOpen[inst✝²] (U i)) → t ⊆ ⋃ i, U i → ∃ t_1, t_1.Countable ∧ t ⊆ ⋃ i ∈ t_1, U i

Tactic:
intro ι U hι hcover

Goal state after:
X : Type u
Y : Type v
ι✝ : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s t✝ : Set X
inst✝ : SecondCountableTopology X
t : Set X
x✝¹ : t ⊆ univ
x✝ : Filter X
ι : Type u
U : ι → Set X
hι : ∀ (i : ι), IsOpen[inst✝²] (U i)
hcover : t ⊆ ⋃ i, U i
⊢ ∃ t_1, t_1.Countable ∧ t ⊆ ⋃ i ∈ t_1, U i
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
s : Set ι
hs : s.Finite
f : ι → Set X
h : ∀ i ∈ s, IsGδ (f i)
⊢ IsGδ (⋃ i ∈ s, f i)

Tactic:
rw [← sUnion_image]
  exact .sUnion (hs.image _) (forall_mem_image.2 h)

Goal state after:
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
hof : ∀ (n : ℕ), IsOpen[inst✝] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : ℕ → Set X := fun n ↦ p '' f n ∪ (closure[inst✝²] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst✝²] (c n)
n : ℕ
⊢ closure[inst✝²] (c n) = univ

Tactic:
subset_antisymm_iff

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)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : ℕ → Set X := fun n ↦ p '' f n ∪ (closure[inst✝²] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst✝²] (c n)
n : ℕ
⊢ closure[inst✝²] (c n) ⊆ univ ∧ univ ⊆ closure[inst✝²] (c n)
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 : IsMeagre s
⊢ IsMeagre (f '' s)

Tactic:
rw [isMeagre_iff_countable_union_isNowhereDense] at *

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 : ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S
⊢ ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ f '' s ⊆ ⋃₀ S
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsCoinducing f
h_fibers : ∀ (y : β), IsConnected (f ⁻¹' {y})
a : α
⊢ f '' f ⁻¹' connectedComponent (f a) = connectedComponent (f a)

Tactic:
image_preimage_eq _ fun y ↦ (h_fibers y).nonempty

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsCoinducing f
h_fibers : ∀ (y : β), IsConnected (f ⁻¹' {y})
a : α
⊢ connectedComponent (f a) = connectedComponent (f a)
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
⊢ T2Space (ConnectedComponents X)

Tactic:
by
  -- Fix 2 distinct connected components, with points a and b
  refine ⟨ConnectedComponents.surjective_coe.forall₂.2 fun a b ne => ?_⟩
  rw [ConnectedComponents.coe_ne_coe] at ne
  have h := connectedComponent_disjoint ne
  -- write ↑b as the intersection of all clopen subsets containing it
  rw [connectedComponent_eq_iInter_isClopen b, disjoint_iff_inter_eq_empty] at h
  -- Now we show that this can be reduced to some clopen containing `↑b` being disjoint to `↑a`
  obtain ⟨U, V, hU, ha, hb, rfl⟩ : ∃ (U : Set X) (V : Set (ConnectedComponents X)),
      IsClopen U ∧ connectedComponent a ∩ U = ∅ ∧ connectedComponent b ⊆ U ∧ (↑) ⁻¹' V = U := by
    have h :=
      (isClosed_connectedComponent (α := X)).isCompact.elim_finite_subfamily_closed
        _ (fun s : { s : Set X // IsClopen s ∧ b ∈ s } => s.2.1.1) h
    obtain ⟨fin_a, ha⟩ := h
    -- This clopen and its complement will separate the connected components of `a` and `b`
    set U : Set X := ⋂ (i : { s // IsClopen s ∧ b ∈ s }) (_ : i ∈ fin_a), i
    have hU : IsClopen U := isClopen_biInter_finset fun i _ => i.2.1
    exact ⟨U, (↑) '' U, hU, ha, subset_iInter₂ fun s _ => s.2.1.connectedComponent_subset s.2.2,
      (connectedComponents_preimage_image U).symm ▸ hU.biUnion_connectedComponent_eq⟩
  rw [ConnectedComponents.isQuotientMap_coe.isClopen_preimage] at hU
  refine ⟨Vᶜ, V, hU.compl.isOpen, hU.isOpen, ?_, hb mem_connectedComponent, disjoint_compl_left⟩
  exact fun h => flip Set.Nonempty.ne_empty ha ⟨a, mem_connectedComponent, h⟩

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

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

Tactic:
have : u₁.toTopologicalSpace = u₂.toTopologicalSpace := TopologicalSpace.ext_nhds fun x ↦ by
    rw [u₁.nhds_eq_comap_uniformity, u₂.nhds_eq_comap_uniformity]
    exact congr_arg (comap _) h

Goal state after:
α : Type ua
u₁ u₂ : UniformSpace α
h : 𝓤 α = 𝓤 α
this : u₁.toTopologicalSpace = u₂.toTopologicalSpace
⊢ u₁ = u₂
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
x y : α
⊢ ∀ {i j : SetRel α α},
    i ∈ 𝓤 α ∧ i.IsSymm → j ∈ 𝓤 α ∧ j.IsSymm → ∃ k, (k ∈ 𝓤 α ∧ k.IsSymm) ∧ ball x k ⊆ ball x i ∧ ball y k ⊆ ball y j

Tactic:
rintro U V ⟨U_in, U_symm⟩ ⟨V_in, V_symm⟩

Goal state after:
α : Type ua
inst✝ : UniformSpace α
x y : α
U V : SetRel α α
U_in : U ∈ 𝓤 α
U_symm : U.IsSymm
V_in : V ∈ 𝓤 α
V_symm : V.IsSymm
⊢ ∃ k, (k ∈ 𝓤 α ∧ k.IsSymm) ∧ ball x k ⊆ ball x U ∧ ball y k ⊆ ball y V
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: case mpr
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ (∃ V ∈ 𝓤 α, SetRel.IsSymm V ∧ ball x V ⊆ s) → ∃ V ∈ 𝓤 α, ball x V ⊆ s

Tactic:
rintro ⟨V, V_in, _, V_sub⟩
    exact ⟨V, V_in, V_sub⟩

Goal state after:
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 ∧ ∀ x ∈ s ia ∩ S ×ˢ S, (f x.1, f x.2) ∈ t ib) ↔
    ∀ (i : ι'), q i → ∃ j, p j ∧ ∀ x ∈ S, ∀ y ∈ S, (x, y) ∈ s j → (f x, f y) ∈ t i

Tactic:
Prod.forall,

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 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
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
⊢ (∀ (x y : α), (∀ r ∈ 𝓤 α, (x, y) ∈ r) → x = y) ↔ (∀ x ∈ (𝓤 α).ker, x ∈ diagonal α) ∧ ∀ (x : α), (x, x) ∈ (𝓤 α).ker

Tactic:
Prod.forall,

Goal state after:
α : Type u
inst✝ : UniformSpace α
⊢ (∀ (x y : α), (∀ r ∈ 𝓤 α, (x, y) ∈ r) → x = y) ↔
    (∀ (a b : α), (a, b) ∈ (𝓤 α).ker → (a, b) ∈ diagonal α) ∧ ∀ (x : α), (x, x) ∈ (𝓤 α).ker
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f₁ : α → β
f₂ : α → γ
h₁ : UniformContinuous f₁
h₂ : UniformContinuous f₂
⊢ UniformContinuous fun a ↦ (f₁ a, f₂ a)

Tactic:
rw [UniformContinuous, uniformity_prod]

Goal state after:
α : Type ua
β : Type ub
γ : Type uc
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f₁ : α → β
f₂ : α → γ
h₁ : UniformContinuous f₁
h₂ : UniformContinuous f₂
⊢ Tendsto (fun x ↦ ((f₁ x.1, f₂ x.1), f₁ x.2, f₂ x.2)) (𝓤 α)
    (Filter.comap (fun p ↦ (p.1.1, p.2.1)) (𝓤 β) ⊓ Filter.comap (fun p ↦ (p.1.2, p.2.2)) (𝓤 γ))
Module: Mathlib.Topology.UniformSpace.Separation

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

Tactic:
simp only [Filter.comap_comap, Function.comp_def, Prod.map_apply]

Goal state after: