awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
apply : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ √x * log x) (Ioi 1)
⊢ StrictConcaveOn ℝ (β := ℝ) (Ioi 1) fun (x : ℝ) ↦ √x * log x
have apply₁ : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 1) x),
  LT.lt (α := ℝ) (deriv^[2] (fun (x : ℝ) ↦ √x * log x) x : ℝ) (0 : ℝ)
Tactic: apply strictConcaveOn_of_deriv2_neg' (convex_Ioi 1) _ fun x hx => ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 1) x
⊢ LT.lt (α := ℝ) (deriv^[2] (fun (x : ℝ) ↦ √x * log x) x : ℝ) (0 : ℝ)
have rw : -log x / (4 * HPow.hPow (β := ℕ) (√x) 3) < 0
Tactic: rw [deriv2_sqrt_mul_log x]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
⊢ StrictConcaveOn ℝ (Icc 0 π) sin
have apply : ∀ (x : ℝ) (hx : x ∈ interior (Icc 0 π)), deriv^[2] sin x < 0
Tactic: apply strictConcaveOn_of_deriv2_neg (convex_Icc _ _) continuousOn_sin fun x hx => ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (hypothesis)
Goal:
x : ℝ
hx : x ∈ interior (Icc 0 π)
⊢ deriv^[2] sin x < 0
have hx₁ : x ∈ Ioo 0 π
Tactic: rw [interior_Icc] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
⊢ StrictConcaveOn ℝ (Icc (-(π / 2)) (π / 2)) cos
have apply : ∀ (x : ℝ) (hx : x ∈ interior (Icc (-(π / 2)) (π / 2))), deriv^[2] cos x < 0
Tactic: apply strictConcaveOn_of_deriv2_neg (convex_Icc _ _) continuousOn_cos fun x hx => ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (hypothesis)
Goal:
x : ℝ
hx : x ∈ interior (Icc (-(π / 2)) (π / 2))
⊢ deriv^[2] cos x < 0
have hx₁ : x ∈ Ioo (-(π / 2)) (π / 2)
Tactic: rw [interior_Icc] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Pow (hypothesis)
Goal:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
⊢ StrictConcaveOn ℝ≥0 (β := ℝ≥0) univ fun (x : ℝ≥0) ↦ x ^ p
have hp₀' : 0 < 1 / p
Tactic: have hp₀' : 0 < 1 / p := div_pos zero_lt_one hp₀
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Pow (hypothesis)
Goal:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
⊢ StrictConcaveOn ℝ≥0 (β := ℝ≥0) univ fun (x : ℝ≥0) ↦ x ^ p
have hp₁' : 1 < 1 / p
Tactic: have hp₁' : 1 < 1 / p := by rw [one_lt_div hp₀]; exact hp₁
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Pow (goal)
Goal:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
⊢ StrictConvexOn ℝ≥0 (E := ℝ≥0) (β := ℝ≥0) univ (⇑f : (a : ℝ≥0) → ℝ≥0)
have refine : ∀ (x : ℝ≥0),
  Membership.mem (γ := Set ℝ≥0) univ x →
    ∀ (y : ℝ≥0),
      Membership.mem (γ := Set ℝ≥0) univ y →
        ∀ (hxy : x ≠ y) (a b : ℝ≥0) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1),
          (f : (a : ℝ≥0) → ℝ≥0) (a • x + b • y) <
            HSMul.hSMul (β := ℝ≥0) a ((f : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) +
              HSMul.hSMul (β := ℝ≥0) b ((f : (a : ℝ≥0) → ℝ≥0) y : ℝ≥0)
Tactic: refine ⟨convex_univ, fun x _ y _ hxy a b ha hb hab => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Pow (hypothesis)
Goal:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
⊢ StrictConcaveOn ℝ≥0 (β := ℝ≥0) univ fun (x : ℝ≥0) ↦ x ^ p
have h₁ : StrictConvexOn ℝ≥0 (E := ℝ≥0) (β := ℝ≥0) univ (⇑f : (a : ℝ≥0) → ℝ≥0)
Tactic: have h₁ : StrictConvexOn ℝ≥0 univ f := by
    refine ⟨convex_univ, fun x _ y _ hxy a b ha hb hab => ?_⟩
    exact (strictConvexOn_rpow hp₁').2 x.2 y.2 (by simp [hxy]) ha hb (by simp; norm_cast)
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Pow (hypothesis)
Goal:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
h₁ : StrictConvexOn ℝ≥0 (E := ℝ≥0) (β := ℝ≥0) univ (⇑f : (a : ℝ≥0) → ℝ≥0)
⊢ StrictConcaveOn ℝ≥0 (β := ℝ≥0) univ fun (x : ℝ≥0) ↦ x ^ p
have h₂ : ∀ (x : ℝ≥0), (f.symm : (a : ℝ≥0) → ℝ≥0) x = x ^ p
Tactic: have h₂ : ∀ x, f.symm x = x ^ p := by simp [f, NNReal.orderIsoRpow_symm_eq]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Pow (goal)
Goal:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
h₁ : StrictConvexOn ℝ≥0 (E := ℝ≥0) (β := ℝ≥0) univ (⇑f : (a : ℝ≥0) → ℝ≥0)
h₂ : ∀ (x : ℝ≥0), (f.symm : (a : ℝ≥0) → ℝ≥0) x = x ^ p
⊢ StrictConcaveOn ℝ≥0 (β := ℝ≥0) univ fun (x : ℝ≥0) ↦ x ^ p
have refine : ∀ (x : ℝ≥0) (mx : Membership.mem (γ := Set ℝ≥0) univ x) (y : ℝ≥0) (my : Membership.mem (γ := Set ℝ≥0) univ y)
  (hxy : x ≠ y) (a b : ℝ≥0) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1),
  HSMul.hSMul (β := ℝ≥0) a ((fun (x : ℝ≥0) ↦ x ^ p) x) + HSMul.hSMul (β := ℝ≥0) b ((fun (x : ℝ≥0) ↦ x ^ p) y) <
    (fun (x : ℝ≥0) ↦ x ^ p) (a • x + b • y)
Tactic: refine ⟨convex_univ, fun x mx y my hxy a b ha hb hab => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Pow (goal)
Goal:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
h₁ : StrictConvexOn ℝ≥0 (E := ℝ≥0) (β := ℝ≥0) univ (⇑f : (a : ℝ≥0) → ℝ≥0)
h₂ : ∀ (x : ℝ≥0), (f.symm : (a : ℝ≥0) → ℝ≥0) x = x ^ p
x : ℝ≥0
mx : Membership.mem (γ := Set ℝ≥0) univ x
y : ℝ≥0
my : Membership.mem (γ := Set ℝ≥0) univ y
hxy : x ≠ y
a b : ℝ≥0
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ HSMul.hSMul (β := ℝ≥0) a ((fun (x : ℝ≥0) ↦ x ^ p) x) + HSMul.hSMul (β := ℝ≥0) b ((fun (x : ℝ≥0) ↦ x ^ p) y) <
    (fun (x : ℝ≥0) ↦ x ^ p) (a • x + b • y)
have simp : HSMul.hSMul (β := ℝ≥0) a ((f.symm : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) +
    HSMul.hSMul (β := ℝ≥0) b ((f.symm : (a : ℝ≥0) → ℝ≥0) y : ℝ≥0) <
  (f.symm : (a : ℝ≥0) → ℝ≥0) (a • x + b • y)
Tactic: simp only [← h₂]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Pow (goal)
Goal:
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
⊢ ConcaveOn ℝ≥0 (β := ℝ≥0) univ fun (x : ℝ≥0) ↦ x ^ p
have inl : ∀ (hp₀ : LE.le (α := ℝ) 0 0) (hp₁ : LE.le (α := ℝ) 0 1),
  ConcaveOn ℝ≥0 (β := ℝ≥0) univ fun (x : ℝ≥0) ↦ HPow.hPow (β := ℝ) x 0
Tactic: rcases eq_or_lt_of_le hp₀ with (rfl | hp₀)
Cleared hypotheses: p, hp₀, hp₁
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Pow (goal)
Goal:
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
inl :
  ∀ (hp₀ : LE.le (α := ℝ) 0 0) (hp₁ : LE.le (α := ℝ) 0 1),
    ConcaveOn ℝ≥0 (β := ℝ≥0) univ fun (x : ℝ≥0) ↦ HPow.hPow (β := ℝ) x 0
⊢ ConcaveOn ℝ≥0 (β := ℝ≥0) univ fun (x : ℝ≥0) ↦ x ^ p
have inr : ∀ (hp₀ : 0 < p), ConcaveOn ℝ≥0 (β := ℝ≥0) univ fun (x : ℝ≥0) ↦ x ^ p
Tactic: rcases eq_or_lt_of_le hp₀ with (rfl | hp₀)
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Pow (goal)
Goal:
p : ℝ
hp₀_1 : 0 ≤ p
hp₁ : p ≤ 1
hp₀ : 0 < p
⊢ ConcaveOn ℝ≥0 (β := ℝ≥0) univ fun (x : ℝ≥0) ↦ x ^ p
have inr : ∀ (hp₀ : LE.le (α := ℝ) 0 1) (hp₁ : LE.le (α := ℝ) 1 1) (hp₀ : LT.lt (α := ℝ) 0 1),
  ConcaveOn ℝ≥0 (β := ℝ≥0) univ fun (x : ℝ≥0) ↦ HPow.hPow (β := ℝ) x 1
Tactic: rcases eq_or_lt_of_le hp₁ with (rfl | hp₁)
Cleared hypotheses: p, hp₀_1, hp₁, hp₀
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Pow (goal)
Goal:
p : ℝ
hp₀_1 : 0 ≤ p
hp₁ : p ≤ 1
hp₀ : 0 < p
inr :
  ∀ (hp₀ : LE.le (α := ℝ) 0 1) (hp₁ : LE.le (α := ℝ) 1 1) (hp₀ : LT.lt (α := ℝ) 0 1),
    ConcaveOn ℝ≥0 (β := ℝ≥0) univ fun (x : ℝ≥0) ↦ HPow.hPow (β := ℝ) x 1
⊢ ConcaveOn ℝ≥0 (β := ℝ≥0) univ fun (x : ℝ≥0) ↦ x ^ p
have inr₁ : ∀ (hp₁ : p < 1), ConcaveOn ℝ≥0 (β := ℝ≥0) univ fun (x : ℝ≥0) ↦ x ^ p
Tactic: rcases eq_or_lt_of_le hp₁ with (rfl | hp₁)
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Pow (goal)
Goal:
⊢ Eq (α := (a : ℝ≥0) → ℝ≥0) (⇑sqrt : (a : ℝ≥0) → ℝ≥0) fun (x : ℝ≥0) ↦ x ^ (1 / 2)
have h : ∀ (x : ℝ≥0), (↑((sqrt : (a : ℝ≥0) → ℝ≥0) x) : ℝ) = (↑(x ^ (1 / 2)) : ℝ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Pow (hypothesis)
Goal:
⊢ StrictConcaveOn ℝ≥0 (E := ℝ≥0) (β := ℝ≥0) univ (⇑sqrt : (a : ℝ≥0) → ℝ≥0)
have this : Eq (α := (a : ℝ≥0) → ℝ≥0) (⇑sqrt : (a : ℝ≥0) → ℝ≥0) fun (x : ℝ≥0) ↦ x ^ (1 / 2)
Tactic: have : NNReal.sqrt = fun x : ℝ≥0 ↦ x ^ (1 / (2 : ℝ)) := by
    ext x; exact mod_cast NNReal.sqrt_eq_rpow x
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Pow (goal)
Goal:
this : Eq (α := (a : ℝ≥0) → ℝ≥0) (⇑sqrt : (a : ℝ≥0) → ℝ≥0) fun (x : ℝ≥0) ↦ x ^ (1 / 2)
⊢ StrictConcaveOn ℝ≥0 (E := ℝ≥0) (β := ℝ≥0) univ (⇑sqrt : (a : ℝ≥0) → ℝ≥0)
have rw : StrictConcaveOn ℝ≥0 (β := ℝ≥0) univ fun (x : ℝ≥0) ↦ x ^ (1 / 2)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Pow (goal)
Goal:
this : Eq (α := (a : ℝ≥0) → ℝ≥0) (⇑sqrt : (a : ℝ≥0) → ℝ≥0) fun (x : ℝ≥0) ↦ x ^ (1 / 2)
⊢ 1 / 2 < 1
have linarith : 1 ≤ 1 / 2 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Pow (goal)
Goal:
this : Eq (α := (a : ℝ≥0) → ℝ≥0) (⇑sqrt : (a : ℝ≥0) → ℝ≥0) fun (x : ℝ≥0) ↦ x ^ (1 / 2)
linarith : 1 ≤ 1 / 2 → 2 / 2 = 1
⊢ 1 / 2 < 1
have linarith₁ : 1 ≤ 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Pow (goal)
Goal:
this : Eq (α := (a : ℝ≥0) → ℝ≥0) (⇑sqrt : (a : ℝ≥0) → ℝ≥0) fun (x : ℝ≥0) ↦ x ^ (1 / 2)
linarith : 1 ≤ 1 / 2 → 2 / 2 = 1
linarith₁ : 1 ≤ 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 1 / 2 < 1
have linarith₂ : 1 ≤ 1 / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Pow (goal)
Goal:
this : Eq (α := (a : ℝ≥0) → ℝ≥0) (⇑sqrt : (a : ℝ≥0) → ℝ≥0) fun (x : ℝ≥0) ↦ x ^ (1 / 2)
linarith : 1 ≤ 1 / 2 → 2 / 2 = 1
linarith₁ : 1 ≤ 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 ≤ 1 / 2 → GT.gt (α := ℝ) 2 0
⊢ 1 / 2 < 1
have linarith₃ : 1 ≤ 1 / 2 → -1 + HMul.hMul (α := ℝ) 1 1 = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Pow (goal)
Goal:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
⊢ StrictConcaveOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ x ^ p
have refine : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ici 0) x) (y : ℝ) (hy : Membership.mem (γ := Set ℝ) (Ici 0) y)
  (hxy : x ≠ y) (a b : ℝ) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1),
  HSMul.hSMul (β := ℝ) a ((fun (x : ℝ) ↦ x ^ p) x) + HSMul.hSMul (β := ℝ) b ((fun (x : ℝ) ↦ x ^ p) y) <
    (fun (x : ℝ) ↦ x ^ p) (a • x + b • y)
Tactic: refine ⟨convex_Ici _, fun x hx y hy hxy a b ha hb hab => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Pow (hypothesis)
Goal:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ici 0) y
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := NNReal.mk x hx
y' : ℝ≥0 := NNReal.mk y hy
a' : ℝ≥0 := NNReal.mk a ⋯
b' : ℝ≥0 := NNReal.mk b ⋯
⊢ HSMul.hSMul (β := ℝ) a ((fun (x : ℝ) ↦ x ^ p) x) + HSMul.hSMul (β := ℝ) b ((fun (x : ℝ) ↦ x ^ p) y) <
    (fun (x : ℝ) ↦ x ^ p) (a • x + b • y)
have hxy' : x' ≠ y'
Tactic: have hxy' : x' ≠ y' := Subtype.coe_ne_coe.1 hxy
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Pow (goal)
Goal:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ici 0) y
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := NNReal.mk x hx
y' : ℝ≥0 := NNReal.mk y hy
a' : ℝ≥0 := NNReal.mk a ⋯
b' : ℝ≥0 := NNReal.mk b ⋯
hxy' : x' ≠ y'
⊢ a' + b' = 1
have a₁ : (↑(a' + b') : ℝ) = (↑1 : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Pow (hypothesis)
Goal:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ici 0) y
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := NNReal.mk x hx
y' : ℝ≥0 := NNReal.mk y hy
a' : ℝ≥0 := NNReal.mk a ⋯
b' : ℝ≥0 := NNReal.mk b ⋯
hxy' : x' ≠ y'
⊢ HSMul.hSMul (β := ℝ) a ((fun (x : ℝ) ↦ x ^ p) x) + HSMul.hSMul (β := ℝ) b ((fun (x : ℝ) ↦ x ^ p) y) <
    (fun (x : ℝ) ↦ x ^ p) (a • x + b • y)
