[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
S✝ T✝ S T : ConvexCone 𝕜 E
h : S.carrier = T.carrier
⊢ S = T
[PROOFSTEP]
cases S
[GOAL]
case mk
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
S T✝ T : ConvexCone 𝕜 E
carrier✝ : Set E
smul_mem'✝ : ∀ ⦃c : 𝕜⦄, 0 < c → ∀ ⦃x : E⦄, x ∈ carrier✝ → c • x ∈ carrier✝
add_mem'✝ : ∀ ⦃x : E⦄, x ∈ carrier✝ → ∀ ⦃y : E⦄, y ∈ carrier✝ → x + y ∈ carrier✝
h : { carrier := carrier✝, smul_mem' := smul_mem'✝, add_mem' := add_mem'✝ }.carrier = T.carrier
⊢ { carrier := carrier✝, smul_mem' := smul_mem'✝, add_mem' := add_mem'✝ } = T
[PROOFSTEP]
cases T
[GOAL]
case mk.mk
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
S T : ConvexCone 𝕜 E
carrier✝¹ : Set E
smul_mem'✝¹ : ∀ ⦃c : 𝕜⦄, 0 < c → ∀ ⦃x : E⦄, x ∈ carrier✝¹ → c • x ∈ carrier✝¹
add_mem'✝¹ : ∀ ⦃x : E⦄, x ∈ carrier✝¹ → ∀ ⦃y : E⦄, y ∈ carrier✝¹ → x + y ∈ carrier✝¹
carrier✝ : Set E
smul_mem'✝ : ∀ ⦃c : 𝕜⦄, 0 < c → ∀ ⦃x : E⦄, x ∈ carrier✝ → c • x ∈ carrier✝
add_mem'✝ : ∀ ⦃x : E⦄, x ∈ carrier✝ → ∀ ⦃y : E⦄, y ∈ carrier✝ → x + y ∈ carrier✝
h :
  { carrier := carrier✝¹, smul_mem' := smul_mem'✝¹, add_mem' := add_mem'✝¹ }.carrier =
    { carrier := carrier✝, smul_mem' := smul_mem'✝, add_mem' := add_mem'✝ }.carrier
⊢ { carrier := carrier✝¹, smul_mem' := smul_mem'✝¹, add_mem' := add_mem'✝¹ } =
    { carrier := carrier✝, smul_mem' := smul_mem'✝, add_mem' := add_mem'✝ }
[PROOFSTEP]
congr
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
S T : ConvexCone 𝕜 E
ι : Sort u_5
f : ι → ConvexCone 𝕜 E
⊢ ↑(iInf f) = ⋂ (i : ι), ↑(f i)
[PROOFSTEP]
simp [iInf]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
S T : ConvexCone 𝕜 E
ι : Sort u_5
x : E
f : ι → ConvexCone 𝕜 E
⊢ (∀ (i : ConvexCone 𝕜 E), i ∈ Set.range f → x ∈ ↑i) ↔ ∀ (i : ι), x ∈ f i
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : LinearOrderedField 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : AddCommMonoid G
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : Module 𝕜 G
f : E →ₗ[𝕜] F
S : ConvexCone 𝕜 F
c : 𝕜
hc : 0 < c
x : E
hx : x ∈ ↑f ⁻¹' ↑S
⊢ c • x ∈ ↑f ⁻¹' ↑S
[PROOFSTEP]
rw [mem_preimage, f.map_smul c]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : LinearOrderedField 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : AddCommMonoid G
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : Module 𝕜 G
f : E →ₗ[𝕜] F
S : ConvexCone 𝕜 F
c : 𝕜
hc : 0 < c
x : E
hx : x ∈ ↑f ⁻¹' ↑S
⊢ c • ↑f x ∈ ↑S
[PROOFSTEP]
exact S.smul_mem hc hx
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : LinearOrderedField 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : AddCommMonoid G
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : Module 𝕜 G
f : E →ₗ[𝕜] F
S : ConvexCone 𝕜 F
x : E
hx : x ∈ ↑f ⁻¹' ↑S
y : E
hy : y ∈ ↑f ⁻¹' ↑S
⊢ x + y ∈ ↑f ⁻¹' ↑S
[PROOFSTEP]
rw [mem_preimage, f.map_add]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : LinearOrderedField 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : AddCommMonoid G
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : Module 𝕜 G
f : E →ₗ[𝕜] F
S : ConvexCone 𝕜 F
x : E
hx : x ∈ ↑f ⁻¹' ↑S
y : E
hy : y ∈ ↑f ⁻¹' ↑S
⊢ ↑f x + ↑f y ∈ ↑S
[PROOFSTEP]
exact S.add_mem hx hy
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : LinearOrderedField 𝕜
inst✝¹ : OrderedAddCommGroup E
inst✝ : Module 𝕜 E
S : ConvexCone 𝕜 E
h : ∀ (x y : E), x ≤ y ↔ y - x ∈ S
⊢ ∀ ⦃a b : E⦄ ⦃c : 𝕜⦄, a < b → 0 < c → c • a ≤ c • b
[PROOFSTEP]
intro x y z xy hz
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : LinearOrderedField 𝕜
inst✝¹ : OrderedAddCommGroup E
inst✝ : Module 𝕜 E
S : ConvexCone 𝕜 E
h : ∀ (x y : E), x ≤ y ↔ y - x ∈ S
x y : E
z : 𝕜
xy : x < y
hz : 0 < z
⊢ z • x ≤ z • y
[PROOFSTEP]
rw [h (z • x) (z • y), ← smul_sub z y x]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : LinearOrderedField 𝕜
inst✝¹ : OrderedAddCommGroup E
inst✝ : Module 𝕜 E
S : ConvexCone 𝕜 E
h : ∀ (x y : E), x ≤ y ↔ y - x ∈ S
x y : E
z : 𝕜
xy : x < y
hz : 0 < z
⊢ z • (y - x) ∈ S
[PROOFSTEP]
exact smul_mem S hz ((h x y).mp xy.le)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
S✝ S : ConvexCone 𝕜 E
⊢ Blunt S ↔ ¬Pointed S
[PROOFSTEP]
rw [pointed_iff_not_blunt, Classical.not_not]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
S✝ S : ConvexCone 𝕜 E
⊢ Salient S ↔ ¬Flat S
[PROOFSTEP]
simp [Salient, Flat]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
S✝ S : ConvexCone 𝕜 E
hS : Flat S
⊢ Pointed S
[PROOFSTEP]
obtain ⟨x, hx, _, hxneg⟩ := hS
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
S✝ S : ConvexCone 𝕜 E
x : E
hx : x ∈ S
left✝ : x ≠ 0
hxneg : -x ∈ S
⊢ Pointed S
[PROOFSTEP]
rw [Pointed, ← add_neg_self x]
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
S✝ S : ConvexCone 𝕜 E
x : E
hx : x ∈ S
left✝ : x ≠ 0
hxneg : -x ∈ S
⊢ x + -x ∈ S
[PROOFSTEP]
exact add_mem S hx hxneg
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
S✝ S : ConvexCone 𝕜 E
⊢ Blunt S → Salient S
[PROOFSTEP]
rw [salient_iff_not_flat, blunt_iff_not_pointed]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
S✝ S : ConvexCone 𝕜 E
⊢ ¬Pointed S → ¬Flat S
[PROOFSTEP]
exact mt Flat.pointed
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
S : ConvexCone 𝕜 E
h₁ : Pointed S
x : E
⊢ x ≤ x
[PROOFSTEP]
change x - x ∈ S
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
S : ConvexCone 𝕜 E
h₁ : Pointed S
x : E
⊢ x - x ∈ S
[PROOFSTEP]
rw [sub_self x]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
S : ConvexCone 𝕜 E
h₁ : Pointed S
x : E
⊢ 0 ∈ S
[PROOFSTEP]
exact h₁
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
S : ConvexCone 𝕜 E
h₁ : Pointed S
x y z : E
xy : x ≤ y
zy : y ≤ z
⊢ x ≤ z
[PROOFSTEP]
simpa using add_mem S zy xy
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
S : ConvexCone 𝕜 E
h₁ : Pointed S
h₂ : Salient S
src✝ : Preorder E := toPreorder S h₁
⊢ ∀ (a b : E), a ≤ b → b ≤ a → a = b
[PROOFSTEP]
intro a b ab ba
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
S : ConvexCone 𝕜 E
h₁ : Pointed S
h₂ : Salient S
src✝ : Preorder E := toPreorder S h₁
a b : E
ab : a ≤ b
ba : b ≤ a
⊢ a = b
[PROOFSTEP]
by_contra h
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
S : ConvexCone 𝕜 E
h₁ : Pointed S
h₂ : Salient S
src✝ : Preorder E := toPreorder S h₁
a b : E
ab : a ≤ b
ba : b ≤ a
h : ¬a = b
⊢ False
[PROOFSTEP]
have h' : b - a ≠ 0 := fun h'' => h (eq_of_sub_eq_zero h'').symm
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
S : ConvexCone 𝕜 E
h₁ : Pointed S
h₂ : Salient S
src✝ : Preorder E := toPreorder S h₁
a b : E
ab : a ≤ b
ba : b ≤ a
h : ¬a = b
h' : b - a ≠ 0
⊢ False
[PROOFSTEP]
have H := h₂ (b - a) ab h'
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
S : ConvexCone 𝕜 E
h₁ : Pointed S
h₂ : Salient S
src✝ : Preorder E := toPreorder S h₁
a b : E
ab : a ≤ b
ba : b ≤ a
h : ¬a = b
h' : b - a ≠ 0
H : ¬-(b - a) ∈ S
⊢ False
[PROOFSTEP]
rw [neg_sub b a] at H
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
S : ConvexCone 𝕜 E
h₁ : Pointed S
h₂ : Salient S
src✝ : Preorder E := toPreorder S h₁
a b : E
ab : a ≤ b
ba : b ≤ a
h : ¬a = b
h' : b - a ≠ 0
H : ¬a - b ∈ S
⊢ False
[PROOFSTEP]
exact H ba
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
S : ConvexCone 𝕜 E
h₁ : Pointed S
h₂ : Salient S
src✝ : PartialOrder E := toPartialOrder S h₁ h₂
⊢ AddCommGroup E
[PROOFSTEP]
infer_instance
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
S : ConvexCone 𝕜 E
h₁ : Pointed S
h₂ : Salient S
src✝¹ : PartialOrder E := toPartialOrder S h₁ h₂
src✝ : AddCommGroup E :=
  let_fun this := inferInstance;
  this
⊢ ∀ (a b : E), a ≤ b → ∀ (c : E), c + a ≤ c + b
[PROOFSTEP]
intro a b hab c
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
S : ConvexCone 𝕜 E
h₁ : Pointed S
h₂ : Salient S
src✝¹ : PartialOrder E := toPartialOrder S h₁ h₂
src✝ : AddCommGroup E :=
  let_fun this := inferInstance;
  this
a b : E
hab : a ≤ b
c : E
⊢ c + a ≤ c + b
[PROOFSTEP]
change c + b - (c + a) ∈ S
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
S : ConvexCone 𝕜 E
h₁ : Pointed S
h₂ : Salient S
src✝¹ : PartialOrder E := toPartialOrder S h₁ h₂
src✝ : AddCommGroup E :=
  let_fun this := inferInstance;
  this
a b : E
hab : a ≤ b
c : E
⊢ c + b - (c + a) ∈ S
[PROOFSTEP]
rw [add_sub_add_left_eq_sub]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
S : ConvexCone 𝕜 E
h₁ : Pointed S
h₂ : Salient S
src✝¹ : PartialOrder E := toPartialOrder S h₁ h₂
src✝ : AddCommGroup E :=
  let_fun this := inferInstance;
  this
a b : E
hab : a ≤ b
c : E
⊢ b - a ∈ S
[PROOFSTEP]
exact hab
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x✝¹ : 𝕜
x✝ : 0 < x✝¹
⊢ ∀ ⦃x : E⦄, x ∈ 0 → x✝¹ • x ∈ 0
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x✝ : E
⊢ x✝ ∈ 0 → ∀ ⦃y : E⦄, y ∈ 0 → x✝ + y ∈ 0
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
⊢ Pointed 0
[PROOFSTEP]
rw [Pointed, mem_zero]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
K₁ K₂ : ConvexCone 𝕜 E
⊢ ∀ ⦃c : 𝕜⦄,
    0 < c → ∀ ⦃x : E⦄, x ∈ {z | ∃ x y, x ∈ K₁ ∧ y ∈ K₂ ∧ x + y = z} → c • x ∈ {z | ∃ x y, x ∈ K₁ ∧ y ∈ K₂ ∧ x + y = z}
[PROOFSTEP]
rintro c hc _ ⟨x, y, hx, hy, rfl⟩
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
K₁ K₂ : ConvexCone 𝕜 E
c : 𝕜
hc : 0 < c
x y : E
hx : x ∈ K₁
hy : y ∈ K₂
⊢ c • (x + y) ∈ {z | ∃ x y, x ∈ K₁ ∧ y ∈ K₂ ∧ x + y = z}
[PROOFSTEP]
rw [smul_add]
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
K₁ K₂ : ConvexCone 𝕜 E
c : 𝕜
hc : 0 < c
x y : E
hx : x ∈ K₁
hy : y ∈ K₂
⊢ c • x + c • y ∈ {z | ∃ x y, x ∈ K₁ ∧ y ∈ K₂ ∧ x + y = z}
[PROOFSTEP]
use c • x, c • y, K₁.smul_mem hc hx, K₂.smul_mem hc hy
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
K₁ K₂ : ConvexCone 𝕜 E
⊢ ∀ ⦃x : E⦄,
    x ∈ {z | ∃ x y, x ∈ K₁ ∧ y ∈ K₂ ∧ x + y = z} →
      ∀ ⦃y : E⦄, y ∈ {z | ∃ x y, x ∈ K₁ ∧ y ∈ K₂ ∧ x + y = z} → x + y ∈ {z | ∃ x y, x ∈ K₁ ∧ y ∈ K₂ ∧ x + y = z}
[PROOFSTEP]
rintro _ ⟨x₁, x₂, hx₁, hx₂, rfl⟩ y ⟨y₁, y₂, hy₁, hy₂, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
K₁ K₂ : ConvexCone 𝕜 E
x₁ x₂ : E
hx₁ : x₁ ∈ K₁
hx₂ : x₂ ∈ K₂
y₁ y₂ : E
hy₁ : y₁ ∈ K₁
hy₂ : y₂ ∈ K₂
⊢ x₁ + x₂ + (y₁ + y₂) ∈ {z | ∃ x y, x ∈ K₁ ∧ y ∈ K₂ ∧ x + y = z}
[PROOFSTEP]
use x₁ + y₁, x₂ + y₂, K₁.add_mem hx₁ hy₁, K₂.add_mem hx₂ hy₂
[GOAL]
case right
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
K₁ K₂ : ConvexCone 𝕜 E
x₁ x₂ : E
hx₁ : x₁ ∈ K₁
hx₂ : x₂ ∈ K₂
y₁ y₂ : E
hy₁ : y₁ ∈ K₁
hy₂ : y₂ ∈ K₂
⊢ x₁ + y₁ + (x₂ + y₂) = x₁ + x₂ + (y₁ + y₂)
[PROOFSTEP]
abel
[GOAL]
case right
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
K₁ K₂ : ConvexCone 𝕜 E
x₁ x₂ : E
hx₁ : x₁ ∈ K₁
hx₂ : x₂ ∈ K₂
y₁ y₂ : E
hy₁ : y₁ ∈ K₁
hy₂ : y₂ ∈ K₂
⊢ x₁ + y₁ + (x₂ + y₂) = x₁ + x₂ + (y₁ + y₂)
[PROOFSTEP]
abel
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x✝ : ConvexCone 𝕜 E
⊢ 0 + x✝ = x✝
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x✝¹ : ConvexCone 𝕜 E
x✝ : E
⊢ x✝ ∈ 0 + x✝¹ ↔ x✝ ∈ x✝¹
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x✝ : ConvexCone 𝕜 E
⊢ x✝ + 0 = x✝
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x✝¹ : ConvexCone 𝕜 E
x✝ : E
⊢ x✝ ∈ x✝¹ + 0 ↔ x✝ ∈ x✝¹
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
⊢ ConvexCone 𝕜 E
[PROOFSTEP]
apply ConvexCone.mk (⋃ (c : 𝕜) (_ : 0 < c), c • s)
[GOAL]
case smul_mem'
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
⊢ ∀ ⦃c : 𝕜⦄, 0 < c → ∀ ⦃x : E⦄, x ∈ ⋃ (c : 𝕜) (_ : 0 < c), c • s → c • x ∈ ⋃ (c : 𝕜) (_ : 0 < c), c • s
[PROOFSTEP]
simp only [mem_iUnion, mem_smul_set]
[GOAL]
case add_mem'
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
⊢ ∀ ⦃x : E⦄,
    x ∈ ⋃ (c : 𝕜) (_ : 0 < c), c • s →
      ∀ ⦃y : E⦄, y ∈ ⋃ (c : 𝕜) (_ : 0 < c), c • s → x + y ∈ ⋃ (c : 𝕜) (_ : 0 < c), c • s
[PROOFSTEP]
simp only [mem_iUnion, mem_smul_set]
[GOAL]
case smul_mem'
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
⊢ ∀ ⦃c : 𝕜⦄, 0 < c → ∀ ⦃x : E⦄, (∃ i h y, y ∈ s ∧ i • y = x) → ∃ i h y, y ∈ s ∧ i • y = c • x
[PROOFSTEP]
rintro c c_pos _ ⟨c', c'_pos, x, hx, rfl⟩
[GOAL]
case smul_mem'.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
c : 𝕜
c_pos : 0 < c
c' : 𝕜
c'_pos : 0 < c'
x : E
hx : x ∈ s
⊢ ∃ i h y, y ∈ s ∧ i • y = c • c' • x
[PROOFSTEP]
exact ⟨c * c', mul_pos c_pos c'_pos, x, hx, (smul_smul _ _ _).symm⟩
[GOAL]
case add_mem'
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
⊢ ∀ ⦃x : E⦄,
    (∃ i h y, y ∈ s ∧ i • y = x) → ∀ ⦃y : E⦄, (∃ i h y_1, y_1 ∈ s ∧ i • y_1 = y) → ∃ i h y_1, y_1 ∈ s ∧ i • y_1 = x + y
[PROOFSTEP]
rintro _ ⟨cx, cx_pos, x, hx, rfl⟩ _ ⟨cy, cy_pos, y, hy, rfl⟩
[GOAL]
case add_mem'.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
cx : 𝕜
cx_pos : 0 < cx
x : E
hx : x ∈ s
cy : 𝕜
cy_pos : 0 < cy
y : E
hy : y ∈ s
⊢ ∃ i h y_1, y_1 ∈ s ∧ i • y_1 = cx • x + cy • y
[PROOFSTEP]
have : 0 < cx + cy := add_pos cx_pos cy_pos
[GOAL]
case add_mem'.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
cx : 𝕜
cx_pos : 0 < cx
x : E
hx : x ∈ s
cy : 𝕜
cy_pos : 0 < cy
y : E
hy : y ∈ s
this : 0 < cx + cy
⊢ ∃ i h y_1, y_1 ∈ s ∧ i • y_1 = cx • x + cy • y
[PROOFSTEP]
refine' ⟨_, this, _, convex_iff_div.1 hs hx hy cx_pos.le cy_pos.le this, _⟩
[GOAL]
case add_mem'.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
cx : 𝕜
cx_pos : 0 < cx
x : E
hx : x ∈ s
cy : 𝕜
cy_pos : 0 < cy
y : E
hy : y ∈ s
this : 0 < cx + cy
⊢ (cx + cy) • ((cx / (cx + cy)) • x + (cy / (cx + cy)) • y) = cx • x + cy • y
[PROOFSTEP]
simp only [smul_add, smul_smul, mul_div_assoc', mul_div_cancel_left _ this.ne']
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
⊢ x ∈ toCone s hs ↔ ∃ c, 0 < c ∧ ∃ y, y ∈ s ∧ c • y = x
[PROOFSTEP]
simp only [toCone, ConvexCone.mem_mk, mem_iUnion, mem_smul_set, eq_comm, exists_prop]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
⊢ x ∈ toCone s hs ↔ ∃ c, 0 < c ∧ c • x ∈ s
[PROOFSTEP]
refine' hs.mem_toCone.trans ⟨_, _⟩
[GOAL]
case refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
⊢ (∃ c, 0 < c ∧ ∃ y, y ∈ s ∧ c • y = x) → ∃ c, 0 < c ∧ c • x ∈ s
[PROOFSTEP]
rintro ⟨c, hc, y, hy, rfl⟩
[GOAL]
case refine'_1.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
c : 𝕜
hc : 0 < c
y : E
hy : y ∈ s
⊢ ∃ c_1, 0 < c_1 ∧ c_1 • c • y ∈ s
[PROOFSTEP]
exact ⟨c⁻¹, inv_pos.2 hc, by rwa [smul_smul, inv_mul_cancel hc.ne', one_smul]⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
c : 𝕜
hc : 0 < c
y : E
hy : y ∈ s
⊢ c⁻¹ • c • y ∈ s
[PROOFSTEP]
rwa [smul_smul, inv_mul_cancel hc.ne', one_smul]
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
⊢ (∃ c, 0 < c ∧ c • x ∈ s) → ∃ c, 0 < c ∧ ∃ y, y ∈ s ∧ c • y = x
[PROOFSTEP]
rintro ⟨c, hc, hcx⟩
[GOAL]
case refine'_2.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
c : 𝕜
hc : 0 < c
hcx : c • x ∈ s
⊢ ∃ c, 0 < c ∧ ∃ y, y ∈ s ∧ c • y = x
[PROOFSTEP]
exact ⟨c⁻¹, inv_pos.2 hc, _, hcx, by rw [smul_smul, inv_mul_cancel hc.ne', one_smul]⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
c : 𝕜
hc : 0 < c
hcx : c • x ∈ s
⊢ c⁻¹ • c • x = x
[PROOFSTEP]
rw [smul_smul, inv_mul_cancel hc.ne', one_smul]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x✝ x : E
hx : x ∈ s
⊢ 1 • x ∈ s
[PROOFSTEP]
rwa [one_smul]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
⊢ IsLeast {t | s ⊆ ↑t} (toCone s hs)
[PROOFSTEP]
refine' ⟨hs.subset_toCone, fun t ht x hx => _⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x✝ : E
t : ConvexCone 𝕜 E
ht : t ∈ {t | s ⊆ ↑t}
x : E
hx : x ∈ toCone s hs
⊢ x ∈ t
[PROOFSTEP]
rcases hs.mem_toCone.1 hx with ⟨c, hc, y, hy, rfl⟩
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
t : ConvexCone 𝕜 E
ht : t ∈ {t | s ⊆ ↑t}
c : 𝕜
hc : 0 < c
y : E
hy : y ∈ s
hx : c • y ∈ toCone s hs
⊢ c • y ∈ t
[PROOFSTEP]
exact t.smul_mem hc (ht hy)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ IsLeast {t | s ⊆ ↑t} (Convex.toCone (↑(convexHull 𝕜) s) (_ : Convex 𝕜 (↑(convexHull 𝕜) s)))
[PROOFSTEP]
convert (convex_convexHull 𝕜 s).toCone_isLeast using 1
[GOAL]
case h.e'_3
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ {t | s ⊆ ↑t} = {t | ↑(convexHull 𝕜) s ⊆ ↑t}
[PROOFSTEP]
ext t
[GOAL]
case h.e'_3.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
t : ConvexCone 𝕜 E
⊢ t ∈ {t | s ⊆ ↑t} ↔ t ∈ {t | ↑(convexHull 𝕜) s ⊆ ↑t}
[PROOFSTEP]
exact ⟨fun h => convexHull_min h t.convex, (subset_convexHull 𝕜 s).trans⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
obtain ⟨y, -, hy⟩ : ∃ y ∈ ⊤, y ∉ f.domain := @SetLike.exists_of_lt (Submodule ℝ E) _ _ _ _ (lt_top_iff_ne_top.2 hdom)
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
obtain ⟨c, le_c, c_le⟩ :
  ∃ c, (∀ x : f.domain, -(x : E) - y ∈ s → f x ≤ c) ∧ ∀ x : f.domain, (x : E) + y ∈ s → c ≤ f x :=
  by
  set Sp := f '' {x : f.domain | (x : E) + y ∈ s}
  set Sn := f '' {x : f.domain | -(x : E) - y ∈ s}
  suffices (upperBounds Sn ∩ lowerBounds Sp).Nonempty by
    simpa only [Set.Nonempty, upperBounds, lowerBounds, ball_image_iff] using this
  refine' exists_between_of_forall_le (Nonempty.image f _) (Nonempty.image f (dense y)) _
  · rcases dense (-y) with ⟨x, hx⟩
    rw [← neg_neg x, AddSubgroupClass.coe_neg, ← sub_eq_add_neg] at hx
    exact ⟨_, hx⟩
  rintro a ⟨xn, hxn, rfl⟩ b ⟨xp, hxp, rfl⟩
  have := s.add_mem hxp hxn
  rw [add_assoc, add_sub_cancel'_right, ← sub_eq_add_neg, ← AddSubgroupClass.coe_sub] at this
  replace := nonneg _ this
  rwa [f.map_sub, sub_nonneg] at this
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
set Sp := f '' {x : f.domain | (x : E) + y ∈ s}
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
set Sn := f '' {x : f.domain | -(x : E) - y ∈ s}
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
suffices (upperBounds Sn ∩ lowerBounds Sp).Nonempty by
  simpa only [Set.Nonempty, upperBounds, lowerBounds, ball_image_iff] using this
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
simpa only [Set.Nonempty, upperBounds, lowerBounds, ball_image_iff] using this
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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)
[PROOFSTEP]
refine' exists_between_of_forall_le (Nonempty.image f _) (Nonempty.image f (dense y)) _
[GOAL]
case refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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}
[PROOFSTEP]
rcases dense (-y) with ⟨x, hx⟩
[GOAL]
case refine'_1.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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}
[PROOFSTEP]
rw [← neg_neg x, AddSubgroupClass.coe_neg, ← sub_eq_add_neg] at hx
[GOAL]
case refine'_1.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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}
[PROOFSTEP]
exact ⟨_, hx⟩
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
rintro a ⟨xn, hxn, rfl⟩ b ⟨xp, hxp, rfl⟩
[GOAL]
case refine'_2.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
have := s.add_mem hxp hxn
[GOAL]
case refine'_2.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
rw [add_assoc, add_sub_cancel'_right, ← sub_eq_add_neg, ← AddSubgroupClass.coe_sub] at this
[GOAL]
case refine'_2.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
replace := nonneg _ this
[GOAL]
case refine'_2.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
rwa [f.map_sub, sub_nonneg] at this
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
refine' ⟨f.supSpanSingleton y (-c) hy, _, _⟩
[GOAL]
case intro.intro.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
refine' lt_iff_le_not_le.2 ⟨f.left_le_sup _ _, fun H => _⟩
[GOAL]
case intro.intro.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
replace H := LinearPMap.domain_mono.monotone H
[GOAL]
case intro.intro.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
rw [LinearPMap.domain_supSpanSingleton, sup_le_iff, span_le, singleton_subset_iff] at H
[GOAL]
case intro.intro.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
exact hy H.2
[GOAL]
case intro.intro.intro.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
rintro ⟨z, hz⟩ hzs
[GOAL]
case intro.intro.intro.intro.refine'_2.mk
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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 }
[PROOFSTEP]
rcases mem_sup.1 hz with ⟨x, hx, y', hy', rfl⟩
[GOAL]
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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 }
[PROOFSTEP]
rcases mem_span_singleton.1 hy' with ⟨r, rfl⟩
[GOAL]
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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 }
[PROOFSTEP]
simp only [Subtype.coe_mk] at hzs
[GOAL]
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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 }
[PROOFSTEP]
erw [LinearPMap.supSpanSingleton_apply_mk _ _ _ _ _ hx, smul_neg, ← sub_eq_add_neg, sub_nonneg]
[GOAL]
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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 }
[PROOFSTEP]
rcases lt_trichotomy r 0 with (hr | hr | hr)
[GOAL]
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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 }
[PROOFSTEP]
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]
    -- Porting note: added type annotation and `by exact`
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
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]
  -- Porting note: added type annotation and `by exact`
