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

Goal state before:
pp: case inr
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)
H : T1Space X
s : Set (CofiniteTopology X)
hs : sᶜ.Finite
⊢ IsOpen[inst✝] (⇑CofiniteTopology.of ⁻¹' s)

Tactic:
← compl_compl s,

Goal state after:
case inr
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)
H : T1Space X
s : Set (CofiniteTopology X)
hs : sᶜ.Finite
⊢ IsOpen[inst✝] (⇑CofiniteTopology.of ⁻¹' sᶜᶜ)
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: case inl
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 : X
x✝ : (x, x) ∈ s ×ˢ s
hx : (x, x).1 ∈ s
hy : (x, x).2 ∈ s
⊢ ∀ᶠ (y : X × X) in 𝓝 (x, x), f y.1 = f y.2 → y.1 = y.2

Tactic:
rcases loc x hx with ⟨u, hu, hf⟩
      exact Filter.mem_of_superset (prod_mem_nhds hu hu) <| forall_prod_set.2 hf

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
hs : s ∈ cofinite
⊢ s ∈ codiscrete X

Tactic:
← compl_compl s,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
hs : s ∈ cofinite
⊢ sᶜᶜ ∈ codiscrete X
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case insert.refine_1
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 : ι), IsCompact (update K x K₁ i)

Tactic:
intro i

Goal state after:
case insert.refine_1
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 : ι
⊢ IsCompact (update K x K₁ i)
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case insert.refine_2
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 : ι), update K x K₁ i ⊆ U i

Tactic:
intro i

Goal state after:
case insert.refine_2
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 : ι
⊢ update K x K₁ i ⊆ U i
Module: Mathlib.Topology.Order.OrderClosed

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

Tactic:
simp only [isClosed_iff_clusterPt, clusterPt_principal_iff_frequently]
  exact fun g hg => monotoneOn_of_frequently_monotoneOn_of_tendsto hg
    fun x _ ↦ continuousAt_apply x g

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

Goal state before:
pp: X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
⊢ R1Space X

Tactic:
let _ := sInf T

Goal state after:
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x✝ : TopologicalSpace X := sInf T
⊢ R1Space X
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
x : α
H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
⊢ IsPreconnected s

Tactic:
rintro u v hu hv hs ⟨z, zs, zu⟩ ⟨y, ys, yv⟩
  have xs : x ∈ s := by
    rcases H y ys with ⟨t, ts, xt, -, -⟩
    exact ts xt
  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11215): TODO: use `wlog xu : x ∈ u := hs xs using u v y z, v u z y`
  cases hs xs with
  | inl xu =>
    rcases H y ys with ⟨t, ts, xt, yt, ht⟩
    have := ht u v hu hv (ts.trans hs) ⟨x, xt, xu⟩ ⟨y, yt, yv⟩
    exact this.imp fun z hz => ⟨ts hz.1, hz.2⟩
  | inr xv =>
    rcases H z zs with ⟨t, ts, xt, zt, ht⟩
    have := ht v u hv hu (ts.trans <| by rwa [union_comm]) ⟨x, xt, xv⟩ ⟨z, zt, zu⟩
    exact this.imp fun _ h => ⟨ts h.1, h.2.2, h.2.1⟩

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

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst✝², inst✝¹] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
U V : Set Y
Uo : IsOpen[inst✝¹] U
Vo : IsOpen[inst✝¹] V
hxU : {f x} ⊆ U
hV : f '' K \ interior s ⊆ V
hd : Disjoint U V
⊢ ∃ L ∈ 𝓝 x, IsCompact L ∧ MapsTo f L s

Tactic:
refine ⟨K \ f ⁻¹' V, sdiff_mem hKx ?_, hKc.diff <| Vo.preimage hf, fun y hy ↦ ?_⟩

Goal state after:
case refine_1
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst✝², inst✝¹] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
U V : Set Y
Uo : IsOpen[inst✝¹] U
Vo : IsOpen[inst✝¹] V
hxU : {f x} ⊆ U
hV : f '' K \ interior s ⊆ V
hd : Disjoint U V
⊢ (f ⁻¹' V)ᶜ ∈ 𝓝 x

case refine_2
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst✝², inst✝¹] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
U V : Set Y
Uo : IsOpen[inst✝¹] U
Vo : IsOpen[inst✝¹] V
hxU : {f x} ⊆ U
hV : f '' K \ interior s ⊆ V
hd : Disjoint U V
y : X
hy : y ∈ K \ f ⁻¹' V
⊢ f y ∈ s
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : R1Space X
inst✝ : WeaklyLocallyCompactSpace X
K : Set X
hK : IsCompact K
⊢ ∃ V, IsOpen[inst✝²] V ∧ K ⊆ V ∧ IsCompact (closure[inst✝²] V)

