simp [mul_sum]
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
⊢ ∑ y ∈ Ici x, (mu 𝕜) x y * ∑ z ∈ Ici y, (zeta 𝕜) y z * f z = ∑ y ∈ Ici x, ∑ z ∈ Ici y, (mu 𝕜) x y * (zeta 𝕜) y z * f z
no goals