[GOAL]
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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 }
[PROOFSTEP]
replace : f (r⁻¹ • ⟨x, hx⟩) ≤ c := le_c (r⁻¹ • ⟨x, hx⟩) (by exact this)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
exact this
[GOAL]
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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 }
[PROOFSTEP]
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
[GOAL]
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro.inr.inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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 }
[PROOFSTEP]
subst r
[GOAL]
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro.inr.inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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 }
[PROOFSTEP]
simp only [zero_smul, add_zero] at hzs ⊢
[GOAL]
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro.inr.inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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 }
[PROOFSTEP]
apply nonneg
[GOAL]
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro.inr.inl.a
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
exact hzs
[GOAL]
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro.inr.inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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 }
[PROOFSTEP]
have : r⁻¹ • x + y ∈ s := by
  rwa [← s.smul_mem_iff hr, smul_add, smul_smul, mul_inv_cancel hr.ne', one_smul]
    -- Porting note: added type annotation and `by exact`
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
rwa [← s.smul_mem_iff hr, smul_add, smul_smul, mul_inv_cancel hr.ne', one_smul]
  -- Porting note: added type annotation and `by exact`
[GOAL]
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro.inr.inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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 }
[PROOFSTEP]
replace : c ≤ f (r⁻¹ • ⟨x, hx⟩) := c_le (r⁻¹ • ⟨x, hx⟩) (by exact this)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
exact this
[GOAL]
case intro.intro.intro.intro.refine'_2.mk.intro.intro.intro.intro.intro.inr.inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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 }
[PROOFSTEP]
rwa [← mul_le_mul_left hr, f.map_smul, smul_eq_mul, ← mul_assoc, mul_inv_cancel hr.ne', one_mul] at this
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
⊢ ∃ q, q ≥ p ∧ q.domain = ⊤ ∧ ∀ (x : { x // x ∈ q.domain }), ↑x ∈ s → 0 ≤ ↑q x
[PROOFSTEP]
set S := {p : E →ₗ.[ℝ] ℝ | ∀ x : p.domain, (x : E) ∈ s → 0 ≤ p x}
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
⊢ ∃ q, q ≥ p ∧ q.domain = ⊤ ∧ ∀ (x : { x // x ∈ q.domain }), ↑x ∈ s → 0 ≤ ↑q x
[PROOFSTEP]
have hSc : ∀ c, c ⊆ S → IsChain (· ≤ ·) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
[GOAL]
case hSc
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
⊢ ∀ (c : Set (E →ₗ.[ℝ] ℝ)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : E →ₗ.[ℝ] ℝ), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : E →ₗ.[ℝ] ℝ), z ∈ c → z ≤ ub
[PROOFSTEP]
intro c hcs c_chain y hy
[GOAL]
case hSc
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x x_1 => x ≤ x_1) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
⊢ ∃ ub, ub ∈ S ∧ ∀ (z : E →ₗ.[ℝ] ℝ), z ∈ c → z ≤ ub
[PROOFSTEP]
clear hp_nonneg hp_dense p
[GOAL]
case hSc
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x x_1 => x ≤ x_1) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
⊢ ∃ ub, ub ∈ S ∧ ∀ (z : E →ₗ.[ℝ] ℝ), z ∈ c → z ≤ ub
[PROOFSTEP]
have cne : c.Nonempty := ⟨y, hy⟩
[GOAL]
case hSc
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x x_1 => x ≤ x_1) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : Set.Nonempty c
⊢ ∃ ub, ub ∈ S ∧ ∀ (z : E →ₗ.[ℝ] ℝ), z ∈ c → z ≤ ub
[PROOFSTEP]
have hcd : DirectedOn (· ≤ ·) c := c_chain.directedOn
[GOAL]
case hSc
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x x_1 => x ≤ x_1) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : Set.Nonempty c
hcd : DirectedOn (fun x x_1 => x ≤ x_1) c
⊢ ∃ ub, ub ∈ S ∧ ∀ (z : E →ₗ.[ℝ] ℝ), z ∈ c → z ≤ ub
[PROOFSTEP]
refine' ⟨LinearPMap.sSup c hcd, _, fun _ ↦ LinearPMap.le_sSup hcd⟩
[GOAL]
case hSc
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x x_1 => x ≤ x_1) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : Set.Nonempty c
hcd : DirectedOn (fun x x_1 => x ≤ x_1) c
⊢ LinearPMap.sSup c hcd ∈ S
[PROOFSTEP]
rintro ⟨x, hx⟩ hxs
[GOAL]
case hSc.mk
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x x_1 => x ≤ x_1) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : Set.Nonempty c
hcd : DirectedOn (fun x x_1 => x ≤ x_1) c
x : E
hx : x ∈ (LinearPMap.sSup c hcd).domain
hxs : ↑{ val := x, property := hx } ∈ s
⊢ 0 ≤ ↑(LinearPMap.sSup c hcd) { val := x, property := hx }
[PROOFSTEP]
have hdir : DirectedOn (· ≤ ·) (LinearPMap.domain '' c) :=
  directedOn_image.2 (hcd.mono fun h ↦ LinearPMap.domain_mono.monotone h)
