[GOAL]
x : ℝ≥0
y : ℝ
⊢ x ^ y = 0 ↔ x = 0 ∧ y ≠ 0
[PROOFSTEP]
rw [← NNReal.coe_eq, coe_rpow, ← NNReal.coe_eq_zero]
[GOAL]
x : ℝ≥0
y : ℝ
⊢ ↑x ^ y = ↑0 ↔ ↑x = 0 ∧ y ≠ 0
[PROOFSTEP]
exact Real.rpow_eq_zero_iff_of_nonneg x.2
[GOAL]
x : ℝ≥0
⊢ x ^ (-1) = x⁻¹
[PROOFSTEP]
simp [rpow_neg]
[GOAL]
y : ℝ
hy : y ≠ 0
x : ℝ≥0
⊢ (x ^ y) ^ (1 / y) = x
[PROOFSTEP]
field_simp [← rpow_mul]
[GOAL]
y : ℝ
hy : y ≠ 0
x : ℝ≥0
⊢ (x ^ (1 / y)) ^ y = x
[PROOFSTEP]
field_simp [← rpow_mul]
[GOAL]
x : ℝ≥0
⊢ ↑sqrt x = x ^ (1 / 2)
[PROOFSTEP]
refine' NNReal.eq _
[GOAL]
x : ℝ≥0
⊢ ↑(↑sqrt x) = ↑(x ^ (1 / 2))
[PROOFSTEP]
push_cast
[GOAL]
x : ℝ≥0
⊢ Real.sqrt ↑x = ↑x ^ (1 / 2)
[PROOFSTEP]
exact Real.sqrt_eq_rpow x.1
[GOAL]
x : ℝ≥0
n : ℕ
⊢ ↑(x ^ ↑n) = ↑(x ^ n)
[PROOFSTEP]
simpa only [coe_rpow, coe_pow] using Real.rpow_nat_cast x n
[GOAL]
x : ℝ≥0
⊢ x ^ 2 = x ^ 2
[PROOFSTEP]
rw [← rpow_nat_cast]
[GOAL]
x : ℝ≥0
⊢ x ^ 2 = x ^ ↑2
[PROOFSTEP]
simp only [Nat.cast_ofNat]
[GOAL]
ι : Type u_1
l : List ι
f : ι → ℝ≥0
r : ℝ
⊢ List.prod (List.map (fun x => f x ^ r) l) = List.prod (List.map f l) ^ r
[PROOFSTEP]
rw [← list_prod_map_rpow, List.map_map]
[GOAL]
ι : Type u_1
l : List ι
f : ι → ℝ≥0
r : ℝ
⊢ List.prod (List.map (fun x => f x ^ r) l) = List.prod (List.map ((fun x => x ^ r) ∘ f) l)
[PROOFSTEP]
rfl
[GOAL]
l : List ℝ
hl : ∀ (x : ℝ), x ∈ l → 0 ≤ x
r : ℝ
⊢ List.prod (List.map (fun x => x ^ r) l) = List.prod l ^ r
[PROOFSTEP]
lift l to List ℝ≥0 using hl
[GOAL]
case intro
r : ℝ
l : List ℝ≥0
⊢ List.prod (List.map (fun x => x ^ r) (List.map toReal l)) = List.prod (List.map toReal l) ^ r
[PROOFSTEP]
have := congr_arg ((↑) : ℝ≥0 → ℝ) (NNReal.list_prod_map_rpow l r)
[GOAL]
case intro
r : ℝ
l : List ℝ≥0
this : ↑(List.prod (List.map (fun x => x ^ r) l)) = ↑(List.prod l ^ r)
⊢ List.prod (List.map (fun x => x ^ r) (List.map toReal l)) = List.prod (List.map toReal l) ^ r
[PROOFSTEP]
push_cast at this
[GOAL]
case intro
r : ℝ
l : List ℝ≥0
this : List.prod (List.map toReal (List.map (fun x => x ^ r) l)) = List.prod (List.map toReal l) ^ r
⊢ List.prod (List.map (fun x => x ^ r) (List.map toReal l)) = List.prod (List.map toReal l) ^ r
[PROOFSTEP]
rw [List.map_map] at this ⊢
[GOAL]
case intro
r : ℝ
l : List ℝ≥0
this : List.prod (List.map (toReal ∘ fun x => x ^ r) l) = List.prod (List.map toReal l) ^ r
⊢ List.prod (List.map ((fun x => x ^ r) ∘ toReal) l) = List.prod (List.map toReal l) ^ r
[PROOFSTEP]
exact_mod_cast this
[GOAL]
ι : Type u_1
l : List ι
f : ι → ℝ
hl : ∀ (i : ι), i ∈ l → 0 ≤ f i
r : ℝ
⊢ List.prod (List.map (fun x => f x ^ r) l) = List.prod (List.map f l) ^ r
[PROOFSTEP]
rw [← Real.list_prod_map_rpow (l.map f) _ r, List.map_map]
[GOAL]
ι : Type u_1
l : List ι
f : ι → ℝ
hl : ∀ (i : ι), i ∈ l → 0 ≤ f i
r : ℝ
⊢ List.prod (List.map (fun x => f x ^ r) l) = List.prod (List.map ((fun x => x ^ r) ∘ f) l)
ι : Type u_1 l : List ι f : ι → ℝ hl : ∀ (i : ι), i ∈ l → 0 ≤ f i r : ℝ ⊢ ∀ (x : ℝ), x ∈ List.map f l → 0 ≤ x
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
l : List ι
f : ι → ℝ
hl : ∀ (i : ι), i ∈ l → 0 ≤ f i
r : ℝ
⊢ ∀ (x : ℝ), x ∈ List.map f l → 0 ≤ x
[PROOFSTEP]
simpa using hl
[GOAL]
ι : Type u_1
s : Multiset ι
f : ι → ℝ
hs : ∀ (i : ι), i ∈ s → 0 ≤ f i
r : ℝ
⊢ Multiset.prod (Multiset.map (fun x => f x ^ r) s) = Multiset.prod (Multiset.map f s) ^ r
[PROOFSTEP]
induction' s using Quotient.inductionOn with l
[GOAL]
case h
ι : Type u_1
s : Multiset ι
f : ι → ℝ
hs✝ : ∀ (i : ι), i ∈ s → 0 ≤ f i
r : ℝ
l : List ι
hs : ∀ (i : ι), i ∈ Quotient.mk (List.isSetoid ι) l → 0 ≤ f i
⊢ Multiset.prod (Multiset.map (fun x => f x ^ r) (Quotient.mk (List.isSetoid ι) l)) =
    Multiset.prod (Multiset.map f (Quotient.mk (List.isSetoid ι) l)) ^ r
