simp only [mul_boole, MulZeroClass.zero_mul, ite_mul, zeta_apply]
𝕄 : 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
⊢ ∑ x_1 ∈ (Ici x).sigma fun y => Ici y, (mu 𝕜) x x_1.fst * (zeta 𝕜) x_1.fst x_1.snd * f x_1.snd =
    ∑ x_1 ∈ (Ici x).sigma fun z => Icc x z, (mu 𝕜) x x_1.snd * (zeta 𝕜) x_1.snd x_1.fst * f x_1.fst
𝕄 : 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
⊢ (∑ x_1 ∈ (Ici x).sigma fun y => Ici y, if x_1.fst ≤ x_1.snd then (mu 𝕜) x x_1.fst * f x_1.snd else 0) =
    ∑ x_1 ∈ (Ici x).sigma fun z => Icc x z, if x_1.snd ≤ x_1.fst then (mu 𝕜) x x_1.snd * f x_1.fst else 0