-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
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
hi :
  ∀ (a : (_ : α) × α),
    Membership.mem (γ := Finset ((_ : α) × α)) ((Ici x).sigma (α := fun (y : α) ↦ α) fun (y : α) ↦ Ici y) a →
      Membership.mem (α := (_ : α) × α) (γ := Finset ((_ : α) × α))
        ((Ici x).sigma (α := fun (z : α) ↦ α) fun (z : α) ↦ Icc x z)
        (match (motive := (_ : α) × α → (_ : α) × α) a with
          | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a :
          (_ : α) × α)
hj :
  ∀ (a : (_ : α) × α),
    Membership.mem (γ := Finset ((_ : α) × α)) ((Ici x).sigma (α := fun (z : α) ↦ α) fun (z : α) ↦ Icc x z) a →
      Membership.mem (α := (_ : α) × α) (γ := Finset ((_ : α) × α))
        ((Ici x).sigma (α := fun (y : α) ↦ α) fun (y : α) ↦ Ici y)
        (match (motive := (_ : α) × α → (_ : α) × α) a with
          | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a :
          (_ : α) × α)
left_neg :
  ∀ (a : (_ : α) × α),
    Membership.mem (γ := Finset ((_ : α) × α)) ((Ici x).sigma (α := fun (y : α) ↦ α) fun (y : α) ↦ Ici y) a →
      (match (motive := (_ : α) × α → (_ : α) × α)
          match (motive := (_ : α) × α → (_ : α) × α) a with
          | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a with
        | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a) =
        a
right_neg :
  ∀ (a : (_ : α) × α),
    Membership.mem (γ := Finset ((_ : α) × α)) ((Ici x).sigma (α := fun (z : α) ↦ α) fun (z : α) ↦ Icc x z) a →
      (match (motive := (_ : α) × α → (_ : α) × α)
          match (motive := (_ : α) × α → (_ : α) × α) a with
          | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a with
        | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a) =
        a
⊢ Eq.{u_2 + 1} (α := 𝕜)
    (∑ x_1 ∈ (Ici x).sigma (α := fun (y : α) ↦ α) fun (y : α) ↦ Ici y,
      if x_1.fst (β := fun (i : α) ↦ α) ≤ x_1.snd (β := fun (i : α) ↦ α) then
        HMul.hMul (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x (x_1.fst (β := fun (i : α) ↦ α)) : 𝕜)
          (f (x_1.snd (β := fun (i : α) ↦ α)))
      else 0)
    (∑ x_1 ∈ (Ici x).sigma (α := fun (z : α) ↦ α) fun (z : α) ↦ Icc x z,
      if x_1.snd (β := fun (i : α) ↦ α) ≤ x_1.fst (β := fun (i : α) ↦ α) then
        HMul.hMul (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x (x_1.snd (β := fun (i : α) ↦ α)) : 𝕜)
          (f (x_1.fst (β := fun (i : α) ↦ α)))
      else 0)
have h₁ : ∀ (a : (_ : α) × α),
  Membership.mem (γ := Finset ((_ : α) × α)) ((Ici x).sigma (α := fun (y : α) ↦ α) fun (y : α) ↦ Ici y) a →
    (if a.fst (β := fun (i : α) ↦ α) ≤ a.snd (β := fun (i : α) ↦ α) then
        HMul.hMul (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x (a.fst (β := fun (i : α) ↦ α)) : 𝕜)
          (f (a.snd (β := fun (i : α) ↦ α)))
      else 0) =
      if
          LE.le.{u_5} (α := α)
            (Sigma.snd (β := fun (i : α) ↦ α)
                (match (motive := (_ : α) × α → (_ : α) × α) a with
                | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a) :
              α)
            (Sigma.fst (β := fun (i : α) ↦ α)
                (match (motive := (_ : α) × α → (_ : α) × α) a with
                | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a) :
              α) then
        HMul.hMul (α := 𝕜)
          ((mu 𝕜 : (a : α) → α → 𝕜) x
              (Sigma.snd (β := fun (i : α) ↦ α)
                (match (motive := (_ : α) × α → (_ : α) × α) a with
                | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a)) :
            𝕜)
          (f
            (Sigma.fst (β := fun (i : α) ↦ α)
              (match (motive := (_ : α) × α → (_ : α) × α) a with
              | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a)))
      else 0
Tactic: apply sum_nbij' (fun ⟨a, b⟩ ↦ ⟨b, a⟩) (fun ⟨a, b⟩ ↦ ⟨b, a⟩)