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
inst_3 : Module.Finite R M
inst_4 : Free R M
f : M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
rw :
  IsUnit (M := Matrix.{u_2, u_2, u_1} (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R)
      ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) f :
        Matrix.{u_2, u_2, u_1} (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) ↔
    IsUnit.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
rw₁ :
  IsUnit (M := Matrix.{u_2, u_2, u_1} (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R)
      ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) f :
        Matrix.{u_2, u_2, u_1} (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) ↔
    IsUnit.{u_1} (M := R)
      (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))
⊢ IsUnit f ↔ IsUnit.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
have rw₂ : IsUnit.{u_1} (M := R)
    (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)) ↔
  IsUnit.{u_1} (M := R)
    (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))
Tactic: rw [← isUnit_toMatrix_iff b, ← det_toMatrix b, Matrix.isUnit_iff_isUnit_det (toMatrix b b f)]
-- 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
f : M →ₗ[R] M
hf : Ne.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (1 : R)
⊢ Free R M
have pos : ∀ (H : ∃ (s : Finset M), Nonempty (Basis (↥s) R M)), Free R M
Tactic: by_cases H : ∃ s : Finset M, Nonempty (Basis s R M)
-- 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
f : M →ₗ[R] M
hf : Ne.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (1 : R)
pos : ∀ (H : ∃ (s : Finset M), Nonempty (Basis (↥s) R M)), Free R M
⊢ Free R M
have neg : ∀ (H : ¬∃ (s : Finset M), Nonempty (Basis (↥s) R M)), Free R M
Tactic: by_cases H : ∃ s : Finset M, Nonempty (Basis s R M)
-- 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
f : M →ₗ[R] M
hf : Ne.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (1 : R)
⊢ Module.Finite R M
have pos : ∀ (H : ∃ (s : Finset M), Nonempty (Basis (↥s) R M)), Module.Finite R M
Tactic: by_cases H : ∃ s : Finset M, Nonempty (Basis s R M)
-- 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
f : M →ₗ[R] M
hf : Ne.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (1 : R)
pos : ∀ (H : ∃ (s : Finset M), Nonempty (Basis (↥s) R M)), Module.Finite R M
⊢ Module.Finite R M
have neg : ∀ (H : ¬∃ (s : Finset M), Nonempty (Basis (↥s) R M)), Module.Finite R M
Tactic: by_cases H : ∃ s : Finset M, Nonempty (Basis s R M)
-- 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
f : M →ₗ[R] M
hf : Ne.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (1 : R)
H : ∃ (s : Finset M), Nonempty (Basis (↥s) R M)
⊢ Module.Finite R M
have pos : ∀ (s : Finset M) (hs : Basis (↥s) R M), Module.Finite R M
Tactic: rcases H with ⟨s, ⟨hs⟩⟩
Cleared hypotheses: 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
inst_3 : IsDomain R
inst_4 : Free R M
f : M →ₗ[R] M
hf : Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (0 : R)
⊢ ⊥ < f.ker
have this : Module.Finite R M
Tactic: have : Module.Finite R M := by simp [finite_of_det_ne_one (f := f), hf]
-- 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
inst_3 : IsDomain R
inst_4 : Free R M
f : M →ₗ[R] M
hf : Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (0 : R)
this : Module.Finite R M
b : Basis (Fin (finrank R M)) R M := finBasis R M
⊢ ⊥ < f.ker
have suffices : ∃ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) (0 : M) ∧ x ≠ 0
Tactic: suffices ∃ x, f x = 0 ∧ x ≠ 0 by simpa [bot_lt_iff_ne_bot, ker_eq_bot']
-- 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
inst_3 : IsDomain R
inst_4 : Free R M
f : M →ₗ[R] M
hf : Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (0 : R)
this : Module.Finite R M
b : Basis (Fin (finrank R M)) R M := finBasis R M
⊢ ∃ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) (0 : M) ∧ x ≠ 0
have obtain : ∀ (v : Fin (finrank R M) → R) (hv_ne_zero : v ≠ 0)
  (hv_zero :
    Eq (α := Fin (finrank R M) → R)
      ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Fin (finrank R M)) (Fin (finrank R M)) R) f *ᵥ v) 0),
  ∃ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) (0 : M) ∧ x ≠ 0
