awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
p : ℝ
hp : 1 < p
x y z : ℝ
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)
⊢ 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:
(hx : 0 ≤ x)
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
this : ∀ (hz : 0 ≤ z), x < y → y < z → (y ^ p - x ^ p) / (y - x) < (z ^ p - y ^ p) / (z - y)
⊢ Membership.mem (γ := Set ℝ) (Ici 0) z → x < y → y < z → (y ^ p - x ^ p) / (y - x) < (z ^ p - y ^ p) / (z - y)

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

Tactic:
have hy : 0 < y := hx.trans_lt hxy
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
⊢ 0 < y ^ p

Tactic:
have hy' : 0 < y ^ p := rpow_pos_of_pos hy _
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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)
trans₁ : p * y ^ (p - 1) < (z ^ p - y ^ p) / (z - y)
⊢ (y ^ p - x ^ p) / (y - x) < (z ^ p - y ^ p) / (z - y)

Tactic:
trans p * y ^ (p - 1)

Premises used: HSub.hSub, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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
rwa rwa₁ rwa₂ rwa₃ : x < y
⊢ 0 < y - x

Tactic:
rwa [sub_pos]

Premises used: sub_pos
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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
⊢ 0 < y - x

Tactic:
have q : 0 < y - x := by rwa [sub_pos]
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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
rw : 1 + p * (x / y - 1) < (1 + (x / y - 1)) ^ p
⊢ (y ^ p - x ^ p) / (y - x) < p * y ^ (p - 1)

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']

Premises used: add_sub_assoc, neg_sub, neg_div, Real.rpow_neg_one, sub_lt_comm, div_lt_div_iff_of_pos_right, mul_assoc, mul_div_assoc, sub_eq_add_neg, sub_sub_cancel_left, HDiv.hDiv, LT.lt.le, sub_div, div_mul_eq_mul_div, Real.div_rpow, div_lt_iff₀, add_comm, LT.lt.ne', add_sub_cancel_right, Real.rpow_sub, div_eq_inv_mul, OfNat.ofNat, div_self, mul_neg
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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
apply₁ : x / y - 1 ≠ 0
⊢ 1 + p * (x / y - 1) < (1 + (x / y - 1)) ^ p

Tactic:
apply one_add_mul_self_lt_rpow_one_add _ _ hp

Premises used: one_add_mul_self_lt_rpow_one_add
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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
rw : 0 ≤ x ∧ 0 ≤ y ∨ x ≤ 0 ∧ y ≤ 0
⊢ -1 ≤ x / y - 1

Tactic:
rw [le_sub_iff_add_le, neg_add_cancel, div_nonneg_iff]

Premises used: neg_add_cancel, div_nonneg_iff, le_sub_iff_add_le
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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
⊢ 0 ≤ x ∧ 0 ≤ y ∨ x ≤ 0 ∧ y ≤ 0

Tactic:
Or.inl ⟨hx, hy.le⟩

Premises used: LT.lt.le, And.intro, Or.inl
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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
⊢ 0 ≤ x ∧ 0 ≤ y ∨ x ≤ 0 ∧ y ≤ 0

Tactic:
exact Or.inl ⟨hx, hy.le⟩

Premises used: Or.inl
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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
rw : x / y ≠ 1
⊢ x / y - 1 ≠ 0

Tactic:
rw [sub_ne_zero]

Premises used: sub_ne_zero
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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

Tactic:
((div_lt_one hy).mpr hxy).ne

Premises used: Iff.mpr, div_lt_one, LT.lt.ne
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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

Tactic:
exact ((div_lt_one hy).mpr hxy).ne

Premises used: Iff.mpr, div_lt_one, LT.lt.ne
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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
rwa rwa₁ rwa₂ rwa₃ : y < z
⊢ 0 < z - y

Tactic:
rwa [sub_pos]

Premises used: sub_pos
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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
⊢ 0 < z - y

Tactic:
have q : 0 < z - y := by rwa [sub_pos]
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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 < z - y
rw : 1 + p * (z / y - 1) < (1 + (z / y - 1)) ^ p
⊢ p * y ^ (p - 1) < (z ^ p - y ^ p) / (z - y)

