awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ) ↦ x / (↑n : 𝕜)) atTop (𝓝 (x * 0))
⊢ Tendsto (fun (n : ℕ) ↦ 1 / (1 + x / (↑n : 𝕜))) atTop (𝓝 (1 / (1 + x * 0)))

Tactic:
refine tendsto_const_nhds.div (tendsto_const_nhds.add ?_) (by simp)

Premises used: tendsto_const_nhds, Filter.Tendsto.div, Filter.Tendsto.add
-- 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 : ℕ) ↦ x * (↑n : 𝕜)⁻¹) atTop (𝓝 (x * 0))
⊢ Tendsto (fun (n : ℕ) ↦ x / (↑n : 𝕜)) atTop (𝓝 (x * 0))

Tactic:
simp_rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- 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))
⊢ Tendsto (fun (n : ℕ) ↦ x * (↑n : 𝕜)⁻¹) atTop (𝓝 (x * 0))

Tactic:
tendsto_const_nhds.mul tendsto_inv_atTop_nhds_zero_nat

Premises used: tendsto_const_nhds, Filter.Tendsto.mul, tendsto_inv_atTop_nhds_zero_nat
-- 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))
⊢ Tendsto (fun (n : ℕ) ↦ x * (↑n : 𝕜)⁻¹) atTop (𝓝 (x * 0))

Tactic:
exact tendsto_const_nhds.mul tendsto_inv_atTop_nhds_zero_nat

Premises used: tendsto_const_nhds, Filter.Tendsto.mul, tendsto_inv_atTop_nhds_zero_nat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Semifield 𝕜
inst_1 : CharZero 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
inst_4 : IsTopologicalSemiring 𝕜
inst_5 : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
hl :
  EventuallyEq.{0, u_4} (β := 𝕜) atTop (fun (k : ℕ) ↦ (a * (↑k : 𝕜)⁻¹ + c) / (b * (↑k : 𝕜)⁻¹ + d)) fun (k : ℕ) ↦
    (a + c * (↑k : 𝕜)) / (b + d * (↑k : 𝕜))
h : Tendsto (fun (k : ℕ) ↦ (a * (↑k : 𝕜)⁻¹ + c) / (b * (↑k : 𝕜)⁻¹ + d)) atTop (𝓝 (c / d))
apply : ℕ → 𝕜
⊢ Tendsto (fun (k : ℕ) ↦ (a + c * (↑k : 𝕜)) / (b + d * (↑k : 𝕜))) atTop (𝓝 (c / d))

Tactic:
apply Filter.Tendsto.congr'

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Semifield 𝕜
inst_1 : CharZero 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
inst_4 : IsTopologicalSemiring 𝕜
inst_5 : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ ℕ → 𝕜

Tactic:
exact fun k ↦ (a * (↑k)⁻¹ + c) / (b * (↑k)⁻¹ + d)

Premises used: HMul.hMul, HDiv.hDiv, Inv.inv, HAdd.hAdd
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Semifield 𝕜
inst_1 : CharZero 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
inst_4 : IsTopologicalSemiring 𝕜
inst_5 : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ ℕ → 𝕜

Tactic:
case f₁ => exact fun k ↦ (a * (↑k)⁻¹ + c) / (b * (↑k)⁻¹ + d)

Premises used: HMul.hMul, HDiv.hDiv, Inv.inv, HAdd.hAdd
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Semifield 𝕜
inst_1 : CharZero 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
inst_4 : IsTopologicalSemiring 𝕜
inst_5 : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ EventuallyEq.{0, u_4} (β := 𝕜) atTop (fun (k : ℕ) ↦ (a * (↑k : 𝕜)⁻¹ + c) / (b * (↑k : 𝕜)⁻¹ + d)) fun (k : ℕ) ↦
    (a + c * (↑k : 𝕜)) / (b + d * (↑k : 𝕜))

Tactic:
(eventually_ne_atTop 0).mp (Eventually.of_forall ?_)

