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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (∀ x ∈ s, x ∈ {x | 𝓝 x ≤ 𝓟 s}) ↔ ∀ x ∈ s, 𝓝 x ≤ 𝓟 s

Tactic:
mem_ofPred

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed (frontier s)

Tactic:
frontier_eq_closure_inter_closure

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed (closure s ∩ closure sᶜ)
Module: Mathlib.Topology.Maps.OpenQuotient

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
ind : IsInducing f
surj : Surjective f
U : Set X
U_open : IsOpen[inst✝¹] U
⊢ IsOpen[inst✝] (f '' U)

Tactic:
obtain ⟨V, hV, rfl⟩ := ind.isOpen_iff.mp U_open
    rwa [V.image_preimage_eq surj]

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

Goal state before:
pp: Y : Type u_2
Z : Type u_3
ι : Type u_4
g : Y → Z
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : ι → Y
l : Filter ι
y : Y
hg : IsInducing g
⊢ Tendsto f l (𝓝 y) ↔ Tendsto (g ∘ f) l (𝓝 (g y))

Tactic:
by
  rw [hg.nhds_eq_comap, tendsto_comap_iff]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
s : Set X
x : X
⊢ f '' s ∈ 𝓝 (f x) ↔ s ∈ 𝓝 x

Tactic:
by
  rw [← hf.map_nhds_eq, mem_map, preimage_image_eq _ hf.injective]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
s : Set (X × Y)
⊢ s ∈ 𝓝 (x, y) ↔ ∃ u ∈ 𝓝 x, ∃ v ∈ 𝓝 y, u ×ˢ v ⊆ s

Tactic:
by rw [nhds_prod_eq, mem_prod_iff]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
X : α → β
s : Set β
t : Set α
a : α
h : a ∈ t
ht : IsOpen[inst✝] t
hs : s ∈ 𝓝 (X a)
⊢ X ⁻¹' s ∈ 𝓝 a

Tactic:
← ht.nhdsWithin_eq h

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
X : α → β
s : Set β
t : Set α
a : α
h : a ∈ t
ht : IsOpen[inst✝] t
hs : s ∈ 𝓝 (X a)
⊢ X ⁻¹' s ∈ 𝓝[t] a
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
u : Set α
ou : IsOpen[inst✝¹] u
useq : s ∩ u = s ∩ f ⁻¹' t
⊢ ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
exact ⟨u, ou, by simpa only [Set.inter_comm, eq_comm] using useq⟩

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
u : Set α
ou : IsOpen[inst✝¹] u
useq : f ⁻¹' t ∩ s = u ∩ s
⊢ ∃ t_1, IsOpen[inst✝¹] t_1 ∧ s ∩ t_1 = s ∩ f ⁻¹' t

Tactic:
exact ⟨u, ou, by simpa only [Set.inter_comm, eq_comm] using useq⟩

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X✝ : Type u
Y : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
X : Type u_5
⊢ ∀ (s : Set (Set X)), (∀ t ∈ s, t.Nonempty → tᶜ.Finite) → (⋃₀ s).Nonempty → (⋃₀ s)ᶜ.Finite

Tactic:
rintro s h ⟨x, t, hts, hzt⟩

Goal state after:
X✝ : Type u
Y : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
X : Type u_5
s : Set (Set X)
h : ∀ t ∈ s, t.Nonempty → tᶜ.Finite
x : X
t : Set X
hts : t ∈ s
hzt : x ∈ t
⊢ (⋃₀ s)ᶜ.Finite
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
s : Set α
a : α
h : a ∈ s
f : α → β
l : Filter β
⊢ Tendsto f (𝓝[s] a) l ↔ Tendsto (s.domRestrict f) (𝓝 ⟨a, h⟩) l

