awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
γ : Type u_5
inst_1 : AddCommMonoid γ
inst_2 : LinearOrder γ
inst_3 : IsOrderedAddMonoid γ
inst_4 : TopologicalSpace γ
inst_5 : OrderTopology γ
f g : α → γ
hf : UpperSemicontinuousOn f s
hg : UpperSemicontinuousOn g s
hcont : ∀ x ∈ s, ContinuousAt (Y := γ) (fun (p : γ × γ) ↦ p.1 + p.2) (f x, g x)
⊢ UpperSemicontinuousOn.{u_1, u_5} (β := γ) (fun (z : α) ↦ f z + g z) s

Tactic:
fun x hx =>
  UpperSemicontinuousWithinAt.add' (hf x hx) (hg x hx) (hcont x hx)

Premises used: UpperSemicontinuousWithinAt.add', SemicontinuousOn
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
γ : Type u_5
inst_1 : AddCommMonoid γ
inst_2 : LinearOrder γ
inst_3 : IsOrderedAddMonoid γ
inst_4 : TopologicalSpace γ
inst_5 : OrderTopology γ
f g : α → γ
hf : UpperSemicontinuous f
hg : UpperSemicontinuous g
hcont : ∀ (x : α), ContinuousAt (Y := γ) (fun (p : γ × γ) ↦ p.1 + p.2) (f x, g x)
⊢ UpperSemicontinuous.{u_1, u_5} (β := γ) fun (z : α) ↦ f z + g z

Tactic:
fun x => UpperSemicontinuousAt.add' (hf x) (hg x) (hcont x)

Premises used: Semicontinuous, UpperSemicontinuousAt.add'
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst_1 : AddCommMonoid γ
inst_2 : LinearOrder γ
inst_3 : IsOrderedAddMonoid γ
inst_4 : TopologicalSpace γ
inst_5 : OrderTopology γ
inst_6 : ContinuousAdd γ
f g : α → γ
hf : UpperSemicontinuousWithinAt f s x
hg : UpperSemicontinuousWithinAt g s x
⊢ UpperSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ f z + g z) s x

Tactic:
hf.add' hg continuous_add.continuousAt

Premises used: Continuous.continuousAt, continuous_add, UpperSemicontinuousWithinAt.add'
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
γ : Type u_5
inst_1 : AddCommMonoid γ
inst_2 : LinearOrder γ
inst_3 : IsOrderedAddMonoid γ
inst_4 : TopologicalSpace γ
inst_5 : OrderTopology γ
inst_6 : ContinuousAdd γ
f g : α → γ
hf : UpperSemicontinuousAt f x
hg : UpperSemicontinuousAt g x
⊢ UpperSemicontinuousAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ f z + g z) x

Tactic:
hf.add' hg continuous_add.continuousAt

Premises used: Continuous.continuousAt, continuous_add, UpperSemicontinuousAt.add'
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
γ : Type u_5
inst_1 : AddCommMonoid γ
inst_2 : LinearOrder γ
inst_3 : IsOrderedAddMonoid γ
inst_4 : TopologicalSpace γ
inst_5 : OrderTopology γ
inst_6 : ContinuousAdd γ
f g : α → γ
hf : UpperSemicontinuousOn f s
hg : UpperSemicontinuousOn g s
⊢ UpperSemicontinuousOn.{u_1, u_5} (β := γ) (fun (z : α) ↦ f z + g z) s

Tactic:
hf.add' hg fun _x _hx => continuous_add.continuousAt

Premises used: UpperSemicontinuousOn.add', Continuous.continuousAt, continuous_add
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
γ : Type u_5
inst_1 : AddCommMonoid γ
inst_2 : LinearOrder γ
inst_3 : IsOrderedAddMonoid γ
inst_4 : TopologicalSpace γ
inst_5 : OrderTopology γ
inst_6 : ContinuousAdd γ
f g : α → γ
hf : UpperSemicontinuous f
hg : UpperSemicontinuous g
⊢ UpperSemicontinuous.{u_1, u_5} (β := γ) fun (z : α) ↦ f z + g z

