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

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
s : Set (Set α)
hsg : t✝ = generateFrom s
hsi : FiniteInter s
t : Set α
ht : t ∈ s
⊢ {t} ∈ {f | f.Finite ∧ f ⊆ s} ∧ (fun f ↦ ⋂₀ f) {t} = t

Tactic:
simpa using

Goal state after:
α : Type u
t✝ : TopologicalSpace α
s : Set (Set α)
hsg : t✝ = generateFrom s
hsi : FiniteInter s
t : Set α
ht : t ∈ s
⊢ t ∈ s
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
r : Set (Set α)
hsg : t = generateFrom r
hsi : ∀ ⦃s : Set α⦄, s ∈ r → ∀ ⦃t : Set α⦄, t ∈ r → s ∩ t ∈ r
⊢ t = generateFrom (insert univ r)

Tactic:
simpa using

Goal state after:
α : Type u
t : TopologicalSpace α
r : Set (Set α)
hsg : t = generateFrom r
hsi : ∀ ⦃s : Set α⦄, s ∈ r → ∀ ⦃t : Set α⦄, t ∈ r → s ∩ t ∈ r
⊢ t = generateFrom r
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_open : ∀ u ∈ s, IsOpen[t] u
h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen[t] u → ∃ v ∈ s, a ∈ v ∧ v ⊆ u
a : α
⊢ ∀ (i : Set α), a ∈ i ∧ IsOpen[t] i → ∃ i', (i' ∈ s ∧ a ∈ i') ∧ id i' ⊆ i

Tactic:
simpa using

Goal state after:
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_open : ∀ u ∈ s, IsOpen[t] u
h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen[t] u → ∃ v ∈ s, a ∈ v ∧ v ⊆ u
a : α
⊢ ∀ (i : Set α), a ∈ i → IsOpen[t] i → ∃ i' ∈ s, a ∈ i' ∧ i' ⊆ i
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
t : Set ↑s
ht : IsOpen[instTopologicalSpaceSubtype] t
⊢ ∃ c, IsOpen[inst✝] c ∧ Subtype.val '' t = c ∩ s

