case intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.10190
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y✝ z : E
s : Set E
hs : StarConvex 𝕜 x s
y : E
hy : y ∈ s
⊢ x ∈ s
𝕜 : Type u_1
E : Type u_2
F : Type ?u.10190
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y z : E
s : Set E
hs : StarConvex 𝕜 x s
h : Set.Nonempty s
⊢ x ∈ s
obtain ⟨y, hy⟩ := h
case h.e'_4
𝕜 : Type u_1
E : Type u_2
F : Type ?u.10190
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y✝ z : E
s : Set E
hs : StarConvex 𝕜 x s
y : E
hy : y ∈ s
⊢ x = 1 • x + 0 • y
case intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.10190
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y✝ z : E
s : Set E
hs : StarConvex 𝕜 x s
y : E
hy : y ∈ s
⊢ x ∈ s
convert hs hy zero_le_one le_rfl (add_zero 1)
no goals
case h.e'_4
𝕜 : Type u_1
E : Type u_2
F : Type ?u.10190
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y✝ z : E
s : Set E
hs : StarConvex 𝕜 x s
y : E
hy : y ∈ s
⊢ x = 1 • x + 0 • y
rw [one_smul, zero_smul, add_zero]