[GOAL]
case hSc.mk
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x x_1 => x ≤ x_1) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : Set.Nonempty c
hcd : DirectedOn (fun x x_1 => x ≤ x_1) c
x : E
hx : x ∈ (LinearPMap.sSup c hcd).domain
hxs : ↑{ val := x, property := hx } ∈ s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) (LinearPMap.domain '' c)
⊢ 0 ≤ ↑(LinearPMap.sSup c hcd) { val := x, property := hx }
[PROOFSTEP]
rcases(mem_sSup_of_directed (cne.image _) hdir).1 hx with ⟨_, ⟨f, hfc, rfl⟩, hfx⟩
[GOAL]
case hSc.mk.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f✝ : E →ₗ.[ℝ] ℝ
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x x_1 => x ≤ x_1) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : Set.Nonempty c
hcd : DirectedOn (fun x x_1 => x ≤ x_1) c
x : E
hx : x ∈ (LinearPMap.sSup c hcd).domain
hxs : ↑{ val := x, property := hx } ∈ s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) (LinearPMap.domain '' c)
f : E →ₗ.[ℝ] ℝ
hfc : f ∈ c
hfx : x ∈ f.domain
⊢ 0 ≤ ↑(LinearPMap.sSup c hcd) { val := x, property := hx }
[PROOFSTEP]
have : f ≤ LinearPMap.sSup c hcd := LinearPMap.le_sSup _ hfc
[GOAL]
case hSc.mk.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f✝ : E →ₗ.[ℝ] ℝ
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x x_1 => x ≤ x_1) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : Set.Nonempty c
hcd : DirectedOn (fun x x_1 => x ≤ x_1) c
x : E
hx : x ∈ (LinearPMap.sSup c hcd).domain
hxs : ↑{ val := x, property := hx } ∈ s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) (LinearPMap.domain '' c)
f : E →ₗ.[ℝ] ℝ
hfc : f ∈ c
hfx : x ∈ f.domain
this : f ≤ LinearPMap.sSup c hcd
⊢ 0 ≤ ↑(LinearPMap.sSup c hcd) { val := x, property := hx }
[PROOFSTEP]
convert ← hcs hfc ⟨x, hfx⟩ hxs using 1
[GOAL]
case h.e'_4
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f✝ : E →ₗ.[ℝ] ℝ
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x x_1 => x ≤ x_1) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : Set.Nonempty c
hcd : DirectedOn (fun x x_1 => x ≤ x_1) c
x : E
hx : x ∈ (LinearPMap.sSup c hcd).domain
hxs : ↑{ val := x, property := hx } ∈ s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) (LinearPMap.domain '' c)
f : E →ₗ.[ℝ] ℝ
hfc : f ∈ c
hfx : x ∈ f.domain
this : f ≤ LinearPMap.sSup c hcd
⊢ ↑f { val := x, property := hfx } = ↑(LinearPMap.sSup c hcd) { val := x, property := hx }
[PROOFSTEP]
exact this.2 rfl
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
hSc :
  ∀ (c : Set (E →ₗ.[ℝ] ℝ)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : E →ₗ.[ℝ] ℝ), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : E →ₗ.[ℝ] ℝ), z ∈ c → z ≤ ub
