awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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) - log 1) / (1 + s - 1) < (log (1 + p * s) - log 1) / (1 + p * s - 1)

Tactic:
strictConcaveOn_log_Ioi.secant_strict_mono (zero_lt_one' ℝ) hs2 hs1 hs4 hs3 _

Premises used: Real, StrictConcaveOn.secant_strict_mono, zero_lt_one', strictConcaveOn_log_Ioi
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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)
inr : 1 + p * s < 1 + s
⊢ log (1 + s) / s < log (1 + p * s) / p / s

Tactic:
convert! strictConcaveOn_log_Ioi.secant_strict_mono (zero_lt_one' ℝ) hs2 hs1 hs4 hs3 _ using 1

Premises used: Real, StrictConcaveOn.secant_strict_mono, zero_lt_one', strictConcaveOn_log_Ioi
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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
h₂ h₃ : log (1 + s) / s = log (1 + s) / s
⊢ log (1 + s) / s = (log (1 + s) - log 1) / (1 + s - 1)

Tactic:
rw [add_sub_cancel_left, log_one, sub_zero]

Premises used: sub_zero, add_sub_cancel_left, Real.log_one
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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)
h₃ h₄ : log (1 + p * s) / (p * s) = log (1 + p * s) / (p * s)
⊢ log (1 + p * s) / p / s = (log (1 + p * s) - log 1) / (1 + p * s - 1)

Tactic:
rw [add_sub_cancel_left, div_div, log_one, sub_zero]

Premises used: sub_zero, add_sub_cancel_left, Real.log_one, div_div
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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
inr : p * s < s
⊢ 1 + p * s < 1 + s

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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
⊢ p * s < s

Tactic:
mul_lt_of_one_lt_left hs' hp

Premises used: mul_lt_of_one_lt_left
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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
⊢ p * s < s

Tactic:
exact mul_lt_of_one_lt_left hs' hp

Premises used: mul_lt_of_one_lt_left
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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
inr : log (1 + p * s) / p / s < log (1 + s) / s
⊢ log (1 + p * s) < log (1 + s) * p

Tactic:
rw [← div_lt_iff₀ hp', ← div_lt_div_iff_of_pos_right hs']

Premises used: div_lt_div_iff_of_pos_right, div_lt_iff₀
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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) / (1 + p * s - 1) < (log (1 + s) - log 1) / (1 + s - 1)

Tactic:
strictConcaveOn_log_Ioi.secant_strict_mono (zero_lt_one' ℝ) hs1 hs2 hs3 hs4 _

Premises used: Real, StrictConcaveOn.secant_strict_mono, zero_lt_one', strictConcaveOn_log_Ioi
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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)
inr : 1 + s < 1 + p * s
⊢ log (1 + p * s) / p / s < log (1 + s) / s

Tactic:
convert! strictConcaveOn_log_Ioi.secant_strict_mono (zero_lt_one' ℝ) hs1 hs2 hs3 hs4 _ using 1

Premises used: Real, StrictConcaveOn.secant_strict_mono, zero_lt_one', strictConcaveOn_log_Ioi
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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)
h₃ h₄ : log (1 + p * s) / (p * s) = log (1 + p * s) / (p * s)
⊢ log (1 + p * s) / p / s = (log (1 + p * s) - log 1) / (1 + p * s - 1)

Tactic:
rw [add_sub_cancel_left, div_div, log_one, sub_zero]

Premises used: sub_zero, add_sub_cancel_left, Real.log_one, div_div
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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
h₂ h₃ : log (1 + s) / s = log (1 + s) / s
⊢ log (1 + s) / s = (log (1 + s) - log 1) / (1 + s - 1)

Tactic:
rw [add_sub_cancel_left, log_one, sub_zero]

Premises used: sub_zero, add_sub_cancel_left, Real.log_one
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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
inr : s < p * s
⊢ 1 + s < 1 + p * s

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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
⊢ s < p * s

