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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
s : Set α
x : α
inst✝ : TopologicalSpace β
⊢ (∀ (i : Set β), IsOpen[inst✝] i ∧ f x ⊆ i → ∀ᶠ (x' : α) in 𝓝[s] x, i ∈ 𝓝ˢ (f x')) ↔
    ∀ (i : Set β), IsOpen[inst✝] i ∧ f x ⊆ i → f ⁻¹' Iic i ∈ 𝓝[s] x

pp: case h₂
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
s : Set α
x : α
inst✝ : TopologicalSpace β
⊢ ∀ ⦃s_1 t : Set β⦄, s_1 ⊆ t → f ⁻¹' Iic s_1 ∈ 𝓝[s] x → f ⁻¹' Iic t ∈ 𝓝[s] x

pp: case h₁
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
s : Set α
x : α
inst✝ : TopologicalSpace β
⊢ ∀ ⦃s_1 t : Set β⦄, s_1 ⊆ t → (∀ᶠ (x' : α) in 𝓝[s] x, s_1 ∈ 𝓝ˢ (f x')) → ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (f x')

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
s : Set α
x : α
inst✝ : TopologicalSpace β
⊢ (∀ (i : Set β), IsOpen[inst✝] i ∧ f x ⊆ i → ∀ᶠ (x' : α) in 𝓝[s] x, i ∈ 𝓝ˢ (f x')) ↔
    ∀ (i : Set β), IsOpen[inst✝] i ∧ f x ⊆ i → f ⁻¹' Iic i ∈ 𝓝[s] x

case h₂
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
s : Set α
x : α
inst✝ : TopologicalSpace β
⊢ ∀ ⦃s_1 t : Set β⦄, s_1 ⊆ t → f ⁻¹' Iic s_1 ∈ 𝓝[s] x → f ⁻¹' Iic t ∈ 𝓝[s] x

case h₁
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
s : Set α
x : α
inst✝ : TopologicalSpace β
⊢ ∀ ⦃s_1 t : Set β⦄, s_1 ⊆ t → (∀ᶠ (x' : α) in 𝓝[s] x, s_1 ∈ 𝓝ˢ (f x')) → ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (f x')
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
inst✝ : TopologicalSpace β
⊢ UpperHemicontinuous f ↔ ∀ (u : Set β), IsClosed[inst✝] u → IsClosed[inst✝¹] (f ⁻¹' Iic uᶜ)ᶜ

Tactic:
conv_rhs =>
    rw [compl_surjective.forall]
    simp [← isOpen_compl_iff]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
inst✝ : TopologicalSpace β
⊢ UpperHemicontinuous f ↔ ∀ (x : Set β), IsOpen[inst✝] x → IsOpen[inst✝¹] (f ⁻¹' Iic x)
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
⊢ (∀ {u : Set α}, IsOpen[inst✝¹] u → IsOpen[inst✝] (kernImage f u)) ↔
    ∀ (u : Set α), IsOpen[inst✝¹] u → IsOpen[inst✝] ((fun x ↦ f ⁻¹' {x}) ⁻¹' Iic u)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
⊢ (∀ {u : Set α}, IsOpen[inst✝¹] u → IsOpen[inst✝] (kernImage f u)) ↔
    ∀ (u : Set α), IsOpen[inst✝¹] u → IsOpen[inst✝] ((fun x ↦ f ⁻¹' {x}) ⁻¹' Iic u)
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
inst✝ : TopologicalSpace β
⊢ LowerHemicontinuous f ↔ ∀ (u : Set β), IsClosed[inst✝] u → IsClosed[inst✝¹] (f ⁻¹' Iic u)

Tactic:
conv_rhs =>
    rw [compl_surjective.forall]
    simp [← isOpen_compl_iff]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
inst✝ : TopologicalSpace β
⊢ LowerHemicontinuous f ↔ ∀ (x : Set β), IsOpen[inst✝] x → IsOpen[inst✝¹] (f ⁻¹' Iic xᶜ)ᶜ
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
⊢ (∀ {u : Set α}, IsClosed[inst✝¹] u → IsClosed[inst✝] (kernImage f u)) ↔
    ∀ (u : Set α), IsClosed[inst✝¹] u → IsClosed[inst✝] ((fun x ↦ f ⁻¹' {x}) ⁻¹' Iic u)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
⊢ (∀ {u : Set α}, IsClosed[inst✝¹] u → IsClosed[inst✝] (kernImage f u)) ↔
    ∀ (u : Set α), IsClosed[inst✝¹] u → IsClosed[inst✝] ((fun x ↦ f ⁻¹' {x}) ⁻¹' Iic u)
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
s : Set α
x : α
hf : ∀ t ∈ 𝓝ˢ (f x), ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (f x')
hg : ∀ t ∈ 𝓝ˢ (g x), ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (g x')
⊢ ∀ t ∈ 𝓝ˢ (f x ∪ g x), ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (f x' ∪ g x')

Tactic:
]

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
s : Set α
x : α
hf : ∀ t ∈ 𝓝ˢ (f x), ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (f x')
hg : ∀ t ∈ 𝓝ˢ (g x), ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (g x')
⊢ ∀ t ∈ 𝓝ˢ (f x ∪ g x), ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (f x' ∪ g x')
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
s : Set α
hf : ∀ x ∈ s, UpperHemicontinuousWithinAt f s x
hg : ∀ x ∈ s, UpperHemicontinuousWithinAt g s x
⊢ ∀ x ∈ s, UpperHemicontinuousWithinAt (fun x ↦ f x ∪ g x) s x

Tactic:
]

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
s : Set α
hf : ∀ x ∈ s, UpperHemicontinuousWithinAt f s x
hg : ∀ x ∈ s, UpperHemicontinuousWithinAt g s x
⊢ ∀ x ∈ s, UpperHemicontinuousWithinAt (fun x ↦ f x ∪ g x) s x
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
x : α
hf : UpperHemicontinuousWithinAt f univ x
hg : UpperHemicontinuousWithinAt g univ x
⊢ UpperHemicontinuousWithinAt (fun x ↦ f x ∪ g x) univ x

Tactic:
]

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
x : α
hf : UpperHemicontinuousWithinAt f univ x
hg : UpperHemicontinuousWithinAt g univ x
⊢ UpperHemicontinuousWithinAt (fun x ↦ f x ∪ g x) univ x
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
hf : ∀ (x : α), UpperHemicontinuousAt f x
hg : ∀ (x : α), UpperHemicontinuousAt g x
⊢ ∀ (x : α), UpperHemicontinuousAt (fun x ↦ f x ∪ g x) x

Tactic:
]

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
hf : ∀ (x : α), UpperHemicontinuousAt f x
hg : ∀ (x : α), UpperHemicontinuousAt g x
⊢ ∀ (x : α), UpperHemicontinuousAt (fun x ↦ f x ∪ g x) x
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
s : Set α
x : α
hf : ∀ (u : Set β), IsOpen[inst✝] u → f x ⊆ u → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ u
u : Set β
hu : IsClosed[inst✝] u
⊢ ∀ (u_1 : Set β), IsOpen[inst✝] u_1 → f x ∩ u ⊆ u_1 → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ∩ u ⊆ u_1

Tactic:
]

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
s : Set α
x : α
hf : ∀ (u : Set β), IsOpen[inst✝] u → f x ⊆ u → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ u
u : Set β
hu : IsClosed[inst✝] u
⊢ ∀ (u_1 : Set β), IsOpen[inst✝] u_1 → f x ∩ u ⊆ u_1 → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ∩ u ⊆ u_1
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
s : Set α
hf : ∀ x ∈ s, UpperHemicontinuousWithinAt f s x
u : Set β
hu : IsClosed[inst✝] u
⊢ ∀ x ∈ s, UpperHemicontinuousWithinAt (fun x ↦ f x ∩ u) s x

Tactic:
]

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
s : Set α
hf : ∀ x ∈ s, UpperHemicontinuousWithinAt f s x
u : Set β
hu : IsClosed[inst✝] u
⊢ ∀ x ∈ s, UpperHemicontinuousWithinAt (fun x ↦ f x ∩ u) s x
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x : α
hf : UpperHemicontinuousWithinAt f univ x
u : Set β
hu : IsClosed[inst✝] u
⊢ UpperHemicontinuousWithinAt (fun x ↦ f x ∩ u) univ x

Tactic:
]

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x : α
hf : UpperHemicontinuousWithinAt f univ x
u : Set β
hu : IsClosed[inst✝] u
⊢ UpperHemicontinuousWithinAt (fun x ↦ f x ∩ u) univ x
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
hf : ∀ (x : α), UpperHemicontinuousAt f x
u : Set β
hu : IsClosed[inst✝] u
⊢ ∀ (x : α), UpperHemicontinuousAt (fun x ↦ f x ∩ u) x

Tactic:
]

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
hf : ∀ (x : α), UpperHemicontinuousAt f x
u : Set β
hu : IsClosed[inst✝] u
⊢ ∀ (x : α), UpperHemicontinuousAt (fun x ↦ f x ∩ u) x
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
s : Set α
γ : Type u_5
inst✝ : TopologicalSpace γ
i : γ → β
hf : ∀ x ∈ s, UpperHemicontinuousWithinAt f s x
hi : IsInducing i
h_cl : IsClosed[inst✝¹] (range i)
⊢ ∀ x ∈ s, UpperHemicontinuousWithinAt (fun x ↦ i ⁻¹' f x) s x

Tactic:
]

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
s : Set α
γ : Type u_5
inst✝ : TopologicalSpace γ
i : γ → β
hf : ∀ x ∈ s, UpperHemicontinuousWithinAt f s x
hi : IsInducing i
h_cl : IsClosed[inst✝¹] (range i)
⊢ ∀ x ∈ s, UpperHemicontinuousWithinAt (fun x ↦ i ⁻¹' f x) s x
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
γ : Type u_5
inst✝ : TopologicalSpace γ
i : γ → β
hf : ∀ (x : α), UpperHemicontinuousAt f x
hi : IsInducing i
h_cl : IsClosed[inst✝¹] (range i)
⊢ ∀ (x : α), UpperHemicontinuousAt (fun x ↦ i ⁻¹' f x) x

Tactic:
]

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
γ : Type u_5
inst✝ : TopologicalSpace γ
i : γ → β
hf : ∀ (x : α), UpperHemicontinuousAt f x
hi : IsInducing i
h_cl : IsClosed[inst✝¹] (range i)
⊢ ∀ (x : α), UpperHemicontinuousAt (fun x ↦ i ⁻¹' f x) x
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ IsClopen (𝒫 ∅)

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ IsClopen (𝒫 ∅)
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
⊢ ∀ ⦃x : Set (Set α)⦄,
    x ∈ {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝] U} →
      IsOpen[generateFrom
            (powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V})]
        {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty}

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
⊢ ∀ ⦃x : Set (Set α)⦄,
    x ∈ {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝] U} →
      IsOpen[generateFrom
            (powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V})]
        {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty}
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
⊢ ∀ ⦃x : Set (Set (Set α))⦄,
    x ∈
        {f |
          f.Finite ∧
            f ⊆ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}} →
      ∀ x_1 ∈ ⋂₀ x,
        ∃ v ∈ (fun u ↦ {s | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}) '' {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝] U},
          x_1 ∈ v ∧ v ⊆ ⋂₀ x

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
⊢ ∀ ⦃x : Set (Set (Set α))⦄,
    x ∈
        {f |
          f.Finite ∧
            f ⊆ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}} →
      ∀ x_1 ∈ ⋂₀ x,
        ∃ v ∈ (fun u ↦ {s | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}) '' {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝] U},
          x_1 ∈ v ∧ v ⊆ ⋂₀ x
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
t : Set (Set (Set α))
ht₁ : t.Finite
ht₂ : t ⊆ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}
s : Set α
hs : s ∈ ⋂₀ t
⊢ ∃ x ∈ {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝] U},
    s ∈ {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ∧ {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ⊆ ⋂₀ t

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
t : Set (Set (Set α))
ht₁ : t.Finite
ht₂ : t ⊆ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}
s : Set α
hs : s ∈ ⋂₀ t
⊢ ∃ x ∈ {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝] U},
    s ∈ {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ∧ {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ⊆ ⋂₀ t
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
t : Set (Set (Set α))
ht₁ : t.Finite
ht₂ : t ∩ powerset '' {U | IsOpen[inst✝] U} ∪ t ∩ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V} = t
s : Set α
hs : s ∈ ⋂₀ t
h✝ : s.Nonempty
⊢ ∃ u v,
    u ⊆ powerset '' {U | IsOpen[inst✝] U} ∧ v ⊆ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {U | IsOpen[inst✝] U} ∧ u ∪ v = t

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
t : Set (Set (Set α))
ht₁ : t.Finite
ht₂ : t ∩ powerset '' {U | IsOpen[inst✝] U} ∪ t ∩ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V} = t
s : Set α
hs : s ∈ ⋂₀ t
h✝ : s.Nonempty
⊢ ∃ u v,
    u ⊆ powerset '' {U | IsOpen[inst✝] U} ∧ v ⊆ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {U | IsOpen[inst✝] U} ∧ u ∪ v = t
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2.inr
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h✝ : s.Nonempty
u v : Set (Set (Set α))
hu : u ⊆ powerset '' {U | IsOpen[inst✝] U}
hv : v ⊆ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {U | IsOpen[inst✝] U}
ht₁ : u.Finite ∧ v.Finite
ht₂ : u ∪ v ⊆ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}
hs : s ∈ ⋂₀ (u ∪ v)
⊢ ∃ x ∈ {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝] U},
    s ∈ {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ∧ {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ⊆ ⋂₀ (u ∪ v)

Tactic:
]

Goal state after:
case refine_2.inr
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h✝ : s.Nonempty
u v : Set (Set (Set α))
hu : u ⊆ powerset '' {U | IsOpen[inst✝] U}
hv : v ⊆ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {U | IsOpen[inst✝] U}
ht₁ : u.Finite ∧ v.Finite
ht₂ : u ∪ v ⊆ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}
hs : s ∈ ⋂₀ (u ∪ v)
⊢ ∃ x ∈ {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝] U},
    s ∈ {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ∧ {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ⊆ ⋂₀ (u ∪ v)
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
x₀ : α
inst✝ : (𝓝 x₀).IsCountablyGenerated
h : ∀ (x : ℕ → α), Tendsto x atTop (𝓝 x₀) → ∀ y₀ ∈ f x₀, ∃ y, (∀ (n : ℕ), y n ∈ f (x n)) ∧ Tendsto y atTop (𝓝 y₀)
⊢ ∀ (u : Set β), IsOpen[inst✝¹] u → (f x₀ ∩ u).Nonempty → ∀ᶠ (x' : α) in 𝓝 x₀, (f x' ∩ u).Nonempty

Tactic:
]

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
x₀ : α
inst✝ : (𝓝 x₀).IsCountablyGenerated
h : ∀ (x : ℕ → α), Tendsto x atTop (𝓝 x₀) → ∀ y₀ ∈ f x₀, ∃ y, (∀ (n : ℕ), y n ∈ f (x n)) ∧ Tendsto y atTop (𝓝 y₀)
⊢ ∀ (u : Set β), IsOpen[inst✝¹] u → (f x₀ ∩ u).Nonempty → ∀ᶠ (x' : α) in 𝓝 x₀, (f x' ∩ u).Nonempty
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
x₀ : α
inst✝ : (𝓝 x₀).IsCountablyGenerated
h : ∀ (x : ℕ → α), Tendsto x atTop (𝓝 x₀) → ∀ y₀ ∈ f x₀, ∃ y, (∀ (n : ℕ), y n ∈ f (x n)) ∧ Tendsto y atTop (𝓝 y₀)
U : Set β
hU : IsOpen[inst✝¹] U
y₀ : β
hy₀f : y₀ ∈ f x₀
hy₀U : y₀ ∈ U
hc : ∃ᶠ (x : α) in 𝓝 x₀, ¬(f x ∩ U).Nonempty
⊢ False

Tactic:
]

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
x₀ : α
inst✝ : (𝓝 x₀).IsCountablyGenerated
h : ∀ (x : ℕ → α), Tendsto x atTop (𝓝 x₀) → ∀ y₀ ∈ f x₀, ∃ y, (∀ (n : ℕ), y n ∈ f (x n)) ∧ Tendsto y atTop (𝓝 y₀)
U : Set β
hU : IsOpen[inst✝¹] U
y₀ : β
hy₀f : y₀ ∈ f x₀
hy₀U : y₀ ∈ U
hc : ∃ᶠ (x : α) in 𝓝 x₀, ¬(f x ∩ U).Nonempty
⊢ False
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2.inr
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h✝ : s.Nonempty
u : Set (Set α)
hu₁ : u ⊆ {U | IsOpen[inst✝] U}
hu₂ : u.Finite
hu : powerset '' u ⊆ powerset '' {U | IsOpen[inst✝] U}
v : Set (Set α)
hv₁ : v ⊆ {U | IsOpen[inst✝] U}
hv₂ : v.Finite
hv : (fun V ↦ {s | (s ∩ V).Nonempty}) '' v ⊆ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {U | IsOpen[inst✝] U}
ht₁ : (powerset '' u).Finite ∧ ((fun V ↦ {s | (s ∩ V).Nonempty}) '' v).Finite
ht₂ :
  powerset '' u ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' v ⊆
    powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}
