awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
E : Type u_2
inst : SeminormedRing E
a b c : ℝ
f g : ℕ → E
hf : IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) a
hg : IsBigO (F := ℝ) atTop g fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) b
h : a + b ≤ c
t : ℕ
ht : 1 ≤ t
⊢ LE.le (α := ℝ) 1 (↑t : ℝ)

Tactic:
replace ht : 1 ≤ (t : ℝ) := Nat.one_le_cast.mpr ht
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
E : Type u_2
inst : SeminormedRing E
a b c : ℝ
f g : ℕ → E
hf : IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) a
hg : IsBigO (F := ℝ) atTop g fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) b
h : a + b ≤ c
t : ℕ
ht : LE.le (α := ℝ) 1 (↑t : ℝ)
h₁ : HPow.hPow (α := ℝ) (↑t : ℝ) (a + b) ≤ HPow.hPow (α := ℝ) (↑t : ℝ) c
⊢ ‖HPow.hPow (α := ℝ) (↑t : ℝ) a * HPow.hPow (α := ℝ) (↑t : ℝ) b‖ ≤ HPow.hPow (α := ℝ) (↑t : ℝ) c

Tactic:
rw [← Real.rpow_add (zero_lt_one.trans_le ht), Real.norm_of_nonneg (Real.rpow_nonneg
    (zero_le_one.trans ht) (a + b))]

Premises used: zero_le_one, zero_lt_one, HAdd.hAdd, LT.lt.trans_le, Real.rpow_add, Real.rpow_nonneg, LE.le.trans, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
E : Type u_2
inst : SeminormedRing E
a b c : ℝ
f g : ℕ → E
hf : IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) a
hg : IsBigO (F := ℝ) atTop g fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) b
h : a + b ≤ c
t : ℕ
ht : LE.le (α := ℝ) 1 (↑t : ℝ)
⊢ HPow.hPow (α := ℝ) (↑t : ℝ) (a + b) ≤ HPow.hPow (α := ℝ) (↑t : ℝ) c

Tactic:
Real.rpow_le_rpow_of_exponent_le ht h

Premises used: Real.rpow_le_rpow_of_exponent_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
E : Type u_2
inst : SeminormedRing E
a b c : ℝ
f g : ℕ → E
hf : IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) a
hg : IsBigO (F := ℝ) atTop g fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) b
h : a + b ≤ c
t : ℕ
ht : LE.le (α := ℝ) 1 (↑t : ℝ)
⊢ HPow.hPow (α := ℝ) (↑t : ℝ) (a + b) ≤ HPow.hPow (α := ℝ) (↑t : ℝ) c

Tactic:
exact Real.rpow_le_rpow_of_exponent_le ht h

Premises used: Real.rpow_le_rpow_of_exponent_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
a b : ℝ
h : a ≤ b
himp : b = 0 → a = 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) x
⊢ Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ ‖x ^ b‖ ≤ ‖x ^ a‖) x} x

Tactic:
simpa [Real.abs_rpow_of_nonneg hx.1, abs_of_nonneg hx.1]
     using Real.rpow_le_rpow_of_exponent_ge_of_imp hx.1 hx.2 h fun _ ↦ himp

Premises used: Real.abs_rpow_of_nonneg, And.right, And.left, abs_of_nonneg, Real.rpow_le_rpow_of_exponent_ge_of_imp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
a b : ℝ
h : a ≤ b
hb : b ≠ 0
⊢ IsBigO (E := ℝ) (F := ℝ) (𝓝[≥] 0) (fun (x : ℝ) ↦ x ^ b) fun (x : ℝ) ↦ x ^ a

Tactic:
.rpow_rpow_nhdsGE_zero_of_le_of_imp h (absurd · hb)

Premises used: absurd, Asymptotics.IsBigO.rpow_rpow_nhdsGE_zero_of_le_of_imp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
a : ℝ
ha : a ≤ 1
⊢ Ne (α := ℝ) 1 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
a : ℝ
ha : a ≤ 1
⊢ IsBigO (F := ℝ) (𝓝[≥] 0) id fun (x : ℝ) ↦ x ^ a

Tactic:
simpa using rpow_rpow_nhdsGE_zero_of_le ha (by simp)

Premises used: Asymptotics.IsBigO.rpow_rpow_nhdsGE_zero_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
s b : ℝ
hb : 0 < b
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ s / rexp (b * x)) atTop (𝓝 0)

Tactic:
simpa only [div_eq_mul_inv, exp_neg, neg_mul] using
      tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero s b hb

Premises used: tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero, div_eq_mul_inv, neg_mul, Real.exp_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
k : ℤ
b : ℝ
hb : 0 < b
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ x ^ k) fun (x : ℝ) ↦ rexp (b * x)

Tactic:
simpa only [Real.rpow_intCast] using isLittleO_rpow_exp_pos_mul_atTop k hb

Premises used: Int.cast, isLittleO_rpow_exp_pos_mul_atTop, Real.rpow_intCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
k : ℕ
b : ℝ
hb : 0 < b
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ x ^ k) fun (x : ℝ) ↦ rexp (b * x)

Tactic:
simpa using isLittleO_zpow_exp_pos_mul_atTop k hb

Premises used: Nat.cast, isLittleO_zpow_exp_pos_mul_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
s : ℝ
⊢ IsLittleO (E := ℝ) atTop (fun (x : ℝ) ↦ x ^ s) rexp

Tactic:
simpa only [one_mul] using isLittleO_rpow_exp_pos_mul_atTop s one_pos

Premises used: isLittleO_rpow_exp_pos_mul_atTop, one_pos, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
a : ℝ
ha : 0 < a
b : ℝ
hgf : ∀ᶠ (x : ℝ) in atTop, x ^ b = 0 → rexp (-a * x) = 0
a₁ : Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (-a * x) / x ^ b) atTop (𝓝 0)
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (-a * x)) fun (x : ℝ) ↦ x ^ b

Tactic:
apply isLittleO_of_tendsto'

Premises used: Asymptotics.isLittleO_of_tendsto'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
a : ℝ
ha : 0 < a
b : ℝ
⊢ ∀ᶠ (x : ℝ) in atTop, x ^ b = 0 → rexp (-a * x) = 0

Tactic:
(eventually_gt_atTop 0).mono fun t ht h => ?_

Premises used: Filter.Eventually.mono, OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
a : ℝ
ha : 0 < a
b : ℝ
hgf : ∀ (t : ℝ) (ht : 0 < t) (h : t ^ b = 0), rexp (-a * t) = 0
⊢ ∀ᶠ (x : ℝ) in atTop, x ^ b = 0 → rexp (-a * x) = 0

Tactic:
refine (eventually_gt_atTop 0).mono fun t ht h => ?_

Premises used: Filter.Eventually.mono, OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
a : ℝ
ha : 0 < a
b t : ℝ
ht : 0 < t
h : t ^ b = 0
⊢ t = 0 ∧ b ≠ 0

Tactic:
rw [rpow_eq_zero_iff_of_nonneg ht.le] at h

Premises used: Real.rpow_eq_zero_iff_of_nonneg, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
a : ℝ
ha : 0 < a
b t : ℝ
ht : 0 < t
h : t = 0 ∧ b ≠ 0
⊢ rexp (-a * t) = 0

Tactic:
(ht.ne' h.1).elim

Premises used: False.elim, LT.lt.ne', And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
a : ℝ
ha : 0 < a
b t : ℝ
ht : 0 < t
h : t = 0 ∧ b ≠ 0
⊢ rexp (-a * t) = 0

Tactic:
exact (ht.ne' h.1).elim

Premises used: False.elim, LT.lt.ne', And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
a : ℝ
ha : 0 < a
b : ℝ
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (-a * x) / x ^ b) atTop (𝓝 0)

Tactic:
(tendsto_exp_mul_div_rpow_atTop (-b) a ha).inv_tendsto_atTop.congr' ?_

Premises used: Filter.Tendsto.inv_tendsto_atTop, Filter.Tendsto.congr', tendsto_exp_mul_div_rpow_atTop, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
a : ℝ
ha : 0 < a
b : ℝ
a₁ : EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ rexp (a * x) / x ^ (-b))⁻¹ fun (x : ℝ) ↦ rexp (-a * x) / x ^ b
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (-a * x) / x ^ b) atTop (𝓝 0)

Tactic:
refine (tendsto_exp_mul_div_rpow_atTop (-b) a ha).inv_tendsto_atTop.congr' ?_

Premises used: Filter.Tendsto.inv_tendsto_atTop, Filter.Tendsto.congr', tendsto_exp_mul_div_rpow_atTop, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
a : ℝ
ha : 0 < a
b : ℝ
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ rexp (a * x) / x ^ (-b))⁻¹ fun (x : ℝ) ↦ rexp (-a * x) / x ^ b

Tactic:
(eventually_ge_atTop 0).mono fun t ht => ?_

Premises used: Filter.EventuallyEq, Filter.Eventually.mono, Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
a : ℝ
ha : 0 < a
b : ℝ
a₁ :
  ∀ (t : ℝ) (ht : 0 ≤ t),
    Eq (α := ℝ) ((fun (x : ℝ) ↦ rexp (a * x) / x ^ (-b))⁻¹ t) ((fun (x : ℝ) ↦ rexp (-a * x) / x ^ b) t)
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ rexp (a * x) / x ^ (-b))⁻¹ fun (x : ℝ) ↦ rexp (-a * x) / x ^ b

Tactic:
refine (eventually_ge_atTop 0).mono fun t ht => ?_

Premises used: Filter.Eventually.mono, Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
a : ℝ
ha : 0 < a
b t : ℝ
ht : 0 ≤ t
⊢ Eq (α := ℝ) ((fun (x : ℝ) ↦ rexp (a * x) / x ^ (-b))⁻¹ t) ((fun (x : ℝ) ↦ rexp (-a * x) / x ^ b) t)

Tactic:
simp [field, Real.exp_neg, rpow_neg ht]

Premises used: Real.exp_neg, Real.rpow_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
k a b : ℝ
ha' : a < b
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ rexp (a * t) * t ^ k) fun (t : ℝ) ↦ rexp (b * t)

Tactic:
(isLittleO_of_tendsto (fun _ h ↦ (Real.exp_ne_zero _ h).elim) ?_)

Premises used: HMul.hMul, False.elim, Asymptotics.isLittleO_of_tendsto, Real.exp_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
k a b : ℝ
ha' : a < b
refine : Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (a * x) * x ^ k / rexp (b * x)) atTop (𝓝 0)
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ rexp (a * t) * t ^ k) fun (t : ℝ) ↦ rexp (b * t)

Tactic:
refine (isLittleO_of_tendsto (fun _ h ↦ (Real.exp_ne_zero _ h).elim) ?_)

Premises used: False.elim, Asymptotics.isLittleO_of_tendsto, Real.exp_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
k a b : ℝ
ha' : a < b
simp_rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ k * rexp (-(b - a) * x)) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (a * x) * x ^ k / rexp (b * x)) atTop (𝓝 0)

Tactic:
simp_rw [← div_mul_eq_mul_div₀, ← Real.exp_sub, ← sub_mul, ← neg_sub b a,
    mul_comm _ (_ ^ k)]

Premises used: neg_sub, sub_mul, HPow.hPow, mul_comm, Real.exp_sub, div_mul_eq_mul_div₀
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
k a b : ℝ
ha' : a < b
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ k * rexp (-(b - a) * x)) atTop (𝓝 0)

Tactic:
tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero _ _ (sub_pos.mpr ha')

Premises used: Iff.mpr, sub_pos, tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
k a b : ℝ
ha' : a < b
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ k * rexp (-(b - a) * x)) atTop (𝓝 0)

Tactic:
exact tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero _ _ (sub_pos.mpr ha')

Premises used: Iff.mpr, sub_pos, tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
r : ℝ
hr : 0 < r
⊢ IsLittleO (F := ℝ) atTop log fun (x : ℝ) ↦ x ^ r

Tactic:
calc
    log =O[atTop] fun x => r * log x := isBigO_self_const_mul hr.ne' _ _
    _ =ᶠ[atTop] fun x => log (x ^ r) :=
      ((eventually_gt_atTop 0).mono fun _ hx => (log_rpow hx _).symm)
    _ =o[atTop] fun x => x ^ r := isLittleO_log_id_atTop.comp_tendsto (tendsto_rpow_atTop hr)

Premises used: Trans.trans, Real.isLittleO_log_id_atTop, tendsto_rpow_atTop, Real.log_rpow, Filter.Eventually.mono, LT.lt.ne', Asymptotics.isBigO_self_const_mul, Asymptotics.IsLittleO.comp_tendsto, OfNat.ofNat, Eq.symm, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
s r : ℝ
hs : 0 < s
r' : ℝ := max r 1
hr : 0 < r'
H : 0 < s / r'
h : ∀ (x : ℝ) (hx : 1 ≤ log x), ‖log x ^ r‖ ≤ log x ^ r'
⊢ EventuallyLE (β := ℝ) atTop (fun (x : ℝ) ↦ ‖log x ^ r‖) fun (x : ℝ) ↦ log x ^ r'

Tactic:
filter_upwards [tendsto_log_atTop.eventually_ge_atTop 1] with x hx

Premises used: Real.tendsto_log_atTop, OfNat.ofNat, Filter.Tendsto.eventually_ge_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
s r : ℝ
hs : 0 < s
r' : ℝ := max r 1
hr : 0 < r'
H : 0 < s / r'
x : ℝ
hx : 1 ≤ log x
⊢ 0 ≤ log x ^ r

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
s r : ℝ
hs : 0 < s
r' : ℝ := max r 1
hr : 0 < r'
H : 0 < s / r'
x : ℝ
hx : 1 ≤ log x
h : log x ^ r ≤ log x ^ r'
⊢ ‖log x ^ r‖ ≤ log x ^ r'

Tactic:
rw [Real.norm_of_nonneg (by positivity)]

Premises used: Real.norm_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
s r : ℝ
hs : 0 < s
r' : ℝ := max r 1
hr : 0 < r'
H : 0 < s / r'
x : ℝ
hx : 1 ≤ log x
h : r ≤ r'
⊢ log x ^ r ≤ log x ^ r'

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
s r : ℝ
hs : 0 < s
r' : ℝ := max r 1
hr : 0 < r'
H : 0 < s / r'
x : ℝ
hx : 1 ≤ log x
⊢ r ≤ r'

Tactic:
le_max_left _ _

Premises used: le_max_left
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
s r : ℝ
hs : 0 < s
r' : ℝ := max r 1
hr : 0 < r'
H : 0 < s / r'
x : ℝ
hx : 1 ≤ log x
⊢ r ≤ r'

Tactic:
exact le_max_left _ _

Premises used: le_max_left
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
s r : ℝ
hs : 0 < s
r' : ℝ := max r 1
hr : 0 < r'
H : 0 < s / r'
x : ℝ
hx : 0 ≤ x
⊢ Eq (α := ℝ) ((fun (x : ℝ) ↦ (x ^ (s / r')) ^ r') x) ((fun (x : ℝ) ↦ x ^ s) x)

Tactic:
simp only [← rpow_mul hx, div_mul_cancel₀ _ hr.ne']

Premises used: div_mul_cancel₀, LT.lt.ne', Real.rpow_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
s r : ℝ
hs : s < 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) x
⊢ Membership.mem (γ := Set ℝ)
    {x : ℝ |
      (fun (x : ℝ) ↦ Eq (α := ℝ) (((fun (x : ℝ) ↦ log x ^ r) ∘ fun (x : ℝ) ↦ x⁻¹) x) ((fun (x : ℝ) ↦ |log x| ^ r) x)) x}
    x

Tactic:
simp [abs_of_nonpos, log_nonpos hx.1 hx.2]

Premises used: Real.log_nonpos, abs_of_nonpos, And.right, And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
s r : ℝ
hs : s < 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioi 0) x
rw : x⁻¹ ^ (-s) = (fun (x : ℝ) ↦ x ^ s) x
rw₁ : (x ^ (-s))⁻¹ = (fun (x : ℝ) ↦ x ^ s) x
rw₂ : (x ^ s)⁻¹⁻¹ = (fun (x : ℝ) ↦ x ^ s) x
rw₃ rw₄ : x ^ s = (fun (x : ℝ) ↦ x ^ s) x
⊢ Eq (α := ℝ) (((fun (x : ℝ) ↦ x ^ (-s)) ∘ fun (x : ℝ) ↦ x⁻¹) x) ((fun (x : ℝ) ↦ x ^ s) x)

Tactic:
rw [Function.comp_apply, inv_rpow hx.out.le, rpow_neg hx.out.le, inv_inv]

Premises used: Real.inv_rpow, Membership.mem.out, LT.lt.le, inv_inv, Function.comp_apply, Real.rpow_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
r : ℝ
hr : r < 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) x
⊢ Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ (fun (x : ℝ) ↦ -HPow.hPow (β := ℝ) |log x| 1) x = log x) x} x

Tactic:
simp [abs_of_nonpos (log_nonpos hx.1 hx.2)]

Premises used: Real.log_nonpos, abs_of_nonpos, And.right, And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
r : ℝ
hr : r < 0
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x / x ^ r) (𝓝[>] 0) (𝓝 0)

Tactic:
(isLittleO_log_rpow_nhdsGT_zero hr).tendsto_div_nhds_zero

Premises used: Asymptotics.IsLittleO.tendsto_div_nhds_zero, isLittleO_log_rpow_nhdsGT_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
r : ℝ
hr : 0 < r
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioi 0) x
rw : log x / (x ^ r)⁻¹ = (fun (x : ℝ) ↦ log x * x ^ r) x
rw₁ rw₂ : log x * x ^ r = (fun (x : ℝ) ↦ log x * x ^ r) x
⊢ log x / x ^ (-r) = (fun (x : ℝ) ↦ log x * x ^ r) x

Tactic:
rw [rpow_neg hx.out.le, div_inv_eq_mul]

Premises used: Membership.mem.out, LT.lt.le, div_inv_eq_mul, Real.rpow_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * HPow.hPow (β := ℝ) x 1) (𝓝[>] 0) (𝓝 0)

Tactic:
have h := tendsto_log_mul_rpow_nhdsGT_zero zero_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
h : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * HPow.hPow (β := ℝ) x 1) (𝓝[>] 0) (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[>] 0) (𝓝 0)

Tactic:
simp only [Real.rpow_one] at h

Premises used: Real.rpow_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
h : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[>] 0) (𝓝 0)
simp : ∀ x < 0, -(log x * |x|) = log x * x
⊢ ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Iio 0) x → (-(fun (x : ℝ) ↦ log x * x) ∘ fun (x : ℝ) ↦ |x|) x = log x * x

Tactic:
simp only [Set.mem_Iio, Pi.neg_apply, Function.comp_apply, log_abs]

Premises used: Set.mem_Iio, Real.log_abs, Function.comp_apply, Pi.neg_apply
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
h : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[>] 0) (𝓝 0)
x : ℝ
hx : x < 0
⊢ -(log x * |x|) = log x * x

Tactic:
simp only [abs_of_nonpos hx.le, mul_neg, neg_neg]

Premises used: neg_neg, LT.lt.le, abs_of_nonpos, mul_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
h : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[>] 0) (𝓝 0)
⊢ ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Iio 0) x → (-(fun (x : ℝ) ↦ log x * x) ∘ fun (x : ℝ) ↦ |x|) x = log x * x

Tactic:
have h_eq : ∀ x ∈ Set.Iio 0, (-(fun x ↦ log x * x) ∘ (fun x ↦ |x|)) x = log x * x := by
    simp only [Set.mem_Iio, Pi.neg_apply, Function.comp_apply, log_abs]
    intro x hx
    simp only [abs_of_nonpos hx.le, mul_neg, neg_neg]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
h : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[>] 0) (𝓝 0)
h_eq :
  ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Iio 0) x → (-(fun (x : ℝ) ↦ log x * x) ∘ fun (x : ℝ) ↦ |x|) x = log x * x
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[<] 0) (𝓝 0)

Tactic:
tendsto_nhdsWithin_congr h_eq ?_

Premises used: tendsto_nhdsWithin_congr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
h : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[>] 0) (𝓝 0)
h_eq :
  ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Iio 0) x → (-(fun (x : ℝ) ↦ log x * x) ∘ fun (x : ℝ) ↦ |x|) x = log x * x
refine : Tendsto (α := ℝ) (β := ℝ) (-(fun (x : ℝ) ↦ log x * x) ∘ fun (x : ℝ) ↦ |x|) (𝓝[<] 0) (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[<] 0) (𝓝 0)

Tactic:
refine tendsto_nhdsWithin_congr h_eq ?_

Premises used: tendsto_nhdsWithin_congr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
h : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[>] 0) (𝓝 0)
h_eq :
  ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Iio 0) x → (-(fun (x : ℝ) ↦ log x * x) ∘ fun (x : ℝ) ↦ |x|) x = log x * x
nth_rewrite : Tendsto (α := ℝ) (β := ℝ) (-(fun (x : ℝ) ↦ log x * x) ∘ fun (x : ℝ) ↦ |x|) (𝓝[<] 0) (𝓝 (-0))
⊢ Tendsto (α := ℝ) (β := ℝ) (-(fun (x : ℝ) ↦ log x * x) ∘ fun (x : ℝ) ↦ |x|) (𝓝[<] 0) (𝓝 0)

Tactic:
nth_rewrite 3 [← neg_zero]

Premises used: neg_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
h : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[>] 0) (𝓝 0)
h_eq :
  ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Iio 0) x → (-(fun (x : ℝ) ↦ log x * x) ∘ fun (x : ℝ) ↦ |x|) x = log x * x
⊢ Tendsto (α := ℝ) (β := ℝ) (-(fun (x : ℝ) ↦ log x * x) ∘ fun (x : ℝ) ↦ |x|) (𝓝[<] 0) (𝓝 (-0))

Tactic:
(h.comp (tendsto_abs_nhdsNE_zero.mono_left ?_)).neg

Premises used: Filter.Tendsto.neg, tendsto_abs_nhdsNE_zero, Filter.Tendsto.mono_left, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
h : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[>] 0) (𝓝 0)
h_eq :
  ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Iio 0) x → (-(fun (x : ℝ) ↦ log x * x) ∘ fun (x : ℝ) ↦ |x|) x = log x * x
⊢ LE.le (α := Filter ℝ) (𝓝[<] 0) (𝓝[≠] 0)

Tactic:
nhdsWithin_mono 0 (fun x hx ↦ ?_)

Premises used: Set.Mem, setOf, OfNat.ofNat, nhdsWithin_mono
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
h : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[>] 0) (𝓝 0)
h_eq :
  ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Iio 0) x → (-(fun (x : ℝ) ↦ log x * x) ∘ fun (x : ℝ) ↦ |x|) x = log x * x
refine : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Set.Iio 0) x), Membership.mem (γ := Set ℝ) {0}ᶜ x
⊢ LE.le (α := Filter ℝ) (𝓝[<] 0) (𝓝[≠] 0)

Tactic:
refine nhdsWithin_mono 0 (fun x hx ↦ ?_)

Premises used: OfNat.ofNat, nhdsWithin_mono
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
h : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[>] 0) (𝓝 0)
h_eq :
  ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Iio 0) x → (-(fun (x : ℝ) ↦ log x * x) ∘ fun (x : ℝ) ↦ |x|) x = log x * x
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Iio 0) x
⊢ x < 0

Tactic:
push _ ∈ _ at hx
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
h : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[>] 0) (𝓝 0)
h_eq :
  ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Iio 0) x → (-(fun (x : ℝ) ↦ log x * x) ∘ fun (x : ℝ) ↦ |x|) x = log x * x
x : ℝ
hx : x < 0
⊢ Membership.mem (γ := Set ℝ) {0}ᶜ x

Tactic:
simp only [Set.mem_compl_iff, Set.mem_singleton_iff, hx.ne, not_false_eq_true]

Premises used: Set.mem_singleton_iff, not_false_eq_true, Set.mem_compl_iff, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x y : ℂ
⊢ x.cpow y = x ^ y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x y : ℂ
⊢ x ^ y = if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)

Tactic:
rfl

Premises used: Complex.cpow, rfl, ite
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x : ℂ
hx : x ≠ 0
y : ℂ
⊢ x ^ y = cexp (log x * y)

Tactic:
if_neg hx

Premises used: Complex.cpow, if_neg, ite
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x : ℂ
⊢ HPow.hPow (β := ℂ) x 0 = 1

Tactic:
simp [cpow_def]

Premises used: Complex.cpow_def
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x y : ℂ
pos : x = 0 → y = 0 → (Eq (α := ℂ) 1 0 ↔ x = 0 ∧ y ≠ 0)
neg : x = 0 → ¬y = 0 → (Eq (α := ℂ) 0 0 ↔ x = 0 ∧ y ≠ 0)
neg₁ : ¬x = 0 → (cexp (log x * y) = 0 ↔ x = 0 ∧ y ≠ 0)
⊢ (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) = 0 ↔ x = 0 ∧ y ≠ 0

Tactic:
split_ifs
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x y : ℂ
h : x = 0
h_1 : y = 0
⊢ Eq (α := ℂ) 1 0 ↔ x = 0 ∧ y ≠ 0

Tactic:
simp [*, exp_ne_zero]

Premises used: Complex.exp_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x y : ℂ
h : x = 0
h_1 : ¬y = 0
⊢ Eq (α := ℂ) 0 0 ↔ x = 0 ∧ y ≠ 0

Tactic:
simp [*, exp_ne_zero]

Premises used: Complex.exp_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x y : ℂ
h : ¬x = 0
⊢ cexp (log x * y) = 0 ↔ x = 0 ∧ y ≠ 0

Tactic:
simp [*, exp_ne_zero]

Premises used: Complex.exp_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x y : ℂ
rw : ¬x ^ y = 0 ↔ x ≠ 0 ∨ y = 0
rw₁ : ¬(x = 0 ∧ y ≠ 0) ↔ x ≠ 0 ∨ y = 0
rw₂ : ¬x = 0 ∨ ¬y ≠ 0 ↔ x ≠ 0 ∨ y = 0
rw₃ : ¬x = 0 ∨ ¬¬y = 0 ↔ x ≠ 0 ∨ y = 0
rw₄ rw₅ : ¬x = 0 ∨ y = 0 ↔ x ≠ 0 ∨ y = 0
⊢ x ^ y ≠ 0 ↔ x ≠ 0 ∨ y = 0

Tactic:
rw [ne_eq, cpow_eq_zero_iff, not_and_or, ne_eq, not_not]

Premises used: Classical.not_not, Complex.cpow_eq_zero_iff, ne_eq, not_and_or
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x y : ℂ
hy : y ≠ 0
⊢ x ^ y ≠ 0 ↔ x ≠ 0

Tactic:
simp [hy]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x : ℂ
h : x ≠ 0
⊢ HPow.hPow (α := ℂ) 0 x = 0

Tactic:
simp [cpow_def, *]

Premises used: Complex.cpow_def
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x a : ℂ
mp : HPow.hPow (α := ℂ) 0 x = a → x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
mpr : x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1 → HPow.hPow (α := ℂ) 0 x = a
⊢ HPow.hPow (α := ℂ) 0 x = a ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x a : ℂ
hyp : HPow.hPow (α := ℂ) 0 x = a
⊢ (if x = 0 then 1 else 0) = a

Tactic:
simp only [cpow_def, if_true] at hyp

Premises used: if_true, Complex.cpow_def
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x a : ℂ
hyp : (if x = 0 then 1 else 0) = a
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x : ℂ
h : x ≠ 0
⊢ HPow.hPow (α := ℂ) 0 x = 0

Tactic:
zero_cpow h

Premises used: Complex.zero_cpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x : ℂ
h : x ≠ 0
⊢ HPow.hPow (α := ℂ) 0 x = 0

Tactic:
exact zero_cpow h

Premises used: Complex.zero_cpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
⊢ HPow.hPow (α := ℂ) (β := ℂ) 0 0 = 1

Tactic:
cpow_zero _

Premises used: Complex.cpow_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
⊢ HPow.hPow (α := ℂ) (β := ℂ) 0 0 = 1

Tactic:
exact cpow_zero _

Premises used: Complex.cpow_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x a : ℂ
rw : a = HPow.hPow (α := ℂ) 0 x ↔ HPow.hPow (α := ℂ) 0 x = a
rw₁ rw₂ : HPow.hPow (α := ℂ) 0 x = a ↔ HPow.hPow (α := ℂ) 0 x = a
⊢ a = HPow.hPow (α := ℂ) 0 x ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
rw [← zero_cpow_eq_iff, eq_comm]

Premises used: Complex.zero_cpow_eq_iff, eq_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x : ℂ
hx : x = 0
⊢ HPow.hPow (β := ℂ) x 1 = x

Tactic:
simp [hx, cpow_def]

Premises used: Complex.cpow_def