case refine'_1
α : Type ?u.10393
β : Type ?u.10396
ι : Type ?u.10399
𝕜 : Type u_1
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
⊢ ℕ → 𝕜

case refine'_2
α : Type ?u.10393
β : Type ?u.10396
ι : Type ?u.10399
𝕜 : Type u_1
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
n : ℕ
hn : n ≠ 0
⊢ ?refine'_1 n = (fun n => ↑n / (↑n + x)) n

case refine'_3
α : Type ?u.10393
β : Type ?u.10396
ι : Type ?u.10399
𝕜 : Type u_1
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
⊢ Tendsto ?refine'_1 atTop (𝓝 1)
α : Type ?u.10393
β : Type ?u.10396
ι : Type ?u.10399
𝕜 : Type u_1
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
⊢ Tendsto (fun n => ↑n / (↑n + x)) atTop (𝓝 1)
refine' Tendsto.congr' ((eventually_ne_atTop 0).mp (eventually_of_forall fun n hn => _)) _
no goals
case refine'_1
α : Type ?u.10393
β : Type ?u.10396
ι : Type ?u.10399
𝕜 : Type u_1
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
⊢ ℕ → 𝕜
exact fun n : ℕ => 1 / (1 + x / n)
no goals
case refine'_2
α : Type ?u.10393
β : Type ?u.10396
ι : Type ?u.10399
𝕜 : Type u_1
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
n : ℕ
hn : n ≠ 0
⊢ 1 / (1 + x / ↑n) = (fun n => ↑n / (↑n + x)) n
field_simp [Nat.cast_ne_zero.mpr hn]
case refine'_3
α : Type ?u.10393
β : Type ?u.10396
ι : Type ?u.10399
𝕜 : Type u_1
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
this : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
⊢ Tendsto (fun n => 1 / (1 + x / ↑n)) atTop (𝓝 1)
case refine'_3
α : Type ?u.10393
β : Type ?u.10396
ι : Type ?u.10399
𝕜 : Type u_1
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
⊢ Tendsto (fun n => 1 / (1 + x / ↑n)) atTop (𝓝 1)
have : 𝓝 (1 : 𝕜) = 𝓝 (1 / (1 + x * (0 : 𝕜))) := by
  rw [MulZeroClass.mul_zero, add_zero, div_one]
