awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (hypothesis)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConcaveOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa : x ≠ a
hya : y ≠ a
hxy : x < y
⊢ (f y - f a) / (y - a) < (f x - f a) / (x - a)
have key : ((-f) x - (-f) a) / (x - a) < ((-f) y - (-f) a) / (y - a)
Tactic: have key := hf.neg.secant_strict_mono ha hx hy hxa hya hxy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
z : 𝕜
hz : z ∈ s ∩ Set.Ioi y
⊢ f y < f z
have refine : y ∈ openSegment 𝕜 x z
Tactic: refine hf.lt_right_of_left_lt hx hz.1 ?_ hxy'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
z : 𝕜
hz : z ∈ s ∩ Set.Ioi y
⊢ y ∈ openSegment 𝕜 x z
have rw : y ∈ Set.Ioo x z
Tactic: rw [openSegment_eq_Ioo (hxy.trans hz.2)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (hypothesis)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
⊢ f u < f v
have step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
Tactic: have step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z := by
    intro z hz
    refine hf.lt_right_of_left_lt hx hz.1 ?_ hxy'
    rw [openSegment_eq_Ioo (hxy.trans hz.2)]
    exact ⟨hxy, hz.2⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
⊢ f u < f v
have inl : ∀ (hu : y ∈ s ∩ Set.Ici y) (huv : y < v), f y < f v
Tactic: rcases eq_or_lt_of_le hu.2 with (rfl | hu2)
Cleared hypotheses: u, hu, huv
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
inl : ∀ (hu : y ∈ s ∩ Set.Ici y) (huv : y < v), f y < f v
⊢ f u < f v
have inr : ∀ (hu2 : y < u), f u < f v
Tactic: rcases eq_or_lt_of_le hu.2 with (rfl | hu2)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu2 : y < u
⊢ f u < f v
have inr : y ∈ s
Tactic: refine hf.lt_right_of_left_lt ?_ hv.1 ?_ (step1 ⟨hu.1, hu2⟩)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu2 : y < u
inr : y ∈ s
⊢ f u < f v
have inr₁ : u ∈ openSegment 𝕜 y v
Tactic: refine hf.lt_right_of_left_lt ?_ hv.1 ?_ (step1 ⟨hu.1, hu2⟩)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu2 : y < u
⊢ y ∈ s
have inr : y ∈ segment 𝕜 x u
Tactic: apply hf.1.segment_subset hx hu.1
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu2 : y < u
⊢ y ∈ segment 𝕜 x u
have inr : y ∈ Set.Icc x u
Tactic: rw [segment_eq_Icc (hxy.le.trans hu.2)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu2 : y < u
⊢ u ∈ openSegment 𝕜 y v
have inr : u ∈ Set.Ioo y v
Tactic: rw [openSegment_eq_Ioo (hu2.trans huv)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (hypothesis)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hy : y ∈ s
hxy : x < y
hxy' : f y < f x
⊢ StrictAntiOn f (s ∩ Set.Iic x)
have this : StrictMonoOn (f ∘ (⇑(-AffineMap.id 𝕜 𝕜) : (a : 𝕜) → 𝕜)) ((⇑(-AffineMap.id 𝕜 𝕜) : (a : 𝕜) → 𝕜) ⁻¹' s ∩ Set.Ici (-x))
Tactic: have := hf.comp_affineMap (-.id ..) |>.strictMonoOn (by simpa) (neg_lt_neg hxy) (by simpa)
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
⊢ StrictConvexOn ℝ univ rexp
have apply : ∀ {x y z : ℝ},
  Membership.mem (γ := Set ℝ) univ x →
    Membership.mem (γ := Set ℝ) univ z → x < y → y < z → (rexp y - rexp x) / (y - x) < (rexp z - rexp y) / (z - y)
Tactic: apply strictConvexOn_of_slope_strict_mono_adjacent convex_univ
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
⊢ (rexp y - rexp x) / (y - x) < (rexp z - rexp y) / (z - y)
have trans : (rexp y - rexp x) / (y - x) < rexp y
Tactic: trans exp y
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
trans : (rexp y - rexp x) / (y - x) < rexp y
⊢ (rexp y - rexp x) / (y - x) < (rexp z - rexp y) / (z - y)
have trans₁ : rexp y < (rexp z - rexp y) / (z - y)
Tactic: trans exp y
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
⊢ 0 < y - x
have linarith : y - x ≤ 0 → x - y + (y - x - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (hypothesis)
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
⊢ (rexp y - rexp x) / (y - x) < rexp y
have h1 : 0 < y - x
Tactic: have h1 : 0 < y - x := by linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
⊢ x - y < 0
have linarith : 0 ≤ x - y → x - y + (0 - (x - y)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (hypothesis)
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
⊢ (rexp y - rexp x) / (y - x) < rexp y
have h2 : x - y < 0
Tactic: have h2 : x - y < 0 := by linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ (rexp y - rexp x) / (y - x) < rexp y
have rw : rexp y - rexp x < rexp y * (y - x)
Tactic: rw [div_lt_iff₀ h1]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ rexp y - rexp x = rexp y - rexp y * rexp (x - y)
have rw : rexp y - rexp x = rexp y - rexp (y + (x - y))
Tactic: rw [← exp_add]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ rexp y * (1 - rexp (x - y)) < rexp y * -(x - y)
have hbc : 1 - rexp (x - y) < -(x - y)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ 1 - rexp (x - y) < -(x - y)
have linarith : -(x - y) ≤ 1 - rexp (x - y) → -(x - y) - (1 - rexp (x - y)) + (x - y + 1 - rexp (x - y)) = 0
Tactic: linarith [add_one_lt_exp h2.ne]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ rexp y - rexp x < rexp y * (y - x)
have exp : rexp y - rexp x = rexp y - rexp y * rexp (x - y)
Tactic: calc
      exp y - exp x = exp y - exp y * exp (x - y) := by rw [← exp_add]; ring_nf
      _ = exp y * (1 - exp (x - y)) := by ring
      _ < exp y * -(x - y) := by gcongr; linarith [add_one_lt_exp h2.ne]
      _ = exp y * (y - x) := by ring
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
exp : rexp y - rexp x = rexp y - rexp y * rexp (x - y)
⊢ rexp y - rexp x < rexp y * (y - x)
have exp₁ : rexp y - rexp y * rexp (x - y) = rexp y * (1 - rexp (x - y))
Tactic: calc
      exp y - exp x = exp y - exp y * exp (x - y) := by rw [← exp_add]; ring_nf
      _ = exp y * (1 - exp (x - y)) := by ring
      _ < exp y * -(x - y) := by gcongr; linarith [add_one_lt_exp h2.ne]
      _ = exp y * (y - x) := by ring
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
exp : rexp y - rexp x = rexp y - rexp y * rexp (x - y)
exp₁ : rexp y - rexp y * rexp (x - y) = rexp y * (1 - rexp (x - y))
⊢ rexp y - rexp x < rexp y * (y - x)
have exp₂ : rexp y * (1 - rexp (x - y)) < rexp y * -(x - y)
Tactic: calc
      exp y - exp x = exp y - exp y * exp (x - y) := by rw [← exp_add]; ring_nf
      _ = exp y * (1 - exp (x - y)) := by ring
      _ < exp y * -(x - y) := by gcongr; linarith [add_one_lt_exp h2.ne]
      _ = exp y * (y - x) := by ring
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
exp : rexp y - rexp x = rexp y - rexp y * rexp (x - y)
exp₁ : rexp y - rexp y * rexp (x - y) = rexp y * (1 - rexp (x - y))
exp₂ : rexp y * (1 - rexp (x - y)) < rexp y * -(x - y)
⊢ rexp y - rexp x < rexp y * (y - x)
have exp₃ : rexp y * -(x - y) = rexp y * (y - x)
Tactic: calc
      exp y - exp x = exp y - exp y * exp (x - y) := by rw [← exp_add]; ring_nf
      _ = exp y * (1 - exp (x - y)) := by ring
      _ < exp y * -(x - y) := by gcongr; linarith [add_one_lt_exp h2.ne]
      _ = exp y * (y - x) := by ring
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
⊢ 0 < z - y
have linarith : z - y ≤ 0 → y - z + (z - y - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (hypothesis)
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
⊢ rexp y < (rexp z - rexp y) / (z - y)
have h1 : 0 < z - y
Tactic: have h1 : 0 < z - y := by linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ rexp y < (rexp z - rexp y) / (z - y)
have rw : rexp y * (z - y) < rexp z - rexp y
Tactic: rw [lt_div_iff₀ h1]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ rexp y * (z - y) < rexp y * (rexp (z - y) - 1)
have hbc : z - y < rexp (z - y) - 1
Tactic: gcongr _ * ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ z - y < rexp (z - y) - 1
have linarith : rexp (z - y) - 1 ≤ z - y → rexp (z - y) - 1 - (z - y) + (z - y + 1 - rexp (z - y)) = 0
Tactic: linarith [add_one_lt_exp h1.ne']
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ rexp (z - y) * rexp y - rexp y ≤ rexp z - rexp y
have rw : rexp (z - y + y) - rexp y ≤ rexp z - rexp y
Tactic: rw [← exp_add]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ rexp (z - y + y) - rexp y ≤ rexp z - rexp y
have ring_nf : rexp z - rexp y ≤ rexp z - rexp y
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ rexp y * (z - y) < rexp z - rexp y
have exp : rexp y * (z - y) < rexp y * (rexp (z - y) - 1)
Tactic: calc
      exp y * (z - y) < exp y * (exp (z - y) - 1) := by
        gcongr _ * ?_
        linarith [add_one_lt_exp h1.ne']
      _ = exp (z - y) * exp y - exp y := by ring
      _ ≤ exp z - exp y := by rw [← exp_add]; ring_nf; rfl
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
exp : rexp y * (z - y) < rexp y * (rexp (z - y) - 1)
⊢ rexp y * (z - y) < rexp z - rexp y
have exp₁ : rexp y * (rexp (z - y) - 1) = rexp (z - y) * rexp y - rexp y
Tactic: calc
      exp y * (z - y) < exp y * (exp (z - y) - 1) := by
        gcongr _ * ?_
        linarith [add_one_lt_exp h1.ne']
      _ = exp (z - y) * exp y - exp y := by ring
      _ ≤ exp z - exp y := by rw [← exp_add]; ring_nf; rfl
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
exp : rexp y * (z - y) < rexp y * (rexp (z - y) - 1)
exp₁ : rexp y * (rexp (z - y) - 1) = rexp (z - y) * rexp y - rexp y
⊢ rexp y * (z - y) < rexp z - rexp y
have exp₂ : rexp (z - y) * rexp y - rexp y ≤ rexp z - rexp y
Tactic: calc
      exp y * (z - y) < exp y * (exp (z - y) - 1) := by
        gcongr _ * ?_
        linarith [add_one_lt_exp h1.ne']
      _ = exp (z - y) * exp y - exp y := by ring
      _ ≤ exp z - exp y := by rw [← exp_add]; ring_nf; rfl
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
⊢ StrictConcaveOn ℝ (Ioi 0) log
have apply : ∀ {x y z : ℝ},
  Membership.mem (γ := Set ℝ) (Ioi 0) x →
    Membership.mem (γ := Set ℝ) (Ioi 0) z → x < y → y < z → (log z - log y) / (z - y) < (log y - log x) / (y - x)
Tactic: apply strictConcaveOn_of_slope_strict_anti_adjacent (convex_Ioi (0 : ℝ))
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
x y z : ℝ
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) x →
    Membership.mem (γ := Set ℝ) (Ioi 0) z → x < y → y < z → (log z - log y) / (z - y) < (log y - log x) / (y - x)
have this : ∀ (hx : 0 < x),
  Membership.mem (γ := Set ℝ) (Ioi 0) z → x < y → y < z → (log z - log y) / (z - y) < (log y - log x) / (y - x)
Tactic: (hx : 0 < x)
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
x y z : ℝ
hx : 0 < x
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) z → x < y → y < z → (log z - log y) / (z - y) < (log y - log x) / (y - x)
have this : ∀ (hz : 0 < z), x < y → y < z → (log z - log y) / (z - y) < (log y - log x) / (y - x)
Tactic: (hz : 0 < z)
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (hypothesis)
Goal:
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
⊢ (log z - log y) / (z - y) < (log y - log x) / (y - x)
have hy : 0 < y
Tactic: have hy : 0 < y := hx.trans hxy
-- 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
⊢ (log z - log y) / (z - y) < (log y - log x) / (y - x)
have trans : (log z - log y) / (z - y) < y⁻¹
Tactic: trans y⁻¹
-- 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
trans : (log z - log y) / (z - y) < y⁻¹
⊢ (log z - log y) / (z - y) < (log y - log x) / (y - x)
have trans₁ : y⁻¹ < (log y - log x) / (y - x)
Tactic: trans y⁻¹
-- 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
⊢ 0 < z - y
have linarith : z - y ≤ 0 → y - z + (z - y - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (hypothesis)
Goal:
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
⊢ (log z - log y) / (z - y) < y⁻¹
have h : 0 < z - y
Tactic: have h : 0 < z - y := by linarith
-- 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 < z - y
⊢ (log z - log y) / (z - y) < y⁻¹
have rw : log z - log y < y⁻¹ * (z - y)
Tactic: rw [div_lt_iff₀ h]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (hypothesis)
Goal:
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < z - y
⊢ log z - log y < y⁻¹ * (z - y)
have hyz' : 0 < z / y
Tactic: have hyz' : 0 < z / y := by positivity
-- 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 < z - y
hyz' : 0 < z / y
⊢ z / y ≠ 1
have contrapose! : ∀ (h : z / y = 1), z - y ≤ 0
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (hypothesis)
Goal:
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
hyz' : 0 < z / y
h : z / y = 1
⊢ z - y ≤ 0
have h₁ : z = y
Tactic: rw [div_eq_one_iff_eq hy.ne'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (hypothesis)
Goal:
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < z - y
hyz' : 0 < z / y
⊢ log z - log y < y⁻¹ * (z - y)
have hyz'' : z / y ≠ 1
Tactic: have hyz'' : z / y ≠ 1 := by
      contrapose! h
      rw [div_eq_one_iff_eq hy.ne'] at h
      simp [h]
-- 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 < z - y
hyz' : 0 < z / y
hyz'' : z / y ≠ 1
⊢ log z - log y = log (z / y)
have rw : log (z / y) = log (z / y)
Tactic: rw [← log_div hz.ne' hy.ne']
-- 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 < z - y
hyz' : 0 < z / y
hyz'' : z / y ≠ 1
⊢ log z - log y < y⁻¹ * (z - y)
have log : log z - log y = log (z / y)
Tactic: calc
      log z - log y = log (z / y) := by rw [← log_div hz.ne' hy.ne']
      _ < z / y - 1 := log_lt_sub_one_of_pos hyz' hyz''
      _ = y⁻¹ * (z - y) := by field
-- 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 < z - y
hyz' : 0 < z / y
hyz'' : z / y ≠ 1
log : Real.log z - Real.log y = Real.log (z / y)
⊢ Real.log z - Real.log y < y⁻¹ * (z - y)
have log₁ : z / y - 1 = y⁻¹ * (z - y)
Tactic: calc
      log z - log y = log (z / y) := by rw [← log_div hz.ne' hy.ne']
      _ < z / y - 1 := log_lt_sub_one_of_pos hyz' hyz''
      _ = y⁻¹ * (z - y) := by field
-- 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
⊢ 0 < y - x
have linarith : y - x ≤ 0 → x - y + (y - x - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (hypothesis)
Goal:
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
⊢ y⁻¹ < (log y - log x) / (y - x)
have h : 0 < y - x
Tactic: have h : 0 < y - x := by linarith
-- 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
⊢ y⁻¹ < (log y - log x) / (y - x)
have rw : y⁻¹ * (y - x) < log y - log x
Tactic: rw [lt_div_iff₀ h]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (hypothesis)
Goal:
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < y - x
⊢ y⁻¹ * (y - x) < log y - log x
have hxy' : 0 < x / y
Tactic: have hxy' : 0 < x / y := by positivity
-- 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
⊢ x / y ≠ 1
have contrapose! : ∀ (h : x / y = 1), y - x ≤ 0
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (hypothesis)
Goal:
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
hxy' : 0 < x / y
h : x / y = 1
⊢ y - x ≤ 0
have h₁ : x = y
Tactic: rw [div_eq_one_iff_eq hy.ne'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (hypothesis)
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
⊢ y⁻¹ * (y - x) < log y - log x
have hxy'' : x / y ≠ 1
Tactic: have hxy'' : x / y ≠ 1 := by
      contrapose! h
      rw [div_eq_one_iff_eq hy.ne'] at h
      simp [h]
-- 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
⊢ 1 - x / y < -log (x / y)
have linarith : -log (x / y) ≤ 1 - x / y →
  -(1 * log (x / y)) - (HMul.hMul (α := ℝ) 1 1 - 1 * (x / y)) +
      (1 * log (x / y) - (1 * (x / y) - HMul.hMul (α := ℝ) 1 1)) =
    0
Tactic: linarith [log_lt_sub_one_of_pos hxy' hxy'']
-- 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
⊢ -log (x / y) = -(log x - log y)
have rw : -(log x - log y) = -(log x - log y)
Tactic: rw [log_div hx.ne' hy.ne']
-- 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
⊢ y⁻¹ * (y - x) < log y - log x
have x₁ : y⁻¹ * (y - x) = 1 - x / y
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 (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
⊢ y⁻¹ * (y - x) < log y - log x
have x₂ : 1 - x / y < -log (x / y)
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 (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)
⊢ y⁻¹ * (y - x) < log y - log x
have x₃ : -log (x / y) = -(log x - log y)
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