-- 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)
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)
a₅ :
  Eq.{u_1 + 1} (α := R)
    ((((LinearEquiv.symm (DistribMulAction.toLinearEquiv R S g) ≪≫ₗ b.repr : (a : S) → m →₀ R)
              (x * HSMul.hSMul (β := S) 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)
a₆ :
  Eq.{u_1 + 1} (α := R)
    ((((b.repr : (a : S) → m →₀ R)
              ((LinearEquiv.symm (DistribMulAction.toLinearEquiv R S g) : (a : S) → S)
                (x * HSMul.hSMul (β := S) 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)
  ((((b.repr : (a : S) → m →₀ R) (g⁻¹ • (x * HSMul.hSMul (β := S) 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]