-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidableEq α
inst_3 : Semiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
a b : α
h_1 : a ≤ b
h₁ :
  ∀ a_1 ∈ (Icc a b).sigma (α := fun (a : α) ↦ α) (Icc a),
    Membership.mem (α := (_ : α) × α) (γ := Finset ((_ : α) × α))
      ((Icc a b).sigma (α := fun (a : α) ↦ α) fun (a : α) ↦ Icc a b)
      (match (motive := (_ : α) × α → (_ : α) × α) a_1 with
        | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a :
        (_ : α) × α)
h₂ :
  ∀ (a_1 : (_ : α) × α),
    Membership.mem (γ := Finset ((_ : α) × α)) ((Icc a b).sigma (α := fun (a : α) ↦ α) fun (a : α) ↦ Icc a b) a_1 →
      Membership.mem (α := (_ : α) × α) ((Icc a b).sigma (α := fun (a : α) ↦ α) (Icc a))
        (match (motive := (_ : α) × α → (_ : α) × α) a_1 with
          | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a :
          (_ : α) × α)
h₃ :
  ∀ a_1 ∈ (Icc a b).sigma (α := fun (a : α) ↦ α) (Icc a),
    (match (motive := (_ : α) × α → (_ : α) × α)
        match (motive := (_ : α) × α → (_ : α) × α) a_1 with
        | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a with
      | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a) =
      a_1
h₄ :
  ∀ (a_1 : (_ : α) × α),
    Membership.mem (γ := Finset ((_ : α) × α)) ((Icc a b).sigma (α := fun (a : α) ↦ α) fun (a : α) ↦ Icc a b) a_1 →
      (match (motive := (_ : α) × α → (_ : α) × α)
          match (motive := (_ : α) × α → (_ : α) × α) a_1 with
          | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a with
        | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a) =
        a_1
h₅ :
  ∀ a_1 ∈ (Icc a b).sigma (α := fun (a : α) ↦ α) (Icc a),
    HMul.hMul (β := 𝕜)
        (HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : α) → α → 𝕜) a (a_1.snd (β := fun (i : α) ↦ α)) : 𝕜)
          ((g : (a : α) → α → 𝕜) (a_1.snd (β := fun (i : α) ↦ α)) (a_1.fst (β := fun (i : α) ↦ α)) : 𝕜))
        ((h : (a : α) → α → 𝕜) (a_1.fst (β := fun (i : α) ↦ α)) b : 𝕜) =
      HMul.hMul (α := 𝕜)
        ((f : (a : α) → α → 𝕜) a
            (Sigma.fst (β := fun (i : α) ↦ α)
              (match (motive := (_ : α) × α → (_ : α) × α) a_1 with
              | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a)) :
          𝕜)
        (HMul.hMul (α := 𝕜) (β := 𝕜)
          ((g : (a : α) → α → 𝕜)
              (Sigma.fst (β := fun (i : α) ↦ α)
                (match (motive := (_ : α) × α → (_ : α) × α) a_1 with
                | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a))
              (Sigma.snd (β := fun (i : α) ↦ α)
                (match (motive := (_ : α) × α → (_ : α) × α) a_1 with
                | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a)) :
            𝕜)
          ((h : (a : α) → α → 𝕜)
              (Sigma.snd (β := fun (i : α) ↦ α)
                  (match (motive := (_ : α) × α → (_ : α) × α) a_1 with
                  | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a) :
                α)
              b :
            𝕜))
⊢ Eq.{u_2 + 1} (α := 𝕜)
    (∑ x ∈ (Icc a b).sigma (α := fun (a : α) ↦ α) (Icc a),
      HMul.hMul (β := 𝕜)
        (HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : α) → α → 𝕜) a (x.snd (β := fun (i : α) ↦ α)) : 𝕜)
          ((g : (a : α) → α → 𝕜) (x.snd (β := fun (i : α) ↦ α)) (x.fst (β := fun (i : α) ↦ α)) : 𝕜))
        ((h : (a : α) → α → 𝕜) (x.fst (β := fun (i : α) ↦ α)) b : 𝕜))
    (∑ x ∈ (Icc a b).sigma (α := fun (a : α) ↦ α) fun (a : α) ↦ Icc a b,
      HMul.hMul (α := 𝕜) ((f : (a : α) → α → 𝕜) a (x.fst (β := fun (i : α) ↦ α)) : 𝕜)
        (HMul.hMul (α := 𝕜) (β := 𝕜)
          ((g : (a : α) → α → 𝕜) (x.fst (β := fun (i : α) ↦ α)) (x.snd (β := fun (i : α) ↦ α)) : 𝕜)
          ((h : (a : α) → α → 𝕜) (x.snd (β := fun (i : α) ↦ α)) b : 𝕜)))

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

Premises used: Finset.sum_nbij'