⊢ ∃ q, q ≥ p ∧ q.domain = ⊤ ∧ ∀ (x : { x // x ∈ q.domain }), ↑x ∈ s → 0 ≤ ↑q x
[PROOFSTEP]
obtain ⟨q, hqs, hpq, hq⟩ := zorn_nonempty_partialOrder₀ S hSc p hp_nonneg
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
hSc :
  ∀ (c : Set (E →ₗ.[ℝ] ℝ)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : E →ₗ.[ℝ] ℝ), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : E →ₗ.[ℝ] ℝ), z ∈ c → z ≤ ub
q : E →ₗ.[ℝ] ℝ
hqs : q ∈ S
hpq : p ≤ q
hq : ∀ (z : E →ₗ.[ℝ] ℝ), z ∈ S → q ≤ z → z = q
⊢ ∃ q, q ≥ p ∧ q.domain = ⊤ ∧ ∀ (x : { x // x ∈ q.domain }), ↑x ∈ s → 0 ≤ ↑q x
[PROOFSTEP]
refine' ⟨q, hpq, _, hqs⟩
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
hSc :
  ∀ (c : Set (E →ₗ.[ℝ] ℝ)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : E →ₗ.[ℝ] ℝ), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : E →ₗ.[ℝ] ℝ), z ∈ c → z ≤ ub
q : E →ₗ.[ℝ] ℝ
hqs : q ∈ S
hpq : p ≤ q
hq : ∀ (z : E →ₗ.[ℝ] ℝ), z ∈ S → q ≤ z → z = q
⊢ q.domain = ⊤
[PROOFSTEP]
contrapose! hq
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
hSc :
  ∀ (c : Set (E →ₗ.[ℝ] ℝ)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : E →ₗ.[ℝ] ℝ), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : E →ₗ.[ℝ] ℝ), z ∈ c → z ≤ ub
q : E →ₗ.[ℝ] ℝ
hqs : q ∈ S
hpq : p ≤ q
hq : q.domain ≠ ⊤
⊢ ∃ z, z ∈ {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x} ∧ q ≤ z ∧ z ≠ q
[PROOFSTEP]
have hqd : ∀ y, ∃ x : q.domain, (x : E) + y ∈ s := fun y ↦
  let ⟨x, hx⟩ := hp_dense y
  ⟨ofLe hpq.left x, hx⟩
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
hSc :
  ∀ (c : Set (E →ₗ.[ℝ] ℝ)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : E →ₗ.[ℝ] ℝ), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : E →ₗ.[ℝ] ℝ), z ∈ c → z ≤ ub
q : E →ₗ.[ℝ] ℝ
hqs : q ∈ S
hpq : p ≤ q
hq : q.domain ≠ ⊤
hqd : ∀ (y : E), ∃ x, ↑x + y ∈ s
⊢ ∃ z, z ∈ {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x} ∧ q ≤ z ∧ z ≠ q
[PROOFSTEP]
rcases step s q hqs hqd hq with ⟨r, hqr, hr⟩
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x}
hSc :
  ∀ (c : Set (E →ₗ.[ℝ] ℝ)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : E →ₗ.[ℝ] ℝ), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : E →ₗ.[ℝ] ℝ), z ∈ c → z ≤ ub
q : E →ₗ.[ℝ] ℝ
hqs : q ∈ S
hpq : p ≤ q
hq : q.domain ≠ ⊤
hqd : ∀ (y : E), ∃ x, ↑x + y ∈ s
r : E →ₗ.[ℝ] ℝ
hqr : q < r
hr : ∀ (x : { x // x ∈ r.domain }), ↑x ∈ s → 0 ≤ ↑r x
⊢ ∃ z, z ∈ {p | ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x} ∧ q ≤ z ∧ z ≠ q
[PROOFSTEP]
exact ⟨r, hr, hqr.le, hqr.ne'⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
rcases RieszExtension.exists_top s f nonneg dense with ⟨⟨g_dom, g⟩, ⟨-, hfg⟩, rfl : g_dom = ⊤, hgs⟩
[GOAL]
case intro.mk.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
refine' ⟨g.comp (LinearMap.id.codRestrict ⊤ fun _ ↦ trivial), _, _⟩
[GOAL]
case intro.mk.intro.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
exact fun x => (hfg rfl).symm
[GOAL]
case intro.mk.intro.intro.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
exact fun x hx => hgs ⟨x, _⟩ hx
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
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) }
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
set f' := (-f).coprod (LinearMap.id.toPMap ⊤)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
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
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
simpa using le_trans (hf ⟨x.1.1, x.2.1⟩) hx
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
have hf'_dense : ∀ y : E × ℝ, ∃ x : f'.domain, ↑x + y ∈ s
[GOAL]
case hf'_dense
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
rintro ⟨x, y⟩
[GOAL]
case hf'_dense.mk
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
refine' ⟨⟨(0, N x - y), ⟨f.domain.zero_mem, trivial⟩⟩, _⟩
[GOAL]
case hf'_dense.mk
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
simp only [ConvexCone.mem_mk, mem_setOf_eq, Prod.fst_add, Prod.snd_add, zero_add, sub_add_cancel, le_rfl]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
obtain ⟨g, g_eq, g_nonneg⟩ := riesz_extension s f' hf'_nonneg hf'_dense
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
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
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
refine ⟨-g.comp (inl ℝ E ℝ), fun x ↦ ?_, fun x ↦ ?_⟩
[GOAL]
case intro.intro.refine_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
simp [g_eq x 0]
[GOAL]
case intro.intro.refine_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
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))
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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)
[PROOFSTEP]
simp [← map_sub, ← map_neg]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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)
[PROOFSTEP]
simpa using g_eq 0 (N x)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
[PROOFSTEP]
simpa using g_nonneg ⟨x, N x⟩ (le_refl (N x))


