-- Mathlib/LinearAlgebra/Determinant.lean
theorem det_pi [Module.Free R M] [Module.Finite R M] (f : ι → M →ₗ[R] M) :
    (LinearMap.pi (fun i ↦ (f i).comp (LinearMap.proj i))).det = ∏ i, (f i).det

Proof state:
case a.mk.mk
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Module.Free.ChooseBasisIndex R M) R M := Module.Free.chooseBasis R M
B : Basis (Module.Free.ChooseBasisIndex R M × ι) R (ι → M) :=
  (Pi.basis fun x => b).reindex
    ((Equiv.sigmaEquivProd ι (Module.Free.ChooseBasisIndex R M)).trans
      (Equiv.prodComm ι (Module.Free.ChooseBasisIndex R M)))
i₁ : Module.Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Module.Free.ChooseBasisIndex R M
j₂ : ι
⊢ (b.repr ((f i₂) (if i₂ = j₂ then b j₁ else 0))) i₁ = if i₂ = j₂ then (b.repr ((f i₂) (b j₁))) i₁ else 0

Tactic:
split_ifs with h

Result:
case pos
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Module.Free.ChooseBasisIndex R M) R M := Module.Free.chooseBasis R M
B : Basis (Module.Free.ChooseBasisIndex R M × ι) R (ι → M) :=
  (Pi.basis fun x => b).reindex
    ((Equiv.sigmaEquivProd ι (Module.Free.ChooseBasisIndex R M)).trans
      (Equiv.prodComm ι (Module.Free.ChooseBasisIndex R M)))
i₁ : Module.Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Module.Free.ChooseBasisIndex R M
j₂ : ι
h : i₂ = j₂
⊢ (b.repr ((f i₂) (b j₁))) i₁ = (b.repr ((f i₂) (b j₁))) i₁

case neg
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Module.Free.ChooseBasisIndex R M) R M := Module.Free.chooseBasis R M
B : Basis (Module.Free.ChooseBasisIndex R M × ι) R (ι → M) :=
  (Pi.basis fun x => b).reindex
    ((Equiv.sigmaEquivProd ι (Module.Free.ChooseBasisIndex R M)).trans
      (Equiv.prodComm ι (Module.Free.ChooseBasisIndex R M)))
i₁ : Module.Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Module.Free.ChooseBasisIndex R M
j₂ : ι
h : ¬i₂ = j₂
⊢ (b.repr ((f i₂) 0)) i₁ = 0

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Module.Free.ChooseBasisIndex R M) R M := Module.Free.chooseBasis R M
B : Basis (Module.Free.ChooseBasisIndex R M × ι) R (ι → M) :=
  (Pi.basis fun x => b).reindex
    ((Equiv.sigmaEquivProd ι (Module.Free.ChooseBasisIndex R M)).trans
      (Equiv.prodComm ι (Module.Free.ChooseBasisIndex R M)))
this : (toMatrix B B) (pi fun i => f i ∘ₗ proj i) = blockDiagonal fun i => (toMatrix b b) (f i)
⊢ ((toMatrix B B) (pi fun i => f i ∘ₗ proj i)).det = ∏ x : ι, ((toMatrix b b) (f x)).det

Tactic:
rw [this, Matrix.det_blockDiagonal]

Result:
no goals

Proof state:
case a.mk.mk
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Module.Free.ChooseBasisIndex R M) R M := Module.Free.chooseBasis R M
B : Basis (Module.Free.ChooseBasisIndex R M × ι) R (ι → M) :=
  (Pi.basis fun x => b).reindex
    ((Equiv.sigmaEquivProd ι (Module.Free.ChooseBasisIndex R M)).trans
      (Equiv.prodComm ι (Module.Free.ChooseBasisIndex R M)))
i₁ : Module.Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Module.Free.ChooseBasisIndex R M
j₂ : ι
⊢ (toMatrix
        ((Pi.basis fun x => b).reindex
          ((Equiv.sigmaEquivProd ι (Module.Free.ChooseBasisIndex R M)).trans
            (Equiv.prodComm ι (Module.Free.ChooseBasisIndex R M))))
        ((Pi.basis fun x => b).reindex
          ((Equiv.sigmaEquivProd ι (Module.Free.ChooseBasisIndex R M)).trans
            (Equiv.prodComm ι (Module.Free.ChooseBasisIndex R M)))))
      (pi fun i => f i ∘ₗ proj i) (i₁, i₂) (j₁, j₂) =
    blockDiagonal (fun i => (toMatrix b b) (f i)) (i₁, i₂) (j₁, j₂)

Tactic:
simp_rw [LinearMap.toMatrix_apply', Matrix.blockDiagonal_apply, Basis.coe_reindex,
  Function.comp_apply, Basis.repr_reindex_apply, Equiv.symm_trans_apply, Equiv.prodComm_symm,
  Equiv.prodComm_apply, Equiv.sigmaEquivProd_symm_apply, Prod.swap_prod_mk, Pi.basis_apply,
  Pi.basis_repr, LinearMap.pi_apply, LinearMap.coe_comp, Function.comp_apply,
  LinearMap.toMatrix_apply', LinearMap.coe_proj, Function.eval, Pi.single_apply]

Result:
case a.mk.mk
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Module.Free.ChooseBasisIndex R M) R M := Module.Free.chooseBasis R M
B : Basis (Module.Free.ChooseBasisIndex R M × ι) R (ι → M) :=
  (Pi.basis fun x => b).reindex
    ((Equiv.sigmaEquivProd ι (Module.Free.ChooseBasisIndex R M)).trans
      (Equiv.prodComm ι (Module.Free.ChooseBasisIndex R M)))
i₁ : Module.Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Module.Free.ChooseBasisIndex R M
j₂ : ι
⊢ (b.repr ((f i₂) (if i₂ = j₂ then b j₁ else 0))) i₁ = if i₂ = j₂ then (b.repr ((f i₂) (b j₁))) i₁ else 0

Proof state:
case neg
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Module.Free.ChooseBasisIndex R M) R M := Module.Free.chooseBasis R M
B : Basis (Module.Free.ChooseBasisIndex R M × ι) R (ι → M) :=
  (Pi.basis fun x => b).reindex
    ((Equiv.sigmaEquivProd ι (Module.Free.ChooseBasisIndex R M)).trans
      (Equiv.prodComm ι (Module.Free.ChooseBasisIndex R M)))
i₁ : Module.Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Module.Free.ChooseBasisIndex R M
j₂ : ι
h : ¬i₂ = j₂
⊢ (b.repr ((f i₂) 0)) i₁ = 0

Tactic:
simp only [map_zero, Finsupp.coe_zero, Pi.zero_apply]

Result:
no goals

Proof state:
case a.mk.mk
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Module.Free.ChooseBasisIndex R M) R M := Module.Free.chooseBasis R M
B : Basis (Module.Free.ChooseBasisIndex R M × ι) R (ι → M) :=
  (Pi.basis fun x => b).reindex
    ((Equiv.sigmaEquivProd ι (Module.Free.ChooseBasisIndex R M)).trans
      (Equiv.prodComm ι (Module.Free.ChooseBasisIndex R M)))
i₁ : Module.Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Module.Free.ChooseBasisIndex R M
j₂ : ι
⊢ (toMatrix B B) (pi fun i => f i ∘ₗ proj i) (i₁, i₂) (j₁, j₂) =
    blockDiagonal (fun i => (toMatrix b b) (f i)) (i₁, i₂) (j₁, j₂)

Tactic:
unfold B

Result:
case a.mk.mk
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Module.Free.ChooseBasisIndex R M) R M := Module.Free.chooseBasis R M
B : Basis (Module.Free.ChooseBasisIndex R M × ι) R (ι → M) :=
  (Pi.basis fun x => b).reindex
    ((Equiv.sigmaEquivProd ι (Module.Free.ChooseBasisIndex R M)).trans
      (Equiv.prodComm ι (Module.Free.ChooseBasisIndex R M)))
i₁ : Module.Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Module.Free.ChooseBasisIndex R M
j₂ : ι
⊢ (toMatrix
        ((Pi.basis fun x => b).reindex
          ((Equiv.sigmaEquivProd ι (Module.Free.ChooseBasisIndex R M)).trans
            (Equiv.prodComm ι (Module.Free.ChooseBasisIndex R M))))
        ((Pi.basis fun x => b).reindex
          ((Equiv.sigmaEquivProd ι (Module.Free.ChooseBasisIndex R M)).trans
            (Equiv.prodComm ι (Module.Free.ChooseBasisIndex R M)))))
      (pi fun i => f i ∘ₗ proj i) (i₁, i₂) (j₁, j₂) =
    blockDiagonal (fun i => (toMatrix b b) (f i)) (i₁, i₂) (j₁, j₂)