Tactic:
simpa using

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
t : Set ↑s
ht : IsOpen[instTopologicalSpaceSubtype] t
⊢ ∃ c, IsOpen[inst✝] c ∧ Subtype.val '' t = c ∩ s
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case refine_2
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : ∀ (U : Set X), IsOpen[inst✝] U → U.Nonempty → (U ∩ s).Nonempty
v : Set X
hv1 : IsOpen[inst✝] v
t : Set X
ht : IsOpen[inst✝] t
ht' : t.Nonempty
hud : ∀ (U : Set ↑s), IsOpen[instTopologicalSpaceSubtype] U → U.Nonempty → (U ∩ Subtype.val ⁻¹' v).Nonempty
x : X
hx : x ∈ t ∩ s
⊢ (s ↓∩ t).Nonempty

Tactic:
simpa using

Goal state after:
case refine_2
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : ∀ (U : Set X), IsOpen[inst✝] U → U.Nonempty → (U ∩ s).Nonempty
v : Set X
hv1 : IsOpen[inst✝] v
t : Set X
ht : IsOpen[inst✝] t
ht' : t.Nonempty
hud : ∀ (U : Set ↑s), IsOpen[instTopologicalSpaceSubtype] U → U.Nonempty → (U ∩ Subtype.val ⁻¹' v).Nonempty
x : X
hx : x ∈ t ∩ s
⊢ (s ↓∩ t).Nonempty
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
t : Set ↑s
ht : IsClosed[instTopologicalSpaceSubtype] t
⊢ ∃ c, IsClosed[inst✝] c ∧ Subtype.val '' t = c ∩ s

Tactic:
simpa using

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
t : Set ↑s
ht : IsClosed[instTopologicalSpaceSubtype] t
⊢ ∃ c, IsClosed[inst✝] c ∧ Subtype.val '' t = c ∩ s
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsOpen[inst✝] s
h : IsOpen[instTopologicalSpaceSubtype] (s ↓∩ t)
⊢ IsOpen[inst✝] (s ∩ t)

Tactic:
simpa using

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsOpen[inst✝] s
h : IsOpen[instTopologicalSpaceSubtype] (s ↓∩ t)
⊢ IsOpen[inst✝] (s ∩ t)
Module: Mathlib.Topology.Constructions

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

Tactic:
simpa using

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsClosed[inst✝] s
h : IsClosed[instTopologicalSpaceSubtype] (s ↓∩ t)
⊢ IsClosed[inst✝] (s ∩ t)
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t : TopologicalSpace α
γ : Type u_2
s : TopologicalSpace β
B₁ : Set (Set α)
B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
f₁ : γ → α
f₂ : γ → β
⊢ IsTopologicalBasis (image2 (fun x1 x2 ↦ f₁ ⁻¹' x1 ∩ f₂ ⁻¹' x2) B₁ B₂)

Tactic:
simpa using

Goal state after:
α : Type u
β : Type u_1
t : TopologicalSpace α
γ : Type u_2
s : TopologicalSpace β
B₁ : Set (Set α)
B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
f₁ : γ → α
f₂ : γ → β
⊢ IsTopologicalBasis (image2 (fun x1 x2 ↦ f₁ ⁻¹' x1 ∩ f₂ ⁻¹' x2) B₁ B₂)
Module: Mathlib.Topology.Constructions

Goal state before:
pp: Y : Type v
n : ℕ
A : Fin (n + 1) → Type u_9
inst✝ : (i : Fin (n + 1)) → TopologicalSpace (A i)
f : Y → A 0
g : Y → (j : Fin n) → A j.succ
l : Filter Y
x : A 0
y : (j : Fin n) → A j.succ
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
j : Fin (n + 1)
⊢ ∀ (i : Fin n), Tendsto (fun i_1 ↦ Fin.cons (f i_1) (g i_1) i.succ) l (𝓝 (Fin.cons x y i.succ))

Tactic:
simpa using

Goal state after:
Y : Type v
n : ℕ
A : Fin (n + 1) → Type u_9
inst✝ : (i : Fin (n + 1)) → TopologicalSpace (A i)
f : Y → A 0
g : Y → (j : Fin n) → A j.succ
l : Filter Y
x : A 0
y : (j : Fin n) → A j.succ
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
j : Fin (n + 1)
⊢ ∀ (i : Fin n), Tendsto (fun i_1 ↦ g i_1 i) l (𝓝 (y i))
Module: Mathlib.Topology.Constructions

Goal state before:
pp: Y : Type v
n : ℕ
A : Fin (n + 1) → Type u_9
inst✝ : (i : Fin (n + 1)) → TopologicalSpace (A i)
f : Y → (j : Fin n) → A j.castSucc
g : Y → A (Fin.last n)
l : Filter Y
x : (j : Fin n) → A j.castSucc
y : A (Fin.last n)
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
j : Fin (n + 1)
⊢ ∀ (i : Fin n), Tendsto (fun i_1 ↦ Fin.snoc (f i_1) (g i_1) i.castSucc) l (𝓝 (Fin.snoc x y i.castSucc))

Tactic:
simpa using

Goal state after:
Y : Type v
n : ℕ
A : Fin (n + 1) → Type u_9
inst✝ : (i : Fin (n + 1)) → TopologicalSpace (A i)
f : Y → (j : Fin n) → A j.castSucc
g : Y → A (Fin.last n)
l : Filter Y
x : (j : Fin n) → A j.castSucc
y : A (Fin.last n)
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
j : Fin (n + 1)
⊢ ∀ (i : Fin n), Tendsto (fun i_1 ↦ f i_1 i) l (𝓝 (x i))
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
g : β → α
x : β
s : Set β
h : LeftInvOn f g s
hx : f (g x) = x
hf : ContinuousWithinAt f (g '' s) (g x)
hg : ContinuousWithinAt g s x
A : g ∘ f =ᶠ[𝓝[g '' s] g x] id
⊢ Tendsto f (𝓝[g '' s] g x) (𝓝[s] x)

Tactic:
simpa using

Goal state after:
case a
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
g : β → α
x : β
s : Set β
h : LeftInvOn f g s
hx : f (g x) = x
hf : ContinuousWithinAt f (g '' s) (g x)
hg : ContinuousWithinAt g s x
A : g ∘ f =ᶠ[𝓝[g '' s] g x] id
⊢ Tendsto f (𝓝[g '' s] g x) (𝓝[s] x)
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
g : β → α
x : β
h : LeftInverse f g
hf : ContinuousWithinAt f (range g) (g x)
hg : ContinuousAt g x
⊢ map g (𝓝 x) = 𝓝[range g] g x

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
g : β → α
x : β
h : LeftInverse f g
hf : ContinuousWithinAt f (range g) (g x)
hg : ContinuousAt g x
⊢ map g (𝓝 x) = 𝓝[range g] g x
Module: Mathlib.Topology.Constructions

Goal state before:
pp: Y : Type v
n : ℕ
A : Fin (n + 1) → Type u_9
inst✝ : (i : Fin (n + 1)) → TopologicalSpace (A i)
i : Fin (n + 1)
f : Y → A i
g : Y → (j : Fin n) → A (i.succAbove j)
l : Filter Y
x : A i
y : (j : Fin n) → A (i.succAbove j)
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
j : Fin (n + 1)
⊢ ∀ (j : Fin n), Tendsto (fun i_1 ↦ i.insertNth (f i_1) (g i_1) (i.succAbove j)) l (𝓝 (i.insertNth x y (i.succAbove j)))

Tactic:
simpa using

Goal state after:
Y : Type v
n : ℕ
A : Fin (n + 1) → Type u_9
inst✝ : (i : Fin (n + 1)) → TopologicalSpace (A i)
i : Fin (n + 1)
f : Y → A i
g : Y → (j : Fin n) → A (i.succAbove j)
l : Filter Y
x : A i
y : (j : Fin n) → A (i.succAbove j)
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
j : Fin (n + 1)
⊢ ∀ (j : Fin n), Tendsto (fun i ↦ g i j) l (𝓝 (y j))
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
h : IsTopologicalBasis ∅
⊢ IsEmpty α

Tactic:
simpa using

Goal state after:
α : Type u
t : TopologicalSpace α
h : IsTopologicalBasis ∅
⊢ IsEmpty α
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
h : IsTopologicalBasis {∅}
⊢ IsEmpty α

Tactic:
simpa using

Goal state after:
α : Type u
t : TopologicalSpace α
h : IsTopologicalBasis {∅}
⊢ IsEmpty α
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
x : α
⊢ ⋃ y, ⋃ (_ : y ≤ x), accumulate s y = ⋃ y, ⋃ (_ : y ≤ x), s y

Tactic:
apply Subset.antisymm

Goal state after:
case h₁
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
x : α
⊢ ⋃ y, ⋃ (_ : y ≤ x), accumulate s y ⊆ ⋃ y, ⋃ (_ : y ≤ x), s y

case h₂
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
x : α
⊢ ⋃ y, ⋃ (_ : y ≤ x), s y ⊆ ⋃ y, ⋃ (_ : y ≤ x), accumulate s y
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ⋃ x, accumulate s x = ⋃ x, s x

Tactic:
apply Subset.antisymm

Goal state after:
case h₁
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ⋃ x, accumulate s x ⊆ ⋃ x, s x

case h₂
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ⋃ x, s x ⊆ ⋃ x, accumulate s x
Module: Mathlib.Topology.Bornology.Basic

Goal state before:
pp: α : Type u_2
s : Set α
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B
union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B
sUnion_univ : ∀ (x : α), {x} ∈ B
⊢ IsBounded s ↔ s ∈ B

Tactic:
rw [isBounded_def, ofBounded_cobounded, compl_mem_comk]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
t u : Set β
h : u ∈ 𝓝ˢ t
⊢ f ⁻¹' u ∈ 𝓝ˢ[s] (s ∩ f ⁻¹' t)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
t u : Set β
h : u ∈ 𝓝ˢ t
⊢ f ⁻¹' u ∈ 𝓝ˢ[s] (s ∩ f ⁻¹' t)
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous[inst✝¹, inst✝] f
s u s' : Set β
h : u ∈ 𝓝ˢ[s'] s
⊢ f ⁻¹' u ∈ 𝓝ˢ[f ⁻¹' s'] (f ⁻¹' s)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous[inst✝¹, inst✝] f
s u s' : Set β
h : u ∈ 𝓝ˢ[s'] s
⊢ f ⁻¹' u ∈ 𝓝ˢ[f ⁻¹' s'] (f ⁻¹' s)
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous[inst✝¹, inst✝] f
s u : Set β
h : u ∈ 𝓝ˢ s
⊢ f ⁻¹' u ∈ 𝓝ˢ (f ⁻¹' s)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous[inst✝¹, inst✝] f
s u : Set β
h : u ∈ 𝓝ˢ s
⊢ f ⁻¹' u ∈ 𝓝ˢ (f ⁻¹' s)
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
T : (i : ι) → TopologicalSpace (A i)
inst✝ : (i : ι) → TopologicalSpace (B i)
f : (i : ι) → A i → B i
hf : ∀ (i : ι), IsClosedEmbedding (f i)
⊢ IsClosed[Pi.topologicalSpace] (range (Pi.map f))

