awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst] s
hf : ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
x : α
y : γ
h : (x, y).1 ∈ s → (x, y).2 < f (x, y).1
hx : x ∉ s
a : α × γ
h₁ : a.1 ∈ sᶜ
h₂ : a.1 ∈ s
⊢ a.2 < f a.1

Tactic:
(h₁ h₂).elim

Premises used: False.elim
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst] s
hf : ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
x : α
y : γ
h : (x, y).1 ∈ s → (x, y).2 < f (x, y).1
hx : x ∉ s
h₁ :
  ∀ (a : α × γ),
    Membership.mem (γ := Set (α × γ))
      {x : α × γ |
        Membership.mem (γ := Set (α × γ)) {x : α × γ | (fun (x : α × γ) ↦ x.1 ∈ sᶜ) x} x →
          Membership.mem (γ := Set (α × γ)) {x : α × γ | (fun (a : α × γ) ↦ a.1 ∈ s → a.2 < f a.1) x} x}
      a
h₂ h₃ : ∀ (a : α × γ) (h₁ : a.1 ∈ sᶜ) (h₂ : a.1 ∈ s), a.2 < f a.1
⊢ ∀ᶠ (a : α × γ) in 𝓝 (x, y), a.1 ∈ s → a.2 < f a.1

Tactic:
filter_upwards [(continuous_fst.tendsto _).eventually (hs.isOpen_compl.eventually_mem hx)]
        with _ h₁ h₂ using (h₁ h₂).elim
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst] s
hf : ∀ (x : α × γ), (x.1 ∈ s → x.2 < f x.1) → ∀ᶠ (a : α × γ) in 𝓝 x, a.1 ∈ s → a.2 < f a.1
x : α
mpr : x ∈ s → ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
⊢ x ∈ s → ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x

Tactic:
_
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst] s
hf : ∀ (x : α × γ), (x.1 ∈ s → x.2 < f x.1) → ∀ᶠ (a : α × γ) in 𝓝 x, a.1 ∈ s → a.2 < f a.1
x : α
h : x ∈ s
y : γ
hy : y < f x
⊢ ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x

Tactic:
((Continuous.prodMk_left y).tendsto x).eventually (hf (x, y) (fun _ => hy))

Premises used: Set.Mem, Prod.mk, Continuous.tendsto, Filter.Tendsto.eventually, Continuous.prodMk_left
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst] s
hf : ∀ (x : α × γ), (x.1 ∈ s → x.2 < f x.1) → ∀ᶠ (a : α × γ) in 𝓝 x, a.1 ∈ s → a.2 < f a.1
x : α
h : x ∈ s
y : γ
hy : y < f x
⊢ ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x

Tactic:
exact ((Continuous.prodMk_left y).tendsto x).eventually (hf (x, y) (fun _ => hy))

Premises used: Prod.mk, Continuous.tendsto, Filter.Tendsto.eventually, Continuous.prodMk_left
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : ClosedIciTopology γ
f : α → γ
⊢ LowerSemicontinuous f ↔ IsClosed[instTopologicalSpaceProd] {p : α × γ | f p.1 ≤ p.2}

Tactic:
simp [← lowerSemicontinuousOn_univ_iff, lowerSemicontinuousOn_iff_isClosed_epigraph]

Premises used: lowerSemicontinuousOn_iff_isClosed_epigraph, lowerSemicontinuousOn_univ_iff
-- 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 γ
δ : Type u_5
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : (g ∘ f) x > y
pos : ∀ (h : ∃ (l : γ), l < f x), ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : δ) ↦ (g ∘ f) x1 > x2) x' y
neg : ∀ (h : ∀ (l : γ), f x ≤ l), ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : δ) ↦ (g ∘ f) x1 > x2) x' y
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : δ) ↦ (g ∘ f) x1 > x2) x' y

Tactic:
by_cases! h : ∃ 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 γ
δ : Type u_5
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : (g ∘ f) x > y
h : ∃ (l : γ), l < f x
⊢ ∃ z < f x, Ioc z (f x) ⊆ g ⁻¹' Ioi y

