-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
o : Type u_3
inst_3 : Fintype o
inst_4 : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ : Perm (n × o) | ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
refine_1 :
  ∀ (a : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
    (ha : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ a),
    (fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
            (x : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ) ↦
          (prodCongrLeft fun (k : o) ↦ σ k ⋯ : n × o ≃ n × o))
        a ha ∈
      preserving_snd
refine_2 :
  ∀ (a₁ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
    (ha₁ : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ a₁)
    (a₂ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
    (ha₂ : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ a₂),
    Eq (α := n × o ≃ n × o)
        ((fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
              (x : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ) ↦
            (prodCongrLeft fun (k : o) ↦ σ k ⋯ : n × o ≃ n × o))
          a₁ ha₁)
        ((fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
              (x : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ) ↦
            (prodCongrLeft fun (k : o) ↦ σ k ⋯ : n × o ≃ n × o))
          a₂ ha₂) →
      a₁ = a₂
refine_3 :
  ∀ b ∈ preserving_snd,
    ∃ (a : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n) (ha :
      Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ a),
      (fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
              (x : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ) ↦
            (prodCongrLeft fun (k : o) ↦ σ k ⋯ : n × o ≃ n × o))
          a ha =
        b
refine_4 :
  ∀ (a : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
    (ha : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ a),
    ∏ x : o,
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (a x ⋯)) : ℤ) : R)
          (∏ x_1 : n, M x ((a x ⋯ : (a : n) → n) x_1) x_1) =
      HMul.hMul (α := R)
        (↑(↑(((sign : Perm (n × o) →* ℤˣ) : (a : Perm (n × o)) → ℤˣ)
                  ((fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
                        (x :
                          Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ
                            σ) ↦
                      (prodCongrLeft fun (k : o) ↦ σ k ⋯ : n × o ≃ n × o))
                    a ha)) :
              ℤ) :
          R)
        (∏ i : n × o,
          blockDiagonal M
            (((fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
                      (x :
                        Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ
                          σ) ↦
                    (prodCongrLeft fun (k : o) ↦ σ k ⋯ : n × o ≃ n × o))
                  a ha :
                (a : n × o) → n × o)
              i)
            i)
⊢ Eq.{v + 1} (α := R)
    (∑ x ∈ preserving_snd,
      HMul.hMul (α := R) (↑(↑(((sign : Perm (n × o) →* ℤˣ) : (a : Perm (n × o)) → ℤˣ) x) : ℤ) : R)
        (∏ i : n × o, blockDiagonal M ((x : (a : n × o) → n × o) i) i))
    (∑ x : (a : o) → a ∈ univ → Perm n,
      ∏ x_1 : o,
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (x x_1 ⋯)) : ℤ) : R)
          (∏ x_2 : n, M x_1 ((x x_1 ⋯ : (a : n) → n) x_2) x_2))

Tactic:
refine (Finset.sum_bij (fun σ _ => prodCongrLeft fun k ↦ σ k (mem_univ k)) ?_ ?_ ?_ ?_).symm

Premises used: Finset.sum_bij, Equiv.prodCongrLeft, Eq.symm