-- Mathlib/Analysis/Convex/Cone/Extension.lean
theorem step (nonneg : ∀ x : f.domain, (x : E) ∈ s → 0 ≤ f x)
    (dense : ∀ y, ∃ x : f.domain, (x : E) + y ∈ s) (hdom : f.domain ≠ ⊤) :
    ∃ g, f < g ∧ ∀ x : g.domain, (x : E) ∈ s → 0 ≤ g x

Proof state:
case intro.intro.intro.intro.refine_1
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (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 : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
H : f.supSpanSingleton y (-c) hy ≤ f
⊢ False

Tactic:
replace H := LinearPMap.domain_mono.monotone H

Result:
case intro.intro.intro.intro.refine_1
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (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 : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
H : (f.supSpanSingleton y (-c) hy).domain ≤ f.domain
⊢ False

Proof state:
case refine_2.intro.intro.intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (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 : ↥f.domain
hxn : xn ∈ {x | -↑x - y ∈ s}
xp : ↥f.domain
hxp : xp ∈ {x | ↑x + y ∈ s}
this : ↑xp + y + (-↑xn - y) ∈ s
⊢ ↑f xn ≤ ↑f xp

Tactic:
rw [add_assoc, add_sub_cancel, ← sub_eq_add_neg, ← AddSubgroupClass.coe_sub] at this

Result:
case refine_2.intro.intro.intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (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 : ↥f.domain
hxn : xn ∈ {x | -↑x - y ∈ s}
xp : ↥f.domain
hxp : xp ∈ {x | ↑x + y ∈ s}
this : ↑(xp - xn) ∈ s
⊢ ↑f xn ≤ ↑f xp

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (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 : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) ⋯).domain
hz : x + r • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x + r • y ∈ s
hr : r < 0
this : -(r⁻¹ • x) - y ∈ s
⊢ -↑(r⁻¹ • ⟨x, hx⟩) - y ∈ s

Tactic:
exact this

Result:
no goals

Proof state:
case intro.intro.intro.intro.refine_2.mk.intro.intro.intro.intro.intro.inr.inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (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 : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
hy' : 0 • y ∈ (LinearPMap.mkSpanSingleton y (-c) ⋯).domain
hz : x + 0 • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x + 0 • y ∈ s
⊢ 0 • c ≤ ↑f ⟨x, hx⟩

Tactic:
simp only [zero_smul, add_zero] at hzs ⊢

Result:
case intro.intro.intro.intro.refine_2.mk.intro.intro.intro.intro.intro.inr.inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (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 : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
hy' : 0 • y ∈ (LinearPMap.mkSpanSingleton y (-c) ⋯).domain
hz : x + 0 • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x ∈ s
⊢ 0 ≤ ↑f ⟨x, hx⟩

Proof state:
case intro.intro.intro.intro.refine_2.mk.intro.intro.intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (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 : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
y' : E
hy' : y' ∈ (LinearPMap.mkSpanSingleton y (-c) ⋯).domain
hz : x + y' ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : ↑⟨x + y', hz⟩ ∈ s
⊢ 0 ≤ ↑(f.supSpanSingleton y (-c) hy) ⟨x + y', hz⟩

Tactic:
rcases mem_span_singleton.1 hy' with ⟨r, rfl⟩

Result:
case intro.intro.intro.intro.refine_2.mk.intro.intro.intro.intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (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 : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) ⋯).domain
hz : x + r • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : ↑⟨x + r • y, hz⟩ ∈ s
⊢ 0 ≤ ↑(f.supSpanSingleton y (-c) hy) ⟨x + r • y, hz⟩

Proof state:
case intro.intro.intro.intro.refine_2.mk.intro.intro.intro.intro.intro.inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (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 : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) ⋯).domain
hz : x + r • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x + r • y ∈ s
hr : r < 0
⊢ r • c ≤ ↑f ⟨x, hx⟩

Tactic:
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]

Result:
case intro.intro.intro.intro.refine_2.mk.intro.intro.intro.intro.intro.inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (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 : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) ⋯).domain
hz : x + r • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x + r • y ∈ s
hr : r < 0
this : -(r⁻¹ • x) - y ∈ s
⊢ r • c ≤ ↑f ⟨x, hx⟩

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (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 : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) ⋯).domain
hz : x + r • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x + r • y ∈ s
hr : 0 < r
⊢ r⁻¹ • x + y ∈ s

Tactic:
rwa [← s.smul_mem_iff hr, smul_add, smul_smul, mul_inv_cancel₀ hr.ne', one_smul]

Result:
no goals