Premises used: Filter.EventuallyEq, Filter.eventually_ne_atTop, Filter.Eventually.of_forall, Filter.Eventually.mp, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Semifield 𝕜
inst_1 : CharZero 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
inst_4 : IsTopologicalSemiring 𝕜
inst_5 : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
hl :
  ∀ (x : ℕ),
    x ≠ 0 →
      Eq.{u_4 + 1} (α := 𝕜) ((fun (k : ℕ) ↦ (a * (↑k : 𝕜)⁻¹ + c) / (b * (↑k : 𝕜)⁻¹ + d)) x)
        ((fun (k : ℕ) ↦ (a + c * (↑k : 𝕜)) / (b + d * (↑k : 𝕜))) x)
⊢ EventuallyEq.{0, u_4} (β := 𝕜) atTop (fun (k : ℕ) ↦ (a * (↑k : 𝕜)⁻¹ + c) / (b * (↑k : 𝕜)⁻¹ + d)) fun (k : ℕ) ↦
    (a + c * (↑k : 𝕜)) / (b + d * (↑k : 𝕜))

Tactic:
refine (eventually_ne_atTop 0).mp (Eventually.of_forall ?_)

Premises used: Filter.eventually_ne_atTop, Filter.Eventually.of_forall, Filter.Eventually.mp, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Semifield 𝕜
inst_1 : CharZero 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
inst_4 : IsTopologicalSemiring 𝕜
inst_5 : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
h : ℕ
hx : h ≠ 0
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : ¬h = 0
⊢ Ne.{u_4 + 1} (α := 𝕜) (↑h : 𝕜) 0

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Semifield 𝕜
inst_1 : CharZero 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
inst_4 : IsTopologicalSemiring 𝕜
inst_5 : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
h : ℕ
hx : h ≠ 0
norm_cast : ¬a + (↑h : 𝕜) * c = 0
⊢ a + (↑h : 𝕜) * c ≠ 0

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Semifield 𝕜
inst_1 : CharZero 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
inst_4 : IsTopologicalSemiring 𝕜
inst_5 : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
h : ℕ
hx : h ≠ 0
norm_cast : ¬b + (↑h : 𝕜) * d = 0
⊢ b + (↑h : 𝕜) * d ≠ 0

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Semifield 𝕜
inst_1 : CharZero 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
inst_4 : IsTopologicalSemiring 𝕜
inst_5 : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
h : ℕ
hx : h ≠ 0
field field₁ field₂ : Ne.{u_4 + 1} (α := 𝕜) (↑h : 𝕜) 0
field₃ : a + (↑h : 𝕜) * c ≠ 0
field₄ : Ne.{u_4 + 1} (α := 𝕜) (↑h : 𝕜) 0
field₅ : b + (↑h : 𝕜) * d ≠ 0
field₆ : Ne.{u_4 + 1} (α := 𝕜) (↑h : 𝕜) 0
field₇ : a + (↑h : 𝕜) * c ≠ 0
field₈ : Ne.{u_4 + 1} (α := 𝕜) (↑h : 𝕜) 0
⊢ (a * (↑h : 𝕜)⁻¹ + c) / (b * (↑h : 𝕜)⁻¹ + d) = (a + c * (↑h : 𝕜)) / (b + d * (↑h : 𝕜))

Tactic:
field (discharger := norm_cast)
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Semifield 𝕜
inst_1 : CharZero 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
inst_4 : IsTopologicalSemiring 𝕜
inst_5 : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
apply : Tendsto (fun (k : ℕ) ↦ a * (↑k : 𝕜)⁻¹ + c) atTop (𝓝 c)
apply₁ : Tendsto (fun (k : ℕ) ↦ b * (↑k : 𝕜)⁻¹ + d) atTop (𝓝 d)
⊢ Tendsto (fun (k : ℕ) ↦ (a * (↑k : 𝕜)⁻¹ + c) / (b * (↑k : 𝕜)⁻¹ + d)) atTop (𝓝 (c / d))

Tactic:
apply Filter.Tendsto.div _ _ hd

