awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
calc : log⁺ (∑ t ∈ s, f t) = log⁺ |∑ t ∈ s, f t|
calc₁ : log⁺ |∑ t ∈ s, f t| ≤ log⁺ (∑ t ∈ s, |f t|)
calc₂ : log⁺ (∑ t ∈ s, |f t|) ≤ log⁺ (∑ t ∈ s, |f t_max|)
calc₃ : log⁺ (∑ t ∈ s, |f t_max|) = log⁺ ((↑s.card : ℝ) * |f t_max|)
⊢ log⁺ (∑ t ∈ s, f t) ≤ log (↑s.card : ℝ) + ∑ t ∈ s, log⁺ (f t)
have calc₄ : log (↑s.card : ℝ) + log⁺ |f t_max| ≤ log (↑s.card : ℝ) + ∑ t ∈ s, log⁺ (f t)
Tactic: calc log⁺ (∑ t ∈ s, f t)
  _ = log⁺ |∑ t ∈ s, f t| := by
    rw [Real.posLog_abs]
  _ ≤ log⁺ (∑ t ∈ s, |f t|) := by
    apply monotoneOn_posLog (by simp) (by simp [Finset.sum_nonneg])
    simp [Finset.abs_sum_le_sum_abs]
  _ ≤ log⁺ (∑ t ∈ s, |f t_max|) := by
    apply monotoneOn_posLog (by simp [Finset.sum_nonneg]) (by simp [mul_nonneg])
    apply Finset.sum_le_sum (fun i ih ↦ ht_max.2 i ih)
  _ = log⁺ (s.card * |f t_max|) := by
    simp [Finset.sum_const]
  _ ≤ log s.card + log⁺ |f t_max| := posLog_nat_mul
  _ ≤ log s.card + ∑ t ∈ s, log⁺ (f t) := by
    gcongr
    rw [posLog_abs]
    apply Finset.single_le_sum (fun _ _ ↦ posLog_nonneg) ht_max.1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
α : Type u_2
s : Finset α
f : α → E
⊢ log⁺ (Norm.norm.{u_1} (E := E) (∑ t ∈ s, f t)) ≤ log (↑s.card : ℝ) + ∑ t ∈ s, log⁺ ‖f t‖
have h₁ : LE.le (α := ℝ) 0 (Norm.norm.{u_1} (E := E) (∑ i ∈ s, f i))
Tactic: grw [norm_sum_le, posLog_sum]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
α : Type u_2
s : Finset α
f : α → E
h₁ : LE.le (α := ℝ) 0 (Norm.norm.{u_1} (E := E) (∑ i ∈ s, f i))
⊢ log⁺ (Norm.norm.{u_1} (E := E) (∑ t ∈ s, f t)) ≤ log (↑s.card : ℝ) + ∑ t ∈ s, log⁺ ‖f t‖
have grw : log⁺ (∑ i ∈ s, ‖f i‖) ≤ log (↑s.card : ℝ) + ∑ t ∈ s, log⁺ ‖f t‖
Tactic: grw [norm_sum_le, posLog_sum]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
α : Type u_2
s : Finset α
f : α → E
h₁ : LE.le (α := ℝ) 0 (Norm.norm.{u_1} (E := E) (∑ i ∈ s, f i))
grw : log⁺ (∑ i ∈ s, ‖f i‖) ≤ log (↑s.card : ℝ) + ∑ t ∈ s, log⁺ ‖f t‖
⊢ log⁺ (Norm.norm.{u_1} (E := E) (∑ t ∈ s, f t)) ≤ log (↑s.card : ℝ) + ∑ t ∈ s, log⁺ ‖f t‖
have grw₁ : log (↑s.card : ℝ) + ∑ t ∈ s, log⁺ ‖f t‖ ≤ log (↑s.card : ℝ) + ∑ t ∈ s, log⁺ ‖f t‖
Tactic: grw [norm_sum_le, posLog_sum]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
x y : ℝ
⊢ log⁺ (x + y) ≤ log 2 + log⁺ x + log⁺ y
have h : log⁺ (x + y) = log⁺ (∑ t : Fin (Nat.succ 0).succ, ![x, y] t)
Tactic: convert! posLog_sum Finset.univ ![x, y] using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
x y : ℝ
h : log⁺ (x + y) = log⁺ (∑ t : Fin (Nat.succ 0).succ, ![x, y] t)
⊢ log⁺ (x + y) ≤ log 2 + log⁺ x + log⁺ y
have h₁ : log 2 + log⁺ x + log⁺ y =
  log (↑(Finset.card (α := Fin (Nat.succ 0).succ) Finset.univ) : ℝ) + ∑ t : Fin (Nat.succ 0).succ, log⁺ (![x, y] t)
