-- 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 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₁

Tactic:
rw [h]

Result:
no goals

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)))
⊢ (toMatrix B B) (pi fun i => f i ∘ₗ proj i) = blockDiagonal fun i => (toMatrix b b) (f i)

Tactic:
ext ⟨i₁, i₂⟩ ⟨j₁, j₂⟩

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 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₂)

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
⊢ LinearMap.det (pi fun i => f i ∘ₗ proj i) = ∏ i : ι, LinearMap.det (f i)

Tactic:
let b := Module.Free.chooseBasis R M

Result:
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
⊢ LinearMap.det (pi fun i => f i ∘ₗ proj i) = ∏ i : ι, LinearMap.det (f i)

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)))
⊢ LinearMap.det (pi fun i => f i ∘ₗ proj i) = ∏ i : ι, LinearMap.det (f i)

Tactic:
simp_rw [← LinearMap.det_toMatrix B, ← LinearMap.det_toMatrix b]

Result:
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)))
⊢ ((toMatrix B B) (pi fun i => f i ∘ₗ proj i)).det = ∏ x : ι, ((toMatrix b b) (f x)).det

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
⊢ LinearMap.det (pi fun i => f i ∘ₗ proj i) = ∏ i : ι, LinearMap.det (f i)

Tactic:
let B := (Pi.basis (fun _ : ι ↦ b)).reindex <|
  (Equiv.sigmaEquivProd _ _).trans (Equiv.prodComm _ _)

Result:
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)))
⊢ LinearMap.det (pi fun i => f i ∘ₗ proj i) = ∏ i : ι, LinearMap.det (f i)