awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
ι : Type u_1
inst : Fintype ι
f : (ι → ℝ × ℝ) → ℝ≥0∞
x : (i : ι) → ℝ × ℝ
hx :
  Membership.mem (γ := Set ((i : ι) → ℝ × ℝ))
    (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target) x
h :
  ((∏ i : ι, ENNReal.ofReal (x i).1) * f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)) =
    ENNReal.ofReal |∏ i : ι, (x i).1| * f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)
⊢ ((∏ i : ι, ENNReal.ofReal (x i).1) * f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)) =
    ENNReal.ofReal |(fderivPiPolarCoordSymm x).det| * f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)
have h₁ : ((∏ i : ι, ENNReal.ofReal (x i).1) * f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)) =
  ENNReal.ofReal (∏ x_1 : ι, |(x x_1).1|) * f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)
Tactic: simp_rw [det_fderivPiPolarCoordSymm, Finset.abs_prod, ENNReal.ofReal_prod_of_nonneg (fun _ _ ↦
    abs_nonneg _), abs_fst_of_mem_pi_polarCoord_target hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
ι : Type u_1
inst : Fintype ι
f : (ι → ℝ × ℝ) → ℝ≥0∞
x : (i : ι) → ℝ × ℝ
hx :
  Membership.mem (γ := Set ((i : ι) → ℝ × ℝ))
    (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target) x
h :
  ((∏ i : ι, ENNReal.ofReal (x i).1) * f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)) =
    ENNReal.ofReal |∏ i : ι, (x i).1| * f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)
h₁ :
  ((∏ i : ι, ENNReal.ofReal (x i).1) * f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)) =
    ENNReal.ofReal (∏ x_1 : ι, |(x x_1).1|) * f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)
⊢ ((∏ i : ι, ENNReal.ofReal (x i).1) * f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)) =
    ENNReal.ofReal |(fderivPiPolarCoordSymm x).det| * f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)
have h₂ : ((∏ i : ι, ENNReal.ofReal (x i).1) * f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)) =
  (∏ i : ι, ENNReal.ofReal |(x i).1|) * f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)
