awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
ha_pos : 0 < a
ha_ne : a ≠ 1
h0 : b / (1 - a) < u₀
n : ℕ
hn : b / (1 - a) < arithGeom a b u₀ n
⊢ b / (1 - a) = a * (b / (1 - a)) + b

Tactic:
grind
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
ha_pos : 0 < a
ha_ne : a ≠ 1
h0 : b / (1 - a) < u₀
n : ℕ
hn : b / (1 - a) < arithGeom a b u₀ n
bc : 0 < a
⊢ a * (b / (1 - a)) + b < a * arithGeom a b u₀ n + b

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
ha_pos : 0 < a
ha_ne : a ≠ 1
h0 : b / (1 - a) < u₀
n : ℕ
hn : b / (1 - a) < arithGeom a b u₀ n
calc : b / (1 - a) = a * (b / (1 - a)) + b
calc₁ : a * (b / (1 - a)) + b < a * arithGeom a b u₀ n + b
⊢ b / (1 - a) < arithGeom a b u₀ (n + 1)

Tactic:
calc b / (1 - a)
    _ = a * (b / (1 - a)) + b := by grind
    _ < a * arithGeom a b u₀ n + b := by gcongr

Premises used: HSub.hSub, HDiv.hDiv, OfNat.ofNat, arithGeom
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
ha_pos : 0 < a
ha_ne : a ≠ 1
h0 : b / (1 - a) < u₀
n : ℕ
zero : b / (1 - a) < arithGeom a b u₀ 0
succ : ∀ (n : ℕ) (hn : b / (1 - a) < arithGeom a b u₀ n), b / (1 - a) < arithGeom a b u₀ (n + 1)
⊢ b / (1 - a) < arithGeom a b u₀ n

Tactic:
induction n with
  | zero => exact h0
  | succ n hn =>
    calc b / (1 - a)
    _ = a * (b / (1 - a)) + b := by grind
    _ < a * arithGeom a b u₀ n + b := by gcongr

Premises used: HSub.hSub, HDiv.hDiv, OfNat.ofNat, arithGeom
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
ha : 1 < a
h0 : b / (1 - a) < u₀
⊢ StrictMono (arithGeom a b u₀)

Tactic:
strictMono_nat_of_lt_succ fun n ↦ ?_

Premises used: strictMono_nat_of_lt_succ
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
ha : 1 < a
h0 : b / (1 - a) < u₀
refine : ∀ (n : ℕ), arithGeom a b u₀ n < arithGeom a b u₀ (n + 1)
⊢ StrictMono (arithGeom a b u₀)

Tactic:
refine strictMono_nat_of_lt_succ fun n ↦ ?_

Premises used: strictMono_nat_of_lt_succ
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
ha : 1 < a
h0 : b / (1 - a) < u₀
n : ℕ
⊢ 0 < a

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
ha : 1 < a
h0 : b / (1 - a) < u₀
n : ℕ
⊢ b / (1 - a) < arithGeom a b u₀ n

Tactic:
have h_lt : b / (1 - a) < arithGeom a b u₀ n := div_lt_arithGeom (by positivity) ha.ne' h0 n
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
ha : 1 < a
h0 : b / (1 - a) < u₀
n : ℕ
h_lt : b / (1 - a) < arithGeom a b u₀ n
⊢ arithGeom a b u₀ n * (1 - a) < b

Tactic:
rw [div_lt_iff_of_neg (sub_neg.mpr ha)] at h_lt

Premises used: sub_neg, Iff.mpr, div_lt_iff_of_neg
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
ha : 1 < a
h0 : b / (1 - a) < u₀
n : ℕ
h_lt : arithGeom a b u₀ n * (1 - a) < b
rw : arithGeom a b u₀ n < a * arithGeom a b u₀ n + b
⊢ arithGeom a b u₀ n < arithGeom a b u₀ (n + 1)

Tactic:
rw [arithGeom_succ]

