awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (Y := γ) (fun (p : γ × γ) ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun (z : α) ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst_4] u
xu : f x ∈ u
v_open : IsOpen[inst_4] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p : γ × γ | y < p.1 + p.2}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∃ (l : γ), l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₂z : g z > z₂
H : g z ≤ g x
⊢ min (g z) (g x) ∈ v

Tactic:
simpa [H] using h₂ ⟨h₂z, H⟩

Premises used: And.intro
-- 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 γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (Y := γ) (fun (p : γ × γ) ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun (z : α) ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst_4] u
xu : f x ∈ u
v_open : IsOpen[inst_4] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p : γ × γ | y < p.1 + p.2}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∃ (l : γ), l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₂z : g z > z₂
H : g x < g z
⊢ min (g z) (g x) ∈ v

Tactic:
simpa [H.le] using h₂ ⟨z₂lt, le_rfl⟩

Premises used: le_rfl, LT.lt.le, And.intro
-- 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 γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (Y := γ) (fun (p : γ × γ) ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun (z : α) ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst_4] u
xu : f x ∈ u
v_open : IsOpen[inst_4] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p : γ × γ | y < p.1 + p.2}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∃ (l : γ), l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₂z : g z > z₂
⊢ min (g z) (g x) ∈ v

Tactic:
have A2 : min (g z) (g x) ∈ v := by
        by_cases! H : g z ≤ g x
        · simpa [H] using h₂ ⟨h₂z, H⟩
        · simpa [H.le] using h₂ ⟨z₂lt, le_rfl⟩
-- 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 γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (Y := γ) (fun (p : γ × γ) ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun (z : α) ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst_4] u
xu : f x ∈ u
v_open : IsOpen[inst_4] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p : γ × γ | y < p.1 + p.2}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∃ (l : γ), l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₂z : g z > z₂
A2 : min (g z) (g x) ∈ v
⊢ (f x, min (g z) (g x)) ∈ u ×ˢ v

Tactic:
have : (f x, min (g z) (g x)) ∈ u ×ˢ v := ⟨xu, A2⟩
-- 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 γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (Y := γ) (fun (p : γ × γ) ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun (z : α) ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst_4] u
xu : f x ∈ u
v_open : IsOpen[inst_4] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p : γ × γ | y < p.1 + p.2}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∃ (l : γ), l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₂z : g z > z₂
A2 : min (g z) (g x) ∈ v
this : (f x, min (g z) (g x)) ∈ u ×ˢ v
⊢ y < f x + min (g z) (g x)

Tactic:
h this

Premises used: Set.Mem, setOf
-- 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 γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (Y := γ) (fun (p : γ × γ) ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun (z : α) ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst_4] u
xu : f x ∈ u
v_open : IsOpen[inst_4] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p : γ × γ | y < p.1 + p.2}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∃ (l : γ), l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₂z : g z > z₂
A2 : min (g z) (g x) ∈ v
this : (f x, min (g z) (g x)) ∈ u ×ˢ v
⊢ f x + min (g z) (g x) ≤ f z + g z

Tactic:
add_le_add (hx₁ (f z)) (min_le_left _ _)

Premises used: add_le_add, min_le_left
-- 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 γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (Y := γ) (fun (p : γ × γ) ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun (z : α) ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst_4] u
xu : f x ∈ u
v_open : IsOpen[inst_4] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p : γ × γ | y < p.1 + p.2}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∃ (l : γ), l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₂z : g z > z₂
A2 : min (g z) (g x) ∈ v
this : (f x, min (g z) (g x)) ∈ u ×ˢ v
⊢ f z + g z > y

Tactic:
calc
        y < f x + min (g z) (g x) := h this
        _ ≤ f z + g z := add_le_add (hx₁ (f z)) (min_le_left _ _)

