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
g : SpecialLinearGroup R V
hR : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
this_1 : Fintype (Module.Free.ChooseBasisIndex R V) := Module.Free.ChooseBasisIndex.fintype R V
e : SpecialLinearGroup R V ≃* Matrix.SpecialLinearGroup.{u_2, u_1} (Module.Free.ChooseBasisIndex R V) R :=
  MulEquiv.symm (Matrix.SpecialLinearGroup.toLin_equiv b)
r : R
hr : r ^ Fintype.card.{u_2} (Module.Free.ChooseBasisIndex R V) = 1
this :
  Eq (α := Matrix.{u_2, u_2, u_1} (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
    (↑((MulEquiv.symm (Matrix.SpecialLinearGroup.toLin_equiv b) :
            (a : SpecialLinearGroup R V) → Matrix.SpecialLinearGroup (Module.Free.ChooseBasisIndex R V) R)
          g) :
      Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
    ((Matrix.of :
        (a : Module.Free.ChooseBasisIndex R V → Module.Free.ChooseBasisIndex R V → R) →
          Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
      fun (i j : Module.Free.ChooseBasisIndex R V) ↦
      ((b.repr : (a : V) → Module.Free.ChooseBasisIndex R V →₀ R)
            ((fun (x : V) ↦ (((↑g : V ≃ₗ[R] V) : (a : V) → V) x : V))
              ((b : (a : Module.Free.ChooseBasisIndex R V) → V) j)) :
          (a : Module.Free.ChooseBasisIndex R V) → R)
        i)
i j : Module.Free.ChooseBasisIndex R V
⊢ Eq.{u_1 + 1} (α := R) (Matrix.diagonal (fun (x : Module.Free.ChooseBasisIndex R V) ↦ r) i j : R)
      ((((b.repr : (a : V) → Module.Free.ChooseBasisIndex R V →₀ R)
                (((↑g : V ≃ₗ[R] V) : (a : V) → V) ((b : (a : Module.Free.ChooseBasisIndex R V) → V) j : V)) :
              Finsupp.{u_2, u_1} (Module.Free.ChooseBasisIndex R V) R) :
            (a : Module.Free.ChooseBasisIndex R V) → R)
          i :
        R) ↔
    Eq.{u_1 + 1} (α := R)
      ((LinearMap.toMatrix b b :
            (a : V →ₗ[R] V) → Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
          (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) i j :
        R)
      ((LinearMap.toMatrix b b :
            (a : V →ₗ[R] V) → Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
          (HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id) i j :
        R)

Tactic:
simp [Matrix.diagonal, LinearMap.toMatrix_apply,
      Finsupp.single, Pi.single_apply, Iff.symm eq_comm]

Premises used: Pi.single_apply, eq_comm, Iff.symm, Matrix.diagonal, LinearMap.toMatrix_apply, Finsupp.single
-- 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 : SpecialLinearGroup R V
hR : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
this : Fintype (Module.Free.ChooseBasisIndex R V) := Module.Free.ChooseBasisIndex.fintype R V
e : SpecialLinearGroup R V ≃* Matrix.SpecialLinearGroup.{u_2, u_1} (Module.Free.ChooseBasisIndex R V) R :=
  MulEquiv.symm (Matrix.SpecialLinearGroup.toLin_equiv b)
r : R
hr : r ^ Fintype.card.{u_2} (Module.Free.ChooseBasisIndex R V) = 1
inr :
  Eq (α := Matrix.{u_2, u_2, u_1} (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
    (↑((MulEquiv.symm (Matrix.SpecialLinearGroup.toLin_equiv b) :
            (a : SpecialLinearGroup R V) → Matrix.SpecialLinearGroup (Module.Free.ChooseBasisIndex R V) R)
          g) :
      Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
    ((Matrix.of :
        (a : Module.Free.ChooseBasisIndex R V → Module.Free.ChooseBasisIndex R V → R) →
          Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
      fun (i j : Module.Free.ChooseBasisIndex R V) ↦
      ((b.repr : (a : V) → Module.Free.ChooseBasisIndex R V →₀ R)
            ((fun (x : V) ↦ (((↑g : V ≃ₗ[R] V) : (a : V) → V) x : V))
              ((b : (a : Module.Free.ChooseBasisIndex R V) → V) j)) :
          (a : Module.Free.ChooseBasisIndex R V) → R)
        i)
⊢ Eq (α := Matrix.{u_2, u_2, u_1} (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
      (Matrix.diagonal fun (x : Module.Free.ChooseBasisIndex R V) ↦ r)
      (↑((MulEquiv.symm (Matrix.SpecialLinearGroup.toLin_equiv b) :
              (a : SpecialLinearGroup R V) → Matrix.SpecialLinearGroup (Module.Free.ChooseBasisIndex R V) R)
            g) :
        Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R) ↔
    (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id

Tactic:
suffices ((Matrix.SpecialLinearGroup.toLin_equiv b).symm g) =
    Matrix.of fun i j ↦ (b.repr (g (b j))) i by
    simp only [this]
    rw [← (LinearMap.toMatrix b b).injective.eq_iff]
    simp only [← Matrix.ext_iff, Matrix.of_apply]
    apply forall₂_congr
    intro i j
    simp [Matrix.diagonal, LinearMap.toMatrix_apply,
      Finsupp.single, Pi.single_apply, Iff.symm eq_comm]
-- 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 : SpecialLinearGroup R V
hR : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
this : Fintype (Module.Free.ChooseBasisIndex R V) := Module.Free.ChooseBasisIndex.fintype R V
e : SpecialLinearGroup R V ≃* Matrix.SpecialLinearGroup.{u_2, u_1} (Module.Free.ChooseBasisIndex R V) R :=
  MulEquiv.symm (Matrix.SpecialLinearGroup.toLin_equiv b)
r : R
hr : r ^ Fintype.card.{u_2} (Module.Free.ChooseBasisIndex R V) = 1
inr :
  ∀ (i j : Module.Free.ChooseBasisIndex R V),
    Eq.{u_1 + 1} (α := R)
      ((↑((MulEquiv.symm (Matrix.SpecialLinearGroup.toLin_equiv b) :
                  (a : SpecialLinearGroup R V) → Matrix.SpecialLinearGroup (Module.Free.ChooseBasisIndex R V) R)
                g) :
            Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
          i j :
        R)
      ((Matrix.of :
            (a : Module.Free.ChooseBasisIndex R V → Module.Free.ChooseBasisIndex R V → R) →
              Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
          (fun (i j : Module.Free.ChooseBasisIndex R V) ↦
            ((b.repr : (a : V) → Module.Free.ChooseBasisIndex R V →₀ R)
                  ((fun (x : V) ↦ (((↑g : V ≃ₗ[R] V) : (a : V) → V) x : V))
                    ((b : (a : Module.Free.ChooseBasisIndex R V) → V) j)) :
                (a : Module.Free.ChooseBasisIndex R V) → R)
              i)
          i j :
        R)
⊢ Eq (α := Matrix.{u_2, u_2, u_1} (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
    (↑((MulEquiv.symm (Matrix.SpecialLinearGroup.toLin_equiv b) :
            (a : SpecialLinearGroup R V) → Matrix.SpecialLinearGroup (Module.Free.ChooseBasisIndex R V) R)
          g) :
      Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
    ((Matrix.of :
        (a : Module.Free.ChooseBasisIndex R V → Module.Free.ChooseBasisIndex R V → R) →
          Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
      fun (i j : Module.Free.ChooseBasisIndex R V) ↦
      ((b.repr : (a : V) → Module.Free.ChooseBasisIndex R V →₀ R)
            ((fun (x : V) ↦ (((↑g : V ≃ₗ[R] V) : (a : V) → V) x : V))
              ((b : (a : Module.Free.ChooseBasisIndex R V) → V) j)) :
          (a : Module.Free.ChooseBasisIndex R V) → R)
        i)

Tactic:
ext
-- 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 : SpecialLinearGroup R V
hR : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
this : Fintype (Module.Free.ChooseBasisIndex R V) := Module.Free.ChooseBasisIndex.fintype R V
e : SpecialLinearGroup R V ≃* Matrix.SpecialLinearGroup.{u_2, u_1} (Module.Free.ChooseBasisIndex R V) R :=
  MulEquiv.symm (Matrix.SpecialLinearGroup.toLin_equiv b)
r : R
hr : r ^ Fintype.card.{u_2} (Module.Free.ChooseBasisIndex R V) = 1
i j : Module.Free.ChooseBasisIndex R V
⊢ Eq.{u_1 + 1} (α := R)
    ((↑((MulEquiv.symm (Matrix.SpecialLinearGroup.toLin_equiv b) :
                (a : SpecialLinearGroup R V) → Matrix.SpecialLinearGroup (Module.Free.ChooseBasisIndex R V) R)
              g) :
          Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
        i j :
      R)
    ((Matrix.of :
          (a : Module.Free.ChooseBasisIndex R V → Module.Free.ChooseBasisIndex R V → R) →
            Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
        (fun (i j : Module.Free.ChooseBasisIndex R V) ↦
          ((b.repr : (a : V) → Module.Free.ChooseBasisIndex R V →₀ R)
                ((fun (x : V) ↦ (((↑g : V ≃ₗ[R] V) : (a : V) → V) x : V))
                  ((b : (a : Module.Free.ChooseBasisIndex R V) → V) j)) :
              (a : Module.Free.ChooseBasisIndex R V) → R)
            i)
        i j :
      R)

Tactic:
simp [Matrix.SpecialLinearGroup.toLin_equiv.symm_toLinearMap_eq, LinearMap.toMatrix_apply]

Premises used: Matrix.SpecialLinearGroup.toLin_equiv.symm_toLinearMap_eq, LinearMap.toMatrix_apply
-- 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 : SpecialLinearGroup R V
hg : Membership.mem (γ := Subgroup (SpecialLinearGroup R V)) (Subgroup.center (SpecialLinearGroup R V)) g
x : V
H : (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) =
  HSMul.hSMul (β := V →ₗ[R] V)
    (⋯.choose (p := fun (r : R) ↦
      r ^ Module.finrank R V = 1 ∧ (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id))
    LinearMap.id :=
  ⋯
⊢ ∀ (x : V),
    Eq (α := V) (((↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) : (a : V) → V) x : V)
      ((HSMul.hSMul (β := V →ₗ[R] V)
              (⋯.choose (p := fun (r : R) ↦
                r ^ Module.finrank R V = 1 ∧
                  (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id))
              LinearMap.id :
            (a : V) → V)
          x :
        V)

Tactic:
rw [LinearMap.ext_iff] at H

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
g : SpecialLinearGroup R V
hg : Membership.mem (γ := Subgroup (SpecialLinearGroup R V)) (Subgroup.center (SpecialLinearGroup R V)) g
x : V
H :
  ∀ (x : V),
    Eq (α := V) (((↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) : (a : V) → V) x : V)
      ((HSMul.hSMul (β := V →ₗ[R] V)
              (⋯.choose (p := fun (r : R) ↦
                r ^ Module.finrank R V = 1 ∧
                  (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id))
              LinearMap.id :
            (a : V) → V)
          x :
        V)
⊢ ((↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) : (a : V) → V) x =
    ⋯.choose (p := fun (r : R) ↦
        r ^ Module.finrank R V = 1 ∧ (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id) •
      x

Tactic:
simp [H]
-- 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)
⊢ IsUnit.{u_1} (M := R)
    ((LinearMap.det : (a : V →ₗ[R] V) → R) (HSMul.hSMul (β := V →ₗ[R] V) (↑(↑r : Rˣ) : R) LinearMap.id) : R)

Tactic:
simp [LinearMap.det_smul, IsUnit.pow]

Premises used: IsUnit.pow, LinearMap.det_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
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
simp : (↑(↑r : Rˣ) : R) ^ Module.finrank R V = 1
⊢ Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) (LinearMap.equivOfIsUnitDet ⋯) : Rˣ) (1 : Rˣ)

Tactic:
simp only [← Units.val_inj, LinearEquiv.coe_det, LinearMap.coe_equivOfIsUnitDet,
      LinearMap.det_smul, LinearMap.det_id, mul_one, Units.val_one]

Premises used: Units.val_inj, LinearMap.det_id, LinearMap.coe_equivOfIsUnitDet, LinearMap.det_smul, Units.val_one, mul_one, LinearEquiv.coe_det
-- 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)
⊢ (↑(↑r : Rˣ) : R) ^ max (Module.finrank R V) 1 = 1

Tactic:
have := (mem_rootsOfUnity' _ _).mp r.prop
-- 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)
this : (↑(↑r : Rˣ) : R) ^ max (Module.finrank R V) 1 = 1
inl :
  ∀ (h : max (Module.finrank R V) 1 = Module.finrank R V) (h' : 1 ≤ Module.finrank R V),
    (↑(↑r : Rˣ) : R) ^ Module.finrank R V = 1
inr : ∀ (h : max (Module.finrank R V) 1 = 1) (h' : Module.finrank R V < 1), (↑(↑r : Rˣ) : R) ^ Module.finrank R V = 1
⊢ (↑(↑r : Rˣ) : R) ^ Module.finrank R V = 1

Tactic:
rcases max_cases (Module.finrank R V) 1 with ⟨h, h'⟩ |  ⟨h, h'⟩

Premises used: max_cases, OfNat.ofNat, Module.finrank
-- 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)
this : (↑(↑r : Rˣ) : R) ^ max (Module.finrank R V) 1 = 1
h : max (Module.finrank R V) 1 = Module.finrank R V
h' : 1 ≤ Module.finrank R V
⊢ (↑(↑r : Rˣ) : R) ^ Module.finrank R V = 1

Tactic:
simp_rw [h] at this
-- 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)
h : max (Module.finrank R V) 1 = Module.finrank R V
h' : 1 ≤ Module.finrank R V
this : (↑(↑r : Rˣ) : R) ^ Module.finrank R V = 1
⊢ (↑(↑r : Rˣ) : R) ^ Module.finrank R V = 1

Tactic:
this
-- 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)
h : max (Module.finrank R V) 1 = Module.finrank R V
h' : 1 ≤ Module.finrank R V
this : (↑(↑r : Rˣ) : R) ^ Module.finrank R V = 1
⊢ (↑(↑r : Rˣ) : R) ^ Module.finrank R V = 1

Tactic:
exact this
-- 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)
this : (↑(↑r : Rˣ) : R) ^ max (Module.finrank R V) 1 = 1
h : max (Module.finrank R V) 1 = 1
h' : Module.finrank R V < 1
⊢ (↑(↑r : Rˣ) : R) = 1

Tactic:
simp_rw [h, pow_one] at this

Premises used: pow_one
-- 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)
h : max (Module.finrank R V) 1 = 1
h' : Module.finrank R V < 1
this : (↑(↑r : Rˣ) : R) = 1
⊢ (↑(↑r : Rˣ) : R) ^ Module.finrank R V = 1

Tactic:
simp [this]
-- 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)
simp :
  ∃ (r_1 : R),
    r_1 ^ Module.finrank R V = 1 ∧
      HSMul.hSMul (β := V →ₗ[R] V) (↑(↑r : Rˣ) : R) LinearMap.id = HSMul.hSMul (β := V →ₗ[R] V) r_1 LinearMap.id
⊢ Membership.mem (γ := Subgroup (SpecialLinearGroup R V)) (Subgroup.center (SpecialLinearGroup R V))
    (Subtype.mk (p := fun (u : V ≃ₗ[R] V) ↦
      Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) u : Rˣ) (1 : Rˣ)) (LinearMap.equivOfIsUnitDet ⋯)
      ⋯)

Tactic:
simp only [mem_center_iff, LinearMap.coe_equivOfIsUnitDet]

Premises used: SpecialLinearGroup.mem_center_iff, LinearMap.coe_equivOfIsUnitDet
-- 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)
h :
  (↑(↑r : Rˣ) : R) ^ Module.finrank R V = 1 ∧
    HSMul.hSMul (β := V →ₗ[R] V) (↑(↑r : Rˣ) : R) LinearMap.id =
      HSMul.hSMul (β := V →ₗ[R] V) (↑(↑r : Rˣ) : R) LinearMap.id
⊢ ∃ (r_1 : R),
    r_1 ^ Module.finrank R V = 1 ∧
      HSMul.hSMul (β := V →ₗ[R] V) (↑(↑r : Rˣ) : R) LinearMap.id = HSMul.hSMul (β := V →ₗ[R] V) r_1 LinearMap.id

Tactic:
use r.val

Premises used: Subtype.val
-- 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)
h : (↑(↑r : Rˣ) : R) ^ Module.finrank R V = 1
⊢ (↑(↑r : Rˣ) : R) ^ Module.finrank R V = 1 ∧
    HSMul.hSMul (β := V →ₗ[R] V) (↑(↑r : Rˣ) : R) LinearMap.id =
      HSMul.hSMul (β := V →ₗ[R] V) (↑(↑r : Rˣ) : R) LinearMap.id

Tactic:
simp only [and_true]

Premises used: and_true
-- 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)
h :
  ∀ (r : Rˣ) (hr : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) r),
    (↑(↑(Subtype.mk (p := fun (x : Rˣ) ↦
                  Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x) r hr) :
              Rˣ) :
          R) ^
        Module.finrank R V =
      1
⊢ (↑(↑r : Rˣ) : R) ^ Module.finrank R V = 1

Tactic:
let ⟨r, hr⟩ := r
-- 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_1 : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
r : Rˣ
hr : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) r
pos :
  ∀ (hV : Module.finrank R V = 0),
    (↑(↑(Subtype.mk (p := fun (x : Rˣ) ↦
                  Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x) r hr) :
              Rˣ) :
          R) ^
        Module.finrank R V =
      1
neg :
  ∀ (hV : ¬Module.finrank R V = 0),
    (↑(↑(Subtype.mk (p := fun (x : Rˣ) ↦
                  Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x) r hr) :
              Rˣ) :
          R) ^
        Module.finrank R V =
      1
⊢ (↑(↑(Subtype.mk (p := fun (x : Rˣ) ↦
                Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x) r hr) :
            Rˣ) :
        R) ^
      Module.finrank R V =
    1

Tactic:
by_cases hV : Module.finrank R V = 0

Premises used: Module.finrank
-- 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_1 : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
r : Rˣ
hr : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) r
hV : Module.finrank R V = 0
⊢ (↑(↑(Subtype.mk (p := fun (x : Rˣ) ↦
                Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x) r hr) :
            Rˣ) :
        R) ^
      Module.finrank R V =
    1

Tactic:
simp [hV]
-- 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_1 : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
r : Rˣ
hr : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) r
hV : ¬Module.finrank R V = 0
⊢ 1 ≤ Module.finrank R V

Tactic:
rw [← ne_eq, ← Nat.one_le_iff_ne_zero] at hV

Premises used: ne_eq, Nat.one_le_iff_ne_zero
-- 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_1 : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
r : Rˣ
hr : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) r
hV : 1 ≤ Module.finrank R V
⊢ (↑r : R) ^ Module.finrank R V = 1

Tactic:
rw [mem_rootsOfUnity', max_eq_left hV] at hr

Premises used: max_eq_left, mem_rootsOfUnity'
-- 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_1 : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
r : Rˣ
hr : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) r
hV : 1 ≤ Module.finrank R V
hr₁ : (↑r : R) ^ Module.finrank R V = 1
⊢ 1 ≤ Module.finrank R V

Tactic:
rw [mem_rootsOfUnity', max_eq_left hV] at hr

Premises used: max_eq_left, mem_rootsOfUnity'
-- 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_1 : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
r : Rˣ
hr_1 : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) r
hr : (↑r : R) ^ Module.finrank R V = 1
hV : 1 ≤ Module.finrank R V
⊢ (↑(↑(Subtype.mk (p := fun (x : Rˣ) ↦
                Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x) r hr_1) :
            Rˣ) :
        R) ^
      Module.finrank R V =
    1

Tactic:
simpa [← Subtype.val_inj, ← Units.val_inj]

Premises used: Subtype.val_inj, Units.val_inj
-- 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 : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : Nontrivial R
hV : Nontrivial V
⊢ 0 < Module.finrank R V

Tactic:
rw [← Module.finrank_pos_iff_of_free (R := R)] at hV

Premises used: Module.finrank_pos_iff_of_free
-- 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 : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : Nontrivial R
hV : 0 < Module.finrank R V
⊢ 1 ≤ Module.finrank R V

Tactic:
replace hV : 1 ≤ Module.finrank R V := hV
-- 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 : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : Nontrivial R
hV : 1 ≤ Module.finrank R V
⊢ ⋯.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) ^
      Module.finrank R V =
    1

Tactic:
have hr := (mem_center_iff.mp g.prop).choose_spec.1