Tactic: obtain ⟨v, hv_ne_zero, hv_zero⟩ := Matrix.exists_mulVec_eq_zero_iff.mpr (det_toMatrix b f ▸ hf)
-- 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
inst_3 : IsDomain R
inst_4 : Free R M
f : M →ₗ[R] M
hf : Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (0 : R)
this : Module.Finite R M
b : Basis (Fin (finrank R M)) R M := finBasis R M
v : Fin (finrank R M) → R
hv_ne_zero : v ≠ 0
hv_zero :
  Eq (α := Fin (finrank R M) → R)
    ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Fin (finrank R M)) (Fin (finrank R M)) R) f *ᵥ v) 0
⊢ ∃ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) (0 : M) ∧ x ≠ 0
have refine : Eq (α := M) ((f : (a : M) → M) ((b.equivFun.symm : (a : Fin (finrank R M) → R) → M) v : M) : M) (0 : M)
Tactic: refine ⟨b.equivFun.symm v, ?_, b.equivFun.symm.map_ne_zero_iff.mpr hv_ne_zero⟩
-- 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
inst_3 : IsDomain R
inst_4 : Free R M
f : M →ₗ[R] M
hf : Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (0 : R)
this : Module.Finite R M
b : Basis (Fin (finrank R M)) R M := finBasis R M
v : Fin (finrank R M) → R
hv_ne_zero : v ≠ 0
hv_zero :
  Eq (α := Fin (finrank R M) → R)
    ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Fin (finrank R M)) (Fin (finrank R M)) R) f *ᵥ v) 0
⊢ Eq (α := M) ((f : (a : M) → M) ((b.equivFun.symm : (a : Fin (finrank R M) → R) → M) v : M) : M) (0 : M)
have rw : Eq.{u_1 + 1} (α := Fin (finrank R M) → R)
  ((b.equivFun : (a : M) → Fin (finrank R M) → R)
      ((f : (a : M) → M) ((b.equivFun.symm : (a : Fin (finrank R M) → R) → M) v : M) : M) :
    Fin (finrank R M) → R)
  ((b.equivFun : (a : M) → Fin (finrank R M) → R) 0 : Fin (finrank R M) → R)
Tactic: rw [← b.equivFun.injective.eq_iff]
-- 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
inst_3 : IsDomain R
inst_4 : Free R M
inst_5 : Module.Finite R M
f : M →ₗ[R] M
⊢ Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (0 : R) ↔ f.ker ≠ ⊥
have mp : Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (0 : R) → f.ker ≠ ⊥
Tactic: constructor
-- 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
inst_3 : IsDomain R
inst_4 : Free R M
inst_5 : Module.Finite R M
f : M →ₗ[R] M
mp : Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (0 : R) → f.ker ≠ ⊥
⊢ Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (0 : R) ↔ f.ker ≠ ⊥
have mpr : f.ker ≠ ⊥ → Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (0 : R)
Tactic: constructor
-- 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
inst_3 : IsDomain R
inst_4 : Free R M
inst_5 : Module.Finite R M
f : M →ₗ[R] M
h : f.ker ≠ ⊥
b : Basis (Fin (finrank R M)) R M := finBasis R M
⊢ Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (0 : R)
have mpr : ∀ v ∈ f.ker, ∀ (hv_ne_zero : v ≠ 0), Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (0 : R)
Tactic: obtain ⟨v, ⟨_, hv_ne_zero⟩⟩ := (ker f).ne_bot_iff.mp 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
inst_3 : IsDomain R
inst_4 : Free R M
inst_5 : Module.Finite R M
f : M →ₗ[R] M
h : f.ker ≠ ⊥
b : Basis (Fin (finrank R M)) R M := finBasis R M
v : M
left : v ∈ f.ker
hv_ne_zero : v ≠ 0
⊢ Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (0 : R)
have mpr : ∃ (v : Fin (finrank R M) → R),
  v ≠ 0 ∧
    Eq (α := Fin (finrank R M) → R)
      ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Fin (finrank R M)) (Fin (finrank R M)) R) f *ᵥ v) 0
