awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < y - x
hxy' : 0 < x / y
hxy'' : x / y ≠ 1
x₁ : y⁻¹ * (y - x) = 1 - x / y
x₂ : 1 - x / y < -log (x / y)
x₃ : -log (x / y) = -(log x - log y)
⊢ y⁻¹ * (y - x) < log y - log x
have x₄ : -(log x - log y) = log y - log x
Tactic: calc
      y⁻¹ * (y - x) = 1 - x / y := by field
      _ < -log (x / y) := by linarith [log_lt_sub_one_of_pos hxy' hxy'']
      _ = -(log x - log y) := by rw [log_div hx.ne' hy.ne']
      _ = log y - log x := by ring
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (hypothesis)
Goal:
s : ℝ
hs : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
⊢ 1 + p * s < (1 + s) ^ p
have hp' : 0 < p
Tactic: have hp' : 0 < p := zero_lt_one.trans hp
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
⊢ 1 + p * s < (1 + s) ^ p
have inl : ∀ (hs : LE.le (α := ℝ) (-1) (-1)) (hs' : Ne (α := ℝ) (-1) 0), 1 + p * -1 < HAdd.hAdd (α := ℝ) 1 (-1) ^ p
Tactic: rcases eq_or_lt_of_le hs with rfl | hs
Cleared hypotheses: s, hs, hs'
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
inl : ∀ (hs : LE.le (α := ℝ) (-1) (-1)) (hs' : Ne (α := ℝ) (-1) 0), 1 + p * -1 < HAdd.hAdd (α := ℝ) 1 (-1) ^ p
⊢ 1 + p * s < (1 + s) ^ p
have inr : ∀ (hs : -1 < s), 1 + p * s < (1 + s) ^ p
Tactic: rcases eq_or_lt_of_le hs with rfl | hs
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : LE.le (α := ℝ) (-1) (-1)
hs' : Ne (α := ℝ) (-1) 0
⊢ 1 + p * -1 < HAdd.hAdd (α := ℝ) 1 (-1) ^ p
have inl : 1 + p * -1 < HPow.hPow (α := ℝ) 0 p
Tactic: rwa [add_neg_cancel, zero_rpow hp'.ne', mul_neg_one, add_neg_lt_iff_lt_add, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : LE.le (α := ℝ) (-1) (-1)
hs' : Ne (α := ℝ) (-1) 0
inl : 1 + p * -1 < HPow.hPow (α := ℝ) 0 p
⊢ 1 + p * -1 < HAdd.hAdd (α := ℝ) 1 (-1) ^ p
have inl₁ : 1 + p * -1 < 0
Tactic: rwa [add_neg_cancel, zero_rpow hp'.ne', mul_neg_one, add_neg_lt_iff_lt_add, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : LE.le (α := ℝ) (-1) (-1)
hs' : Ne (α := ℝ) (-1) 0
inl : 1 + p * -1 < HPow.hPow (α := ℝ) 0 p
inl₁ : 1 + p * -1 < 0
⊢ 1 + p * -1 < HAdd.hAdd (α := ℝ) 1 (-1) ^ p
have inl₂ : 1 + -p < 0
Tactic: rwa [add_neg_cancel, zero_rpow hp'.ne', mul_neg_one, add_neg_lt_iff_lt_add, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : LE.le (α := ℝ) (-1) (-1)
hs' : Ne (α := ℝ) (-1) 0
inl : 1 + p * -1 < HPow.hPow (α := ℝ) 0 p
inl₁ : 1 + p * -1 < 0
inl₂ : 1 + -p < 0
⊢ 1 + p * -1 < HAdd.hAdd (α := ℝ) 1 (-1) ^ p
have inl₃ : 1 < 0 + p
Tactic: rwa [add_neg_cancel, zero_rpow hp'.ne', mul_neg_one, add_neg_lt_iff_lt_add, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (hypothesis)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
⊢ 1 + p * s < (1 + s) ^ p
have hs1 : 0 < 1 + s
Tactic: have hs1 : 0 < 1 + s := neg_lt_iff_pos_add'.mp hs
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
⊢ 1 + p * s < (1 + s) ^ p
have inr : ∀ (hs2 : 1 + p * s ≤ 0), 1 + p * s < (1 + s) ^ p
Tactic: rcases le_or_gt (1 + p * s) 0 with hs2 | hs2
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
inr : ∀ (hs2 : 1 + p * s ≤ 0), 1 + p * s < (1 + s) ^ p
⊢ 1 + p * s < (1 + s) ^ p
have inr₁ : ∀ (hs2 : 0 < 1 + p * s), 1 + p * s < (1 + s) ^ p
Tactic: rcases le_or_gt (1 + p * s) 0 with hs2 | hs2
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (hypothesis)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
⊢ 1 + p * s < (1 + s) ^ p
have hs3 : 1 + s ≠ 1
Tactic: have hs3 : 1 + s ≠ 1 := hs' ∘ add_eq_left.mp
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
⊢ 1 + p * s ≠ 1
have contrapose : ∀ (hs' : 1 + p * s = 1), s = 0
Tactic: contrapose hs'
Cleared hypotheses: hs'
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs' : 1 + p * s = 1
⊢ s = 0
have rwa : ∀ (hs' : p * s = 0), s = 0
Tactic: rwa [add_eq_left, mul_eq_zero, eq_false_intro hp'.ne', false_or] at hs'
Cleared hypotheses: hs'
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs' : 1 + p * s = 1
rwa : ∀ (hs' : p * s = 0), s = 0
⊢ s = 0
have rwa₁ : ∀ (hs' : p = 0 ∨ s = 0), s = 0
Tactic: rwa [add_eq_left, mul_eq_zero, eq_false_intro hp'.ne', false_or] at hs'
Cleared hypotheses: hs'
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs' : 1 + p * s = 1
rwa : ∀ (hs' : p * s = 0), s = 0
rwa₁ : ∀ (hs' : p = 0 ∨ s = 0), s = 0
⊢ s = 0
have rwa₂ : ∀ (hs' : False ∨ s = 0), s = 0
Tactic: rwa [add_eq_left, mul_eq_zero, eq_false_intro hp'.ne', false_or] at hs'
Cleared hypotheses: hs'
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs' : 1 + p * s = 1
rwa : ∀ (hs' : p * s = 0), s = 0
rwa₁ : ∀ (hs' : p = 0 ∨ s = 0), s = 0
rwa₂ : ∀ (hs' : False ∨ s = 0), s = 0
⊢ s = 0
have rwa₃ : ∀ (hs' : s = 0), s = 0
Tactic: rwa [add_eq_left, mul_eq_zero, eq_false_intro hp'.ne', false_or] at hs'
Cleared hypotheses: hs'
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (hypothesis)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
⊢ 1 + p * s < (1 + s) ^ p
have hs4 : 1 + p * s ≠ 1
Tactic: have hs4 : 1 + p * s ≠ 1 := by
    contrapose hs'; rwa [add_eq_left, mul_eq_zero, eq_false_intro hp'.ne', false_or] at hs'
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
⊢ 1 + p * s < (1 + s) ^ p
have inr : rexp (log (1 + p * s)) < rexp (log (1 + s) * p)
Tactic: rw [rpow_def_of_pos hs1, ← exp_log hs2]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
⊢ rexp (log (1 + p * s)) < rexp (log (1 + s) * p)
have inr : log (1 + p * s) < log (1 + s) * p
Tactic: apply exp_strictMono
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
⊢ log (1 + p * s) < log (1 + s) * p
have inr : ∀ (hs' : s < 0), log (1 + p * s) < log (1 + s) * p
Tactic: rcases lt_or_gt_of_ne hs' with hs' | hs'
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
inr : ∀ (hs' : s < 0), log (1 + p * s) < log (1 + s) * p
⊢ log (1 + p * s) < log (1 + s) * p
have inr₁ : ∀ (hs' : 0 < s), log (1 + p * s) < log (1 + s) * p
Tactic: rcases lt_or_gt_of_ne hs' with hs' | hs'
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
⊢ log (1 + p * s) < log (1 + s) * p
have inr : log (1 + s) / s < log (1 + p * s) / p / s
Tactic: rw [← div_lt_iff₀ hp', ← div_lt_div_right_of_neg hs']
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
⊢ log (1 + s) / s < log (1 + p * s) / p / s
have h : log (1 + s) / s = (log (1 + s) - log 1) / (1 + s - 1)
Tactic: convert! strictConcaveOn_log_Ioi.secant_strict_mono (zero_lt_one' ℝ) hs2 hs1 hs4 hs3 _ using 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
h : log (1 + s) / s = (log (1 + s) - log 1) / (1 + s - 1)
⊢ log (1 + s) / s < log (1 + p * s) / p / s
have h₁ : log (1 + p * s) / p / s = (log (1 + p * s) - log 1) / (1 + p * s - 1)
Tactic: convert! strictConcaveOn_log_Ioi.secant_strict_mono (zero_lt_one' ℝ) hs2 hs1 hs4 hs3 _ using 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
h : log (1 + s) / s = (log (1 + s) - log 1) / (1 + s - 1)
h₁ : log (1 + p * s) / p / s = (log (1 + p * s) - log 1) / (1 + p * s - 1)
⊢ log (1 + s) / s < log (1 + p * s) / p / s
have inr : 1 + p * s < 1 + s
Tactic: convert! strictConcaveOn_log_Ioi.secant_strict_mono (zero_lt_one' ℝ) hs2 hs1 hs4 hs3 _ using 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
⊢ log (1 + s) / s = (log (1 + s) - log 1) / (1 + s - 1)
have h : log (1 + s) / s = (log (1 + s) - log 1) / s
Tactic: rw [add_sub_cancel_left, log_one, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
h : log (1 + s) / s = (log (1 + s) - log 1) / s
⊢ log (1 + s) / s = (log (1 + s) - log 1) / (1 + s - 1)
have h₁ : log (1 + s) / s = (log (1 + s) - 0) / s
Tactic: rw [add_sub_cancel_left, log_one, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
h : log (1 + s) / s = (log (1 + s) - log 1) / s
h₁ : log (1 + s) / s = (log (1 + s) - 0) / s
⊢ log (1 + s) / s = (log (1 + s) - log 1) / (1 + s - 1)
have h₂ : log (1 + s) / s = log (1 + s) / s
Tactic: rw [add_sub_cancel_left, log_one, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
⊢ log (1 + p * s) / p / s = (log (1 + p * s) - log 1) / (1 + p * s - 1)
have h : log (1 + p * s) / p / s = (log (1 + p * s) - log 1) / (p * s)
Tactic: rw [add_sub_cancel_left, div_div, log_one, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
h : log (1 + p * s) / p / s = (log (1 + p * s) - log 1) / (p * s)
⊢ log (1 + p * s) / p / s = (log (1 + p * s) - log 1) / (1 + p * s - 1)
have h₁ : log (1 + p * s) / (p * s) = (log (1 + p * s) - log 1) / (p * s)
Tactic: rw [add_sub_cancel_left, div_div, log_one, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
h : log (1 + p * s) / p / s = (log (1 + p * s) - log 1) / (p * s)
h₁ : log (1 + p * s) / (p * s) = (log (1 + p * s) - log 1) / (p * s)
⊢ log (1 + p * s) / p / s = (log (1 + p * s) - log 1) / (1 + p * s - 1)
have h₂ : log (1 + p * s) / (p * s) = (log (1 + p * s) - 0) / (p * s)
Tactic: rw [add_sub_cancel_left, div_div, log_one, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
h : log (1 + p * s) / p / s = (log (1 + p * s) - log 1) / (p * s)
h₁ : log (1 + p * s) / (p * s) = (log (1 + p * s) - log 1) / (p * s)
h₂ : log (1 + p * s) / (p * s) = (log (1 + p * s) - 0) / (p * s)
⊢ log (1 + p * s) / p / s = (log (1 + p * s) - log 1) / (1 + p * s - 1)
have h₃ : log (1 + p * s) / (p * s) = log (1 + p * s) / (p * s)
Tactic: rw [add_sub_cancel_left, div_div, log_one, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
⊢ 1 + p * s < 1 + s
have inr : p * s < s
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
⊢ log (1 + p * s) < log (1 + s) * p
have inr : log (1 + p * s) / p / s < log (1 + s) / s
Tactic: rw [← div_lt_iff₀ hp', ← div_lt_div_iff_of_pos_right hs']
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
⊢ log (1 + p * s) / p / s < log (1 + s) / s
have h : log (1 + p * s) / p / s = (log (1 + p * s) - log 1) / (1 + p * s - 1)
Tactic: convert! strictConcaveOn_log_Ioi.secant_strict_mono (zero_lt_one' ℝ) hs1 hs2 hs3 hs4 _ using 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
h : log (1 + p * s) / p / s = (log (1 + p * s) - log 1) / (1 + p * s - 1)
⊢ log (1 + p * s) / p / s < log (1 + s) / s
have h₁ : log (1 + s) / s = (log (1 + s) - log 1) / (1 + s - 1)
Tactic: convert! strictConcaveOn_log_Ioi.secant_strict_mono (zero_lt_one' ℝ) hs1 hs2 hs3 hs4 _ using 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
h : log (1 + p * s) / p / s = (log (1 + p * s) - log 1) / (1 + p * s - 1)
h₁ : log (1 + s) / s = (log (1 + s) - log 1) / (1 + s - 1)
⊢ log (1 + p * s) / p / s < log (1 + s) / s
have inr : 1 + s < 1 + p * s
Tactic: convert! strictConcaveOn_log_Ioi.secant_strict_mono (zero_lt_one' ℝ) hs1 hs2 hs3 hs4 _ using 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
⊢ log (1 + p * s) / p / s = (log (1 + p * s) - log 1) / (1 + p * s - 1)
have h : log (1 + p * s) / p / s = (log (1 + p * s) - log 1) / (p * s)
Tactic: rw [add_sub_cancel_left, div_div, log_one, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
h : log (1 + p * s) / p / s = (log (1 + p * s) - log 1) / (p * s)
⊢ log (1 + p * s) / p / s = (log (1 + p * s) - log 1) / (1 + p * s - 1)
have h₁ : log (1 + p * s) / (p * s) = (log (1 + p * s) - log 1) / (p * s)
Tactic: rw [add_sub_cancel_left, div_div, log_one, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
h : log (1 + p * s) / p / s = (log (1 + p * s) - log 1) / (p * s)
h₁ : log (1 + p * s) / (p * s) = (log (1 + p * s) - log 1) / (p * s)
⊢ log (1 + p * s) / p / s = (log (1 + p * s) - log 1) / (1 + p * s - 1)
have h₂ : log (1 + p * s) / (p * s) = (log (1 + p * s) - 0) / (p * s)
Tactic: rw [add_sub_cancel_left, div_div, log_one, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
h : log (1 + p * s) / p / s = (log (1 + p * s) - log 1) / (p * s)
h₁ : log (1 + p * s) / (p * s) = (log (1 + p * s) - log 1) / (p * s)
h₂ : log (1 + p * s) / (p * s) = (log (1 + p * s) - 0) / (p * s)
⊢ log (1 + p * s) / p / s = (log (1 + p * s) - log 1) / (1 + p * s - 1)
have h₃ : log (1 + p * s) / (p * s) = log (1 + p * s) / (p * s)
Tactic: rw [add_sub_cancel_left, div_div, log_one, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
⊢ log (1 + s) / s = (log (1 + s) - log 1) / (1 + s - 1)
have h : log (1 + s) / s = (log (1 + s) - log 1) / s
Tactic: rw [add_sub_cancel_left, log_one, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
h : log (1 + s) / s = (log (1 + s) - log 1) / s
⊢ log (1 + s) / s = (log (1 + s) - log 1) / (1 + s - 1)
have h₁ : log (1 + s) / s = (log (1 + s) - 0) / s
Tactic: rw [add_sub_cancel_left, log_one, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
h : log (1 + s) / s = (log (1 + s) - log 1) / s
h₁ : log (1 + s) / s = (log (1 + s) - 0) / s
⊢ log (1 + s) / s = (log (1 + s) - log 1) / (1 + s - 1)
have h₂ : log (1 + s) / s = log (1 + s) / s
Tactic: rw [add_sub_cancel_left, log_one, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
⊢ 1 + s < 1 + p * s
have inr : s < p * s
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs : -1 ≤ s
p : ℝ
hp : 1 ≤ p
⊢ 1 + p * s ≤ (1 + s) ^ p
have inl : ∀ (hp : LE.le (α := ℝ) 1 1), 1 + 1 * s ≤ HPow.hPow (β := ℝ) (1 + s) 1
Tactic: rcases eq_or_lt_of_le hp with (rfl | hp)
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs : -1 ≤ s
p : ℝ
hp : 1 ≤ p
inl : ∀ (hp : LE.le (α := ℝ) 1 1), 1 + 1 * s ≤ HPow.hPow (β := ℝ) (1 + s) 1
⊢ 1 + p * s ≤ (1 + s) ^ p
have inr : ∀ (hp : 1 < p), 1 + p * s ≤ (1 + s) ^ p
Tactic: rcases eq_or_lt_of_le hp with (rfl | hp)
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs : -1 ≤ s
p : ℝ
hp_1 : 1 ≤ p
hp : 1 < p
⊢ 1 + p * s ≤ (1 + s) ^ p
have pos : ∀ (hs' : s = 0), 1 + p * s ≤ (1 + s) ^ p
Tactic: by_cases hs' : s = 0
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs : -1 ≤ s
p : ℝ
hp_1 : 1 ≤ p
hp : 1 < p
pos : ∀ (hs' : s = 0), 1 + p * s ≤ (1 + s) ^ p
⊢ 1 + p * s ≤ (1 + s) ^ p
have neg : ∀ (hs' : ¬s = 0), 1 + p * s ≤ (1 + s) ^ p
Tactic: by_cases hs' : s = 0
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
⊢ (1 + s) ^ p < 1 + p * s
have inl : ∀ (hs : LE.le (α := ℝ) (-1) (-1)) (hs' : Ne (α := ℝ) (-1) 0), HAdd.hAdd (α := ℝ) 1 (-1) ^ p < 1 + p * -1
Tactic: rcases eq_or_lt_of_le hs with rfl | hs
Cleared hypotheses: s, hs, hs'
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
inl : ∀ (hs : LE.le (α := ℝ) (-1) (-1)) (hs' : Ne (α := ℝ) (-1) 0), HAdd.hAdd (α := ℝ) 1 (-1) ^ p < 1 + p * -1
⊢ (1 + s) ^ p < 1 + p * s
have inr : ∀ (hs : -1 < s), (1 + s) ^ p < 1 + p * s
Tactic: rcases eq_or_lt_of_le hs with rfl | hs
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : LE.le (α := ℝ) (-1) (-1)
hs' : Ne (α := ℝ) (-1) 0
⊢ HAdd.hAdd (α := ℝ) 1 (-1) ^ p < 1 + p * -1
have inl : HPow.hPow (α := ℝ) 0 p < 1 + p * -1
Tactic: rwa [add_neg_cancel, zero_rpow hp1.ne', mul_neg_one, lt_add_neg_iff_add_lt, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : LE.le (α := ℝ) (-1) (-1)
hs' : Ne (α := ℝ) (-1) 0
inl : HPow.hPow (α := ℝ) 0 p < 1 + p * -1
⊢ HAdd.hAdd (α := ℝ) 1 (-1) ^ p < 1 + p * -1
have inl₁ : 0 < 1 + p * -1
Tactic: rwa [add_neg_cancel, zero_rpow hp1.ne', mul_neg_one, lt_add_neg_iff_add_lt, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : LE.le (α := ℝ) (-1) (-1)
hs' : Ne (α := ℝ) (-1) 0
inl : HPow.hPow (α := ℝ) 0 p < 1 + p * -1
inl₁ : 0 < 1 + p * -1
⊢ HAdd.hAdd (α := ℝ) 1 (-1) ^ p < 1 + p * -1
have inl₂ : 0 < 1 + -p
Tactic: rwa [add_neg_cancel, zero_rpow hp1.ne', mul_neg_one, lt_add_neg_iff_add_lt, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : LE.le (α := ℝ) (-1) (-1)
hs' : Ne (α := ℝ) (-1) 0
inl : HPow.hPow (α := ℝ) 0 p < 1 + p * -1
inl₁ : 0 < 1 + p * -1
inl₂ : 0 < 1 + -p
⊢ HAdd.hAdd (α := ℝ) 1 (-1) ^ p < 1 + p * -1
have inl₃ : 0 + p < 1
Tactic: rwa [add_neg_cancel, zero_rpow hp1.ne', mul_neg_one, lt_add_neg_iff_add_lt, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (hypothesis)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
⊢ (1 + s) ^ p < 1 + p * s
have hs1 : 0 < 1 + s
Tactic: have hs1 : 0 < 1 + s := neg_lt_iff_pos_add'.mp hs
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
⊢ 0 < 1 + p * s
have rw : -1 < p * s
Tactic: rw [← neg_lt_iff_pos_add']
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
⊢ -1 < p * s
have inl : ∀ (h : s < 0), -1 < p * s
Tactic: rcases lt_or_gt_of_ne hs' with h | h