Premises used: arithGeom_succ
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
ha : 1 < a
h0 : b / (1 - a) < u₀
n : ℕ
h_lt : arithGeom a b u₀ n * (1 - a) < b
linarith :
  a * arithGeom a b u₀ n + b ≤ arithGeom a b u₀ n →
    arithGeom a b u₀ n * (1 - a) - b + (a * arithGeom a b u₀ n + b - arithGeom a b u₀ n) = 0
⊢ arithGeom a b u₀ n < a * arithGeom a b u₀ n + b

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
ha : 1 < a
h0 : b / (1 - a) < u₀
rw : Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ a ^ n * (u₀ - b / (1 - a)) + b / (1 - a)) atTop atTop
⊢ Tendsto (arithGeom a b u₀) atTop atTop

Tactic:
rw [arithGeom_eq' ha.ne']

Premises used: arithGeom_eq', LT.lt.ne'
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
ha : 1 < a
h0 : b / (1 - a) < u₀
⊢ Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ a ^ n * (u₀ - b / (1 - a)) + b / (1 - a)) atTop atTop

Tactic:
tendsto_atTop_add_const_right _ _ ?_

Premises used: Filter.tendsto_atTop_add_const_right
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
ha : 1 < a
h0 : b / (1 - a) < u₀
refine : Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ a ^ n * (u₀ - b / (1 - a))) atTop atTop
⊢ Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ a ^ n * (u₀ - b / (1 - a)) + b / (1 - a)) atTop atTop

Tactic:
refine tendsto_atTop_add_const_right _ _ ?_

Premises used: Filter.tendsto_atTop_add_const_right
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
ha : 1 < a
h0 : b / (1 - a) < u₀
⊢ Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ a ^ n * (u₀ - b / (1 - a))) atTop atTop

Tactic:
Tendsto.atTop_mul_const (sub_pos.mpr h0) ?_

Premises used: Iff.mpr, sub_pos, Filter.Tendsto.atTop_mul_const
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
ha : 1 < a
h0 : b / (1 - a) < u₀
refine : Tendsto (α := ℕ) (HPow.hPow a) atTop atTop
⊢ Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ a ^ n * (u₀ - b / (1 - a))) atTop atTop

Tactic:
refine Tendsto.atTop_mul_const (sub_pos.mpr h0) ?_

Premises used: Iff.mpr, sub_pos, Filter.Tendsto.atTop_mul_const
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
ha : 1 < a
h0 : b / (1 - a) < u₀
⊢ Tendsto (α := ℕ) (HPow.hPow a) atTop atTop

Tactic:
tendsto_pow_atTop_atTop_of_one_lt ha

Premises used: tendsto_pow_atTop_atTop_of_one_lt
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
ha : 1 < a
h0 : b / (1 - a) < u₀
⊢ Tendsto (α := ℕ) (HPow.hPow a) atTop atTop

Tactic:
exact tendsto_pow_atTop_atTop_of_one_lt ha

Premises used: tendsto_pow_atTop_atTop_of_one_lt
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
inst_4 : TopologicalSpace R
inst_5 : OrderTopology R
ha_pos : 0 ≤ a
ha : a < 1
rw : Tendsto (fun (n : ℕ) ↦ a ^ n * (u₀ - b / (1 - a)) + b / (1 - a)) atTop (𝓝 (b / (1 - a)))
⊢ Tendsto (arithGeom a b u₀) atTop (𝓝 (b / (1 - a)))

