𝕜 : Type ?u.285824
E : Type u_1
F : Type ?u.285830
G : Type ?u.285833
inst✝¹ : AddCommGroup E
inst✝ : 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 : { x // x ∈ f.domain }), ↑f x ≤ N ↑x
s : ConvexCone ℝ (E × ℝ) :=
  { carrier := {p | N p.fst ≤ p.snd},
    smul_mem' := (_ : ∀ (c : ℝ), 0 < c → ∀ (p : E × ℝ), p ∈ {p | N p.fst ≤ p.snd} → N (c • p.fst) ≤ c * p.snd),
    add_mem' :=
      (_ :
        ∀ (x : E × ℝ),
          x ∈ {p | N p.fst ≤ p.snd} → ∀ (y : E × ℝ), y ∈ {p | N p.fst ≤ p.snd} → N (x.fst + y.fst) ≤ (x + y).snd) }
⊢ ∃ g, (∀ (x : { x // x ∈ f.domain }), ↑g ↑x = ↑f x) ∧ ∀ (x : E), ↑g x ≤ N x
𝕜 : Type ?u.285824
E : Type u_1
F : Type ?u.285830
G : Type ?u.285833
inst✝¹ : AddCommGroup E
inst✝ : 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 : { x // x ∈ f.domain }), ↑f x ≤ N ↑x
⊢ ∃ g, (∀ (x : { x // x ∈ f.domain }), ↑g ↑x = ↑f x) ∧ ∀ (x : E), ↑g x ≤ N x
let s : ConvexCone ℝ (E × ℝ) :=
  { carrier := { p : E × ℝ | N p.1 ≤ p.2 }
    smul_mem' := fun c hc p hp =>
      calc
        N (c • p.1) = c * N p.1 := N_hom c hc p.1
        _ ≤ c * p.2 := mul_le_mul_of_nonneg_left hp hc.le
    add_mem' := fun x hx y hy => (N_add _ _).trans (add_le_add hx hy) }
𝕜 : Type ?u.285824
E : Type u_1
F : Type ?u.285830
G : Type ?u.285833
inst✝¹ : AddCommGroup E
inst✝ : 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 : { x // x ∈ f.domain }), ↑f x ≤ N ↑x
s : ConvexCone ℝ (E × ℝ) :=
  { carrier := {p | N p.fst ≤ p.snd},
    smul_mem' := (_ : ∀ (c : ℝ), 0 < c → ∀ (p : E × ℝ), p ∈ {p | N p.fst ≤ p.snd} → N (c • p.fst) ≤ c * p.snd),
    add_mem' :=
      (_ :
        ∀ (x : E × ℝ),
          x ∈ {p | N p.fst ≤ p.snd} → ∀ (y : E × ℝ), y ∈ {p | N p.fst ≤ p.snd} → N (x.fst + y.fst) ≤ (x + y).snd) }
f' : E × ℝ →ₗ.[ℝ] ℝ := LinearPMap.coprod (-f) (toPMap LinearMap.id ⊤)
⊢ ∃ g, (∀ (x : { x // x ∈ f.domain }), ↑g ↑x = ↑f x) ∧ ∀ (x : E), ↑g x ≤ N x
𝕜 : Type ?u.285824
E : Type u_1
F : Type ?u.285830
G : Type ?u.285833
inst✝¹ : AddCommGroup E
inst✝ : 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 : { x // x ∈ f.domain }), ↑f x ≤ N ↑x
s : ConvexCone ℝ (E × ℝ) :=
  { carrier := {p | N p.fst ≤ p.snd},
    smul_mem' := (_ : ∀ (c : ℝ), 0 < c → ∀ (p : E × ℝ), p ∈ {p | N p.fst ≤ p.snd} → N (c • p.fst) ≤ c * p.snd),
    add_mem' :=
      (_ :
        ∀ (x : E × ℝ),
          x ∈ {p | N p.fst ≤ p.snd} → ∀ (y : E × ℝ), y ∈ {p | N p.fst ≤ p.snd} → N (x.fst + y.fst) ≤ (x + y).snd) }
⊢ ∃ g, (∀ (x : { x // x ∈ f.domain }), ↑g ↑x = ↑f x) ∧ ∀ (x : E), ↑g x ≤ N x
set f' := (-f).coprod (LinearMap.id.toPMap ⊤)
𝕜 : Type ?u.285824
E : Type u_1
F : Type ?u.285830
G : Type ?u.285833
inst✝¹ : AddCommGroup E
inst✝ : 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 : { x // x ∈ f.domain }), ↑f x ≤ N ↑x
s : ConvexCone ℝ (E × ℝ) :=
  { carrier := {p | N p.fst ≤ p.snd},
    smul_mem' := (_ : ∀ (c : ℝ), 0 < c → ∀ (p : E × ℝ), p ∈ {p | N p.fst ≤ p.snd} → N (c • p.fst) ≤ c * p.snd),
    add_mem' :=
      (_ :
        ∀ (x : E × ℝ),
          x ∈ {p | N p.fst ≤ p.snd} → ∀ (y : E × ℝ), y ∈ {p | N p.fst ≤ p.snd} → N (x.fst + y.fst) ≤ (x + y).snd) }
f' : E × ℝ →ₗ.[ℝ] ℝ := LinearPMap.coprod (-f) (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : { x // x ∈ f'.domain }), ↑x ∈ s → 0 ≤ ↑f' x
⊢ ∃ g, (∀ (x : { x // x ∈ f.domain }), ↑g ↑x = ↑f x) ∧ ∀ (x : E), ↑g x ≤ N x
𝕜 : Type ?u.285824
E : Type u_1
F : Type ?u.285830
G : Type ?u.285833
inst✝¹ : AddCommGroup E
inst✝ : 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 : { x // x ∈ f.domain }), ↑f x ≤ N ↑x
s : ConvexCone ℝ (E × ℝ) :=
  { carrier := {p | N p.fst ≤ p.snd},
    smul_mem' := (_ : ∀ (c : ℝ), 0 < c → ∀ (p : E × ℝ), p ∈ {p | N p.fst ≤ p.snd} → N (c • p.fst) ≤ c * p.snd),
    add_mem' :=
      (_ :
        ∀ (x : E × ℝ),
          x ∈ {p | N p.fst ≤ p.snd} → ∀ (y : E × ℝ), y ∈ {p | N p.fst ≤ p.snd} → N (x.fst + y.fst) ≤ (x + y).snd) }
f' : E × ℝ →ₗ.[ℝ] ℝ := LinearPMap.coprod (-f) (toPMap LinearMap.id ⊤)
⊢ ∃ g, (∀ (x : { x // x ∈ f.domain }), ↑g ↑x = ↑f x) ∧ ∀ (x : E), ↑g x ≤ N x
have hf'_nonneg : ∀ x : f'.domain, x.1 ∈ s → 0 ≤ f' x := fun x (hx : N x.1.1 ≤ x.1.2) ↦ by
  simpa using le_trans (hf ⟨x.1.1, x.2.1⟩) hx
case hf'_dense
𝕜 : Type ?u.285824
E : Type u_1
F : Type ?u.285830
G : Type ?u.285833
inst✝¹ : AddCommGroup E
inst✝ : 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 : { x // x ∈ f.domain }), ↑f x ≤ N ↑x
s : ConvexCone ℝ (E × ℝ) :=
  { carrier := {p | N p.fst ≤ p.snd},
    smul_mem' := (_ : ∀ (c : ℝ), 0 < c → ∀ (p : E × ℝ), p ∈ {p | N p.fst ≤ p.snd} → N (c • p.fst) ≤ c * p.snd),
    add_mem' :=
      (_ :
        ∀ (x : E × ℝ),
          x ∈ {p | N p.fst ≤ p.snd} → ∀ (y : E × ℝ), y ∈ {p | N p.fst ≤ p.snd} → N (x.fst + y.fst) ≤ (x + y).snd) }
f' : E × ℝ →ₗ.[ℝ] ℝ := LinearPMap.coprod (-f) (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : { x // x ∈ f'.domain }), ↑x ∈ s → 0 ≤ ↑f' x
⊢ ∀ (y : E × ℝ), ∃ x, ↑x + y ∈ s

𝕜 : Type ?u.285824
E : Type u_1
F : Type ?u.285830
G : Type ?u.285833
inst✝¹ : AddCommGroup E
inst✝ : 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 : { x // x ∈ f.domain }), ↑f x ≤ N ↑x
s : ConvexCone ℝ (E × ℝ) :=
  { carrier := {p | N p.fst ≤ p.snd},
    smul_mem' := (_ : ∀ (c : ℝ), 0 < c → ∀ (p : E × ℝ), p ∈ {p | N p.fst ≤ p.snd} → N (c • p.fst) ≤ c * p.snd),
    add_mem' :=
      (_ :
        ∀ (x : E × ℝ),
          x ∈ {p | N p.fst ≤ p.snd} → ∀ (y : E × ℝ), y ∈ {p | N p.fst ≤ p.snd} → N (x.fst + y.fst) ≤ (x + y).snd) }
f' : E × ℝ →ₗ.[ℝ] ℝ := LinearPMap.coprod (-f) (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : { x // x ∈ f'.domain }), ↑x ∈ s → 0 ≤ ↑f' x
hf'_dense : ∀ (y : E × ℝ), ∃ x, ↑x + y ∈ s
⊢ ∃ g, (∀ (x : { x // x ∈ f.domain }), ↑g ↑x = ↑f x) ∧ ∀ (x : E), ↑g x ≤ N x
𝕜 : Type ?u.285824
E : Type u_1
F : Type ?u.285830
G : Type ?u.285833
inst✝¹ : AddCommGroup E
inst✝ : 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 : { x // x ∈ f.domain }), ↑f x ≤ N ↑x
s : ConvexCone ℝ (E × ℝ) :=
  { carrier := {p | N p.fst ≤ p.snd},
    smul_mem' := (_ : ∀ (c : ℝ), 0 < c → ∀ (p : E × ℝ), p ∈ {p | N p.fst ≤ p.snd} → N (c • p.fst) ≤ c * p.snd),
    add_mem' :=
      (_ :
        ∀ (x : E × ℝ),
          x ∈ {p | N p.fst ≤ p.snd} → ∀ (y : E × ℝ), y ∈ {p | N p.fst ≤ p.snd} → N (x.fst + y.fst) ≤ (x + y).snd) }
f' : E × ℝ →ₗ.[ℝ] ℝ := LinearPMap.coprod (-f) (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : { x // x ∈ f'.domain }), ↑x ∈ s → 0 ≤ ↑f' x
⊢ ∃ g, (∀ (x : { x // x ∈ f.domain }), ↑g ↑x = ↑f x) ∧ ∀ (x : E), ↑g x ≤ N x
have hf'_dense : ∀ y : E × ℝ, ∃ x : f'.domain, ↑x + y ∈ s
case intro.intro
𝕜 : Type ?u.285824
E : Type u_1
F : Type ?u.285830
G : Type ?u.285833
inst✝¹ : AddCommGroup E
inst✝ : 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 : { x // x ∈ f.domain }), ↑f x ≤ N ↑x
s : ConvexCone ℝ (E × ℝ) :=
  { carrier := {p | N p.fst ≤ p.snd},
    smul_mem' := (_ : ∀ (c : ℝ), 0 < c → ∀ (p : E × ℝ), p ∈ {p | N p.fst ≤ p.snd} → N (c • p.fst) ≤ c * p.snd),
    add_mem' :=
      (_ :
        ∀ (x : E × ℝ),
          x ∈ {p | N p.fst ≤ p.snd} → ∀ (y : E × ℝ), y ∈ {p | N p.fst ≤ p.snd} → N (x.fst + y.fst) ≤ (x + y).snd) }
f' : E × ℝ →ₗ.[ℝ] ℝ := LinearPMap.coprod (-f) (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : { x // x ∈ f'.domain }), ↑x ∈ s → 0 ≤ ↑f' x
hf'_dense : ∀ (y : E × ℝ), ∃ x, ↑x + y ∈ s
g : E × ℝ →ₗ[ℝ] ℝ
g_eq : ∀ (x : { x // x ∈ f'.domain }), ↑g ↑x = ↑f' x
g_nonneg : ∀ (x : E × ℝ), x ∈ s → 0 ≤ ↑g x
⊢ ∃ g, (∀ (x : { x // x ∈ f.domain }), ↑g ↑x = ↑f x) ∧ ∀ (x : E), ↑g x ≤ N x
𝕜 : Type ?u.285824
E : Type u_1
F : Type ?u.285830
G : Type ?u.285833
inst✝¹ : AddCommGroup E
inst✝ : 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 : { x // x ∈ f.domain }), ↑f x ≤ N ↑x
s : ConvexCone ℝ (E × ℝ) :=
  { carrier := {p | N p.fst ≤ p.snd},
    smul_mem' := (_ : ∀ (c : ℝ), 0 < c → ∀ (p : E × ℝ), p ∈ {p | N p.fst ≤ p.snd} → N (c • p.fst) ≤ c * p.snd),
    add_mem' :=
      (_ :
        ∀ (x : E × ℝ),
          x ∈ {p | N p.fst ≤ p.snd} → ∀ (y : E × ℝ), y ∈ {p | N p.fst ≤ p.snd} → N (x.fst + y.fst) ≤ (x + y).snd) }
f' : E × ℝ →ₗ.[ℝ] ℝ := LinearPMap.coprod (-f) (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : { x // x ∈ f'.domain }), ↑x ∈ s → 0 ≤ ↑f' x
hf'_dense : ∀ (y : E × ℝ), ∃ x, ↑x + y ∈ s
⊢ ∃ g, (∀ (x : { x // x ∈ f.domain }), ↑g ↑x = ↑f x) ∧ ∀ (x : E), ↑g x ≤ N x
obtain ⟨g, g_eq, g_nonneg⟩ := riesz_extension s f' hf'_nonneg hf'_dense
case intro.intro
𝕜 : Type ?u.285824
E : Type u_1
F : Type ?u.285830
G : Type ?u.285833
inst✝¹ : AddCommGroup E
inst✝ : 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 : { x // x ∈ f.domain }), ↑f x ≤ N ↑x
s : ConvexCone ℝ (E × ℝ) :=
  { carrier := {p | N p.fst ≤ p.snd},
    smul_mem' := (_ : ∀ (c : ℝ), 0 < c → ∀ (p : E × ℝ), p ∈ {p | N p.fst ≤ p.snd} → N (c • p.fst) ≤ c * p.snd),
    add_mem' :=
      (_ :
        ∀ (x : E × ℝ),
          x ∈ {p | N p.fst ≤ p.snd} → ∀ (y : E × ℝ), y ∈ {p | N p.fst ≤ p.snd} → N (x.fst + y.fst) ≤ (x + y).snd) }
f' : E × ℝ →ₗ.[ℝ] ℝ := LinearPMap.coprod (-f) (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : { x // x ∈ f'.domain }), ↑x ∈ s → 0 ≤ ↑f' x
hf'_dense : ∀ (y : E × ℝ), ∃ x, ↑x + y ∈ s
g : E × ℝ →ₗ[ℝ] ℝ
g_nonneg : ∀ (x : E × ℝ), x ∈ s → 0 ≤ ↑g x
g_eq : ∀ (x : { x // x ∈ f.domain }) (y : ℝ), ↑g (↑x, y) = y - ↑f x
⊢ ∃ g, (∀ (x : { x // x ∈ f.domain }), ↑g ↑x = ↑f x) ∧ ∀ (x : E), ↑g x ≤ N x
case intro.intro
𝕜 : Type ?u.285824
E : Type u_1
F : Type ?u.285830
G : Type ?u.285833
inst✝¹ : AddCommGroup E
inst✝ : 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 : { x // x ∈ f.domain }), ↑f x ≤ N ↑x
s : ConvexCone ℝ (E × ℝ) :=
  { carrier := {p | N p.fst ≤ p.snd},
    smul_mem' := (_ : ∀ (c : ℝ), 0 < c → ∀ (p : E × ℝ), p ∈ {p | N p.fst ≤ p.snd} → N (c • p.fst) ≤ c * p.snd),
    add_mem' :=
      (_ :
        ∀ (x : E × ℝ),
          x ∈ {p | N p.fst ≤ p.snd} → ∀ (y : E × ℝ), y ∈ {p | N p.fst ≤ p.snd} → N (x.fst + y.fst) ≤ (x + y).snd) }
f' : E × ℝ →ₗ.[ℝ] ℝ := LinearPMap.coprod (-f) (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : { x // x ∈ f'.domain }), ↑x ∈ s → 0 ≤ ↑f' x
hf'_dense : ∀ (y : E × ℝ), ∃ x, ↑x + y ∈ s
g : E × ℝ →ₗ[ℝ] ℝ
g_eq : ∀ (x : { x // x ∈ f'.domain }), ↑g ↑x = ↑f' x
g_nonneg : ∀ (x : E × ℝ), x ∈ s → 0 ≤ ↑g x
⊢ ∃ g, (∀ (x : { x // x ∈ f.domain }), ↑g ↑x = ↑f x) ∧ ∀ (x : E), ↑g x ≤ N x
replace g_eq : ∀ (x : f.domain) (y : ℝ), g (x, y) = y - f x := fun x y ↦
  (g_eq ⟨(x, y), ⟨x.2, trivial⟩⟩).trans (sub_eq_neg_add _ _).symm
case intro.intro.refine_1
𝕜 : Type ?u.285824
E : Type u_1
F : Type ?u.285830
G : Type ?u.285833
inst✝¹ : AddCommGroup E
inst✝ : 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 : { x // x ∈ f.domain }), ↑f x ≤ N ↑x
s : ConvexCone ℝ (E × ℝ) :=
  { carrier := {p | N p.fst ≤ p.snd},
    smul_mem' := (_ : ∀ (c : ℝ), 0 < c → ∀ (p : E × ℝ), p ∈ {p | N p.fst ≤ p.snd} → N (c • p.fst) ≤ c * p.snd),
    add_mem' :=
      (_ :
        ∀ (x : E × ℝ),
          x ∈ {p | N p.fst ≤ p.snd} → ∀ (y : E × ℝ), y ∈ {p | N p.fst ≤ p.snd} → N (x.fst + y.fst) ≤ (x + y).snd) }
f' : E × ℝ →ₗ.[ℝ] ℝ := LinearPMap.coprod (-f) (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : { x // x ∈ f'.domain }), ↑x ∈ s → 0 ≤ ↑f' x
hf'_dense : ∀ (y : E × ℝ), ∃ x, ↑x + y ∈ s
g : E × ℝ →ₗ[ℝ] ℝ
g_nonneg : ∀ (x : E × ℝ), x ∈ s → 0 ≤ ↑g x
g_eq : ∀ (x : { x // x ∈ f.domain }) (y : ℝ), ↑g (↑x, y) = y - ↑f x
x : { x // x ∈ f.domain }
⊢ ↑(-comp g (inl ℝ E ℝ)) ↑x = ↑f x

case intro.intro.refine_2
𝕜 : Type ?u.285824
E : Type u_1
F : Type ?u.285830
G : Type ?u.285833
inst✝¹ : AddCommGroup E
inst✝ : 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 : { x // x ∈ f.domain }), ↑f x ≤ N ↑x
s : ConvexCone ℝ (E × ℝ) :=
  { carrier := {p | N p.fst ≤ p.snd},
    smul_mem' := (_ : ∀ (c : ℝ), 0 < c → ∀ (p : E × ℝ), p ∈ {p | N p.fst ≤ p.snd} → N (c • p.fst) ≤ c * p.snd),
    add_mem' :=
      (_ :
        ∀ (x : E × ℝ),
          x ∈ {p | N p.fst ≤ p.snd} → ∀ (y : E × ℝ), y ∈ {p | N p.fst ≤ p.snd} → N (x.fst + y.fst) ≤ (x + y).snd) }
f' : E × ℝ →ₗ.[ℝ] ℝ := LinearPMap.coprod (-f) (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : { x // x ∈ f'.domain }), ↑x ∈ s → 0 ≤ ↑f' x
hf'_dense : ∀ (y : E × ℝ), ∃ x, ↑x + y ∈ s
g : E × ℝ →ₗ[ℝ] ℝ
g_nonneg : ∀ (x : E × ℝ), x ∈ s → 0 ≤ ↑g x
g_eq : ∀ (x : { x // x ∈ f.domain }) (y : ℝ), ↑g (↑x, y) = y - ↑f x
x : E
⊢ ↑(-comp g (inl ℝ E ℝ)) x ≤ N x
case intro.intro
𝕜 : Type ?u.285824
E : Type u_1
F : Type ?u.285830
G : Type ?u.285833
inst✝¹ : AddCommGroup E
inst✝ : 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 : { x // x ∈ f.domain }), ↑f x ≤ N ↑x
s : ConvexCone ℝ (E × ℝ) :=
  { carrier := {p | N p.fst ≤ p.snd},
    smul_mem' := (_ : ∀ (c : ℝ), 0 < c → ∀ (p : E × ℝ), p ∈ {p | N p.fst ≤ p.snd} → N (c • p.fst) ≤ c * p.snd),
    add_mem' :=
      (_ :
        ∀ (x : E × ℝ),
          x ∈ {p | N p.fst ≤ p.snd} → ∀ (y : E × ℝ), y ∈ {p | N p.fst ≤ p.snd} → N (x.fst + y.fst) ≤ (x + y).snd) }
f' : E × ℝ →ₗ.[ℝ] ℝ := LinearPMap.coprod (-f) (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : { x // x ∈ f'.domain }), ↑x ∈ s → 0 ≤ ↑f' x
hf'_dense : ∀ (y : E × ℝ), ∃ x, ↑x + y ∈ s
g : E × ℝ →ₗ[ℝ] ℝ
g_nonneg : ∀ (x : E × ℝ), x ∈ s → 0 ≤ ↑g x
g_eq : ∀ (x : { x // x ∈ f.domain }) (y : ℝ), ↑g (↑x, y) = y - ↑f x
⊢ ∃ g, (∀ (x : { x // x ∈ f.domain }), ↑g ↑x = ↑f x) ∧ ∀ (x : E), ↑g x ≤ N x
refine ⟨-g.comp (inl ℝ E ℝ), fun x ↦ ?_, fun x ↦ ?_⟩
no goals
𝕜 : Type ?u.285824
E : Type u_1
F : Type ?u.285830
G : Type ?u.285833
inst✝¹ : AddCommGroup E
inst✝ : 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 : { x // x ∈ f.domain }), ↑f x ≤ N ↑x
s : ConvexCone ℝ (E × ℝ) :=
  { carrier := {p | N p.fst ≤ p.snd},
    smul_mem' := (_ : ∀ (c : ℝ), 0 < c → ∀ (p : E × ℝ), p ∈ {p | N p.fst ≤ p.snd} → N (c • p.fst) ≤ c * p.snd),
    add_mem' :=
      (_ :
        ∀ (x : E × ℝ),
          x ∈ {p | N p.fst ≤ p.snd} → ∀ (y : E × ℝ), y ∈ {p | N p.fst ≤ p.snd} → N (x.fst + y.fst) ≤ (x + y).snd) }
f' : E × ℝ →ₗ.[ℝ] ℝ := LinearPMap.coprod (-f) (toPMap LinearMap.id ⊤)
x : { x // x ∈ f'.domain }
hx : N (↑x).fst ≤ (↑x).snd
⊢ 0 ≤ ↑f' x
simpa using le_trans (hf ⟨x.1.1, x.2.1⟩) hx
case hf'_dense.mk
𝕜 : Type ?u.285824
E : Type u_1
F : Type ?u.285830
G : Type ?u.285833
inst✝¹ : AddCommGroup E
inst✝ : 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 : { x // x ∈ f.domain }), ↑f x ≤ N ↑x
s : ConvexCone ℝ (E × ℝ) :=
  { carrier := {p | N p.fst ≤ p.snd},
    smul_mem' := (_ : ∀ (c : ℝ), 0 < c → ∀ (p : E × ℝ), p ∈ {p | N p.fst ≤ p.snd} → N (c • p.fst) ≤ c * p.snd),
    add_mem' :=
      (_ :
        ∀ (x : E × ℝ),
          x ∈ {p | N p.fst ≤ p.snd} → ∀ (y : E × ℝ), y ∈ {p | N p.fst ≤ p.snd} → N (x.fst + y.fst) ≤ (x + y).snd) }
f' : E × ℝ →ₗ.[ℝ] ℝ := LinearPMap.coprod (-f) (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : { x // x ∈ f'.domain }), ↑x ∈ s → 0 ≤ ↑f' x
x : E
y : ℝ
⊢ ∃ x_1, ↑x_1 + (x, y) ∈ s
case hf'_dense
𝕜 : Type ?u.285824
E : Type u_1
F : Type ?u.285830
G : Type ?u.285833
inst✝¹ : AddCommGroup E
inst✝ : 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 : { x // x ∈ f.domain }), ↑f x ≤ N ↑x
s : ConvexCone ℝ (E × ℝ) :=
  { carrier := {p | N p.fst ≤ p.snd},
    smul_mem' := (_ : ∀ (c : ℝ), 0 < c → ∀ (p : E × ℝ), p ∈ {p | N p.fst ≤ p.snd} → N (c • p.fst) ≤ c * p.snd),
    add_mem' :=
      (_ :
        ∀ (x : E × ℝ),
          x ∈ {p | N p.fst ≤ p.snd} → ∀ (y : E × ℝ), y ∈ {p | N p.fst ≤ p.snd} → N (x.fst + y.fst) ≤ (x + y).snd) }
f' : E × ℝ →ₗ.[ℝ] ℝ := LinearPMap.coprod (-f) (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : { x // x ∈ f'.domain }), ↑x ∈ s → 0 ≤ ↑f' x
⊢ ∀ (y : E × ℝ), ∃ x, ↑x + y ∈ s
rintro ⟨x, y⟩
case hf'_dense.mk
𝕜 : Type ?u.285824
E : Type u_1
F : Type ?u.285830
G : Type ?u.285833
inst✝¹ : AddCommGroup E
inst✝ : 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 : { x // x ∈ f.domain }), ↑f x ≤ N ↑x
s : ConvexCone ℝ (E × ℝ) :=
  { carrier := {p | N p.fst ≤ p.snd},
    smul_mem' := (_ : ∀ (c : ℝ), 0 < c → ∀ (p : E × ℝ), p ∈ {p | N p.fst ≤ p.snd} → N (c • p.fst) ≤ c * p.snd),
    add_mem' :=
      (_ :
        ∀ (x : E × ℝ),
          x ∈ {p | N p.fst ≤ p.snd} → ∀ (y : E × ℝ), y ∈ {p | N p.fst ≤ p.snd} → N (x.fst + y.fst) ≤ (x + y).snd) }
f' : E × ℝ →ₗ.[ℝ] ℝ := LinearPMap.coprod (-f) (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : { x // x ∈ f'.domain }), ↑x ∈ s → 0 ≤ ↑f' x
x : E
y : ℝ
⊢ ↑{ val := (0, N x - y),
          property := (_ : (0, N x - y).fst ∈ ↑(-f).domain ∧ (0, N x - y).snd ∈ ↑(toPMap LinearMap.id ⊤).domain) } +
      (x, y) ∈
    s
case hf'_dense.mk
𝕜 : Type ?u.285824
E : Type u_1
F : Type ?u.285830
G : Type ?u.285833
inst✝¹ : AddCommGroup E
inst✝ : 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 : { x // x ∈ f.domain }), ↑f x ≤ N ↑x
s : ConvexCone ℝ (E × ℝ) :=
  { carrier := {p | N p.fst ≤ p.snd},
    smul_mem' := (_ : ∀ (c : ℝ), 0 < c → ∀ (p : E × ℝ), p ∈ {p | N p.fst ≤ p.snd} → N (c • p.fst) ≤ c * p.snd),
    add_mem' :=
      (_ :
        ∀ (x : E × ℝ),
          x ∈ {p | N p.fst ≤ p.snd} → ∀ (y : E × ℝ), y ∈ {p | N p.fst ≤ p.snd} → N (x.fst + y.fst) ≤ (x + y).snd) }
f' : E × ℝ →ₗ.[ℝ] ℝ := LinearPMap.coprod (-f) (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : { x // x ∈ f'.domain }), ↑x ∈ s → 0 ≤ ↑f' x
x : E
y : ℝ
⊢ ∃ x_1, ↑x_1 + (x, y) ∈ s
refine' ⟨⟨(0, N x - y), ⟨f.domain.zero_mem, trivial⟩⟩, _⟩
no goals
case hf'_dense.mk
𝕜 : Type ?u.285824
E : Type u_1
F : Type ?u.285830
G : Type ?u.285833
inst✝¹ : AddCommGroup E
inst✝ : 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 : { x // x ∈ f.domain }), ↑f x ≤ N ↑x
s : ConvexCone ℝ (E × ℝ) :=
  { carrier := {p | N p.fst ≤ p.snd},
    smul_mem' := (_ : ∀ (c : ℝ), 0 < c → ∀ (p : E × ℝ), p ∈ {p | N p.fst ≤ p.snd} → N (c • p.fst) ≤ c * p.snd),
    add_mem' :=
      (_ :
        ∀ (x : E × ℝ),
          x ∈ {p | N p.fst ≤ p.snd} → ∀ (y : E × ℝ), y ∈ {p | N p.fst ≤ p.snd} → N (x.fst + y.fst) ≤ (x + y).snd) }
f' : E × ℝ →ₗ.[ℝ] ℝ := LinearPMap.coprod (-f) (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : { x // x ∈ f'.domain }), ↑x ∈ s → 0 ≤ ↑f' x
x : E
y : ℝ
⊢ ↑{ val := (0, N x - y),
          property := (_ : (0, N x - y).fst ∈ ↑(-f).domain ∧ (0, N x - y).snd ∈ ↑(toPMap LinearMap.id ⊤).domain) } +
      (x, y) ∈
    s
simp only [ConvexCone.mem_mk, mem_setOf_eq, Prod.fst_add, Prod.snd_add, zero_add,
  sub_add_cancel, le_rfl]
no goals
case intro.intro.refine_1
𝕜 : Type ?u.285824
E : Type u_1
F : Type ?u.285830
G : Type ?u.285833
inst✝¹ : AddCommGroup E
inst✝ : 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 : { x // x ∈ f.domain }), ↑f x ≤ N ↑x
s : ConvexCone ℝ (E × ℝ) :=
  { carrier := {p | N p.fst ≤ p.snd},
    smul_mem' := (_ : ∀ (c : ℝ), 0 < c → ∀ (p : E × ℝ), p ∈ {p | N p.fst ≤ p.snd} → N (c • p.fst) ≤ c * p.snd),
    add_mem' :=
      (_ :
        ∀ (x : E × ℝ),
          x ∈ {p | N p.fst ≤ p.snd} → ∀ (y : E × ℝ), y ∈ {p | N p.fst ≤ p.snd} → N (x.fst + y.fst) ≤ (x + y).snd) }
f' : E × ℝ →ₗ.[ℝ] ℝ := LinearPMap.coprod (-f) (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : { x // x ∈ f'.domain }), ↑x ∈ s → 0 ≤ ↑f' x
hf'_dense : ∀ (y : E × ℝ), ∃ x, ↑x + y ∈ s
g : E × ℝ →ₗ[ℝ] ℝ
g_nonneg : ∀ (x : E × ℝ), x ∈ s → 0 ≤ ↑g x
g_eq : ∀ (x : { x // x ∈ f.domain }) (y : ℝ), ↑g (↑x, y) = y - ↑f x
x : { x // x ∈ f.domain }
⊢ ↑(-comp g (inl ℝ E ℝ)) ↑x = ↑f x
simp [g_eq x 0]
no goals
case intro.intro.refine_2
𝕜 : Type ?u.285824
E : Type u_1
F : Type ?u.285830
G : Type ?u.285833
inst✝¹ : AddCommGroup E
inst✝ : 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 : { x // x ∈ f.domain }), ↑f x ≤ N ↑x
s : ConvexCone ℝ (E × ℝ) :=
  { carrier := {p | N p.fst ≤ p.snd},
    smul_mem' := (_ : ∀ (c : ℝ), 0 < c → ∀ (p : E × ℝ), p ∈ {p | N p.fst ≤ p.snd} → N (c • p.fst) ≤ c * p.snd),
    add_mem' :=
      (_ :
        ∀ (x : E × ℝ),
          x ∈ {p | N p.fst ≤ p.snd} → ∀ (y : E × ℝ), y ∈ {p | N p.fst ≤ p.snd} → N (x.fst + y.fst) ≤ (x + y).snd) }
f' : E × ℝ →ₗ.[ℝ] ℝ := LinearPMap.coprod (-f) (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : { x // x ∈ f'.domain }), ↑x ∈ s → 0 ≤ ↑f' x
hf'_dense : ∀ (y : E × ℝ), ∃ x, ↑x + y ∈ s
g : E × ℝ →ₗ[ℝ] ℝ
g_nonneg : ∀ (x : E × ℝ), x ∈ s → 0 ≤ ↑g x
g_eq : ∀ (x : { x // x ∈ f.domain }) (y : ℝ), ↑g (↑x, y) = y - ↑f x
x : E
⊢ ↑(-comp g (inl ℝ E ℝ)) x ≤ N x
calc -g (x, 0) = g (0, N x) - g (x, N x) := by simp [← map_sub, ← map_neg]
  _ = N x - g (x, N x) := by simpa using g_eq 0 (N x)
  _ ≤ N x := by simpa using g_nonneg ⟨x, N x⟩ (le_refl (N x))
no goals
𝕜 : Type ?u.285824
E : Type u_1
F : Type ?u.285830
G : Type ?u.285833
inst✝¹ : AddCommGroup E
inst✝ : 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 : { x // x ∈ f.domain }), ↑f x ≤ N ↑x
s : ConvexCone ℝ (E × ℝ) :=
  { carrier := {p | N p.fst ≤ p.snd},
    smul_mem' := (_ : ∀ (c : ℝ), 0 < c → ∀ (p : E × ℝ), p ∈ {p | N p.fst ≤ p.snd} → N (c • p.fst) ≤ c * p.snd),
    add_mem' :=
      (_ :
        ∀ (x : E × ℝ),
          x ∈ {p | N p.fst ≤ p.snd} → ∀ (y : E × ℝ), y ∈ {p | N p.fst ≤ p.snd} → N (x.fst + y.fst) ≤ (x + y).snd) }
f' : E × ℝ →ₗ.[ℝ] ℝ := LinearPMap.coprod (-f) (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : { x // x ∈ f'.domain }), ↑x ∈ s → 0 ≤ ↑f' x
hf'_dense : ∀ (y : E × ℝ), ∃ x, ↑x + y ∈ s
g : E × ℝ →ₗ[ℝ] ℝ
g_nonneg : ∀ (x : E × ℝ), x ∈ s → 0 ≤ ↑g x
g_eq : ∀ (x : { x // x ∈ f.domain }) (y : ℝ), ↑g (↑x, y) = y - ↑f x
x : E
⊢ -↑g (x, 0) = ↑g (0, N x) - ↑g (x, N x)
simp [← map_sub, ← map_neg]
no goals
𝕜 : Type ?u.285824
E : Type u_1
F : Type ?u.285830
G : Type ?u.285833
inst✝¹ : AddCommGroup E
inst✝ : 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 : { x // x ∈ f.domain }), ↑f x ≤ N ↑x
s : ConvexCone ℝ (E × ℝ) :=
  { carrier := {p | N p.fst ≤ p.snd},
    smul_mem' := (_ : ∀ (c : ℝ), 0 < c → ∀ (p : E × ℝ), p ∈ {p | N p.fst ≤ p.snd} → N (c • p.fst) ≤ c * p.snd),
    add_mem' :=
      (_ :
        ∀ (x : E × ℝ),
          x ∈ {p | N p.fst ≤ p.snd} → ∀ (y : E × ℝ), y ∈ {p | N p.fst ≤ p.snd} → N (x.fst + y.fst) ≤ (x + y).snd) }
f' : E × ℝ →ₗ.[ℝ] ℝ := LinearPMap.coprod (-f) (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : { x // x ∈ f'.domain }), ↑x ∈ s → 0 ≤ ↑f' x
hf'_dense : ∀ (y : E × ℝ), ∃ x, ↑x + y ∈ s
g : E × ℝ →ₗ[ℝ] ℝ
g_nonneg : ∀ (x : E × ℝ), x ∈ s → 0 ≤ ↑g x
g_eq : ∀ (x : { x // x ∈ f.domain }) (y : ℝ), ↑g (↑x, y) = y - ↑f x
x : E
⊢ ↑g (0, N x) - ↑g (x, N x) = N x - ↑g (x, N x)
simpa using g_eq 0 (N x)
no goals
𝕜 : Type ?u.285824
E : Type u_1
F : Type ?u.285830
G : Type ?u.285833
inst✝¹ : AddCommGroup E
inst✝ : 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 : { x // x ∈ f.domain }), ↑f x ≤ N ↑x
s : ConvexCone ℝ (E × ℝ) :=
  { carrier := {p | N p.fst ≤ p.snd},
    smul_mem' := (_ : ∀ (c : ℝ), 0 < c → ∀ (p : E × ℝ), p ∈ {p | N p.fst ≤ p.snd} → N (c • p.fst) ≤ c * p.snd),
    add_mem' :=
      (_ :
        ∀ (x : E × ℝ),
          x ∈ {p | N p.fst ≤ p.snd} → ∀ (y : E × ℝ), y ∈ {p | N p.fst ≤ p.snd} → N (x.fst + y.fst) ≤ (x + y).snd) }
f' : E × ℝ →ₗ.[ℝ] ℝ := LinearPMap.coprod (-f) (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : { x // x ∈ f'.domain }), ↑x ∈ s → 0 ≤ ↑f' x
hf'_dense : ∀ (y : E × ℝ), ∃ x, ↑x + y ∈ s
g : E × ℝ →ₗ[ℝ] ℝ
g_nonneg : ∀ (x : E × ℝ), x ∈ s → 0 ≤ ↑g x
g_eq : ∀ (x : { x // x ∈ f.domain }) (y : ℝ), ↑g (↑x, y) = y - ↑f x
x : E
⊢ N x - ↑g (x, N x) ≤ N x
simpa using g_nonneg ⟨x, N x⟩ (le_refl (N x))