awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
x : α
⊢ LowerSemicontinuousWithinAt f univ x ↔ LowerSemicontinuousAt 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 : Preorder β
f : α → β
x : α
s : Set α
h : LowerSemicontinuousAt f x
⊢ LowerSemicontinuousWithinAt 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 : Preorder β
f : α → β
x : α
s : Set α
h : LowerSemicontinuousOn f s
hx : x ∈ s
⊢ LowerSemicontinuousWithinAt f s x

Tactic:
h.semicontinuousWithinAt hx

Premises used: SemicontinuousOn.semicontinuousWithinAt
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
s t : Set α
h : LowerSemicontinuousOn f s
hst : t ⊆ s
⊢ LowerSemicontinuousOn 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 : Preorder β
f : α → β
⊢ LowerSemicontinuousOn f univ ↔ LowerSemicontinuous 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 : Preorder β
f : α → β
s : Set α
⊢ LowerSemicontinuous (s.restrict (π := fun (a : α) ↦ β) f) ↔ LowerSemicontinuousOn f s

Tactic:
semicontinuous_restrict_iff (r := (f · > ·))

Premises used: semicontinuous_restrict_iff, Set.restrict
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
h : LowerSemicontinuous f
x : α
⊢ LowerSemicontinuousAt f x

Tactic:
h x
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
h : LowerSemicontinuous f
s : Set α
x : α
⊢ LowerSemicontinuousWithinAt 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 : Preorder β
f : α → β
h : LowerSemicontinuous f
s : Set α
⊢ LowerSemicontinuousOn 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 : Preorder β
x : α
s : Set α
z : β
⊢ LowerSemicontinuousWithinAt.{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 : Preorder β
x : α
z : β
⊢ LowerSemicontinuousAt.{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 : Preorder β
s : Set α
z : β
⊢ LowerSemicontinuousOn.{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 : Preorder β
z : β
⊢ LowerSemicontinuous.{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 : Preorder β
f : α → β
s : Set α
g : γ → α
x : γ
t : Set γ
hf : LowerSemicontinuousWithinAt f s (g x)
hg : ContinuousWithinAt g t x
hg' : MapsTo g t s
⊢ LowerSemicontinuousWithinAt (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 : Preorder β
f : α → β
g : γ → α
x : γ
hf : LowerSemicontinuousAt f (g x)
hg : ContinuousAt g x
⊢ LowerSemicontinuousAt (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 : Preorder β
f : α → β
s : Set α
g : γ → α
t : Set γ
hf : LowerSemicontinuousOn f s
hg : ContinuousOn g t
hg' : MapsTo g t s
⊢ LowerSemicontinuousOn (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 : Preorder β
f : α → β
g : γ → α
hf : LowerSemicontinuous f
hg : Continuous[inst_1, inst] g
⊢ LowerSemicontinuous (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 : Preorder β
f : α → β
x : α
s t : Set α
h : UpperSemicontinuousWithinAt f s x
hst : t ⊆ s
⊢ UpperSemicontinuousWithinAt 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 : Preorder β
f g : α → β
s : Set α
a : α
h : UpperSemicontinuousWithinAt f s a
has : a ∈ s
hfg : ∀ᶠ (x : α) in 𝓝[s] a, f x = g x
⊢ UpperSemicontinuousWithinAt g s a

Tactic:
LowerSemicontinuousWithinAt.congr_of_eventuallyEq (β := βᵒᵈ) h has hfg

Premises used: LowerSemicontinuousWithinAt.congr_of_eventuallyEq, OrderDual
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
x : α
⊢ UpperSemicontinuousWithinAt f univ x ↔ UpperSemicontinuousAt 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 : Preorder β
f : α → β
s : Set α
⊢ UpperSemicontinuous (s.restrict (π := fun (a : α) ↦ β) f) ↔ UpperSemicontinuousOn f s

Tactic:
lowerSemicontinuous_restrict_iff (β := βᵒᵈ)

Premises used: lowerSemicontinuous_restrict_iff, OrderDual
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
x : α
s : Set α
h : UpperSemicontinuousAt f x
⊢ UpperSemicontinuousWithinAt 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 : Preorder β
f : α → β
x : α
s : Set α
h : UpperSemicontinuousOn f s
hx : x ∈ s
⊢ UpperSemicontinuousWithinAt f s x

Tactic:
h x hx
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
s t : Set α
h : UpperSemicontinuousOn f s
hst : t ⊆ s
⊢ UpperSemicontinuousOn 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 : Preorder β
f : α → β
⊢ UpperSemicontinuousOn f univ ↔ UpperSemicontinuous 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 : Preorder β
f : α → β
h : UpperSemicontinuous f
x : α
⊢ UpperSemicontinuousAt f x

Tactic:
h x
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
h : UpperSemicontinuous f
s : Set α
x : α
⊢ UpperSemicontinuousWithinAt 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 : Preorder β
f : α → β
h : UpperSemicontinuous f
s : Set α
⊢ UpperSemicontinuousOn 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 : Preorder β
x : α
s : Set α
z : β
⊢ UpperSemicontinuousWithinAt.{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 : Preorder β
x : α
z : β
⊢ UpperSemicontinuousAt.{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 : Preorder β
s : Set α
z : β
⊢ UpperSemicontinuousOn.{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 : Preorder β
z : β
⊢ UpperSemicontinuous.{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 : Preorder β
f : α → β
s : Set α
g : γ → α
c : γ
t : Set γ
hf : UpperSemicontinuousWithinAt f s (g c)
hg : ContinuousWithinAt g t c
hg' : MapsTo g t s
⊢ UpperSemicontinuousWithinAt (f ∘ g) t c

Tactic:
SemicontinuousWithinAt.comp (r := (f · < ·)) 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 : Preorder β
f : α → β
g : γ → α
c : γ
hf : UpperSemicontinuousAt f (g c)
hg : ContinuousAt g c
⊢ UpperSemicontinuousAt (f ∘ g) c

Tactic:
SemicontinuousAt.comp (r := (f · < ·)) 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 : Preorder β
f : α → β
s : Set α
g : γ → α
t : Set γ
hf : UpperSemicontinuousOn f s
hg : ContinuousOn g t
hg' : MapsTo g t s
⊢ UpperSemicontinuousOn (f ∘ g) t

Tactic:
SemicontinuousOn.comp (r := (f · < ·)) 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 : Preorder β
f : α → β
g : γ → α
hf : UpperSemicontinuous f
hg : Continuous[inst_1, inst] g
⊢ UpperSemicontinuous (f ∘ g)

Tactic:
Semicontinuous.comp (r := (f · < ·)) hf hg

Premises used: Semicontinuous.comp
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder β
f : α → β
x : α
s : Set α
⊢ LowerSemicontinuousWithinAt f s x ↔ ∀ (y : β), (∃ᶠ (x' : α) in 𝓝[s] x, f x' ≤ y) → f x ≤ y

Tactic:
simp [semicontinuousWithinAt_iff_frequently]

Premises used: semicontinuousWithinAt_iff_frequently
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder β
f : α → β
s : Set α
⊢ LowerSemicontinuousOn f s ↔ ∀ x ∈ s, ∀ (y : β), (∃ᶠ (x' : α) in 𝓝[s] x, f x' ≤ y) → f x ≤ y

Tactic:
simp [semicontinuousOn_iff_frequently]

Premises used: semicontinuousOn_iff_frequently
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder β
f : α → β
x : α
⊢ LowerSemicontinuousAt f x ↔ ∀ (y : β), (∃ᶠ (x' : α) in 𝓝 x, f x' ≤ y) → f x ≤ y

Tactic:
simp [semicontinuousAt_iff_frequently]

Premises used: semicontinuousAt_iff_frequently
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder β
f : α → β
⊢ LowerSemicontinuous f ↔ ∀ (x : α) (y : β), (∃ᶠ (x' : α) in 𝓝 x, f x' ≤ y) → f x ≤ y

Tactic:
simp [semicontinuous_iff_frequently]

Premises used: semicontinuous_iff_frequently
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder β
f : α → β
x : α
s : Set α
⊢ UpperSemicontinuousWithinAt f s x ↔ ∀ (y : β), (∃ᶠ (x' : α) in 𝓝[s] x, f x' ≥ y) → f x ≥ y

Tactic:
simp [semicontinuousWithinAt_iff_frequently]

Premises used: semicontinuousWithinAt_iff_frequently
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder β
f : α → β
s : Set α
⊢ UpperSemicontinuousOn f s ↔ ∀ x ∈ s, ∀ (y : β), (∃ᶠ (x' : α) in 𝓝[s] x, f x' ≥ y) → f x ≥ y

Tactic:
simp [semicontinuousOn_iff_frequently]

Premises used: semicontinuousOn_iff_frequently
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder β
f : α → β
x : α
⊢ UpperSemicontinuousAt f x ↔ ∀ (y : β), (∃ᶠ (x' : α) in 𝓝 x, f x' ≥ y) → f x ≥ y

Tactic:
simp [semicontinuousAt_iff_frequently]

Premises used: semicontinuousAt_iff_frequently
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder β
f : α → β
⊢ UpperSemicontinuous f ↔ ∀ (x : α) (y : β), (∃ᶠ (x' : α) in 𝓝 x, f x' ≥ y) → f x ≥ y

Tactic:
simp [semicontinuous_iff_frequently]

Premises used: semicontinuous_iff_frequently
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
x : α
⊢ LowerHemicontinuousWithinAt f s x ↔
    ∀ (u : Set β), IsOpen[inst_1] u → (f x ∩ u).Nonempty → ∀ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ u).Nonempty

Tactic:
simp +contextual [SemicontinuousWithinAt]

Premises used: SemicontinuousWithinAt
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
⊢ LowerHemicontinuousOn f s ↔ ∀ x ∈ s, LowerHemicontinuousWithinAt f s x

Tactic:
Iff.rfl

Premises used: Iff.rfl, SemicontinuousOn
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
⊢ LowerHemicontinuousAt f x ↔
    ∀ (u : Set β), IsOpen[inst_1] u → (f x ∩ u).Nonempty → ∀ᶠ (x' : α) in 𝓝 x, (f x' ∩ u).Nonempty

Tactic:
simp +contextual [SemicontinuousAt]

Premises used: SemicontinuousAt
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
⊢ LowerHemicontinuous f ↔ ∀ (x : α), LowerHemicontinuousAt f x

Tactic:
Iff.rfl

Premises used: Iff.rfl, Semicontinuous
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
x : α
⊢ UpperHemicontinuousWithinAt f s x ↔ ∀ t ∈ 𝓝ˢ (f x), ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (f x')

Tactic:
Iff.rfl

Premises used: Iff.rfl, SemicontinuousWithinAt
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
⊢ UpperHemicontinuousOn f s ↔ ∀ x ∈ s, UpperHemicontinuousWithinAt f s x

Tactic:
Iff.rfl

Premises used: Iff.rfl, SemicontinuousOn
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
⊢ UpperHemicontinuousAt f x ↔ ∀ t ∈ 𝓝ˢ (f x), ∀ᶠ (x' : α) in 𝓝 x, t ∈ 𝓝ˢ (f x')

Tactic:
Iff.rfl

Premises used: Iff.rfl, SemicontinuousAt
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
⊢ UpperHemicontinuous f ↔ ∀ (x : α), UpperHemicontinuousAt f x

Tactic:
Iff.rfl

Premises used: Iff.rfl, Semicontinuous
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
s t : Set α
h : LowerHemicontinuousWithinAt f s x
hst : t ⊆ s
⊢ LowerHemicontinuousWithinAt 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 : LowerHemicontinuousWithinAt f s a
has : a ∈ s
hfg : f =ᶠ[𝓝[s] a] g
h₁ :
  ∀ (x : α) (hx : f x = g x) (y : Set β), IsOpen[inst_1] y ∧ (f x ∩ y).Nonempty ↔ IsOpen[inst_1] y ∧ (g x ∩ y).Nonempty
⊢ ∀ᶠ (x : α) in 𝓝[s] a, ∀ (y : Set β), IsOpen[inst_1] y ∧ (f x ∩ y).Nonempty ↔ IsOpen[inst_1] y ∧ (g x ∩ y).Nonempty

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 : LowerHemicontinuousWithinAt f s a
has : a ∈ s
hfg : f =ᶠ[𝓝[s] a] g
x : α
hx : f x = g x
⊢ ∀ (y : Set β), IsOpen[inst_1] y ∧ (f x ∩ y).Nonempty ↔ IsOpen[inst_1] y ∧ (g x ∩ y).Nonempty

Tactic:
simp [hx]
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
⊢ LowerHemicontinuousWithinAt f univ x ↔ LowerHemicontinuousAt 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 β
x : α
s : Set α
h : LowerHemicontinuousAt f x
⊢ LowerHemicontinuousWithinAt 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 : LowerHemicontinuousOn f s
hx : x ∈ s
⊢ LowerHemicontinuousWithinAt f s x

Tactic:
h.semicontinuousWithinAt hx

Premises used: SemicontinuousOn.semicontinuousWithinAt
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s t : Set α
h : LowerHemicontinuousOn f s
hst : t ⊆ s
⊢ LowerHemicontinuousOn 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 β
⊢ LowerHemicontinuousOn f univ ↔ LowerHemicontinuous 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 β
s : Set α
⊢ LowerHemicontinuous (s.restrict (π := fun (a : α) ↦ Set β) f) ↔ LowerHemicontinuousOn f s

Tactic:
semicontinuous_restrict_iff (r := (fun x t ↦ IsOpen t ∧ ((f x) ∩ t).Nonempty))

Premises used: semicontinuous_restrict_iff, Set.restrict
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
h : LowerHemicontinuous f
x : α
⊢ LowerHemicontinuousAt 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 : LowerHemicontinuous f
s : Set α
x : α
⊢ LowerHemicontinuousWithinAt 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 : LowerHemicontinuous f
s : Set α
⊢ LowerHemicontinuousOn 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 β), IsOpen[inst_1] x_1ᶜ → (f x ∩ x_1ᶜ).Nonempty → ∀ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ x_1ᶜ).Nonempty) ↔
    ∀ (t : Set β), IsClosed[inst_1] t → (∃ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ t) → f x ⊆ t
⊢ LowerHemicontinuousWithinAt f s x ↔ ∀ (t : Set β), IsClosed[inst_1] t → (∃ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ t) → f x ⊆ t

Tactic:
rw [lowerHemicontinuousWithinAt_iff, compl_surjective.forall]

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

Tactic:
simp only [isOpen_compl_iff]

Premises used: isOpen_compl_iff
-- 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 β), IsClosed[inst_1] x_1 → (f x ∩ x_1ᶜ).Nonempty → ∀ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ x_1ᶜ).Nonempty) ↔
    ∀ (t : Set β), IsClosed[inst_1] t → (∃ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ t) → f x ⊆ t

Tactic:
forall₂_congr fun t ht ↦ ?_

Premises used: forall₂_congr
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
s : Set α
refine :
  ∀ (t : Set β) (ht : IsClosed[inst_1] t),
    ((f x ∩ tᶜ).Nonempty → ∀ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ tᶜ).Nonempty) ↔ (∃ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ t) → f x ⊆ t
⊢ (∀ (x_1 : Set β), IsClosed[inst_1] x_1 → (f x ∩ x_1ᶜ).Nonempty → ∀ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ x_1ᶜ).Nonempty) ↔
    ∀ (t : Set β), IsClosed[inst_1] t → (∃ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ t) → f x ⊆ t

Tactic:
refine forall₂_congr fun t ht ↦ ?_

Premises used: forall₂_congr
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
s : Set α
t : Set β
ht : IsClosed[inst_1] t
rw : (¬∀ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ tᶜ).Nonempty) → ¬(f x ∩ tᶜ).Nonempty ↔ (∃ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ t) → f x ⊆ t
⊢ ((f x ∩ tᶜ).Nonempty → ∀ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ tᶜ).Nonempty) ↔ (∃ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ t) → f x ⊆ t

Tactic:
rw [← not_imp_not]

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

Tactic:
simp [not_nonempty_iff_eq_empty, ← disjoint_iff_inter_eq_empty, disjoint_compl_right_iff_subset]

Premises used: Set.not_nonempty_iff_eq_empty, Set.disjoint_compl_right_iff_subset, Set.disjoint_iff_inter_eq_empty