awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
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 : Nontrivial V
hι : ¬IsEmpty ι
this : FaithfulSMul R 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ˣ)
have neg : HSMul.hSMul.{u_4, u_5, u_5} (α := R) (β := V →ₗ[R] V)
    (↑(↑((MulEquiv.trans (centerCongr (toLin_equiv b)) centerEquivRootsOfUnity :
                (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
              g) :
          Rˣ) :
      R)
    LinearMap.id =
  HSMul.hSMul.{u_4, u_5, u_5} (α := R) (β := V →ₗ[R] V)
    (↑(↑((center_equiv_rootsOfUnity :
                (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
              g) :
          Rˣ) :
      R)
    LinearMap.id
Tactic: suffices (((((Subgroup.centerCongr (Matrix.SpecialLinearGroup.toLin_equiv b)).trans
      centerEquivRootsOfUnity g).val : R) • LinearMap.id) : V →ₗ[R] V) =
        ((Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity g).val : R) • LinearMap.id by
      rw [← Units.val_inj]
      apply FaithfulSMul.eq_of_smul_eq_smul (α := V)
      intro x
      simp only [MulEquiv.trans_apply, LinearMap.ext_iff, LinearMap.smul_apply, LinearMap.id_coe,
        id_eq] at this
      rw [MulEquiv.trans_apply, this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
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 : Nontrivial V
hι : ¬IsEmpty ι
this : FaithfulSMul R V
⊢ HSMul.hSMul.{u_4, u_5, u_5} (α := R) (β := V →ₗ[R] V)
      (↑(↑((MulEquiv.trans (centerCongr (toLin_equiv b)) centerEquivRootsOfUnity :
                  (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
                g) :
            Rˣ) :
        R)
      LinearMap.id =
    HSMul.hSMul.{u_4, u_5, u_5} (α := R) (β := V →ₗ[R] V)
      (↑(↑((center_equiv_rootsOfUnity :
                  (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
                g) :
            Rˣ) :
        R)
      LinearMap.id
have neg : HSMul.hSMul.{u_4, u_5, u_5} (α := R) (β := V →ₗ[R] V)
    (↑(↑((centerEquivRootsOfUnity :
                (a : ↥(center (_root_.SpecialLinearGroup R V))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
              ((centerCongr (toLin_equiv b) :
                  (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(center (_root_.SpecialLinearGroup R V)))
                g)) :
          Rˣ) :
      R)
    LinearMap.id =
  HSMul.hSMul.{u_4, u_5, u_5} (α := R) (β := V →ₗ[R] V)
    (↑(↑((center_equiv_rootsOfUnity :
                (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
              g) :
          Rˣ) :
      R)
    LinearMap.id
Tactic: simp only [MulEquiv.trans_apply]
-- 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))
h : Nontrivial R
hV : Nontrivial V
hι : ¬IsEmpty ι
this : FaithfulSMul R V
⊢ HSMul.hSMul.{u_4, u_5, u_5} (α := R) (β := V →ₗ[R] V)
      (↑(↑((centerEquivRootsOfUnity :
                  (a : ↥(center (_root_.SpecialLinearGroup R V))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
                ((centerCongr (toLin_equiv b) :
                    (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(center (_root_.SpecialLinearGroup R V)))
                  g)) :
            Rˣ) :
        R)
      LinearMap.id =
    HSMul.hSMul.{u_4, u_5, u_5} (α := R) (β := V →ₗ[R] V)
      (↑(↑((center_equiv_rootsOfUnity :
                  (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
                g) :
            Rˣ) :
        R)
      LinearMap.id
have hgg' : Eq.{u_5 + 1} (α := _root_.SpecialLinearGroup R V)
  ((↑((centerCongr (toLin_equiv b) :
            (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(center (_root_.SpecialLinearGroup R V)))
          g) :
      _root_.SpecialLinearGroup R V) :
    _root_.SpecialLinearGroup R V)
  ((toLin_equiv b : (a : Matrix.SpecialLinearGroup ι R) → _root_.SpecialLinearGroup R V)
      (↑g : Matrix.SpecialLinearGroup ι R) :
    _root_.SpecialLinearGroup R V)
Tactic: have hgg' := Subgroup.centerCongr_apply_coe (Matrix.SpecialLinearGroup.toLin_equiv b) g
-- 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))
h : Nontrivial R
hV : Nontrivial V
hι : ¬IsEmpty ι
this : FaithfulSMul R V
hgg' :
  Eq.{u_5 + 1} (α := _root_.SpecialLinearGroup R V)
    ((↑((centerCongr (toLin_equiv b) :
              (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(center (_root_.SpecialLinearGroup R V)))
            g) :
        _root_.SpecialLinearGroup R V) :
      _root_.SpecialLinearGroup R V)
    ((toLin_equiv b : (a : Matrix.SpecialLinearGroup ι R) → _root_.SpecialLinearGroup R V)
        (↑g : Matrix.SpecialLinearGroup ι R) :
      _root_.SpecialLinearGroup R V)
⊢ HSMul.hSMul.{u_4, u_5, u_5} (α := R) (β := V →ₗ[R] V)
      (↑(↑((centerEquivRootsOfUnity :
                  (a : ↥(center (_root_.SpecialLinearGroup R V))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
                ((centerCongr (toLin_equiv b) :
                    (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(center (_root_.SpecialLinearGroup R V)))
                  g)) :
            Rˣ) :
        R)
      LinearMap.id =
    HSMul.hSMul.{u_4, u_5, u_5} (α := R) (β := V →ₗ[R] V)
      (↑(↑((center_equiv_rootsOfUnity :
                  (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
                g) :
            Rˣ) :
        R)
      LinearMap.id
have hgg'₁ : ∀ (x : V),
  Eq (α := V)
    (((↑(↑(↑((centerCongr (toLin_equiv b) :
                          (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(center (_root_.SpecialLinearGroup R V)))
                        g) :
                    _root_.SpecialLinearGroup R V) :
                V ≃ₗ[R] V) :
            V →ₗ[R] V) :
          (a : V) → V)
        x :
      V)
    (((↑(↑((toLin_equiv b : (a : Matrix.SpecialLinearGroup ι R) → _root_.SpecialLinearGroup R V)
                    (↑g : Matrix.SpecialLinearGroup ι R)) :
                V ≃ₗ[R] V) :
            V →ₗ[R] V) :
          (a : V) → V)
        x :
      V)
Tactic: rw [← Subtype.coe_inj, ← LinearEquiv.toLinearMap_inj, LinearMap.ext_iff] at hgg'
Cleared hypotheses: hgg'
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
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 : Nontrivial V
hι : ¬IsEmpty ι
this : FaithfulSMul R V
hgg' :
  ∀ (x : V),
    Eq (α := V)
      (((↑(↑(↑((centerCongr (toLin_equiv b) :
                            (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(center (_root_.SpecialLinearGroup R V)))
                          g) :
                      _root_.SpecialLinearGroup R V) :
                  V ≃ₗ[R] V) :
              V →ₗ[R] V) :
            (a : V) → V)
          x :
        V)
      (((↑(↑((toLin_equiv b : (a : Matrix.SpecialLinearGroup ι R) → _root_.SpecialLinearGroup R V)
                      (↑g : Matrix.SpecialLinearGroup ι R)) :
                  V ≃ₗ[R] V) :
              V →ₗ[R] V) :
            (a : V) → V)
          x :
        V)
⊢ HSMul.hSMul.{u_4, u_5, u_5} (α := R) (β := V →ₗ[R] V)
      (↑(↑((centerEquivRootsOfUnity :
                  (a : ↥(center (_root_.SpecialLinearGroup R V))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
                ((centerCongr (toLin_equiv b) :
                    (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(center (_root_.SpecialLinearGroup R V)))
                  g)) :
            Rˣ) :
        R)
      LinearMap.id =
    HSMul.hSMul.{u_4, u_5, u_5} (α := R) (β := V →ₗ[R] V)
      (↑(↑((center_equiv_rootsOfUnity :
                  (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
                g) :
            Rˣ) :
        R)
      LinearMap.id
have neg : let g' : ↥(center (_root_.SpecialLinearGroup R V)) :=
  (centerCongr (toLin_equiv b) :
      (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(center (_root_.SpecialLinearGroup R V)))
    g;
∀
  (hgg' :
    ∀ (x : V),
      Eq (α := V) (((↑(↑(↑g' : _root_.SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) : (a : V) → V) x : V)
        (((↑(↑((toLin_equiv b : (a : Matrix.SpecialLinearGroup ι R) → _root_.SpecialLinearGroup R V)
                        (↑g : Matrix.SpecialLinearGroup ι R)) :
                    V ≃ₗ[R] V) :
                V →ₗ[R] V) :
              (a : V) → V)
            x :
          V)),
  HSMul.hSMul.{u_4, u_5, u_5} (α := R) (β := V →ₗ[R] V)
      (↑(↑((centerEquivRootsOfUnity :
                  (a : ↥(center (_root_.SpecialLinearGroup R V))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
                g') :
            Rˣ) :
        R)
      LinearMap.id =
    HSMul.hSMul.{u_4, u_5, u_5} (α := R) (β := V →ₗ[R] V)
      (↑(↑((center_equiv_rootsOfUnity :
                  (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
                g) :
            Rˣ) :
        R)
      LinearMap.id
Tactic: set g' := ((Subgroup.centerCongr (Matrix.SpecialLinearGroup.toLin_equiv b)) g)
Cleared hypotheses: hgg'
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
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 : Nontrivial V
hι : ¬IsEmpty ι
this : FaithfulSMul R V
g' : ↥(center (_root_.SpecialLinearGroup R V)) :=
  (centerCongr (toLin_equiv b) :
      (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(center (_root_.SpecialLinearGroup R V)))
    g
hgg' :
  ∀ (x : V),
    Eq (α := V) (((↑(↑(↑g' : _root_.SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) : (a : V) → V) x : V)
      (((↑(↑((toLin_equiv b : (a : Matrix.SpecialLinearGroup ι R) → _root_.SpecialLinearGroup R V)
                      (↑g : Matrix.SpecialLinearGroup ι R)) :
                  V ≃ₗ[R] V) :
              V →ₗ[R] V) :
            (a : V) → V)
          x :
        V)
⊢ HSMul.hSMul.{u_4, u_5, u_5} (α := R) (β := V →ₗ[R] V)
      (↑(↑((centerEquivRootsOfUnity :
                  (a : ↥(center (_root_.SpecialLinearGroup R V))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
                g') :
            Rˣ) :
        R)
      LinearMap.id =
    HSMul.hSMul.{u_4, u_5, u_5} (α := R) (β := V →ₗ[R] V)
      (↑(↑((center_equiv_rootsOfUnity :
                  (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
                g) :
            Rˣ) :
        R)
      LinearMap.id
have neg : ∀ (x : V),
  Eq (α := V)
    ((HSMul.hSMul.{u_4, u_5, u_5} (α := R) (β := V →ₗ[R] V)
            (↑(↑((centerEquivRootsOfUnity :
                        (a : ↥(center (_root_.SpecialLinearGroup R V))) →
                          ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
                      g') :
                  Rˣ) :
              R)
            LinearMap.id :
          (a : V) → V)
        x :
      V)
    ((HSMul.hSMul.{u_4, u_5, u_5} (α := R) (β := V →ₗ[R] V)
            (↑(↑((center_equiv_rootsOfUnity :
                        (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
                      g) :
                  Rˣ) :
              R)
            LinearMap.id :
          (a : V) → V)
        x :
      V)
Tactic: ext x
-- 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))
h : Nontrivial R
hV : Nontrivial V
hι : ¬IsEmpty ι
this : FaithfulSMul R V
g' : ↥(center (_root_.SpecialLinearGroup R V)) :=
  (centerCongr (toLin_equiv b) :
      (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(center (_root_.SpecialLinearGroup R V)))
    g
hgg' :
  ∀ (x : V),
    Eq (α := V) (((↑(↑(↑g' : _root_.SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) : (a : V) → V) x : V)
      (((↑(↑((toLin_equiv b : (a : Matrix.SpecialLinearGroup ι R) → _root_.SpecialLinearGroup R V)
                      (↑g : Matrix.SpecialLinearGroup ι R)) :
                  V ≃ₗ[R] V) :
              V →ₗ[R] V) :
            (a : V) → V)
          x :
        V)
x : V
⊢ Eq (α := V)
    ((HSMul.hSMul.{u_4, u_5, u_5} (α := R) (β := V →ₗ[R] V)
            (↑(↑((centerEquivRootsOfUnity :
                        (a : ↥(center (_root_.SpecialLinearGroup R V))) →
                          ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
                      g') :
                  Rˣ) :
              R)
            LinearMap.id :
          (a : V) → V)
        x :
      V)
    ((HSMul.hSMul.{u_4, u_5, u_5} (α := R) (β := V →ₗ[R] V)
            (↑(↑((center_equiv_rootsOfUnity :
                        (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
                      g) :
                  Rˣ) :
              R)
            LinearMap.id :
          (a : V) → V)
        x :
      V)
have this₁ : HSMul.hSMul.{u_4, u_5, u_5} (α := ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
    ((centerEquivRootsOfUnity :
          (a : ↥(center (_root_.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' : _root_.SpecialLinearGroup R V) : V ≃ₗ[R] V) : (a : V) → V) x : V)) x
Tactic: have := centerEquivRootsOfUnity_apply_apply g' x
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
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 : Nontrivial V
hι : ¬IsEmpty ι
this_1 : FaithfulSMul R V
g' : ↥(center (_root_.SpecialLinearGroup R V)) :=
  (centerCongr (toLin_equiv b) :
      (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(center (_root_.SpecialLinearGroup R V)))
    g
hgg' :
  ∀ (x : V),
    Eq (α := V) (((↑(↑(↑g' : _root_.SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) : (a : V) → V) x : V)
      (((↑(↑((toLin_equiv b : (a : Matrix.SpecialLinearGroup ι R) → _root_.SpecialLinearGroup R V)
                      (↑g : Matrix.SpecialLinearGroup ι R)) :
                  V ≃ₗ[R] V) :
              V →ₗ[R] V) :
            (a : V) → V)
          x :
        V)
x : V
this :
  HSMul.hSMul.{u_4, u_5, u_5} (α := R)
      (↑(↑((centerEquivRootsOfUnity :
                  (a : ↥(center (_root_.SpecialLinearGroup R V))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
                g') :
            Rˣ) :
        R)
      x =
    ((↑(↑g' : _root_.SpecialLinearGroup R V) : V ≃ₗ[R] V) : (a : V) → V) x
⊢ Eq (α := V)
    ((HSMul.hSMul.{u_4, u_5, u_5} (α := R) (β := V →ₗ[R] V)
            (↑(↑((centerEquivRootsOfUnity :
                        (a : ↥(center (_root_.SpecialLinearGroup R V))) →
                          ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
                      g') :
                  Rˣ) :
              R)
            LinearMap.id :
          (a : V) → V)
        x :
      V)
    ((HSMul.hSMul.{u_4, u_5, u_5} (α := R) (β := V →ₗ[R] V)
            (↑(↑((center_equiv_rootsOfUnity :
                        (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
                      g) :
                  Rˣ) :
              R)
            LinearMap.id :
          (a : V) → V)
        x :
      V)
have neg : HSMul.hSMul.{u_4, u_5, u_5} (α := R)
    (↑(↑((centerEquivRootsOfUnity :
                (a : ↥(center (_root_.SpecialLinearGroup R V))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
              g') :
          Rˣ) :
      R)
    x =
  HSMul.hSMul.{u_4, u_5, u_5} (α := R)
    (↑(↑((center_equiv_rootsOfUnity :
                (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
              g) :
          Rˣ) :
      R)
    x
Tactic: simp only [LinearMap.smul_apply, LinearMap.id_coe, id_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
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 : Nontrivial V
hι : ¬IsEmpty ι
this_1 : FaithfulSMul R V
g' : ↥(center (_root_.SpecialLinearGroup R V)) :=
  (centerCongr (toLin_equiv b) :
      (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(center (_root_.SpecialLinearGroup R V)))
    g
hgg' :
  ∀ (x : V),
    Eq (α := V) (((↑(↑(↑g' : _root_.SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) : (a : V) → V) x : V)
      (((↑(↑((toLin_equiv b : (a : Matrix.SpecialLinearGroup ι R) → _root_.SpecialLinearGroup R V)
                      (↑g : Matrix.SpecialLinearGroup ι R)) :
                  V ≃ₗ[R] V) :
              V →ₗ[R] V) :
            (a : V) → V)
          x :
        V)
x : V
this :
  HSMul.hSMul.{u_4, u_5, u_5} (α := R)
      (↑(↑((centerEquivRootsOfUnity :
                  (a : ↥(center (_root_.SpecialLinearGroup R V))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
                g') :
            Rˣ) :
        R)
      x =
    ((↑(↑g' : _root_.SpecialLinearGroup R V) : V ≃ₗ[R] V) : (a : V) → V) x
⊢ HSMul.hSMul.{u_4, u_5, u_5} (α := R)
      (↑(↑((centerEquivRootsOfUnity :
                  (a : ↥(center (_root_.SpecialLinearGroup R V))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
                g') :
            Rˣ) :
        R)
      x =
    HSMul.hSMul.{u_4, u_5, u_5} (α := R)
      (↑(↑((center_equiv_rootsOfUnity :
                  (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
                g) :
            Rˣ) :
        R)
      x
have neg : (HSMul.hSMul.{u_4, u_5, u_5} (α := R) (β := V →ₗ[R] V)
        (↑(↑((center_equiv_rootsOfUnity :
                    (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
                  g) :
              Rˣ) :
          R)
        LinearMap.id :
      (a : V) → V)
    x =
  HSMul.hSMul.{u_4, u_5, u_5} (α := R)
    (↑(↑((center_equiv_rootsOfUnity :
                (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
              g) :
          Rˣ) :
      R)
    x
Tactic: rw [this, ← LinearEquiv.coe_toLinearMap, hgg',
      Matrix.SpecialLinearGroup.toLin_equiv.toLinearMap_eq,
      Matrix.SpecialLinearGroup.eq_scalar_center_equiv_rootsOfUnity g,
      Matrix.toLin_scalar]
-- Lean 4 proof step from Mathlib.LinearAlgebra.StdBasis (goal)
Goal:
ι : Type u_7
R : Type u_8
inst : Semiring R
inst_1 : DecidableEq ι
⊢ LinearIndependent R (M := (j : ι) → R) fun (i : ι) ↦ single (M := fun (i : ι) ↦ R) i 1
have rw : LinearIndependent (ι := (_ : ι) × PUnit.{1}) R (M := (j : ι) → R)
  ((fun (i : ι) ↦ single (M := fun (i : ι) ↦ R) i 1) ∘ (⇑(Equiv.sigmaPUnit ι) : (a : (_ : ι) × PUnit.{1}) → ι))
Tactic: rw [← linearIndependent_equiv (Equiv.sigmaPUnit ι)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.StdBasis (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
inst_5 : DecidableEq ι
v : ι → M
hv : ∀ (i : ι), v i ≠ 0
⊢ LinearIndependent R (M := (j : ι) → M) fun (i : ι) ↦ single (M := fun (i : ι) ↦ M) i (v i)
have rw : LinearIndependent (ι := (_ : ι) × PUnit.{1}) R (M := (j : ι) → M)
  ((fun (i : ι) ↦ single (M := fun (i : ι) ↦ M) i (v i)) ∘ (⇑(Equiv.sigmaPUnit ι) : (a : (_ : ι) × PUnit.{1}) → ι))
Tactic: rw [← linearIndependent_equiv (Equiv.sigmaPUnit ι)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.StdBasis (goal)
Goal:
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst : Semiring R
inst_1 : (i : η) → AddCommMonoid (Ms i)
inst_2 : (i : η) → Module.{u_2, u_6} R (Ms i)
inst_3 : Fintype η
inst_4 : DecidableEq η
s : (j : η) → Basis.{u_5, u_2, u_6} (ιs j) R (Ms j)
j : η
i : ιs j
⊢ Eq (α := (j : η) × ιs j →₀ R)
    (((Pi.basis (ιs := ιs) (Ms := Ms) s).repr : (a : (j : η) → Ms j) → (j : η) × ιs j →₀ R)
        (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) :
      (j : η) × ιs j →₀ R)
    (Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (j : η) × ιs j →₀ R)
have h : ∀ (j' : η) (i' : ιs j'),
  Eq.{u_2 + 1} (α := R)
    (((((Pi.basis (ιs := ιs) (Ms := Ms) s).repr : (a : (j : η) → Ms j) → (j : η) × ιs j →₀ R)
              (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) :
            (j : η) × ιs j →₀ R) :
          (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
      R)
    ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
      R)
Tactic: ext ⟨j', i'⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.StdBasis (goal)
Goal:
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst : Semiring R
inst_1 : (i : η) → AddCommMonoid (Ms i)
inst_2 : (i : η) → Module.{u_2, u_6} R (Ms i)
inst_3 : Fintype η
inst_4 : DecidableEq η
s : (j : η) → Basis.{u_5, u_2, u_6} (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
⊢ Eq.{u_2 + 1} (α := R)
    (((((Pi.basis (ιs := ιs) (Ms := Ms) s).repr : (a : (j : η) → Ms j) → (j : η) × ιs j →₀ R)
              (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) :
            (j : η) × ιs j →₀ R) :
          (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
      R)
    ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
      R)
have pos : ∀ (hj : j = j'),
  Eq.{u_2 + 1} (α := R)
    (((((Pi.basis (ιs := ιs) (Ms := Ms) s).repr : (a : (j : η) → Ms j) → (j : η) × ιs j →₀ R)
              (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) :
            (j : η) × ιs j →₀ R) :
          (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
      R)
    ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
      R)
Tactic: by_cases hj : j = j'