Premises used: Filter.Tendsto.div
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Semifield 𝕜
inst_1 : CharZero 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
inst_4 : IsTopologicalSemiring 𝕜
inst_5 : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
apply : Tendsto.{0, u_4} (β := 𝕜) (fun (x : ℕ) ↦ a * (↑x : 𝕜)⁻¹) atTop (𝓝 0)
⊢ Tendsto (fun (k : ℕ) ↦ a * (↑k : 𝕜)⁻¹ + c) atTop (𝓝 c)

Tactic:
apply zero_add (_ : 𝕜) ▸ Filter.Tendsto.add_const _ _
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Semifield 𝕜
inst_1 : CharZero 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
inst_4 : IsTopologicalSemiring 𝕜
inst_5 : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
apply : Tendsto.{0, u_4} (β := 𝕜) (fun (x : ℕ) ↦ (↑x : 𝕜)⁻¹) atTop (𝓝 0)
⊢ Tendsto.{0, u_4} (β := 𝕜) (fun (x : ℕ) ↦ a * (↑x : 𝕜)⁻¹) atTop (𝓝 0)

Tactic:
apply mul_zero (_ : 𝕜) ▸ Filter.Tendsto.const_mul _ _
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Semifield 𝕜
inst_1 : CharZero 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
inst_4 : IsTopologicalSemiring 𝕜
inst_5 : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ Tendsto.{0, u_4} (β := 𝕜) (fun (x : ℕ) ↦ (↑x : 𝕜)⁻¹) atTop (𝓝 0)

Tactic:
tendsto_inv_atTop_nhds_zero_nat

Premises used: tendsto_inv_atTop_nhds_zero_nat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Semifield 𝕜
inst_1 : CharZero 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
inst_4 : IsTopologicalSemiring 𝕜
inst_5 : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ Tendsto.{0, u_4} (β := 𝕜) (fun (x : ℕ) ↦ (↑x : 𝕜)⁻¹) atTop (𝓝 0)

Tactic:
exact tendsto_inv_atTop_nhds_zero_nat

Premises used: tendsto_inv_atTop_nhds_zero_nat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Semifield 𝕜
inst_1 : CharZero 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
inst_4 : IsTopologicalSemiring 𝕜
inst_5 : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
apply : Tendsto.{0, u_4} (β := 𝕜) (fun (x : ℕ) ↦ b * (↑x : 𝕜)⁻¹) atTop (𝓝 0)
⊢ Tendsto (fun (k : ℕ) ↦ b * (↑k : 𝕜)⁻¹ + d) atTop (𝓝 d)

Tactic:
apply zero_add (_ : 𝕜) ▸ Filter.Tendsto.add_const _ _
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Semifield 𝕜
inst_1 : CharZero 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
inst_4 : IsTopologicalSemiring 𝕜
inst_5 : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
apply : Tendsto.{0, u_4} (β := 𝕜) (fun (x : ℕ) ↦ (↑x : 𝕜)⁻¹) atTop (𝓝 0)
⊢ Tendsto.{0, u_4} (β := 𝕜) (fun (x : ℕ) ↦ b * (↑x : 𝕜)⁻¹) atTop (𝓝 0)

Tactic:
apply mul_zero (_ : 𝕜) ▸ Filter.Tendsto.const_mul _ _
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
m : ℕ
hm : 0 < m
⊢ ∀ᶠ (n : ℕ) in atTop, LE.le (α := ℝ) 0 ((fun (n : ℕ) ↦ ((↑(n % m) : ℝ) : ℝ)) n)

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
m : ℕ
hm : 0 < m
⊢ ∀ᶠ (n : ℕ) in atTop, LE.le (α := ℝ) 0 ((fun (n : ℕ) ↦ ((↑(n % m) : ℝ) : ℝ)) n)

