awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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, LowerSemicontinuousWithinAt (f i) univ x
⊢ LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ a, f i z) univ x

Tactic:
exact lowerSemicontinuousWithinAt_sum ha

Premises used: lowerSemicontinuousWithinAt_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, LowerSemicontinuousOn (f i) s
⊢ LowerSemicontinuousOn.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ a, f i z) s

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

Premises used: lowerSemicontinuousWithinAt_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, LowerSemicontinuous (f i)
⊢ LowerSemicontinuous.{u_1, u_5} (β := γ) fun (z : α) ↦ ∑ i ∈ a, f i z

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

Premises used: lowerSemicontinuousAt_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 : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : (fun (x : α) ↦ max (f x) (g x)) a > b
simp : ∀ (hb : b < f a ∨ b < g a), ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∨ b < g x'
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, (fun (x1 : α) (x2 : β) ↦ (fun (x : α) ↦ max (f x) (g x)) x1 > x2) x' b

Tactic:
simp only [lt_sup_iff] at hb ⊢

Premises used: lt_sup_iff
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_4
β : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder β
f g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < f a ∨ b < g a
inl : ∀ (hb : b < f a), ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∨ b < g x'
inr : ∀ (hb : b < g a), ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∨ b < g x'
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∨ b < g x'

Tactic:
rcases hb with hb | hb
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_4
β : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder β
f g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < f a
x : α
⊢ f x > b → b < f x ∨ b < g x

Tactic:
Or.intro_left _

Premises used: Or.intro_left
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_4
β : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder β
f g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < f a
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x' : α) ↦ ((fun (x1 : α) (x2 : β) ↦ f x1 > x2) x' b : Prop)) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x' : α) ↦ b < f x' ∨ b < g x') x} x}
      a
h₁ h₂ : ∀ (x : α), f x > b → b < f x ∨ b < g x
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∨ b < g x'

Tactic:
filter_upwards [hf b hb] with x using Or.intro_left _

Premises used: Or.intro_left
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_4
β : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder β
f g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < g a
x : α
⊢ g x > b → b < f x ∨ b < g x

Tactic:
Or.intro_right _

Premises used: Or.intro_right
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_4
β : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder β
f g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < g a
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x' : α) ↦ ((fun (x1 : α) (x2 : β) ↦ g x1 > x2) x' b : Prop)) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x' : α) ↦ b < f x' ∨ b < g x') x} x}
      a
h₁ h₂ : ∀ (x : α), g x > b → b < f x ∨ b < g x
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∨ b < g x'

Tactic:
filter_upwards [hg b hb] with x using Or.intro_right _

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

Tactic:
rw [← lowerSemicontinuousWithinAt_univ_iff] at *

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

Tactic:
hf.sup hg

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

Tactic:
exact hf.sup hg

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

Tactic:
fun a ha ↦
  LowerSemicontinuousWithinAt.sup (hf a ha) (hg a ha)

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

Tactic:
fun a ↦
  LowerSemicontinuousAt.sup (hf a) (hg a)

Premises used: LowerSemicontinuousAt.sup, Semicontinuous
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_4
β : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder β
f g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : (fun (x : α) ↦ min (f x) (g x)) a > b
simp : ∀ (hb : b < f a ∧ b < g a), ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∧ b < g x'
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, (fun (x1 : α) (x2 : β) ↦ (fun (x : α) ↦ min (f x) (g x)) x1 > x2) x' b

Tactic:
simp only [lt_inf_iff] at hb ⊢

Premises used: lt_inf_iff
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_4
β : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder β
f g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < f a ∧ b < g a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∧ b < g x'

Tactic:
Eventually.and (hf b hb.1) (hg b hb.2)

Premises used: Filter.Eventually.and, And.right, And.left
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_4
β : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder β
f g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < f a ∧ b < g a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∧ b < g x'

Tactic:
exact Eventually.and (hf b hb.1) (hg b hb.2)

