-- Mathlib/Topology/Semicontinuous.lean
theorem LowerSemicontinuousWithinAt.add' {f g : α → γ} (hf : LowerSemicontinuousWithinAt f s x)
    (hg : LowerSemicontinuousWithinAt g s x)
    (hcont : ContinuousAt (fun p : γ × γ => p.1 + p.2) (f x, g x)) :
    LowerSemicontinuousWithinAt (fun z => f z + g z) s x

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
s : Set α
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.1 + p.2) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen 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 : z₁ < f z
h₂z : z₂ < g z
⊢ f z ⊓ f x ∈ u

Tactic:
by_cases H : f z ≤ f x

Result:
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
s : Set α
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.1 + p.2) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen 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 : z₁ < f z
h₂z : z₂ < g z
H : f z ≤ f x
⊢ f z ⊓ f x ∈ u

case neg
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
s : Set α
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.1 + p.2) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen 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 : z₁ < f z
h₂z : z₂ < g z
H : ¬f z ≤ f x
⊢ f z ⊓ f x ∈ u

Proof state:
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
s : Set α
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.1 + p.2) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen 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, y < (fun z => f z + g z) x'

Tactic:
by_cases hx₂ : ∃ l, l < g x

Result:
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
s : Set α
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.1 + p.2) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen 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, y < (fun z => f z + g z) x'

case neg
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
s : Set α
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.1 + p.2) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen 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, y < (fun z => f z + g z) x'

Proof state:
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
s : Set α
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.1 + p.2) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen 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 : z₁ < f z
H : f z ≤ f x
⊢ f z ⊓ f x ∈ u

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

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
s : Set α
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.1 + p.2) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen 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 : z₂ < g z
A2 : g z ⊓ g x ∈ v
⊢ y < f z + g z

Tactic:
have : (f x, min (g z) (g x)) ∈ u ×ˢ v := ⟨xu, A2⟩

Result:
case h
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
s : Set α
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.1 + p.2) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen 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 : z₂ < g z
A2 : g z ⊓ g x ∈ v
this : (f x, g z ⊓ g x) ∈ u ×ˢ v
⊢ y < f z + g z

Proof state:
case pos.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
s : Set α
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.1 + p.2) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen 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, y < (fun z => f z + g z) x'

Tactic:
filter_upwards [hg z₂ z₂lt] with z h₂z

Result:
case h
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
s : Set α
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.1 + p.2) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen 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 : z₂ < g z
⊢ y < f z + g z