case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : a = 0
⊢ untop' 0 (a * b) = untop' 0 a * untop' 0 b

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
⊢ untop' 0 (a * b) = untop' 0 a * untop' 0 b
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
⊢ untop' 0 (a * b) = untop' 0 a * untop' 0 b
by_cases ha : a = 0
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
hb : b = 0
⊢ untop' 0 (a * b) = untop' 0 a * untop' 0 b

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
hb : ¬b = 0
⊢ untop' 0 (a * b) = untop' 0 a * untop' 0 b
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
⊢ untop' 0 (a * b) = untop' 0 a * untop' 0 b
by_cases hb : b = 0
case neg.top
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithTop α
hb : ¬b = 0
ha : ¬⊤ = 0
⊢ untop' 0 (⊤ * b) = untop' 0 ⊤ * untop' 0 b

case neg.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithTop α
hb : ¬b = 0
a✝ : α
ha : ¬↑a✝ = 0
⊢ untop' 0 (↑a✝ * b) = untop' 0 ↑a✝ * untop' 0 b
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
hb : ¬b = 0
⊢ untop' 0 (a * b) = untop' 0 a * untop' 0 b
induction a using WithTop.recTopCoe
case neg.coe.top
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
ha : ¬↑a✝ = 0
hb : ¬⊤ = 0
⊢ untop' 0 (↑a✝ * ⊤) = untop' 0 ↑a✝ * untop' 0 ⊤

case neg.coe.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝¹ : α
ha : ¬↑a✝¹ = 0
a✝ : α
hb : ¬↑a✝ = 0
⊢ untop' 0 (↑a✝¹ * ↑a✝) = untop' 0 ↑a✝¹ * untop' 0 ↑a✝
case neg.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithTop α
hb : ¬b = 0
a✝ : α
ha : ¬↑a✝ = 0
⊢ untop' 0 (↑a✝ * b) = untop' 0 ↑a✝ * untop' 0 b
induction b using WithTop.recTopCoe
no goals
case neg.coe.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝¹ : α
ha : ¬↑a✝¹ = 0
a✝ : α
hb : ¬↑a✝ = 0
⊢ untop' 0 (↑a✝¹ * ↑a✝) = untop' 0 ↑a✝¹ * untop' 0 ↑a✝
rw [← coe_mul, untop'_coe, untop'_coe, untop'_coe]
no goals
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : a = 0
⊢ untop' 0 (a * b) = untop' 0 a * untop' 0 b
rw [ha, zero_mul, ← coe_zero, untop'_coe, zero_mul]
no goals
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
hb : b = 0
⊢ untop' 0 (a * b) = untop' 0 a * untop' 0 b
rw [hb, mul_zero, ← coe_zero, untop'_coe, mul_zero]
no goals
case neg.top
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithTop α
hb : ¬b = 0
ha : ¬⊤ = 0
⊢ untop' 0 (⊤ * b) = untop' 0 ⊤ * untop' 0 b
rw [top_mul hb, untop'_top, zero_mul]
no goals
case neg.coe.top
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
ha : ¬↑a✝ = 0
hb : ¬⊤ = 0
⊢ untop' 0 (↑a✝ * ⊤) = untop' 0 ↑a✝ * untop' 0 ⊤
rw [mul_top ha, untop'_top, mul_zero]