awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
| ∀ (x : Set β), IsClosed[inst_1] xᶜ → IsClosed[inst] (f ⁻¹' Iic xᶜ)
have simp : ∀ (x : Set β), IsOpen[inst_1] x → IsOpen[inst] (f ⁻¹' Iic xᶜ)ᶜ
Tactic: simp [← isOpen_compl_iff]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
| ∀ (u : Set β), IsClosed[inst_1] u → IsClosed[inst] (f ⁻¹' Iic u)
have rw : ∀ (x : Set β), IsOpen[inst_1] x → IsOpen[inst] (f ⁻¹' Iic xᶜ)ᶜ
Tactic: rw [compl_surjective.forall]
    simp [← isOpen_compl_iff]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
⊢ LowerHemicontinuous f ↔ ∀ (u : Set β), IsClosed[inst_1] u → IsClosed[inst] (f ⁻¹' Iic u)
have conv_rhs : LowerHemicontinuous f ↔ ∀ (x : Set β), IsOpen[inst_1] x → IsOpen[inst] (f ⁻¹' Iic xᶜ)ᶜ
Tactic: conv_rhs =>
    rw [compl_surjective.forall]
    simp [← isOpen_compl_iff]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
⊢ IsOpenMap f ↔ LowerHemicontinuous.{u_2, u_1} (β := α) fun (x : β) ↦ f ⁻¹' {x}
have rw : (∀ {u : Set α}, IsClosed[inst] u → IsClosed[inst_1] (kernImage f u)) ↔
  ∀ (u : Set α), IsClosed[inst] u → IsClosed[inst_1] ((fun (x : β) ↦ f ⁻¹' {x}) ⁻¹' Iic u)
Tactic: rw [isOpenMap_iff_kernImage, lowerHemicontinuous_iff_isClosed_preimage_Iic]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
⊢ UpperHemicontinuousWithinAt.{u_1, u_2} (β := β) (fun (x : α) ↦ {f x}) s x ↔ ContinuousWithinAt f s x
have refine : UpperHemicontinuousWithinAt.{u_1, u_2} (β := β) (fun (x : α) ↦ {f x}) s x → ContinuousWithinAt f s x
Tactic: refine ⟨?_, fun hf ↦ upperHemicontinuous_singleton_id.upperHemicontinuousWithinAt _ _ |>.comp hf
    (mapsTo_image _ _)⟩
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
⊢ UpperHemicontinuousWithinAt.{u_1, u_2} (β := β) (fun (x : α) ↦ {f x}) s x → ContinuousWithinAt f s x
have simp : (∀ t ∈ 𝓝 (f x), ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝 (f x')) → ∀ s_1 ∈ 𝓝 (f x), ∀ᶠ (x : α) in 𝓝[s] x, f x ∈ s_1
Tactic: simp only [upperHemicontinuousWithinAt_iff, nhdsSet_singleton, ContinuousWithinAt,
    tendsto_iff_forall_eventually_mem]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
h : ∀ t ∈ 𝓝 (f x), ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝 (f x')
t : Set β
ht : t ∈ 𝓝 (f x)
⊢ ∀ᶠ (x : α) in 𝓝[s] x, f x ∈ t
have h₁ : ∀ (x : α), t ∈ 𝓝 (f x) → f x ∈ t
Tactic: filter_upwards [h t ht] with x
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (hypothesis)
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → Set β
s : Set α
x : α
hf : UpperHemicontinuousWithinAt f s x
hg : UpperHemicontinuousWithinAt g s x
⊢ UpperHemicontinuousWithinAt.{u_3, u_4} (β := β) (fun (x : α) ↦ f x ∪ g x) s x
have hf₁ : ∀ t ∈ 𝓝ˢ (f x), ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (f x')
Tactic: rw [upperHemicontinuousWithinAt_iff] at hf hg ⊢
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (hypothesis)
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → Set β
s : Set α
x : α
hf : UpperHemicontinuousWithinAt f s x
hg : UpperHemicontinuousWithinAt g s x
hf₁ : ∀ t ∈ 𝓝ˢ (f x), ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (f x')
⊢ UpperHemicontinuousWithinAt.{u_3, u_4} (β := β) (fun (x : α) ↦ f x ∪ g x) s x
have hg₁ : ∀ t ∈ 𝓝ˢ (g x), ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (g x')
Tactic: rw [upperHemicontinuousWithinAt_iff] at hf hg ⊢
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (hypothesis)
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → Set β
s : Set α
hf : UpperHemicontinuousOn f s
hg : UpperHemicontinuousOn g s
⊢ UpperHemicontinuousOn.{u_3, u_4} (β := β) (fun (x : α) ↦ f x ∪ g x) s
have hf₁ : ∀ x ∈ s, UpperHemicontinuousWithinAt f s x
Tactic: rw [upperHemicontinuousOn_iff] at hf hg ⊢
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (hypothesis)
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → Set β
s : Set α
hf : UpperHemicontinuousOn f s
hg : UpperHemicontinuousOn g s
hf₁ : ∀ x ∈ s, UpperHemicontinuousWithinAt f s x
⊢ UpperHemicontinuousOn.{u_3, u_4} (β := β) (fun (x : α) ↦ f x ∪ g x) s
have hg₁ : ∀ x ∈ s, UpperHemicontinuousWithinAt g s x
Tactic: rw [upperHemicontinuousOn_iff] at hf hg ⊢
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → Set β
x : α
hf : UpperHemicontinuousAt f x
hg : UpperHemicontinuousAt g x
⊢ UpperHemicontinuousAt.{u_3, u_4} (β := β) (fun (x : α) ↦ f x ∪ g x) x
have rw : ∀ (hf : UpperHemicontinuousWithinAt f univ x) (hg : UpperHemicontinuousWithinAt g univ x),
  UpperHemicontinuousWithinAt.{u_3, u_4} (β := β) (fun (x : α) ↦ f x ∪ g x) univ x
Tactic: rw [← upperHemicontinuousWithinAt_univ_iff] at hf hg ⊢
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (hypothesis)
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → Set β
hf : UpperHemicontinuous f
hg : UpperHemicontinuous g
⊢ UpperHemicontinuous.{u_3, u_4} (β := β) fun (x : α) ↦ f x ∪ g x
have hf₁ : ∀ (x : α), UpperHemicontinuousAt f x
Tactic: rw [upperHemicontinuous_iff] at hf hg ⊢
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (hypothesis)
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → Set β
hf : UpperHemicontinuous f
hg : UpperHemicontinuous g
hf₁ : ∀ (x : α), UpperHemicontinuousAt f x
⊢ UpperHemicontinuous.{u_3, u_4} (β := β) fun (x : α) ↦ f x ∪ g x
have hg₁ : ∀ (x : α), UpperHemicontinuousAt g x
Tactic: rw [upperHemicontinuous_iff] at hf hg ⊢
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
x : α
hf : UpperHemicontinuousWithinAt f s x
u : Set β
hu : IsClosed[inst_1] u
⊢ UpperHemicontinuousWithinAt.{u_3, u_4} (β := β) (fun (x : α) ↦ f x ∩ u) s x
have rw : ∀ (hf : ∀ (u : Set β), IsOpen[inst_1] u → f x ⊆ u → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ u) {u : Set β}
  (hu : IsClosed[inst_1] u) (u_1 : Set β), IsOpen[inst_1] u_1 → f x ∩ u ⊆ u_1 → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ∩ u ⊆ u_1
Tactic: rw [upperHemicontinuousWithinAt_iff_forall_isOpen] at hf ⊢
Cleared hypotheses: hf, u, hu
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (hypothesis)
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
x : α
hf : ∀ (u : Set β), IsOpen[inst_1] u → f x ⊆ u → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ u
u : Set β
hu : IsClosed[inst_1] u
t : Set β
ht_open : IsOpen[inst_1] t
ht : f x ∩ u ⊆ t
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, f x' ∩ u ⊆ t
have hf₁ : ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ t ∪ uᶜ
Tactic: specialize hf (t ∪ uᶜ) (ht_open.union hu.isOpen_compl) (by grind)
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
hf : UpperHemicontinuousOn f s
u : Set β
hu : IsClosed[inst_1] u
⊢ UpperHemicontinuousOn.{u_3, u_4} (β := β) (fun (x : α) ↦ f x ∩ u) s
have rw : ∀ (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: rw [upperHemicontinuousOn_iff] at hf ⊢
Cleared hypotheses: hf, u, hu
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
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
⊢ UpperHemicontinuousAt.{u_3, u_4} (β := β) (fun (x : α) ↦ f x ∩ u) x
have 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
Tactic: rw [← upperHemicontinuousWithinAt_univ_iff] at hf ⊢
Cleared hypotheses: hf, u, hu
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
hf : UpperHemicontinuous f
u : Set β
hu : IsClosed[inst_1] u
⊢ UpperHemicontinuous.{u_3, u_4} (β := β) fun (x : α) ↦ f x ∩ u
have 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
Tactic: rw [upperHemicontinuous_iff] at hf ⊢
Cleared hypotheses: hf, u, hu
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
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
have refine : ∀ (u : Set γ) (hu : IsOpen[inst_2] u) (hifu : i ⁻¹' f x ⊆ u), ∀ᶠ (x' : α) in 𝓝[s] x, i ⁻¹' f x' ⊆ u
Tactic: refine .of_forall_isOpen fun u hu hifu ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
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
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, i ⁻¹' f x' ⊆ u
have 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
Tactic: obtain ⟨v, hv, rfl⟩ := hi.isOpen_iff.mp hu
Cleared hypotheses: u, hu, hifu
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
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
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, i ⁻¹' f x' ⊆ i ⁻¹' v
have simp_rw : ∀ (hifu : f x ∩ range i ⊆ v), ∀ᶠ (x' : α) in 𝓝[s] x, f x' ∩ range i ⊆ v
Tactic: simp_rw [← preimage_inter_range (s := f _), preimage_subset_preimage_iff inter_subset_right]
    at hifu ⊢
Cleared hypotheses: hifu
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (hypothesis)
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)
⊢ UpperHemicontinuousOn.{u_3, u_5} (β := γ) (fun (x : α) ↦ i ⁻¹' f x) s
have hf₁ : ∀ x ∈ s, UpperHemicontinuousWithinAt f s x
Tactic: rw [upperHemicontinuousOn_iff] at hf ⊢
Cleared hypotheses: hf, hi, h_cl
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (hypothesis)
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)
⊢ UpperHemicontinuous.{u_3, u_5} (β := γ) fun (x : α) ↦ i ⁻¹' f x
have hf₁ : ∀ (x : α), UpperHemicontinuousAt f x
Tactic: rw [upperHemicontinuous_iff] at hf ⊢
Cleared hypotheses: hf, hi, h_cl
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
hf : UpperHemicontinuous f
⊢ IsClosed[inst] {x : α | (f x).Nonempty}
have simp : ∀ (x : α), Membership.mem (γ := Set α) {a : α | f a = ∅} x → {a : α | f a = ∅} ∈ 𝓝 x
Tactic: simp only [← isOpen_compl_iff, compl_setOf, not_nonempty_iff_eq_empty, isOpen_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
hf : UpperHemicontinuous f
x : α
⊢ Membership.mem (γ := Set α) {a : α | f a = ∅} x → {a : α | f a = ∅} ∈ 𝓝 x
have f₁ : ∀ (hx : f x = ∅), {a : α | f a = ∅} ∈ 𝓝 x
Tactic: (hx : f x = ∅)
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (hypothesis)
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
hf : UpperHemicontinuous f
x : α
hx : f x = ∅
⊢ {a : α | f a = ∅} ∈ 𝓝 x
have hf₁ : ∀ (x : α), ∀ t ∈ 𝓝ˢ (f x), ∀ᶠ (x' : α) in 𝓝 x, t ∈ 𝓝ˢ (f x')
Tactic: simp_rw [upperHemicontinuous_iff, upperHemicontinuousAt_iff] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
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₀
have refine : ∀ (t : Set β) (ht : IsClosed[inst_1] t) (hft : ∃ᶠ (x' : α) in 𝓝 x₀, (f x' ∩ t).Nonempty), (f x₀ ∩ t).Nonempty
Tactic: refine .of_frequently fun t ht hft ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
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
⊢ (f x₀ ∩ t).Nonempty
have obtain : ∀ (x : ℕ → α) (hx : Tendsto x atTop (𝓝 x₀)) (hfx : ∀ (n : ℕ), (f (x n) ∩ t).Nonempty), (f x₀ ∩ t).Nonempty
Tactic: obtain ⟨x, hx, hfx⟩ := exists_seq_forall_of_frequently hft
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
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
⊢ (f x₀ ∩ t).Nonempty
have choose : ∀ (y : (n : ℕ) → β) (hy : ∀ (n : ℕ), y n ∈ f (x n) ∩ t), (f x₀ ∩ t).Nonempty
Tactic: choose y hy using hfx
Cleared hypotheses: hfx
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
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
have refine : ∀ᶠ (x : ℕ) in atTop, y x ∈ K
Tactic: refine Eventually.frequently ?_
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
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
⊢ ∀ᶠ (x : ℕ) in atTop, y x ∈ K
have h₁ : ∀ (n : ℕ) (hn : n ∈ x ⁻¹' {x : α | f x ⊆ K}), y n ∈ K
Tactic: filter_upwards [hx hf] with n hn
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
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
⊢ (f x₀ ∩ t).Nonempty
have obtain : ∀ (y₀ : β) (hy₀ : y₀ ∈ K) (φ : ℕ → ℕ) (hφ : StrictMono φ) (hyφ : Tendsto (y ∘ φ) atTop (𝓝 y₀)), (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
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (hypothesis)
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₀)
⊢ (f x₀ ∩ t).Nonempty
have h₁ : y₀ ∈ f x₀
Tactic: specialize h (x ∘ φ) (hx.comp hφ.tendsto_atTop) (y ∘ φ) (fun n ↦ (hy _).1) _ hyφ
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
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₀)
⊢ y₀ ∈ f x₀
have by_contra : ∀ (this : y₀ ∉ f x₀), False
Tactic: by_contra
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
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₀
⊢ False
have obtain : ∀ (s : Set β) (hs : s ∈ 𝓝ˢ (f x₀)) (t : Set β) (ht : t ∈ 𝓝 y₀) (hst : Disjoint s t), False
Tactic: obtain ⟨s, hs, t, ht, hst⟩ := Filter.disjoint_iff.mp <| RegularSpace.regular hf_closed this
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
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_1 : y₀ ∉ f x₀
s : Set β
hs : s ∈ 𝓝ˢ (f x₀)
t : Set β
ht : t ∈ 𝓝 y₀
hst : Disjoint s t
this : ∃ᶠ (n : ι) in l, y n ∈ s
⊢ False
have apply : ∀ᶠ (x : ι) in l, ¬(fun (n : ι) ↦ y n ∈ s) x
Tactic: apply this
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
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_1 : y₀ ∉ f x₀
s : Set β
hs : s ∈ 𝓝ˢ (f x₀)
t : Set β
ht : t ∈ 𝓝 y₀
hst : Disjoint s t
this : ∃ᶠ (n : ι) in l, y n ∈ s
⊢ ∀ᶠ (x : ι) in l, ¬(fun (n : ι) ↦ y n ∈ s) x
have h : ∀ (n : ι) (hn : n ∈ y ⁻¹' t) (hyn : y n ∈ s), False
Tactic: filter_upwards [hy₀ ht] with n hn hyn
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
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₀
s : Set β
hs : s ∈ 𝓝ˢ (f x₀)
t : Set β
ht : t ∈ 𝓝 y₀
hst : Disjoint s t
⊢ False
have suffices : ∃ᶠ (n : ι) in l, y n ∈ s
Tactic: suffices ∃ᶠ n in l, y n ∈ s by
    apply this
    filter_upwards [hy₀ ht] with n hn hyn
    exact hst.notMem_of_mem_left hyn hn
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
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₀
s : Set β
hs : s ∈ 𝓝ˢ (f x₀)
t : Set β
ht : t ∈ 𝓝 y₀
hst : Disjoint s t
⊢ ∃ᶠ (n : ι) in l, y n ∈ s
have apply : ∀ᶠ (x_1 : ι) in l, y x_1 ∈ f (x x_1) → y x_1 ∈ s
Tactic: apply hy.mp
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
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₀
s : Set β
hs : s ∈ 𝓝ˢ (f x₀)
t : Set β
ht : t ∈ 𝓝 y₀
hst : Disjoint s t
⊢ ∀ᶠ (x_1 : ι) in l, y x_1 ∈ f (x x_1) → y x_1 ∈ s
have h : ∀ (n : ι) (hn : n ∈ x ⁻¹' {x : α | s ∈ 𝓝ˢ (f x)}) (hyn : y n ∈ f (x n)), y n ∈ s
Tactic: filter_upwards [hx (hf s hs)] with n hn hyn
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (hypothesis)
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₀
s : Set β
hs : s ∈ 𝓝ˢ (f x₀)
t : Set β
ht : t ∈ 𝓝 y₀
hst : Disjoint s t
n : ι
hn : n ∈ x ⁻¹' {x : α | s ∈ 𝓝ˢ (f x)}
hyn : y n ∈ f (x n)
⊢ y n ∈ s
have hn₁ : f (x n) ⊆ interior s
Tactic: simp only [← subset_interior_iff_mem_nhdsSet, preimage_setOf_eq, mem_setOf_eq] at hn
Cleared hypotheses: hn