𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
⊢ y - x ∈ tangentConeAt ℝ s x
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
⊢ y - x ∈ tangentConeAt ℝ s x
let c := fun n : ℕ => (2 : ℝ) ^ (n + 1)
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
⊢ y - x ∈ tangentConeAt ℝ s x
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
⊢ y - x ∈ tangentConeAt ℝ s x
let d := fun n : ℕ => (c n)⁻¹ • (y - x)
case refine'_1
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ x + d n ∈ openSegment ℝ x y

case refine'_2
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
⊢ Tendsto (fun n => ‖c n‖) atTop atTop

case refine'_3
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
⊢ Tendsto (fun n => c n • d n) atTop (𝓝 (y - x))
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
⊢ y - x ∈ tangentConeAt ℝ s x
refine' ⟨c, d, Filter.univ_mem' fun n => h _, _, _⟩
case refine'_1
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ x + d n ∈ openSegment ℝ x y

case refine'_2
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
⊢ Tendsto (fun n => ‖c n‖) atTop atTop

case refine'_3
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
⊢ Tendsto (fun n => c n • d n) atTop (𝓝 (y - x))
case refine'_1
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ x + d n ∈ openSegment ℝ x y

case refine'_2
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
⊢ Tendsto (fun n => ‖c n‖) atTop atTop

case refine'_3
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
⊢ Tendsto (fun n => c n • d n) atTop (𝓝 (y - x))
show x + d n ∈ openSegment ℝ x y
case refine'_2
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
⊢ Tendsto (fun n => ‖c n‖) atTop atTop

case refine'_3
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
⊢ Tendsto (fun n => c n • d n) atTop (𝓝 (y - x))
case refine'_2
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
⊢ Tendsto (fun n => ‖c n‖) atTop atTop

case refine'_3
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
⊢ Tendsto (fun n => c n • d n) atTop (𝓝 (y - x))
show Filter.Tendsto (fun n : ℕ => ‖c n‖) Filter.atTop Filter.atTop
case refine'_3
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
⊢ Tendsto (fun n => c n • d n) atTop (𝓝 (y - x))
case refine'_3
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
⊢ Tendsto (fun n => c n • d n) atTop (𝓝 (y - x))
show Filter.Tendsto (fun n : ℕ => c n • d n) Filter.atTop (𝓝 (y - x))
case refine'_1
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ x + d n ∈ (fun θ => (1 - θ) • x + θ • y) '' Ioo 0 1
case refine'_1
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ x + d n ∈ openSegment ℝ x y
rw [openSegment_eq_image]
case refine'_1.refine'_1
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ 0 < (c n)⁻¹

case refine'_1.refine'_2
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ (c n)⁻¹ < 1

case refine'_1.refine'_3
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ (fun θ => (1 - θ) • x + θ • y) (c n)⁻¹ = x + d n
case refine'_1
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ x + d n ∈ (fun θ => (1 - θ) • x + θ • y) '' Ioo 0 1
refine' ⟨(c n)⁻¹, ⟨_, _⟩, _⟩
case refine'_1.refine'_1
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ 0 < c n
case refine'_1.refine'_1
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ 0 < (c n)⁻¹
rw [inv_pos]
case refine'_1.refine'_1.H
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ 0 < 2
case refine'_1.refine'_1
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ 0 < c n
apply pow_pos
no goals
case refine'_1.refine'_1.H
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ 0 < 2
norm_num
case refine'_1.refine'_2.ha
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ 1 < c n
case refine'_1.refine'_2
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ (c n)⁻¹ < 1
apply inv_lt_one
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ 1 < 2
case refine'_1.refine'_2.ha
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ 1 < c n
apply one_lt_pow _ (Nat.succ_ne_zero _)
no goals
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ 1 < 2
norm_num
case refine'_1.refine'_3
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ x - (2 ^ (n + 1))⁻¹ • x + (2 ^ (n + 1))⁻¹ • y = x + ((2 ^ (n + 1))⁻¹ • y - (2 ^ (n + 1))⁻¹ • x)
case refine'_1.refine'_3
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ (fun θ => (1 - θ) • x + θ • y) (c n)⁻¹ = x + d n
simp only [sub_smul, smul_sub, one_smul]
no goals
case refine'_1.refine'_3
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ x - (2 ^ (n + 1))⁻¹ • x + (2 ^ (n + 1))⁻¹ • y = x + ((2 ^ (n + 1))⁻¹ • y - (2 ^ (n + 1))⁻¹ • x)
abel
case refine'_2
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
this : (fun n => ‖c n‖) = c
⊢ Tendsto (fun n => ‖c n‖) atTop atTop
case refine'_2
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
⊢ Tendsto (fun n => ‖c n‖) atTop atTop
have : (fun n : ℕ => ‖c n‖) = c := by
  ext n
  exact abs_of_nonneg (pow_nonneg (by norm_num) _)
case refine'_2
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
this : (fun n => ‖c n‖) = c
⊢ Tendsto c atTop atTop
case refine'_2
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
this : (fun n => ‖c n‖) = c
⊢ Tendsto (fun n => ‖c n‖) atTop atTop
rw [this]
no goals
case refine'_2
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
this : (fun n => ‖c n‖) = c
⊢ Tendsto c atTop atTop
exact (tendsto_pow_atTop_atTop_of_one_lt (by norm_num)).comp (tendsto_add_atTop_nat 1)
case h
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ ‖c n‖ = c n
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
⊢ (fun n => ‖c n‖) = c
ext n
no goals
case h
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ ‖c n‖ = c n
exact abs_of_nonneg (pow_nonneg (by norm_num) _)
no goals
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ 0 ≤ 2
norm_num
no goals
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
this : (fun n => ‖c n‖) = c
⊢ 1 < 2
norm_num
case refine'_3
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
this : (fun n => c n • d n) = fun x_1 => y - x
⊢ Tendsto (fun n => c n • d n) atTop (𝓝 (y - x))
case refine'_3
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
⊢ Tendsto (fun n => c n • d n) atTop (𝓝 (y - x))
have : (fun n : ℕ => c n • d n) = fun _ => y - x := by
  ext n
  simp only [smul_smul]
  rw [mul_inv_cancel, one_smul]
  exact pow_ne_zero _ (by norm_num)
case refine'_3
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
this : (fun n => c n • d n) = fun x_1 => y - x
⊢ Tendsto (fun x_1 => y - x) atTop (𝓝 (y - x))
case refine'_3
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
this : (fun n => c n • d n) = fun x_1 => y - x
⊢ Tendsto (fun n => c n • d n) atTop (𝓝 (y - x))
rw [this]
no goals
case refine'_3
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
this : (fun n => c n • d n) = fun x_1 => y - x
⊢ Tendsto (fun x_1 => y - x) atTop (𝓝 (y - x))
apply tendsto_const_nhds
case h
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ c n • d n = y - x
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
⊢ (fun n => c n • d n) = fun x_1 => y - x
ext n
case h
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ (2 ^ (n + 1) * (2 ^ (n + 1))⁻¹) • (y - x) = y - x
case h
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ c n • d n = y - x
simp only [smul_smul]
case h
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ 2 ^ (n + 1) ≠ 0
case h
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ (2 ^ (n + 1) * (2 ^ (n + 1))⁻¹) • (y - x) = y - x
rw [mul_inv_cancel, one_smul]
no goals
case h
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ 2 ^ (n + 1) ≠ 0
exact pow_ne_zero _ (by norm_num)
no goals
𝕜 : Type ?u.89534
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.89540
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.89635
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
x y : G
h : openSegment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ (n + 1)
d : ℕ → G := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ 2 ≠ 0
norm_num