Tactic:
by
  rcases exists_compact_superset hK with ⟨K', hK', hKK'⟩
  exact ⟨interior K', isOpen_interior, hKK', hK'.closure_of_subset interior_subset⟩

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

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
h : F ∈ 𝓝 x
⊢ connectedComponentIn F x ∈ 𝓝 x

Tactic:
(LocallyConnectedSpace.open_connected_basis x).mem_iff

Goal state after:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
h : ∃ i, (IsOpen[inst✝¹] i ∧ x ∈ i ∧ IsConnected i) ∧ id i ⊆ F
⊢ connectedComponentIn F x ∈ 𝓝 x
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: case refine_1
ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝ : CountableInterFilter l✝
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : S ⊆ {s | sᶜ ∈ l}
⊢ ⋃₀ (compl '' S) ∈ l

Tactic:
apply hUnion (compl '' S) (hSc.image _)

Goal state after:
case refine_1
ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝ : CountableInterFilter l✝
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : S ⊆ {s | sᶜ ∈ l}
⊢ ∀ s ∈ compl '' S, s ∈ l
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: case refine_2
ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝ : CountableInterFilter l✝
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
s t : Set α
ht : s ∈ {s | sᶜ ∈ l}
hsub : s ⊆ t
⊢ t ∈ {s | sᶜ ∈ l}

Tactic:
mem_ofPred_eq

Goal state after:
case refine_2
ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝ : CountableInterFilter l✝
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
s t : Set α
ht : s ∈ {s | sᶜ ∈ l}
hsub : s ⊆ t
⊢ tᶜ ∈ l
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: case right
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
r : Set ↑s
hr : r.Countable
hs : s ⊆ ⋃ i ∈ r, interior (U ↑i ⋯)
⊢ ∀ i ∈ r, interior (U ↑i ⋯) ⊆ ⋃ x ∈ r, U ↑x ⋯

Tactic:
intro i

Goal state after:
case right
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
r : Set ↑s
hr : r.Countable
hs : s ⊆ ⋃ i ∈ r, interior (U ↑i ⋯)
i : ↑s
⊢ i ∈ r → interior (U ↑i ⋯) ⊆ ⋃ x ∈ r, U ↑x ⋯
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s u : Set α
hs : IsPreconnected s
hu : IsOpen[inst✝] u
h'u : (s ∩ u).Nonempty
h : closure[inst✝] u ∩ s ⊆ u
⊢ s ⊆ u

