mathlib-initiative/mathlib-tactics huggingface dataset:
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

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t : TopologicalSpace α
B : Set (Set α)
s : Set α
inst✝² : TopologicalSpace β
inst✝¹ : SeparableSpace α
inst✝ : SeparableSpace β
⊢ SeparableSpace (α ⊕ β)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝ : DiscreteTopology α
⊢ SeparableSpace α ↔ Countable α

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝ : SeparableSpace α
ι : Type u_2
s : ι → Set α
hd : Pairwise (Disjoint on s)
ho : ∀ (i : ι), IsOpen[t] (s i)
hne : ∀ (i : ι), (s i).Nonempty
⊢ Countable ι

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
s u : Set α
hs : IsSeparable s
hu : u ⊆ s
⊢ IsSeparable u

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
ι : Sort u_2
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (i : ι), IsSeparable (s i)
⊢ IsSeparable (⋃ i, s i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
s t : Set α
⊢ IsSeparable (s ∪ t) ↔ IsSeparable s ∧ IsSeparable t

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
s : Set α
⊢ IsSeparable (closure[t] s) ↔ IsSeparable s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : Finite ι
s : Set ((a : ι) → A a)
val✝ : Fintype ι
a : (a : ι) → A a
x✝¹ : a ∈ s
x✝ : ∃ u, (∀ (a_1 : ι), IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1) ∧ univ.pi u ⊆ s
u : (a : ι) → Set (A a)
h1 : ∀ (a_1 : ι), IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1
right✝ : univ.pi u ⊆ s
⊢ (↑Finset.univ).pi u ⊆ s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : Finite ι
s : Set ((a : ι) → A a)
⊢ IsOpen[Pi.topologicalSpace] s ↔ ∀ f ∈ s, ∃ u, (∀ (a : ι), IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ univ.pi u ⊆ s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
i : Set ι
s : (a : ι) → Set (A a)
hs : ∀ a ∈ i, IsClosed[T a] (s a)
⊢ IsClosed[Pi.topologicalSpace] (i.pi s)

Tactic:
by

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

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

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
I : Set ι
s : (i : ι) → Set (A i)
a : (i : ι) → A i
hs : I.pi s ∈ 𝓝 a
i : ι
hi : i ∈ I
⊢ s i ∈ 𝓝 (a i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
i : Set ι
s : (a : ι) → Set (A a)
x : (a : ι) → A a
hi : i.Finite
hs : ∀ a ∈ i, s a ∈ 𝓝 (x a)
⊢ i.pi s ∈ 𝓝 x

Tactic:
rw [pi_def, biInter_mem hi]

Goal state after:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
i : Set ι
s : (a : ι) → Set (A a)
x : (a : ι) → A a
hi : i.Finite
hs : ∀ a ∈ i, s a ∈ 𝓝 (x a)
⊢ ∀ i_1 ∈ i, eval i_1 ⁻¹' s i_1 ∈ 𝓝 x
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
i : Set ι
s : (a : ι) → Set (A a)
x : (a : ι) → A a
hi : i.Finite
hs : ∀ a ∈ i, s a ∈ 𝓝 (x a)
⊢ i.pi s ∈ 𝓝 x

Tactic:
by

Goal state after:
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
H : ∀ i ∈ I, (u i ∩ c i).Nonempty
⊢ ∃ f, g ⟨I, f⟩ ∈ (↑I).pi u

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (A i)
a : (i : ι) → A i
⊢ I.pi s ∈ 𝓝 a ↔ ∀ i ∈ I, s i ∈ 𝓝 (a i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (A i)
⊢ interior (I.pi s) = I.pi fun i ↦ interior (s i)

Tactic:
by

Goal state after:
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 : (a : ι) → A a
hs : s ∈ 𝓝 x
y : (a : ι) → A a
⊢ ∃ I, I.piecewise x y ∈ s

Tactic:
by

Goal state after:
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)
h : ∀ (i : ι), IsSeparable (s i)
⊢ IsSeparable (univ.pi s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: ι : Type u_2
inst✝¹ : Countable ι
α : ι → Type u_3
s : (i : ι) → Set (α i)
inst✝ : (i : ι) → TopologicalSpace (α i)
h : ∀ (i : ι), IsSeparable (s i)
⊢ IsSeparable {f | ∀ (i : ι), f i ∈ s i}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s : Set α
t : Set β
hs : IsSeparable s
ht : IsSeparable t
⊢ IsSeparable (s ×ˢ t)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_9
g : (a : ι) → Set (Set (A a))
⊢ Pi.topologicalSpace = generateFrom {t | ∃ s i, (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
⊢ Pi.topologicalSpace = Pi.topologicalSpace

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s : Set α
hs : IsSeparable s
f : α → β
hf : Continuous[t, inst✝] f
⊢ IsSeparable (f '' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
s : Set α
hs : Dense s
⊢ IsSeparable s ↔ SeparableSpace α

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

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

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
s : Set ((i : ι) → X i)
x✝ : s ∈ {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}
t : (a : ι) → Set (X a)
ht : ∀ (a : ι), t a ∈ g a
Eq : s = univ.pi t
⊢ (∀ a ∈ Finset.univ, t a ∈ g a) ∧ s = (↑Finset.univ).pi t

Tactic:
by

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

Goal state before:
pp: α : Type u
f : Filter α
h₁ : f.NeBot
h₂ : ∀ (g : Filter α), g.NeBot → g ≤ f → f ≤ g
g : Filter α
neBot'✝ : g.NeBot
le_of_le✝ : ∀ (g_1 : Filter α), g_1.NeBot → g_1 ≤ g → g ≤ g_1
x✝ : ↑{ toFilter := f, neBot' := h₁, le_of_le := h₂ } = ↑{ toFilter := g, neBot' := neBot'✝, le_of_le := le_of_le✝ }
⊢ { toFilter := f, neBot' := h₁, le_of_le := h₂ } = { toFilter := g, neBot' := neBot'✝, le_of_le := le_of_le✝ }

Tactic:
by

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

Goal state before:
pp: α : Type u
f : Ultrafilter α
g : Filter α
hg : (g ⊓ ↑f).NeBot
⊢ (↑f ⊓ g).NeBot

Tactic:
by

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

Goal state before:
pp: α : Type u
f : Ultrafilter α
g : Filter α
⊢ Disjoint (↑f) g ↔ ¬↑f ≤ g

Tactic:
by

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

Goal state before:
pp: α : Type u
f : Ultrafilter α
s : Set α
hsc : sᶜ ∉ f
h : ↑f ⊓ 𝓟 s = ⊥
⊢ ↑f ⊓ 𝓟 sᶜᶜ = ⊥

Tactic:
by

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

Goal state before:
pp: α : Type u
f : Ultrafilter α
s : Set α
⊢ sᶜ ∈ f ↔ s ∉ f

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Filter α
h : ∀ (s : Set α), sᶜ ∉ f ↔ s ∈ f
hf : f = ⊥
⊢ False

Tactic:
by

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

Goal state before:
pp: α : Type u
u : Ultrafilter α
f g : Filter α
⊢ ¬↑u ≤ f ⊔ g ↔ ¬(↑u ≤ f ∨ ↑u ≤ g)

Tactic:
by

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

Goal state before:
pp: α : Type u
f : Ultrafilter α
s t : Set α
⊢ s ∪ t ∈ f ↔ s ∈ f ∨ t ∈ f

Tactic:
by

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

Goal state before:
pp: α : Type u
f : Ultrafilter α
p q : α → Prop
⊢ (∀ᶠ (x : α) in ↑f, p x → q x) ↔ (∀ᶠ (x : α) in ↑f, p x) → ∀ᶠ (x : α) in ↑f, q x

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
f g✝ : Ultrafilter α
s t : Set α
p q : α → Prop
m : α → β
u : Ultrafilter β
inj : Injective m
large : range m ∈ u
g : Filter α
hg : g.NeBot
hgu : g ≤ Filter.comap m ↑u
⊢ Filter.comap m ↑u ≤ g

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter α
h₀ : optParam (Injective id) ⋯
⊢ range id ∈ f

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter γ
m : α → β
n : β → γ
inj₀ : Injective n
large₀ : range n ∈ f
inj₁ : Injective m
large₁ : range m ∈ f.comap inj₀ large₀
inj₂ : optParam (Injective (n ∘ m)) ⋯
⊢ range (n ∘ m) ∈ f

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
f g : Ultrafilter α
s✝ t : Set α
p q : α → Prop
α✝ : Type ?u.21
a : α✝
s : Set α✝
⊢ sᶜ ∉ pure a ↔ s ∈ pure a

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
m : α → β
a : α
inj : Injective m
large : range m ∈ pure (m a)
⊢ 𝓟 (m ⁻¹' {m a}) = ↑(pure a)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s✝ t : Set α
p q : α → Prop
f : Ultrafilter α
m : α → Ultrafilter β
s : Set β
⊢ (sᶜ ∉ (↑f).bind fun x ↦ ↑(m x)) ↔ s ∈ (↑f).bind fun x ↦ ↑(m x)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
⊢ IsTopologicalBasis {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i}

Tactic:
by

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

Goal state before:
pp: α : Type u
f : Filter α
hf : f.NeBot
x : α
⊢ f = pure x ↔ {x} ∈ f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
⊢ Pi.topologicalSpace = generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}

Tactic:
by

Goal state after:
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
⊢ (range Subtype.val)ᶜ ∉ f

Tactic:
by

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

Goal state before:
pp: α : Type u
f : Filter α
s : Set α
⊢ s ∈ f ↔ ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g

Tactic:
by

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

Goal state before:
pp: α : Type u
f f' : Filter α
⊢ ⨆ g, ⨆ (_ : ↑g ≤ f), ↑g ≤ f' ↔ f ≤ f'

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
⊢ s ∈ ofComapInfPrincipal h

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
X : Type u_9
f : X → (i : ι) → A i
⊢ induced f Pi.topologicalSpace = ⨅ i, induced (fun x ↦ f x i) inferInstance

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
this : f.NeBot
⊢ Filter.map m (Filter.comap m ↑g) ⊓ Filter.map m (𝓟 s) = Filter.map m (Filter.comap m ↑g) ⊓ 𝓟 (m '' s)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
⊢ map m (ofComapInfPrincipal h) = g

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
ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
κ : Type u_8
inst✝⁴ : TopologicalSpace X
T : (i : ι) → TopologicalSpace (A i)
inst✝³ : (i : ι) → TopologicalSpace (B i)
f : X → (i : ι) → A i
inst✝² : TopologicalSpace Z
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), DiscreteTopology (A i)
x : (i : ι) → A i
⊢ IsOpen[topologicalSpace] (univ.pi fun i ↦ {x i})

Tactic:
exact isOpen_set_pi finite_univ fun i _ => (isOpen_discrete {x i})

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
ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
κ : Type u_8
inst✝⁴ : TopologicalSpace X
T : (i : ι) → TopologicalSpace (A i)
inst✝³ : (i : ι) → TopologicalSpace (B i)
f : X → (i : ι) → A i
inst✝² : TopologicalSpace Z
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), DiscreteTopology (A i)
x : (i : ι) → A i
⊢ IsOpen[topologicalSpace] {x}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
n : Type u_9
m : Type u_10
f : m → n
hf : Surjective f
⊢ IsEmbedding fun x ↦ x ∘ f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
s : Set (Sigma σ)
⊢ IsOpen[instTopologicalSpaceSigma] s ↔ ∀ (i : ι), IsOpen[inst✝ i] (Sigma.mk i ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
s : Set (Sigma σ)
⊢ IsClosed[instTopologicalSpaceSigma] s ↔ ∀ (i : ι), IsClosed[inst✝ i] (Sigma.mk i ⁻¹' s)

Tactic:
by

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

Goal state before:
pp: α : Type u
f : Ultrafilter α
s : Set (Set α)
hs : s.Finite
⊢ ⋃₀ s ∈ f ↔ ∃ t ∈ s, t ∈ f

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : Ultrafilter α
is : Set β
s : β → Set α
his : is.Finite
⊢ ⋃ i ∈ is, s i ∈ f ↔ ∃ i ∈ is, s i ∈ f

Tactic:
by

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

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

Tactic:
by

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

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

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

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case inl
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
j : ι
s : Set (σ j)
hs : IsOpen[inst✝ j] s
⊢ IsOpen[inst✝ j] (Sigma.mk j ⁻¹' Sigma.mk j '' s)

pp: case inr
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsOpen[inst✝ i] s
j : ι
hne : j ≠ i
⊢ IsOpen[inst✝ j] (Sigma.mk j ⁻¹' Sigma.mk i '' s)

Tactic:
· rwa [preimage_image_eq _ sigma_mk_injective]

Goal state after:
case inr
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsOpen[inst✝ i] s
j : ι
hne : j ≠ i
⊢ IsOpen[inst✝ j] (Sigma.mk j ⁻¹' Sigma.mk i '' s)
Module: Mathlib.Topology.Ultrafilter

Goal state before:
pp: X : Type u
x : X
inst✝ : TopologicalSpace X
f : Filter X
⊢ ClusterPt x f ↔ ∃ u, ↑u ≤ f ∧ ↑u ≤ 𝓝 x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
⊢ IsTopologicalBasis {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
⊢ IsTopologicalBasis {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = (↑F).pi U}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
⊢ IsOpenMap (Sigma.mk i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Ultrafilter

Goal state before:
pp: X : Type u
α : Type u_1
x : X
inst✝ : TopologicalSpace X
F : Filter α
u : α → X
⊢ MapClusterPt x F u ↔ ∃ U, ↑U ≤ F ∧ Tendsto u (↑U) (𝓝 x)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Ultrafilter

Goal state before:
pp: X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ IsOpen[inst✝] s ↔ ∀ x ∈ s, ∀ (l : Ultrafilter X), ↑l ≤ 𝓝 x → s ∈ l

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Ultrafilter

Goal state before:
pp: X : Type u
x : X
s : Set X
inst✝ : TopologicalSpace X
⊢ x ∈ closure[inst✝] s ↔ ∃ u, s ∈ u ∧ ↑u ≤ 𝓝 x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Ultrafilter

Goal state before:
pp: X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ IsClosed[inst✝] s ↔ ∀ (x : X) (u : Ultrafilter X), ↑u ≤ 𝓝 x → s ∈ u → x ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Ultrafilter

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ Continuous[inst✝¹, inst✝] f ↔ ∀ (x : X) (g : Ultrafilter X), ↑g ≤ 𝓝 x → Tendsto f (↑g) (𝓝 (f x))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case pos
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
i : ι
U : (i : ι) → Set (X i)
s : Finset ι
hU : ∀ i ∈ s, U i ∈ {U | IsOpen[inst✝ i] U}
h : ((↑s).pi U).Nonempty
hi : i ∈ s
⊢ IsOpen[inst✝ i] (U i)

Tactic:
exact hU _ hi

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case inl
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
j : ι
s : Set (σ j)
hs : IsClosed[inst✝ j] s
⊢ IsClosed[inst✝ j] (Sigma.mk j ⁻¹' Sigma.mk j '' s)

pp: case inr
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsClosed[inst✝ i] s
j : ι
hne : j ≠ i
⊢ IsClosed[inst✝ j] (Sigma.mk j ⁻¹' Sigma.mk i '' s)

Tactic:
· rwa [preimage_image_eq _ sigma_mk_injective]

Goal state after:
case inr
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsClosed[inst✝ i] s
j : ι
hne : j ≠ i
⊢ IsClosed[inst✝ j] (Sigma.mk j ⁻¹' Sigma.mk i '' s)
Module: Mathlib.Topology.Bases

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
i : ι
⊢ IsOpenMap (eval i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
⊢ IsClosedMap (Sigma.mk i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
x : Sigma σ
⊢ 𝓝 x = Filter.map (mk x.fst) (𝓝 x.snd)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

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

Tactic:
by

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

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝¹ : TopologicalSpace β
inst✝ : FirstCountableTopology β
f : α → β
hf : IsInducing f
⊢ FirstCountableTopology α

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
s : Set ι
⊢ IsOpen[instTopologicalSpaceSigma] (Sigma.fst ⁻¹' s)

Tactic:
rw [← biUnion_of_singleton s, preimage_iUnion₂]

Goal state after:
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
s : Set ι
⊢ IsOpen[instTopologicalSpaceSigma] (⋃ i ∈ s, Sigma.fst ⁻¹' {i})
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝¹ : FirstCountableTopology α
x : α
f : Filter α
inst✝ : f.IsCountablyGenerated
hx : ClusterPt x f
⊢ ∃ ψ, Tendsto ψ atTop (𝓝 x) ∧ Tendsto ψ atTop f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝¹ : FirstCountableTopology α
ι : Type u_1
f : Filter ι
inst✝ : f.IsCountablyGenerated
x : α
u : ι → α
hx : MapClusterPt x f u
⊢ ∃ ψ, Tendsto (u ∘ ψ) atTop (𝓝 x) ∧ Tendsto ψ atTop f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
s : Set ι
⊢ IsOpen[instTopologicalSpaceSigma] (Sigma.fst ⁻¹' s)

Tactic:
by

Goal state after: