-- 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
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
⊢ ∀ x ∈ univ, x ∉ preserving_snd → ↑↑(sign x) * ∏ i : n × o, blockDiagonal M (x i) i = 0

Tactic:
intro σ _ hσ

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
σ : Perm (n × o)
a✝ : σ ∈ univ
hσ : σ ∉ preserving_snd
⊢ ↑↑(sign σ) * ∏ i : n × o, blockDiagonal M (σ i) i = 0

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σ : σ ∈ preserving_snd
⊢ ∃ a, ∃ (ha : a ∈ univ), (fun σ x => prodCongrLeft fun k => σ k ⋯) a ha = σ

Tactic:
rw [mem_preserving_snd] at hσ

Result:
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
⊢ ∃ a, ∃ (ha : a ∈ univ), (fun σ x => prodCongrLeft fun k => σ k ⋯) a ha = σ

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

Tactic:
exact hkx

Result:
no goals

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

Tactic:
simp only

Result:
no goals

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 : (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

Tactic:
simp only at eq

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
⊢ (σ x hx) k = (σ' x hx) k

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₁ : (a : o) → a ∈ univ → Perm n) (ha₁ : a₁ ∈ univ) (a₂ : (a : o) → a ∈ univ → Perm n) (ha₂ : a₂ ∈ univ),
    (fun σ x => prodCongrLeft fun k => σ k ⋯) a₁ ha₁ = (fun σ x => prodCongrLeft fun k => σ k ⋯) a₂ ha₂ → a₁ = a₂

Tactic:
intro σ _ σ' _ eq

Result:
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₂✝
⊢ σ = σ'

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
⊢ (σ x hx) k = (σ' x hx) k

Tactic:
have :
  ∀ k x,
    prodCongrLeft (fun k => σ k (Finset.mem_univ _)) (k, x) =
      prodCongrLeft (fun k => σ' k (Finset.mem_univ _)) (k, x) :=
  fun k x => by rw [eq]

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