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

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s✝ t✝ : Set X✝
X : ι → Type u_4
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), LocallyCompactSpace (X i)
inst✝ : Finite ι
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
⊢ ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s

Tactic:
refine ⟨(Set.univ : Set ι).pi n'', ?_, subset_trans (fun _ h => ?_) hsub, isCompact_univ_pi hc⟩

Goal state after:
case refine_1
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s✝ t✝ : Set X✝
X : ι → Type u_4
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), LocallyCompactSpace (X i)
inst✝ : Finite ι
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
⊢ univ.pi n'' ∈ 𝓝 t

case refine_2
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s✝ t✝ : Set X✝
X : ι → Type u_4
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), LocallyCompactSpace (X i)
inst✝ : Finite ι
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
x✝ : (i : ι) → X i
h : x✝ ∈ univ.pi n''
⊢ x✝ ∈ s.pi n'
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_1
f : Filter α
⊢ f.smallSets = generate (powerset '' f.sets)

Tactic:
by
  simp_rw [generate_eq_biInf, smallSets, iInf_image, Filter.lift', Filter.lift, Function.comp_apply,
    Filter.mem_sets]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen[inst✝¹] U
hZ : IsClosed[inst✝¹] Z
hUZ : range f = U ∩ Z
x : X
H : U ∈ 𝓝 (f x)
⊢ (𝓝 x).HasBasis (fun s ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U) fun s ↦ f ⁻¹' (s ∩ Z)

Tactic:
hf.nhds_eq_comap,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen[inst✝¹] U
hZ : IsClosed[inst✝¹] Z
hUZ : range f = U ∩ Z
x : X
H : U ∈ 𝓝 (f x)
⊢ (comap f (𝓝 (f x))).HasBasis (fun s ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U) fun s ↦ f ⁻¹' (s ∩ Z)
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
x : X
n : ℕ
hn : x ∈ K n
⊢ ∃ n, K n ∈ 𝓝 x

Tactic:
exact ⟨n + 1, mem_interior_iff_mem_nhds.mp <| K.subset_interior_succ n hn⟩

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

Goal state before:
pp: α β : Type u
s : Set α
f : α → Set β
α✝ β✝ γ✝ : Type u_1
x✝² : Set α✝
x✝¹ : α✝ → Set β✝
x✝ : β✝ → Set γ✝
⊢ x✝² >>= x✝¹ >>= x✝ = x✝² >>= fun x ↦ x✝¹ x >>= x✝

Tactic:
by simp only [bind_def, biUnion_iUnion]

Goal state after:
Module: Mathlib.Order.UpperLower.Principal

Goal state before:
pp: α : Type u_1
ι : Sort u_3
inst✝ : CompleteLattice α
f : ι → α
c : α
⊢ c ∈ Ici (⨆ i, f i) ↔ c ∈ ⨆ i, Ici (f i)

Tactic:
by simp only [mem_Ici_iff, mem_iSup_iff, iSup_le_iff]

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

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
ks : IsCompact s
ι : Type u_3
t : ι → Set X
I : Set ι
htc : ∀ i ∈ I, IsClosed[instTopologicalSpaceSubtype] (s ↓∩ t i)
hst : s ∩ ⋂ i ∈ I, t i = ∅
this : univ ∩ ⋂ i, (fun i ↦ s ↓∩ t ↑i) i = ∅
⊢ ∃ u, s ∩ ⋂ i ∈ u, t ↑i = ∅

Tactic:
simpa [eq_empty_iff_forall_notMem] using
      (isCompact_iff_isCompact_univ.mp ks).elim_finite_subfamily_closed
      (fun i : I ↦ s ↓∩ t i) (fun i ↦ htc i.val i.prop) this

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
s : Set X
f g : X → Y
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : IsOpen[inst✝²] s
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝², inst✝¹] g
hspec : ∀ (x : X), f x ⤳ g x
⊢ Continuous[inst✝², inst✝¹] (s.piecewise f g)

Tactic:
by
  have : ∀ U, IsOpen U → g ⁻¹' U ⊆ f ⁻¹' U := fun U hU x hx ↦ (hspec x).mem_open hU hx
  rw [continuous_def]
  intro U hU
  rw [piecewise_preimage, ite_eq_of_subset_right _ (this U hU)]
  exact hU.preimage hf |>.inter hs |>.union (hU.preimage hg)

