case refine'_1
𝕜 : Type u_2
E : Type u_1
F : Type ?u.167255
G : Type ?u.167258
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

case refine'_2
𝕜 : Type u_2
E : Type u_1
F : Type ?u.167255
G : Type ?u.167258
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
𝕜 : Type u_2
E : Type u_1
F : Type ?u.167255
G : Type ?u.167258
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
refine' hs.mem_toCone.trans ⟨_, _⟩
case refine'_1.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.167255
G : Type ?u.167258
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
case refine'_1
𝕜 : Type u_2
E : Type u_1
F : Type ?u.167255
G : Type ?u.167258
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
rintro ⟨c, hc, y, hy, rfl⟩
no goals
case refine'_1.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.167255
G : Type ?u.167258
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
exact ⟨c⁻¹, inv_pos.2 hc, by rwa [smul_smul, inv_mul_cancel hc.ne', one_smul]⟩
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.167255
G : Type ?u.167258
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
rwa [smul_smul, inv_mul_cancel hc.ne', one_smul]
case refine'_2.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.167255
G : Type ?u.167258
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
case refine'_2
𝕜 : Type u_2
E : Type u_1
F : Type ?u.167255
G : Type ?u.167258
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
rintro ⟨c, hc, hcx⟩
no goals
case refine'_2.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.167255
G : Type ?u.167258
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
exact ⟨c⁻¹, inv_pos.2 hc, _, hcx, by rw [smul_smul, inv_mul_cancel hc.ne', one_smul]⟩
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.167255
G : Type ?u.167258
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
rw [smul_smul, inv_mul_cancel hc.ne', one_smul]