Premises used: add_le_add, min_le_left, Min.min
-- 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 γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (Y := γ) (fun (p : γ × γ) ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun (z : α) ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst_4] u
xu : f x ∈ u
v_open : IsOpen[inst_4] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p : γ × γ | y < p.1 + p.2}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ¬∃ (l : γ), l < g x
⊢ ∀ (x_1 : γ), g x ≤ x_1

Tactic:
simp only [not_exists, not_lt] at hx₁ hx₂

Premises used: not_exists, not_lt
-- 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 γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (Y := γ) (fun (p : γ × γ) ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun (z : α) ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst_4] u
xu : f x ∈ u
v_open : IsOpen[inst_4] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p : γ × γ | y < p.1 + p.2}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∀ (x_1 : γ), g x ≤ x_1
neg : ∀ (x : α), (fun (x1 : α) (x2 : γ) ↦ (fun (z : α) ↦ f z + g z) x1 > x2) x y
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : γ) ↦ (fun (z : α) ↦ f z + g z) x1 > x2) x' y

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_5
inst_1 : AddCommMonoid γ
inst_2 : LinearOrder γ
inst_3 : IsOrderedAddMonoid γ
inst_4 : TopologicalSpace γ
inst_5 : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (Y := γ) (fun (p : γ × γ) ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun (z : α) ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst_4] u
xu : f x ∈ u
v_open : IsOpen[inst_4] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p : γ × γ | y < p.1 + p.2}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∀ (x_1 : γ), g x ≤ x_1
z : α
⊢ (f x, g x) ∈ u ×ˢ v

Tactic:
have : (f x, g x) ∈ u ×ˢ v := ⟨xu, xv⟩
-- 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 γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (Y := γ) (fun (p : γ × γ) ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun (z : α) ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst_4] u
xu : f x ∈ u
v_open : IsOpen[inst_4] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p : γ × γ | y < p.1 + p.2}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∀ (x_1 : γ), g x ≤ x_1
z : α
this : (f x, g x) ∈ u ×ˢ v
⊢ y < f x + g x

Tactic:
h this

Premises used: Set.Mem, setOf
-- 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 γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (Y := γ) (fun (p : γ × γ) ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun (z : α) ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst_4] u
xu : f x ∈ u
v_open : IsOpen[inst_4] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p : γ × γ | y < p.1 + p.2}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∀ (x_1 : γ), g x ≤ x_1
z : α
this : (f x, g x) ∈ u ×ˢ v
⊢ f x + g x ≤ f z + g z

Tactic:
add_le_add (hx₁ (f z)) (hx₂ (g z))

Premises used: add_le_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 γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (Y := γ) (fun (p : γ × γ) ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun (z : α) ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst_4] u
xu : f x ∈ u
v_open : IsOpen[inst_4] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p : γ × γ | y < p.1 + p.2}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∀ (x_1 : γ), g x ≤ x_1
z : α
this : (f x, g x) ∈ u ×ˢ v
⊢ (fun (x1 : α) (x2 : γ) ↦ (fun (z : α) ↦ f z + g z) x1 > x2) z y

Tactic:
calc
        y < f x + g x := h this
        _ ≤ f z + g z := add_le_add (hx₁ (f z)) (hx₂ (g z))

Premises used: add_le_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 γ
f g : α → γ
hf : LowerSemicontinuousAt f x
hg : LowerSemicontinuousAt g x
hcont : ContinuousAt (Y := γ) (fun (p : γ × γ) ↦ p.1 + p.2) (f x, g x)
simp_rw :
  ∀ (hf : LowerSemicontinuousWithinAt f univ x) (hg : LowerSemicontinuousWithinAt g univ x),
    LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ f z + g z) univ x
⊢ LowerSemicontinuousAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ f z + g z) 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 : α
γ : Type u_5
inst_1 : AddCommMonoid γ
inst_2 : LinearOrder γ
inst_3 : IsOrderedAddMonoid γ
inst_4 : TopologicalSpace γ
inst_5 : OrderTopology γ
f g : α → γ
hcont : ContinuousAt (Y := γ) (fun (p : γ × γ) ↦ p.1 + p.2) (f x, g x)
hf : LowerSemicontinuousWithinAt f univ x
hg : LowerSemicontinuousWithinAt g univ x
⊢ LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ f z + g z) univ x

