awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
m : Type u_3
inst_3 : Fintype m
inst_4 : DecidableEq m
b : Basis m R S
x y : S
rw :
  (toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R)
      (HMul.hMul (α := End R S) (β := End R S) ((lmul R S : (a : S) → End R S) x : End R S)
        ((lmul R S : (a : S) → End R S) y : End R S)) =
    HMul.hMul (α := Matrix m m R) (β := Matrix m m R)
      ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) : Matrix m m R)
      ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) y) : Matrix m m R)
⊢ (toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) (x * y)) =
    HMul.hMul (α := Matrix m m R) (β := Matrix m m R)
      ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) : Matrix m m R)
      ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) y) : Matrix m m R)
have rw₁ : HMul.hMul (α := Matrix m m R) (β := Matrix m m R)
    ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) : Matrix m m R)
    ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) y) : Matrix m m R) =
  HMul.hMul (α := Matrix m m R) (β := Matrix m m R)
    ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) : Matrix m m R)
    ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) y) : Matrix m m R)
Tactic: rw [map_mul, LinearMap.toMatrix_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
m : Type u_3
inst_3 : Fintype m
inst_4 : DecidableEq m
b : Basis m R S
⊢ Eq (α := Matrix m m R)
    ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) 0) : Matrix m m R)
    (0 : Matrix m m R)
have rw : Eq (α := Matrix m m R) ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) 0) 0
Tactic: rw [map_zero, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
m : Type u_3
inst_3 : Fintype m
inst_4 : DecidableEq m
b : Basis m R S
rw : Eq (α := Matrix m m R) ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) 0) 0
⊢ Eq (α := Matrix m m R)
    ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) 0) : Matrix m m R)
    (0 : Matrix m m R)
have rw₁ : Eq (α := Matrix m m R) 0 0
Tactic: rw [map_zero, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
m : Type u_3
inst_3 : Fintype m
inst_4 : DecidableEq m
b : Basis m R S
x y : S
⊢ (toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) (x + y)) =
    HAdd.hAdd (α := Matrix m m R) (β := Matrix m m R)
      ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) : Matrix m m R)
      ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) y) : Matrix m m R)
have rw : (toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R)
    (HAdd.hAdd (α := End R S) (β := End R S) ((lmul R S : (a : S) → End R S) x : End R S)
      ((lmul R S : (a : S) → End R S) y : End R S)) =
  HAdd.hAdd (α := Matrix m m R) (β := Matrix m m R)
    ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) : Matrix m m R)
    ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) y) : Matrix m m R)
Tactic: rw [map_add, map_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
m : Type u_3
inst_3 : Fintype m
inst_4 : DecidableEq m
b : Basis m R S
x y : S
rw :
  (toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R)
      (HAdd.hAdd (α := End R S) (β := End R S) ((lmul R S : (a : S) → End R S) x : End R S)
        ((lmul R S : (a : S) → End R S) y : End R S)) =
    HAdd.hAdd (α := Matrix m m R) (β := Matrix m m R)
      ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) : Matrix m m R)
      ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) y) : Matrix m m R)
⊢ (toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) (x + y)) =
    HAdd.hAdd (α := Matrix m m R) (β := Matrix m m R)
      ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) : Matrix m m R)
      ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) y) : Matrix m m R)
have rw₁ : HAdd.hAdd (α := Matrix m m R) (β := Matrix m m R)
    ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) : Matrix m m R)
    ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) y) : Matrix m m R) =
  HAdd.hAdd (α := Matrix m m R) (β := Matrix m m R)
    ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) : Matrix m m R)
    ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) y) : Matrix m m R)
Tactic: rw [map_add, map_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
m : Type u_3
inst_3 : Fintype m
inst_4 : DecidableEq m
b : Basis m R S
r : R
⊢ Eq (α := Matrix m m R)
    ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R)
        ((lmul R S : (a : S) → End R S) ((algebraMap R S : (a : R) → S) r : S)) :
      Matrix m m R)
    ((algebraMap R (Matrix m m R) : (a : R) → Matrix m m R) r : Matrix m m R)
