awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
hA : Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) A
i : n
r : R
hr : (scalar n : (a : R) → Matrix n n R) r = (↑A : Matrix n n R)
⊢ (scalar n : (a : R) → Matrix n n R) ((↑A : Matrix n n R) i i) = (↑A : Matrix n n R)

Tactic:
simp [← congr_fun₂ hr i i, ← hr]

Premises used: congr_fun₂
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : ↥(center (SpecialLinearGroup n R))
i : n
⊢ (scalar n : (a : R) → Matrix n n R) ((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i) =
    (↑(↑A : SpecialLinearGroup n R) : Matrix n n R)

Tactic:
scalar_eq_self_of_mem_center A.property i

Premises used: Matrix.SpecialLinearGroup.scalar_eq_self_of_mem_center, Subtype.property
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
inl :
  ∀ (hn : IsEmpty n),
    Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) A ↔
      ∃ (r : R), r ^ Fintype.card n = 1 ∧ (scalar n : (a : R) → Matrix n n R) r = (↑A : Matrix n n R)
inr :
  ∀ (i : n),
    Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) A ↔
      ∃ (r : R), r ^ Fintype.card n = 1 ∧ (scalar n : (a : R) → Matrix n n R) r = (↑A : Matrix n n R)
⊢ Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) A ↔
    ∃ (r : R), r ^ Fintype.card n = 1 ∧ (scalar n : (a : R) → Matrix n n R) r = (↑A : Matrix n n R)

Tactic:
rcases isEmpty_or_nonempty n with hn | ⟨⟨i⟩⟩

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
hn : IsEmpty n
⊢ Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) A →
    ∃ (r : R), r ^ Fintype.card n = 1 ∧ (scalar n : (a : R) → Matrix n n R) r = (↑A : Matrix n n R)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
hn : IsEmpty n
⊢ (∃ (r : R), r ^ Fintype.card n = 1 ∧ (scalar n : (a : R) → Matrix n n R) r = (↑A : Matrix n n R)) →
    Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) A

Tactic:
simp [Subsingleton.elim A 1]

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
hn : IsEmpty n
⊢ Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) A ↔
    ∃ (r : R), r ^ Fintype.card n = 1 ∧ (scalar n : (a : R) → Matrix n n R) r = (↑A : Matrix n n R)

Tactic:
exact ⟨by aesop, by simp [Subsingleton.elim A 1]⟩
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
i : n
⊢ Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) A ↔
    ∃ (r : R), r ^ Fintype.card n = 1 ∧ (scalar n : (a : R) → Matrix n n R) r = (↑A : Matrix n n R)

Tactic:
⟨fun h ↦ ⟨A i i, ?_, ?_⟩, fun ⟨r, _, hr⟩ ↦ Subgroup.mem_center_iff.mpr fun B ↦ ?_⟩

Premises used: Iff.mpr, Matrix.SpecialLinearGroup, Subgroup.mem_center_iff, Membership.mem, Subgroup.center, _private.0.Matrix.SpecialLinearGroup.mem_center_iff.match_3, And.intro, Iff.intro, Exists.intro, Subtype.val
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
i : n
inr :
  ∀ (h : Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) A),
    (↑A : Matrix n n R) i i ^ Fintype.card n = 1
inr₁ :
  ∀ (h : Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) A),
    (scalar n : (a : R) → Matrix n n R) ((↑A : Matrix n n R) i i) = (↑A : Matrix n n R)
inr₂ :
  (∃ (r : R), r ^ Fintype.card n = 1 ∧ (scalar n : (a : R) → Matrix n n R) r = (↑A : Matrix n n R)) →
    ∀ (r : R),
      r ^ Fintype.card n = 1 →
        ∀ (hr : (scalar n : (a : R) → Matrix n n R) r = (↑A : Matrix n n R)) (B : SpecialLinearGroup n R), B * A = A * B
⊢ Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) A ↔
    ∃ (r : R), r ^ Fintype.card n = 1 ∧ (scalar n : (a : R) → Matrix n n R) r = (↑A : Matrix n n R)