Tactic:
hf.add' hg hcont

Premises used: LowerSemicontinuousWithinAt.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 γ
f g : α → γ
hcont : ContinuousAt (Y := γ) (fun (p : γ × γ) ↦ p.1 + p.2) (f x, g x)
hf : LowerSemicontinuousWithinAt f univ x
hg : LowerSemicontinuousWithinAt g univ x
⊢ LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ f z + g z) univ x

Tactic:
exact hf.add' hg hcont

Premises used: LowerSemicontinuousWithinAt.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 γ
f g : α → γ
hf : LowerSemicontinuousOn f s
hg : LowerSemicontinuousOn g s
hcont : ∀ x ∈ s, ContinuousAt (Y := γ) (fun (p : γ × γ) ↦ p.1 + p.2) (f x, g x)
⊢ LowerSemicontinuousOn.{u_1, u_5} (β := γ) (fun (z : α) ↦ f z + g z) s

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

Premises used: LowerSemicontinuousWithinAt.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 : LowerSemicontinuous f
hg : LowerSemicontinuous g
hcont : ∀ (x : α), ContinuousAt (Y := γ) (fun (p : γ × γ) ↦ p.1 + p.2) (f x, g x)
⊢ LowerSemicontinuous.{u_1, u_5} (β := γ) fun (z : α) ↦ f z + g z

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

Premises used: Semicontinuous, LowerSemicontinuousAt.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 : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
⊢ LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ f z + g z) s x

Tactic:
hf.add' hg continuous_add.continuousAt

Premises used: Continuous.continuousAt, LowerSemicontinuousWithinAt.add', continuous_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 : LowerSemicontinuousAt f x
hg : LowerSemicontinuousAt g x
⊢ LowerSemicontinuousAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ f z + g z) x

Tactic:
hf.add' hg continuous_add.continuousAt

Premises used: Continuous.continuousAt, continuous_add, LowerSemicontinuousAt.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 : LowerSemicontinuousOn f s
hg : LowerSemicontinuousOn g s
⊢ LowerSemicontinuousOn.{u_1, u_5} (β := γ) (fun (z : α) ↦ f z + g z) s

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

Premises used: LowerSemicontinuousOn.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 : LowerSemicontinuous f
hg : LowerSemicontinuous g
⊢ LowerSemicontinuous.{u_1, u_5} (β := γ) fun (z : α) ↦ f z + g z

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

Premises used: Continuous.continuousAt, continuous_add, LowerSemicontinuous.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 : ι → α → γ
ha : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ ∅, f i z) s x

Tactic:
lowerSemicontinuousWithinAt_const

Premises used: Multiset.sum, Multiset.foldr, lowerSemicontinuousWithinAt_const, List.foldr, Finset.sum
-- 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 : ι → α → γ
ha : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ ∅, f i z) s x

Tactic:
exact lowerSemicontinuousWithinAt_const

Premises used: lowerSemicontinuousWithinAt_const
-- 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 : ι
s_1 : Finset ι
ia : a ∉ s_1
IH :
  ∀ (ha : ∀ i ∈ s_1, LowerSemicontinuousWithinAt (f i) s x),
    LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ s_1, f i z) s x
ha : ∀ i ∈ Insert.insert a s_1, LowerSemicontinuousWithinAt (f i) s x
insert : LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ f a z + ∑ i ∈ s_1, f i z) s x
⊢ LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ Insert.insert a s_1, f i z) s x

Tactic:
simp only [ia, Finset.sum_insert, not_false_iff]

Premises used: Finset.sum_insert, not_false_iff
-- 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 : ι
s_1 : Finset ι
ia : a ∉ s_1
IH :
  ∀ (ha : ∀ i ∈ s_1, LowerSemicontinuousWithinAt (f i) s x),
    LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ s_1, f i z) s x
