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
⊢ 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 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ˣ)
Tactic: by_cases hV : Subsingleton V
-- 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
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ˣ)
⊢ 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 : ∀ (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ˣ)
Tactic: by_cases hV : Subsingleton V
-- 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 : 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ˣ)
have 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
Tactic: convert! Eq.refl (1 : Rˣ)
-- 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_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
⊢ 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 h₁ : Eq.{u_4 + 1} (α := Rˣ)
  (↑((center_equiv_rootsOfUnity :
          (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
        g) :
    Rˣ)
  1
Tactic: convert! Eq.refl (1 : Rˣ)
-- 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 : 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ˣ)
    1
have h : max (Module.finrank R V) 1 = 1
Tactic: apply rootsOfUnity.eq_one
-- 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 : Subsingleton V
⊢ max (Module.finrank R V) 1 = 1
have hV₁ : Module.finrank R V = 0
Tactic: rw [← Module.finrank_eq_zero_iff_of_free (R := R)] at hV
Cleared hypotheses: hV
-- 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 : Subsingleton V
⊢ Eq.{u_4 + 1} (α := Rˣ)
    (↑((center_equiv_rootsOfUnity :
            (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
          g) :
      Rˣ)
    1
have h : max (Fintype.card ι) 1 = 1
Tactic: apply rootsOfUnity.eq_one
-- 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 : Subsingleton V
⊢ max (Fintype.card ι) 1 = 1
have hV₁ : Module.finrank R V = 0
Tactic: rw [← Module.finrank_eq_zero_iff_of_free (R := R)] at hV
Cleared hypotheses: hV
-- 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 : ¬Subsingleton V
hι : IsEmpty ι
⊢ Subsingleton V
have rw : Module.finrank R V = 0
Tactic: rw [← Module.finrank_eq_zero_iff_of_free (R := R),
        Module.finrank_eq_card_basis b, Fintype.card_of_isEmpty]
-- 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 : ¬Subsingleton V
hι : IsEmpty ι
rw : Module.finrank R V = 0
⊢ Subsingleton V
have rw₁ : Fintype.card ι = 0
Tactic: rw [← Module.finrank_eq_zero_iff_of_free (R := R),
        Module.finrank_eq_card_basis b, Fintype.card_of_isEmpty]
-- 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 : ¬Subsingleton V
hι : IsEmpty ι
rw : Module.finrank R V = 0
rw₁ : Fintype.card ι = 0
⊢ Subsingleton V
have rw₂ : Eq (α := ℕ) 0 0
Tactic: rw [← Module.finrank_eq_zero_iff_of_free (R := R),
        Module.finrank_eq_card_basis b, Fintype.card_of_isEmpty]
-- 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 : ¬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ˣ)
have hι : ¬IsEmpty ι
Tactic: have hι : ¬ IsEmpty ι := fun hι ↦ hV (by
      rw [← Module.finrank_eq_zero_iff_of_free (R := R),
        Module.finrank_eq_card_basis b, Fintype.card_of_isEmpty])
-- 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 : ¬Subsingleton V
hι : ¬IsEmpty ι
⊢ 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 hV₁ : Nontrivial V
Tactic: rw [not_subsingleton_iff_nontrivial] at hV
Cleared hypotheses: hV, hι
-- 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 ι
⊢ 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 this : FaithfulSMul R V
Tactic: have := Module.Free.instFaithfulSMulOfNontrivial R V
-- 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
this :
  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
⊢ 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 rw : 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ˣ) :
    R)
  (↑(↑((center_equiv_rootsOfUnity :
              (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
            g) :
        Rˣ) :
    R)
Tactic: rw [← Units.val_inj]
-- 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
this :
  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
⊢ 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ˣ) :
      R)
    (↑(↑((center_equiv_rootsOfUnity :
                (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
              g) :
          Rˣ) :
      R)
have apply : ∀ (a : V),
  HSMul.hSMul.{u_4, u_5, u_5} (α := R)
      (↑(↑((MulEquiv.trans (centerCongr (toLin_equiv b)) centerEquivRootsOfUnity :
                  (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
                g) :
            Rˣ) :
        R)
      a =
    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)
      a
Tactic: apply FaithfulSMul.eq_of_smul_eq_smul (α := V)
-- 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_1 : FaithfulSMul R V
this :
  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
x : V
⊢ HSMul.hSMul.{u_4, u_5, u_5} (α := R)
      (↑(↑((MulEquiv.trans (centerCongr (toLin_equiv b)) centerEquivRootsOfUnity :
                  (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(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 this₁ : ∀ (x : V),
  HSMul.hSMul.{u_4, u_5, u_5} (α := R)
      (↑(↑((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)
      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 [MulEquiv.trans_apply, LinearMap.ext_iff, LinearMap.smul_apply, LinearMap.id_coe,
        id_eq] at this
Cleared hypotheses: 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_1 : FaithfulSMul R V
x : V
this :
  ∀ (x : V),
    HSMul.hSMul.{u_4, u_5, u_5} (α := R)
        (↑(↑((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)
        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
⊢ HSMul.hSMul.{u_4, u_5, u_5} (α := R)
      (↑(↑((MulEquiv.trans (centerCongr (toLin_equiv b)) centerEquivRootsOfUnity :
                  (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(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 rw : HSMul.hSMul.{u_4, u_5, u_5} (α := R)
    (↑(↑((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)
    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 [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_1 : FaithfulSMul R V
x : V
this :
  ∀ (x : V),
    HSMul.hSMul.{u_4, u_5, u_5} (α := R)
        (↑(↑((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)
        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
rw :
  HSMul.hSMul.{u_4, u_5, u_5} (α := R)
      (↑(↑((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)
      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
⊢ HSMul.hSMul.{u_4, u_5, u_5} (α := R)
      (↑(↑((MulEquiv.trans (centerCongr (toLin_equiv b)) centerEquivRootsOfUnity :
                  (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(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 rw₁ : 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 =
  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 [MulEquiv.trans_apply, this]