𝕜 : Type ?u.268240
E : Type u_1
F : Type ?u.268246
G : Type ?u.268249
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
⊢ ∃ q, q ≥ p ∧ q.domain = ⊤ ∧ ∀ (x : { x // x ∈ q.domain }), ↑x ∈ s → 0 ≤ ↑q x
𝕜 : Type ?u.268240
E : Type u_1
F : Type ?u.268246
G : Type ?u.268249
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
⊢ ∃ q, q ≥ p ∧ q.domain = ⊤ ∧ ∀ (x : { x // x ∈ q.domain }), ↑x ∈ s → 0 ≤ ↑q x
set S := { p : E →ₗ.[ℝ] ℝ | ∀ x : p.domain, (x : E) ∈ s → 0 ≤ p x }
case intro.intro.intro
𝕜 : Type ?u.268240
E : Type u_1
F : Type ?u.268246
G : Type ?u.268249
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
hSc :
  ∀ (c : Set (E →ₗ.[ℝ] ℝ)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : E →ₗ.[ℝ] ℝ), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : E →ₗ.[ℝ] ℝ), z ∈ c → z ≤ ub
q : E →ₗ.[ℝ] ℝ
hqs : q ∈ S
hpq : p ≤ q
hq : ∀ (z : E →ₗ.[ℝ] ℝ), z ∈ S → q ≤ z → z = q
⊢ ∃ q, q ≥ p ∧ q.domain = ⊤ ∧ ∀ (x : { x // x ∈ q.domain }), ↑x ∈ s → 0 ≤ ↑q x
𝕜 : Type ?u.268240
E : Type u_1
F : Type ?u.268246
G : Type ?u.268249
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
hSc :
  ∀ (c : Set (E →ₗ.[ℝ] ℝ)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : E →ₗ.[ℝ] ℝ), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : E →ₗ.[ℝ] ℝ), z ∈ c → z ≤ ub
⊢ ∃ q, q ≥ p ∧ q.domain = ⊤ ∧ ∀ (x : { x // x ∈ q.domain }), ↑x ∈ s → 0 ≤ ↑q x
obtain ⟨q, hqs, hpq, hq⟩ := zorn_nonempty_partialOrder₀ S hSc p hp_nonneg
case hSc
𝕜 : Type ?u.268240
E : Type u_1
F : Type ?u.268246
G : Type ?u.268249
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x x_1 => x ≤ x_1) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
⊢ ∃ ub, ub ∈ S ∧ ∀ (z : E →ₗ.[ℝ] ℝ), z ∈ c → z ≤ ub
case hSc
𝕜 : Type ?u.268240
E : Type u_1
F : Type ?u.268246
G : Type ?u.268249
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
⊢ ∀ (c : Set (E →ₗ.[ℝ] ℝ)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : E →ₗ.[ℝ] ℝ), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : E →ₗ.[ℝ] ℝ), z ∈ c → z ≤ ub
intro c hcs c_chain y hy
case hSc
𝕜 : Type ?u.268240
E : Type u_1
F : Type ?u.268246
G : Type ?u.268249
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x x_1 => x ≤ x_1) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
⊢ ∃ ub, ub ∈ S ∧ ∀ (z : E →ₗ.[ℝ] ℝ), z ∈ c → z ≤ ub
case hSc
𝕜 : Type ?u.268240
E : Type u_1
F : Type ?u.268246
G : Type ?u.268249
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x x_1 => x ≤ x_1) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
⊢ ∃ ub, ub ∈ S ∧ ∀ (z : E →ₗ.[ℝ] ℝ), z ∈ c → z ≤ ub
clear hp_nonneg hp_dense p
case hSc
𝕜 : Type ?u.268240
E : Type u_1
F : Type ?u.268246
G : Type ?u.268249
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x x_1 => x ≤ x_1) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : Set.Nonempty c
⊢ ∃ ub, ub ∈ S ∧ ∀ (z : E →ₗ.[ℝ] ℝ), z ∈ c → z ≤ ub
case hSc
𝕜 : Type ?u.268240
E : Type u_1
F : Type ?u.268246
G : Type ?u.268249
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x x_1 => x ≤ x_1) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
⊢ ∃ ub, ub ∈ S ∧ ∀ (z : E →ₗ.[ℝ] ℝ), z ∈ c → z ≤ ub
have cne : c.Nonempty := ⟨y, hy⟩
case hSc
𝕜 : Type ?u.268240
E : Type u_1
F : Type ?u.268246
G : Type ?u.268249
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x x_1 => x ≤ x_1) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : Set.Nonempty c
hcd : DirectedOn (fun x x_1 => x ≤ x_1) c
⊢ LinearPMap.sSup c hcd ∈ S
case hSc
𝕜 : Type ?u.268240
E : Type u_1
F : Type ?u.268246
G : Type ?u.268249
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x x_1 => x ≤ x_1) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : Set.Nonempty c
hcd : DirectedOn (fun x x_1 => x ≤ x_1) c
⊢ ∃ ub, ub ∈ S ∧ ∀ (z : E →ₗ.[ℝ] ℝ), z ∈ c → z ≤ ub
refine' ⟨LinearPMap.sSup c hcd, _, fun _ ↦ LinearPMap.le_sSup hcd⟩
case hSc.mk
𝕜 : Type ?u.268240
E : Type u_1
F : Type ?u.268246
G : Type ?u.268249
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x x_1 => x ≤ x_1) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : Set.Nonempty c
hcd : DirectedOn (fun x x_1 => x ≤ x_1) c
x : E
hx : x ∈ (LinearPMap.sSup c hcd).domain
hxs : ↑{ val := x, property := hx } ∈ s
⊢ 0 ≤ ↑(LinearPMap.sSup c hcd) { val := x, property := hx }
case hSc
𝕜 : Type ?u.268240
E : Type u_1
F : Type ?u.268246
G : Type ?u.268249
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x x_1 => x ≤ x_1) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : Set.Nonempty c
hcd : DirectedOn (fun x x_1 => x ≤ x_1) c
⊢ LinearPMap.sSup c hcd ∈ S
rintro ⟨x, hx⟩ hxs
case hSc.mk.intro.intro.intro.intro
𝕜 : Type ?u.268240
E : Type u_1
F : Type ?u.268246
G : Type ?u.268249
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f✝ : E →ₗ.[ℝ] ℝ
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x x_1 => x ≤ x_1) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : Set.Nonempty c
hcd : DirectedOn (fun x x_1 => x ≤ x_1) c
x : E
hx : x ∈ (LinearPMap.sSup c hcd).domain
hxs : ↑{ val := x, property := hx } ∈ s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) (LinearPMap.domain '' c)
f : E →ₗ.[ℝ] ℝ
hfc : f ∈ c
hfx : x ∈ f.domain
⊢ 0 ≤ ↑(LinearPMap.sSup c hcd) { val := x, property := hx }
case hSc.mk
𝕜 : Type ?u.268240
E : Type u_1
F : Type ?u.268246
G : Type ?u.268249
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x x_1 => x ≤ x_1) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : Set.Nonempty c
hcd : DirectedOn (fun x x_1 => x ≤ x_1) c
x : E
hx : x ∈ (LinearPMap.sSup c hcd).domain
hxs : ↑{ val := x, property := hx } ∈ s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) (LinearPMap.domain '' c)
⊢ 0 ≤ ↑(LinearPMap.sSup c hcd) { val := x, property := hx }
rcases (mem_sSup_of_directed (cne.image _) hdir).1 hx with ⟨_, ⟨f, hfc, rfl⟩, hfx⟩
case hSc.mk.intro.intro.intro.intro
𝕜 : Type ?u.268240
E : Type u_1
F : Type ?u.268246
G : Type ?u.268249
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f✝ : E →ₗ.[ℝ] ℝ
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x x_1 => x ≤ x_1) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : Set.Nonempty c
hcd : DirectedOn (fun x x_1 => x ≤ x_1) c
x : E
hx : x ∈ (LinearPMap.sSup c hcd).domain
hxs : ↑{ val := x, property := hx } ∈ s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) (LinearPMap.domain '' c)
f : E →ₗ.[ℝ] ℝ
hfc : f ∈ c
hfx : x ∈ f.domain
this : f ≤ LinearPMap.sSup c hcd
⊢ 0 ≤ ↑(LinearPMap.sSup c hcd) { val := x, property := hx }
case hSc.mk.intro.intro.intro.intro
𝕜 : Type ?u.268240
E : Type u_1
F : Type ?u.268246
G : Type ?u.268249
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f✝ : E →ₗ.[ℝ] ℝ
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x x_1 => x ≤ x_1) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : Set.Nonempty c
hcd : DirectedOn (fun x x_1 => x ≤ x_1) c
x : E
hx : x ∈ (LinearPMap.sSup c hcd).domain
hxs : ↑{ val := x, property := hx } ∈ s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) (LinearPMap.domain '' c)
f : E →ₗ.[ℝ] ℝ
hfc : f ∈ c
hfx : x ∈ f.domain
⊢ 0 ≤ ↑(LinearPMap.sSup c hcd) { val := x, property := hx }
have : f ≤ LinearPMap.sSup c hcd := LinearPMap.le_sSup _ hfc
case h.e'_4
𝕜 : Type ?u.268240
E : Type u_1
F : Type ?u.268246
G : Type ?u.268249
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f✝ : E →ₗ.[ℝ] ℝ
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x x_1 => x ≤ x_1) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : Set.Nonempty c
hcd : DirectedOn (fun x x_1 => x ≤ x_1) c
x : E
hx : x ∈ (LinearPMap.sSup c hcd).domain
hxs : ↑{ val := x, property := hx } ∈ s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) (LinearPMap.domain '' c)
f : E →ₗ.[ℝ] ℝ
hfc : f ∈ c
hfx : x ∈ f.domain
this : f ≤ LinearPMap.sSup c hcd
⊢ ↑f { val := x, property := hfx } = ↑(LinearPMap.sSup c hcd) { val := x, property := hx }
case hSc.mk.intro.intro.intro.intro
𝕜 : Type ?u.268240
E : Type u_1
F : Type ?u.268246
G : Type ?u.268249
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f✝ : E →ₗ.[ℝ] ℝ
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x x_1 => x ≤ x_1) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : Set.Nonempty c
hcd : DirectedOn (fun x x_1 => x ≤ x_1) c
x : E
hx : x ∈ (LinearPMap.sSup c hcd).domain
hxs : ↑{ val := x, property := hx } ∈ s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) (LinearPMap.domain '' c)
f : E →ₗ.[ℝ] ℝ
hfc : f ∈ c
hfx : x ∈ f.domain
this : f ≤ LinearPMap.sSup c hcd
⊢ 0 ≤ ↑(LinearPMap.sSup c hcd) { val := x, property := hx }
convert ← hcs hfc ⟨x, hfx⟩ hxs using 1
no goals
case h.e'_4
𝕜 : Type ?u.268240
E : Type u_1
F : Type ?u.268246
G : Type ?u.268249
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f✝ : E →ₗ.[ℝ] ℝ
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x x_1 => x ≤ x_1) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : Set.Nonempty c
hcd : DirectedOn (fun x x_1 => x ≤ x_1) c
x : E
hx : x ∈ (LinearPMap.sSup c hcd).domain
hxs : ↑{ val := x, property := hx } ∈ s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) (LinearPMap.domain '' c)
f : E →ₗ.[ℝ] ℝ
hfc : f ∈ c
hfx : x ∈ f.domain
this : f ≤ LinearPMap.sSup c hcd
⊢ ↑f { val := x, property := hfx } = ↑(LinearPMap.sSup c hcd) { val := x, property := hx }
exact this.2 rfl
case intro.intro.intro
𝕜 : Type ?u.268240
E : Type u_1
F : Type ?u.268246
G : Type ?u.268249
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
hSc :
  ∀ (c : Set (E →ₗ.[ℝ] ℝ)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : E →ₗ.[ℝ] ℝ), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : E →ₗ.[ℝ] ℝ), z ∈ c → z ≤ ub