case refine'_3
α : Type ?u.10393
β : Type ?u.10396
ι : Type ?u.10399
𝕜 : Type u_1
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
this : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
⊢ Tendsto (fun n => 1 / (1 + x / ↑n)) atTop (𝓝 (1 / (1 + x * 0)))
case refine'_3
α : Type ?u.10393
β : Type ?u.10396
ι : Type ?u.10399
𝕜 : Type u_1
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
this : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
⊢ Tendsto (fun n => 1 / (1 + x / ↑n)) atTop (𝓝 1)
rw [this]
case refine'_3
α : Type ?u.10393
β : Type ?u.10396
ι : Type ?u.10399
𝕜 : Type u_1
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
this : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
⊢ Tendsto (fun n => x / ↑n) atTop (𝓝 (x * 0))
case refine'_3
α : Type ?u.10393
β : Type ?u.10396
ι : Type ?u.10399
𝕜 : Type u_1
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
this : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
⊢ Tendsto (fun n => 1 / (1 + x / ↑n)) atTop (𝓝 (1 / (1 + x * 0)))
refine' tendsto_const_nhds.div (tendsto_const_nhds.add _) (by simp)
case refine'_3
α : Type ?u.10393
β : Type ?u.10396
ι : Type ?u.10399
𝕜 : Type u_1
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
this : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
⊢ Tendsto (fun n => x * (↑n)⁻¹) atTop (𝓝 (x * 0))
case refine'_3
α : Type ?u.10393
β : Type ?u.10396
ι : Type ?u.10399
𝕜 : Type u_1
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
this : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
⊢ Tendsto (fun n => x / ↑n) atTop (𝓝 (x * 0))
simp_rw [div_eq_mul_inv]
case refine'_3
α : Type ?u.10393
β : Type ?u.10396
ι : Type ?u.10399
𝕜 : Type u_1
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
this : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
⊢ Tendsto (fun n => (↑n)⁻¹) atTop (𝓝 0)
case refine'_3
α : Type ?u.10393
β : Type ?u.10396
ι : Type ?u.10399
𝕜 : Type u_1
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
this : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
⊢ Tendsto (fun n => x * (↑n)⁻¹) atTop (𝓝 (x * 0))
refine' tendsto_const_nhds.mul _
case refine'_3
α : Type ?u.10393
β : Type ?u.10396
ι : Type ?u.10399
𝕜 : Type u_1
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
this✝ : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
this : Tendsto (↑(algebraMap ℝ 𝕜) ∘ fun n => (↑n)⁻¹) atTop (𝓝 (↑(algebraMap ℝ 𝕜) 0))
⊢ Tendsto (fun n => (↑n)⁻¹) atTop (𝓝 0)
case refine'_3
α : Type ?u.10393
β : Type ?u.10396
ι : Type ?u.10399
𝕜 : Type u_1
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
this : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
⊢ Tendsto (fun n => (↑n)⁻¹) atTop (𝓝 0)
have := ((continuous_algebraMap ℝ 𝕜).tendsto _).comp tendsto_inverse_atTop_nhds_0_nat
case refine'_3
α : Type ?u.10393
β : Type ?u.10396
ι : Type ?u.10399
𝕜 : Type u_1
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
this✝ : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
this : ∀ (s : Set 𝕜), s ∈ 𝓝 0 → ∃ a, ∀ (b : ℕ), b ≥ a → (↑(algebraMap ℝ 𝕜) ∘ fun n => (↑n)⁻¹) b ∈ s
⊢ Tendsto (fun n => (↑n)⁻¹) atTop (𝓝 0)
case refine'_3
α : Type ?u.10393
β : Type ?u.10396
ι : Type ?u.10399
𝕜 : Type u_1
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
this✝ : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
this : Tendsto (↑(algebraMap ℝ 𝕜) ∘ fun n => (↑n)⁻¹) atTop (𝓝 (↑(algebraMap ℝ 𝕜) 0))
⊢ Tendsto (fun n => (↑n)⁻¹) atTop (𝓝 0)
rw [map_zero, Filter.tendsto_atTop'] at this
case refine'_3
α : Type ?u.10393
β : Type ?u.10396
ι : Type ?u.10399
𝕜 : Type u_1
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
this✝ : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
this : ∀ (s : Set 𝕜), s ∈ 𝓝 0 → ∃ a, ∀ (b : ℕ), b ≥ a → (↑(algebraMap ℝ 𝕜) ∘ fun n => (↑n)⁻¹) b ∈ s
⊢ ∀ (s : Set 𝕜), s ∈ 𝓝 0 → ∃ a, ∀ (b : ℕ), b ≥ a → (↑b)⁻¹ ∈ s
case refine'_3
α : Type ?u.10393
β : Type ?u.10396
ι : Type ?u.10399
𝕜 : Type u_1
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
this✝ : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
this : ∀ (s : Set 𝕜), s ∈ 𝓝 0 → ∃ a, ∀ (b : ℕ), b ≥ a → (↑(algebraMap ℝ 𝕜) ∘ fun n => (↑n)⁻¹) b ∈ s
⊢ Tendsto (fun n => (↑n)⁻¹) atTop (𝓝 0)
refine' Iff.mpr tendsto_atTop' _
case refine'_3
α : Type ?u.10393
β : Type ?u.10396
ι : Type ?u.10399
𝕜 : Type u_1
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
this✝ : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
this : ∀ (s : Set 𝕜), s ∈ 𝓝 0 → ∃ a, ∀ (b : ℕ), b ≥ a → (↑(algebraMap ℝ 𝕜) ∘ fun n => (↑n)⁻¹) b ∈ s
s✝ : Set 𝕜
a✝ : s✝ ∈ 𝓝 0
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → (↑b)⁻¹ ∈ s✝
case refine'_3
α : Type ?u.10393
β : Type ?u.10396
ι : Type ?u.10399
𝕜 : Type u_1
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
this✝ : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
this : ∀ (s : Set 𝕜), s ∈ 𝓝 0 → ∃ a, ∀ (b : ℕ), b ≥ a → (↑(algebraMap ℝ 𝕜) ∘ fun n => (↑n)⁻¹) b ∈ s
⊢ ∀ (s : Set 𝕜), s ∈ 𝓝 0 → ∃ a, ∀ (b : ℕ), b ≥ a → (↑b)⁻¹ ∈ s
intros
no goals
case refine'_3
α : Type ?u.10393
β : Type ?u.10396
ι : Type ?u.10399
𝕜 : Type u_1
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
this✝ : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
this : ∀ (s : Set 𝕜), s ∈ 𝓝 0 → ∃ a, ∀ (b : ℕ), b ≥ a → (↑(algebraMap ℝ 𝕜) ∘ fun n => (↑n)⁻¹) b ∈ s
s✝ : Set 𝕜
a✝ : s✝ ∈ 𝓝 0
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → (↑b)⁻¹ ∈ s✝
simp_all only [comp_apply, map_inv₀, map_natCast]
no goals
α : Type ?u.10393
β : Type ?u.10396
ι : Type ?u.10399
𝕜 : Type u_1
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
⊢ 𝓝 1 = 𝓝 (1 / (1 + x * 0))
rw [MulZeroClass.mul_zero, add_zero, div_one]
no goals
α : Type ?u.10393
β : Type ?u.10396
ι : Type ?u.10399
𝕜 : Type u_1
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
this : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
⊢ 1 + x * 0 ≠ 0
simp