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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx : x ∈ s ∩ {a | p a} ∪ s ∩ {a | p a}ᶜ
hx' : x ∉ frontier {a | p a}
⊢ ContinuousWithinAt (fun a ↦ if p a then f a else g a) (s ∩ {a | p a} ∪ s ∩ {a | p a}ᶜ) x

Tactic:
]

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx : x ∈ s ∩ {a | p a} ∪ s ∩ {a | p a}ᶜ
hx' : x ∉ frontier {a | p a}
⊢ ContinuousWithinAt (fun a ↦ if p a then f a else g a) (s ∩ {a | p a} ∪ s ∩ {a | p a}ᶜ) x
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
hs : IsCompact s
t : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : IsOpen[instTopologicalSpaceProd] n
hp : ∃ i, ((IsOpen[inst✝¹] i.1 ∧ s ⊆ i.1) ∧ IsOpen[inst✝] i.2 ∧ t ⊆ i.2) ∧ i.1 ×ˢ i.2 ⊆ n
⊢ ∃ u v, IsOpen[inst✝¹] u ∧ IsOpen[inst✝] v ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ v ⊆ n

Tactic:
]

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
hs : IsCompact s
t : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : IsOpen[instTopologicalSpaceProd] n
hp : ∃ i, ((IsOpen[inst✝¹] i.1 ∧ s ⊆ i.1) ∧ IsOpen[inst✝] i.2 ∧ t ⊆ i.2) ∧ i.1 ×ˢ i.2 ⊆ n
⊢ ∃ u v, IsOpen[inst✝¹] u ∧ IsOpen[inst✝] v ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ v ⊆ n
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s s' : Set X
hs : IsCompact s
t t' : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : ∃ t₁ ∈ 𝓝ˢ[s'] s, ∃ t₂ ∈ 𝓝ˢ[t'] t, t₁ ×ˢ t₂ ⊆ n
⊢ ∃ u ∈ 𝓝ˢ[s'] s, ∃ v ∈ 𝓝ˢ[t'] t, u ×ˢ v ⊆ n

Tactic:
]

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s s' : Set X
hs : IsCompact s
t t' : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : ∃ t₁ ∈ 𝓝ˢ[s'] s, ∃ t₂ ∈ 𝓝ˢ[t'] t, t₁ ×ˢ t₂ ⊆ n
⊢ ∃ u ∈ 𝓝ˢ[s'] s, ∃ v ∈ 𝓝ˢ[t'] t, u ×ˢ v ⊆ n
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s s' : Set X
hs : IsCompact s
t : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : {a | ∀ b ∈ t, (a, b) ∈ n} ∈ 𝓝ˢ[s'] s
⊢ ∃ u ∈ 𝓝ˢ[s'] s, u ×ˢ t ⊆ n

Tactic:
]

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s s' : Set X
hs : IsCompact s
t : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : {a | ∀ b ∈ t, (a, b) ∈ n} ∈ 𝓝ˢ[s'] s
⊢ ∃ u ∈ 𝓝ˢ[s'] s, u ×ˢ t ⊆ n
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
hs : IsCompact s
t t' : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : ∃ t₁ ∈ 𝓟 s, ∃ t₂ ∈ 𝓝ˢ[t'] t, t₁ ×ˢ t₂ ⊆ n
⊢ ∃ u ∈ 𝓝ˢ[t'] t, s ×ˢ u ⊆ n

Tactic:
]

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
hs : IsCompact s
t t' : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : ∃ t₁ ∈ 𝓟 s, ∃ t₂ ∈ 𝓝ˢ[t'] t, t₁ ×ˢ t₂ ⊆ n
⊢ ∃ u ∈ 𝓝ˢ[t'] t, s ×ˢ u ⊆ n
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : x ∉ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}
h : x ∈ (interior {a | p a})ᶜ
⊢ x ∉ interior {a | p a}

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : x ∉ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}
h : x ∈ (interior {a | p a})ᶜ
⊢ x ∉ interior {a | p a}
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
tfae_2_to_3 : pure x ≤ 𝓝 y → ∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s
tfae_3_to_4 : (∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s) → ∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s
tfae_4_to_5 : (∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s) → y ∈ closure[inst✝] {x}
tfae_6_iff_5 : closure[inst✝] {y} ⊆ closure[inst✝] {x} ↔ y ∈ closure[inst✝] {x}
⊢ ClusterPt y (pure x) ↔ ClusterPt y (pure x)

Tactic:
]

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

Goal state before:
pp: X : Type u
Y : Type v
ι : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s t : Set X
f : X → Y
inst✝ : NoncompactSpace X
i✝ : Set X
hs : i✝ = univ
⊢ ¬IsCompact i✝

Tactic:
]

