awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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 : ℝ)
h1 : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ * (↑q : ℝ) < p * (↑q : ℝ)
⊢ HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ * (↑q : ℝ) = HSub.hSub (α := ℝ) (↑q : ℝ) 1
have calc : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ * (↑q : ℝ) = (↑q : ℝ) - HMul.hMul (α := ℝ) (↑q : ℝ)⁻¹ (↑q : ℝ)
Tactic: calc (1 - (q : ℝ)⁻¹) * ↑q
            _ = q - (q : ℝ)⁻¹ * (q : ℝ) := by ring
            _ = q - 1 := by simp [qpos.ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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 : ℝ)
h1 : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ * (↑q : ℝ) < p * (↑q : ℝ)
calc : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ * (↑q : ℝ) = (↑q : ℝ) - HMul.hMul (α := ℝ) (↑q : ℝ)⁻¹ (↑q : ℝ)
⊢ HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ * (↑q : ℝ) = HSub.hSub (α := ℝ) (↑q : ℝ) 1
have calc₁ : (↑q : ℝ) - HMul.hMul (α := ℝ) (↑q : ℝ)⁻¹ (↑q : ℝ) = HSub.hSub (α := ℝ) (↑q : ℝ) 1
Tactic: calc (1 - (q : ℝ)⁻¹) * ↑q
            _ = q - (q : ℝ)⁻¹ * (q : ℝ) := by ring
            _ = q - 1 := by simp [qpos.ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
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 : ℝ)
h1 : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ * (↑q : ℝ) < p * (↑q : ℝ)
⊢ HSub.hSub (α := ℝ) (↑q : ℝ) 1 < p * (↑q : ℝ)
have h2 : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ * (↑q : ℝ) = HSub.hSub (α := ℝ) (↑q : ℝ) 1
Tactic: have h2 : (1 - (q : ℝ)⁻¹) * ↑q = q - 1 := by calc (1 - (q : ℝ)⁻¹) * ↑q
            _ = q - (q : ℝ)⁻¹ * (q : ℝ) := by ring
            _ = q - 1 := by simp [qpos.ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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 : ℝ)
h1 : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ * (↑q : ℝ) < p * (↑q : ℝ)
h2 : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ * (↑q : ℝ) = HSub.hSub (α := ℝ) (↑q : ℝ) 1
⊢ HSub.hSub (α := ℝ) (↑q : ℝ) 1 < p * (↑q : ℝ)
have rwa : ∀ (h1 : HSub.hSub (α := ℝ) (↑q : ℝ) 1 < p * (↑q : ℝ))
  (h2 : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ * (↑q : ℝ) = HSub.hSub (α := ℝ) (↑q : ℝ) 1),
  HSub.hSub (α := ℝ) (↑q : ℝ) 1 < p * (↑q : ℝ)
Tactic: rwa [h2] at h1
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
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 : ℝ)
⊢ HAdd.hAdd (α := ℝ) (-1) (↑q : ℝ) - (↑q : ℝ) * p + p < p
have this₁ : 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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 : ℝ)
⊢ HAdd.hAdd (α := ℝ) (-1) (↑q : ℝ) - (↑q : ℝ) * p + p < p
have nlinarith : p ≤ HAdd.hAdd (α := ℝ) (-1) (↑q : ℝ) - (↑q : ℝ) * p + p →
  HSub.hSub (α := ℝ) (↑q : ℝ) 1 - p * (↑q : ℝ) + (p - (HAdd.hAdd (α := ℝ) (-1) (↑q : ℝ) - (↑q : ℝ) * p + p)) = 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
⊢ StrictMonoOn binEntropy (Icc 0 2⁻¹)
have rw : StrictMonoOn (qaryEntropy 2) (Icc 0 (1 - 1 / 2))
Tactic: rw [show Icc (0 : ℝ) 2⁻¹ = Icc 0 (1 - 1 / 2) by norm_num, ← qaryEntropy_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
⊢ StrictAntiOn binEntropy (Icc 2⁻¹ 1)
have rw : StrictAntiOn (qaryEntropy 2) (Icc (1 / 2) 1)
Tactic: rw [show (Icc (2⁻¹ : ℝ) 1) = Icc (1 / 2) 1 by norm_num, ← qaryEntropy_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
⊢ StrictAntiOn (qaryEntropy 2) (Icc (1 / 2) 1)
have h : Icc (1 / 2) 1 = Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑2 : ℝ)) 1
Tactic: convert! qaryEntropy_strictAntiOn (by rfl) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
⊢ StrictConcaveOn ℝ (Icc 0 1) (qaryEntropy q)
have apply : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (interior (Icc 0 1)) x → deriv^[2] (qaryEntropy q) x < 0
Tactic: apply strictConcaveOn_of_deriv2_neg (convex_Icc 0 1) qaryEntropy_continuous.continuousOn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
p : ℝ
hp : Membership.mem (γ := Set ℝ) (interior (Icc 0 1)) p
⊢ deriv^[2] (qaryEntropy q) p < 0
have rw : -1 / (p * (1 - p)) < 0
Tactic: rw [deriv2_qaryEntropy]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
q : ℕ
p : ℝ
hp : Membership.mem (γ := Set ℝ) (interior (Icc 0 1)) p
⊢ -1 / (p * (1 - p)) < 0
have hp₁ : 0 < p ∧ p < 1
Tactic: simp_all only [interior_Icc, mem_Ioo]
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
p : ℝ
hp : 0 < p ∧ p < 1
⊢ -1 / (p * (1 - p)) < 0
have ha : LT.lt (α := ℝ) (-1) 0
Tactic: apply div_neg_of_neg_of_pos
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
p : ℝ
hp : 0 < p ∧ p < 1
ha : LT.lt (α := ℝ) (-1) 0
⊢ -1 / (p * (1 - p)) < 0
have hb : 0 < p * (1 - p)
Tactic: apply div_neg_of_neg_of_pos
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Choose (goal)
Goal:
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)
have succ : IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ HMul.hMul (α := ℝ) (↑(n - k) : ℝ) (↑(n.descFactorial k) : ℝ)) fun (n : ℕ) ↦
  (↑n : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) k
Tactic: simp_rw [descFactorial_succ, cast_mul, _root_.pow_succ']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Choose (goal)
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
have succ : IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑(n - k) : ℝ)) Nat.cast
Tactic: refine IsEquivalent.mul ?_ h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Choose (hypothesis)
Goal:
k : ℕ
h : IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑(n.descFactorial k) : ℝ)) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k
⊢ IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑(n - k) : ℝ)) Nat.cast
have hz : ∀ᶠ (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)⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Choose (goal)
Goal:
k : ℕ
h : IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑(n.descFactorial k) : ℝ)) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k
hz : ∀ᶠ (x : ℕ) in atTop, Ne (α := ℝ) (↑x : ℝ) 0
⊢ IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑(n - k) : ℝ)) Nat.cast
have succ : Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℕ → ℝ) (β := ℕ → ℝ) (fun (n : ℕ) ↦ (↑(n - k) : ℝ)) Nat.cast (n + k))
  atTop (𝓝 1)
Tactic: rw [isEquivalent_iff_tendsto_one hz, ← tendsto_add_atTop_iff_nat k]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Choose (goal)
Goal:
k : ℕ
⊢ IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑(n.descFactorial k) : ℝ)) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k
have zero : IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑(n.descFactorial 0) : ℝ)) fun (n : ℕ) ↦
  HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 0
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 : ℝ)
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Choose (goal)
Goal:
k : ℕ
zero :
  IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑(n.descFactorial 0) : ℝ)) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 0
⊢ IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑(n.descFactorial k) : ℝ)) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k
have 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)
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 : ℝ)
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Choose (goal)
Goal:
k n : ℕ
| (↑(n.choose k) : ℝ)
have h : HDiv.hDiv (α := ℝ) (↑(n.descFactorial k) : ℝ) (↑k ! : ℝ)
Tactic: rw [choose_eq_descFactorial_div_factorial,
      cast_div (n.factorial_dvd_descFactorial k) (mod_cast k.factorial_ne_zero)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Choose (goal)
Goal:
k : ℕ
⊢ IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑(n.choose k) : ℝ)) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑n : ℝ) k / (↑k ! : ℝ)
have conv_lhs : IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(n.descFactorial k) : ℝ) (↑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)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Choose (goal)
Goal:
k : ℕ
⊢ IsTheta (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(n.choose k) : ℝ)) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k
have apply : IsTheta (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k / (↑k ! : ℝ)) fun (n : ℕ) ↦
  HPow.hPow (α := ℝ) (↑n : ℝ) k
