awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
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
⊢ ∀ᶠ (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
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
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
⊢ 0 < 1 / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s)) 1

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
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
⊢ ∀ᶠ (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)
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
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
funProp : ∀ x ∈ s, x ≠ 0
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) s

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
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
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) s

Tactic:
have hcont : ContinuousOn (fun x => ‖log x‖ ^ 2) s := by fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
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
funProp : ∀ x ∈ s, x ≠ 0
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ ‖log x‖) s

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
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
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ ‖log x‖) s

Tactic:
have hcont' : ContinuousOn (fun x => ‖log x‖) s := by fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
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 : ℝ
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)) ≤ ε
⊢ 0 < p ∧ 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₂⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
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
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)) ≤ ε
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 0,
    ∀ x ∈ s, Membership.mem (γ := Set (ℝ × ℝ)) {p : ℝ × ℝ | dist p.1 p.2 ≤ ε} (log x, n⁻¹ * (x ^ n - 1))

Tactic:
filter_upwards [h₁, h₂] with p ⟨hp₁,hp₂⟩ hp₃
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
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‖ = p * ‖log x‖

Tactic:
grind [norm_mul, Real.norm_of_nonneg]

Premises used: norm_mul, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
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
ha : 0 ≤ ‖log x‖
⊢ p * ‖log x‖ ≤ 1 / HAdd.hAdd (α := ℝ) (sSup ((fun (y : ℝ) ↦ ‖log y‖) '' s)) 1 * ‖log x‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
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
hbc : ‖log x‖ ≤ sSup ((fun (y : ℝ) ↦ ‖log y‖) '' s)
⊢ 1 / HAdd.hAdd (α := ℝ) (sSup ((fun (y : ℝ) ↦ ‖log y‖) '' s)) 1 * ‖log x‖ ≤ 1 / (‖log x‖ + 1) * ‖log x‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
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
⊢ Membership.mem (γ := Set ℝ) ((fun (y : ℝ) ↦ ‖log y‖) '' s) ‖log x‖

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
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
hbc : BddAbove (α := ℝ) ((fun (y : ℝ) ↦ ‖log y‖) '' s)
⊢ ‖log x‖ ≤ sSup ((fun (y : ℝ) ↦ ‖log y‖) '' s)

Tactic:
refine le_csSup ?_ (by grind)

Premises used: le_csSup
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
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
⊢ BddAbove (α := ℝ) ((fun (y : ℝ) ↦ ‖log y‖) '' s)

Tactic:
grind [IsCompact.bddAbove, ← IsCompact.image_of_continuousOn]

Premises used: IsCompact.bddAbove, IsCompact.image_of_continuousOn
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
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 / (‖log x‖ + 1) * ‖log x‖ = ‖log x‖ / (‖log x‖ + 1)

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
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
rw : ‖log x‖ ≤ ‖log x‖ + 1
rw₁ : 0 < ‖log x‖ + 1
⊢ ‖log x‖ / (‖log x‖ + 1) ≤ 1

Tactic:
rw [div_le_one₀]

Premises used: div_le_one₀
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
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‖ ≤ ‖log x‖ + 1

Tactic:
grind [norm_nonneg]

Premises used: norm_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
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
⊢ 0 < ‖log x‖ + 1

Tactic:
grind [norm_nonneg]

Premises used: norm_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
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

Tactic:
have hx' : ‖p * log x‖ ≤ 1 := calc
    _ = p * ‖log x‖ := by grind [norm_mul, Real.norm_of_nonneg]
    _ ≤ 1 / (sSup ((fun y => ‖log y‖) '' s) + 1) * ‖log x‖ := by gcongr
    _ ≤ 1 / (‖log x‖ + 1) * ‖log x‖ := by
        gcongr
        refine le_csSup ?_ (by grind)
        grind [IsCompact.bddAbove, ← IsCompact.image_of_continuousOn]
    _ = ‖log x‖ / (‖log x‖ + 1) := by grind
    _ ≤ 1 := by rw [div_le_one₀] <;> grind [norm_nonneg]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
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
hx' : ‖p * log x‖ ≤ 1
⊢ 0 ≤ p⁻¹

Tactic:
grind [_root_.inv_nonneg]

Premises used: inv_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
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
hx' : ‖p * log x‖ ≤ 1
⊢ 0 ≤ p⁻¹

Tactic:
have pinv_nonneg : 0 ≤ p⁻¹ := by grind [_root_.inv_nonneg]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
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
hx' : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
h : ‖p⁻¹ * (x ^ p - 1) - log x‖ ≤ ε
⊢ dist (log x) (p⁻¹ * (x ^ p - 1)) ≤ ε

Tactic:
rw [dist_eq_norm']

Premises used: dist_eq_norm'
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
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
hx' : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
⊢ ‖p⁻¹ * (x ^ p - 1) - log x‖ ≤ p * HPow.hPow (β := ℕ) ‖log x‖ 2

Tactic:
Real.norm_inv_mul_rpow_sub_one_sub_log_le hp₁ (hs hx) hx'

Premises used: Real.norm_inv_mul_rpow_sub_one_sub_log_le
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
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
hx' : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
hbc : HPow.hPow (β := ℕ) ‖log x‖ 2 ≤ sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)
⊢ p * HPow.hPow (β := ℕ) ‖log x‖ 2 ≤ p * sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
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
hx' : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
⊢ Membership.mem (γ := Set ℝ) ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s) (HPow.hPow (β := ℕ) ‖log x‖ 2)

Tactic:
grind