Tactic:
have h0 : ∀ᶠ n : ℕ in atTop, 0 ≤ (fun n : ℕ => ((n % m : ℕ) : ℝ)) n := by aesop
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
m : ℕ
hm : 0 < m
h0 : ∀ᶠ (n : ℕ) in atTop, LE.le (α := ℝ) 0 ((fun (n : ℕ) ↦ ((↑(n % m) : ℝ) : ℝ)) n)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(n % m) : ℝ) (↑n : ℝ)) atTop (𝓝 0)

Tactic:
tendsto_bdd_div_atTop_nhds_zero h0
    (.of_forall (fun n ↦ cast_le.mpr (mod_lt n hm).le)) tendsto_natCast_atTop_atTop

Premises used: Iff.mpr, tendsto_bdd_div_atTop_nhds_zero, LT.lt.le, Filter.Eventually.of_forall, Nat.mod_lt, tendsto_natCast_atTop_atTop, Nat.cast_le
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
m : ℕ
hm : 0 < m
h0 : ∀ᶠ (n : ℕ) in atTop, LE.le (α := ℝ) 0 ((fun (n : ℕ) ↦ ((↑(n % m) : ℝ) : ℝ)) n)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(n % m) : ℝ) (↑n : ℝ)) atTop (𝓝 0)

Tactic:
exact tendsto_bdd_div_atTop_nhds_zero h0
    (.of_forall (fun n ↦ cast_le.mpr (mod_lt n hm).le)) tendsto_natCast_atTop_atTop

