-- 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 : AddCommMonoid 𝕜
inst_3 : Monoid 𝕜
inst_4 : Semiring 𝕝
inst_5 : AddCommMonoid 𝕞
inst_6 : SMul 𝕜 𝕝
inst_7 : Module 𝕝 𝕞
inst_8 : DistribMulAction 𝕜 𝕞
inst_9 : IsScalarTower 𝕜 𝕝 𝕞
f : IncidenceAlgebra 𝕜 α
g : IncidenceAlgebra 𝕝 α
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),
    HSMul.hSMul (β := 𝕞)
        (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) (β := 𝕝) ((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 : 𝕞) =
      HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜)
        ((f : (a : α) → α → 𝕜) a
            (Sigma.fst (β := fun (i : α) ↦ α)
              (match (motive := (_ : α) × α → (_ : α) × α) a_1 with
              | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a)) :
          𝕜)
        (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕝) (β := 𝕞)
          ((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_4 + 1} (α := 𝕞)
    (∑ x ∈ (Icc a b).sigma (α := fun (a : α) ↦ α) (Icc a),
      HSMul.hSMul (β := 𝕞)
        (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) (β := 𝕝) ((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,
      HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜) ((f : (a : α) → α → 𝕜) a (x.fst (β := fun (i : α) ↦ α)) : 𝕜)
        (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕝) (β := 𝕞)
          ((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'