awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
hf : ∀ x ∈ s, UpperHemicontinuousWithinAt f s x
u : Set β
hu : IsClosed[inst_1] u
⊢ ∀ x ∈ s, UpperHemicontinuousWithinAt.{u_3, u_4} (β := β) (fun (x : α) ↦ f x ∩ u) s x

Tactic:
exact (hf · · |>.inter hu)

Premises used: UpperHemicontinuousWithinAt.inter
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
hf : UpperHemicontinuousAt f x
u : Set β
hu : IsClosed[inst_1] u
rw :
  ∀ (hf : UpperHemicontinuousWithinAt f univ x) {u : Set β} (hu : IsClosed[inst_1] u),
    UpperHemicontinuousWithinAt.{u_3, u_4} (β := β) (fun (x : α) ↦ f x ∩ u) univ x
⊢ UpperHemicontinuousAt.{u_3, u_4} (β := β) (fun (x : α) ↦ f x ∩ u) x

Tactic:
rw [← upperHemicontinuousWithinAt_univ_iff] at hf ⊢

Premises used: upperHemicontinuousWithinAt_univ_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
hf : UpperHemicontinuousWithinAt f univ x
u : Set β
hu : IsClosed[inst_1] u
⊢ UpperHemicontinuousWithinAt.{u_3, u_4} (β := β) (fun (x : α) ↦ f x ∩ u) univ x

Tactic:
hf.inter hu

Premises used: UpperHemicontinuousWithinAt.inter
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
hf : UpperHemicontinuousWithinAt f univ x
u : Set β
hu : IsClosed[inst_1] u
⊢ UpperHemicontinuousWithinAt.{u_3, u_4} (β := β) (fun (x : α) ↦ f x ∩ u) univ x

Tactic:
exact hf.inter hu

Premises used: UpperHemicontinuousWithinAt.inter
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
hf : UpperHemicontinuous f
u : Set β
hu : IsClosed[inst_1] u
rw :
  ∀ (hf : ∀ (x : α), UpperHemicontinuousAt f x) {u : Set β} (hu : IsClosed[inst_1] u) (x : α),
    UpperHemicontinuousAt.{u_3, u_4} (β := β) (fun (x : α) ↦ f x ∩ u) x
⊢ UpperHemicontinuous.{u_3, u_4} (β := β) fun (x : α) ↦ f x ∩ u

Tactic:
rw [upperHemicontinuous_iff] at hf ⊢

Premises used: upperHemicontinuous_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
hf : ∀ (x : α), UpperHemicontinuousAt f x
u : Set β
hu : IsClosed[inst_1] u
⊢ ∀ (x : α), UpperHemicontinuousAt.{u_3, u_4} (β := β) (fun (x : α) ↦ f x ∩ u) x

Tactic:
fun x ↦ (hf x).inter hu

Premises used: UpperHemicontinuousAt.inter
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
hf : ∀ (x : α), UpperHemicontinuousAt f x
u : Set β
hu : IsClosed[inst_1] u
⊢ ∀ (x : α), UpperHemicontinuousAt.{u_3, u_4} (β := β) (fun (x : α) ↦ f x ∩ u) x

Tactic:
exact fun x ↦ (hf x).inter hu