[GOAL]
x : ℂ
h : cos x ≠ 0
⊢ HasStrictDerivAt tan (↑1 / cos x ^ 2) x
[PROOFSTEP]
convert (hasStrictDerivAt_sin x).div (hasStrictDerivAt_cos x) h using 1
[GOAL]
case h.e'_7
x : ℂ
h : cos x ≠ 0
⊢ ↑1 / cos x ^ 2 = (cos x * cos x - sin x * -sin x) / cos x ^ 2
[PROOFSTEP]
rw_mod_cast [← sin_sq_add_cos_sq x]
[GOAL]
case h.e'_7
x : ℂ
h : ¬cos x = 0
⊢ (sin x ^ 2 + cos x ^ 2) / cos x ^ 2 = (cos x * cos x - sin x * -sin x) / cos x ^ 2
[PROOFSTEP]
ring
[GOAL]
x : ℂ
hx : cos x = 0
⊢ Tendsto (fun x => ↑abs (tan x)) (𝓝[{x}ᶜ] x) atTop
[PROOFSTEP]
simp only [tan_eq_sin_div_cos, ← norm_eq_abs, norm_div]
[GOAL]
x : ℂ
hx : cos x = 0
⊢ Tendsto (fun x => ‖sin x‖ / ‖cos x‖) (𝓝[{x}ᶜ] x) atTop
[PROOFSTEP]
have A : sin x ≠ 0 := fun h => by simpa [*, sq] using sin_sq_add_cos_sq x
[GOAL]
x : ℂ
hx : cos x = 0
h : sin x = 0
⊢ False
[PROOFSTEP]
simpa [*, sq] using sin_sq_add_cos_sq x
[GOAL]
x : ℂ
hx : cos x = 0
A : sin x ≠ 0
⊢ Tendsto (fun x => ‖sin x‖ / ‖cos x‖) (𝓝[{x}ᶜ] x) atTop
[PROOFSTEP]
have B : Tendsto cos (𝓝[≠] x) (𝓝[≠] 0) := hx ▸ (hasDerivAt_cos x).tendsto_punctured_nhds (neg_ne_zero.2 A)
[GOAL]
x : ℂ
hx : cos x = 0
A : sin x ≠ 0
B : Tendsto cos (𝓝[{x}ᶜ] x) (𝓝[{0}ᶜ] 0)
⊢ Tendsto (fun x => ‖sin x‖ / ‖cos x‖) (𝓝[{x}ᶜ] x) atTop
[PROOFSTEP]
exact
  continuous_sin.continuousWithinAt.norm.mul_atTop (norm_pos_iff.2 A)
    (tendsto_norm_nhdsWithin_zero.comp B).inv_tendsto_zero
[GOAL]
x : ℂ
⊢ ContinuousAt tan x ↔ cos x ≠ 0
[PROOFSTEP]
refine' ⟨fun hc h₀ => _, fun h => (hasDerivAt_tan h).continuousAt⟩
[GOAL]
x : ℂ
hc : ContinuousAt tan x
h₀ : cos x = 0
⊢ False
[PROOFSTEP]
exact not_tendsto_nhds_of_tendsto_atTop (tendsto_abs_tan_of_cos_eq_zero h₀) _ (hc.norm.tendsto.mono_left inf_le_left)
[GOAL]
x : ℂ
h : cos x = 0
⊢ deriv tan x = ↑1 / cos x ^ 2
[PROOFSTEP]
have : ¬DifferentiableAt ℂ tan x := mt differentiableAt_tan.1 (Classical.not_not.2 h)
[GOAL]
x : ℂ
h : cos x = 0
this : ¬DifferentiableAt ℂ tan x
⊢ deriv tan x = ↑1 / cos x ^ 2
[PROOFSTEP]
simp [deriv_zero_of_not_differentiableAt this, h, sq]


