simp [he]
case pos
𝕄 : 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, (mu 𝕜) a x * (zeta 𝕜) x b = 1
no goals