awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
rw :
  (∀ (t : Set β), IsClosed[inst_1] t → (∃ᶠ (x' : α) in 𝓝[univ] x, f x' ⊆ t) → f x ⊆ t) ↔
    ∀ (t : Set β), IsClosed[inst_1] t → (∃ᶠ (x' : α) in 𝓝 x, f x' ⊆ t) → f x ⊆ t
⊢ LowerHemicontinuousAt f x ↔ ∀ (t : Set β), IsClosed[inst_1] t → (∃ᶠ (x' : α) in 𝓝 x, f x' ⊆ t) → f x ⊆ t

Tactic:
rw [← lowerHemicontinuousWithinAt_univ_iff, lowerHemicontinuousWithinAt_iff_frequently]

Premises used: lowerHemicontinuousWithinAt_iff_frequently, lowerHemicontinuousWithinAt_univ_iff
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
⊢ (∀ (t : Set β), IsClosed[inst_1] t → (∃ᶠ (x' : α) in 𝓝[univ] x, f x' ⊆ t) → f x ⊆ t) ↔
    ∀ (t : Set β), IsClosed[inst_1] t → (∃ᶠ (x' : α) in 𝓝 x, f x' ⊆ t) → f x ⊆ t

Tactic:
simp
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
s : Set α
z : Set β
⊢ LowerHemicontinuousWithinAt.{u_1, u_2} (β := β) (fun (_x : α) ↦ z) s x

Tactic:
SemicontinuousWithinAt.const

Premises used: SemicontinuousWithinAt.const
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
z : Set β
⊢ LowerHemicontinuousAt.{u_1, u_2} (β := β) (fun (_x : α) ↦ z) x

Tactic:
SemicontinuousAt.const

Premises used: SemicontinuousAt.const
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
z : Set β
⊢ LowerHemicontinuousOn.{u_1, u_2} (β := β) (fun (_x : α) ↦ z) s

Tactic:
SemicontinuousOn.const

Premises used: SemicontinuousOn.const
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
z : Set β
⊢ LowerHemicontinuous.{u_1, u_2} (β := β) fun (_x : α) ↦ z

Tactic:
Semicontinuous.const

Premises used: Semicontinuous.const
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace γ
inst_2 : TopologicalSpace β
f : α → Set β
s : Set α
g : γ → α
x : γ
t : Set γ
hf : LowerHemicontinuousWithinAt f s (g x)
hg : ContinuousWithinAt g t x
hg' : MapsTo g t s
⊢ LowerHemicontinuousWithinAt (f ∘ g) t x

Tactic:
SemicontinuousWithinAt.comp hf hg hg'

Premises used: SemicontinuousWithinAt.comp
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace γ
inst_2 : TopologicalSpace β
f : α → Set β
g : γ → α
x : γ
hf : LowerHemicontinuousAt f (g x)
hg : ContinuousAt g x
⊢ LowerHemicontinuousAt (f ∘ g) x

Tactic:
SemicontinuousAt.comp hf hg

Premises used: SemicontinuousAt.comp
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace γ
inst_2 : TopologicalSpace β
f : α → Set β
s : Set α
g : γ → α
t : Set γ
hf : LowerHemicontinuousOn f s
hg : ContinuousOn g t
hg' : MapsTo g t s
⊢ LowerHemicontinuousOn (f ∘ g) t

Tactic:
SemicontinuousOn.comp hf hg hg'

Premises used: SemicontinuousOn.comp
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace γ
inst_2 : TopologicalSpace β
f : α → Set β
g : γ → α
hf : LowerHemicontinuous f
hg : Continuous[inst_1, inst] g
⊢ LowerHemicontinuous (f ∘ g)

Tactic:
Semicontinuous.comp hf hg

Premises used: Semicontinuous.comp
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
s t : Set α
h : UpperHemicontinuousWithinAt f s x
hst : t ⊆ s
⊢ UpperHemicontinuousWithinAt f t x

Tactic:
SemicontinuousWithinAt.mono h hst

Premises used: SemicontinuousWithinAt.mono
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → Set β
s : Set α
a : α
h : UpperHemicontinuousWithinAt f s a
has : a ∈ s
hfg : ∀ᶠ (x : α) in 𝓝[s] a, f x = g x
h₁ : ∀ (x : α) (hx : f x = g x) (y : Set β), y ∈ 𝓝ˢ (f x) ↔ y ∈ 𝓝ˢ (g x)
⊢ ∀ᶠ (x : α) in 𝓝[s] a, ∀ (y : Set β), y ∈ 𝓝ˢ (f x) ↔ y ∈ 𝓝ˢ (g x)

Tactic:
filter_upwards [hfg] with x hx
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → Set β
s : Set α
a : α
h : UpperHemicontinuousWithinAt f s a
has : a ∈ s
hfg : ∀ᶠ (x : α) in 𝓝[s] a, f x = g x
x : α
hx : f x = g x
⊢ ∀ (y : Set β), y ∈ 𝓝ˢ (f x) ↔ y ∈ 𝓝ˢ (g x)

Tactic:
simp [hx]
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
⊢ UpperHemicontinuousWithinAt f univ x ↔ UpperHemicontinuousAt f x

Tactic:
semicontinuousWithinAt_univ_iff

Premises used: semicontinuousWithinAt_univ_iff
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
⊢ UpperHemicontinuous (s.restrict (π := fun (a : α) ↦ Set β) f) ↔ UpperHemicontinuousOn f s

Tactic:
semicontinuous_restrict_iff (r := (fun x t ↦ t ∈ 𝓝ˢ (f x)))

Premises used: Set.Mem, setOf, semicontinuous_restrict_iff, Set.restrict
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
s : Set α
h : UpperHemicontinuousAt f x
⊢ UpperHemicontinuousWithinAt f s x

Tactic:
h.semicontinuousWithinAt s

Premises used: SemicontinuousAt.semicontinuousWithinAt
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
s : Set α
h : UpperHemicontinuousOn f s
hx : x ∈ s
⊢ UpperHemicontinuousWithinAt f s x

Tactic:
h x hx
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s t : Set α
h : UpperHemicontinuousOn f s
hst : t ⊆ s
⊢ UpperHemicontinuousOn f t

Tactic:
SemicontinuousOn.mono h hst

Premises used: SemicontinuousOn.mono
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
⊢ UpperHemicontinuousOn f univ ↔ UpperHemicontinuous f

Tactic:
semicontinuousOn_univ_iff

Premises used: semicontinuousOn_univ_iff
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
h : UpperHemicontinuous f
x : α
⊢ UpperHemicontinuousAt f x

Tactic:
h x
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
h : UpperHemicontinuous f
s : Set α
x : α
⊢ UpperHemicontinuousWithinAt f s x

Tactic:
(h x).semicontinuousWithinAt s

Premises used: SemicontinuousAt.semicontinuousWithinAt
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
h : UpperHemicontinuous f
s : Set α
⊢ UpperHemicontinuousOn f s

Tactic:
h.semicontinuousOn s

Premises used: Semicontinuous.semicontinuousOn
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
s : Set α
rw :
  (∀ (x_1 : Set β), (∃ᶠ (x' : α) in 𝓝[s] x, x_1ᶜ ∉ 𝓝ˢ (f x')) → x_1ᶜ ∉ 𝓝ˢ (f x)) ↔
    ∀ (t : Set β), IsClosed[inst_1] t → (∃ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty
⊢ UpperHemicontinuousWithinAt f s x ↔
    ∀ (t : Set β), IsClosed[inst_1] t → (∃ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty

Tactic:
rw [UpperHemicontinuousWithinAt, semicontinuousWithinAt_iff_frequently, compl_surjective.forall]

Premises used: Function.Surjective.forall, semicontinuousWithinAt_iff_frequently, compl_surjective, UpperHemicontinuousWithinAt
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
s : Set α
⊢ (∀ (x_1 : Set β), (∃ᶠ (x' : α) in 𝓝[s] x, x_1ᶜ ∉ 𝓝ˢ (f x')) → x_1ᶜ ∉ 𝓝ˢ (f x)) ↔
    ∀ (t : Set β), IsClosed[inst_1] t → (∃ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty

Tactic:
simp [← subset_interior_iff_mem_nhdsSet, not_subset, forall_isClosed_iff, inter_nonempty]

Premises used: Set.inter_nonempty, forall_isClosed_iff, subset_interior_iff_mem_nhdsSet, Set.not_subset
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
rw :
  (∀ (t : Set β), IsClosed[inst_1] t → (∃ᶠ (x' : α) in 𝓝[univ] x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty) ↔
    ∀ (t : Set β), IsClosed[inst_1] t → (∃ᶠ (x' : α) in 𝓝 x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty
⊢ UpperHemicontinuousAt f x ↔
    ∀ (t : Set β), IsClosed[inst_1] t → (∃ᶠ (x' : α) in 𝓝 x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty

Tactic:
rw [← upperHemicontinuousWithinAt_univ_iff, upperHemicontinuousWithinAt_iff_frequently]

Premises used: upperHemicontinuousWithinAt_iff_frequently, upperHemicontinuousWithinAt_univ_iff
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
⊢ (∀ (t : Set β), IsClosed[inst_1] t → (∃ᶠ (x' : α) in 𝓝[univ] x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty) ↔
    ∀ (t : Set β), IsClosed[inst_1] t → (∃ᶠ (x' : α) in 𝓝 x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty

Tactic:
simp
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
s : Set α
z : Set β
⊢ UpperHemicontinuousWithinAt.{u_1, u_2} (β := β) (fun (_x : α) ↦ z) s x

Tactic:
SemicontinuousWithinAt.const

Premises used: Set.Mem, SemicontinuousWithinAt.const, setOf
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
z : Set β
⊢ UpperHemicontinuousAt.{u_1, u_2} (β := β) (fun (_x : α) ↦ z) x

Tactic:
SemicontinuousAt.const

Premises used: Set.Mem, setOf, SemicontinuousAt.const
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
z : Set β
⊢ UpperHemicontinuousOn.{u_1, u_2} (β := β) (fun (_x : α) ↦ z) s

Tactic:
SemicontinuousOn.const

Premises used: Set.Mem, setOf, SemicontinuousOn.const
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
z : Set β
⊢ UpperHemicontinuous.{u_1, u_2} (β := β) fun (_x : α) ↦ z

Tactic:
Semicontinuous.const

Premises used: Set.Mem, setOf, Semicontinuous.const
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace γ
inst_2 : TopologicalSpace β
f : α → Set β
s : Set α
g : γ → α
c : γ
t : Set γ
hf : UpperHemicontinuousWithinAt f s (g c)
hg : ContinuousWithinAt g t c
hg' : MapsTo g t s
⊢ UpperHemicontinuousWithinAt (f ∘ g) t c

Tactic:
SemicontinuousWithinAt.comp (r := (fun x t ↦ t ∈ 𝓝ˢ (f x))) hf hg hg'

Premises used: Set.Mem, setOf, SemicontinuousWithinAt.comp
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace γ
inst_2 : TopologicalSpace β
f : α → Set β
s : Set α
g : γ → α
t : Set γ
hf : UpperHemicontinuousOn f s
hg : ContinuousOn g t
hg' : MapsTo g t s
⊢ UpperHemicontinuousOn (f ∘ g) t

Tactic:
SemicontinuousOn.comp (r := (fun x t ↦ t ∈ 𝓝ˢ (f x))) hf hg hg'

Premises used: Set.Mem, setOf, SemicontinuousOn.comp
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace γ
inst_2 : TopologicalSpace β
f : α → Set β
g : γ → α
hf : UpperHemicontinuous f
hg : Continuous[inst_1, inst] g
⊢ UpperHemicontinuous (f ∘ g)

Tactic:
Semicontinuous.comp (r := (fun x t ↦ t ∈ 𝓝ˢ (f x))) hf hg

Premises used: Set.Mem, setOf, Semicontinuous.comp
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
x : α
rw :
  (∀ (i : Set β), IsOpen[inst_1] i ∧ f x ⊆ i → ∀ᶠ (x' : α) in 𝓝[s] x, i ∈ 𝓝ˢ (f x')) ↔
    ∀ (u : Set β), IsOpen[inst_1] u → f x ⊆ u → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ u
rw₁ : ∀ ⦃s_1 t : Set β⦄, s_1 ⊆ t → (∀ᶠ (x' : α) in 𝓝[s] x, s_1 ∈ 𝓝ˢ (f x')) → ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (f x')
⊢ UpperHemicontinuousWithinAt f s x ↔ ∀ (u : Set β), IsOpen[inst_1] u → f x ⊆ u → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ u

Tactic:
rw [upperHemicontinuousWithinAt_iff, hasBasis_nhdsSet _ |>.forall_iff ?mono]

Premises used: hasBasis_nhdsSet, upperHemicontinuousWithinAt_iff, Filter.HasBasis.forall_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
x : α
t₁ t₂ : Set β
ht : t₁ ⊆ t₂
h : ∀ᶠ (x' : α) in 𝓝[s] x, t₁ ∈ 𝓝ˢ (f x')
x' : α
⊢ t₁ ∈ 𝓝ˢ (f x') → t₂ ∈ 𝓝ˢ (f x')

Tactic:
gcongr
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
x : α
⊢ ∀ ⦃s_1 t : Set β⦄, s_1 ⊆ t → (∀ᶠ (x' : α) in 𝓝[s] x, s_1 ∈ 𝓝ˢ (f x')) → ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (f x')

Tactic:
exact fun t₁ t₂ ht h ↦ h.mp <| .of_forall fun x' ↦ by gcongr
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
x : α
⊢ ∀ ⦃s_1 t : Set β⦄, s_1 ⊆ t → (∀ᶠ (x' : α) in 𝓝[s] x, s_1 ∈ 𝓝ˢ (f x')) → ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (f x')

Tactic:
case mono => exact fun t₁ t₂ ht h ↦ h.mp <| .of_forall fun x' ↦ by gcongr
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
x : α
simp :
  (∀ (i : Set β), IsOpen[inst_1] i → f x ⊆ i → ∀ᶠ (x' : α) in 𝓝[s] x, i ∈ 𝓝ˢ (f x')) ↔
    ∀ (u : Set β), IsOpen[inst_1] u → f x ⊆ u → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ u
⊢ (∀ (i : Set β), IsOpen[inst_1] i ∧ f x ⊆ i → ∀ᶠ (x' : α) in 𝓝[s] x, i ∈ 𝓝ˢ (f x')) ↔
    ∀ (u : Set β), IsOpen[inst_1] u → f x ⊆ u → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ u

Tactic:
simp only [and_imp]

Premises used: and_imp
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
x : α
h :
  ∀ (a : Set β) (b : IsOpen[inst_1] a),
    (f x ⊆ a → ∀ᶠ (x' : α) in 𝓝[s] x, a ∈ 𝓝ˢ (f x')) ↔ f x ⊆ a → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ a
⊢ (∀ (i : Set β), IsOpen[inst_1] i → f x ⊆ i → ∀ᶠ (x' : α) in 𝓝[s] x, i ∈ 𝓝ˢ (f x')) ↔
    ∀ (u : Set β), IsOpen[inst_1] u → f x ⊆ u → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ u

Tactic:
apply forall₂_congr

Premises used: forall₂_congr
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
x : α
⊢ ∀ (a : Set β) (b : IsOpen[inst_1] a),
    (f x ⊆ a → ∀ᶠ (x' : α) in 𝓝[s] x, a ∈ 𝓝ˢ (f x')) ↔ f x ⊆ a → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ a

Tactic:
simp +contextual [← subset_interior_iff_mem_nhdsSet, IsOpen.interior_eq]

Premises used: subset_interior_iff_mem_nhdsSet, IsOpen.interior_eq
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
⊢ UpperHemicontinuousOn f s ↔ ∀ x ∈ s, ∀ (u : Set β), IsOpen[inst_1] u → f x ⊆ u → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ u

Tactic:
simp [upperHemicontinuousOn_iff, upperHemicontinuousWithinAt_iff_forall_isOpen]

Premises used: upperHemicontinuousWithinAt_iff_forall_isOpen, upperHemicontinuousOn_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
⊢ UpperHemicontinuousAt f x ↔ ∀ (u : Set β), IsOpen[inst_1] u → f x ⊆ u → ∀ᶠ (x' : α) in 𝓝 x, f x' ⊆ u

Tactic:
simpa [upperHemicontinuousWithinAt_univ_iff] using
    upperHemicontinuousWithinAt_iff_forall_isOpen (s := Set.univ)

Premises used: upperHemicontinuousWithinAt_iff_forall_isOpen, upperHemicontinuousWithinAt_univ_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
⊢ UpperHemicontinuous f ↔ ∀ (x : α) (u : Set β), IsOpen[inst_1] u → f x ⊆ u → ∀ᶠ (x' : α) in 𝓝 x, f x' ⊆ u

Tactic:
simp [upperHemicontinuous_iff, upperHemicontinuousAt_iff_forall_isOpen]

Premises used: upperHemicontinuousAt_iff_forall_isOpen, upperHemicontinuous_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
x : α
rw :
  (∀ (i : Set β), IsOpen[inst_1] i ∧ f x ⊆ i → ∀ᶠ (x' : α) in 𝓝[s] x, i ∈ 𝓝ˢ (f x')) ↔
    ∀ (i : Set β), IsOpen[inst_1] i ∧ f x ⊆ i → f ⁻¹' Iic i ∈ 𝓝[s] x
rw₁ : ∀ ⦃s_1 t : Set β⦄, s_1 ⊆ t → f ⁻¹' Iic s_1 ∈ 𝓝[s] x → f ⁻¹' Iic t ∈ 𝓝[s] x
rw₂ : ∀ ⦃s_1 t : Set β⦄, s_1 ⊆ t → (∀ᶠ (x' : α) in 𝓝[s] x, s_1 ∈ 𝓝ˢ (f x')) → ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (f x')
⊢ (∀ t ∈ 𝓝ˢ (f x), ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (f x')) ↔ ∀ u ∈ 𝓝ˢ (f x), f ⁻¹' Iic u ∈ 𝓝[s] x

Tactic:
rw [hasBasis_nhdsSet (f x) |>.forall_iff ?h₁, hasBasis_nhdsSet (f x) |>.forall_iff ?h₂]

Premises used: hasBasis_nhdsSet, Filter.HasBasis.forall_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s_1 : Set α
x : α
s t : Set β
hst : s ⊆ t
hxy : s ≤ t
⊢ f ⁻¹' Iic s ∈ 𝓝[s_1] x → f ⁻¹' Iic t ∈ 𝓝[s_1] x

Tactic:
gcongr
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s_1 : Set α
x : α
s t : Set β
hst : s ⊆ t
⊢ s ≤ t

Tactic:
hst
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s_1 : Set α
x : α
s t : Set β
hst : s ⊆ t
⊢ s ≤ t

Tactic:
exact hst
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
x : α
⊢ ∀ ⦃s_1 t : Set β⦄, s_1 ⊆ t → f ⁻¹' Iic s_1 ∈ 𝓝[s] x → f ⁻¹' Iic t ∈ 𝓝[s] x

Tactic:
case h₂ =>
    intro s t hst
    gcongr
    exact hst
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s_1 : Set α
x : α
s t : Set β
hst : s ⊆ t
⊢ (∀ᶠ (x' : α) in 𝓝[s_1] x, s ∈ 𝓝ˢ (f x')) → ∀ᶠ (x' : α) in 𝓝[s_1] x, t ∈ 𝓝ˢ (f x')

Tactic:
gcongr
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
x : α
⊢ ∀ ⦃s_1 t : Set β⦄, s_1 ⊆ t → (∀ᶠ (x' : α) in 𝓝[s] x, s_1 ∈ 𝓝ˢ (f x')) → ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (f x')

Tactic:
case h₁ =>
    intro s t hst
    gcongr
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
x : α
⊢ (∀ (i : Set β), IsOpen[inst_1] i ∧ f x ⊆ i → ∀ᶠ (x' : α) in 𝓝[s] x, i ∈ 𝓝ˢ (f x')) ↔
    ∀ (i : Set β), IsOpen[inst_1] i ∧ f x ⊆ i → f ⁻¹' Iic i ∈ 𝓝[s] x

Tactic:
forall₂_congr fun u ⟨hu, hfu⟩ ↦ ?_

Premises used: nhdsWithin, Filter.Eventually, Membership.mem, Iff, forall₂_congr, Set.preimage, _private.0.upperHemicontinuousWithinAt_iff_preimage_Iic.match_1, Set.Iic, nhdsSet
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
x : α
refine :
  ∀ (u : Set β),
    IsOpen[inst_1] u ∧ f x ⊆ u →
      ∀ (hu : IsOpen[inst_1] u) (hfu : f x ⊆ u), (∀ᶠ (x' : α) in 𝓝[s] x, u ∈ 𝓝ˢ (f x')) ↔ f ⁻¹' Iic u ∈ 𝓝[s] x
⊢ (∀ (i : Set β), IsOpen[inst_1] i ∧ f x ⊆ i → ∀ᶠ (x' : α) in 𝓝[s] x, i ∈ 𝓝ˢ (f x')) ↔
    ∀ (i : Set β), IsOpen[inst_1] i ∧ f x ⊆ i → f ⁻¹' Iic i ∈ 𝓝[s] x

Tactic:
refine forall₂_congr fun u ⟨hu, hfu⟩ ↦ ?_

Premises used: forall₂_congr
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
x : α
u : Set β
h : IsOpen[inst_1] u ∧ f x ⊆ u
hu : IsOpen[inst_1] u
hfu : f x ⊆ u
⊢ (∀ᶠ (x' : α) in 𝓝[s] x, u ∈ 𝓝ˢ (f x')) ↔ f ⁻¹' Iic u ∈ 𝓝[s] x

Tactic:
simp [hu.mem_nhdsSet, eventually_iff, Iic]

Premises used: Filter.eventually_iff, Set.Iic, IsOpen.mem_nhdsSet
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
⊢ UpperHemicontinuousAt f x ↔ ∀ u ∈ 𝓝ˢ (f x), f ⁻¹' Iic u ∈ 𝓝 x

Tactic:
simpa [upperHemicontinuousWithinAt_univ_iff] using
    upperHemicontinuousWithinAt_iff_preimage_Iic (s := univ)

Premises used: upperHemicontinuousWithinAt_iff_preimage_Iic, upperHemicontinuousWithinAt_univ_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
⊢ UpperHemicontinuousOn f s ↔ ∀ x ∈ s, ∀ u ∈ 𝓝ˢ (f x), f ⁻¹' Iic u ∈ 𝓝[s] x

Tactic:
simp [upperHemicontinuousOn_iff, upperHemicontinuousWithinAt_iff_preimage_Iic]

Premises used: upperHemicontinuousWithinAt_iff_preimage_Iic, upperHemicontinuousOn_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
⊢ UpperHemicontinuous f ↔ ∀ (x : α), ∀ u ∈ 𝓝ˢ (f x), f ⁻¹' Iic u ∈ 𝓝 x

Tactic:
simp [upperHemicontinuous_iff, upperHemicontinuousAt_iff_preimage_Iic]

Premises used: upperHemicontinuousAt_iff_preimage_Iic, upperHemicontinuous_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
simp_rw :
  (∀ (x : α), ∀ u ∈ 𝓝ˢ (f x), f ⁻¹' Iic u ∈ 𝓝 x) ↔
    ∀ (u : Set β), IsOpen[inst_1] u → ∀ x ∈ f ⁻¹' Iic u, f ⁻¹' Iic u ∈ 𝓝 x
⊢ UpperHemicontinuous f ↔ ∀ (u : Set β), IsOpen[inst_1] u → IsOpen[inst] (f ⁻¹' Iic u)

Tactic:
simp_rw [upperHemicontinuous_iff_preimage_Iic, isOpen_iff_mem_nhds (s := f ⁻¹' (Iic _))]

Premises used: upperHemicontinuous_iff_preimage_Iic, isOpen_iff_mem_nhds
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
enter : ∀ (x : α), ∀ u ∈ 𝓝ˢ (f x), f ⁻¹' Iic u ∈ 𝓝 x
| (∀ (x : α), ∀ u ∈ 𝓝ˢ (f x), f ⁻¹' Iic u ∈ 𝓝 x) ↔
    ∀ (u : Set β), IsOpen[inst_1] u → ∀ x ∈ f ⁻¹' Iic u, f ⁻¹' Iic u ∈ 𝓝 x

Tactic:
enter [1, x]
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
s t : Set β
hst : s ⊆ t
hxy : s ≤ t
⊢ f ⁻¹' Iic s ∈ 𝓝 x → f ⁻¹' Iic t ∈ 𝓝 x

Tactic:
gcongr
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
s t : Set β
hst : s ⊆ t
⊢ s ≤ t

Tactic:
hst
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
s t : Set β
hst : s ⊆ t
⊢ s ≤ t

Tactic:
exact hst