have a : ∀ (i j : m),
  Eq.{u_1 + 1} (α := R)
    ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R)
        ((lmul R S : (a : S) → End R S) ((algebraMap R S : (a : R) → S) r : S)) i j :
      R)
    ((algebraMap R (Matrix m m R) : (a : R) → Matrix m m R) r i j : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
m : Type u_3
inst_3 : Fintype m
inst_4 : DecidableEq m
b : Basis m R S
r : R
i j : m
⊢ Eq.{u_1 + 1} (α := R)
    ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R)
        ((lmul R S : (a : S) → End R S) ((algebraMap R S : (a : R) → S) r : S)) i j :
      R)
    ((algebraMap R (Matrix m m R) : (a : R) → Matrix m m R) r i j : R)
have a : Eq.{u_1 + 1} (α := R) ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lsmul R R S : (a : R) → End R S) r) i j : R)
  ((algebraMap R (Matrix m m R) : (a : R) → Matrix m m R) r i j : R)
Tactic: rw [lmul_algebraMap, toMatrix_lsmul, algebraMap_eq_diagonal, Pi.algebraMap_def,
      Algebra.algebraMap_self_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
m : Type u_3
inst_3 : Fintype m
inst_4 : DecidableEq m
b : Basis m R S
r : R
i j : m
a :
  Eq.{u_1 + 1} (α := R) ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lsmul R R S : (a : R) → End R S) r) i j : R)
    ((algebraMap R (Matrix m m R) : (a : R) → Matrix m m R) r i j : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R)
        ((lmul R S : (a : S) → End R S) ((algebraMap R S : (a : R) → S) r : S)) i j :
      R)
    ((algebraMap R (Matrix m m R) : (a : R) → Matrix m m R) r i j : R)
have a₁ : Eq.{u_1 + 1} (α := R) (Matrix.diagonal (fun (x : m) ↦ r) i j : R)
  ((algebraMap R (Matrix m m R) : (a : R) → Matrix m m R) r i j : R)
Tactic: rw [lmul_algebraMap, toMatrix_lsmul, algebraMap_eq_diagonal, Pi.algebraMap_def,
      Algebra.algebraMap_self_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
m : Type u_3
inst_3 : Fintype m
inst_4 : DecidableEq m
b : Basis m R S
r : R
i j : m
a :
  Eq.{u_1 + 1} (α := R) ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lsmul R R S : (a : R) → End R S) r) i j : R)
    ((algebraMap R (Matrix m m R) : (a : R) → Matrix m m R) r i j : R)
a₁ :
  Eq.{u_1 + 1} (α := R) (Matrix.diagonal (fun (x : m) ↦ r) i j : R)
    ((algebraMap R (Matrix m m R) : (a : R) → Matrix m m R) r i j : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R)
        ((lmul R S : (a : S) → End R S) ((algebraMap R S : (a : R) → S) r : S)) i j :
      R)
    ((algebraMap R (Matrix m m R) : (a : R) → Matrix m m R) r i j : R)
have a₂ : Eq.{u_1 + 1} (α := R) (Matrix.diagonal (fun (x : m) ↦ r) i j)
  (Matrix.diagonal ((algebraMap R (m → R) : (a : R) → m → R) r) i j)
Tactic: rw [lmul_algebraMap, toMatrix_lsmul, algebraMap_eq_diagonal, Pi.algebraMap_def,
      Algebra.algebraMap_self_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
m : Type u_3
inst_3 : Fintype m
inst_4 : DecidableEq m
b : Basis m R S
r : R
i j : m
a :
  Eq.{u_1 + 1} (α := R) ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lsmul R R S : (a : R) → End R S) r) i j : R)
    ((algebraMap R (Matrix m m R) : (a : R) → Matrix m m R) r i j : R)
a₁ :
  Eq.{u_1 + 1} (α := R) (Matrix.diagonal (fun (x : m) ↦ r) i j : R)
    ((algebraMap R (Matrix m m R) : (a : R) → Matrix m m R) r i j : R)
a₂ :
  Eq.{u_1 + 1} (α := R) (Matrix.diagonal (fun (x : m) ↦ r) i j)
    (Matrix.diagonal ((algebraMap R (m → R) : (a : R) → m → R) r) i j)
⊢ Eq.{u_1 + 1} (α := R)
    ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R)
        ((lmul R S : (a : S) → End R S) ((algebraMap R S : (a : R) → S) r : S)) i j :
      R)
    ((algebraMap R (Matrix m m R) : (a : R) → Matrix m m R) r i j : R)