Tactic:
rw [arithGeom_eq' ha.ne]

Premises used: arithGeom_eq', LT.lt.ne
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
inst_4 : TopologicalSpace R
inst_5 : OrderTopology R
ha_pos : 0 ≤ a
ha : a < 1
rw : 𝓝 (0 + b / (1 - a))
| 𝓝 (b / (1 - a))

Tactic:
rw [← zero_add (b / (1 - a))]

Premises used: HSub.hSub, HDiv.hDiv, zero_add, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
inst_4 : TopologicalSpace R
inst_5 : OrderTopology R
ha_pos : 0 ≤ a
ha : a < 1
conv_rhs : Tendsto (fun (n : ℕ) ↦ a ^ n * (u₀ - b / (1 - a)) + b / (1 - a)) atTop (𝓝 (0 + b / (1 - a)))
⊢ Tendsto (fun (n : ℕ) ↦ a ^ n * (u₀ - b / (1 - a)) + b / (1 - a)) atTop (𝓝 (b / (1 - a)))

Tactic:
conv_rhs => rw [← zero_add (b / (1 - a))]

Premises used: HSub.hSub, HDiv.hDiv, zero_add, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
inst_4 : TopologicalSpace R
inst_5 : OrderTopology R
ha_pos : 0 ≤ a
ha : a < 1
⊢ Tendsto (fun (n : ℕ) ↦ a ^ n * (u₀ - b / (1 - a)) + b / (1 - a)) atTop (𝓝 (0 + b / (1 - a)))

Tactic:
Tendsto.add ?_ tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.add
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
inst_4 : TopologicalSpace R
inst_5 : OrderTopology R
ha_pos : 0 ≤ a
ha : a < 1
refine : Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ a ^ n * (u₀ - b / (1 - a))) atTop (𝓝 0)
⊢ Tendsto (fun (n : ℕ) ↦ a ^ n * (u₀ - b / (1 - a)) + b / (1 - a)) atTop (𝓝 (0 + b / (1 - a)))

Tactic:
refine Tendsto.add ?_ tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.add
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
inst_4 : TopologicalSpace R
inst_5 : OrderTopology R
ha_pos : 0 ≤ a
ha : a < 1
rw : 𝓝 (0 * (u₀ - b / (1 - a)))
| 𝓝 0

Tactic:
rw [← zero_mul (u₀ - (b / (1 - a)))]

Premises used: MulZeroClass.zero_mul, HSub.hSub, HDiv.hDiv, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
inst_4 : TopologicalSpace R
inst_5 : OrderTopology R
ha_pos : 0 ≤ a
ha : a < 1
conv_rhs : Tendsto (fun (n : ℕ) ↦ a ^ n * (u₀ - b / (1 - a))) atTop (𝓝 (0 * (u₀ - b / (1 - a))))
⊢ Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ a ^ n * (u₀ - b / (1 - a))) atTop (𝓝 0)

Tactic:
conv_rhs => rw [← zero_mul (u₀ - (b / (1 - a)))]

Premises used: MulZeroClass.zero_mul, HSub.hSub, HDiv.hDiv, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
inst_4 : TopologicalSpace R
inst_5 : OrderTopology R
ha_pos : 0 ≤ a
ha : a < 1
⊢ Tendsto (fun (n : ℕ) ↦ a ^ n * (u₀ - b / (1 - a))) atTop (𝓝 (0 * (u₀ - b / (1 - a))))

Tactic:
(tendsto_pow_atTop_nhds_zero_of_lt_one ha_pos ha).mul_const _

Premises used: Filter.Tendsto.mul_const, tendsto_pow_atTop_nhds_zero_of_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
inst_4 : TopologicalSpace R
inst_5 : OrderTopology R
ha_pos : 0 ≤ a
ha : a < 1
⊢ Tendsto (fun (n : ℕ) ↦ a ^ n * (u₀ - b / (1 - a))) atTop (𝓝 (0 * (u₀ - b / (1 - a))))

Tactic:
exact (tendsto_pow_atTop_nhds_zero_of_lt_one ha_pos ha).mul_const _

Premises used: Filter.Tendsto.mul_const, tendsto_pow_atTop_nhds_zero_of_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
⊢ Tendsto (β := ℚ≥0) (fun (n : ℕ) ↦ (↑n : ℚ≥0)⁻¹) atTop (𝓝 0)

Tactic:
tendsto_inv_atTop_zero.comp tendsto_natCast_atTop_atTop

Premises used: tendsto_inv_atTop_zero, tendsto_natCast_atTop_atTop, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Semiring 𝕜
inst_1 : Algebra ℚ≥0 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
⊢ Tendsto (α := ℕ) (β := 𝕜) (comp (β := ℚ≥0) (⇑(algebraMap ℚ≥0 𝕜) : (a : ℚ≥0) → 𝕜) fun (n : ℕ) ↦ (↑n : ℚ≥0)⁻¹ : ℕ → 𝕜)
    atTop (𝓝 ((algebraMap ℚ≥0 𝕜 : (a : ℚ≥0) → 𝕜) 0) : Filter 𝕜)

