awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h :
  Eq (α := Set ℝ) (Set.Ioi 0.5)
    (Set.preimage (β := ℝ) (⇑(HSMul.hSMul (α := ℝ) (β := ℝ →ₗ[ℝ] ℝ) 2 LinearMap.id) : (a : ℝ) → ℝ) (Set.Ioi 1))
⊢ ConcaveOn ℝ (β := ℝ) (Set.Ioi 0.5) fun (x : ℝ) ↦ √(2 * x) * log (2 * x)

Tactic:
convert!
        ((strictConcaveOn_sqrt_mul_log_Ioi.concaveOn.comp_linearMap ((2 : ℝ) • LinearMap.id)))
        using 1

Premises used: LinearMap.id, ConcaveOn.comp_linearMap, strictConcaveOn_sqrt_mul_log_Ioi, HSMul.hSMul, StrictConcaveOn.concaveOn, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Set.Ioi 0.5) x ↔
      Membership.mem (γ := Set ℝ)
        (Set.preimage (β := ℝ) (⇑(HSMul.hSMul (α := ℝ) (β := ℝ →ₗ[ℝ] ℝ) 2 LinearMap.id) : (a : ℝ) → ℝ) (Set.Ioi 1)) x
⊢ Eq (α := Set ℝ) (Set.Ioi 0.5)
    (Set.preimage (β := ℝ) (⇑(HSMul.hSMul (α := ℝ) (β := ℝ →ₗ[ℝ] ℝ) 2 LinearMap.id) : (a : ℝ) → ℝ) (Set.Ioi 1))

Tactic:
ext x
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x_1 : ℝ
x_large : 512 ≤ x_1
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x_1
x : ℝ
h : 0.5 < x ↔ 1 < 2 * x
⊢ Membership.mem (γ := Set ℝ) (Set.Ioi 0.5) x ↔
    Membership.mem (γ := Set ℝ)
      (Set.preimage (β := ℝ) (⇑(HSMul.hSMul (α := ℝ) (β := ℝ →ₗ[ℝ] ℝ) 2 LinearMap.id) : (a : ℝ) → ℝ) (Set.Ioi 1)) x

Tactic:
simp only [Set.mem_Ioi, Set.mem_preimage, LinearMap.smul_apply,
        LinearMap.id_coe, id_eq, smul_eq_mul]

Premises used: LinearMap.smul_apply, LinearMap.id_coe, Set.mem_Ioi, smul_eq_mul, Set.mem_preimage, id_eq
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x_1 : ℝ
x_large : 512 ≤ x_1
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x_1
x : ℝ
h : HMul.hMul (α := ℝ) 2 0.5 < 2 * x ↔ 1 < 2 * x
⊢ 0.5 < x ↔ 1 < 2 * x

Tactic:
rw [← mul_lt_mul_iff_right₀ (two_pos)]

Premises used: two_pos, mul_lt_mul_iff_right₀
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x_1 : ℝ
x_large : 512 ≤ x_1
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x_1
x : ℝ
h : 1 < 2 * x ↔ 1 < 2 * x
⊢ HMul.hMul (α := ℝ) 2 0.5 < 2 * x ↔ 1 < 2 * x

Tactic:
norm_num1
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x_1 : ℝ
x_large : 512 ≤ x_1
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x_1
x : ℝ
⊢ 1 < 2 * x ↔ 1 < 2 * x

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
hg : 0 ≤ log 4 / 3
hg₁ : ConvexOn ℝ (β := ℝ) (Set.Ioi 0.5) fun (x : ℝ) ↦ x
⊢ ConvexOn ℝ (E := ℝ) (Set.Ioi 0.5) (HMul.hMul (log 4 / 3))

Tactic:
apply ConvexOn.smul

Premises used: ConvexOn.smul
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
⊢ LE.le (α := ℝ) 1 4

Tactic:
norm_num1
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
⊢ LE.le (α := ℝ) 0 3

Tactic:
norm_num1
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
⊢ 0 ≤ log 4 / 3

Tactic:
refine div_nonneg (log_nonneg (by norm_num1)) (by norm_num1)

Premises used: Real.log_nonneg, div_nonneg
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
⊢ ConvexOn ℝ (β := ℝ) (Set.Ioi 0.5) fun (x : ℝ) ↦ x