Tactic: simp_rw [det_fderivPiPolarCoordSymm, Finset.abs_prod, ENNReal.ofReal_prod_of_nonneg (fun _ _ ↦
    abs_nonneg _), abs_fst_of_mem_pi_polarCoord_target hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
f : (ι → ℂ) → ℝ≥0∞
e : ((a : ι) → ℝ × ℝ) ≃ᵐ ((a : ι) → ℂ) :=
  MeasurableEquiv.piCongrRight (π := fun (x : ι) ↦ ℝ × ℝ) (π' := fun (x : ι) ↦ ℂ) fun (x : ι) ↦
    measurableEquivRealProd.symm
⊢ (∫⁻ (p : (i : ι) → ℝ × ℝ) in Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ Complex.polarCoord.target,
      (∏ i : ι, ENNReal.ofReal (p i).1) * f fun (i : ι) ↦ (↑Complex.polarCoord.symm : ℝ × ℝ → ℂ) (p i)) =
    ∫⁻ (p : ι → ℂ), f p
have this : MeasurePreserving (β := (i : ι) → ℂ)
  (fun (a : (i : ι) → ℝ × ℝ) (i : ι) ↦ (measurableEquivRealProd.symm : (a : ℝ × ℝ) → ℂ) (a i))
  (volume : Measure ((i : ι) → ℝ × ℝ)) (volume : Measure ((i : ι) → ℂ))
Tactic: have := volume_preserving_pi (fun _ : ι ↦ Complex.volume_preserving_equiv_real_prod.symm)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
ι : Type u_1
inst : Fintype ι
f : (ι → ℂ) → ℝ≥0∞
e : ((a : ι) → ℝ × ℝ) ≃ᵐ ((a : ι) → ℂ) :=
  MeasurableEquiv.piCongrRight (π := fun (x : ι) ↦ ℝ × ℝ) (π' := fun (x : ι) ↦ ℂ) fun (x : ι) ↦
    measurableEquivRealProd.symm
this :
  MeasurePreserving (β := (i : ι) → ℂ)
    (fun (a : (i : ι) → ℝ × ℝ) (i : ι) ↦ (measurableEquivRealProd.symm : (a : ℝ × ℝ) → ℂ) (a i))
    (volume : Measure ((i : ι) → ℝ × ℝ)) (volume : Measure ((i : ι) → ℂ))
⊢ (∫⁻ (p : (i : ι) → ℝ × ℝ) in Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ Complex.polarCoord.target,
      (∏ i : ι, ENNReal.ofReal (p i).1) * f fun (i : ι) ↦ (↑Complex.polarCoord.symm : ℝ × ℝ → ℂ) (p i)) =
    ∫⁻ (p : ι → ℂ), f p
have rw : (∫⁻ (p : (i : ι) → ℝ × ℝ) in Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ Complex.polarCoord.target,
    (∏ i : ι, ENNReal.ofReal (p i).1) * f fun (i : ι) ↦ (↑Complex.polarCoord.symm : ℝ × ℝ → ℂ) (p i)) =
  ∫⁻ (a : (i : ι) → ℝ × ℝ),
    f fun (i : ι) ↦ (measurableEquivRealProd.symm : (a : ℝ × ℝ) → ℂ) (a i) ∂(volume : Measure ((i : ι) → ℝ × ℝ))
Tactic: rw [← MeasurePreserving.lintegral_comp_emb this e.measurableEmbedding]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolynomialExp (goal)
Goal:
p : ℝ[X]
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ eval x p / rexp x) atTop (𝓝 0)
have monomial : ∀ (n : ℕ) (c : ℝ), Tendsto (β := ℝ) (fun (x : ℝ) ↦ eval x ((monomial n : (a : ℝ) → ℝ[X]) c) / rexp x) atTop (𝓝 0)
Tactic: induction p using Polynomial.induction_on' with
  | monomial n c => simpa [exp_neg, div_eq_mul_inv, mul_assoc]
    using tendsto_const_nhds.mul (tendsto_pow_mul_exp_neg_atTop_nhds_zero n)
  | add p q hp hq => simpa [add_div] using hp.add hq
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolynomialExp (goal)
Goal:
p : ℝ[X]
monomial :
  ∀ (n : ℕ) (c : ℝ),
    Tendsto (β := ℝ) (fun (x : ℝ) ↦ eval x ((Polynomial.monomial n : (a : ℝ) → ℝ[X]) c) / rexp x) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ eval x p / rexp x) atTop (𝓝 0)
have add : ∀ (p q : ℝ[X]) (hp : Tendsto (β := ℝ) (fun (x : ℝ) ↦ eval x p / rexp x) atTop (𝓝 0))
  (hq : Tendsto (β := ℝ) (fun (x : ℝ) ↦ eval x q / rexp x) atTop (𝓝 0)),
  Tendsto (β := ℝ) (fun (x : ℝ) ↦ eval x (p + q) / rexp x) atTop (𝓝 0)
Tactic: induction p using Polynomial.induction_on' with
  | monomial n c => simpa [exp_neg, div_eq_mul_inv, mul_assoc]
    using tendsto_const_nhds.mul (tendsto_pow_mul_exp_neg_atTop_nhds_zero n)
  | add p q hp hq => simpa [add_div] using hp.add hq
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
y : ℝ
hy : 0 < y
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ y) atTop atTop
have rw : ∀ (i : ℝ), 0 ≤ i → ∀ᶠ (x : ℝ) in atTop, x ^ y ∈ Set.Ici i
Tactic: rw [(atTop_basis' 0).tendsto_right_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
y : ℝ
hy : 0 < y
b : ℝ
hb : 0 ≤ b
⊢ ∀ᶠ (x : ℝ) in atTop, x ^ y ∈ Set.Ici b
have h : ∀ (x : ℝ) (hx₀ : 0 ≤ x) (hx : b ^ (1 / y) ≤ x), x ^ y ∈ Set.Ici b
Tactic: filter_upwards [eventually_ge_atTop 0, eventually_ge_atTop (b ^ (1 / y))] with x hx₀ hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
y : ℝ
hr : y < 0
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ y) (𝓝[>] 0) atTop
have simp_rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x⁻¹ ^ (-y)) (𝓝[>] 0) atTop
Tactic: simp_rw +singlePass [← neg_neg y, Real.rpow_neg_eq_inv_rpow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ b ^ x) atTop (𝓝 0)
have rcases : ∀ (hb : b < 0), Tendsto (β := ℝ) (fun (x : ℝ) ↦ b ^ x) atTop (𝓝 0)
Tactic: rcases lt_trichotomy b 0 with hb | rfl | hb
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
rcases : ∀ (hb : b < 0), Tendsto (β := ℝ) (fun (x : ℝ) ↦ b ^ x) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ b ^ x) atTop (𝓝 0)
have rcases₁ : ∀ (hb₀ : LT.lt (α := ℝ) (-1) 0) (hb₁ : LT.lt (α := ℝ) 0 1),
  Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 0 x) atTop (𝓝 0)
