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 ⊤
y : ℝ
⊢ 0 ^ y * 0 ^ y = 0 ^ y
rw [zero_rpow_def]
case inl
y : ℝ
h✝ : 0 < y
⊢ 0 * 0 = 0

case inr.inl
y : ℝ
h✝¹ : ¬0 < y
h✝ : y = 0
⊢ 1 * 1 = 1

case inr.inr
y : ℝ
h✝¹ : ¬0 < y
h✝ : ¬y = 0
⊢ ⊤ * ⊤ = ⊤
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 ⊤
split_ifs
no goals
case inl
y : ℝ
h✝ : 0 < y
⊢ 0 * 0 = 0

case inr.inl
y : ℝ
h✝¹ : ¬0 < y
h✝ : y = 0
⊢ 1 * 1 = 1

case inr.inr
y : ℝ
h✝¹ : ¬0 < y
h✝ : ¬y = 0
⊢ ⊤ * ⊤ = ⊤
exacts [MulZeroClass.zero_mul _, one_mul _, top_mul_top]