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

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : α
ha : ¬a = 0
⊢ ↑(a * b) = ↑a * ↑b
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : α
⊢ ↑(a * b) = ↑a * ↑b
by_cases ha : a = 0
no goals
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : α
ha : a = 0
⊢ ↑(a * b) = ↑a * ↑b
simp [ha]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : α
ha : ¬a = 0
hb : b = 0
⊢ ↑(a * b) = ↑a * ↑b

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : α
ha : ¬a = 0
hb : ¬b = 0
⊢ ↑(a * b) = ↑a * ↑b
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : α
ha : ¬a = 0
⊢ ↑(a * b) = ↑a * ↑b
by_cases hb : b = 0
no goals
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : α
ha : ¬a = 0
hb : b = 0
⊢ ↑(a * b) = ↑a * ↑b
simp [hb]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : α
ha : ¬a = 0
hb : ¬b = 0
⊢ ↑(a * b) = Option.map₂ (fun x x_1 => x * x_1) ↑a ↑b
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : α
ha : ¬a = 0
hb : ¬b = 0
⊢ ↑(a * b) = ↑a * ↑b
simp [*, mul_def]
no goals
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : α
ha : ¬a = 0
hb : ¬b = 0
⊢ ↑(a * b) = Option.map₂ (fun x x_1 => x * x_1) ↑a ↑b
rfl