-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
inst_4 : Module.Finite R V
g : SpecialLinearGroup R V
hR : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
this_1 : Fintype (Module.Free.ChooseBasisIndex R V) := Module.Free.ChooseBasisIndex.fintype R V
e : SpecialLinearGroup R V ≃* Matrix.SpecialLinearGroup.{u_2, u_1} (Module.Free.ChooseBasisIndex R V) R :=
  MulEquiv.symm (Matrix.SpecialLinearGroup.toLin_equiv b)
r : R
hr : r ^ Fintype.card.{u_2} (Module.Free.ChooseBasisIndex R V) = 1
this :
  Eq (α := Matrix.{u_2, u_2, u_1} (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
    (↑((MulEquiv.symm (Matrix.SpecialLinearGroup.toLin_equiv b) :
            (a : SpecialLinearGroup R V) → Matrix.SpecialLinearGroup (Module.Free.ChooseBasisIndex R V) R)
          g) :
      Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
    ((Matrix.of :
        (a : Module.Free.ChooseBasisIndex R V → Module.Free.ChooseBasisIndex R V → R) →
          Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
      fun (i j : Module.Free.ChooseBasisIndex R V) ↦
      ((b.repr : (a : V) → Module.Free.ChooseBasisIndex R V →₀ R)
            ((fun (x : V) ↦ (((↑g : V ≃ₗ[R] V) : (a : V) → V) x : V))
              ((b : (a : Module.Free.ChooseBasisIndex R V) → V) j)) :
          (a : Module.Free.ChooseBasisIndex R V) → R)
        i)
⊢ Eq (α := Matrix.{u_2, u_2, u_1} (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
      (Matrix.diagonal fun (x : Module.Free.ChooseBasisIndex R V) ↦ r)
      ((Matrix.of :
          (a : Module.Free.ChooseBasisIndex R V → Module.Free.ChooseBasisIndex R V → R) →
            Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
        fun (i j : Module.Free.ChooseBasisIndex R V) ↦
        (((b.repr : (a : V) → Module.Free.ChooseBasisIndex R V →₀ R)
                (((↑g : V ≃ₗ[R] V) : (a : V) → V) ((b : (a : Module.Free.ChooseBasisIndex R V) → V) j : V)) :
              Finsupp.{u_2, u_1} (Module.Free.ChooseBasisIndex R V) R) :
            (a : Module.Free.ChooseBasisIndex R V) → R)
          i) ↔
    (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id
have rw : Eq (α := Matrix.{u_2, u_2, u_1} (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
    (Matrix.diagonal fun (x : Module.Free.ChooseBasisIndex R V) ↦ r)
    ((Matrix.of :
        (a : Module.Free.ChooseBasisIndex R V → Module.Free.ChooseBasisIndex R V → R) →
          Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
      fun (i j : Module.Free.ChooseBasisIndex R V) ↦
      (((b.repr : (a : V) → Module.Free.ChooseBasisIndex R V →₀ R)
              (((↑g : V ≃ₗ[R] V) : (a : V) → V) ((b : (a : Module.Free.ChooseBasisIndex R V) → V) j : V)) :
            Finsupp.{u_2, u_1} (Module.Free.ChooseBasisIndex R V) R) :
          (a : Module.Free.ChooseBasisIndex R V) → R)
        i) ↔
  Eq (α := Matrix.{u_2, u_2, u_1} (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
    ((LinearMap.toMatrix b b :
          (a : V →ₗ[R] V) → Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
        (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) :
      Matrix.{u_2, u_2, u_1} (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
    ((LinearMap.toMatrix b b :
          (a : V →ₗ[R] V) → Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
        (HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id) :
      Matrix.{u_2, u_2, u_1} (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
Tactic: rw [← (LinearMap.toMatrix b b).injective.eq_iff]