Goal state after:
X : Type u
Y : Type v
ι : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s t : Set X
f : X → Y
inst✝ : NoncompactSpace X
i✝ : Set X
hs : i✝ = univ
⊢ ¬IsCompact i✝
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
ι : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s t : Set X
f : X → Y
inst✝ : NoncompactSpace X
i✝ : Set X
hs : i✝ = univ
⊢ ¬IsCompact univ

Tactic:
]

Goal state after:
X : Type u
Y : Type v
ι : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s t : Set X
f : X → Y
inst✝ : NoncompactSpace X
i✝ : Set X
hs : i✝ = univ
⊢ ¬IsCompact univ
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s K : Set X
hs : s.Infinite
hK : IsCompact K
hsub : s ⊆ K
x : X
hx : x ∈ K ∧ ClusterPt x (cofinite ⊓ 𝓟 s)
⊢ x ∈ K ∧ ClusterPt x (cofinite ⊓ 𝓟 s)

Tactic:
]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s K : Set X
hs : s.Infinite
hK : IsCompact K
hsub : s ⊆ K
x : X
hx : x ∈ K ∧ ClusterPt x (cofinite ⊓ 𝓟 s)
⊢ x ∈ K ∧ ClusterPt x (cofinite ⊓ 𝓟 s)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
⊢ ∀ (i' : Set X), IsCompact i' → ∃ i, IsCompact i ∧ f ⁻¹' iᶜ ⊆ i'ᶜ

Tactic:
]

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
⊢ ∀ (i' : Set X), IsCompact i' → ∃ i, IsCompact i ∧ f ⁻¹' iᶜ ⊆ i'ᶜ
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
g : X → Y
f : Filter X
hg : Continuous[inst✝¹, inst✝] g
hf : Disjoint f (cocompact X)
⊢ f ⊓ comap g (cocompact Y) ≤ ⊥

Tactic:
]

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
g : X → Y
f : Filter X
hg : Continuous[inst✝¹, inst✝] g
hf : Disjoint f (cocompact X)
⊢ f ⊓ comap g (cocompact Y) ≤ ⊥
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
f : X → Y
s : Set X
h : pure x ≤ 𝓝 y
hf : ContinuousWithinAt f s y
hx : x ∈ s
⊢ pure (f x) ≤ 𝓝 (f y)

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
f : X → Y
s : Set X
h : pure x ≤ 𝓝 y
hf : ContinuousWithinAt f s y
hx : x ∈ s
⊢ pure (f x) ≤ 𝓝 (f y)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace X
f : X → Y
hf : Continuous[inst✝², inst✝¹] f
⊢ IsCompact (f '' univ)

Tactic:
]

Goal state after:
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace X
f : X → Y
hf : Continuous[inst✝², inst✝¹] f
⊢ IsCompact (f '' univ)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝², inst✝¹] f
inst✝ : CompactSpace X
hf' : Surjective f
⊢ IsCompact (range f)

Tactic:
]

Goal state after:
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝², inst✝¹] f
inst✝ : CompactSpace X
hf' : Surjective f
⊢ IsCompact (range f)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
hf' : IsClosed[inst✝] (range f)
K : Set Y
hK : IsCompact (K ∩ range f)
⊢ IsCompact (K ∩ range f)

Tactic:
]

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
hf' : IsClosed[inst✝] (range f)
K : Set Y
hK : IsCompact (K ∩ range f)
⊢ IsCompact (K ∩ range f)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
K : Set Y
Kf : K ⊆ range f
⊢ IsCompact K ↔ IsCompact K

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ (¬∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s) ↔ ∃ S, IsOpen[inst✝] S ∧ y ∈ S ∧ x ∉ S

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ (¬∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s) ↔ ∃ S, IsOpen[inst✝] S ∧ y ∈ S ∧ x ∉ S
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsCompact s ↔ IsCompact s

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ (¬∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s) ↔ ∃ S, IsClosed[inst✝] S ∧ x ∈ S ∧ y ∉ S

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ (¬∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s) ↔ ∃ S, IsClosed[inst✝] S ∧ x ∈ S ∧ y ∉ S
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s : Set X
f g : X → Y
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : IsOpen[inst✝²] s
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝², inst✝¹] g
hspec : ∀ (x : X), f x ⤳ g x
this : ∀ (U : Set Y), IsOpen[inst✝¹] U → g ⁻¹' U ⊆ f ⁻¹' U
⊢ ∀ (s_1 : Set Y), IsOpen[inst✝¹] s_1 → IsOpen[inst✝²] (s.piecewise f g ⁻¹' s_1)

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s : Set X
f g : X → Y
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : IsOpen[inst✝²] s
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝², inst✝¹] g
hspec : ∀ (x : X), f x ⤳ g x
this : ∀ (U : Set Y), IsOpen[inst✝¹] U → g ⁻¹' U ⊆ f ⁻¹' U
⊢ ∀ (s_1 : Set Y), IsOpen[inst✝¹] s_1 → IsOpen[inst✝²] (s.piecewise f g ⁻¹' s_1)
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s : Set X
f g : X → Y
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : IsOpen[inst✝²] s
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝², inst✝¹] g
hspec : ∀ (x : X), f x ⤳ g x
this : ∀ (U : Set Y), IsOpen[inst✝¹] U → g ⁻¹' U ⊆ f ⁻¹' U
U : Set Y
hU : IsOpen[inst✝¹] U
⊢ IsOpen[inst✝²] (f ⁻¹' U ∩ s ∪ g ⁻¹' U)

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s : Set X
f g : X → Y
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : IsOpen[inst✝²] s
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝², inst✝¹] g
hspec : ∀ (x : X), f x ⤳ g x
this : ∀ (U : Set Y), IsOpen[inst✝¹] U → g ⁻¹' U ⊆ f ⁻¹' U
U : Set Y
hU : IsOpen[inst✝¹] U
⊢ IsOpen[inst✝²] (f ⁻¹' U ∩ s ∪ g ⁻¹' U)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : CompactSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ IsCompact (range f)

