-- Mathlib/Analysis/Calculus/TangentCone.lean
theorem mem_tangentCone_of_openSegment_subset {s : Set G} {x y : G} (h : openSegment ℝ x y ⊆ s) :
    y - x ∈ tangentConeAt ℝ s x

Proof state:
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
n : ℕ
hn : n ≠ 0
⊢ x + (1 / 2) ^ n • (y - x) ∈ openSegment ℝ x y

Tactic:
rw [openSegment_eq_image]

Result:
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
n : ℕ
hn : n ≠ 0
⊢ x + (1 / 2) ^ n • (y - x) ∈ (fun θ => (1 - θ) • x + θ • y) '' Ioo 0 1

Proof state:
case refine_3
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
n : ℕ
hn : n ≠ 0
⊢ (fun θ => (1 - θ) • x + θ • y) ((1 / 2) ^ n) = x + (1 / 2) ^ n • (y - x)

Tactic:
simp only [sub_smul, one_smul, smul_sub]

Result:
case refine_3
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
n : ℕ
hn : n ≠ 0
⊢ x - (1 / 2) ^ n • x + (1 / 2) ^ n • y = x + ((1 / 2) ^ n • y - (1 / 2) ^ n • x)

Proof state:
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
⊢ y - x ∈ tangentConeAt ℝ s x

Tactic:
refine mem_tangentConeAt_of_pow_smul one_half_pos.ne' (by norm_num) ?_

Result:
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
⊢ ∀ᶠ (n : ℕ) in atTop, x + (1 / 2) ^ n • (y - x) ∈ s

Proof state:
case refine_1
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
n : ℕ
hn : n ≠ 0
⊢ 0 < (1 / 2) ^ n

Tactic:
exact pow_pos one_half_pos _

Result:
no goals

Proof state:
case refine_3
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
n : ℕ
hn : n ≠ 0
⊢ x - (1 / 2) ^ n • x + (1 / 2) ^ n • y = x + ((1 / 2) ^ n • y - (1 / 2) ^ n • x)

Tactic:
abel

Result:
no goals

Proof state:
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
n : ℕ
hn : n ≠ 0
⊢ x + (1 / 2) ^ n • (y - x) ∈ (fun θ => (1 - θ) • x + θ • y) '' Ioo 0 1

Tactic:
refine ⟨(1 / 2) ^ n, ⟨?_, ?_⟩, ?_⟩

Result:
case refine_1
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
n : ℕ
hn : n ≠ 0
⊢ 0 < (1 / 2) ^ n

case refine_2
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
n : ℕ
hn : n ≠ 0
⊢ (1 / 2) ^ n < 1

case refine_3
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
n : ℕ
hn : n ≠ 0
⊢ (fun θ => (1 - θ) • x + θ • y) ((1 / 2) ^ n) = x + (1 / 2) ^ n • (y - x)

Proof state:
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
⊢ ‖1 / 2‖ < 1

Tactic:
norm_num

Result:
no goals

Proof state:
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
⊢ ∀ᶠ (n : ℕ) in atTop, x + (1 / 2) ^ n • (y - x) ∈ s

Tactic:
refine (eventually_ne_atTop 0).mono fun n hn ↦ (h ?_)

Result:
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
n : ℕ
hn : n ≠ 0
⊢ x + (1 / 2) ^ n • (y - x) ∈ openSegment ℝ x y

Proof state:
case refine_2
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
n : ℕ
hn : n ≠ 0
⊢ (1 / 2) ^ n < 1

Tactic:
exact pow_lt_one₀ one_half_pos.le one_half_lt_one hn

Result:
no goals