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

Goal state before:
pp: α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝² : TopologicalSpace β
inst✝¹ : FirstCountableTopology α
inst✝ : FirstCountableTopology β
x✝ : α × β
x : α
y : β
⊢ (𝓝 (x, y)).IsCountablyGenerated

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
ι : Type u_1
X : ι → Type u_2
inst✝² : Countable ι
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), FirstCountableTopology (X i)
f : (i : ι) → X i
⊢ (𝓝 f).IsCountablyGenerated

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
ι : Type u_5
σ : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : TopologicalSpace X
f : Sigma σ → X
⊢ Continuous[instTopologicalSpaceSigma, inst✝] f ↔ ∀ (i : ι), Continuous[inst✝¹ i, inst✝] fun a ↦ f ⟨i, a⟩

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
⊢ ∃ b, b.Countable ∧ ∅ ∉ b ∧ IsTopologicalBasis b

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : t.Countable ∧ ∅ ∉ t ∧ IsTopologicalBasis t
hn : t = ∅
⊢ IsTopologicalBasis (range fun n ↦ ∅)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
⊢ ∃ b, IsTopologicalBasis (range b)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝¹ : Countable α
inst✝ : FirstCountableTopology α
⊢ ∃ b, b.Countable ∧ t = generateFrom b

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace β
inst✝ : SecondCountableTopology β
f : α → β
⊢ SecondCountableTopology α

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u_1
ι : Sort u_2
inst✝ : Countable ι
t : ι → TopologicalSpace α
ht : ∀ (i : ι), SecondCountableTopology α
⊢ SecondCountableTopology α

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
⊢ SeparableSpace α

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
ι : Type u_5
σ : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : TopologicalSpace X
f : Sigma σ → X
⊢ IsInducing f ↔
    (∀ (i : ι), IsInducing (f ∘ Sigma.mk i)) ∧ ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
