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 : DecidableEq ι
inst_4 : Fintype ι
ι' : Type u_6
inst_5 : Fintype ι'
inst_6 : DecidableEq ι'
b : Basis ι R M
v : ι → M
e : ι' ≃ ι
rw :
  Eq.{u_1 + 1} (α := R)
    ((b.det : (a : ι → M) → R)
        (Function.comp.{u_4 + 1, u_6 + 1, u_2 + 1} (β := ι') (v ∘ (⇑e : (a : ι') → ι)) (⇑e.symm : (a : ι) → ι')) :
      R)
    ((b.det : (a : ι → M) → R) v : R)
rw₁ :
  Eq.{u_1 + 1} (α := R)
    ((b.det : (a : ι → M) → R)
        (v ∘ Function.comp.{u_4 + 1, u_6 + 1, u_4 + 1} (β := ι') (⇑e : (a : ι') → ι) (⇑e.symm : (a : ι) → ι')) :
      R)
    ((b.det : (a : ι → M) → R) v : R)
rw₂ : Eq.{u_1 + 1} (α := R) ((b.det : (a : ι → M) → R) (v ∘ _root_.id) : R) ((b.det : (a : ι → M) → R) v : R)
⊢ Eq.{u_1 + 1} (α := R) (((b.reindex e.symm).det : (a : ι' → M) → R) (v ∘ (⇑e : (a : ι') → ι)) : R)
    ((b.det : (a : ι → M) → R) v : R)