Goal state after:
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
inst✝¹ : CompactSpace X
inst✝ : CompactSpace Y
⊢ IsCompact univ

Tactic:
← range_inl_union_range_inr

Goal state after:
X : Type u
Y : Type v
ι : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
s t : Set X
f : X → Y
inst✝¹ : CompactSpace X
inst✝ : CompactSpace Y
⊢ IsCompact (range Sum.inl ∪ range Sum.inr)
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
⊢ IsDiscrete S ↔ ∀ s ⊆ S, ∃ U, IsClosed[inst✝] U ∧ U ∩ S = s

Tactic:
by
  rw [isDiscrete_iff_forall_subset_exists_isOpen]
  constructor <;> intro h s sS
  · obtain ⟨U, Uo, Us⟩ := h (sᶜ ∩ S) inter_subset_right
    exact ⟨Uᶜ, isClosed_compl_iff.mpr Uo, by rw [left_eq_inter.mpr sS]; simp_all [Set.ext_iff]⟩
  · obtain ⟨U, Uo, Us⟩ := h (sᶜ ∩ S) inter_subset_right
    exact ⟨Uᶜ, isOpen_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: case mp
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 ∈ 𝓝 z, (t ∩ (U \ s)).Finite

Tactic:
obtain ⟨t, h₁t, h₂t⟩ := h z h₁z

Goal state after:
case mp
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) = ∅
⊢ ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite
Module: Mathlib.Topology.DiscreteSubset

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

Tactic:
obtain ⟨t, h₁t, h₂t⟩ := h z h₁z

Goal state after:
case mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite
z : X
h₁z : z ∈ U
t : Set X
h₁t : t ∈ 𝓝 z
h₂t : (t ∩ (U \ s)).Finite
⊢ ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: case mp
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
a : α
⊢ Disjoint (𝓝 a) atBot → ¬IsBot a

Tactic:
intro hd

Goal state after:
case mp
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
a : α
hd : Disjoint (𝓝 a) atBot
⊢ ¬IsBot a
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : ClosedIicTopology α
s : Set α
hs : Dense s
htop : ∀ (x : α), IsTop x → x ∈ s
x : α
⊢ ∃ y ∈ s, x ≤ y

Tactic:
by
  by_cases hx : IsTop x
  · exact ⟨x, htop x hx, le_rfl⟩
  · simp only [IsTop, not_forall, not_le] at hx
    rcases hs.exists_mem_open isOpen_Ioi hx with ⟨y, hys, hy : x < y⟩
    exact ⟨y, hys, hy.le⟩

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

Goal state before:
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_of_ne hi, h2K]

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
S : Set (Set α)
K : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) S
H : ∀ s ∈ S, IsPreconnected s
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
Huv : ⋃₀ S ⊆ u ∪ v
a : α
hau : a ∈ u
s : Set α
hsS : s ∈ S
has : a ∈ s
b : α
hbv : b ∈ v
t : Set α
htS : t ∈ S
hbt : b ∈ t
⊢ (⋃₀ S ∩ (u ∩ v)).Nonempty