Tactic: apply (isEquivalent_choose k).trans_isTheta
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Choose (goal)
Goal:
k : ℕ
⊢ IsTheta (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k / (↑k ! : ℝ)) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑n : ℝ) k
have simp_rw : IsTheta (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑k ! : ℝ)⁻¹ * HPow.hPow (α := ℝ) (↑n : ℝ) k) fun (n : ℕ) ↦
  HPow.hPow (α := ℝ) (↑n : ℝ) k
Tactic: simp_rw [div_eq_mul_inv, mul_comm _ (_⁻¹)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.CompareExp (hypothesis)
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
⊢ LE.le (α := ℝ) ((fun (x : ℂ) ↦ ‖Real.log ‖x‖‖) z) ((fun (z : ℂ) ↦ Real.log √2 + Real.log (max z.re |z.im|)) z)
have h2 : 0 < √2
Tactic: have h2 : 0 < √2 := by simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.CompareExp (hypothesis)
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
⊢ LE.le (α := ℝ) ((fun (x : ℂ) ↦ ‖Real.log ‖x‖‖) z) ((fun (z : ℂ) ↦ Real.log √2 + Real.log (max z.re |z.im|)) z)
have hz' : 1 ≤ ‖z‖
Tactic: have hz' : 1 ≤ ‖z‖ := hz.trans (re_le_norm z)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.CompareExp (hypothesis)
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
⊢ LE.le (α := ℝ) ((fun (x : ℂ) ↦ ‖Real.log ‖x‖‖) z) ((fun (z : ℂ) ↦ Real.log √2 + Real.log (max z.re |z.im|)) z)
have hm₀ : 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)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.CompareExp (goal)
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < 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)
have simp : Real.log ‖z‖ ≤ Real.log √2 + Real.log (max z.re |z.im|)
Tactic: simp only [Real.norm_of_nonneg (Real.log_nonneg hz')]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.CompareExp (goal)
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < max z.re |z.im|
⊢ Real.log ‖z‖ ≤ Real.log √2 + Real.log (max z.re |z.im|)
have rw : ‖z‖ ≤ √2 * max |z.re| |z.im|
Tactic: rw [← Real.log_mul, Real.log_le_log_iff, ← abs_of_nonneg (le_trans zero_le_one hz)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.CompareExp (goal)
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|
⊢ Real.log ‖z‖ ≤ Real.log √2 + Real.log (max z.re |z.im|)
have h : 0 < ‖z‖
Tactic: rw [← Real.log_mul, Real.log_le_log_iff, ← abs_of_nonneg (le_trans zero_le_one hz)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.CompareExp (goal)
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‖
⊢ Real.log ‖z‖ ≤ Real.log √2 + Real.log (max z.re |z.im|)
have h₁ : 0 < √2 * max z.re |z.im|
Tactic: rw [← Real.log_mul, Real.log_le_log_iff, ← abs_of_nonneg (le_trans zero_le_one hz)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.CompareExp (goal)
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|
⊢ Real.log ‖z‖ ≤ Real.log √2 + Real.log (max z.re |z.im|)
have hx : √2 ≠ 0
Tactic: rw [← Real.log_mul, Real.log_le_log_iff, ← abs_of_nonneg (le_trans zero_le_one hz)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.CompareExp (goal)
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
⊢ Real.log ‖z‖ ≤ Real.log √2 + Real.log (max z.re |z.im|)
have hy : max z.re |z.im| ≠ 0
Tactic: rw [← Real.log_mul, Real.log_le_log_iff, ← abs_of_nonneg (le_trans zero_le_one hz)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.CompareExp (goal)
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
⊢ ∀ᶠ (x : ℂ) in l, (↑n : ℝ) * ‖Real.log (max x.re |x.im|)‖ ≤ ‖x.re‖
have 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‖
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₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.CompareExp (goal)
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
⊢ (↑n : ℝ) * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖
have h : ∀ (hle : |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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.CompareExp (goal)
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‖
⊢ (↑n : ℝ) * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖
have h₂ : ∀ (hle : z.re ≤ |z.im|), (↑n : ℝ) * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖
Tactic: rcases le_total |z.im| z.re with hle | hle
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.CompareExp (hypothesis)
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|
⊢ (↑n : ℝ) * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖
have H : 1 < |z.im|
Tactic: have H : 1 < |z.im| := h₁.trans_le hle
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.CompareExp (goal)
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : (↑n : ℝ) * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ n ≤ Real.exp z.re
hle : z.re ≤ |z.im|
h₁ : 1 < z.re
H : 1 < |z.im|
⊢ (↑n : ℝ) * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖
have h : (↑n : ℝ) * ‖Real.log |z.im|‖ ≤ ‖z.re‖
Tactic: rwa [max_eq_right hle, Real.norm_eq_abs, Real.norm_eq_abs, abs_of_pos (Real.log_pos H),
              ← Real.log_pow, Real.log_le_iff_le_exp (pow_pos (one_pos.trans H) _),
              abs_of_pos (one_pos.trans h₁)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.CompareExp (goal)
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : (↑n : ℝ) * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ n ≤ Real.exp z.re
hle : z.re ≤ |z.im|
h₁ : 1 < z.re
H : 1 < |z.im|
h : (↑n : ℝ) * ‖Real.log |z.im|‖ ≤ ‖z.re‖
⊢ (↑n : ℝ) * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖
have h₂ : (↑n : ℝ) * |Real.log |z.im|| ≤ ‖z.re‖
Tactic: rwa [max_eq_right hle, Real.norm_eq_abs, Real.norm_eq_abs, abs_of_pos (Real.log_pos H),
              ← Real.log_pow, Real.log_le_iff_le_exp (pow_pos (one_pos.trans H) _),
              abs_of_pos (one_pos.trans h₁)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.CompareExp (goal)
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : (↑n : ℝ) * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ n ≤ Real.exp z.re
hle : z.re ≤ |z.im|
h₁ : 1 < z.re
H : 1 < |z.im|
h : (↑n : ℝ) * ‖Real.log |z.im|‖ ≤ ‖z.re‖
h₂ : (↑n : ℝ) * |Real.log |z.im|| ≤ ‖z.re‖
⊢ (↑n : ℝ) * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖
have h₃ : (↑n : ℝ) * |Real.log |z.im|| ≤ |z.re|
Tactic: rwa [max_eq_right hle, Real.norm_eq_abs, Real.norm_eq_abs, abs_of_pos (Real.log_pos H),
              ← Real.log_pow, Real.log_le_iff_le_exp (pow_pos (one_pos.trans H) _),
              abs_of_pos (one_pos.trans h₁)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.CompareExp (goal)
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : (↑n : ℝ) * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ n ≤ Real.exp z.re
hle : z.re ≤ |z.im|
h₁ : 1 < z.re
H : 1 < |z.im|
h : (↑n : ℝ) * ‖Real.log |z.im|‖ ≤ ‖z.re‖
h₂ : (↑n : ℝ) * |Real.log |z.im|| ≤ ‖z.re‖
h₃ : (↑n : ℝ) * |Real.log |z.im|| ≤ |z.re|
⊢ (↑n : ℝ) * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖
have h₄ : (↑n : ℝ) * Real.log |z.im| ≤ |z.re|
Tactic: rwa [max_eq_right hle, Real.norm_eq_abs, Real.norm_eq_abs, abs_of_pos (Real.log_pos H),
              ← Real.log_pow, Real.log_le_iff_le_exp (pow_pos (one_pos.trans H) _),
              abs_of_pos (one_pos.trans h₁)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.CompareExp (goal)
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : (↑n : ℝ) * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ n ≤ Real.exp z.re
hle : z.re ≤ |z.im|
h₁ : 1 < z.re
H : 1 < |z.im|
h : (↑n : ℝ) * ‖Real.log |z.im|‖ ≤ ‖z.re‖
h₂ : (↑n : ℝ) * |Real.log |z.im|| ≤ ‖z.re‖
h₃ : (↑n : ℝ) * |Real.log |z.im|| ≤ |z.re|
h₄ : (↑n : ℝ) * Real.log |z.im| ≤ |z.re|
⊢ (↑n : ℝ) * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖
have h₅ : Real.log (|z.im| ^ n) ≤ |z.re|
Tactic: rwa [max_eq_right hle, Real.norm_eq_abs, Real.norm_eq_abs, abs_of_pos (Real.log_pos H),
              ← Real.log_pow, Real.log_le_iff_le_exp (pow_pos (one_pos.trans H) _),
              abs_of_pos (one_pos.trans h₁)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.CompareExp (goal)
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : (↑n : ℝ) * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ n ≤ Real.exp z.re
hle : z.re ≤ |z.im|
h₁ : 1 < z.re
H : 1 < |z.im|
h : (↑n : ℝ) * ‖Real.log |z.im|‖ ≤ ‖z.re‖
h₂ : (↑n : ℝ) * |Real.log |z.im|| ≤ ‖z.re‖
h₃ : (↑n : ℝ) * |Real.log |z.im|| ≤ |z.re|
h₄ : (↑n : ℝ) * Real.log |z.im| ≤ |z.re|
h₅ : Real.log (|z.im| ^ n) ≤ |z.re|
⊢ (↑n : ℝ) * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖
have h₆ : |z.im| ^ n ≤ Real.exp |z.re|
Tactic: rwa [max_eq_right hle, Real.norm_eq_abs, Real.norm_eq_abs, abs_of_pos (Real.log_pos H),
              ← Real.log_pow, Real.log_le_iff_le_exp (pow_pos (one_pos.trans H) _),
              abs_of_pos (one_pos.trans h₁)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.CompareExp (goal)
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
a : ℂ
b : ℝ
hb : 0 < b
⊢ IsLittleO (E := ℝ) (F := ℝ) l (fun (z : ℂ) ↦ Real.exp (a.re * Real.log ‖z‖)) fun (x : ℂ) ↦ ‖cexp ((↑b : ℂ) * x)‖
have simp : Tendsto (β := ℝ) (fun (x : ℂ) ↦ b * x.re - a.re * Real.log ‖x‖) l atTop
Tactic: simp only [norm_exp, re_ofReal_mul, Real.isLittleO_exp_comp_exp_comp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.CompareExp (goal)
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
a : ℂ
b : ℝ
hb : 0 < b
⊢ Tendsto (β := ℝ) (fun (x : ℂ) ↦ b * x.re - a.re * Real.log ‖x‖) l atTop
have refine : IsLittleO (E := ℝ) (F := ℝ) l (fun (x : ℂ) ↦ a.re * Real.log ‖x‖) fun (x : ℂ) ↦ b * x.re
Tactic: refine (IsEquivalent.refl.sub_isLittleO ?_).symm.tendsto_atTop
          (hl.tendsto_re.const_mul_atTop hb)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.CompareExp (goal)
Goal:
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ z : ℂ
hz : z ≠ 0
⊢ z ^ a₁ * cexp ((↑b₁ : ℂ) * z) = z ^ a₂ * cexp ((↑b₁ : ℂ) * z) * z ^ (a₁ - a₂)
have rw : z ^ a₁ * cexp ((↑b₁ : ℂ) * z) = z ^ a₂ * z ^ (a₁ - a₂) * cexp ((↑b₁ : ℂ) * z)
Tactic: rw [mul_right_comm, ← cpow_add _ _ hz, add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.CompareExp (goal)
Goal:
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ z : ℂ
hz : z ≠ 0
rw : z ^ a₁ * cexp ((↑b₁ : ℂ) * z) = z ^ a₂ * z ^ (a₁ - a₂) * cexp ((↑b₁ : ℂ) * z)
⊢ z ^ a₁ * cexp ((↑b₁ : ℂ) * z) = z ^ a₂ * cexp ((↑b₁ : ℂ) * z) * z ^ (a₁ - a₂)
have rw₁ : z ^ a₁ * cexp ((↑b₁ : ℂ) * z) = z ^ (a₂ + (a₁ - a₂)) * cexp ((↑b₁ : ℂ) * z)
Tactic: rw [mul_right_comm, ← cpow_add _ _ hz, add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.CompareExp (goal)
Goal:
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ z : ℂ
hz : z ≠ 0
rw : z ^ a₁ * cexp ((↑b₁ : ℂ) * z) = z ^ a₂ * z ^ (a₁ - a₂) * cexp ((↑b₁ : ℂ) * z)
rw₁ : z ^ a₁ * cexp ((↑b₁ : ℂ) * z) = z ^ (a₂ + (a₁ - a₂)) * cexp ((↑b₁ : ℂ) * z)
⊢ z ^ a₁ * cexp ((↑b₁ : ℂ) * z) = z ^ a₂ * cexp ((↑b₁ : ℂ) * z) * z ^ (a₁ - a₂)
have rw₂ : z ^ a₁ * cexp ((↑b₁ : ℂ) * z) = z ^ a₁ * cexp ((↑b₁ : ℂ) * z)
Tactic: rw [mul_right_comm, ← cpow_add _ _ hz, add_sub_cancel]