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 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 :
  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
⊢ 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:
suffices (Hgh.choose • LinearMap.id : V →ₗ[R] V)
      = (Hg.choose • LinearMap.id) * (Hh.choose • LinearMap.id) by
      apply FaithfulSMul.eq_of_smul_eq_smul (α := V)
      intro x
      simp [mul_smul,
        ← mem_center_iff_spec (g * h).prop, ← mem_center_iff_spec h.prop,
        ← mem_center_iff_spec g.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
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 :=
  ⋯
⊢ 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

Tactic:
simp [← Hgh.choose_spec.2, ← Hh.choose_spec.2, ← Hg.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
g : ↥(Subgroup.center (SpecialLinearGroup R V))
simp :
  (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
    if Subsingleton R then LinearMap.id
    else
      if Subsingleton V then LinearMap.id
      else
        HSMul.hSMul (β := V →ₗ[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))
          LinearMap.id
⊢ (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(rootsOfUnity (max (Module.finrank R V) 1) R)) (β := V →ₗ[R] V)
      ((centerEquivRootsOfUnity :
            (a : ↥(Subgroup.center (SpecialLinearGroup R V))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
          g :
        ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
      LinearMap.id

Tactic:
simp only [centerEquivRootsOfUnity, Or.by_cases, MulEquiv.coe_mk, Equiv.coe_fn_mk,
    dite_smul, one_smul, Subgroup.mk_smul, Units.smul_isUnit, dite_eq_ite]

Premises used: Units.smul_isUnit, SpecialLinearGroup.centerEquivRootsOfUnity, MulEquiv.coe_mk, one_smul, Or.by_cases, Equiv.coe_fn_mk, dite_eq_ite, dite_smul, Subgroup.mk_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 : ↥(Subgroup.center (SpecialLinearGroup R V))
pos : ∀ (hR : Subsingleton R), (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = LinearMap.id
pos₁ :
  ∀ (hR : ¬Subsingleton R) (hV : Subsingleton V),
    (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = LinearMap.id
neg :
  ∀ (hR : ¬Subsingleton R) (hV : ¬Subsingleton V),
    (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
      HSMul.hSMul (β := V →ₗ[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))
        LinearMap.id
⊢ (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
    if Subsingleton R then LinearMap.id
    else
      if Subsingleton V then LinearMap.id
      else
        HSMul.hSMul (β := V →ₗ[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))
          LinearMap.id

Tactic:
split_ifs with hR 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 : Subsingleton R
⊢ Subsingleton V

Tactic:
have : Subsingleton V := Module.subsingleton 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 : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : Subsingleton R
this : Subsingleton V
⊢ (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = LinearMap.id

Tactic:
apply Subsingleton.eq_one

Premises used: Subsingleton.eq_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
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV : Subsingleton V
⊢ (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = LinearMap.id

Tactic:
apply Subsingleton.eq_one

Premises used: Subsingleton.eq_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
g : ↥(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 : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV : Nontrivial V
neg neg₁ :
  (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
    (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V)
⊢ (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
    HSMul.hSMul (β := V →ₗ[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))
      LinearMap.id

Tactic:
rw [← (mem_center_iff.mp g.prop).choose_spec.2]

Premises used: Exists.choose_spec, SpecialLinearGroup.mem_center_iff, And.right, 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 : ↥(Subgroup.center (SpecialLinearGroup R V))
x : V
simp :
  HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
      ((centerEquivRootsOfUnity :
            (a : ↥(Subgroup.center (SpecialLinearGroup R V))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
          g :
        ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
      x =
    ((↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : (a : V) → V) x
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
      ((centerEquivRootsOfUnity :
            (a : ↥(Subgroup.center (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 : SpecialLinearGroup R V) : V ≃ₗ[R] V) : (a : V) → V) x : V)) x

Tactic:
simp only
-- 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))
x : V
rw :
  HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
      ((centerEquivRootsOfUnity :
            (a : ↥(Subgroup.center (SpecialLinearGroup R V))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
          g :
        ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
      x =
    (HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(rootsOfUnity (max (Module.finrank R V) 1) R)) (β := V →ₗ[R] V)
          ((centerEquivRootsOfUnity :
                (a : ↥(Subgroup.center (SpecialLinearGroup R V))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
              g :
            ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
          LinearMap.id :
        (a : V) → V)
      x
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
      ((centerEquivRootsOfUnity :
            (a : ↥(Subgroup.center (SpecialLinearGroup R V))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
          g :
        ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
      x =
    ((↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : (a : V) → V) x

Tactic:
rw [← LinearEquiv.coe_toLinearMap, centerEquivRootsOfUnity_apply]

Premises used: SpecialLinearGroup.centerEquivRootsOfUnity_apply, LinearEquiv.coe_toLinearMap
-- 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))
x : V
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
      ((centerEquivRootsOfUnity :
            (a : ↥(Subgroup.center (SpecialLinearGroup R V))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
          g :
        ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
      x =
    (HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(rootsOfUnity (max (Module.finrank R V) 1) R)) (β := V →ₗ[R] V)
          ((centerEquivRootsOfUnity :
                (a : ↥(Subgroup.center (SpecialLinearGroup R V))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
              g :
            ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
          LinearMap.id :
        (a : V) → V)
      x

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
r : ↥(rootsOfUnity n R)
hn : n = 1
⊢ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity n R) (↑r : Rˣ)

Tactic:
have h := r.prop
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
r : ↥(rootsOfUnity n R)
hn : n = 1
h : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity n R) (↑r : Rˣ)
⊢ (↑r : Rˣ) = 1

Tactic:
simpa only [mem_rootsOfUnity, hn, pow_one] using h

Premises used: mem_rootsOfUnity, 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
d1 : Module.finrank R V ≤ 1
g : ↥(Subgroup.center (SpecialLinearGroup R V))
rw :
  Eq.{u_1 + 1} (α := Rˣ)
    (↑((centerEquivRootsOfUnity :
            (a : ↥(Subgroup.center (SpecialLinearGroup R V))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
          g) :
      Rˣ)
    1
⊢ Eq.{u_1 + 1} (α := ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
    ((centerEquivRootsOfUnity :
          (a : ↥(Subgroup.center (SpecialLinearGroup R V))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
        g :
      ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
    (1 : ↥(rootsOfUnity (max (Module.finrank R V) 1) R))

Tactic:
rw [← Subtype.coe_inj, OneMemClass.coe_one]

Premises used: OneMemClass.coe_one, Subtype.coe_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
d1 : Module.finrank R V ≤ 1
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hn : max (Module.finrank R V) 1 = 1
⊢ Eq.{u_1 + 1} (α := Rˣ)
    (↑((centerEquivRootsOfUnity :
            (a : ↥(Subgroup.center (SpecialLinearGroup R V))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
          g) :
      Rˣ)
    1

Tactic:
apply rootsOfUnity.eq_one

Premises used: rootsOfUnity.eq_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
d1 : Module.finrank R V ≤ 1
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hn hn₁ : Eq (α := ℕ) 1 1
⊢ max (Module.finrank R V) 1 = 1

Tactic:
rw [Nat.max_eq_right d1]

Premises used: Nat.max_eq_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)
simp : HSMul.hSMul (β := V →ₗ[R] V) (↑(↑r : Rˣ) : R) LinearMap.id = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id
⊢ (↑(↑(↑((MulEquiv.symm centerEquivRootsOfUnity :
                    (a : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)) → ↥(Subgroup.center (SpecialLinearGroup R V)))
                  r) :
              SpecialLinearGroup R V) :
          V ≃ₗ[R] V) :
      V →ₗ[R] V) =
    HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id

Tactic:
simp only [centerEquivRootsOfUnity, MulEquiv.symm_mk, MulEquiv.coe_mk, Equiv.coe_fn_symm_mk,
    centerEquivRootsOfUnity_invFun, LinearMap.coe_equivOfIsUnitDet]

Premises used: SpecialLinearGroup.centerEquivRootsOfUnity_invFun, MulEquiv.symm_mk, Equiv.coe_fn_symm_mk, SpecialLinearGroup.centerEquivRootsOfUnity, MulEquiv.coe_mk, 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)
⊢ HSMul.hSMul (β := V →ₗ[R] V) (↑(↑r : Rˣ) : R) LinearMap.id = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id

Tactic:
congr
-- 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))
⊢ Nontrivial R

Tactic:
nontriviality R
-- 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
pos :
  ∀ (hV : Subsingleton V),
    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ˣ)
neg :
  ∀ (hV : ¬Subsingleton V),
    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ˣ)
⊢ 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:
by_cases hV : Subsingleton V

Premises used: Subsingleton
-- 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
⊢ Eq.{u_4 + 1} (α := Rˣ) 1 1

Tactic:
Eq.refl (1 : Rˣ)

Premises used: Eq.refl, OfNat.ofNat
-- 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_1 : Nontrivial R
hV : Subsingleton V
h :
  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ˣ)
    1
h₁ :
  Eq.{u_4 + 1} (α := Rˣ)
    (↑((center_equiv_rootsOfUnity :
            (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
          g) :
      Rˣ)
    1
⊢ 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:
convert! Eq.refl (1 : Rˣ)

Premises used: Eq.refl, OfNat.ofNat
-- 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_1 : Nontrivial R
hV : Subsingleton V
h : max (Module.finrank R V) 1 = 1
⊢ 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ˣ)
    1

Tactic:
apply rootsOfUnity.eq_one

Premises used: rootsOfUnity.eq_one
-- 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
⊢ Module.finrank R V = 0

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

Premises used: Module.finrank_eq_zero_iff_of_free
-- 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 : Module.finrank R V = 0
⊢ max (Module.finrank R V) 1 = 1

Tactic:
simp only [hV, sup_eq_right, zero_le_one, ← Module.finrank_eq_card_basis b]

Premises used: Module.finrank_eq_card_basis, zero_le_one, sup_eq_right
-- 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_1 : Nontrivial R
hV : Subsingleton V
h : max (Fintype.card ι) 1 = 1
⊢ Eq.{u_4 + 1} (α := Rˣ)
    (↑((center_equiv_rootsOfUnity :
            (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
          g) :
      Rˣ)
    1

Tactic:
apply rootsOfUnity.eq_one

Premises used: rootsOfUnity.eq_one
-- 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 : Module.finrank R V = 0
⊢ max (Fintype.card ι) 1 = 1

Tactic:
simp only [hV, sup_eq_right, zero_le_one, ← Module.finrank_eq_card_basis b]

Premises used: Module.finrank_eq_card_basis, zero_le_one, sup_eq_right
-- 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 ι
rw : Module.finrank R V = 0
rw₁ : Fintype.card ι = 0
rw₂ rw₃ : Eq (α := ℕ) 0 0
⊢ Subsingleton V

Tactic:
rw [← Module.finrank_eq_zero_iff_of_free (R := R),
        Module.finrank_eq_card_basis b, Fintype.card_of_isEmpty]

Premises used: Fintype.card_of_isEmpty, Module.finrank_eq_card_basis, Module.finrank_eq_zero_iff_of_free