Tactic:
refine ⟨fun h ↦ ⟨A i i, ?_, ?_⟩, fun ⟨r, _, hr⟩ ↦ Subgroup.mem_center_iff.mpr fun B ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
i : n
h : Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) A
⊢ Eq.{v + 1} (α := R) (det.{v, u} (n := n) ((scalar n : (a : R) → Matrix n n R) ((↑A : Matrix n n R) i i))) 1

Tactic:
have : det ((scalar n) (A i i)) = 1 := (scalar_eq_self_of_mem_center h i).symm ▸ A.property
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
i : n
h : Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) A
this : Eq.{v + 1} (α := R) (det.{v, u} (n := n) ((scalar n : (a : R) → Matrix n n R) ((↑A : Matrix n n R) i i))) 1
⊢ (↑A : Matrix n n R) i i ^ Fintype.card n = 1

Tactic:
simpa using this
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
i : n
h : Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) A
⊢ (scalar n : (a : R) → Matrix n n R) ((↑A : Matrix n n R) i i) = (↑A : Matrix n n R)

Tactic:
scalar_eq_self_of_mem_center h i

Premises used: Matrix.SpecialLinearGroup.scalar_eq_self_of_mem_center
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
i : n
h : Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) A
⊢ (scalar n : (a : R) → Matrix n n R) ((↑A : Matrix n n R) i i) = (↑A : Matrix n n R)

Tactic:
exact scalar_eq_self_of_mem_center h i

Premises used: Matrix.SpecialLinearGroup.scalar_eq_self_of_mem_center
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
i : n
h : ∃ (r : R), r ^ Fintype.card n = 1 ∧ (scalar n : (a : R) → Matrix n n R) r = (↑A : Matrix n n R)
r : R
left : r ^ Fintype.card n = 1
hr : (scalar n : (a : R) → Matrix n n R) r = (↑A : Matrix n n R)
B : SpecialLinearGroup n R
inr : (↑(B * A) : Matrix n n R) = (↑(A * B) : Matrix n n R)
⊢ B * A = A * B

Tactic:
suffices ↑ₘ(B * A) = ↑ₘ(A * B) from Subtype.val_injective this
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
i : n
h : ∃ (r : R), r ^ Fintype.card n = 1 ∧ (scalar n : (a : R) → Matrix n n R) r = (↑A : Matrix n n R)
r : R
left : r ^ Fintype.card n = 1
hr : (scalar n : (a : R) → Matrix n n R) r = (↑A : Matrix n n R)
B : SpecialLinearGroup n R
⊢ (↑(B * A) : Matrix n n R) = (↑(A * B) : Matrix n n R)

Tactic:
simpa only [coe_mul, ← hr] using (scalar_commute (n := n) r (Commute.all r) B).symm

Premises used: Matrix.scalar_commute, Commute.symm, Subtype.val, Commute.all, Matrix.SpecialLinearGroup.coe_mul
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
i : n
A : ↥(center (SpecialLinearGroup n R))
this : Nonempty n
obtain :
  ∀ (r : R) (hr : r ^ Fintype.card n = 1)
    (hr' : (scalar n : (a : R) → Matrix n n R) r = (↑(↑A : SpecialLinearGroup n R) : Matrix n n R)),
    (↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i ^ Fintype.card n = 1
⊢ (↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i ^ Fintype.card n = 1

Tactic:
obtain ⟨r, hr, hr'⟩ := mem_center_iff.mp A.property

Premises used: Iff.mp, Subtype.property, Matrix.SpecialLinearGroup.mem_center_iff
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
i : n
A : ↥(center (SpecialLinearGroup n R))
this : Nonempty n
r : R
hr : r ^ Fintype.card n = 1
hr' : (scalar n : (a : R) → Matrix n n R) r = (↑(↑A : SpecialLinearGroup n R) : Matrix n n R)
⊢ (↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i = r

Tactic:
simp only [← hr', scalar_apply, diagonal_apply_eq]

Premises used: Matrix.diagonal_apply_eq, Matrix.scalar_apply
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
i : n
A : ↥(center (SpecialLinearGroup n R))
this : Nonempty n
r : R
hr : r ^ Fintype.card n = 1
hr' : (scalar n : (a : R) → Matrix n n R) r = (↑(↑A : SpecialLinearGroup n R) : Matrix n n R)
⊢ (↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i = r

Tactic:
replace hr' : A.val i i = r := by simp only [← hr', scalar_apply, diagonal_apply_eq]
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
i : n
A : ↥(center (SpecialLinearGroup n R))
this : Nonempty n
r : R
hr : r ^ Fintype.card n = 1
hr' : (↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i = r
⊢ (↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i ^ Fintype.card n = 1

Tactic:
simp only [hr', hr]
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
i : n
a : ↥(rootsOfUnity (Fintype.card n) R)
⊢ (HSMul.hSMul (β := Matrix n n R) a 1).det = 1

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
i : n
a : ↥(rootsOfUnity (Fintype.card n) R)
B : SpecialLinearGroup n R
⊢ (↑(B * Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) (HSMul.hSMul (β := Matrix n n R) a 1) ⋯) : Matrix n n R) =
    (↑(Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) (HSMul.hSMul (β := Matrix n n R) a 1) ⋯ * B) : Matrix n n R)

Tactic:
simp [coe_mul]

Premises used: Matrix.SpecialLinearGroup.coe_mul
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
i : n
A : ↥(center (SpecialLinearGroup n R))
⊢ (fun (a : ↥(rootsOfUnity (Fintype.card n) R)) ↦
        (Subtype.mk (p := fun (x : SpecialLinearGroup n R) ↦
            Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) x)
            (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) (HSMul.hSMul (β := Matrix n n R) a 1) ⋯) ⋯ :
          ↥(center (SpecialLinearGroup n R))))
      ((fun (A : ↥(center (SpecialLinearGroup n R))) ↦
          (rootsOfUnity.mkOfPowEq ((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i) ⋯ :
            ↥(rootsOfUnity (Fintype.card n) R)))
        A) =
    A

Tactic:
SetCoe.ext <| SetCoe.ext ?_

Premises used: SetCoe.ext
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
i : n
A : ↥(center (SpecialLinearGroup n R))
refine :
  (↑(↑((fun (a : ↥(rootsOfUnity (Fintype.card n) R)) ↦
                (Subtype.mk (p := fun (x : SpecialLinearGroup n R) ↦
                    Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) x)
                    (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) (HSMul.hSMul (β := Matrix n n R) a 1) ⋯) ⋯ :
                  ↥(center (SpecialLinearGroup n R))))
              ((fun (A : ↥(center (SpecialLinearGroup n R))) ↦
                  (rootsOfUnity.mkOfPowEq ((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i) ⋯ :
                    ↥(rootsOfUnity (Fintype.card n) R)))
                A)) :
          SpecialLinearGroup n R) :
      Matrix n n R) =
    (↑(↑A : SpecialLinearGroup n R) : Matrix n n R)
⊢ (fun (a : ↥(rootsOfUnity (Fintype.card n) R)) ↦
        (Subtype.mk (p := fun (x : SpecialLinearGroup n R) ↦
            Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) x)
            (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) (HSMul.hSMul (β := Matrix n n R) a 1) ⋯) ⋯ :
          ↥(center (SpecialLinearGroup n R))))
      ((fun (A : ↥(center (SpecialLinearGroup n R))) ↦
          (rootsOfUnity.mkOfPowEq ((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i) ⋯ :
            ↥(rootsOfUnity (Fintype.card n) R)))
        A) =
    A

Tactic:
refine SetCoe.ext <| SetCoe.ext ?_

Premises used: SetCoe.ext
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
i : n
A : ↥(center (SpecialLinearGroup n R))
obtain :
  ∀ (r : R),
    r ^ Fintype.card n = 1 →
      ∀ (hr : (scalar n : (a : R) → Matrix n n R) r = (↑(↑A : SpecialLinearGroup n R) : Matrix n n R)),
        (↑(↑((fun (a : ↥(rootsOfUnity (Fintype.card n) R)) ↦
                      (Subtype.mk (p := fun (x : SpecialLinearGroup n R) ↦
                          Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) x)
                          (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) (HSMul.hSMul (β := Matrix n n R) a 1) ⋯)
                          ⋯ :
                        ↥(center (SpecialLinearGroup n R))))
                    ((fun (A : ↥(center (SpecialLinearGroup n R))) ↦
                        (rootsOfUnity.mkOfPowEq ((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i) ⋯ :
                          ↥(rootsOfUnity (Fintype.card n) R)))
                      A)) :
                SpecialLinearGroup n R) :
            Matrix n n R) =
          (↑(↑A : SpecialLinearGroup n R) : Matrix n n R)
⊢ (↑(↑((fun (a : ↥(rootsOfUnity (Fintype.card n) R)) ↦
                (Subtype.mk (p := fun (x : SpecialLinearGroup n R) ↦
                    Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) x)
                    (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) (HSMul.hSMul (β := Matrix n n R) a 1) ⋯) ⋯ :
                  ↥(center (SpecialLinearGroup n R))))
              ((fun (A : ↥(center (SpecialLinearGroup n R))) ↦
                  (rootsOfUnity.mkOfPowEq ((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i) ⋯ :
                    ↥(rootsOfUnity (Fintype.card n) R)))
                A)) :
          SpecialLinearGroup n R) :
      Matrix n n R) =
    (↑(↑A : SpecialLinearGroup n R) : Matrix n n R)

