awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_4
inst_3 : Fintype ι
inst_4 : Free R M
inst_5 : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R ((j : ι) → M) :=
  Basis.reindex (Pi.basis (ιs := fun (x : ι) ↦ Free.ChooseBasisIndex R M) (Ms := fun (x : ι) ↦ M) fun (x : ι) ↦ b)
    (Equiv.trans (Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)) (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
i₁ : Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Free.ChooseBasisIndex R M
j₂ : ι
⊢ Eq.{u_1 + 1} (α := R)
    ((((b.repr : (a : M) → Free.ChooseBasisIndex R M →₀ R)
              ((f i₂ : (a : M) → M) (if i₂ = j₂ then (b : (a : Free.ChooseBasisIndex R M) → M) j₁ else 0 : M)) :
            Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R M) R) :
          (a : Free.ChooseBasisIndex R M) → R)
        i₁ :
      R)
    (if i₂ = j₂ then
        (((b.repr : (a : M) → Free.ChooseBasisIndex R M →₀ R)
                ((f i₂ : (a : M) → M) ((b : (a : Free.ChooseBasisIndex R M) → M) j₁ : M)) :
              Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R M) R) :
            (a : Free.ChooseBasisIndex R M) → R)
          i₁
      else 0 :
      R)
have pos : ∀ (h : i₂ = j₂),
  Eq.{u_1 + 1} (α := R)
    ((((b.repr : (a : M) → Free.ChooseBasisIndex R M →₀ R)
              ((f i₂ : (a : M) → M) ((b : (a : Free.ChooseBasisIndex R M) → M) j₁ : M)) :
            Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R M) R) :
          (a : Free.ChooseBasisIndex R M) → R)
        i₁ :
      R)
    ((((b.repr : (a : M) → Free.ChooseBasisIndex R M →₀ R)
              ((f i₂ : (a : M) → M) ((b : (a : Free.ChooseBasisIndex R M) → M) j₁ : M)) :
            Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R M) R) :
          (a : Free.ChooseBasisIndex R M) → R)
        i₁ :
      R)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_4
inst_3 : Fintype ι
inst_4 : Free R M
inst_5 : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R ((j : ι) → M) :=
  Basis.reindex (Pi.basis (ιs := fun (x : ι) ↦ Free.ChooseBasisIndex R M) (Ms := fun (x : ι) ↦ M) fun (x : ι) ↦ b)
    (Equiv.trans (Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)) (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
i₁ : Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Free.ChooseBasisIndex R M
j₂ : ι
pos :
  ∀ (h : i₂ = j₂),
    Eq.{u_1 + 1} (α := R)
      ((((b.repr : (a : M) → Free.ChooseBasisIndex R M →₀ R)
                ((f i₂ : (a : M) → M) ((b : (a : Free.ChooseBasisIndex R M) → M) j₁ : M)) :
              Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R M) R) :
            (a : Free.ChooseBasisIndex R M) → R)
          i₁ :
        R)
      ((((b.repr : (a : M) → Free.ChooseBasisIndex R M →₀ R)
                ((f i₂ : (a : M) → M) ((b : (a : Free.ChooseBasisIndex R M) → M) j₁ : M)) :
              Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R M) R) :
            (a : Free.ChooseBasisIndex R M) → R)
          i₁ :
        R)
⊢ Eq.{u_1 + 1} (α := R)
    ((((b.repr : (a : M) → Free.ChooseBasisIndex R M →₀ R)
              ((f i₂ : (a : M) → M) (if i₂ = j₂ then (b : (a : Free.ChooseBasisIndex R M) → M) j₁ else 0 : M)) :
            Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R M) R) :
          (a : Free.ChooseBasisIndex R M) → R)
        i₁ :
      R)
    (if i₂ = j₂ then
        (((b.repr : (a : M) → Free.ChooseBasisIndex R M →₀ R)
                ((f i₂ : (a : M) → M) ((b : (a : Free.ChooseBasisIndex R M) → M) j₁ : M)) :
              Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R M) R) :
            (a : Free.ChooseBasisIndex R M) → R)
          i₁
      else 0 :
      R)