Tactic:
exists_Ioc_subset_of_mem_nhds (hg (Ioi_mem_nhds hy)) h

Premises used: Ioi_mem_nhds, 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 γ
δ : Type u_5
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : (g ∘ f) x > y
h : ∃ (l : γ), l < f x
pos :
  ∀ (z : γ) (zlt : z < f x) (hz : Ioc z (f x) ⊆ g ⁻¹' Ioi y),
    ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : δ) ↦ (g ∘ f) x1 > x2) x' y
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : δ) ↦ (g ∘ f) x1 > x2) x' y

Tactic:
obtain ⟨z, zlt, hz⟩ : ∃ z < f x, Ioc z (f x) ⊆ g ⁻¹' Ioi y :=
      exists_Ioc_subset_of_mem_nhds (hg (Ioi_mem_nhds hy)) h

Premises used: Ioi_mem_nhds, Set.Ioi, 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 γ
δ : Type u_5
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : (g ∘ f) x > y
h : ∃ (l : γ), l < f x
z : γ
zlt : z < f x
hz : Ioc z (f x) ⊆ g ⁻¹' Ioi y
h₁ : ∀ (a : α) (ha : f a > z), (g ∘ f) a > y
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : δ) ↦ (g ∘ f) x1 > x2) x' y

Tactic:
filter_upwards [hf z zlt] with a ha
-- 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 γ
δ : Type u_5
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : (g ∘ f) x > y
h : ∃ (l : γ), l < f x
z : γ
zlt : z < f x
hz : Ioc z (f x) ⊆ g ⁻¹' Ioi y
a : α
ha : f a > z
⊢ min (f x) (f a) ∈ Ioc z (f x)

Tactic:
simp [zlt, ha]
-- 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 γ
δ : Type u_5
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : (g ∘ f) x > y
h : ∃ (l : γ), l < f x
z : γ
zlt : z < f x
hz : Ioc z (f x) ⊆ g ⁻¹' Ioi y
a : α
ha : f a > z
⊢ g (min (f x) (f a)) ≤ g (f a)

Tactic:
gmon (min_le_right _ _)

Premises used: min_le_right
-- 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 γ
δ : Type u_5
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : (g ∘ f) x > y
h : ∃ (l : γ), l < f x
z : γ
zlt : z < f x
hz : Ioc z (f x) ⊆ g ⁻¹' Ioi y
a : α
ha : f a > z
⊢ (g ∘ f) a > y

Tactic:
calc
      y < g (min (f x) (f a)) := hz (by simp [zlt, ha])
      _ ≤ g (f a) := gmon (min_le_right _ _)

Premises used: min_le_right, Min.min
-- 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 γ
δ : Type u_5
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : (g ∘ f) x > y
h : ∀ (l : γ), f x ≤ l
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : δ) ↦ (g ∘ f) x1 > x2) x' y

Tactic:
Filter.Eventually.of_forall fun a => hy.trans_le (gmon (h (f a)))

Premises used: Filter.Eventually.of_forall, LT.lt.trans_le
-- 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 γ
δ : Type u_5
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : (g ∘ f) x > y
h : ∀ (l : γ), f x ≤ l
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : δ) ↦ (g ∘ f) x1 > x2) x' y

Tactic:
exact Filter.Eventually.of_forall fun a => hy.trans_le (gmon (h (f a)))

Premises used: Filter.Eventually.of_forall, LT.lt.trans_le
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
δ : Type u_5
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousAt f x
gmon : Monotone g
simp : ∀ (hf : LowerSemicontinuousWithinAt f univ x), LowerSemicontinuousWithinAt (g ∘ f) univ x
⊢ LowerSemicontinuousAt (g ∘ f) x

Tactic:
simp only [← lowerSemicontinuousWithinAt_univ_iff] at hf ⊢

Premises used: lowerSemicontinuousWithinAt_univ_iff
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
δ : Type u_5
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
gmon : Monotone g
hf : LowerSemicontinuousWithinAt f univ x
⊢ LowerSemicontinuousWithinAt (g ∘ f) univ x

