no goals
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : α
hb : b ≠ 0
⊢ (if ⊤ = 0 ∨ ↑b = 0 then 0 else ⊤) = ⊤
simp [hb]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : α
hb : b ≠ 0
a : α
⊢ ↑(a * b) = Option.bind ↑a fun a => Option.some (a * b)
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : α
hb : b ≠ 0
a : α
⊢ Option.some a * ↑b = Option.bind (Option.some a) fun a => Option.some (a * b)
rw [some_eq_coe, ← coe_mul]
no goals
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : α
hb : b ≠ 0
a : α
⊢ ↑(a * b) = Option.bind ↑a fun a => Option.some (a * b)
rfl