Tactic: rcases lt_trichotomy b 0 with hb | rfl | hb
Cleared hypotheses: b, hb₀, hb₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
rcases : ∀ (hb : b < 0), Tendsto (β := ℝ) (fun (x : ℝ) ↦ b ^ x) atTop (𝓝 0)
rcases₁ :
  ∀ (hb₀ : LT.lt (α := ℝ) (-1) 0) (hb₁ : LT.lt (α := ℝ) 0 1),
    Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 0 x) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ b ^ x) atTop (𝓝 0)
have rcases₂ : ∀ (hb : 0 < b), Tendsto (β := ℝ) (fun (x : ℝ) ↦ b ^ x) atTop (𝓝 0)
Tactic: rcases lt_trichotomy b 0 with hb | rfl | hb
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ b ^ x) atTop (𝓝 0)
have simp_rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (log b * x) * cos (x * π)) atTop (𝓝 0)
Tactic: simp_rw [Real.rpow_def_of_nonpos hb.le, hb.ne, ite_false]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (log b * x) * cos (x * π)) atTop (𝓝 0)
have rw : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (log b * x) * cos (x * π)) fun (_x : ℝ) ↦ HMul.hMul (α := ℝ) 1 1
Tactic: rw [← isLittleO_const_iff (c := (1 : ℝ)) one_ne_zero, (one_mul (1 : ℝ)).symm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (log b * x) * cos (x * π)) fun (_x : ℝ) ↦ HMul.hMul (α := ℝ) 1 1
have refine : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (log b * x)) fun (_x : ℝ) ↦ 1
Tactic: refine IsLittleO.mul_isBigO ?exp ?cos
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
refine : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (log b * x)) fun (_x : ℝ) ↦ 1
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (log b * x) * cos (x * π)) fun (_x : ℝ) ↦ HMul.hMul (α := ℝ) 1 1
have refine₁ : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ cos (x * π)) fun (_x : ℝ) ↦ 1
Tactic: refine IsLittleO.mul_isBigO ?exp ?cos
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (log b * x)) fun (_x : ℝ) ↦ 1
have rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (log b * x)) atTop (𝓝 0)
Tactic: rw [isLittleO_const_iff one_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (log b * x)) atTop (𝓝 0)
have refine : log b < 0
Tactic: refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_neg ?_).mpr tendsto_id
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ 0 < -b
have linarith : -b ≤ 0 → b - 0 + (-b - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ log b < 0
have rw : -b < 1
Tactic: rw [← log_neg_eq_log, log_neg_iff (by linarith)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ -b < 1
have linarith : 1 ≤ -b → -1 - b + (1 - -b) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ cos (x * π)) fun (_x : ℝ) ↦ 1
have rw : ∃ (c : ℝ), ∀ᶠ (x : ℝ) in atTop, ‖cos (x * π)‖ ≤ c * Norm.norm (E := ℝ) 1
Tactic: rw [isBigO_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ cos (x * π)) fun (_x : ℝ) ↦ 1
have case : ∃ (c : ℝ), ∀ᶠ (x : ℝ) in atTop, ‖cos (x * π)‖ ≤ c * Norm.norm (E := ℝ) 1
Tactic: case cos =>
      rw [isBigO_iff]
      exact ⟨1, Eventually.of_forall fun x => by simp [Real.abs_cos_le_one]⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
hb₀ : LT.lt (α := ℝ) (-1) 0
hb₁ : LT.lt (α := ℝ) 0 1
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 0 x) atTop (𝓝 0)
have refine : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 0 x) atTop (pure 0)
Tactic: refine Tendsto.mono_right ?_ (Iff.mpr pure_le_nhds_iff rfl)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
hb₀ : LT.lt (α := ℝ) (-1) 0
hb₁ : LT.lt (α := ℝ) 0 1
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 0 x) atTop (pure 0)
have rw : ∀ᶠ (x : ℝ) in atTop, HPow.hPow (α := ℝ) 0 x = 0
Tactic: rw [tendsto_pure]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
hb₀ : LT.lt (α := ℝ) (-1) 0
hb₁ : LT.lt (α := ℝ) 0 1
⊢ ∀ᶠ (x : ℝ) in atTop, HPow.hPow (α := ℝ) 0 x = 0
have h : ∀ (a : ℝ) (hx : a ≠ 0), HPow.hPow (α := ℝ) 0 a = 0
Tactic: filter_upwards [eventually_ne_atTop 0] with _ hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ b ^ x) atTop (𝓝 0)
have simp_rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (log b * x)) atTop (𝓝 0)
Tactic: simp_rw [Real.rpow_def_of_pos hb]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (log b * x)) atTop (𝓝 0)
have refine : log b < 0
Tactic: refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_neg ?_).mpr tendsto_id
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ b ^ x) atTop (𝓝 0)
have case : Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (log b * x)) atTop (𝓝 0)
Tactic: case inr.inr => -- b > 0
    simp_rw [Real.rpow_def_of_pos hb]
    refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_neg ?_).mpr tendsto_id
    exact (log_neg_iff hb).mpr hb₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
case : Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (log b * x)) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ b ^ x) atTop (𝓝 0)
have case₁ : log b < 0
Tactic: case inr.inr => -- b > 0
    simp_rw [Real.rpow_def_of_pos hb]
    refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_neg ?_).mpr tendsto_id
    exact (log_neg_iff hb).mpr hb₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ b ^ x) atBot atTop
have simp_rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (log b * x)) atBot atTop
Tactic: simp_rw [Real.rpow_def_of_pos (by positivity : 0 < b)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (log b * x)) atBot atTop
have refine : log b < 0
Tactic: refine tendsto_exp_atTop.comp <| (tendsto_const_mul_atTop_iff_neg <| tendsto_id (α := ℝ)).mpr ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
b : ℝ
hb : 1 < b
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ b ^ x) atBot (𝓝 0)
have simp_rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (log b * x)) atBot (𝓝 0)
Tactic: simp_rw [Real.rpow_def_of_pos (by positivity : 0 < b)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
b : ℝ
hb : 1 < b
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (log b * x)) atBot (𝓝 0)
have refine : 0 < log b
Tactic: refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_pos ?_).mpr tendsto_id
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
a b c : ℝ
hb : 0 ≠ b
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ (a / (b * x + c))) atTop (𝓝 1)
have simpa : (rexp ∘ fun (x : ℝ) ↦ a * (x / (b * rexp x + c))) ∘ log =ᶠ[atTop] fun (x : ℝ) ↦ x ^ (a / (b * x + c))
Tactic: refine
    Tendsto.congr' ?_
      ((tendsto_exp_nhds_zero_nhds_one.comp
            (by
              simpa only [mul_zero, pow_one] using
                (tendsto_const_nhds (x := a)).mul
                  (tendsto_div_pow_mul_exp_add_atTop b c 1 hb))).comp
        tendsto_log_atTop)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
a b c : ℝ
hb : 0 ≠ b
⊢ (rexp ∘ fun (x : ℝ) ↦ a * (x / (b * rexp x + c))) ∘ log =ᶠ[atTop] fun (x : ℝ) ↦ x ^ (a / (b * x + c))
have apply : EqOn ((rexp ∘ fun (x : ℝ) ↦ a * (x / (b * rexp x + c))) ∘ log) (fun (x : ℝ) ↦ x ^ (a / (b * x + c))) (Set.Ioi 0)
Tactic: apply eventuallyEq_of_mem (Ioi_mem_atTop (0 : ℝ))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (hypothesis)
Goal:
a b c : ℝ
hb : 0 ≠ b
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioi 0) x
⊢ ((rexp ∘ fun (x : ℝ) ↦ a * (x / (b * rexp x + c))) ∘ log) x = (fun (x : ℝ) ↦ x ^ (a / (b * x + c))) x
have hx₁ : 0 < x
Tactic: simp only [Set.mem_Ioi, Function.comp_apply] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
a b c : ℝ
hb : 0 ≠ b
x : ℝ
hx : 0 < x
⊢ rexp (a * (log x / (b * rexp (log x) + c))) = x ^ (a / (b * x + c))
have rw : rexp (a * (log x / (b * x + c))) = rexp (a / (b * x + c) * log x)
Tactic: rw [exp_log hx, ← exp_log (rpow_pos_of_pos hx (a / (b * x + c))), log_rpow hx (a / (b * x + c))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ (1 / x)) atTop (𝓝 1)
have h : ∀ (x : ℝ), x = 1 * x + 0
Tactic: convert! tendsto_rpow_div_mul_add (1 : ℝ) _ (0 : ℝ) zero_ne_one
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ (-1 / x)) atTop (𝓝 1)
have h : ∀ (x : ℝ), x = 1 * x + 0
Tactic: convert! tendsto_rpow_div_mul_add (-(1 : ℝ)) _ (0 : ℝ) zero_ne_one
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
s : ℝ
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp x / x ^ s) atTop atTop
have obtain : ∀ (n : ℕ) (hn : s < (↑n : ℝ)), Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp x / x ^ s) atTop atTop
Tactic: obtain ⟨n, hn⟩ := archimedean_iff_nat_lt.1 Real.instArchimedean s
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
s : ℝ
n : ℕ
hn : s < (↑n : ℝ)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp x / x ^ s) atTop atTop
have refine : EventuallyLE (β := ℝ) atTop (fun (x : ℝ) ↦ rexp x / x ^ n) fun (x : ℝ) ↦ rexp x / x ^ s
Tactic: refine tendsto_atTop_mono' _ ?_ (tendsto_exp_div_pow_atTop n)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
s : ℝ
n : ℕ
hn : s < (↑n : ℝ)
⊢ EventuallyLE (β := ℝ) atTop (fun (x : ℝ) ↦ rexp x / x ^ n) fun (x : ℝ) ↦ rexp x / x ^ s
have h : ∀ (x : ℝ) (hx₀ : 0 < x) (hx₁ : 1 ≤ x), rexp x / x ^ n ≤ rexp x / x ^ s
Tactic: filter_upwards [eventually_gt_atTop (0 : ℝ), eventually_ge_atTop (1 : ℝ)] with x hx₀ hx₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
s : ℝ
n : ℕ
hn : s < (↑n : ℝ)
x : ℝ
hx₀ : 0 < x
hx₁ : 1 ≤ x
⊢ rexp x / x ^ n ≤ rexp x / x ^ s
have h : x ^ s ≤ x ^ n
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
s b : ℝ
hb : 0 < b
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (b * x) / x ^ s) atTop atTop
have refine : EventuallyEq (β := ℝ) atTop ((fun (x : ℝ) ↦ x ^ b) ∘ fun (x : ℝ) ↦ rexp x / x ^ (s / b)) fun (x : ℝ) ↦
  rexp (b * x) / x ^ s
Tactic: refine ((tendsto_rpow_atTop hb).comp (tendsto_exp_div_rpow_atTop (s / b))).congr' ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
s b : ℝ
hb : 0 < b
⊢ EventuallyEq (β := ℝ) atTop ((fun (x : ℝ) ↦ x ^ b) ∘ fun (x : ℝ) ↦ rexp x / x ^ (s / b)) fun (x : ℝ) ↦
    rexp (b * x) / x ^ s
have h : ∀ (x : ℝ) (hx₀ : 0 ≤ x), ((fun (x : ℝ) ↦ x ^ b) ∘ fun (x : ℝ) ↦ rexp x / x ^ (s / b)) x = rexp (b * x) / x ^ s
Tactic: filter_upwards [eventually_ge_atTop (0 : ℝ)] with x hx₀
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
s b : ℝ
hb : 0 < b
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ s * rexp (-b * x)) atTop (𝓝 0)
have refine : EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ rexp (b * x) / x ^ s)⁻¹ fun (x : ℝ) ↦ x ^ s * rexp (-b * x)
Tactic: refine (tendsto_exp_mul_div_rpow_atTop s b hb).inv_tendsto_atTop.congr' ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
s b : ℝ
hb : 0 < b
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ rexp (b * x) / x ^ s)⁻¹ fun (x : ℝ) ↦ x ^ s * rexp (-b * x)
have h : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      (fun (x : ℝ) ↦ Eq (α := ℝ) ((fun (x : ℝ) ↦ rexp (b * x) / x ^ s)⁻¹ x) ((fun (x : ℝ) ↦ x ^ s * rexp (-b * x)) x))
        x}
    a