Tactic:
convexOn_id (convex_Ioi (0.5 : ℝ))

Premises used: convexOn_id, OfScientific.ofScientific, Bool.true, convex_Ioi
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
⊢ ConvexOn ℝ (β := ℝ) (Set.Ioi 0.5) fun (x : ℝ) ↦ x

Tactic:
exact convexOn_id (convex_Ioi (0.5 : ℝ))

Premises used: convexOn_id, OfScientific.ofScientific, Bool.true, convex_Ioi
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
⊢ ConcaveOn ℝ (Set.Ioi 0.5) f

Tactic:
have h : ConcaveOn ℝ (Set.Ioi 0.5) f := by
    apply ConcaveOn.sub
    · apply ConcaveOn.add
      · exact strictConcaveOn_log_Ioi.concaveOn.subset
          (Set.Ioi_subset_Ioi (by norm_num)) (convex_Ioi 0.5)
      convert!
        ((strictConcaveOn_sqrt_mul_log_Ioi.concaveOn.comp_linearMap ((2 : ℝ) • LinearMap.id)))
        using 1
      ext x
      simp only [Set.mem_Ioi, Set.mem_preimage, LinearMap.smul_apply,
        LinearMap.id_coe, id_eq, smul_eq_mul]
      rw [← mul_lt_mul_iff_right₀ (two_pos)]
      norm_num1
      rfl
    apply ConvexOn.smul
    · refine div_nonneg (log_nonneg (by norm_num1)) (by norm_num1)
    · exact convexOn_id (convex_Ioi (0.5 : ℝ))
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : ∃ (x1 : ℝ) (x2 : ℝ), 0.5 < x1 ∧ x1 < x2 ∧ x2 ≤ x ∧ 0 ≤ f x1 ∧ f x2 ≤ 0
obtain : ∀ (x1 x2 : ℝ) (h1 : 0.5 < x1) (h2 : x1 < x2) (h0 : x2 ≤ x) (h3 : 0 ≤ f x1) (h4 : f x2 ≤ 0), f x ≤ 0
⊢ f x ≤ 0

Tactic:
obtain ⟨x1, x2, h1, h2, h0, h3, h4⟩ := this
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
x1 x2 : ℝ
h1 : 0.5 < x1
h2 : x1 < x2
h0 : x2 ≤ x
h3 : 0 ≤ f x1
h4 : f x2 ≤ 0
⊢ f x ≤ 0

Tactic:
(h.right_le_of_le_left'' h1 ((h1.trans h2).trans_le h0) h2 h0 (h4.trans h3)).trans h4

Premises used: ConcaveOn.right_le_of_le_left'', LT.lt.trans_le, LT.lt.trans, LE.le.trans
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
x1 x2 : ℝ
h1 : 0.5 < x1
h2 : x1 < x2
h0 : x2 ≤ x
h3 : 0 ≤ f x1
h4 : f x2 ≤ 0
⊢ f x ≤ 0

Tactic:
exact (h.right_le_of_le_left'' h1 ((h1.trans h2).trans_le h0) h2 h0 (h4.trans h3)).trans h4

Premises used: ConcaveOn.right_le_of_le_left'', LT.lt.trans_le, LT.lt.trans, LE.le.trans
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
suffices : ∃ (x1 : ℝ) (x2 : ℝ), 0.5 < x1 ∧ x1 < x2 ∧ x2 ≤ x ∧ 0 ≤ f x1 ∧ f x2 ≤ 0
⊢ f x ≤ 0

Tactic:
suffices ∃ x1 x2, 0.5 < x1 ∧ x1 < x2 ∧ x2 ≤ x ∧ 0 ≤ f x1 ∧ f x2 ≤ 0 by
    obtain ⟨x1, x2, h1, h2, h0, h3, h4⟩ := this
    exact (h.right_le_of_le_left'' h1 ((h1.trans h2).trans_le h0) h2 h0 (h4.trans h3)).trans h4
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
⊢ LT.lt (α := ℝ) 0.5 18

Tactic:
norm_num1
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
⊢ LT.lt (α := ℝ) 18 512