Premises used: Filter.Eventually.and, And.right, And.left
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_4
β : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder β
f g : α → β
a : α
hf : LowerSemicontinuousAt f a
hg : LowerSemicontinuousAt g a
rw :
  ∀ (hf : LowerSemicontinuousWithinAt f univ a) (hg : LowerSemicontinuousWithinAt g univ a),
    LowerSemicontinuousWithinAt.{u_4, u_5} (β := β) (fun (x : α) ↦ min (f x) (g x)) univ a
⊢ LowerSemicontinuousAt.{u_4, u_5} (β := β) (fun (x : α) ↦ min (f x) (g x)) a

Tactic:
rw [← lowerSemicontinuousWithinAt_univ_iff] at *

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

Tactic:
hf.inf hg

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

Tactic:
exact hf.inf hg

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

Tactic:
fun a ha ↦
  LowerSemicontinuousWithinAt.inf (hf a ha) (hg a ha)

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

Tactic:
fun a ↦
  LowerSemicontinuousAt.inf (hf a) (hg a)

Premises used: LowerSemicontinuousAt.inf, Semicontinuous
-- 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, BddAbove.{u_6} (α := δ') (range fun (i : ι) ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
inl : IsEmpty ι → LowerSemicontinuousWithinAt.{u_1, u_6} (β := δ') (fun (x' : α) ↦ ⨆ (i : ι), f i x') s x
inr : Nonempty ι → LowerSemicontinuousWithinAt.{u_1, u_6} (β := δ') (fun (x' : α) ↦ ⨆ (i : ι), f i x') s x
⊢ LowerSemicontinuousWithinAt.{u_1, u_6} (β := δ') (fun (x' : α) ↦ ⨆ (i : ι), f i x') s x

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- 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, BddAbove.{u_6} (α := δ') (range fun (i : ι) ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h_1 : IsEmpty ι
⊢ LowerSemicontinuousWithinAt.{u_1, u_6} (β := δ') (fun (x' : α) ↦ ⨆ (i : ι), f i x') s x

Tactic:
simpa only [iSup_of_empty'] using lowerSemicontinuousWithinAt_const

Premises used: lowerSemicontinuousWithinAt_const, iSup_of_empty'
-- 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, BddAbove.{u_6} (α := δ') (range fun (i : ι) ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h_1 : Nonempty ι
y : δ'
hy : (fun (x' : α) ↦ (⨆ (i : ι), f i x' : δ')) x > y
inr :
  ∀ (i : ι) (hi : y < f i x),
    ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : δ') ↦ (fun (x' : α) ↦ (⨆ (i : ι), f i x' : δ')) x1 > x2) x' y
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : δ') ↦ (fun (x' : α) ↦ (⨆ (i : ι), f i x' : δ')) x1 > x2) x' y

Tactic:
rcases exists_lt_of_lt_ciSup hy with ⟨i, hi⟩

Premises used: exists_lt_of_lt_ciSup
-- 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, BddAbove.{u_6} (α := δ') (range fun (i : ι) ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h_1 : Nonempty ι
y_1 : δ'
hy_1 : (fun (x' : α) ↦ (⨆ (i : ι), f i x' : δ')) x > y_1
i : ι
hi : y_1 < f i x
y : α
hy : f i y > y_1
hy' : BddAbove.{u_6} (α := δ') (range fun (i : ι) ↦ f i y)
⊢ ⨆ (i : ι), f i y > y_1

Tactic:
hy.trans_le (le_ciSup hy' i)

Premises used: le_ciSup, LT.lt.trans_le
-- 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, BddAbove.{u_6} (α := δ') (range fun (i : ι) ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h_1 : Nonempty ι
y : δ'
hy : (fun (x' : α) ↦ (⨆ (i : ι), f i x' : δ')) x > y
i : ι
hi : y < f i x
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x' : α) ↦ ((fun (x1 : α) (x2 : δ') ↦ f i x1 > x2) x' y : Prop)) x}
            x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α)
                  {x : α | (fun (y : α) ↦ BddAbove.{u_6} (α := δ') (range fun (i : ι) ↦ f i y)) x} x →
                Membership.mem (γ := Set α)
                  {x : α |
                    (fun (x' : α) ↦
                        ((fun (x1 : α) (x2 : δ') ↦ (fun (x' : α) ↦ (⨆ (i : ι), f i x' : δ')) x1 > x2) x' y : Prop))
                      x}
                  x}
            x}
      a
h₂ h₃ :
  ∀ (y_1 : α) (hy : f i y_1 > y) (hy' : BddAbove.{u_6} (α := δ') (range fun (i : ι) ↦ f i y_1)), ⨆ (i : ι), f i y_1 > y
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : δ') ↦ (fun (x' : α) ↦ (⨆ (i : ι), f i x' : δ')) x1 > x2) x' y

Tactic:
filter_upwards [h i y hi, bdd] with y hy hy' using hy.trans_le (le_ciSup hy' i)
-- 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 : ι), LowerSemicontinuousWithinAt (f i) s x
⊢ ∀ᶠ (y : α) in 𝓝[s] x, BddAbove.{u_5} (α := δ) (range fun (i : ι) ↦ f i y)