Tactic:
hg.comp_lowerSemicontinuousWithinAt hf gmon

Premises used: ContinuousAt.comp_lowerSemicontinuousWithinAt
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
δ : Type u_5
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
gmon : Monotone g
hf : LowerSemicontinuousWithinAt f univ x
⊢ LowerSemicontinuousWithinAt (g ∘ f) univ x

Tactic:
exact hg.comp_lowerSemicontinuousWithinAt hf gmon

Premises used: ContinuousAt.comp_lowerSemicontinuousWithinAt
-- 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 γ
δ : Type u_5
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderTopology δ
g : γ → δ
f : α → γ
hg : Continuous[inst_2, inst_5] g
hf : LowerSemicontinuousOn f s
gmon : Monotone g
⊢ LowerSemicontinuousOn (g ∘ f) s

Tactic:
fun x hx => hg.continuousAt.comp_lowerSemicontinuousWithinAt (hf x hx) gmon

Premises used: Continuous.continuousAt, ContinuousAt.comp_lowerSemicontinuousWithinAt, SemicontinuousOn
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
δ : Type u_5
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderTopology δ
g : γ → δ
f : α → γ
hg : Continuous[inst_2, inst_5] g
hf : LowerSemicontinuous f
gmon : Monotone g
⊢ LowerSemicontinuous (g ∘ f)

Tactic:
fun x =>
  hg.continuousAt.comp_lowerSemicontinuousAt (hf x) gmon

Premises used: ContinuousAt.comp_lowerSemicontinuousAt, Continuous.continuousAt, Semicontinuous
-- 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 γ
δ : Type u_5
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Antitone g
⊢ UpperSemicontinuousWithinAt (g ∘ f) s x

Tactic:
ContinuousAt.comp_lowerSemicontinuousWithinAt (δ := δᵒᵈ) hg hf gmon

Premises used: ContinuousAt.comp_lowerSemicontinuousWithinAt, OrderDual
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
δ : Type u_5
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousAt f x
gmon : Antitone g
⊢ UpperSemicontinuousAt (g ∘ f) x

Tactic:
ContinuousAt.comp_lowerSemicontinuousAt (δ := δᵒᵈ) hg hf gmon

Premises used: ContinuousAt.comp_lowerSemicontinuousAt, OrderDual
-- 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 γ
δ : Type u_5
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderTopology δ
g : γ → δ
f : α → γ
hg : Continuous[inst_2, inst_5] g
hf : LowerSemicontinuousOn f s
gmon : Antitone g
⊢ UpperSemicontinuousOn (g ∘ f) s

Tactic:
fun x hx => hg.continuousAt.comp_lowerSemicontinuousWithinAt_antitone (hf x hx) gmon

Premises used: ContinuousAt.comp_lowerSemicontinuousWithinAt_antitone, Continuous.continuousAt, SemicontinuousOn
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
δ : Type u_5
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderTopology δ
g : γ → δ
f : α → γ
hg : Continuous[inst_2, inst_5] g
hf : LowerSemicontinuous f
gmon : Antitone g
⊢ UpperSemicontinuous (g ∘ f)

Tactic:
fun x =>
  hg.continuousAt.comp_lowerSemicontinuousAt_antitone (hf x) gmon

Premises used: ContinuousAt.comp_lowerSemicontinuousAt_antitone, Continuous.continuousAt, Semicontinuous
-- 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 : Set γ) (v : Set γ),
    IsOpen[inst_4] u ∧ f x ∈ u ∧ IsOpen[inst_4] v ∧ g x ∈ v ∧ u ×ˢ v ⊆ {p : γ × γ | y < p.1 + p.2}

Tactic:
mem_nhds_prod_iff'.1 (hcont (isOpen_Ioi.mem_nhds hy))

