-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
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)
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)
⊢ 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

Tactic:
rw [← (LinearMap.toMatrix b b).injective.eq_iff]

Premises used: Function.Injective.eq_iff, LinearEquiv.injective, LinearMap.toMatrix