Tactic:
norm_num1
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
refine_1 : 0 ≤ f 18
refine_2 : f 512 ≤ 0
⊢ ∃ (x1 : ℝ) (x2 : ℝ), 0.5 < x1 ∧ x1 < x2 ∧ x2 ≤ x ∧ 0 ≤ f x1 ∧ f x2 ≤ 0

Tactic:
refine ⟨18, 512, by norm_num1, by norm_num1, x_large, ?_, ?_⟩
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
⊢ LT.lt (α := ℝ) 0 6

Tactic:
norm_num1
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
⊢ HMul.hMul (α := ℝ) 6 6 = HMul.hMul (α := ℝ) 2 18

Tactic:
norm_num1
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
⊢ √(HMul.hMul (α := ℝ) 2 18) = 6

Tactic:
have : √(2 * 18 : ℝ) = 6 := (sqrt_eq_iff_mul_self_eq_of_pos (by norm_num1)).mpr (by norm_num1)
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(HMul.hMul (α := ℝ) 2 18) = 6
⊢ LT.lt (α := ℝ) 0 18

Tactic:
norm_num1
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(HMul.hMul (α := ℝ) 2 18) = 6
⊢ 0 < 18 * HMul.hMul (α := ℝ) 2 18 ^ √(HMul.hMul (α := ℝ) 2 18) / HPow.hPow (α := ℝ) 4 (18 / 3)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(HMul.hMul (α := ℝ) 2 18) = 6
⊢ 0 < HPow.hPow (α := ℝ) 4 (18 / 3)

Tactic:
norm_num1
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(HMul.hMul (α := ℝ) 2 18) = 6
refine_1 : HPow.hPow (α := ℝ) 4 (18 / 3) ≤ 18 * HPow.hPow (β := ℝ) (HMul.hMul (α := ℝ) 2 18) 6
⊢ 0 ≤ f 18

Tactic:
rw [hf _ (by norm_num1), log_nonneg_iff (by positivity), this, one_le_div (by norm_num1)]

Premises used: one_le_div, Real.log_nonneg_iff
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(HMul.hMul (α := ℝ) 2 18) = 6
⊢ HPow.hPow (α := ℝ) 4 (18 / 3) ≤ 18 * HPow.hPow (β := ℝ) (HMul.hMul (α := ℝ) 2 18) 6

Tactic:
norm_num1
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
⊢ LT.lt (α := ℝ) 0 32

Tactic:
norm_num1
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
⊢ HMul.hMul (α := ℝ) 32 32 = HMul.hMul (α := ℝ) 2 512

Tactic:
norm_num1
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
⊢ √(HMul.hMul (α := ℝ) 2 512) = 32

Tactic:
have : √(2 * 512) = 32 :=
      (sqrt_eq_iff_mul_self_eq_of_pos (by norm_num1)).mpr (by norm_num1)
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(HMul.hMul (α := ℝ) 2 512) = 32
⊢ LT.lt (α := ℝ) 0 512

Tactic:
norm_num1
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(HMul.hMul (α := ℝ) 2 512) = 32
⊢ 0 < HPow.hPow (α := ℝ) 4 (512 / 3)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(HMul.hMul (α := ℝ) 2 512) = 32
refine_2 : 512 * HPow.hPow (β := ℝ) (HMul.hMul (α := ℝ) 2 512) 32 ≤ HPow.hPow (α := ℝ) 4 (512 / 3)
⊢ f 512 ≤ 0

