-- 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:
case intro.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
σ : Perm (n × o)
a✝ : σ ∈ univ
hσ : ¬∀ (x : n × o), (σ x).2 = x.2
k : n
x : o
hkx : ¬(σ (k, x)).2 = (k, x).2
⊢ ↑↑(sign σ) * ∏ i : n × o, blockDiagonal M (σ i) i = 0

Tactic:
rw [Finset.prod_eq_zero (Finset.mem_univ (k, x)), mul_zero]

Result:
case intro.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
σ : Perm (n × o)
a✝ : σ ∈ univ
hσ : ¬∀ (x : n × o), (σ x).2 = x.2
k : n
x : o
hkx : ¬(σ (k, x)).2 = (k, x).2
⊢ blockDiagonal M (σ (k, x)) (k, x) = 0

Proof state:
case 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
⊢ ∀ (a : (a : o) → a ∈ univ → Perm n) (ha : a ∈ univ),
    ∏ x : o, ↑↑(sign (a x ⋯)) * ∏ x_1 : n, M x ((a x ⋯) x_1) x_1 =
      ↑↑(sign ((fun σ x => prodCongrLeft fun k => σ k ⋯) a ha)) *
        ∏ i : n × o, blockDiagonal M (((fun σ x => prodCongrLeft fun k => σ k ⋯) a ha) i) i

Tactic:
intro σ _

Result:
case 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
σ : (a : o) → a ∈ univ → Perm n
ha✝ : σ ∈ univ
⊢ ∏ x : o, ↑↑(sign (σ x ⋯)) * ∏ x_1 : n, M x ((σ x ⋯) x_1) x_1 =
    ↑↑(sign ((fun σ x => prodCongrLeft fun k => σ k ⋯) σ ha✝)) *
      ∏ i : n × o, blockDiagonal M (((fun σ x => prodCongrLeft fun k => σ k ⋯) σ ha✝) i) i

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
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
⊢ ∀ (x : n × o), (σ⁻¹ x).2 = x.2

Tactic:
intro x

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
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
x : n × o
⊢ (σ⁻¹ x).2 = x.2

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
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)
k : o
x : n
⊢ ((σ⁻¹ (σ (σ⁻¹ (x, k)))).1, k) = σ⁻¹ (x, k)

Tactic:
ext

Result:
case fst
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)
k : o
x : n
⊢ ((σ⁻¹ (σ (σ⁻¹ (x, k)))).1, k).1 = (σ⁻¹ (x, k)).1

case snd
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)
k : o
x : n
⊢ ((σ⁻¹ (σ (σ⁻¹ (x, k)))).1, k).2 = (σ⁻¹ (x, k)).2

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
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✝ k : n
x : o
⊢ (prodCongrLeft fun k => σ k ⋯) (k, x) = (prodCongrLeft fun k => σ' k ⋯) (k, x)

Tactic:
rw [eq]

Result:
no goals

Proof state:
case 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
σ : (a : o) → a ∈ univ → Perm n
ha₁✝ : σ ∈ univ
σ' : (a : o) → a ∈ univ → Perm n
ha₂✝ : σ' ∈ univ
eq : (fun σ x => prodCongrLeft fun k => σ k ⋯) σ ha₁✝ = (fun σ x => prodCongrLeft fun k => σ k ⋯) σ' ha₂✝
⊢ σ = σ'

Tactic:
ext x hx k

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 : (fun σ x => prodCongrLeft fun k => σ k ⋯) σ ha₁✝ = (fun σ x => prodCongrLeft fun k => σ k ⋯) σ' ha₂✝
x : o
hx : x ∈ univ
k : n
⊢ (σ x hx) k = (σ' x hx) k