ha : ∀ i ∈ insert a s_1, LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ f a z + ∑ i ∈ s_1, f i z) s x

Tactic:
LowerSemicontinuousWithinAt.add (ha _ (Finset.mem_insert_self ..))
          (IH fun j ja => ha j (Finset.mem_insert_of_mem ja))

Premises used: Finset.mem_insert_self, LowerSemicontinuousWithinAt.add, Finset.mem_insert_of_mem
-- 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 : ι
s_1 : Finset ι
ia : a ∉ s_1
IH :
  ∀ (ha : ∀ i ∈ s_1, LowerSemicontinuousWithinAt (f i) s x),
    LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ s_1, f i z) s x
ha : ∀ i ∈ insert a s_1, LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ f a z + ∑ i ∈ s_1, f i z) s x

Tactic:
exact
        LowerSemicontinuousWithinAt.add (ha _ (Finset.mem_insert_self ..))
          (IH fun j ja => ha j (Finset.mem_insert_of_mem ja))

Premises used: Finset.mem_insert_self, LowerSemicontinuousWithinAt.add, Finset.mem_insert_of_mem
-- 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, LowerSemicontinuousWithinAt (f i) s x
empty :
  ∀ (ha : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → LowerSemicontinuousWithinAt (f i) s x),
    LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ ∅, f i z) s x
insert :
  ∀ (a : ι) (s_1 : Finset ι) (ia : a ∉ s_1)
    (IH :
      ∀ (ha : ∀ i ∈ s_1, LowerSemicontinuousWithinAt (f i) s x),
        LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ s_1, f i z) s x)
    (ha : ∀ i ∈ Insert.insert a s_1, LowerSemicontinuousWithinAt (f i) s x),
    LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ Insert.insert a s_1, f i z) s x
⊢ LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ a, f i z) s x

Tactic:
induction a using Finset.induction_on with
    | empty => exact lowerSemicontinuousWithinAt_const
    | insert _ _ ia IH =>
      simp only [ia, Finset.sum_insert, not_false_iff]
      exact
        LowerSemicontinuousWithinAt.add (ha _ (Finset.mem_insert_self ..))
          (IH fun j ja => ha j (Finset.mem_insert_of_mem ja))

Premises used: Insert.insert, lowerSemicontinuousWithinAt_const, Finset.sum_insert, not_false_iff
-- 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, LowerSemicontinuousWithinAt (f i) s x
empty :
  ∀ (ha : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → LowerSemicontinuousWithinAt (f i) s x),
    LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ ∅, f i z) s x
insert :
  ∀ (a : ι) (s_1 : Finset ι) (ia : a ∉ s_1)
    (IH :
      ∀ (ha : ∀ i ∈ s_1, LowerSemicontinuousWithinAt (f i) s x),
        LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ s_1, f i z) s x)
    (ha : ∀ i ∈ Insert.insert a s_1, LowerSemicontinuousWithinAt (f i) s x),
    LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ Insert.insert a s_1, f i z) s x
⊢ LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ a, f i z) s x

Tactic:
classical
    induction a using Finset.induction_on with
    | empty => exact lowerSemicontinuousWithinAt_const
    | insert _ _ ia IH =>
      simp only [ia, Finset.sum_insert, not_false_iff]
      exact
        LowerSemicontinuousWithinAt.add (ha _ (Finset.mem_insert_self ..))
          (IH fun j ja => ha j (Finset.mem_insert_of_mem ja))

Premises used: Insert.insert, lowerSemicontinuousWithinAt_const, Finset.sum_insert, not_false_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, LowerSemicontinuousAt (f i) x
simp_rw :
  ∀ (ha : ∀ i ∈ a, LowerSemicontinuousWithinAt (f i) univ x),
    LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ a, f i z) univ x
⊢ LowerSemicontinuousAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ a, f i z) 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 : α
ι : 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:
lowerSemicontinuousWithinAt_sum ha

Premises used: lowerSemicontinuousWithinAt_sum