case intro.intro
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
⊢ ∃ g, f < g ∧ ∀ (x : { x // x ∈ g.domain }), ↑x ∈ s → 0 ≤ ↑g x
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
⊢ ∃ g, f < g ∧ ∀ (x : { x // x ∈ g.domain }), ↑x ∈ s → 0 ≤ ↑g x
obtain ⟨y, -, hy⟩ : ∃ y ∈ ⊤, y ∉ f.domain :=
  @SetLike.exists_of_lt (Submodule ℝ E) _ _ _ _ (lt_top_iff_ne_top.2 hdom)
case intro.intro.intro.intro.refine'_1
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
⊢ f < LinearPMap.supSpanSingleton f y (-c) hy

case intro.intro.intro.intro.refine'_2
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
⊢ ∀ (x : { x // x ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain }),
    ↑x ∈ s → 0 ≤ ↑(LinearPMap.supSpanSingleton f y (-c) hy) x
case intro.intro.intro.intro
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
⊢ ∃ g, f < g ∧ ∀ (x : { x // x ∈ g.domain }), ↑x ∈ s → 0 ≤ ↑g x
refine' ⟨f.supSpanSingleton y (-c) hy, _, _⟩
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
⊢ ∃ c, (∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c) ∧ ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
⊢ ∃ c, (∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c) ∧ ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
set Sp := f '' { x : f.domain | (x : E) + y ∈ s }
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
⊢ ∃ c, (∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c) ∧ ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
⊢ ∃ c, (∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c) ∧ ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
set Sn := f '' { x : f.domain | -(x : E) - y ∈ s }
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
⊢ Set.Nonempty (upperBounds Sn ∩ lowerBounds Sp)
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
⊢ ∃ c, (∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c) ∧ ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
suffices (upperBounds Sn ∩ lowerBounds Sp).Nonempty by
  simpa only [Set.Nonempty, upperBounds, lowerBounds, ball_image_iff] using this
case refine'_1
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
⊢ Set.Nonempty {x | -↑x - y ∈ s}

case refine'_2
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
⊢ ∀ (x : ℝ), x ∈ Sn → ∀ (y : ℝ), y ∈ Sp → x ≤ y
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
⊢ Set.Nonempty (upperBounds Sn ∩ lowerBounds Sp)
refine' exists_between_of_forall_le (Nonempty.image f _) (Nonempty.image f (dense y)) _
case refine'_2.intro.intro.intro.intro
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
xn : { x // x ∈ f.domain }
hxn : xn ∈ {x | -↑x - y ∈ s}
xp : { x // x ∈ f.domain }
hxp : xp ∈ {x | ↑x + y ∈ s}
⊢ ↑f xn ≤ ↑f xp
case refine'_2
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
⊢ ∀ (x : ℝ), x ∈ Sn → ∀ (y : ℝ), y ∈ Sp → x ≤ y
rintro a ⟨xn, hxn, rfl⟩ b ⟨xp, hxp, rfl⟩
case refine'_2.intro.intro.intro.intro
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
xn : { x // x ∈ f.domain }
hxn : xn ∈ {x | -↑x - y ∈ s}
xp : { x // x ∈ f.domain }
hxp : xp ∈ {x | ↑x + y ∈ s}
this : ↑xp + y + (-↑xn - y) ∈ s
⊢ ↑f xn ≤ ↑f xp
case refine'_2.intro.intro.intro.intro
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
xn : { x // x ∈ f.domain }
hxn : xn ∈ {x | -↑x - y ∈ s}
xp : { x // x ∈ f.domain }
hxp : xp ∈ {x | ↑x + y ∈ s}
⊢ ↑f xn ≤ ↑f xp
have := s.add_mem hxp hxn
case refine'_2.intro.intro.intro.intro
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
xn : { x // x ∈ f.domain }
hxn : xn ∈ {x | -↑x - y ∈ s}
xp : { x // x ∈ f.domain }
hxp : xp ∈ {x | ↑x + y ∈ s}
this✝ : ↑xp - ↑xn ∈ s
this : ↑(xp - xn) ∈ s
⊢ ↑f xn ≤ ↑f xp
case refine'_2.intro.intro.intro.intro
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
xn : { x // x ∈ f.domain }
hxn : xn ∈ {x | -↑x - y ∈ s}
xp : { x // x ∈ f.domain }
hxp : xp ∈ {x | ↑x + y ∈ s}
this : ↑xp + y + (-↑xn - y) ∈ s
⊢ ↑f xn ≤ ↑f xp
rw [add_assoc, add_sub_cancel'_right, ← sub_eq_add_neg, ← AddSubgroupClass.coe_sub] at this
case refine'_2.intro.intro.intro.intro
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
xn : { x // x ∈ f.domain }
hxn : xn ∈ {x | -↑x - y ∈ s}
xp : { x // x ∈ f.domain }
hxp : xp ∈ {x | ↑x + y ∈ s}
this✝ : ↑xp - ↑xn ∈ s
this : 0 ≤ ↑f (xp - xn)
⊢ ↑f xn ≤ ↑f xp
case refine'_2.intro.intro.intro.intro
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
xn : { x // x ∈ f.domain }
hxn : xn ∈ {x | -↑x - y ∈ s}
xp : { x // x ∈ f.domain }
hxp : xp ∈ {x | ↑x + y ∈ s}
this✝ : ↑xp - ↑xn ∈ s
this : ↑(xp - xn) ∈ s
⊢ ↑f xn ≤ ↑f xp
replace := nonneg _ this
no goals
case refine'_2.intro.intro.intro.intro
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
xn : { x // x ∈ f.domain }
hxn : xn ∈ {x | -↑x - y ∈ s}
xp : { x // x ∈ f.domain }
hxp : xp ∈ {x | ↑x + y ∈ s}
this✝ : ↑xp - ↑xn ∈ s
this : 0 ≤ ↑f (xp - xn)
⊢ ↑f xn ≤ ↑f xp
rwa [f.map_sub, sub_nonneg] at this
no goals
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
this : Set.Nonempty (upperBounds Sn ∩ lowerBounds Sp)
⊢ ∃ c, (∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c) ∧ ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
simpa only [Set.Nonempty, upperBounds, lowerBounds, ball_image_iff] using this
case refine'_1.intro
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
x : { x // x ∈ f.domain }
hx : ↑x + -y ∈ s
⊢ Set.Nonempty {x | -↑x - y ∈ s}
case refine'_1
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
⊢ Set.Nonempty {x | -↑x - y ∈ s}
rcases dense (-y) with ⟨x, hx⟩
case refine'_1.intro
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
x : { x // x ∈ f.domain }
hx : -↑(-x) - y ∈ s
⊢ Set.Nonempty {x | -↑x - y ∈ s}
case refine'_1.intro
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
x : { x // x ∈ f.domain }
hx : ↑x + -y ∈ s
⊢ Set.Nonempty {x | -↑x - y ∈ s}
rw [← neg_neg x, AddSubgroupClass.coe_neg, ← sub_eq_add_neg] at hx
no goals
case refine'_1.intro
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
x : { x // x ∈ f.domain }
hx : -↑(-x) - y ∈ s
⊢ Set.Nonempty {x | -↑x - y ∈ s}
exact ⟨_, hx⟩
case intro.intro.intro.intro.refine'_1
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
H : LinearPMap.supSpanSingleton f y (-c) hy ≤ f
⊢ False
case intro.intro.intro.intro.refine'_1
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
⊢ f < LinearPMap.supSpanSingleton f y (-c) hy
refine' lt_iff_le_not_le.2 ⟨f.left_le_sup _ _, fun H => _⟩
case intro.intro.intro.intro.refine'_1
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
H : (LinearPMap.supSpanSingleton f y (-c) hy).domain ≤ f.domain
⊢ False
case intro.intro.intro.intro.refine'_1
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
H : LinearPMap.supSpanSingleton f y (-c) hy ≤ f
⊢ False
replace H := LinearPMap.domain_mono.monotone H
case intro.intro.intro.intro.refine'_1
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
H : f.domain ≤ f.domain ∧ y ∈ ↑f.domain
⊢ False
case intro.intro.intro.intro.refine'_1
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
H : (LinearPMap.supSpanSingleton f y (-c) hy).domain ≤ f.domain
⊢ False
rw [LinearPMap.domain_supSpanSingleton, sup_le_iff, span_le, singleton_subset_iff] at H
no goals
case intro.intro.intro.intro.refine'_1
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
H : f.domain ≤ f.domain ∧ y ∈ ↑f.domain
⊢ False
exact hy H.2
case intro.intro.intro.intro.refine'_2.mk
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
z : E
hz : z ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain
hzs : ↑{ val := z, property := hz } ∈ s
⊢ 0 ≤ ↑(LinearPMap.supSpanSingleton f y (-c) hy) { val := z, property := hz }
case intro.intro.intro.intro.refine'_2
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
⊢ ∀ (x : { x // x ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain }),
    ↑x ∈ s → 0 ≤ ↑(LinearPMap.supSpanSingleton f y (-c) hy) x
rintro ⟨z, hz⟩ hzs
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
y' : E
hy' : y' ∈ (LinearPMap.mkSpanSingleton y (-c) (_ : y = 0 → False)).domain
hz : x + y' ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain
hzs : ↑{ val := x + y', property := hz } ∈ s
⊢ 0 ≤ ↑(LinearPMap.supSpanSingleton f y (-c) hy) { val := x + y', property := hz }
case intro.intro.intro.intro.refine'_2.mk
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
z : E
hz : z ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain
hzs : ↑{ val := z, property := hz } ∈ s
⊢ 0 ≤ ↑(LinearPMap.supSpanSingleton f y (-c) hy) { val := z, property := hz }
rcases mem_sup.1 hz with ⟨x, hx, y', hy', rfl⟩
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) (_ : y = 0 → False)).domain
hz : x + r • y ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain
hzs : ↑{ val := x + r • y, property := hz } ∈ s
⊢ 0 ≤ ↑(LinearPMap.supSpanSingleton f y (-c) hy) { val := x + r • y, property := hz }
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
y' : E
hy' : y' ∈ (LinearPMap.mkSpanSingleton y (-c) (_ : y = 0 → False)).domain
hz : x + y' ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain
hzs : ↑{ val := x + y', property := hz } ∈ s
⊢ 0 ≤ ↑(LinearPMap.supSpanSingleton f y (-c) hy) { val := x + y', property := hz }
rcases mem_span_singleton.1 hy' with ⟨r, rfl⟩
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) (_ : y = 0 → False)).domain
hz : x + r • y ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain
hzs : x + r • y ∈ s
⊢ 0 ≤ ↑(LinearPMap.supSpanSingleton f y (-c) hy) { val := x + r • y, property := hz }
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) (_ : y = 0 → False)).domain
hz : x + r • y ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain
hzs : ↑{ val := x + r • y, property := hz } ∈ s
⊢ 0 ≤ ↑(LinearPMap.supSpanSingleton f y (-c) hy) { val := x + r • y, property := hz }
simp only [Subtype.coe_mk] at hzs
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) (_ : y = 0 → False)).domain
hz : x + r • y ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain
hzs : x + r • y ∈ s
⊢ r • c ≤ ↑f { val := x, property := hx }
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) (_ : y = 0 → False)).domain
hz : x + r • y ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain
hzs : x + r • y ∈ s
⊢ 0 ≤ ↑(LinearPMap.supSpanSingleton f y (-c) hy) { val := x + r • y, property := hz }
erw [LinearPMap.supSpanSingleton_apply_mk _ _ _ _ _ hx, smul_neg, ← sub_eq_add_neg, sub_nonneg]
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro.inl
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) (_ : y = 0 → False)).domain
hz : x + r • y ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain
hzs : x + r • y ∈ s
hr : r < 0
⊢ r • c ≤ ↑f { val := x, property := hx }

case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro.inr.inl
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) (_ : y = 0 → False)).domain
hz : x + r • y ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain
hzs : x + r • y ∈ s
hr : r = 0
⊢ r • c ≤ ↑f { val := x, property := hx }

case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro.inr.inr
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) (_ : y = 0 → False)).domain
hz : x + r • y ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain
hzs : x + r • y ∈ s
hr : 0 < r
⊢ r • c ≤ ↑f { val := x, property := hx }
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) (_ : y = 0 → False)).domain
hz : x + r • y ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain
hzs : x + r • y ∈ s
⊢ r • c ≤ ↑f { val := x, property := hx }
rcases lt_trichotomy r 0 with (hr | hr | hr)
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro.inl
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) (_ : y = 0 → False)).domain
hz : x + r • y ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain
hzs : x + r • y ∈ s
hr : r < 0
this : -(r⁻¹ • x) - y ∈ s
⊢ r • c ≤ ↑f { val := x, property := hx }
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro.inl
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) (_ : y = 0 → False)).domain
hz : x + r • y ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain
hzs : x + r • y ∈ s
hr : r < 0
⊢ r • c ≤ ↑f { val := x, property := hx }
have : -(r⁻¹ • x) - y ∈ s := by
  rwa [← s.smul_mem_iff (neg_pos.2 hr), smul_sub, smul_neg, neg_smul, neg_neg, smul_smul,
    mul_inv_cancel hr.ne, one_smul, sub_eq_add_neg, neg_smul, neg_neg]
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro.inl
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) (_ : y = 0 → False)).domain
hz : x + r • y ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain
hzs : x + r • y ∈ s
hr : r < 0
this : ↑f (r⁻¹ • { val := x, property := hx }) ≤ c
⊢ r • c ≤ ↑f { val := x, property := hx }
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro.inl
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) (_ : y = 0 → False)).domain
hz : x + r • y ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain
hzs : x + r • y ∈ s
hr : r < 0
this : -(r⁻¹ • x) - y ∈ s
⊢ r • c ≤ ↑f { val := x, property := hx }
replace : f (r⁻¹ • ⟨x, hx⟩) ≤ c := le_c (r⁻¹ • ⟨x, hx⟩) (by exact this)
no goals
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro.inl
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) (_ : y = 0 → False)).domain
hz : x + r • y ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain
hzs : x + r • y ∈ s
hr : r < 0
this : ↑f (r⁻¹ • { val := x, property := hx }) ≤ c
⊢ r • c ≤ ↑f { val := x, property := hx }
rwa [← mul_le_mul_left (neg_pos.2 hr), neg_mul, neg_mul, neg_le_neg_iff, f.map_smul,
  smul_eq_mul, ← mul_assoc, mul_inv_cancel hr.ne, one_mul] at this
no goals
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) (_ : y = 0 → False)).domain
hz : x + r • y ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain
hzs : x + r • y ∈ s
hr : r < 0
⊢ -(r⁻¹ • x) - y ∈ s
rwa [← s.smul_mem_iff (neg_pos.2 hr), smul_sub, smul_neg, neg_smul, neg_neg, smul_smul,
  mul_inv_cancel hr.ne, one_smul, sub_eq_add_neg, neg_smul, neg_neg]
no goals
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) (_ : y = 0 → False)).domain
hz : x + r • y ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain
hzs : x + r • y ∈ s
hr : r < 0
this : -(r⁻¹ • x) - y ∈ s
⊢ -↑(r⁻¹ • { val := x, property := hx }) - y ∈ s
exact this
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro.inr.inl
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
hy' : 0 • y ∈ (LinearPMap.mkSpanSingleton y (-c) (_ : y = 0 → False)).domain
hz : x + 0 • y ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain
hzs : x + 0 • y ∈ s
⊢ 0 • c ≤ ↑f { val := x, property := hx }
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro.inr.inl
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) (_ : y = 0 → False)).domain
hz : x + r • y ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain
hzs : x + r • y ∈ s
hr : r = 0
⊢ r • c ≤ ↑f { val := x, property := hx }
subst r
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro.inr.inl
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
hy' : 0 • y ∈ (LinearPMap.mkSpanSingleton y (-c) (_ : y = 0 → False)).domain
hz : x + 0 • y ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain
hzs : x ∈ s
⊢ 0 ≤ ↑f { val := x, property := hx }
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro.inr.inl
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
hy' : 0 • y ∈ (LinearPMap.mkSpanSingleton y (-c) (_ : y = 0 → False)).domain
hz : x + 0 • y ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain
hzs : x + 0 • y ∈ s
⊢ 0 • c ≤ ↑f { val := x, property := hx }
simp only [zero_smul, add_zero] at hzs⊢
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro.inr.inl.a
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
hy' : 0 • y ∈ (LinearPMap.mkSpanSingleton y (-c) (_ : y = 0 → False)).domain
hz : x + 0 • y ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain
hzs : x ∈ s
⊢ ↑{ val := x, property := hx } ∈ s
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro.inr.inl
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
hy' : 0 • y ∈ (LinearPMap.mkSpanSingleton y (-c) (_ : y = 0 → False)).domain
hz : x + 0 • y ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain
hzs : x ∈ s
⊢ 0 ≤ ↑f { val := x, property := hx }
apply nonneg
no goals
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro.inr.inl.a
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
hy' : 0 • y ∈ (LinearPMap.mkSpanSingleton y (-c) (_ : y = 0 → False)).domain
hz : x + 0 • y ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain
hzs : x ∈ s
⊢ ↑{ val := x, property := hx } ∈ s
exact hzs
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro.inr.inr
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) (_ : y = 0 → False)).domain
hz : x + r • y ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain
hzs : x + r • y ∈ s
hr : 0 < r
this : r⁻¹ • x + y ∈ s
⊢ r • c ≤ ↑f { val := x, property := hx }
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro.inr.inr
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) (_ : y = 0 → False)).domain
hz : x + r • y ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain
hzs : x + r • y ∈ s
hr : 0 < r
⊢ r • c ≤ ↑f { val := x, property := hx }
have : r⁻¹ • x + y ∈ s := by
  rwa [← s.smul_mem_iff hr, smul_add, smul_smul, mul_inv_cancel hr.ne', one_smul]
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro.inr.inr
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) (_ : y = 0 → False)).domain
hz : x + r • y ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain
hzs : x + r • y ∈ s
hr : 0 < r
this : c ≤ ↑f (r⁻¹ • { val := x, property := hx })
⊢ r • c ≤ ↑f { val := x, property := hx }
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro.inr.inr
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) (_ : y = 0 → False)).domain
hz : x + r • y ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain
hzs : x + r • y ∈ s
hr : 0 < r
this : r⁻¹ • x + y ∈ s
⊢ r • c ≤ ↑f { val := x, property := hx }
replace : c ≤ f (r⁻¹ • ⟨x, hx⟩) := c_le (r⁻¹ • ⟨x, hx⟩) (by exact this)
no goals
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro.inr.inr
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) (_ : y = 0 → False)).domain
hz : x + r • y ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain
hzs : x + r • y ∈ s
hr : 0 < r
this : c ≤ ↑f (r⁻¹ • { val := x, property := hx })
⊢ r • c ≤ ↑f { val := x, property := hx }
rwa [← mul_le_mul_left hr, f.map_smul, smul_eq_mul, ← mul_assoc, mul_inv_cancel hr.ne',
  one_mul] at this
no goals
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) (_ : y = 0 → False)).domain
hz : x + r • y ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain
hzs : x + r • y ∈ s
hr : 0 < r
⊢ r⁻¹ • x + y ∈ s
rwa [← s.smul_mem_iff hr, smul_add, smul_smul, mul_inv_cancel hr.ne', one_smul]
no goals
𝕜 : Type ?u.190292
E : Type u_1
F : Type ?u.190298
G : Type ?u.190301
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
hdom : f.domain ≠ ⊤
y : E
hy : ¬y ∈ f.domain
c : ℝ
le_c : ∀ (x : { x // x ∈ f.domain }), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : { x // x ∈ f.domain }), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) (_ : y = 0 → False)).domain
hz : x + r • y ∈ (LinearPMap.supSpanSingleton f y (-c) hy).domain
hzs : x + r • y ∈ s
hr : 0 < r
this : r⁻¹ • x + y ∈ s
⊢ ↑(r⁻¹ • { val := x, property := hx }) + y ∈ s
exact this