Tactic:
obtain ⟨r, hrS, hsr, htr⟩ : ∃ r ∈ S, s ⊆ r ∧ t ⊆ r := K s hsS t htS

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
S : Set (Set α)
K : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) S
H : ∀ s ∈ S, IsPreconnected s
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
Huv : ⋃₀ S ⊆ u ∪ v
a : α
hau : a ∈ u
s : Set α
hsS : s ∈ S
has : a ∈ s
b : α
hbv : b ∈ v
t : Set α
htS : t ∈ S
hbt : b ∈ t
r : Set α
hrS : r ∈ S
hsr : s ⊆ r
htr : t ⊆ r
⊢ (⋃₀ S ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
x✝ : α
h : (𝓝 x✝).HasBasis (fun s ↦ IsOpen[inst✝] s ∧ x✝ ∈ s ∧ IsConnected s) id
U : Set α
hU : U ∈ 𝓝 x✝
⊢ ∃ V ⊆ U, IsOpen[inst✝] V ∧ x✝ ∈ V ∧ IsConnected V

Tactic:
rcases h.mem_iff.mp hU with ⟨V, hV, hVU⟩

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
x✝ : α
h : (𝓝 x✝).HasBasis (fun s ↦ IsOpen[inst✝] s ∧ x✝ ∈ s ∧ IsConnected s) id
U : Set α
hU : U ∈ 𝓝 x✝
V : Set α
hV : IsOpen[inst✝] V ∧ x✝ ∈ V ∧ IsConnected V
hVU : id V ⊆ U
⊢ ∃ V ⊆ U, IsOpen[inst✝] V ∧ x✝ ∈ V ∧ IsConnected V
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
⊢ IsConnected s ↔
    ∀ (U : Finset (Set α)),
      (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
        (∀ u ∈ U, IsOpen[inst✝] u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u

Tactic:
rw [IsConnected, isPreconnected_iff_subset_of_disjoint]

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
⊢ (s.Nonempty ∧ ∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v) ↔
    ∀ (U : Finset (Set α)),
      (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
        (∀ u ∈ U, IsOpen[inst✝] u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst✝] (U i)
hsU : s ⊆ ⋃ i, U i
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → (∃ r, r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
hcountable_union :
  ∀ (S : Set (Set X)),
    S.Countable → (∀ s ∈ S, ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i
x : X
hx : x ∈ s
⊢ ∃ t ∈ 𝓝[s] x, ∃ r, r.Countable ∧ t ⊆ ⋃ i ∈ r, U i

Tactic:
let ⟨i, hi⟩ := mem_iUnion.1 (hsU hx)

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst✝] (U i)
hsU : s ⊆ ⋃ i, U i
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → (∃ r, r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
hcountable_union :
  ∀ (S : Set (Set X)),
    S.Countable → (∀ s ∈ S, ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i
x : X
hx : x ∈ s
i : ι
hi : x ∈ U i
⊢ ∃ t ∈ 𝓝[s] x, ∃ r, r.Countable ∧ t ⊆ ⋃ i ∈ r, U i
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
ι : Type v
inst✝ : Nonempty ι
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst✝¹] (U i)
hsU : s ⊆ ⋃ i, U i
c : Set ι
c_count : c.Countable
c_cov : s ⊆ ⋃ i ∈ c, U i
⊢ ∃ f, s ⊆ ⋃ n, U (f n)

Tactic:
rcases c.eq_empty_or_nonempty with rfl | c_nonempty

Goal state after:
case inl
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
ι : Type v
inst✝ : Nonempty ι
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst✝¹] (U i)
hsU : s ⊆ ⋃ i, U i
c_count : ∅.Countable
c_cov : s ⊆ ⋃ i ∈ ∅, U i
⊢ ∃ f, s ⊆ ⋃ n, U (f n)

case inr
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
ι : Type v
inst✝ : Nonempty ι
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst✝¹] (U i)
hsU : s ⊆ ⋃ i, U i
c : Set ι
c_count : c.Countable
c_cov : s ⊆ ⋃ i ∈ c, U i
c_nonempty : c.Nonempty
⊢ ∃ f, s ⊆ ⋃ n, U (f n)
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
this✝ : IsPreconnected (Subtype.val ⁻¹' s)
h2xs : ⟨x, ⋯⟩ ∈ Subtype.val ⁻¹' s
this : Subtype.val ⁻¹' s ⊆ connectedComponent ⟨x, ⋯⟩
⊢ s ⊆ connectedComponentIn F x

Tactic:
connectedComponentIn_eq_image (hsF hxs)

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
this✝ : IsPreconnected (Subtype.val ⁻¹' s)
h2xs : ⟨x, ⋯⟩ ∈ Subtype.val ⁻¹' s
this : Subtype.val ⁻¹' s ⊆ connectedComponent ⟨x, ⋯⟩
⊢ s ⊆ Subtype.val '' connectedComponent ⟨x, ⋯⟩
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : LindelofSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ IsLindelof univ

Tactic:
rw [hf.isInducing.isLindelof_iff, image_univ]; exact hf.isClosed_range.isLindelof

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 univ

Tactic:
← range_inl_union_range_inr

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : CompletelyNormalSpace X
inst✝ : R0Space X
⊢ ∀ (x : SeparationQuotient X), IsClosed {x}

Tactic:
((t1Space_TFAE (SeparationQuotient X)).out 1 0 :),

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : CompletelyNormalSpace X
inst✝ : R0Space X
⊢ T1Space (SeparationQuotient X)
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: case refine_1.inr
X : Type u_1
inst✝ : TopologicalSpace X
T : Set (Set X)
hT✝ : ∀ t ∈ T, IsOpen[inst✝] t
T_count : T.Countable
hT : T.Nonempty
⊢ ∃ f, (∀ (n : ℕ), IsOpen[inst✝] (f n)) ∧ ⋂₀ T = ⋂ n, f n

Tactic:
obtain ⟨f, hf⟩ : ∃ (f : ℕ → Set X), T = range f := Countable.exists_eq_range T_count hT

Goal state after:
case refine_1.inr
X : Type u_1
inst✝ : TopologicalSpace X
T : Set (Set X)
hT✝ : ∀ t ∈ T, IsOpen[inst✝] t
T_count : T.Countable
hT : T.Nonempty
f : ℕ → Set X
hf : T = range f
⊢ ∃ f, (∀ (n : ℕ), IsOpen[inst✝] (f n)) ∧ ⋂₀ T = ⋂ n, f 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 : ∀ x ∈ s, closure[inst✝¹] s ∉ 𝓝 x
⊢ ∀ ⦃x : X⦄, x ∈ s → closure[inst✝] (f '' s) ∉ 𝓝 (f x)

Tactic:
hf.nhds_eq_comap,

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 : ∀ x ∈ s, closure[inst✝¹] s ∉ comap f (𝓝 (f x))
⊢ ∀ ⦃x : X⦄, x ∈ s → closure[inst✝] (f '' s) ∉ 𝓝 (f x)
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝² : TopologicalSpace α
s t u v : Set α
inst✝¹ : TopologicalSpace β
inst✝ : TotallyDisconnectedSpace β
f : α → β
x : α
⊢ connectedComponent (mk x) = {mk x}

Tactic:
rw [← ConnectedComponents.isQuotientMap_coe.image_connectedComponent, ←
    connectedComponents_preimage_singleton, image_preimage_eq _ ConnectedComponents.surjective_coe]

Goal state after:
case h_fibers
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝² : TopologicalSpace α
s t u v : Set α
inst✝¹ : TopologicalSpace β
inst✝ : TotallyDisconnectedSpace β
f : α → β
x : α
⊢ ∀ (y : ConnectedComponents α), IsConnected (mk ⁻¹' {y})
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
I : Set ι
c : I.Countable
f : ι → Set X
h : ∀ i ∈ I, IsMeagre (f i)
⊢ IsMeagre (⋃ i ∈ I, f i)

Tactic:
suffices IsMeagre (⋃ i : I, f i) by simpa
  have : Countable I := c
  apply isMeagre_iUnion
  intro ⟨i, hi⟩
  exact h i hi

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

Goal state before:
pp: case mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s t : Set X
ts : t ⊆ s
ho : IsGδ t
hd : Dense t
⊢ s ∈ residual X

Tactic:
exact mem_of_superset (residual_of_dense_Gδ ho hd) ts

Goal state after:
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
⊢ ¬(Disjoint on U) i j

Tactic:
rw [Set.not_disjoint_iff]

Goal state after:
α : 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
⊢ ∃ x ∈ U i, x ∈ U j
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case inr.succ.succ
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : Infinite (ConnectedComponents α)
h✝ : Nonempty α
n : ℕ
U : Fin (n + 1) → Set α
h₁ : ∀ (i : Fin (n + 1)), IsClopen (U i)
h₂ : ∀ (i : Fin (n + 1)), (U i).Nonempty
h₃ : Pairwise (Disjoint on U)
h₄ : ⋃ i, U i = univ
i : Fin (n + 1)
hi : ¬IsConnected (U i)
⊢ ∃ U,
    (∀ (i : Fin (n + 1 + 1)), IsClopen (U i)) ∧
      (∀ (i : Fin (n + 1 + 1)), (U i).Nonempty) ∧ Pairwise (Disjoint on U) ∧ ⋃ i, U i = univ

Tactic:
obtain ⟨U, rfl⟩ := (Equiv.piCongrLeft (fun _ ↦ Set α) (Equiv.swap 0 i)).symm.surjective U

Goal state after:
case inr.succ.succ
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : Infinite (ConnectedComponents α)
h✝ : Nonempty α
n : ℕ
i : Fin (n + 1)
U : Fin (n + 1) → Set α
h₁ : ∀ (i_1 : Fin (n + 1)), IsClopen ((Equiv.piCongrLeft (fun x ↦ Set α) (Equiv.swap 0 i)).symm U i_1)
h₂ : ∀ (i_1 : Fin (n + 1)), ((Equiv.piCongrLeft (fun x ↦ Set α) (Equiv.swap 0 i)).symm U i_1).Nonempty
h₃ : Pairwise (Disjoint on (Equiv.piCongrLeft (fun x ↦ Set α) (Equiv.swap 0 i)).symm U)
h₄ : ⋃ i_1, (Equiv.piCongrLeft (fun x ↦ Set α) (Equiv.swap 0 i)).symm U i_1 = univ
hi : ¬IsConnected ((Equiv.piCongrLeft (fun x ↦ Set α) (Equiv.swap 0 i)).symm U i)
⊢ ∃ U,
    (∀ (i : Fin (n + 1 + 1)), IsClopen (U i)) ∧
      (∀ (i : Fin (n + 1 + 1)), (U i).Nonempty) ∧ Pairwise (Disjoint on U) ∧ ⋃ i, U i = univ
Module: Mathlib.Topology.UniformSpace.DiscreteUniformity

Goal state before:
pp: X : Type u_2
inst✝ : UniformSpace X
⊢ DiscreteUniformity X ↔ SetRel.id ∈ uniformity X

Tactic:
by
  rw [← uniformSpace_eq_bot, discreteUniformity_iff_eq_bot]

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : SetRel α α → Filter β
h : Monotone f
⊢ ((𝓤 α).lift fun s ↦ f (s ○ s)) = ((𝓤 α).lift' fun s ↦ s ○ s).lift f

Tactic:
lift_lift'_assoc

Goal state after:
α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : SetRel α α → Filter β
h : Monotone f
⊢ ((𝓤 α).lift fun s ↦ f (s ○ s)) = (𝓤 α).lift fun s ↦ f (s ○ s)

case hg
α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : SetRel α α → Filter β
h : Monotone f
⊢ Monotone fun s ↦ s ○ s

case hh
α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : SetRel α α → Filter β
h : Monotone f
⊢ Monotone f
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
ι : Sort u_2
u : ι → UniformSpace α
a : α
⊢ 𝓝 a = 𝓝 a

Tactic:
simp only [@nhds_eq_comap_uniformity _ (iInf u), nhds_iInf,
    iInf_uniformity, @nhds_eq_comap_uniformity _ (u _), Filter.comap_iInf]

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

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : (𝓤 β).IsCountablyGenerated
⊢ (𝓤 (α ⊕ β)).IsCountablyGenerated

Tactic:
Sum.uniformity

Goal state after:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : (𝓤 β).IsCountablyGenerated
⊢ (map (Prod.map inl inl) (𝓤 α) ⊔ map (Prod.map inr inr) (𝓤 β)).IsCountablyGenerated
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : UniformSpace γ
f : α → β
inst✝¹ : CompleteSpace α
inst✝ : CompleteSpace β
⊢ IsComplete univ

Tactic:
← range_inl_union_range_inr

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : UniformSpace γ
f : α → β
inst✝¹ : CompleteSpace α
inst✝ : CompleteSpace β
⊢ IsComplete (range Sum.inl ∪ range Sum.inr)
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : TopologicalSpace α
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
f : α → β
f₂ : α → γ
m : β → γ → δ
hf : HasCompactMulSupport f
hf₂ : HasCompactMulSupport f₂
hm : m 1 1 = 1
⊢ HasCompactMulSupport fun x ↦ m (f x) (f₂ x)

Tactic:
hasCompactMulSupport_iff_eventuallyEq

Goal state after:
α : Type u_2
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : TopologicalSpace α
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
f : α → β
f₂ : α → γ
m : β → γ → δ
hf : f =ᶠ[coclosedCompact α] 1
hf₂ : f₂ =ᶠ[coclosedCompact α] 1
hm : m 1 1 = 1
⊢ (fun x ↦ m (f x) (f₂ x)) =ᶠ[coclosedCompact α] 1