awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Slope
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 ∈ Set.Ioo y v

Tactic:
exact ⟨hu2, huv⟩
-- Module: Mathlib.Analysis.Convex.Slope
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
⊢ Membership.mem (γ := Set 𝕜) ((⇑(-AffineMap.id 𝕜 𝕜) : (a : 𝕜) → 𝕜) ⁻¹' s) (-y)

Tactic:
simpa
-- Module: Mathlib.Analysis.Convex.Slope
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
⊢ (f ∘ (⇑(-AffineMap.id 𝕜 𝕜) : (a : 𝕜) → 𝕜)) (-y) < (f ∘ (⇑(-AffineMap.id 𝕜 𝕜) : (a : 𝕜) → 𝕜)) (-x)

Tactic:
simpa
-- Module: Mathlib.Analysis.Convex.Slope
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
⊢ 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)
-- Module: Mathlib.Analysis.Convex.Slope
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
this :
  StrictMonoOn (f ∘ (⇑(-AffineMap.id 𝕜 𝕜) : (a : 𝕜) → 𝕜)) ((⇑(-AffineMap.id 𝕜 𝕜) : (a : 𝕜) → 𝕜) ⁻¹' s ∩ Set.Ici (-x))
x_1 : 𝕜
h : x_1 ∈ s ∩ Set.Iic x
⊢ -id x_1 ∈ (⇑(-AffineMap.id 𝕜 𝕜) : (a : 𝕜) → 𝕜) ⁻¹' s ∩ Set.Ici (-x)

Tactic:
simpa
-- Module: Mathlib.Analysis.Convex.Slope
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
this :
  StrictMonoOn (f ∘ (⇑(-AffineMap.id 𝕜 𝕜) : (a : 𝕜) → 𝕜)) ((⇑(-AffineMap.id 𝕜 𝕜) : (a : 𝕜) → 𝕜) ⁻¹' s ∩ Set.Ici (-x))
⊢ StrictAntiOn f (s ∩ Set.Iic x)

Tactic:
simpa [Function.comp_def] using this.comp_strictAntiOn strictMonoOn_id.neg fun _ _ ↦ by simpa

Premises used: strictMonoOn_id, StrictMonoOn.comp_strictAntiOn, StrictMonoOn.neg, Function.comp_def
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConcaveOn 𝕜 s f
x y : 𝕜
hy : y ∈ s
hxy : x < y
hxy' : f x < f y
⊢ StrictMonoOn f (s ∩ Set.Iic x)

Tactic:
simpa using (neg_convexOn_iff.mpr hf |>.strictAntiOn hy hxy <| neg_lt_neg hxy').neg

Premises used: Iff.mpr, StrictAntiOn.neg, neg_convexOn_iff, neg_lt_neg, ConvexOn.strictAntiOn
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConcaveOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f y < f x
⊢ StrictAntiOn f (s ∩ Set.Ici y)

Tactic:
simpa using (neg_convexOn_iff.mpr hf |>.strictMonoOn hx hxy <| neg_lt_neg hxy').neg

Premises used: Iff.mpr, StrictMonoOn.neg, neg_convexOn_iff, neg_lt_neg, ConvexOn.strictMonoOn
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
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)
⊢ StrictConvexOn ℝ univ rexp

Tactic:
apply strictConvexOn_of_slope_strict_mono_adjacent convex_univ

Premises used: strictConvexOn_of_slope_strict_mono_adjacent, convex_univ
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
trans : (rexp y - rexp x) / (y - x) < rexp y
trans₁ : rexp y < (rexp z - rexp y) / (z - y)
⊢ (rexp y - rexp x) / (y - x) < (rexp z - rexp y) / (z - y)

Tactic:
trans exp y

Premises used: Real.exp
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
linarith : y - x ≤ 0 → x - y + (y - x - 0) = 0
⊢ 0 < y - x

Tactic:
linarith
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
⊢ 0 < y - x

Tactic:
have h1 : 0 < y - x := by linarith
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
linarith : 0 ≤ x - y → x - y + (0 - (x - y)) = 0
⊢ x - y < 0

Tactic:
linarith
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
⊢ x - y < 0

Tactic:
have h2 : x - y < 0 := by linarith
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
rw : rexp y - rexp x < rexp y * (y - x)
⊢ (rexp y - rexp x) / (y - x) < rexp y

Tactic:
rw [div_lt_iff₀ h1]

Premises used: div_lt_iff₀
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
rw : rexp y - rexp x = rexp y - rexp (y + (x - y))
⊢ rexp y - rexp x = rexp y - rexp y * rexp (x - y)

Tactic:
rw [← exp_add]

Premises used: Real.exp_add
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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 + (x - y))

Tactic:
ring_nf
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ rexp y - rexp y * rexp (x - y) = rexp y * (1 - rexp (x - y))

Tactic:
ring
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
hbc : 1 - rexp (x - y) < -(x - y)
⊢ rexp y * (1 - rexp (x - y)) < rexp y * -(x - y)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
linarith : -(x - y) ≤ 1 - rexp (x - y) → -(x - y) - (1 - rexp (x - y)) + (x - y + 1 - rexp (x - y)) = 0
⊢ 1 - rexp (x - y) < -(x - y)

Tactic:
linarith [add_one_lt_exp h2.ne]

Premises used: Real.add_one_lt_exp, LT.lt.ne
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ rexp y * -(x - y) = rexp y * (y - x)

Tactic:
ring
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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)
exp₃ : rexp y * -(x - y) = rexp y * (y - x)
⊢ rexp y - rexp x < 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

Premises used: HSub.hSub, Real.exp, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
linarith : z - y ≤ 0 → y - z + (z - y - 0) = 0
⊢ 0 < z - y

Tactic:
linarith
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
⊢ 0 < z - y

Tactic:
have h1 : 0 < z - y := by linarith
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
rw : rexp y * (z - y) < rexp z - rexp y
⊢ rexp y < (rexp z - rexp y) / (z - y)

Tactic:
rw [lt_div_iff₀ h1]

Premises used: lt_div_iff₀
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
hbc : z - y < rexp (z - y) - 1
⊢ rexp y * (z - y) < rexp y * (rexp (z - y) - 1)

Tactic:
gcongr _ * ?_
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
linarith : rexp (z - y) - 1 ≤ z - y → rexp (z - y) - 1 - (z - y) + (z - y + 1 - rexp (z - y)) = 0
⊢ z - y < rexp (z - y) - 1

Tactic:
linarith [add_one_lt_exp h1.ne']

Premises used: LT.lt.ne', Real.add_one_lt_exp
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ rexp y * (rexp (z - y) - 1) = rexp (z - y) * rexp y - rexp y

Tactic:
ring
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
rw : rexp (z - y + y) - rexp y ≤ rexp z - rexp y
⊢ rexp (z - y) * rexp y - rexp y ≤ rexp z - rexp y

Tactic:
rw [← exp_add]

Premises used: Real.exp_add
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
ring_nf : rexp z - rexp y ≤ rexp z - rexp y
⊢ rexp (z - y + y) - rexp y ≤ rexp z - rexp y

Tactic:
ring_nf
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ rexp z - rexp y ≤ rexp z - rexp y

Tactic:
rfl
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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
exp₂ : rexp (z - y) * rexp y - rexp y ≤ rexp z - rexp y
⊢ rexp y * (z - 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

Premises used: HSub.hSub, Real.exp, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
⊢ ConvexOn ℝ univ rexp

Tactic:
strictConvexOn_exp.convexOn

Premises used: strictConvexOn_exp, StrictConvexOn.convexOn
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
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)
⊢ StrictConcaveOn ℝ (Ioi 0) log

Tactic:
apply strictConcaveOn_of_slope_strict_anti_adjacent (convex_Ioi (0 : ℝ))

Premises used: strictConcaveOn_of_slope_strict_anti_adjacent, OfNat.ofNat, convex_Ioi
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x y z : ℝ
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)
⊢ 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:
(hx : 0 < x)
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x y z : ℝ
hx : 0 < x
this : ∀ (hz : 0 < z), x < y → y < z → (log z - log y) / (z - y) < (log y - log x) / (y - x)
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) z → x < y → y < z → (log z - log y) / (z - y) < (log y - log x) / (y - x)