Premises used: UpperHemicontinuousAt.inter
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
x : α
γ : Type u_5
inst_2 : TopologicalSpace γ
i : γ → β
hf : UpperHemicontinuousWithinAt f s x
hi : IsInducing i
h_cl : IsClosed[inst_1] (range i)
⊢ UpperHemicontinuousWithinAt.{u_3, u_5} (β := γ) (fun (x : α) ↦ i ⁻¹' f x) s x

Tactic:
.of_forall_isOpen fun u hu hifu ↦ ?_

Premises used: UpperHemicontinuousWithinAt.of_forall_isOpen
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
x : α
γ : Type u_5
inst_2 : TopologicalSpace γ
i : γ → β
hf : UpperHemicontinuousWithinAt f s x
hi : IsInducing i
h_cl : IsClosed[inst_1] (range i)
refine : ∀ (u : Set γ) (hu : IsOpen[inst_2] u) (hifu : i ⁻¹' f x ⊆ u), ∀ᶠ (x' : α) in 𝓝[s] x, i ⁻¹' f x' ⊆ u
⊢ UpperHemicontinuousWithinAt.{u_3, u_5} (β := γ) (fun (x : α) ↦ i ⁻¹' f x) s x

Tactic:
refine .of_forall_isOpen fun u hu hifu ↦ ?_
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
x : α
γ : Type u_5
inst_2 : TopologicalSpace γ
i : γ → β
hf : UpperHemicontinuousWithinAt f s x
hi : IsInducing i
h_cl : IsClosed[inst_1] (range i)
u : Set γ
hu : IsOpen[inst_2] u
hifu : i ⁻¹' f x ⊆ u
obtain :
  ∀ (v : Set β) (hv : IsOpen[inst_1] v) (hu : IsOpen[inst_2] (i ⁻¹' v)) (hifu : i ⁻¹' f x ⊆ i ⁻¹' v),
    ∀ᶠ (x' : α) in 𝓝[s] x, i ⁻¹' f x' ⊆ i ⁻¹' v
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, i ⁻¹' f x' ⊆ u

Tactic:
obtain ⟨v, hv, rfl⟩ := hi.isOpen_iff.mp hu

Premises used: Topology.IsInducing.isOpen_iff, Iff.mp, rfl
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
x : α
γ : Type u_5
inst_2 : TopologicalSpace γ
i : γ → β
hf : UpperHemicontinuousWithinAt f s x
hi : IsInducing i
h_cl : IsClosed[inst_1] (range i)
v : Set β
hv : IsOpen[inst_1] v
hu : IsOpen[inst_2] (i ⁻¹' v)
hifu : i ⁻¹' f x ⊆ i ⁻¹' v
simp_rw : ∀ (hifu : f x ∩ range i ⊆ v), ∀ᶠ (x' : α) in 𝓝[s] x, f x' ∩ range i ⊆ v
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, i ⁻¹' f x' ⊆ i ⁻¹' v

Tactic:
simp_rw [← preimage_inter_range (s := f _), preimage_subset_preimage_iff inter_subset_right]
    at hifu ⊢

Premises used: Set.preimage_subset_preimage_iff, Set.preimage_inter_range, Set.inter_subset_right
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
x : α
γ : Type u_5
inst_2 : TopologicalSpace γ
i : γ → β
hf : UpperHemicontinuousWithinAt f s x
hi : IsInducing i
h_cl : IsClosed[inst_1] (range i)
v : Set β
hv : IsOpen[inst_1] v
hu : IsOpen[inst_2] (i ⁻¹' v)
hifu : f x ∩ range i ⊆ v
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, f x' ∩ range i ⊆ v

Tactic:
hf.inter h_cl |>.forall_isOpen v hv hifu

Premises used: UpperHemicontinuousWithinAt.inter, UpperHemicontinuousWithinAt.forall_isOpen
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
x : α
γ : Type u_5
inst_2 : TopologicalSpace γ
i : γ → β
hf : UpperHemicontinuousWithinAt f s x
hi : IsInducing i
h_cl : IsClosed[inst_1] (range i)
v : Set β
hv : IsOpen[inst_1] v
hu : IsOpen[inst_2] (i ⁻¹' v)
hifu : f x ∩ range i ⊆ v
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, f x' ∩ range i ⊆ v

Tactic:
exact hf.inter h_cl |>.forall_isOpen v hv hifu

Premises used: UpperHemicontinuousWithinAt.inter, UpperHemicontinuousWithinAt.forall_isOpen
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
γ : Type u_5
inst_2 : TopologicalSpace γ
i : γ → β
hf : UpperHemicontinuousOn f s
hi : IsInducing i
h_cl : IsClosed[inst_1] (range i)
⊢ ∀ x ∈ s, UpperHemicontinuousWithinAt f s x

Tactic:
rw [upperHemicontinuousOn_iff] at hf ⊢

Premises used: upperHemicontinuousOn_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
γ : Type u_5
inst_2 : TopologicalSpace γ
i : γ → β
hf : UpperHemicontinuousOn f s
hi : IsInducing i
h_cl : IsClosed[inst_1] (range i)
hf₁ : ∀ x ∈ s, UpperHemicontinuousWithinAt f s x
⊢ IsInducing i

Tactic:
rw [upperHemicontinuousOn_iff] at hf ⊢

Premises used: upperHemicontinuousOn_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
γ : Type u_5
inst_2 : TopologicalSpace γ
i : γ → β
hf : UpperHemicontinuousOn f s
hi : IsInducing i
h_cl : IsClosed[inst_1] (range i)
hf₁ : ∀ x ∈ s, UpperHemicontinuousWithinAt f s x
hi₁ : IsInducing i
⊢ IsClosed[inst_1] (range i)

Tactic:
rw [upperHemicontinuousOn_iff] at hf ⊢

Premises used: upperHemicontinuousOn_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
γ : Type u_5
inst_2 : TopologicalSpace γ
i : γ → β
hf : ∀ x ∈ s, UpperHemicontinuousWithinAt f s x
hi : IsInducing i
h_cl : IsClosed[inst_1] (range i)
⊢ ∀ x ∈ s, UpperHemicontinuousWithinAt.{u_3, u_5} (β := γ) (fun (x : α) ↦ i ⁻¹' f x) s x

Tactic:
fun x hx ↦ (hf x hx).isInducing_comp hi h_cl

Premises used: UpperHemicontinuousWithinAt.isInducing_comp
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
γ : Type u_5
inst_2 : TopologicalSpace γ
i : γ → β
hf : ∀ x ∈ s, UpperHemicontinuousWithinAt f s x
hi : IsInducing i
h_cl : IsClosed[inst_1] (range i)
⊢ ∀ x ∈ s, UpperHemicontinuousWithinAt.{u_3, u_5} (β := γ) (fun (x : α) ↦ i ⁻¹' f x) s x

Tactic:
exact fun x hx ↦ (hf x hx).isInducing_comp hi h_cl

Premises used: UpperHemicontinuousWithinAt.isInducing_comp
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
γ : Type u_5
inst_2 : TopologicalSpace γ
i : γ → β
hf : UpperHemicontinuousAt f x
hi : IsInducing i
h_cl : IsClosed[inst_1] (range i)
⊢ UpperHemicontinuousAt.{u_3, u_5} (β := γ) (fun (x : α) ↦ i ⁻¹' f x) x

Tactic:
simpa [upperHemicontinuousWithinAt_univ_iff] using
    hf.upperHemicontinuousWithinAt (s := Set.univ) |>.isInducing_comp hi h_cl

Premises used: UpperHemicontinuousAt.upperHemicontinuousWithinAt, Set.univ, UpperHemicontinuousWithinAt.isInducing_comp, upperHemicontinuousWithinAt_univ_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
γ : Type u_5
inst_2 : TopologicalSpace γ
i : γ → β
hf : UpperHemicontinuous f
hi : IsInducing i
h_cl : IsClosed[inst_1] (range i)
⊢ ∀ (x : α), UpperHemicontinuousAt f x

Tactic:
rw [upperHemicontinuous_iff] at hf ⊢

Premises used: upperHemicontinuous_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
γ : Type u_5
inst_2 : TopologicalSpace γ
i : γ → β
hf : UpperHemicontinuous f
hi : IsInducing i
h_cl : IsClosed[inst_1] (range i)
hf₁ : ∀ (x : α), UpperHemicontinuousAt f x
⊢ IsInducing i

Tactic:
rw [upperHemicontinuous_iff] at hf ⊢

Premises used: upperHemicontinuous_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
γ : Type u_5
inst_2 : TopologicalSpace γ
i : γ → β
hf : UpperHemicontinuous f
hi : IsInducing i
h_cl : IsClosed[inst_1] (range i)
hf₁ : ∀ (x : α), UpperHemicontinuousAt f x
hi₁ : IsInducing i
⊢ IsClosed[inst_1] (range i)

Tactic:
rw [upperHemicontinuous_iff] at hf ⊢

Premises used: upperHemicontinuous_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
γ : Type u_5
inst_2 : TopologicalSpace γ
i : γ → β
hf : ∀ (x : α), UpperHemicontinuousAt f x
hi : IsInducing i
h_cl : IsClosed[inst_1] (range i)
⊢ ∀ (x : α), UpperHemicontinuousAt.{u_3, u_5} (β := γ) (fun (x : α) ↦ i ⁻¹' f x) x

Tactic:
fun x ↦ (hf x).isInducing_comp hi h_cl

Premises used: UpperHemicontinuousAt.isInducing_comp
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
γ : Type u_5
inst_2 : TopologicalSpace γ
i : γ → β
hf : ∀ (x : α), UpperHemicontinuousAt f x
hi : IsInducing i
h_cl : IsClosed[inst_1] (range i)
⊢ ∀ (x : α), UpperHemicontinuousAt.{u_3, u_5} (β := γ) (fun (x : α) ↦ i ⁻¹' f x) x

Tactic:
exact fun x ↦ (hf x).isInducing_comp hi h_cl

Premises used: UpperHemicontinuousAt.isInducing_comp
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
hf : UpperHemicontinuous f
simp : ∀ (x : α), Membership.mem (γ := Set α) {a : α | f a = ∅} x → {a : α | f a = ∅} ∈ 𝓝 x
⊢ IsClosed[inst] {x : α | (f x).Nonempty}

Tactic:
simp only [← isOpen_compl_iff, compl_setOf, not_nonempty_iff_eq_empty, isOpen_iff_mem_nhds]

Premises used: Set.not_nonempty_iff_eq_empty, isOpen_iff_mem_nhds, isOpen_compl_iff, Set.compl_setOf
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
hf : UpperHemicontinuous f
x : α
f₁ : ∀ (hx : f x = ∅), {a : α | f a = ∅} ∈ 𝓝 x
⊢ Membership.mem (γ := Set α) {a : α | f a = ∅} x → {a : α | f a = ∅} ∈ 𝓝 x

Tactic:
(hx : f x = ∅)
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
hf : UpperHemicontinuous f
x : α
hx : f x = ∅
⊢ ∀ (x : α), ∀ t ∈ 𝓝ˢ (f x), ∀ᶠ (x' : α) in 𝓝 x, t ∈ 𝓝ˢ (f x')

Tactic:
simp_rw [upperHemicontinuous_iff, upperHemicontinuousAt_iff] at hf

Premises used: upperHemicontinuousAt_iff, upperHemicontinuous_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
hx : f x = ∅
hf : ∀ (x : α), ∀ t ∈ 𝓝ˢ (f x), ∀ᶠ (x' : α) in 𝓝 x, t ∈ 𝓝ˢ (f x')
⊢ {a : α | f a = ∅} ∈ 𝓝 x

Tactic:
simpa [hx, empty_mem_iff_bot, nhdsSet_eq_bot_iff] using hf x ∅

Premises used: nhdsSet_eq_bot_iff, Filter.empty_mem_iff_bot, EmptyCollection.emptyCollection
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x₀ : α
inst_2 : (𝓝 x₀).IsCountablyGenerated
K : Set β
hK : IsSeqCompact K
hf : ∀ᶠ (x : α) in 𝓝 x₀, f x ⊆ K
h :
  ∀ (x : ℕ → α),
    Tendsto x atTop (𝓝 x₀) → ∀ (y : ℕ → β), (∀ (n : ℕ), y n ∈ f (x n)) → ∀ (y₀ : β), Tendsto y atTop (𝓝 y₀) → y₀ ∈ f x₀
⊢ UpperHemicontinuousAt f x₀

Tactic:
.of_frequently fun t ht hft ↦ ?_

Premises used: UpperHemicontinuousAt.of_frequently
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x₀ : α
inst_2 : (𝓝 x₀).IsCountablyGenerated
K : Set β
hK : IsSeqCompact K
hf : ∀ᶠ (x : α) in 𝓝 x₀, f x ⊆ K
h :
  ∀ (x : ℕ → α),
    Tendsto x atTop (𝓝 x₀) → ∀ (y : ℕ → β), (∀ (n : ℕ), y n ∈ f (x n)) → ∀ (y₀ : β), Tendsto y atTop (𝓝 y₀) → y₀ ∈ f x₀
refine : ∀ (t : Set β) (ht : IsClosed[inst_1] t) (hft : ∃ᶠ (x' : α) in 𝓝 x₀, (f x' ∩ t).Nonempty), (f x₀ ∩ t).Nonempty
⊢ UpperHemicontinuousAt f x₀

Tactic:
refine .of_frequently fun t ht hft ↦ ?_
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x₀ : α
inst_2 : (𝓝 x₀).IsCountablyGenerated
K : Set β
hK : IsSeqCompact K
hf : ∀ᶠ (x : α) in 𝓝 x₀, f x ⊆ K
h :
  ∀ (x : ℕ → α),
    Tendsto x atTop (𝓝 x₀) → ∀ (y : ℕ → β), (∀ (n : ℕ), y n ∈ f (x n)) → ∀ (y₀ : β), Tendsto y atTop (𝓝 y₀) → y₀ ∈ f x₀
t : Set β
ht : IsClosed[inst_1] t
hft : ∃ᶠ (x' : α) in 𝓝 x₀, (f x' ∩ t).Nonempty
obtain : ∀ (x : ℕ → α) (hx : Tendsto x atTop (𝓝 x₀)) (hfx : ∀ (n : ℕ), (f (x n) ∩ t).Nonempty), (f x₀ ∩ t).Nonempty
⊢ (f x₀ ∩ t).Nonempty

Tactic:
obtain ⟨x, hx, hfx⟩ := exists_seq_forall_of_frequently hft

Premises used: Filter.exists_seq_forall_of_frequently
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x₀ : α
inst_2 : (𝓝 x₀).IsCountablyGenerated
K : Set β
hK : IsSeqCompact K
hf : ∀ᶠ (x : α) in 𝓝 x₀, f x ⊆ K
h :
  ∀ (x : ℕ → α),
    Tendsto x atTop (𝓝 x₀) → ∀ (y : ℕ → β), (∀ (n : ℕ), y n ∈ f (x n)) → ∀ (y₀ : β), Tendsto y atTop (𝓝 y₀) → y₀ ∈ f x₀
t : Set β
ht : IsClosed[inst_1] t
hft : ∃ᶠ (x' : α) in 𝓝 x₀, (f x' ∩ t).Nonempty
x : ℕ → α
hx : Tendsto x atTop (𝓝 x₀)
hfx : ∀ (n : ℕ), (f (x n) ∩ t).Nonempty
choose : ∀ (y : (n : ℕ) → β) (hy : ∀ (n : ℕ), y n ∈ f (x n) ∩ t), (f x₀ ∩ t).Nonempty
⊢ (f x₀ ∩ t).Nonempty

Tactic:
choose y hy using hfx
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x₀ : α
inst_2 : (𝓝 x₀).IsCountablyGenerated
K : Set β
hK : IsSeqCompact K
hf : ∀ᶠ (x : α) in 𝓝 x₀, f x ⊆ K
h :
  ∀ (x : ℕ → α),
    Tendsto x atTop (𝓝 x₀) → ∀ (y : ℕ → β), (∀ (n : ℕ), y n ∈ f (x n)) → ∀ (y₀ : β), Tendsto y atTop (𝓝 y₀) → y₀ ∈ f x₀
t : Set β
ht : IsClosed[inst_1] t
hft : ∃ᶠ (x' : α) in 𝓝 x₀, (f x' ∩ t).Nonempty
x : ℕ → α
hx : Tendsto x atTop (𝓝 x₀)
y : (n : ℕ) → β
hy : ∀ (n : ℕ), y n ∈ f (x n) ∩ t
⊢ ∃ᶠ (n : ℕ) in atTop, y n ∈ K

Tactic:
Eventually.frequently ?_

Premises used: Filter.Eventually.frequently
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x₀ : α
inst_2 : (𝓝 x₀).IsCountablyGenerated
K : Set β
hK : IsSeqCompact K
hf : ∀ᶠ (x : α) in 𝓝 x₀, f x ⊆ K
h :
  ∀ (x : ℕ → α),
    Tendsto x atTop (𝓝 x₀) → ∀ (y : ℕ → β), (∀ (n : ℕ), y n ∈ f (x n)) → ∀ (y₀ : β), Tendsto y atTop (𝓝 y₀) → y₀ ∈ f x₀
t : Set β
ht : IsClosed[inst_1] t
hft : ∃ᶠ (x' : α) in 𝓝 x₀, (f x' ∩ t).Nonempty
x : ℕ → α
hx : Tendsto x atTop (𝓝 x₀)
y : (n : ℕ) → β
hy : ∀ (n : ℕ), y n ∈ f (x n) ∩ t
refine : ∀ᶠ (x : ℕ) in atTop, y x ∈ K
⊢ ∃ᶠ (n : ℕ) in atTop, y n ∈ K

Tactic:
refine Eventually.frequently ?_

Premises used: Filter.Eventually.frequently
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x₀ : α
inst_2 : (𝓝 x₀).IsCountablyGenerated
K : Set β
hK : IsSeqCompact K
hf : ∀ᶠ (x : α) in 𝓝 x₀, f x ⊆ K
h :
  ∀ (x : ℕ → α),
    Tendsto x atTop (𝓝 x₀) → ∀ (y : ℕ → β), (∀ (n : ℕ), y n ∈ f (x n)) → ∀ (y₀ : β), Tendsto y atTop (𝓝 y₀) → y₀ ∈ f x₀
t : Set β
ht : IsClosed[inst_1] t
hft : ∃ᶠ (x' : α) in 𝓝 x₀, (f x' ∩ t).Nonempty
x : ℕ → α
hx : Tendsto x atTop (𝓝 x₀)
y : (n : ℕ) → β
hy : ∀ (n : ℕ), y n ∈ f (x n) ∩ t
h₁ : ∀ (n : ℕ) (hn : n ∈ x ⁻¹' {x : α | f x ⊆ K}), y n ∈ K
⊢ ∀ᶠ (x : ℕ) in atTop, y x ∈ K

Tactic:
filter_upwards [hx hf] with n hn
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x₀ : α
inst_2 : (𝓝 x₀).IsCountablyGenerated
K : Set β
hK : IsSeqCompact K
hf : ∀ᶠ (x : α) in 𝓝 x₀, f x ⊆ K
h :
  ∀ (x : ℕ → α),
    Tendsto x atTop (𝓝 x₀) → ∀ (y : ℕ → β), (∀ (n : ℕ), y n ∈ f (x n)) → ∀ (y₀ : β), Tendsto y atTop (𝓝 y₀) → y₀ ∈ f x₀
t : Set β
ht : IsClosed[inst_1] t
hft : ∃ᶠ (x' : α) in 𝓝 x₀, (f x' ∩ t).Nonempty
x : ℕ → α
hx : Tendsto x atTop (𝓝 x₀)
y : (n : ℕ) → β
hy : ∀ (n : ℕ), y n ∈ f (x n) ∩ t
n : ℕ
hn : n ∈ x ⁻¹' {x : α | f x ⊆ K}
⊢ y n ∈ K

Tactic:
hn (hy n).1

Premises used: And.left
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x₀ : α
inst_2 : (𝓝 x₀).IsCountablyGenerated
K : Set β
hK : IsSeqCompact K
hf : ∀ᶠ (x : α) in 𝓝 x₀, f x ⊆ K
h :
  ∀ (x : ℕ → α),
    Tendsto x atTop (𝓝 x₀) → ∀ (y : ℕ → β), (∀ (n : ℕ), y n ∈ f (x n)) → ∀ (y₀ : β), Tendsto y atTop (𝓝 y₀) → y₀ ∈ f x₀
t : Set β
ht : IsClosed[inst_1] t
hft : ∃ᶠ (x' : α) in 𝓝 x₀, (f x' ∩ t).Nonempty
x : ℕ → α
hx : Tendsto x atTop (𝓝 x₀)
y : (n : ℕ) → β
hy : ∀ (n : ℕ), y n ∈ f (x n) ∩ t
n : ℕ
hn : n ∈ x ⁻¹' {x : α | f x ⊆ K}
⊢ y n ∈ K

Tactic:
exact hn (hy n).1

Premises used: And.left
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x₀ : α
inst_2 : (𝓝 x₀).IsCountablyGenerated
K : Set β
hK : IsSeqCompact K
hf : ∀ᶠ (x : α) in 𝓝 x₀, f x ⊆ K
h :
  ∀ (x : ℕ → α),
    Tendsto x atTop (𝓝 x₀) → ∀ (y : ℕ → β), (∀ (n : ℕ), y n ∈ f (x n)) → ∀ (y₀ : β), Tendsto y atTop (𝓝 y₀) → y₀ ∈ f x₀
t : Set β
ht : IsClosed[inst_1] t
hft : ∃ᶠ (x' : α) in 𝓝 x₀, (f x' ∩ t).Nonempty
x : ℕ → α
hx : Tendsto x atTop (𝓝 x₀)
y : (n : ℕ) → β
hy : ∀ (n : ℕ), y n ∈ f (x n) ∩ t
obtain :
  ∀ (y₀ : β) (hy₀ : y₀ ∈ K) (φ : ℕ → ℕ) (hφ : StrictMono φ) (hyφ : Tendsto (y ∘ φ) atTop (𝓝 y₀)), (f x₀ ∩ t).Nonempty
⊢ (f x₀ ∩ t).Nonempty

Tactic:
obtain ⟨y₀, hy₀, φ, hφ, hyφ⟩ := hK.subseq_of_frequently_in (x := y) <| by
    refine Eventually.frequently ?_
    filter_upwards [hx hf] with n hn
    exact hn (hy n).1

Premises used: IsSeqCompact.subseq_of_frequently_in
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x₀ : α
inst_2 : (𝓝 x₀).IsCountablyGenerated
K : Set β
hK : IsSeqCompact K
hf : ∀ᶠ (x : α) in 𝓝 x₀, f x ⊆ K
h :
  ∀ (x : ℕ → α),
    Tendsto x atTop (𝓝 x₀) → ∀ (y : ℕ → β), (∀ (n : ℕ), y n ∈ f (x n)) → ∀ (y₀ : β), Tendsto y atTop (𝓝 y₀) → y₀ ∈ f x₀
t : Set β
ht : IsClosed[inst_1] t
hft : ∃ᶠ (x' : α) in 𝓝 x₀, (f x' ∩ t).Nonempty
x : ℕ → α
hx : Tendsto x atTop (𝓝 x₀)
y : (n : ℕ) → β
hy : ∀ (n : ℕ), y n ∈ f (x n) ∩ t
y₀ : β
hy₀ : y₀ ∈ K
φ : ℕ → ℕ
hφ : StrictMono φ
hyφ : Tendsto (y ∘ φ) atTop (𝓝 y₀)
⊢ y₀ ∈ f x₀

Tactic:
specialize h (x ∘ φ) (hx.comp hφ.tendsto_atTop) (y ∘ φ) (fun n ↦ (hy _).1) _ hyφ

Premises used: Function.comp, StrictMono.tendsto_atTop, And.left, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x₀ : α
inst_2 : (𝓝 x₀).IsCountablyGenerated
K : Set β
hK : IsSeqCompact K
hf : ∀ᶠ (x : α) in 𝓝 x₀, f x ⊆ K
t : Set β
ht : IsClosed[inst_1] t
hft : ∃ᶠ (x' : α) in 𝓝 x₀, (f x' ∩ t).Nonempty
x : ℕ → α
hx : Tendsto x atTop (𝓝 x₀)
y : (n : ℕ) → β
hy : ∀ (n : ℕ), y n ∈ f (x n) ∩ t
y₀ : β
hy₀ : y₀ ∈ K
φ : ℕ → ℕ
hφ : StrictMono φ
hyφ : Tendsto (y ∘ φ) atTop (𝓝 y₀)
h : y₀ ∈ f x₀
⊢ (f x₀ ∩ t).Nonempty

Tactic:
⟨y₀, h, ht.closure_eq ▸ mem_closure_of_tendsto hyφ <| .of_forall fun n ↦ (hy _).2⟩

Premises used: Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x₀ : α
inst_2 : (𝓝 x₀).IsCountablyGenerated
K : Set β
hK : IsSeqCompact K
hf : ∀ᶠ (x : α) in 𝓝 x₀, f x ⊆ K
t : Set β
ht : IsClosed[inst_1] t
hft : ∃ᶠ (x' : α) in 𝓝 x₀, (f x' ∩ t).Nonempty
x : ℕ → α
hx : Tendsto x atTop (𝓝 x₀)
y : (n : ℕ) → β
hy : ∀ (n : ℕ), y n ∈ f (x n) ∩ t
y₀ : β
hy₀ : y₀ ∈ K
φ : ℕ → ℕ
hφ : StrictMono φ
hyφ : Tendsto (y ∘ φ) atTop (𝓝 y₀)
h : y₀ ∈ f x₀
⊢ (f x₀ ∩ t).Nonempty

Tactic:
exact ⟨y₀, h, ht.closure_eq ▸ mem_closure_of_tendsto hyφ <| .of_forall fun n ↦ (hy _).2⟩
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : RegularSpace β
f : α → Set β
x₀ : α
l : Filter ι
hf : UpperHemicontinuousAt f x₀
hf_closed : IsClosed[inst_1] (f x₀)
x : ι → α
hx : Tendsto x l (𝓝 x₀)
y : ι → β
hy : ∃ᶠ (n : ι) in l, y n ∈ f (x n)
y₀ : β
hy₀ : Tendsto y l (𝓝 y₀)
by_contra : ∀ (this : y₀ ∉ f x₀), False
⊢ y₀ ∈ f x₀

Tactic:
by_contra
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : RegularSpace β
f : α → Set β
x₀ : α
l : Filter ι
hf : UpperHemicontinuousAt f x₀
hf_closed : IsClosed[inst_1] (f x₀)
x : ι → α
hx : Tendsto x l (𝓝 x₀)
y : ι → β
hy : ∃ᶠ (n : ι) in l, y n ∈ f (x n)
y₀ : β
hy₀ : Tendsto y l (𝓝 y₀)
this : y₀ ∉ f x₀
obtain : ∀ (s : Set β) (hs : s ∈ 𝓝ˢ (f x₀)) (t : Set β) (ht : t ∈ 𝓝 y₀) (hst : Disjoint s t), False
⊢ False

Tactic:
obtain ⟨s, hs, t, ht, hst⟩ := Filter.disjoint_iff.mp <| RegularSpace.regular hf_closed this

Premises used: Filter.disjoint_iff, RegularSpace.regular, Iff.mp