Tactic:
obtain ⟨r, _, hr⟩ := mem_center_iff.mp A.property

Premises used: Iff.mp, Subtype.property, Matrix.SpecialLinearGroup.mem_center_iff
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
i : n
A : ↥(center (SpecialLinearGroup n R))
r : R
left : r ^ Fintype.card n = 1
hr : (scalar n : (a : R) → Matrix n n R) r = (↑(↑A : SpecialLinearGroup n R) : Matrix n n R)
⊢ (↑(↑((fun (a : ↥(rootsOfUnity (Fintype.card n) R)) ↦
                (Subtype.mk (p := fun (x : SpecialLinearGroup n R) ↦
                    Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) x)
                    (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) (HSMul.hSMul (β := Matrix n n R) a 1) ⋯) ⋯ :
                  ↥(center (SpecialLinearGroup n R))))
              ((fun (A : ↥(center (SpecialLinearGroup n R))) ↦
                  (rootsOfUnity.mkOfPowEq ((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i) ⋯ :
                    ↥(rootsOfUnity (Fintype.card n) R)))
                A)) :
          SpecialLinearGroup n R) :
      Matrix n n R) =
    (↑(↑A : SpecialLinearGroup n R) : Matrix n n R)

Tactic:
simpa [← hr, Submonoid.smul_def, Units.smul_def] using smul_one_eq_diagonal r

Premises used: Matrix.smul_one_eq_diagonal, Submonoid.smul_def, Units.smul_def
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
i : n
a : ↥(rootsOfUnity (Fintype.card n) R)
obtain :
  ∀ (a inv : R) (val_inv : a * inv = 1) (inv_val : inv * a = 1)
    (ha :
      Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card n) R)
        { val := a, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }),
    (fun (A : ↥(center (SpecialLinearGroup n R))) ↦
          (rootsOfUnity.mkOfPowEq ((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i) ⋯ :
            ↥(rootsOfUnity (Fintype.card n) R)))
        ((fun (a : ↥(rootsOfUnity (Fintype.card n) R)) ↦
            (Subtype.mk (p := fun (x : SpecialLinearGroup n R) ↦
                Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) x)
                (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) (HSMul.hSMul (β := Matrix n n R) a 1) ⋯) ⋯ :
              ↥(center (SpecialLinearGroup n R))))
          (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card n) R) x)
            { val := a, inv := inv, val_inv := val_inv, inv_val := inv_val } ha)) =
      Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card n) R) x)
        { val := a, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ } ha
⊢ (fun (A : ↥(center (SpecialLinearGroup n R))) ↦
        (rootsOfUnity.mkOfPowEq ((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i) ⋯ :
          ↥(rootsOfUnity (Fintype.card n) R)))
      ((fun (a : ↥(rootsOfUnity (Fintype.card n) R)) ↦
          (Subtype.mk (p := fun (x : SpecialLinearGroup n R) ↦
              Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) x)
              (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) (HSMul.hSMul (β := Matrix n n R) a 1) ⋯) ⋯ :
            ↥(center (SpecialLinearGroup n R))))
        a) =
    a

Tactic:
obtain ⟨⟨a, _⟩, ha⟩ := a
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
i : n
a inv : R
val_inv : a * inv = 1
inv_val : inv * a = 1
ha :
  Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card n) R)
    { val := a, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }
⊢ (↑(↑((fun (A : ↥(center (SpecialLinearGroup n R))) ↦
                (rootsOfUnity.mkOfPowEq ((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i) ⋯ :
                  ↥(rootsOfUnity (Fintype.card n) R)))
              ((fun (a : ↥(rootsOfUnity (Fintype.card n) R)) ↦
                  (Subtype.mk (p := fun (x : SpecialLinearGroup n R) ↦
                      Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) x)
                      (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) (HSMul.hSMul (β := Matrix n n R) a 1) ⋯) ⋯ :
                    ↥(center (SpecialLinearGroup n R))))
                (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card n) R) x)
                  { val := a, inv := inv, val_inv := val_inv, inv_val := inv_val } ha))) :
          Rˣ) :
      R) =
    (↑(↑(Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card n) R) x)
              { val := a, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ } ha) :
          Rˣ) :
      R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
i : n
a inv : R
val_inv : a * inv = 1
inv_val : inv * a = 1
ha :
  Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card n) R)
    { val := a, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }
⊢ (fun (A : ↥(center (SpecialLinearGroup n R))) ↦
        (rootsOfUnity.mkOfPowEq ((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i) ⋯ :
          ↥(rootsOfUnity (Fintype.card n) R)))
      ((fun (a : ↥(rootsOfUnity (Fintype.card n) R)) ↦
          (Subtype.mk (p := fun (x : SpecialLinearGroup n R) ↦
              Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) x)
              (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) (HSMul.hSMul (β := Matrix n n R) a 1) ⋯) ⋯ :
            ↥(center (SpecialLinearGroup n R))))
        (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card n) R) x)
          { val := a, inv := inv, val_inv := val_inv, inv_val := inv_val } ha)) =
    Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card n) R) x)
      { val := a, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ } ha

Tactic:
exact SetCoe.ext <| Units.ext <| by simp

Premises used: SetCoe.ext, Units.ext
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
i : n
A B : ↥(center (SpecialLinearGroup n R))
dsimp :
  rootsOfUnity.mkOfPowEq
      (((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) * (↑(↑B : SpecialLinearGroup n R) : Matrix n n R)) i i) ⋯ =
    HMul.hMul (α := ↥(rootsOfUnity (Fintype.card n) R))
      (rootsOfUnity.mkOfPowEq ((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i) ⋯)
      (rootsOfUnity.mkOfPowEq ((↑(↑B : SpecialLinearGroup n R) : Matrix n n R) i i) ⋯)
⊢ rootsOfUnity.mkOfPowEq ((↑(↑(A * B) : SpecialLinearGroup n R) : Matrix n n R) i i) ⋯ =
    HMul.hMul (α := ↥(rootsOfUnity (Fintype.card n) R))
      (rootsOfUnity.mkOfPowEq ((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i) ⋯)
      (rootsOfUnity.mkOfPowEq ((↑(↑B : SpecialLinearGroup n R) : Matrix n n R) i i) ⋯)

Tactic:
dsimp
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
i : n
A B : ↥(center (SpecialLinearGroup n R))
a :
  (↑(↑(rootsOfUnity.mkOfPowEq
              (((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) * (↑(↑B : SpecialLinearGroup n R) : Matrix n n R)) i i)
              ⋯) :
          Rˣ) :
      R) =
    (↑(↑(HMul.hMul (α := ↥(rootsOfUnity (Fintype.card n) R))
              (rootsOfUnity.mkOfPowEq ((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i) ⋯)
              (rootsOfUnity.mkOfPowEq ((↑(↑B : SpecialLinearGroup n R) : Matrix n n R) i i) ⋯)) :
          Rˣ) :
      R)
⊢ rootsOfUnity.mkOfPowEq
      (((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) * (↑(↑B : SpecialLinearGroup n R) : Matrix n n R)) i i) ⋯ =
    HMul.hMul (α := ↥(rootsOfUnity (Fintype.card n) R))
      (rootsOfUnity.mkOfPowEq ((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i) ⋯)
      (rootsOfUnity.mkOfPowEq ((↑(↑B : SpecialLinearGroup n R) : Matrix n n R) i i) ⋯)

Tactic:
ext