q : E →ₗ.[ℝ] ℝ
hqs : q ∈ S
hpq : p ≤ q
hq : ∀ (z : E →ₗ.[ℝ] ℝ), z ∈ S → q ≤ z → z = q
⊢ q.domain = ⊤
case intro.intro.intro
𝕜 : Type ?u.268240
E : Type u_1
F : Type ?u.268246
G : Type ?u.268249
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
hSc :
  ∀ (c : Set (E →ₗ.[ℝ] ℝ)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : E →ₗ.[ℝ] ℝ), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : E →ₗ.[ℝ] ℝ), z ∈ c → z ≤ ub
q : E →ₗ.[ℝ] ℝ
hqs : q ∈ S
hpq : p ≤ q
hq : ∀ (z : E →ₗ.[ℝ] ℝ), z ∈ S → q ≤ z → z = q
⊢ ∃ q, q ≥ p ∧ q.domain = ⊤ ∧ ∀ (x : { x // x ∈ q.domain }), ↑x ∈ s → 0 ≤ ↑q x
refine' ⟨q, hpq, _, hqs⟩
case intro.intro.intro
𝕜 : Type ?u.268240
E : Type u_1
F : Type ?u.268246
G : Type ?u.268249
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
hSc :
  ∀ (c : Set (E →ₗ.[ℝ] ℝ)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : E →ₗ.[ℝ] ℝ), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : E →ₗ.[ℝ] ℝ), z ∈ c → z ≤ ub
q : E →ₗ.[ℝ] ℝ
hqs : q ∈ S
hpq : p ≤ q
hq : q.domain ≠ ⊤
⊢ ∃ z, z ∈ {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x} ∧ q ≤ z ∧ z ≠ q
case intro.intro.intro
𝕜 : Type ?u.268240
E : Type u_1
F : Type ?u.268246
G : Type ?u.268249
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
hSc :
  ∀ (c : Set (E →ₗ.[ℝ] ℝ)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : E →ₗ.[ℝ] ℝ), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : E →ₗ.[ℝ] ℝ), z ∈ c → z ≤ ub
