Theorem: ENat.Tendsto.const_mul (Matroid/ForMathlib/ENatTopology.lean)

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f : Filter α
m : α → ℕ∞
a b : ℕ∞
hm : Tendsto m f (𝓝 b)
hb : b ≠ 0 ∨ a ≠ ⊤
this : a = 0
⊢ Tendsto (fun b => a * m b) f (𝓝 (a * b))
Tactic:
simp [this, tendsto_const_nhds]
State after:
no goals