Tactic:
(continuous_algebraMap ℚ≥0 𝕜).continuousAt.tendsto.comp tendsto_inv_atTop_nhds_zero_nat

Premises used: continuous_algebraMap, NNRat, NNRat.tendsto_inv_atTop_nhds_zero_nat, Continuous.continuousAt, ContinuousAt.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Semiring 𝕜
inst_1 : Algebra ℚ≥0 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
h : Eq (α := 𝕜) (0 : 𝕜) ((algebraMap ℚ≥0 𝕜 : (a : ℚ≥0) → 𝕜) 0 : 𝕜)
⊢ Tendsto (α := ℕ) (β := 𝕜) (comp (β := ℚ≥0) (⇑(algebraMap ℚ≥0 𝕜) : (a : ℚ≥0) → 𝕜) fun (n : ℕ) ↦ (↑n : ℚ≥0)⁻¹) atTop
    (𝓝 0)

Tactic:
convert! (continuous_algebraMap ℚ≥0 𝕜).continuousAt.tendsto.comp tendsto_inv_atTop_nhds_zero_nat

Premises used: continuous_algebraMap, NNRat, NNRat.tendsto_inv_atTop_nhds_zero_nat, Continuous.continuousAt, ContinuousAt.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Semiring 𝕜
inst_1 : Algebra ℚ≥0 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
h h₁ : Eq.{u_4 + 1} (α := 𝕜) 0 0
⊢ Eq (α := 𝕜) (0 : 𝕜) ((algebraMap ℚ≥0 𝕜 : (a : ℚ≥0) → 𝕜) 0 : 𝕜)

Tactic:
rw [map_zero]

Premises used: map_zero
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : DivisionSemiring 𝕜
inst_1 : CharZero 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
⊢ Tendsto (α := ℕ) (β := 𝕜) (comp (β := ℚ≥0) (⇑(algebraMap ℚ≥0 𝕜) : (a : ℚ≥0) → 𝕜) fun (n : ℕ) ↦ (↑n : ℚ≥0)⁻¹) atTop
    (𝓝 0)

Tactic:
NNRat.tendsto_algebraMap_inv_atTop_nhds_zero_nat 𝕜

Premises used: NNRat.tendsto_algebraMap_inv_atTop_nhds_zero_nat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : DivisionSemiring 𝕜
inst_1 : CharZero 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
h :
  ∀ (x : ℕ),
    Eq (α := 𝕜) (↑x : 𝕜)⁻¹ (comp (β := ℚ≥0) (⇑(algebraMap ℚ≥0 𝕜) : (a : ℚ≥0) → 𝕜) (fun (n : ℕ) ↦ (↑n : ℚ≥0)⁻¹) x)
⊢ Tendsto.{0, u_4} (β := 𝕜) (fun (n : ℕ) ↦ (↑n : 𝕜)⁻¹) atTop (𝓝 0)

Tactic:
convert! NNRat.tendsto_algebraMap_inv_atTop_nhds_zero_nat 𝕜

Premises used: NNRat.tendsto_algebraMap_inv_atTop_nhds_zero_nat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : DivisionSemiring 𝕜
inst_1 : CharZero 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
x : ℕ
⊢ Eq (α := 𝕜) (↑x : 𝕜)⁻¹ (comp (β := ℚ≥0) (⇑(algebraMap ℚ≥0 𝕜) : (a : ℚ≥0) → 𝕜) (fun (n : ℕ) ↦ (↑n : ℚ≥0)⁻¹) x)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : DivisionSemiring 𝕜
inst_1 : CharZero 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
inst_4 : ContinuousMul 𝕜
C : 𝕜
⊢ Tendsto.{0, u_4} (β := 𝕜) (fun (n : ℕ) ↦ C / (↑n : 𝕜)) atTop (𝓝 0)

Tactic:
simpa only [mul_zero, div_eq_mul_inv] using
    (tendsto_const_nhds (x := C)).mul tendsto_inv_atTop_nhds_zero_nat