Tactic:
have A : s ⊆ u ∪ (closure u)ᶜ := by
    intro x hx
    by_cases xu : x ∈ u
    · exact Or.inl xu
    · right
      intro h'x
      exact xu (h (mem_inter h'x hx))

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s u : Set α
hs : IsPreconnected s
hu : IsOpen[inst✝] u
h'u : (s ∩ u).Nonempty
h : closure[inst✝] u ∩ s ⊆ u
A : s ⊆ u ∪ (closure[inst✝] u)ᶜ
⊢ s ⊆ u
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_3
T : Set (TopologicalSpace X)
h : ∀ t ∈ T, RegularSpace X
⊢ RegularSpace X

Tactic:
let _ := sInf T

Goal state after:
X : Type u_3
T : Set (TopologicalSpace X)
h : ∀ t ∈ T, RegularSpace X
x✝ : TopologicalSpace X := sInf T
⊢ RegularSpace X
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
x y : X
h : ¬Inseparable x y
⊢ ∃ U₁ ∈ 𝓝 x,
    ∃ V₁ ∈ 𝓝 x,
      ∃ U₂ ∈ 𝓝 y,
        ∃ V₂ ∈ 𝓝 y,
          IsClosed[inst✝¹] V₁ ∧
            IsClosed[inst✝¹] V₂ ∧ IsOpen[inst✝¹] U₁ ∧ IsOpen[inst✝¹] U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂

Tactic:
rcases r1_separation h with ⟨U₁, U₂, U₁_op, U₂_op, x_in, y_in, H⟩

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
x y : X
h : ¬Inseparable x y
U₁ U₂ : Set X
U₁_op : IsOpen[inst✝¹] U₁
U₂_op : IsOpen[inst✝¹] U₂
x_in : x ∈ U₁
y_in : y ∈ U₂
H : Disjoint U₁ U₂
⊢ ∃ U₁ ∈ 𝓝 x,
    ∃ V₁ ∈ 𝓝 x,
      ∃ U₂ ∈ 𝓝 y,
        ∃ V₂ ∈ 𝓝 y,
          IsClosed[inst✝¹] V₁ ∧
            IsClosed[inst✝¹] V₂ ∧ IsOpen[inst✝¹] U₁ ∧ IsOpen[inst✝¹] U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
⊢ ∀ {ι_1 : Type u} (U : ι_1 → Set X),
    (∀ (i : ι_1), IsOpen[inst✝] (U i)) → ⋃ i ∈ s, f i ⊆ ⋃ i, U i → ∃ t, t.Countable ∧ ⋃ i ∈ s, f i ⊆ ⋃ i ∈ t, U i

Tactic:
intro i

Goal state after:
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),
    (∀ (i : i), IsOpen[inst✝] (U i)) → ⋃ i ∈ s, f i ⊆ ⋃ i, U i → ∃ t, t.Countable ∧ ⋃ i ∈ s, f i ⊆ ⋃ i_1 ∈ t, U i_1
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

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 : ι
⊢ i ∈ s → f i ⊆ ⋃ i ∈ ⋃ i ∈ s, r i, U i
Module: Mathlib.Topology.Connected.Basic

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

Tactic:
connectedComponentIn_eq_image hy,

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
a b : Set α
ha : IsClopen a
hb : IsClopen b
ha' : a.Nonempty
hb' : b.Nonempty
hab : Disjoint a b
hs : IsClopen (a ∪ b)
H : IsPreconnected (a ∪ b)
⊢ ((a ∪ b) ∩ b).Nonempty

Tactic:
union_inter_cancel_right

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
a b : Set α
ha : IsClopen a
hb : IsClopen b
ha' : a.Nonempty
hb' : b.Nonempty
hab : Disjoint a b
hs : IsClopen (a ∪ b)
H : IsPreconnected (a ∪ b)
⊢ b.Nonempty
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: case mp.refine_1
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : Y → ι
h₁ : IsLindelof (⋃ i, (b ∘ f') i)
h₂ : IsOpen[inst✝] (⋃ i, (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ ⋃ i, (b ∘ f') i ⊆ ⋃ i ∈ t, (b ∘ f') i
⊢ ∀ i ∈ t, (b ∘ f') i ⊆ ⋃ i ∈ f' '' t, b i

Tactic:
intro i

Goal state after:
case mp.refine_1
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : Y → ι
h₁ : IsLindelof (⋃ i, (b ∘ f') i)
h₂ : IsOpen[inst✝] (⋃ i, (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ ⋃ i, (b ∘ f') i ⊆ ⋃ i ∈ t, (b ∘ f') i
i : Y
⊢ i ∈ t → (b ∘ f') i ⊆ ⋃ i ∈ f' '' t, b i
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
r : X → X → Prop
inst✝ : LindelofSpace X
⊢ IsLindelof univ

Tactic:
by
    rw [← range_quot_mk]
    exact isLindelof_range continuous_quot_mk

Goal state after:
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
T : Set (Set X)
isNowhereDense : ∀ t ∈ T, IsNowhereDense t
countable : T.Countable
cover : s ⊆ ⋃₀ T
u : Set Y
⊢ u ∈ image f '' T → IsNowhereDense u

Tactic:
⟨t, tT, tu⟩

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
T : Set (Set X)
isNowhereDense : ∀ t ∈ T, IsNowhereDense t
countable : T.Countable
cover : s ⊆ ⋃₀ T
u : Set Y
t : Set X
tT : t ∈ T
tu : f '' t = u
⊢ IsNowhereDense u
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: case pos
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
s : Set X
H : IsClopen s ∧ x ∈ s ∧ s ⊆ v ∪ u
H1 : IsClopen (s ∩ u)
H2 : IsClopen (s ∩ v)
hxu : x ∈ u
⊢ ⋂ s, ↑s ⊆ u

Tactic:
· apply Subset.trans _ s.inter_subset_right
        exact iInter_subset (fun s : { s : Set X // IsClopen s ∧ x ∈ s } => s.1)
          ⟨s ∩ u, H1, mem_inter H.2.1 hxu⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
p' : Filter α
h : TendstoUniformlyOnFilter F f p p'
hx : 𝓟 {x} ≤ p'
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ ∀ (a : ι), (∀ᶠ (y : α) in p', (f y, F a y) ∈ u) → a ∈ (fun x_1 ↦ (f x, F x_1 x)) ⁻¹' u

Tactic:
intro i

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
p' : Filter α
h : TendstoUniformlyOnFilter F f p p'
hx : 𝓟 {x} ≤ p'
u : Set (β × β)
hu : u ∈ 𝓤 β
i : ι
⊢ (∀ᶠ (y : α) in p', (f y, F i y) ∈ u) → i ∈ (fun x_1 ↦ (f x, F x_1 x)) ⁻¹' u
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
⊢ T0Space α ↔ (𝓤 α).ker = diagonal α

Tactic:
simp_rw [t0Space_iff_uniformity, subset_antisymm_iff, diagonal_subset_iff, subset_def,
    Prod.forall, Filter.mem_ker, mem_diagonal_iff, iff_self_and]

Goal state after:
α : Type u
inst✝ : UniformSpace α
⊢ (∀ (x y : α), (∀ r ∈ 𝓤 α, (x, y) ∈ r) → x = y) → ∀ (x : α), ∀ s ∈ 𝓤 α, (x, x) ∈ s
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
ι : Type u_1
I : Set ι
hI : I.Finite
f : ι → Filter α
⊢ (⨆ i ∈ I, f i).TotallyBounded ↔ ∀ i ∈ I, (f i).TotallyBounded

Tactic:
have := hI.to_subtype
  rw [iSup_subtype', totallyBounded_iSup, Subtype.forall]

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
⊢ ∀ (i : ℕ), p i → ∃ t, t.Finite ∧ interUnionBalls xs u U ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U i}

Tactic:
intro i

Goal state after:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
i : ℕ
⊢ p i → ∃ t, t.Finite ∧ interUnionBalls xs u U ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U i}
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
inst✝ : CompleteSpace α
xs : ℕ → α
u : ℕ → ℕ
⊢ IsCompact (closure[uniformSpace.toTopologicalSpace] (interUnionBalls xs u U))

Tactic:
rw [isCompact_iff_totallyBounded_isComplete]

Goal state after:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
inst✝ : CompleteSpace α
xs : ℕ → α
u : ℕ → ℕ
⊢ TotallyBounded (closure[uniformSpace.toTopologicalSpace] (interUnionBalls xs u U)) ∧
    IsComplete (closure[uniformSpace.toTopologicalSpace] (interUnionBalls xs u U))
Module: Mathlib.Topology.UniformSpace.CompleteSeparated

Goal state before:
pp: α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : T0Space α
s : Set α
h : IsComplete s
a : α
ha : ClusterPt a (𝓟 s)
f : Filter α := 𝓝[s] a
this : Cauchy f
y : α
ys : y ∈ s
fy : f ≤ 𝓝 y
⊢ a ∈ s

Tactic:
rwa [(tendsto_nhds_unique' ha inf_le_left fy : a = y)]

Goal state after:
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: case refine_3
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i ↦ mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := {i ∈ hnf.toFinset | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset | x ∉ U j}
z : X
hzn : z ∈ n
hz : ∀ (i : ι), (mulSupport (f i) ∩ n).Nonempty → x ∉ U i → z ∈ (mulTSupport (f i))ᶜ
⊢ (mulSupport fun i ↦ f i z) ⊆ ↑hnf.toFinset

Tactic:
intro i

Goal state after:
case refine_3
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i ↦ mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := {i ∈ hnf.toFinset | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset | x ∉ U j}
z : X
hzn : z ∈ n
hz : ∀ (i : ι), (mulSupport (f i) ∩ n).Nonempty → x ∉ U i → z ∈ (mulTSupport (f i))ᶜ
i : ι
⊢ (i ∈ mulSupport fun i ↦ f i z) → i ∈ ↑hnf.toFinset
Module: Mathlib.Topology.UniformSpace.Equiv

Goal state before:
pp: α : Type u
β : Type u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
h : α ≃ᵤ β
⊢ IsUniformInducing (⇑h.symm ∘ ⇑h)

Tactic:
simp only [symm_comp_self, IsUniformInducing.id]

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

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
f : α → β
hf : IsUniformEmbedding f
⊢ UniformContinuous (f ∘ ⇑(Equiv.ofInjective f ⋯).symm)

Tactic:
Equiv.self_comp_ofInjective_symm

Goal state after:
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
f : α → β
hf : IsUniformEmbedding f
⊢ UniformContinuous Subtype.val