awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
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)
⊢ Tendsto.{0, u_4} (β := 𝕜) (fun (n : ℕ) ↦ (↑n : 𝕜) / ((↑n : 𝕜) + x)) atTop (𝓝 1)
have convert_6 : Tendsto.{0, u_4} (β := 𝕜) (fun (n : ℕ) ↦ 1 / (1 + x / (↑n : 𝕜))) atTop (𝓝 1)
Tactic: convert! Tendsto.congr' ((eventually_ne_atTop 0).mp (Eventually.of_forall fun n hn ↦ _)) _
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
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))
have rw : 𝓝 1 = 𝓝 (1 / HAdd.hAdd (α := 𝕜) 1 0)
Tactic: rw [mul_zero, add_zero, div_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
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)
⊢ 𝓝 1 = 𝓝 (1 / (1 + x * 0))
have rw₁ : 𝓝 1 = 𝓝 (1 / 1)
Tactic: rw [mul_zero, add_zero, div_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
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)
⊢ 𝓝 1 = 𝓝 (1 / (1 + x * 0))
have rw₂ : Eq.{u_4 + 1} (α := Filter 𝕜) (𝓝 1) (𝓝 1)
Tactic: rw [mul_zero, add_zero, div_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (hypothesis)
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 : ℕ) ↦ 1 / (1 + x / (↑n : 𝕜))) atTop (𝓝 1)
have this : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
Tactic: have : 𝓝 (1 : 𝕜) = 𝓝 (1 / (1 + x * (0 : 𝕜))) := by
      rw [mul_zero, add_zero, div_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
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.{0, u_4} (β := 𝕜) (fun (n : ℕ) ↦ 1 / (1 + x / (↑n : 𝕜))) atTop (𝓝 1)
have convert_6 : Tendsto (fun (n : ℕ) ↦ 1 / (1 + x / (↑n : 𝕜))) atTop (𝓝 (1 / (1 + x * 0)))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
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 : ℕ) ↦ 1 / (1 + x / (↑n : 𝕜))) atTop (𝓝 (1 / (1 + x * 0)))
have convert_6 : Tendsto (fun (n : ℕ) ↦ x / (↑n : 𝕜)) atTop (𝓝 (x * 0))
Tactic: refine tendsto_const_nhds.div (tendsto_const_nhds.add ?_) (by simp)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
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))
have convert_6 : Tendsto (fun (n : ℕ) ↦ x * (↑n : 𝕜)⁻¹) atTop (𝓝 (x * 0))
Tactic: simp_rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
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 (fun (k : ℕ) ↦ (a + c * (↑k : 𝕜)) / (b + d * (↑k : 𝕜))) atTop (𝓝 (c / d))
have hl : EventuallyEq.{0, u_4} (β := 𝕜) atTop (fun (k : ℕ) ↦ (a * (↑k : 𝕜)⁻¹ + c) / (b * (↑k : 𝕜)⁻¹ + d)) fun (k : ℕ) ↦
  (a + c * (↑k : 𝕜)) / (b + d * (↑k : 𝕜))