Tactic:
(hz : 0 < z)
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
⊢ 0 < y

Tactic:
have hy : 0 < y := hx.trans hxy
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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⁻¹
trans₁ : y⁻¹ < (log y - log x) / (y - x)
⊢ (log z - log y) / (z - y) < (log y - log x) / (y - x)

Tactic:
trans y⁻¹
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
linarith : z - y ≤ 0 → y - z + (z - y - 0) = 0
⊢ 0 < z - y

Tactic:
linarith
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
⊢ 0 < z - y

Tactic:
have h : 0 < z - y := by linarith
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < z - y
rw : log z - log y < y⁻¹ * (z - y)
⊢ (log z - log y) / (z - y) < y⁻¹

Tactic:
rw [div_lt_iff₀ h]

Premises used: div_lt_iff₀
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < z - y
⊢ 0 < z / y

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < z - y
⊢ 0 < z / y

Tactic:
have hyz' : 0 < z / y := by positivity
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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
contrapose! : ∀ (h : z / y = 1), z - y ≤ 0
⊢ z / y ≠ 1

Tactic:
contrapose! h
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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

Tactic:
rw [div_eq_one_iff_eq hy.ne'] at h

Premises used: div_eq_one_iff_eq, LT.lt.ne'
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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
⊢ z - y ≤ 0

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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

Tactic:
have hyz'' : z / y ≠ 1 := by
      contrapose! h
      rw [div_eq_one_iff_eq hy.ne'] at h
      simp [h]
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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
rw rw₁ : log (z / y) = log (z / y)
⊢ log z - log y = log (z / y)

Tactic:
rw [← log_div hz.ne' hy.ne']

Premises used: Real.log_div, LT.lt.ne'
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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 / y) < z / y - 1

Tactic:
log_lt_sub_one_of_pos hyz' hyz''

Premises used: Real.log_lt_sub_one_of_pos
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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
⊢ z / y - 1 = y⁻¹ * (z - y)

Tactic:
field
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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)
log₁ : z / y - 1 = y⁻¹ * (z - y)
⊢ Real.log z - Real.log y < 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