Tactic: convert! posLog_sum Finset.univ ![x, y] using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
a b : E
⊢ log⁺ ‖a + b‖ ≤ log⁺ ‖a‖ + log⁺ ‖b‖ + log 2
have h₁ : LE.le (α := ℝ) 0 ‖a + b‖
Tactic: grw [norm_add_le, posLog_add, add_rotate]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
a b : E
h₁ : LE.le (α := ℝ) 0 ‖a + b‖
⊢ log⁺ ‖a + b‖ ≤ log⁺ ‖a‖ + log⁺ ‖b‖ + log 2
have grw : log⁺ (‖a‖ + ‖b‖) ≤ log⁺ ‖a‖ + log⁺ ‖b‖ + log 2
Tactic: grw [norm_add_le, posLog_add, add_rotate]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
a b : E
h₁ : LE.le (α := ℝ) 0 ‖a + b‖
grw : log⁺ (‖a‖ + ‖b‖) ≤ log⁺ ‖a‖ + log⁺ ‖b‖ + log 2
⊢ log⁺ ‖a + b‖ ≤ log⁺ ‖a‖ + log⁺ ‖b‖ + log 2
have grw₁ : log 2 + log⁺ ‖a‖ + log⁺ ‖b‖ ≤ log⁺ ‖a‖ + log⁺ ‖b‖ + log 2
Tactic: grw [norm_add_le, posLog_add, add_rotate]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
a b : E
h₁ : LE.le (α := ℝ) 0 ‖a + b‖
grw : log⁺ (‖a‖ + ‖b‖) ≤ log⁺ ‖a‖ + log⁺ ‖b‖ + log 2
grw₁ : log 2 + log⁺ ‖a‖ + log⁺ ‖b‖ ≤ log⁺ ‖a‖ + log⁺ ‖b‖ + log 2
⊢ log⁺ ‖a + b‖ ≤ log⁺ ‖a‖ + log⁺ ‖b‖ + log 2
have grw₂ : log⁺ ‖a‖ + log⁺ ‖b‖ + log 2 ≤ log⁺ ‖a‖ + log⁺ ‖b‖ + log 2
Tactic: grw [norm_add_le, posLog_add, add_rotate]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (hypothesis)
Goal:
p x : ℝ
p_pos : 0 < p
x_pos : 0 < x
hx : ‖p * log x‖ ≤ 1
⊢ ‖p⁻¹ * (x ^ p - 1) - log x‖ ≤ p * HPow.hPow (β := ℕ) ‖log x‖ 2
have pinv_nonneg : 0 ≤ p⁻¹
Tactic: have pinv_nonneg : 0 ≤ p⁻¹ := by grind [_root_.inv_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (goal)
Goal:
p x : ℝ
p_pos : 0 < p
x_pos : 0 < x
hx : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
⊢ ‖p⁻¹ * (x ^ p - 1 - p * log x)‖ = p⁻¹ * ‖rexp (p * log x) - 1 - p * log x‖
have simp : p⁻¹ * ‖x ^ p - 1 - p * log x‖ = p⁻¹ * ‖rexp (p * log x) - 1 - p * log x‖
Tactic: simp only [norm_mul, Real.norm_of_nonneg (r := p⁻¹) pinv_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (goal)
Goal:
p x : ℝ
p_pos : 0 < p
x_pos : 0 < x
hx : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
⊢ p⁻¹ * ‖x ^ p - 1 - p * log x‖ = p⁻¹ * ‖rexp (p * log x) - 1 - p * log x‖
have e_a : x ^ p = rexp (p * log x)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (goal)
Goal:
p x : ℝ
p_pos : 0 < p
x_pos : 0 < x
hx : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
⊢ x ^ p = rexp (p * log x)
have e_a : x ^ p = rexp (log x * p)
Tactic: rw [mul_comm, Real.exp_mul, Real.exp_log (by grind)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (goal)
Goal:
p x : ℝ
p_pos : 0 < p
x_pos : 0 < x
hx : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
e_a : x ^ p = rexp (log x * p)
⊢ x ^ p = rexp (p * log x)
have e_a₁ : x ^ p = rexp (log x) ^ p
Tactic: rw [mul_comm, Real.exp_mul, Real.exp_log (by grind)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (goal)
Goal:
p x : ℝ
p_pos : 0 < p
x_pos : 0 < x
hx : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
e_a : x ^ p = rexp (log x * p)
e_a₁ : x ^ p = rexp (log x) ^ p
⊢ x ^ p = rexp (p * log x)
have e_a₂ : x ^ p = x ^ p
Tactic: rw [mul_comm, Real.exp_mul, Real.exp_log (by grind)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (goal)
Goal:
p x : ℝ
p_pos : 0 < p
x_pos : 0 < x
hx : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
⊢ p⁻¹ * ‖rexp (p * log x) - 1 - p * log x‖ ≤ p⁻¹ * HPow.hPow (β := ℕ) ‖p * log x‖ 2
have hbc : ‖rexp (p * log x) - 1 - p * log x‖ ≤ HPow.hPow (β := ℕ) ‖p * log x‖ 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (goal)
Goal:
p x : ℝ
p_pos : 0 < p
x_pos : 0 < x
hx : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
⊢ p⁻¹ * HPow.hPow (β := ℕ) ‖p * log x‖ 2 = p * HPow.hPow (β := ℕ) ‖log x‖ 2
have simp : p⁻¹ * HPow.hPow (β := ℕ) (‖p‖ * ‖log x‖) 2 = p * HPow.hPow (β := ℕ) ‖log x‖ 2
Tactic: simp only [norm_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (goal)
Goal:
p x : ℝ
p_pos : 0 < p
x_pos : 0 < x
hx : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
⊢ ‖p⁻¹ * (x ^ p - 1) - log x‖ ≤ p * HPow.hPow (β := ℕ) ‖log x‖ 2
have _ : ‖p⁻¹ * (x ^ p - 1) - log x‖ = ‖p⁻¹ * (x ^ p - 1 - p * log x)‖
Tactic: calc
    _ = ‖p⁻¹ * ((x ^ p - 1) - p * log x)‖ := by grind
    _ = p⁻¹ * ‖(rexp (p * log x) - 1) - p * log x‖ := by
          simp only [norm_mul, Real.norm_of_nonneg (r := p⁻¹) pinv_nonneg]
          congr
          rw [mul_comm, Real.exp_mul, Real.exp_log (by grind)]
    _ ≤ p⁻¹ * ‖p * log x‖ ^ 2 := by
          gcongr
          refine Real.norm_exp_sub_one_sub_id_le ?_
          simp only [hx]
    _ = p * ‖log x‖ ^ 2 := by
          simp only [norm_mul]
          grind [Real.norm_of_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (goal)
Goal:
p x : ℝ
p_pos : 0 < p
x_pos : 0 < x
hx : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
_ : ‖p⁻¹ * (x ^ p - 1) - log x‖ = ‖p⁻¹ * (x ^ p - 1 - p * log x)‖
⊢ ‖p⁻¹ * (x ^ p - 1) - log x‖ ≤ p * HPow.hPow (β := ℕ) ‖log x‖ 2
have _₁ : ‖p⁻¹ * (x ^ p - 1 - p * log x)‖ = p⁻¹ * ‖rexp (p * log x) - 1 - p * log x‖
Tactic: calc
    _ = ‖p⁻¹ * ((x ^ p - 1) - p * log x)‖ := by grind
    _ = p⁻¹ * ‖(rexp (p * log x) - 1) - p * log x‖ := by
          simp only [norm_mul, Real.norm_of_nonneg (r := p⁻¹) pinv_nonneg]
          congr
          rw [mul_comm, Real.exp_mul, Real.exp_log (by grind)]
    _ ≤ p⁻¹ * ‖p * log x‖ ^ 2 := by
          gcongr
          refine Real.norm_exp_sub_one_sub_id_le ?_
          simp only [hx]
    _ = p * ‖log x‖ ^ 2 := by
          simp only [norm_mul]
          grind [Real.norm_of_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (goal)
Goal:
p x : ℝ
p_pos : 0 < p
x_pos : 0 < x
hx : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
_ : ‖p⁻¹ * (x ^ p - 1) - log x‖ = ‖p⁻¹ * (x ^ p - 1 - p * log x)‖
_₁ : ‖p⁻¹ * (x ^ p - 1 - p * log x)‖ = p⁻¹ * ‖rexp (p * log x) - 1 - p * log x‖
⊢ ‖p⁻¹ * (x ^ p - 1) - log x‖ ≤ p * HPow.hPow (β := ℕ) ‖log x‖ 2
have _₂ : p⁻¹ * ‖rexp (p * log x) - 1 - p * log x‖ ≤ p⁻¹ * HPow.hPow (β := ℕ) ‖p * log x‖ 2
Tactic: calc
    _ = ‖p⁻¹ * ((x ^ p - 1) - p * log x)‖ := by grind
    _ = p⁻¹ * ‖(rexp (p * log x) - 1) - p * log x‖ := by
          simp only [norm_mul, Real.norm_of_nonneg (r := p⁻¹) pinv_nonneg]
          congr
          rw [mul_comm, Real.exp_mul, Real.exp_log (by grind)]
    _ ≤ p⁻¹ * ‖p * log x‖ ^ 2 := by
          gcongr
          refine Real.norm_exp_sub_one_sub_id_le ?_
          simp only [hx]
    _ = p * ‖log x‖ ^ 2 := by
          simp only [norm_mul]
          grind [Real.norm_of_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (goal)
Goal:
p x : ℝ
p_pos : 0 < p
x_pos : 0 < x
hx : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
_ : ‖p⁻¹ * (x ^ p - 1) - log x‖ = ‖p⁻¹ * (x ^ p - 1 - p * log x)‖
_₁ : ‖p⁻¹ * (x ^ p - 1 - p * log x)‖ = p⁻¹ * ‖rexp (p * log x) - 1 - p * log x‖
_₂ : p⁻¹ * ‖rexp (p * log x) - 1 - p * log x‖ ≤ p⁻¹ * HPow.hPow (β := ℕ) ‖p * log x‖ 2
⊢ ‖p⁻¹ * (x ^ p - 1) - log x‖ ≤ p * HPow.hPow (β := ℕ) ‖log x‖ 2
have _₃ : p⁻¹ * HPow.hPow (β := ℕ) ‖p * log x‖ 2 = p * HPow.hPow (β := ℕ) ‖log x‖ 2
Tactic: calc
    _ = ‖p⁻¹ * ((x ^ p - 1) - p * log x)‖ := by grind
    _ = p⁻¹ * ‖(rexp (p * log x) - 1) - p * log x‖ := by
          simp only [norm_mul, Real.norm_of_nonneg (r := p⁻¹) pinv_nonneg]
          congr
          rw [mul_comm, Real.exp_mul, Real.exp_log (by grind)]
    _ ≤ p⁻¹ * ‖p * log x‖ ^ 2 := by
          gcongr
          refine Real.norm_exp_sub_one_sub_id_le ?_
          simp only [hx]
    _ = p * ‖log x‖ ^ 2 := by
          simp only [norm_mul]
          grind [Real.norm_of_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (goal)
Goal:
⊢ TendstoLocallyUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) log (𝓝[>] 0) (Ioi 0)
have refine : ∀ K ⊆ Ioi 0, IsCompact K → TendstoUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) log (𝓝[>] 0) K
Tactic: refine (tendstoLocallyUniformlyOn_iff_forall_isCompact isOpen_Ioi).mpr ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (goal)
Goal:
s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
⊢ TendstoUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) log (𝓝[>] 0) s
have rw : ∀ (i : ℝ),
  0 < i →
    ∀ᶠ (n : ℝ) in 𝓝[>] 0,
      ∀ x ∈ s, Membership.mem (γ := Set (ℝ × ℝ)) {p : ℝ × ℝ | dist p.1 p.2 ≤ i} (log x, n⁻¹ * (x ^ n - 1))
Tactic: rw [Metric.uniformity_basis_dist_le.tendstoUniformlyOn_iff_of_uniformity]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (hypothesis)
Goal:
s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ε / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)) 1
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 0,
    ∀ x ∈ s, Membership.mem (γ := Set (ℝ × ℝ)) {p : ℝ × ℝ | dist p.1 p.2 ≤ ε} (log x, n⁻¹ * (x ^ n - 1))
have hxs : ∀ x ∈ s, x ≠ 0
Tactic: have hxs : ∀ x ∈ s, x ≠ 0 := by grind
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (goal)
Goal:
s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ε / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)) 1
hxs : ∀ x ∈ s, x ≠ 0
⊢ LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s))
have refine : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s) x → 0 ≤ x
Tactic: refine Real.sSup_nonneg ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (hypothesis)
Goal:
s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ε / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)) 1
hxs : ∀ x ∈ s, x ≠ 0
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 0,
    ∀ x ∈ s, Membership.mem (γ := Set (ℝ × ℝ)) {p : ℝ × ℝ | dist p.1 p.2 ≤ ε} (log x, n⁻¹ * (x ^ n - 1))
have sSup_nonneg : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s))
Tactic: have sSup_nonneg : 0 ≤ sSup ((fun x => ‖log x‖ ^ 2) '' s) := by
    refine Real.sSup_nonneg ?_
    grind [← sq_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (goal)
Goal:
s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ε / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)) 1
hxs : ∀ x ∈ s, x ≠ 0
sSup_nonneg : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s))
⊢ LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s))
have refine : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ((fun (x : ℝ) ↦ ‖log x‖) '' s) x → 0 ≤ x
Tactic: refine Real.sSup_nonneg ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (hypothesis)
Goal:
s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ε / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)) 1
hxs : ∀ x ∈ s, x ≠ 0
sSup_nonneg : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s))
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 0,
    ∀ x ∈ s, Membership.mem (γ := Set (ℝ × ℝ)) {p : ℝ × ℝ | dist p.1 p.2 ≤ ε} (log x, n⁻¹ * (x ^ n - 1))
have sSup_nonneg' : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s))
Tactic: have sSup_nonneg' : 0 ≤ sSup ((fun x => ‖log x‖) '' s) := by
    refine Real.sSup_nonneg ?_
    grind [← sq_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (hypothesis)
Goal:
s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ε / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)) 1
hxs : ∀ x ∈ s, x ≠ 0
sSup_nonneg : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s))
sSup_nonneg' : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s))
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 0,
    ∀ x ∈ s, Membership.mem (γ := Set (ℝ × ℝ)) {p : ℝ × ℝ | dist p.1 p.2 ≤ ε} (log x, n⁻¹ * (x ^ n - 1))