Tactic:
rw [hf _ (by norm_num1), log_nonpos_iff (hf' _ (by norm_num1)).le, this,
        div_le_one (by positivity)]

Premises used: LT.lt.le, div_le_one, Real.log_nonpos_iff
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(HMul.hMul (α := ℝ) 2 512) = 32
⊢ 512 = HPow.hPow (α := ℝ) (β := ℕ) 2 9

Tactic:
norm_num1
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(HMul.hMul (α := ℝ) 2 512) = 32
refine_2 :
  HPow.hPow (α := ℝ) (β := ℕ) 2 9 * HPow.hPow (β := ℝ) (HMul.hMul (α := ℝ) 2 512) 32 ≤ HPow.hPow (α := ℝ) 4 (512 / 3)
⊢ 512 * HPow.hPow (β := ℝ) (HMul.hMul (α := ℝ) 2 512) 32 ≤ HPow.hPow (α := ℝ) 4 (512 / 3)

Tactic:
conv in 512 => equals 2 ^ 9 => norm_num1
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(HMul.hMul (α := ℝ) 2 512) = 32
⊢ HMul.hMul (α := ℝ) 2 512 = HPow.hPow (α := ℝ) (β := ℕ) 2 10

Tactic:
norm_num1
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(HMul.hMul (α := ℝ) 2 512) = 32
refine_2 :
  HPow.hPow (α := ℝ) (β := ℕ) 2 9 * HPow.hPow (β := ℝ) (HPow.hPow (α := ℝ) (β := ℕ) 2 10) 32 ≤
    HPow.hPow (α := ℝ) 4 (512 / 3)
⊢ HPow.hPow (α := ℝ) (β := ℕ) 2 9 * HPow.hPow (β := ℝ) (HMul.hMul (α := ℝ) 2 512) 32 ≤ HPow.hPow (α := ℝ) 4 (512 / 3)

Tactic:
conv in 2 * 512 => equals 2 ^ 10 => norm_num1
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(HMul.hMul (α := ℝ) 2 512) = 32
refine_2 : HPow.hPow (α := ℝ) 2 (9 + HMul.hMul (α := ℕ) 10 32) ≤ HPow.hPow (α := ℝ) 4 (512 / 3)
⊢ HPow.hPow (α := ℝ) (β := ℕ) 2 9 * HPow.hPow (β := ℝ) (HPow.hPow (α := ℝ) (β := ℕ) 2 10) (↑32 : ℝ) ≤
    HPow.hPow (α := ℝ) 4 (512 / 3)

Tactic:
rw [rpow_natCast, ← pow_mul, ← pow_add]

Premises used: pow_add, pow_mul, Real.rpow_natCast
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(HMul.hMul (α := ℝ) 2 512) = 32
rw : 4 = HPow.hPow (α := ℝ) (β := ℕ) 2 2
⊢ 4 = HPow.hPow (α := ℝ) (β := ℝ) 2 2

Tactic:
rw [rpow_two]

Premises used: Real.rpow_two
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(HMul.hMul (α := ℝ) 2 512) = 32
⊢ 4 = HPow.hPow (α := ℝ) (β := ℕ) 2 2

Tactic:
norm_num1
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(HMul.hMul (α := ℝ) 2 512) = 32
refine_2 : HPow.hPow (α := ℝ) 2 (9 + HMul.hMul (α := ℕ) 10 32) ≤ HPow.hPow (α := ℝ) (β := ℝ) 2 2 ^ (512 / 3)
⊢ HPow.hPow (α := ℝ) 2 (9 + HMul.hMul (α := ℕ) 10 32) ≤ HPow.hPow (α := ℝ) 4 (512 / 3)

Tactic:
conv in 4 => equals 2 ^ (2 : ℝ) => rw [rpow_two]; norm_num1

Premises used: Real.rpow_two, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(HMul.hMul (α := ℝ) 2 512) = 32
refine_2 : HPow.hPow (α := ℝ) (β := ℝ) 2 (↑(9 + HMul.hMul (α := ℕ) 10 32) : ℝ) ≤ HPow.hPow (α := ℝ) 2 (2 * (512 / 3))
refine_2₁ : LE.le (α := ℝ) 0 2
⊢ HPow.hPow (α := ℝ) 2 (9 + HMul.hMul (α := ℕ) 10 32) ≤ HPow.hPow (α := ℝ) (β := ℝ) 2 2 ^ (512 / 3)

Tactic:
rw [← rpow_mul, ← rpow_natCast]

Premises used: Real.rpow_mul, Real.rpow_natCast
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(HMul.hMul (α := ℝ) 2 512) = 32
refine_2 : LE.le (α := ℝ) 1 2
refine_2₁ : (↑(9 + HMul.hMul (α := ℕ) 10 32) : ℝ) ≤ 2 * (512 / 3)
⊢ HPow.hPow (α := ℝ) (β := ℝ) 2 (↑(9 + HMul.hMul (α := ℕ) 10 32) : ℝ) ≤ HPow.hPow (α := ℝ) 2 (2 * (512 / 3))

Tactic:
apply rpow_le_rpow_of_exponent_le

Premises used: Real.rpow_le_rpow_of_exponent_le