α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Zero α
inst✝ : Mul α
⊢ Option.map₂ (fun x x_1 => x * x_1) ⊤ ⊤ = ⊤
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Zero α
inst✝ : Mul α
⊢ ⊤ * ⊤ = ⊤
simp [mul_def]
no goals
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Zero α
inst✝ : Mul α
⊢ Option.map₂ (fun x x_1 => x * x_1) ⊤ ⊤ = ⊤
rfl