have pbound_pos : 0 < pbound
Tactic: have pbound_pos : 0 < pbound := by positivity
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (hypothesis)
Goal:
s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ε / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)) 1
hxs : ∀ x ∈ s, x ≠ 0
sSup_nonneg : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s))
sSup_nonneg' : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s))
pbound_pos : 0 < pbound
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 0,
    ∀ x ∈ s, Membership.mem (γ := Set (ℝ × ℝ)) {p : ℝ × ℝ | dist p.1 p.2 ≤ ε} (log x, n⁻¹ * (x ^ n - 1))
have h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < pbound
Tactic: have h₁ : ∀ᶠ p : ℝ in 𝓝[>] 0, 0 < p ∧ p < pbound := nhdsGT_basis 0 |>.mem_of_mem pbound_pos
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (hypothesis)
Goal:
s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ε / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)) 1
hxs : ∀ x ∈ s, x ≠ 0
sSup_nonneg : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s))
sSup_nonneg' : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s))
pbound_pos : 0 < pbound
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < pbound
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 0,
    ∀ x ∈ s, Membership.mem (γ := Set (ℝ × ℝ)) {p : ℝ × ℝ | dist p.1 p.2 ≤ ε} (log x, n⁻¹ * (x ^ n - 1))
have h₂ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, p ≤ 1 / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s)) 1
Tactic: have h₂ : ∀ᶠ p : ℝ in 𝓝[>] 0, p ≤ 1 / (sSup ((fun x => ‖log x‖) '' s) + 1) :=
    Eventually.filter_mono nhdsWithin_le_nhds <| eventually_le_nhds (by positivity)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (hypothesis)
