α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Zero α
inst✝¹ : Mul α
inst✝ : LT α
a b : WithTop α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ a * b ≠ ⊤
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Zero α
inst✝¹ : Mul α
inst✝ : LT α
a b : WithTop α
ha : a < ⊤
hb : b < ⊤
⊢ a * b < ⊤
rw [WithTop.lt_top_iff_ne_top] at *
no goals
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Zero α
inst✝¹ : Mul α
inst✝ : LT α
a b : WithTop α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ a * b ≠ ⊤
simp only [Ne.def, mul_eq_top_iff, *, and_false, false_and, false_or]