Tactic:
nhdsWithin_eq_map_subtype_coe h,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
s : Set α
a : α
h : a ∈ s
f : α → β
l : Filter β
⊢ Tendsto f (map Subtype.val (𝓝 ⟨a, h⟩)) l ↔ Tendsto (s.domRestrict f) (𝓝 ⟨a, h⟩) l
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: case refine_1
α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s u : Set α
this : TopologicalSpace α := TopologicalSpace.induced f t
x✝ : ∃ U, (∃ t_1, IsOpen[t] t_1 ∧ f ⁻¹' t_1 = U) ∧ s ⊆ U ∧ U ⊆ u
v : Set α
v' : Set β
hv' : IsOpen[t] v' ∧ f ⁻¹' v' = v
hv : s ⊆ v ∧ v ⊆ u
⊢ f '' s ⊆ v'

Tactic:
exact (image_mono hv.1).trans (by simp [hv'])

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_nhds : ∀ (a : α), (𝓝 a).HasBasis (fun t ↦ t ∈ s ∧ a ∈ t) id
t₁ : Set α
ht₁ : t₁ ∈ s
t₂ : Set α
ht₂ : t₂ ∈ s
x : α
hx : x ∈ t₁ ∩ t₂
⊢ ∃ t₃ ∈ s, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

Tactic:
by
    simpa only [and_assoc, (h_nhds x).mem_iff]
      using! (inter_mem ((h_nhds _).mem_of_mem ⟨ht₁, hx.1⟩) ((h_nhds _).mem_of_mem ⟨ht₂, hx.2⟩))

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ s ∩ closure[inst✝] (s ∩ t) ⊆ s ∧ s ∩ closure[inst✝] (s ∩ t) ⊆ t ↔ s ∩ closure[inst✝] (s ∩ t) ⊆ t

pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ s ∩ t ⊆ s ∩ closure[inst✝] (s ∩ t)

Tactic:
and_iff_right

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ s ∩ closure[inst✝] (s ∩ t) ⊆ t ↔ s ∩ closure[inst✝] (s ∩ t) ⊆ t

X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ s ∩ closure[inst✝] (s ∩ t) ⊆ s

X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ s ∩ t ⊆ s ∩ closure[inst✝] (s ∩ t)
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ s ∈ 𝓝 a ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s

Tactic:
by
  change s ∈ (𝓝 a).sets ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s
  rw [hb.eq_generateFrom, nhds_generateFrom, biInf_sets_eq]
  · simp [and_assoc, and_left_comm]
  · rintro s ⟨hs₁, hs₂⟩ t ⟨ht₁, ht₂⟩
    let ⟨u, hu₁, hu₂, hu₃⟩ := hb.1 _ hs₂ _ ht₂ _ ⟨hs₁, ht₁⟩
    exact ⟨u, ⟨hu₂, hu₁⟩, le_principal_iff.2 (hu₃.trans inter_subset_left),
      le_principal_iff.2 (hu₃.trans inter_subset_right)⟩
  · rcases eq_univ_iff_forall.1 hb.sUnion_eq a with ⟨i, h1, h2⟩
    exact ⟨i, h2, h1⟩

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
h : IsInducing (Sum.elim f g)
C : Set Z
C_closed : IsClosed[inst✝] C
hC : Sum.elim f g ⁻¹' C = range inl
⊢ Disjoint (closure[inst✝] (range f)) (range g)

Tactic:
have A : closure (range f) ⊆ C := by
    rw [C_closed.closure_subset_iff, ← elim_comp_inl f g, range_comp, image_subset_iff, hC]

Goal state after:
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
h : IsInducing (Sum.elim f g)
C : Set Z
C_closed : IsClosed[inst✝] C
hC : Sum.elim f g ⁻¹' C = range inl
A : closure[inst✝] (range f) ⊆ C
⊢ Disjoint (closure[inst✝] (range f)) (range g)
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝¹ : SeparableSpace α
inst✝ : Nonempty α
s : Set α
hs : s.Countable
s_dense : Dense s
u : ℕ → α
hu : s ⊆ range u
⊢ ∃ u, DenseRange u

Tactic:
exact ⟨u, s_dense.mono hu⟩

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

Goal state before:
pp: α : Type u_2
β : Type u_3
x✝ : Bornology α
inst✝ : Bornology β
f : α → β
⊢ comap f (cobounded β) ≤ cobounded α ↔ ∀ ⦃s : Set α⦄, IsBounded s → IsBounded (f '' s)

Tactic:
refine
    ⟨fun h s hs => ?_, fun h t ht =>
      ⟨(f '' tᶜ)ᶜ, h <| IsCobounded.compl ht, compl_subset_comm.1 <| subset_preimage_image _ _⟩⟩
  obtain ⟨t, ht, hts⟩ := h hs.compl
  rw [subset_compl_comm, ← preimage_compl] at hts
  exact (IsCobounded.compl ht).subset ((image_mono hts).trans <| image_preimage_subset _ _)

Goal state after:
Module: Mathlib.Order.ZornAtoms

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x1 x2 ↦ x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c
⊢ IsCoatomic α

Tactic:
by
  refine ⟨fun x => le_top.eq_or_lt.imp_right fun hx => ?_⟩
  have := zorn_le_nonempty₀ (Ico x ⊤) (fun c hxc hc y hy => ?_) x (left_mem_Ico.2 hx)
  · obtain ⟨y, hxy, hmax⟩ := this
    refine ⟨y, ⟨hmax.prop.2.ne, fun z hyz ↦ le_top.eq_or_lt.resolve_right fun hz => ?_⟩, hxy⟩
    exact hyz.ne <| hmax.eq_of_le ⟨hxy.trans hyz.le, hz⟩ hyz.le
  rcases h c hc ⟨y, hy⟩ fun h => (hxc h).2.ne rfl with ⟨z, hz, hcz⟩
  exact ⟨z, ⟨le_trans (hxc hy).1 (hcz hy), hz.lt_top⟩, hcz⟩

Goal state after:
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
g : Filter α
p : Filter α → Prop
hp : Monotone p
H : ∀ (f : Ultrafilter α), ↑f ≤ g → p ↑f
⊢ ∀ (f : Filter α), f.NeBot → f ≤ g → p f

Tactic:
f

Goal state after:
α : Type u
g : Filter α
p : Filter α → Prop
hp : Monotone p
H : ∀ (f : Ultrafilter α), ↑f ≤ g → p ↑f
f : Filter α
⊢ f.NeBot → f ≤ g → p f
Module: Mathlib.Order.Filter.Ultrafilter.Basic

Goal state before:
pp: α : Type u
f : Ultrafilter α
s : Set α
h : s.Finite
h' : s ∈ f
⊢ ∃ x ∈ s, f = pure x

Tactic:
by
  rw [← biUnion_of_singleton s] at h'
  rcases (Ultrafilter.finite_biUnion_mem_iff h).mp h' with ⟨a, has, haf⟩
  exact ⟨a, has, eq_of_le (Filter.le_pure_iff.2 haf)⟩

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case right.a
α : Type u
t : TopologicalSpace α
inst✝¹ : Countable α
inst✝ : FirstCountableTopology α
b : α → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun i ↦ b x i
⊢ t ≤ generateFrom (range (uncurry b))

Tactic:
rw [le_generateFrom_iff_subset_isOpen]
      rintro _ ⟨⟨x, n⟩, rfl⟩
      exact (hxb x n).right

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

Goal state before:
pp: case refine_3
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✝ : ∀ (i : ι), CompactSpace (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
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)
i : ι
⊢ IsCompact (if i ∈ s then n'' i else univ)

Tactic:
by_cases h : i ∈ s

Goal state after:
case pos
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✝ : ∀ (i : ι), CompactSpace (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
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)
i : ι
h : i ∈ s
⊢ IsCompact (if i ∈ s then n'' i else univ)

case neg
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✝ : ∀ (i : ι), CompactSpace (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
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)
i : ι
h : i ∉ s
⊢ IsCompact (if i ∈ s then n'' i else univ)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case inl
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hfc : Continuous[inst✝¹, inst✝] f
l : Filter Y
hne : l.NeBot
s t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
y : Y
hyt : y ∈ t
hf : Tendsto f (cocompact X) (𝓝 y)
hle : l ≤ 𝓟 (insert y (range f))
hsy : s ∈ 𝓝 y
⊢ y ∈ f '' K

pp: case inr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous[inst✝¹, inst✝] f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y (range f))
s : Set Y
hsy : s ∈ 𝓝 y
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
x : X
hyt : f x ∈ t
⊢ f x ∈ f '' K

Tactic:
exacts [(hd.le_bot ⟨mem_of_mem_nhds hsy, hyt⟩).elim,
      mem_image_of_mem _ (not_not.1 fun hxK => hd.le_bot ⟨hKs hxK, hyt⟩)]

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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
h : ∀ (i : ι) (f : Ultrafilter (X i)), s i ∈ ↑f → ∃ x ∈ s i, ↑f ≤ 𝓝 x
⊢ ∀ (f : Ultrafilter ((i : ι) → X i)),
    {x | ∀ (i : ι), x i ∈ s i} ∈ ↑f → ∃ x ∈ {x | ∀ (i : ι), x i ∈ s i}, ∀ (i : ι), Tendsto (eval i) (↑f) (𝓝 (x i))

Tactic:
f

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
h : ∀ (i : ι) (f : Ultrafilter (X i)), s i ∈ ↑f → ∃ x ∈ s i, ↑f ≤ 𝓝 x
f : Ultrafilter ((i : ι) → X i)
⊢ {x | ∀ (i : ι), x i ∈ s i} ∈ ↑f → ∃ x ∈ {x | ∀ (i : ι), x i ∈ s i}, ∀ (i : ι), Tendsto (eval i) (↑f) (𝓝 (x i))
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
t : Finset (Set X)
⊢ (∀ u ∈ t, IsOpen[inst✝] u) → (∀ u ∈ t, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑t).Nonempty ↔
    (∀ x ∈ t, IsClosed[inst✝] ((Function.Involutive.toPerm compl ⋯) x)) →
      s ⊆ ⋃ a ∈ ↑t, (Function.Involutive.toPerm compl ⋯) a →
        ∃ z, (∃ a ∈ t, (Function.Involutive.toPerm compl ⋯) a = z) ∧ s ⊆ z

Tactic:
Function.Involutive.coe_toPerm,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
t : Finset (Set X)
⊢ (∀ u ∈ t, IsOpen[inst✝] u) → (∀ u ∈ t, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑t).Nonempty ↔
    (∀ x ∈ t, IsClosed[inst✝] xᶜ) → s ⊆ ⋃ a ∈ ↑t, aᶜ → ∃ z, (∃ a ∈ t, aᶜ = z) ∧ s ⊆ z
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
U s : Set X
h : sᶜ ∈ codiscreteWithin U
⊢ IsDiscrete (sᶜ ∪ Uᶜ)ᶜ

Tactic:
isDiscrete_iff_nhdsNE

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
U s : Set X
h : sᶜ ∈ codiscreteWithin U
⊢ ∀ x ∈ (sᶜ ∪ Uᶜ)ᶜ, 𝓝[≠] x ⊓ 𝓟 (sᶜ ∪ Uᶜ)ᶜ = ⊥
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : Set X
cond : ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ ↑F
x : X
hx : x ∈ U
⊢ ∀ (l : Ultrafilter X), ↑l ≤ 𝓝 x → U ∈ l

Tactic:
f

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : Set X
cond : ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ ↑F
x : X
hx : x ∈ U
f : Ultrafilter X
⊢ ↑f ≤ 𝓝 x → U ∈ f
Module: Mathlib.Order.SuccPred.Relation

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

Tactic:
ih

Goal state after:
case refine_2
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m✝ : α
hnm✝ : n ≤ m✝
m : α
hnm : n ≤ m
ih : (∀ i ∈ Ico n m, r i (succ i)) → ReflTransGen r n m
⊢ (∀ i ∈ Ico n (succ m), r i (succ i)) → ReflTransGen r n (succ m)
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 m n, r (succ i) i
hmn : m ≤ n
⊢ ReflTransGen r n m

Tactic:
rw [← reflTransGen_swap]
  exact reflTransGen_of_succ_of_le (swap r) h hmn

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_mem_codiscrete_iff

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K : Set X
hK : IsCompact K
x✝ : X
⊢ x✝ ∈ closure[inst✝¹] K ↔ x✝ ∈ ⋃ x ∈ K, {y | Inseparable x y}

Tactic:
simp [hK.mem_closure_iff_exists_inseparable]

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
x✝ : TopologicalSpace X := sInf T
x y : X
⊢ x ⤳ y ∨ Disjoint (𝓝 x) (𝓝 y)

Tactic:
simp only [Specializes, nhds_sInf]

Goal state after:
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x✝ : TopologicalSpace X := sInf T
x y : X
⊢ ⨅ t ∈ T, 𝓝 x ≤ ⨅ t ∈ T, 𝓝 y ∨ Disjoint (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_3
t₁ t₂ : TopologicalSpace X
h₁ : R1Space X
h₂ : R1Space X
⊢ R1Space X

Tactic:
rw [inf_eq_iInf]

Goal state after:
X : Type u_3
t₁ t₂ : TopologicalSpace X
h₁ : R1Space X
h₂ : R1Space X
⊢ R1Space X
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous[inst✝, inst✝³] f
hg : Continuous[inst✝, inst✝³] g
⊢ Continuous[inst✝, inst✝³] fun b ↦ max (f b) (g b)

Tactic:
simp only [max_def]
  exact hg.if_ge hf hg hf fun x => id

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsLindelof s
p : Set X → Prop
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s
hcountable_union : ∀ (S : Set (Set X)), S.Countable → (∀ s ∈ S, p s) → p (⋃₀ S)
hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t
f : Filter X := ofCountableUnion {t | p t} hcountable_union ⋯
⊢ ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f

Tactic:
by simpa [f] using! hnhds

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
hsf : s ⊆ range f
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
⊢ (f ⁻¹' s ∩ (u ∩ v)).Nonempty

Tactic:
replace hsf : f '' f ⁻¹' s = s := image_preimage_eq_of_subset hsf
    obtain ⟨_, has, ⟨a, hau, rfl⟩, hav⟩ : (s ∩ (f '' u ∩ f '' v)).Nonempty := by
      refine isPreconnected_closed_iff.1 hs (f '' u) (f '' v) (hf u hu) (hf v hv) ?_ ?_ ?_
      · simpa only [hsf, image_union] using image_mono (f := f) hsuv
      · simpa only [image_preimage_inter] using hsu.image f
      · simpa only [image_preimage_inter] using hsv.image f
    · exact ⟨a, has, hau, hinj.mem_set_image.1 hav⟩

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hs : IsPreconnected s
hsv : (s ∩ v).Nonempty
⊢ False

Tactic:
obtain ⟨x, _, hx⟩ := hs u v hu hv hsuv hsu hsv

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hs : IsPreconnected s
hsv : (s ∩ v).Nonempty
x : α
left✝ : x ∈ s
hx : x ∈ u ∩ v
⊢ False
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_3
t₁ t₂ : TopologicalSpace X
h₁ : RegularSpace X
h₂ : RegularSpace X
⊢ RegularSpace X

Tactic:
rw [inf_eq_iInf]

Goal state after:
X : Type u_3
t₁ t₂ : TopologicalSpace X
h₁ : RegularSpace X
h₂ : RegularSpace X
⊢ RegularSpace X
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: case inl
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hfc : Continuous[inst✝², inst✝¹] f
l : Filter Y
hne : l.NeBot
inst✝ : CountableInterFilter l
s t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsLindelof K
hKs : Kᶜ ⊆ f ⁻¹' s
y : Y
hyt : y ∈ t
hf : Tendsto f (coLindelof X) (𝓝 y)
hle : l ≤ 𝓟 (insert y (range f))
hsy : s ∈ 𝓝 y
⊢ y ∈ f '' K

pp: case inr
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (coLindelof X) (𝓝 y)
hfc : Continuous[inst✝², inst✝¹] f
l : Filter Y
hne : l.NeBot
inst✝ : CountableInterFilter l
hle : l ≤ 𝓟 (insert y (range f))
s : Set Y
hsy : s ∈ 𝓝 y
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsLindelof K
hKs : Kᶜ ⊆ f ⁻¹' s
x : X
hyt : f x ∈ t
⊢ f x ∈ f '' K

Tactic:
exacts [(hd.le_bot ⟨mem_of_mem_nhds hsy, hyt⟩).elim,
      mem_image_of_mem _ (not_not.1 fun hxK => hd.le_bot ⟨hKs hxK, hyt⟩)]

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ x,
      ((∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed[inst✝] x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable) ∧
        ⋂ a ∈ x, aᶜ ⊆ sᶜ) ↔
    ∃ S, ((∀ t ∈ S, IsNowhereDense t) ∧ S.Countable) ∧ s ⊆ ⋃₀ S

Tactic:
← compl_iUnion₂,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ x,
      ((∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed[inst✝] x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable) ∧
        (⋃ i ∈ x, i)ᶜ ⊆ sᶜ) ↔
    ∃ S, ((∀ t ∈ S, IsNowhereDense t) ∧ S.Countable) ∧ s ⊆ ⋃₀ S
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
s : Set X
H : IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v
H1 : IsClopen (s ∩ u)
⊢ ⋂ s, ↑s ⊆ a ∨ ⋂ s, ↑s ⊆ b

Tactic:
rw [union_comm] at H

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
s : Set X
H : IsClopen s ∧ x ∈ s ∧ s ⊆ v ∪ u
H1 : IsClopen (s ∩ u)
⊢ ⋂ s, ↑s ⊆ a ∨ ⋂ s, ↑s ⊆ b
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed[inst✝²] (f i)
hU : s ⊆ ⋃ i, f i
g : ι → Set X := fun i ↦ (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen[inst✝²] (g i)
hgd : Dense (⋂ i, g i)
x : X
hxs : x ∈ s
hxg : x ∈ ⋂ i, g i
⊢ x ∈ ⋃ i, interior (f i)

Tactic:
mem_iInter

Goal state after:
X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed[inst✝²] (f i)
hU : s ⊆ ⋃ i, f i
g : ι → Set X := fun i ↦ (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen[inst✝²] (g i)
hgd : Dense (⋂ i, g i)
x : X
hxs : x ∈ s
hxg : ∀ (i : ι), x ∈ g i
⊢ x ∈ ⋃ i, interior (f i)
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
m n : ℕ
⊢ Fin.appendEquiv m n = (sumArrowHomeomorphProdArrow.symm.trans (piCongrLeft finSumFinEquiv)).toEquiv

Tactic:
by
  apply Equiv.symm_bijective.injective
  ext x i <;> simp

Goal state after: