awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (l : γ), f x ≤ l
pos : ∀ (Hu : ∃ (u : γ), f x < u), f ⁻¹' v ∈ 𝓝[s] x
neg : ∀ (Hu : ∀ (u : γ), u ≤ f x), f ⁻¹' v ∈ 𝓝[s] x
⊢ f ⁻¹' v ∈ 𝓝[s] x

Tactic:
by_cases! Hu : ∃ u, f x < u
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (l : γ), f x ≤ l
Hu : ∃ (u : γ), f x < u
pos : ∀ (u : γ) (fxu : f x < u) (hu : Ico (f x) u ⊆ v), f ⁻¹' v ∈ 𝓝[s] x
⊢ f ⁻¹' v ∈ 𝓝[s] x

Tactic:
rcases exists_Ico_subset_of_mem_nhds hv Hu with ⟨u, fxu, hu⟩

Premises used: exists_Ico_subset_of_mem_nhds
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (l : γ), f x ≤ l
Hu : ∃ (u : γ), f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
h : ∀ (a : α) (lfa : f a < u), a ∈ f ⁻¹' v
⊢ f ⁻¹' v ∈ 𝓝[s] x

Tactic:
filter_upwards [h₂ u fxu] with a lfa
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (l : γ), f x ≤ l
Hu : ∃ (u : γ), f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
a : α
lfa : f a < u
h : f a ∈ Ico (f x) u
⊢ a ∈ f ⁻¹' v

Tactic:
apply hu
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (l : γ), f x ≤ l
Hu : ∃ (u : γ), f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
a : α
lfa : f a < u
⊢ f a ∈ Ico (f x) u

Tactic:
⟨Hl (f a), lfa⟩

Premises used: Set.Mem, setOf, Set.Ico, And.intro
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (l : γ), f x ≤ l
Hu : ∃ (u : γ), f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
a : α
lfa : f a < u
⊢ f a ∈ Ico (f x) u

Tactic:
exact ⟨Hl (f a), lfa⟩
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (l : γ), f x ≤ l
Hu : ∀ (u : γ), u ≤ f x
neg : ∀ (x : α), f x ∈ v
⊢ f ⁻¹' v ∈ 𝓝[s] x

Tactic:
apply Filter.Eventually.of_forall

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (l : γ), f x ≤ l
Hu : ∀ (u : γ), u ≤ f x
a : α
⊢ f a = f x

Tactic:
have : f a = f x := le_antisymm (Hu _) (Hl _)
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (l : γ), f x ≤ l
Hu : ∀ (u : γ), u ≤ f x
a : α
this : f a = f x
neg : f x ∈ v
⊢ f a ∈ v

Tactic:
rw [this]
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (l : γ), f x ≤ l
Hu : ∀ (u : γ), u ≤ f x
a : α
this : f a = f x
⊢ f x ∈ v

Tactic:
mem_of_mem_nhds hv

Premises used: mem_of_mem_nhds
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (l : γ), f x ≤ l
Hu : ∀ (u : γ), u ≤ f x
a : α
this : f a = f x
⊢ f x ∈ v

Tactic:
exact mem_of_mem_nhds hv

Premises used: mem_of_mem_nhds
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
f : α → γ
simp_rw : ContinuousWithinAt f univ x ↔ LowerSemicontinuousAt f x ∧ UpperSemicontinuousAt f x
simp_rw₁ : ContinuousWithinAt f univ x ↔ LowerSemicontinuousWithinAt f univ x ∧ UpperSemicontinuousAt f x
simp_rw₂ : ContinuousWithinAt f univ x ↔ LowerSemicontinuousWithinAt f univ x ∧ UpperSemicontinuousWithinAt f univ x
⊢ ContinuousAt f x ↔ LowerSemicontinuousAt f x ∧ UpperSemicontinuousAt f x

Tactic:
simp_rw [← continuousWithinAt_univ, ← lowerSemicontinuousWithinAt_univ_iff, ←
    upperSemicontinuousWithinAt_univ_iff, continuousWithinAt_iff_lower_upperSemicontinuousWithinAt]

Premises used: continuousWithinAt_univ, continuousWithinAt_iff_lower_upperSemicontinuousWithinAt, lowerSemicontinuousWithinAt_univ_iff, upperSemicontinuousWithinAt_univ_iff
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
f : α → γ
simp :
  (∀ x ∈ s, LowerSemicontinuousWithinAt f s x ∧ UpperSemicontinuousWithinAt f s x) ↔
    LowerSemicontinuousOn f s ∧ UpperSemicontinuousOn f s
⊢ ContinuousOn f s ↔ LowerSemicontinuousOn f s ∧ UpperSemicontinuousOn f s

Tactic:
simp only [ContinuousOn, continuousWithinAt_iff_lower_upperSemicontinuousWithinAt]

Premises used: continuousWithinAt_iff_lower_upperSemicontinuousWithinAt, ContinuousOn
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
f : α → γ
⊢ (∀ x ∈ s, LowerSemicontinuousWithinAt f s x ∧ UpperSemicontinuousWithinAt f s x) ↔
    LowerSemicontinuousOn f s ∧ UpperSemicontinuousOn f s

Tactic:
⟨fun H => ⟨fun x hx => (H x hx).1, fun x hx => (H x hx).2⟩, fun H x hx => ⟨H.1 x hx, H.2 x hx⟩⟩

Premises used: And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
f : α → γ
⊢ (∀ x ∈ s, LowerSemicontinuousWithinAt f s x ∧ UpperSemicontinuousWithinAt f s x) ↔
    LowerSemicontinuousOn f s ∧ UpperSemicontinuousOn f s

Tactic:
exact
    ⟨fun H => ⟨fun x hx => (H x hx).1, fun x hx => (H x hx).2⟩, fun H x hx => ⟨H.1 x hx, H.2 x hx⟩⟩
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
f : α → γ
simp_rw : ContinuousOn f univ ↔ LowerSemicontinuous f ∧ UpperSemicontinuous f
simp_rw₁ : LowerSemicontinuousOn f univ ∧ UpperSemicontinuousOn f univ ↔ LowerSemicontinuous f ∧ UpperSemicontinuous f
simp_rw₂ : LowerSemicontinuous f ∧ UpperSemicontinuousOn f univ ↔ LowerSemicontinuous f ∧ UpperSemicontinuous f
⊢ Continuous[inst, inst_2] f ↔ LowerSemicontinuous f ∧ UpperSemicontinuous f

Tactic:
simp_rw [← continuousOn_univ, continuousOn_iff_lower_upperSemicontinuousOn,
    lowerSemicontinuousOn_univ_iff, upperSemicontinuousOn_univ_iff]

Premises used: continuousOn_iff_lower_upperSemicontinuousOn, continuousOn_univ, lowerSemicontinuousOn_univ_iff, upperSemicontinuousOn_univ_iff
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
r : α → β → Prop
x : α
s : Set α
⊢ SemicontinuousWithinAt r s x ↔ ∀ (y : β), (∃ᶠ (x' : α) in 𝓝[s] x, ¬r x' y) → ¬r x y

Tactic:
simp only [← not_eventually, not_imp_not, SemicontinuousWithinAt]

Premises used: Filter.not_eventually, SemicontinuousWithinAt, not_imp_not
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
r : α → β → Prop
s : Set α
⊢ SemicontinuousOn r s ↔ ∀ x ∈ s, ∀ (y : β), (∃ᶠ (x' : α) in 𝓝[s] x, ¬r x' y) → ¬r x y

Tactic:
simp only [← not_eventually, not_imp_not, SemicontinuousWithinAt, SemicontinuousOn]

Premises used: Filter.not_eventually, SemicontinuousOn, SemicontinuousWithinAt, not_imp_not
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
r : α → β → Prop
x : α
⊢ SemicontinuousAt r x ↔ ∀ (y : β), (∃ᶠ (x' : α) in 𝓝 x, ¬r x' y) → ¬r x y

Tactic:
simp only [← not_eventually, not_imp_not, SemicontinuousAt]

Premises used: Filter.not_eventually, SemicontinuousAt, not_imp_not
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
r : α → β → Prop
⊢ Semicontinuous r ↔ ∀ (x : α) (y : β), (∃ᶠ (x' : α) in 𝓝 x, ¬r x' y) → ¬r x y

Tactic:
simp only [← not_eventually, not_imp_not, Semicontinuous, SemicontinuousAt]

Premises used: Filter.not_eventually, Semicontinuous, SemicontinuousAt, not_imp_not
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
r : α → β → Prop
x : α
s t : Set α
h : SemicontinuousWithinAt r s x
hst : t ⊆ s
⊢ SemicontinuousWithinAt r t x

Tactic:
fun y hy =>
  Filter.Eventually.filter_mono (nhdsWithin_mono _ hst) (h y hy)

Premises used: Filter.Eventually.filter_mono, nhdsWithin_mono, SemicontinuousWithinAt
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
r r' : α → β → Prop
s : Set α
a : α
h : SemicontinuousWithinAt r s a
has : a ∈ s
hfg : ∀ᶠ (x : α) in 𝓝[s] a, ∀ (y : β), r x y ↔ r' x y
b : β
hb : r' a b
⊢ ∀ᶠ (x : α) in 𝓝[s] a, r x = r' x

Tactic:
simp_rw [← propext_iff, ← funext_iff] at hfg

Premises used: funext_iff, propext_iff
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
r r' : α → β → Prop
s : Set α
a : α
h : SemicontinuousWithinAt r s a
has : a ∈ s
b : β
hb : r' a b
hfg : ∀ᶠ (x : α) in 𝓝[s] a, r x = r' x
⊢ r a b

Tactic:
rw [← Filter.EventuallyEq.eq_of_nhdsWithin hfg has] at hb

Premises used: Filter.EventuallyEq.eq_of_nhdsWithin
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
r r' : α → β → Prop
s : Set α
a : α
h : SemicontinuousWithinAt r s a
has : a ∈ s
b : β
hb : r' a b
hfg : ∀ᶠ (x : α) in 𝓝[s] a, r x = r' x
hb₁ : r a b
⊢ ∀ᶠ (x : α) in 𝓝[s] a, r x = r' x

Tactic:
rw [← Filter.EventuallyEq.eq_of_nhdsWithin hfg has] at hb

Premises used: Filter.EventuallyEq.eq_of_nhdsWithin
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
r r' : α → β → Prop
s : Set α
a : α
h : SemicontinuousWithinAt r s a
has : a ∈ s
b : β
hb : r a b
hfg : ∀ᶠ (x : α) in 𝓝[s] a, r x = r' x
h₁ : ∀ (x : α) (hx : r x = r' x) (hxb : r x b), r' x b
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, r' x' b

Tactic:
filter_upwards [hfg, h b hb] with x hx hxb
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
r r' : α → β → Prop
s : Set α
a : α
h : SemicontinuousWithinAt r s a
has : a ∈ s
b : β
hb : r a b
hfg : ∀ᶠ (x : α) in 𝓝[s] a, r x = r' x
x : α
hx : r x = r' x
hxb : r x b
⊢ r' x b

Tactic:
hx ▸ hxb

Premises used: Eq.rec
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
r r' : α → β → Prop
s : Set α
a : α
h : SemicontinuousWithinAt r s a
has : a ∈ s
b : β
hb : r a b
hfg : ∀ᶠ (x : α) in 𝓝[s] a, r x = r' x
x : α
hx : r x = r' x
hxb : r x b
⊢ r' x b

Tactic:
exact hx ▸ hxb
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
r : α → β → Prop
x : α
⊢ SemicontinuousWithinAt r univ x ↔ SemicontinuousAt r x

Tactic:
simp [SemicontinuousWithinAt, SemicontinuousAt, nhdsWithin_univ]

Premises used: nhdsWithin_univ, SemicontinuousAt, SemicontinuousWithinAt
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
r : α → β → Prop
x : α
s : Set α
h : SemicontinuousAt r x
⊢ SemicontinuousWithinAt r s x

Tactic:
fun y hy =>
  Filter.Eventually.filter_mono nhdsWithin_le_nhds (h y hy)

Premises used: Filter.Eventually.filter_mono, nhdsWithin_le_nhds, SemicontinuousWithinAt
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
r : α → β → Prop
x : α
s : Set α
h : SemicontinuousOn r s
hx : x ∈ s
⊢ SemicontinuousWithinAt r s x

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

Tactic:
fun x hx => (h x (hst hx)).mono hst

Premises used: SemicontinuousOn, SemicontinuousWithinAt.mono
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
r : α → β → Prop
⊢ SemicontinuousOn r univ ↔ Semicontinuous r

Tactic:
simp [SemicontinuousOn, Semicontinuous, semicontinuousWithinAt_univ_iff]

Premises used: semicontinuousWithinAt_univ_iff, Semicontinuous, SemicontinuousOn
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
r : α → β → Prop
s : Set α
rw :
  (∀ (x : α) (h : x ∈ s),
      SemicontinuousAt (s.restrict (π := fun (a : α) ↦ β → Prop) r) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h)) ↔
    ∀ x ∈ s, SemicontinuousWithinAt r s x
⊢ Semicontinuous (s.restrict (π := fun (a : α) ↦ β → Prop) r) ↔ SemicontinuousOn r s

Tactic:
rw [SemicontinuousOn, Semicontinuous, SetCoe.forall]

Premises used: Semicontinuous, SetCoe.forall, SemicontinuousOn
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
r : α → β → Prop
s : Set α
⊢ (∀ (x : α) (h : x ∈ s),
      SemicontinuousAt (s.restrict (π := fun (a : α) ↦ β → Prop) r) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h)) ↔
    ∀ x ∈ s, SemicontinuousWithinAt r s x

Tactic:
forall₂_congr fun a ha ↦ forall₂_congr fun b _ ↦ ?_

Premises used: forall₂_congr
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
r : α → β → Prop
s : Set α
refine :
  ∀ (a : α) (ha : a ∈ s) (b : β),
    s.restrict (π := fun (a : α) ↦ β → Prop) r (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha) b →
      ((∀ᶠ (x' : (↑s : Type u_1)) in 𝓝 (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha),
          s.restrict (π := fun (a : α) ↦ β → Prop) r x' b) ↔
        ∀ᶠ (x' : α) in 𝓝[s] a, r x' b)
⊢ (∀ (x : α) (h : x ∈ s),
      SemicontinuousAt (s.restrict (π := fun (a : α) ↦ β → Prop) r) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h)) ↔
    ∀ x ∈ s, SemicontinuousWithinAt r s x

Tactic:
refine forall₂_congr fun a ha ↦ forall₂_congr fun b _ ↦ ?_

Premises used: forall₂_congr
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
r : α → β → Prop
s : Set α
a : α
ha : a ∈ s
b : β
h : s.restrict (π := fun (a : α) ↦ β → Prop) r (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha) b
⊢ (∀ᶠ (x' : (↑s : Type u_1)) in 𝓝 (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha),
      s.restrict (π := fun (a : α) ↦ β → Prop) r x' b) ↔
    ∀ᶠ (x' : α) in 𝓝[s] a, r x' b

Tactic:
simp only [nhdsWithin_eq_map_subtype_coe ha, eventually_map, restrict]

Premises used: nhdsWithin_eq_map_subtype_coe, Filter.eventually_map, Set.restrict
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
r : α → β → Prop
h : Semicontinuous r
x : α
⊢ SemicontinuousAt r x

Tactic:
h x
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
r : α → β → Prop
h : Semicontinuous r
s : Set α
x : α
⊢ SemicontinuousWithinAt r 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 α
r : α → β → Prop
h : Semicontinuous r
s : Set α
⊢ SemicontinuousOn r s

Tactic:
fun x _hx => h.semicontinuousWithinAt s x

Premises used: Semicontinuous.semicontinuousWithinAt, SemicontinuousOn
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
x : α
s : Set α
f : β → Prop
⊢ SemicontinuousWithinAt.{u_1, u_2} (β := β) (fun (_x : α) ↦ f) s x

Tactic:
fun _y hy => Filter.Eventually.of_forall fun _x => hy

Premises used: Filter.Eventually.of_forall, SemicontinuousWithinAt
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
x : α
f : β → Prop
⊢ SemicontinuousAt.{u_1, u_2} (β := β) (fun (_x : α) ↦ f) x

Tactic:
fun _y hy =>
  Filter.Eventually.of_forall fun _x => hy

Premises used: Filter.Eventually.of_forall, SemicontinuousAt
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
f : β → Prop
⊢ SemicontinuousOn.{u_1, u_2} (β := β) (fun (_x : α) ↦ f) s

Tactic:
fun _x _hx =>
  SemicontinuousWithinAt.const

Premises used: SemicontinuousWithinAt.const, SemicontinuousOn
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : β → Prop
⊢ Semicontinuous.{u_1, u_2} (β := β) fun (_x : α) ↦ f

Tactic:
fun _x =>
  SemicontinuousAt.const

Premises used: SemicontinuousAt.const, Semicontinuous
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace γ
r : α → β → Prop
x : γ
g : γ → α
s : Set γ
t : Set α
h : SemicontinuousWithinAt r t (g x)
hg : ContinuousWithinAt g s x
hst : MapsTo g s t
⊢ SemicontinuousWithinAt (r ∘ g) s x

Tactic:
(hg.tendsto_nhdsWithin hst <| h · ·)

Premises used: Set.Mem, Filter.Eventually, setOf, ContinuousWithinAt.tendsto_nhdsWithin, Set.preimage, SemicontinuousWithinAt
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
r : α → β → Prop
γ : Type u_4
inst_1 : TopologicalSpace γ
g : γ → α
s : Set γ
t : Set α
h : SemicontinuousOn r t
hg : ContinuousOn g s
hst : MapsTo g s t
⊢ SemicontinuousOn (r ∘ g) s

Tactic:
fun x hx ↦ h (g x) (hst hx) |>.comp (hg x hx) hst

Premises used: SemicontinuousWithinAt.comp, SemicontinuousOn
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
r : α → β → Prop
γ : Type u_4
inst_1 : TopologicalSpace γ
x : γ
g : γ → α
h : SemicontinuousAt r (g x)
hg : ContinuousAt g x
⊢ SemicontinuousAt (r ∘ g) x

Tactic:
(hg <| h · ·)

Premises used: Set.Mem, Filter.Eventually, setOf, Set.preimage, SemicontinuousAt
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
r : α → β → Prop
γ : Type u_4
inst_1 : TopologicalSpace γ
g : γ → α
h : Semicontinuous r
hg : Continuous[inst_1, inst] g
⊢ Semicontinuous (r ∘ g)

Tactic:
fun _ ↦ (h.semicontinuousAt _).comp hg.continuousAt

Premises used: Semicontinuous.semicontinuousAt, Continuous.continuousAt, Semicontinuous, 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 g : α → β
x : α
s t : Set α
y z : β
simp_rw :
  (∀ (x : α), SemicontinuousAt (fun (x1 : α) (x2 : β) ↦ ¬f x1 ≤ x2) x) ↔
    ∀ (x : α) (y : β), (∃ᶠ (x' : α) in 𝓝 x, f x' ≤ y) → f x ≤ y
simp_rw₁ :
  (∀ (x : α) (y : β), ¬f x ≤ y → ∀ᶠ (x' : α) in 𝓝 x, ¬f x' ≤ y) ↔
    ∀ (x : α) (y : β), (∃ᶠ (x' : α) in 𝓝 x, f x' ≤ y) → f x ≤ y
simp_rw₂ :
  (∀ (x : α) (y : β), ¬f x ≤ y → ¬∃ᶠ (x : α) in 𝓝 x, f x ≤ y) ↔
    ∀ (x : α) (y : β), (∃ᶠ (x' : α) in 𝓝 x, f x' ≤ y) → f x ≤ y
⊢ (Semicontinuous fun (x1 : α) (x2 : β) ↦ ¬f x1 ≤ x2) ↔ ∀ (x : α) (y : β), (∃ᶠ (x' : α) in 𝓝 x, f x' ≤ y) → f x ≤ y

Tactic:
simp_rw [Semicontinuous, SemicontinuousAt, ← not_frequently, not_imp_not]

Premises used: Filter.not_frequently, Semicontinuous, SemicontinuousAt, not_imp_not
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
s : Set α
x : α
⊢ LowerSemicontinuousWithinAt f s x ↔ ∀ y < f x, ∀ᶠ (x' : α) in 𝓝[s] x, y < 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 : Preorder β
f : α → β
s : Set α
⊢ LowerSemicontinuousOn f s ↔ ∀ x ∈ s, LowerSemicontinuousWithinAt 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 : Preorder β
f : α → β
x : α
⊢ LowerSemicontinuousAt f x ↔ ∀ y < f x, ∀ᶠ (x' : α) in 𝓝 x, y < 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 : Preorder β
f : α → β
⊢ LowerSemicontinuous f ↔ ∀ (x : α), LowerSemicontinuousAt 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 : Preorder β
f : α → β
s : Set α
x : α
⊢ UpperSemicontinuousWithinAt f s x ↔ ∀ (y : β), f x < y → ∀ᶠ (x' : α) in 𝓝[s] x, f x' < y

Tactic:
Iff.rfl

Premises used: Iff.rfl, SemicontinuousWithinAt
-- Module: Mathlib.Topology.Semicontinuity.Defs
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
s : Set α
⊢ UpperSemicontinuousOn f s ↔ ∀ x ∈ s, UpperSemicontinuousWithinAt 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 : Preorder β
f : α → β
x : α
⊢ UpperSemicontinuousAt f x ↔ ∀ (y : β), f x < y → ∀ᶠ (x' : α) in 𝓝 x, f x' < y

Tactic:
Iff.rfl

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

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

Tactic:
simp [hx]