awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
S : Set (E →ₗ.[ℝ] ℝ) := {p : E →ₗ.[ℝ] ℝ | ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : c.Nonempty
hcd : DirectedOn (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c
x : E
hx : x ∈ (LinearPMap.sSup c hcd).domain
hxs : (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ (LinearPMap.sSup c hcd).domain) x hx) : E) ∈ s
hdir : DirectedOn (fun (x1 x2 : Submodule ℝ E) ↦ x1 ≤ x2) (LinearPMap.domain '' c)
rcases :
  ∀ (f : E →ₗ.[ℝ] ℝ) (hfc : f ∈ c) (hfx : x ∈ f.domain),
    0 ≤
      (↑(LinearPMap.sSup c hcd) : ↥(LinearPMap.sSup c hcd).domain → ℝ)
        (Subtype.mk (p := fun (x : E) ↦ x ∈ (LinearPMap.sSup c hcd).domain) x hx)
⊢ 0 ≤
    (↑(LinearPMap.sSup c hcd) : ↥(LinearPMap.sSup c hcd).domain → ℝ)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ (LinearPMap.sSup c hcd).domain) x hx)

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

Premises used: Set.Nonempty.image, Iff.mp, Submodule.mem_sSup_of_directed, rfl
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
S : Set (E →ₗ.[ℝ] ℝ) := {p : E →ₗ.[ℝ] ℝ | ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : c.Nonempty
hcd : DirectedOn (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c
x : E
hx : x ∈ (LinearPMap.sSup c hcd).domain
hxs : (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ (LinearPMap.sSup c hcd).domain) x hx) : E) ∈ s
hdir : DirectedOn (fun (x1 x2 : Submodule ℝ E) ↦ x1 ≤ x2) (LinearPMap.domain '' c)
f : E →ₗ.[ℝ] ℝ
hfc : f ∈ c
hfx : x ∈ f.domain
⊢ f ≤ LinearPMap.sSup c hcd

Tactic:
have : f ≤ LinearPMap.sSup c hcd := LinearPMap.le_sSup _ hfc
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
S : Set (E →ₗ.[ℝ] ℝ) := {p : E →ₗ.[ℝ] ℝ | ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : c.Nonempty
hcd : DirectedOn (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c
x : E
hx : x ∈ (LinearPMap.sSup c hcd).domain
hxs : (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ (LinearPMap.sSup c hcd).domain) x hx) : E) ∈ s
hdir : DirectedOn (fun (x1 x2 : Submodule ℝ E) ↦ x1 ≤ x2) (LinearPMap.domain '' c)
f : E →ₗ.[ℝ] ℝ
hfc : f ∈ c
hfx : x ∈ f.domain
this : f ≤ LinearPMap.sSup c hcd
⊢ 0 ≤ (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx)

Tactic:
hcs hfc ⟨x, hfx⟩ hxs

Premises used: Subtype.mk
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
S : Set (E →ₗ.[ℝ] ℝ) := {p : E →ₗ.[ℝ] ℝ | ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : c.Nonempty
hcd : DirectedOn (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c
x : E
hx : x ∈ (LinearPMap.sSup c hcd).domain
hxs : (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ (LinearPMap.sSup c hcd).domain) x hx) : E) ∈ s
hdir : DirectedOn (fun (x1 x2 : Submodule ℝ E) ↦ x1 ≤ x2) (LinearPMap.domain '' c)
f : E →ₗ.[ℝ] ℝ
hfc : f ∈ c
hfx : x ∈ f.domain
this : f ≤ LinearPMap.sSup c hcd
h :
  (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx) =
    (↑(LinearPMap.sSup c hcd) : ↥(LinearPMap.sSup c hcd).domain → ℝ)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ (LinearPMap.sSup c hcd).domain) x hx)
⊢ 0 ≤
    (↑(LinearPMap.sSup c hcd) : ↥(LinearPMap.sSup c hcd).domain → ℝ)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ (LinearPMap.sSup c hcd).domain) x hx)

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

Premises used: Subtype.mk
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
S : Set (E →ₗ.[ℝ] ℝ) := {p : E →ₗ.[ℝ] ℝ | ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : c.Nonempty
hcd : DirectedOn (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c
x : E
hx : x ∈ (LinearPMap.sSup c hcd).domain
hxs : (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ (LinearPMap.sSup c hcd).domain) x hx) : E) ∈ s
hdir : DirectedOn (fun (x1 x2 : Submodule ℝ E) ↦ x1 ≤ x2) (LinearPMap.domain '' c)
f : E →ₗ.[ℝ] ℝ
hfc : f ∈ c
hfx : x ∈ f.domain
this : f ≤ LinearPMap.sSup c hcd
⊢ (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx) =
    (↑(LinearPMap.sSup c hcd) : ↥(LinearPMap.sSup c hcd).domain → ℝ)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ (LinearPMap.sSup c hcd).domain) x hx)

Tactic:
this.2 rfl

Premises used: And.right, rfl
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
S : Set (E →ₗ.[ℝ] ℝ) := {p : E →ₗ.[ℝ] ℝ | ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : c.Nonempty
hcd : DirectedOn (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c
x : E
hx : x ∈ (LinearPMap.sSup c hcd).domain
hxs : (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ (LinearPMap.sSup c hcd).domain) x hx) : E) ∈ s
hdir : DirectedOn (fun (x1 x2 : Submodule ℝ E) ↦ x1 ≤ x2) (LinearPMap.domain '' c)
f : E →ₗ.[ℝ] ℝ
hfc : f ∈ c
hfx : x ∈ f.domain
this : f ≤ LinearPMap.sSup c hcd
⊢ (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx) =
    (↑(LinearPMap.sSup c hcd) : ↥(LinearPMap.sSup c hcd).domain → ℝ)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ (LinearPMap.sSup c hcd).domain) x hx)

Tactic:
exact this.2 rfl

Premises used: And.right
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x
hp_dense : ∀ (y : E), ∃ (x : ↥p.domain), (↑x : E) + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p : E →ₗ.[ℝ] ℝ | ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x}
⊢ ∀ c ⊆ S, IsChain (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub

Tactic:
have hSc : ∀ c, c ⊆ S → IsChain (· ≤ ·) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub := by
    intro c hcs c_chain y hy
    clear hp_nonneg hp_dense p
    have cne : c.Nonempty := ⟨y, hy⟩
    have hcd : DirectedOn (· ≤ ·) c := c_chain.directedOn
    refine ⟨LinearPMap.sSup c hcd, ?_, fun _ ↦ LinearPMap.le_sSup hcd⟩
    rintro ⟨x, hx⟩ hxs
    have hdir : DirectedOn (· ≤ ·) (LinearPMap.domain '' c) :=
      directedOn_image.2 (hcd.mono LinearPMap.domain_mono.monotone)
    rcases (mem_sSup_of_directed (cne.image _) hdir).1 hx with ⟨_, ⟨f, hfc, rfl⟩, hfx⟩
    have : f ≤ LinearPMap.sSup c hcd := LinearPMap.le_sSup _ hfc
    convert! ← hcs hfc ⟨x, hfx⟩ hxs using 1
    exact this.2 rfl
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x
hp_dense : ∀ (y : E), ∃ (x : ↥p.domain), (↑x : E) + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p : E →ₗ.[ℝ] ℝ | ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x}
hSc : ∀ c ⊆ S, IsChain (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
obtain :
  ∀ (q : E →ₗ.[ℝ] ℝ) (hpq : p ≤ q) (hqs : q ∈ S)
    (hq : ∀ ⦃y : E →ₗ.[ℝ] ℝ⦄, (fun (x : E →ₗ.[ℝ] ℝ) ↦ x ∈ S) y → q ≤ y → y ≤ q),
    ∃ q ≥ p, q.domain = ⊤ ∧ ∀ (x : ↥q.domain), (↑x : E) ∈ s → 0 ≤ (↑q : ↥q.domain → ℝ) x
⊢ ∃ q ≥ p, q.domain = ⊤ ∧ ∀ (x : ↥q.domain), (↑x : E) ∈ s → 0 ≤ (↑q : ↥q.domain → ℝ) x

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

Premises used: zorn_le_nonempty₀
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x
hp_dense : ∀ (y : E), ∃ (x : ↥p.domain), (↑x : E) + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p : E →ₗ.[ℝ] ℝ | ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x}
hSc : ∀ c ⊆ S, IsChain (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
q : E →ₗ.[ℝ] ℝ
hpq : p ≤ q
hqs : q ∈ S
hq : ∀ ⦃y : E →ₗ.[ℝ] ℝ⦄, (fun (x : E →ₗ.[ℝ] ℝ) ↦ x ∈ S) y → q ≤ y → y ≤ q
⊢ ∃ q ≥ p, q.domain = ⊤ ∧ ∀ (x : ↥q.domain), (↑x : E) ∈ s → 0 ≤ (↑q : ↥q.domain → ℝ) x

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

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x
hp_dense : ∀ (y : E), ∃ (x : ↥p.domain), (↑x : E) + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p : E →ₗ.[ℝ] ℝ | ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x}
hSc : ∀ c ⊆ S, IsChain (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
q : E →ₗ.[ℝ] ℝ
hpq : p ≤ q
hqs : q ∈ S
hq : ∀ ⦃y : E →ₗ.[ℝ] ℝ⦄, (fun (x : E →ₗ.[ℝ] ℝ) ↦ x ∈ S) y → q ≤ y → y ≤ q
refine : q.domain = ⊤
⊢ ∃ q ≥ p, q.domain = ⊤ ∧ ∀ (x : ↥q.domain), (↑x : E) ∈ s → 0 ≤ (↑q : ↥q.domain → ℝ) x

Tactic:
refine ⟨q, hpq, ?_, hqs⟩
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x
hp_dense : ∀ (y : E), ∃ (x : ↥p.domain), (↑x : E) + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p : E →ₗ.[ℝ] ℝ | ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x}
hSc : ∀ c ⊆ S, IsChain (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
q : E →ₗ.[ℝ] ℝ
hpq : p ≤ q
hqs : q ∈ S
hq : ∀ ⦃y : E →ₗ.[ℝ] ℝ⦄, (fun (x : E →ₗ.[ℝ] ℝ) ↦ x ∈ S) y → q ≤ y → y ≤ q
contrapose! : ∀ (hq : q.domain ≠ ⊤), ∃ y ∈ S, q ≤ y ∧ ¬y ≤ q
⊢ q.domain = ⊤

Tactic:
contrapose! hq
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x
hp_dense : ∀ (y : E), ∃ (x : ↥p.domain), (↑x : E) + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p : E →ₗ.[ℝ] ℝ | ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x}
hSc : ∀ c ⊆ S, IsChain (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
q : E →ₗ.[ℝ] ℝ
hpq : p ≤ q
hqs : q ∈ S
hq : q.domain ≠ ⊤
⊢ ∀ (y : E), ∃ (x : ↥q.domain), (↑x : E) + y ∈ s

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⟩
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x
hp_dense : ∀ (y : E), ∃ (x : ↥p.domain), (↑x : E) + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p : E →ₗ.[ℝ] ℝ | ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x}
hSc : ∀ c ⊆ S, IsChain (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ 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 : ↥q.domain), (↑x : E) + y ∈ s
rcases :
  ∀ (r : E →ₗ.[ℝ] ℝ) (hqr : q < r) (hr : ∀ (x : ↥r.domain), (↑x : E) ∈ s → 0 ≤ (↑r : ↥r.domain → ℝ) x),
    ∃ y ∈ S, q ≤ y ∧ ¬y ≤ q
⊢ ∃ y ∈ S, q ≤ y ∧ ¬y ≤ q

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

Premises used: RieszExtension.step
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x
hp_dense : ∀ (y : E), ∃ (x : ↥p.domain), (↑x : E) + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p : E →ₗ.[ℝ] ℝ | ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x}
hSc : ∀ c ⊆ S, IsChain (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ 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 : ↥q.domain), (↑x : E) + y ∈ s
r : E →ₗ.[ℝ] ℝ
hqr : q < r
hr : ∀ (x : ↥r.domain), (↑x : E) ∈ s → 0 ≤ (↑r : ↥r.domain → ℝ) x
⊢ ∃ y ∈ S, q ≤ y ∧ ¬y ≤ q

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

Premises used: LE.le.antisymm, LT.lt.le, LT.lt.ne', And.intro, Exists.intro
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x
hp_dense : ∀ (y : E), ∃ (x : ↥p.domain), (↑x : E) + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p : E →ₗ.[ℝ] ℝ | ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x}
hSc : ∀ c ⊆ S, IsChain (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ 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 : ↥q.domain), (↑x : E) + y ∈ s
r : E →ₗ.[ℝ] ℝ
hqr : q < r
hr : ∀ (x : ↥r.domain), (↑x : E) ∈ s → 0 ≤ (↑r : ↥r.domain → ℝ) x
⊢ ∃ y ∈ S, q ≤ y ∧ ¬y ≤ q

Tactic:
exact ⟨r, hr, hqr.le, fun hrq ↦ hqr.ne' <| hrq.antisymm hqr.le⟩
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
rcases :
  ∀ (g : ↥⊤ →ₗ[ℝ] ℝ)
    (hfg :
      ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ }.domain⦄ (_h : (↑x : E) = (↑y : E)),
        (↑f : ↥f.domain → ℝ) x =
          (↑{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ } : ↥{ domain := ⊤, toFun := g }.domain → ℝ) y)
    (hgs :
      ∀ (x : ↥{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ }.domain),
        (↑x : E) ∈ s → 0 ≤ (↑{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ } : ↥{ domain := ⊤, toFun := g }.domain → ℝ) x),
    ∃ (g : E →ₗ[ℝ] ℝ),
      (∀ (x : ↥f.domain), (g : (a : E) → ℝ) (↑x : E) = (↑f : ↥f.domain → ℝ) x) ∧
        ∀ x ∈ s, LE.le (α := ℝ) (0 : ℝ) ((g : (a : E) → ℝ) x : ℝ)
⊢ ∃ (g : E →ₗ[ℝ] ℝ),
    (∀ (x : ↥f.domain), (g : (a : E) → ℝ) (↑x : E) = (↑f : ↥f.domain → ℝ) x) ∧
      ∀ x ∈ s, LE.le (α := ℝ) (0 : ℝ) ((g : (a : E) → ℝ) x : ℝ)

Tactic:
rcases RieszExtension.exists_top s f nonneg dense
    with ⟨⟨g_dom, g⟩, ⟨-, hfg⟩, rfl : g_dom = ⊤, hgs⟩

Premises used: RieszExtension.exists_top, rfl
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
g : ↥⊤ →ₗ[ℝ] ℝ
hfg :
  ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ }.domain⦄ (_h : (↑x : E) = (↑y : E)),
    (↑f : ↥f.domain → ℝ) x = (↑{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ } : ↥{ domain := ⊤, toFun := g }.domain → ℝ) y
hgs :
  ∀ (x : ↥{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ }.domain),
    (↑x : E) ∈ s → 0 ≤ (↑{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ } : ↥{ domain := ⊤, toFun := g }.domain → ℝ) x
⊢ ∃ (g : E →ₗ[ℝ] ℝ),
    (∀ (x : ↥f.domain), (g : (a : E) → ℝ) (↑x : E) = (↑f : ↥f.domain → ℝ) x) ∧
      ∀ x ∈ s, LE.le (α := ℝ) (0 : ℝ) ((g : (a : E) → ℝ) x : ℝ)

Tactic:
⟨g.comp (LinearMap.id.codRestrict ⊤ fun _ ↦ trivial), ?_, ?_⟩

Premises used: LinearMap.id, trivial, LinearMap.comp, And.intro, Exists.intro, LinearMap.codRestrict, Top.top
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
g : ↥⊤ →ₗ[ℝ] ℝ
hfg :
  ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ }.domain⦄ (_h : (↑x : E) = (↑y : E)),
    (↑f : ↥f.domain → ℝ) x = (↑{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ } : ↥{ domain := ⊤, toFun := g }.domain → ℝ) y
hgs :
  ∀ (x : ↥{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ }.domain),
    (↑x : E) ∈ s → 0 ≤ (↑{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ } : ↥{ domain := ⊤, toFun := g }.domain → ℝ) x