ι : Type u_1
s : ι → Set α
H : ∀ (i : ι), IsOpen[t] (s i)
⊢ ∃ T, T.Countable ∧ ⋃ i ∈ T, s i = ⋃ i, s i

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : (k : κ) → TopologicalSpace (τ k)
f₁ : ι → κ
f₂ : (i : ι) → σ i → τ (f₁ i)
⊢ (∀ (i : ι), Continuous[inst✝¹ i, instTopologicalSpaceSigma] fun a ↦ Sigma.map f₁ f₂ ⟨i, a⟩) ↔
    ∀ (i : ι), Continuous[inst✝¹ i, inst✝ (f₁ i)] (f₂ i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
ι : Type u_5
σ : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : TopologicalSpace X
f : Sigma σ → X
⊢ IsOpenMap f ↔ ∀ (i : ι), IsOpenMap fun a ↦ f ⟨i, a⟩

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : (k : κ) → TopologicalSpace (τ k)
f₁ : ι → κ
f₂ : (i : ι) → σ i → τ (f₁ i)
h₁ : Injective f₁
⊢ IsInducing (Sigma.map f₁ f₂) ↔ ∀ (i : ι), IsInducing (f₂ i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : (k : κ) → TopologicalSpace (τ k)
f₁ : ι → κ
f₂ : (i : ι) → σ i → τ (f₁ i)
h : Injective f₁
⊢ IsEmbedding (Sigma.map f₁ f₂) ↔ ∀ (i : ι), IsEmbedding (f₂ i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : (k : κ) → TopologicalSpace (τ k)
f₁ : ι → κ
f₂ : (i : ι) → σ i → τ (f₁ i)
h : Injective f₁
⊢ IsOpenEmbedding (Sigma.map f₁ f₂) ↔ ∀ (i : ι), IsOpenEmbedding (f₂ i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
ι : Type u_1
I : Set ι
s : ι → Set α
H : ∀ i ∈ I, IsOpen[t] (s i)
⊢ ∃ T ⊆ I, T.Countable ∧ ⋃ i ∈ T, s i = ⋃ i ∈ I, s i

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
S : Set (Set α)
H : ∀ s ∈ S, IsOpen[t] s
⊢ ∃ T, T.Countable ∧ T ⊆ S ∧ ⋃₀ T = ⋃₀ S

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set (ULift.{v, u} X)
⊢ IsOpen[topologicalSpace] s ↔ IsOpen[inst✝] (up ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
⊢ ∃ s, s.Countable ∧ ⋃ x ∈ s, f x = univ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set (ULift.{v, u} X)
⊢ IsClosed[topologicalSpace] s ↔ IsClosed[inst✝] (up ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
⊢ Continuous[ULift.topologicalSpace, ULift.topologicalSpace] (ULift.map f)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ x ∈ s, f x ∈ 𝓝[s] x
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
⊢ IsClosed[inst✝] (range ULift.down)

Tactic:
by

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
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(ULift.{v, u} X, ULift.{u, v} Y)
⊢ Continuous[inst✝¹, inst✝] (ULift.down ∘ ⇑f ∘ ULift.up)

Tactic:
by

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
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
⊢ Continuous[ULift.topologicalSpace, ULift.topologicalSpace] (ULift.up ∘ ⇑f ∘ ULift.down)

Tactic:
by

Goal state after:
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✝
ι : Type u_4
inst✝² : Finite ι
X : ι → Type u_5
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), WeaklyLocallyCompactSpace (X i)
f : (i : ι) → X i
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
t : Set ↑s
ht : IsOpen[instTopologicalSpaceSubtype] t
hs : IsOpen[inst✝] s
⊢ IsOpen[inst✝] (Subtype.val '' t)

Tactic:
by

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✝ : WeaklyLocallyCompactSpace X
f : X → Y
hf : IsOpenQuotientMap f
⊢ ∀ (x : Y), ∃ s, IsCompact s ∧ s ∈ 𝓝 x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t✝] u
a : α → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
⊢ ∃ T, T.Countable ∧ ⋃ i ∈ T, a ↑i = ⋃ i, a ↑i

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
t : Set ↑s
ht : IsClosed[instTopologicalSpaceSubtype] t
hs : IsClosed[inst✝] s
⊢ IsClosed[inst✝] (Subtype.val '' t)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : WeaklyLocallyCompactSpace X
K : Set X
hK : IsCompact K
⊢ ∃ K', IsCompact K' ∧ K ⊆ interior K'

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_1
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t✝] u
a : α → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
T : Set ↑u
T_count : T.Countable
hT : ⋃ i ∈ T, a ↑i = ⋃ i, a ↑i
x : α
xu : x ∈ u
⊢ ⟨x, xu⟩ ∈ (fun x ↦ a ↑x) ⁻¹' t

Tactic:
exact hat x xu

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyCompactSpace X
x : X
⊢ ∀ t ∈ 𝓝 x, ∃ r ∈ 𝓝 x, IsCompact r ∧ r ⊆ t

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
p : X × Y → Prop
⊢ (∀ᶠ (q : X × Y) in 𝓝ˢ (s ×ˢ t), p q) ↔
    ∀ x ∈ s,
      ∀ y ∈ t,
        ∃ px,
          (∀ᶠ (x' : X) in 𝓝 x, px x') ∧ ∃ py, (∀ᶠ (y' : Y) in 𝓝 y, py y') ∧ ∀ {x : X}, px x → ∀ {y : Y}, py y → p (x, y)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t✝] u
⊢ ∃ s ⊆ t, s.Countable ∧ u = ⋃ a ∈ s, a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : Set α → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
⊢ ⋃ u ∈ countableBasis α, s u ⊆ t

Tactic:
by

Goal state after:
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)
hn : n ∈ 𝓝 t
⊢ ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case h_open
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : Set α → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
⊢ ∀ u ∈ ⋃ u ∈ countableBasis α, s u, IsOpen[t✝] u

Tactic:
simp only [mem_iUnion, exists_prop, forall_exists_index, and_imp]
    have := @ht.isOpen
    grind

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : Set α → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
x : α
v : Set α
hx : x ∈ v
hv : IsOpen[t✝] v
u : Set α
u_mem : u ∈ countableBasis α
xu : x ∈ u
uv : u ⊆ v
⊢ x ∈ ⋃ a ∈ s u, a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : Set α → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
x : α
v : Set α
hx : x ∈ v
hv : IsOpen[t✝] v
u : Set α
u_mem : u ∈ countableBasis α
xu : x ∈ u
uv : u ⊆ v
this : x ∈ ⋃ a ∈ s u, a
⊢ ∃ w ∈ s u, x ∈ w

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.SmallSets

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_1
⊢ GaloisConnection (fun L ↦ L.bind 𝓟) smallSets

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_4
ι : Sort u_5
p : ι → Prop
l : Filter α
s : ι → Set α
q : Set α → Prop
hl : l.HasBasis p s
hq : ∀ ⦃s t : Set α⦄, s ⊆ t → q t → q s
⊢ (∀ᶠ (s : Set α) in l.smallSets, q s) ↔ ∃ i, p i ∧ q (s i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_4
l : Filter α
p : Set α → Prop
hp : ∀ ⦃s t : Set α⦄, s ⊆ t → p s → p t
⊢ ∀ ⦃s t : Set α⦄, s ⊆ t → ¬p t → ¬p s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
⊢ ∃ s ⊆ t, s.Countable ∧ IsTopologicalBasis s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_4
l : Filter α
p : Set α → Prop
hp : ∀ ⦃s t : Set α⦄, s ⊆ t → p s → p t
⊢ (∃ᶠ (s : Set α) in l.smallSets, p s) ↔ ∀ t ∈ l, p t

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_4
ι : Sort u_5
p : ι → Prop
l : Filter α
s : ι → Set α
q : Set α → Prop
hl : l.HasBasis p s
hq : ∀ ⦃s t : Set α⦄, s ⊆ t → q s → q t
⊢ (∃ᶠ (s : Set α) in l.smallSets, q s) ↔ ∀ (i : ι), p i → q (s i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
f : α → β
⊢ Tendsto (fun x ↦ f '' x) la.smallSets lb.smallSets ↔ Tendsto f la lb

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_1
⊢ ⊥.smallSets = pure ∅

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_1
⊢ ⊤.smallSets = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter β
f : α → β
⊢ (comap f l).smallSets = comap (image f) l.smallSets

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_3
l✝ l' la : Filter α
lb : Filter β
l : Filter α
⊢ l.smallSets.NeBot

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
u : Set α
hu : u ∈ s'
⊢ ∃ f, f.Finite ∧ f ⊆ t ∧ ⋂₀ f = u

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
s t : α → Set β
ht : Tendsto t la lb.smallSets
hst : ∀ᶠ (x : α) in la, s x ⊆ t x
⊢ Tendsto s la lb.smallSets

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_1
l l' : Filter α
p : α → Prop
⊢ (∃ s ∈ l, ∀ᶠ (x : α) in l', x ∈ s → p x) ↔ ∃ s ∈ l, ∃ t ∈ l', ∀ x ∈ t, x ∈ s → p x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_1
l l' : Filter α
p : α → Prop
⊢ (∃ s ∈ l, ∃ t ∈ l', ∀ x ∈ t, x ∈ s → p x) ↔ ∀ᶠ (x : α) in l ⊓ l', p x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_1
l : Filter α
p : α → Prop
⊢ (∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, p x) ↔ ∀ᶠ (x : α) in l, p x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
⊢ ⋃ u ∈ s', f u ⊆ t

Tactic:
by

Goal state after:
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✝ : ∀ (i : ι), CompactSpace (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
hn : n ∈ 𝓝 t
⊢ ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyCompactSpace X
x : X
U : Set X
hU : IsOpen[inst✝¹] U
hx : x ∈ U
⊢ ∃ K, IsCompact K ∧ x ∈ interior K ∧ K ⊆ U

Tactic:
by

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✝ : LocallyCompactPair X Y
f : X → Y
K : Set X
U : Set Y
hf : Continuous[inst✝², inst✝¹] f
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hKU : MapsTo f K U
⊢ ∃ L ∈ 𝓝ˢ K, IsCompact L ∧ MapsTo f L U

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyCompactSpace X
K : Set X
hK : IsCompact K
⊢ ∀ ⦃s t : Set X⦄, s ⊆ t → (∃ r ∈ 𝓝ˢ K, IsCompact r ∧ r ⊆ s) → ∃ r ∈ 𝓝ˢ K, IsCompact r ∧ r ⊆ t

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
g : ι' → ι
hf : LocallyFinite f
hg : InjOn g {i | (f (g i)).Nonempty}
x : X
⊢ ∃ t ∈ 𝓝 x, {i | ((f ∘ g) i ∩ t).Nonempty}.Finite

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
g : ι' → ι
hg : Surjective g
hfg : LocallyFinite (f ∘ g)
⊢ LocallyFinite f

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyCompactSpace X
K : Set X
hK : IsCompact K
U : Set X
hU : IsOpen[inst✝¹] U
h_KU : K ⊆ U
L : Set X
hL : IsCompact L
hKL : K ⊆ interior L
hLU : L ⊆ U
⊢ L ∈ 𝓝ˢ K

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyCompactSpace X
K : Set X
hK : IsCompact K
⊢ (𝓝ˢ K).HasBasis (fun L ↦ L ∈ 𝓝ˢ K ∧ IsCompact L) id

Tactic:
rw [hasBasis_self, (hasBasis_nhdsSet _).forall_iff (by grind)]
  intro U ⟨hU, h_KU⟩
  obtain ⟨L, hL, hKL, hLU⟩ := exists_compact_between hK hU h_KU
  exact ⟨L, by rwa [← subset_interior_iff_mem_nhdsSet], hL, hLU⟩

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyCompactSpace X
K : Set X
hK : IsCompact K
⊢ (𝓝ˢ K).HasBasis (fun L ↦ L ∈ 𝓝ˢ K ∧ IsCompact L) id

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : {i | (f i ∩ U).Nonempty}.Finite
⊢ 𝓝[⋃ i, f i] a = 𝓝[⋃ i, f i ∩ U] a

Tactic:
by

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 X
f : X → Y
hf : IsOpenQuotientMap f
⊢ ∀ (x : Y), ∀ n ∈ 𝓝 x, ∃ s ∈ 𝓝 x, s ⊆ n ∧ IsCompact s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : {i | (f i ∩ U).Nonempty}.Finite
⊢ 𝓝[⋃ i, f i ∩ U] a = 𝓝[⋃ i ∈ {j | (f j ∩ U).Nonempty}, f i ∩ U] a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
a : X
⊢ 𝓝[⋃ i, f i] a = ⨆ i, 𝓝[f i] a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure[inst✝¹] (f i), ContinuousWithinAt g (f i) x
⊢ ContinuousOn g (⋃ i, f i)

Tactic:
by

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
⊢ (𝓝 x).HasBasis (fun s ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U) fun s ↦ f ⁻¹' (s ∩ Z)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
⊢ LocallyFinite fun i ↦ closure[inst✝] (f i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
h : LocallyFinite f
⊢ closure[inst✝] (⋃ i, f i) = ⋃ i, closure[inst✝] (f i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed[inst✝] (f i)
⊢ IsClosed[inst✝] (⋃ i, f i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed[inst✝] (f i)
x : X
this : IsClosed[inst✝] (⋃ i, f ↑i)
⊢ IsOpen[inst✝] (⋂ i, ⋂ (_ : x ∉ f i), (f i)ᶜ)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed[inst✝] (f i)
x : X
⊢ ⋂ i, ⋂ (_ : x ∉ f i), (f i)ᶜ ∈ 𝓝 x

Tactic:
by

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
this : ∀ (x : X), (𝓝 x).HasBasis (fun s ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U) fun s ↦ f ⁻¹' (s ∩ Z)
x : X
s : Set Y
x✝ : (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U
left✝ : s ∈ 𝓝 (f x)
hs : IsCompact s
hsU : s ⊆ U
⊢ s ∩ Z ⊆ U ∩ Z

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: X : Type u_4
inst✝ : TopologicalSpace X
π : X → Sort u_6
f : ℕ → (x : X) → π x
hf : LocallyFinite fun n ↦ {x | f (n + 1) x ≠ f n x}
⊢ ∃ F, ∀ (x : X), ∀ᶠ (p : ℕ × X) in atTop ×ˢ 𝓝 x, f p.1 p.2 = F p.2

Tactic:
by

Goal state after: