awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
qpos : LT.lt (α := ℝ) 0 (↑q : ℝ)
⊢ HSub.hSub (α := ℝ) (↑q : ℝ) 1 < p * (↑q : ℝ)

Tactic:
have : (q : ℝ) - 1 < p * q := by
          have h1 := mul_lt_mul_of_pos_right hp.1 qpos
          have h2 : (1 - (q : ℝ)⁻¹) * ↑q = q - 1 := by calc (1 - (q : ℝ)⁻¹) * ↑q
            _ = q - (q : ℝ)⁻¹ * (q : ℝ) := by ring
            _ = q - 1 := by simp [qpos.ne']
          rwa [h2] at h1
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this_1 : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
qpos : LT.lt (α := ℝ) 0 (↑q : ℝ)
this : HSub.hSub (α := ℝ) (↑q : ℝ) 1 < p * (↑q : ℝ)
nlinarith :
  p ≤ HAdd.hAdd (α := ℝ) (-1) (↑q : ℝ) - (↑q : ℝ) * p + p →
    HSub.hSub (α := ℝ) (↑q : ℝ) 1 - p * (↑q : ℝ) + (p - (HAdd.hAdd (α := ℝ) (-1) (↑q : ℝ) - (↑q : ℝ) * p + p)) = 0
⊢ HAdd.hAdd (α := ℝ) (-1) (↑q : ℝ) - (↑q : ℝ) * p + p < p

Tactic:
nlinarith
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
⊢ p ≠ 1

Tactic:
(ne_of_gt (lt_add_neg_iff_lt.mp zero_lt_1_sub_p : p < 1)).symm

Premises used: ne_of_gt, lt_add_neg_iff_lt, Ne.symm, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
⊢ p ≠ 1

Tactic:
exact (ne_of_gt (lt_add_neg_iff_lt.mp zero_lt_1_sub_p : p < 1)).symm

Premises used: ne_of_gt, lt_add_neg_iff_lt, Ne.symm, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
⊢ Icc 0 2⁻¹ = Icc 0 (1 - 1 / 2)

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
rw : StrictMonoOn (qaryEntropy 2) (Icc 0 (1 - 1 / 2))
⊢ StrictMonoOn binEntropy (Icc 0 2⁻¹)

Tactic:
rw [show Icc (0 : ℝ) 2⁻¹ = Icc 0 (1 - 1 / 2) by norm_num, ← qaryEntropy_two]

Premises used: Real.qaryEntropy_two
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
⊢ LE.le (α := ℕ) 2 2

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
⊢ StrictMonoOn (qaryEntropy 2) (Icc 0 (1 - 1 / 2))

Tactic:
exact qaryEntropy_strictMonoOn (by rfl)

Premises used: Real.qaryEntropy_strictMonoOn
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
⊢ Icc 2⁻¹ 1 = Icc (1 / 2) 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
rw : StrictAntiOn (qaryEntropy 2) (Icc (1 / 2) 1)
⊢ StrictAntiOn binEntropy (Icc 2⁻¹ 1)

Tactic:
rw [show (Icc (2⁻¹ : ℝ) 1) = Icc (1 / 2) 1 by norm_num, ← qaryEntropy_two]

Premises used: Real.qaryEntropy_two
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
h : Icc (1 / 2) 1 = Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑2 : ℝ)) 1
⊢ StrictAntiOn (qaryEntropy 2) (Icc (1 / 2) 1)

Tactic:
convert! qaryEntropy_strictAntiOn (by rfl) using 1

Premises used: Real.qaryEntropy_strictAntiOn
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
⊢ Icc (1 / 2) 1 = Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑2 : ℝ)) 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
apply : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (interior (Icc 0 1)) x → deriv^[2] (qaryEntropy q) x < 0
⊢ StrictConcaveOn ℝ (Icc 0 1) (qaryEntropy q)

Tactic:
apply strictConcaveOn_of_deriv2_neg (convex_Icc 0 1) qaryEntropy_continuous.continuousOn

Premises used: Continuous.continuousOn, Real.qaryEntropy_continuous, convex_Icc, strictConcaveOn_of_deriv2_neg, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
hp : Membership.mem (γ := Set ℝ) (interior (Icc 0 1)) p
rw : -1 / (p * (1 - p)) < 0
⊢ deriv^[2] (qaryEntropy q) p < 0

Tactic:
rw [deriv2_qaryEntropy]

Premises used: Real.deriv2_qaryEntropy
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
hp : Membership.mem (γ := Set ℝ) (interior (Icc 0 1)) p
⊢ 0 < p ∧ p < 1

Tactic:
simp_all only [interior_Icc, mem_Ioo]

Premises used: Set.mem_Ioo, interior_Icc
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
hp : 0 < p ∧ p < 1
ha : LT.lt (α := ℝ) (-1) 0
hb : 0 < p * (1 - p)
⊢ -1 / (p * (1 - p)) < 0

Tactic:
apply div_neg_of_neg_of_pos

Premises used: div_neg_of_neg_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
hp : 0 < p ∧ p < 1
⊢ 0 < log 2

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
hp : 0 < p ∧ p < 1
⊢ LT.lt (α := ℝ) (-1) 0

Tactic:
norm_num [show 0 < log 2 by positivity]
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
hp : 0 < p ∧ p < 1
⊢ 0 < p * (1 - p)

Tactic:
simp_all only [mul_pos_iff_of_pos_left, sub_pos]

Premises used: sub_pos, mul_pos_iff_of_pos_left
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
⊢ StrictConcaveOn ℝ (Icc 0 1) binEntropy

Tactic:
qaryEntropy_two ▸ strictConcaveOn_qaryEntropy

Premises used: Real.qaryEntropy_two, Eq.rec, Real.strictConcaveOn_qaryEntropy
-- Module: Mathlib.Analysis.SpecialFunctions.Choose
Goal:
⊢ IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑(n.descFactorial 0) : ℝ)) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 0

Tactic:
simpa using IsEquivalent.refl

Premises used: Asymptotics.IsEquivalent.refl
-- Module: Mathlib.Analysis.SpecialFunctions.Choose
Goal:
k : ℕ
h : IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑(n.descFactorial k) : ℝ)) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k
succ :
  IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ HMul.hMul (α := ℝ) (↑(n - k) : ℝ) (↑(n.descFactorial k) : ℝ))
    fun (n : ℕ) ↦ (↑n : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) k
⊢ IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑(n.descFactorial (k + 1)) : ℝ)) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑n : ℝ) (k + 1)

Tactic:
simp_rw [descFactorial_succ, cast_mul, _root_.pow_succ']

Premises used: Nat.descFactorial_succ, Nat.cast_mul, pow_succ'
-- Module: Mathlib.Analysis.SpecialFunctions.Choose
Goal:
k : ℕ
h : IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑(n.descFactorial k) : ℝ)) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k
⊢ IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ HMul.hMul (α := ℝ) (↑(n - k) : ℝ) (↑(n.descFactorial k) : ℝ))
    fun (n : ℕ) ↦ (↑n : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) k

Tactic:
IsEquivalent.mul ?_ h

Premises used: Asymptotics.IsEquivalent.mul
-- Module: Mathlib.Analysis.SpecialFunctions.Choose
Goal:
k : ℕ
h : IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑(n.descFactorial k) : ℝ)) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k
succ : IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑(n - k) : ℝ)) Nat.cast
⊢ IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ HMul.hMul (α := ℝ) (↑(n - k) : ℝ) (↑(n.descFactorial k) : ℝ))
    fun (n : ℕ) ↦ (↑n : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) k

Tactic:
refine IsEquivalent.mul ?_ h

Premises used: Asymptotics.IsEquivalent.mul
-- Module: Mathlib.Analysis.SpecialFunctions.Choose
Goal:
k : ℕ
h : IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑(n.descFactorial k) : ℝ)) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k
⊢ ∀ᶠ (x : ℕ) in atTop, Ne (α := ℝ) (↑x : ℝ) 0

Tactic:
have hz : ∀ᶠ (x : ℕ) in atTop, (x : ℝ) ≠ 0 :=
      eventually_atTop.mpr ⟨1, fun n hn ↦ ne_of_gt (mod_cast hn)⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Choose
Goal:
k : ℕ
h : IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑(n.descFactorial k) : ℝ)) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k
hz : ∀ᶠ (x : ℕ) in atTop, Ne (α := ℝ) (↑x : ℝ) 0
succ :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℕ → ℝ) (β := ℕ → ℝ) (fun (n : ℕ) ↦ (↑(n - k) : ℝ)) Nat.cast (n + k))
    atTop (𝓝 1)
⊢ IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑(n - k) : ℝ)) Nat.cast

Tactic:
rw [isEquivalent_iff_tendsto_one hz, ← tendsto_add_atTop_iff_nat k]

Premises used: Asymptotics.isEquivalent_iff_tendsto_one, Filter.tendsto_add_atTop_iff_nat
-- Module: Mathlib.Analysis.SpecialFunctions.Choose
Goal:
k : ℕ
h : IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑(n.descFactorial k) : ℝ)) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k
hz : ∀ᶠ (x : ℕ) in atTop, Ne (α := ℝ) (↑x : ℝ) 0
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℕ → ℝ) (β := ℕ → ℝ) (fun (n : ℕ) ↦ (↑(n - k) : ℝ)) Nat.cast (n + k))
    atTop (𝓝 1)

Tactic:
simpa using tendsto_natCast_div_add_atTop (k : ℝ)

Premises used: tendsto_natCast_div_add_atTop, Nat.cast
-- Module: Mathlib.Analysis.SpecialFunctions.Choose
Goal:
k : ℕ
zero :
  IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑(n.descFactorial 0) : ℝ)) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 0
succ :
  ∀ (k : ℕ)
    (h :
      IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑(n.descFactorial k) : ℝ)) fun (n : ℕ) ↦
        HPow.hPow (α := ℝ) (↑n : ℝ) k),
    IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑(n.descFactorial (k + 1)) : ℝ)) fun (n : ℕ) ↦
      HPow.hPow (α := ℝ) (↑n : ℝ) (k + 1)
⊢ IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑(n.descFactorial k) : ℝ)) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k

Tactic:
induction k with
  | zero => simpa using IsEquivalent.refl
  | succ k h =>
    simp_rw [descFactorial_succ, cast_mul, _root_.pow_succ']
    refine IsEquivalent.mul ?_ h
    have hz : ∀ᶠ (x : ℕ) in atTop, (x : ℝ) ≠ 0 :=
      eventually_atTop.mpr ⟨1, fun n hn ↦ ne_of_gt (mod_cast hn)⟩
    rw [isEquivalent_iff_tendsto_one hz, ← tendsto_add_atTop_iff_nat k]
    simpa using tendsto_natCast_div_add_atTop (k : ℝ)

Premises used: tendsto_natCast_div_add_atTop, Nat.cast, Nat.descFactorial_succ, Nat.cast_mul, Asymptotics.IsEquivalent.refl, Filter.tendsto_add_atTop_iff_nat, Nat.zero, Nat.succ, pow_succ'
-- Module: Mathlib.Analysis.SpecialFunctions.Choose
Goal:
k n : ℕ
h : HDiv.hDiv (α := ℝ) (↑(n.descFactorial k) : ℝ) (↑k ! : ℝ)
| (↑(n.choose k) : ℝ)

Tactic:
rw [choose_eq_descFactorial_div_factorial,
      cast_div (n.factorial_dvd_descFactorial k) (mod_cast k.factorial_ne_zero)]

Premises used: Nat.cast_div, Nat.factorial_dvd_descFactorial, Nat.choose_eq_descFactorial_div_factorial
-- Module: Mathlib.Analysis.SpecialFunctions.Choose
Goal:
k : ℕ
conv_lhs :
  IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(n.descFactorial k) : ℝ) (↑k ! : ℝ)) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑n : ℝ) k / (↑k ! : ℝ)
⊢ IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑(n.choose k) : ℝ)) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑n : ℝ) k / (↑k ! : ℝ)

Tactic:
conv_lhs =>
    intro n
    rw [choose_eq_descFactorial_div_factorial,
      cast_div (n.factorial_dvd_descFactorial k) (mod_cast k.factorial_ne_zero)]

Premises used: Nat.choose_eq_descFactorial_div_factorial
-- Module: Mathlib.Analysis.SpecialFunctions.Choose
Goal:
k : ℕ
⊢ IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(n.descFactorial k) : ℝ) (↑k ! : ℝ)) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑n : ℝ) k / (↑k ! : ℝ)

Tactic:
(isEquivalent_descFactorial k).div IsEquivalent.refl

Premises used: isEquivalent_descFactorial, Asymptotics.IsEquivalent.div, Asymptotics.IsEquivalent.refl
-- Module: Mathlib.Analysis.SpecialFunctions.Choose
Goal:
k : ℕ
⊢ IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(n.descFactorial k) : ℝ) (↑k ! : ℝ)) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑n : ℝ) k / (↑k ! : ℝ)

Tactic:
exact (isEquivalent_descFactorial k).div IsEquivalent.refl

Premises used: isEquivalent_descFactorial, Asymptotics.IsEquivalent.div, Asymptotics.IsEquivalent.refl
-- Module: Mathlib.Analysis.SpecialFunctions.Choose
Goal:
k : ℕ
apply :
  IsTheta (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k / (↑k ! : ℝ)) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑n : ℝ) k
⊢ IsTheta (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(n.choose k) : ℝ)) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k

Tactic:
apply (isEquivalent_choose k).trans_isTheta

Premises used: isEquivalent_choose, Asymptotics.IsEquivalent.trans_isTheta
-- Module: Mathlib.Analysis.SpecialFunctions.Choose
Goal:
k : ℕ
simp_rw :
  IsTheta (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑k ! : ℝ)⁻¹ * HPow.hPow (α := ℝ) (↑n : ℝ) k) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑n : ℝ) k
⊢ IsTheta (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k / (↑k ! : ℝ)) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑n : ℝ) k

Tactic:
simp_rw [div_eq_mul_inv, mul_comm _ (_⁻¹)]

Premises used: div_eq_mul_inv, Inv.inv, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Choose
Goal:
k : ℕ
⊢ IsTheta (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑k ! : ℝ)⁻¹ * HPow.hPow (α := ℝ) (↑n : ℝ) k) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑n : ℝ) k

Tactic:
isTheta_rfl.const_mul_left <| inv_ne_zero (mod_cast k.factorial_ne_zero)

Premises used: Asymptotics.IsTheta.const_mul_left, congrArg, cast, Ne, Nat.cast, Asymptotics.isTheta_rfl, Nat.factorial_ne_zero, Nat.factorial, inv_ne_zero, Nat.cast_inj._simp_1, Nat.cast_zero, Eq.symm, Not, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Choose
Goal:
k : ℕ
⊢ IsTheta (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑k ! : ℝ)⁻¹ * HPow.hPow (α := ℝ) (↑n : ℝ) k) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑n : ℝ) k

Tactic:
exact isTheta_rfl.const_mul_left <| inv_ne_zero (mod_cast k.factorial_ne_zero)

Premises used: Asymptotics.IsTheta.const_mul_left, Asymptotics.isTheta_rfl, inv_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hre : Tendsto re l atTop
r : ℝ
hr : IsBigO (F := ℝ) l im fun (z : ℂ) ↦ z.re ^ r
n : ℕ
z : ℂ
hz : 0 ≤ z.re
⊢ Eq (α := ℝ) ((fun (z : ℂ) ↦ (z.re ^ r) ^ n) z) ((fun (z : ℂ) ↦ z.re ^ (r * (↑n : ℝ))) z)

Tactic:
simp only [Real.rpow_mul hz r n, Real.rpow_natCast]

Premises used: Nat.cast, Real.rpow_mul, Real.rpow_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hre : Tendsto re l atTop
n : ℕ
hr : IsBigO (F := ℝ) l im fun (z : ℂ) ↦ z.re ^ n
⊢ IsExpCmpFilter l

Tactic:
of_isBigO_im_re_rpow hre n <| mod_cast hr

Premises used: congrArg, Complex.im, Asymptotics.IsBigO, cast, Nat.cast, Complex.IsExpCmpFilter.of_isBigO_im_re_rpow, Complex.re, funext, Eq.symm, Real.rpow_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hre : Tendsto re l atTop
him : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (z : ℂ) ↦ |z.im|
⊢ IsBigO (F := ℝ) l im fun (z : ℂ) ↦ HPow.hPow (β := ℕ) z.re 0

Tactic:
simpa only [pow_zero] using him.isBigO_const (f := im) one_ne_zero

Premises used: Filter.IsBoundedUnder.isBigO_const, pow_zero, one_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hre : Tendsto re l atTop
him_le : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l im
him_ge : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) l im
⊢ IsExpCmpFilter l

Tactic:
of_boundedUnder_abs_im hre <| isBoundedUnder_le_abs.2 ⟨him_le, him_ge⟩

Premises used: Iff.mpr, And.intro, Filter.isBoundedUnder_le_abs, Complex.IsExpCmpFilter.of_boundedUnder_abs_im
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
⊢ ∀ᶠ (w : ℂ) in l, w ≠ 0

Tactic:
hl.tendsto_re.eventually_ne_atTop' _

Premises used: Filter.Tendsto.eventually_ne_atTop', Complex.IsExpCmpFilter.tendsto_re
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
⊢ Tendsto (β := ℝ) (fun (z : ℂ) ↦ |z.re|) l atTop

Tactic:
tendsto_abs_atTop_atTop.comp hl.tendsto_re

Premises used: abs, Complex.IsExpCmpFilter.tendsto_re, Filter.Tendsto.comp, Filter.tendsto_abs_atTop_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
⊢ Tendsto norm l atTop

Tactic:
tendsto_atTop_mono abs_re_le_norm hl.tendsto_abs_re

Premises used: Filter.tendsto_atTop_mono, Complex.abs_re_le_norm, Complex.IsExpCmpFilter.tendsto_abs_re
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
⊢ IsLittleO (E := ℝ) l (fun (z : ℂ) ↦ Real.log z.re) re

Tactic:
Real.isLittleO_log_id_atTop.comp_tendsto hl.tendsto_re

Premises used: Real.isLittleO_log_id_atTop, Complex.IsExpCmpFilter.tendsto_re, Real.log, dite, Asymptotics.IsLittleO.comp_tendsto
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
⊢ Eq (α := (z : ℂ) → ℝ) (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (z.im ^ n) 2) fun (z : ℂ) ↦ z.im ^ (2 * n)

Tactic:
simp only [pow_mul']

Premises used: pow_mul'
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
⊢ Eq (α := (z : ℂ) → ℝ) (fun (z : ℂ) ↦ Real.exp z.re) fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (Real.exp z.re) 1

Tactic:
simp only [pow_one]

Premises used: pow_one
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
⊢ l.EventuallyLE (β := ℝ) (fun (z : ℂ) ↦ |z.im| ^ n) fun (z : ℂ) ↦ Real.exp z.re

Tactic:
simpa using (hl.isLittleO_im_pow_exp_re n).bound zero_lt_one

Premises used: Asymptotics.IsLittleO.bound, zero_lt_one, Complex.IsExpCmpFilter.isLittleO_im_pow_exp_re
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
⊢ 0 < √2

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
⊢ 0 < √2

Tactic:
have h2 : 0 < √2 := by simp
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
⊢ 1 ≤ ‖z‖

Tactic:
have hz' : 1 ≤ ‖z‖ := hz.trans (re_le_norm z)
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
⊢ 0 < max z.re |z.im|

Tactic:
have hm₀ : 0 < max z.re |z.im| := lt_max_iff.2 (Or.inl <| one_pos.trans_le hz)
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < max z.re |z.im|
simp : Real.log ‖z‖ ≤ Real.log √2 + Real.log (max z.re |z.im|)
⊢ LE.le (α := ℝ) ((fun (x : ℂ) ↦ ‖Real.log ‖x‖‖) z) ((fun (z : ℂ) ↦ Real.log √2 + Real.log (max z.re |z.im|)) z)

Tactic:
simp only [Real.norm_of_nonneg (Real.log_nonneg hz')]

Premises used: Real.log_nonneg, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < max z.re |z.im|
rw : ‖z‖ ≤ √2 * max |z.re| |z.im|
h : 0 < ‖z‖
h₁ : 0 < √2 * max z.re |z.im|
hx : √2 ≠ 0
hy : max z.re |z.im| ≠ 0
⊢ Real.log ‖z‖ ≤ Real.log √2 + Real.log (max z.re |z.im|)

Tactic:
rw [← Real.log_mul, Real.log_le_log_iff, ← abs_of_nonneg (le_trans zero_le_one hz)]

Premises used: zero_le_one, Real.log_le_log_iff, abs_of_nonneg, Real.log_mul, le_trans
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < max z.re |z.im|
⊢ ‖z‖ ≤ √2 * max |z.re| |z.im|

Tactic:
norm_le_sqrt_two_mul_max z

Premises used: Complex.norm_le_sqrt_two_mul_max
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < max z.re |z.im|
⊢ 0 < ‖z‖

Tactic:
one_pos.trans_le hz'

Premises used: LT.lt.trans_le, one_pos
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < max z.re |z.im|
⊢ 0 < √2 * max z.re |z.im|

Tactic:
mul_pos h2 hm₀

Premises used: mul_pos
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < max z.re |z.im|
⊢ √2 ≠ 0

Tactic:
h2.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < max z.re |z.im|
⊢ max z.re |z.im| ≠ 0

Tactic:
hm₀.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < max z.re |z.im|
⊢ ‖z‖ ≤ √2 * max |z.re| |z.im|

Tactic:
exacts [norm_le_sqrt_two_mul_max z, one_pos.trans_le hz', mul_pos h2 hm₀, h2.ne', hm₀.ne']

Premises used: LT.lt.ne', mul_pos, LT.lt.trans_le, Complex.norm_le_sqrt_two_mul_max, one_pos
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
h :
  ∀ (z : ℂ) (hre : (↑n : ℝ) * ‖Real.log z.re‖ ≤ ‖z.re‖) (him : |z.im| ^ n ≤ Real.exp z.re) (h₁ : 1 < z.re),
    (↑n : ℝ) * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖
⊢ ∀ᶠ (x : ℂ) in l, (↑n : ℝ) * ‖Real.log (max x.re |x.im|)‖ ≤ ‖x.re‖

Tactic:
filter_upwards [isLittleO_iff_nat_mul_le'.1 hl.isLittleO_log_re_re n,
            hl.abs_im_pow_eventuallyLE_exp_re n,
            hl.tendsto_re.eventually_gt_atTop 1] with z hre him h₁

Premises used: Complex.IsExpCmpFilter.tendsto_re, Iff.mp, Complex.IsExpCmpFilter.isLittleO_log_re_re, Complex.IsExpCmpFilter.abs_im_pow_eventuallyLE_exp_re, OfNat.ofNat, Filter.Tendsto.eventually_gt_atTop, Asymptotics.isLittleO_iff_nat_mul_le'
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : (↑n : ℝ) * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ n ≤ Real.exp z.re
h₁ : 1 < z.re
h : ∀ (hle : |z.im| ≤ z.re), (↑n : ℝ) * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖
h₂ : ∀ (hle : z.re ≤ |z.im|), (↑n : ℝ) * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖
⊢ (↑n : ℝ) * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖

Tactic:
rcases le_total |z.im| z.re with hle | hle

Premises used: abs, Complex.im, le_total, Complex.re
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : (↑n : ℝ) * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ n ≤ Real.exp z.re
h₁ : 1 < z.re
hle : |z.im| ≤ z.re
h h₂ h₃ h₄ : (↑n : ℝ) * ‖Real.log z.re‖ ≤ ‖z.re‖
⊢ (↑n : ℝ) * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖

Tactic:
rwa [max_eq_left hle]

Premises used: max_eq_left
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : (↑n : ℝ) * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ n ≤ Real.exp z.re
h₁ : 1 < z.re
hle : z.re ≤ |z.im|
⊢ 1 < |z.im|

Tactic:
have H : 1 < |z.im| := h₁.trans_le hle
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : (↑n : ℝ) * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ n ≤ Real.exp z.re
h₁ : 1 < z.re
hle : z.re ≤ |z.im|
H : 1 < |z.im|
⊢ 1 < z.re

Tactic:
norm_cast at *
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : (↑n : ℝ) * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ n ≤ Real.exp z.re
h₁ : 1 < z.re
hle : z.re ≤ |z.im|
H : 1 < |z.im|
h₂ : 1 < z.re
⊢ 1 < |z.im|

Tactic:
norm_cast at *