Tactic:
hf.add' hg fun _x => continuous_add.continuousAt

Premises used: UpperSemicontinuous.add', Continuous.continuousAt, continuous_add
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
ι : Type u_4
γ : Type u_5
inst_1 : AddCommMonoid γ
inst_2 : LinearOrder γ
inst_3 : IsOrderedAddMonoid γ
inst_4 : TopologicalSpace γ
inst_5 : OrderTopology γ
inst_6 : ContinuousAdd γ
f : ι → α → γ
a : Finset ι
ha : ∀ i ∈ a, UpperSemicontinuousWithinAt (f i) s x
⊢ UpperSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ a, f i z) s x

Tactic:
lowerSemicontinuousWithinAt_sum (γ := γᵒᵈ) ha

Premises used: lowerSemicontinuousWithinAt_sum, OrderDual
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
ι : Type u_4
γ : Type u_5
inst_1 : AddCommMonoid γ
inst_2 : LinearOrder γ
inst_3 : IsOrderedAddMonoid γ
inst_4 : TopologicalSpace γ
inst_5 : OrderTopology γ
inst_6 : ContinuousAdd γ
f : ι → α → γ
a : Finset ι
ha : ∀ i ∈ a, UpperSemicontinuousAt (f i) x
simp_rw :
  ∀ (ha : ∀ i ∈ a, UpperSemicontinuousWithinAt (f i) univ x),
    UpperSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ a, f i z) univ x
⊢ UpperSemicontinuousAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ a, f i z) x

Tactic:
simp_rw [← upperSemicontinuousWithinAt_univ_iff] at *

Premises used: upperSemicontinuousWithinAt_univ_iff
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
ι : Type u_4
γ : Type u_5
inst_1 : AddCommMonoid γ
inst_2 : LinearOrder γ
inst_3 : IsOrderedAddMonoid γ
inst_4 : TopologicalSpace γ
inst_5 : OrderTopology γ
inst_6 : ContinuousAdd γ
f : ι → α → γ
a : Finset ι
ha : ∀ i ∈ a, UpperSemicontinuousWithinAt (f i) univ x
⊢ UpperSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ a, f i z) univ x

Tactic:
upperSemicontinuousWithinAt_sum ha

Premises used: upperSemicontinuousWithinAt_sum
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
ι : Type u_4
γ : Type u_5
inst_1 : AddCommMonoid γ
inst_2 : LinearOrder γ
inst_3 : IsOrderedAddMonoid γ
inst_4 : TopologicalSpace γ
inst_5 : OrderTopology γ
inst_6 : ContinuousAdd γ
f : ι → α → γ
a : Finset ι
ha : ∀ i ∈ a, UpperSemicontinuousWithinAt (f i) univ x
⊢ UpperSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ a, f i z) univ x

Tactic:
exact upperSemicontinuousWithinAt_sum ha

Premises used: upperSemicontinuousWithinAt_sum
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
ι : Type u_4
γ : Type u_5
inst_1 : AddCommMonoid γ
inst_2 : LinearOrder γ
inst_3 : IsOrderedAddMonoid γ
inst_4 : TopologicalSpace γ
inst_5 : OrderTopology γ
inst_6 : ContinuousAdd γ
f : ι → α → γ
a : Finset ι
ha : ∀ i ∈ a, UpperSemicontinuousOn (f i) s
⊢ UpperSemicontinuousOn.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ a, f i z) s

Tactic:
fun x hx =>
  upperSemicontinuousWithinAt_sum fun i hi => ha i hi x hx

Premises used: upperSemicontinuousWithinAt_sum, SemicontinuousOn
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_4
γ : Type u_5
inst_1 : AddCommMonoid γ
inst_2 : LinearOrder γ
inst_3 : IsOrderedAddMonoid γ
inst_4 : TopologicalSpace γ
inst_5 : OrderTopology γ
inst_6 : ContinuousAdd γ
f : ι → α → γ
a : Finset ι
ha : ∀ i ∈ a, UpperSemicontinuous (f i)
⊢ UpperSemicontinuous.{u_1, u_5} (β := γ) fun (z : α) ↦ ∑ i ∈ a, f i z