q : E →ₗ.[ℝ] ℝ
hqs : q ∈ S
hpq : p ≤ q
hq : ∀ (z : E →ₗ.[ℝ] ℝ), z ∈ S → q ≤ z → z = q
⊢ q.domain = ⊤
contrapose! hq
case intro.intro.intro
𝕜 : Type ?u.268240
E : Type u_1
F : Type ?u.268246
G : Type ?u.268249
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
hSc :
  ∀ (c : Set (E →ₗ.[ℝ] ℝ)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : E →ₗ.[ℝ] ℝ), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : E →ₗ.[ℝ] ℝ), z ∈ c → z ≤ ub
q : E →ₗ.[ℝ] ℝ
hqs : q ∈ S
hpq : p ≤ q
hq : q.domain ≠ ⊤
hqd : ∀ (y : E), ∃ x, ↑x + y ∈ s
⊢ ∃ z, z ∈ {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x} ∧ q ≤ z ∧ z ≠ q
case intro.intro.intro
𝕜 : Type ?u.268240
E : Type u_1
F : Type ?u.268246
G : Type ?u.268249
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
hSc :
  ∀ (c : Set (E →ₗ.[ℝ] ℝ)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : E →ₗ.[ℝ] ℝ), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : E →ₗ.[ℝ] ℝ), z ∈ c → z ≤ ub