Tactic:
]

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : CompactSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ IsCompact (range f)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x
⊢ ∀ (f : Ultrafilter (X × Y)), s ×ˢ t ∈ f → ∃ x ∈ s ×ˢ t, ↑f ≤ 𝓝 x

Tactic:
]

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x
⊢ ∀ (f : Ultrafilter (X × Y)), s ×ˢ t ∈ f → ∃ x ∈ s ×ˢ t, ↑f ≤ 𝓝 x
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ S, (∀ s ∈ S, IsClosed[inst✝] s) ∧ ⋃₀ S = sᶜ) → ∃ S, (∀ s ∈ S, IsOpen[inst✝] s) ∧ ⋂₀ S = s

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ S, (∀ s ∈ S, IsClosed[inst✝] s) ∧ ⋃₀ S = sᶜ) → ∃ S, (∀ s ∈ S, IsOpen[inst✝] s) ∧ ⋂₀ S = s
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
h : SpecializingMap f
x : X
⊢ IsClosed[inst✝] (closure[inst✝] {f x})

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
h : SpecializingMap f
x : X
⊢ IsClosed[inst✝] (closure[inst✝] {f x})
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case hpg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure[inst✝²] {a | p a})
hg : ContinuousOn g (s ∩ closure[inst✝²] {a | ¬p a})
a : α
has : a ∈ s
left✝ : a ∈ closure[inst✝²] {a | p a}
ha : a ∈ closure[inst✝²] {a | p a}ᶜ
⊢ Tendsto g (𝓝[s ∩ closure[inst✝²] {a | ¬p a}] a) (𝓝 (g a))

Tactic:
]

Goal state after:
case hpg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure[inst✝²] {a | p a})
hg : ContinuousOn g (s ∩ closure[inst✝²] {a | ¬p a})
a : α
has : a ∈ s
left✝ : a ∈ closure[inst✝²] {a | p a}
ha : a ∈ closure[inst✝²] {a | p a}ᶜ
⊢ Tendsto g (𝓝[s ∩ closure[inst✝²] {a | ¬p a}] a) (𝓝 (g a))
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
x : X
sx : x ∈ s
hx : ↑f ≤ comap Prod.fst (𝓝 x)
y : Y
ty : y ∈ t
hy : ↑f ≤ comap Prod.snd (𝓝 y)
⊢ ∃ x ∈ s ×ˢ t, ↑f ≤ 𝓝 x

Tactic:
]

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
x : X
sx : x ∈ s
hx : ↑f ≤ comap Prod.fst (𝓝 x)
y : Y
ty : y ∈ t
hy : ↑f ≤ comap Prod.snd (𝓝 y)
⊢ ∃ x ∈ s ×ˢ t, ↑f ≤ 𝓝 x
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen[inst✝] s
⊢ IsOpen[inst✝] s

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen[inst✝] s
⊢ IsOpen[inst✝] s
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ IsClosed univ

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ IsClosed univ
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x : X
⊢ map mk (comap mk (𝓝 (mk x))) = 𝓝 (mk x)

Tactic:
map_comap_of_surjective surjective_mk

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x : X
⊢ 𝓝 (mk x) = 𝓝 (mk x)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
x : X
sx : x ∈ s
hx : ↑f ≤ comap Prod.fst (𝓝 x)
y : Y
ty : y ∈ t
hy : ↑f ≤ comap Prod.snd (𝓝 y)
⊢ ↑f ≤ 𝓝 x ×ˢ 𝓝 y

