awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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}
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : γ) ↦ (fun (z : α) ↦ f z + g z) x1 > x2) x' y
have pos : ∀ (hx₁ : ∃ (l : γ), l < f x), ∀ᶠ (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
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : γ) ↦ (fun (z : α) ↦ f z + g z) x1 > x2) x' y
have neg : ∀ (hx₁ : ¬∃ (l : γ), l < f x), ∀ᶠ (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
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : γ) ↦ (fun (z : α) ↦ f z + g z) x1 > x2) x' y
have 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
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₁
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : γ) ↦ (fun (z : α) ↦ f z + g z) x1 > x2) x' y
have pos : ∀ (hx₂ : ∃ (l : γ), l < g x), ∀ᶠ (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
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : γ) ↦ (fun (z : α) ↦ f z + g z) x1 > x2) x' y
have neg : ∀ (hx₂ : ¬∃ (l : γ), l < g x), ∀ᶠ (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
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : γ) ↦ (fun (z : α) ↦ f z + g z) x1 > x2) x' y
have 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
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₂
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : γ) ↦ (fun (z : α) ↦ f z + g z) x1 > x2) x' y
have h₃ : ∀ (z : α) (h₁z : f z > z₁) (h₂z : g z > z₂), f z + g z > y
Tactic: filter_upwards [hf z₁ z₁lt, hg z₂ z₂lt] with z h₁z h₂z
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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₂
⊢ min (f z) (f x) ∈ u
have pos : ∀ (H : f z ≤ f x), min (f z) (f x) ∈ u
Tactic: by_cases! H : f z ≤ f x
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ min (f z) (f x) ∈ u
have neg : ∀ (H : f x < f z), min (f z) (f x) ∈ u
Tactic: by_cases! H : f z ≤ f x
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (hypothesis)
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₂
⊢ f z + g z > y
have A1 : min (f z) (f x) ∈ u
Tactic: have A1 : min (f z) (f x) ∈ u := by
        by_cases! H : f z ≤ f x
        · simpa [H] using h₁ ⟨h₁z, H⟩
        · simpa [H.le]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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₂
A1 : min (f z) (f x) ∈ u
⊢ min (g z) (g x) ∈ v
have pos : ∀ (H : g z ≤ g x), min (g z) (g x) ∈ v
Tactic: by_cases! H : g z ≤ g x
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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₂
A1 : min (f z) (f x) ∈ u
pos : ∀ (H : g z ≤ g x), min (g z) (g x) ∈ v
⊢ min (g z) (g x) ∈ v
have neg : ∀ (H : g x < g z), min (g z) (g x) ∈ v
Tactic: by_cases! H : g z ≤ g x
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (hypothesis)
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₂
A1 : min (f z) (f x) ∈ u
⊢ f z + g z > y
have A2 : 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]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (hypothesis)
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₂
A1 : min (f z) (f x) ∈ u
A2 : min (g z) (g x) ∈ v
⊢ f z + g z > y
have this : (min (f z) (f x), min (g z) (g x)) ∈ u ×ˢ v
Tactic: have : (min (f z) (f x), min (g z) (g x)) ∈ u ×ˢ v := ⟨A1, A2⟩
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (hypothesis)
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
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : γ) ↦ (fun (z : α) ↦ f z + g z) x1 > x2) x' y
have hx₃ : ∀ (x_1 : γ), g x ≤ x_1
Tactic: simp only [not_exists, not_lt] at hx₂
Cleared hypotheses: hx₂
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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₂ : ∀ (x_1 : γ), g x ≤ x_1
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : γ) ↦ (fun (z : α) ↦ f z + g z) x1 > x2) x' y
have h₂ : ∀ (z : α) (h₁z : f z > z₁), f z + g z > y
Tactic: filter_upwards [hf z₁ z₁lt] with z h₁z
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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₂ : ∀ (x_1 : γ), g x ≤ x_1
z : α
h₁z : f z > z₁
⊢ min (f z) (f x) ∈ u
have pos : ∀ (H : f z ≤ f x), min (f z) (f x) ∈ u
Tactic: by_cases! H : f z ≤ f x
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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₂ : ∀ (x_1 : γ), g x ≤ x_1
z : α
h₁z : f z > z₁
pos : ∀ (H : f z ≤ f x), min (f z) (f x) ∈ u
⊢ min (f z) (f x) ∈ u
have neg : ∀ (H : f x < f z), min (f z) (f x) ∈ u
Tactic: by_cases! H : f z ≤ f x
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (hypothesis)
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₂ : ∀ (x_1 : γ), g x ≤ x_1
z : α
h₁z : f z > z₁
⊢ f z + g z > y
have A1 : min (f z) (f x) ∈ u
Tactic: have A1 : min (f z) (f x) ∈ u := by
        by_cases! H : f z ≤ f x
        · simpa [H] using h₁ ⟨h₁z, H⟩
        · simpa [H.le]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (hypothesis)
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₂ : ∀ (x_1 : γ), g x ≤ x_1
z : α
h₁z : f z > z₁
A1 : min (f z) (f x) ∈ u
⊢ f z + g z > y
have this : (min (f z) (f x), g x) ∈ u ×ˢ v
Tactic: have : (min (f z) (f x), g x) ∈ u ×ˢ v := ⟨A1, xv⟩
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (hypothesis)
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
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : γ) ↦ (fun (z : α) ↦ f z + g z) x1 > x2) x' y
have hx₂ : ∀ (x_1 : γ), f x ≤ x_1
Tactic: simp only [not_exists, not_lt] at hx₁
Cleared hypotheses: hx₁
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : γ) ↦ (fun (z : α) ↦ f z + g z) x1 > x2) x' y
have pos : ∀ (hx₂ : ∃ (l : γ), l < g x), ∀ᶠ (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
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
pos :
  ∀ (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
have neg : ∀ (hx₂ : ¬∃ (l : γ), l < g x), ∀ᶠ (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
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : γ) ↦ (fun (z : α) ↦ f z + g z) x1 > x2) x' y
have 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
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₂
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : γ) ↦ (fun (z : α) ↦ f z + g z) x1 > x2) x' y
have h₁ : ∀ (z : α) (h₂z : g z > z₂), f z + g z > y
Tactic: filter_upwards [hg z₂ z₂lt] with z h₂z
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
have pos : ∀ (H : g z ≤ g x), min (g z) (g x) ∈ v
Tactic: by_cases! H : g z ≤ g x