awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
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
⊢ 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
have neg : (↑(↑(↑(centerEquivRootsOfUnity_invFun r) : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
  HSMul.hSMul (β := V →ₗ[R] V) (↑(↑r : Rˣ) : R) LinearMap.id
Tactic: rw [← H.choose_spec.2]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (hypothesis)
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
⊢ 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))
          ⋯))
      ⋯
have hV₁ : Nontrivial V
Tactic: rw [not_subsingleton_iff_nontrivial] at hV
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (hypothesis)
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
⊢ 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))
          ⋯))
      ⋯
have this : FaithfulSMul R V
Tactic: have := Module.Free.instFaithfulSMulOfNontrivial R V
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
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 :=
  ⋯
⊢ 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))
          ⋯))
      ⋯
have neg : sorry.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: simp only [← Subtype.val_inj, ← Units.val_inj, IsUnit.unit_spec, Units.val_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
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
⊢ 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)
have 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
Tactic: apply FaithfulSMul.eq_of_smul_eq_smul (α := V)
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
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 :=
  ⋯
⊢ 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)
have 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
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
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))
⊢ (↑(↑(↑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
have 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)
        (sorry.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: 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
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))
⊢ (↑(↑(↑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
have pos : ∀ (hR : Subsingleton R), (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = LinearMap.id
Tactic: split_ifs with hR hV
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
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
⊢ (↑(↑(↑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
have pos₁ : ∀ (hR : ¬Subsingleton R) (hV : Subsingleton V),
  (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = LinearMap.id
Tactic: split_ifs with hR hV
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
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
⊢ (↑(↑(↑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
have neg : ∀ (hR : ¬Subsingleton R) (hV : ¬Subsingleton V),
  (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
    HSMul.hSMul (β := V →ₗ[R] V)
      (sorry.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
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (hypothesis)
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
⊢ (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) = LinearMap.id
have this : Subsingleton V
Tactic: have : Subsingleton V := Module.subsingleton R V
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (hypothesis)
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) =
    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
have hV₁ : Nontrivial V
Tactic: rw [not_subsingleton_iff_nontrivial] at hV
Cleared hypotheses: hV
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
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
⊢ (↑(↑(↑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
have neg : (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
  (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V)
Tactic: rw [← (mem_center_iff.mp g.prop).choose_spec.2]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
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 =
    ((↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : (a : V) → V) x
have 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
Tactic: rw [← LinearEquiv.coe_toLinearMap, centerEquivRootsOfUnity_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
r : ↥(rootsOfUnity n R)
hn : n = 1
⊢ (↑r : Rˣ) = 1
have h : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity n R) (↑r : Rˣ)
Tactic: have h := r.prop
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
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))
⊢ 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))
have rw : Eq.{u_1 + 1} (α := Rˣ)
  (↑((centerEquivRootsOfUnity :
          (a : ↥(Subgroup.center (SpecialLinearGroup R V))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
        g) :
    Rˣ)
  1
Tactic: rw [← Subtype.coe_inj, OneMemClass.coe_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
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))
⊢ Eq.{u_1 + 1} (α := Rˣ)
    (↑((centerEquivRootsOfUnity :
            (a : ↥(Subgroup.center (SpecialLinearGroup R V))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
          g) :
      Rˣ)
    1
have hn : max (Module.finrank R V) 1 = 1
Tactic: apply rootsOfUnity.eq_one
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
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))
⊢ max (Module.finrank R V) 1 = 1
have hn : Eq (α := ℕ) 1 1
Tactic: rw [Nat.max_eq_right d1]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
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)
⊢ (↑(↑(↑((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
have simp : HSMul.hSMul (β := V →ₗ[R] V) (↑(↑r : Rˣ) : R) LinearMap.id = 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (hypothesis)
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))
⊢ 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ˣ)
have a : Nontrivial R
Tactic: nontriviality R