case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.77348
G : Type ?u.77351
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
𝕜 : Type u_1
E : Type u_2
F : Type ?u.77348
G : Type ?u.77351
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
S✝ S : ConvexCone 𝕜 E
hS : Flat S
⊢ Pointed S
obtain ⟨x, hx, _, hxneg⟩ := hS
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.77348
G : Type ?u.77351
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
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.77348
G : Type ?u.77351
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
rw [Pointed, ← add_neg_self x]
no goals
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.77348
G : Type ?u.77351
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
exact add_mem S hx hxneg