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

Goal state before:
pp: case mpr
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
H : ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})
s : Set Y
⊢ comap f (𝓝ˢ (⋃ x ∈ s, {x})) ≤ 𝓝ˢ (f ⁻¹' ⋃ x ∈ s, {x})

Tactic:
[

Goal state after:
case mpr
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
H : ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})
s : Set Y
⊢ comap f (𝓝ˢ (⋃ x ∈ s, {x})) ≤ 𝓝ˢ (f ⁻¹' ⋃ x ∈ s, {x})
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f_closed : IsClosedMap f
f_cont : Continuous[inst✝¹, inst✝] f
F : Filter X
⊢ (map f F).lift' closure[inst✝] = map f (F.lift' closure[inst✝¹])

Tactic:
rw [map_lift'_eq2 (monotone_closure Y), map_lift'_eq (monotone_closure X)]

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f_closed : IsClosedMap f
f_cont : Continuous[inst✝¹, inst✝] f
F : Filter X
⊢ F.lift' (closure[inst✝] ∘ image f) = F.lift' (image f ∘ closure[inst✝¹])
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hg : IsOpenEmbedding g
⊢ IsOpenMap f ↔ IsOpenMap (g ∘ f)

Tactic:
[

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hg : IsOpenEmbedding g
⊢ IsOpenMap f ↔ IsOpenMap (g ∘ f)
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hg : IsClosedEmbedding g
⊢ IsClosedEmbedding (g ∘ f) ↔ IsClosedEmbedding f

Tactic:
[

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hg : IsClosedEmbedding g
⊢ IsClosedEmbedding (g ∘ f) ↔ IsClosedEmbedding f
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
x : α
⊢ t ∈ 𝓝[s] x ↔ s =ᶠ[𝓝 x] s ∩ t

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
x : α
⊢ t ∈ 𝓝[s] x ↔ s =ᶠ[𝓝 x] s ∩ t
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u_5
Y : Type u_6
s : Set (Set X)
t : Set (Set Y)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (X × Y) := generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) s t)
u : Set X
hu : u ∈ s
⊢ ⋃ v ∈ t, u ×ˢ v = Prod.fst ⁻¹' u

Tactic:
[

Goal state after:
X : Type u_5
Y : Type u_6
s : Set (Set X)
t : Set (Set Y)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (X × Y) := generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) s t)
u : Set X
hu : u ∈ s
⊢ ⋃ v ∈ t, u ×ˢ v = Prod.fst ⁻¹' u
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u_5
Y : Type u_6
s : Set (Set X)
t : Set (Set Y)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (X × Y) := generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) s t)
v : Set Y
hv : v ∈ t
⊢ ⋃ u ∈ s, u ×ˢ v = Prod.snd ⁻¹' v

Tactic:
[

Goal state after:
X : Type u_5
Y : Type u_6
s : Set (Set X)
t : Set (Set Y)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (X × Y) := generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) s t)
v : Set Y
hv : v ∈ t
⊢ ⋃ u ∈ s, u ×ˢ v = Prod.snd ⁻¹' v
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set (X × Y)
⊢ (∀ x ∈ s, s ∈ 𝓝 x) ↔
    ∀ (a : X) (b : Y), (a, b) ∈ s → ∃ u v, IsOpen[inst✝¹] u ∧ IsOpen[inst✝] v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ s

