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
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((f' : (a : M) → M) ((e : (a : M) → M) x : M) : M)
this :
  Associated.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (f' ∘ₗ (↑e : M →ₗ[R] M)) : R)
    ((LinearMap.det : (a : M →ₗ[R] M) → R) f' : R)
⊢ f = f' ∘ₗ (↑e : M →ₗ[R] M)
have h₁ : ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((f' ∘ₗ (↑e : M →ₗ[R] M) : (a : M) → M) x : M)
Tactic: ext x
-- 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
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((f' : (a : M) → M) ((e : (a : M) → M) x : M) : M)
⊢ Associated.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f' : R)
have suffices : Associated.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (f' ∘ₗ (↑e : M →ₗ[R] M)) : R)
  ((LinearMap.det : (a : M →ₗ[R] M) → R) f' : R)
Tactic: suffices Associated (LinearMap.det (f' ∘ₗ ↑e)) (LinearMap.det f') by
    convert! this using 2
    ext x
    exact h x
-- 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
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((f' : (a : M) → M) ((e : (a : M) → M) x : M) : M)
⊢ Associated.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (f' ∘ₗ (↑e : M →ₗ[R] M)) : R)
    ((LinearMap.det : (a : M →ₗ[R] M) → R) f' : R)
have rw : Associated
  (HMul.hMul (α := R) (β := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f' : R)
    ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑e : M →ₗ[R] M) : R))
  (HMul.hMul (α := R) (β := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f' : R) (1 : R))
Tactic: rw [← mul_one (LinearMap.det f'), LinearMap.det_comp]
-- 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
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
f : N →ₗ[R] M
e e' : M ≃ₗ[R] N
⊢ Associated.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (f ∘ₗ (↑e : M →ₗ[R] N)) : R)
    ((LinearMap.det : (a : M →ₗ[R] M) → R) (f ∘ₗ (↑e' : M →ₗ[R] N)) : R)
have refine : ∀ (x : M),
  Eq (α := M) ((f ∘ₗ (↑e : M →ₗ[R] N) : (a : M) → M) x : M)
    ((f ∘ₗ (↑e' : M →ₗ[R] N) : (a : M) → M) ((e ≪≫ₗ e'.symm : (a : M) → M) x : M) : M)
Tactic: refine LinearMap.associated_det_of_eq_comp (e.trans e'.symm) _ _ ?_
-- 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 ι
e : Basis ι R M
u : (i : ι) → M
i : ι
c : R
x : M
⊢ (fun (v : (i : ι) → M) ↦ (e.toMatrix v).det) (update (β := fun (x : ι) ↦ M) u i (c • x)) =
    HSMul.hSMul (β := R) c ((fun (v : (i : ι) → M) ↦ (e.toMatrix v).det) (update (β := fun (x : ι) ↦ M) u i x))
have simp : ((e.toMatrix u).updateCol i
      (⇑(HSMul.hSMul (β := ι →₀ R) c ((e.repr : (a : M) → ι →₀ R) x : ι →₀ R)) : (a : ι) → R)).det =
  c * ((e.toMatrix u).updateCol i (⇑((e.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R)).det
Tactic: simp only [e.toMatrix_update, smul_eq_mul, map_smul]
-- 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 ι
e : Basis ι R M
v : ι → M
i j : ι
h : v i = v j
hij : i ≠ j
⊢ Eq.{u_1 + 1} (α := R)
    (MultilinearMap.toFun (R := R) (M₁ := fun (x : ι) ↦ M)
      (MultilinearMap.mk' (M₁ := fun (x : ι) ↦ M) (fun (v : (i : ι) → M) ↦ (e.toMatrix v).det) ⋯ ⋯) v)
    0
have dsimp : (e.toMatrix v).det = 0
Tactic: dsimp
-- 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 ι
e : Basis ι R M
v : ι → M
i j : ι
h : v i = v j
hij : i ≠ j
⊢ (e.toMatrix v).det = 0
have rw : ((e.toMatrix v)ᵀ.updateRow i ((e.toMatrix v)ᵀ j)).det = 0
Tactic: rw [← Function.update_eq_self i v, h, ← det_transpose, e.toMatrix_update, ← updateRow_transpose,
      ← e.toMatrix_transpose_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 ι
e : Basis ι R M
v : ι → M
i j : ι
h : v i = v j
hij : i ≠ j
⊢ ((e.toMatrix v)ᵀ.updateRow i ((e.toMatrix v)ᵀ j)).det = 0
have apply : (e.toMatrix v)ᵀ.updateRow i ((e.toMatrix v)ᵀ j) i = (e.toMatrix v)ᵀ.updateRow i ((e.toMatrix v)ᵀ j) j
Tactic: apply det_zero_of_row_eq hij
-- 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 ι
e : Basis ι R M
v : ι → M
i j : ι
h : v i = v j
hij : i ≠ j
⊢ (e.toMatrix v)ᵀ.updateRow i ((e.toMatrix v)ᵀ j) i = (e.toMatrix v)ᵀ.updateRow i ((e.toMatrix v)ᵀ j) j
have rw : (e.toMatrix v)ᵀ.updateRow i ((e.toMatrix v)ᵀ j) i = (e.toMatrix v)ᵀ j
Tactic: rw [updateRow_ne hij.symm, updateRow_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
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
e : Basis ι R M
v : ι → M
i j : ι
h : v i = v j
hij : i ≠ j
rw : (e.toMatrix v)ᵀ.updateRow i ((e.toMatrix v)ᵀ j) i = (e.toMatrix v)ᵀ j
⊢ (e.toMatrix v)ᵀ.updateRow i ((e.toMatrix v)ᵀ j) i = (e.toMatrix v)ᵀ.updateRow i ((e.toMatrix v)ᵀ j) j
have rw₁ : (e.toMatrix v)ᵀ j = (e.toMatrix v)ᵀ j
Tactic: rw [updateRow_ne hij.symm, updateRow_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
inst_5 : IsEmpty ι
⊢ e.det = AlternatingMap.constOfIsEmpty R M ι 1
have H : ∀ (v : ι → M),
  Eq.{u_1 + 1} (α := R) ((e.det : (a : ι → M) → R) v : R)
    ((AlternatingMap.constOfIsEmpty R M ι 1 : (a : ι → M) → R) v : R)
Tactic: ext v
-- 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
G : Type u_5
inst_5 : Group G
inst_6 : DistribMulAction G M
inst_7 : SMulCommClass G R M
g : G
v : ι → M
⊢ Eq.{u_1 + 1} (α := R) (((g • e).det : (a : ι → M) → R) v : R) ((e.det : (a : ι → M) → R) (g⁻¹ • v) : R)
have simp_rw : ((g • e).toMatrix v).det = (e.toMatrix (g⁻¹ • v)).det
Tactic: simp_rw [det_apply, toMatrix_smul_left]
-- 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
⊢ LinearIndependent R v ∧ Eq (α := Submodule R M) (span R (Set.range v)) ⊤ ↔
    IsUnit.{u_1} (M := R) ((e.det : (a : ι → M) → R) v : R)
have mp : LinearIndependent R v ∧ Eq (α := Submodule R M) (span R (Set.range v)) ⊤ →
  IsUnit.{u_1} (M := R) ((e.det : (a : ι → M) → R) v : 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
ι : Type u_4
inst_3 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
v : ι → M
mp :
  LinearIndependent R v ∧ Eq (α := Submodule R M) (span R (Set.range v)) ⊤ →
    IsUnit.{u_1} (M := R) ((e.det : (a : ι → M) → R) v : R)
⊢ LinearIndependent R v ∧ Eq (α := Submodule R M) (span R (Set.range v)) ⊤ ↔
    IsUnit.{u_1} (M := R) ((e.det : (a : ι → M) → R) v : R)
have mpr : IsUnit.{u_1} (M := R) ((e.det : (a : ι → M) → R) v : R) →
  LinearIndependent R v ∧ Eq (α := Submodule R M) (span R (Set.range v)) ⊤
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
ι : Type u_4
inst_3 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hspan : Eq (α := Submodule R M) (span R (Set.range v)) ⊤
v' : Basis ι R M := Basis.mk hli ⋯
⊢ IsUnit.{u_1} (M := R) ((e.det : (a : ι → M) → R) v : R)
have mp : IsUnit (e.toMatrix v).det
Tactic: rw [e.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
ι : Type u_4
inst_3 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hspan : Eq (α := Submodule R M) (span R (Set.range v)) ⊤
v' : Basis ι R M := Basis.mk hli ⋯
⊢ IsUnit (e.toMatrix v).det
have h : e.toMatrix v = (LinearMap.toMatrix v' e : (a : M →ₗ[R] M) → Matrix ι ι R) (↑(LinearEquiv.refl R M) : M →ₗ[R] M)
Tactic: convert! LinearEquiv.isUnit_det (LinearEquiv.refl R M) v' e using 2
-- 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
hspan : Eq (α := Submodule R M) (span R (Set.range v)) ⊤
v' : Basis ι R M := Basis.mk hli ⋯
⊢ e.toMatrix v = (LinearMap.toMatrix v' e : (a : M →ₗ[R] M) → Matrix ι ι R) (↑(LinearEquiv.refl R M) : M →ₗ[R] M)
have h : ∀ (i j : ι),
  e.toMatrix v i j =
    (LinearMap.toMatrix v' e : (a : M →ₗ[R] M) → Matrix ι ι R) (↑(LinearEquiv.refl R M) : M →ₗ[R] M) i j
Tactic: ext i j
-- 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 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
v : ι → M
h : IsUnit.{u_1} (M := R) ((e.det : (a : ι → M) → R) v : R)
⊢ LinearIndependent R v ∧ Eq (α := Submodule R M) (span R (Set.range v)) ⊤
have h₁ : IsUnit.{u_1} (M := R)
  (Matrix.det.{u_1, u_4} (n := ι)
    ((LinearMap.toMatrix e e : (a : M →ₗ[R] M) → Matrix ι ι R) ((e.constr ℕ : (a : ι → M) → M →ₗ[R] M) v)))
Tactic: rw [Basis.det_apply, Basis.toMatrix_eq_toMatrix_constr] at h
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
ι : Type u_4
inst_3 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
v : ι → M
h :
  IsUnit.{u_1} (M := R)
    (Matrix.det.{u_1, u_4} (n := ι)
      ((LinearMap.toMatrix e e : (a : M →ₗ[R] M) → Matrix ι ι R) ((e.constr ℕ : (a : ι → M) → M →ₗ[R] M) v)))
⊢ LinearIndependent R v ∧ Eq (α := Submodule R M) (span R (Set.range v)) ⊤
have v'_def : let v' := e.map (LinearEquiv.ofIsUnitDet h);
v' = e.map (LinearEquiv.ofIsUnitDet h)
Tactic: set v' := Basis.map e (LinearEquiv.ofIsUnitDet h) with v'_def
-- 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
h :
  IsUnit.{u_1} (M := R)
    (Matrix.det.{u_1, u_4} (n := ι)
      ((LinearMap.toMatrix e e : (a : M →ₗ[R] M) → Matrix ι ι R) ((e.constr ℕ : (a : ι → M) → M →ₗ[R] M) v)))
v' : Basis ι R M := e.map (LinearEquiv.ofIsUnitDet h)
v'_def : v' = e.map (LinearEquiv.ofIsUnitDet h)
⊢ (⇑v' : (a : ι) → M) = v
have h₁ : ∀ (i : ι), (v' : (a : ι) → M) i = v i
Tactic: ext 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
h :
  IsUnit.{u_1} (M := R)
    (Matrix.det.{u_1, u_4} (n := ι)
      ((LinearMap.toMatrix e e : (a : M →ₗ[R] M) → Matrix ι ι R) ((e.constr ℕ : (a : ι → M) → M →ₗ[R] M) v)))
v' : Basis ι R M := e.map (LinearEquiv.ofIsUnitDet h)
v'_def : v' = e.map (LinearEquiv.ofIsUnitDet h)
i : ι
h₁ : (e.map (LinearEquiv.ofIsUnitDet h) : (a : ι) → M) i = v i
⊢ (v' : (a : ι) → M) i = v i
have h₂ : (LinearEquiv.ofIsUnitDet h : (a : M) → M) ((e : (a : ι) → M) i : M) = v i
Tactic: rw [v'_def, Basis.map_apply, LinearEquiv.ofIsUnitDet_apply, e.constr_basis]
-- 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
h :
  IsUnit.{u_1} (M := R)
    (Matrix.det.{u_1, u_4} (n := ι)
      ((LinearMap.toMatrix e e : (a : M →ₗ[R] M) → Matrix ι ι R) ((e.constr ℕ : (a : ι → M) → M →ₗ[R] M) v)))
v' : Basis ι R M := e.map (LinearEquiv.ofIsUnitDet h)
v'_def : v' = e.map (LinearEquiv.ofIsUnitDet h)
i : ι
h₁ : (e.map (LinearEquiv.ofIsUnitDet h) : (a : ι) → M) i = v i
h₂ : (LinearEquiv.ofIsUnitDet h : (a : M) → M) ((e : (a : ι) → M) i : M) = v i
⊢ (v' : (a : ι) → M) i = v i
have h₃ : (((e.constr ℕ : (a : ι → M) → M →ₗ[R] M) v : M →ₗ[R] M) : (a : M) → M) ((e : (a : ι) → M) i : M) = v i
Tactic: rw [v'_def, Basis.map_apply, LinearEquiv.ofIsUnitDet_apply, e.constr_basis]
-- 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
h :
  IsUnit.{u_1} (M := R)
    (Matrix.det.{u_1, u_4} (n := ι)
      ((LinearMap.toMatrix e e : (a : M →ₗ[R] M) → Matrix ι ι R) ((e.constr ℕ : (a : ι → M) → M →ₗ[R] M) v)))
v' : Basis ι R M := e.map (LinearEquiv.ofIsUnitDet h)
v'_def : v' = e.map (LinearEquiv.ofIsUnitDet h)
i : ι
h₁ : (e.map (LinearEquiv.ofIsUnitDet h) : (a : ι) → M) i = v i
h₂ : (LinearEquiv.ofIsUnitDet h : (a : M) → M) ((e : (a : ι) → M) i : M) = v i
h₃ : (((e.constr ℕ : (a : ι → M) → M →ₗ[R] M) v : M →ₗ[R] M) : (a : M) → M) ((e : (a : ι) → M) i : M) = v i
⊢ (v' : (a : ι) → M) i = v i
have h₄ : v i = v i
Tactic: rw [v'_def, Basis.map_apply, LinearEquiv.ofIsUnitDet_apply, e.constr_basis]
-- 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 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
v : ι → M
h :
  IsUnit.{u_1} (M := R)
    (Matrix.det.{u_1, u_4} (n := ι)
      ((LinearMap.toMatrix e e : (a : M →ₗ[R] M) → Matrix ι ι R) ((e.constr ℕ : (a : ι → M) → M →ₗ[R] M) v)))
v' : Basis ι R M := e.map (LinearEquiv.ofIsUnitDet h)
v'_def : v' = e.map (LinearEquiv.ofIsUnitDet h)
⊢ LinearIndependent R v ∧ Eq (α := Submodule R M) (span R (Set.range v)) ⊤
have this : (⇑v' : (a : ι) → M) = v
Tactic: have : ⇑v' = v := by
      ext i
      rw [v'_def, Basis.map_apply, LinearEquiv.ofIsUnitDet_apply, e.constr_basis]
-- 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
h :
  IsUnit.{u_1} (M := R)
    (Matrix.det.{u_1, u_4} (n := ι)
      ((LinearMap.toMatrix e e : (a : M →ₗ[R] M) → Matrix ι ι R) ((e.constr ℕ : (a : ι → M) → M →ₗ[R] M) v)))
v' : Basis ι R M := e.map (LinearEquiv.ofIsUnitDet h)
v'_def : v' = e.map (LinearEquiv.ofIsUnitDet h)
this : (⇑v' : (a : ι) → M) = v
⊢ LinearIndependent R v ∧ Eq (α := Submodule R M) (span R (Set.range v)) ⊤
have mpr : LinearIndependent.{u_4, u_1, u_2} (ι := ι) R (M := M) (⇑v' : (a : ι) → M) ∧
  Eq.{u_2 + 1} (α := Submodule R M) (span R (Set.range.{u_2, u_4 + 1} (ι := ι) (⇑v' : (a : ι) → M))) ⊤
Tactic: rw [← this]
-- 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
f : M [⋀^ι]→ₗ[R] R
⊢ f = HSMul.hSMul (α := R) ((f : (a : ι → M) → R) (⇑e : (a : ι) → M) : R) e.det
have refine : ∀ (i : ι → ι) (h : Injective i),
  Eq.{u_1 + 1} (α := R) ((f : (a : ι → M) → R) fun (i_1 : ι) ↦ (e : (a : ι) → M) (i i_1) : R)
    ((HSMul.hSMul (α := R) ((f : (a : ι → M) → R) (⇑e : (a : ι) → M) : R) e.det : (a : ι → M) → R) fun (i_1 : ι) ↦
        (e : (a : ι) → M) (i i_1) :
      R)
Tactic: refine Basis.ext_alternating e fun i 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 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
f : M [⋀^ι]→ₗ[R] R
i : ι → ι
h : Injective i
σ : Equiv.Perm ι := Equiv.ofBijective i ⋯
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : ι → M) → R) fun (i_1 : ι) ↦ (e : (a : ι) → M) (i i_1) : R)
    ((HSMul.hSMul (α := R) ((f : (a : ι → M) → R) (⇑e : (a : ι) → M) : R) e.det : (a : ι → M) → R) fun (i_1 : ι) ↦
        (e : (a : ι) → M) (i i_1) :
      R)
have change : Eq.{u_1 + 1} (α := R) ((f : (a : ι → M) → R) (Function.comp (β := ι) (⇑e : (a : ι) → M) (⇑σ : (a : ι) → ι)) : R)
  ((HSMul.hSMul (α := R) ((f : (a : ι → M) → R) (⇑e : (a : ι) → M) : R) e.det : (a : ι → M) → R)
      (Function.comp (β := ι) (⇑e : (a : ι) → M) (⇑σ : (a : ι) → ι)) :
    R)
Tactic: change f (e ∘ σ) = (f e • e.det) (e ∘ σ)
-- 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_5
inst_3 : Finite ι
e : Basis ι R M
f : M [⋀^ι]→ₗ[R] R
h : Eq.{u_1 + 1} (α := R) ((f : (a : ι → M) → R) (⇑e : (a : ι) → M) : R) (0 : R)
⊢ f = 0
have intro : ∀ (val : Fintype ι), f = 0
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Type u_5
inst_3 : CommRing A
inst_4 : Module A M
e : Basis ι A M
f : M →ₗ[A] M
v : ι → M
⊢ (e.det : (a : ι → M) → A) ((⇑f : (a : M) → M) ∘ v) =
    HMul.hMul (α := A) (β := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A) ((e.det : (a : ι → M) → A) v : A)
have rw : (e.toMatrix ((⇑f : (a : M) → M) ∘ v)).det =
  HMul.hMul (α := A) (β := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A) ((e.det : (a : ι → M) → A) v : A)
Tactic: rw [det_apply, det_apply, ← f.det_toMatrix e, ← Matrix.det_mul,
    e.toMatrix_eq_toMatrix_constr (f ∘ v), e.toMatrix_eq_toMatrix_constr v, ← toMatrix_comp,
    e.constr_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Type u_5
inst_3 : CommRing A
inst_4 : Module A M
e : Basis ι A M
f : M →ₗ[A] M
v : ι → M
rw :
  (e.toMatrix ((⇑f : (a : M) → M) ∘ v)).det =
    HMul.hMul (α := A) (β := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A) ((e.det : (a : ι → M) → A) v : A)
⊢ (e.det : (a : ι → M) → A) ((⇑f : (a : M) → M) ∘ v) =
    HMul.hMul (α := A) (β := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A) ((e.det : (a : ι → M) → A) v : A)
have rw₁ : (e.toMatrix ((⇑f : (a : M) → M) ∘ v)).det =
  HMul.hMul (α := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A) (e.toMatrix v).det
Tactic: rw [det_apply, det_apply, ← f.det_toMatrix e, ← Matrix.det_mul,
    e.toMatrix_eq_toMatrix_constr (f ∘ v), e.toMatrix_eq_toMatrix_constr v, ← toMatrix_comp,
    e.constr_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Type u_5
inst_3 : CommRing A
inst_4 : Module A M
e : Basis ι A M
f : M →ₗ[A] M
v : ι → M
rw :
  (e.toMatrix ((⇑f : (a : M) → M) ∘ v)).det =
    HMul.hMul (α := A) (β := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A) ((e.det : (a : ι → M) → A) v : A)
rw₁ :
  (e.toMatrix ((⇑f : (a : M) → M) ∘ v)).det =
    HMul.hMul (α := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A) (e.toMatrix v).det
⊢ (e.det : (a : ι → M) → A) ((⇑f : (a : M) → M) ∘ v) =
    HMul.hMul (α := A) (β := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A) ((e.det : (a : ι → M) → A) v : A)
have rw₂ : (e.toMatrix ((⇑f : (a : M) → M) ∘ v)).det =
  Matrix.det.{u_5, u_4} (n := ι) ((LinearMap.toMatrix e e : (a : M →ₗ[A] M) → Matrix ι ι A) f) * (e.toMatrix v).det
Tactic: rw [det_apply, det_apply, ← f.det_toMatrix e, ← Matrix.det_mul,
    e.toMatrix_eq_toMatrix_constr (f ∘ v), e.toMatrix_eq_toMatrix_constr v, ← toMatrix_comp,
    e.constr_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Type u_5
inst_3 : CommRing A
inst_4 : Module A M
e : Basis ι A M
f : M →ₗ[A] M
v : ι → M
rw :
  (e.toMatrix ((⇑f : (a : M) → M) ∘ v)).det =
    HMul.hMul (α := A) (β := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A) ((e.det : (a : ι → M) → A) v : A)
rw₁ :
  (e.toMatrix ((⇑f : (a : M) → M) ∘ v)).det =
    HMul.hMul (α := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A) (e.toMatrix v).det
rw₂ :
  (e.toMatrix ((⇑f : (a : M) → M) ∘ v)).det =
    Matrix.det.{u_5, u_4} (n := ι) ((LinearMap.toMatrix e e : (a : M →ₗ[A] M) → Matrix ι ι A) f) * (e.toMatrix v).det
⊢ (e.det : (a : ι → M) → A) ((⇑f : (a : M) → M) ∘ v) =
    HMul.hMul (α := A) (β := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A) ((e.det : (a : ι → M) → A) v : A)
have rw₃ : (e.toMatrix ((⇑f : (a : M) → M) ∘ v)).det =
  (HMul.hMul (α := Matrix ι ι A) ((LinearMap.toMatrix e e : (a : M →ₗ[A] M) → Matrix ι ι A) f : Matrix ι ι A)
      (e.toMatrix v)).det
Tactic: rw [det_apply, det_apply, ← f.det_toMatrix e, ← Matrix.det_mul,
    e.toMatrix_eq_toMatrix_constr (f ∘ v), e.toMatrix_eq_toMatrix_constr v, ← toMatrix_comp,
    e.constr_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Type u_5
inst_3 : CommRing A
inst_4 : Module A M
e : Basis ι A M
f : M →ₗ[A] M
v : ι → M
rw :
  (e.toMatrix ((⇑f : (a : M) → M) ∘ v)).det =
    HMul.hMul (α := A) (β := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A) ((e.det : (a : ι → M) → A) v : A)
rw₁ :
  (e.toMatrix ((⇑f : (a : M) → M) ∘ v)).det =
    HMul.hMul (α := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A) (e.toMatrix v).det
rw₂ :
  (e.toMatrix ((⇑f : (a : M) → M) ∘ v)).det =
    Matrix.det.{u_5, u_4} (n := ι) ((LinearMap.toMatrix e e : (a : M →ₗ[A] M) → Matrix ι ι A) f) * (e.toMatrix v).det
rw₃ :
  (e.toMatrix ((⇑f : (a : M) → M) ∘ v)).det =
    (HMul.hMul (α := Matrix ι ι A) ((LinearMap.toMatrix e e : (a : M →ₗ[A] M) → Matrix ι ι A) f : Matrix ι ι A)
        (e.toMatrix v)).det
⊢ (e.det : (a : ι → M) → A) ((⇑f : (a : M) → M) ∘ v) =
    HMul.hMul (α := A) (β := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A) ((e.det : (a : ι → M) → A) v : A)
have rw₄ : Matrix.det.{u_5, u_4} (n := ι)
    ((LinearMap.toMatrix e e : (a : M →ₗ[A] M) → Matrix ι ι A)
      ((e.constr ℕ : (a : ι → M) → M →ₗ[A] M) ((⇑f : (a : M) → M) ∘ v))) =
  (HMul.hMul (α := Matrix ι ι A) ((LinearMap.toMatrix e e : (a : M →ₗ[A] M) → Matrix ι ι A) f : Matrix ι ι A)
      (e.toMatrix v)).det
Tactic: rw [det_apply, det_apply, ← f.det_toMatrix e, ← Matrix.det_mul,
    e.toMatrix_eq_toMatrix_constr (f ∘ v), e.toMatrix_eq_toMatrix_constr v, ← toMatrix_comp,
    e.constr_comp]