have a₃ : Eq.{u_1 + 1} (α := R) (Matrix.diagonal (fun (x : m) ↦ r) i j)
  (Matrix.diagonal (fun (i : m) ↦ (algebraMap R R : (a : R) → R) r) i j)
Tactic: rw [lmul_algebraMap, toMatrix_lsmul, algebraMap_eq_diagonal, Pi.algebraMap_def,
      Algebra.algebraMap_self_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
m : Type u_3
inst_3 : Fintype m
inst_4 : DecidableEq m
b : Basis m R S
r : R
i j : m
a :
  Eq.{u_1 + 1} (α := R) ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lsmul R R S : (a : R) → End R S) r) i j : R)
    ((algebraMap R (Matrix m m R) : (a : R) → Matrix m m R) r i j : R)
a₁ :
  Eq.{u_1 + 1} (α := R) (Matrix.diagonal (fun (x : m) ↦ r) i j : R)
    ((algebraMap R (Matrix m m R) : (a : R) → Matrix m m R) r i j : R)
a₂ :
  Eq.{u_1 + 1} (α := R) (Matrix.diagonal (fun (x : m) ↦ r) i j)
    (Matrix.diagonal ((algebraMap R (m → R) : (a : R) → m → R) r) i j)
a₃ :
  Eq.{u_1 + 1} (α := R) (Matrix.diagonal (fun (x : m) ↦ r) i j)
    (Matrix.diagonal (fun (i : m) ↦ (algebraMap R R : (a : R) → R) r) i j)
⊢ Eq.{u_1 + 1} (α := R)
    ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R)
        ((lmul R S : (a : S) → End R S) ((algebraMap R S : (a : R) → S) r : S)) i j :
      R)
    ((algebraMap R (Matrix m m R) : (a : R) → Matrix m m R) r i j : R)
have a₄ : Eq.{u_1 + 1} (α := R) (Matrix.diagonal (fun (x : m) ↦ r) i j) (Matrix.diagonal (fun (i : m) ↦ r) i j)
Tactic: rw [lmul_algebraMap, toMatrix_lsmul, algebraMap_eq_diagonal, Pi.algebraMap_def,
      Algebra.algebraMap_self_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
m : Type u_3
inst_3 : Fintype m
inst_4 : DecidableEq m
b : Basis m R S
x : S
i j : m
⊢ Eq.{u_1 + 1} (α := R) ((leftMulMatrix b : (a : S) → Matrix m m R) x i j : R)
    ((((b.repr : (a : S) → m →₀ R) (HMul.hMul (β := S) x ((b : (a : m) → S) j : S)) : m →₀ R) : (a : m) → R) i : R)
have rw : Eq.{u_1 + 1} (α := R) ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) i j : R)
  ((((b.repr : (a : S) → m →₀ R) (HMul.hMul (β := S) x ((b : (a : m) → S) j : S)) : m →₀ R) : (a : m) → R) i : R)
Tactic: rw [leftMulMatrix_apply, toMatrix_lmul' b x i j]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
m : Type u_3
inst_3 : Fintype m
inst_4 : DecidableEq m
b : Basis m R S
x : S
i j : m
rw :
  Eq.{u_1 + 1} (α := R) ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) i j : R)
    ((((b.repr : (a : S) → m →₀ R) (HMul.hMul (β := S) x ((b : (a : m) → S) j : S)) : m →₀ R) : (a : m) → R) i : R)
⊢ Eq.{u_1 + 1} (α := R) ((leftMulMatrix b : (a : S) → Matrix m m R) x i j : R)
    ((((b.repr : (a : S) → m →₀ R) (HMul.hMul (β := S) x ((b : (a : m) → S) j : S)) : m →₀ R) : (a : m) → R) i : R)
have rw₁ : Eq.{u_1 + 1} (α := R)
  ((((b.repr : (a : S) → m →₀ R) (HMul.hMul (β := S) x ((b : (a : m) → S) j : S)) : m →₀ R) : (a : m) → R) i : R)
  ((((b.repr : (a : S) → m →₀ R) (HMul.hMul (β := S) x ((b : (a : m) → S) j : S)) : m →₀ R) : (a : m) → R) i : R)
