case inl.inr.hx
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : x = 0 ∨ y = 0
h✝ : ¬z = 0
⊢ 0 ≤ x

case inr
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬(x = 0 ∨ y = 0)
⊢ exp (log (x * y) * z) = x ^ z * y ^ z

case hx
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
⊢ 0 ≤ x * y
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
⊢ (x * y) ^ z = x ^ z * y ^ z
iterate 2 rw [Real.rpow_def_of_nonneg]; split_ifs with h_ifs <;> simp_all
case inl.inr
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : x = 0 ∨ y = 0
h✝ : ¬z = 0
⊢ (if x = 0 then if z = 0 then 1 else 0 else exp (log x * z)) = 0 ∨ y ^ z = 0

case inl.inr.hx
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : x = 0 ∨ y = 0
h✝ : ¬z = 0
⊢ 0 ≤ x

case inr
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬(x = 0 ∨ y = 0)
⊢ exp (log (x * y) * z) = x ^ z * y ^ z

case hx
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
⊢ 0 ≤ x * y
case inl.inr
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : x = 0 ∨ y = 0
h✝ : ¬z = 0
⊢ x ^ z = 0 ∨ y ^ z = 0

case inr
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬(x = 0 ∨ y = 0)
⊢ exp (log (x * y) * z) = x ^ z * y ^ z

case hx
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
⊢ 0 ≤ x * y
rw [Real.rpow_def_of_nonneg]
case inl.inr.hx
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : x = 0 ∨ y = 0
h✝ : ¬z = 0
⊢ 0 ≤ x

case inr
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬(x = 0 ∨ y = 0)
⊢ exp (log (x * y) * z) = x ^ z * y ^ z

case hx
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
⊢ 0 ≤ x * y
case inl.inr
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : x = 0 ∨ y = 0
h✝ : ¬z = 0
⊢ (if x = 0 then if z = 0 then 1 else 0 else exp (log x * z)) = 0 ∨ y ^ z = 0

case inl.inr.hx
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : x = 0 ∨ y = 0
h✝ : ¬z = 0
⊢ 0 ≤ x

case inr
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬(x = 0 ∨ y = 0)
⊢ exp (log (x * y) * z) = x ^ z * y ^ z

case hx
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
⊢ 0 ≤ x * y
split_ifs with h_ifs <;> simp_all
no goals
case inl.inr.hx
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : x = 0 ∨ y = 0
h✝ : ¬z = 0
⊢ 0 ≤ x
exact h
case inr
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
⊢ exp (log (x * y) * z) = x ^ z * y ^ z
case inr
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬(x = 0 ∨ y = 0)
⊢ exp (log (x * y) * z) = x ^ z * y ^ z
rw [not_or] at h_ifs
no goals
case inr
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
hx : 0 < x
hy : 0 < y
⊢ exp (log (x * y) * z) = x ^ z * y ^ z
rw [log_mul (ne_of_gt hx) (ne_of_gt hy), add_mul, exp_add, rpow_def_of_pos hx,
  rpow_def_of_pos hy]
case inl
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
h₂ : 0 < x
⊢ 0 < x

case inr
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
h₂ : 0 = x
⊢ 0 < x
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
⊢ 0 < x
cases' lt_or_eq_of_le h with h₂ h₂
case inr.h
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
h₂ : 0 = x
⊢ False
case inr
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
h₂ : 0 = x
⊢ 0 < x
exfalso
case inr.h
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
h₂ : 0 = x
⊢ x = 0
case inr.h
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
h₂ : 0 = x
⊢ False
apply h_ifs.1
no goals
case inr.h
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
h₂ : 0 = x
⊢ x = 0
exact Eq.symm h₂
no goals
case inl
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
h₂ : 0 < x
⊢ 0 < x
exact h₂
case inl
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
hx : 0 < x
h₂ : 0 < y
⊢ 0 < y

case inr
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
hx : 0 < x
h₂ : 0 = y
⊢ 0 < y
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
hx : 0 < x
⊢ 0 < y
cases' lt_or_eq_of_le h₁ with h₂ h₂
case inr.h
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
hx : 0 < x
h₂ : 0 = y
⊢ False
case inr
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
hx : 0 < x
h₂ : 0 = y
⊢ 0 < y
exfalso
case inr.h
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
hx : 0 < x
h₂ : 0 = y
⊢ y = 0
case inr.h
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
hx : 0 < x
h₂ : 0 = y
⊢ False
apply h_ifs.2
no goals
case inr.h
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
hx : 0 < x
h₂ : 0 = y
⊢ y = 0
exact Eq.symm h₂
no goals
case inl
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
hx : 0 < x
h₂ : 0 < y
⊢ 0 < y
exact h₂
no goals
case hx
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
⊢ 0 ≤ x * y
exact mul_nonneg h h₁