-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_blockDiagonal {o : Type*} [Fintype o] [DecidableEq o] (M : o → Matrix n n R) :
    (blockDiagonal M).det = ∏ k, (M k).det

Proof state:
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
⊢ ∑ σ : Perm (n × o), ↑↑(sign σ) * ∏ i : n × o, blockDiagonal M (σ i) i =
    ∑ x : (a : o) → a ∈ univ → Perm n, ∏ x_1 : o, ↑↑(sign (x x_1 ⋯)) * ∏ x_2 : n, M x_1 ((x x_1 ⋯) x_2) x_2

Tactic:
let preserving_snd : Finset (Equiv.Perm (n × o)) := {σ | ∀ x, (σ x).snd = x.snd}

Result:
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (σ x).2 = x.2) univ
⊢ ∑ σ : Perm (n × o), ↑↑(sign σ) * ∏ i : n × o, blockDiagonal M (σ i) i =
    ∑ x : (a : o) → a ∈ univ → Perm n, ∏ x_1 : o, ↑↑(sign (x x_1 ⋯)) * ∏ x_2 : n, M x_1 ((x x_1 ⋯) x_2) x_2

Proof state:
case refine_2.h.h.H
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (σ x).2 = x.2) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
σ : (a : o) → a ∈ univ → Perm n
ha₁✝ : σ ∈ univ
σ' : (a : o) → a ∈ univ → Perm n
ha₂✝ : σ' ∈ univ
eq : (prodCongrLeft fun k => σ k ⋯) = prodCongrLeft fun k => σ' k ⋯
x : o
hx : x ∈ univ
k : n
this : ∀ (k : n) (x : o), (prodCongrLeft fun k => σ k ⋯) (k, x) = (prodCongrLeft fun k => σ' k ⋯) (k, x)
⊢ (σ x hx) k = (σ' x hx) k

Tactic:
simp only [prodCongrLeft_apply, Prod.mk.inj_iff] at this

Result:
case refine_2.h.h.H
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (σ x).2 = x.2) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
σ : (a : o) → a ∈ univ → Perm n
ha₁✝ : σ ∈ univ
σ' : (a : o) → a ∈ univ → Perm n
ha₂✝ : σ' ∈ univ
eq : (prodCongrLeft fun k => σ k ⋯) = prodCongrLeft fun k => σ' k ⋯
x : o
hx : x ∈ univ
k : n
this : ∀ (k : n) (x : o), (σ x ⋯) k = (σ' x ⋯) k ∧ True
⊢ (σ x hx) k = (σ' x hx) k

Proof state:
case refine_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (σ x).2 = x.2) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
σ : (a : o) → a ∈ univ → Perm n
ha✝ : σ ∈ univ
⊢ ∀ (x : n × o), (((fun σ x => prodCongrLeft fun k => σ k ⋯) σ ha✝) x).2 = x.2

Tactic:
rintro ⟨-, x⟩

Result:
case refine_1.mk
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (σ x).2 = x.2) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
σ : (a : o) → a ∈ univ → Perm n
ha✝ : σ ∈ univ
fst✝ : n
x : o
⊢ (((fun σ x => prodCongrLeft fun k => σ k ⋯) σ ha✝) (fst✝, x)).2 = (fst✝, x).2

Proof state:
case refine_3
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (σ x).2 = x.2) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (σ x).2 = x.2
hσ' : ∀ (x : n × o), (σ⁻¹ x).2 = x.2
mk_apply_eq : ∀ (k : o) (x : n), ((σ (x, k)).1, k) = σ (x, k)
mk_inv_apply_eq : ∀ (k : o) (x : n), ((σ⁻¹ (x, k)).1, k) = σ⁻¹ (x, k)
⊢ ∃ a, ∃ (ha : a ∈ univ), (fun σ x => prodCongrLeft fun k => σ k ⋯) a ha = σ

Tactic:
refine ⟨fun k _ => ⟨fun x => (σ (x, k)).fst, fun x => (σ⁻¹ (x, k)).fst, ?_, ?_⟩, ?_, ?_⟩

Result:
case refine_3.refine_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (σ x).2 = x.2) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (σ x).2 = x.2
hσ' : ∀ (x : n × o), (σ⁻¹ x).2 = x.2
mk_apply_eq : ∀ (k : o) (x : n), ((σ (x, k)).1, k) = σ (x, k)
mk_inv_apply_eq : ∀ (k : o) (x : n), ((σ⁻¹ (x, k)).1, k) = σ⁻¹ (x, k)
k : o
x✝ : k ∈ univ
⊢ LeftInverse (fun x => (σ⁻¹ (x, k)).1) fun x => (σ (x, k)).1

case refine_3.refine_2
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (σ x).2 = x.2) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (σ x).2 = x.2
hσ' : ∀ (x : n × o), (σ⁻¹ x).2 = x.2
mk_apply_eq : ∀ (k : o) (x : n), ((σ (x, k)).1, k) = σ (x, k)
mk_inv_apply_eq : ∀ (k : o) (x : n), ((σ⁻¹ (x, k)).1, k) = σ⁻¹ (x, k)
k : o
x✝ : k ∈ univ
⊢ RightInverse (fun x => (σ⁻¹ (x, k)).1) fun x => (σ (x, k)).1

case refine_3.refine_3
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (σ x).2 = x.2) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (σ x).2 = x.2
hσ' : ∀ (x : n × o), (σ⁻¹ x).2 = x.2
mk_apply_eq : ∀ (k : o) (x : n), ((σ (x, k)).1, k) = σ (x, k)
mk_inv_apply_eq : ∀ (k : o) (x : n), ((σ⁻¹ (x, k)).1, k) = σ⁻¹ (x, k)
⊢ (fun k x => { toFun := fun x => (σ (x, k)).1, invFun := fun x => (σ⁻¹ (x, k)).1, left_inv := ⋯, right_inv := ⋯ }) ∈
    univ

case refine_3.refine_4
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (σ x).2 = x.2) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (σ x).2 = x.2
hσ' : ∀ (x : n × o), (σ⁻¹ x).2 = x.2
mk_apply_eq : ∀ (k : o) (x : n), ((σ (x, k)).1, k) = σ (x, k)
mk_inv_apply_eq : ∀ (k : o) (x : n), ((σ⁻¹ (x, k)).1, k) = σ⁻¹ (x, k)
⊢ (fun σ x => prodCongrLeft fun k => σ k ⋯)
      (fun k x => { toFun := fun x => (σ (x, k)).1, invFun := fun x => (σ⁻¹ (x, k)).1, left_inv := ⋯, right_inv := ⋯ })
      ?refine_3.refine_3 =
    σ