Premises used: tendsto_const_nhds, div_eq_mul_inv, MulZeroClass.mul_zero, Filter.Tendsto.mul, tendsto_inv_atTop_nhds_zero_nat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : DivisionSemiring 𝕜
inst_1 : CharZero 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
⊢ Tendsto.{0, u_4} (β := 𝕜) (fun (n : ℕ) ↦ HDiv.hDiv (α := 𝕜) 1 (↑n : 𝕜)) atTop (𝓝 0)

Tactic:
simp [tendsto_inv_atTop_nhds_zero_nat]

Premises used: tendsto_inv_atTop_nhds_zero_nat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
C : EReal
h : C ≠ ⊥
h' : C ≠ ⊤
h₁ : ∀ (n : ℕ), C / (↑n : EReal) = (↑(C.toReal / (↑n : ℝ)) : EReal)
⊢ Eq (α := (n : ℕ) → EReal) (fun (n : ℕ) ↦ C / (↑n : EReal)) fun (n : ℕ) ↦ (↑(C.toReal / (↑n : ℝ)) : EReal)

Tactic:
ext n
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
C : EReal
h : C ≠ ⊥
h' : C ≠ ⊤
n : ℕ
h₁ : (↑C.toReal : EReal) / (↑n : EReal) = (↑(C.toReal / (↑n : ℝ)) : EReal)
h₂ : (↑C.toReal : EReal) / (↑(↑n : ℝ) : EReal) = (↑(C.toReal / (↑n : ℝ)) : EReal)
h₃ h₄ : (↑(C.toReal / (↑n : ℝ)) : EReal) = (↑(C.toReal / (↑n : ℝ)) : EReal)
⊢ C / (↑n : EReal) = (↑(C.toReal / (↑n : ℝ)) : EReal)

Tactic:
nth_rw 1 [← coe_toReal h' h, ← coe_coe_eq_natCast n, ← coe_div C.toReal n]

Premises used: EReal.coe_coe_eq_natCast, Nat.cast, EReal.coe_toReal, EReal.toReal, EReal.coe_div
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
C : EReal
h : C ≠ ⊥
h' : C ≠ ⊤
⊢ Eq (α := (n : ℕ) → EReal) (fun (n : ℕ) ↦ C / (↑n : EReal)) fun (n : ℕ) ↦ (↑(C.toReal / (↑n : ℝ)) : EReal)

Tactic:
have : (fun n : ℕ ↦ C / n) = fun n : ℕ ↦ ((C.toReal / n : ℝ) : EReal) := by
    ext n
    nth_rw 1 [← coe_toReal h' h, ← coe_coe_eq_natCast n, ← coe_div C.toReal n]
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
C : EReal
h : C ≠ ⊥
h' : C ≠ ⊤
this : Eq (α := (n : ℕ) → EReal) (fun (n : ℕ) ↦ C / (↑n : EReal)) fun (n : ℕ) ↦ (↑(C.toReal / (↑n : ℝ)) : EReal)
rw : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C.toReal / (↑n : ℝ)) atTop (𝓝 0)
⊢ Tendsto (β := EReal) (fun (n : ℕ) ↦ C / (↑n : EReal)) atTop (𝓝 0)

Tactic:
rw [this, ← coe_zero, tendsto_coe]

Premises used: EReal.coe_zero, EReal.tendsto_coe
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
C : EReal
h : C ≠ ⊥
h' : C ≠ ⊤
this : Eq (α := (n : ℕ) → EReal) (fun (n : ℕ) ↦ C / (↑n : EReal)) fun (n : ℕ) ↦ (↑(C.toReal / (↑n : ℝ)) : EReal)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ C.toReal / (↑n : ℝ)) atTop (𝓝 0)

Tactic:
_root_.tendsto_const_div_atTop_nhds_zero_nat C.toReal

Premises used: tendsto_const_div_atTop_nhds_zero_nat, EReal.toReal
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
C : EReal
h : C ≠ ⊥
h' : C ≠ ⊤
this : Eq (α := (n : ℕ) → EReal) (fun (n : ℕ) ↦ C / (↑n : EReal)) fun (n : ℕ) ↦ (↑(C.toReal / (↑n : ℝ)) : EReal)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ C.toReal / (↑n : ℝ)) atTop (𝓝 0)