Tactic:
fun x => upperSemicontinuousAt_sum fun i hi => ha i hi x

Premises used: upperSemicontinuousAt_sum, Semicontinuous
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_4
β : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder β
f g : α → β
s : Set α
a : α
hf : UpperSemicontinuousWithinAt f s a
hg : UpperSemicontinuousWithinAt g s a
⊢ UpperSemicontinuousWithinAt.{u_4, u_5} (β := β) (fun (x : α) ↦ min (f x) (g x)) s a

Tactic:
LowerSemicontinuousWithinAt.sup (β := βᵒᵈ) hf hg

Premises used: LowerSemicontinuousWithinAt.sup, OrderDual
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_4
β : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder β
f g : α → β
a : α
hf : UpperSemicontinuousAt f a
hg : UpperSemicontinuousAt g a
⊢ UpperSemicontinuousAt.{u_4, u_5} (β := β) (fun (x : α) ↦ min (f x) (g x)) a

Tactic:
LowerSemicontinuousAt.sup (β := βᵒᵈ) hf hg

Premises used: LowerSemicontinuousAt.sup, OrderDual
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_4
β : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder β
f g : α → β
s : Set α
hf : UpperSemicontinuousOn f s
hg : UpperSemicontinuousOn g s
⊢ UpperSemicontinuousOn.{u_4, u_5} (β := β) (fun (x : α) ↦ min (f x) (g x)) s

Tactic:
LowerSemicontinuousOn.sup (β := βᵒᵈ) hf hg

Premises used: OrderDual, LowerSemicontinuousOn.sup
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_4
β : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder β
f g : α → β
hf : UpperSemicontinuous f
hg : UpperSemicontinuous g
⊢ UpperSemicontinuous.{u_4, u_5} (β := β) fun (x : α) ↦ min (f x) (g x)

Tactic:
LowerSemicontinuous.sup (β := βᵒᵈ) hf hg

Premises used: LowerSemicontinuous.sup, OrderDual
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_4
β : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder β
f g : α → β
s : Set α
a : α
hf : UpperSemicontinuousWithinAt f s a
hg : UpperSemicontinuousWithinAt g s a
⊢ UpperSemicontinuousWithinAt.{u_4, u_5} (β := β) (fun (x : α) ↦ max (f x) (g x)) s a

Tactic:
LowerSemicontinuousWithinAt.inf (β := βᵒᵈ) hf hg

Premises used: LowerSemicontinuousWithinAt.inf, OrderDual
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_4
β : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder β
f g : α → β
a : α
hf : UpperSemicontinuousAt f a
hg : UpperSemicontinuousAt g a
⊢ UpperSemicontinuousAt.{u_4, u_5} (β := β) (fun (x : α) ↦ max (f x) (g x)) a

Tactic:
LowerSemicontinuousAt.inf (β := βᵒᵈ) hf hg

Premises used: LowerSemicontinuousAt.inf, OrderDual
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_4
β : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder β
f g : α → β
s : Set α
hf : UpperSemicontinuousOn f s
hg : UpperSemicontinuousOn g s
⊢ UpperSemicontinuousOn.{u_4, u_5} (β := β) (fun (x : α) ↦ max (f x) (g x)) s

Tactic:
LowerSemicontinuousOn.inf (β := βᵒᵈ) hf hg

Premises used: LowerSemicontinuousOn.inf, OrderDual
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_4
β : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder β
f g : α → β
hf : UpperSemicontinuous f
hg : UpperSemicontinuous g
⊢ UpperSemicontinuous.{u_4, u_5} (β := β) fun (x : α) ↦ max (f x) (g x)

Tactic:
LowerSemicontinuous.inf (β := βᵒᵈ) hf hg