Tactic: apply Filter.Tendsto.congr'
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
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 : 𝕜))
⊢ Tendsto (fun (k : ℕ) ↦ (a + c * (↑k : 𝕜)) / (b + d * (↑k : 𝕜))) atTop (𝓝 (c / d))
have h : Tendsto (fun (k : ℕ) ↦ (a * (↑k : 𝕜)⁻¹ + c) / (b * (↑k : 𝕜)⁻¹ + d)) atTop (𝓝 (c / d))
Tactic: apply Filter.Tendsto.congr'
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
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))
⊢ Tendsto (fun (k : ℕ) ↦ (a + c * (↑k : 𝕜)) / (b + d * (↑k : 𝕜))) atTop (𝓝 (c / d))
have apply : ℕ → 𝕜
Tactic: apply Filter.Tendsto.congr'
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
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 : 𝕜))
have 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)
Tactic: refine (eventually_ne_atTop 0).mp (Eventually.of_forall ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
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
⊢ Ne.{u_4 + 1} (α := 𝕜) (↑h : 𝕜) 0
have norm_cast : ¬h = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
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
⊢ a + (↑h : 𝕜) * c ≠ 0
have norm_cast : ¬a + (↑h : 𝕜) * c = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
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
⊢ b + (↑h : 𝕜) * d ≠ 0
have norm_cast : ¬b + (↑h : 𝕜) * d = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
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
⊢ (a * (↑h : 𝕜)⁻¹ + c) / (b * (↑h : 𝕜)⁻¹ + d) = (a + c * (↑h : 𝕜)) / (b + d * (↑h : 𝕜))
have field : Ne.{u_4 + 1} (α := 𝕜) (↑h : 𝕜) 0
Tactic: field (discharger := norm_cast)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
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
⊢ (a * (↑h : 𝕜)⁻¹ + c) / (b * (↑h : 𝕜)⁻¹ + d) = (a + c * (↑h : 𝕜)) / (b + d * (↑h : 𝕜))
have field₃ : a + (↑h : 𝕜) * c ≠ 0
Tactic: field (discharger := norm_cast)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
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
⊢ (a * (↑h : 𝕜)⁻¹ + c) / (b * (↑h : 𝕜)⁻¹ + d) = (a + c * (↑h : 𝕜)) / (b + d * (↑h : 𝕜))
have field₅ : b + (↑h : 𝕜) * d ≠ 0
Tactic: field (discharger := norm_cast)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
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 (fun (k : ℕ) ↦ (a * (↑k : 𝕜)⁻¹ + c) / (b * (↑k : 𝕜)⁻¹ + d)) atTop (𝓝 (c / d))
have apply : Tendsto (fun (k : ℕ) ↦ a * (↑k : 𝕜)⁻¹ + c) atTop (𝓝 c)
Tactic: apply Filter.Tendsto.div _ _ hd
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
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)
⊢ Tendsto (fun (k : ℕ) ↦ (a * (↑k : 𝕜)⁻¹ + c) / (b * (↑k : 𝕜)⁻¹ + d)) atTop (𝓝 (c / d))
have apply₁ : Tendsto (fun (k : ℕ) ↦ b * (↑k : 𝕜)⁻¹ + d) atTop (𝓝 d)
Tactic: apply Filter.Tendsto.div _ _ hd
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
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 (fun (k : ℕ) ↦ a * (↑k : 𝕜)⁻¹ + c) atTop (𝓝 c)
have apply : Tendsto.{0, u_4} (β := 𝕜) (fun (x : ℕ) ↦ a * (↑x : 𝕜)⁻¹) atTop (𝓝 0)
Tactic: apply zero_add (_ : 𝕜) ▸ Filter.Tendsto.add_const _ _
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
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 : ℕ) ↦ a * (↑x : 𝕜)⁻¹) atTop (𝓝 0)
have apply : Tendsto.{0, u_4} (β := 𝕜) (fun (x : ℕ) ↦ (↑x : 𝕜)⁻¹) atTop (𝓝 0)
Tactic: apply mul_zero (_ : 𝕜) ▸ Filter.Tendsto.const_mul _ _
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
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 (fun (k : ℕ) ↦ b * (↑k : 𝕜)⁻¹ + d) atTop (𝓝 d)
have apply : Tendsto.{0, u_4} (β := 𝕜) (fun (x : ℕ) ↦ b * (↑x : 𝕜)⁻¹) atTop (𝓝 0)
Tactic: apply zero_add (_ : 𝕜) ▸ Filter.Tendsto.add_const _ _
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
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 : ℕ) ↦ b * (↑x : 𝕜)⁻¹) atTop (𝓝 0)
have apply : Tendsto.{0, u_4} (β := 𝕜) (fun (x : ℕ) ↦ (↑x : 𝕜)⁻¹) atTop (𝓝 0)
Tactic: apply mul_zero (_ : 𝕜) ▸ Filter.Tendsto.const_mul _ _
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (hypothesis)
Goal:
m : ℕ
hm : 0 < m
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(n % m) : ℝ) (↑n : ℝ)) atTop (𝓝 0)
have h0 : ∀ᶠ (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
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
a c : ℝ
ha : a ≠ 0
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ (a * x + c)⁻¹) atTop (𝓝 0)
have inl : ∀ (ha' : a < 0), Tendsto (β := ℝ) (fun (x : ℝ) ↦ (a * x + c)⁻¹) atTop (𝓝 0)
Tactic: obtain ha' | ha' := lt_or_gt_of_ne ha
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
a c : ℝ
ha : a ≠ 0
inl : ∀ (ha' : a < 0), Tendsto (β := ℝ) (fun (x : ℝ) ↦ (a * x + c)⁻¹) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ (a * x + c)⁻¹) atTop (𝓝 0)
have inr : ∀ (ha' : 0 < a), Tendsto (β := ℝ) (fun (x : ℝ) ↦ (a * x + c)⁻¹) atTop (𝓝 0)
Tactic: obtain ha' | ha' := lt_or_gt_of_ne ha
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
α : Type u_4
G : Type u_5
inst : GroupWithZero G
f g : α → G
l : Filter α
hg : Tendsto g l (𝓟 {0}ᶜ)
⊢ EventuallyEq.{u_4, u_5} (β := G) l (fun (x : α) ↦ f x / g x * g x) fun (x : α) ↦ f x
have h : ∀ (x : α) (hx : x ∈ g ⁻¹' {0}ᶜ), f x / g x * g x = f x
Tactic: filter_upwards [hg.le_comap <| preimage_mem_comap (m := g) (mem_principal_self {0}ᶜ)] with x hx
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
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 : α) ↦ g x / f x) l (𝓝 a⁻¹)
have simp_rw : Tendsto (fun (x : α) ↦ (f x / g x)⁻¹) l (𝓝 a⁻¹)
Tactic: simp_rw [← inv_div (f _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
α : Type u_1
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
inst_4 : Archimedean α
r : α
h : 1 < r
⊢ Tendsto.{0, u_1} (β := α) (fun (n : ℕ) ↦ r ^ n) atTop atTop
have obtain : ∀ (r : α) (r0 : 0 < r) (h : 1 < 1 + r), Tendsto.{0, u_1} (β := α) (fun (n : ℕ) ↦ (1 + r) ^ n) atTop atTop
Tactic: obtain ⟨r, r0, rfl⟩ := exists_pos_add_of_lt' h
Cleared hypotheses: r, h
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
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 : ℕ) ↦ (1 + r) ^ n) atTop atTop
have rw : Tendsto.{0, u_1} (β := α) (fun (n : ℕ) ↦ (r + 1) ^ n) atTop atTop
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
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} (β := 𝕜) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0) ↔ |r| < 1
have rw : Tendsto.{0, u_4} (α := ℕ) (β := 𝕜) (abs ∘ fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0) ↔ |r| < 1
Tactic: rw [tendsto_zero_iff_abs_tendsto_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
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
have refine_1 : ∀ (h : Tendsto.{0, u_4} (α := ℕ) (β := 𝕜) (abs ∘ fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0)) (hr_le : ¬|r| < 1), False
Tactic: refine ⟨fun h ↦ by_contra (fun hr_le ↦ ?_), fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
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
⊢ Tendsto.{0, u_4} (α := ℕ) (β := 𝕜) (abs ∘ fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0) ↔ |r| < 1
have refine_2 : ∀ (h : |r| < 1), Tendsto.{0, u_4} (α := ℕ) (β := 𝕜) (abs ∘ fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0)
Tactic: refine ⟨fun h ↦ by_contra (fun hr_le ↦ ?_), fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
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
⊢ False
have pos : ∀ (hr : 1 = |r|), False
Tactic: by_cases hr : 1 = |r|
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
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
⊢ False
have neg : ∀ (hr : ¬1 = |r|), False
Tactic: by_cases hr : 1 = |r|
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (hypothesis)
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|
⊢ False
have h₁ : 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]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (hypothesis)
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)
⊢ False
have h₁ : Tendsto.{0, u_4} (β := 𝕜) (fun (n : ℕ) ↦ 1) atTop (𝓝 0)
Tactic: simp only [hr.symm, one_pow] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
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|
⊢ False
have apply : Tendsto.{0, u_4} (β := 𝕜) (fun (n : ℕ) ↦ |r| ^ n) atTop atTop
Tactic: apply @not_tendsto_nhds_of_tendsto_atTop 𝕜 ℕ _ _ _ _ atTop _ (fun n ↦ |r| ^ n) _ 0 _
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
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|
apply : Tendsto.{0, u_4} (β := 𝕜) (fun (n : ℕ) ↦ |r| ^ n) atTop atTop
⊢ False
have apply₁ : Tendsto.{0, u_4} (β := 𝕜) (fun (n : ℕ) ↦ |r| ^ n) atTop (𝓝 0)
Tactic: apply @not_tendsto_nhds_of_tendsto_atTop 𝕜 ℕ _ _ _ _ atTop _ (fun n ↦ |r| ^ n) _ 0 _
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
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 atTop
have refine : ∀ (b : 𝕜), ∃ (a : ℕ), b ≤ |r| ^ a
Tactic: refine (pow_right_strictMono₀ <| lt_of_le_of_ne (le_of_not_gt hr_le)
          hr).monotone.tendsto_atTop_atTop (fun b ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
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|
b : 𝕜
⊢ ∃ (a : ℕ), b ≤ |r| ^ a
have obtain : ∀ (n : ℕ) (hn : b < |r| ^ n), ∃ (a : ℕ), b ≤ |r| ^ a
Tactic: obtain ⟨n, hn⟩ := (pow_unbounded_of_one_lt b (lt_of_le_of_ne (le_of_not_gt hr_le) hr))
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ k < n, c * u k < u (k + 1)
⊢ c ^ n * u 0 < u n
have apply : HPow.hPow (β := ℕ) c 0 * u 0 ≤ u 0
Tactic: apply (monotone_mul_left_of_nonneg hc).seq_pos_lt_seq_of_le_of_lt hn _ _ h
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ k < n, c * u k < u (k + 1)
apply : HPow.hPow (β := ℕ) c 0 * u 0 ≤ u 0
⊢ c ^ n * u 0 < u n
have apply₁ : ∀ k < n, c ^ (k + 1) * u 0 ≤ c * (c ^ k * u 0)
Tactic: apply (monotone_mul_left_of_nonneg hc).seq_pos_lt_seq_of_le_of_lt hn _ _ h
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
h : ∀ k < n, c * u k ≤ u (k + 1)
⊢ c ^ n * u 0 ≤ u n
have apply : HPow.hPow (β := ℕ) c 0 * u 0 ≤ u 0
Tactic: apply (monotone_mul_left_of_nonneg hc).seq_le_seq n _ _ h
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
h : ∀ k < n, c * u k ≤ u (k + 1)
apply : HPow.hPow (β := ℕ) c 0 * u 0 ≤ u 0
⊢ c ^ n * u 0 ≤ u n
have apply₁ : ∀ k < n, c ^ (k + 1) * u 0 ≤ c * (c ^ k * u 0)
Tactic: apply (monotone_mul_left_of_nonneg hc).seq_le_seq n _ _ h
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ k < n, u (k + 1) < c * u k
⊢ u n < c ^ n * u 0
have apply : u 0 ≤ HPow.hPow (β := ℕ) c 0 * u 0
Tactic: apply (monotone_mul_left_of_nonneg hc).seq_pos_lt_seq_of_lt_of_le hn _ h _
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ k < n, u (k + 1) < c * u k
apply : u 0 ≤ HPow.hPow (β := ℕ) c 0 * u 0
⊢ u n < c ^ n * u 0
have apply₁ : ∀ k < n, c * (c ^ k * u 0) ≤ c ^ (k + 1) * u 0
Tactic: apply (monotone_mul_left_of_nonneg hc).seq_pos_lt_seq_of_lt_of_le hn _ h _
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
h : ∀ k < n, u (k + 1) ≤ c * u k
⊢ u n ≤ c ^ n * u 0
have apply : u 0 ≤ HPow.hPow (β := ℕ) c 0 * u 0
Tactic: apply (monotone_mul_left_of_nonneg hc).seq_le_seq n _ h _
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
h : ∀ k < n, u (k + 1) ≤ c * u k
apply : u 0 ≤ HPow.hPow (β := ℕ) c 0 * u 0
⊢ u n ≤ c ^ n * u 0
have apply₁ : ∀ k < n, c * (c ^ k * u 0) ≤ c ^ (k + 1) * u 0
Tactic: apply (monotone_mul_left_of_nonneg hc).seq_le_seq n _ h _
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
r : ℝ≥0∞
hr : r < 1
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0)
have rcases : ∀ (r : ℝ≥0) (hr' hr : (↑r : ℝ≥0∞) < 1), Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (↑r : ℝ≥0∞) ^ n) atTop (𝓝 0)
Tactic: rcases ENNReal.lt_iff_exists_coe.1 hr with ⟨r, rfl, hr'⟩
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
r : ℝ≥0
hr' hr : (↑r : ℝ≥0∞) < 1
⊢ Tendsto (fun (n : ℕ) ↦ (↑r : ℝ≥0∞) ^ n) atTop (𝓝 (↑0 : ℝ≥0∞))
have norm_cast : ∀ (hr' hr : r < 1), Tendsto (α := ℕ) (HPow.hPow r) atTop (𝓝 0)
Tactic: norm_cast at *
Cleared hypotheses: hr', hr
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
r : ℝ≥0∞
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0) ↔ r < 1
have refine : ∀ (h : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0)), r < 1
Tactic: refine ⟨fun h ↦ ?_, tendsto_pow_atTop_nhds_zero_of_lt_one⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
r : ℝ≥0∞
h : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0)
⊢ r < 1
have lift : r ≠ ∞
Tactic: lift r to NNReal