-- Mathlib/Analysis/Convex/Cone/InnerDual.lean
theorem ConvexCone.pointed_of_nonempty_of_isClosed (K : ConvexCone ℝ H) (ne : (K : Set H).Nonempty)
    (hc : IsClosed (K : Set H)) : K.Pointed

Proof state:
case intro
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
⊢ K.Pointed

Tactic:
have fI : f '' Set.Ioi 0 ⊆ (K : Set H) := by
  rintro _ ⟨_, h, rfl⟩
  exact K.smul_mem (Set.mem_Ioi.1 h) hx

Result:
case intro
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
fI : f '' Ioi 0 ⊆ ↑K
⊢ K.Pointed

Proof state:
case intro
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
fI : f '' Ioi 0 ⊆ ↑K
clf : closure (f '' Ioi 0) ⊆ ↑K
fc : ContinuousWithinAt f (Ioi 0) 0
mem₀ : f 0 ∈ closure (f '' Ioi 0)
f₀ : f 0 = 0
⊢ K.Pointed

Tactic:
simpa only [f₀, ConvexCone.Pointed, ← SetLike.mem_coe] using mem_of_subset_of_mem clf mem₀

Result:
no goals

Proof state:
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
K : ConvexCone ℝ H
ne : (↑K).Nonempty
hc : IsClosed ↑K
⊢ K.Pointed

Tactic:
obtain ⟨x, hx⟩ := ne

Result:
case intro
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
⊢ K.Pointed

Proof state:
case intro
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
fI : f '' Ioi 0 ⊆ ↑K
clf : closure (f '' Ioi 0) ⊆ ↑K
⊢ K.Pointed

Tactic:
have fc : ContinuousWithinAt f (Set.Ioi (0 : ℝ)) 0 :=
  (continuous_id.smul continuous_const).continuousWithinAt

Result:
case intro
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
fI : f '' Ioi 0 ⊆ ↑K
clf : closure (f '' Ioi 0) ⊆ ↑K
fc : ContinuousWithinAt f (Ioi 0) 0
⊢ K.Pointed

Proof state:
case intro
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
fI : f '' Ioi 0 ⊆ ↑K
clf : closure (f '' Ioi 0) ⊆ ↑K
fc : ContinuousWithinAt f (Ioi 0) 0
⊢ K.Pointed

Tactic:
have mem₀ := fc.mem_closure_image (by rw [closure_Ioi (0 : ℝ), mem_Ici])

Result:
case intro
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
fI : f '' Ioi 0 ⊆ ↑K
clf : closure (f '' Ioi 0) ⊆ ↑K
fc : ContinuousWithinAt f (Ioi 0) 0
mem₀ : f 0 ∈ closure (f '' Ioi 0)
⊢ K.Pointed

Proof state:
case intro
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
fI : f '' Ioi 0 ⊆ ↑K
⊢ K.Pointed

Tactic:
have clf : closure (f '' Set.Ioi 0) ⊆ (K : Set H) := hc.closure_subset_iff.2 fI

Result:
case intro
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
fI : f '' Ioi 0 ⊆ ↑K
clf : closure (f '' Ioi 0) ⊆ ↑K
⊢ K.Pointed

Proof state:
case intro
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
fI : f '' Ioi 0 ⊆ ↑K
clf : closure (f '' Ioi 0) ⊆ ↑K
fc : ContinuousWithinAt f (Ioi 0) 0
mem₀ : f 0 ∈ closure (f '' Ioi 0)
⊢ K.Pointed

Tactic:
have f₀ : f 0 = 0 := zero_smul ℝ x

Result:
case intro
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
fI : f '' Ioi 0 ⊆ ↑K
clf : closure (f '' Ioi 0) ⊆ ↑K
fc : ContinuousWithinAt f (Ioi 0) 0
mem₀ : f 0 ∈ closure (f '' Ioi 0)
f₀ : f 0 = 0
⊢ K.Pointed

Proof state:
case intro.intro
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
w✝ : ℝ
h : w✝ ∈ Ioi 0
⊢ f w✝ ∈ ↑K

Tactic:
exact K.smul_mem (Set.mem_Ioi.1 h) hx

Result:
no goals

Proof state:
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
fI : f '' Ioi 0 ⊆ ↑K
clf : closure (f '' Ioi 0) ⊆ ↑K
fc : ContinuousWithinAt f (Ioi 0) 0
⊢ 0 ∈ closure (Ioi 0)

Tactic:
rw [closure_Ioi (0 : ℝ), mem_Ici]

Result:
no goals

Proof state:
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
⊢ f '' Ioi 0 ⊆ ↑K

Tactic:
rintro _ ⟨_, h, rfl⟩

Result:
case intro.intro
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
w✝ : ℝ
h : w✝ ∈ Ioi 0
⊢ f w✝ ∈ ↑K