-- Mathlib/Analysis/Convex/Cone/Extension.lean
theorem exists_top (p : E →ₗ.[ℝ] ℝ) (hp_nonneg : ∀ x : p.domain, (x : E) ∈ s → 0 ≤ p x)
    (hp_dense : ∀ y, ∃ x : p.domain, (x : E) + y ∈ s) :
    ∃ q ≥ p, q.domain = ⊤ ∧ ∀ x : q.domain, (x : E) ∈ s → 0 ≤ q x

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x}
hSc : ∀ c ⊆ S, IsChain (fun x1 x2 => x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
⊢ ∃ q ≥ p, q.domain = ⊤ ∧ ∀ (x : ↥q.domain), ↑x ∈ s → 0 ≤ ↑q x

Tactic:
obtain ⟨q, hpq, hqs, hq⟩ := zorn_le_nonempty₀ S hSc p hp_nonneg

Result:
case intro.intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x}
hSc : ∀ c ⊆ S, IsChain (fun x1 x2 => x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
q : E →ₗ.[ℝ] ℝ
hpq : p ≤ q
hqs : q ∈ S
hq : ∀ ⦃y : E →ₗ.[ℝ] ℝ⦄, (fun x => x ∈ S) y → q ≤ y → y ≤ q
⊢ ∃ q ≥ p, q.domain = ⊤ ∧ ∀ (x : ↥q.domain), ↑x ∈ s → 0 ≤ ↑q x

Proof state:
case mk
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x1 x2 => x1 ≤ x2) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : c.Nonempty
hcd : DirectedOn (fun x1 x2 => x1 ≤ x2) c
x : E
hx : x ∈ (LinearPMap.sSup c hcd).domain
hxs : ↑⟨x, hx⟩ ∈ s
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) (LinearPMap.domain '' c)
⊢ 0 ≤ ↑(LinearPMap.sSup c hcd) ⟨x, hx⟩

Tactic:
rcases (mem_sSup_of_directed (cne.image _) hdir).1 hx with ⟨_, ⟨f, hfc, rfl⟩, hfx⟩

Result:
case mk.intro.intro.intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x1 x2 => x1 ≤ x2) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : c.Nonempty
hcd : DirectedOn (fun x1 x2 => x1 ≤ x2) c
x : E
hx : x ∈ (LinearPMap.sSup c hcd).domain
hxs : ↑⟨x, hx⟩ ∈ s
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) (LinearPMap.domain '' c)
f : E →ₗ.[ℝ] ℝ
hfc : f ∈ c
hfx : x ∈ f.domain
⊢ 0 ≤ ↑(LinearPMap.sSup c hcd) ⟨x, hx⟩

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x1 x2 => x1 ≤ x2) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
⊢ ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub

Tactic:
have cne : c.Nonempty := ⟨y, hy⟩

Result:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x1 x2 => x1 ≤ x2) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : c.Nonempty
⊢ ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
⊢ ∃ q ≥ p, q.domain = ⊤ ∧ ∀ (x : ↥q.domain), ↑x ∈ s → 0 ≤ ↑q x

Tactic:
set S := { p : E →ₗ.[ℝ] ℝ | ∀ x : p.domain, (x : E) ∈ s → 0 ≤ p x }

Result:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x}
⊢ ∃ q ≥ p, q.domain = ⊤ ∧ ∀ (x : ↥q.domain), ↑x ∈ s → 0 ≤ ↑q x

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x1 x2 => x1 ≤ x2) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
⊢ ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub

Tactic:
clear hp_nonneg hp_dense p

Result:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x1 x2 => x1 ≤ x2) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
⊢ ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub

Proof state:
case intro.intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x}
hSc : ∀ c ⊆ S, IsChain (fun x1 x2 => x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
q : E →ₗ.[ℝ] ℝ
hpq : p ≤ q
hqs : q ∈ S
hq : q.domain ≠ ⊤
hqd : ∀ (y : E), ∃ x, ↑x + y ∈ s
⊢ ∃ y ∈ S, q ≤ y ∧ ¬y ≤ q

Tactic:
rcases step s q hqs hqd hq with ⟨r, hqr, hr⟩

Result:
case intro.intro.intro.intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x}
hSc : ∀ c ⊆ S, IsChain (fun x1 x2 => x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
q : E →ₗ.[ℝ] ℝ
hpq : p ≤ q
hqs : q ∈ S
hq : q.domain ≠ ⊤
hqd : ∀ (y : E), ∃ x, ↑x + y ∈ s
r : E →ₗ.[ℝ] ℝ
hqr : q < r
hr : ∀ (x : ↥r.domain), ↑x ∈ s → 0 ≤ ↑r x
⊢ ∃ y ∈ S, q ≤ y ∧ ¬y ≤ q

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x1 x2 => x1 ≤ x2) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : c.Nonempty
hcd : DirectedOn (fun x1 x2 => x1 ≤ x2) c
⊢ LinearPMap.sSup c hcd ∈ S

Tactic:
rintro ⟨x, hx⟩ hxs

Result:
case mk
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x1 x2 => x1 ≤ x2) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : c.Nonempty
hcd : DirectedOn (fun x1 x2 => x1 ≤ x2) c
x : E
hx : x ∈ (LinearPMap.sSup c hcd).domain
hxs : ↑⟨x, hx⟩ ∈ s
⊢ 0 ≤ ↑(LinearPMap.sSup c hcd) ⟨x, hx⟩

Proof state:
case mk.intro.intro.intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x1 x2 => x1 ≤ x2) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : c.Nonempty
hcd : DirectedOn (fun x1 x2 => x1 ≤ x2) c
x : E
hx : x ∈ (LinearPMap.sSup c hcd).domain
hxs : ↑⟨x, hx⟩ ∈ s
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) (LinearPMap.domain '' c)
f : E →ₗ.[ℝ] ℝ
hfc : f ∈ c
hfx : x ∈ f.domain
⊢ 0 ≤ ↑(LinearPMap.sSup c hcd) ⟨x, hx⟩

Tactic:
have : f ≤ LinearPMap.sSup c hcd := LinearPMap.le_sSup _ hfc

Result:
case mk.intro.intro.intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x1 x2 => x1 ≤ x2) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : c.Nonempty
hcd : DirectedOn (fun x1 x2 => x1 ≤ x2) c
x : E
hx : x ∈ (LinearPMap.sSup c hcd).domain
hxs : ↑⟨x, hx⟩ ∈ s
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) (LinearPMap.domain '' c)
f : E →ₗ.[ℝ] ℝ
hfc : f ∈ c
hfx : x ∈ f.domain
this : f ≤ LinearPMap.sSup c hcd
⊢ 0 ≤ ↑(LinearPMap.sSup c hcd) ⟨x, hx⟩