Goal:
s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ε / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)) 1
hxs : ∀ x ∈ s, x ≠ 0
sSup_nonneg : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s))
sSup_nonneg' : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s))
pbound_pos : 0 < pbound
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < pbound
h₂ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, p ≤ 1 / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s)) 1
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 0,
    ∀ x ∈ s, Membership.mem (γ := Set (ℝ × ℝ)) {p : ℝ × ℝ | dist p.1 p.2 ≤ ε} (log x, n⁻¹ * (x ^ n - 1))
have hcont : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) s
Tactic: have hcont : ContinuousOn (fun x => ‖log x‖ ^ 2) s := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (hypothesis)
Goal:
s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ε / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)) 1
hxs : ∀ x ∈ s, x ≠ 0
sSup_nonneg : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s))
sSup_nonneg' : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s))
pbound_pos : 0 < pbound
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < pbound
h₂ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, p ≤ 1 / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s)) 1
hcont : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) s
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 0,
    ∀ x ∈ s, Membership.mem (γ := Set (ℝ × ℝ)) {p : ℝ × ℝ | dist p.1 p.2 ≤ ε} (log x, n⁻¹ * (x ^ n - 1))
have hcont' : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ ‖log x‖) s
Tactic: have hcont' : ContinuousOn (fun x => ‖log x‖) s := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (goal)
Goal:
s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ε / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)) 1
hxs : ∀ x ∈ s, x ≠ 0
sSup_nonneg : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s))
sSup_nonneg' : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s))
pbound_pos : 0 < pbound
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < pbound
h₂ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, p ≤ 1 / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s)) 1
hcont : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) s
hcont' : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ ‖log x‖) s
p : ℝ
⊢ 0 < p ∧ p < pbound →
    p ≤ 1 / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s)) 1 → ∀ x ∈ s, dist (log x) (p⁻¹ * (x ^ p - 1)) ≤ ε