Premises used: mem_nhds_prod_iff', isOpen_Ioi, IsOpen.mem_nhds, Iff.mp
-- 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
obtain :
  ∀ (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}),
    ∀ᶠ (x' : α) in 𝓝[s] 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:
obtain ⟨u, v, u_open, xu, v_open, xv, h⟩ :
    ∃ u v : Set γ,
      IsOpen u ∧ f x ∈ u ∧ IsOpen v ∧ g x ∈ v ∧ u ×ˢ v ⊆ { p : γ × γ | y < p.fst + p.snd } :=
    mem_nhds_prod_iff'.1 (hcont (isOpen_Ioi.mem_nhds hy))

Premises used: mem_nhds_prod_iff', isOpen_Ioi, IsOpen.mem_nhds, Iff.mp, Set
-- 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}
pos :
  ∀ (hx₁ : ∃ (l : γ), l < f x), ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : γ) ↦ (fun (z : α) ↦ f z + g z) x1 > x2) x' y
neg :
  ∀ (hx₁ : ¬∃ (l : γ), l < f x), ∀ᶠ (x' : α) in 𝓝[s] 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:
by_cases hx₁ : ∃ l, l < f x
-- 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₁ : ∃ (l : γ), l < f x
⊢ ∃ z₁ < f x, Ioc z₁ (f x) ⊆ u

Tactic:
exists_Ioc_subset_of_mem_nhds (u_open.mem_nhds xu) hx₁

Premises used: exists_Ioc_subset_of_mem_nhds, IsOpen.mem_nhds
-- 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₁ : ∃ (l : γ), l < f x
pos :
  ∀ (z₁ : γ) (z₁lt : z₁ < f x) (h₁ : Ioc z₁ (f x) ⊆ u),
    ∀ᶠ (x' : α) in 𝓝[s] 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:
obtain ⟨z₁, z₁lt, h₁⟩ : ∃ z₁ < f x, Ioc z₁ (f x) ⊆ u :=
      exists_Ioc_subset_of_mem_nhds (u_open.mem_nhds xu) hx₁

Premises used: exists_Ioc_subset_of_mem_nhds, IsOpen.mem_nhds
-- 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₁ : ∃ (l : γ), l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
pos :
  ∀ (hx₂ : ∃ (l : γ), l < g x), ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : γ) ↦ (fun (z : α) ↦ f z + g z) x1 > x2) x' y
neg :
  ∀ (hx₂ : ¬∃ (l : γ), l < g x), ∀ᶠ (x' : α) in 𝓝[s] 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:
by_cases hx₂ : ∃ l, l < g x
-- 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₁ : ∃ (l : γ), l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∃ (l : γ), l < g x
⊢ ∃ z₂ < g x, Ioc z₂ (g x) ⊆ v

Tactic:
exists_Ioc_subset_of_mem_nhds (v_open.mem_nhds xv) hx₂

Premises used: exists_Ioc_subset_of_mem_nhds, IsOpen.mem_nhds
-- 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₁ : ∃ (l : γ), l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∃ (l : γ), l < g x
pos :
  ∀ (z₂ : γ) (z₂lt : z₂ < g x) (h₂ : Ioc z₂ (g x) ⊆ v),
    ∀ᶠ (x' : α) in 𝓝[s] 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:
obtain ⟨z₂, z₂lt, h₂⟩ : ∃ z₂ < g x, Ioc z₂ (g x) ⊆ v :=
        exists_Ioc_subset_of_mem_nhds (v_open.mem_nhds xv) hx₂

Premises used: exists_Ioc_subset_of_mem_nhds, IsOpen.mem_nhds
-- 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₁ : ∃ (l : γ), l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∃ (l : γ), l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
h₃ : ∀ (z : α) (h₁z : f z > z₁) (h₂z : g z > z₂), f z + g z > y
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : γ) ↦ (fun (z : α) ↦ f z + g z) x1 > x2) x' y

Tactic:
filter_upwards [hf z₁ z₁lt, hg z₂ z₂lt] with z h₁z h₂z
-- 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₁ : ∃ (l : γ), l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∃ (l : γ), l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₁z : f z > z₁
h₂z : g z > z₂
pos : ∀ (H : f z ≤ f x), min (f z) (f x) ∈ u
neg : ∀ (H : f x < f z), min (f z) (f x) ∈ u
⊢ min (f z) (f x) ∈ u

Tactic:
by_cases! H : f z ≤ f x