Tactic:
[

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set (X × Y)
⊢ (∀ x ∈ s, s ∈ 𝓝 x) ↔
    ∀ (a : X) (b : Y), (a, b) ∈ s → ∃ u v, IsOpen[inst✝¹] u ∧ IsOpen[inst✝] v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ s
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: Y : Type v
W : Type u_1
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace W
X : Type u_5
Z : Type u_6
f : X → Y
g : Z → W
⊢ induced Prod.fst (induced f inst✝¹) ⊓ induced Prod.snd (induced g inst✝) =
    induced (fun p ↦ (f p.1, g p.2)) (induced Prod.fst inst✝¹ ⊓ induced Prod.snd inst✝)

Tactic:
[

Goal state after:
Y : Type v
W : Type u_1
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace W
X : Type u_5
Z : Type u_6
f : X → Y
g : Z → W
⊢ induced Prod.fst (induced f inst✝¹) ⊓ induced Prod.snd (induced g inst✝) =
    induced (fun p ↦ (f p.1, g p.2)) (induced Prod.fst inst✝¹ ⊓ induced Prod.snd inst✝)
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
S : Set X
x : ↑S
⊢ 𝓝[≠] x = ⊥ ↔ 𝓝[(S ↓∩ {↑x})ᶜ] x = ⊥

Tactic:
← image_singleton,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
S : Set X
x : ↑S
⊢ 𝓝[≠] x = ⊥ ↔ 𝓝[(S ↓∩ ↑{x})ᶜ] x = ⊥
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
f : β → α
a : α
s : Set α
l : Filter β
h : Tendsto f l (𝓝[s] a)
⊢ ∀ᶠ (i : β) in l, f i ∈ s

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
f : β → α
a : α
s : Set α
l : Filter β
h : Tendsto f l (𝓝[s] a)
⊢ ∀ᶠ (i : β) in l, f i ∈ s
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
s : Set (CofiniteTopology X)
⊢ IsOpen s ↔ s.Nonempty → sᶜ.Finite

Tactic:
[

Goal state after:
X : Type u
s : Set (CofiniteTopology X)
⊢ IsOpen s ↔ s.Nonempty → sᶜ.Finite
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
x : CofiniteTopology X
U : Set (CofiniteTopology X)
⊢ U ∈ 𝓝 x ↔ U ∈ pure x ⊔ cofinite

Tactic:
[

Goal state after:
X : Type u
x : CofiniteTopology X
U : Set (CofiniteTopology X)
⊢ U ∈ 𝓝 x ↔ U ∈ pure x ⊔ cofinite
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
x✝ : X × Y
a : X
b : Y
⊢ (a, b) ∈ closure[instTopologicalSpaceProd] (s ×ˢ t) ↔ (a, b) ∈ closure[inst✝¹] s ×ˢ closure[inst✝] t

Tactic:
[

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
x✝ : X × Y
a : X
b : Y
⊢ (a, b) ∈ closure[instTopologicalSpaceProd] (s ×ˢ t) ↔ (a, b) ∈ closure[inst✝¹] s ×ˢ closure[inst✝] t
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
x✝ : X × Y
a : X
b : Y
⊢ (a, b) ∈ interior (s ×ˢ t) ↔ (a, b) ∈ interior s ×ˢ interior t

Tactic:
by simp only [mem_interior_iff_mem_nhds, mem_prod, prod_mem_nhds_iff]

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

Goal state before:
pp: X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : IsInducing f
hg : IsInducing g
x✝ : X × Z
x : X
z : Z
⊢ 𝓝 (x, z) = comap (Prod.map f g) (𝓝 (Prod.map f g (x, z)))

Tactic:
[

Goal state after:
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : IsInducing f
hg : IsInducing g
x✝ : X × Z
x : X
z : Z
⊢ 𝓝 (x, z) = comap (Prod.map f g) (𝓝 (Prod.map f g (x, z)))
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
x : X
f : Y → Z
⊢ (IsInducing fun x' ↦ (x, f x')) ↔ IsInducing f

Tactic:
[

Goal state after:
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
x : X
f : Y → Z
⊢ (IsInducing fun x' ↦ (x, f x')) ↔ IsInducing f
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s u : Set α
this : TopologicalSpace α := TopologicalSpace.induced f t
⊢ u ∈ 𝓝ˢ s ↔ ∃ v ∈ 𝓝ˢ (f '' s), f ⁻¹' v ⊆ u

Tactic:
[

Goal state after:
α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s u : Set α
this : TopologicalSpace α := TopologicalSpace.induced f t
⊢ u ∈ 𝓝ˢ s ↔ ∃ v ∈ 𝓝ˢ (f '' s), f ⁻¹' v ⊆ u
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
y : Y
f : X → Z
⊢ (IsInducing fun x ↦ (f x, y)) ↔ IsInducing f

Tactic:
[

Goal state after:
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
y : Y
f : X → Z
⊢ (IsInducing fun x ↦ (f x, y)) ↔ IsInducing f
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
β : Type u_5
T : Set (Set β)
f : α → β
x : α
x✝ : x ∈ s
⊢ ContinuousWithinAt f s x ↔ ∀ t ∈ T, f x ∈ t → f ⁻¹' t ∈ 𝓝[s] x

Tactic:
delta ContinuousWithinAt

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
β : Type u_5
T : Set (Set β)
f : α → β
x : α
x✝ : x ∈ s
⊢ Tendsto f (𝓝[s] x) (𝓝 (f x)) ↔ ∀ t ∈ T, f x ∈ t → f ⁻¹' t ∈ 𝓝[s] x
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hs : ∀ (a : X), f a ∈ s
⊢ Continuous[inst✝¹, instTopologicalSpaceSubtype] (codRestrict f s hs) → Continuous[inst✝¹, inst✝] f

Tactic:
[

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hs : ∀ (a : X), f a ∈ s
⊢ Continuous[inst✝¹, instTopologicalSpaceSubtype] (codRestrict f s hs) → Continuous[inst✝¹, inst✝] f
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ ContinuousWithinAt f s (x.1, x.2) ↔ ContinuousWithinAt (fun x_1 ↦ f (x.1, x_1)) {b | (x.1, b) ∈ s} x.2

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ ContinuousWithinAt f s (x.1, x.2) ↔ ContinuousWithinAt (fun x_1 ↦ f (x.1, x_1)) {b | (x.1, b) ∈ s} x.2
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ ContinuousWithinAt f s (x.1, x.2) ↔ ContinuousWithinAt (fun x_1 ↦ f (x_1, x.2)) {a | (a, x.2) ∈ s} x.1

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ ContinuousWithinAt f s (x.1, x.2) ↔ ContinuousWithinAt (fun x_1 ↦ f (x_1, x.2)) {a | (a, x.2) ∈ s} x.1
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
x : α × β
⊢ ContinuousAt f x ↔ ContinuousAt (fun x_1 ↦ f (x.1, x_1)) x.2

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
x : α × β
⊢ ContinuousAt f x ↔ ContinuousAt (fun x_1 ↦ f (x.1, x_1)) x.2
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
x : α × β
⊢ ContinuousAt f x ↔ ContinuousAt (fun x_1 ↦ f (x_1, x.2)) x.1

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
x : α × β
⊢ ContinuousAt f x ↔ ContinuousAt (fun x_1 ↦ f (x_1, x.2)) x.1
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
s : Set (α × β)
⊢ ContinuousOn f s ↔ ∀ (a : α), ContinuousOn (fun x ↦ f (a, x)) {b | (a, b) ∈ s}

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
s : Set (α × β)
⊢ ContinuousOn f s ↔ ∀ (a : α), ContinuousOn (fun x ↦ f (a, x)) {b | (a, b) ∈ s}
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
s : Set (α × β)
⊢ ContinuousOn f s ↔ ∀ (b : β), ContinuousOn (fun x ↦ f (x, b)) {a | (a, b) ∈ s}

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
s : Set (α × β)
⊢ ContinuousOn f s ↔ ∀ (b : β), ContinuousOn (fun x ↦ f (x, b)) {a | (a, b) ∈ s}
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
s : Set (α × β)
⊢ ContinuousOn f s ↔ ∀ (b : β), ContinuousOn (fun x ↦ f (x, b)) {a | (a, b) ∈ s}

Tactic:
simp_rw [ContinuousOn, Prod.forall, continuousWithinAt_prod_of_discrete_right]; apply forall_comm

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] f ↔ ∀ (a : α), Continuous[inst✝², inst✝¹] fun x ↦ f (a, x)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] f ↔ ∀ (a : α), Continuous[inst✝², inst✝¹] fun x ↦ f (a, x)
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] f ↔ ∀ (b : β), Continuous[inst✝³, inst✝¹] fun x ↦ f (x, b)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] f ↔ ∀ (b : β), Continuous[inst✝³, inst✝¹] fun x ↦ f (x, b)
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
⊢ IsOpenMap f ↔ ∀ (a : α), IsOpenMap fun x ↦ f (a, x)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
⊢ IsOpenMap f ↔ ∀ (a : α), IsOpenMap fun x ↦ f (a, x)
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
⊢ IsOpenMap f ↔ ∀ (b : β), IsOpenMap fun x ↦ f (x, b)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
⊢ IsOpenMap f ↔ ∀ (b : β), IsOpenMap fun x ↦ f (x, b)
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
𝔖 : Set (Set ι)
⊢ induced (⋃₀ 𝔖).domRestrict topologicalSpace = ⨅ S ∈ 𝔖, induced S.domRestrict topologicalSpace

Tactic:
[

Goal state after:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
𝔖 : Set (Set ι)
⊢ induced (⋃₀ 𝔖).domRestrict topologicalSpace = ⨅ S ∈ 𝔖, induced S.domRestrict topologicalSpace
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
⊢ IsEmbedding (Sum.elim f g) ↔
    IsEmbedding f ∧
      IsEmbedding g ∧ Disjoint (closure[inst✝] (range f)) (range g) ∧ Disjoint (range f) (closure[inst✝] (range g))

Tactic:
[

Goal state after:
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
⊢ IsEmbedding (Sum.elim f g) ↔
    IsEmbedding f ∧
      IsEmbedding g ∧ Disjoint (closure[inst✝] (range f)) (range g) ∧ Disjoint (range f) (closure[inst✝] (range g))
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : β → γ
hg : IsInducing g
s : Set α
x : α
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (g ∘ f) s x

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : β → γ
hg : IsInducing g
s : Set α
x : α
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (g ∘ f) s x
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : β → γ
hg : IsInducing g
s : Set α
⊢ ContinuousOn f s ↔ ContinuousOn (g ∘ f) s

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : β → γ
hg : IsInducing g
s : Set α
⊢ ContinuousOn f s ↔ ContinuousOn (g ∘ f) s
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
⊢ (∀ x ∈ s, 𝓝 x ≤ 𝓟 s) ↔ ∀ f ∈ s, ∃ I u, (∀ a ∈ I, IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ (↑I).pi u ⊆ s

Tactic:
[

Goal state after:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
⊢ (∀ x ∈ s, 𝓝 x ≤ 𝓟 s) ↔ ∀ f ∈ s, ∃ I u, (∀ a ∈ I, IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ (↑I).pi u ⊆ s
Module: Mathlib.Topology.Bases

Goal state before:
pp: case inr
α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
h✝ : Nonempty α
s : Set β
s_cnt : s.Countable
s_dense : Dense s
⊢ Dense (invFun f '' s)

Tactic:
[

Goal state after:
case inr
α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
h✝ : Nonempty α
s : Set β
s_cnt : s.Countable
s_dense : Dense s
⊢ Dense (invFun f '' s)
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case refine_1.refine_1
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (i : ι) → Set (A i)
h1 : ∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1
h2 : (↑I).pi t ⊆ s
i : ι
hi : i ∈ I
⊢ IsOpen[T i] (eval i '' (↑I).pi fun a_1 ↦ ⋯.choose) ∧ a i ∈ eval i '' (↑I).pi fun a_1 ↦ ⋯.choose

Tactic:
[

Goal state after:
case refine_1.refine_1
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (i : ι) → Set (A i)
h1 : ∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1
h2 : (↑I).pi t ⊆ s
i : ι
hi : i ∈ I
⊢ IsOpen[T i] (eval i '' (↑I).pi fun a_1 ↦ ⋯.choose) ∧ a i ∈ eval i '' (↑I).pi fun a_1 ↦ ⋯.choose
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: β : Type u_2
s : ℕ → Set β
n : ℕ
⊢ accumulate s n = ⋃ k, ⋃ (_ : k < n + 1), s k

Tactic:
[

Goal state after:
β : Type u_2
s : ℕ → Set β
n : ℕ
⊢ accumulate s n = ⋃ k, ⋃ (_ : k < n + 1), s k
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : LE α
x : α
z : β
⊢ z ∈ accumulate s x ↔ ∃ y ≤ x, z ∈ s y

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : LE α
x : α
z : β
⊢ z ∈ accumulate s x ↔ ∃ y ≤ x, z ∈ s y
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case h
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I).pi t ⊆ s
i : ι
hi : i ∈ I
⊢ (t i ⊆ if i ∈ I then t i else univ) ∧ IsOpen[T i] (t i) ∧ a i ∈ t i

Tactic:
[

Goal state after:
case h
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I).pi t ⊆ s
i : ι
hi : i ∈ I
⊢ (t i ⊆ if i ∈ I then t i else univ) ∧ IsOpen[T i] (t i) ∧ a i ∈ t i
Module: Mathlib.Topology.Bornology.Basic

Goal state before:
pp: α : Type u_2
x✝ : Bornology α
x : α
⊢ IsBounded {x}

Tactic:
isBounded_def

Goal state after:
α : Type u_2
x✝ : Bornology α
x : α
⊢ {x}ᶜ ∈ cobounded α
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case h
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I).pi t ⊆ s
i : ι
hi : i ∉ I
⊢ (univ ⊆ if i ∈ I then t i else univ) ∧ IsOpen[T i] univ ∧ a i ∈ univ

Tactic:
[

Goal state after:
case h
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I).pi t ⊆ s
i : ι
hi : i ∉ I
⊢ (univ ⊆ if i ∈ I then t i else univ) ∧ IsOpen[T i] univ ∧ a i ∈ univ
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 β
s : Set α
hsc : s.Countable
hsd : Dense s
t : Set β
htc : t.Countable
htd : Dense t
⊢ Dense (Sum.inl '' s ∪ Sum.inr '' t)

Tactic:
[

Goal state after:
α : Type u
β : Type u_1
t✝ : TopologicalSpace α
B : Set (Set α)
s✝ : Set α
inst✝² : TopologicalSpace β
inst✝¹ : SeparableSpace α
inst✝ : SeparableSpace β
s : Set α
hsc : s.Countable
hsd : Dense s
t : Set β
htc : t.Countable
htd : Dense t
⊢ Dense (Sum.inl '' s ∪ Sum.inr '' t)