awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ (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) (β := Matrix ι ι A)
      ((LinearMap.toMatrix e e : (a : M →ₗ[A] M) → Matrix ι ι A) f : Matrix ι ι A)
      ((LinearMap.toMatrix e e : (a : M →ₗ[A] M) → Matrix ι ι A) ((e.constr ℕ : (a : ι → M) → M →ₗ[A] M) v) :
        Matrix ι ι A)).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
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
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) (β := Matrix ι ι A)
        ((LinearMap.toMatrix e e : (a : M →ₗ[A] M) → Matrix ι ι A) f : Matrix ι ι A)
        ((LinearMap.toMatrix e e : (a : M →ₗ[A] M) → Matrix ι ι A) ((e.constr ℕ : (a : ι → M) → M →ₗ[A] M) v) :
          Matrix ι ι A)).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₆ : Eq.{u_5 + 1} (α := A)
  (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))))
  (Matrix.det.{u_5, u_4} (n := ι)
    ((LinearMap.toMatrix e e : (a : M →ₗ[A] M) → Matrix ι ι A) (f ∘ₗ (e.constr ℕ : (a : ι → M) → M →ₗ[A] M) v)))
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
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
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) (β := Matrix ι ι A)
        ((LinearMap.toMatrix e e : (a : M →ₗ[A] M) → Matrix ι ι A) f : Matrix ι ι A)
        ((LinearMap.toMatrix e e : (a : M →ₗ[A] M) → Matrix ι ι A) ((e.constr ℕ : (a : ι → M) → M →ₗ[A] M) v) :
          Matrix ι ι A)).det
rw₆ :
  Eq.{u_5 + 1} (α := A)
    (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))))
    (Matrix.det.{u_5, u_4} (n := ι)
      ((LinearMap.toMatrix e e : (a : M →ₗ[A] M) → Matrix ι ι A) (f ∘ₗ (e.constr ℕ : (a : ι → M) → M →ₗ[A] M) v)))
⊢ (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₇ : Eq.{u_5 + 1} (α := A)
  (Matrix.det.{u_5, u_4} (n := ι)
    ((LinearMap.toMatrix e e : (a : M →ₗ[A] M) → Matrix ι ι A) (f ∘ₗ (e.constr ℕ : (a : ι → M) → M →ₗ[A] M) v)))
  (Matrix.det.{u_5, u_4} (n := ι)
    ((LinearMap.toMatrix e e : (a : M →ₗ[A] M) → Matrix ι ι A) (f ∘ₗ (e.constr ℕ : (a : ι → M) → M →ₗ[A] M) v)))
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
M' : Type u_3
inst_1 : AddCommGroup M'
ι : Type u_4
inst_2 : DecidableEq ι
inst_3 : Fintype ι
A : Type u_5
inst_4 : CommRing A
inst_5 : Module A M
inst_6 : Module A M'
b : Basis ι A M
b' : Basis ι A M'
f : M →ₗ[A] M'
⊢ Eq.{u_5 + 1} (α := A)
    ((b'.det : (a : ι → M') → A)
        (Function.comp.{u_4 + 1, u_2 + 1, u_3 + 1} (β := M) (⇑f : (a : M) → M') (⇑b : (a : ι) → M)) :
      A)
    ((LinearMap.det : (a : M' →ₗ[A] M') → A) (f ∘ₗ (↑(b'.equiv b (Equiv.refl ι)) : M' →ₗ[A] M)) : A)
have rw : Matrix.det (b'.toMatrix (Function.comp.{u_4 + 1, u_2 + 1, u_3 + 1} (β := M) (⇑f : (a : M) → M') (⇑b : (a : ι) → M))) =
  Matrix.det.{u_5, u_4} (n := ι) ((LinearMap.toMatrix b b' : (a : M →ₗ[A] M') → Matrix ι ι A) f)
Tactic: rw [det_apply, ← LinearMap.det_toMatrix b', LinearMap.toMatrix_comp _ b, Matrix.det_mul,
    LinearMap.toMatrix_basis_equiv, Matrix.det_one, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
M' : Type u_3
inst_1 : AddCommGroup M'
ι : Type u_4
inst_2 : DecidableEq ι
inst_3 : Fintype ι
A : Type u_5
inst_4 : CommRing A
inst_5 : Module A M
inst_6 : Module A M'
b : Basis ι A M
b' : Basis ι A M'
f : M →ₗ[A] M'
⊢ Matrix.det (b'.toMatrix (Function.comp.{u_4 + 1, u_2 + 1, u_3 + 1} (β := M) (⇑f : (a : M) → M') (⇑b : (a : ι) → M))) =
    Matrix.det.{u_5, u_4} (n := ι) ((LinearMap.toMatrix b b' : (a : M →ₗ[A] M') → Matrix ι ι A) f)
