-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A : Matrix n n R
i j : n
h : i ≠ j
f : (_ : n) × Perm n → (_ : n) × Perm n :=
  fun (x : (_ : n) × Perm n) ↦
    match (motive := (_ : n) × Perm n → (_ : n) × Perm n) x with
    | ⟨x, σ⟩ => Sigma.mk (β := fun (x : n) ↦ Perm n) ((σ : (a : n) → n) i) (σ * swap i j)
t : (s : ℤˣ) → Finset ((_ : n) × Perm n) :=
  fun (s : ℤˣ) ↦ Finset.sigma (α := fun (x : n) ↦ Perm n) univ fun (x : n) ↦ {σ ∈ ofSign s | (σ : (a : n) → n) j = x}
hf : ∀ {s : ℤˣ}, ∀ p ∈ t s, f (f p) = p
refine_1 :
  ∀ (a : (_ : n) × Perm n)
    (ha :
      Membership.mem (γ := Finset ((_ : n) × Perm n))
        (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦ {x ∈ ofSign 1 | (x : (a : n) → n) j = a}) a),
    Membership.mem (γ := Finset ((_ : n) × Perm n))
      (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦ {x ∈ ofSign (-1) | (x : (a : n) → n) j = a})
      ((fun (p : (_ : n) × Perm n)
            (x :
              Membership.mem (γ := Finset ((_ : n) × Perm n))
                (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦ {x ∈ ofSign 1 | (x : (a : n) → n) j = a})
                p) ↦
          f p)
        a ha)
refine_2 :
  ∀ (a : (_ : n) × Perm n)
    (ha :
      Membership.mem (γ := Finset ((_ : n) × Perm n))
        (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦ {x ∈ ofSign (-1) | (x : (a : n) → n) j = a}) a),
    Membership.mem (γ := Finset ((_ : n) × Perm n))
      (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦ {x ∈ ofSign 1 | (x : (a : n) → n) j = a})
      ((fun (p : (_ : n) × Perm n)
            (x :
              Membership.mem (γ := Finset ((_ : n) × Perm n))
                (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦
                  {x ∈ ofSign (-1) | (x : (a : n) → n) j = a})
                p) ↦
          f p)
        a ha)
refine_3 :
  ∀ (a : (_ : n) × Perm n)
    (ha :
      Membership.mem (γ := Finset ((_ : n) × Perm n))
        (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦ {x ∈ ofSign 1 | (x : (a : n) → n) j = a}) a),
    A i (a.fst (β := fun (i : n) ↦ Perm n)) * ∏ k ∈ {j}ᶜ, A k ((a.snd (β := fun (i : n) ↦ Perm n) : (a : n) → n) k) =
      A i
          (Sigma.fst (β := fun (i : n) ↦ Perm n)
            ((fun (p : (_ : n) × Perm n)
                  (x :
                    Membership.mem (γ := Finset ((_ : n) × Perm n))
                      (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦
                        {x ∈ ofSign 1 | (x : (a : n) → n) j = a})
                      p) ↦
                f p)
              a ha)) *
        ∏ k ∈ {j}ᶜ,
          A k
            (((Sigma.snd (β := fun (i : n) ↦ Perm n)
                    ((fun (p : (_ : n) × Perm n)
                          (x :
                            Membership.mem (γ := Finset ((_ : n) × Perm n))
                              (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦
                                {x ∈ ofSign 1 | (x : (a : n) → n) j = a})
                              p) ↦
                        f p)
                      a ha) :
                  Perm n) :
                (a : n) → n)
              k)
⊢ Eq.{u_3 + 1} (α := R)
    (∑ x ∈ Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦ {x ∈ ofSign 1 | (x : (a : n) → n) j = a},
      A i (x.fst (β := fun (i : n) ↦ Perm n)) * ∏ k ∈ {j}ᶜ, A k ((x.snd (β := fun (i : n) ↦ Perm n) : (a : n) → n) k))
    (∑ x ∈ Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦ {x ∈ ofSign (-1) | (x : (a : n) → n) j = a},
      A i (x.fst (β := fun (i : n) ↦ Perm n)) * ∏ k ∈ {j}ᶜ, A k ((x.snd (β := fun (i : n) ↦ Perm n) : (a : n) → n) k))

Tactic:
refine sum_bij' (fun p _ ↦ f p) (fun p _ ↦ f p) ?_ ?_ hf hf ?_

Premises used: Finset.sum_bij'