Tactic:
exact _root_.tendsto_const_div_atTop_nhds_zero_nat C.toReal

Premises used: tendsto_const_div_atTop_nhds_zero_nat, EReal.toReal
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : DivisionSemiring 𝕜
inst_1 : CharZero 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
this : Tendsto.{0, u_4} (β := 𝕜) (fun (n : ℕ) ↦ HDiv.hDiv (α := 𝕜) 1 (↑(n + 1) : 𝕜)) atTop (𝓝 0)
⊢ Tendsto.{0, u_4} (β := 𝕜) (fun (n : ℕ) ↦ 1 / HAdd.hAdd (α := 𝕜) (↑n : 𝕜) 1) atTop (𝓝 0)

Tactic:
simpa
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
A : Type u_5
inst : Semifield 𝕜
inst_1 : CharZero 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
inst_4 : Semiring A
inst_5 : Algebra 𝕜 A
inst_6 : TopologicalSpace A
inst_7 : ContinuousSMul 𝕜 A
⊢ Tendsto.{0, u_5} (α := ℕ) (β := A)
    (comp.{1, u_4 + 1, u_5 + 1} (β := 𝕜) (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) fun (n : ℕ) ↦ (↑n : 𝕜)⁻¹ : ℕ → A) atTop
    (𝓝 ((algebraMap 𝕜 A : (a : 𝕜) → A) 0) : Filter A)

Tactic:
(continuous_algebraMap 𝕜 A).continuousAt.tendsto.comp tendsto_inv_atTop_nhds_zero_nat

Premises used: continuous_algebraMap, Continuous.continuousAt, ContinuousAt.tendsto, Filter.Tendsto.comp, tendsto_inv_atTop_nhds_zero_nat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
A : Type u_5
inst : Semifield 𝕜
inst_1 : CharZero 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
inst_4 : Semiring A
inst_5 : Algebra 𝕜 A
inst_6 : TopologicalSpace A
inst_7 : ContinuousSMul 𝕜 A
h : Eq.{u_5 + 1} (α := A) (0 : A) ((algebraMap 𝕜 A : (a : 𝕜) → A) 0 : A)
⊢ Tendsto.{0, u_5} (α := ℕ) (β := A)
    (comp.{1, u_4 + 1, u_5 + 1} (β := 𝕜) (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) fun (n : ℕ) ↦ (↑n : 𝕜)⁻¹) atTop (𝓝 0)

Tactic:
convert! (continuous_algebraMap 𝕜 A).continuousAt.tendsto.comp tendsto_inv_atTop_nhds_zero_nat

Premises used: continuous_algebraMap, Continuous.continuousAt, ContinuousAt.tendsto, Filter.Tendsto.comp, tendsto_inv_atTop_nhds_zero_nat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
A : Type u_5
inst : Semifield 𝕜
inst_1 : CharZero 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
inst_4 : Semiring A
inst_5 : Algebra 𝕜 A
inst_6 : TopologicalSpace A
inst_7 : ContinuousSMul 𝕜 A
h h₁ : Eq.{u_5 + 1} (α := A) 0 0
⊢ Eq.{u_5 + 1} (α := A) (0 : A) ((algebraMap 𝕜 A : (a : 𝕜) → A) 0 : A)

Tactic:
rw [map_zero]

Premises used: map_zero
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : DivisionSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : CharZero 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
inst_4 : IsTopologicalSemiring 𝕜
inst_5 : ContinuousInv₀ 𝕜
x : 𝕜
⊢ Tendsto.{0, u_4} (β := 𝕜) (fun (n : ℕ) ↦ (↑n : 𝕜) / ((↑n : 𝕜) + x)) atTop (𝓝 1)

Tactic:
Tendsto.congr' ((eventually_ne_atTop 0).mp (Eventually.of_forall fun n hn ↦ _)) _

