-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : OrderTop α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
y :
  Eq.{u_2 + 1} (α := 𝕜) (∑ y ∈ Ici x, HMul.hMul (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) (g y))
    (∑ y ∈ Ici x, HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) (∑ z ∈ Ici y, f z : 𝕜))
y₁ :
  Eq.{u_2 + 1} (α := 𝕜)
    (∑ y ∈ Ici x, HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) (∑ z ∈ Ici y, f z : 𝕜))
    (∑ y ∈ Ici x,
      HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜)
        (∑ z ∈ Ici y, HMul.hMul (α := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) y z : 𝕜) (f z) : 𝕜))
y₂ :
  Eq.{u_2 + 1} (α := 𝕜)
    (∑ y ∈ Ici x,
      HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜)
        (∑ z ∈ Ici y, HMul.hMul (α := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) y z : 𝕜) (f z) : 𝕜))
    (∑ y ∈ Ici x,
      ∑ z ∈ Ici y,
        HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) y z : 𝕜) * f z)
y₃ :
  Eq.{u_2 + 1} (α := 𝕜)
    (∑ y ∈ Ici x,
      ∑ z ∈ Ici y,
        HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) y z : 𝕜) * f z)
    (∑ z ∈ Ici x,
      ∑ y ∈ Icc x z,
        HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) y z : 𝕜) * f z)
y₄ :
  Eq.{u_2 + 1} (α := 𝕜)
    (∑ z ∈ Ici x,
      ∑ y ∈ Icc x z,
        HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) y z : 𝕜) * f z)
    (∑ z ∈ Ici x,
      HMul.hMul (α := 𝕜) ((HMul.hMul (α := IncidenceAlgebra 𝕜 α) (mu 𝕜) (zeta 𝕜) : (a : α) → α → 𝕜) x z : 𝕜) (f z))
y₅ :
  Eq.{u_2 + 1} (α := 𝕜)
    (∑ z ∈ Ici x,
      HMul.hMul (α := 𝕜) ((HMul.hMul (α := IncidenceAlgebra 𝕜 α) (mu 𝕜) (zeta 𝕜) : (a : α) → α → 𝕜) x z : 𝕜) (f z))
    (∑ y ∈ Ici x, ∑ z ∈ Ici y, HMul.hMul (α := 𝕜) ((1 : (a : α) → α → 𝕜) x z : 𝕜) (f z))
y₆ : ∑ y ∈ Ici x, ∑ z ∈ Ici y, HMul.hMul (α := 𝕜) ((1 : (a : α) → α → 𝕜) x z : 𝕜) (f z) = f x
⊢ ∑ y ∈ Ici x, HMul.hMul (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) (g y) = f x

Tactic:
calc
    ∑ y ∈ Ici x, mu 𝕜 x y * g y = ∑ y ∈ Ici x, mu 𝕜 x y * ∑ z ∈ Ici y, f z := by simp_rw [h]
    _ = ∑ y ∈ Ici x, mu 𝕜 x y * ∑ z ∈ 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 ∈ Ici x, ∑ z ∈ Ici y, mu 𝕜 x y * zeta 𝕜 y z * f z := by simp [mul_sum]
    _ = ∑ z ∈ Ici x, ∑ y ∈ Icc x z, mu 𝕜 x y * zeta 𝕜 y z * f z := by
      rw [sum_sigma' (Ici x) fun y ↦ Ici y]
      rw [sum_sigma' (Ici x) fun z ↦ Icc x z]
      simp only [mul_boole, 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 ∈ Ici x, (mu 𝕜 * zeta 𝕜 : IncidenceAlgebra 𝕜 α) x z * f z := by
      simp_rw [mul_apply, sum_mul]
    _ = ∑ y ∈ Ici x, ∑ z ∈ Ici y, (1 : IncidenceAlgebra 𝕜 α) x z * f z := by
      simp only [mu_mul_zeta 𝕜, one_apply, ite_mul, one_mul, zero_mul, sum_ite_eq, mem_Ici, le_refl,
        ↓reduceIte, ← add_sum_Ioi_eq_sum_Ici, left_eq_add]
      exact sum_eq_zero fun y hy ↦ if_neg (mem_Ioi.mp hy).not_ge
    _ = f x := by
      simp only [one_apply, ite_mul, one_mul, zero_mul, sum_ite_eq, mem_Ici,
        ← add_sum_Ioi_eq_sum_Ici, le_refl, ↓reduceIte, add_eq_left]
      exact sum_eq_zero fun y hy ↦ if_neg (mem_Ioi.mp hy).not_ge

Premises used: Finset.Ici