refine_1 :
  ∀ (x : ↥f.domain), (g ∘ₗ LinearMap.codRestrict ⊤ LinearMap.id ⋯ : (a : E) → ℝ) (↑x : E) = (↑f : ↥f.domain → ℝ) x
refine_2 : ∀ x ∈ s, LE.le (α := ℝ) (0 : ℝ) ((g ∘ₗ LinearMap.codRestrict ⊤ LinearMap.id ⋯ : (a : E) → ℝ) x : ℝ)
⊢ ∃ (g : E →ₗ[ℝ] ℝ),
    (∀ (x : ↥f.domain), (g : (a : E) → ℝ) (↑x : E) = (↑f : ↥f.domain → ℝ) x) ∧
      ∀ x ∈ s, LE.le (α := ℝ) (0 : ℝ) ((g : (a : E) → ℝ) x : ℝ)

Tactic:
refine ⟨g.comp (LinearMap.id.codRestrict ⊤ fun _ ↦ trivial), ?_, ?_⟩
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
g : ↥⊤ →ₗ[ℝ] ℝ
hfg :
  ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ }.domain⦄ (_h : (↑x : E) = (↑y : E)),
    (↑f : ↥f.domain → ℝ) x = (↑{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ } : ↥{ domain := ⊤, toFun := g }.domain → ℝ) y
hgs :
  ∀ (x : ↥{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ }.domain),
    (↑x : E) ∈ s → 0 ≤ (↑{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ } : ↥{ domain := ⊤, toFun := g }.domain → ℝ) x
⊢ ∀ (x : ↥f.domain), (g ∘ₗ LinearMap.codRestrict ⊤ LinearMap.id ⋯ : (a : E) → ℝ) (↑x : E) = (↑f : ↥f.domain → ℝ) x

Tactic:
fun x => (hfg rfl).symm

Premises used: Eq.symm, LinearPMap.toFun'
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
g : ↥⊤ →ₗ[ℝ] ℝ
hfg :
  ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ }.domain⦄ (_h : (↑x : E) = (↑y : E)),
    (↑f : ↥f.domain → ℝ) x = (↑{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ } : ↥{ domain := ⊤, toFun := g }.domain → ℝ) y
hgs :
  ∀ (x : ↥{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ }.domain),
    (↑x : E) ∈ s → 0 ≤ (↑{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ } : ↥{ domain := ⊤, toFun := g }.domain → ℝ) x
⊢ ∀ (x : ↥f.domain), (g ∘ₗ LinearMap.codRestrict ⊤ LinearMap.id ⋯ : (a : E) → ℝ) (↑x : E) = (↑f : ↥f.domain → ℝ) x

Tactic:
exact fun x => (hfg rfl).symm

Premises used: Eq.symm
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
g : ↥⊤ →ₗ[ℝ] ℝ
hfg :
  ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ }.domain⦄ (_h : (↑x : E) = (↑y : E)),
    (↑f : ↥f.domain → ℝ) x = (↑{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ } : ↥{ domain := ⊤, toFun := g }.domain → ℝ) y
hgs :
  ∀ (x : ↥{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ }.domain),
    (↑x : E) ∈ s → 0 ≤ (↑{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ } : ↥{ domain := ⊤, toFun := g }.domain → ℝ) x
⊢ ∀ x ∈ s, LE.le (α := ℝ) (0 : ℝ) ((g ∘ₗ LinearMap.codRestrict ⊤ LinearMap.id ⋯ : (a : E) → ℝ) x : ℝ)

Tactic:
fun x hx => hgs ⟨x, _⟩ hx

Premises used: trivial, Set.Mem, Subtype.mk, LinearPMap.toFun'
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
g : ↥⊤ →ₗ[ℝ] ℝ
hfg :
  ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ }.domain⦄ (_h : (↑x : E) = (↑y : E)),
    (↑f : ↥f.domain → ℝ) x = (↑{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ } : ↥{ domain := ⊤, toFun := g }.domain → ℝ) y
hgs :
  ∀ (x : ↥{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ }.domain),
    (↑x : E) ∈ s → 0 ≤ (↑{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ } : ↥{ domain := ⊤, toFun := g }.domain → ℝ) x