[GOAL]
x : ℝ
h₁ : x ≠ -1
h₂ : x ≠ 1
⊢ HasStrictDerivAt arcsin (1 / sqrt (1 - x ^ 2)) x ∧ ContDiffAt ℝ ⊤ arcsin x
[PROOFSTEP]
cases' h₁.lt_or_lt with h₁ h₁
[GOAL]
case inl
x : ℝ
h₁✝ : x ≠ -1
h₂ : x ≠ 1
h₁ : x < -1
⊢ HasStrictDerivAt arcsin (1 / sqrt (1 - x ^ 2)) x ∧ ContDiffAt ℝ ⊤ arcsin x
[PROOFSTEP]
have : 1 - x ^ 2 < 0 := by nlinarith [h₁]
[GOAL]
x : ℝ
h₁✝ : x ≠ -1
h₂ : x ≠ 1
h₁ : x < -1
⊢ 1 - x ^ 2 < 0
[PROOFSTEP]
nlinarith [h₁]
[GOAL]
case inl
x : ℝ
h₁✝ : x ≠ -1
h₂ : x ≠ 1
h₁ : x < -1
this : 1 - x ^ 2 < 0
⊢ HasStrictDerivAt arcsin (1 / sqrt (1 - x ^ 2)) x ∧ ContDiffAt ℝ ⊤ arcsin x
[PROOFSTEP]
rw [sqrt_eq_zero'.2 this.le, div_zero]
[GOAL]
case inl
x : ℝ
h₁✝ : x ≠ -1
h₂ : x ≠ 1
h₁ : x < -1
this : 1 - x ^ 2 < 0
⊢ HasStrictDerivAt arcsin 0 x ∧ ContDiffAt ℝ ⊤ arcsin x
[PROOFSTEP]
have : arcsin =ᶠ[𝓝 x] fun _ => -(π / 2) := (gt_mem_nhds h₁).mono fun y hy => arcsin_of_le_neg_one hy.le
[GOAL]
case inl
x : ℝ
h₁✝ : x ≠ -1
h₂ : x ≠ 1
h₁ : x < -1
this✝ : 1 - x ^ 2 < 0
this : arcsin =ᶠ[𝓝 x] fun x => -(π / 2)
⊢ HasStrictDerivAt arcsin 0 x ∧ ContDiffAt ℝ ⊤ arcsin x
[PROOFSTEP]
exact ⟨(hasStrictDerivAt_const _ _).congr_of_eventuallyEq this.symm, contDiffAt_const.congr_of_eventuallyEq this⟩
[GOAL]
case inr
x : ℝ
h₁✝ : x ≠ -1
h₂ : x ≠ 1
h₁ : -1 < x
⊢ HasStrictDerivAt arcsin (1 / sqrt (1 - x ^ 2)) x ∧ ContDiffAt ℝ ⊤ arcsin x
[PROOFSTEP]
cases' h₂.lt_or_lt with h₂ h₂
[GOAL]
case inr.inl
x : ℝ
h₁✝ : x ≠ -1
h₂✝ : x ≠ 1
h₁ : -1 < x
h₂ : x < 1
⊢ HasStrictDerivAt arcsin (1 / sqrt (1 - x ^ 2)) x ∧ ContDiffAt ℝ ⊤ arcsin x
[PROOFSTEP]
have : 0 < sqrt (1 - x ^ 2) := sqrt_pos.2 (by nlinarith [h₁, h₂])
[GOAL]
x : ℝ
h₁✝ : x ≠ -1
h₂✝ : x ≠ 1
h₁ : -1 < x
h₂ : x < 1
⊢ 0 < 1 - x ^ 2
[PROOFSTEP]
nlinarith [h₁, h₂]
[GOAL]
case inr.inl
x : ℝ
h₁✝ : x ≠ -1
h₂✝ : x ≠ 1
h₁ : -1 < x
h₂ : x < 1
this : 0 < sqrt (1 - x ^ 2)
⊢ HasStrictDerivAt arcsin (1 / sqrt (1 - x ^ 2)) x ∧ ContDiffAt ℝ ⊤ arcsin x
[PROOFSTEP]
simp only [← cos_arcsin, one_div] at this ⊢
[GOAL]
case inr.inl
x : ℝ
h₁✝ : x ≠ -1
h₂✝ : x ≠ 1
h₁ : -1 < x
h₂ : x < 1
this : 0 < cos (arcsin x)
⊢ HasStrictDerivAt arcsin (cos (arcsin x))⁻¹ x ∧ ContDiffAt ℝ ⊤ arcsin x
[PROOFSTEP]
exact
  ⟨sinLocalHomeomorph.hasStrictDerivAt_symm ⟨h₁, h₂⟩ this.ne' (hasStrictDerivAt_sin _),
    sinLocalHomeomorph.contDiffAt_symm_deriv this.ne' ⟨h₁, h₂⟩ (hasDerivAt_sin _) contDiff_sin.contDiffAt⟩
[GOAL]
case inr.inr
x : ℝ
h₁✝ : x ≠ -1
h₂✝ : x ≠ 1
h₁ : -1 < x
h₂ : 1 < x
⊢ HasStrictDerivAt arcsin (1 / sqrt (1 - x ^ 2)) x ∧ ContDiffAt ℝ ⊤ arcsin x
[PROOFSTEP]
have : 1 - x ^ 2 < 0 := by nlinarith [h₂]
[GOAL]
x : ℝ
h₁✝ : x ≠ -1
h₂✝ : x ≠ 1
h₁ : -1 < x
h₂ : 1 < x
⊢ 1 - x ^ 2 < 0
[PROOFSTEP]
nlinarith [h₂]
[GOAL]
case inr.inr
x : ℝ
h₁✝ : x ≠ -1
h₂✝ : x ≠ 1
h₁ : -1 < x
h₂ : 1 < x
this : 1 - x ^ 2 < 0
⊢ HasStrictDerivAt arcsin (1 / sqrt (1 - x ^ 2)) x ∧ ContDiffAt ℝ ⊤ arcsin x
[PROOFSTEP]
rw [sqrt_eq_zero'.2 this.le, div_zero]
[GOAL]
case inr.inr
x : ℝ
h₁✝ : x ≠ -1
h₂✝ : x ≠ 1
h₁ : -1 < x
h₂ : 1 < x
this : 1 - x ^ 2 < 0
⊢ HasStrictDerivAt arcsin 0 x ∧ ContDiffAt ℝ ⊤ arcsin x
[PROOFSTEP]
have : arcsin =ᶠ[𝓝 x] fun _ => π / 2 := (lt_mem_nhds h₂).mono fun y hy => arcsin_of_one_le hy.le
[GOAL]
case inr.inr
x : ℝ
h₁✝ : x ≠ -1
h₂✝ : x ≠ 1
h₁ : -1 < x
h₂ : 1 < x
this✝ : 1 - x ^ 2 < 0
this : arcsin =ᶠ[𝓝 x] fun x => π / 2
⊢ HasStrictDerivAt arcsin 0 x ∧ ContDiffAt ℝ ⊤ arcsin x
[PROOFSTEP]
exact ⟨(hasStrictDerivAt_const _ _).congr_of_eventuallyEq this.symm, contDiffAt_const.congr_of_eventuallyEq this⟩
[GOAL]
x : ℝ
h : x ≠ -1
⊢ HasDerivWithinAt arcsin (1 / sqrt (1 - x ^ 2)) (Ici x) x
[PROOFSTEP]
rcases eq_or_ne x 1 with (rfl | h')
[GOAL]
case inl
h : 1 ≠ -1
⊢ HasDerivWithinAt arcsin (1 / sqrt (1 - 1 ^ 2)) (Ici 1) 1
[PROOFSTEP]
convert (hasDerivWithinAt_const (1 : ℝ) _ (π / 2)).congr _ _
[GOAL]
case h.e'_7
h : 1 ≠ -1
⊢ 1 / sqrt (1 - 1 ^ 2) = 0
[PROOFSTEP]
simp (config := { contextual := true }) [arcsin_of_one_le]
[GOAL]
case inl.convert_3
h : 1 ≠ -1
⊢ ∀ (x : ℝ), x ∈ Ici 1 → arcsin x = π / 2
[PROOFSTEP]
simp (config := { contextual := true }) [arcsin_of_one_le]
[GOAL]
case inl.convert_4
h : 1 ≠ -1
⊢ arcsin 1 = π / 2
[PROOFSTEP]
simp (config := { contextual := true }) [arcsin_of_one_le]
[GOAL]
case inr
x : ℝ
h : x ≠ -1
h' : x ≠ 1
⊢ HasDerivWithinAt arcsin (1 / sqrt (1 - x ^ 2)) (Ici x) x
[PROOFSTEP]
exact (hasDerivAt_arcsin h h').hasDerivWithinAt
[GOAL]
x : ℝ
h : x ≠ 1
⊢ HasDerivWithinAt arcsin (1 / sqrt (1 - x ^ 2)) (Iic x) x
[PROOFSTEP]
rcases em (x = -1) with (rfl | h')
[GOAL]
case inl
h : -1 ≠ 1
⊢ HasDerivWithinAt arcsin (1 / sqrt (1 - (-1) ^ 2)) (Iic (-1)) (-1)
[PROOFSTEP]
convert (hasDerivWithinAt_const (-1 : ℝ) _ (-(π / 2))).congr _ _
[GOAL]
case h.e'_7
h : -1 ≠ 1
⊢ 1 / sqrt (1 - (-1) ^ 2) = 0
[PROOFSTEP]
simp (config := { contextual := true }) [arcsin_of_le_neg_one]
[GOAL]
case inl.convert_3
h : -1 ≠ 1
⊢ ∀ (x : ℝ), x ∈ Iic (-1) → arcsin x = -(π / 2)
[PROOFSTEP]
simp (config := { contextual := true }) [arcsin_of_le_neg_one]
[GOAL]
case inl.convert_4
h : -1 ≠ 1
⊢ arcsin (-1) = -(π / 2)
[PROOFSTEP]
simp (config := { contextual := true }) [arcsin_of_le_neg_one]
[GOAL]
case inr
x : ℝ
h : x ≠ 1
h' : ¬x = -1
⊢ HasDerivWithinAt arcsin (1 / sqrt (1 - x ^ 2)) (Iic x) x
[PROOFSTEP]
exact (hasDerivAt_arcsin h' h).hasDerivWithinAt
[GOAL]
x : ℝ
⊢ DifferentiableWithinAt ℝ arcsin (Ici x) x ↔ x ≠ -1
[PROOFSTEP]
refine' ⟨_, fun h => (hasDerivWithinAt_arcsin_Ici h).differentiableWithinAt⟩
[GOAL]
x : ℝ
⊢ DifferentiableWithinAt ℝ arcsin (Ici x) x → x ≠ -1
[PROOFSTEP]
rintro h rfl
[GOAL]
h : DifferentiableWithinAt ℝ arcsin (Ici (-1)) (-1)
⊢ False
[PROOFSTEP]
have : sin ∘ arcsin =ᶠ[𝓝[≥] (-1 : ℝ)] id := by
  filter_upwards [Icc_mem_nhdsWithin_Ici ⟨le_rfl, neg_lt_self (zero_lt_one' ℝ)⟩] with x using sin_arcsin'
[GOAL]
h : DifferentiableWithinAt ℝ arcsin (Ici (-1)) (-1)
⊢ sin ∘ arcsin =ᶠ[𝓝[Ici (-1)] (-1)] id
[PROOFSTEP]
filter_upwards [Icc_mem_nhdsWithin_Ici ⟨le_rfl, neg_lt_self (zero_lt_one' ℝ)⟩] with x using sin_arcsin'
[GOAL]
h : DifferentiableWithinAt ℝ arcsin (Ici (-1)) (-1)
this : sin ∘ arcsin =ᶠ[𝓝[Ici (-1)] (-1)] id
⊢ False
[PROOFSTEP]
have := h.hasDerivWithinAt.sin.congr_of_eventuallyEq this.symm (by simp)
[GOAL]
h : DifferentiableWithinAt ℝ arcsin (Ici (-1)) (-1)
this : sin ∘ arcsin =ᶠ[𝓝[Ici (-1)] (-1)] id
⊢ id (-1) = sin (arcsin (-1))
[PROOFSTEP]
simp
[GOAL]
h : DifferentiableWithinAt ℝ arcsin (Ici (-1)) (-1)
this✝ : sin ∘ arcsin =ᶠ[𝓝[Ici (-1)] (-1)] id
this : HasDerivWithinAt id (cos (arcsin (-1)) * derivWithin arcsin (Ici (-1)) (-1)) (Ici (-1)) (-1)
⊢ False
[PROOFSTEP]
simpa using (uniqueDiffOn_Ici _ _ left_mem_Ici).eq_deriv _ this (hasDerivWithinAt_id _ _)
[GOAL]
x : ℝ
⊢ DifferentiableWithinAt ℝ arcsin (Iic x) x ↔ x ≠ 1
[PROOFSTEP]
refine' ⟨fun h => _, fun h => (hasDerivWithinAt_arcsin_Iic h).differentiableWithinAt⟩
[GOAL]
x : ℝ
h : DifferentiableWithinAt ℝ arcsin (Iic x) x
⊢ x ≠ 1
[PROOFSTEP]
rw [← neg_neg x, ← image_neg_Ici] at h
[GOAL]
x : ℝ
h : DifferentiableWithinAt ℝ arcsin (Neg.neg '' Ici (-x)) (- -x)
⊢ x ≠ 1
[PROOFSTEP]
have := (h.comp (-x) differentiableWithinAt_id.neg (mapsTo_image _ _)).neg
[GOAL]
x : ℝ
h : DifferentiableWithinAt ℝ arcsin (Neg.neg '' Ici (-x)) (- -x)
this : DifferentiableWithinAt ℝ (fun y => -(arcsin ∘ Neg.neg) y) (Ici (-x)) (-x)
⊢ x ≠ 1
[PROOFSTEP]
simpa [(· ∘ ·), differentiableWithinAt_arcsin_Ici] using this
[GOAL]
⊢ deriv arcsin = fun x => 1 / sqrt (1 - x ^ 2)
[PROOFSTEP]
funext x
[GOAL]
case h
x : ℝ
⊢ deriv arcsin x = 1 / sqrt (1 - x ^ 2)
[PROOFSTEP]
by_cases h : x ≠ -1 ∧ x ≠ 1
[GOAL]
case pos
x : ℝ
h : x ≠ -1 ∧ x ≠ 1
⊢ deriv arcsin x = 1 / sqrt (1 - x ^ 2)
[PROOFSTEP]
exact (hasDerivAt_arcsin h.1 h.2).deriv
[GOAL]
case neg
x : ℝ
h : ¬(x ≠ -1 ∧ x ≠ 1)
⊢ deriv arcsin x = 1 / sqrt (1 - x ^ 2)
[PROOFSTEP]
rw [deriv_zero_of_not_differentiableAt (mt differentiableAt_arcsin.1 h)]
[GOAL]
case neg
x : ℝ
h : ¬(x ≠ -1 ∧ x ≠ 1)
⊢ 0 = 1 / sqrt (1 - x ^ 2)
[PROOFSTEP]
simp only [not_and_or, Ne.def, Classical.not_not] at h
[GOAL]
case neg
x : ℝ
h : x = -1 ∨ x = 1
⊢ 0 = 1 / sqrt (1 - x ^ 2)
[PROOFSTEP]
rcases h with (rfl | rfl)
[GOAL]
case neg.inl
⊢ 0 = 1 / sqrt (1 - (-1) ^ 2)
[PROOFSTEP]
simp
[GOAL]
case neg.inr
⊢ 0 = 1 / sqrt (1 - 1 ^ 2)
[PROOFSTEP]
simp
[GOAL]
x : ℝ
⊢ -deriv (fun y => arcsin y) x = -(1 / sqrt (1 - x ^ 2))
[PROOFSTEP]
simp only [deriv_arcsin]
[GOAL]
x : ℝ
n : ℕ∞
⊢ ContDiffAt ℝ n arccos x ↔ n = 0 ∨ x ≠ -1 ∧ x ≠ 1
[PROOFSTEP]
refine' Iff.trans ⟨fun h => _, fun h => _⟩ contDiffAt_arcsin_iff
[GOAL]
case refine'_1
x : ℝ
n : ℕ∞
h : ContDiffAt ℝ n arccos x
⊢ ContDiffAt ℝ n arcsin x
[PROOFSTEP]
simpa [arccos] using (@contDiffAt_const _ _ _ _ _ _ _ _ _ _ (π / 2)).sub h
[GOAL]
case refine'_2
x : ℝ
n : ℕ∞
h : ContDiffAt ℝ n arcsin x
⊢ ContDiffAt ℝ n arccos x
[PROOFSTEP]
simpa [arccos] using (@contDiffAt_const _ _ _ _ _ _ _ _ _ _ (π / 2)).sub h