-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem mul_rpow_eq_ite (x y : ℝ≥0∞) (z : ℝ) :
    (x * y) ^ z = if (x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0) ∧ z < 0 then ⊤ else x ^ z * y ^ z

Proof state:
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

Tactic:
simp only [*, if_false]

Result:
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 (False ∧ ↑x✝ = ⊤ ∨ ↑x✝¹ = ⊤ ∧ False) ∧ z < 0 then ⊤ else ↑x✝¹ ^ z * ↑x✝ ^ z

Proof state:
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

Tactic:
rcases hz with hz | hz <;> simp [*]

Result:
no goals

Proof state:
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

Tactic:
induction x

Result:
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

Proof state:
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

Tactic:
rcases hz with hz | hz <;> simp [hz, top_unique hxy]

Result:
no goals

Proof state:
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

Tactic:
rcases eq_or_ne x 0 with (rfl | hx0)

Result:
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

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

Tactic:
rcases eq_or_ne z 0 with (rfl | hz)

Result:
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

Proof state:
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

Tactic:
convert this y x z hz (le_of_not_le hxy) using 2 <;> simp only [mul_comm, and_comm, or_comm]

Result:
no goals

Proof state:
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

Tactic:
induction y

Result:
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

Proof state:
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

Tactic:
induction y <;> rcases hz with hz | hz <;> simp [*, hz.not_lt]

Result:
no goals

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

Tactic:
simp

Result:
no goals

Proof state:
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

Tactic:
rcases eq_or_ne y 0 with (rfl | hy0)

Result:
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

Proof state:
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) = if (False ∧ ↑x✝ = ⊤ ∨ ↑x✝¹ = ⊤ ∧ False) ∧ z < 0 then ⊤ else ↑x✝¹ ^ z * ↑x✝ ^ z

Tactic:
norm_cast

Result:
no goals

Proof state:
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 (False ∧ ↑x✝ = ⊤ ∨ ↑x✝¹ = ⊤ ∧ False) ∧ z < 0 then ⊤ else ↑x✝¹ ^ z * ↑x✝ ^ z

Tactic:
norm_cast at *

Result:
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 = if (False ∧ ↑x✝ = ⊤ ∨ ↑x✝¹ = ⊤ ∧ False) ∧ z < 0 then ⊤ else ↑x✝¹ ^ z * ↑x✝ ^ z

Proof state:
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

Tactic:
exact (hx0 (bot_unique hxy)).elim

Result:
no goals

Proof state:
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 = if (False ∧ ↑x✝ = ⊤ ∨ ↑x✝¹ = ⊤ ∧ False) ∧ z < 0 then ⊤ else ↑x✝¹ ^ z * ↑x✝ ^ z

Tactic:
rw [← coe_rpow_of_ne_zero (mul_ne_zero hx0 hy0), NNReal.mul_rpow]

Result:
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) = if (False ∧ ↑x✝ = ⊤ ∨ ↑x✝¹ = ⊤ ∧ False) ∧ z < 0 then ⊤ else ↑x✝¹ ^ z * ↑x✝ ^ z

Proof state:
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

Tactic:
rw [ne_eq, coe_eq_zero] at hx0

Result:
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

Proof state:
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

Tactic:
replace hz := hz.lt_or_lt

Result:
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

Proof state:
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

Tactic:
wlog hxy : x ≤ y

Result:
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