have h : ∀ (hp₁ : 0 < p) (hp₂ : p < pbound),
  p ≤ 1 / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s)) 1 → ∀ x ∈ s, dist (log x) (p⁻¹ * (x ^ p - 1)) ≤ ε
Tactic: ⟨hp₁,hp₂⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (goal)
Goal:
s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ε / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)) 1
hxs : ∀ x ∈ s, x ≠ 0
sSup_nonneg : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s))
sSup_nonneg' : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s))
pbound_pos : 0 < pbound
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < pbound
h₂ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, p ≤ 1 / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s)) 1
hcont : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) s
hcont' : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ ‖log x‖) s
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 0,
    ∀ x ∈ s, Membership.mem (γ := Set (ℝ × ℝ)) {p : ℝ × ℝ | dist p.1 p.2 ≤ ε} (log x, n⁻¹ * (x ^ n - 1))
have h : ∀ (p : ℝ) (hp₁ : 0 < p) (hp₂ : p < pbound) (hp₃ : p ≤ 1 / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s)) 1),
  ∀ x ∈ s, dist (log x) (p⁻¹ * (x ^ p - 1)) ≤ ε
Tactic: filter_upwards [h₁, h₂] with p ⟨hp₁,hp₂⟩ hp₃
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (goal)
Goal:
s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ε / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)) 1
hxs : ∀ x ∈ s, x ≠ 0
sSup_nonneg : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s))
sSup_nonneg' : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s))
pbound_pos : 0 < pbound
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < pbound
h₂ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, p ≤ 1 / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s)) 1
hcont : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) s
hcont' : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ ‖log x‖) s
p : ℝ
hp₁ : 0 < p
hp₂ : p < pbound
hp₃ : p ≤ 1 / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s)) 1
x : ℝ
hx : x ∈ s
⊢ p * ‖log x‖ ≤ 1 / HAdd.hAdd (α := ℝ) (sSup ((fun (y : ℝ) ↦ ‖log y‖) '' s)) 1 * ‖log x‖
have ha : 0 ≤ ‖log x‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (goal)
Goal:
s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ε / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)) 1
hxs : ∀ x ∈ s, x ≠ 0
sSup_nonneg : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s))
sSup_nonneg' : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s))
pbound_pos : 0 < pbound
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < pbound
h₂ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, p ≤ 1 / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s)) 1
hcont : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) s
hcont' : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ ‖log x‖) s
p : ℝ
hp₁ : 0 < p
hp₂ : p < pbound
hp₃ : p ≤ 1 / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s)) 1
x : ℝ
hx : x ∈ s
⊢ 1 / HAdd.hAdd (α := ℝ) (sSup ((fun (y : ℝ) ↦ ‖log y‖) '' s)) 1 * ‖log x‖ ≤ 1 / (‖log x‖ + 1) * ‖log x‖
have hbc : ‖log x‖ ≤ sSup ((fun (y : ℝ) ↦ ‖log y‖) '' s)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (goal)
Goal:
s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ε / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)) 1
hxs : ∀ x ∈ s, x ≠ 0
sSup_nonneg : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s))
sSup_nonneg' : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s))
pbound_pos : 0 < pbound
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < pbound
h₂ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, p ≤ 1 / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s)) 1
hcont : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) s
hcont' : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ ‖log x‖) s
p : ℝ
hp₁ : 0 < p
hp₂ : p < pbound
hp₃ : p ≤ 1 / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s)) 1
x : ℝ
hx : x ∈ s
⊢ ‖log x‖ ≤ sSup ((fun (y : ℝ) ↦ ‖log y‖) '' s)
have hbc : BddAbove (α := ℝ) ((fun (y : ℝ) ↦ ‖log y‖) '' s)
Tactic: refine le_csSup ?_ (by grind)