have neg : ∀ (h : ¬i₂ = j₂),
  Eq.{u_1 + 1} (α := R)
    ((((b.repr : (a : M) → Free.ChooseBasisIndex R M →₀ R) ((f i₂ : (a : M) → M) 0) :
            Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R M) R) :
          (a : Free.ChooseBasisIndex R M) → R)
        i₁ :
      R)
    (0 : R)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_4
inst_3 : Fintype ι
inst_4 : Free R M
inst_5 : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R ((j : ι) → M) :=
  Basis.reindex (Pi.basis (ιs := fun (x : ι) ↦ Free.ChooseBasisIndex R M) (Ms := fun (x : ι) ↦ M) fun (x : ι) ↦ b)
    (Equiv.trans (Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)) (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
i₁ : Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Free.ChooseBasisIndex R M
j₂ : ι
h : i₂ = j₂
⊢ Eq.{u_1 + 1} (α := R)
    ((((b.repr : (a : M) → Free.ChooseBasisIndex R M →₀ R)
              ((f i₂ : (a : M) → M) ((b : (a : Free.ChooseBasisIndex R M) → M) j₁ : M)) :
            Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R M) R) :
          (a : Free.ChooseBasisIndex R M) → R)
        i₁ :
      R)
    ((((b.repr : (a : M) → Free.ChooseBasisIndex R M →₀ R)
              ((f i₂ : (a : M) → M) ((b : (a : Free.ChooseBasisIndex R M) → M) j₁ : M)) :
            Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R M) R) :
          (a : Free.ChooseBasisIndex R M) → R)
        i₁ :
      R)
have pos : Eq.{u_1 + 1} (α := R)
  ((((b.repr : (a : M) → Free.ChooseBasisIndex R M →₀ R)
            ((f j₂ : (a : M) → M) ((b : (a : Free.ChooseBasisIndex R M) → M) j₁ : M)) :
          Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R M) R) :
        (a : Free.ChooseBasisIndex R M) → R)
      i₁ :
    R)
  ((((b.repr : (a : M) → Free.ChooseBasisIndex R M →₀ R)
            ((f j₂ : (a : M) → M) ((b : (a : Free.ChooseBasisIndex R M) → M) j₁ : M)) :
          Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R M) R) :
        (a : Free.ChooseBasisIndex R M) → R)
      i₁ :
    R)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_4
inst_3 : Fintype ι
inst_4 : Free R M
inst_5 : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R ((j : ι) → M) :=
  Basis.reindex (Pi.basis (ιs := fun (x : ι) ↦ Free.ChooseBasisIndex R M) (Ms := fun (x : ι) ↦ M) fun (x : ι) ↦ b)
    (Equiv.trans (Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)) (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
⊢ Eq.{u_1 + 1} (α := R)
    (det (n := Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι)
      ((toMatrix B B :
          (a : ((j : ι) → M) →ₗ[R] (j : ι) → M) →
            Matrix (Free.ChooseBasisIndex R M × ι) (Free.ChooseBasisIndex R M × ι) R)
        (pi (φ := fun (i : ι) ↦ M) fun (i : ι) ↦ f i ∘ₗ proj (φ := fun (i : ι) ↦ M) i)))
    (∏ x : ι,
      det.{u_1, u_2} (n := Free.ChooseBasisIndex R M)
        ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) (f x)))