Premises used: LowerSemicontinuous.inf, OrderDual
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
ι : Sort u_4
δ' : Type u_6
inst_1 : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddBelow.{u_6} (α := δ') (range fun (i : ι) ↦ f i y)
h : ∀ (i : ι), UpperSemicontinuousWithinAt (f i) s x
⊢ UpperSemicontinuousWithinAt.{u_1, u_6} (β := δ') (fun (x' : α) ↦ ⨅ (i : ι), f i x') s x

Tactic:
lowerSemicontinuousWithinAt_ciSup (δ' := δ'ᵒᵈ) bdd h

Premises used: iInf, lowerSemicontinuousWithinAt_ciSup, OrderDual
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
ι : Sort u_4
δ : Type u_5
inst_1 : CompleteLinearOrder δ
f : ι → α → δ
h : ∀ (i : ι), UpperSemicontinuousWithinAt (f i) s x
⊢ UpperSemicontinuousWithinAt.{u_1, u_5} (β := δ) (fun (x' : α) ↦ ⨅ (i : ι), f i x') s x

Tactic:
lowerSemicontinuousWithinAt_iSup (δ := δᵒᵈ) h

Premises used: lowerSemicontinuousWithinAt_iSup, iInf, OrderDual
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
ι : Sort u_4
δ : Type u_5
inst_1 : CompleteLinearOrder δ
p : ι → Prop
f : (i : ι) → p i → α → δ
h : ∀ (i : ι) (hi : p i), UpperSemicontinuousWithinAt (f i hi) s x
⊢ UpperSemicontinuousWithinAt.{u_1, u_5} (β := δ) (fun (x' : α) ↦ ⨅ (i : ι), ⨅ (hi : p i), f i hi x') s x

Tactic:
upperSemicontinuousWithinAt_iInf fun i => upperSemicontinuousWithinAt_iInf fun hi => h i hi

Premises used: upperSemicontinuousWithinAt_iInf
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
ι : Sort u_4
δ' : Type u_6
inst_1 : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝 x, BddBelow.{u_6} (α := δ') (range fun (i : ι) ↦ f i y)
h : ∀ (i : ι), UpperSemicontinuousAt (f i) x
⊢ UpperSemicontinuousAt.{u_1, u_6} (β := δ') (fun (x' : α) ↦ ⨅ (i : ι), f i x') x

Tactic:
@lowerSemicontinuousAt_ciSup α _ x ι δ'ᵒᵈ _ f bdd h

Premises used: iInf, OrderDual, lowerSemicontinuousAt_ciSup
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
ι : Sort u_4
δ : Type u_5
inst_1 : CompleteLinearOrder δ
f : ι → α → δ
h : ∀ (i : ι), UpperSemicontinuousAt (f i) x
⊢ UpperSemicontinuousAt.{u_1, u_5} (β := δ) (fun (x' : α) ↦ ⨅ (i : ι), f i x') x

Tactic:
@lowerSemicontinuousAt_iSup α _ x ι δᵒᵈ _ f h

Premises used: iInf, OrderDual, lowerSemicontinuousAt_iSup
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
ι : Sort u_4
δ : Type u_5
inst_1 : CompleteLinearOrder δ
p : ι → Prop
f : (i : ι) → p i → α → δ
h : ∀ (i : ι) (hi : p i), UpperSemicontinuousAt (f i hi) x
⊢ UpperSemicontinuousAt.{u_1, u_5} (β := δ) (fun (x' : α) ↦ ⨅ (i : ι), ⨅ (hi : p i), f i hi x') x

Tactic:
upperSemicontinuousAt_iInf fun i => upperSemicontinuousAt_iInf fun hi => h i hi

Premises used: upperSemicontinuousAt_iInf
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
ι : Sort u_4
δ' : Type u_6
inst_1 : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ x ∈ s, BddBelow.{u_6} (α := δ') (range fun (i : ι) ↦ f i x)
h : ∀ (i : ι), UpperSemicontinuousOn (f i) s
⊢ UpperSemicontinuousOn.{u_1, u_6} (β := δ') (fun (x' : α) ↦ ⨅ (i : ι), f i x') s

Tactic:
fun x hx =>
  upperSemicontinuousWithinAt_ciInf (eventually_nhdsWithin_of_forall bdd) fun i => h i x hx

Premises used: SemicontinuousOn, upperSemicontinuousWithinAt_ciInf, eventually_nhdsWithin_of_forall
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
ι : Sort u_4
δ : Type u_5
inst_1 : CompleteLinearOrder δ
f : ι → α → δ
h : ∀ (i : ι), UpperSemicontinuousOn (f i) s
⊢ UpperSemicontinuousOn.{u_1, u_5} (β := δ) (fun (x' : α) ↦ ⨅ (i : ι), f i x') s

Tactic:
fun x hx =>
  upperSemicontinuousWithinAt_iInf fun i => h i x hx

Premises used: upperSemicontinuousWithinAt_iInf, SemicontinuousOn
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
ι : Sort u_4
δ : Type u_5
inst_1 : CompleteLinearOrder δ
p : ι → Prop
f : (i : ι) → p i → α → δ
h : ∀ (i : ι) (hi : p i), UpperSemicontinuousOn (f i hi) s
⊢ UpperSemicontinuousOn.{u_1, u_5} (β := δ) (fun (x' : α) ↦ ⨅ (i : ι), ⨅ (hi : p i), f i hi x') s

Tactic:
upperSemicontinuousOn_iInf fun i => upperSemicontinuousOn_iInf fun hi => h i hi

Premises used: upperSemicontinuousOn_iInf
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Sort u_4
δ' : Type u_6
inst_1 : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ (x : α), BddBelow.{u_6} (α := δ') (range fun (i : ι) ↦ f i x)
h : ∀ (i : ι), UpperSemicontinuous (f i)
⊢ UpperSemicontinuous.{u_1, u_6} (β := δ') fun (x' : α) ↦ ⨅ (i : ι), f i x'

Tactic:
fun x =>
  upperSemicontinuousAt_ciInf (Eventually.of_forall bdd) fun i => h i x

Premises used: Filter.Eventually.of_forall, Semicontinuous, upperSemicontinuousAt_ciInf
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Sort u_4
δ : Type u_5
inst_1 : CompleteLinearOrder δ
f : ι → α → δ
h : ∀ (i : ι), UpperSemicontinuous (f i)
⊢ UpperSemicontinuous.{u_1, u_5} (β := δ) fun (x' : α) ↦ ⨅ (i : ι), f i x'

Tactic:
fun x => upperSemicontinuousAt_iInf fun i => h i x

Premises used: Semicontinuous, upperSemicontinuousAt_iInf
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Sort u_4
δ : Type u_5
inst_1 : CompleteLinearOrder δ
p : ι → Prop
f : (i : ι) → p i → α → δ
h : ∀ (i : ι) (hi : p i), UpperSemicontinuous (f i hi)
⊢ UpperSemicontinuous.{u_1, u_5} (β := δ) fun (x' : α) ↦ ⨅ (i : ι), ⨅ (hi : p i), f i hi x'

Tactic:
upperSemicontinuous_iInf fun i => upperSemicontinuous_iInf fun hi => h i hi

Premises used: upperSemicontinuous_iInf
-- 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 : α → γ
⊢ ContinuousWithinAt f s x ↔ LowerSemicontinuousWithinAt f s x ∧ UpperSemicontinuousWithinAt f s x

Tactic:
⟨fun h => ⟨h.lowerSemicontinuousWithinAt, h.upperSemicontinuousWithinAt⟩, ?_⟩

Premises used: ContinuousWithinAt.lowerSemicontinuousWithinAt, And.intro, Iff.intro, ContinuousWithinAt.upperSemicontinuousWithinAt
-- 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 : α → γ
refine : LowerSemicontinuousWithinAt f s x ∧ UpperSemicontinuousWithinAt f s x → ContinuousWithinAt f s x
⊢ ContinuousWithinAt f s x ↔ LowerSemicontinuousWithinAt f s x ∧ UpperSemicontinuousWithinAt f s x

Tactic:
refine ⟨fun h => ⟨h.lowerSemicontinuousWithinAt, h.upperSemicontinuousWithinAt⟩, ?_⟩
-- 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)
pos : ∀ (Hl : ∃ (l : γ), l < f x), f ⁻¹' v ∈ 𝓝[s] x
neg : ∀ (Hl : ∀ (l : γ), f x ≤ l), f ⁻¹' v ∈ 𝓝[s] x
⊢ f ⁻¹' v ∈ 𝓝[s] x

Tactic:
by_cases! Hl : ∃ l, l < f x
-- 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 : γ), l < f x
pos : ∀ (l : γ) (lfx : l < f x) (hl : Ioc l (f x) ⊆ v), f ⁻¹' v ∈ 𝓝[s] x
⊢ f ⁻¹' v ∈ 𝓝[s] x

Tactic:
rcases exists_Ioc_subset_of_mem_nhds hv Hl with ⟨l, lfx, hl⟩

Premises used: exists_Ioc_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 : γ), l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
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 : γ), l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
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 : γ), l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∃ (u : γ), f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
h : ∀ (a : α) (lfa : f a > l) (fau : f a < u), a ∈ f ⁻¹' v
⊢ f ⁻¹' v ∈ 𝓝[s] x

Tactic:
filter_upwards [h₁ l lfx, h₂ u fxu] with a lfa fau
-- 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 : γ), l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∃ (u : γ), f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
a : α
lfa : f a > l
fau : f a < u
h : ∀ (h : f a ≤ f x), a ∈ f ⁻¹' v
h₃ : ∀ (h : f x < f a), a ∈ f ⁻¹' v
⊢ a ∈ f ⁻¹' v

Tactic:
rcases le_or_gt (f a) (f x) with h | h

Premises used: le_or_gt
-- 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 : γ), l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∃ (u : γ), f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
a : α
lfa : f a > l
fau : f a < u
h : f a ≤ f x
⊢ a ∈ f ⁻¹' v

Tactic:
hl ⟨lfa, h⟩

Premises used: Set.Mem, setOf, Set.preimage, 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 : γ), l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∃ (u : γ), f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
a : α
lfa : f a > l
fau : f a < u
h : f a ≤ f x
⊢ a ∈ f ⁻¹' v

Tactic:
exact hl ⟨lfa, h⟩

Premises used: 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 : γ), l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∃ (u : γ), f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
a : α
lfa : f a > l
fau : f a < u
h : f x < f a
⊢ a ∈ f ⁻¹' v

Tactic:
hu ⟨le_of_lt h, fau⟩

Premises used: Set.Mem, setOf, le_of_lt, Set.preimage, 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 : γ), l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∃ (u : γ), f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
a : α
lfa : f a > l
fau : f a < u
h : f x < f a
⊢ a ∈ f ⁻¹' v

Tactic:
exact hu ⟨le_of_lt h, fau⟩

Premises used: le_of_lt, 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 : γ), l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∀ (u : γ), u ≤ f x
a : α
lfa : f a > l
⊢ a ∈ f ⁻¹' v

Tactic:
hl ⟨lfa, Hu (f a)⟩

Premises used: Set.Mem, setOf, Set.preimage, 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 : γ), l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∀ (u : γ), u ≤ f x
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x' : α) ↦ ((fun (x1 : α) (x2 : γ) ↦ f x1 > x2) x' l : Prop)) x} x →
          x ∈ f ⁻¹' v}
      a
h₃ h₄ : ∀ (a : α) (lfa : f a > l), a ∈ f ⁻¹' v
⊢ f ⁻¹' v ∈ 𝓝[s] x

Tactic:
filter_upwards [h₁ l lfx] with a lfa using hl ⟨lfa, Hu (f a)⟩