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
g : ↥(Subgroup.center (SpecialLinearGroup R V))
⊢ centerEquivRootsOfUnity_invFun
      ((fun (g : ↥(Subgroup.center (SpecialLinearGroup R V))) ↦
          (⋯.by_cases (fun (x : Subsingleton R) ↦ 1) fun (hR : Nontrivial R) ↦
              ⋯.by_cases (fun (x : Subsingleton V) ↦ 1) fun (hV : Nontrivial V) ↦
                have hV : 1 ≤ Module.finrank R V := ⋯;
                have hr := ⋯;
                let r :=
                  ⋯.choose (p := fun (r : R) ↦
                    r ^ Module.finrank R V = 1 ∧
                      (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
                        HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id);
                have this : IsUnit r := ⋯;
                Subtype.mk (p := fun (x : Rˣ) ↦
                  Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x) this.unit ⋯ :
            ↥(rootsOfUnity (max (Module.finrank R V) 1) R)))
        g) =
    g
have simp : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V →ₗ[R] V)
    (↑(↑(sorry.by_cases (fun (x : Subsingleton R) ↦ 1) fun (hR : Nontrivial R) ↦
              sorry.by_cases (fun (x : Subsingleton V) ↦ 1) fun (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 :=
                    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))
                    sorry)
                  sorry) :
          Rˣ) :
      R)
    LinearMap.id =
  (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V)
Tactic: simp only [centerEquivRootsOfUnity_invFun, ← Subtype.val_inj,
      ← LinearEquiv.toLinearMap_inj, LinearMap.coe_equivOfIsUnitDet]
-- 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))
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V →ₗ[R] V)
      (↑(↑(⋯.by_cases (fun (x : Subsingleton R) ↦ 1) fun (hR : Nontrivial R) ↦
                ⋯.by_cases (fun (x : Subsingleton V) ↦ 1) fun (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) =
                            HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id))
                      ⋯)
                    ⋯) :
            Rˣ) :
        R)
      LinearMap.id =
    (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V)
have simp : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V →ₗ[R] V)
    (↑(↑(if h : Subsingleton R then 1
            else
              if h : Subsingleton V then 1
              else
                Subtype.mk (p := fun (x : Rˣ) ↦
                  Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x)
                  (IsUnit.unit (a :=
                    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))
                    sorry)
                  sorry) :
          Rˣ) :
      R)
    LinearMap.id =
  (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V)
Tactic: simp only [Or.by_cases]
-- 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))
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V →ₗ[R] V)
      (↑(↑(if h : Subsingleton R then 1
              else
                if h : Subsingleton V then 1
                else
                  Subtype.mk (p := fun (x : Rˣ) ↦
                    Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x)
                    (IsUnit.unit (a :=
                      ⋯.choose (p := fun (r : R) ↦
                        r ^ Module.finrank R V = 1 ∧
                          (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
                            HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id))
                      ⋯)
                    ⋯) :
            Rˣ) :
        R)
      LinearMap.id =
    (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V)
have pos : ∀ (hR : Subsingleton R),
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V →ₗ[R] V) (↑(↑1 : Rˣ) : R) LinearMap.id =
    (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V)
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),
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V →ₗ[R] V) (↑(↑1 : Rˣ) : R) LinearMap.id =
      (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V →ₗ[R] V)
      (↑(↑(if h : Subsingleton R then 1
              else
                if h : Subsingleton V then 1
                else
                  Subtype.mk (p := fun (x : Rˣ) ↦
                    Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x)
                    (IsUnit.unit (a :=
                      ⋯.choose (p := fun (r : R) ↦
                        r ^ Module.finrank R V = 1 ∧
                          (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
                            HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id))
                      ⋯)
                    ⋯) :
            Rˣ) :
        R)
      LinearMap.id =
    (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V)
have pos₁ : ∀ (hR : ¬Subsingleton R) (hV : Subsingleton V),
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V →ₗ[R] V) (↑(↑1 : Rˣ) : R) LinearMap.id =
    (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V)
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),
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V →ₗ[R] V) (↑(↑1 : Rˣ) : R) LinearMap.id =
      (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V)
pos₁ :
  ∀ (hR : ¬Subsingleton R) (hV : Subsingleton V),
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V →ₗ[R] V) (↑(↑1 : Rˣ) : R) LinearMap.id =
      (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V →ₗ[R] V)
      (↑(↑(if h : Subsingleton R then 1
              else
                if h : Subsingleton V then 1
                else
                  Subtype.mk (p := fun (x : Rˣ) ↦
                    Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x)
                    (IsUnit.unit (a :=
                      ⋯.choose (p := fun (r : R) ↦
                        r ^ Module.finrank R V = 1 ∧
                          (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) =
                            HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id))
                      ⋯)
                    ⋯) :
            Rˣ) :
        R)
      LinearMap.id =
    (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V)