Tactic: filter_upwards with x using by simp [exp_neg, inv_div, div_eq_mul_inv _ (exp _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
s b : ℝ
hb : 0 < b
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        (fun (x : ℝ) ↦ Eq (α := ℝ) ((fun (x : ℝ) ↦ rexp (b * x) / x ^ s)⁻¹ x) ((fun (x : ℝ) ↦ x ^ s * rexp (-b * x)) x))
          x}
      a
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ rexp (b * x) / x ^ s)⁻¹ fun (x : ℝ) ↦ x ^ s * rexp (-b * x)
have h₁ : ∀ (a : ℝ), (fun (x : ℝ) ↦ rexp (b * x) / x ^ s)⁻¹ a = a ^ s * rexp (-b * a)
Tactic: filter_upwards with x using by simp [exp_neg, inv_div, div_eq_mul_inv _ (exp _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
y : ℝ
hy : 0 < y
⊢ Tendsto (β := ℝ≥0) (fun (x : ℝ≥0) ↦ x ^ y) atTop atTop
have rw : ∀ (b : ℝ≥0), ∃ (i : ℝ≥0), ∀ (a : ℝ≥0), i ≤ a → b ≤ a ^ y
Tactic: rw [Filter.tendsto_atTop_atTop]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
y : ℝ
hy : 0 < y
b : ℝ≥0
⊢ ∃ (i : ℝ≥0), ∀ (a : ℝ≥0), i ≤ a → b ≤ a ^ y
have obtain : ∀ (c : ℝ) (hc : ∀ (a : ℝ), c ≤ a → (↑b : ℝ) ≤ a ^ y), ∃ (i : ℝ≥0), ∀ (a : ℝ≥0), i ≤ a → b ≤ a ^ y
Tactic: obtain ⟨c, hc⟩ := tendsto_atTop_atTop.mp (tendsto_rpow_atTop hy) b
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
y : ℝ
hy : 0 < y
b : ℝ≥0
c : ℝ
hc : ∀ (a : ℝ), c ≤ a → (↑b : ℝ) ≤ a ^ y
⊢ ∃ (i : ℝ≥0), ∀ (a : ℝ≥0), i ≤ a → b ≤ a ^ y
have h : ∀ (a : ℝ≥0), c.toNNReal ≤ a → b ≤ a ^ y
Tactic: use c.toNNReal
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
y : ℝ
hy : 0 < y
⊢ Tendsto (β := ℝ≥0∞) (fun (x : ℝ≥0∞) ↦ x ^ y) (𝓝 ∞) (𝓝 ∞)
have rw : ∀ (x : ℝ≥0), ∀ᶠ (a : ℝ≥0∞) in 𝓝 ∞, (↑x : ℝ≥0∞) < a ^ y
Tactic: rw [ENNReal.tendsto_nhds_top_iff_nnreal]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
y : ℝ
hy : 0 < y
x : ℝ≥0
⊢ ∀ᶠ (a : ℝ≥0∞) in 𝓝 ∞, (↑x : ℝ≥0∞) < a ^ y
have obtain : ∀ (c : ℝ≥0), True → ∀ (hc : ∀ x_1 ∈ Set.Ioi c, x_1 ^ y ∈ Set.Ioi x), ∀ᶠ (a : ℝ≥0∞) in 𝓝 ∞, (↑x : ℝ≥0∞) < a ^ y
Tactic: obtain ⟨c, _, hc⟩ :=
    (atTop_basis_Ioi.tendsto_iff atTop_basis_Ioi).mp (NNReal.tendsto_rpow_atTop hy) x trivial
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (hypothesis)
Goal:
y : ℝ
hy : 0 < y
x c : ℝ≥0
left : True
hc : ∀ x_1 ∈ Set.Ioi c, x_1 ^ y ∈ Set.Ioi x
⊢ ∀ᶠ (a : ℝ≥0∞) in 𝓝 ∞, (↑x : ℝ≥0∞) < a ^ y
have hc' : Membership.mem (γ := Filter ℝ≥0∞) (𝓝 ∞) (Set.Ioi (↑c : ℝ≥0∞))
Tactic: have hc' : Set.Ioi ↑c ∈ 𝓝 (⊤ : ℝ≥0∞) := Ioi_mem_nhds ENNReal.coe_lt_top
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
y : ℝ
hy : 0 < y
x c : ℝ≥0
left : True
hc : ∀ x_1 ∈ Set.Ioi c, x_1 ^ y ∈ Set.Ioi x
hc' : Membership.mem (γ := Filter ℝ≥0∞) (𝓝 ∞) (Set.Ioi (↑c : ℝ≥0∞))
⊢ ∀ᶠ (a : ℝ≥0∞) in 𝓝 ∞, (↑x : ℝ≥0∞) < a ^ y
have h : ∀ (a : ℝ≥0∞) (ha : a ∈ Set.Ioi (↑c : ℝ≥0∞)), (↑x : ℝ≥0∞) < a ^ y
Tactic: filter_upwards [hc'] with a ha
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
y : ℝ
hy : 0 < y
x c : ℝ≥0
left : True
hc : ∀ x_1 ∈ Set.Ioi c, x_1 ^ y ∈ Set.Ioi x
hc' : Membership.mem (γ := Filter ℝ≥0∞) (𝓝 ∞) (Set.Ioi (↑c : ℝ≥0∞))
a : ℝ≥0∞
ha : a ∈ Set.Ioi (↑c : ℝ≥0∞)
⊢ (↑x : ℝ≥0∞) < a ^ y
have pos : ∀ (ha' : a = ∞), (↑x : ℝ≥0∞) < a ^ y
Tactic: by_cases ha' : a = ⊤
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
y : ℝ
hy : 0 < y
x c : ℝ≥0
left : True
hc : ∀ x_1 ∈ Set.Ioi c, x_1 ^ y ∈ Set.Ioi x
hc' : Membership.mem (γ := Filter ℝ≥0∞) (𝓝 ∞) (Set.Ioi (↑c : ℝ≥0∞))
a : ℝ≥0∞
ha : a ∈ Set.Ioi (↑c : ℝ≥0∞)
pos : ∀ (ha' : a = ∞), (↑x : ℝ≥0∞) < a ^ y
⊢ (↑x : ℝ≥0∞) < a ^ y
have neg : ∀ (ha' : ¬a = ∞), (↑x : ℝ≥0∞) < a ^ y
Tactic: by_cases ha' : a = ⊤