X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
x : X
⊢ Tendsto (fun n => approx (n + 1) c x) atTop (𝓝 (midpoint ℝ (CU.lim (left c) x) (CU.lim (right c) x)))
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
x : X
⊢ CU.lim c x = midpoint ℝ (CU.lim (left c) x) (CU.lim (right c) x)
refine' tendsto_nhds_unique (c.tendsto_approx_atTop x) ((tendsto_add_atTop_iff_nat 1).1 _)
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
x : X
⊢ Tendsto (fun n => midpoint ℝ (approx (Nat.add n 0) (left c) x) (approx (Nat.add n 0) (right c) x)) atTop
    (𝓝 (midpoint ℝ (CU.lim (left c) x) (CU.lim (right c) x)))
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
x : X
⊢ Tendsto (fun n => approx (n + 1) c x) atTop (𝓝 (midpoint ℝ (CU.lim (left c) x) (CU.lim (right c) x)))
simp only [approx]
no goals
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
x : X
⊢ Tendsto (fun n => midpoint ℝ (approx (Nat.add n 0) (left c) x) (approx (Nat.add n 0) (right c) x)) atTop
    (𝓝 (midpoint ℝ (CU.lim (left c) x) (CU.lim (right c) x)))
exact (c.left.tendsto_approx_atTop x).midpoint (c.right.tendsto_approx_atTop x)