Tactic:
simpa using

Goal state after:
ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
T : (i : ι) → TopologicalSpace (A i)
inst✝ : (i : ι) → TopologicalSpace (B i)
f : (i : ι) → A i → B i
hf : ∀ (i : ι), IsClosedEmbedding (f i)
⊢ IsClosed[Pi.topologicalSpace] (univ.pi fun i ↦ range (f i))
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
T : (i : ι) → TopologicalSpace (A i)
inst✝¹ : (i : ι) → TopologicalSpace (B i)
inst✝ : Finite ι
f : (i : ι) → A i → B i
hf : ∀ (i : ι), IsOpenEmbedding (f i)
⊢ IsOpen[Pi.topologicalSpace] (range (Pi.map f))

Tactic:
simpa using

Goal state after:
ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
T : (i : ι) → TopologicalSpace (A i)
inst✝¹ : (i : ι) → TopologicalSpace (B i)
inst✝ : Finite ι
f : (i : ι) → A i → B i
hf : ∀ (i : ι), IsOpenEmbedding (f i)
⊢ IsOpen[Pi.topologicalSpace] (univ.pi fun i ↦ range (f i))
Module: Mathlib.Topology.Bases

Goal state before:
pp: ι : Type u_2
inst✝¹ : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst✝ : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure[inst✝ i] (c i)
this : ∀ (i : ι), Countable ↑(c i)
g : (I : Finset ι) × ((i : ↥I) → ↑(c ↑i)) → (i : ι) → X i :=
  fun x i ↦
    match x with
    | ⟨I, f⟩ => if hi : i ∈ I then ↑(f ⟨i, hi⟩) else f₀ i
