awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 < z - y
⊢ p * y ^ (p - 1) < (z ^ p - y ^ p) / (z - y)
have rw : 1 + p * (z / y - 1) < (1 + (z / y - 1)) ^ p
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']
-- 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 < z - y
⊢ 1 + p * (z / y - 1) < (1 + (z / y - 1)) ^ p
have apply : -1 ≤ z / 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 < z - y
apply : -1 ≤ z / y - 1
⊢ 1 + p * (z / y - 1) < (1 + (z / y - 1)) ^ p
have apply₁ : z / 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 < z - y
⊢ -1 ≤ z / y - 1
have rw : 0 ≤ z ∧ 0 ≤ y ∨ z ≤ 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 < z - y
⊢ z / y - 1 ≠ 0
have rw : z / y ≠ 1
Tactic: rw [sub_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
p : ℝ
hp : 1 ≤ p
⊢ ConvexOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ x ^ p
have inl : ∀ (hp : LE.le (α := ℝ) 1 1), ConvexOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ HPow.hPow (β := ℝ) x 1
Tactic: rcases eq_or_lt_of_le hp with (rfl | hp)
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
p : ℝ
hp : 1 ≤ p
inl : ∀ (hp : LE.le (α := ℝ) 1 1), ConvexOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ HPow.hPow (β := ℝ) x 1
⊢ ConvexOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ x ^ p
have inr : ∀ (hp : 1 < p), ConvexOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ x ^ p
Tactic: rcases eq_or_lt_of_le hp with (rfl | hp)
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
b : ℝ
hb : 0 < b
⊢ ConvexOn ℝ (β := ℝ) univ fun (x : ℝ) ↦ b ^ x
have h : Eq (α := ℝ → ℝ) (fun (x : ℝ) ↦ b ^ x)
  (rexp ∘ (⇑((LinearMap.mul ℝ ℝ : (a : ℝ) → ℝ →ₗ[ℝ] ℝ) (log b) : ℝ →ₗ[ℝ] ℝ) : (a : ℝ) → ℝ))
Tactic: convert! convexOn_exp.comp_linearMap (LinearMap.mul ℝ ℝ (Real.log b)) using 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
b : ℝ
hb : 0 < b
⊢ Eq (α := ℝ → ℝ) (fun (x : ℝ) ↦ b ^ x)
    (rexp ∘ (⇑((LinearMap.mul ℝ ℝ : (a : ℝ) → ℝ →ₗ[ℝ] ℝ) (log b) : ℝ →ₗ[ℝ] ℝ) : (a : ℝ) → ℝ))
have h : ∀ (x : ℝ), b ^ x = (rexp ∘ (⇑((LinearMap.mul ℝ ℝ : (a : ℝ) → ℝ →ₗ[ℝ] ℝ) (log b) : ℝ →ₗ[ℝ] ℝ) : (a : ℝ) → ℝ)) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
⊢ StrictConcaveOn ℝ (Iio 0) log
have 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)
Tactic: refine ⟨convex_Iio _, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
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)
have 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)
Tactic: (hx : x < 0)
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
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)
have 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)
Tactic: (hy : y < 0)
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
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
have linarith : -x ≤ 0 → x - 0 + (-x - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (hypothesis)
Goal:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • log x + b • log y < log (a • x + b • y)
have hx' : 0 < -x
Tactic: have hx' : 0 < -x := by linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
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
have linarith : -y ≤ 0 → y - 0 + (-y - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (hypothesis)
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
⊢ a • log x + b • log y < log (a • x + b • y)
have hy' : 0 < -y
Tactic: have hy' : 0 < -y := by linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
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
have contrapose : ∀ (hxy : -x = -y), x = y
Tactic: contrapose hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
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
⊢ x = y
have linarith : x < y → -x - -y + (x - y) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
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
⊢ x = y
have linarith₁ : y < x → -(-x - -y) + (y - x) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (hypothesis)
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
⊢ a • log x + b • log y < log (a • x + b • y)
have hxy' : -x ≠ -y
Tactic: have hxy' : -x ≠ -y := by contrapose hxy; linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
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
⊢ log (a • -x + b • -y) = log (-(a • x + b • y))
have e_x : a • -x + b • -y = -(a • x + b • y)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
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
⊢ log (-(a • x + b • y)) = log (a • x + b • y)
have rw : log (a • x + b • y) = log (a • x + b • y)
Tactic: rw [log_neg_eq_log]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
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)
have a₁ : a • log x + b • log y = a • log (-x) + b • log (-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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
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 x + b • log y < log (a • x + b • y)
have a₂ : log (a • -x + b • -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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
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 x + b • log y < log (a • x + b • y)
have a₃ : log (-(a • x + b • 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
t : ℝ
ht : |t| ≤ 1
x : ℝ
⊢ rexp (t * x) ≤ cosh x + t * sinh x
have rw : ∀ (ht : -1 ≤ t ∧ t ≤ 1) (x : ℝ), rexp (t * x) ≤ cosh x + t * sinh x
Tactic: rw [abs_le] at ht
Cleared hypotheses: ht, x
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
t : ℝ
ht : -1 ≤ t ∧ t ≤ 1
x : ℝ
⊢ 0 ≤ (1 + t) / 2
have linarith : (1 + t) / 2 < 0 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
t : ℝ
ht : -1 ≤ t ∧ t ≤ 1
x : ℝ
linarith : (1 + t) / 2 < 0 → 2 / 2 = 1
⊢ 0 ≤ (1 + t) / 2
have linarith₁ : (1 + t) / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
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
⊢ 0 ≤ (1 + t) / 2
have linarith₂ : (1 + t) / 2 < 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
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
⊢ 0 ≤ (1 + t) / 2
have linarith₃ : (1 + t) / 2 < 0 → -1 - t + (HMul.hMul (α := ℝ) 1 1 + 1 * t - HMul.hMul (α := ℝ) 2 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
t : ℝ
ht : -1 ≤ t ∧ t ≤ 1
x : ℝ
⊢ 0 ≤ (1 - t) / 2
have linarith : (1 - t) / 2 < 0 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
t : ℝ
ht : -1 ≤ t ∧ t ≤ 1
x : ℝ
linarith : (1 - t) / 2 < 0 → 2 / 2 = 1
⊢ 0 ≤ (1 - t) / 2
have linarith₁ : (1 - t) / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
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
⊢ 0 ≤ (1 - t) / 2
have linarith₂ : (1 - t) / 2 < 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
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
⊢ 0 ≤ (1 - t) / 2
have linarith₃ : (1 - t) / 2 < 0 → t - 1 + (HMul.hMul (α := ℝ) 1 1 - 1 * t - HMul.hMul (α := ℝ) 2 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
t : ℝ
ht : -1 ≤ t ∧ t ≤ 1
x : ℝ
⊢ (1 + t) / 2 * rexp x + (1 - t) / 2 * rexp (-x) = cosh x + t * sinh x
have rw : (1 + t) / 2 * rexp x + (1 - t) / 2 * rexp (-x) = (rexp x + rexp (-x)) / 2 + t * ((rexp x - rexp (-x)) / 2)
Tactic: rw [cosh_eq, sinh_eq]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
t : ℝ
ht : -1 ≤ t ∧ t ≤ 1
x : ℝ
⊢ rexp (t * x) ≤ cosh x + t * sinh x
have _ : rexp (t * x) = rexp ((1 + t) / 2 * x + (1 - t) / 2 * -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
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Basic (goal)
Goal:
t : ℝ
ht : -1 ≤ t ∧ t ≤ 1
x : ℝ
_ : rexp (t * x) = rexp ((1 + t) / 2 * x + (1 - t) / 2 * -x)
⊢ rexp (t * x) ≤ cosh x + t * sinh x
have _₁ : (1 + t) / 2 * rexp x + (1 - t) / 2 * rexp (-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
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
n : ℕ
hn : 2 ≤ n
⊢ StrictConvexOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ x ^ n
have apply : StrictMonoOn (α := ℝ) (β := ℝ) (deriv fun (x : ℝ) ↦ x ^ n) (interior (Ici 0))
Tactic: apply StrictMonoOn.strictConvexOn_of_deriv (convex_Ici _) (continuousOn_pow _)
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
n : ℕ
hn : 2 ≤ n
⊢ StrictMonoOn (β := ℝ) (fun (x : ℝ) ↦ deriv (fun (x : ℝ) ↦ x ^ n) x) fun (a : ℝ) ↦ interior (fun (a : ℝ) ↦ Ici 0 a) a
have simp_rw : StrictMonoOn (β := ℝ) (fun (x : ℝ) ↦ (↑n : ℝ) * x ^ (n - 1)) fun (a : ℝ) ↦ Ioi 0 a
Tactic: simp_rw [deriv_pow_field, interior_Ici]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
n : ℕ
hn : Even n
h : n ≠ 0
⊢ StrictConvexOn ℝ (β := ℝ) univ fun (x : ℝ) ↦ x ^ n
have apply : StrictMono (α := ℝ) (β := ℝ) (deriv fun (a : ℝ) ↦ a ^ n)
Tactic: apply StrictMono.strictConvexOn_univ_of_deriv (continuous_pow n)
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
n : ℕ
hn : Even n
h : n ≠ 0
⊢ StrictMono (β := ℝ) fun (x : ℝ) ↦ deriv (fun (a : ℝ) ↦ a ^ n) x
have simp_rw : StrictMono (β := ℝ) fun (x : ℝ) ↦ (↑n : ℝ) * x ^ (n - 1)
Tactic: simp_rw [deriv_pow_field]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (hypothesis)
Goal:
n : ℕ
hn : Even n
h : n ≠ 0
⊢ StrictMono (β := ℝ) fun (x : ℝ) ↦ (↑n : ℝ) * x ^ (n - 1)
have h₁ : 0 < n
Tactic: replace h := Nat.pos_of_ne_zero h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
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
⊢ 0 ≤ (if f x ≤ 0 then -1 else 1) * f x
have pos : ∀ (hx : f x ≤ 0), 0 ≤ -1 * f x
Tactic: split_ifs with hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
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
⊢ 0 ≤ (if f x ≤ 0 then -1 else 1) * f x
have neg : ∀ (hx : ¬f x ≤ 0), 0 ≤ 1 * f x
Tactic: split_ifs with hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
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
have linarith : 1 * f x < 0 → 0 - f x + (1 * f x - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
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})
⊢ Eq.{u_2 + 1} (α := β) (∏ x ∈ s, (if f x ≤ 0 then -1 else 1) * f x) (∏ x ∈ s, f x)
have rw : HMul.hMul (α := β) (∏ x ∈ s, if f x ≤ 0 then -1 else 1) (∏ x ∈ s, f x) = ∏ x ∈ s, f x
Tactic: rw [Finset.prod_mul_distrib, Finset.prod_ite, Finset.prod_const_one, mul_one,
        Finset.prod_const, neg_one_pow_eq_pow_mod_two, Nat.even_iff.1 h0, pow_zero, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
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})
rw : HMul.hMul (α := β) (∏ x ∈ s, if f x ≤ 0 then -1 else 1) (∏ x ∈ s, f x) = ∏ x ∈ s, f x
⊢ Eq.{u_2 + 1} (α := β) (∏ x ∈ s, (if f x ≤ 0 then -1 else 1) * f x) (∏ x ∈ s, f x)
have rw₁ : HMul.hMul (α := β) (∏ x ∈ s with f x ≤ 0, -1) (∏ x ∈ s with ¬f x ≤ 0, 1) * ∏ x ∈ s, f x = ∏ x ∈ s, f x
Tactic: rw [Finset.prod_mul_distrib, Finset.prod_ite, Finset.prod_const_one, mul_one,
        Finset.prod_const, neg_one_pow_eq_pow_mod_two, Nat.even_iff.1 h0, pow_zero, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
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})
rw : HMul.hMul (α := β) (∏ x ∈ s, if f x ≤ 0 then -1 else 1) (∏ x ∈ s, f x) = ∏ x ∈ s, f x
rw₁ : HMul.hMul (α := β) (∏ x ∈ s with f x ≤ 0, -1) (∏ x ∈ s with ¬f x ≤ 0, 1) * ∏ x ∈ s, f x = ∏ x ∈ s, f x
⊢ Eq.{u_2 + 1} (α := β) (∏ x ∈ s, (if f x ≤ 0 then -1 else 1) * f x) (∏ x ∈ s, f x)
have rw₂ : HMul.hMul (α := β) (∏ x ∈ s with f x ≤ 0, -1) 1 * ∏ x ∈ s, f x = ∏ x ∈ s, f x
Tactic: rw [Finset.prod_mul_distrib, Finset.prod_ite, Finset.prod_const_one, mul_one,
        Finset.prod_const, neg_one_pow_eq_pow_mod_two, Nat.even_iff.1 h0, pow_zero, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
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})
rw : HMul.hMul (α := β) (∏ x ∈ s, if f x ≤ 0 then -1 else 1) (∏ x ∈ s, f x) = ∏ x ∈ s, f x
rw₁ : HMul.hMul (α := β) (∏ x ∈ s with f x ≤ 0, -1) (∏ x ∈ s with ¬f x ≤ 0, 1) * ∏ x ∈ s, f x = ∏ x ∈ s, f x
rw₂ : HMul.hMul (α := β) (∏ x ∈ s with f x ≤ 0, -1) 1 * ∏ x ∈ s, f x = ∏ x ∈ s, f x
⊢ Eq.{u_2 + 1} (α := β) (∏ x ∈ s, (if f x ≤ 0 then -1 else 1) * f x) (∏ x ∈ s, f x)
have rw₃ : HMul.hMul (α := β) (∏ x ∈ s with f x ≤ 0, -1) (∏ x ∈ s, f x) = ∏ x ∈ s, f x
Tactic: rw [Finset.prod_mul_distrib, Finset.prod_ite, Finset.prod_const_one, mul_one,
        Finset.prod_const, neg_one_pow_eq_pow_mod_two, Nat.even_iff.1 h0, pow_zero, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
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})
rw : HMul.hMul (α := β) (∏ x ∈ s, if f x ≤ 0 then -1 else 1) (∏ x ∈ s, f x) = ∏ x ∈ s, f x
rw₁ : HMul.hMul (α := β) (∏ x ∈ s with f x ≤ 0, -1) (∏ x ∈ s with ¬f x ≤ 0, 1) * ∏ x ∈ s, f x = ∏ x ∈ s, f x
rw₂ : HMul.hMul (α := β) (∏ x ∈ s with f x ≤ 0, -1) 1 * ∏ x ∈ s, f x = ∏ x ∈ s, f x
rw₃ : HMul.hMul (α := β) (∏ x ∈ s with f x ≤ 0, -1) (∏ x ∈ s, f x) = ∏ x ∈ s, f x
⊢ Eq.{u_2 + 1} (α := β) (∏ x ∈ s, (if f x ≤ 0 then -1 else 1) * f x) (∏ x ∈ s, f x)
have rw₄ : HPow.hPow (α := β) (-1) #({x ∈ s | f x ≤ 0}) * ∏ x ∈ s, f x = ∏ x ∈ s, f x
Tactic: rw [Finset.prod_mul_distrib, Finset.prod_ite, Finset.prod_const_one, mul_one,
        Finset.prod_const, neg_one_pow_eq_pow_mod_two, Nat.even_iff.1 h0, pow_zero, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
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})
rw : HMul.hMul (α := β) (∏ x ∈ s, if f x ≤ 0 then -1 else 1) (∏ x ∈ s, f x) = ∏ x ∈ s, f x
rw₁ : HMul.hMul (α := β) (∏ x ∈ s with f x ≤ 0, -1) (∏ x ∈ s with ¬f x ≤ 0, 1) * ∏ x ∈ s, f x = ∏ x ∈ s, f x
rw₂ : HMul.hMul (α := β) (∏ x ∈ s with f x ≤ 0, -1) 1 * ∏ x ∈ s, f x = ∏ x ∈ s, f x
rw₃ : HMul.hMul (α := β) (∏ x ∈ s with f x ≤ 0, -1) (∏ x ∈ s, f x) = ∏ x ∈ s, f x
rw₄ : HPow.hPow (α := β) (-1) #({x ∈ s | f x ≤ 0}) * ∏ x ∈ s, f x = ∏ x ∈ s, f x
⊢ Eq.{u_2 + 1} (α := β) (∏ x ∈ s, (if f x ≤ 0 then -1 else 1) * f x) (∏ x ∈ s, f x)
have rw₅ : HPow.hPow (α := β) (-1) (#({x ∈ s | f x ≤ 0}) % 2) * ∏ x ∈ s, f x = ∏ x ∈ s, f x
Tactic: rw [Finset.prod_mul_distrib, Finset.prod_ite, Finset.prod_const_one, mul_one,
        Finset.prod_const, neg_one_pow_eq_pow_mod_two, Nat.even_iff.1 h0, pow_zero, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
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})
rw : HMul.hMul (α := β) (∏ x ∈ s, if f x ≤ 0 then -1 else 1) (∏ x ∈ s, f x) = ∏ x ∈ s, f x
rw₁ : HMul.hMul (α := β) (∏ x ∈ s with f x ≤ 0, -1) (∏ x ∈ s with ¬f x ≤ 0, 1) * ∏ x ∈ s, f x = ∏ x ∈ s, f x
rw₂ : HMul.hMul (α := β) (∏ x ∈ s with f x ≤ 0, -1) 1 * ∏ x ∈ s, f x = ∏ x ∈ s, f x
rw₃ : HMul.hMul (α := β) (∏ x ∈ s with f x ≤ 0, -1) (∏ x ∈ s, f x) = ∏ x ∈ s, f x
rw₄ : HPow.hPow (α := β) (-1) #({x ∈ s | f x ≤ 0}) * ∏ x ∈ s, f x = ∏ x ∈ s, f x
rw₅ : HPow.hPow (α := β) (-1) (#({x ∈ s | f x ≤ 0}) % 2) * ∏ x ∈ s, f x = ∏ x ∈ s, f x
⊢ Eq.{u_2 + 1} (α := β) (∏ x ∈ s, (if f x ≤ 0 then -1 else 1) * f x) (∏ x ∈ s, f x)
have rw₆ : HPow.hPow (α := β) (β := ℕ) (-1) 0 * ∏ x ∈ s, f x = ∏ x ∈ s, f x
Tactic: rw [Finset.prod_mul_distrib, Finset.prod_ite, Finset.prod_const_one, mul_one,
        Finset.prod_const, neg_one_pow_eq_pow_mod_two, Nat.even_iff.1 h0, pow_zero, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
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})
rw : HMul.hMul (α := β) (∏ x ∈ s, if f x ≤ 0 then -1 else 1) (∏ x ∈ s, f x) = ∏ x ∈ s, f x
rw₁ : HMul.hMul (α := β) (∏ x ∈ s with f x ≤ 0, -1) (∏ x ∈ s with ¬f x ≤ 0, 1) * ∏ x ∈ s, f x = ∏ x ∈ s, f x
rw₂ : HMul.hMul (α := β) (∏ x ∈ s with f x ≤ 0, -1) 1 * ∏ x ∈ s, f x = ∏ x ∈ s, f x
rw₃ : HMul.hMul (α := β) (∏ x ∈ s with f x ≤ 0, -1) (∏ x ∈ s, f x) = ∏ x ∈ s, f x
rw₄ : HPow.hPow (α := β) (-1) #({x ∈ s | f x ≤ 0}) * ∏ x ∈ s, f x = ∏ x ∈ s, f x
rw₅ : HPow.hPow (α := β) (-1) (#({x ∈ s | f x ≤ 0}) % 2) * ∏ x ∈ s, f x = ∏ x ∈ s, f x
rw₆ : HPow.hPow (α := β) (β := ℕ) (-1) 0 * ∏ x ∈ s, f x = ∏ x ∈ s, f x
⊢ Eq.{u_2 + 1} (α := β) (∏ x ∈ s, (if f x ≤ 0 then -1 else 1) * f x) (∏ x ∈ s, f x)
have rw₇ : HMul.hMul (α := β) 1 (∏ x ∈ s, f x) = ∏ x ∈ s, f x
Tactic: rw [Finset.prod_mul_distrib, Finset.prod_ite, Finset.prod_const_one, mul_one,
        Finset.prod_const, neg_one_pow_eq_pow_mod_two, Nat.even_iff.1 h0, pow_zero, one_mul]