simp only [and_imp, Prod.forall, ← ENat.one_le_iff_pos]
case inl
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
x : ℕ
hforall : ∀ᶠ (c : ℕ∞ × ℕ∞) in 𝓝 (⊤, b), ↑x < c.1 ∧ 0 < c.2
⊢ ∀ (x_1 : ℕ∞ × ℕ∞), ↑x < x_1.1 ∧ 0 < x_1.2 → ↑x < x_1.1 * x_1.2
case inl
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
x : ℕ
hforall : ∀ᶠ (c : ℕ∞ × ℕ∞) in 𝓝 (⊤, b), ↑x < c.1 ∧ 0 < c.2
⊢ ∀ (a b : ℕ∞), ↑x < a → 1 ≤ b → ↑x < a * b