-- 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))
simp :
  Eq.{u_1 + 1} (α := ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
    (if h : Subsingleton R then 1
    else
      if h : Subsingleton V then 1
      else
        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))
            ⋯)
          ⋯)
    (if h : Subsingleton R then
      if h : Subsingleton R then 1
      else
        if h : Subsingleton V then 1
        else
          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) =
                    HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id))
              ⋯)
            ⋯
    else
      if h : Subsingleton V then
        if h : Subsingleton R then 1
        else
          if h : Subsingleton V then 1
          else
            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) =
                      HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id))
                ⋯)
              ⋯
      else
        if h_1 : Subsingleton R then
          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 ∧
                  (↑(↑(↑h : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
                    HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id))
              ⋯)
            ⋯
        else
          if h_2 : Subsingleton V then
            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 ∧
                    (↑(↑(↑h : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
                      HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id))
                ⋯)
              ⋯
          else
            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))
                  ⋯))
              ⋯)
⊢ (⋯.by_cases (fun (x : Subsingleton R) ↦ 1) fun (hR : Nontrivial R) ↦
      ⋯.by_cases (fun (x : Subsingleton V) ↦ 1) fun (hV : Nontrivial V) ↦
        have hV : 1 ≤ Module.finrank R V := ⋯;
        have hr := ⋯;
        let r :=
          ⋯.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);
        have this : IsUnit r := ⋯;
        Subtype.mk (p := fun (x : Rˣ) ↦
          Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x) this.unit ⋯) =
    HMul.hMul (α := ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
      (⋯.by_cases (fun (x : Subsingleton R) ↦ 1) fun (hR : Nontrivial R) ↦
        ⋯.by_cases (fun (x : Subsingleton V) ↦ 1) fun (hV : Nontrivial V) ↦
          have hV : 1 ≤ Module.finrank R V := ⋯;
          have hr := ⋯;
          let r :=
            ⋯.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);
          have this : IsUnit r := ⋯;
          Subtype.mk (p := fun (x : Rˣ) ↦
            Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x) this.unit ⋯)
      (⋯.by_cases (fun (x : Subsingleton R) ↦ 1) fun (hR : Nontrivial R) ↦
        ⋯.by_cases (fun (x : Subsingleton V) ↦ 1) fun (hV : Nontrivial V) ↦
          have hV : 1 ≤ Module.finrank R V := ⋯;
          have hr := ⋯;
          let r :=
            ⋯.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);
          have this : IsUnit r := ⋯;
          Subtype.mk (p := fun (x : Rˣ) ↦
            Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x) this.unit ⋯)

Tactic:
simp only [Or.by_cases, Subgroup.coe_mul, coe_mul, LinearEquiv.coe_toLinearMap_mul,
      mul_dite, mul_one, dite_mul, one_mul, MulMemClass.mk_mul_mk]

Premises used: LinearEquiv.coe_toLinearMap_mul, SpecialLinearGroup.coe_mul, Subgroup.coe_mul, Or.by_cases, dite_mul, MulMemClass.mk_mul_mk, mul_one, one_mul, mul_dite