[PROOFSTEP]
simpa using Real.list_prod_map_rpow' l f hs r
[GOAL]
x y : ℝ≥0
z : ℝ
hz : 0 < z
⊢ x ≤ y ^ (1 / z) ↔ x ^ z ≤ y
[PROOFSTEP]
rw [← rpow_le_rpow_iff hz, rpow_self_rpow_inv hz.ne']
[GOAL]
x y : ℝ≥0
z : ℝ
hz : 0 < z
⊢ x ^ (1 / z) ≤ y ↔ x ≤ y ^ z
[PROOFSTEP]
rw [← rpow_le_rpow_iff hz, rpow_self_rpow_inv hz.ne']
[GOAL]
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
⊢ 0 < x ^ p
[PROOFSTEP]
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
[GOAL]
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
⊢ ∀ {p : ℝ}, 0 < p → 0 < x ^ p
[PROOFSTEP]
intro p hp_pos
[GOAL]
p✝ : ℝ
x : ℝ≥0
hx_pos : 0 < x
p : ℝ
hp_pos : 0 < p
⊢ 0 < x ^ p
[PROOFSTEP]
rw [← zero_rpow hp_pos.ne']
[GOAL]
p✝ : ℝ
x : ℝ≥0
hx_pos : 0 < x
p : ℝ
hp_pos : 0 < p
⊢ 0 ^ p < x ^ p
[PROOFSTEP]
exact rpow_lt_rpow hx_pos hp_pos
[GOAL]
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
⊢ 0 < x ^ p
[PROOFSTEP]
rcases lt_trichotomy (0 : ℝ) p with (hp_pos | rfl | hp_neg)
[GOAL]
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
[PROOFSTEP]
exact rpow_pos_of_nonneg hp_pos
[GOAL]
case inr.inl
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
⊢ 0 < x ^ 0
[PROOFSTEP]
simp only [zero_lt_one, rpow_zero]
[GOAL]
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
[PROOFSTEP]
rw [← neg_neg p, rpow_neg, inv_pos]
[GOAL]
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)
[PROOFSTEP]
exact rpow_pos_of_nonneg (neg_pos.mpr hp_neg)
[GOAL]
x : ℝ≥0
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
⊢ x ^ z ≤ x
[PROOFSTEP]
rcases eq_bot_or_bot_lt x with (rfl | (h : 0 < x))
[GOAL]
case inl
z : ℝ
h_one_le : 1 ≤ z
hx : ⊥ ≤ 1
⊢ ⊥ ^ z ≤ ⊥
[PROOFSTEP]
have : z ≠ 0 := by linarith
[GOAL]
z : ℝ
h_one_le : 1 ≤ z
hx : ⊥ ≤ 1
⊢ z ≠ 0
[PROOFSTEP]
linarith
[GOAL]
case inl
z : ℝ
h_one_le : 1 ≤ z
hx : ⊥ ≤ 1
this : z ≠ 0
⊢ ⊥ ^ z ≤ ⊥
[PROOFSTEP]
simp [this]
[GOAL]
case inr
x : ℝ≥0
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
h : 0 < x
⊢ x ^ z ≤ x
[PROOFSTEP]
nth_rw 2 [← NNReal.rpow_one x]
[GOAL]
case inr
x : ℝ≥0
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
h : 0 < x
⊢ x ^ z ≤ x ^ 1
[PROOFSTEP]
exact NNReal.rpow_le_rpow_of_exponent_ge h hx h_one_le
[GOAL]
x : ℝ
hx : x ≠ 0
y z : ℝ≥0
hyz : (fun y => y ^ x) y = (fun y => y ^ x) z
⊢ y = z
[PROOFSTEP]
simpa only [rpow_inv_rpow_self hx] using congr_arg (fun y => y ^ (1 / x)) hyz
[GOAL]
x : ℝ
hx : x ≠ 0
y : ℝ≥0
⊢ (fun y => y ^ x) (y ^ x⁻¹) = y
[PROOFSTEP]
simp_rw [← rpow_mul, _root_.inv_mul_cancel hx, rpow_one]
[GOAL]
x y : ℝ≥0
z : ℝ
hz : z ≠ 0
⊢ x = y ^ (1 / z) ↔ x ^ z = y
[PROOFSTEP]
rw [← rpow_eq_rpow_iff hz, rpow_self_rpow_inv hz]
[GOAL]
x y : ℝ≥0
z : ℝ
hz : z ≠ 0
⊢ x ^ (1 / z) = y ↔ x = y ^ z
[PROOFSTEP]
rw [← rpow_eq_rpow_iff hz, rpow_self_rpow_inv hz]
[GOAL]
x : ℝ≥0
n : ℕ
hn : n ≠ 0
⊢ (x ^ n) ^ (↑n)⁻¹ = x
[PROOFSTEP]
rw [← NNReal.coe_eq, coe_rpow, NNReal.coe_pow]
[GOAL]
x : ℝ≥0
n : ℕ
hn : n ≠ 0
⊢ (↑x ^ n) ^ (↑n)⁻¹ = ↑x
[PROOFSTEP]
exact Real.pow_nat_rpow_nat_inv x.2 hn
[GOAL]
x : ℝ≥0
n : ℕ
hn : n ≠ 0
⊢ (x ^ (↑n)⁻¹) ^ n = x
[PROOFSTEP]
rw [← NNReal.coe_eq, NNReal.coe_pow, coe_rpow]
[GOAL]
x : ℝ≥0
n : ℕ
hn : n ≠ 0
⊢ (↑x ^ (↑n)⁻¹) ^ n = ↑x
[PROOFSTEP]
exact Real.rpow_nat_inv_pow_nat x.2 hn
[GOAL]
x y : ℝ
hx : 0 ≤ x
⊢ toNNReal (x ^ y) = toNNReal x ^ y
[PROOFSTEP]
nth_rw 1 [← Real.coe_toNNReal x hx]
[GOAL]
x y : ℝ
hx : 0 ≤ x
⊢ toNNReal (↑(toNNReal x) ^ y) = toNNReal x ^ y
[PROOFSTEP]
rw [← NNReal.coe_rpow, Real.toNNReal_coe]
[GOAL]
z : ℝ
h : 0 < z
x y : ℝ≥0
hxy : x < y
⊢ (fun x => x ^ z) x < (fun x => x ^ z) y
[PROOFSTEP]
simp only [NNReal.rpow_lt_rpow hxy h, coe_lt_coe]
[GOAL]
z : ℝ
h : 0 ≤ z
h0 : 0 = z
⊢ Monotone fun x => x ^ 0
[PROOFSTEP]
simp only [rpow_zero, monotone_const]
[GOAL]
y : ℝ
hy : 0 < y
x : ℝ≥0
⊢ (fun x => x ^ y) ((fun x => x ^ (1 / y)) x) = x
[PROOFSTEP]
dsimp
[GOAL]
y : ℝ
hy : 0 < y
x : ℝ≥0
⊢ (x ^ (1 / y)) ^ y = x
[PROOFSTEP]
rw [← rpow_mul, one_div_mul_cancel hy.ne.symm, rpow_one]
[GOAL]
y : ℝ
hy : 0 < y
⊢ OrderIso.symm (orderIsoRpow y hy) = orderIsoRpow (1 / y) (_ : 0 < 1 / y)
[PROOFSTEP]
simp only [orderIsoRpow, one_div_one_div]
[GOAL]
y : ℝ
hy : 0 < y
⊢ OrderIso.symm
      (StrictMono.orderIsoOfRightInverse (fun x => x ^ y) (_ : StrictMono fun x => x ^ y) (fun x => x ^ (1 / y))
        (_ : ∀ (x : ℝ≥0), (fun x => x ^ y) ((fun x => x ^ (1 / y)) x) = x)) =
    StrictMono.orderIsoOfRightInverse (fun x => x ^ (1 / y)) (_ : StrictMono fun x => x ^ (1 / y)) (fun x => x ^ y)
      (_ : Function.RightInverse (fun x => x ^ y) fun x => x ^ (1 / y))
[PROOFSTEP]
rfl
[GOAL]
x : ℝ≥0∞
⊢ x ^ 0 = 1
[PROOFSTEP]
cases x
[GOAL]
case none
⊢ none ^ 0 = 1
[PROOFSTEP]
dsimp only [(· ^ ·), Pow.pow, rpow]
[GOAL]
case none
⊢ (if 0 < 0 then ⊤ else if 0 = 0 then 1 else 0) = 1
[PROOFSTEP]
simp [lt_irrefl]
[GOAL]
case some
val✝ : ℝ≥0
⊢ Option.some val✝ ^ 0 = 1
[PROOFSTEP]
dsimp only [(· ^ ·), Pow.pow, rpow]
[GOAL]
case some
val✝ : ℝ≥0
⊢ (if val✝ = 0 ∧ 0 < 0 then ⊤ else ↑(NNReal.rpow val✝ 0)) = 1
[PROOFSTEP]
simp [lt_irrefl]
[GOAL]
y : ℝ
h : 0 < y
⊢ ⊤ ^ y = ⊤
[PROOFSTEP]
simp [top_rpow_def, h]
[GOAL]
y : ℝ
h : y < 0
⊢ ⊤ ^ y = 0
[PROOFSTEP]
simp [top_rpow_def, asymm h, ne_of_lt h]
[GOAL]
y : ℝ
h : 0 < y
⊢ 0 ^ y = 0
[PROOFSTEP]
rw [← ENNReal.coe_zero, ← ENNReal.some_eq_coe]
[GOAL]
y : ℝ
h : 0 < y
⊢ Option.some 0 ^ y = Option.some 0
[PROOFSTEP]
dsimp only [(· ^ ·), rpow, Pow.pow]
[GOAL]
y : ℝ
h : 0 < y
⊢ (if 0 = 0 ∧ y < 0 then ⊤ else ↑(NNReal.rpow 0 y)) = Option.some 0
[PROOFSTEP]
simp [h, asymm h, ne_of_gt h]
[GOAL]
y : ℝ
h : y < 0
⊢ 0 ^ y = ⊤
[PROOFSTEP]
rw [← ENNReal.coe_zero, ← ENNReal.some_eq_coe]
[GOAL]
y : ℝ
h : y < 0
⊢ Option.some 0 ^ y = ⊤
[PROOFSTEP]
dsimp only [(· ^ ·), rpow, Pow.pow]
[GOAL]
y : ℝ
h : y < 0
⊢ (if 0 = 0 ∧ y < 0 then ⊤ else ↑(NNReal.rpow 0 y)) = ⊤
[PROOFSTEP]
simp [h, ne_of_gt h]
[GOAL]
y : ℝ
⊢ 0 ^ y = if 0 < y then 0 else if y = 0 then 1 else ⊤
[PROOFSTEP]
rcases lt_trichotomy (0 : ℝ) y with (H | rfl | H)
[GOAL]
case inl
y : ℝ
H : 0 < y
⊢ 0 ^ y = if 0 < y then 0 else if y = 0 then 1 else ⊤
[PROOFSTEP]
simp [H, ne_of_gt, zero_rpow_of_pos, lt_irrefl]
[GOAL]
case inr.inl
⊢ 0 ^ 0 = if 0 < 0 then 0 else if 0 = 0 then 1 else ⊤
[PROOFSTEP]
simp [lt_irrefl]
[GOAL]
case inr.inr
y : ℝ
H : y < 0
⊢ 0 ^ y = if 0 < y then 0 else if y = 0 then 1 else ⊤
[PROOFSTEP]
simp [H, asymm H, ne_of_lt, zero_rpow_of_neg]
[GOAL]
y : ℝ
⊢ 0 ^ y * 0 ^ y = 0 ^ y
[PROOFSTEP]
rw [zero_rpow_def]
[GOAL]
y : ℝ
⊢ ((if 0 < y then 0 else if y = 0 then 1 else ⊤) * if 0 < y then 0 else if y = 0 then 1 else ⊤) =
    if 0 < y then 0 else if y = 0 then 1 else ⊤
[PROOFSTEP]
split_ifs
[GOAL]
case pos
y : ℝ
h✝ : 0 < y
⊢ 0 * 0 = 0
case pos
y : ℝ
h✝¹ : ¬0 < y
h✝ : y = 0
⊢ 1 * 1 = 1
case neg y : ℝ h✝¹ : ¬0 < y h✝ : ¬y = 0 ⊢ ⊤ * ⊤ = ⊤
[PROOFSTEP]
exacts [zero_mul _, one_mul _, top_mul_top]
[GOAL]
x : ℝ≥0
h : x ≠ 0
y : ℝ
⊢ ↑x ^ y = ↑(x ^ y)
[PROOFSTEP]
rw [← ENNReal.some_eq_coe]
[GOAL]
x : ℝ≥0
h : x ≠ 0
y : ℝ
⊢ Option.some x ^ y = ↑(x ^ y)
[PROOFSTEP]
dsimp only [(· ^ ·), Pow.pow, rpow]
[GOAL]
x : ℝ≥0
h : x ≠ 0
y : ℝ
⊢ (if x = 0 ∧ y < 0 then ⊤ else ↑(NNReal.rpow x y)) = ↑(NNReal.rpow x y)
[PROOFSTEP]
simp [h]
[GOAL]
x : ℝ≥0
y : ℝ
h : 0 ≤ y
⊢ ↑x ^ y = ↑(x ^ y)
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : x = 0
⊢ ↑x ^ y = ↑(x ^ y)
[PROOFSTEP]
rcases le_iff_eq_or_lt.1 h with (H | H)
[GOAL]
case pos.inl
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : x = 0
H : 0 = y
⊢ ↑x ^ y = ↑(x ^ y)
[PROOFSTEP]
simp [hx, H.symm]
[GOAL]
case pos.inr
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : x = 0
H : 0 < y
⊢ ↑x ^ y = ↑(x ^ y)
[PROOFSTEP]
simp [hx, zero_rpow_of_pos H, NNReal.zero_rpow (ne_of_gt H)]
[GOAL]
case neg
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : ¬x = 0
⊢ ↑x ^ y = ↑(x ^ y)
[PROOFSTEP]
exact coe_rpow_of_ne_zero hx _
[GOAL]
x : ℝ≥0∞
⊢ x ^ 1 = x
[PROOFSTEP]
cases x
[GOAL]
case none
⊢ none ^ 1 = none
[PROOFSTEP]
exact dif_pos zero_lt_one
[GOAL]
case some
val✝ : ℝ≥0
⊢ Option.some val✝ ^ 1 = Option.some val✝
[PROOFSTEP]
change ite _ _ _ = _
[GOAL]
case some
val✝ : ℝ≥0
⊢ (if val✝ = 0 ∧ 1 < 0 then ⊤ else ↑(val✝ ^ 1)) = Option.some val✝
[PROOFSTEP]
simp only [NNReal.rpow_one, some_eq_coe, ite_eq_right_iff, top_ne_coe, and_imp]
[GOAL]
case some
val✝ : ℝ≥0
⊢ val✝ = 0 → 1 < 0 → False
[PROOFSTEP]
exact fun _ => zero_le_one.not_lt
[GOAL]
x : ℝ
⊢ 1 ^ x = 1
[PROOFSTEP]
rw [← coe_one, coe_rpow_of_ne_zero one_ne_zero]
[GOAL]
x : ℝ
⊢ ↑(1 ^ x) = ↑1
[PROOFSTEP]
simp
[GOAL]
x : ℝ≥0∞
y : ℝ
⊢ x ^ y = 0 ↔ x = 0 ∧ 0 < y ∨ x = ⊤ ∧ y < 0
[PROOFSTEP]
cases' x with x
[GOAL]
case none
y : ℝ
⊢ none ^ y = 0 ↔ none = 0 ∧ 0 < y ∨ none = ⊤ ∧ y < 0
[PROOFSTEP]
rcases lt_trichotomy y 0 with (H | H | H)
[GOAL]
case none.inl
y : ℝ
H : y < 0
⊢ none ^ y = 0 ↔ none = 0 ∧ 0 < y ∨ none = ⊤ ∧ y < 0
[PROOFSTEP]
simp [H, top_rpow_of_neg, top_rpow_of_pos, le_of_lt]
[GOAL]
case none.inr.inl
y : ℝ
H : y = 0
⊢ none ^ y = 0 ↔ none = 0 ∧ 0 < y ∨ none = ⊤ ∧ y < 0
[PROOFSTEP]
simp [H, top_rpow_of_neg, top_rpow_of_pos, le_of_lt]
[GOAL]
case none.inr.inr
y : ℝ
H : 0 < y
⊢ none ^ y = 0 ↔ none = 0 ∧ 0 < y ∨ none = ⊤ ∧ y < 0
[PROOFSTEP]
simp [H, top_rpow_of_neg, top_rpow_of_pos, le_of_lt]
[GOAL]
case some
y : ℝ
x : ℝ≥0
⊢ Option.some x ^ y = 0 ↔ Option.some x = 0 ∧ 0 < y ∨ Option.some x = ⊤ ∧ y < 0
[PROOFSTEP]
by_cases h : x = 0
[GOAL]
case pos
y : ℝ
x : ℝ≥0
h : x = 0
⊢ Option.some x ^ y = 0 ↔ Option.some x = 0 ∧ 0 < y ∨ Option.some x = ⊤ ∧ y < 0
[PROOFSTEP]
rcases lt_trichotomy y 0 with (H | H | H)
[GOAL]
case pos.inl
y : ℝ
x : ℝ≥0
h : x = 0
H : y < 0
⊢ Option.some x ^ y = 0 ↔ Option.some x = 0 ∧ 0 < y ∨ Option.some x = ⊤ ∧ y < 0
[PROOFSTEP]
simp [h, H, zero_rpow_of_neg, zero_rpow_of_pos, le_of_lt]
[GOAL]
case pos.inr.inl
y : ℝ
x : ℝ≥0
h : x = 0
H : y = 0
⊢ Option.some x ^ y = 0 ↔ Option.some x = 0 ∧ 0 < y ∨ Option.some x = ⊤ ∧ y < 0
[PROOFSTEP]
simp [h, H, zero_rpow_of_neg, zero_rpow_of_pos, le_of_lt]
[GOAL]
case pos.inr.inr
y : ℝ
x : ℝ≥0
h : x = 0
H : 0 < y
⊢ Option.some x ^ y = 0 ↔ Option.some x = 0 ∧ 0 < y ∨ Option.some x = ⊤ ∧ y < 0
[PROOFSTEP]
simp [h, H, zero_rpow_of_neg, zero_rpow_of_pos, le_of_lt]
[GOAL]
case neg
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ Option.some x ^ y = 0 ↔ Option.some x = 0 ∧ 0 < y ∨ Option.some x = ⊤ ∧ y < 0
[PROOFSTEP]
simp [coe_rpow_of_ne_zero h, h]
[GOAL]
x : ℝ≥0∞
y : ℝ
⊢ x ^ y = ⊤ ↔ x = 0 ∧ y < 0 ∨ x = ⊤ ∧ 0 < y
[PROOFSTEP]
cases' x with x
[GOAL]
case none
y : ℝ
⊢ none ^ y = ⊤ ↔ none = 0 ∧ y < 0 ∨ none = ⊤ ∧ 0 < y
[PROOFSTEP]
rcases lt_trichotomy y 0 with (H | H | H)
[GOAL]
case none.inl
y : ℝ
H : y < 0
⊢ none ^ y = ⊤ ↔ none = 0 ∧ y < 0 ∨ none = ⊤ ∧ 0 < y
[PROOFSTEP]
simp [H, top_rpow_of_neg, top_rpow_of_pos, le_of_lt]
[GOAL]
case none.inr.inl
y : ℝ
H : y = 0
⊢ none ^ y = ⊤ ↔ none = 0 ∧ y < 0 ∨ none = ⊤ ∧ 0 < y
[PROOFSTEP]
simp [H, top_rpow_of_neg, top_rpow_of_pos, le_of_lt]
[GOAL]
case none.inr.inr
y : ℝ
H : 0 < y
⊢ none ^ y = ⊤ ↔ none = 0 ∧ y < 0 ∨ none = ⊤ ∧ 0 < y
[PROOFSTEP]
simp [H, top_rpow_of_neg, top_rpow_of_pos, le_of_lt]
[GOAL]
case some
y : ℝ
x : ℝ≥0
⊢ Option.some x ^ y = ⊤ ↔ Option.some x = 0 ∧ y < 0 ∨ Option.some x = ⊤ ∧ 0 < y
[PROOFSTEP]
by_cases h : x = 0
[GOAL]
case pos
y : ℝ
x : ℝ≥0
h : x = 0
⊢ Option.some x ^ y = ⊤ ↔ Option.some x = 0 ∧ y < 0 ∨ Option.some x = ⊤ ∧ 0 < y
[PROOFSTEP]
rcases lt_trichotomy y 0 with (H | H | H)
[GOAL]
case pos.inl
y : ℝ
x : ℝ≥0
h : x = 0
H : y < 0
⊢ Option.some x ^ y = ⊤ ↔ Option.some x = 0 ∧ y < 0 ∨ Option.some x = ⊤ ∧ 0 < y
[PROOFSTEP]
simp [h, H, zero_rpow_of_neg, zero_rpow_of_pos, le_of_lt]
[GOAL]
case pos.inr.inl
y : ℝ
x : ℝ≥0
h : x = 0
H : y = 0
⊢ Option.some x ^ y = ⊤ ↔ Option.some x = 0 ∧ y < 0 ∨ Option.some x = ⊤ ∧ 0 < y
[PROOFSTEP]
simp [h, H, zero_rpow_of_neg, zero_rpow_of_pos, le_of_lt]
[GOAL]
case pos.inr.inr
y : ℝ
x : ℝ≥0
h : x = 0
H : 0 < y
⊢ Option.some x ^ y = ⊤ ↔ Option.some x = 0 ∧ y < 0 ∨ Option.some x = ⊤ ∧ 0 < y
[PROOFSTEP]
simp [h, H, zero_rpow_of_neg, zero_rpow_of_pos, le_of_lt]
[GOAL]
case neg
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ Option.some x ^ y = ⊤ ↔ Option.some x = 0 ∧ y < 0 ∨ Option.some x = ⊤ ∧ 0 < y
[PROOFSTEP]
simp [coe_rpow_of_ne_zero h, h]
[GOAL]
x : ℝ≥0∞
y : ℝ
hy : 0 < y
⊢ x ^ y = ⊤ ↔ x = ⊤
[PROOFSTEP]
simp [rpow_eq_top_iff, hy, asymm hy]
[GOAL]
x : ℝ≥0∞
y : ℝ
hy0 : 0 ≤ y
⊢ x ^ y = ⊤ → x = ⊤
[PROOFSTEP]
rw [ENNReal.rpow_eq_top_iff]
[GOAL]
x : ℝ≥0∞
y : ℝ
hy0 : 0 ≤ y
⊢ x = 0 ∧ y < 0 ∨ x = ⊤ ∧ 0 < y → x = ⊤
[PROOFSTEP]
rintro (h | h)
[GOAL]
case inl
x : ℝ≥0∞
y : ℝ
hy0 : 0 ≤ y
h : x = 0 ∧ y < 0
⊢ x = ⊤
[PROOFSTEP]
exfalso
[GOAL]
case inl.h
x : ℝ≥0∞
y : ℝ
hy0 : 0 ≤ y
h : x = 0 ∧ y < 0
⊢ False
[PROOFSTEP]
rw [lt_iff_not_ge] at h
[GOAL]
case inl.h
x : ℝ≥0∞
y : ℝ
hy0 : 0 ≤ y
h : x = 0 ∧ ¬y ≥ 0
⊢ False
[PROOFSTEP]
exact h.right hy0
[GOAL]
case inr
x : ℝ≥0∞
y : ℝ
hy0 : 0 ≤ y
h : x = ⊤ ∧ 0 < y
⊢ x = ⊤
[PROOFSTEP]
exact h.left
[GOAL]
x : ℝ≥0∞
y z : ℝ
hx : x ≠ 0
h'x : x ≠ ⊤
⊢ x ^ (y + z) = x ^ y * x ^ z
[PROOFSTEP]
cases' x with x
[GOAL]
case none
y z : ℝ
hx : none ≠ 0
h'x : none ≠ ⊤
⊢ none ^ (y + z) = none ^ y * none ^ z
[PROOFSTEP]
exact (h'x rfl).elim
[GOAL]
case some
y z : ℝ
x : ℝ≥0
hx : Option.some x ≠ 0
h'x : Option.some x ≠ ⊤
⊢ Option.some x ^ (y + z) = Option.some x ^ y * Option.some x ^ z
[PROOFSTEP]
have : x ≠ 0 := fun h => by simp [h] at hx
[GOAL]
y z : ℝ
x : ℝ≥0
hx : Option.some x ≠ 0
h'x : Option.some x ≠ ⊤
h : x = 0
⊢ False
[PROOFSTEP]
simp [h] at hx
[GOAL]
case some
y z : ℝ
x : ℝ≥0
hx : Option.some x ≠ 0
h'x : Option.some x ≠ ⊤
this : x ≠ 0
⊢ Option.some x ^ (y + z) = Option.some x ^ y * Option.some x ^ z
[PROOFSTEP]
simp [coe_rpow_of_ne_zero this, NNReal.rpow_add this]
[GOAL]
x : ℝ≥0∞
y : ℝ
⊢ x ^ (-y) = (x ^ y)⁻¹
[PROOFSTEP]
cases' x with x
[GOAL]
case none
y : ℝ
⊢ none ^ (-y) = (none ^ y)⁻¹
[PROOFSTEP]
rcases lt_trichotomy y 0 with (H | H | H)
[GOAL]
case none.inl
y : ℝ
H : y < 0
⊢ none ^ (-y) = (none ^ y)⁻¹
[PROOFSTEP]
simp [top_rpow_of_pos, top_rpow_of_neg, H, neg_pos.mpr]
[GOAL]
case none.inr.inl
y : ℝ
H : y = 0
⊢ none ^ (-y) = (none ^ y)⁻¹
[PROOFSTEP]
simp [top_rpow_of_pos, top_rpow_of_neg, H, neg_pos.mpr]
[GOAL]
case none.inr.inr
y : ℝ
H : 0 < y
⊢ none ^ (-y) = (none ^ y)⁻¹
[PROOFSTEP]
simp [top_rpow_of_pos, top_rpow_of_neg, H, neg_pos.mpr]
[GOAL]
case some
y : ℝ
x : ℝ≥0
⊢ Option.some x ^ (-y) = (Option.some x ^ y)⁻¹
[PROOFSTEP]
by_cases h : x = 0
[GOAL]
case pos
y : ℝ
x : ℝ≥0
h : x = 0
⊢ Option.some x ^ (-y) = (Option.some x ^ y)⁻¹
[PROOFSTEP]
rcases lt_trichotomy y 0 with (H | H | H)
[GOAL]
case pos.inl
y : ℝ
x : ℝ≥0
h : x = 0
H : y < 0
⊢ Option.some x ^ (-y) = (Option.some x ^ y)⁻¹
[PROOFSTEP]
simp [h, zero_rpow_of_pos, zero_rpow_of_neg, H, neg_pos.mpr]
[GOAL]
case pos.inr.inl
y : ℝ
x : ℝ≥0
h : x = 0
H : y = 0
⊢ Option.some x ^ (-y) = (Option.some x ^ y)⁻¹
[PROOFSTEP]
simp [h, zero_rpow_of_pos, zero_rpow_of_neg, H, neg_pos.mpr]
[GOAL]
case pos.inr.inr
y : ℝ
x : ℝ≥0
h : x = 0
H : 0 < y
⊢ Option.some x ^ (-y) = (Option.some x ^ y)⁻¹
[PROOFSTEP]
simp [h, zero_rpow_of_pos, zero_rpow_of_neg, H, neg_pos.mpr]
[GOAL]
case neg
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ Option.some x ^ (-y) = (Option.some x ^ y)⁻¹
[PROOFSTEP]
have A : x ^ y ≠ 0 := by simp [h]
[GOAL]
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ x ^ y ≠ 0
[PROOFSTEP]
simp [h]
[GOAL]
case neg
y : ℝ
x : ℝ≥0
h : ¬x = 0
A : x ^ y ≠ 0
⊢ Option.some x ^ (-y) = (Option.some x ^ y)⁻¹
[PROOFSTEP]
simp [coe_rpow_of_ne_zero h, ← coe_inv A, NNReal.rpow_neg]
[GOAL]
x : ℝ≥0∞
y z : ℝ
hx : x ≠ 0
h'x : x ≠ ⊤
⊢ x ^ (y - z) = x ^ y / x ^ z
[PROOFSTEP]
rw [sub_eq_add_neg, rpow_add _ _ hx h'x, rpow_neg, div_eq_mul_inv]
[GOAL]
x : ℝ≥0∞
⊢ x ^ (-1) = x⁻¹
[PROOFSTEP]
simp [rpow_neg]
[GOAL]
x : ℝ≥0∞
y z : ℝ
⊢ x ^ (y * z) = (x ^ y) ^ z
[PROOFSTEP]
cases' x with x
[GOAL]
case none
y z : ℝ
⊢ none ^ (y * z) = (none ^ y) ^ z
[PROOFSTEP]
rcases lt_trichotomy y 0 with (Hy | Hy | Hy)
[GOAL]
case none.inl
y z : ℝ
Hy : y < 0
⊢ none ^ (y * z) = (none ^ y) ^ z
[PROOFSTEP]
rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
[GOAL]
case none.inr.inl
y z : ℝ
Hy : y = 0
⊢ none ^ (y * z) = (none ^ y) ^ z
[PROOFSTEP]
rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
[GOAL]
case none.inr.inr
y z : ℝ
Hy : 0 < y
⊢ none ^ (y * z) = (none ^ y) ^ z
[PROOFSTEP]
rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
[GOAL]
case none.inl.inl
y z : ℝ
Hy : y < 0
Hz : z < 0
⊢ none ^ (y * z) = (none ^ y) ^ z
[PROOFSTEP]
simp [Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos, mul_pos_of_neg_of_neg,
  mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]
[GOAL]
case none.inl.inr.inl
y z : ℝ
Hy : y < 0
Hz : z = 0
⊢ none ^ (y * z) = (none ^ y) ^ z
[PROOFSTEP]
simp [Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos, mul_pos_of_neg_of_neg,
  mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]
[GOAL]
case none.inl.inr.inr
y z : ℝ
Hy : y < 0
Hz : 0 < z
⊢ none ^ (y * z) = (none ^ y) ^ z
[PROOFSTEP]
simp [Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos, mul_pos_of_neg_of_neg,
  mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]
[GOAL]
case none.inr.inl.inl
y z : ℝ
Hy : y = 0
Hz : z < 0
⊢ none ^ (y * z) = (none ^ y) ^ z
[PROOFSTEP]
simp [Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos, mul_pos_of_neg_of_neg,
  mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]
[GOAL]
case none.inr.inl.inr.inl
y z : ℝ
Hy : y = 0
Hz : z = 0
⊢ none ^ (y * z) = (none ^ y) ^ z
[PROOFSTEP]
simp [Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos, mul_pos_of_neg_of_neg,
  mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]
[GOAL]
case none.inr.inl.inr.inr
y z : ℝ
Hy : y = 0
Hz : 0 < z
⊢ none ^ (y * z) = (none ^ y) ^ z
[PROOFSTEP]
simp [Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos, mul_pos_of_neg_of_neg,
  mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]
[GOAL]
case none.inr.inr.inl
y z : ℝ
Hy : 0 < y
Hz : z < 0
⊢ none ^ (y * z) = (none ^ y) ^ z
[PROOFSTEP]
simp [Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos, mul_pos_of_neg_of_neg,
  mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]
[GOAL]
case none.inr.inr.inr.inl
y z : ℝ
Hy : 0 < y
Hz : z = 0
⊢ none ^ (y * z) = (none ^ y) ^ z
[PROOFSTEP]
simp [Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos, mul_pos_of_neg_of_neg,
  mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]
[GOAL]
case none.inr.inr.inr.inr
y z : ℝ
Hy : 0 < y
Hz : 0 < z
⊢ none ^ (y * z) = (none ^ y) ^ z
[PROOFSTEP]
simp [Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos, mul_pos_of_neg_of_neg,
  mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]
[GOAL]
case some
y z : ℝ
x : ℝ≥0
⊢ Option.some x ^ (y * z) = (Option.some x ^ y) ^ z
[PROOFSTEP]
by_cases h : x = 0
[GOAL]
case pos
y z : ℝ
x : ℝ≥0
h : x = 0
⊢ Option.some x ^ (y * z) = (Option.some x ^ y) ^ z
[PROOFSTEP]
rcases lt_trichotomy y 0 with (Hy | Hy | Hy)
[GOAL]
case pos.inl
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y < 0
⊢ Option.some x ^ (y * z) = (Option.some x ^ y) ^ z
[PROOFSTEP]
rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
[GOAL]
case pos.inr.inl
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y = 0
⊢ Option.some x ^ (y * z) = (Option.some x ^ y) ^ z
[PROOFSTEP]
rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
[GOAL]
case pos.inr.inr
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : 0 < y
⊢ Option.some x ^ (y * z) = (Option.some x ^ y) ^ z
[PROOFSTEP]
rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
[GOAL]
case pos.inl.inl
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y < 0
Hz : z < 0
⊢ Option.some x ^ (y * z) = (Option.some x ^ y) ^ z
[PROOFSTEP]
simp [h, Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos, mul_pos_of_neg_of_neg,
  mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]
[GOAL]
case pos.inl.inr.inl
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y < 0
Hz : z = 0
⊢ Option.some x ^ (y * z) = (Option.some x ^ y) ^ z
[PROOFSTEP]
simp [h, Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos, mul_pos_of_neg_of_neg,
  mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]
[GOAL]
case pos.inl.inr.inr
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y < 0
Hz : 0 < z
⊢ Option.some x ^ (y * z) = (Option.some x ^ y) ^ z
[PROOFSTEP]
simp [h, Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos, mul_pos_of_neg_of_neg,
  mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]
[GOAL]
case pos.inr.inl.inl
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y = 0
Hz : z < 0
⊢ Option.some x ^ (y * z) = (Option.some x ^ y) ^ z
[PROOFSTEP]
simp [h, Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos, mul_pos_of_neg_of_neg,
  mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]
[GOAL]
case pos.inr.inl.inr.inl
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y = 0
Hz : z = 0
⊢ Option.some x ^ (y * z) = (Option.some x ^ y) ^ z
[PROOFSTEP]
simp [h, Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos, mul_pos_of_neg_of_neg,
  mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]
[GOAL]
case pos.inr.inl.inr.inr
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y = 0
Hz : 0 < z
⊢ Option.some x ^ (y * z) = (Option.some x ^ y) ^ z
[PROOFSTEP]
simp [h, Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos, mul_pos_of_neg_of_neg,
  mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]
[GOAL]
case pos.inr.inr.inl
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : 0 < y
Hz : z < 0
⊢ Option.some x ^ (y * z) = (Option.some x ^ y) ^ z
[PROOFSTEP]
simp [h, Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos, mul_pos_of_neg_of_neg,
  mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]
[GOAL]
case pos.inr.inr.inr.inl
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : 0 < y
Hz : z = 0
⊢ Option.some x ^ (y * z) = (Option.some x ^ y) ^ z
[PROOFSTEP]
simp [h, Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos, mul_pos_of_neg_of_neg,
  mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]
[GOAL]
case pos.inr.inr.inr.inr
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : 0 < y
Hz : 0 < z
⊢ Option.some x ^ (y * z) = (Option.some x ^ y) ^ z
[PROOFSTEP]
simp [h, Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos, mul_pos_of_neg_of_neg,
  mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]
[GOAL]
case neg
y z : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ Option.some x ^ (y * z) = (Option.some x ^ y) ^ z
[PROOFSTEP]
have : x ^ y ≠ 0 := by simp [h]
[GOAL]
y z : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ x ^ y ≠ 0
[PROOFSTEP]
simp [h]
[GOAL]
case neg
y z : ℝ
x : ℝ≥0
h : ¬x = 0
this : x ^ y ≠ 0
⊢ Option.some x ^ (y * z) = (Option.some x ^ y) ^ z
[PROOFSTEP]
simp [coe_rpow_of_ne_zero h, coe_rpow_of_ne_zero this, NNReal.rpow_mul]
[GOAL]
x : ℝ≥0∞
n : ℕ
⊢ x ^ ↑n = x ^ n
[PROOFSTEP]
cases x
[GOAL]
case none
n : ℕ
⊢ none ^ ↑n = none ^ n
[PROOFSTEP]
cases n
[GOAL]
case none.zero
⊢ none ^ ↑Nat.zero = none ^ Nat.zero
[PROOFSTEP]
simp [top_rpow_of_pos (Nat.cast_add_one_pos _), top_pow (Nat.succ_pos _)]
[GOAL]
case none.succ
n✝ : ℕ
⊢ none ^ ↑(Nat.succ n✝) = none ^ Nat.succ n✝
[PROOFSTEP]
simp [top_rpow_of_pos (Nat.cast_add_one_pos _), top_pow (Nat.succ_pos _)]
[GOAL]
case some
n : ℕ
val✝ : ℝ≥0
⊢ Option.some val✝ ^ ↑n = Option.some val✝ ^ n
[PROOFSTEP]
simp [coe_rpow_of_nonneg _ (Nat.cast_nonneg n)]
[GOAL]
x : ℝ≥0∞
⊢ x ^ 2 = x ^ 2
[PROOFSTEP]
rw [← rpow_nat_cast]
[GOAL]
x : ℝ≥0∞
⊢ x ^ 2 = x ^ ↑2
[PROOFSTEP]
simp only [Nat.cast_ofNat]
[GOAL]
x y : ℝ≥0∞
z : ℝ
⊢ (x * y) ^ z = if (x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0) ∧ z < 0 then ⊤ else x ^ z * y ^ z
[PROOFSTEP]
rcases eq_or_ne z 0 with (rfl | hz)
[GOAL]
case inl
x y : ℝ≥0∞
⊢ (x * y) ^ 0 = if (x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0) ∧ 0 < 0 then ⊤ else x ^ 0 * y ^ 0
[PROOFSTEP]
simp
[GOAL]
case inr
x y : ℝ≥0∞
z : ℝ
hz : z ≠ 0
⊢ (x * y) ^ z = if (x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0) ∧ z < 0 then ⊤ else x ^ z * y ^ z
[PROOFSTEP]
replace hz := hz.lt_or_lt
[GOAL]
case inr
x y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
⊢ (x * y) ^ z = if (x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0) ∧ z < 0 then ⊤ else x ^ z * y ^ z
[PROOFSTEP]
wlog hxy : x ≤ y
[GOAL]
case inr.inr
x y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
this :
  ∀ (x y : ℝ≥0∞) (z : ℝ),
    z < 0 ∨ 0 < z → x ≤ y → (x * y) ^ z = if (x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0) ∧ z < 0 then ⊤ else x ^ z * y ^ z
hxy : ¬x ≤ y
⊢ (x * y) ^ z = if (x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0) ∧ z < 0 then ⊤ else x ^ z * y ^ z
[PROOFSTEP]
convert this y x z hz (le_of_not_le hxy) using 2
[GOAL]
case h.e'_2.h.e'_5
x y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
this :
  ∀ (x y : ℝ≥0∞) (z : ℝ),
    z < 0 ∨ 0 < z → x ≤ y → (x * y) ^ z = if (x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0) ∧ z < 0 then ⊤ else x ^ z * y ^ z
hxy : ¬x ≤ y
⊢ x * y = y * x
[PROOFSTEP]
simp only [mul_comm, and_comm, or_comm]
[GOAL]
case h.e'_3.h₁.a
x y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
this :
  ∀ (x y : ℝ≥0∞) (z : ℝ),
    z < 0 ∨ 0 < z → x ≤ y → (x * y) ^ z = if (x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0) ∧ z < 0 then ⊤ else x ^ z * y ^ z
hxy : ¬x ≤ y
⊢ (x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0) ∧ z < 0 ↔ (y = 0 ∧ x = ⊤ ∨ y = ⊤ ∧ x = 0) ∧ z < 0
[PROOFSTEP]
simp only [mul_comm, and_comm, or_comm]
[GOAL]
case h.e'_3.h₃
x y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
this :
  ∀ (x y : ℝ≥0∞) (z : ℝ),
    z < 0 ∨ 0 < z → x ≤ y → (x * y) ^ z = if (x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0) ∧ z < 0 then ⊤ else x ^ z * y ^ z
hxy : ¬x ≤ y
a✝ : ¬((y = 0 ∧ x = ⊤ ∨ y = ⊤ ∧ x = 0) ∧ z < 0)
⊢ x ^ z * y ^ z = y ^ z * x ^ z
[PROOFSTEP]
simp only [mul_comm, and_comm, or_comm]
[GOAL]
x y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
hxy : x ≤ y
⊢ (x * y) ^ z = if (x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0) ∧ z < 0 then ⊤ else x ^ z * y ^ z
[PROOFSTEP]
rcases eq_or_ne x 0 with (rfl | hx0)
[GOAL]
case inl
y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
hxy : 0 ≤ y
⊢ (0 * y) ^ z = if (0 = 0 ∧ y = ⊤ ∨ 0 = ⊤ ∧ y = 0) ∧ z < 0 then ⊤ else 0 ^ z * y ^ z
[PROOFSTEP]
induction y using ENNReal.recTopCoe
[GOAL]
case inl.top
z : ℝ
hz : z < 0 ∨ 0 < z
hxy : 0 ≤ ⊤
⊢ (0 * ⊤) ^ z = if (0 = 0 ∧ ⊤ = ⊤ ∨ 0 = ⊤ ∧ ⊤ = 0) ∧ z < 0 then ⊤ else 0 ^ z * ⊤ ^ z
[PROOFSTEP]
cases' hz with hz hz
[GOAL]
case inl.coe
z : ℝ
hz : z < 0 ∨ 0 < z
x✝ : ℝ≥0
hxy : 0 ≤ ↑x✝
⊢ (0 * ↑x✝) ^ z = if (0 = 0 ∧ ↑x✝ = ⊤ ∨ 0 = ⊤ ∧ ↑x✝ = 0) ∧ z < 0 then ⊤ else 0 ^ z * ↑x✝ ^ z
[PROOFSTEP]
cases' hz with hz hz
[GOAL]
case inl.top.inl
z : ℝ
hxy : 0 ≤ ⊤
hz : z < 0
⊢ (0 * ⊤) ^ z = if (0 = 0 ∧ ⊤ = ⊤ ∨ 0 = ⊤ ∧ ⊤ = 0) ∧ z < 0 then ⊤ else 0 ^ z * ⊤ ^ z
[PROOFSTEP]
simp [*, hz.not_lt]
[GOAL]
case inl.top.inr
z : ℝ
hxy : 0 ≤ ⊤
hz : 0 < z
⊢ (0 * ⊤) ^ z = if (0 = 0 ∧ ⊤ = ⊤ ∨ 0 = ⊤ ∧ ⊤ = 0) ∧ z < 0 then ⊤ else 0 ^ z * ⊤ ^ z
[PROOFSTEP]
simp [*, hz.not_lt]
[GOAL]
case inl.coe.inl
z : ℝ
x✝ : ℝ≥0
hxy : 0 ≤ ↑x✝
hz : z < 0
⊢ (0 * ↑x✝) ^ z = if (0 = 0 ∧ ↑x✝ = ⊤ ∨ 0 = ⊤ ∧ ↑x✝ = 0) ∧ z < 0 then ⊤ else 0 ^ z * ↑x✝ ^ z
[PROOFSTEP]
simp [*, hz.not_lt]
[GOAL]
case inl.coe.inr
z : ℝ
x✝ : ℝ≥0
hxy : 0 ≤ ↑x✝
hz : 0 < z
⊢ (0 * ↑x✝) ^ z = if (0 = 0 ∧ ↑x✝ = ⊤ ∨ 0 = ⊤ ∧ ↑x✝ = 0) ∧ z < 0 then ⊤ else 0 ^ z * ↑x✝ ^ z
[PROOFSTEP]
simp [*, hz.not_lt]
[GOAL]
case inr
x y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
hxy : x ≤ y
hx0 : x ≠ 0
⊢ (x * y) ^ z = if (x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0) ∧ z < 0 then ⊤ else x ^ z * y ^ z
[PROOFSTEP]
rcases eq_or_ne y 0 with (rfl | hy0)
[GOAL]
case inr.inl
x : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
hx0 : x ≠ 0
hxy : x ≤ 0
⊢ (x * 0) ^ z = if (x = 0 ∧ 0 = ⊤ ∨ x = ⊤ ∧ 0 = 0) ∧ z < 0 then ⊤ else x ^ z * 0 ^ z
[PROOFSTEP]
exact (hx0 (bot_unique hxy)).elim
[GOAL]
case inr.inr
x y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
hxy : x ≤ y
hx0 : x ≠ 0
hy0 : y ≠ 0
⊢ (x * y) ^ z = if (x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0) ∧ z < 0 then ⊤ else x ^ z * y ^ z
[PROOFSTEP]
induction x using ENNReal.recTopCoe
[GOAL]
case inr.inr.top
y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
hy0 : y ≠ 0
hxy : ⊤ ≤ y
hx0 : ⊤ ≠ 0
⊢ (⊤ * y) ^ z = if (⊤ = 0 ∧ y = ⊤ ∨ ⊤ = ⊤ ∧ y = 0) ∧ z < 0 then ⊤ else ⊤ ^ z * y ^ z
[PROOFSTEP]
cases' hz with hz hz
[GOAL]
case inr.inr.top.inl
y : ℝ≥0∞
z : ℝ
hy0 : y ≠ 0
hxy : ⊤ ≤ y
hx0 : ⊤ ≠ 0
hz : z < 0
⊢ (⊤ * y) ^ z = if (⊤ = 0 ∧ y = ⊤ ∨ ⊤ = ⊤ ∧ y = 0) ∧ z < 0 then ⊤ else ⊤ ^ z * y ^ z
[PROOFSTEP]
simp [hz, top_unique hxy]
[GOAL]
case inr.inr.top.inr
y : ℝ≥0∞
z : ℝ
hy0 : y ≠ 0
hxy : ⊤ ≤ y
hx0 : ⊤ ≠ 0
hz : 0 < z
⊢ (⊤ * y) ^ z = if (⊤ = 0 ∧ y = ⊤ ∨ ⊤ = ⊤ ∧ y = 0) ∧ z < 0 then ⊤ else ⊤ ^ z * y ^ z
[PROOFSTEP]
simp [hz, top_unique hxy]
[GOAL]
case inr.inr.coe
y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
hy0 : y ≠ 0
x✝ : ℝ≥0
hxy : ↑x✝ ≤ y
hx0 : ↑x✝ ≠ 0
⊢ (↑x✝ * y) ^ z = if (↑x✝ = 0 ∧ y = ⊤ ∨ ↑x✝ = ⊤ ∧ y = 0) ∧ z < 0 then ⊤ else ↑x✝ ^ z * y ^ z
[PROOFSTEP]
induction y using ENNReal.recTopCoe
[GOAL]
case inr.inr.coe.top
z : ℝ
hz : z < 0 ∨ 0 < z
x✝ : ℝ≥0
hx0 : ↑x✝ ≠ 0
hy0 : ⊤ ≠ 0
hxy : ↑x✝ ≤ ⊤
⊢ (↑x✝ * ⊤) ^ z = if (↑x✝ = 0 ∧ ⊤ = ⊤ ∨ ↑x✝ = ⊤ ∧ ⊤ = 0) ∧ z < 0 then ⊤ else ↑x✝ ^ z * ⊤ ^ z
[PROOFSTEP]
rw [ne_eq, coe_eq_zero] at hx0
[GOAL]
case inr.inr.coe.top
z : ℝ
hz : z < 0 ∨ 0 < z
x✝ : ℝ≥0
hx0 : ¬x✝ = 0
hy0 : ⊤ ≠ 0
hxy : ↑x✝ ≤ ⊤
⊢ (↑x✝ * ⊤) ^ z = if (↑x✝ = 0 ∧ ⊤ = ⊤ ∨ ↑x✝ = ⊤ ∧ ⊤ = 0) ∧ z < 0 then ⊤ else ↑x✝ ^ z * ⊤ ^ z
[PROOFSTEP]
cases' hz with hz hz
[GOAL]
case inr.inr.coe.top.inl
z : ℝ
x✝ : ℝ≥0
hx0 : ¬x✝ = 0
hy0 : ⊤ ≠ 0
hxy : ↑x✝ ≤ ⊤
hz : z < 0
⊢ (↑x✝ * ⊤) ^ z = if (↑x✝ = 0 ∧ ⊤ = ⊤ ∨ ↑x✝ = ⊤ ∧ ⊤ = 0) ∧ z < 0 then ⊤ else ↑x✝ ^ z * ⊤ ^ z
[PROOFSTEP]
simp [*]
[GOAL]
case inr.inr.coe.top.inr
z : ℝ
x✝ : ℝ≥0
hx0 : ¬x✝ = 0
hy0 : ⊤ ≠ 0
hxy : ↑x✝ ≤ ⊤
hz : 0 < z
⊢ (↑x✝ * ⊤) ^ z = if (↑x✝ = 0 ∧ ⊤ = ⊤ ∨ ↑x✝ = ⊤ ∧ ⊤ = 0) ∧ z < 0 then ⊤ else ↑x✝ ^ z * ⊤ ^ z
[PROOFSTEP]
simp [*]
[GOAL]
case inr.inr.coe.coe
z : ℝ
hz : z < 0 ∨ 0 < z
x✝¹ : ℝ≥0
hx0 : ↑x✝¹ ≠ 0
x✝ : ℝ≥0
hy0 : ↑x✝ ≠ 0
hxy : ↑x✝¹ ≤ ↑x✝
⊢ (↑x✝¹ * ↑x✝) ^ z = if (↑x✝¹ = 0 ∧ ↑x✝ = ⊤ ∨ ↑x✝¹ = ⊤ ∧ ↑x✝ = 0) ∧ z < 0 then ⊤ else ↑x✝¹ ^ z * ↑x✝ ^ z
[PROOFSTEP]
simp only [*, false_and_iff, and_false_iff, false_or_iff, if_false]
[GOAL]
case inr.inr.coe.coe
z : ℝ
hz : z < 0 ∨ 0 < z
x✝¹ : ℝ≥0
hx0 : ↑x✝¹ ≠ 0
x✝ : ℝ≥0
hy0 : ↑x✝ ≠ 0
hxy : ↑x✝¹ ≤ ↑x✝
⊢ (↑x✝¹ * ↑x✝) ^ z = ↑x✝¹ ^ z * ↑x✝ ^ z
[PROOFSTEP]
norm_cast at *
[GOAL]
case inr.inr.coe.coe
z : ℝ
x✝¹ x✝ : ℝ≥0
hz : z < 0 ∨ 0 < z
hx0 : ¬x✝¹ = 0
hy0 : ¬x✝ = 0
hxy : x✝¹ ≤ x✝
⊢ ↑(x✝¹ * x✝) ^ z = ↑x✝¹ ^ z * ↑x✝ ^ z
[PROOFSTEP]
rw [coe_rpow_of_ne_zero (mul_ne_zero hx0 hy0), NNReal.mul_rpow]
[GOAL]
case inr.inr.coe.coe
z : ℝ
x✝¹ x✝ : ℝ≥0
hz : z < 0 ∨ 0 < z
hx0 : ¬x✝¹ = 0
hy0 : ¬x✝ = 0
hxy : x✝¹ ≤ x✝
⊢ ↑(x✝¹ ^ z * x✝ ^ z) = ↑x✝¹ ^ z * ↑x✝ ^ z
[PROOFSTEP]
norm_cast
[GOAL]
x y : ℝ≥0∞
hx : x ≠ ⊤
hy : y ≠ ⊤
z : ℝ
⊢ (x * y) ^ z = x ^ z * y ^ z
[PROOFSTEP]
simp [*, mul_rpow_eq_ite]
[GOAL]
x y : ℝ≥0∞
hx : x ≠ 0
hy : y ≠ 0
z : ℝ
⊢ (x * y) ^ z = x ^ z * y ^ z
[PROOFSTEP]
simp [*, mul_rpow_eq_ite]
[GOAL]
x y : ℝ≥0∞
z : ℝ
hz : 0 ≤ z
⊢ (x * y) ^ z = x ^ z * y ^ z
[PROOFSTEP]
simp [hz.not_lt, mul_rpow_eq_ite]
[GOAL]
x : ℝ≥0∞
y : ℝ
⊢ x⁻¹ ^ y = (x ^ y)⁻¹
[PROOFSTEP]
rcases eq_or_ne y 0 with (rfl | hy)
[GOAL]
case inl
x : ℝ≥0∞
⊢ x⁻¹ ^ 0 = (x ^ 0)⁻¹
[PROOFSTEP]
simp only [rpow_zero, inv_one]
[GOAL]
case inr
x : ℝ≥0∞
y : ℝ
hy : y ≠ 0
⊢ x⁻¹ ^ y = (x ^ y)⁻¹
[PROOFSTEP]
replace hy := hy.lt_or_lt
[GOAL]
case inr
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
⊢ x⁻¹ ^ y = (x ^ y)⁻¹
[PROOFSTEP]
rcases eq_or_ne x 0 with (rfl | h0)
[GOAL]
case inr.inl
y : ℝ
hy : y < 0 ∨ 0 < y
⊢ 0⁻¹ ^ y = (0 ^ y)⁻¹
[PROOFSTEP]
cases hy
[GOAL]
case inr.inl.inl
y : ℝ
h✝ : y < 0
⊢ 0⁻¹ ^ y = (0 ^ y)⁻¹
[PROOFSTEP]
simp [*]
[GOAL]
case inr.inl.inr
y : ℝ
h✝ : 0 < y
⊢ 0⁻¹ ^ y = (0 ^ y)⁻¹
[PROOFSTEP]
simp [*]
[GOAL]
case inr.inr
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : x ≠ 0
⊢ x⁻¹ ^ y = (x ^ y)⁻¹
[PROOFSTEP]
rcases eq_or_ne x ⊤ with (rfl | h_top)
[GOAL]
case inr.inr.inl
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : ⊤ ≠ 0
⊢ ⊤⁻¹ ^ y = (⊤ ^ y)⁻¹
[PROOFSTEP]
cases hy
[GOAL]
case inr.inr.inl.inl
y : ℝ
h0 : ⊤ ≠ 0
h✝ : y < 0
⊢ ⊤⁻¹ ^ y = (⊤ ^ y)⁻¹
[PROOFSTEP]
simp [*]
[GOAL]
case inr.inr.inl.inr
y : ℝ
h0 : ⊤ ≠ 0
h✝ : 0 < y
⊢ ⊤⁻¹ ^ y = (⊤ ^ y)⁻¹
[PROOFSTEP]
simp [*]
[GOAL]
case inr.inr.inr
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : x ≠ 0
h_top : x ≠ ⊤
⊢ x⁻¹ ^ y = (x ^ y)⁻¹
[PROOFSTEP]
apply ENNReal.eq_inv_of_mul_eq_one_left
[GOAL]
case inr.inr.inr.h
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : x ≠ 0
h_top : x ≠ ⊤
⊢ x⁻¹ ^ y * x ^ y = 1
[PROOFSTEP]
rw [← mul_rpow_of_ne_zero (ENNReal.inv_ne_zero.2 h_top) h0, ENNReal.inv_mul_cancel h0 h_top, one_rpow]
[GOAL]
x y : ℝ≥0∞
z : ℝ
hz : 0 ≤ z
⊢ (x / y) ^ z = x ^ z / y ^ z
[PROOFSTEP]
rw [div_eq_mul_inv, mul_rpow_of_nonneg _ _ hz, inv_rpow, div_eq_mul_inv]
[GOAL]
z : ℝ
h : 0 < z
⊢ StrictMono fun x => x ^ z
[PROOFSTEP]
intro x y hxy
[GOAL]
z : ℝ
h : 0 < z
x y : ℝ≥0∞
hxy : x < y
⊢ (fun x => x ^ z) x < (fun x => x ^ z) y
[PROOFSTEP]
lift x to ℝ≥0 using ne_top_of_lt hxy
[GOAL]
case intro
z : ℝ
h : 0 < z
y : ℝ≥0∞
x : ℝ≥0
hxy : ↑x < y
⊢ (fun x => x ^ z) ↑x < (fun x => x ^ z) y
[PROOFSTEP]
rcases eq_or_ne y ∞ with (rfl | hy)
[GOAL]
case intro.inl
z : ℝ
h : 0 < z
x : ℝ≥0
hxy : ↑x < ⊤
⊢ (fun x => x ^ z) ↑x < (fun x => x ^ z) ⊤
[PROOFSTEP]
simp only [top_rpow_of_pos h, coe_rpow_of_nonneg _ h.le, coe_lt_top]
[GOAL]
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
[PROOFSTEP]
lift y to ℝ≥0 using hy
[GOAL]
case intro.inr.intro
z : ℝ
h : 0 < z
x y : ℝ≥0
hxy : ↑x < ↑y
⊢ (fun x => x ^ z) ↑x < (fun x => x ^ z) ↑y
[PROOFSTEP]
simp only [coe_rpow_of_nonneg _ h.le, NNReal.rpow_lt_rpow (coe_lt_coe.1 hxy) h, coe_lt_coe]
[GOAL]
z : ℝ
h : 0 ≤ z
h0 : 0 = z
⊢ Monotone fun x => x ^ 0
[PROOFSTEP]
simp only [rpow_zero, monotone_const]
[GOAL]
y : ℝ
hy : 0 < y
x : ℝ≥0∞
⊢ (fun x => x ^ y) ((fun x => x ^ (1 / y)) x) = x
[PROOFSTEP]
dsimp
[GOAL]
y : ℝ
hy : 0 < y
x : ℝ≥0∞
⊢ (x ^ (1 / y)) ^ y = x
[PROOFSTEP]
rw [← rpow_mul, one_div_mul_cancel hy.ne.symm, rpow_one]
[GOAL]
y : ℝ
hy : 0 < y
⊢ OrderIso.symm (orderIsoRpow y hy) = orderIsoRpow (1 / y) (_ : 0 < 1 / y)
[PROOFSTEP]
simp only [orderIsoRpow, one_div_one_div]
[GOAL]
y : ℝ
hy : 0 < y
⊢ OrderIso.symm
      (StrictMono.orderIsoOfRightInverse (fun x => x ^ y) (_ : StrictMono fun x => x ^ y) (fun x => x ^ (1 / y))
        (_ : ∀ (x : ℝ≥0∞), (fun x => x ^ y) ((fun x => x ^ (1 / y)) x) = x)) =
    StrictMono.orderIsoOfRightInverse (fun x => x ^ (1 / y)) (_ : StrictMono fun x => x ^ (1 / y)) (fun x => x ^ y)
      (_ : Function.RightInverse (fun x => x ^ y) fun x => x ^ (1 / y))
[PROOFSTEP]
rfl
[GOAL]
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ≤ y ^ (1 / z) ↔ x ^ z ≤ y
[PROOFSTEP]
nth_rw 1 [← rpow_one x]
[GOAL]
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ 1 ≤ y ^ (1 / z) ↔ x ^ z ≤ y
[PROOFSTEP]
nth_rw 1 [← @_root_.mul_inv_cancel _ _ z hz.ne']
[GOAL]
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ (z * z⁻¹) ≤ y ^ (1 / z) ↔ x ^ z ≤ y
[PROOFSTEP]
rw [rpow_mul, ← one_div, @rpow_le_rpow_iff _ _ (1 / z) (by simp [hz])]
[GOAL]
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ 0 < 1 / z
[PROOFSTEP]
simp [hz]
[GOAL]
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x < y ^ (1 / z) ↔ x ^ z < y
[PROOFSTEP]
nth_rw 1 [← rpow_one x]
[GOAL]
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ 1 < y ^ (1 / z) ↔ x ^ z < y
[PROOFSTEP]
nth_rw 1 [← @_root_.mul_inv_cancel _ _ z (ne_of_lt hz).symm]
[GOAL]
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ (z * z⁻¹) < y ^ (1 / z) ↔ x ^ z < y
[PROOFSTEP]
rw [rpow_mul, ← one_div, @rpow_lt_rpow_iff _ _ (1 / z) (by simp [hz])]
[GOAL]
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ 0 < 1 / z
[PROOFSTEP]
simp [hz]
[GOAL]
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ (1 / z) ≤ y ↔ x ≤ y ^ z
[PROOFSTEP]
nth_rw 1 [← ENNReal.rpow_one y]
[GOAL]
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ (1 / z) ≤ y ^ 1 ↔ x ≤ y ^ z
[PROOFSTEP]
nth_rw 2 [← @_root_.mul_inv_cancel _ _ z hz.ne.symm]
[GOAL]
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ (1 / z) ≤ y ^ (z * z⁻¹) ↔ x ≤ y ^ z
[PROOFSTEP]
rw [ENNReal.rpow_mul, ← one_div, ENNReal.rpow_le_rpow_iff (one_div_pos.2 hz)]
[GOAL]
x : ℝ≥0∞
y z : ℝ
hx : 1 < x
hx' : x ≠ ⊤
hyz : y < z
⊢ x ^ y < x ^ z
[PROOFSTEP]
lift x to ℝ≥0 using hx'
[GOAL]
case intro
y z : ℝ
hyz : y < z
x : ℝ≥0
hx : 1 < ↑x
⊢ ↑x ^ y < ↑x ^ z
[PROOFSTEP]
rw [one_lt_coe_iff] at hx
[GOAL]
case intro
y z : ℝ
hyz : y < z
x : ℝ≥0
hx : 1 < x
⊢ ↑x ^ y < ↑x ^ z
[PROOFSTEP]
simp [coe_rpow_of_ne_zero (ne_of_gt (lt_trans zero_lt_one hx)), NNReal.rpow_lt_rpow_of_exponent_lt hx hyz]
[GOAL]
x : ℝ≥0∞
y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ x ^ y ≤ x ^ z
[PROOFSTEP]
cases x
[GOAL]
case none
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ none
⊢ none ^ y ≤ none ^ z
[PROOFSTEP]
rcases lt_trichotomy y 0 with (Hy | Hy | Hy)
[GOAL]
case none.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ none
Hy : y < 0
⊢ none ^ y ≤ none ^ z
[PROOFSTEP]
rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
[GOAL]
case none.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ none
Hy : y = 0
⊢ none ^ y ≤ none ^ z
[PROOFSTEP]
rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
[GOAL]
case none.inr.inr
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ none
Hy : 0 < y
⊢ none ^ y ≤ none ^ z
[PROOFSTEP]
rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
[GOAL]
case none.inl.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ none
Hy : y < 0
Hz : z < 0
⊢ none ^ y ≤ none ^ z
[PROOFSTEP]
simp [Hy, Hz, top_rpow_of_neg, top_rpow_of_pos, le_refl]
[GOAL]
case none.inl.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ none
Hy : y < 0
Hz : z = 0
⊢ none ^ y ≤ none ^ z
[PROOFSTEP]
simp [Hy, Hz, top_rpow_of_neg, top_rpow_of_pos, le_refl]
[GOAL]
case none.inl.inr.inr
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ none
Hy : y < 0
Hz : 0 < z
⊢ none ^ y ≤ none ^ z
[PROOFSTEP]
simp [Hy, Hz, top_rpow_of_neg, top_rpow_of_pos, le_refl]
[GOAL]
case none.inr.inl.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ none
Hy : y = 0
Hz : z < 0
⊢ none ^ y ≤ none ^ z
[PROOFSTEP]
simp [Hy, Hz, top_rpow_of_neg, top_rpow_of_pos, le_refl]
[GOAL]
case none.inr.inl.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ none
Hy : y = 0
Hz : z = 0
⊢ none ^ y ≤ none ^ z
[PROOFSTEP]
simp [Hy, Hz, top_rpow_of_neg, top_rpow_of_pos, le_refl]
[GOAL]
case none.inr.inl.inr.inr
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ none
Hy : y = 0
Hz : 0 < z
⊢ none ^ y ≤ none ^ z
[PROOFSTEP]
simp [Hy, Hz, top_rpow_of_neg, top_rpow_of_pos, le_refl]
[GOAL]
case none.inr.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ none
Hy : 0 < y
Hz : z < 0
⊢ none ^ y ≤ none ^ z
[PROOFSTEP]
simp [Hy, Hz, top_rpow_of_neg, top_rpow_of_pos, le_refl]
[GOAL]
case none.inr.inr.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ none
Hy : 0 < y
Hz : z = 0
⊢ none ^ y ≤ none ^ z
[PROOFSTEP]
simp [Hy, Hz, top_rpow_of_neg, top_rpow_of_pos, le_refl]
[GOAL]
case none.inr.inr.inr.inr
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ none
Hy : 0 < y
Hz : 0 < z
⊢ none ^ y ≤ none ^ z
[PROOFSTEP]
simp [Hy, Hz, top_rpow_of_neg, top_rpow_of_pos, le_refl]
[GOAL]
case none.inr.inl.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ none
Hy : y = 0
Hz : z < 0
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case none.inr.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ none
Hy : 0 < y
Hz : z < 0
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case none.inr.inr.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ none
Hy : 0 < y
Hz : z = 0
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case some
y z : ℝ
hyz : y ≤ z
val✝ : ℝ≥0
hx : 1 ≤ Option.some val✝
⊢ Option.some val✝ ^ y ≤ Option.some val✝ ^ z
[PROOFSTEP]
simp only [one_le_coe_iff, some_eq_coe] at hx
[GOAL]
case some
y z : ℝ
hyz : y ≤ z
val✝ : ℝ≥0
hx : 1 ≤ val✝
⊢ Option.some val✝ ^ y ≤ Option.some val✝ ^ z
[PROOFSTEP]
simp [coe_rpow_of_ne_zero (ne_of_gt (lt_of_lt_of_le zero_lt_one hx)), NNReal.rpow_le_rpow_of_exponent_le hx hyz]
[GOAL]
x : ℝ≥0∞
y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ x ^ y < x ^ z
[PROOFSTEP]
lift x to ℝ≥0 using ne_of_lt (lt_of_lt_of_le hx1 le_top)
[GOAL]
case intro
y z : ℝ
hyz : z < y
x : ℝ≥0
hx0 : 0 < ↑x
hx1 : ↑x < 1
⊢ ↑x ^ y < ↑x ^ z
[PROOFSTEP]
simp only [coe_lt_one_iff, coe_pos] at hx0 hx1
[GOAL]
case intro
y z : ℝ
hyz : z < y
x : ℝ≥0
hx0 : 0 < x
hx1 : x < 1
⊢ ↑x ^ y < ↑x ^ z
[PROOFSTEP]
simp [coe_rpow_of_ne_zero (ne_of_gt hx0), NNReal.rpow_lt_rpow_of_exponent_gt hx0 hx1 hyz]
[GOAL]
x : ℝ≥0∞
y z : ℝ
hx1 : x ≤ 1
hyz : z ≤ y
⊢ x ^ y ≤ x ^ z
[PROOFSTEP]
lift x to ℝ≥0 using ne_of_lt (lt_of_le_of_lt hx1 coe_lt_top)
[GOAL]
case intro
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
⊢ ↑x ^ y ≤ ↑x ^ z
[PROOFSTEP]
by_cases h : x = 0
[GOAL]
case pos
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
⊢ ↑x ^ y ≤ ↑x ^ z
[PROOFSTEP]
rcases lt_trichotomy y 0 with (Hy | Hy | Hy)
[GOAL]
case pos.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y < 0
⊢ ↑x ^ y ≤ ↑x ^ z
[PROOFSTEP]
rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
[GOAL]
case pos.inr.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y = 0
⊢ ↑x ^ y ≤ ↑x ^ z
[PROOFSTEP]
rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
[GOAL]
case pos.inr.inr
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : 0 < y
⊢ ↑x ^ y ≤ ↑x ^ z
[PROOFSTEP]
rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
[GOAL]
case pos.inl.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y < 0
Hz : z < 0
⊢ ↑x ^ y ≤ ↑x ^ z
[PROOFSTEP]
simp [Hy, Hz, h, zero_rpow_of_neg, zero_rpow_of_pos, le_refl]
[GOAL]
case pos.inl.inr.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y < 0
Hz : z = 0
⊢ ↑x ^ y ≤ ↑x ^ z
[PROOFSTEP]
simp [Hy, Hz, h, zero_rpow_of_neg, zero_rpow_of_pos, le_refl]
[GOAL]
case pos.inl.inr.inr
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y < 0
Hz : 0 < z
⊢ ↑x ^ y ≤ ↑x ^ z
[PROOFSTEP]
simp [Hy, Hz, h, zero_rpow_of_neg, zero_rpow_of_pos, le_refl]
[GOAL]
case pos.inr.inl.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y = 0
Hz : z < 0
⊢ ↑x ^ y ≤ ↑x ^ z
[PROOFSTEP]
simp [Hy, Hz, h, zero_rpow_of_neg, zero_rpow_of_pos, le_refl]
[GOAL]
case pos.inr.inl.inr.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y = 0
Hz : z = 0
⊢ ↑x ^ y ≤ ↑x ^ z
[PROOFSTEP]
simp [Hy, Hz, h, zero_rpow_of_neg, zero_rpow_of_pos, le_refl]
[GOAL]
case pos.inr.inl.inr.inr
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y = 0
Hz : 0 < z
⊢ ↑x ^ y ≤ ↑x ^ z
[PROOFSTEP]
simp [Hy, Hz, h, zero_rpow_of_neg, zero_rpow_of_pos, le_refl]
[GOAL]
case pos.inr.inr.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : 0 < y
Hz : z < 0
⊢ ↑x ^ y ≤ ↑x ^ z
[PROOFSTEP]
simp [Hy, Hz, h, zero_rpow_of_neg, zero_rpow_of_pos, le_refl]
[GOAL]
case pos.inr.inr.inr.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : 0 < y
Hz : z = 0
⊢ ↑x ^ y ≤ ↑x ^ z
[PROOFSTEP]
simp [Hy, Hz, h, zero_rpow_of_neg, zero_rpow_of_pos, le_refl]
[GOAL]
case pos.inr.inr.inr.inr
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : 0 < y
Hz : 0 < z
⊢ ↑x ^ y ≤ ↑x ^ z
[PROOFSTEP]
simp [Hy, Hz, h, zero_rpow_of_neg, zero_rpow_of_pos, le_refl]
[GOAL]
case pos.inl.inr.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y < 0
Hz : z = 0
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case pos.inl.inr.inr
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y < 0
Hz : 0 < z
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case pos.inr.inl.inr.inr
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y = 0
Hz : 0 < z
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case neg
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : ¬x = 0
⊢ ↑x ^ y ≤ ↑x ^ z
[PROOFSTEP]
rw [coe_le_one_iff] at hx1
[GOAL]
case neg
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : x ≤ 1
h : ¬x = 0
⊢ ↑x ^ y ≤ ↑x ^ z
[PROOFSTEP]
simp [coe_rpow_of_ne_zero h, NNReal.rpow_le_rpow_of_exponent_ge (bot_lt_iff_ne_bot.mpr h) hx1 hyz]
[GOAL]
x : ℝ≥0∞
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
⊢ x ^ z ≤ x
[PROOFSTEP]
nth_rw 2 [← ENNReal.rpow_one x]
[GOAL]
x : ℝ≥0∞
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
⊢ x ^ z ≤ x ^ 1
[PROOFSTEP]
exact ENNReal.rpow_le_rpow_of_exponent_ge hx h_one_le
[GOAL]
x : ℝ≥0∞
z : ℝ
hx : 1 ≤ x
h_one_le : 1 ≤ z
⊢ x ≤ x ^ z
[PROOFSTEP]
nth_rw 1 [← ENNReal.rpow_one x]
[GOAL]
x : ℝ≥0∞
z : ℝ
hx : 1 ≤ x
h_one_le : 1 ≤ z
⊢ x ^ 1 ≤ x ^ z
[PROOFSTEP]
exact ENNReal.rpow_le_rpow_of_exponent_le hx h_one_le
[GOAL]
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
⊢ 0 < x ^ p
[PROOFSTEP]
by_cases hp_zero : p = 0
[GOAL]
case pos
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p = 0
⊢ 0 < x ^ p
[PROOFSTEP]
simp [hp_zero, zero_lt_one]
[GOAL]
case neg
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : ¬p = 0
⊢ 0 < x ^ p
[PROOFSTEP]
rw [← Ne.def] at hp_zero
[GOAL]
case neg
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p ≠ 0
⊢ 0 < x ^ p
[PROOFSTEP]
have hp_pos := lt_of_le_of_ne hp_nonneg hp_zero.symm
[GOAL]
case neg
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p ≠ 0
hp_pos : 0 < p
⊢ 0 < x ^ p
[PROOFSTEP]
rw [← zero_rpow_of_pos hp_pos]
[GOAL]
case neg
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p ≠ 0
hp_pos : 0 < p
⊢ 0 ^ p < x ^ p
[PROOFSTEP]
exact rpow_lt_rpow hx_pos hp_pos
[GOAL]
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hx_ne_top : x ≠ ⊤
⊢ 0 < x ^ p
[PROOFSTEP]
cases' lt_or_le 0 p with hp_pos hp_nonpos
[GOAL]
case inl
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hx_ne_top : x ≠ ⊤
hp_pos : 0 < p
⊢ 0 < x ^ p
[PROOFSTEP]
exact rpow_pos_of_nonneg hx_pos (le_of_lt hp_pos)
[GOAL]
case inr
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hx_ne_top : x ≠ ⊤
hp_nonpos : p ≤ 0
⊢ 0 < x ^ p
[PROOFSTEP]
rw [← neg_neg p, rpow_neg, ENNReal.inv_pos]
[GOAL]
case inr
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hx_ne_top : x ≠ ⊤
hp_nonpos : p ≤ 0
⊢ x ^ (-p) ≠ ⊤
[PROOFSTEP]
exact rpow_ne_top_of_nonneg (Right.nonneg_neg_iff.mpr hp_nonpos) hx_ne_top
[GOAL]
x : ℝ≥0∞
z : ℝ
hx : x < 1
hz : 0 < z
⊢ x ^ z < 1
[PROOFSTEP]
lift x to ℝ≥0 using ne_of_lt (lt_of_lt_of_le hx le_top)
[GOAL]
case intro
z : ℝ
hz : 0 < z
x : ℝ≥0
hx : ↑x < 1
⊢ ↑x ^ z < 1
[PROOFSTEP]
simp only [coe_lt_one_iff] at hx
[GOAL]
case intro
z : ℝ
hz : 0 < z
x : ℝ≥0
hx : x < 1
⊢ ↑x ^ z < 1
[PROOFSTEP]
simp [coe_rpow_of_nonneg _ (le_of_lt hz), NNReal.rpow_lt_one hx hz]
[GOAL]
x : ℝ≥0∞
z : ℝ
hx : x ≤ 1
hz : 0 ≤ z
⊢ x ^ z ≤ 1
[PROOFSTEP]
lift x to ℝ≥0 using ne_of_lt (lt_of_le_of_lt hx coe_lt_top)
[GOAL]
case intro
z : ℝ
hz : 0 ≤ z
x : ℝ≥0
hx : ↑x ≤ 1
⊢ ↑x ^ z ≤ 1
[PROOFSTEP]
simp only [coe_le_one_iff] at hx
[GOAL]
case intro
z : ℝ
hz : 0 ≤ z
x : ℝ≥0
hx : x ≤ 1
⊢ ↑x ^ z ≤ 1
[PROOFSTEP]
simp [coe_rpow_of_nonneg _ hz, NNReal.rpow_le_one hx hz]
[GOAL]
x : ℝ≥0∞
z : ℝ
hx : 1 < x
hz : z < 0
⊢ x ^ z < 1
[PROOFSTEP]
cases x
[GOAL]
case none
z : ℝ
hz : z < 0
hx : 1 < none
⊢ none ^ z < 1
[PROOFSTEP]
simp [top_rpow_of_neg hz, zero_lt_one]
[GOAL]
case some
z : ℝ
hz : z < 0
val✝ : ℝ≥0
hx : 1 < Option.some val✝
⊢ Option.some val✝ ^ z < 1
[PROOFSTEP]
simp only [some_eq_coe, one_lt_coe_iff] at hx
[GOAL]
case some
z : ℝ
hz : z < 0
val✝ : ℝ≥0
hx : 1 < val✝
⊢ Option.some val✝ ^ z < 1
[PROOFSTEP]
simp [coe_rpow_of_ne_zero (ne_of_gt (lt_trans zero_lt_one hx)), NNReal.rpow_lt_one_of_one_lt_of_neg hx hz]
[GOAL]
x : ℝ≥0∞
z : ℝ
hx : 1 ≤ x
hz : z < 0
⊢ x ^ z ≤ 1
[PROOFSTEP]
cases x
[GOAL]
case none
z : ℝ
hz : z < 0
hx : 1 ≤ none
⊢ none ^ z ≤ 1
[PROOFSTEP]
simp [top_rpow_of_neg hz, zero_lt_one]
[GOAL]
case some
z : ℝ
hz : z < 0
val✝ : ℝ≥0
hx : 1 ≤ Option.some val✝
⊢ Option.some val✝ ^ z ≤ 1
[PROOFSTEP]
simp only [one_le_coe_iff, some_eq_coe] at hx
[GOAL]
case some
z : ℝ
hz : z < 0
val✝ : ℝ≥0
hx : 1 ≤ val✝
⊢ Option.some val✝ ^ z ≤ 1
[PROOFSTEP]
simp [coe_rpow_of_ne_zero (ne_of_gt (lt_of_lt_of_le zero_lt_one hx)),
  NNReal.rpow_le_one_of_one_le_of_nonpos hx (le_of_lt hz)]
[GOAL]
x : ℝ≥0∞
z : ℝ
hx : 1 < x
hz : 0 < z
⊢ 1 < x ^ z
[PROOFSTEP]
cases x
[GOAL]
case none
z : ℝ
hz : 0 < z
hx : 1 < none
⊢ 1 < none ^ z
[PROOFSTEP]
simp [top_rpow_of_pos hz]
[GOAL]
case some
z : ℝ
hz : 0 < z
val✝ : ℝ≥0
hx : 1 < Option.some val✝
⊢ 1 < Option.some val✝ ^ z
[PROOFSTEP]
simp only [some_eq_coe, one_lt_coe_iff] at hx
[GOAL]
case some
z : ℝ
hz : 0 < z
val✝ : ℝ≥0
hx : 1 < val✝
⊢ 1 < Option.some val✝ ^ z
[PROOFSTEP]
simp [coe_rpow_of_nonneg _ (le_of_lt hz), NNReal.one_lt_rpow hx hz]
[GOAL]
x : ℝ≥0∞
z : ℝ
hx : 1 ≤ x
hz : 0 < z
⊢ 1 ≤ x ^ z
[PROOFSTEP]
cases x
[GOAL]
case none
z : ℝ
hz : 0 < z
hx : 1 ≤ none
⊢ 1 ≤ none ^ z
[PROOFSTEP]
simp [top_rpow_of_pos hz]
[GOAL]
case some
z : ℝ
hz : 0 < z
val✝ : ℝ≥0
hx : 1 ≤ Option.some val✝
⊢ 1 ≤ Option.some val✝ ^ z
[PROOFSTEP]
simp only [one_le_coe_iff, some_eq_coe] at hx
[GOAL]
case some
z : ℝ
hz : 0 < z
val✝ : ℝ≥0
hx : 1 ≤ val✝
⊢ 1 ≤ Option.some val✝ ^ z
[PROOFSTEP]
simp [coe_rpow_of_nonneg _ (le_of_lt hz), NNReal.one_le_rpow hx (le_of_lt hz)]
[GOAL]
x : ℝ≥0∞
z : ℝ
hx1 : 0 < x
hx2 : x < 1
hz : z < 0
⊢ 1 < x ^ z
[PROOFSTEP]
lift x to ℝ≥0 using ne_of_lt (lt_of_lt_of_le hx2 le_top)
[GOAL]
case intro
z : ℝ
hz : z < 0
x : ℝ≥0
hx1 : 0 < ↑x
hx2 : ↑x < 1
⊢ 1 < ↑x ^ z
[PROOFSTEP]
simp only [coe_lt_one_iff, coe_pos] at hx1 hx2 ⊢
[GOAL]
case intro
z : ℝ
hz : z < 0
x : ℝ≥0
hx1 : 0 < x
hx2 : x < 1
⊢ 1 < ↑x ^ z
[PROOFSTEP]
simp [coe_rpow_of_ne_zero (ne_of_gt hx1), NNReal.one_lt_rpow_of_pos_of_lt_one_of_neg hx1 hx2 hz]
[GOAL]
x : ℝ≥0∞
z : ℝ
hx1 : 0 < x
hx2 : x ≤ 1
hz : z < 0
⊢ 1 ≤ x ^ z
[PROOFSTEP]
lift x to ℝ≥0 using ne_of_lt (lt_of_le_of_lt hx2 coe_lt_top)
[GOAL]
case intro
z : ℝ
hz : z < 0
x : ℝ≥0
hx1 : 0 < ↑x
hx2 : ↑x ≤ 1
⊢ 1 ≤ ↑x ^ z
[PROOFSTEP]
simp only [coe_le_one_iff, coe_pos] at hx1 hx2 ⊢
[GOAL]
case intro
z : ℝ
hz : z < 0
x : ℝ≥0
hx1 : 0 < x
hx2 : x ≤ 1
⊢ 1 ≤ ↑x ^ z
[PROOFSTEP]
simp [coe_rpow_of_ne_zero (ne_of_gt hx1), NNReal.one_le_rpow_of_pos_of_le_one_of_nonpos hx1 hx2 (le_of_lt hz)]
[GOAL]
x : ℝ≥0∞
z : ℝ
⊢ ENNReal.toNNReal x ^ z = ENNReal.toNNReal (x ^ z)
[PROOFSTEP]
rcases lt_trichotomy z 0 with (H | H | H)
[GOAL]
case inl
x : ℝ≥0∞
z : ℝ
H : z < 0
⊢ ENNReal.toNNReal x ^ z = ENNReal.toNNReal (x ^ z)
[PROOFSTEP]
cases' x with x
[GOAL]
case inl.none
z : ℝ
H : z < 0
⊢ ENNReal.toNNReal none ^ z = ENNReal.toNNReal (none ^ z)
[PROOFSTEP]
simp [H, ne_of_lt]
[GOAL]
case inl.some
z : ℝ
H : z < 0
x : ℝ≥0
⊢ ENNReal.toNNReal (Option.some x) ^ z = ENNReal.toNNReal (Option.some x ^ z)
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
z : ℝ
H : z < 0
x : ℝ≥0
hx : x = 0
⊢ ENNReal.toNNReal (Option.some x) ^ z = ENNReal.toNNReal (Option.some x ^ z)
[PROOFSTEP]
simp [hx, H, ne_of_lt]
[GOAL]
case neg
z : ℝ
H : z < 0
x : ℝ≥0
hx : ¬x = 0
⊢ ENNReal.toNNReal (Option.some x) ^ z = ENNReal.toNNReal (Option.some x ^ z)
[PROOFSTEP]
simp [coe_rpow_of_ne_zero hx]
[GOAL]
case inr.inl
x : ℝ≥0∞
z : ℝ
H : z = 0
⊢ ENNReal.toNNReal x ^ z = ENNReal.toNNReal (x ^ z)
[PROOFSTEP]
simp [H]
[GOAL]
case inr.inr
x : ℝ≥0∞
z : ℝ
H : 0 < z
⊢ ENNReal.toNNReal x ^ z = ENNReal.toNNReal (x ^ z)
[PROOFSTEP]
cases x
[GOAL]
case inr.inr.none
z : ℝ
H : 0 < z
⊢ ENNReal.toNNReal none ^ z = ENNReal.toNNReal (none ^ z)
[PROOFSTEP]
simp [H, ne_of_gt]
[GOAL]
case inr.inr.some
z : ℝ
H : 0 < z
val✝ : ℝ≥0
⊢ ENNReal.toNNReal (Option.some val✝) ^ z = ENNReal.toNNReal (Option.some val✝ ^ z)
[PROOFSTEP]
simp [coe_rpow_of_nonneg _ (le_of_lt H)]
[GOAL]
x : ℝ≥0∞
z : ℝ
⊢ ENNReal.toReal x ^ z = ENNReal.toReal (x ^ z)
[PROOFSTEP]
rw [ENNReal.toReal, ENNReal.toReal, ← NNReal.coe_rpow, ENNReal.toNNReal_rpow]
[GOAL]
x p : ℝ
hx_pos : 0 < x
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
[PROOFSTEP]
simp_rw [ENNReal.ofReal]
[GOAL]
x p : ℝ
hx_pos : 0 < x
⊢ ↑(toNNReal x) ^ p = ↑(toNNReal (x ^ p))
[PROOFSTEP]
rw [coe_rpow_of_ne_zero, coe_eq_coe, Real.toNNReal_rpow_of_nonneg hx_pos.le]
[GOAL]
case h
x p : ℝ
hx_pos : 0 < x
⊢ toNNReal x ≠ 0
[PROOFSTEP]
simp [hx_pos]
[GOAL]
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
[PROOFSTEP]
by_cases hp0 : p = 0
[GOAL]
case pos
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : p = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
[PROOFSTEP]
simp [hp0]
[GOAL]
case neg
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
[PROOFSTEP]
by_cases hx0 : x = 0
[GOAL]
case pos
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
hx0 : x = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
[PROOFSTEP]
rw [← Ne.def] at hp0
[GOAL]
case pos
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : p ≠ 0
hx0 : x = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
[PROOFSTEP]
have hp_pos : 0 < p := lt_of_le_of_ne hp_nonneg hp0.symm
[GOAL]
case pos
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : p ≠ 0
hx0 : x = 0
hp_pos : 0 < p
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
[PROOFSTEP]
simp [hx0, hp_pos, hp_pos.ne.symm]
[GOAL]
case neg
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
hx0 : ¬x = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
[PROOFSTEP]
rw [← Ne.def] at hx0
[GOAL]
case neg
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
hx0 : x ≠ 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
[PROOFSTEP]
exact ofReal_rpow_of_pos (hx_nonneg.lt_of_ne hx0.symm)
[GOAL]
x : ℝ
hx : x ≠ 0
⊢ Function.Injective fun y => y ^ x
[PROOFSTEP]
intro y z hyz
[GOAL]
x : ℝ
hx : x ≠ 0
y z : ℝ≥0∞
hyz : (fun y => y ^ x) y = (fun y => y ^ x) z
⊢ y = z
[PROOFSTEP]
dsimp only at hyz
[GOAL]
x : ℝ
hx : x ≠ 0
y z : ℝ≥0∞
hyz : y ^ x = z ^ x
⊢ y = z
[PROOFSTEP]
rw [← rpow_one y, ← rpow_one z, ← _root_.mul_inv_cancel hx, rpow_mul, rpow_mul, hyz]
[GOAL]
x : ℝ
hx : x ≠ 0
y : ℝ≥0∞
⊢ (fun y => y ^ x) (y ^ x⁻¹) = y
[PROOFSTEP]
simp_rw [← rpow_mul, _root_.inv_mul_cancel hx, rpow_one]