case inl
x y : ℝ≥0∞
⊢ (x * y) ^ 0 = if (x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0) ∧ 0 < 0 then ⊤ else x ^ 0 * y ^ 0

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
x y : ℝ≥0∞
z : ℝ
⊢ (x * y) ^ z = if (x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0) ∧ z < 0 then ⊤ else x ^ z * y ^ z
rcases eq_or_ne z 0 with (rfl | hz)
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
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
replace hz := hz.lt_or_lt
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

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
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
wlog hxy : x ≤ y
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

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
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
rcases eq_or_ne x 0 with (rfl | hx0)
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

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
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
rcases eq_or_ne y 0 with (rfl | hy0)
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

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
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
induction x using ENNReal.recTopCoe
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

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
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
induction y using ENNReal.recTopCoe
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
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
simp only [*, false_and_iff, and_false_iff, false_or_iff, if_false]
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
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
norm_cast at *
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
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
rw [coe_rpow_of_ne_zero (mul_ne_zero hx0 hy0), NNReal.mul_rpow]
no goals
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
norm_cast
no goals
case inl
x y : ℝ≥0∞
⊢ (x * y) ^ 0 = if (x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0) ∧ 0 < 0 then ⊤ else x ^ 0 * y ^ 0
simp
no goals
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
convert this y x z hz (le_of_not_le hxy) using 2 <;> simp only [mul_comm, and_comm, or_comm]
no goals
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
induction y using ENNReal.recTopCoe <;> cases' hz with hz hz <;> simp [*, hz.not_lt]
no goals
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
exact (hx0 (bot_unique hxy)).elim
no goals
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
cases' hz with hz hz <;> simp [hz, top_unique hxy]
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
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
rw [ne_eq, coe_eq_zero] at hx0
no goals
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
cases' hz with hz hz <;> simp [*]