⊢ ∀ x ∈ s, LE.le (α := ℝ) (0 : ℝ) ((g ∘ₗ LinearMap.codRestrict ⊤ LinearMap.id ⋯ : (a : E) → ℝ) x : ℝ)

Tactic:
exact fun x hx => hgs ⟨x, _⟩ hx

Premises used: Subtype.mk
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), (↑f : ↥f.domain → ℝ) x ≤ N (↑x : E)
c : ℝ
hc : 0 < c
p : E × ℝ
hp : Membership.mem (γ := Set (E × ℝ)) {p : E × ℝ | N p.1 ≤ p.2} p
hbc : N p.1 ≤ p.2
⊢ c * N p.1 ≤ c * p.2

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), (↑f : ↥f.domain → ℝ) x ≤ N (↑x : E)
c : ℝ
hc : 0 < c
p : E × ℝ
hp : Membership.mem (γ := Set (E × ℝ)) {p : E × ℝ | N p.1 ≤ p.2} p
⊢ N p.1 ≤ p.2

Tactic:
hp

Premises used: Set.Mem
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), (↑f : ↥f.domain → ℝ) x ≤ N (↑x : E)
c : ℝ
hc : 0 < c
p : E × ℝ
hp : Membership.mem (γ := Set (E × ℝ)) {p : E × ℝ | N p.1 ≤ p.2} p
⊢ N p.1 ≤ p.2

Tactic:
exact hp
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), (↑f : ↥f.domain → ℝ) x ≤ N (↑x : E)
s : ConvexCone ℝ (E × ℝ) := { carrier := {p : E × ℝ | N p.1 ≤ p.2}, smul_mem' := ⋯, add_mem' := ⋯ }
f' : E × ℝ →ₗ.[ℝ] ℝ := (-f).coprod (toPMap LinearMap.id ⊤)
x : ↥f'.domain
hx : N (↑x : E × ℝ).1 ≤ (↑x : E × ℝ).2
⊢ 0 ≤ (↑f' : ↥f'.domain → ℝ) x

Tactic:
simpa [f'] using le_trans (hf ⟨x.1.1, x.2.1⟩) hx

Premises used: Prod.fst, Subtype.mk, And.left, Subtype.val, Subtype.property, le_trans
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), (↑f : ↥f.domain → ℝ) x ≤ N (↑x : E)
s : ConvexCone ℝ (E × ℝ) := { carrier := {p : E × ℝ | N p.1 ≤ p.2}, smul_mem' := ⋯, add_mem' := ⋯ }
f' : E × ℝ →ₗ.[ℝ] ℝ := (-f).coprod (toPMap LinearMap.id ⊤)
⊢ ∀ (x : ↥f'.domain), (↑x : E × ℝ) ∈ s → 0 ≤ (↑f' : ↥f'.domain → ℝ) x

Tactic:
have hf'_nonneg : ∀ x : f'.domain, x.1 ∈ s → 0 ≤ f' x := fun x (hx : N x.1.1 ≤ x.1.2) ↦ by
    simpa [f'] using le_trans (hf ⟨x.1.1, x.2.1⟩) hx
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), (↑f : ↥f.domain → ℝ) x ≤ N (↑x : E)
s : ConvexCone ℝ (E × ℝ) := { carrier := {p : E × ℝ | N p.1 ≤ p.2}, smul_mem' := ⋯, add_mem' := ⋯ }
f' : E × ℝ →ₗ.[ℝ] ℝ := (-f).coprod (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : ↥f'.domain), (↑x : E × ℝ) ∈ s → 0 ≤ (↑f' : ↥f'.domain → ℝ) x
x : E
y : ℝ
⊢ ∃ (x_1 : ↥f'.domain), (↑x_1 : E × ℝ) + (x, y) ∈ s

Tactic:
⟨⟨(0, N x - y), ⟨f.domain.zero_mem, trivial⟩⟩, ?_⟩

Premises used: trivial, HSub.hSub, Prod.mk, Subtype.mk, Submodule.zero_mem, And.intro, Exists.intro, OfNat.ofNat, LinearPMap.domain