awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
hR : ¬Subsingleton R
hV_1 : ¬Subsingleton V
hV : Nontrivial V
this_1 : FaithfulSMul R V
H :
  ∃ (r_1 : R),
    r_1 ^ Module.finrank R V = 1 ∧
      (↑(↑(↑(centerEquivRootsOfUnity_invFun r) : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
        HSMul.hSMul (β := V →ₗ[R] V) r_1 LinearMap.id
this :
  HSMul.hSMul (β := V →ₗ[R] V)
      (H.choose (p := fun (r_1 : R) ↦
        r_1 ^ Module.finrank R V = 1 ∧
          (↑(↑(↑(centerEquivRootsOfUnity_invFun r) : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
            HSMul.hSMul (β := V →ₗ[R] V) r_1 LinearMap.id))
      LinearMap.id =
    HSMul.hSMul (β := V →ₗ[R] V) (↑(↑r : Rˣ) : R) LinearMap.id
x : V
rw :
  ∀
    (this :
      ∀ (x : V),
        Eq (α := V)
          ((HSMul.hSMul (β := V →ₗ[R] V)
                  (H.choose (p := fun (r_1 : R) ↦
                    r_1 ^ Module.finrank R V = 1 ∧
                      (↑(↑(↑(centerEquivRootsOfUnity_invFun r) : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
                        HSMul.hSMul (β := V →ₗ[R] V) r_1 LinearMap.id))
                  LinearMap.id :
                (a : V) → V)
              x :
            V)
          ((HSMul.hSMul (β := V →ₗ[R] V) (↑(↑r : Rˣ) : R) LinearMap.id : (a : V) → V) x : V))
    (x : V),
    ⋯.choose (p := fun (r_1 : R) ↦
          r_1 ^ Module.finrank R V = 1 ∧
            (↑(↑(↑(centerEquivRootsOfUnity_invFun r) : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
              HSMul.hSMul (β := V →ₗ[R] V) r_1 LinearMap.id) •
        x =
      (↑(↑r : Rˣ) : R) • x
⊢ ⋯.choose (p := fun (r_1 : R) ↦
        r_1 ^ Module.finrank R V = 1 ∧
          (↑(↑(↑(centerEquivRootsOfUnity_invFun r) : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
            HSMul.hSMul (β := V →ₗ[R] V) r_1 LinearMap.id) •
      x =
    (↑(↑r : Rˣ) : R) • x

Tactic:
rw [LinearMap.ext_iff] at this

Premises used: LinearMap.ext_iff
-- 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
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
hR : ¬Subsingleton R
hV_1 : ¬Subsingleton V
hV : Nontrivial V
this_1 : FaithfulSMul R V
H :
  ∃ (r_1 : R),
    r_1 ^ Module.finrank R V = 1 ∧
      (↑(↑(↑(centerEquivRootsOfUnity_invFun r) : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
        HSMul.hSMul (β := V →ₗ[R] V) r_1 LinearMap.id
this :
  ∀ (x : V),
    H.choose (p := fun (r_1 : R) ↦
          r_1 ^ Module.finrank R V = 1 ∧
            (↑(↑(↑(centerEquivRootsOfUnity_invFun r) : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
              HSMul.hSMul (β := V →ₗ[R] V) r_1 LinearMap.id) •
        x =
      (↑(↑r : Rˣ) : R) • x
x : V
rw rw₁ : (↑(↑r : Rˣ) : R) • x = (↑(↑r : Rˣ) : R) • x
⊢ ⋯.choose (p := fun (r_1 : R) ↦
        r_1 ^ Module.finrank R V = 1 ∧
          (↑(↑(↑(centerEquivRootsOfUnity_invFun r) : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
            HSMul.hSMul (β := V →ₗ[R] V) r_1 LinearMap.id) •
      x =
    (↑(↑r : Rˣ) : R) • x

Tactic:
rw [this x]
-- 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
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
hR : ¬Subsingleton R
hV_1 : ¬Subsingleton V
hV : Nontrivial V
this : FaithfulSMul R V
H :
  ∃ (r_1 : R),
    r_1 ^ Module.finrank R V = 1 ∧
      (↑(↑(↑(centerEquivRootsOfUnity_invFun r) : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
        HSMul.hSMul (β := V →ₗ[R] V) r_1 LinearMap.id
neg :
  HSMul.hSMul (β := V →ₗ[R] V)
      (H.choose (p := fun (r_1 : R) ↦
        r_1 ^ Module.finrank R V = 1 ∧
          (↑(↑(↑(centerEquivRootsOfUnity_invFun r) : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
            HSMul.hSMul (β := V →ₗ[R] V) r_1 LinearMap.id))
      LinearMap.id =
    HSMul.hSMul (β := V →ₗ[R] V) (↑(↑r : Rˣ) : R) LinearMap.id
⊢ ⋯.choose (p := fun (r_1 : R) ↦
      r_1 ^ Module.finrank R V = 1 ∧
        (↑(↑(↑(centerEquivRootsOfUnity_invFun r) : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
          HSMul.hSMul (β := V →ₗ[R] V) r_1 LinearMap.id) =
    (↑(↑r : Rˣ) : R)

Tactic:
suffices (H.choose • LinearMap.id : V →ₗ[R] V) = (r.val : R) • LinearMap.id by
        apply FaithfulSMul.eq_of_smul_eq_smul (α := V)
        intro x
        rw [LinearMap.ext_iff] at this
        simp only [LinearMap.smul_apply, LinearMap.id_coe, id_eq] at this
        rw [this x]
-- 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
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
hR : ¬Subsingleton R
hV_1 : ¬Subsingleton V
hV : Nontrivial V
this : FaithfulSMul R V
H :
  ∃ (r_1 : R),
    r_1 ^ Module.finrank R V = 1 ∧
      (↑(↑(↑(centerEquivRootsOfUnity_invFun r) : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
        HSMul.hSMul (β := V →ₗ[R] V) r_1 LinearMap.id
neg :
  (↑(↑(↑(centerEquivRootsOfUnity_invFun r) : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
    HSMul.hSMul (β := V →ₗ[R] V) (↑(↑r : Rˣ) : R) LinearMap.id
⊢ HSMul.hSMul (β := V →ₗ[R] V)
      (H.choose (p := fun (r_1 : R) ↦
        r_1 ^ Module.finrank R V = 1 ∧
          (↑(↑(↑(centerEquivRootsOfUnity_invFun r) : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
            HSMul.hSMul (β := V →ₗ[R] V) r_1 LinearMap.id))
      LinearMap.id =
    HSMul.hSMul (β := V →ₗ[R] V) (↑(↑r : Rˣ) : R) LinearMap.id

Tactic:
rw [← H.choose_spec.2]

Premises used: Exists.choose_spec, And.right
-- 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
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
hR : ¬Subsingleton R
hV_1 : ¬Subsingleton V
hV : Nontrivial V
this : FaithfulSMul R V
H :
  ∃ (r_1 : R),
    r_1 ^ Module.finrank R V = 1 ∧
      (↑(↑(↑(centerEquivRootsOfUnity_invFun r) : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
        HSMul.hSMul (β := V →ₗ[R] V) r_1 LinearMap.id
⊢ (↑(↑(↑(centerEquivRootsOfUnity_invFun r) : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
    HSMul.hSMul (β := V →ₗ[R] V) (↑(↑r : Rˣ) : R) LinearMap.id

Tactic:
simp [centerEquivRootsOfUnity_invFun]

Premises used: SpecialLinearGroup.centerEquivRootsOfUnity_invFun
-- 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 h : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : Subsingleton R
⊢ Eq.{u_1 + 1} (α := ↥(rootsOfUnity (max (Module.finrank R V) 1) R)) 1 1

Tactic:
rfl
-- 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 h : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV : Subsingleton V
⊢ Eq.{u_1 + 1} (α := ↥(rootsOfUnity (max (Module.finrank R V) 1) R)) 1 1

Tactic:
rfl
-- 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 h : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV : ¬Subsingleton V
⊢ Nontrivial V

Tactic:
rw [not_subsingleton_iff_nontrivial] at hV

Premises used: not_subsingleton_iff_nontrivial
-- 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 h : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV_1 : ¬Subsingleton V
hV : Nontrivial V
⊢ FaithfulSMul R V

Tactic:
have := Module.Free.instFaithfulSMulOfNontrivial R V
-- 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 h : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV_1 : ¬Subsingleton V
hV : Nontrivial V
this : FaithfulSMul R V
neg :
  let Hg := ⋯;
  Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x)
      (IsUnit.unit (a :=
        ⋯.choose (p := fun (r : R) ↦
          r ^ Module.finrank R V = 1 ∧
            (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) *
                (↑(↑(↑h : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
              HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id))
        ⋯)
      ⋯ =
    Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x)
      (HMul.hMul (α := Rˣ)
        (IsUnit.unit (a :=
          Hg.choose (p := fun (r : R) ↦
            r ^ Module.finrank R V = 1 ∧
              (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
                HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id))
          ⋯)
        (IsUnit.unit (a :=
          ⋯.choose (p := fun (r : R) ↦
            r ^ Module.finrank R V = 1 ∧
              (↑(↑(↑h : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
                HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id))
          ⋯))
      ⋯
⊢ Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x)
      (IsUnit.unit (a :=
        ⋯.choose (p := fun (r : R) ↦
          r ^ Module.finrank R V = 1 ∧
            (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) *
                (↑(↑(↑h : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
              HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id))
        ⋯)
      ⋯ =
    Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x)
      (HMul.hMul (α := Rˣ)
        (IsUnit.unit (a :=
          ⋯.choose (p := fun (r : R) ↦
            r ^ Module.finrank R V = 1 ∧
              (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
                HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id))
          ⋯)
        (IsUnit.unit (a :=
          ⋯.choose (p := fun (r : R) ↦
            r ^ Module.finrank R V = 1 ∧
              (↑(↑(↑h : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
                HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id))
          ⋯))
      ⋯

Tactic:
set Hg := (mem_center_iff.mp g.prop)

Premises used: SpecialLinearGroup.mem_center_iff, Subtype.prop, Iff.mp
-- 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 h : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV_1 : ¬Subsingleton V
hV : Nontrivial V
this : FaithfulSMul R V
Hg : ∃ (r : R),
  r ^ Module.finrank R V = 1 ∧
    (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id :=
  ⋯
neg :
  let Hh := ⋯;
  Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x)
      (IsUnit.unit (a :=
        ⋯.choose (p := fun (r : R) ↦
          r ^ Module.finrank R V = 1 ∧
            (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) *
                (↑(↑(↑h : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
              HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id))
        ⋯)
      ⋯ =
    Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x)
      (HMul.hMul (α := Rˣ)
        (IsUnit.unit (a :=
          Hg.choose (p := fun (r : R) ↦
            r ^ Module.finrank R V = 1 ∧
              (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
                HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id))
          ⋯)
        (IsUnit.unit (a :=
          Hh.choose (p := fun (r : R) ↦
            r ^ Module.finrank R V = 1 ∧
              (↑(↑(↑h : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
                HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id))
          ⋯))
      ⋯
⊢ Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x)
      (IsUnit.unit (a :=
        ⋯.choose (p := fun (r : R) ↦
          r ^ Module.finrank R V = 1 ∧
            (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) *
                (↑(↑(↑h : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
              HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id))
        ⋯)
      ⋯ =
    Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x)
      (HMul.hMul (α := Rˣ)
        (IsUnit.unit (a :=
          Hg.choose (p := fun (r : R) ↦
            r ^ Module.finrank R V = 1 ∧
              (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
                HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id))
          ⋯)
        (IsUnit.unit (a :=
          ⋯.choose (p := fun (r : R) ↦
            r ^ Module.finrank R V = 1 ∧
              (↑(↑(↑h : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
                HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id))
          ⋯))
      ⋯

Tactic:
set Hh := (mem_center_iff.mp h.prop)

Premises used: SpecialLinearGroup.mem_center_iff, Subtype.prop, Iff.mp
-- 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 h : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV_1 : ¬Subsingleton V
hV : Nontrivial V
this : FaithfulSMul R V
Hg : ∃ (r : R),
  r ^ Module.finrank R V = 1 ∧
    (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id :=
  ⋯
Hh : ∃ (r : R),
  r ^ Module.finrank R V = 1 ∧
    (↑(↑(↑h : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id :=
  ⋯
Hgh : ∃ (r : R),
  r ^ Module.finrank R V = 1 ∧
    (↑(↑(↑(g * h) : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id :=
  ⋯
neg :
  ⋯.choose (p := fun (r : R) ↦
      r ^ Module.finrank R V = 1 ∧
        (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) *
            (↑(↑(↑h : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
          HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id) =
    Hg.choose (p := fun (r : R) ↦
        r ^ Module.finrank R V = 1 ∧
          (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id) *
      Hh.choose (p := fun (r : R) ↦
        r ^ Module.finrank R V = 1 ∧
          (↑(↑(↑h : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id)
⊢ Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x)
      (IsUnit.unit (a :=
        ⋯.choose (p := fun (r : R) ↦
          r ^ Module.finrank R V = 1 ∧
            (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) *
                (↑(↑(↑h : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
              HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id))
        ⋯)
      ⋯ =
    Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x)
      (HMul.hMul (α := Rˣ)
        (IsUnit.unit (a :=
          Hg.choose (p := fun (r : R) ↦
            r ^ Module.finrank R V = 1 ∧
              (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
                HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id))
          ⋯)
        (IsUnit.unit (a :=
          Hh.choose (p := fun (r : R) ↦
            r ^ Module.finrank R V = 1 ∧
              (↑(↑(↑h : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
                HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id))
          ⋯))
      ⋯

Tactic:
simp only [← Subtype.val_inj, ← Units.val_inj, IsUnit.unit_spec, Units.val_mul]

Premises used: Subtype.val_inj, Units.val_inj, IsUnit.unit_spec, Units.val_mul
-- 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 h : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV_1 : ¬Subsingleton V
hV : Nontrivial V
this : FaithfulSMul R V
Hg : ∃ (r : R),
  r ^ Module.finrank R V = 1 ∧
    (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id :=
  ⋯
Hh : ∃ (r : R),
  r ^ Module.finrank R V = 1 ∧
    (↑(↑(↑h : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id :=
  ⋯
Hgh : ∃ (r : R),
  r ^ Module.finrank R V = 1 ∧
    (↑(↑(↑(g * h) : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id :=
  ⋯
neg :
  Hgh.choose (p := fun (r : R) ↦
      r ^ Module.finrank R V = 1 ∧
        (↑(↑(↑(g * h) : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
          HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id) =
    Hg.choose (p := fun (r : R) ↦
        r ^ Module.finrank R V = 1 ∧
          (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id) *
      Hh.choose (p := fun (r : R) ↦
        r ^ Module.finrank R V = 1 ∧
          (↑(↑(↑h : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id)
⊢ ⋯.choose (p := fun (r : R) ↦
      r ^ Module.finrank R V = 1 ∧
        (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) *
            (↑(↑(↑h : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
          HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id) =
    Hg.choose (p := fun (r : R) ↦
        r ^ Module.finrank R V = 1 ∧
          (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id) *
      Hh.choose (p := fun (r : R) ↦
        r ^ Module.finrank R V = 1 ∧
          (↑(↑(↑h : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id)

Tactic:
change Hgh.choose = Hg.choose * Hh.choose

Premises used: Exists.choose
-- 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 h : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV_1 : ¬Subsingleton V
hV : Nontrivial V
this_1 : FaithfulSMul R V
Hg : ∃ (r : R),
  r ^ Module.finrank R V = 1 ∧
    (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id :=
  ⋯
Hh : ∃ (r : R),
  r ^ Module.finrank R V = 1 ∧
    (↑(↑(↑h : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id :=
  ⋯
Hgh : ∃ (r : R),
  r ^ Module.finrank R V = 1 ∧
    (↑(↑(↑(g * h) : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id :=
  ⋯
this :
  HSMul.hSMul (β := V →ₗ[R] V)
      (Hgh.choose (p := fun (r : R) ↦
        r ^ Module.finrank R V = 1 ∧
          (↑(↑(↑(g * h) : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
            HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id))
      LinearMap.id =
    HSMul.hSMul (β := V →ₗ[R] V)
        (Hg.choose (p := fun (r : R) ↦
          r ^ Module.finrank R V = 1 ∧
            (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id))
        LinearMap.id *
      HSMul.hSMul (β := V →ₗ[R] V)
        (Hh.choose (p := fun (r : R) ↦
          r ^ Module.finrank R V = 1 ∧
            (↑(↑(↑h : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id))
        LinearMap.id
apply :
  ∀ (a : V),
    Hgh.choose (p := fun (r : R) ↦
          r ^ Module.finrank R V = 1 ∧
            (↑(↑(↑(g * h) : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
              HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id) •
        a =
      (Hg.choose (p := fun (r : R) ↦
            r ^ Module.finrank R V = 1 ∧
              (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
                HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id) *
          Hh.choose (p := fun (r : R) ↦
            r ^ Module.finrank R V = 1 ∧
              (↑(↑(↑h : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
                HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id)) •
        a
⊢ Hgh.choose (p := fun (r : R) ↦
      r ^ Module.finrank R V = 1 ∧
        (↑(↑(↑(g * h) : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
          HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id) =
    Hg.choose (p := fun (r : R) ↦
        r ^ Module.finrank R V = 1 ∧
          (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id) *
      Hh.choose (p := fun (r : R) ↦
        r ^ Module.finrank R V = 1 ∧
          (↑(↑(↑h : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id)

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_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 h : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV_1 : ¬Subsingleton V
hV : Nontrivial V
this_1 : FaithfulSMul R V
Hg : ∃ (r : R),
  r ^ Module.finrank R V = 1 ∧
    (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id :=
  ⋯
Hh : ∃ (r : R),
  r ^ Module.finrank R V = 1 ∧
    (↑(↑(↑h : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id :=
  ⋯
Hgh : ∃ (r : R),
  r ^ Module.finrank R V = 1 ∧
    (↑(↑(↑(g * h) : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id :=
  ⋯
this :
  HSMul.hSMul (β := V →ₗ[R] V)
      (Hgh.choose (p := fun (r : R) ↦
        r ^ Module.finrank R V = 1 ∧
          (↑(↑(↑(g * h) : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
            HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id))
      LinearMap.id =
    HSMul.hSMul (β := V →ₗ[R] V)
        (Hg.choose (p := fun (r : R) ↦
          r ^ Module.finrank R V = 1 ∧
            (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id))
        LinearMap.id *
      HSMul.hSMul (β := V →ₗ[R] V)
        (Hh.choose (p := fun (r : R) ↦
          r ^ Module.finrank R V = 1 ∧
            (↑(↑(↑h : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id))
        LinearMap.id
x : V
⊢ Hgh.choose (p := fun (r : R) ↦
        r ^ Module.finrank R V = 1 ∧
          (↑(↑(↑(g * h) : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
            HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id) •
      x =
    (Hg.choose (p := fun (r : R) ↦
          r ^ Module.finrank R V = 1 ∧
            (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id) *
        Hh.choose (p := fun (r : R) ↦
          r ^ Module.finrank R V = 1 ∧
            (↑(↑(↑h : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
              HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id)) •
      x

Tactic:
simp [mul_smul,
        ← mem_center_iff_spec (g * h).prop, ← mem_center_iff_spec h.prop,
        ← mem_center_iff_spec g.prop]

Premises used: SpecialLinearGroup.mem_center_iff_spec, HMul.hMul, Subtype.prop, SemigroupAction.mul_smul