-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ 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))
have 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 sorry)) : ℤ) : R)
        (∏ x_1 : n, M x ((a x sorry : (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 sorry : 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 sorry : n × o ≃ n × o))
                a ha :
              (a : n × o) → n × o)
            i)
          i)
Tactic: refine (Finset.sum_bij (fun σ _ => prodCongrLeft fun k ↦ σ k (mem_univ k)) ?_ ?_ ?_ ?_).symm