Premises used: Filter.eventually_ne_atTop, Filter.Eventually.of_forall, Filter.Eventually.mp, Filter.Tendsto.congr', OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : DivisionSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : CharZero 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
inst_4 : IsTopologicalSemiring 𝕜
inst_5 : ContinuousInv₀ 𝕜
x : 𝕜
convert_2 : ℕ → 𝕜
convert_5 : ∀ (n : ℕ) (hn : n ≠ 0), 1 / (1 + x / (↑n : 𝕜)) = (↑n : 𝕜) / ((↑n : 𝕜) + x)
convert_6 : Tendsto.{0, u_4} (β := 𝕜) (fun (n : ℕ) ↦ 1 / (1 + x / (↑n : 𝕜))) atTop (𝓝 1)
⊢ Tendsto.{0, u_4} (β := 𝕜) (fun (n : ℕ) ↦ (↑n : 𝕜) / ((↑n : 𝕜) + x)) atTop (𝓝 1)

Tactic:
convert! Tendsto.congr' ((eventually_ne_atTop 0).mp (Eventually.of_forall fun n hn ↦ _)) _

Premises used: Filter.eventually_ne_atTop, Filter.Eventually.of_forall, Filter.Eventually.mp, Filter.Tendsto.congr', OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : DivisionSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : CharZero 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
inst_4 : IsTopologicalSemiring 𝕜
inst_5 : ContinuousInv₀ 𝕜
x : 𝕜
⊢ ℕ → 𝕜

Tactic:
exact fun n : ℕ ↦ 1 / (1 + x / n)

Premises used: HDiv.hDiv, Nat.cast, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : DivisionSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : CharZero 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
inst_4 : IsTopologicalSemiring 𝕜
inst_5 : ContinuousInv₀ 𝕜
x : 𝕜
n : ℕ
hn : n ≠ 0
⊢ 1 / (1 + x / (↑n : 𝕜)) = (↑n : 𝕜) / ((↑n : 𝕜) + x)

Tactic:
simp [Nat.cast_ne_zero.mpr hn, add_div']

Premises used: Iff.mpr, add_div', Nat.cast_ne_zero
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : DivisionSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : CharZero 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
inst_4 : IsTopologicalSemiring 𝕜
inst_5 : ContinuousInv₀ 𝕜
x : 𝕜
rw : 𝓝 1 = 𝓝 (1 / HAdd.hAdd (α := 𝕜) 1 0)
rw₁ : 𝓝 1 = 𝓝 (1 / 1)
rw₂ rw₃ : Eq.{u_4 + 1} (α := Filter 𝕜) (𝓝 1) (𝓝 1)
⊢ 𝓝 1 = 𝓝 (1 / (1 + x * 0))

Tactic:
rw [mul_zero, add_zero, div_one]

Premises used: MulZeroClass.mul_zero, add_zero, div_one
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : DivisionSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : CharZero 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
inst_4 : IsTopologicalSemiring 𝕜
inst_5 : ContinuousInv₀ 𝕜
x : 𝕜
⊢ 𝓝 1 = 𝓝 (1 / (1 + x * 0))

Tactic:
have : 𝓝 (1 : 𝕜) = 𝓝 (1 / (1 + x * (0 : 𝕜))) := by
      rw [mul_zero, add_zero, div_one]
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : DivisionSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : CharZero 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
inst_4 : IsTopologicalSemiring 𝕜
inst_5 : ContinuousInv₀ 𝕜
x : 𝕜
this : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
convert_6 : Tendsto (fun (n : ℕ) ↦ 1 / (1 + x / (↑n : 𝕜))) atTop (𝓝 (1 / (1 + x * 0)))
⊢ Tendsto.{0, u_4} (β := 𝕜) (fun (n : ℕ) ↦ 1 / (1 + x / (↑n : 𝕜))) atTop (𝓝 1)

Tactic:
rw [this]
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : DivisionSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : CharZero 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
inst_4 : IsTopologicalSemiring 𝕜
inst_5 : ContinuousInv₀ 𝕜
x : 𝕜
this : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
⊢ 1 + x * 0 ≠ 0

Tactic:
simp