Tactic:
rw [lt_div_iff₀ q, ← div_lt_div_iff_of_pos_right hy', _root_.sub_div, div_self hy'.ne',
      ← div_rpow hz hy.le, lt_sub_iff_add_lt', ← add_sub_cancel_right (z / y) 1, add_comm _ 1,
      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, _root_.sub_div, div_self hy.ne']

Premises used: add_sub_assoc, Real.rpow_neg_one, lt_sub_iff_add_lt', lt_div_iff₀, div_lt_div_iff_of_pos_right, mul_assoc, mul_div_assoc, sub_sub_cancel_left, HDiv.hDiv, LT.lt.le, sub_div, div_mul_eq_mul_div, Real.div_rpow, add_comm, LT.lt.ne', add_sub_cancel_right, Real.rpow_sub, div_eq_inv_mul, OfNat.ofNat, div_self
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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 < z - y
apply : -1 ≤ z / y - 1
apply₁ : z / y - 1 ≠ 0
⊢ 1 + p * (z / y - 1) < (1 + (z / y - 1)) ^ p

Tactic:
apply one_add_mul_self_lt_rpow_one_add _ _ hp

Premises used: one_add_mul_self_lt_rpow_one_add
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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 < z - y
rw : 0 ≤ z ∧ 0 ≤ y ∨ z ≤ 0 ∧ y ≤ 0
⊢ -1 ≤ z / y - 1

Tactic:
rw [le_sub_iff_add_le, neg_add_cancel, div_nonneg_iff]

Premises used: neg_add_cancel, div_nonneg_iff, le_sub_iff_add_le
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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 < z - y
⊢ 0 ≤ z ∧ 0 ≤ y ∨ z ≤ 0 ∧ y ≤ 0

Tactic:
Or.inl ⟨hz, hy.le⟩

Premises used: LT.lt.le, And.intro, Or.inl
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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 < z - y
⊢ 0 ≤ z ∧ 0 ≤ y ∨ z ≤ 0 ∧ y ≤ 0

Tactic:
exact Or.inl ⟨hz, hy.le⟩

Premises used: Or.inl
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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 < z - y
rw : z / y ≠ 1
⊢ z / y - 1 ≠ 0

Tactic:
rw [sub_ne_zero]

Premises used: sub_ne_zero
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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 < z - y
⊢ z / y ≠ 1

Tactic:
((one_lt_div hy).mpr hyz).ne'

Premises used: Iff.mpr, one_lt_div, LT.lt.ne'
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
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 < z - y
⊢ z / y ≠ 1

Tactic:
exact ((one_lt_div hy).mpr hyz).ne'

Premises used: Iff.mpr, one_lt_div, LT.lt.ne'
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
p : ℝ
hp : 1 ≤ p
inl : ∀ (hp : LE.le (α := ℝ) 1 1), ConvexOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ HPow.hPow (β := ℝ) x 1
inr : ∀ (hp : 1 < p), ConvexOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ x ^ p
⊢ ConvexOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ x ^ 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:
hp : LE.le (α := ℝ) 1 1
⊢ ConvexOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ HPow.hPow (β := ℝ) x 1

Tactic:
simpa using convexOn_id (convex_Ici _)

Premises used: convexOn_id, convex_Ici
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
p : ℝ
hp_1 : 1 ≤ p
hp : 1 < p
⊢ ConvexOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ x ^ p

Tactic:
(strictConvexOn_rpow hp).convexOn

Premises used: strictConvexOn_rpow, StrictConvexOn.convexOn
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
p : ℝ
hp_1 : 1 ≤ p
hp : 1 < p
⊢ ConvexOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ x ^ p

Tactic:
exact (strictConvexOn_rpow hp).convexOn

Premises used: strictConvexOn_rpow, StrictConvexOn.convexOn
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
b : ℝ
hb : 0 < b
⊢ ConvexOn ℝ (E := ℝ)
    (preimage (β := ℝ) (⇑((LinearMap.mul ℝ ℝ : (a : ℝ) → ℝ →ₗ[ℝ] ℝ) (log b) : ℝ →ₗ[ℝ] ℝ) : (a : ℝ) → ℝ) univ)
    (rexp ∘ (⇑((LinearMap.mul ℝ ℝ : (a : ℝ) → ℝ →ₗ[ℝ] ℝ) (log b) : ℝ →ₗ[ℝ] ℝ) : (a : ℝ) → ℝ))

Tactic:
convexOn_exp.comp_linearMap (LinearMap.mul ℝ ℝ (Real.log b))

Premises used: Real, Real.log, convexOn_exp, LinearMap.mul, DFunLike.coe, ConvexOn.comp_linearMap
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
b : ℝ
hb : 0 < b
h :
  Eq (α := ℝ → ℝ) (fun (x : ℝ) ↦ b ^ x)
    (rexp ∘ (⇑((LinearMap.mul ℝ ℝ : (a : ℝ) → ℝ →ₗ[ℝ] ℝ) (log b) : ℝ →ₗ[ℝ] ℝ) : (a : ℝ) → ℝ))
⊢ ConvexOn ℝ (β := ℝ) univ fun (x : ℝ) ↦ b ^ x

Tactic:
convert! convexOn_exp.comp_linearMap (LinearMap.mul ℝ ℝ (Real.log b)) using 1

Premises used: Real, Real.log, convexOn_exp, LinearMap.mul, DFunLike.coe, ConvexOn.comp_linearMap
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
b : ℝ
hb : 0 < b
h : ∀ (x : ℝ), b ^ x = (rexp ∘ (⇑((LinearMap.mul ℝ ℝ : (a : ℝ) → ℝ →ₗ[ℝ] ℝ) (log b) : ℝ →ₗ[ℝ] ℝ) : (a : ℝ) → ℝ)) x
⊢ Eq (α := ℝ → ℝ) (fun (x : ℝ) ↦ b ^ x)
    (rexp ∘ (⇑((LinearMap.mul ℝ ℝ : (a : ℝ) → ℝ →ₗ[ℝ] ℝ) (log b) : ℝ →ₗ[ℝ] ℝ) : (a : ℝ) → ℝ))

Tactic:
ext x
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
b : ℝ
hb : 0 < b
x : ℝ
⊢ b ^ x = (rexp ∘ (⇑((LinearMap.mul ℝ ℝ : (a : ℝ) → ℝ →ₗ[ℝ] ℝ) (log b) : ℝ →ₗ[ℝ] ℝ) : (a : ℝ) → ℝ)) x

Tactic:
simp [Real.rpow_def_of_pos hb]

Premises used: Real.rpow_def_of_pos
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
⊢ StrictConcaveOn ℝ (Iio 0) log

Tactic:
⟨convex_Iio _, ?_⟩

Premises used: StrictConcaveOn, And.intro, convex_Iio
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
refine :
  ∀ ⦃x : ℝ⦄,
    Membership.mem (γ := Set ℝ) (Iio 0) x →
      ∀ ⦃y : ℝ⦄,
        Membership.mem (γ := Set ℝ) (Iio 0) y →
          x ≠ y → ∀ ⦃a b : ℝ⦄, 0 < a → 0 < b → a + b = 1 → a • log x + b • log y < log (a • x + b • y)
⊢ StrictConcaveOn ℝ (Iio 0) log

Tactic:
refine ⟨convex_Iio _, ?_⟩
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x : ℝ
x₁ :
  ∀ (hx : x < 0) ⦃y : ℝ⦄,
    Membership.mem (γ := Set ℝ) (Iio 0) y →
      x ≠ y → ∀ ⦃a b : ℝ⦄, 0 < a → 0 < b → a + b = 1 → a • log x + b • log y < log (a • x + b • y)
⊢ Membership.mem (γ := Set ℝ) (Iio 0) x →
    ∀ ⦃y : ℝ⦄,
      Membership.mem (γ := Set ℝ) (Iio 0) y →
        x ≠ y → ∀ ⦃a b : ℝ⦄, 0 < a → 0 < b → a + b = 1 → a • log x + b • log y < log (a • x + b • y)

Tactic:
(hx : x < 0)
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x : ℝ
hx : x < 0
y : ℝ
y₁ : ∀ (hy : y < 0), x ≠ y → ∀ ⦃a b : ℝ⦄, 0 < a → 0 < b → a + b = 1 → a • log x + b • log y < log (a • x + b • y)
⊢ Membership.mem (γ := Set ℝ) (Iio 0) y →
    x ≠ y → ∀ ⦃a b : ℝ⦄, 0 < a → 0 < b → a + b = 1 → a • log x + b • log y < log (a • x + b • y)

Tactic:
(hy : y < 0)
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
linarith : -x ≤ 0 → x - 0 + (-x - 0) = 0
⊢ 0 < -x

Tactic:
linarith
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 < -x

Tactic:
have hx' : 0 < -x := by linarith
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
linarith : -y ≤ 0 → y - 0 + (-y - 0) = 0
⊢ 0 < -y

Tactic:
linarith
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
⊢ 0 < -y

Tactic:
have hy' : 0 < -y := by linarith
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
contrapose : ∀ (hxy : -x = -y), x = y
⊢ -x ≠ -y

Tactic:
contrapose hxy
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
hxy : -x = -y
linarith : x < y → -x - -y + (x - y) = 0
linarith₁ : y < x → -(-x - -y) + (y - x) = 0
⊢ x = y

Tactic:
linarith
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
⊢ -x ≠ -y

Tactic:
have hxy' : -x ≠ -y := by contrapose hxy; linarith
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
hxy' : -x ≠ -y
⊢ a • log x + b • log y = a • log (-x) + b • log (-y)

Tactic:
simp_rw [log_neg_eq_log]

Premises used: Real.log_neg_eq_log
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
hxy' : -x ≠ -y
⊢ a • log (-x) + b • log (-y) < log (a • -x + b • -y)

Tactic:
strictConcaveOn_log_Ioi.2 hx' hy' hxy' ha hb hab

Premises used: And.right, strictConcaveOn_log_Ioi
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
hxy' : -x ≠ -y
e_x : a • -x + b • -y = -(a • x + b • y)
⊢ log (a • -x + b • -y) = log (-(a • x + b • y))

Tactic:
congr 1
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
hxy' : -x ≠ -y
⊢ a * -x + b * -y = -(a * x + b * y)

Tactic:
ring
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
hxy' : -x ≠ -y
rw rw₁ : log (a • x + b • y) = log (a • x + b • y)
⊢ log (-(a • x + b • y)) = log (a • x + b • y)

Tactic:
rw [log_neg_eq_log]

Premises used: Real.log_neg_eq_log
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
hxy' : -x ≠ -y
a₁ : a • log x + b • log y = a • log (-x) + b • log (-y)
a₂ : log (a • -x + b • -y) = log (-(a • x + b • y))
a₃ : log (-(a • x + b • y)) = log (a • x + b • y)
⊢ a • log x + b • log y < log (a • x + b • y)

Tactic:
calc
    a • log x + b • log y = a • log (-x) + b • log (-y) := by simp_rw [log_neg_eq_log]
    _ < log (a • -x + b • -y) := strictConcaveOn_log_Ioi.2 hx' hy' hxy' ha hb hab
    _ = log (-(a • x + b • y)) := by congr 1; simp only [smul_eq_mul]; ring
    _ = _ := by rw [log_neg_eq_log]

Premises used: Real.log, And.right, HAdd.hAdd, HSMul.hSMul, strictConcaveOn_log_Ioi, Neg.neg
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
t : ℝ
ht : |t| ≤ 1
x : ℝ
rw : ∀ (ht : -1 ≤ t ∧ t ≤ 1) (x : ℝ), rexp (t * x) ≤ cosh x + t * sinh x
⊢ rexp (t * x) ≤ cosh x + t * sinh x

Tactic:
rw [abs_le] at ht

Premises used: abs_le
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
t : ℝ
ht : -1 ≤ t ∧ t ≤ 1
x : ℝ
⊢ rexp (t * x) = rexp ((1 + t) / 2 * x + (1 - t) / 2 * -x)

Tactic:
ring_nf
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
t : ℝ
ht : -1 ≤ t ∧ t ≤ 1
x : ℝ
linarith : (1 + t) / 2 < 0 → 2 / 2 = 1
linarith₁ : (1 + t) / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : (1 + t) / 2 < 0 → GT.gt (α := ℝ) 2 0
linarith₃ : (1 + t) / 2 < 0 → -1 - t + (HMul.hMul (α := ℝ) 1 1 + 1 * t - HMul.hMul (α := ℝ) 2 0) = 0
⊢ 0 ≤ (1 + t) / 2

Tactic:
linarith
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
t : ℝ
ht : -1 ≤ t ∧ t ≤ 1
x : ℝ
linarith : (1 - t) / 2 < 0 → 2 / 2 = 1
linarith₁ : (1 - t) / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : (1 - t) / 2 < 0 → GT.gt (α := ℝ) 2 0
linarith₃ : (1 - t) / 2 < 0 → t - 1 + (HMul.hMul (α := ℝ) 1 1 - 1 * t - HMul.hMul (α := ℝ) 2 0) = 0
⊢ 0 ≤ (1 - t) / 2

Tactic:
linarith
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
t : ℝ
ht : -1 ≤ t ∧ t ≤ 1
x : ℝ
⊢ (1 + t) / 2 + (1 - t) / 2 = 1

Tactic:
ring
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
t : ℝ
ht : -1 ≤ t ∧ t ≤ 1
x : ℝ
rw : (1 + t) / 2 * rexp x + (1 - t) / 2 * rexp (-x) = (rexp x + rexp (-x)) / 2 + t * ((rexp x - rexp (-x)) / 2)
⊢ (1 + t) / 2 * rexp x + (1 - t) / 2 * rexp (-x) = cosh x + t * sinh x

Tactic:
rw [cosh_eq, sinh_eq]

Premises used: Real.sinh_eq, Real.cosh_eq
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
t : ℝ
ht : -1 ≤ t ∧ t ≤ 1
x : ℝ
⊢ (1 + t) / 2 * rexp x + (1 - t) / 2 * rexp (-x) = (rexp x + rexp (-x)) / 2 + t * ((rexp x - rexp (-x)) / 2)

Tactic:
ring
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic
Goal:
t : ℝ
ht : -1 ≤ t ∧ t ≤ 1
x : ℝ
_ : rexp (t * x) = rexp ((1 + t) / 2 * x + (1 - t) / 2 * -x)
_₁ : (1 + t) / 2 * rexp x + (1 - t) / 2 * rexp (-x) = cosh x + t * sinh x
⊢ rexp (t * x) ≤ cosh x + t * sinh x

Tactic:
calc
    _ = exp ((1 + t) / 2 * x + (1 - t) / 2 * (-x)) := by ring_nf
    _ ≤ (1 + t) / 2 * exp x + (1 - t) / 2 * exp (-x) :=
        convexOn_exp.2 (Set.mem_univ _) (Set.mem_univ _) (by linarith) (by linarith) <| by ring
    _ = _ := by rw [cosh_eq, sinh_eq]; ring

Premises used: HMul.hMul, HSub.hSub, HDiv.hDiv, Real.exp, And.right, HAdd.hAdd, Set.mem_univ, convexOn_exp, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
n : ℕ
hn : 2 ≤ n
apply : StrictMonoOn (α := ℝ) (β := ℝ) (deriv fun (x : ℝ) ↦ x ^ n) (interior (Ici 0))
⊢ StrictConvexOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ x ^ n

Tactic:
apply StrictMonoOn.strictConvexOn_of_deriv (convex_Ici _) (continuousOn_pow _)

Premises used: StrictMonoOn.strictConvexOn_of_deriv, continuousOn_pow, convex_Ici
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
n : ℕ
hn : 2 ≤ n
simp_rw : StrictMonoOn (β := ℝ) (fun (x : ℝ) ↦ (↑n : ℝ) * x ^ (n - 1)) fun (a : ℝ) ↦ Ioi 0 a
⊢ StrictMonoOn (β := ℝ) (fun (x : ℝ) ↦ deriv (fun (x : ℝ) ↦ x ^ n) x) fun (a : ℝ) ↦ interior (fun (a : ℝ) ↦ Ici 0 a) a

Tactic:
simp_rw [deriv_pow_field, interior_Ici]

Premises used: interior_Ici, deriv_pow_field
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : 0 < x
y : ℝ
h : Membership.mem (γ := Set ℝ) (fun (a : ℝ) ↦ Ioi 0 a) y
hxy : x < y
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
n : ℕ
hn : 2 ≤ n
⊢ StrictMonoOn (β := ℝ) (fun (x : ℝ) ↦ (↑n : ℝ) * x ^ (n - 1)) fun (a : ℝ) ↦ Ioi 0 a

Tactic:
exact fun x (hx : 0 < x) y _ hxy => mul_lt_mul_of_pos_left
    (pow_lt_pow_left₀ hxy hx.le <| Nat.sub_ne_zero_of_lt hn) (by positivity)

Premises used: mul_lt_mul_of_pos_left, LT.lt.le, Nat.sub_ne_zero_of_lt, pow_lt_pow_left₀
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
n : ℕ
hn : Even n
h : n ≠ 0
apply : StrictMono (α := ℝ) (β := ℝ) (deriv fun (a : ℝ) ↦ a ^ n)
⊢ StrictConvexOn ℝ (β := ℝ) univ fun (x : ℝ) ↦ x ^ n

Tactic:
apply StrictMono.strictConvexOn_univ_of_deriv (continuous_pow n)

Premises used: StrictMono.strictConvexOn_univ_of_deriv, continuous_pow
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
n : ℕ
hn : Even n
h : n ≠ 0
simp_rw : StrictMono (β := ℝ) fun (x : ℝ) ↦ (↑n : ℝ) * x ^ (n - 1)
⊢ StrictMono (β := ℝ) fun (x : ℝ) ↦ deriv (fun (a : ℝ) ↦ a ^ n) x

Tactic:
simp_rw [deriv_pow_field]

Premises used: deriv_pow_field
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
n : ℕ
hn : Even n
h : n ≠ 0
⊢ 0 < n

Tactic:
replace h := Nat.pos_of_ne_zero h
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
n : ℕ
hn : Even n
h : 0 < n
⊢ StrictMono (β := ℝ) fun (x : ℝ) ↦ (↑n : ℝ) * x ^ (n - 1)

Tactic:
StrictMono.const_mul (Odd.strictMono_pow <| Nat.Even.sub_odd h hn <| Nat.odd_iff.2 rfl)
    (Nat.cast_pos.2 h)

Premises used: Iff.mpr, StrictMono.const_mul, Nat.cast_pos, Nat.Even.sub_odd, Odd.strictMono_pow, Nat.odd_iff, rfl
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
n : ℕ
hn : Even n
h : 0 < n
⊢ StrictMono (β := ℝ) fun (x : ℝ) ↦ (↑n : ℝ) * x ^ (n - 1)

Tactic:
exact StrictMono.const_mul (Odd.strictMono_pow <| Nat.Even.sub_odd h hn <| Nat.odd_iff.2 rfl)
    (Nat.cast_pos.2 h)

Premises used: Iff.mpr, StrictMono.const_mul, Nat.Even.sub_odd, Odd.strictMono_pow, Nat.odd_iff, rfl
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
α : Type u_1
β : Type u_2
inst : CommRing β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
f : α → β
inst_3 : DecidablePred fun (x : α) ↦ f x ≤ 0
s : Finset α
h0 : Even #({x ∈ s | f x ≤ 0})
x : α
h : x ∈ s
pos : ∀ (hx : f x ≤ 0), 0 ≤ -1 * f x
neg : ∀ (hx : ¬f x ≤ 0), 0 ≤ 1 * f x
⊢ 0 ≤ (if f x ≤ 0 then -1 else 1) * f x

Tactic:
split_ifs with hx
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
α : Type u_1
β : Type u_2
inst : CommRing β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
f : α → β
inst_3 : DecidablePred fun (x : α) ↦ f x ≤ 0
s : Finset α
h0 : Even #({x ∈ s | f x ≤ 0})
x : α
h : x ∈ s
hx : f x ≤ 0
⊢ 0 ≤ -1 * f x

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
α : Type u_1
β : Type u_2
inst : CommRing β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
f : α → β
inst_3 : DecidablePred fun (x : α) ↦ f x ≤ 0
s : Finset α
h0 : Even #({x ∈ s | f x ≤ 0})
x : α
h : x ∈ s
hx : ¬f x ≤ 0
linarith : 1 * f x < 0 → 0 - f x + (1 * f x - 0) = 0
⊢ 0 ≤ 1 * f x

Tactic:
linarith