-- 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
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
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
⊢ 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)

Tactic:
apply sum_nbij' (fun ⟨a, b⟩ ↦ ⟨b, a⟩) (fun ⟨a, b⟩ ↦ ⟨b, a⟩)

Premises used: Finset.sum_nbij'