f✝ : (i : ι) → X i
hf : f✝ ∈ univ.pi s
o : Set ((i : ι) → X i)
ho : IsOpen[Pi.topologicalSpace] o
hfo : f✝ ∈ o
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst✝ a] (u a) ∧ f✝ a ∈ u a
hI : (↑I).pi u ⊆ o
f : (i : ι) → i ∈ I → X i
hfu : ∀ (i : ι) (a : i ∈ I), f i a ∈ u i
hfc : ∀ (i : ι) (a : i ∈ I), f i a ∈ c i
i : ι
hi : i ∈ I
⊢ g ⟨I, fun i ↦ ⟨f ↑i ⋯, ⋯⟩⟩ i ∈ u i

Tactic:
simpa using

Goal state after:
ι : Type u_2
inst✝¹ : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst✝ : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure[inst✝ i] (c i)
this : ∀ (i : ι), Countable ↑(c i)
g : (I : Finset ι) × ((i : ↥I) → ↑(c ↑i)) → (i : ι) → X i :=
  fun x i ↦
    match x with
    | ⟨I, f⟩ => if hi : i ∈ I then ↑(f ⟨i, hi⟩) else f₀ i
f✝ : (i : ι) → X i
hf : f✝ ∈ univ.pi s
o : Set ((i : ι) → X i)
ho : IsOpen[Pi.topologicalSpace] o
hfo : f✝ ∈ o
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst✝ a] (u a) ∧ f✝ a ∈ u a
hI : (↑I).pi u ⊆ o
f : (i : ι) → i ∈ I → X i
hfu : ∀ (i : ι) (a : i ∈ I), f i a ∈ u i
hfc : ∀ (i : ι) (a : i ∈ I), f i a ∈ c i
i : ι
hi : i ∈ I
⊢ f i ⋯ ∈ u i
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : DecidableEq ι
s : Set ((a : ι) → A a)
x y : (a : ι) → A a
I : Finset ι
t : (i : ι) → Set (A i)
htx : ∀ (i : ι), t i ∈ 𝓝 (x i)
hts : (↑I).pi t ⊆ s
i : ι
hi : i ∈ ↑I
⊢ I.piecewise x y i ∈ t i

Tactic:
simpa using

Goal state after:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : DecidableEq ι
s : Set ((a : ι) → A a)
x y : (a : ι) → A a
I : Finset ι
t : (i : ι) → Set (A i)
htx : ∀ (i : ι), t i ∈ 𝓝 (x i)
hts : (↑I).pi t ⊆ s
i : ι
hi : i ∈ ↑I
⊢ x i ∈ t i
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
s : Set α
inst✝ : SeparableSpace ↑s
⊢ IsSeparable s

Tactic:
simpa using

Goal state after:
α : Type u
t : TopologicalSpace α
s : Set α
inst✝ : SeparableSpace ↑s
⊢ IsSeparable s
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
f : Filter α
s : Set α
H : ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g
hf : s ∉ f
g : Filter ↑sᶜ := comap Subtype.val f
this : g.NeBot
⊢ False

Tactic:
simpa using

Goal state after:
α : Type u
f : Filter α
s : Set α
H : ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g
hf : s ∉ f
g : Filter ↑sᶜ := comap Subtype.val f
this : g.NeBot
⊢ False
Module: Mathlib.Order.Filter.Ultrafilter.Basic

