awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inl : ∀ (h : s < 0), -1 < p * s
⊢ -1 < p * s
have inr : ∀ (h : 0 < s), -1 < p * s
Tactic: rcases lt_or_gt_of_ne hs' with h | h
-- 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
hs1 : 0 < 1 + s
⊢ (1 + s) ^ p < 1 + p * s
have hs2 : 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)
-- 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
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
⊢ (1 + s) ^ p < 1 + p * s
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 : ℝ
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
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 : ℝ
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
⊢ s = 0
have rwa : ∀ (hs' : p * s = 0), s = 0
Tactic: rwa [add_eq_left, mul_eq_zero, eq_false_intro hp1.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 : ℝ
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
⊢ s = 0
have rwa₁ : ∀ (hs' : p = 0 ∨ s = 0), s = 0
Tactic: rwa [add_eq_left, mul_eq_zero, eq_false_intro hp1.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 : ℝ
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
⊢ s = 0
have rwa₂ : ∀ (hs' : False ∨ s = 0), s = 0
Tactic: rwa [add_eq_left, mul_eq_zero, eq_false_intro hp1.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 : ℝ
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
⊢ s = 0
have rwa₃ : ∀ (hs' : s = 0), s = 0
Tactic: rwa [add_eq_left, mul_eq_zero, eq_false_intro hp1.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 : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
⊢ (1 + s) ^ p < 1 + p * s
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 hp1.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 : ℝ
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
⊢ (1 + s) ^ p < 1 + p * s
have inr : rexp (log (1 + s) * p) < rexp (log (1 + p * s))
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 : ℝ
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
⊢ rexp (log (1 + s) * p) < rexp (log (1 + p * s))
have inr : log (1 + s) * p < log (1 + p * s)
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 : ℝ
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
⊢ log (1 + s) * p < log (1 + p * s)
have inr : ∀ (hs' : s < 0), log (1 + s) * p < log (1 + p * s)
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 : ℝ
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)
⊢ log (1 + s) * p < log (1 + p * s)
have inr₁ : ∀ (hs' : 0 < s), log (1 + s) * p < log (1 + p * s)
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 : ℝ
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 + s) * p < log (1 + p * s)
have inr : log (1 + p * s) / p / s < log (1 + s) / s
Tactic: rw [← lt_div_iff₀ hp1, ← 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 : ℝ
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) / 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 : ℝ
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)
⊢ 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 : ℝ
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)
⊢ 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 : ℝ
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) / 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 : ℝ
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)
⊢ 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 : ℝ
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)
⊢ 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 : ℝ
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)
⊢ 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 : ℝ
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 + 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 : ℝ
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
⊢ 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 : ℝ
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
⊢ 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 : ℝ
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
⊢ 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 : -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) * p < log (1 + p * s)
have inr : log (1 + s) / s < log (1 + p * s) / p / s
Tactic: rw [← lt_div_iff₀ hp1, ← 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 : ℝ
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) / 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 : ℝ
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)
⊢ 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 : ℝ
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)
⊢ 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 : ℝ
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) / 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 : ℝ
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
⊢ 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 : ℝ
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
⊢ 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 : ℝ
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 + 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 : ℝ
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)
⊢ 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 : ℝ
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)
⊢ 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 : ℝ
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)
⊢ 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 : ℝ
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
⊢ 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 ≤ s
p : ℝ
hp1 : 0 ≤ p
hp2 : p ≤ 1
⊢ (1 + s) ^ p ≤ 1 + p * s
have inl : ∀ (hp1 : LE.le (α := ℝ) 0 0) (hp2 : LE.le (α := ℝ) 0 1), HPow.hPow (β := ℝ) (1 + s) 0 ≤ 1 + 0 * s
Tactic: rcases eq_or_lt_of_le hp1 with (rfl | hp1)
Cleared hypotheses: p, hp1, hp2
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
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
⊢ (1 + s) ^ p ≤ 1 + p * s
have inr : ∀ (hp1 : 0 < p), (1 + s) ^ p ≤ 1 + p * s
Tactic: rcases eq_or_lt_of_le hp1 with (rfl | hp1)
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs : -1 ≤ s
p : ℝ
hp1_1 : 0 ≤ p
hp2 : p ≤ 1
hp1 : 0 < p
⊢ (1 + s) ^ p ≤ 1 + p * s
have inr : ∀ (hp1 : LE.le (α := ℝ) 0 1) (hp2 : LE.le (α := ℝ) 1 1) (hp1 : LT.lt (α := ℝ) 0 1),
  HPow.hPow (β := ℝ) (1 + s) 1 ≤ 1 + 1 * s