have e_M : Eq (α := Matrix ι ι A)
  (b'.toMatrix (Function.comp.{u_4 + 1, u_2 + 1, u_3 + 1} (β := M) (⇑f : (a : M) → M') (⇑b : (a : ι) → M)))
  ((LinearMap.toMatrix b b' : (a : M →ₗ[A] M') → Matrix ι ι A) f)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
M' : Type u_3
inst_1 : AddCommGroup M'
ι : Type u_4
inst_2 : DecidableEq ι
inst_3 : Fintype ι
A : Type u_5
inst_4 : CommRing A
inst_5 : Module A M
inst_6 : Module A M'
b : Basis ι A M
b' : Basis ι A M'
f : M →ₗ[A] M'
⊢ Eq (α := Matrix ι ι A)
    (b'.toMatrix (Function.comp.{u_4 + 1, u_2 + 1, u_3 + 1} (β := M) (⇑f : (a : M) → M') (⇑b : (a : ι) → M)))
    ((LinearMap.toMatrix b b' : (a : M →ₗ[A] M') → Matrix ι ι A) f)
have e_M : ∀ (i j : ι),
  b'.toMatrix (Function.comp.{u_4 + 1, u_2 + 1, u_3 + 1} (β := M) (⇑f : (a : M) → M') (⇑b : (a : ι) → M)) i j =
    (LinearMap.toMatrix b b' : (a : M →ₗ[A] M') → Matrix ι ι A) f i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
M' : Type u_3
inst_1 : AddCommGroup M'
ι : Type u_4
inst_2 : DecidableEq ι
inst_3 : Fintype ι
A : Type u_5
inst_4 : CommRing A
inst_5 : Module A M
inst_6 : Module A M'
b : Basis ι A M
b' : Basis ι A M'
f : M →ₗ[A] M'
i j : ι
⊢ b'.toMatrix (Function.comp.{u_4 + 1, u_2 + 1, u_3 + 1} (β := M) (⇑f : (a : M) → M') (⇑b : (a : ι) → M)) i j =
    (LinearMap.toMatrix b b' : (a : M →ₗ[A] M') → Matrix ι ι A) f i j
have e_M : Eq.{u_5 + 1} (α := A)
  (((b'.repr : (a : M') → ι →₀ A)
          (Function.comp.{u_4 + 1, u_2 + 1, u_3 + 1} (β := M) (⇑f : (a : M) → M') (⇑b : (a : ι) → M) j) :
        (a : ι) → A)
      i :
    A)
  ((LinearMap.toMatrix b b' : (a : M →ₗ[A] M') → Matrix ι ι A) f i j : A)
Tactic: rw [toMatrix_apply, LinearMap.toMatrix_apply, Function.comp_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
M' : Type u_3
inst_1 : AddCommGroup M'
ι : Type u_4
inst_2 : DecidableEq ι
inst_3 : Fintype ι
A : Type u_5
inst_4 : CommRing A
inst_5 : Module A M
inst_6 : Module A M'
b : Basis ι A M
b' : Basis ι A M'
f : M →ₗ[A] M'
i j : ι
e_M :
  Eq.{u_5 + 1} (α := A)
    (((b'.repr : (a : M') → ι →₀ A)
            (Function.comp.{u_4 + 1, u_2 + 1, u_3 + 1} (β := M) (⇑f : (a : M) → M') (⇑b : (a : ι) → M) j) :
          (a : ι) → A)
        i :
      A)
    ((LinearMap.toMatrix b b' : (a : M →ₗ[A] M') → Matrix ι ι A) f i j : A)
⊢ b'.toMatrix (Function.comp.{u_4 + 1, u_2 + 1, u_3 + 1} (β := M) (⇑f : (a : M) → M') (⇑b : (a : ι) → M)) i j =
    (LinearMap.toMatrix b b' : (a : M →ₗ[A] M') → Matrix ι ι A) f i j