have neg : ∀ (hR : ¬Subsingleton R) (hV : ¬Subsingleton V),
  HSMul.hSMul (β := V →ₗ[R] V)
      (↑(↑(Subtype.mk (p := fun (x : Rˣ) ↦
                Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x)
                (IsUnit.unit (a :=
                  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))
                  sorry)
                sorry) :
            Rˣ) :
        R)
      LinearMap.id =
    (↑(↑(↑g : SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V)
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
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
⊢ (if h : Subsingleton R then 1
    else
      if h : Subsingleton V then 1
      else
        Subtype.mk (p := fun (x : Rˣ) ↦
          Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x)
          (IsUnit.unit (a :=
            ⋯.choose (p := fun (r_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))
            ⋯)
          ⋯) =
    r
have pos : ∀ (hR : Subsingleton R), 1 = r
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
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
pos : ∀ (hR : Subsingleton R), 1 = r
⊢ (if h : Subsingleton R then 1
    else
      if h : Subsingleton V then 1
      else
        Subtype.mk (p := fun (x : Rˣ) ↦
          Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x)
          (IsUnit.unit (a :=
            ⋯.choose (p := fun (r_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))
            ⋯)
          ⋯) =
    r
have pos₁ : ∀ (hR : ¬Subsingleton R) (hV : Subsingleton V), 1 = r
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
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
pos : ∀ (hR : Subsingleton R), 1 = r
pos₁ : ∀ (hR : ¬Subsingleton R) (hV : Subsingleton V), 1 = r
⊢ (if h : Subsingleton R then 1
    else
      if h : Subsingleton V then 1
      else
        Subtype.mk (p := fun (x : Rˣ) ↦
          Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (max (Module.finrank R V) 1) R) x)
          (IsUnit.unit (a :=
            ⋯.choose (p := fun (r_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))
            ⋯)
          ⋯) =
    r
have neg : ∀ (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 :=
        sorry.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))
        sorry)
      sorry =
    r
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
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
hR : ¬Subsingleton R
hV : Subsingleton V
⊢ 1 = r
have hR₁ : Nontrivial R
Tactic: replace hR := not_subsingleton_iff_nontrivial.mp hR
Cleared hypotheses: hR
-- 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)
hV : Subsingleton V
hR : Nontrivial R
⊢ 1 = r
have pos : r = 1
Tactic: symm
-- 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
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
hV : Subsingleton V
hR : Nontrivial R
⊢ r = 1
have hV₁ : Module.finrank R V = 0
Tactic: rw [← Module.finrank_eq_zero_iff_of_free (R := R)] at hV
Cleared hypotheses: hV, hR
-- 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
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
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_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))
        ⋯)
      ⋯ =
    r
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
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
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_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))
        ⋯)
      ⋯ =
    r
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
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
hR : ¬Subsingleton R
hV_1 : ¬Subsingleton V
hV : Nontrivial V
this : FaithfulSMul R 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_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))
        ⋯)
      ⋯ =
    r
have neg : sorry.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) =
  (↑(↑r : Rˣ) : R)
Tactic: simp only [← Subtype.val_inj, ← Units.val_inj, IsUnit.unit_spec]
-- 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
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
hR : ¬Subsingleton R
hV_1 : ¬Subsingleton V
hV : Nontrivial V
this : FaithfulSMul R V
⊢ ⋯.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) =
    (↑(↑r : Rˣ) : R)
have 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
Tactic: have H := mem_center_iff.mp (Subtype.prop (centerEquivRootsOfUnity_invFun r))
-- 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_1 : 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
this :
  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
⊢ ⋯.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) =
    (↑(↑r : Rˣ) : R)
have apply : ∀ (a : V),
  sorry.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) •
      a =
    (↑(↑r : Rˣ) : R) • 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
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
hR : ¬Subsingleton R
hV_1 : ¬Subsingleton V
hV : Nontrivial V
this_1 : 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
this :
  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
x : V
⊢ ⋯.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) •
      x =
    (↑(↑r : Rˣ) : R) • x
have rw : ∀
  (this :
    ∀ (x : V),
      Eq (α := V)
        ((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 :
              (a : V) → V)
            x :
          V)
        ((HSMul.hSMul (β := V →ₗ[R] V) (↑(↑r : Rˣ) : R) LinearMap.id : (a : V) → V) x : V))
  (x : V),
  sorry.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) •
      x =
    (↑(↑r : Rˣ) : R) • x
Tactic: rw [LinearMap.ext_iff] at this
Cleared hypotheses: this, x
-- 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_1 : 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
this :
  ∀ (x : 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) •
        x =
      (↑(↑r : Rˣ) : R) • x
x : V
⊢ ⋯.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) •
      x =
    (↑(↑r : Rˣ) : R) • x
have rw : (↑(↑r : Rˣ) : R) • x = (↑(↑r : Rˣ) : R) • x
Tactic: rw [this x]
-- 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
⊢ ⋯.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) =
    (↑(↑r : Rˣ) : R)
have neg : 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
Tactic: suffices (H.choose • LinearMap.id : V →ₗ[R] V) = (r.val : R) • LinearMap.id by
        apply FaithfulSMul.eq_of_smul_eq_smul (α := V)
        intro x
        rw [LinearMap.ext_iff] at this
        simp only [LinearMap.smul_apply, LinearMap.id_coe, id_eq] at this
        rw [this x]