Premises used: Iff.mpr, tendsto_bdd_div_atTop_nhds_zero, LT.lt.le, Filter.Eventually.of_forall, Nat.mod_lt, tendsto_natCast_atTop_atTop, Nat.cast_le
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
a c : ℝ
ha : a ≠ 0
inl : ∀ (ha' : a < 0), Tendsto (β := ℝ) (fun (x : ℝ) ↦ (a * x + c)⁻¹) atTop (𝓝 0)
inr : ∀ (ha' : 0 < a), Tendsto (β := ℝ) (fun (x : ℝ) ↦ (a * x + c)⁻¹) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ (a * x + c)⁻¹) atTop (𝓝 0)

Tactic:
obtain ha' | ha' := lt_or_gt_of_ne ha

Premises used: lt_or_gt_of_ne
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
a c : ℝ
ha : a ≠ 0
ha' : a < 0
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ (a * x + c)⁻¹) atTop (𝓝 0)

Tactic:
tendsto_inv_atBot_zero.comp
      (tendsto_atBot_add_const_right _ c (tendsto_id.const_mul_atTop_of_neg ha'))

Premises used: Filter.tendsto_id, tendsto_inv_atBot_zero, Filter.Tendsto.const_mul_atTop_of_neg, Filter.tendsto_atBot_add_const_right, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
a c : ℝ
ha : a ≠ 0
ha' : a < 0
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ (a * x + c)⁻¹) atTop (𝓝 0)

Tactic:
exact tendsto_inv_atBot_zero.comp
      (tendsto_atBot_add_const_right _ c (tendsto_id.const_mul_atTop_of_neg ha'))

Premises used: Filter.tendsto_id, tendsto_inv_atBot_zero, Filter.Tendsto.const_mul_atTop_of_neg, Filter.tendsto_atBot_add_const_right, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
a c : ℝ
ha : a ≠ 0
ha' : 0 < a
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ (a * x + c)⁻¹) atTop (𝓝 0)

Tactic:
tendsto_inv_atTop_zero.comp
      (tendsto_atTop_add_const_right _ c (tendsto_id.const_mul_atTop ha'))

Premises used: Filter.tendsto_atTop_add_const_right, tendsto_inv_atTop_zero, Filter.Tendsto.const_mul_atTop, Filter.tendsto_id, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
a c : ℝ
ha : a ≠ 0
ha' : 0 < a
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ (a * x + c)⁻¹) atTop (𝓝 0)

Tactic:
exact tendsto_inv_atTop_zero.comp
      (tendsto_atTop_add_const_right _ c (tendsto_id.const_mul_atTop ha'))

Premises used: Filter.tendsto_atTop_add_const_right, tendsto_inv_atTop_zero, Filter.Tendsto.const_mul_atTop, Filter.tendsto_id, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
α : Type u_4
G : Type u_5
inst : GroupWithZero G
f g : α → G
l : Filter α
hg : Tendsto g l (𝓟 {0}ᶜ)
h : ∀ (x : α) (hx : x ∈ g ⁻¹' {0}ᶜ), f x / g x * g x = f x
⊢ EventuallyEq.{u_4, u_5} (β := G) l (fun (x : α) ↦ f x / g x * g x) fun (x : α) ↦ f x

Tactic:
filter_upwards [hg.le_comap <| preimage_mem_comap (m := g) (mem_principal_self {0}ᶜ)] with x hx

Premises used: Filter.Tendsto.le_comap, Filter.mem_principal_self, Compl.compl, Filter.preimage_mem_comap, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
α : Type u_4
G : Type u_5
inst : GroupWithZero G
f g : α → G
l : Filter α
hg : Tendsto g l (𝓟 {0}ᶜ)
x : α
hx : x ∈ g ⁻¹' {0}ᶜ
⊢ f x / g x * g x = f x

Tactic:
simp_all
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
α : Type u_4
K : Type u_5
inst : DivisionSemiring K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
f g : α → K
l : Filter α
hg : Tendsto g l atTop
⊢ Subset (α := Set K) (Set.Ioi 0) {0}ᶜ

Tactic:
simp
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
α : Type u_4
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : TopologicalSpace K
inst_4 : OrderTopology K
f g : α → K
l : Filter α
hg : Tendsto g l atTop
a : K
ha : 0 < a
hlim : Tendsto (fun (x : α) ↦ f x / g x) l (𝓝 a)
⊢ Tendsto f l atTop

Tactic:
(hlim.pos_mul_atTop ha hg).congr' (EventuallyEq.div_mul_cancel_atTop hg)

Premises used: Filter.Tendsto.pos_mul_atTop, Filter.EventuallyEq.div_mul_cancel_atTop, Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
α : Type u_4
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : TopologicalSpace K
inst_4 : OrderTopology K
inst_5 : ContinuousInv K
f g : α → K
l : Filter α
hf : Tendsto f l atTop
a : K
ha : 0 < a
hlim : Tendsto (fun (x : α) ↦ f x / g x) l (𝓝 a)
simp_rw : Tendsto (fun (x : α) ↦ (f x / g x)⁻¹) l (𝓝 a⁻¹)
⊢ Tendsto (fun (x : α) ↦ g x / f x) l (𝓝 a⁻¹)

Tactic:
simp_rw [← inv_div (f _)]

Premises used: inv_div
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
α : Type u_4
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : TopologicalSpace K
inst_4 : OrderTopology K
inst_5 : ContinuousInv K
f g : α → K
l : Filter α
hf : Tendsto f l atTop
a : K
ha : 0 < a
hlim : Tendsto (fun (x : α) ↦ f x / g x) l (𝓝 a)
⊢ Tendsto (fun (x : α) ↦ (f x / g x)⁻¹) l (𝓝 a⁻¹)

Tactic:
Filter.Tendsto.inv (f := fun x => f x / g x) hlim

Premises used: Filter.Tendsto.inv
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
α : Type u_4
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : TopologicalSpace K
inst_4 : OrderTopology K
inst_5 : ContinuousInv K
f g : α → K
l : Filter α
hf : Tendsto f l atTop
a : K
ha : 0 < a
hlim : Tendsto (fun (x : α) ↦ f x / g x) l (𝓝 a)
⊢ Tendsto (fun (x : α) ↦ (f x / g x)⁻¹) l (𝓝 a⁻¹)

Tactic:
exact Filter.Tendsto.inv (f := fun x => f x / g x) hlim

Premises used: Filter.Tendsto.inv
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
α : Type u_4
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : TopologicalSpace K
inst_4 : OrderTopology K
inst_5 : ContinuousInv K
f g : α → K
l : Filter α
a : K
ha : 0 < a
hlim : Tendsto (fun (x : α) ↦ f x / g x) l (𝓝 a)
⊢ Tendsto f l atTop ↔ Tendsto g l atTop

Tactic:
⟨fun hf ↦ hf.den ha hlim, fun hg ↦ hg.num ha hlim⟩

Premises used: Filter.Tendsto.num, Filter.Tendsto.den, Iff.intro
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
α : Type u_1
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
r : α
h : 0 < r
⊢ Tendsto.{0, u_1} (β := α) (fun (n : ℕ) ↦ (r + 1) ^ n) atTop atTop

Tactic:
tendsto_atTop_atTop_of_monotone' (pow_right_mono₀ <| le_add_of_nonneg_left h.le) <|
    not_bddAbove_iff.2 fun _ ↦ Set.exists_range_iff.2 <| add_one_pow_unbounded_of_pos _ h

Premises used: Iff.mpr, LT.lt.le, add_one_pow_unbounded_of_pos, pow_right_mono₀, Filter.tendsto_atTop_atTop_of_monotone', Set.exists_range_iff, not_bddAbove_iff, le_add_of_nonneg_left
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
α : Type u_1
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
inst_4 : Archimedean α
r : α
h : 1 < r
obtain : ∀ (r : α) (r0 : 0 < r) (h : 1 < 1 + r), Tendsto.{0, u_1} (β := α) (fun (n : ℕ) ↦ (1 + r) ^ n) atTop atTop
⊢ Tendsto.{0, u_1} (β := α) (fun (n : ℕ) ↦ r ^ n) atTop atTop

Tactic:
obtain ⟨r, r0, rfl⟩ := exists_pos_add_of_lt' h

Premises used: exists_pos_add_of_lt', rfl
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
α : Type u_1
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
inst_4 : Archimedean α
r : α
r0 : 0 < r
h : 1 < 1 + r
rw : Tendsto.{0, u_1} (β := α) (fun (n : ℕ) ↦ (r + 1) ^ n) atTop atTop
⊢ Tendsto.{0, u_1} (β := α) (fun (n : ℕ) ↦ (1 + r) ^ n) atTop atTop

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
α : Type u_1
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
inst_4 : Archimedean α
r : α
r0 : 0 < r
h : 1 < 1 + r
⊢ Tendsto.{0, u_1} (β := α) (fun (n : ℕ) ↦ (r + 1) ^ n) atTop atTop

Tactic:
tendsto_add_one_pow_atTop_atTop_of_pos r0

Premises used: tendsto_add_one_pow_atTop_atTop_of_pos
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
α : Type u_1
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
inst_4 : Archimedean α
r : α
r0 : 0 < r
h : 1 < 1 + r
⊢ Tendsto.{0, u_1} (β := α) (fun (n : ℕ) ↦ (r + 1) ^ n) atTop atTop

Tactic:
exact tendsto_add_one_pow_atTop_atTop_of_pos r0

Premises used: tendsto_add_one_pow_atTop_atTop_of_pos
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : ExistsAddOfLE 𝕜
inst_4 : Archimedean 𝕜
inst_5 : TopologicalSpace 𝕜
inst_6 : OrderTopology 𝕜
r : 𝕜
h₁ : 0 ≤ r
h₂ : r < 1
hr : 0 = r
⊢ Tendsto.{0, u_4} (β := 𝕜) (fun (n : ℕ) ↦ r ^ (n + 1)) atTop (𝓝 0)

Tactic:
simp [_root_.pow_succ, ← hr]

Premises used: pow_succ
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : ExistsAddOfLE 𝕜
inst_4 : Archimedean 𝕜
inst_5 : TopologicalSpace 𝕜
inst_6 : OrderTopology 𝕜
r : 𝕜
h₁ : 0 ≤ r
h₂ : r < 1
hr : 0 < r
this : Tendsto.{0, u_4} (β := 𝕜) (fun (n : ℕ) ↦ r⁻¹ ^ n) atTop atTop
n : ℕ
⊢ ((fun (r : 𝕜) ↦ r⁻¹) ∘ fun (n : ℕ) ↦ r⁻¹ ^ n) n = r ^ n

Tactic:
simp
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
r : 𝕜
rw : Tendsto.{0, u_4} (α := ℕ) (β := 𝕜) (abs ∘ fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0) ↔ |r| < 1
⊢ Tendsto.{0, u_4} (β := 𝕜) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0) ↔ |r| < 1

Tactic:
rw [tendsto_zero_iff_abs_tendsto_zero]

Premises used: tendsto_zero_iff_abs_tendsto_zero
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
r : 𝕜
⊢ Tendsto.{0, u_4} (α := ℕ) (β := 𝕜) (abs ∘ fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0) ↔ |r| < 1

Tactic:
⟨fun h ↦ by_contra (fun hr_le ↦ ?_), fun h ↦ ?_⟩

Premises used: Iff.intro, by_contra
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
r : 𝕜
refine_1 : ∀ (h : Tendsto.{0, u_4} (α := ℕ) (β := 𝕜) (abs ∘ fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0)) (hr_le : ¬|r| < 1), False
refine_2 : ∀ (h : |r| < 1), Tendsto.{0, u_4} (α := ℕ) (β := 𝕜) (abs ∘ fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0)
⊢ Tendsto.{0, u_4} (α := ℕ) (β := 𝕜) (abs ∘ fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0) ↔ |r| < 1

Tactic:
refine ⟨fun h ↦ by_contra (fun hr_le ↦ ?_), fun h ↦ ?_⟩
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
r : 𝕜
h : Tendsto.{0, u_4} (α := ℕ) (β := 𝕜) (abs ∘ fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
pos : ∀ (hr : 1 = |r|), False
neg : ∀ (hr : ¬1 = |r|), False
⊢ False

Tactic:
by_cases hr : 1 = |r|
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
r : 𝕜
h : Tendsto.{0, u_4} (α := ℕ) (β := 𝕜) (abs ∘ fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : 1 = |r|
⊢ Tendsto.{0, u_4} (β := 𝕜) (fun (n : ℕ) ↦ |r| ^ n) atTop (𝓝 0)

Tactic:
simpa only [← abs_pow, h]

Premises used: abs_pow
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
r : 𝕜
h : Tendsto.{0, u_4} (α := ℕ) (β := 𝕜) (abs ∘ fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : 1 = |r|
⊢ Tendsto.{0, u_4} (β := 𝕜) (fun (n : ℕ) ↦ |r| ^ n) atTop (𝓝 0)

Tactic:
replace h : Tendsto (fun n : ℕ ↦ |r| ^ n) atTop (𝓝 0) := by simpa only [← abs_pow, h]
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
r : 𝕜
hr_le : ¬|r| < 1
hr : 1 = |r|
h : Tendsto.{0, u_4} (β := 𝕜) (fun (n : ℕ) ↦ |r| ^ n) atTop (𝓝 0)
⊢ Tendsto.{0, u_4} (β := 𝕜) (fun (n : ℕ) ↦ 1) atTop (𝓝 0)

Tactic:
simp only [hr.symm, one_pow] at h

Premises used: one_pow, Eq.symm
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
r : 𝕜
hr_le : ¬|r| < 1
hr : 1 = |r|
h : Tendsto.{0, u_4} (β := 𝕜) (fun (n : ℕ) ↦ 1) atTop (𝓝 0)
⊢ False

Tactic:
zero_ne_one <| tendsto_nhds_unique h tendsto_const_nhds

Premises used: tendsto_const_nhds, zero_ne_one, tendsto_nhds_unique
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
r : 𝕜
hr_le : ¬|r| < 1
hr : 1 = |r|
h : Tendsto.{0, u_4} (β := 𝕜) (fun (n : ℕ) ↦ 1) atTop (𝓝 0)
⊢ False

Tactic:
exact zero_ne_one <| tendsto_nhds_unique h tendsto_const_nhds

Premises used: tendsto_const_nhds, zero_ne_one, tendsto_nhds_unique