awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ¬Subsingleton V
⊢ ¬IsEmpty ι

Tactic:
have hι : ¬ IsEmpty ι := fun hι ↦ hV (by
      rw [← Module.finrank_eq_zero_iff_of_free (R := R),
        Module.finrank_eq_card_basis b, Fintype.card_of_isEmpty])
-- 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 : ¬Subsingleton V
hι : ¬IsEmpty ι
⊢ Nontrivial V

Tactic:
rw [not_subsingleton_iff_nontrivial] at hV

Premises used: not_subsingleton_iff_nontrivial
-- 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 : ¬Subsingleton V
hι : ¬IsEmpty ι
hV₁ : Nontrivial V
⊢ ¬IsEmpty ι

Tactic:
rw [not_subsingleton_iff_nontrivial] at hV

Premises used: not_subsingleton_iff_nontrivial
-- 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 ι
⊢ FaithfulSMul R V

Tactic:
have := Module.Free.instFaithfulSMulOfNontrivial R V
-- 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_1 : FaithfulSMul R V
this :
  HSMul.hSMul.{u_4, u_5, u_5} (α := R) (β := V →ₗ[R] V)
      (↑(↑((MulEquiv.trans (centerCongr (toLin_equiv b)) centerEquivRootsOfUnity :
                  (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(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
rw :
  Eq.{u_4 + 1} (α := R)
    (↑(↑((MulEquiv.trans (centerCongr (toLin_equiv b)) centerEquivRootsOfUnity :
                (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
              g) :
          Rˣ) :
      R)
    (↑(↑((center_equiv_rootsOfUnity :
                (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
              g) :
          Rˣ) :
      R)
⊢ Eq.{u_4 + 1} (α := Rˣ)
    (↑((MulEquiv.trans (centerCongr (toLin_equiv b)) centerEquivRootsOfUnity :
            (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
          g) :
      Rˣ)
    (↑((center_equiv_rootsOfUnity :
            (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
          g) :
      Rˣ)

Tactic:
rw [← Units.val_inj]

Premises used: Units.val_inj
-- 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_1 : FaithfulSMul R V
this :
  HSMul.hSMul.{u_4, u_5, u_5} (α := R) (β := V →ₗ[R] V)
      (↑(↑((MulEquiv.trans (centerCongr (toLin_equiv b)) centerEquivRootsOfUnity :
                  (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(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
apply :
  ∀ (a : V),
    HSMul.hSMul.{u_4, u_5, u_5} (α := R)
        (↑(↑((MulEquiv.trans (centerCongr (toLin_equiv b)) centerEquivRootsOfUnity :
                    (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
                  g) :
              Rˣ) :
          R)
        a =
      HSMul.hSMul.{u_4, u_5, u_5} (α := R)
        (↑(↑((center_equiv_rootsOfUnity :
                    (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
                  g) :
              Rˣ) :
          R)
        a
⊢ Eq.{u_4 + 1} (α := R)
    (↑(↑((MulEquiv.trans (centerCongr (toLin_equiv b)) centerEquivRootsOfUnity :
                (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
              g) :
          Rˣ) :
      R)
    (↑(↑((center_equiv_rootsOfUnity :
                (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
              g) :
          Rˣ) :
      R)

Tactic:
apply FaithfulSMul.eq_of_smul_eq_smul (α := V)

Premises used: FaithfulSMul.eq_of_smul_eq_smul
-- 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_1 : FaithfulSMul R V
this :
  HSMul.hSMul.{u_4, u_5, u_5} (α := R) (β := V →ₗ[R] V)
      (↑(↑((MulEquiv.trans (centerCongr (toLin_equiv b)) centerEquivRootsOfUnity :
                  (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(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
x : V
⊢ ∀ (x : V),
    HSMul.hSMul.{u_4, u_5, u_5} (α := R)
        (↑(↑((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)
        x =
      HSMul.hSMul.{u_4, u_5, u_5} (α := R)
        (↑(↑((center_equiv_rootsOfUnity :
                    (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
                  g) :
              Rˣ) :
          R)
        x

Tactic:
simp only [MulEquiv.trans_apply, LinearMap.ext_iff, LinearMap.smul_apply, LinearMap.id_coe,
        id_eq] at this

Premises used: LinearMap.smul_apply, LinearMap.id_coe, LinearMap.ext_iff, MulEquiv.trans_apply, id_eq
-- 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_1 : FaithfulSMul R V
x : V
this :
  ∀ (x : V),
    HSMul.hSMul.{u_4, u_5, u_5} (α := R)
        (↑(↑((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)
        x =
      HSMul.hSMul.{u_4, u_5, u_5} (α := R)
        (↑(↑((center_equiv_rootsOfUnity :
                    (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
                  g) :
              Rˣ) :
          R)
        x
rw :
  HSMul.hSMul.{u_4, u_5, u_5} (α := R)
      (↑(↑((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)
      x =
    HSMul.hSMul.{u_4, u_5, u_5} (α := R)
      (↑(↑((center_equiv_rootsOfUnity :
                  (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
                g) :
            Rˣ) :
        R)
      x
rw₁ rw₂ :
  HSMul.hSMul.{u_4, u_5, u_5} (α := R)
      (↑(↑((center_equiv_rootsOfUnity :
                  (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
                g) :
            Rˣ) :
        R)
      x =
    HSMul.hSMul.{u_4, u_5, u_5} (α := R)
      (↑(↑((center_equiv_rootsOfUnity :
                  (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
                g) :
            Rˣ) :
        R)
      x
⊢ HSMul.hSMul.{u_4, u_5, u_5} (α := R)
      (↑(↑((MulEquiv.trans (centerCongr (toLin_equiv b)) centerEquivRootsOfUnity :
                  (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
                g) :
            Rˣ) :
        R)
      x =
    HSMul.hSMul.{u_4, u_5, u_5} (α := R)
      (↑(↑((center_equiv_rootsOfUnity :
                  (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
                g) :
            Rˣ) :
        R)
      x

Tactic:
rw [MulEquiv.trans_apply, this]

Premises used: MulEquiv.trans_apply
-- 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
neg :
  HSMul.hSMul.{u_4, u_5, u_5} (α := R) (β := V →ₗ[R] V)
      (↑(↑((MulEquiv.trans (centerCongr (toLin_equiv b)) centerEquivRootsOfUnity :
                  (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(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
⊢ Eq.{u_4 + 1} (α := Rˣ)
    (↑((MulEquiv.trans (centerCongr (toLin_equiv b)) centerEquivRootsOfUnity :
            (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
          g) :
      Rˣ)
    (↑((center_equiv_rootsOfUnity :
            (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
          g) :
      Rˣ)

Tactic:
suffices (((((Subgroup.centerCongr (Matrix.SpecialLinearGroup.toLin_equiv b)).trans
      centerEquivRootsOfUnity g).val : R) • LinearMap.id) : V →ₗ[R] V) =
        ((Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity g).val : R) • LinearMap.id by
      rw [← Units.val_inj]
      apply FaithfulSMul.eq_of_smul_eq_smul (α := V)
      intro x
      simp only [MulEquiv.trans_apply, LinearMap.ext_iff, LinearMap.smul_apply, LinearMap.id_coe,
        id_eq] at this
      rw [MulEquiv.trans_apply, this]
-- 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
neg :
  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
⊢ HSMul.hSMul.{u_4, u_5, u_5} (α := R) (β := V →ₗ[R] V)
      (↑(↑((MulEquiv.trans (centerCongr (toLin_equiv b)) centerEquivRootsOfUnity :
                  (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(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

Tactic:
simp only [MulEquiv.trans_apply]

Premises used: MulEquiv.trans_apply
-- 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
⊢ Eq.{u_5 + 1} (α := _root_.SpecialLinearGroup R V)
    ((↑((centerCongr (toLin_equiv b) :
              (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(center (_root_.SpecialLinearGroup R V)))
            g) :
        _root_.SpecialLinearGroup R V) :
      _root_.SpecialLinearGroup R V)
    ((toLin_equiv b : (a : Matrix.SpecialLinearGroup ι R) → _root_.SpecialLinearGroup R V)
        (↑g : Matrix.SpecialLinearGroup ι R) :
      _root_.SpecialLinearGroup R V)

Tactic:
have hgg' := Subgroup.centerCongr_apply_coe (Matrix.SpecialLinearGroup.toLin_equiv b) g
-- 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' :
  Eq.{u_5 + 1} (α := _root_.SpecialLinearGroup R V)
    ((↑((centerCongr (toLin_equiv b) :
              (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(center (_root_.SpecialLinearGroup R V)))
            g) :
        _root_.SpecialLinearGroup R V) :
      _root_.SpecialLinearGroup R V)
    ((toLin_equiv b : (a : Matrix.SpecialLinearGroup ι R) → _root_.SpecialLinearGroup R V)
        (↑g : Matrix.SpecialLinearGroup ι R) :
      _root_.SpecialLinearGroup R V)
⊢ ∀ (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)

Tactic:
rw [← Subtype.coe_inj, ← LinearEquiv.toLinearMap_inj, LinearMap.ext_iff] at hgg'

Premises used: LinearEquiv.toLinearMap_inj, Subtype.coe_inj, LinearMap.ext_iff
-- 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
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)
neg :
  ∀ (x : V),
    Eq (α := 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 :
            (a : V) → V)
          x :
        V)
      ((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 :
            (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

Tactic:
ext x
-- 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
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)
x : V
⊢ HSMul.hSMul.{u_4, u_5, u_5} (α := ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
      ((centerEquivRootsOfUnity :
            (a : ↥(center (_root_.SpecialLinearGroup R V))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
          g' :
        ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
      x =
    (fun (x : V) ↦ (((↑(↑g' : _root_.SpecialLinearGroup R V) : V ≃ₗ[R] V) : (a : V) → V) x : V)) x

Tactic:
have := centerEquivRootsOfUnity_apply_apply g' x
-- 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_1 : FaithfulSMul R V
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)
x : V
this :
  HSMul.hSMul.{u_4, u_5, u_5} (α := R)
      (↑(↑((centerEquivRootsOfUnity :
                  (a : ↥(center (_root_.SpecialLinearGroup R V))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
                g') :
            Rˣ) :
        R)
      x =
    ((↑(↑g' : _root_.SpecialLinearGroup R V) : V ≃ₗ[R] V) : (a : V) → V) x
neg :
  HSMul.hSMul.{u_4, u_5, u_5} (α := R)
      (↑(↑((centerEquivRootsOfUnity :
                  (a : ↥(center (_root_.SpecialLinearGroup R V))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
                g') :
            Rˣ) :
        R)
      x =
    HSMul.hSMul.{u_4, u_5, u_5} (α := R)
      (↑(↑((center_equiv_rootsOfUnity :
                  (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
                g) :
            Rˣ) :
        R)
      x
⊢ Eq (α := 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 :
          (a : V) → V)
        x :
      V)
    ((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 :
          (a : V) → V)
        x :
      V)

Tactic:
simp only [LinearMap.smul_apply, LinearMap.id_coe, id_eq]

Premises used: LinearMap.smul_apply, LinearMap.id_coe, id_eq