-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_4
inst : CommRing R
V : Type u_5
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
inst_4 : Module.Finite R V
ι : Type u_6
inst_5 : Fintype ι
inst_6 : DecidableEq ι
b : Module.Basis ι R V
g : ↥(center (Matrix.SpecialLinearGroup ι R))
h : Nontrivial R
hV : Nontrivial V
hι : ¬IsEmpty ι
this : FaithfulSMul R V
hgg' :
  ∀ (x : V),
    Eq (α := V)
      (((↑(↑(↑((centerCongr (toLin_equiv b) :
                            (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(center (_root_.SpecialLinearGroup R V)))
                          g) :
                      _root_.SpecialLinearGroup R V) :
                  V ≃ₗ[R] V) :
              V →ₗ[R] V) :
            (a : V) → V)
          x :
        V)
      (((↑(↑((toLin_equiv b : (a : Matrix.SpecialLinearGroup ι R) → _root_.SpecialLinearGroup R V)
                      (↑g : Matrix.SpecialLinearGroup ι R)) :
                  V ≃ₗ[R] V) :
              V →ₗ[R] V) :
            (a : V) → V)
          x :
        V)
neg :
  let g' : ↥(center (_root_.SpecialLinearGroup R V)) :=
    (centerCongr (toLin_equiv b) :
        (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(center (_root_.SpecialLinearGroup R V)))
      g;
  ∀
    (hgg' :
      ∀ (x : V),
        Eq (α := V) (((↑(↑(↑g' : _root_.SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) : (a : V) → V) x : V)
          (((↑(↑((toLin_equiv b : (a : Matrix.SpecialLinearGroup ι R) → _root_.SpecialLinearGroup R V)
                          (↑g : Matrix.SpecialLinearGroup ι R)) :
                      V ≃ₗ[R] V) :
                  V →ₗ[R] V) :
                (a : V) → V)
              x :
            V)),
    HSMul.hSMul.{u_4, u_5, u_5} (α := R) (β := V →ₗ[R] V)
        (↑(↑((centerEquivRootsOfUnity :
                    (a : ↥(center (_root_.SpecialLinearGroup R V))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
                  g') :
              Rˣ) :
          R)
        LinearMap.id =
      HSMul.hSMul.{u_4, u_5, u_5} (α := R) (β := V →ₗ[R] V)
        (↑(↑((center_equiv_rootsOfUnity :
                    (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
                  g) :
              Rˣ) :
          R)
        LinearMap.id
⊢ HSMul.hSMul.{u_4, u_5, u_5} (α := R) (β := V →ₗ[R] V)
      (↑(↑((centerEquivRootsOfUnity :
                  (a : ↥(center (_root_.SpecialLinearGroup R V))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
                ((centerCongr (toLin_equiv b) :
                    (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(center (_root_.SpecialLinearGroup R V)))
                  g)) :
            Rˣ) :
        R)
      LinearMap.id =
    HSMul.hSMul.{u_4, u_5, u_5} (α := R) (β := V →ₗ[R] V)
      (↑(↑((center_equiv_rootsOfUnity :
                  (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
                g) :
            Rˣ) :
        R)
      LinearMap.id

Tactic:
set g' := ((Subgroup.centerCongr (Matrix.SpecialLinearGroup.toLin_equiv b)) g)

Premises used: Matrix.SpecialLinearGroup.toLin_equiv, Subgroup.centerCongr, DFunLike.coe