q : E →ₗ.[ℝ] ℝ
hqs : q ∈ S
hpq : p ≤ q
hq : q.domain ≠ ⊤
⊢ ∃ z, z ∈ {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x} ∧ q ≤ z ∧ z ≠ q
have hqd : ∀ y, ∃ x : q.domain, (x : E) + y ∈ s := fun y ↦
  let ⟨x, hx⟩ := hp_dense y
  ⟨ofLe hpq.left x, hx⟩
case intro.intro.intro.intro.intro
𝕜 : Type ?u.268240
E : Type u_1
F : Type ?u.268246
G : Type ?u.268249
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
hSc :
  ∀ (c : Set (E →ₗ.[ℝ] ℝ)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : E →ₗ.[ℝ] ℝ), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : E →ₗ.[ℝ] ℝ), z ∈ c → z ≤ ub
q : E →ₗ.[ℝ] ℝ
hqs : q ∈ S
hpq : p ≤ q
hq : q.domain ≠ ⊤
hqd : ∀ (y : E), ∃ x, ↑x + y ∈ s
r : E →ₗ.[ℝ] ℝ
hqr : q < r
hr : ∀ (x : { x // x ∈ r.domain }), ↑x ∈ s → 0 ≤ ↑r x
⊢ ∃ z, z ∈ {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x} ∧ q ≤ z ∧ z ≠ q
case intro.intro.intro
𝕜 : Type ?u.268240
E : Type u_1
F : Type ?u.268246
G : Type ?u.268249
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
hSc :
  ∀ (c : Set (E →ₗ.[ℝ] ℝ)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : E →ₗ.[ℝ] ℝ), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : E →ₗ.[ℝ] ℝ), z ∈ c → z ≤ ub
q : E →ₗ.[ℝ] ℝ
hqs : q ∈ S
hpq : p ≤ q
hq : q.domain ≠ ⊤
hqd : ∀ (y : E), ∃ x, ↑x + y ∈ s
⊢ ∃ z, z ∈ {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x} ∧ q ≤ z ∧ z ≠ q
rcases step s q hqs hqd hq with ⟨r, hqr, hr⟩
no goals
case intro.intro.intro.intro.intro
𝕜 : Type ?u.268240
E : Type u_1
F : Type ?u.268246
G : Type ?u.268249
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
hSc :
  ∀ (c : Set (E →ₗ.[ℝ] ℝ)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : E →ₗ.[ℝ] ℝ), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : E →ₗ.[ℝ] ℝ), z ∈ c → z ≤ ub
q : E →ₗ.[ℝ] ℝ
hqs : q ∈ S
hpq : p ≤ q
hq : q.domain ≠ ⊤
hqd : ∀ (y : E), ∃ x, ↑x + y ∈ s
r : E →ₗ.[ℝ] ℝ
hqr : q < r
hr : ∀ (x : { x // x ∈ r.domain }), ↑x ∈ s → 0 ≤ ↑r x
⊢ ∃ z, z ∈ {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x} ∧ q ≤ z ∧ z ≠ q
exact ⟨r, hr, hqr.le, hqr.ne'⟩