have this : Eq (α := Matrix (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R)
  ((toMatrix B B :
        (a : ((j : ι) → M) →ₗ[R] (j : ι) → M) →
          Matrix (Free.ChooseBasisIndex R M × ι) (Free.ChooseBasisIndex R M × ι) R)
      (pi (φ := fun (j : ι) ↦ M) fun (i : ι) ↦ f i ∘ₗ proj (φ := fun (j : ι) ↦ M) i) :
    Matrix (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R)
  (blockDiagonal fun (i : ι) ↦
      (toMatrix b b : (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) (f i) :
    Matrix (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R)
Tactic: have : ((LinearMap.toMatrix B B) (LinearMap.pi fun i ↦ f i ∘ₗ LinearMap.proj i)) =
      Matrix.blockDiagonal (fun i ↦ LinearMap.toMatrix b b (f i)) := by
    ext ⟨i₁, i₂⟩ ⟨j₁, j₂⟩
    unfold B
    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]
    split_ifs with h
    · rw [h]
    · simp only [map_zero, Finsupp.coe_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_4
inst_3 : Fintype ι
inst_4 : Free R M
inst_5 : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R ((j : ι) → M) :=
  Basis.reindex (Pi.basis (ιs := fun (x : ι) ↦ Free.ChooseBasisIndex R M) (Ms := fun (x : ι) ↦ M) fun (x : ι) ↦ b)
    (Equiv.trans (Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)) (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
this :
  Eq (α := Matrix (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R)
    ((toMatrix B B :
          (a : ((j : ι) → M) →ₗ[R] (j : ι) → M) →
            Matrix (Free.ChooseBasisIndex R M × ι) (Free.ChooseBasisIndex R M × ι) R)
        (pi (φ := fun (j : ι) ↦ M) fun (i : ι) ↦ f i ∘ₗ proj (φ := fun (j : ι) ↦ M) i) :
      Matrix (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R)
    (blockDiagonal fun (i : ι) ↦
        (toMatrix b b : (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) (f i) :
      Matrix (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R)
⊢ Eq.{u_1 + 1} (α := R)
    (det (n := Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι)
      ((toMatrix B B :
          (a : ((j : ι) → M) →ₗ[R] (j : ι) → M) →
            Matrix (Free.ChooseBasisIndex R M × ι) (Free.ChooseBasisIndex R M × ι) R)
        (pi (φ := fun (i : ι) ↦ M) fun (i : ι) ↦ f i ∘ₗ proj (φ := fun (i : ι) ↦ M) i)))
    (∏ x : ι,
      det.{u_1, u_2} (n := Free.ChooseBasisIndex R M)
        ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) (f x)))
have rw : Eq.{u_1 + 1} (α := R)
  (det (n := Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι)
    (blockDiagonal fun (i : ι) ↦
      (toMatrix b b : (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) (f i)))
  (∏ x : ι,
    det.{u_1, u_2} (n := Free.ChooseBasisIndex R M)
      ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) (f x)))
Tactic: rw [this, Matrix.det_blockDiagonal]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_4
inst_3 : Fintype ι
inst_4 : Free R M
inst_5 : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R ((j : ι) → M) :=
  Basis.reindex (Pi.basis (ιs := fun (x : ι) ↦ Free.ChooseBasisIndex R M) (Ms := fun (x : ι) ↦ M) fun (x : ι) ↦ b)
    (Equiv.trans (Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)) (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
this :
  Eq (α := Matrix (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R)
    ((toMatrix B B :
          (a : ((j : ι) → M) →ₗ[R] (j : ι) → M) →
            Matrix (Free.ChooseBasisIndex R M × ι) (Free.ChooseBasisIndex R M × ι) R)
        (pi (φ := fun (j : ι) ↦ M) fun (i : ι) ↦ f i ∘ₗ proj (φ := fun (j : ι) ↦ M) i) :
      Matrix (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R)
    (blockDiagonal fun (i : ι) ↦
        (toMatrix b b : (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) (f i) :
      Matrix (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R)
rw :
  Eq.{u_1 + 1} (α := R)
    (det (n := Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι)
      (blockDiagonal fun (i : ι) ↦
        (toMatrix b b : (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) (f i)))
    (∏ x : ι,
      det.{u_1, u_2} (n := Free.ChooseBasisIndex R M)
        ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) (f x)))
⊢ Eq.{u_1 + 1} (α := R)
    (det (n := Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι)
      ((toMatrix B B :
          (a : ((j : ι) → M) →ₗ[R] (j : ι) → M) →
            Matrix (Free.ChooseBasisIndex R M × ι) (Free.ChooseBasisIndex R M × ι) R)
        (pi (φ := fun (i : ι) ↦ M) fun (i : ι) ↦ f i ∘ₗ proj (φ := fun (i : ι) ↦ M) i)))
    (∏ x : ι,
      det.{u_1, u_2} (n := Free.ChooseBasisIndex R M)
        ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) (f x)))
have rw₁ : Eq.{u_1 + 1} (α := R)
  (∏ k : ι,
    det.{u_1, u_2} (n := Free.ChooseBasisIndex R M)
      ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) (f k)))
  (∏ x : ι,
    det.{u_1, u_2} (n := Free.ChooseBasisIndex R M)
      ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) (f x)))
Tactic: rw [this, Matrix.det_blockDiagonal]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_4
inst_3 : Fintype ι
inst_4 : Free R M
inst_5 : Module.Finite R M
f : ι → M →ₗ[R] M
let let₁ let₂ let₃ :
  Eq.{u_1 + 1} (α := R)
    (((LinearMap.det (M := (i : ι) → M) (A := R) : (((i : ι) → M) →ₗ[R] (i : ι) → M) →* R) :
          (a : ((i : ι) → M) →ₗ[R] (i : ι) → M) → R)
        (pi (φ := fun (i : ι) ↦ M) fun (i : ι) ↦ f i ∘ₗ proj (φ := fun (i : ι) ↦ M) i :
          ((i : ι) → M) →ₗ[R] (i : ι) → M) :
      R)
    (∏ i : ι, (LinearMap.det : (a : M →ₗ[R] M) → R) (f i) : R)
⊢ Eq.{u_1 + 1} (α := R)
    (((LinearMap.det (M := (i : ι) → M) (A := R) : (((i : ι) → M) →ₗ[R] (i : ι) → M) →* R) :
          (a : ((i : ι) → M) →ₗ[R] (i : ι) → M) → R)
        (pi (φ := fun (i : ι) ↦ M) fun (i : ι) ↦ f i ∘ₗ proj (φ := fun (i : ι) ↦ M) i :
          ((i : ι) → M) →ₗ[R] (i : ι) → M) :
      R)
    (∏ i : ι, (LinearMap.det : (a : M →ₗ[R] M) → R) (f i) : R)
have let₄ : let b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M;
let B : Basis (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R ((j : ι) → M) :=
  Basis.reindex (Pi.basis (ιs := fun (x : ι) ↦ Free.ChooseBasisIndex R M) (Ms := fun (x : ι) ↦ M) fun (x : ι) ↦ b)
    (Equiv.trans (Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)) (Equiv.prodComm ι (Free.ChooseBasisIndex R M)));
Eq.{u_1 + 1} (α := R)
  (det (n := Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι)
    ((toMatrix B B :
        (a : ((j : ι) → M) →ₗ[R] (j : ι) → M) →
          Matrix (Free.ChooseBasisIndex R M × ι) (Free.ChooseBasisIndex R M × ι) R)
      (pi (φ := fun (i : ι) ↦ M) fun (i : ι) ↦ f i ∘ₗ proj (φ := fun (i : ι) ↦ M) i)))
  (∏ x : ι,
    det.{u_1, u_2} (n := Free.ChooseBasisIndex R M)
      ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) (f x)))
Tactic: classical
  let b := Module.Free.chooseBasis R M
  let B := (Pi.basis (fun _ : ι ↦ b)).reindex <|
    (Equiv.sigmaEquivProd _ _).trans (Equiv.prodComm _ _)
  simp_rw [← LinearMap.det_toMatrix B, ← LinearMap.det_toMatrix b]
  have : ((LinearMap.toMatrix B B) (LinearMap.pi fun i ↦ f i ∘ₗ LinearMap.proj i)) =
      Matrix.blockDiagonal (fun i ↦ LinearMap.toMatrix b b (f i)) := by
    ext ⟨i₁, i₂⟩ ⟨j₁, j₂⟩
    unfold B
    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]
    split_ifs with h
    · rw [h]
    · simp only [map_zero, Finsupp.coe_zero, Pi.zero_apply]
  rw [this, Matrix.det_blockDiagonal]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_5
S : Type u_6
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Free R S
x : R
⊢ ((LinearMap.det.{u_6, u_5} (M := S) (A := R) : MonoidHom.{u_6, u_5} (S →ₗ[R] S) R) : (a : S →ₗ[R] S) → R)
      ((lsmul R R S : (a : R) → End R S) x : End R S) =
    x ^ finrank R S
have rw : ((LinearMap.det.{u_6, u_5} (M := S) (A := R) : MonoidHom.{u_6, u_5} (S →ₗ[R] S) R) : (a : S →ₗ[R] S) → R)
    (HSMul.hSMul (β := End R S) x 1) =
  x ^ finrank R S
Tactic: rw [lsmul_eq_smul_one, LinearMap.det_smul, map_one, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_5
S : Type u_6
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Free R S
x : R
rw :
  ((LinearMap.det.{u_6, u_5} (M := S) (A := R) : MonoidHom.{u_6, u_5} (S →ₗ[R] S) R) : (a : S →ₗ[R] S) → R)
      (HSMul.hSMul (β := End R S) x 1) =
    x ^ finrank R S
⊢ ((LinearMap.det.{u_6, u_5} (M := S) (A := R) : MonoidHom.{u_6, u_5} (S →ₗ[R] S) R) : (a : S →ₗ[R] S) → R)
      ((lsmul R R S : (a : R) → End R S) x : End R S) =
    x ^ finrank R S
have rw₁ : HMul.hMul (β := R) (x ^ finrank R S)
    (((LinearMap.det.{u_6, u_5} (M := S) (A := R) : MonoidHom.{u_6, u_5} (S →ₗ[R] S) R) : (a : S →ₗ[R] S) → R) 1 : R) =
  x ^ finrank R S
Tactic: rw [lsmul_eq_smul_one, LinearMap.det_smul, map_one, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_5
S : Type u_6
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Free R S
x : R
rw :
  ((LinearMap.det.{u_6, u_5} (M := S) (A := R) : MonoidHom.{u_6, u_5} (S →ₗ[R] S) R) : (a : S →ₗ[R] S) → R)
      (HSMul.hSMul (β := End R S) x 1) =
    x ^ finrank R S
rw₁ :
  HMul.hMul (β := R) (x ^ finrank R S)
      (((LinearMap.det.{u_6, u_5} (M := S) (A := R) : MonoidHom.{u_6, u_5} (S →ₗ[R] S) R) : (a : S →ₗ[R] S) → R) 1 :
        R) =
    x ^ finrank R S
⊢ ((LinearMap.det.{u_6, u_5} (M := S) (A := R) : MonoidHom.{u_6, u_5} (S →ₗ[R] S) R) : (a : S →ₗ[R] S) → R)
      ((lsmul R R S : (a : R) → End R S) x : End R S) =
    x ^ finrank R S
have rw₂ : x ^ finrank R S * 1 = x ^ finrank R S
Tactic: rw [lsmul_eq_smul_one, LinearMap.det_smul, map_one, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_5
S : Type u_6
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Free R S
x : R
rw :
  ((LinearMap.det.{u_6, u_5} (M := S) (A := R) : MonoidHom.{u_6, u_5} (S →ₗ[R] S) R) : (a : S →ₗ[R] S) → R)
      (HSMul.hSMul (β := End R S) x 1) =
    x ^ finrank R S
rw₁ :
  HMul.hMul (β := R) (x ^ finrank R S)
      (((LinearMap.det.{u_6, u_5} (M := S) (A := R) : MonoidHom.{u_6, u_5} (S →ₗ[R] S) R) : (a : S →ₗ[R] S) → R) 1 :
        R) =
    x ^ finrank R S
rw₂ : x ^ finrank R S * 1 = x ^ finrank R S
⊢ ((LinearMap.det.{u_6, u_5} (M := S) (A := R) : MonoidHom.{u_6, u_5} (S →ₗ[R] S) R) : (a : S →ₗ[R] S) → R)
      ((lsmul R R S : (a : R) → End R S) x : End R S) =
    x ^ finrank R S
have rw₃ : x ^ finrank R S = x ^ finrank R S
Tactic: rw [lsmul_eq_smul_one, LinearMap.det_smul, map_one, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M ≃ₗ[R] M
e : M ≃ₗ[R] M'
⊢ Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : M' ≃ₗ[R] M') → Rˣ) (e.symm ≪≫ₗ f ≪≫ₗ e) : Rˣ)
    ((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f : Rˣ)
have rw : Eq.{u_1 + 1} (α := R) (↑((LinearEquiv.det : (a : M' ≃ₗ[R] M') → Rˣ) (e.symm ≪≫ₗ f ≪≫ₗ e)) : R)
  (↑((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f) : R)
Tactic: rw [← Units.val_inj, coe_det, coe_det, ← comp_coe, ← comp_coe, LinearMap.det_conj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M ≃ₗ[R] M
e : M ≃ₗ[R] M'
rw :
  Eq.{u_1 + 1} (α := R) (↑((LinearEquiv.det : (a : M' ≃ₗ[R] M') → Rˣ) (e.symm ≪≫ₗ f ≪≫ₗ e)) : R)
    (↑((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f) : R)
⊢ Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : M' ≃ₗ[R] M') → Rˣ) (e.symm ≪≫ₗ f ≪≫ₗ e) : Rˣ)
    ((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f : Rˣ)
have rw₁ : Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M' →ₗ[R] M') → R) (↑(e.symm ≪≫ₗ f ≪≫ₗ e) : M' →ₗ[R] M') : R)
  ((↑((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f) : R) : R)
Tactic: rw [← Units.val_inj, coe_det, coe_det, ← comp_coe, ← comp_coe, LinearMap.det_conj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M ≃ₗ[R] M
e : M ≃ₗ[R] M'
rw :
  Eq.{u_1 + 1} (α := R) (↑((LinearEquiv.det : (a : M' ≃ₗ[R] M') → Rˣ) (e.symm ≪≫ₗ f ≪≫ₗ e)) : R)
    (↑((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f) : R)
rw₁ :
  Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M' →ₗ[R] M') → R) (↑(e.symm ≪≫ₗ f ≪≫ₗ e) : M' →ₗ[R] M') : R)
    ((↑((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f) : R) : R)
⊢ Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : M' ≃ₗ[R] M') → Rˣ) (e.symm ≪≫ₗ f ≪≫ₗ e) : Rˣ)
    ((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f : Rˣ)
have rw₂ : Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M' →ₗ[R] M') → R) (↑(e.symm ≪≫ₗ f ≪≫ₗ e) : M' →ₗ[R] M') : R)
  ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R)