have hab' : a' + b' = 1
Tactic: have hab' : a' + b' = 1 := by ext; simp [a', b', hab]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Pow (goal)
Goal:
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
⊢ ConcaveOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ x ^ p
have inl : ∀ (hp₀ : LE.le (α := ℝ) 0 0) (hp₁ : LE.le (α := ℝ) 0 1),
  ConcaveOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ HPow.hPow (β := ℝ) x 0
Tactic: rcases eq_or_lt_of_le hp₀ with (rfl | hp₀)
Cleared hypotheses: p, hp₀, hp₁
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Pow (goal)
Goal:
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
inl :
  ∀ (hp₀ : LE.le (α := ℝ) 0 0) (hp₁ : LE.le (α := ℝ) 0 1),
    ConcaveOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ HPow.hPow (β := ℝ) x 0
⊢ ConcaveOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ x ^ p
have inr : ∀ (hp₀ : 0 < p), ConcaveOn ℝ (β := ℝ) (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.Pow (goal)
Goal:
p : ℝ
hp₀_1 : 0 ≤ p
hp₁ : p ≤ 1
hp₀ : 0 < p
⊢ ConcaveOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ x ^ p
have inr : ∀ (hp₀ : LE.le (α := ℝ) 0 1) (hp₁ : LE.le (α := ℝ) 1 1) (hp₀ : LT.lt (α := ℝ) 0 1),
  ConcaveOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ HPow.hPow (β := ℝ) x 1
Tactic: rcases eq_or_lt_of_le hp₁ with (rfl | hp₁)
Cleared hypotheses: p, hp₀_1, hp₁, hp₀
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Pow (goal)
Goal:
p : ℝ
hp₀_1 : 0 ≤ p
hp₁ : p ≤ 1
hp₀ : 0 < p
inr :
  ∀ (hp₀ : LE.le (α := ℝ) 0 1) (hp₁ : LE.le (α := ℝ) 1 1) (hp₀ : LT.lt (α := ℝ) 0 1),
    ConcaveOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ HPow.hPow (β := ℝ) x 1
⊢ ConcaveOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ x ^ p
have inr₁ : ∀ (hp₁ : p < 1), ConcaveOn ℝ (β := ℝ) (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.Pow (goal)
Goal:
⊢ StrictConcaveOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ √x
have rw : StrictConcaveOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ (fun (x : ℝ) ↦ x ^ (1 / 2)) x
Tactic: rw [funext Real.sqrt_eq_rpow]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Pow (goal)
Goal:
⊢ 1 / 2 < 1
have linarith : 1 ≤ 1 / 2 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Pow (goal)
Goal:
linarith : 1 ≤ 1 / 2 → 2 / 2 = 1
⊢ 1 / 2 < 1
have linarith₁ : 1 ≤ 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Pow (goal)
Goal:
linarith : 1 ≤ 1 / 2 → 2 / 2 = 1
linarith₁ : 1 ≤ 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 1 / 2 < 1
have linarith₂ : 1 ≤ 1 / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Pow (goal)
Goal:
linarith : 1 ≤ 1 / 2 → 2 / 2 = 1
linarith₁ : 1 ≤ 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 ≤ 1 / 2 → GT.gt (α := ℝ) 2 0
⊢ 1 / 2 < 1
have linarith₃ : 1 ≤ 1 / 2 → -1 + HMul.hMul (α := ℝ) 1 1 = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x : E
s : Set E
⊢ StarConvex 𝕜 x s ↔ ∀ ⦃y : E⦄, y ∈ s → [x -[𝕜] y] ⊆ s
have mp : StarConvex 𝕜 x s → ∀ ⦃y : E⦄, y ∈ s → [x -[𝕜] y] ⊆ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x : E
s : Set E
mp : StarConvex 𝕜 x s → ∀ ⦃y : E⦄, y ∈ s → [x -[𝕜] y] ⊆ s
⊢ StarConvex 𝕜 x s ↔ ∀ ⦃y : E⦄, y ∈ s → [x -[𝕜] y] ⊆ s
have mpr : (∀ ⦃y : E⦄, y ∈ s → [x -[𝕜] y] ⊆ s) → StarConvex 𝕜 x s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x : E
s : Set E
⊢ StarConvex 𝕜 x s ↔ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → HSMul.hSMul (β := Set E) a {x} + b • s ⊆ s
have fun : StarConvex 𝕜 x s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → HSMul.hSMul (β := Set E) a {x} + b • s ⊆ s
Tactic: refine
    ⟨?_, fun h y hy a b ha hb hab =>
      h ha hb hab (add_mem_add (smul_mem_smul_set <| mem_singleton _) ⟨_, hy, rfl⟩)⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x : E
ι : Sort u_4
s : ι → Set E
hs : ∀ (i : ι), StarConvex 𝕜 x (s i)
y : E
hy : Membership.mem (γ := Set E) (⋃ (i : ι), s i) y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ Membership.mem (γ := Set E) (⋃ (i : ι), s i) (a • x + b • y)
have rw : ∀ (hy : ∃ (i : ι), y ∈ s i) ⦃a b : 𝕜⦄ (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∃ (i : ι), a • x + b • y ∈ s i
Tactic: rw [mem_iUnion] at hy ⊢
Cleared hypotheses: hy, a, b, ha, hb, hab
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x : E
ι : Sort u_4
s : ι → Set E
hs : ∀ (i : ι), StarConvex 𝕜 x (s i)
y : E
hy : ∃ (i : ι), y ∈ s i
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∃ (i : ι), a • x + b • y ∈ s i
have obtain : ∀ (i : ι) (hy : y ∈ s i), ∃ (i : ι), a • x + b • y ∈ s i
Tactic: obtain ⟨i, hy⟩ := hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x : E
S : Set (Set E)
hS : ∀ s ∈ S, StarConvex 𝕜 x s
⊢ StarConvex 𝕜 x (⋃₀ S)
have rw : StarConvex 𝕜 x (⋃ (i : (↑S : Type u_2)), (↑i : Set E))
Tactic: rw [sUnion_eq_iUnion]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
inst_4 : ZeroLEOneClass 𝕜
hs : StarConvex 𝕜 x s
h : s.Nonempty
⊢ x ∈ s
have obtain : ∀ (y : E) (hy : y ∈ s), x ∈ s
Tactic: obtain ⟨y, hy⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
inst_4 : ZeroLEOneClass 𝕜
hs : StarConvex 𝕜 x s
y : E
hy : y ∈ s
⊢ x ∈ s
have h : x = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y
Tactic: convert! hs hy zero_le_one le_rfl (add_zero 1)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
inst_4 : ZeroLEOneClass 𝕜
hs : StarConvex 𝕜 x s
y : E
hy : y ∈ s
⊢ x = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y
have h : x = x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y
Tactic: rw [one_smul, zero_smul, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
inst_4 : ZeroLEOneClass 𝕜
hs : StarConvex 𝕜 x s
y : E
hy : y ∈ s
h : x = x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y
⊢ x = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y
have h₁ : x = x + 0
Tactic: rw [one_smul, zero_smul, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
inst_4 : ZeroLEOneClass 𝕜
hs : StarConvex 𝕜 x s
y : E
hy : y ∈ s
h : x = x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y
h₁ : x = x + 0
⊢ x = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y
have h₂ : x = x
Tactic: rw [one_smul, zero_smul, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
⊢ StarConvex 𝕜 x s ↔ ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
have refine : (∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s) → StarConvex 𝕜 x s
Tactic: refine ⟨fun h y hy a b ha hb hab => h hy ha.le hb.le hab, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s
have inl : ∀ (ha : LE.le.{u_1} (α := 𝕜) 0 0) (hab : 0 + b = 1), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + b • y ∈ s
Tactic: obtain rfl | ha := ha.eq_or_lt
Cleared hypotheses: a, ha, hab
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
inl : ∀ (ha : LE.le.{u_1} (α := 𝕜) 0 0) (hab : 0 + b = 1), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + b • y ∈ s
⊢ a • x + b • y ∈ s
have inr : ∀ (ha : 0 < a), a • x + b • y ∈ s
Tactic: obtain rfl | ha := ha.eq_or_lt
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
b : 𝕜
hb : 0 ≤ b
ha : LE.le.{u_1} (α := 𝕜) 0 0
hab : 0 + b = 1
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + b • y ∈ s
have hab₁ : b = 1
Tactic: rw [zero_add] at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
b : 𝕜
hb : 0 ≤ b
ha : LE.le.{u_1} (α := 𝕜) 0 0
hab : b = 1
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + b • y ∈ s
have inl : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 y ∈ s
Tactic: rwa [hab, one_smul, zero_smul, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
b : 𝕜
hb : 0 ≤ b
ha : LE.le.{u_1} (α := 𝕜) 0 0
hab : b = 1
inl : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 y ∈ s
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + b • y ∈ s
have inl₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + y ∈ s
Tactic: rwa [hab, one_smul, zero_smul, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
b : 𝕜
hb : 0 ≤ b
ha : LE.le.{u_1} (α := 𝕜) 0 0
hab : b = 1
inl : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 y ∈ s
inl₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + y ∈ s
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + b • y ∈ s
have inl₂ : 0 + y ∈ s
Tactic: rwa [hab, one_smul, zero_smul, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha_1 : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha : 0 < a
⊢ a • x + b • y ∈ s
have inr : ∀ (hb : LE.le.{u_1} (α := 𝕜) 0 0) (hab : a + 0 = 1), a • x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y ∈ s
Tactic: obtain rfl | hb := hb.eq_or_lt
Cleared hypotheses: b, hb, hab