have rw₃ : Eq.{u_1 + 1} (α := R) ((b.det : (a : ι → M) → R) v : R) ((b.det : (a : ι → M) → R) v : R)
Tactic: rw [det_reindex, Function.comp_assoc, e.self_comp_symm, Function.comp_id]
-- 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'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
b : Basis ι R M
f : M ≃ₗ[R] M'
v : ι → M'
⊢ Eq.{u_1 + 1} (α := R) (((b.map f).det : (a : ι → M') → R) v : R)
    ((b.det : (a : ι → M) → R) ((⇑f.symm : (a : M') → M) ∘ v) : R)
have rw : ((b.map f).toMatrix v).det = (b.det : (a : ι → M) → R) ((⇑f.symm : (a : M') → M) ∘ v)
Tactic: rw [det_apply, toMatrix_map, det_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
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
b : Basis ι R M
f : M ≃ₗ[R] M'
v : ι → M'
rw : ((b.map f).toMatrix v).det = (b.det : (a : ι → M) → R) ((⇑f.symm : (a : M') → M) ∘ v)
⊢ Eq.{u_1 + 1} (α := R) (((b.map f).det : (a : ι → M') → R) v : R)
    ((b.det : (a : ι → M) → R) ((⇑f.symm : (a : M') → M) ∘ v) : R)
have rw₁ : (b.toMatrix ((⇑f.symm : (a : M') → M) ∘ v)).det = (b.det : (a : ι → M) → R) ((⇑f.symm : (a : M') → M) ∘ v)
Tactic: rw [det_apply, toMatrix_map, det_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
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
b : Basis ι R M
f : M ≃ₗ[R] M'
v : ι → M'
rw : ((b.map f).toMatrix v).det = (b.det : (a : ι → M) → R) ((⇑f.symm : (a : M') → M) ∘ v)
rw₁ : (b.toMatrix ((⇑f.symm : (a : M') → M) ∘ v)).det = (b.det : (a : ι → M) → R) ((⇑f.symm : (a : M') → M) ∘ v)
⊢ Eq.{u_1 + 1} (α := R) (((b.map f).det : (a : ι → M') → R) v : R)
    ((b.det : (a : ι → M) → R) ((⇑f.symm : (a : M') → M) ∘ v) : R)
have rw₂ : (b.toMatrix ((⇑f.symm : (a : M') → M) ∘ v)).det = (b.toMatrix ((⇑f.symm : (a : M') → M) ∘ v)).det
Tactic: rw [det_apply, toMatrix_map, det_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : Fintype ι
⊢ Eq (α := (ι → R) [⋀^ι]→ₗ[R] R) (Basis.det (R := R) (M := ι → R) (ι := ι) (basisFun R ι) : (ι → R) [⋀^ι]→ₗ[R] R)
    (detRowAlternating : (ι → R) [⋀^ι]→ₗ[R] R)
have H : ∀ (M : ι → ι → R),
  Eq.{u_1 + 1} (α := R)
    (((Basis.det (R := R) (M := ι → R) (ι := ι) (basisFun R ι) : (ι → R) [⋀^ι]→ₗ[R] R) : (a : ι → ι → R) → R) M : R)
    ((detRowAlternating : (a : ι → ι → R) → R) M : R)
Tactic: ext M
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : Fintype ι
M : ι → ι → R
⊢ Eq.{u_1 + 1} (α := R)
    (((Basis.det (R := R) (M := ι → R) (ι := ι) (basisFun R ι) : (ι → R) [⋀^ι]→ₗ[R] R) : (a : ι → ι → R) → R) M : R)
    ((detRowAlternating : (a : ι → ι → R) → R) M : R)
have H : (Basis.toMatrix (basisFun R ι) M).det = (detRowAlternating : (a : ι → ι → R) → R) M
Tactic: rw [Basis.det_apply, Basis.coePiBasisFun.toMatrix_eq_transpose, det_transpose, det]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : Fintype ι
M : ι → ι → R
H : (Basis.toMatrix (basisFun R ι) M).det = (detRowAlternating : (a : ι → ι → R) → R) M
⊢ Eq.{u_1 + 1} (α := R)
    (((Basis.det (R := R) (M := ι → R) (ι := ι) (basisFun R ι) : (ι → R) [⋀^ι]→ₗ[R] R) : (a : ι → ι → R) → R) M : R)
    ((detRowAlternating : (a : ι → ι → R) → R) M : R)
have H₁ : Mᵀ.det = (detRowAlternating : (a : ι → ι → R) → R) M
Tactic: rw [Basis.det_apply, Basis.coePiBasisFun.toMatrix_eq_transpose, det_transpose, det]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : Fintype ι
M : ι → ι → R
H : (Basis.toMatrix (basisFun R ι) M).det = (detRowAlternating : (a : ι → ι → R) → R) M
H₁ : Mᵀ.det = (detRowAlternating : (a : ι → ι → R) → R) M
⊢ Eq.{u_1 + 1} (α := R)
    (((Basis.det (R := R) (M := ι → R) (ι := ι) (basisFun R ι) : (ι → R) [⋀^ι]→ₗ[R] R) : (a : ι → ι → R) → R) M : R)
    ((detRowAlternating : (a : ι → ι → R) → R) M : R)
have H₂ : det M = (detRowAlternating : (a : ι → ι → R) → R) M
Tactic: rw [Basis.det_apply, Basis.coePiBasisFun.toMatrix_eq_transpose, det_transpose, det]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : Fintype ι
M : ι → ι → R
H : (Basis.toMatrix (basisFun R ι) M).det = (detRowAlternating : (a : ι → ι → R) → R) M
H₁ : Mᵀ.det = (detRowAlternating : (a : ι → ι → R) → R) M
H₂ : det M = (detRowAlternating : (a : ι → ι → R) → R) M
⊢ Eq.{u_1 + 1} (α := R)
    (((Basis.det (R := R) (M := ι → R) (ι := ι) (basisFun R ι) : (ι → R) [⋀^ι]→ₗ[R] R) : (a : ι → ι → R) → R) M : R)
    ((detRowAlternating : (a : ι → ι → R) → R) M : R)
have H₃ : Eq.{u_1 + 1} (α := R) ((detRowAlternating : (a : ι → ι → R) → R) M : R)
  ((detRowAlternating : (a : ι → ι → R) → R) M : R)
Tactic: rw [Basis.det_apply, Basis.coePiBasisFun.toMatrix_eq_transpose, det_transpose, det]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : Fintype ι
v : ι → ι → R
⊢ Eq.{u_1 + 1} (α := R)
    (((Basis.det (R := R) (M := ι → R) (ι := ι) (basisFun R ι) : (ι → R) [⋀^ι]→ₗ[R] R) : (a : ι → ι → R) → R) v : R)
    (det.{u_1, u_4} (n := ι) ((of : (a : ι → ι → R) → Matrix ι ι R) v) : R)
have rw : Eq.{u_1 + 1} (α := R) ((detRowAlternating : (a : ι → ι → R) → R) v : R)
  (det.{u_1, u_4} (n := ι) ((of : (a : ι → ι → R) → Matrix ι ι R) v) : R)
Tactic: rw [Pi.basisFun_det]
-- 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 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hsp : LE.le (α := Submodule R M) ⊤ (span R (Set.range v))
i : ι
⊢ HSMul.hSMul (α := R) ((e.det : (a : ι → M) → R) v : R) ((Basis.mk hli hsp).coord i) =
    (↑e.det : MultilinearMap R (fun (x : ι) ↦ M) R).toLinearMap (M₁ := fun (x : ι) ↦ M) v i
have apply : ∀ (i_1 : ι),
  Eq.{u_1 + 1} (α := R)
    ((HSMul.hSMul (α := R) ((e.det : (a : ι → M) → R) v : R) ((Basis.mk hli hsp).coord i) : (a : M) → R)
        ((Basis.mk hli hsp : (a : ι) → M) i_1 : M) :
      R)
    (((↑e.det : MultilinearMap R (fun (x : ι) ↦ M) R).toLinearMap (M₁ := fun (x : ι) ↦ M) v i : (a : M) → R)
        ((Basis.mk hli hsp : (a : ι) → M) i_1 : M) :
      R)
Tactic: apply (Basis.mk hli hsp).ext
-- 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 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hsp : LE.le (α := Submodule R M) ⊤ (span R (Set.range v))
i k : ι
⊢ Eq.{u_1 + 1} (α := R)
    ((HSMul.hSMul (α := R) ((e.det : (a : ι → M) → R) v : R) ((Basis.mk hli hsp).coord i) : (a : M) → R)
        ((Basis.mk hli hsp : (a : ι) → M) k : M) :
      R)
    (((↑e.det : MultilinearMap R (fun (x : ι) ↦ M) R).toLinearMap (M₁ := fun (x : ι) ↦ M) v i : (a : M) → R)
        ((Basis.mk hli hsp : (a : ι) → M) k : M) :
      R)
have inl : Eq.{u_1 + 1} (α := R)
  ((HSMul.hSMul (α := R) ((e.det : (a : ι → M) → R) v : R) ((Basis.mk hli hsp).coord k) : (a : M) → R)
      ((Basis.mk hli hsp : (a : ι) → M) k : M) :
    R)
  (((↑e.det : MultilinearMap R (fun (x : ι) ↦ M) R).toLinearMap (M₁ := fun (x : ι) ↦ M) v k : (a : M) → R)
      ((Basis.mk hli hsp : (a : ι) → M) k : M) :
    R)
Tactic: rcases eq_or_ne k i with (rfl | hik)
Cleared hypotheses: i
-- 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 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hsp : LE.le (α := Submodule R M) ⊤ (span R (Set.range v))
i k : ι
inl :
  Eq.{u_1 + 1} (α := R)
    ((HSMul.hSMul (α := R) ((e.det : (a : ι → M) → R) v : R) ((Basis.mk hli hsp).coord k) : (a : M) → R)
        ((Basis.mk hli hsp : (a : ι) → M) k : M) :
      R)
    (((↑e.det : MultilinearMap R (fun (x : ι) ↦ M) R).toLinearMap (M₁ := fun (x : ι) ↦ M) v k : (a : M) → R)
        ((Basis.mk hli hsp : (a : ι) → M) k : M) :
      R)
⊢ Eq.{u_1 + 1} (α := R)
    ((HSMul.hSMul (α := R) ((e.det : (a : ι → M) → R) v : R) ((Basis.mk hli hsp).coord i) : (a : M) → R)
        ((Basis.mk hli hsp : (a : ι) → M) k : M) :
      R)
    (((↑e.det : MultilinearMap R (fun (x : ι) ↦ M) R).toLinearMap (M₁ := fun (x : ι) ↦ M) v i : (a : M) → R)
        ((Basis.mk hli hsp : (a : ι) → M) k : M) :
      R)
have inr : ∀ (hik : k ≠ i),
  Eq.{u_1 + 1} (α := R)
    ((HSMul.hSMul (α := R) ((e.det : (a : ι → M) → R) v : R) ((Basis.mk hli hsp).coord i) : (a : M) → R)
        ((Basis.mk hli hsp : (a : ι) → M) k : M) :
      R)
    (((↑e.det : MultilinearMap R (fun (x : ι) ↦ M) R).toLinearMap (M₁ := fun (x : ι) ↦ M) v i : (a : M) → R)
        ((Basis.mk hli hsp : (a : ι) → M) k : M) :
      R)
Tactic: rcases eq_or_ne k i with (rfl | hik)
-- 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 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hsp : LE.le (α := Submodule R M) ⊤ (span R (Set.range v))
k : ι
⊢ Eq.{u_1 + 1} (α := R)
    ((HSMul.hSMul (α := R) ((e.det : (a : ι → M) → R) v : R) ((Basis.mk hli hsp).coord k) : (a : M) → R)
        ((Basis.mk hli hsp : (a : ι) → M) k : M) :
      R)
    (((↑e.det : MultilinearMap R (fun (x : ι) ↦ M) R).toLinearMap (M₁ := fun (x : ι) ↦ M) v k : (a : M) → R)
        ((Basis.mk hli hsp : (a : ι) → M) k : M) :
      R)
have inl : HMul.hMul (α := R) (β := R) ((e.det : (a : ι → M) → R) v : R) (((Basis.mk hli hsp).coord k : (a : M) → R) (v k) : R) =
  ((↑e.det : MultilinearMap R (fun (x : ι) ↦ M) R) : (a : (i : ι) → M) → R) (update (β := fun (x : ι) ↦ M) v k (v k))
Tactic: simp only [smul_eq_mul, coe_mk, LinearMap.smul_apply,
      MultilinearMap.toLinearMap_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 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hsp : LE.le (α := Submodule R M) ⊤ (span R (Set.range v))
i k : ι
hik : k ≠ i
⊢ Eq.{u_1 + 1} (α := R)
    ((HSMul.hSMul (α := R) ((e.det : (a : ι → M) → R) v : R) ((Basis.mk hli hsp).coord i) : (a : M) → R)
        ((Basis.mk hli hsp : (a : ι) → M) k : M) :
      R)
    (((↑e.det : MultilinearMap R (fun (x : ι) ↦ M) R).toLinearMap (M₁ := fun (x : ι) ↦ M) v i : (a : M) → R)
        ((Basis.mk hli hsp : (a : ι) → M) k : M) :
      R)
have inr : HMul.hMul (α := R) (β := R) ((e.det : (a : ι → M) → R) v : R) (((Basis.mk hli hsp).coord i : (a : M) → R) (v k) : R) =
  ((↑e.det : MultilinearMap R (fun (x : ι) ↦ M) R) : (a : (i : ι) → M) → R) (update (β := fun (x : ι) ↦ M) v i (v k))
Tactic: simp only [smul_eq_mul, coe_mk, LinearMap.smul_apply,
      MultilinearMap.toLinearMap_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 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hsp : LE.le (α := Submodule R M) ⊤ (span R (Set.range v))
k : ι
⊢ HMul.hMul (α := R) (β := R) ((e.det : (a : ι → M) → R) v : R) (((Basis.mk hli hsp).coord k : (a : M) → R) (v k) : R) =
    ((↑e.det : MultilinearMap R (fun (x : ι) ↦ M) R) : (a : (i : ι) → M) → R) (update (β := fun (x : ι) ↦ M) v k (v k))
have inl : Eq.{u_1 + 1} (α := R) ((e.det : (a : ι → M) → R) v : R)
  (((↑e.det : MultilinearMap R (fun (x : ι) ↦ M) R) : (a : (i : ι) → M) → R) v : R)
Tactic: rw [mk_coord_apply_eq, mul_one, update_eq_self]
-- 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 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hsp : LE.le (α := Submodule R M) ⊤ (span R (Set.range v))
i k : ι
hik : k ≠ i
⊢ HMul.hMul (α := R) (β := R) ((e.det : (a : ι → M) → R) v : R) (((Basis.mk hli hsp).coord i : (a : M) → R) (v k) : R) =
    ((↑e.det : MultilinearMap R (fun (x : ι) ↦ M) R) : (a : (i : ι) → M) → R) (update (β := fun (x : ι) ↦ M) v i (v k))
have inr : Eq.{u_1 + 1} (α := R)
  (((↑e.det : MultilinearMap R (fun (x : ι) ↦ M) R) : (a : (i : ι) → M) → R) (update (β := fun (x : ι) ↦ M) v i (v k)) :
    R)
  (0 : R)
Tactic: rw [mk_coord_apply_ne hik, mul_zero, eq_comm]
-- 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 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
w : ι → Rˣ
⊢ (e.unitsSMul w).det = HSMul.hSMul (α := R) (↑(∏ i : ι, w i)⁻¹ : R) e.det
have H : ∀ (f : ι → M),
  Eq.{u_1 + 1} (α := R) (((e.unitsSMul w).det : (a : ι → M) → R) f : R)
    ((HSMul.hSMul (α := R) (↑(∏ i : ι, w i)⁻¹ : R) e.det : (a : ι → M) → R) f : R)
Tactic: ext 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
ι : Type u_4
inst_3 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
w : ι → Rˣ
f : ι → M
⊢ Eq.{u_1 + 1} (α := R) (((e.unitsSMul w).det : (a : ι → M) → R) f : R)
    ((HSMul.hSMul (α := R) (↑(∏ i : ι, w i)⁻¹ : R) e.det : (a : ι → M) → R) f : R)
have H : (Matrix.det.{u_1, u_4} (n := ι) fun (i j : ι) ↦
    ((((e.unitsSMul w).repr : (a : M) → ι →₀ R) (f j) : ι →₀ R) : (a : ι) → R) i) =
  HSMul.hSMul (α := R) (β := R) (↑(∏ i : ι, w i)⁻¹ : R)
    (Matrix.det.{u_1, u_4} (n := ι) fun (i j : ι) ↦ (((e.repr : (a : M) → ι →₀ R) (f j) : ι →₀ R) : (a : ι) → R) i)
Tactic: change
    (Matrix.det fun i j => (e.unitsSMul w).repr (f j) i) =
      (↑(∏ i, w i)⁻¹ : R) • Matrix.det fun i j => e.repr (f j) i
-- 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 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
w : ι → Rˣ
f : ι → M
⊢ (Matrix.det.{u_1, u_4} (n := ι) fun (i j : ι) ↦
      ((((e.unitsSMul w).repr : (a : M) → ι →₀ R) (f j) : ι →₀ R) : (a : ι) → R) i) =
    HSMul.hSMul (α := R) (β := R) (↑(∏ i : ι, w i)⁻¹ : R)
      (Matrix.det.{u_1, u_4} (n := ι) fun (i j : ι) ↦ (((e.repr : (a : M) → ι →₀ R) (f j) : ι →₀ R) : (a : ι) → R) i)
have H : (Matrix.det.{u_1, u_4} (n := ι) fun (i j : ι) ↦
    HSMul.hSMul (β := R) (w i)⁻¹ ((((e.repr : (a : M) → ι →₀ R) (f j) : ι →₀ R) : (a : ι) → R) i : R)) =
  HSMul.hSMul (α := R) (β := R) (↑(∏ i : ι, w i)⁻¹ : R)
    (Matrix.det.{u_1, u_4} (n := ι) fun (i j : ι) ↦ (((e.repr : (a : M) → ι →₀ R) (f j) : ι →₀ R) : (a : ι) → R) i)
Tactic: simp only [e.repr_unitsSMul]
-- 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 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
w : ι → Rˣ
f : ι → M
⊢ (Matrix.det.{u_1, u_4} (n := ι) fun (i j : ι) ↦
      HSMul.hSMul (β := R) (w i)⁻¹ ((((e.repr : (a : M) → ι →₀ R) (f j) : ι →₀ R) : (a : ι) → R) i : R)) =
    HSMul.hSMul (α := R) (β := R) (↑(∏ i : ι, w i)⁻¹ : R)
      (Matrix.det.{u_1, u_4} (n := ι) fun (i j : ι) ↦ (((e.repr : (a : M) → ι →₀ R) (f j) : ι →₀ R) : (a : ι) → R) i)
have h : Eq.{u_1 + 1} (α := R) (↑(∏ i : ι, w i)⁻¹ : R) (∏ i : ι, (↑(w i)⁻¹ : R))
Tactic: convert! Matrix.det_mul_column (fun i => (↑(w i)⁻¹ : R)) fun i j => e.repr (f j) i
-- 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 : Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
⊢ Eq.{u_1 + 1} (α := R)
    (((LinearMap.det (M := Dual R M) (A := R) : (Dual R M →ₗ[R] Dual R M) →* R) : (a : Dual R M →ₗ[R] Dual R M) → R)
        f.dualMap :
      R)
    ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
have have : ∀ (this : Fintype (Free.ChooseBasisIndex R M)),
  Eq.{u_1 + 1} (α := R)
    (((LinearMap.det (M := Dual R M) (A := R) : (Dual R M →ₗ[R] Dual R M) →* R) : (a : Dual R M →ₗ[R] Dual R M) → R)
        f.dualMap :
      R)
    ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
Tactic: have : Fintype (Module.Free.ChooseBasisIndex R M) :=
    Module.Free.ChooseBasisIndex.fintype 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
inst_3 : Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
this : Fintype (Free.ChooseBasisIndex R M)
⊢ Eq.{u_1 + 1} (α := R)
    (((LinearMap.det (M := Dual R M) (A := R) : (Dual R M →ₗ[R] Dual R M) →* R) : (a : Dual R M →ₗ[R] Dual R M) → R)
        f.dualMap :
      R)
    ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
have rw : Eq.{u_1 + 1} (α := R)
  (det.{u_1, u_2} (n := Free.ChooseBasisIndex R M)
    ((toMatrix b.dualBasis b.dualBasis :
        (a : Dual R M →ₗ[R] Dual R M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R)
      f.dualMap))
  (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 [← LinearMap.det_toMatrix b, ← LinearMap.det_toMatrix b.dualBasis]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_6
V : Type u_7
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Finite R V
W : Submodule R V
inst_4 : Free.{u_6, u_7} R ↥W
inst_5 : Module.Finite.{u_6, u_7} R ↥W
inst_6 : Free.{u_6, u_7} R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW : (a : ↥W →ₗ[R] ↥W) → Matrix m m R) (e.restrict he)
B : Matrix m n R :=
  (of : (a : m → n → R) → Matrix m n R) fun (i : m) (l : n) ↦
    ((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R)
            ((e : (a : V) → V) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inr l) : V)) :
          Finsupp.{u_7, u_6} (m ⊕ n) R) :
        (a : m ⊕ n) → R)
      (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ : (a : V ⧸ W →ₗ[R] V ⧸ W) → Matrix n n R) (W.mapQ W e he)
this : (toMatrix b b : (a : V →ₗ[R] V) → Matrix (m ⊕ n) (m ⊕ n) R) e = fromBlocks A B 0 D
⊢ (LinearMap.det : (a : V →ₗ[R] V) → R) e =
    HMul.hMul (α := R) (β := R) ((LinearMap.det : (a : ↥W →ₗ[R] ↥W) → R) (e.restrict he) : R)
      ((LinearMap.det : (a : V ⧸ W →ₗ[R] V ⧸ W) → R) (W.mapQ W e he) : R)
have rw : Matrix.det.{u_6, u_7} (n := m ⊕ n) ((toMatrix b b : (a : V →ₗ[R] V) → Matrix (m ⊕ n) (m ⊕ n) R) e) =
  HMul.hMul (α := R) (β := R) ((LinearMap.det : (a : ↥W →ₗ[R] ↥W) → R) (e.restrict he) : R)
    ((LinearMap.det : (a : V ⧸ W →ₗ[R] V ⧸ W) → R) (W.mapQ W e he) : R)
Tactic: rw [← LinearMap.det_toMatrix b, this, ← LinearMap.det_toMatrix bW,
      ← LinearMap.det_toMatrix bQ, Matrix.det_fromBlocks_zero₂₁]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_6
V : Type u_7
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Finite R V
W : Submodule R V
inst_4 : Free.{u_6, u_7} R ↥W
inst_5 : Module.Finite.{u_6, u_7} R ↥W
inst_6 : Free.{u_6, u_7} R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW : (a : ↥W →ₗ[R] ↥W) → Matrix m m R) (e.restrict he)
B : Matrix m n R :=
  (of : (a : m → n → R) → Matrix m n R) fun (i : m) (l : n) ↦
    ((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R)
            ((e : (a : V) → V) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inr l) : V)) :
          Finsupp.{u_7, u_6} (m ⊕ n) R) :
        (a : m ⊕ n) → R)
      (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ : (a : V ⧸ W →ₗ[R] V ⧸ W) → Matrix n n R) (W.mapQ W e he)
this : (toMatrix b b : (a : V →ₗ[R] V) → Matrix (m ⊕ n) (m ⊕ n) R) e = fromBlocks A B 0 D
rw :
  Matrix.det.{u_6, u_7} (n := m ⊕ n) ((toMatrix b b : (a : V →ₗ[R] V) → Matrix (m ⊕ n) (m ⊕ n) R) e) =
    HMul.hMul (α := R) (β := R) ((LinearMap.det : (a : ↥W →ₗ[R] ↥W) → R) (e.restrict he) : R)
      ((LinearMap.det : (a : V ⧸ W →ₗ[R] V ⧸ W) → R) (W.mapQ W e he) : R)
⊢ (LinearMap.det : (a : V →ₗ[R] V) → R) e =
    HMul.hMul (α := R) (β := R) ((LinearMap.det : (a : ↥W →ₗ[R] ↥W) → R) (e.restrict he) : R)
      ((LinearMap.det : (a : V ⧸ W →ₗ[R] V ⧸ W) → R) (W.mapQ W e he) : R)
have rw₁ : (fromBlocks A B 0 D).det =
  HMul.hMul (α := R) (β := R) ((LinearMap.det : (a : ↥W →ₗ[R] ↥W) → R) (e.restrict he) : R)
    ((LinearMap.det : (a : V ⧸ W →ₗ[R] V ⧸ W) → R) (W.mapQ W e he) : R)
Tactic: rw [← LinearMap.det_toMatrix b, this, ← LinearMap.det_toMatrix bW,
      ← LinearMap.det_toMatrix bQ, Matrix.det_fromBlocks_zero₂₁]