case intro.mk.intro.intro.intro
𝕜 : Type ?u.280700
E : Type u_1
F : Type ?u.280706
G : Type ?u.280709
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : { x // x ∈ f.domain }), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
g : { x // x ∈ ⊤ } →ₗ[ℝ] ℝ
hfg :
  ∀ ⦃x : { x // x ∈ f.domain }⦄ ⦃y : { x // x ∈ { domain := ⊤, toFun := g }.domain }⦄,
    ↑x = ↑y → ↑f x = ↑{ domain := ⊤, toFun := g } y
hgs : ∀ (x : { x // x ∈ { domain := ⊤, toFun := g }.domain }), ↑x ∈ s → 0 ≤ ↑{ domain := ⊤, toFun := g } x
⊢ ∃ g, (∀ (x : { x // x ∈ f.domain }), ↑g ↑x = ↑f x) ∧ ∀ (x : E), x ∈ s → 0 ≤ ↑g x
𝕜 : Type ?u.280700
E : Type u_1
F : Type ?u.280706
G : Type ?u.280709
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : { x // x ∈ f.domain }), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
⊢ ∃ g, (∀ (x : { x // x ∈ f.domain }), ↑g ↑x = ↑f x) ∧ ∀ (x : E), x ∈ s → 0 ≤ ↑g x
rcases RieszExtension.exists_top s f nonneg dense
  with ⟨⟨g_dom, g⟩, ⟨-, hfg⟩, rfl : g_dom = ⊤, hgs⟩
case intro.mk.intro.intro.intro.refine'_1
𝕜 : Type ?u.280700
E : Type u_1
F : Type ?u.280706
G : Type ?u.280709
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : { x // x ∈ f.domain }), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
g : { x // x ∈ ⊤ } →ₗ[ℝ] ℝ
hfg :
  ∀ ⦃x : { x // x ∈ f.domain }⦄ ⦃y : { x // x ∈ { domain := ⊤, toFun := g }.domain }⦄,
    ↑x = ↑y → ↑f x = ↑{ domain := ⊤, toFun := g } y
hgs : ∀ (x : { x // x ∈ { domain := ⊤, toFun := g }.domain }), ↑x ∈ s → 0 ≤ ↑{ domain := ⊤, toFun := g } x
⊢ ∀ (x : { x // x ∈ f.domain }), ↑(comp g (LinearMap.codRestrict ⊤ LinearMap.id (_ : E → True))) ↑x = ↑f x

case intro.mk.intro.intro.intro.refine'_2
𝕜 : Type ?u.280700
E : Type u_1
F : Type ?u.280706
G : Type ?u.280709
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : { x // x ∈ f.domain }), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
g : { x // x ∈ ⊤ } →ₗ[ℝ] ℝ
hfg :
  ∀ ⦃x : { x // x ∈ f.domain }⦄ ⦃y : { x // x ∈ { domain := ⊤, toFun := g }.domain }⦄,
    ↑x = ↑y → ↑f x = ↑{ domain := ⊤, toFun := g } y
hgs : ∀ (x : { x // x ∈ { domain := ⊤, toFun := g }.domain }), ↑x ∈ s → 0 ≤ ↑{ domain := ⊤, toFun := g } x
⊢ ∀ (x : E), x ∈ s → 0 ≤ ↑(comp g (LinearMap.codRestrict ⊤ LinearMap.id (_ : E → True))) x
case intro.mk.intro.intro.intro
𝕜 : Type ?u.280700
E : Type u_1
F : Type ?u.280706
G : Type ?u.280709
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : { x // x ∈ f.domain }), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
g : { x // x ∈ ⊤ } →ₗ[ℝ] ℝ
hfg :
  ∀ ⦃x : { x // x ∈ f.domain }⦄ ⦃y : { x // x ∈ { domain := ⊤, toFun := g }.domain }⦄,
    ↑x = ↑y → ↑f x = ↑{ domain := ⊤, toFun := g } y
hgs : ∀ (x : { x // x ∈ { domain := ⊤, toFun := g }.domain }), ↑x ∈ s → 0 ≤ ↑{ domain := ⊤, toFun := g } x
⊢ ∃ g, (∀ (x : { x // x ∈ f.domain }), ↑g ↑x = ↑f x) ∧ ∀ (x : E), x ∈ s → 0 ≤ ↑g x
refine' ⟨g.comp (LinearMap.id.codRestrict ⊤ fun _ ↦ trivial), _, _⟩
no goals
case intro.mk.intro.intro.intro.refine'_1
𝕜 : Type ?u.280700
E : Type u_1
F : Type ?u.280706
G : Type ?u.280709
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : { x // x ∈ f.domain }), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
g : { x // x ∈ ⊤ } →ₗ[ℝ] ℝ
hfg :
  ∀ ⦃x : { x // x ∈ f.domain }⦄ ⦃y : { x // x ∈ { domain := ⊤, toFun := g }.domain }⦄,
    ↑x = ↑y → ↑f x = ↑{ domain := ⊤, toFun := g } y
hgs : ∀ (x : { x // x ∈ { domain := ⊤, toFun := g }.domain }), ↑x ∈ s → 0 ≤ ↑{ domain := ⊤, toFun := g } x
⊢ ∀ (x : { x // x ∈ f.domain }), ↑(comp g (LinearMap.codRestrict ⊤ LinearMap.id (_ : E → True))) ↑x = ↑f x
exact fun x => (hfg rfl).symm
no goals
case intro.mk.intro.intro.intro.refine'_2
𝕜 : Type ?u.280700
E : Type u_1
F : Type ?u.280706
G : Type ?u.280709
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : { x // x ∈ f.domain }), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
g : { x // x ∈ ⊤ } →ₗ[ℝ] ℝ
hfg :
  ∀ ⦃x : { x // x ∈ f.domain }⦄ ⦃y : { x // x ∈ { domain := ⊤, toFun := g }.domain }⦄,
    ↑x = ↑y → ↑f x = ↑{ domain := ⊤, toFun := g } y
hgs : ∀ (x : { x // x ∈ { domain := ⊤, toFun := g }.domain }), ↑x ∈ s → 0 ≤ ↑{ domain := ⊤, toFun := g } x
⊢ ∀ (x : E), x ∈ s → 0 ≤ ↑(comp g (LinearMap.codRestrict ⊤ LinearMap.id (_ : E → True))) x
exact fun x hx => hgs ⟨x, _⟩ hx