Tactic: rcases eq_or_lt_of_le hp2 with (rfl | hp2)
Cleared hypotheses: p, hp1_1, hp2, hp1
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
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
⊢ (1 + s) ^ p ≤ 1 + p * s
have inr₁ : ∀ (hp2 : p < 1), (1 + s) ^ p ≤ 1 + p * s
Tactic: rcases eq_or_lt_of_le hp2 with (rfl | hp2)
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
s : ℝ
hs : -1 ≤ s
p : ℝ
hp1_1 : 0 ≤ p
hp2_1 : p ≤ 1
hp1 : 0 < p
hp2 : p < 1
⊢ (1 + s) ^ p ≤ 1 + p * s
have pos : ∀ (hs' : s = 0), (1 + s) ^ p ≤ 1 + p * s
Tactic: by_cases hs' : s = 0
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
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
⊢ (1 + s) ^ p ≤ 1 + p * s
have neg : ∀ (hs' : ¬s = 0), (1 + s) ^ p ≤ 1 + p * s
Tactic: by_cases hs' : s = 0
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
p : ℝ
hp : 1 < p
⊢ StrictConvexOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ x ^ p
have 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)
Tactic: apply strictConvexOn_of_slope_strict_mono_adjacent (convex_Ici (0 : ℝ))
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
p : ℝ
hp : 1 < p
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)
have this : ∀ (hx : 0 ≤ x),
  Membership.mem (γ := Set ℝ) (Ici 0) z → x < y → y < z → (y ^ p - x ^ p) / (y - x) < (z ^ p - y ^ p) / (z - y)
Tactic: (hx : 0 ≤ x)
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
⊢ Membership.mem (γ := Set ℝ) (Ici 0) z → x < y → y < z → (y ^ p - x ^ p) / (y - x) < (z ^ p - y ^ p) / (z - y)
have this : ∀ (hz : 0 ≤ z), x < y → y < z → (y ^ p - x ^ p) / (y - x) < (z ^ p - y ^ p) / (z - y)
Tactic: (hz : 0 ≤ z)
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (hypothesis)
Goal:
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
⊢ (y ^ p - x ^ p) / (y - x) < (z ^ p - y ^ p) / (z - y)
have hy : 0 < y
Tactic: have hy : 0 < y := hx.trans_lt hxy
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (hypothesis)
Goal:
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
⊢ (y ^ p - x ^ p) / (y - x) < (z ^ p - y ^ p) / (z - y)
have hy' : 0 < y ^ p
Tactic: have hy' : 0 < y ^ p := rpow_pos_of_pos hy _
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
⊢ (y ^ p - x ^ p) / (y - x) < (z ^ p - y ^ p) / (z - y)
have trans : (y ^ p - x ^ p) / (y - x) < p * y ^ (p - 1)
Tactic: trans p * y ^ (p - 1)
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
trans : (y ^ p - x ^ p) / (y - x) < p * y ^ (p - 1)
⊢ (y ^ p - x ^ p) / (y - x) < (z ^ p - y ^ p) / (z - y)
have trans₁ : p * y ^ (p - 1) < (z ^ p - y ^ p) / (z - y)
Tactic: trans p * y ^ (p - 1)
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (hypothesis)
Goal:
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
⊢ (y ^ p - x ^ p) / (y - x) < p * y ^ (p - 1)
have q : 0 < y - x
Tactic: have q : 0 < y - x := by rwa [sub_pos]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < y - x
⊢ (y ^ p - x ^ p) / (y - x) < p * y ^ (p - 1)
have rw : 1 + p * (x / y - 1) < (1 + (x / y - 1)) ^ p
Tactic: rw [div_lt_iff₀ q, ← div_lt_div_iff_of_pos_right hy', _root_.sub_div, div_self hy'.ne',
      ← div_rpow hx hy.le, sub_lt_comm, ← add_sub_cancel_right (x / y) 1, add_comm, add_sub_assoc,
      ← div_mul_eq_mul_div, mul_div_assoc, ← rpow_sub hy, sub_sub_cancel_left, rpow_neg_one,
      mul_assoc, ← div_eq_inv_mul, sub_eq_add_neg, ← mul_neg, ← neg_div, neg_sub, _root_.sub_div,
      div_self hy.ne']
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < y - x
⊢ 1 + p * (x / y - 1) < (1 + (x / y - 1)) ^ p
have apply : -1 ≤ x / y - 1
Tactic: apply one_add_mul_self_lt_rpow_one_add _ _ hp
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < y - x
apply : -1 ≤ x / y - 1
⊢ 1 + p * (x / y - 1) < (1 + (x / y - 1)) ^ p
have apply₁ : x / y - 1 ≠ 0
Tactic: apply one_add_mul_self_lt_rpow_one_add _ _ hp
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < y - x
⊢ -1 ≤ x / y - 1
have rw : 0 ≤ x ∧ 0 ≤ y ∨ x ≤ 0 ∧ y ≤ 0
Tactic: rw [le_sub_iff_add_le, neg_add_cancel, div_nonneg_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < y - x
⊢ x / y - 1 ≠ 0
have rw : x / y ≠ 1
Tactic: rw [sub_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (hypothesis)
Goal:
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
⊢ p * y ^ (p - 1) < (z ^ p - y ^ p) / (z - y)
have q : 0 < z - y
Tactic: have q : 0 < z - y := by rwa [sub_pos]