calc
  ∑ y in Ici x, mu 𝕜 x y * g y = ∑ y in Ici x, mu 𝕜 x y * ∑ z in Ici y, f z := by simp_rw [h]
  _ = ∑ y in Ici x, mu 𝕜 x y * ∑ z in Ici y, zeta 𝕜 y z * f z := by
    congr with y
    rw [sum_congr rfl fun z hz ↦ ?_]
    rw [zeta_apply, if_pos (mem_Ici.mp ‹_›), one_mul]
  _ = ∑ y in Ici x, ∑ z in Ici y, mu 𝕜 x y * zeta 𝕜 y z * f z := by simp [mul_sum]
  _ = ∑ z in Ici x, ∑ y in Icc x z, mu 𝕜 x y * zeta 𝕜 y z * f z := by
    erw [sum_sigma' (Ici x) fun y ↦ Ici y]
    erw [sum_sigma' (Ici x) fun z ↦ Icc x z]
    simp only [mul_boole, MulZeroClass.zero_mul, ite_mul, zeta_apply]
    apply sum_nbij' (fun ⟨a, b⟩ ↦ ⟨b, a⟩) (fun ⟨a, b⟩ ↦ ⟨b, a⟩) <;>
      aesop (add simp mul_assoc) (add unsafe le_trans)
  _ = ∑ z in Ici x, (mu 𝕜 * zeta 𝕜 : IncidenceAlgebra 𝕜 α) x z * f z := by
    simp_rw [mul_apply, sum_mul]
  _ = ∑ y in Ici x, ∑ z in Ici y, (1 : IncidenceAlgebra 𝕜 α) x z * f z := by
    simp [mu_mul_zeta 𝕜, ← add_sum_Ioi]
    exact sum_eq_zero fun y hy ↦ if_neg (mem_Ioi.mp hy).not_le
  _ = f x := by
    simp [one_apply, ← add_sum_Ioi]
    exact sum_eq_zero fun y hy ↦ if_neg (mem_Ioi.mp hy).not_le
𝕄 : 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 * g y = f x
no goals