case inl
hp : 1 ≤ 1
⊢ ConvexOn ℝ (Ici 0) fun x => x ^ 1

case inr
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
⊢ ConvexOn ℝ (Ici 0) fun x => x ^ p
p : ℝ
hp : 1 ≤ p
⊢ ConvexOn ℝ (Ici 0) fun x => x ^ p
rcases eq_or_lt_of_le hp with (rfl | hp)
no goals
case inr
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
⊢ ConvexOn ℝ (Ici 0) fun x => x ^ p
exact (strictConvexOn_rpow hp).convexOn
no goals
case inl
hp : 1 ≤ 1
⊢ ConvexOn ℝ (Ici 0) fun x => x ^ 1
simpa using convexOn_id (convex_Ici _)