Tactic: rw [← Units.val_inj, coe_det, coe_det, ← comp_coe, ← comp_coe, LinearMap.det_conj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M ≃ₗ[R] M
e : M ≃ₗ[R] M'
rw :
  Eq.{u_1 + 1} (α := R) (↑((LinearEquiv.det : (a : M' ≃ₗ[R] M') → Rˣ) (e.symm ≪≫ₗ f ≪≫ₗ e)) : R)
    (↑((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f) : R)
rw₁ :
  Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M' →ₗ[R] M') → R) (↑(e.symm ≪≫ₗ f ≪≫ₗ e) : M' →ₗ[R] M') : R)
    ((↑((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f) : R) : R)
rw₂ :
  Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M' →ₗ[R] M') → R) (↑(e.symm ≪≫ₗ f ≪≫ₗ e) : M' →ₗ[R] M') : R)
    ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R)
⊢ Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : M' ≃ₗ[R] M') → Rˣ) (e.symm ≪≫ₗ f ≪≫ₗ e) : Rˣ)
    ((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f : Rˣ)
have rw₃ : Eq.{u_1 + 1} (α := R)
  ((LinearMap.det : (a : M' →ₗ[R] M') → R) ((↑e : M →ₗ[R] M') ∘ₗ (↑(e.symm ≪≫ₗ f) : M' →ₗ[R] M)) : R)
  ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R)
Tactic: rw [← Units.val_inj, coe_det, coe_det, ← comp_coe, ← comp_coe, LinearMap.det_conj]