case inl
x✝ y✝ z✝ x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
⊢ x ^ y * x ^ z ≤ x ^ (y + z)

case inr
x✝ y✝ z✝ x : ℝ
hx : 0 ≤ x
y z : ℝ
pos : 0 < x
⊢ x ^ y * x ^ z ≤ x ^ (y + z)
x✝ y✝ z✝ x : ℝ
hx : 0 ≤ x
y z : ℝ
⊢ x ^ y * x ^ z ≤ x ^ (y + z)
rcases le_iff_eq_or_lt.1 hx with (H | pos)
case pos
x✝ y✝ z✝ x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
⊢ x ^ y * x ^ z ≤ x ^ (y + z)

case neg
x✝ y✝ z✝ x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : ¬y + z = 0
⊢ x ^ y * x ^ z ≤ x ^ (y + z)
case inl
x✝ y✝ z✝ x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
⊢ x ^ y * x ^ z ≤ x ^ (y + z)
by_cases h : y + z = 0
case pos
x✝ y✝ z✝ x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
⊢ 0 ^ y * 0 ^ z ≤ 1
case pos
x✝ y✝ z✝ x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
⊢ x ^ y * x ^ z ≤ x ^ (y + z)
simp only [H.symm, h, rpow_zero]
no goals
case pos
x✝ y✝ z✝ x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
⊢ 0 ^ y * 0 ^ z ≤ 1
calc
  (0 : ℝ) ^ y * 0 ^ z ≤ 1 * 1 :=
    mul_le_mul (zero_rpow_le_one y) (zero_rpow_le_one z) (zero_rpow_nonneg z) zero_le_one
  _ = 1 := by simp
no goals
x✝ y✝ z✝ x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
⊢ 1 * 1 = 1
simp
no goals
case neg
x✝ y✝ z✝ x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : ¬y + z = 0
⊢ x ^ y * x ^ z ≤ x ^ (y + z)
simp [rpow_add', ← H, h]
no goals
case inr
x✝ y✝ z✝ x : ℝ
hx : 0 ≤ x
y z : ℝ
pos : 0 < x
⊢ x ^ y * x ^ z ≤ x ^ (y + z)
simp [rpow_add pos]