U : Set α := ⋂₀ u
hU : IsOpen[inst✝] U
hs : s ⊆ U ∧ ∀ i ∈ v, s ∈ {s | (s ∩ i).Nonempty}
⊢ ∃ x ∈ {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝] U},
    s ∈ {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ∧
      {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ⊆ 𝒫 U ∩ ⋂ a ∈ v, {s | (s ∩ a).Nonempty}

Tactic:
]

Goal state after:
case refine_2.inr
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h✝ : s.Nonempty
u : Set (Set α)
hu₁ : u ⊆ {U | IsOpen[inst✝] U}
hu₂ : u.Finite
hu : powerset '' u ⊆ powerset '' {U | IsOpen[inst✝] U}
v : Set (Set α)
hv₁ : v ⊆ {U | IsOpen[inst✝] U}
hv₂ : v.Finite
hv : (fun V ↦ {s | (s ∩ V).Nonempty}) '' v ⊆ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {U | IsOpen[inst✝] U}
ht₁ : (powerset '' u).Finite ∧ ((fun V ↦ {s | (s ∩ V).Nonempty}) '' v).Finite
ht₂ :
  powerset '' u ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' v ⊆
    powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}
U : Set α := ⋂₀ u
hU : IsOpen[inst✝] U
hs : s ⊆ U ∧ ∀ i ∈ v, s ∈ {s | (s ∩ i).Nonempty}
⊢ ∃ x ∈ {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝] U},
    s ∈ {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ∧
      {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ⊆ 𝒫 U ∩ ⋂ a ∈ v, {s | (s ∩ a).Nonempty}
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
x₀ : α
hf : LowerHemicontinuousAt f x₀
x : ℕ → α
hx : Tendsto x atTop (𝓝 x₀)
y₀ : β
hy₀ : y₀ ∈ f x₀
inst✝ : (𝓝 y₀).IsCountablyGenerated
U : ℕ → Set β
hU : ∀ (i : ℕ), y₀ ∈ U i ∧ IsOpen[inst✝¹] (U i)
hUbasis : (𝓝 y₀).HasAntitoneBasis fun i ↦ U i
hev : ∀ (k : ℕ), ∀ᶠ (n : ℕ) in atTop, (f (x n) ∩ U k).Nonempty
g : ℕ → ℕ := fun n ↦ Nat.findGreatest (fun k ↦ (f (x n) ∩ U k).Nonempty) n
key : ∀ (n k : ℕ), k ≤ n → (f (x n) ∩ U k).Nonempty → (f (x n) ∩ U (g n)).Nonempty
y : ℕ → β := fun n ↦ if h : (f (x n) ∩ U (g n)).Nonempty then h.some else y₀
hy : ∀ (n : ℕ), (f (x n) ∩ U (g n)).Nonempty → y n ∈ f (x n) ∩ U (g n)
⊢ ∀ (i : ℕ), True → ∀ᶠ (x : ℕ) in atTop, y x ∈ U i

Tactic:
]

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
x₀ : α
hf : LowerHemicontinuousAt f x₀
x : ℕ → α
hx : Tendsto x atTop (𝓝 x₀)
y₀ : β
hy₀ : y₀ ∈ f x₀
inst✝ : (𝓝 y₀).IsCountablyGenerated
U : ℕ → Set β
hU : ∀ (i : ℕ), y₀ ∈ U i ∧ IsOpen[inst✝¹] (U i)
hUbasis : (𝓝 y₀).HasAntitoneBasis fun i ↦ U i
hev : ∀ (k : ℕ), ∀ᶠ (n : ℕ) in atTop, (f (x n) ∩ U k).Nonempty
g : ℕ → ℕ := fun n ↦ Nat.findGreatest (fun k ↦ (f (x n) ∩ U k).Nonempty) n
key : ∀ (n k : ℕ), k ≤ n → (f (x n) ∩ U k).Nonempty → (f (x n) ∩ U (g n)).Nonempty
y : ℕ → β := fun n ↦ if h : (f (x n) ∩ U (g n)).Nonempty then h.some else y₀
hy : ∀ (n : ℕ), (f (x n) ∩ U (g n)).Nonempty → y n ∈ f (x n) ∩ U (g n)
⊢ ∀ (i : ℕ), True → ∀ᶠ (x : ℕ) in atTop, y x ∈ U i
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
hg : HasOpenCGraph g
hf : ∀ (u : Set β), IsOpen[inst✝] u → IsOpen[inst✝¹] {x | (f x ∩ u).Nonempty}
t : Set β
ht : IsOpen[inst✝] t
⊢ ∀ x ∈ {x | (f x ∩ g x ∩ t).Nonempty}, ∃ t_1 ⊆ {x | (f x ∩ g x ∩ t).Nonempty}, IsOpen[inst✝¹] t_1 ∧ x ∈ t_1

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
hg : HasOpenCGraph g
hf : ∀ (u : Set β), IsOpen[inst✝] u → IsOpen[inst✝¹] {x | (f x ∩ u).Nonempty}
t : Set β
ht : IsOpen[inst✝] t
⊢ ∀ x ∈ {x | (f x ∩ g x ∩ t).Nonempty}, ∃ t_1 ⊆ {x | (f x ∩ g x ∩ t).Nonempty}, IsOpen[inst✝¹] t_1 ∧ x ∈ t_1
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
U : SetRel α α
inst✝ : U.IsSymm
⊢ hausdorffEntourage U = hausdorffEntourage U

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
⊢ ∀ ⦃x : Set α × Set (Set α)⦄,
    x ∈ {p | IsOpen[inst✝] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1} →
      IsOpen[TopologicalSpace.vietoris α] {s | s ⊆ x.1 ∧ ∀ U ∈ x.2, (s ∩ U).Nonempty}

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
⊢ ∀ ⦃x : Set α × Set (Set α)⦄,
    x ∈ {p | IsOpen[inst✝] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1} →
      IsOpen[TopologicalSpace.vietoris α] {s | s ⊆ x.1 ∧ ∀ U ∈ x.2, (s ∩ U).Nonempty}
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
⊢ ∀ ⦃x : Set (Set α)⦄,
    x ∈ {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝] U} →
      ∀ x_1 ∈ {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty},
        ∃
          v ∈
            (fun p ↦ {s | s ⊆ p.1 ∧ ∀ U ∈ p.2, (s ∩ U).Nonempty}) ''
              {p | IsOpen[inst✝] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1},
          x_1 ∈ v ∧ v ⊆ {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty}

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
⊢ ∀ ⦃x : Set (Set α)⦄,
    x ∈ {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝] U} →
      ∀ x_1 ∈ {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty},
        ∃
          v ∈
            (fun p ↦ {s | s ⊆ p.1 ∧ ∀ U ∈ p.2, (s ∩ U).Nonempty}) ''
              {p | IsOpen[inst✝] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1},
          x_1 ∈ v ∧ v ⊆ {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty}
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → Set β
s : Set α
ι : Type u_3
F : ι → α → Set β
l : Filter ι
inst✝¹ : l.NeBot
inst✝ : UniformSpace β
htendsto : TendstoUniformlyOn F f l s
hF : ∀ (n : ι), LowerHemicontinuousOn (F n) s
⊢ ∀ x ∈ s, LowerHemicontinuousWithinAt f s x

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → Set β
s : Set α
ι : Type u_3
F : ι → α → Set β
l : Filter ι
inst✝¹ : l.NeBot
inst✝ : UniformSpace β
htendsto : TendstoUniformlyOn F f l s
hF : ∀ (n : ι), LowerHemicontinuousOn (F n) s
⊢ ∀ x ∈ s, LowerHemicontinuousWithinAt f s x
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → Set β
s : Set α
ι : Type u_3
F : ι → α → Set β
l : Filter ι
inst✝¹ : l.NeBot
inst✝ : UniformSpace β
htendsto : TendstoUniformlyOn F f l s
hF : ∀ (n : ι), LowerHemicontinuousOn (F n) s
x₀ : α
hx₀s : x₀ ∈ s
⊢ ∀ (u : Set β), IsOpen[inst✝.toTopologicalSpace] u → (f x₀ ∩ u).Nonempty → ∀ᶠ (x' : α) in 𝓝[s] x₀, (f x' ∩ u).Nonempty

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → Set β
s : Set α
ι : Type u_3
F : ι → α → Set β
l : Filter ι
inst✝¹ : l.NeBot
inst✝ : UniformSpace β
htendsto : TendstoUniformlyOn F f l s
hF : ∀ (n : ι), LowerHemicontinuousOn (F n) s
x₀ : α
hx₀s : x₀ ∈ s
⊢ ∀ (u : Set β), IsOpen[inst✝.toTopologicalSpace] u → (f x₀ ∩ u).Nonempty → ∀ᶠ (x' : α) in 𝓝[s] x₀, (f x' ∩ u).Nonempty