Goal state before:
pp: α : Type u
β : Type v
f : Ultrafilter α
inst✝ : Finite β
P : β → α → Prop
⊢ (∀ᶠ (i : α) in ↑f, ∃ a, P a i) ↔ ∃ a, ∀ᶠ (i : α) in ↑f, P a i

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
f : Ultrafilter α
inst✝ : Finite β
P : β → α → Prop
⊢ (∀ᶠ (i : α) in ↑f, ∃ a, P a i) ↔ ∃ a, ∀ᶠ (i : α) in ↑f, P a i
Module: Mathlib.Order.Filter.Ultrafilter.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
l₁ : Filter α
l₂ : Filter β
⊢ Tendsto f l₁ l₂ ↔ ∀ (g : Ultrafilter α), ↑g ≤ l₁ → Tendsto f (↑g) l₂

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
f : α → β
l₁ : Filter α
l₂ : Filter β
⊢ l₁ ≤ comap f l₂ ↔ ∀ (g : Ultrafilter α), ↑g ≤ l₁ → ↑g ≤ comap f l₂
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : SeparableSpace α
inst✝ : PartialOrder α
⊢ ∃ s, s.Countable ∧ Dense s ∧ (∀ (x : α), IsBot x → x ∈ s) ∧ ∀ (x : α), IsTop x → x ∈ s

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : SeparableSpace α
inst✝ : PartialOrder α
⊢ ∃ s, s.Countable ∧ Dense s ∧ (∀ (x : α), IsBot x → x ∈ s) ∧ ∀ (x : α), IsTop x → x ∈ s
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case refine_1
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : TopologicalSpace X
f : Sigma σ → X
h : IsInducing f
i : ι
U : Set X
hUo : IsOpen[inst✝] U
hU : f ⁻¹' U = range (Sigma.mk i)
⊢ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i

Tactic:
simpa using

Goal state after:
case refine_1
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : TopologicalSpace X
f : Sigma σ → X
h : IsInducing f
i : ι
U : Set X
hUo : IsOpen[inst✝] U
hU : f ⁻¹' U = range (Sigma.mk i)
⊢ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
Module: Mathlib.Topology.Bases

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

Tactic:
by
  choose p hp using fun s : countableBasis α => nonempty_of_mem_countableBasis s.2
  exact ⟨⟨range p, countable_range _, (isBasis_countableBasis α).dense_iff.2 fun o ho _ =>
          ⟨p ⟨o, ho⟩, hp ⟨o, _⟩, mem_range_self _⟩⟩⟩

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
x✝¹ : (∀ (i : ι), IsInducing (f ∘ Sigma.mk i)) ∧ ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
h₁ : ∀ (i : ι), IsInducing (f ∘ Sigma.mk i)
h₂ : ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
x✝ : Sigma σ
i : ι
x : σ i
U : Set X
hUo : IsOpen[inst✝] U
hU : ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
y : Sigma σ
hy : y ∈ f ⁻¹' U
⊢ y ∈ range (Sigma.mk i)

Tactic:
simpa using

Goal state after:
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : TopologicalSpace X
f : Sigma σ → X
x✝¹ : (∀ (i : ι), IsInducing (f ∘ Sigma.mk i)) ∧ ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
h₁ : ∀ (i : ι), IsInducing (f ∘ Sigma.mk i)
h₂ : ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
x✝ : Sigma σ
i : ι
x : σ i
U : Set X
hUo : IsOpen[inst✝] U
hU : ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
y : Sigma σ
hy : y ∈ f ⁻¹' U
⊢ y.fst = i
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:
simpa using

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyCompactSpace X
x : X
⊢ ∀ t ∈ 𝓝 x, ∃ r, (IsCompact r ∧ r ⊆ t) ∧ r ∈ 𝓝 x
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_2
α : 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
⊢ u = ⋃ i, a ↑i

Tactic:
apply Subset.antisymm

Goal state after:
case refine_2.h₁
α : 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
⊢ u ⊆ ⋃ i, a ↑i

case refine_2.h₂
α : 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
⊢ ⋃ i, a ↑i ⊆ u
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:
simpa using

Goal state after:
α : 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
⊢ ∀ i ∈ countableBasis α, s i ⊆ t
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:
simpa using

Goal state after:
α : 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
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:
simpa using

Goal state after:
α : 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
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:
simpa using

Goal state after:
α : Type u_1
l : Filter α
p : α → Prop
⊢ (∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, p x) ↔ ∀ᶠ (x : α) in l, p x
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:
simpa using

Goal state after:
α : 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
⊢ ∀ i ∈ s', f i ⊆ t
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:
simpa using

Goal state after:
ι : 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