simp only [zeta_apply, one_mul, ite_mul]
case neg
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b : α
a✝ : a ≤ b
he : ¬a = b
⊢ ∑ x ∈ Icc a b, (zeta 𝕜) a x * (IncidenceAlgebra.mu' 𝕜) x b = 0
case neg
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b : α
a✝ : a ≤ b
he : ¬a = b
⊢ (∑ x ∈ Icc a b, if a ≤ x then (IncidenceAlgebra.mu' 𝕜) x b else 0 * (IncidenceAlgebra.mu' 𝕜) x b) = 0