p : ℝ
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
⊢ 0 < x ^ p
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
⊢ 0 < x ^ p
have rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p := by
  intro p hp_pos
  rw [← zero_rpow hp_pos.ne']
  exact rpow_lt_rpow hx_pos hp_pos
case inl
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
hp_pos : 0 < p
⊢ 0 < x ^ p

case inr.inl
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
⊢ 0 < x ^ 0

case inr.inr
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
hp_neg : p < 0
⊢ 0 < x ^ p
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
⊢ 0 < x ^ p
rcases lt_trichotomy (0 : ℝ) p with (hp_pos | rfl | hp_neg)
p✝ : ℝ
x : ℝ≥0
hx_pos : 0 < x
p : ℝ
hp_pos : 0 < p
⊢ 0 < x ^ p
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
⊢ ∀ {p : ℝ}, 0 < p → 0 < x ^ p
intro p hp_pos
p✝ : ℝ
x : ℝ≥0
hx_pos : 0 < x
p : ℝ
hp_pos : 0 < p
⊢ 0 ^ p < x ^ p
p✝ : ℝ
x : ℝ≥0
hx_pos : 0 < x
p : ℝ
hp_pos : 0 < p
⊢ 0 < x ^ p
rw [← zero_rpow hp_pos.ne']
no goals
p✝ : ℝ
x : ℝ≥0
hx_pos : 0 < x
p : ℝ
hp_pos : 0 < p
⊢ 0 ^ p < x ^ p
exact rpow_lt_rpow hx_pos hp_pos
no goals
case inl
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
hp_pos : 0 < p
⊢ 0 < x ^ p
exact rpow_pos_of_nonneg hp_pos
no goals
case inr.inl
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
⊢ 0 < x ^ 0
simp only [zero_lt_one, rpow_zero]
case inr.inr
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
hp_neg : p < 0
⊢ 0 < x ^ (-p)
case inr.inr
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
hp_neg : p < 0
⊢ 0 < x ^ p
rw [← neg_neg p, rpow_neg, inv_pos]
no goals
case inr.inr
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
hp_neg : p < 0
⊢ 0 < x ^ (-p)
exact rpow_pos_of_nonneg (neg_pos.mpr hp_neg)