awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₁
inst_6 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst_7 : Fintype m
M₃ : Type u_7
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
v₃ : Basis l R M₃
inst_10 : Finite l
inst_11 : DecidableEq m
A : Matrix l m R
B : Matrix m n R
x : M₁
⊢ Eq.{u_7 + 1} (α := M₃)
    ((((toLin v₁ v₃ : (a : Matrix l n R) → M₁ →ₗ[R] M₃) (A * B) : M₁ →ₗ[R] M₃) : (a : M₁) → M₃) x : M₃)
    ((((toLin v₂ v₃ : (a : Matrix l m R) → M₂ →ₗ[R] M₃) A : M₂ →ₗ[R] M₃) : (a : M₂) → M₃)
        ((((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) B : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x : M₂) :
      M₃)
have rw : Eq.{u_7 + 1} (α := M₃)
  (((toLin v₂ v₃ : (a : Matrix l m R) → M₂ →ₗ[R] M₃) A ∘ₗ (toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) B :
        (a : M₁) → M₃)
      x :
    M₃)
  ((((toLin v₂ v₃ : (a : Matrix l m R) → M₂ →ₗ[R] M₃) A : M₂ →ₗ[R] M₃) : (a : M₂) → M₃)
      ((((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) B : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x : M₂) :
    M₃)
Tactic: rw [Matrix.toLin_mul v₁ v₂, LinearMap.comp_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₁
inst_6 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst_7 : Fintype m
M₃ : Type u_7
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
v₃ : Basis l R M₃
inst_10 : Finite l
inst_11 : DecidableEq m
A : Matrix l m R
B : Matrix m n R
x : M₁
rw :
  Eq.{u_7 + 1} (α := M₃)
    (((toLin v₂ v₃ : (a : Matrix l m R) → M₂ →ₗ[R] M₃) A ∘ₗ (toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) B :
          (a : M₁) → M₃)
        x :
      M₃)
    ((((toLin v₂ v₃ : (a : Matrix l m R) → M₂ →ₗ[R] M₃) A : M₂ →ₗ[R] M₃) : (a : M₂) → M₃)
        ((((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) B : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x : M₂) :
      M₃)
⊢ Eq.{u_7 + 1} (α := M₃)
    ((((toLin v₁ v₃ : (a : Matrix l n R) → M₁ →ₗ[R] M₃) (A * B) : M₁ →ₗ[R] M₃) : (a : M₁) → M₃) x : M₃)
    ((((toLin v₂ v₃ : (a : Matrix l m R) → M₂ →ₗ[R] M₃) A : M₂ →ₗ[R] M₃) : (a : M₂) → M₃)
        ((((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) B : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x : M₂) :
      M₃)
have rw₁ : Eq.{u_7 + 1} (α := M₃)
  ((((toLin v₂ v₃ : (a : Matrix l m R) → M₂ →ₗ[R] M₃) A : M₂ →ₗ[R] M₃) : (a : M₂) → M₃)
      ((((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) B : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x : M₂) :
    M₃)
  ((((toLin v₂ v₃ : (a : Matrix l m R) → M₂ →ₗ[R] M₃) A : M₂ →ₗ[R] M₃) : (a : M₂) → M₃)
      ((((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) B : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x : M₂) :
    M₃)
Tactic: rw [Matrix.toLin_mul v₁ v₂, LinearMap.comp_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₁
inst_6 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst_7 : Fintype m
M₃ : Type u_7
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
v₃ : Basis l R M₃
inst_10 : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : M₁
⊢ (((toLin v₂ v₁ : (a : Matrix n m R) → M₂ →ₗ[R] M₁) M' : M₂ →ₗ[R] M₁) : (a : M₂) → M₁)
      ((((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) M : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x : M₂) =
    x
have rw : (((toLin v₁ v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) (M' * M) : M₁ →ₗ[R] M₁) : (a : M₁) → M₁) x = x
Tactic: rw [← Matrix.toLin_mul_apply, hM'M, Matrix.toLin_one, id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₁
inst_6 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst_7 : Fintype m
M₃ : Type u_7
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
v₃ : Basis l R M₃
inst_10 : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : M₁
rw : (((toLin v₁ v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) (M' * M) : M₁ →ₗ[R] M₁) : (a : M₁) → M₁) x = x
⊢ (((toLin v₂ v₁ : (a : Matrix n m R) → M₂ →ₗ[R] M₁) M' : M₂ →ₗ[R] M₁) : (a : M₂) → M₁)
      ((((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) M : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x : M₂) =
    x
have rw₁ : ((toLin v₁ v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) 1 : (a : M₁) → M₁) x = x
Tactic: rw [← Matrix.toLin_mul_apply, hM'M, Matrix.toLin_one, id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₁
inst_6 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst_7 : Fintype m
M₃ : Type u_7
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
v₃ : Basis l R M₃
inst_10 : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : M₁
rw : (((toLin v₁ v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) (M' * M) : M₁ →ₗ[R] M₁) : (a : M₁) → M₁) x = x
rw₁ : ((toLin v₁ v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) 1 : (a : M₁) → M₁) x = x
⊢ (((toLin v₂ v₁ : (a : Matrix n m R) → M₂ →ₗ[R] M₁) M' : M₂ →ₗ[R] M₁) : (a : M₂) → M₁)
      ((((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) M : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x : M₂) =
    x
have rw₂ : (LinearMap.id : (a : M₁) → M₁) x = x
Tactic: rw [← Matrix.toLin_mul_apply, hM'M, Matrix.toLin_one, id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₁
inst_6 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst_7 : Fintype m
M₃ : Type u_7
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
v₃ : Basis l R M₃
inst_10 : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : M₁
rw : (((toLin v₁ v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) (M' * M) : M₁ →ₗ[R] M₁) : (a : M₁) → M₁) x = x
rw₁ : ((toLin v₁ v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) 1 : (a : M₁) → M₁) x = x
rw₂ : (LinearMap.id : (a : M₁) → M₁) x = x
⊢ (((toLin v₂ v₁ : (a : Matrix n m R) → M₂ →ₗ[R] M₁) M' : M₂ →ₗ[R] M₁) : (a : M₂) → M₁)
      ((((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) M : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x : M₂) =
    x
have rw₃ : x = x
Tactic: rw [← Matrix.toLin_mul_apply, hM'M, Matrix.toLin_one, id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₁
inst_6 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst_7 : Fintype m
M₃ : Type u_7
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
v₃ : Basis l R M₃
inst_10 : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : M₂
⊢ (((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) M : M₁ →ₗ[R] M₂) : (a : M₁) → M₂)
      ((((toLin v₂ v₁ : (a : Matrix n m R) → M₂ →ₗ[R] M₁) M' : M₂ →ₗ[R] M₁) : (a : M₂) → M₁) x : M₁) =
    x
have rw : (((toLin v₂ v₂ : (a : Matrix m m R) → M₂ →ₗ[R] M₂) (M * M') : M₂ →ₗ[R] M₂) : (a : M₂) → M₂) x = x
Tactic: rw [← Matrix.toLin_mul_apply, hMM', Matrix.toLin_one, id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₁
inst_6 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst_7 : Fintype m
M₃ : Type u_7
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
v₃ : Basis l R M₃
inst_10 : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : M₂
rw : (((toLin v₂ v₂ : (a : Matrix m m R) → M₂ →ₗ[R] M₂) (M * M') : M₂ →ₗ[R] M₂) : (a : M₂) → M₂) x = x
⊢ (((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) M : M₁ →ₗ[R] M₂) : (a : M₁) → M₂)
      ((((toLin v₂ v₁ : (a : Matrix n m R) → M₂ →ₗ[R] M₁) M' : M₂ →ₗ[R] M₁) : (a : M₂) → M₁) x : M₁) =
    x
have rw₁ : ((toLin v₂ v₂ : (a : Matrix m m R) → M₂ →ₗ[R] M₂) 1 : (a : M₂) → M₂) x = x
Tactic: rw [← Matrix.toLin_mul_apply, hMM', Matrix.toLin_one, id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₁
inst_6 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst_7 : Fintype m
M₃ : Type u_7
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
v₃ : Basis l R M₃
inst_10 : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : M₂
rw : (((toLin v₂ v₂ : (a : Matrix m m R) → M₂ →ₗ[R] M₂) (M * M') : M₂ →ₗ[R] M₂) : (a : M₂) → M₂) x = x
rw₁ : ((toLin v₂ v₂ : (a : Matrix m m R) → M₂ →ₗ[R] M₂) 1 : (a : M₂) → M₂) x = x
⊢ (((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) M : M₁ →ₗ[R] M₂) : (a : M₁) → M₂)
      ((((toLin v₂ v₁ : (a : Matrix n m R) → M₂ →ₗ[R] M₁) M' : M₂ →ₗ[R] M₁) : (a : M₂) → M₁) x : M₁) =
    x
have rw₂ : (LinearMap.id : (a : M₂) → M₂) x = x
Tactic: rw [← Matrix.toLin_mul_apply, hMM', Matrix.toLin_one, id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₁
inst_6 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst_7 : Fintype m
M₃ : Type u_7
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
v₃ : Basis l R M₃
inst_10 : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : M₂
rw : (((toLin v₂ v₂ : (a : Matrix m m R) → M₂ →ₗ[R] M₂) (M * M') : M₂ →ₗ[R] M₂) : (a : M₂) → M₂) x = x
rw₁ : ((toLin v₂ v₂ : (a : Matrix m m R) → M₂ →ₗ[R] M₂) 1 : (a : M₂) → M₂) x = x
rw₂ : (LinearMap.id : (a : M₂) → M₂) x = x
⊢ (((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) M : M₁ →ₗ[R] M₂) : (a : M₁) → M₂)
      ((((toLin v₂ v₁ : (a : Matrix n m R) → M₂ →ₗ[R] M₁) M' : M₂ →ₗ[R] M₁) : (a : M₂) → M₁) x : M₁) =
    x
have rw₃ : x = x
Tactic: rw [← Matrix.toLin_mul_apply, hMM', Matrix.toLin_one, id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
f : M₁ →ₗ[R] M₁
⊢ (toLinAlgEquiv v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f) = f
have rw : (toLinAlgEquiv v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁)
    ((AlgEquiv.symm (toLinAlgEquiv v₁) : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f) =
  f
Tactic: rw [← Matrix.toLinAlgEquiv_symm, AlgEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
f : M₁ →ₗ[R] M₁
rw :
  (toLinAlgEquiv v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁)
      ((AlgEquiv.symm (toLinAlgEquiv v₁) : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f) =
    f
⊢ (toLinAlgEquiv v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f) = f
have rw₁ : f = f
Tactic: rw [← Matrix.toLinAlgEquiv_symm, AlgEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
M : Matrix n n R
⊢ (toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) ((toLinAlgEquiv v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) M) = M
have rw : (AlgEquiv.symm (toLinAlgEquiv v₁) : (a : M₁ →ₗ[R] M₁) → Matrix n n R)
    ((toLinAlgEquiv v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) M) =
  M
Tactic: rw [← Matrix.toLinAlgEquiv_symm, AlgEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
M : Matrix n n R
rw :
  (AlgEquiv.symm (toLinAlgEquiv v₁) : (a : M₁ →ₗ[R] M₁) → Matrix n n R)
      ((toLinAlgEquiv v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) M) =
    M
⊢ (toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) ((toLinAlgEquiv v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) M) = M
have rw₁ : M = M
Tactic: rw [← Matrix.toLinAlgEquiv_symm, AlgEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
M : Matrix n n R
v : M₁
⊢ Eq.{u_5 + 1} (α := M₁)
    ((v₁.equivFun.symm : (a : n → R) → M₁)
        ((((toLinAlgEquiv' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) M : (n → R) →ₗ[R] n → R) : (a : n → R) → n → R)
            (⇑((v₁.repr : (a : M₁) → n →₀ R) v : n →₀ R) : (a : n) → R) :
          n → R) :
      M₁)
    (∑ j : n,
        HSMul.hSMul (β := M₁) ((M *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) v : n →₀ R) : (a : n) → R)) j)
          ((v₁ : (a : n) → M₁) j : M₁) :
      M₁)
have rw : Eq.{u_5 + 1} (α := M₁)
  ((v₁.equivFun.symm : (a : n → R) → M₁) (M *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) v : n →₀ R) : (a : n) → R)) : M₁)
  (∑ j : n,
      HSMul.hSMul (β := M₁) ((M *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) v : n →₀ R) : (a : n) → R)) j)
        ((v₁ : (a : n) → M₁) j : M₁) :
    M₁)
Tactic: rw [Matrix.toLinAlgEquiv'_apply, v₁.equivFun_symm_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
M : Matrix n n R
v : M₁
rw :
  Eq.{u_5 + 1} (α := M₁)
    ((v₁.equivFun.symm : (a : n → R) → M₁) (M *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) v : n →₀ R) : (a : n) → R)) : M₁)
    (∑ j : n,
        HSMul.hSMul (β := M₁) ((M *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) v : n →₀ R) : (a : n) → R)) j)
          ((v₁ : (a : n) → M₁) j : M₁) :
      M₁)
⊢ Eq.{u_5 + 1} (α := M₁)
    ((v₁.equivFun.symm : (a : n → R) → M₁)
        ((((toLinAlgEquiv' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) M : (n → R) →ₗ[R] n → R) : (a : n → R) → n → R)
            (⇑((v₁.repr : (a : M₁) → n →₀ R) v : n →₀ R) : (a : n) → R) :
          n → R) :
      M₁)
    (∑ j : n,
        HSMul.hSMul (β := M₁) ((M *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) v : n →₀ R) : (a : n) → R)) j)
          ((v₁ : (a : n) → M₁) j : M₁) :
      M₁)
have rw₁ : Eq.{u_5 + 1} (α := M₁)
  (∑ i : n,
    HSMul.hSMul (β := M₁) ((M *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) v : n →₀ R) : (a : n) → R)) i)
      ((v₁ : (a : n) → M₁) i : M₁))
  (∑ j : n,
    HSMul.hSMul (β := M₁) ((M *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) v : n →₀ R) : (a : n) → R)) j)
      ((v₁ : (a : n) → M₁) j : M₁))
Tactic: rw [Matrix.toLinAlgEquiv'_apply, v₁.equivFun_symm_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
⊢ Eq (α := Matrix n n R) ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) id : Matrix n n R) (1 : Matrix n n R)
have simp_rw : Eq (α := Matrix n n R)
  ((AlgEquiv.ofLinearEquiv (toMatrix v₁ v₁) sorry sorry : (a : M₁ →ₗ[R] M₁) → Matrix n n R) id : Matrix n n R)
  (1 : Matrix n n R)
Tactic: simp_rw [LinearMap.toMatrixAlgEquiv, AlgEquiv.ofLinearEquiv_apply, LinearMap.toMatrix_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
simp_rw :
  Eq (α := Matrix n n R)
    ((AlgEquiv.ofLinearEquiv (toMatrix v₁ v₁) ⋯ ⋯ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) id : Matrix n n R)
    (1 : Matrix n n R)
⊢ Eq (α := Matrix n n R) ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) id : Matrix n n R) (1 : Matrix n n R)
have simp_rw₁ : Eq (α := Matrix n n R) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) id : Matrix n n R) (1 : Matrix n n R)
Tactic: simp_rw [LinearMap.toMatrixAlgEquiv, AlgEquiv.ofLinearEquiv_apply, LinearMap.toMatrix_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
⊢ Eq.{u_5 + 1} (α := M₁ →ₗ[R] M₁) ((toLinAlgEquiv v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) 1) LinearMap.id
have rw : Eq.{u_5 + 1} (α := M₁ →ₗ[R] M₁)
  ((toLinAlgEquiv v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁)
      ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) LinearMap.id) :
    M₁ →ₗ[R] M₁)
  (LinearMap.id : M₁ →ₗ[R] M₁)
Tactic: rw [← LinearMap.toMatrixAlgEquiv_id v₁, Matrix.toLinAlgEquiv_toMatrixAlgEquiv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
rw :
  Eq.{u_5 + 1} (α := M₁ →ₗ[R] M₁)
    ((toLinAlgEquiv v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁)
        ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) LinearMap.id) :
      M₁ →ₗ[R] M₁)
    (LinearMap.id : M₁ →ₗ[R] M₁)
⊢ Eq.{u_5 + 1} (α := M₁ →ₗ[R] M₁) ((toLinAlgEquiv v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) 1) LinearMap.id
have rw₁ : Eq.{u_5 + 1} (α := M₁ →ₗ[R] M₁) LinearMap.id LinearMap.id
Tactic: rw [← LinearMap.toMatrixAlgEquiv_id v₁, Matrix.toLinAlgEquiv_toMatrixAlgEquiv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
inst_5 : DecidableEq M₁
f : M₁ →ₗ[R] M₁
k i : n
⊢ Eq.{u_1 + 1} (α := R)
    ((toMatrixAlgEquiv v₁.reindexRange :
          (a : M₁ →ₗ[R] M₁) →
            Matrix (↑(Set.range (⇑v₁ : (a : n) → M₁)) : Type u_5) (↑(Set.range (⇑v₁ : (a : n) → M₁)) : Type u_5) R)
        f
        (Subtype.mk (p := fun (x : M₁) ↦
          Membership.mem (γ := Set M₁) (Set.range.{u_5, u_4 + 1} (ι := n) (⇑v₁ : (a : n) → M₁)) x)
          ((v₁ : (a : n) → M₁) k) ⋯)
        (Subtype.mk (p := fun (x : M₁) ↦
          Membership.mem (γ := Set M₁) (Set.range.{u_5, u_4 + 1} (ι := n) (⇑v₁ : (a : n) → M₁)) x)
          ((v₁ : (a : n) → M₁) i) ⋯) :
      R)
    ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f k i : R)
have simp_rw : Eq.{u_1 + 1} (α := R)
  ((((v₁.reindexRange.repr : (a : M₁) → (↑(Set.range (⇑v₁ : (a : n) → M₁)) : Type u_5) →₀ R)
            ((f : (a : M₁) → M₁)
              ((v₁.reindexRange : (a : (↑(Set.range (⇑v₁ : (a : n) → M₁)) : Type u_5)) → M₁)
                  (Subtype.mk (p := fun (x : M₁) ↦
                      Membership.mem (γ := Set M₁) (Set.range.{u_5, u_4 + 1} (ι := n) (⇑v₁ : (a : n) → M₁)) x)
                      ((v₁ : (a : n) → M₁) i) sorry :
                    { x : M₁ //
                      Membership.mem (γ := Set M₁) (Set.range.{u_5, u_4 + 1} (ι := n) (⇑v₁ : (a : n) → M₁)) x }) :
                M₁)) :
          Finsupp.{u_5, u_1} (↑(Set.range.{u_5, u_4 + 1} (ι := n) (⇑v₁ : (a : n) → M₁)) : Type u_5) R) :
        (a : (↑(Set.range (⇑v₁ : (a : n) → M₁)) : Type u_5)) → R)
      (Subtype.mk (p := fun (x : M₁) ↦
          Membership.mem (γ := Set M₁) (Set.range.{u_5, u_4 + 1} (ι := n) (⇑v₁ : (a : n) → M₁)) x)
          ((v₁ : (a : n) → M₁) k) sorry :
        { x : M₁ // Membership.mem (γ := Set M₁) (Set.range.{u_5, u_4 + 1} (ι := n) (⇑v₁ : (a : n) → M₁)) x }) :
    R)
  ((((v₁.repr : (a : M₁) → n →₀ R) ((f : (a : M₁) → M₁) ((v₁ : (a : n) → M₁) i : M₁)) : n →₀ R) : (a : n) → R) k : R)
Tactic: simp_rw [LinearMap.toMatrixAlgEquiv_apply, Basis.reindexRange_self, Basis.reindexRange_repr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
inst_5 : DecidableEq M₁
f : M₁ →ₗ[R] M₁
k i : n
simp_rw :
  Eq.{u_1 + 1} (α := R)
    ((((v₁.reindexRange.repr : (a : M₁) → (↑(Set.range (⇑v₁ : (a : n) → M₁)) : Type u_5) →₀ R)
              ((f : (a : M₁) → M₁)
                ((v₁.reindexRange : (a : (↑(Set.range (⇑v₁ : (a : n) → M₁)) : Type u_5)) → M₁)
                    (Subtype.mk (p := fun (x : M₁) ↦
                        Membership.mem (γ := Set M₁) (Set.range.{u_5, u_4 + 1} (ι := n) (⇑v₁ : (a : n) → M₁)) x)
                        ((v₁ : (a : n) → M₁) i) ⋯ :
                      { x : M₁ //
                        Membership.mem (γ := Set M₁) (Set.range.{u_5, u_4 + 1} (ι := n) (⇑v₁ : (a : n) → M₁)) x }) :
                  M₁)) :
            Finsupp.{u_5, u_1} (↑(Set.range.{u_5, u_4 + 1} (ι := n) (⇑v₁ : (a : n) → M₁)) : Type u_5) R) :
          (a : (↑(Set.range (⇑v₁ : (a : n) → M₁)) : Type u_5)) → R)
        (Subtype.mk (p := fun (x : M₁) ↦
            Membership.mem (γ := Set M₁) (Set.range.{u_5, u_4 + 1} (ι := n) (⇑v₁ : (a : n) → M₁)) x)
            ((v₁ : (a : n) → M₁) k) ⋯ :
          { x : M₁ // Membership.mem (γ := Set M₁) (Set.range.{u_5, u_4 + 1} (ι := n) (⇑v₁ : (a : n) → M₁)) x }) :
      R)
    ((((v₁.repr : (a : M₁) → n →₀ R) ((f : (a : M₁) → M₁) ((v₁ : (a : n) → M₁) i : M₁)) : n →₀ R) : (a : n) → R) k : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((toMatrixAlgEquiv v₁.reindexRange :
          (a : M₁ →ₗ[R] M₁) →
            Matrix (↑(Set.range (⇑v₁ : (a : n) → M₁)) : Type u_5) (↑(Set.range (⇑v₁ : (a : n) → M₁)) : Type u_5) R)
        f
        (Subtype.mk (p := fun (x : M₁) ↦
          Membership.mem (γ := Set M₁) (Set.range.{u_5, u_4 + 1} (ι := n) (⇑v₁ : (a : n) → M₁)) x)
          ((v₁ : (a : n) → M₁) k) ⋯)
        (Subtype.mk (p := fun (x : M₁) ↦
          Membership.mem (γ := Set M₁) (Set.range.{u_5, u_4 + 1} (ι := n) (⇑v₁ : (a : n) → M₁)) x)
          ((v₁ : (a : n) → M₁) i) ⋯) :
      R)
    ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f k i : R)
have simp_rw₁ : Eq.{u_1 + 1} (α := R)
  ((((v₁.reindexRange.repr : (a : M₁) → (↑(Set.range (⇑v₁ : (a : n) → M₁)) : Type u_5) →₀ R)
            ((f : (a : M₁) → M₁) ((v₁ : (a : n) → M₁) i : M₁)) :
          Finsupp.{u_5, u_1} (↑(Set.range.{u_5, u_4 + 1} (ι := n) (⇑v₁ : (a : n) → M₁)) : Type u_5) R) :
        (a : (↑(Set.range (⇑v₁ : (a : n) → M₁)) : Type u_5)) → R)
      (Subtype.mk (p := fun (x : M₁) ↦
          Membership.mem (γ := Set M₁) (Set.range.{u_5, u_4 + 1} (ι := n) (⇑v₁ : (a : n) → M₁)) x)
          ((v₁ : (a : n) → M₁) k) sorry :
        { x : M₁ // Membership.mem (γ := Set M₁) (Set.range.{u_5, u_4 + 1} (ι := n) (⇑v₁ : (a : n) → M₁)) x }) :
    R)
  ((((v₁.repr : (a : M₁) → n →₀ R) ((f : (a : M₁) → M₁) ((v₁ : (a : n) → M₁) i : M₁)) : n →₀ R) : (a : n) → R) k : R)
Tactic: simp_rw [LinearMap.toMatrixAlgEquiv_apply, Basis.reindexRange_self, Basis.reindexRange_repr]