Tactic:
]

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
x : X
sx : x ∈ s
hx : ↑f ≤ comap Prod.fst (𝓝 x)
y : Y
ty : y ∈ t
hy : ↑f ≤ comap Prod.snd (𝓝 y)
⊢ ↑f ≤ 𝓝 x ×ˢ 𝓝 y
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x : X
⊢ 𝓝 (mk x) = 𝓝 (mk x)

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ map mk (comap mk (𝓝ˢ (mk '' s))) = 𝓝ˢ (mk '' s)

Tactic:
map_comap_of_surjective surjective_mk

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ 𝓝ˢ (mk '' s) = 𝓝ˢ (mk '' s)
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ 𝓝ˢ (mk '' s) = 𝓝ˢ (mk '' s)

Tactic:
]

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

Goal state before:
pp: X : Type u
Y : Type v
ι : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
s t : Set X
f : X → Y
inst✝¹ : CompactSpace X
inst✝ : CompactSpace Y
⊢ IsCompact (univ ×ˢ univ)

Tactic:
]

Goal state after:
X : Type u
Y : Type v
ι : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
s t : Set X
f : X → Y
inst✝¹ : CompactSpace X
inst✝ : CompactSpace Y
⊢ IsCompact (univ ×ˢ univ)
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ frontier {x | p x}, Tendsto f (𝓝[{x | p x}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ frontier {x | p x}, Tendsto g (𝓝[{x | ¬p x}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f {x | p x}
hg : ContinuousOn g {x | ¬p x}
⊢ ContinuousOn (fun a ↦ if p a then f a else g a) univ

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ frontier {x | p x}, Tendsto f (𝓝[{x | p x}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ frontier {x | p x}, Tendsto g (𝓝[{x | ¬p x}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f {x | p x}
hg : ContinuousOn g {x | ¬p x}
⊢ ContinuousOn (fun a ↦ if p a then f a else g a) univ
Module: Mathlib.Topology.Compactness.Compact

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

Tactic:
]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
⊢ 𝓝 (mk x) ×ˢ 𝓝 (mk y) = 𝓝 (mk x) ×ˢ 𝓝 (mk y)

Tactic:
]

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

Goal state before:
pp: X✝ : Type u
Y : Type v
ι : Type u_1
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s t : Set X✝
f : X✝ → Y
X : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), CompactSpace (X i)
⊢ IsCompact (⋃ a, range (Sigma.mk a))

Tactic:
]

Goal state after:
X✝ : Type u
Y : Type v
ι : Type u_1
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s t : Set X✝
f : X✝ → Y
X : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), CompactSpace (X i)
⊢ IsCompact (⋃ a, range (Sigma.mk a))
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ι
t : (i : ι) → Set (X i)
hs : s.Finite
ht : ∀ i ∈ s, IsCompact (t i)
⊢ IsCompact (⋃ i ∈ s, Sigma.mk i '' t i)

Tactic:
]

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ι
t : (i : ι) → Set (X i)
hs : s.Finite
ht : ∀ i ∈ s, IsCompact (t i)
⊢ IsCompact (⋃ i ∈ s, Sigma.mk i '' t i)
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set (SeparationQuotient X)
x : X
⊢ 𝓝 (mk x) ⊓ 𝓟 s = 𝓝 (mk x) ⊓ 𝓟 s

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ frontier {x | p x}, f a = g a
hf : ContinuousOn f (closure[inst✝²] {x | p x})
hg : ContinuousOn g (closure[inst✝²] {x | ¬p x})
⊢ ContinuousOn (fun a ↦ if p a then f a else g a) univ

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ frontier {x | p x}, f a = g a
hf : ContinuousOn f (closure[inst✝²] {x | p x})
hg : ContinuousOn g (closure[inst✝²] {x | ¬p x})
⊢ ContinuousOn (fun a ↦ if p a then f a else g a) univ
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y → α
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
x : X
y : Y
l : Filter α
⊢ Tendsto (uncurry (lift₂ f hf) ∘ Prod.map mk mk) (𝓝 (x, y)) l ↔ Tendsto (uncurry f) (𝓝 (x, y)) l

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y → α
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
x : X
y : Y
l : Filter α
⊢ Tendsto (uncurry (lift₂ f hf) ∘ Prod.map mk mk) (𝓝 (x, y)) l ↔ Tendsto (uncurry f) (𝓝 (x, y)) l
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y → α
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
x : X
y : Y
l : Filter α
⊢ Tendsto (uncurry (lift₂ f hf)) (𝓝 (mk x, mk y)) l ↔ Tendsto (uncurry f) (𝓝 (x, y)) l

Tactic:
rw [← map_prod_map_mk_nhds, tendsto_map'_iff]

Goal state after:
X : Type u_1
Y : Type u_2
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y → α
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
x : X
y : Y
l : Filter α
⊢ Tendsto (uncurry (lift₂ f hf) ∘ Prod.map mk mk) (𝓝 (x, y)) l ↔ Tendsto (uncurry f) (𝓝 (x, y)) l