Tactic:
simp
-- 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), LowerSemicontinuousWithinAt (f i hi) s x
⊢ LowerSemicontinuousWithinAt.{u_1, u_5} (β := δ) (fun (x' : α) ↦ ⨆ (i : ι), ⨆ (hi : p i), f i hi x') s x

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

Premises used: lowerSemicontinuousWithinAt_iSup
-- 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, BddAbove.{u_6} (α := δ') (range fun (i : ι) ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousAt (f i) x
simp_rw :
  ∀ (h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) univ x),
    LowerSemicontinuousWithinAt.{u_1, u_6} (β := δ') (fun (x' : α) ↦ ⨆ (i : ι), f i x') univ x
⊢ LowerSemicontinuousAt.{u_1, u_6} (β := δ') (fun (x' : α) ↦ ⨆ (i : ι), f i x') x

Tactic:
simp_rw [← lowerSemicontinuousWithinAt_univ_iff] at *

Premises used: lowerSemicontinuousWithinAt_univ_iff
-- 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, BddAbove.{u_6} (α := δ') (range fun (i : ι) ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) univ x
⊢ ∀ᶠ (y : α) in 𝓝[univ] x, BddAbove.{u_6} (α := δ') (range fun (i : ι) ↦ f i y)

Tactic:
rw [← nhdsWithin_univ] at bdd

Premises used: nhdsWithin_univ
-- 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, BddAbove.{u_6} (α := δ') (range fun (i : ι) ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) univ x
bdd₁ : ∀ᶠ (y : α) in 𝓝[univ] x, BddAbove.{u_6} (α := δ') (range fun (i : ι) ↦ f i y)
⊢ ∀ (i : ι), LowerSemicontinuousWithinAt (f i) univ x

Tactic:
rw [← nhdsWithin_univ] at bdd

Premises used: nhdsWithin_univ
-- 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 𝓝[univ] x, BddAbove.{u_6} (α := δ') (range fun (i : ι) ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) univ x
⊢ LowerSemicontinuousWithinAt.{u_1, u_6} (β := δ') (fun (x' : α) ↦ ⨆ (i : ι), f i x') univ x

Tactic:
lowerSemicontinuousWithinAt_ciSup bdd h

Premises used: lowerSemicontinuousWithinAt_ciSup
-- 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 𝓝[univ] x, BddAbove.{u_6} (α := δ') (range fun (i : ι) ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) univ x
⊢ LowerSemicontinuousWithinAt.{u_1, u_6} (β := δ') (fun (x' : α) ↦ ⨆ (i : ι), f i x') univ x

Tactic:
exact lowerSemicontinuousWithinAt_ciSup bdd h

Premises used: lowerSemicontinuousWithinAt_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 : ι), LowerSemicontinuousAt (f i) x
⊢ ∀ᶠ (y : α) in 𝓝 x, BddAbove.{u_5} (α := δ) (range fun (i : ι) ↦ f i y)

Tactic:
simp
-- 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), LowerSemicontinuousAt (f i hi) x
⊢ LowerSemicontinuousAt.{u_1, u_5} (β := δ) (fun (x' : α) ↦ ⨆ (i : ι), ⨆ (hi : p i), f i hi x') x

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

Premises used: lowerSemicontinuousAt_iSup
-- 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, BddAbove.{u_6} (α := δ') (range fun (i : ι) ↦ f i x)
h : ∀ (i : ι), LowerSemicontinuousOn (f i) s
⊢ LowerSemicontinuousOn.{u_1, u_6} (β := δ') (fun (x' : α) ↦ ⨆ (i : ι), f i x') s

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

Premises used: lowerSemicontinuousWithinAt_ciSup, SemicontinuousOn, 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 : ι), LowerSemicontinuousOn (f i) s
⊢ ∀ x ∈ s, BddAbove.{u_5} (α := δ) (range fun (i : ι) ↦ f i x)

Tactic:
simp
-- 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), LowerSemicontinuousOn (f i hi) s
⊢ LowerSemicontinuousOn.{u_1, u_5} (β := δ) (fun (x' : α) ↦ ⨆ (i : ι), ⨆ (hi : p i), f i hi x') s

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

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

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

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

Tactic:
simp
-- 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), LowerSemicontinuous (f i hi)
⊢ LowerSemicontinuous.{u_1, u_5} (β := δ) fun (x' : α) ↦ ⨆ (i : ι), ⨆ (hi : p i), f i hi x'

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

Premises used: lowerSemicontinuous_iSup
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
ι : Type u_4
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
simp_rw : LowerSemicontinuousWithinAt (β := ℝ≥0∞) (fun (x' : α) ↦ ⨆ (s : Finset ι), ∑ i ∈ s, f i x') s x
⊢ LowerSemicontinuousWithinAt (β := ℝ≥0∞) (fun (x' : α) ↦ ∑' (i : ι), f i x') s x

Tactic:
simp_rw [ENNReal.tsum_eq_iSup_sum]

Premises used: ENNReal.tsum_eq_iSup_sum
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
ι : Type u_4
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt (β := ℝ≥0∞) (fun (x' : α) ↦ ⨆ (s : Finset ι), ∑ i ∈ s, f i x') s x

Tactic:
lowerSemicontinuousWithinAt_iSup fun b => ?_

Premises used: lowerSemicontinuousWithinAt_iSup
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
ι : Type u_4
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
refine : ∀ (b : Finset ι), LowerSemicontinuousWithinAt (β := ℝ≥0∞) (fun (x' : α) ↦ ∑ i ∈ b, f i x') s x
⊢ LowerSemicontinuousWithinAt (β := ℝ≥0∞) (fun (x' : α) ↦ ⨆ (s : Finset ι), ∑ i ∈ s, f i x') s x

Tactic:
refine lowerSemicontinuousWithinAt_iSup fun b => ?_

Premises used: lowerSemicontinuousWithinAt_iSup
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
ι : Type u_4
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
b : Finset ι
⊢ LowerSemicontinuousWithinAt (β := ℝ≥0∞) (fun (x' : α) ↦ ∑ i ∈ b, f i x') s x

Tactic:
lowerSemicontinuousWithinAt_sum fun i _hi => h i

Premises used: lowerSemicontinuousWithinAt_sum
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
ι : Type u_4
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
b : Finset ι
⊢ LowerSemicontinuousWithinAt (β := ℝ≥0∞) (fun (x' : α) ↦ ∑ i ∈ b, f i x') s x

Tactic:
exact lowerSemicontinuousWithinAt_sum fun i _hi => h i

Premises used: lowerSemicontinuousWithinAt_sum
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
ι : Type u_4
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousAt (f i) x
simp_rw :
  ∀ (h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) univ x),
    LowerSemicontinuousWithinAt (β := ℝ≥0∞) (fun (x' : α) ↦ ∑' (i : ι), f i x') univ x
⊢ LowerSemicontinuousAt (β := ℝ≥0∞) (fun (x' : α) ↦ ∑' (i : ι), f i x') x

Tactic:
simp_rw [← lowerSemicontinuousWithinAt_univ_iff] at *

Premises used: lowerSemicontinuousWithinAt_univ_iff