Tactic:
lt_mul_of_one_lt_left hs' hp

Premises used: lt_mul_of_one_lt_left
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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
⊢ s < p * s

Tactic:
exact lt_mul_of_one_lt_left hs' hp

Premises used: lt_mul_of_one_lt_left
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs : -1 ≤ s
p : ℝ
hp : 1 ≤ p
inl : ∀ (hp : LE.le (α := ℝ) 1 1), 1 + 1 * s ≤ HPow.hPow (β := ℝ) (1 + s) 1
inr : ∀ (hp : 1 < p), 1 + p * s ≤ (1 + s) ^ p
⊢ 1 + p * s ≤ (1 + s) ^ p

Tactic:
rcases eq_or_lt_of_le hp with (rfl | hp)

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs : -1 ≤ s
hp : LE.le (α := ℝ) 1 1
⊢ 1 + 1 * s ≤ HPow.hPow (β := ℝ) (1 + s) 1

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs : -1 ≤ s
p : ℝ
hp_1 : 1 ≤ p
hp : 1 < p
pos : ∀ (hs' : s = 0), 1 + p * s ≤ (1 + s) ^ p
neg : ∀ (hs' : ¬s = 0), 1 + p * s ≤ (1 + s) ^ p
⊢ 1 + p * s ≤ (1 + s) ^ p

Tactic:
by_cases hs' : s = 0
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs : -1 ≤ s
p : ℝ
hp_1 : 1 ≤ p
hp : 1 < p
hs' : s = 0
⊢ 1 + p * s ≤ (1 + s) ^ p

Tactic:
simp [hs']
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs : -1 ≤ s
p : ℝ
hp_1 : 1 ≤ p
hp : 1 < p
hs' : ¬s = 0
⊢ 1 + p * s ≤ (1 + s) ^ p

Tactic:
(one_add_mul_self_lt_rpow_one_add hs hs' hp).le

Premises used: LT.lt.le, one_add_mul_self_lt_rpow_one_add
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs : -1 ≤ s
p : ℝ
hp_1 : 1 ≤ p
hp : 1 < p
hs' : ¬s = 0
⊢ 1 + p * s ≤ (1 + s) ^ p

Tactic:
exact (one_add_mul_self_lt_rpow_one_add hs hs' hp).le

Premises used: LT.lt.le, one_add_mul_self_lt_rpow_one_add
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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
inr : ∀ (hs : -1 < s), (1 + s) ^ p < 1 + p * s
⊢ (1 + s) ^ p < 1 + p * s

Tactic:
rcases eq_or_lt_of_le hs with rfl | hs

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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
inl₃ : 0 + p < 1
inl₄ inl₅ inl₆ inl₇ : p < 1
⊢ HAdd.hAdd (α := ℝ) 1 (-1) ^ p < 1 + p * -1

Tactic:
rwa [add_neg_cancel, zero_rpow hp1.ne', mul_neg_one, lt_add_neg_iff_add_lt, zero_add]

Premises used: add_neg_cancel, lt_add_neg_iff_add_lt, zero_add, Real.zero_rpow, LT.lt.ne', mul_neg_one
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
⊢ 0 < 1 + s

Tactic:
have hs1 : 0 < 1 + s := neg_lt_iff_pos_add'.mp hs
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
rw : -1 < p * s
⊢ 0 < 1 + p * s

Tactic:
rw [← neg_lt_iff_pos_add']

Premises used: neg_lt_iff_pos_add'
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
inl : ∀ (h : s < 0), -1 < p * s
inr : ∀ (h : 0 < s), -1 < p * s
⊢ -1 < p * s

Tactic:
rcases lt_or_gt_of_ne hs' with h | h

Premises used: lt_or_gt_of_ne
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
h : s < 0
⊢ -1 < p * s

Tactic:
hs.trans (lt_mul_of_lt_one_left h hp2)

Premises used: lt_mul_of_lt_one_left, LT.lt.trans
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
h : s < 0
⊢ -1 < p * s

Tactic:
exact hs.trans (lt_mul_of_lt_one_left h hp2)

Premises used: lt_mul_of_lt_one_left, LT.lt.trans
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
h : 0 < s
⊢ -1 < p * s

Tactic:
neg_one_lt_zero.trans (mul_pos hp1 h)

Premises used: mul_pos, LT.lt.trans, neg_one_lt_zero
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
h : 0 < s
⊢ -1 < p * s

Tactic:
exact neg_one_lt_zero.trans (mul_pos hp1 h)

Premises used: mul_pos, LT.lt.trans, neg_one_lt_zero
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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

Tactic:
have hs2 : 0 < 1 + p * s := by
    rw [← neg_lt_iff_pos_add']
    rcases lt_or_gt_of_ne hs' with h | h
    · exact hs.trans (lt_mul_of_lt_one_left h hp2)
    · exact neg_one_lt_zero.trans (mul_pos hp1 h)
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
⊢ 1 + s ≠ 1

Tactic:
have hs3 : 1 + s ≠ 1 := hs' ∘ add_eq_left.mp
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
contrapose : ∀ (hs' : 1 + p * s = 1), s = 0
⊢ 1 + p * s ≠ 1

Tactic:
contrapose hs'
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs_1 : -1 ≤ s
p : ℝ
hp1 : 0 < p
hp2 : p < 1
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
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (hs' : s = 0), s = 0
⊢ s = 0

Tactic:
rwa [add_eq_left, mul_eq_zero, eq_false_intro hp1.ne', false_or] at hs'

Premises used: false_or, mul_eq_zero, LT.lt.ne', add_eq_left, eq_false_intro
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
⊢ 1 + p * s ≠ 1

Tactic:
have hs4 : 1 + p * s ≠ 1 := by
    contrapose hs'; rwa [add_eq_left, mul_eq_zero, eq_false_intro hp1.ne', false_or] at hs'
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
inr : rexp (log (1 + s) * p) < rexp (log (1 + p * s))
⊢ (1 + s) ^ p < 1 + p * s

Tactic:
rw [rpow_def_of_pos hs1, ← exp_log hs2]

Premises used: Real.rpow_def_of_pos, Real.exp_log
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
inr : log (1 + s) * p < log (1 + p * s)
⊢ rexp (log (1 + s) * p) < rexp (log (1 + p * s))

Tactic:
apply exp_strictMono

Premises used: Real.exp_strictMono
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
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 + s) * p < log (1 + p * s)
inr₁ : ∀ (hs' : 0 < s), log (1 + s) * p < log (1 + p * s)
⊢ log (1 + s) * p < log (1 + p * s)

Tactic:
rcases lt_or_gt_of_ne hs' with hs' | hs'

Premises used: lt_or_gt_of_ne
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
inr : log (1 + p * s) / p / s < log (1 + s) / s
⊢ log (1 + s) * p < log (1 + p * s)

Tactic:
rw [← lt_div_iff₀ hp1, ← div_lt_div_right_of_neg hs']

Premises used: lt_div_iff₀, div_lt_div_right_of_neg
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
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) / (1 + p * s - 1) < (log (1 + s) - log 1) / (1 + s - 1)

Tactic:
strictConcaveOn_log_Ioi.secant_strict_mono (zero_lt_one' ℝ) hs1 hs2 hs3 hs4 _

Premises used: Real, StrictConcaveOn.secant_strict_mono, zero_lt_one', strictConcaveOn_log_Ioi
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
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) / (1 + p * s - 1)
h₁ : log (1 + s) / s = (log (1 + s) - log 1) / (1 + s - 1)
inr : 1 + s < 1 + p * s
⊢ log (1 + p * s) / p / s < log (1 + s) / s

Tactic:
convert! strictConcaveOn_log_Ioi.secant_strict_mono (zero_lt_one' ℝ) hs1 hs2 hs3 hs4 _ using 1

Premises used: Real, StrictConcaveOn.secant_strict_mono, zero_lt_one', strictConcaveOn_log_Ioi
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
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)
h₃ h₄ : log (1 + p * s) / (p * s) = log (1 + p * s) / (p * s)
⊢ log (1 + p * s) / p / s = (log (1 + p * s) - log 1) / (1 + p * s - 1)

Tactic:
rw [add_sub_cancel_left, div_div, log_one, sub_zero]

Premises used: sub_zero, add_sub_cancel_left, Real.log_one, div_div
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
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
h₂ h₃ : log (1 + s) / s = log (1 + s) / s
⊢ log (1 + s) / s = (log (1 + s) - log 1) / (1 + s - 1)

Tactic:
rw [add_sub_cancel_left, log_one, sub_zero]

Premises used: sub_zero, add_sub_cancel_left, Real.log_one
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
inr : s < p * s
⊢ 1 + s < 1 + p * s

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
⊢ s < p * s

Tactic:
lt_mul_of_lt_one_left hs' hp2

Premises used: lt_mul_of_lt_one_left
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
⊢ s < p * s

Tactic:
exact lt_mul_of_lt_one_left hs' hp2

Premises used: lt_mul_of_lt_one_left
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
inr : log (1 + s) / s < log (1 + p * s) / p / s
⊢ log (1 + s) * p < log (1 + p * s)

Tactic:
rw [← lt_div_iff₀ hp1, ← div_lt_div_iff_of_pos_right hs']

Premises used: lt_div_iff₀, div_lt_div_iff_of_pos_right
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
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) - log 1) / (1 + s - 1) < (log (1 + p * s) - log 1) / (1 + p * s - 1)

Tactic:
strictConcaveOn_log_Ioi.secant_strict_mono (zero_lt_one' ℝ) hs2 hs1 hs4 hs3 _

Premises used: Real, StrictConcaveOn.secant_strict_mono, zero_lt_one', strictConcaveOn_log_Ioi
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
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) / (1 + s - 1)
h₁ : log (1 + p * s) / p / s = (log (1 + p * s) - log 1) / (1 + p * s - 1)
inr : 1 + p * s < 1 + s
⊢ log (1 + s) / s < log (1 + p * s) / p / s

Tactic:
convert! strictConcaveOn_log_Ioi.secant_strict_mono (zero_lt_one' ℝ) hs2 hs1 hs4 hs3 _ using 1

Premises used: Real, StrictConcaveOn.secant_strict_mono, zero_lt_one', strictConcaveOn_log_Ioi
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
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
h₂ h₃ : log (1 + s) / s = log (1 + s) / s
⊢ log (1 + s) / s = (log (1 + s) - log 1) / (1 + s - 1)

Tactic:
rw [add_sub_cancel_left, log_one, sub_zero]

Premises used: sub_zero, add_sub_cancel_left, Real.log_one
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
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)
h₃ h₄ : log (1 + p * s) / (p * s) = log (1 + p * s) / (p * s)
⊢ log (1 + p * s) / p / s = (log (1 + p * s) - log 1) / (1 + p * s - 1)

Tactic:
rw [add_sub_cancel_left, div_div, log_one, sub_zero]

Premises used: sub_zero, add_sub_cancel_left, Real.log_one, div_div
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
inr : p * s < s
⊢ 1 + p * s < 1 + s

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
⊢ p * s < s

Tactic:
mul_lt_of_lt_one_left hs' hp2

Premises used: mul_lt_of_lt_one_left
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs'_1 : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
⊢ p * s < s

Tactic:
exact mul_lt_of_lt_one_left hs' hp2

Premises used: mul_lt_of_lt_one_left
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs : -1 ≤ s
p : ℝ
hp1 : 0 ≤ p
hp2 : p ≤ 1
inl : ∀ (hp1 : LE.le (α := ℝ) 0 0) (hp2 : LE.le (α := ℝ) 0 1), HPow.hPow (β := ℝ) (1 + s) 0 ≤ 1 + 0 * s
inr : ∀ (hp1 : 0 < p), (1 + s) ^ p ≤ 1 + p * s
⊢ (1 + s) ^ p ≤ 1 + p * s

Tactic:
rcases eq_or_lt_of_le hp1 with (rfl | hp1)

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs : -1 ≤ s
hp1 : LE.le (α := ℝ) 0 0
hp2 : LE.le (α := ℝ) 0 1
⊢ HPow.hPow (β := ℝ) (1 + s) 0 ≤ 1 + 0 * s

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs : -1 ≤ s
p : ℝ
hp1_1 : 0 ≤ p
hp2 : p ≤ 1
hp1 : 0 < p
inr :
  ∀ (hp1 : LE.le (α := ℝ) 0 1) (hp2 : LE.le (α := ℝ) 1 1) (hp1 : LT.lt (α := ℝ) 0 1),
    HPow.hPow (β := ℝ) (1 + s) 1 ≤ 1 + 1 * s
inr₁ : ∀ (hp2 : p < 1), (1 + s) ^ p ≤ 1 + p * s
⊢ (1 + s) ^ p ≤ 1 + p * s

Tactic:
rcases eq_or_lt_of_le hp2 with (rfl | hp2)

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs : -1 ≤ s
hp1_1 : LE.le (α := ℝ) 0 1
hp2 : LE.le (α := ℝ) 1 1
hp1 : LT.lt (α := ℝ) 0 1
⊢ HPow.hPow (β := ℝ) (1 + s) 1 ≤ 1 + 1 * s

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs : -1 ≤ s
p : ℝ
hp1_1 : 0 ≤ p
hp2_1 : p ≤ 1
hp1 : 0 < p
hp2 : p < 1
pos : ∀ (hs' : s = 0), (1 + s) ^ p ≤ 1 + p * s
neg : ∀ (hs' : ¬s = 0), (1 + s) ^ p ≤ 1 + p * s
⊢ (1 + s) ^ p ≤ 1 + p * s

Tactic:
by_cases hs' : s = 0
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs : -1 ≤ s
p : ℝ
hp1_1 : 0 ≤ p
hp2_1 : p ≤ 1
hp1 : 0 < p
hp2 : p < 1
hs' : s = 0
⊢ (1 + s) ^ p ≤ 1 + p * s

Tactic:
simp [hs']
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs : -1 ≤ s
p : ℝ
hp1_1 : 0 ≤ p
hp2_1 : p ≤ 1
hp1 : 0 < p
hp2 : p < 1
hs' : ¬s = 0
⊢ (1 + s) ^ p ≤ 1 + p * s

Tactic:
(rpow_one_add_lt_one_add_mul_self hs hs' hp1 hp2).le

Premises used: LT.lt.le, rpow_one_add_lt_one_add_mul_self
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs : -1 ≤ s
p : ℝ
hp1_1 : 0 ≤ p
hp2_1 : p ≤ 1
hp1 : 0 < p
hp2 : p < 1
hs' : ¬s = 0
⊢ (1 + s) ^ p ≤ 1 + p * s

Tactic:
exact (rpow_one_add_lt_one_add_mul_self hs hs' hp1 hp2).le

Premises used: LT.lt.le, rpow_one_add_lt_one_add_mul_self
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
p : ℝ
hp : 1 < p
apply :
  ∀ {x y z : ℝ},
    Membership.mem (γ := Set ℝ) (Ici 0) x →
      Membership.mem (γ := Set ℝ) (Ici 0) z → x < y → y < z → (y ^ p - x ^ p) / (y - x) < (z ^ p - y ^ p) / (z - y)
⊢ StrictConvexOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ x ^ p

Tactic:
apply strictConvexOn_of_slope_strict_mono_adjacent (convex_Ici (0 : ℝ))

Premises used: strictConvexOn_of_slope_strict_mono_adjacent, convex_Ici, OfNat.ofNat