Premises used: HSub.hSub, HDiv.hDiv, Real.log_lt_sub_one_of_pos, Real.log
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
linarith : y - x ≤ 0 → x - y + (y - x - 0) = 0
⊢ 0 < y - x

Tactic:
linarith
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
⊢ 0 < y - x

Tactic:
have h : 0 < y - x := by linarith
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < y - x
rw : y⁻¹ * (y - x) < log y - log x
⊢ y⁻¹ < (log y - log x) / (y - x)

Tactic:
rw [lt_div_iff₀ h]

Premises used: lt_div_iff₀
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < y - x
⊢ 0 < x / y

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < y - x
⊢ 0 < x / y

Tactic:
have hxy' : 0 < x / y := by positivity
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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
contrapose! : ∀ (h : x / y = 1), y - x ≤ 0
⊢ x / y ≠ 1

Tactic:
contrapose! h
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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
⊢ x = y

Tactic:
rw [div_eq_one_iff_eq hy.ne'] at h

Premises used: div_eq_one_iff_eq, LT.lt.ne'
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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
⊢ y - x ≤ 0

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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

Tactic:
have hxy'' : x / y ≠ 1 := by
      contrapose! h
      rw [div_eq_one_iff_eq hy.ne'] at h
      simp [h]
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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) = 1 - x / y

Tactic:
field
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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
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
⊢ 1 - x / y < -log (x / y)

Tactic:
linarith [log_lt_sub_one_of_pos hxy' hxy'']

Premises used: Real.log_lt_sub_one_of_pos
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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
rw rw₁ : -(log x - log y) = -(log x - log y)
⊢ -log (x / y) = -(log x - log y)

Tactic:
rw [log_div hx.ne' hy.ne']

Premises used: Real.log_div, LT.lt.ne'
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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 - log y) = log y - log x

Tactic:
ring
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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)
x₄ : -(log x - log y) = log y - log x
⊢ y⁻¹ * (y - x) < 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

Premises used: HSub.hSub, HDiv.hDiv, Real.log
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
⊢ 0 < p

Tactic:
have hp' : 0 < p := zero_lt_one.trans hp
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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
inr : ∀ (hs : -1 < s), 1 + p * s < (1 + s) ^ p
⊢ 1 + p * s < (1 + s) ^ p

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 : ℝ
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
inl₃ : 1 < 0 + p
inl₄ inl₅ inl₆ inl₇ : 1 < p
⊢ 1 + p * -1 < HAdd.hAdd (α := ℝ) 1 (-1) ^ p

Tactic:
rwa [add_neg_cancel, zero_rpow hp'.ne', mul_neg_one, add_neg_lt_iff_lt_add, zero_add]

Premises used: add_neg_cancel, zero_add, Real.zero_rpow, LT.lt.ne', mul_neg_one, add_neg_lt_iff_lt_add
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
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 : ℝ
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
inr₁ : ∀ (hs2 : 0 < 1 + p * s), 1 + p * s < (1 + s) ^ p
⊢ 1 + p * s < (1 + s) ^ p

Tactic:
rcases le_or_gt (1 + p * s) 0 with hs2 | hs2

Premises used: HMul.hMul, le_or_gt, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 1 + p * s ≤ 0
⊢ 1 + p * s < (1 + s) ^ p

Tactic:
hs2.trans_lt (rpow_pos_of_pos hs1 _)

Premises used: Real.rpow_pos_of_pos, LE.le.trans_lt
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
s : ℝ
hs_1 : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 1 + p * s ≤ 0
⊢ 1 + p * s < (1 + s) ^ p

Tactic:
exact hs2.trans_lt (rpow_pos_of_pos hs1 _)

Premises used: Real.rpow_pos_of_pos, LE.le.trans_lt
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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 + 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 : ℝ
hp : 1 < p
hp' : 0 < p
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 : ℝ
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
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (hs' : s = 0), s = 0
⊢ s = 0

Tactic:
rwa [add_eq_left, mul_eq_zero, eq_false_intro hp'.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 : ℝ
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

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'
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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 : rexp (log (1 + p * s)) < rexp (log (1 + s) * p)
⊢ 1 + p * s < (1 + s) ^ p

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 : ℝ
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 : log (1 + p * s) < log (1 + s) * p
⊢ rexp (log (1 + p * s)) < rexp (log (1 + s) * p)

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 : ℝ
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
inr₁ : ∀ (hs' : 0 < s), log (1 + p * s) < log (1 + s) * p
⊢ log (1 + p * s) < log (1 + s) * p

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 : ℝ
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 : log (1 + s) / s < log (1 + p * s) / p / s
⊢ log (1 + p * s) < log (1 + s) * p

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

Premises used: div_lt_div_right_of_neg, div_lt_iff₀