Tactic: rw [← det_toMatrix b, ← Matrix.exists_mulVec_eq_zero_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (hypothesis)
Goal:
M : Type u_2
inst : AddCommGroup M
𝕜 : Type u_7
inst_1 : Field 𝕜
inst_2 : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : Eq.{u_7 + 1} (α := 𝕜) ((LinearMap.det : (a : M →ₗ[𝕜] M) → 𝕜) f : 𝕜) (0 : 𝕜)
⊢ f.range < ⊤
have this : Module.Finite 𝕜 M
Tactic: have : Module.Finite 𝕜 M := by simp [finite_of_det_ne_one (f := f), hf]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
𝕜 : Type u_7
inst_1 : Field 𝕜
inst_2 : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : Eq.{u_7 + 1} (α := 𝕜) ((LinearMap.det : (a : M →ₗ[𝕜] M) → 𝕜) f : 𝕜) (0 : 𝕜)
this : Module.Finite 𝕜 M
⊢ f.range < ⊤
have rw : ⊥ < f.ker
Tactic: rw [lt_top_iff_ne_top, ne_eq, ← ker_eq_bot_iff_range_eq_top, ← ne_eq, ← bot_lt_iff_ne_bot]
-- 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'
inst_5 : Free R M
inst_6 : Free R M'
inst_7 : Module.Finite R M
inst_8 : Module.Finite R M'
f : End R M
f' : End R M'
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
b' : Basis (Free.ChooseBasisIndex R M') R M' := Free.chooseBasis R M'
⊢ ((LinearMap.det (M := M × M') (A := R) : (M × M' →ₗ[R] M × M') →* R) : (a : M × M' →ₗ[R] M × M') → R) (prodMap f f') =
    HMul.hMul (α := R) (β := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
      ((LinearMap.det : (a : M' →ₗ[R] M') → R) f' : R)
have rw : det (n := Sum.{u_2, u_3} (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M'))
    ((toMatrix (b.prod b') (b.prod b') :
        (a : M × M' →ₗ[R] M × M') →
          Matrix (Free.ChooseBasisIndex R M ⊕ Free.ChooseBasisIndex R M')
            (Free.ChooseBasisIndex R M ⊕ Free.ChooseBasisIndex R M') R)
      (prodMap f f')) =
  HMul.hMul (α := R) (β := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
    ((LinearMap.det : (a : M' →ₗ[R] M') → R) f' : R)
Tactic: rw [← det_toMatrix (b.prod b'), ← det_toMatrix b, ← det_toMatrix b', toMatrix_prodMap,
    det_fromBlocks_zero₂₁, det_toMatrix]
-- 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'
inst_5 : Free R M
inst_6 : Free R M'
inst_7 : Module.Finite R M
inst_8 : Module.Finite R M'
f : End R M
f' : End R M'
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
b' : Basis (Free.ChooseBasisIndex R M') R M' := Free.chooseBasis R M'
rw :
  det (n := Sum.{u_2, u_3} (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M'))
      ((toMatrix (b.prod b') (b.prod b') :
          (a : M × M' →ₗ[R] M × M') →
            Matrix (Free.ChooseBasisIndex R M ⊕ Free.ChooseBasisIndex R M')
              (Free.ChooseBasisIndex R M ⊕ Free.ChooseBasisIndex R M') R)
        (prodMap f f')) =
    HMul.hMul (α := R) (β := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
      ((LinearMap.det : (a : M' →ₗ[R] M') → R) f' : R)
⊢ ((LinearMap.det (M := M × M') (A := R) : (M × M' →ₗ[R] M × M') →* R) : (a : M × M' →ₗ[R] M × M') → R) (prodMap f f') =
    HMul.hMul (α := R) (β := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
      ((LinearMap.det : (a : M' →ₗ[R] M') → R) f' : R)
have rw₁ : det (n := Sum.{u_2, u_3} (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M'))
    ((toMatrix (b.prod b') (b.prod b') :
        (a : M × M' →ₗ[R] M × M') →
          Matrix (Free.ChooseBasisIndex R M ⊕ Free.ChooseBasisIndex R M')
            (Free.ChooseBasisIndex R M ⊕ Free.ChooseBasisIndex R M') R)
      (prodMap f f')) =
  HMul.hMul (α := R) (β := R)
    (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) :
      R)
    ((LinearMap.det : (a : M' →ₗ[R] M') → R) f' : R)
Tactic: rw [← det_toMatrix (b.prod b'), ← det_toMatrix b, ← det_toMatrix b', toMatrix_prodMap,
    det_fromBlocks_zero₂₁, det_toMatrix]
-- 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'
inst_5 : Free R M
inst_6 : Free R M'
inst_7 : Module.Finite R M
inst_8 : Module.Finite R M'
f : End R M
f' : End R M'
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
b' : Basis (Free.ChooseBasisIndex R M') R M' := Free.chooseBasis R M'
rw :
  det (n := Sum.{u_2, u_3} (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M'))
      ((toMatrix (b.prod b') (b.prod b') :
          (a : M × M' →ₗ[R] M × M') →
            Matrix (Free.ChooseBasisIndex R M ⊕ Free.ChooseBasisIndex R M')
              (Free.ChooseBasisIndex R M ⊕ Free.ChooseBasisIndex R M') R)
        (prodMap f f')) =
    HMul.hMul (α := R) (β := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
      ((LinearMap.det : (a : M' →ₗ[R] M') → R) f' : R)
rw₁ :
  det (n := Sum.{u_2, u_3} (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M'))
      ((toMatrix (b.prod b') (b.prod b') :
          (a : M × M' →ₗ[R] M × M') →
            Matrix (Free.ChooseBasisIndex R M ⊕ Free.ChooseBasisIndex R M')
              (Free.ChooseBasisIndex R M ⊕ Free.ChooseBasisIndex R M') R)
        (prodMap f f')) =
    HMul.hMul (α := R) (β := R)
      (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) :
        R)
      ((LinearMap.det : (a : M' →ₗ[R] M') → R) f' : R)
⊢ ((LinearMap.det (M := M × M') (A := R) : (M × M' →ₗ[R] M × M') →* R) : (a : M × M' →ₗ[R] M × M') → R) (prodMap f f') =
    HMul.hMul (α := R) (β := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
      ((LinearMap.det : (a : M' →ₗ[R] M') → R) f' : R)
have rw₂ : det (n := Sum.{u_2, u_3} (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M'))
    ((toMatrix (b.prod b') (b.prod b') :
        (a : M × M' →ₗ[R] M × M') →
          Matrix (Free.ChooseBasisIndex R M ⊕ Free.ChooseBasisIndex R M')
            (Free.ChooseBasisIndex R M ⊕ Free.ChooseBasisIndex R M') R)
      (prodMap f f')) =
  HMul.hMul (α := R)
    (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))
    (det.{u_1, u_3} (n := Free.ChooseBasisIndex R M')
      ((toMatrix b' b' : (a : M' →ₗ[R] M') → Matrix (Free.ChooseBasisIndex R M') (Free.ChooseBasisIndex R M') R) f'))
Tactic: rw [← det_toMatrix (b.prod b'), ← det_toMatrix b, ← det_toMatrix b', toMatrix_prodMap,
    det_fromBlocks_zero₂₁, det_toMatrix]
-- 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)))
⊢ 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 simp_rw : 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: simp_rw [← LinearMap.det_toMatrix B, ← LinearMap.det_toMatrix b]
-- 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)))
⊢ 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)
have a : ∀ (i₁ : Free.ChooseBasisIndex R M) (i₂ : ι) (j₁ : Free.ChooseBasisIndex R M) (j₂ : ι),
  Eq.{u_1 + 1} (α := 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) (i₁, i₂) (j₁, j₂) :
      R)
    (blockDiagonal
        (fun (i : ι) ↦
          (toMatrix b b : (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) (f i))
        (i₁, i₂) (j₁, j₂) :
      R)
Tactic: ext ⟨i₁, i₂⟩ ⟨j₁, j₂⟩
-- 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)
    ((toMatrix
            (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))))
            (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)))) :
          (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) (i₁, i₂) (j₁, j₂) :
      R)
    (blockDiagonal
        (fun (i : ι) ↦
          (toMatrix b b : (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) (f i))
        (i₁, i₂) (j₁, j₂) :
      R)
have a : 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)
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]