have e_M₁ : Eq.{u_5 + 1} (α := A)
  (((b'.repr : (a : M') → ι →₀ A)
          (Function.comp.{u_4 + 1, u_2 + 1, u_3 + 1} (β := M) (⇑f : (a : M) → M') (⇑b : (a : ι) → M) j) :
        (a : ι) → A)
      i :
    A)
  ((((b'.repr : (a : M') → ι →₀ A) ((f : (a : M) → M') ((b : (a : ι) → M) j : M)) : ι →₀ A) : (a : ι) → A) i : A)
Tactic: rw [toMatrix_apply, LinearMap.toMatrix_apply, Function.comp_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
M' : Type u_3
inst_1 : AddCommGroup M'
ι : Type u_4
inst_2 : DecidableEq ι
inst_3 : Fintype ι
A : Type u_5
inst_4 : CommRing A
inst_5 : Module A M
inst_6 : Module A M'
b : Basis ι A M
b' : Basis ι A M'
f : M →ₗ[A] M'
i j : ι
e_M :
  Eq.{u_5 + 1} (α := A)
    (((b'.repr : (a : M') → ι →₀ A)
            (Function.comp.{u_4 + 1, u_2 + 1, u_3 + 1} (β := M) (⇑f : (a : M) → M') (⇑b : (a : ι) → M) j) :
          (a : ι) → A)
        i :
      A)
    ((LinearMap.toMatrix b b' : (a : M →ₗ[A] M') → Matrix ι ι A) f i j : A)
e_M₁ :
  Eq.{u_5 + 1} (α := A)
    (((b'.repr : (a : M') → ι →₀ A)
            (Function.comp.{u_4 + 1, u_2 + 1, u_3 + 1} (β := M) (⇑f : (a : M) → M') (⇑b : (a : ι) → M) j) :
          (a : ι) → A)
        i :
      A)
    ((((b'.repr : (a : M') → ι →₀ A) ((f : (a : M) → M') ((b : (a : ι) → M) j : M)) : ι →₀ A) : (a : ι) → A) i : A)
⊢ b'.toMatrix (Function.comp.{u_4 + 1, u_2 + 1, u_3 + 1} (β := M) (⇑f : (a : M) → M') (⇑b : (a : ι) → M)) i j =
    (LinearMap.toMatrix b b' : (a : M →ₗ[A] M') → Matrix ι ι A) f i j
have e_M₂ : Eq.{u_5 + 1} (α := A)
  ((((b'.repr : (a : M') → ι →₀ A) ((f : (a : M) → M') ((b : (a : ι) → M) j : M)) : ι →₀ A) : (a : ι) → A) i : A)
  ((((b'.repr : (a : M') → ι →₀ A) ((f : (a : M) → M') ((b : (a : ι) → M) j : M)) : ι →₀ A) : (a : ι) → A) i : A)
Tactic: rw [toMatrix_apply, LinearMap.toMatrix_apply, Function.comp_apply]
-- 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
b b' b'' : Basis ι A M
⊢ Eq (α := (a : ι) → M) (⇑b'' : (a : ι) → M)
    (Function.comp (β := M) (⇑(↑(b'.equiv b'' (Equiv.refl ι)) : M →ₗ[A] M) : (a : M) → M) (⇑b' : (a : ι) → M))
have h : ∀ (x : ι),
  Eq (α := M) ((b'' : (a : ι) → M) x : M)
    (Function.comp (β := M) (⇑(↑(b'.equiv b'' (Equiv.refl ι)) : M →ₗ[A] M) : (a : M) → M) (⇑b' : (a : ι) → M) x : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (hypothesis)
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
b b' b'' : Basis ι A M
⊢ HMul.hMul (α := A) (β := A) ((b.det : (a : ι → M) → A) (⇑b' : (a : ι) → M) : A)
      ((b'.det : (a : ι → M) → A) (⇑b'' : (a : ι) → M) : A) =
    (b.det : (a : ι → M) → A) (⇑b'' : (a : ι) → M)
have this : Eq (α := (a : ι) → M) (⇑b'' : (a : ι) → M)
  (Function.comp (β := M) (⇑(↑(b'.equiv b'' (Equiv.refl ι)) : M →ₗ[A] M) : (a : M) → M) (⇑b' : (a : ι) → M))
Tactic: have : b'' = (b'.equiv b'' (Equiv.refl ι)).toLinearMap ∘ b' := by
    ext; simp
-- 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
b b' b'' : Basis ι A M
this :
  Eq (α := (a : ι) → M) (⇑b'' : (a : ι) → M)
    (Function.comp (β := M) (⇑(↑(b'.equiv b'' (Equiv.refl ι)) : M →ₗ[A] M) : (a : M) → M) (⇑b' : (a : ι) → M))
| (b.det : (a : ι → M) → A) (⇑b'' : (a : ι) → M)
have rw : HMul.hMul (α := A) (β := A) ((b.det : (a : ι → M) → A) (⇑b' : (a : ι) → M) : A)
  ((b'.det : (a : ι → M) → A) (⇑b'' : (a : ι) → M) : A)
Tactic: rw [this, Basis.det_comp, det_basis, mul_comm]
-- 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
b b' b'' : Basis ι A M
this :
  Eq (α := (a : ι) → M) (⇑b'' : (a : ι) → M)
    (Function.comp (β := M) (⇑(↑(b'.equiv b'' (Equiv.refl ι)) : M →ₗ[A] M) : (a : M) → M) (⇑b' : (a : ι) → M))
⊢ HMul.hMul (α := A) (β := A) ((b.det : (a : ι → M) → A) (⇑b' : (a : ι) → M) : A)
      ((b'.det : (a : ι → M) → A) (⇑b'' : (a : ι) → M) : A) =
    (b.det : (a : ι → M) → A) (⇑b'' : (a : ι) → M)
have conv_rhs : HMul.hMul (α := A) (β := A) ((b.det : (a : ι → M) → A) (⇑b' : (a : ι) → M) : A)
    ((b'.det : (a : ι → M) → A) (⇑b'' : (a : ι) → M) : A) =
  (b.det : (a : ι → M) → A) (⇑b'' : (a : ι) → M)
Tactic: conv_rhs =>
    rw [this, Basis.det_comp, det_basis, mul_comm]
-- 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
b b' b'' : Basis ι A M
this :
  Eq (α := (a : ι) → M) (⇑b'' : (a : ι) → M)
    (Function.comp (β := M) (⇑(↑(b'.equiv b'' (Equiv.refl ι)) : M →ₗ[A] M) : (a : M) → M) (⇑b' : (a : ι) → M))
conv_rhs :
  HMul.hMul (α := A) (β := A) ((b.det : (a : ι → M) → A) (⇑b' : (a : ι) → M) : A)
      ((b'.det : (a : ι → M) → A) (⇑b'' : (a : ι) → M) : A) =
    (b.det : (a : ι → M) → A) (⇑b'' : (a : ι) → M)
⊢ HMul.hMul (α := A) (β := A) ((b.det : (a : ι → M) → A) (⇑b' : (a : ι) → M) : A)
      ((b'.det : (a : ι → M) → A) (⇑b'' : (a : ι) → M) : A) =
    (b.det : (a : ι → M) → A) (⇑b'' : (a : ι) → M)
have conv_rhs₁ : HMul.hMul (α := A) (β := A) ((b.det : (a : ι → M) → A) (⇑b' : (a : ι) → M) : A)
    ((b'.det : (a : ι → M) → A) (⇑b'' : (a : ι) → M) : A) =
  HMul.hMul (α := A) (β := A) ((b.det : (a : ι → M) → A) (⇑b' : (a : ι) → M) : A)
    ((b'.det : (a : ι → M) → A) (⇑b'' : (a : ι) → M) : A)
Tactic: conv_rhs =>
    rw [this, Basis.det_comp, det_basis, mul_comm]
-- 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
b b' : Basis ι A M
⊢ (↑(IsUnit.unit (a := (b.det : (a : ι → M) → A) (⇑b' : (a : ι) → M)) ⋯)⁻¹ : A) =
    (b'.det : (a : ι → M) → A) (⇑b : (a : ι) → M)
have rw : HMul.hMul (α := A) (β := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) (↑(b.equiv b' (Equiv.refl ι)) : M →ₗ[A] M) : A)
    ((LinearMap.det : (a : M →ₗ[A] M) → A) (↑(b'.equiv b (Equiv.refl ι)) : M →ₗ[A] M) : A) =
  1
Tactic: rw [← Units.mul_eq_one_iff_inv_eq, IsUnit.unit_spec, ← det_basis, ← det_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 ι
ι' : Type u_6
inst_5 : Fintype ι'
inst_6 : DecidableEq ι'
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
⊢ Eq.{u_1 + 1} (α := R) (((b.reindex e).det : (a : ι' → M) → R) v : R)
    ((b.det : (a : ι → M) → R) (v ∘ (⇑e : (a : ι) → ι')) : R)
have rw : ((b.reindex e).toMatrix v).det = (b.det : (a : ι → M) → R) (v ∘ (⇑e : (a : ι) → ι'))
Tactic: rw [det_apply, toMatrix_reindex', det_reindexAlgEquiv, 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 ι
ι' : Type u_6
inst_5 : Fintype ι'
inst_6 : DecidableEq ι'
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
rw : ((b.reindex e).toMatrix v).det = (b.det : (a : ι → M) → R) (v ∘ (⇑e : (a : ι) → ι'))
⊢ Eq.{u_1 + 1} (α := R) (((b.reindex e).det : (a : ι' → M) → R) v : R)
    ((b.det : (a : ι → M) → R) (v ∘ (⇑e : (a : ι) → ι')) : R)
have rw₁ : Eq.{u_1 + 1} (α := R)
  (Matrix.det.{u_1, u_6} (n := ι')
      ((reindexAlgEquiv R R e : (a : Matrix ι ι R) → Matrix ι' ι' R) (b.toMatrix (v ∘ (⇑e : (a : ι) → ι')))) :
    R)
  ((b.det : (a : ι → M) → R) (v ∘ (⇑e : (a : ι) → ι')) : R)
Tactic: rw [det_apply, toMatrix_reindex', det_reindexAlgEquiv, 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 ι
ι' : Type u_6
inst_5 : Fintype ι'
inst_6 : DecidableEq ι'
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
rw : ((b.reindex e).toMatrix v).det = (b.det : (a : ι → M) → R) (v ∘ (⇑e : (a : ι) → ι'))
rw₁ :
  Eq.{u_1 + 1} (α := R)
    (Matrix.det.{u_1, u_6} (n := ι')
        ((reindexAlgEquiv R R e : (a : Matrix ι ι R) → Matrix ι' ι' R) (b.toMatrix (v ∘ (⇑e : (a : ι) → ι')))) :
      R)
    ((b.det : (a : ι → M) → R) (v ∘ (⇑e : (a : ι) → ι')) : R)
⊢ Eq.{u_1 + 1} (α := R) (((b.reindex e).det : (a : ι' → M) → R) v : R)
    ((b.det : (a : ι → M) → R) (v ∘ (⇑e : (a : ι) → ι')) : R)
have rw₂ : Matrix.det (b.toMatrix (v ∘ (⇑e : (a : ι) → ι'))) = (b.det : (a : ι → M) → R) (v ∘ (⇑e : (a : ι) → ι'))
Tactic: rw [det_apply, toMatrix_reindex', det_reindexAlgEquiv, 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 ι
ι' : Type u_6
inst_5 : Fintype ι'
inst_6 : DecidableEq ι'
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
rw : ((b.reindex e).toMatrix v).det = (b.det : (a : ι → M) → R) (v ∘ (⇑e : (a : ι) → ι'))
rw₁ :
  Eq.{u_1 + 1} (α := R)
    (Matrix.det.{u_1, u_6} (n := ι')
        ((reindexAlgEquiv R R e : (a : Matrix ι ι R) → Matrix ι' ι' R) (b.toMatrix (v ∘ (⇑e : (a : ι) → ι')))) :
      R)
    ((b.det : (a : ι → M) → R) (v ∘ (⇑e : (a : ι) → ι')) : R)
rw₂ : Matrix.det (b.toMatrix (v ∘ (⇑e : (a : ι) → ι'))) = (b.det : (a : ι → M) → R) (v ∘ (⇑e : (a : ι) → ι'))
⊢ Eq.{u_1 + 1} (α := R) (((b.reindex e).det : (a : ι' → M) → R) v : R)
    ((b.det : (a : ι → M) → R) (v ∘ (⇑e : (a : ι) → ι')) : R)
have rw₃ : Matrix.det (b.toMatrix (v ∘ (⇑e : (a : ι) → ι'))) = Matrix.det (b.toMatrix (v ∘ (⇑e : (a : ι) → ι')))
Tactic: rw [det_apply, toMatrix_reindex', det_reindexAlgEquiv, 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 ι
ι' : Type u_6
inst_5 : Fintype ι'
inst_6 : DecidableEq ι'
b : Basis ι R M
v : ι → M
e : ι' ≃ ι
⊢ 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)
      (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)
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
ι : 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)
⊢ 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 ∘ Function.comp.{u_4 + 1, u_6 + 1, u_4 + 1} (β := ι') (⇑e : (a : ι') → ι) (⇑e.symm : (a : ι) → ι')) :
    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
ι : 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)
⊢ 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 ∘ _root_.id) : R) ((b.det : (a : ι → M) → R) v : R)
Tactic: rw [det_reindex, Function.comp_assoc, e.self_comp_symm, Function.comp_id]