z : ℝ
h : 0 < z
x y : ℝ≥0∞
hxy : x < y
⊢ (fun x => x ^ z) x < (fun x => x ^ z) y
z : ℝ
h : 0 < z
⊢ StrictMono fun x => x ^ z
intro x y hxy
case intro
z : ℝ
h : 0 < z
y : ℝ≥0∞
x : ℝ≥0
hxy : ↑x < y
⊢ (fun x => x ^ z) ↑x < (fun x => x ^ z) y
z : ℝ
h : 0 < z
x y : ℝ≥0∞
hxy : x < y
⊢ (fun x => x ^ z) x < (fun x => x ^ z) y
lift x to ℝ≥0 using ne_top_of_lt hxy
case intro.inl
z : ℝ
h : 0 < z
x : ℝ≥0
hxy : ↑x < ⊤
⊢ (fun x => x ^ z) ↑x < (fun x => x ^ z) ⊤

case intro.inr
z : ℝ
h : 0 < z
y : ℝ≥0∞
x : ℝ≥0
hxy : ↑x < y
hy : y ≠ ⊤
⊢ (fun x => x ^ z) ↑x < (fun x => x ^ z) y
case intro
z : ℝ
h : 0 < z
y : ℝ≥0∞
x : ℝ≥0
hxy : ↑x < y
⊢ (fun x => x ^ z) ↑x < (fun x => x ^ z) y
rcases eq_or_ne y ∞ with (rfl | hy)
no goals
case intro.inl
z : ℝ
h : 0 < z
x : ℝ≥0
hxy : ↑x < ⊤
⊢ (fun x => x ^ z) ↑x < (fun x => x ^ z) ⊤
simp only [top_rpow_of_pos h, coe_rpow_of_nonneg _ h.le, coe_lt_top]
case intro.inr.intro
z : ℝ
h : 0 < z
x y : ℝ≥0
hxy : ↑x < ↑y
⊢ (fun x => x ^ z) ↑x < (fun x => x ^ z) ↑y
case intro.inr
z : ℝ
h : 0 < z
y : ℝ≥0∞
x : ℝ≥0
hxy : ↑x < y
hy : y ≠ ⊤
⊢ (fun x => x ^ z) ↑x < (fun x => x ^ z) y
lift y to ℝ≥0 using hy
no goals
case intro.inr.intro
z : ℝ
h : 0 < z
x y : ℝ≥0
hxy : ↑x < ↑y
⊢ (fun x => x ^ z) ↑x < (fun x => x ^ z) ↑y
simp only [coe_rpow_of_nonneg _ h.le, NNReal.rpow_lt_rpow (coe_lt_coe.1 hxy) h, coe_lt_coe]