Theorem: ENat.iSup_mul (Matroid/ForMathlib/ENatTopology.lean)

State before:
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
ι : Sort u_4
c : ℕ∞
f : ι → ℕ∞
⊢ (⨆ i, f i) * c = ⨆ i, f i * c
Tactic:
simp_rw [mul_comm, ENat.mul_iSup]
State after:
no goals