-- 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:
case h.e'_4
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
⊢ ↑f ⟨x, hfx⟩ = ↑(LinearPMap.sSup c hcd) ⟨x, hx⟩

Tactic:
exact this.2 rfl

Result:
no goals

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 ≠ ⊤
⊢ ∃ y ∈ S, q ≤ y ∧ ¬y ≤ q

Tactic:
have hqd : ∀ y, ∃ x : q.domain, (x : E) + y ∈ s := fun y ↦
  let ⟨x, hx⟩ := hp_dense y
  ⟨Submodule.inclusion hpq.left x, hx⟩

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 : q.domain ≠ ⊤
hqd : ∀ (y : E), ∃ x, ↑x + y ∈ s
⊢ ∃ y ∈ S, q ≤ y ∧ ¬y ≤ q

Proof state:
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

Tactic:
exact ⟨r, hr, hqr.le, fun hrq ↦ hqr.ne' <| hrq.antisymm hqr.le⟩

Result:
no goals

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 : ∀ ⦃y : E →ₗ.[ℝ] ℝ⦄, (fun x => x ∈ S) y → q ≤ y → y ≤ q
⊢ q.domain = ⊤

Tactic:
contrapose! hq

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 : q.domain ≠ ⊤
⊢ ∃ y ∈ S, q ≤ y ∧ ¬y ≤ q

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 : ∀ ⦃y : E →ₗ.[ℝ] ℝ⦄, (fun x => x ∈ S) y → q ≤ y → y ≤ q
⊢ ∃ q ≥ p, q.domain = ⊤ ∧ ∀ (x : ↥q.domain), ↑x ∈ s → 0 ≤ ↑q x

Tactic:
refine ⟨q, hpq, ?_, hqs⟩

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.domain = ⊤

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 ⊆ S, IsChain (fun x1 x2 => x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub

Tactic:
intro c hcs c_chain y hy

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}
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 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⟩

Tactic:
convert ← hcs hfc ⟨x, hfx⟩ hxs using 1

Result:
case h.e'_4
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
⊢ ↑f ⟨x, hfx⟩ = ↑(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
cne : c.Nonempty
hcd : DirectedOn (fun x1 x2 => x1 ≤ x2) c
⊢ ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub

Tactic:
refine ⟨LinearPMap.sSup c hcd, ?_, fun _ ↦ LinearPMap.le_sSup hcd⟩

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
hcd : DirectedOn (fun x1 x2 => x1 ≤ x2) c
⊢ LinearPMap.sSup c hcd ∈ S