Tactic: rw [leftMulMatrix_apply, toMatrix_lmul' b x i j]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
m : Type u_3
inst_3 : Fintype m
inst_4 : DecidableEq m
b : Basis m R S
x x' : S
h :
  Eq (α := Matrix m m R) ((leftMulMatrix b : (a : S) → Matrix m m R) x : Matrix m m R)
    ((leftMulMatrix b : (a : S) → Matrix m m R) x' : Matrix m m R)
⊢ Eq (α := S) ((((lmul R S : (a : S) → End R S) x : End R S) : (a : S) → S) 1 : S)
    ((((lmul R S : (a : S) → End R S) x' : End R S) : (a : S) → S) 1 : S)
have rw : Eq (α := S) ((((lmul R S : (a : S) → End R S) x' : End R S) : (a : S) → S) 1 : S)
  ((((lmul R S : (a : S) → End R S) x' : End R S) : (a : S) → S) 1 : S)
Tactic: rw [(LinearMap.toMatrix b b).injective h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
m : Type u_3
inst_3 : Fintype m
inst_4 : DecidableEq m
b : Basis m R S
G : Type u_4
inst_5 : Group G
inst_6 : DistribMulAction G S
inst_7 : SMulCommClass G R S
inst_8 : SMulCommClass G S S
g : G
x : S
⊢ Eq (α := Matrix m m R) ((leftMulMatrix (g • b) : (a : S) → Matrix m m R) x : Matrix m m R)
    ((leftMulMatrix b : (a : S) → Matrix m m R) x : Matrix m m R)
have a : ∀ (i j : m),
  Eq.{u_1 + 1} (α := R) ((leftMulMatrix (g • b) : (a : S) → Matrix m m R) x i j : R)
    ((leftMulMatrix b : (a : S) → Matrix m m R) x i j : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
m : Type u_3
inst_3 : Fintype m
inst_4 : DecidableEq m
b : Basis m R S
G : Type u_4
inst_5 : Group G
inst_6 : DistribMulAction G S
inst_7 : SMulCommClass G R S
inst_8 : SMulCommClass G S S
g : G
x : S
i j : m
⊢ Eq.{u_1 + 1} (α := R) ((leftMulMatrix (g • b) : (a : S) → Matrix m m R) x i j : R)
    ((leftMulMatrix b : (a : S) → Matrix m m R) x i j : R)
have a : Eq.{u_1 + 1} (α := R)
  ((toMatrix (g • b) (g • b) : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) i j : R)
  ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) i j : R)
Tactic: simp_rw [leftMulMatrix_apply, LinearMap.toMatrix_apply, coe_lmul_eq_mul, LinearMap.mul_apply',
    Basis.repr_smul, Basis.smul_apply, LinearEquiv.trans_apply,
    DistribMulAction.toLinearEquiv_symm_apply, mul_smul_comm, inv_smul_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
m : Type u_3
inst_3 : Fintype m
inst_4 : DecidableEq m
b : Basis m R S
G : Type u_4
inst_5 : Group G
inst_6 : DistribMulAction G S
inst_7 : SMulCommClass G R S
inst_8 : SMulCommClass G S S
g : G
x : S
i j : m
a :
  Eq.{u_1 + 1} (α := R)
    ((toMatrix (g • b) (g • b) : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) i j : R)
    ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) i j : R)
⊢ Eq.{u_1 + 1} (α := R) ((leftMulMatrix (g • b) : (a : S) → Matrix m m R) x i j : R)
    ((leftMulMatrix b : (a : S) → Matrix m m R) x i j : R)
have a₁ : Eq.{u_1 + 1} (α := R)
  (((((g • b).repr : (a : S) → m →₀ R)
            ((((lmul R S : (a : S) → End R S) x : End R S) : (a : S) → S) ((g • b : (a : m) → S) j : S)) :
          m →₀ R) :
        (a : m) → R)
      i :
    R)
  ((((b.repr : (a : S) → m →₀ R)
            ((((lmul R S : (a : S) → End R S) x : End R S) : (a : S) → S) ((b : (a : m) → S) j : S)) :
          m →₀ R) :
        (a : m) → R)
      i :
    R)
Tactic: simp_rw [leftMulMatrix_apply, LinearMap.toMatrix_apply, coe_lmul_eq_mul, LinearMap.mul_apply',
    Basis.repr_smul, Basis.smul_apply, LinearEquiv.trans_apply,
    DistribMulAction.toLinearEquiv_symm_apply, mul_smul_comm, inv_smul_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
m : Type u_3
inst_3 : Fintype m
inst_4 : DecidableEq m
b : Basis m R S
G : Type u_4
inst_5 : Group G
inst_6 : DistribMulAction G S
inst_7 : SMulCommClass G R S
inst_8 : SMulCommClass G S S
g : G
x : S
i j : m
a :
  Eq.{u_1 + 1} (α := R)
    ((toMatrix (g • b) (g • b) : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) i j : R)
    ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) i j : R)
a₁ :
  Eq.{u_1 + 1} (α := R)
    (((((g • b).repr : (a : S) → m →₀ R)
              ((((lmul R S : (a : S) → End R S) x : End R S) : (a : S) → S) ((g • b : (a : m) → S) j : S)) :
            m →₀ R) :
          (a : m) → R)
        i :
      R)
    ((((b.repr : (a : S) → m →₀ R)
              ((((lmul R S : (a : S) → End R S) x : End R S) : (a : S) → S) ((b : (a : m) → S) j : S)) :
            m →₀ R) :
          (a : m) → R)
        i :
      R)
⊢ Eq.{u_1 + 1} (α := R) ((leftMulMatrix (g • b) : (a : S) → Matrix m m R) x i j : R)
    ((leftMulMatrix b : (a : S) → Matrix m m R) x i j : R)
have a₂ : Eq.{u_1 + 1} (α := R)
  (((((g • b).repr : (a : S) → m →₀ R)
            ((((LinearMap.mul R S : (a : S) → S →ₗ[R] S) x : S →ₗ[R] S) : (a : S) → S) ((g • b : (a : m) → S) j : S)) :
          m →₀ R) :
        (a : m) → R)
      i :
    R)
  ((((b.repr : (a : S) → m →₀ R)
            ((((LinearMap.mul R S : (a : S) → S →ₗ[R] S) x : S →ₗ[R] S) : (a : S) → S) ((b : (a : m) → S) j : S)) :
          m →₀ R) :
        (a : m) → R)
      i :
    R)
Tactic: simp_rw [leftMulMatrix_apply, LinearMap.toMatrix_apply, coe_lmul_eq_mul, LinearMap.mul_apply',
    Basis.repr_smul, Basis.smul_apply, LinearEquiv.trans_apply,
    DistribMulAction.toLinearEquiv_symm_apply, mul_smul_comm, inv_smul_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
m : Type u_3
inst_3 : Fintype m
inst_4 : DecidableEq m
b : Basis m R S
G : Type u_4
inst_5 : Group G
inst_6 : DistribMulAction G S
inst_7 : SMulCommClass G R S
inst_8 : SMulCommClass G S S
g : G
x : S
i j : m
a :
  Eq.{u_1 + 1} (α := R)
    ((toMatrix (g • b) (g • b) : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) i j : R)
    ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) i j : R)
a₁ :
  Eq.{u_1 + 1} (α := R)
    (((((g • b).repr : (a : S) → m →₀ R)
              ((((lmul R S : (a : S) → End R S) x : End R S) : (a : S) → S) ((g • b : (a : m) → S) j : S)) :
            m →₀ R) :
          (a : m) → R)
        i :
      R)
    ((((b.repr : (a : S) → m →₀ R)
              ((((lmul R S : (a : S) → End R S) x : End R S) : (a : S) → S) ((b : (a : m) → S) j : S)) :
            m →₀ R) :
          (a : m) → R)
        i :
      R)
a₂ :
  Eq.{u_1 + 1} (α := R)
    (((((g • b).repr : (a : S) → m →₀ R)
              ((((LinearMap.mul R S : (a : S) → S →ₗ[R] S) x : S →ₗ[R] S) : (a : S) → S)
                ((g • b : (a : m) → S) j : S)) :
            m →₀ R) :
          (a : m) → R)
        i :
      R)
    ((((b.repr : (a : S) → m →₀ R)
              ((((LinearMap.mul R S : (a : S) → S →ₗ[R] S) x : S →ₗ[R] S) : (a : S) → S) ((b : (a : m) → S) j : S)) :
            m →₀ R) :
          (a : m) → R)
        i :
      R)
⊢ Eq.{u_1 + 1} (α := R) ((leftMulMatrix (g • b) : (a : S) → Matrix m m R) x i j : R)
    ((leftMulMatrix b : (a : S) → Matrix m m R) x i j : R)
have a₃ : Eq.{u_1 + 1} (α := R)
  (((((g • b).repr : (a : S) → m →₀ R) (HMul.hMul (β := S) x ((g • b : (a : m) → S) j : S)) : m →₀ R) : (a : m) → R) i :
    R)
  ((((b.repr : (a : S) → m →₀ R) (HMul.hMul (β := S) x ((b : (a : m) → S) j : S)) : m →₀ R) : (a : m) → R) i : R)
Tactic: simp_rw [leftMulMatrix_apply, LinearMap.toMatrix_apply, coe_lmul_eq_mul, LinearMap.mul_apply',
    Basis.repr_smul, Basis.smul_apply, LinearEquiv.trans_apply,
    DistribMulAction.toLinearEquiv_symm_apply, mul_smul_comm, inv_smul_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
m : Type u_3
inst_3 : Fintype m
inst_4 : DecidableEq m
b : Basis m R S
G : Type u_4
inst_5 : Group G
inst_6 : DistribMulAction G S
inst_7 : SMulCommClass G R S
inst_8 : SMulCommClass G S S
g : G
x : S
i j : m
a :
  Eq.{u_1 + 1} (α := R)
    ((toMatrix (g • b) (g • b) : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) i j : R)
    ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) i j : R)
a₁ :
  Eq.{u_1 + 1} (α := R)
    (((((g • b).repr : (a : S) → m →₀ R)
              ((((lmul R S : (a : S) → End R S) x : End R S) : (a : S) → S) ((g • b : (a : m) → S) j : S)) :
            m →₀ R) :
          (a : m) → R)
        i :
      R)
    ((((b.repr : (a : S) → m →₀ R)
              ((((lmul R S : (a : S) → End R S) x : End R S) : (a : S) → S) ((b : (a : m) → S) j : S)) :
            m →₀ R) :
          (a : m) → R)
        i :
      R)
a₂ :
  Eq.{u_1 + 1} (α := R)
    (((((g • b).repr : (a : S) → m →₀ R)
              ((((LinearMap.mul R S : (a : S) → S →ₗ[R] S) x : S →ₗ[R] S) : (a : S) → S)
                ((g • b : (a : m) → S) j : S)) :
            m →₀ R) :
          (a : m) → R)
        i :
      R)
    ((((b.repr : (a : S) → m →₀ R)
              ((((LinearMap.mul R S : (a : S) → S →ₗ[R] S) x : S →ₗ[R] S) : (a : S) → S) ((b : (a : m) → S) j : S)) :
            m →₀ R) :
          (a : m) → R)
        i :
      R)
a₃ :
  Eq.{u_1 + 1} (α := R)
    (((((g • b).repr : (a : S) → m →₀ R) (HMul.hMul (β := S) x ((g • b : (a : m) → S) j : S)) : m →₀ R) : (a : m) → R)
        i :
      R)
    ((((b.repr : (a : S) → m →₀ R) (HMul.hMul (β := S) x ((b : (a : m) → S) j : S)) : m →₀ R) : (a : m) → R) i : R)
⊢ Eq.{u_1 + 1} (α := R) ((leftMulMatrix (g • b) : (a : S) → Matrix m m R) x i j : R)
    ((leftMulMatrix b : (a : S) → Matrix m m R) x i j : R)
have a₄ : Eq.{u_1 + 1} (α := R)
  ((((LinearEquiv.symm (DistribMulAction.toLinearEquiv R S g) ≪≫ₗ b.repr : (a : S) → m →₀ R)
            (HMul.hMul (β := S) x ((g • b : (a : m) → S) j : S)) :
          m →₀ R) :
        (a : m) → R)
      i :
    R)
  ((((b.repr : (a : S) → m →₀ R) (HMul.hMul (β := S) x ((b : (a : m) → S) j : S)) : m →₀ R) : (a : m) → R) i : R)
Tactic: simp_rw [leftMulMatrix_apply, LinearMap.toMatrix_apply, coe_lmul_eq_mul, LinearMap.mul_apply',
    Basis.repr_smul, Basis.smul_apply, LinearEquiv.trans_apply,
    DistribMulAction.toLinearEquiv_symm_apply, mul_smul_comm, inv_smul_smul]