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
u : LinearMap.GeneralLinearGroup R V
v : SpecialLinearGroup R V
hv : (toGeneralLinearGroup : (a : SpecialLinearGroup R V) → LinearMap.GeneralLinearGroup R V) v = u
⊢ Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) u.toLinearEquiv : Rˣ) (1 : Rˣ)
have mp : Eq.{u_1 + 1} (α := Rˣ)
  ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) ((toLinearEquiv : (a : SpecialLinearGroup R V) → V ≃ₗ[R] V) v) : Rˣ)
  (1 : Rˣ)
Tactic: rw [← hv, toGeneralLinearGroup_toLinearEquiv_apply]
-- 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
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : Module.Free R V
inst_6 : Module.Finite R V
g : SpecialLinearGroup R V
⊢ Eq.{u_3 + 1} (α := Sˣ)
    (((LinearEquiv.det (R := S) (M := S ⊗[R] V) : (S ⊗[R] V ≃ₗ[S] S ⊗[R] V) →* Sˣ) : (a : S ⊗[R] V ≃ₗ[S] S ⊗[R] V) → Sˣ)
        (LinearEquiv.baseChange R S V V (↑g : V ≃ₗ[R] V)) :
      Sˣ)
    (1 : Sˣ)
have rw : Eq.{u_3 + 1} (α := Sˣ)
  (((Units.map (↑(algebraMap R S) : R →* S) : MonoidHom.{u_1, u_3} Rˣ Sˣ) : (a : Rˣ) → Sˣ)
      ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) (↑g : V ≃ₗ[R] V)) :
    Sˣ)
  (1 : Sˣ)
Tactic: rw [LinearEquiv.det_baseChange, g.prop, map_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
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : Module.Free R V
inst_6 : Module.Finite R V
g : SpecialLinearGroup R V
rw :
  Eq.{u_3 + 1} (α := Sˣ)
    (((Units.map (↑(algebraMap R S) : R →* S) : MonoidHom.{u_1, u_3} Rˣ Sˣ) : (a : Rˣ) → Sˣ)
        ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) (↑g : V ≃ₗ[R] V)) :
      Sˣ)
    (1 : Sˣ)
⊢ Eq.{u_3 + 1} (α := Sˣ)
    (((LinearEquiv.det (R := S) (M := S ⊗[R] V) : (S ⊗[R] V ≃ₗ[S] S ⊗[R] V) →* Sˣ) : (a : S ⊗[R] V ≃ₗ[S] S ⊗[R] V) → Sˣ)
        (LinearEquiv.baseChange R S V V (↑g : V ≃ₗ[R] V)) :
      Sˣ)
    (1 : Sˣ)
have rw₁ : Eq.{u_3 + 1} (α := Sˣ) (((Units.map (↑(algebraMap R S) : R →* S) : MonoidHom.{u_1, u_3} Rˣ Sˣ) : (a : Rˣ) → Sˣ) 1) 1
Tactic: rw [LinearEquiv.det_baseChange, g.prop, map_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
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : Module.Free R V
inst_6 : Module.Finite R V
g : SpecialLinearGroup R V
rw :
  Eq.{u_3 + 1} (α := Sˣ)
    (((Units.map (↑(algebraMap R S) : R →* S) : MonoidHom.{u_1, u_3} Rˣ Sˣ) : (a : Rˣ) → Sˣ)
        ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) (↑g : V ≃ₗ[R] V)) :
      Sˣ)
    (1 : Sˣ)
rw₁ :
  Eq.{u_3 + 1} (α := Sˣ) (((Units.map (↑(algebraMap R S) : R →* S) : MonoidHom.{u_1, u_3} Rˣ Sˣ) : (a : Rˣ) → Sˣ) 1) 1
⊢ Eq.{u_3 + 1} (α := Sˣ)
    (((LinearEquiv.det (R := S) (M := S ⊗[R] V) : (S ⊗[R] V ≃ₗ[S] S ⊗[R] V) →* Sˣ) : (a : S ⊗[R] V ≃ₗ[S] S ⊗[R] V) → Sˣ)
        (LinearEquiv.baseChange R S V V (↑g : V ≃ₗ[R] V)) :
      Sˣ)
    (1 : Sˣ)
have rw₂ : Eq.{u_3 + 1} (α := Sˣ) 1 1
Tactic: rw [LinearEquiv.det_baseChange, g.prop, map_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
W : Type u_3
X : Type u_4
inst_3 : AddCommGroup W
inst_4 : Module R W
inst_5 : AddCommGroup X
inst_6 : Module R X
e : V ≃ₗ[R] W
g : SpecialLinearGroup R W
⊢ Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) (e ≪≫ₗ (↑g : W ≃ₗ[R] W) ≪≫ₗ e.symm) : Rˣ) (1 : Rˣ)
have nth_rewrite : Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) (e.symm.symm ≪≫ₗ (↑g : W ≃ₗ[R] W) ≪≫ₗ e.symm) : Rˣ)
  (1 : Rˣ)
Tactic: nth_rewrite 1 [← LinearEquiv.symm_symm e]
-- 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
W : Type u_3
X : Type u_4
inst_3 : AddCommGroup W
inst_4 : Module R W
inst_5 : AddCommGroup X
inst_6 : Module R X
e : V ≃ₗ[R] W
g : SpecialLinearGroup R W
⊢ Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) (e.symm.symm ≪≫ₗ (↑g : W ≃ₗ[R] W) ≪≫ₗ e.symm) : Rˣ)
    (1 : Rˣ)
have rw : Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : W ≃ₗ[R] W) → Rˣ) (↑g : W ≃ₗ[R] W) : Rˣ) (1 : Rˣ)
Tactic: rw [LinearEquiv.det_conj g e.symm, 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
W : Type u_3
X : Type u_4
inst_3 : AddCommGroup W
inst_4 : Module R W
inst_5 : AddCommGroup X
inst_6 : Module R X
e : V ≃ₗ[R] W
g : SpecialLinearGroup R W
rw : Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : W ≃ₗ[R] W) → Rˣ) (↑g : W ≃ₗ[R] W) : Rˣ) (1 : Rˣ)
⊢ Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) (e.symm.symm ≪≫ₗ (↑g : W ≃ₗ[R] W) ≪≫ₗ e.symm) : Rˣ)
    (1 : Rˣ)
have rw₁ : Eq.{u_1 + 1} (α := Rˣ) 1 1
Tactic: rw [LinearEquiv.det_conj g e.symm, 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
n : Type u_3
inst_3 : Fintype n
inst_4 : DecidableEq n
b : Module.Basis n R V
A : SpecialLinearGroup n R
⊢ Eq (α := Matrix n n R)
    ((fun (a : { A : Matrix n n R // A.det = 1 }) ↦ (↑a : Matrix n n R))
      ((fun (u : _root_.SpecialLinearGroup R (n → R)) ↦
          (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1)
              ((LinearMap.toMatrix' : (a : (n → R) →ₗ[R] n → R) → Matrix n n R)
                (↑(↑u : (n → R) ≃ₗ[R] n → R) : (n → R) →ₗ[R] n → R))
              ⋯ :
            { A : Matrix n n R // A.det = 1 }))
        ((fun (A : SpecialLinearGroup n R) ↦
            (Subtype.mk (p := fun (u : (n → R) ≃ₗ[R] n → R) ↦
                Eq.{u_1 + 1} (α := Rˣ)
                  (((LinearEquiv.det (R := R) (M := n → R) : ((n → R) ≃ₗ[R] n → R) →* Rˣ) :
                        (a : (n → R) ≃ₗ[R] n → R) → Rˣ)
                      u :
                    Rˣ)
                  (1 : Rˣ))
                ((toLin' : (a : SpecialLinearGroup n R) → (n → R) ≃ₗ[R] n → R) A) ⋯ :
              { u : (n → R) ≃ₗ[R] n → R //
                Eq.{u_1 + 1} (α := Rˣ)
                  (((LinearEquiv.det (R := R) (M := n → R) : ((n → R) ≃ₗ[R] n → R) →* Rˣ) :
                        (a : (n → R) ≃ₗ[R] n → R) → Rˣ)
                      u :
                    Rˣ)
                  (1 : Rˣ) }))
          A)))
    ((fun (a : { A : Matrix n n R // A.det = 1 }) ↦ (↑a : Matrix n n R)) A)
have rw : Eq (α := (n → R) →ₗ[R] n → R)
  (↑(↑((fun (A : SpecialLinearGroup n R) ↦
              (Subtype.mk (p := fun (u : (n → R) ≃ₗ[R] n → R) ↦
                  Eq.{u_1 + 1} (α := Rˣ)
                    (((LinearEquiv.det (R := R) (M := n → R) : ((n → R) ≃ₗ[R] n → R) →* Rˣ) :
                          (a : (n → R) ≃ₗ[R] n → R) → Rˣ)
                        u :
                      Rˣ)
                    (1 : Rˣ))
                  ((toLin' : (a : SpecialLinearGroup n R) → (n → R) ≃ₗ[R] n → R) A) sorry :
                { u : (n → R) ≃ₗ[R] n → R //
                  Eq.{u_1 + 1} (α := Rˣ)
                    (((LinearEquiv.det (R := R) (M := n → R) : ((n → R) ≃ₗ[R] n → R) →* Rˣ) :
                          (a : (n → R) ≃ₗ[R] n → R) → Rˣ)
                        u :
                      Rˣ)
                    (1 : Rˣ) }))
            A) :
        (n → R) ≃ₗ[R] n → R) :
    (n → R) →ₗ[R] n → R)
  ((LinearEquiv.symm LinearMap.toMatrix' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R)
    ((fun (a : { A : Matrix n n R // A.det = 1 }) ↦ (↑a : Matrix n n R)) A))
Tactic: rw [← LinearEquiv.eq_symm_apply, LinearMap.toMatrix'_symm,
      Matrix.SpecialLinearGroup.toLin'_to_linearMap]
-- 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
h : Module.finrank R V ≤ 1
⊢ Eq.{u_2 + 1} (α := Subgroup (SpecialLinearGroup R V)) (Subgroup.center (SpecialLinearGroup R V)) ⊥
have a : Nontrivial R
Tactic: nontriviality 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
h : Module.finrank R V ≤ 1
h_1 : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
⊢ Subsingleton.{u_2 + 1} (Module.Free.ChooseBasisIndex R V)
have rwa : Nat.card.{u_2} (Module.Free.ChooseBasisIndex R V) ≤ 1
Tactic: rwa [← Finite.card_le_one_iff_subsingleton,
      Nat.card_eq_fintype_card, ← Module.finrank_eq_card_basis b]
-- 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
h : Module.finrank R V ≤ 1
h_1 : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
rwa : Nat.card.{u_2} (Module.Free.ChooseBasisIndex R V) ≤ 1
⊢ Subsingleton.{u_2 + 1} (Module.Free.ChooseBasisIndex R V)
have rwa₁ : Fintype.card.{u_2} (Module.Free.ChooseBasisIndex R V) ≤ 1
Tactic: rwa [← Finite.card_le_one_iff_subsingleton,
      Nat.card_eq_fintype_card, ← Module.finrank_eq_card_basis b]
-- 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
h : Module.finrank R V ≤ 1
h_1 : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
⊢ Eq.{u_2 + 1} (α := Subgroup (SpecialLinearGroup R V)) (Subgroup.center (SpecialLinearGroup R V)) ⊥
have this : Subsingleton.{u_2 + 1} (Module.Free.ChooseBasisIndex R V)
Tactic: have : Subsingleton (Module.Free.ChooseBasisIndex R V) := by
    rwa [← Finite.card_le_one_iff_subsingleton,
      Nat.card_eq_fintype_card, ← Module.finrank_eq_card_basis b]
-- 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
h : Module.finrank R V ≤ 1
h_1 : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
this : Subsingleton.{u_2 + 1} (Module.Free.ChooseBasisIndex R V)
⊢ Eq.{u_2 + 1} (α := Subgroup (SpecialLinearGroup R V)) (Subgroup.center (SpecialLinearGroup R V)) ⊥
have this₁ : Subsingleton ↥(Subgroup.center (Matrix.SpecialLinearGroup.{u_2, u_1} (Module.Free.ChooseBasisIndex R V) R))
Tactic: have : Subsingleton (Subgroup.center
    (Matrix.SpecialLinearGroup (Module.Free.ChooseBasisIndex R V) R)) := by
    infer_instance
-- 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
h : Module.finrank R V ≤ 1
h_1 : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
this_1 : Subsingleton.{u_2 + 1} (Module.Free.ChooseBasisIndex R V)
this : Subsingleton ↥(Subgroup.center (Matrix.SpecialLinearGroup.{u_2, u_1} (Module.Free.ChooseBasisIndex R V) R))
⊢ Eq.{u_2 + 1} (α := Subgroup (SpecialLinearGroup R V)) (Subgroup.center (SpecialLinearGroup R V)) ⊥
have this₁ : Subsingleton.{u_2 + 1} ↥(Subgroup.center (SpecialLinearGroup R V))
Tactic: rw [Equiv.subsingleton_congr
    (Subgroup.centerCongr (Matrix.SpecialLinearGroup.toLin_equiv b)).toEquiv] at this
Cleared hypotheses: this
-- 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 : SpecialLinearGroup R V
⊢ Membership.mem (γ := Subgroup (SpecialLinearGroup R V)) (Subgroup.center (SpecialLinearGroup R V)) g ↔
    ∃ (r : R),
      r ^ Module.finrank R V = 1 ∧ (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id
have inl : ∀ (hR : Subsingleton R),
  Membership.mem (γ := Subgroup (SpecialLinearGroup R V)) (Subgroup.center (SpecialLinearGroup R V)) g ↔
    ∃ (r : R),
      r ^ Module.finrank R V = 1 ∧ (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id
Tactic: rcases subsingleton_or_nontrivial R with hR | 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
g : SpecialLinearGroup R V
inl :
  ∀ (hR : Subsingleton R),
    Membership.mem (γ := Subgroup (SpecialLinearGroup R V)) (Subgroup.center (SpecialLinearGroup R V)) g ↔
      ∃ (r : R),
        r ^ Module.finrank R V = 1 ∧ (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id
⊢ Membership.mem (γ := Subgroup (SpecialLinearGroup R V)) (Subgroup.center (SpecialLinearGroup R V)) g ↔
    ∃ (r : R),
      r ^ Module.finrank R V = 1 ∧ (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id
have inr : ∀ (hR : Nontrivial R),
  Membership.mem (γ := Subgroup (SpecialLinearGroup R V)) (Subgroup.center (SpecialLinearGroup R V)) g ↔
    ∃ (r : R),
      r ^ Module.finrank R V = 1 ∧ (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id
Tactic: rcases subsingleton_or_nontrivial R with hR | 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
g : SpecialLinearGroup R V
hR : Subsingleton R
⊢ Membership.mem (γ := Subgroup (SpecialLinearGroup R V)) (Subgroup.center (SpecialLinearGroup R V)) g ↔
    ∃ (r : R),
      r ^ Module.finrank R V = 1 ∧ (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id
have this : Subsingleton.{u_2 + 1} (SpecialLinearGroup R V)
Tactic: have : Subsingleton (SpecialLinearGroup R V) := inferInstance
-- 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 : SpecialLinearGroup R V
hR : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
this : Fintype (Module.Free.ChooseBasisIndex R V) := Module.Free.ChooseBasisIndex.fintype R V
⊢ Membership.mem (γ := Subgroup (SpecialLinearGroup R V)) (Subgroup.center (SpecialLinearGroup R V)) g ↔
    ∃ (r : R),
      r ^ Module.finrank R V = 1 ∧ (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id
have inr : Membership.mem (γ := Subgroup (SpecialLinearGroup R V)) (Subgroup.center (SpecialLinearGroup R V)) g ↔
  ∃ (r : R),
    r ^ Fintype.card.{u_2} (Module.Free.ChooseBasisIndex R V) = 1 ∧
      (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id
Tactic: rw [Module.finrank_eq_card_basis b]
-- 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 : SpecialLinearGroup R V
hR : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
this : Fintype (Module.Free.ChooseBasisIndex R V) := Module.Free.ChooseBasisIndex.fintype R V
e : SpecialLinearGroup R V ≃* Matrix.SpecialLinearGroup.{u_2, u_1} (Module.Free.ChooseBasisIndex R V) R :=
  MulEquiv.symm (Matrix.SpecialLinearGroup.toLin_equiv b)
⊢ Membership.mem (γ := Subgroup (SpecialLinearGroup R V)) (Subgroup.center (SpecialLinearGroup R V)) g ↔
    ∃ (r : R),
      r ^ Fintype.card.{u_2} (Module.Free.ChooseBasisIndex R V) = 1 ∧
        (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id
have inr : Membership.mem (α := Matrix.SpecialLinearGroup.{u_2, u_1} (Module.Free.ChooseBasisIndex R V) R) (γ :=
    Subgroup (Matrix.SpecialLinearGroup.{u_2, u_1} (Module.Free.ChooseBasisIndex R V) R))
    (Subgroup.center (Matrix.SpecialLinearGroup.{u_2, u_1} (Module.Free.ChooseBasisIndex R V) R))
    ((e : (a : SpecialLinearGroup R V) → Matrix.SpecialLinearGroup (Module.Free.ChooseBasisIndex R V) R) g :
      Matrix.SpecialLinearGroup.{u_2, u_1} (Module.Free.ChooseBasisIndex R V) R) ↔
  ∃ (r : R),
    r ^ Fintype.card.{u_2} (Module.Free.ChooseBasisIndex R V) = 1 ∧
      (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id
Tactic: rw [← show e g ∈ Subgroup.center _ ↔ g ∈ Subgroup.center _ from
    MulEquivClass.apply_mem_center_iff e]
-- 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 : SpecialLinearGroup R V
hR : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
this : Fintype (Module.Free.ChooseBasisIndex R V) := Module.Free.ChooseBasisIndex.fintype R V
e : SpecialLinearGroup R V ≃* Matrix.SpecialLinearGroup.{u_2, u_1} (Module.Free.ChooseBasisIndex R V) R :=
  MulEquiv.symm (Matrix.SpecialLinearGroup.toLin_equiv b)
⊢ Membership.mem (α := Matrix.SpecialLinearGroup.{u_2, u_1} (Module.Free.ChooseBasisIndex R V) R) (γ :=
      Subgroup (Matrix.SpecialLinearGroup.{u_2, u_1} (Module.Free.ChooseBasisIndex R V) R))
      (Subgroup.center (Matrix.SpecialLinearGroup.{u_2, u_1} (Module.Free.ChooseBasisIndex R V) R))
      ((e : (a : SpecialLinearGroup R V) → Matrix.SpecialLinearGroup (Module.Free.ChooseBasisIndex R V) R) g :
        Matrix.SpecialLinearGroup.{u_2, u_1} (Module.Free.ChooseBasisIndex R V) R) ↔
    ∃ (r : R),
      r ^ Fintype.card.{u_2} (Module.Free.ChooseBasisIndex R V) = 1 ∧
        (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id
have inr : (∃ (r : R),
    r ^ Fintype.card.{u_2} (Module.Free.ChooseBasisIndex R V) = 1 ∧
      Eq (α := Matrix.{u_2, u_2, u_1} (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
        ((Matrix.scalar (Module.Free.ChooseBasisIndex R V) :
              (a : R) → Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
            r :
          Matrix.{u_2, u_2, u_1} (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
        ((↑((e : (a : SpecialLinearGroup R V) → Matrix.SpecialLinearGroup (Module.Free.ChooseBasisIndex R V) R) g) :
            Matrix.{u_2, u_2, u_1} (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R) :
          Matrix.{u_2, u_2, u_1} (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)) ↔
  ∃ (r : R),
    r ^ Fintype.card.{u_2} (Module.Free.ChooseBasisIndex R V) = 1 ∧
      (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id
Tactic: rw [Matrix.SpecialLinearGroup.mem_center_iff]
-- 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 : SpecialLinearGroup R V
hR : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
this : Fintype (Module.Free.ChooseBasisIndex R V) := Module.Free.ChooseBasisIndex.fintype R V
e : SpecialLinearGroup R V ≃* Matrix.SpecialLinearGroup.{u_2, u_1} (Module.Free.ChooseBasisIndex R V) R :=
  MulEquiv.symm (Matrix.SpecialLinearGroup.toLin_equiv b)
⊢ (∃ (r : R),
      r ^ Fintype.card.{u_2} (Module.Free.ChooseBasisIndex R V) = 1 ∧
        Eq (α := Matrix.{u_2, u_2, u_1} (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
          ((Matrix.scalar (Module.Free.ChooseBasisIndex R V) :
                (a : R) → Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
              r :
            Matrix.{u_2, u_2, u_1} (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
          ((↑((e : (a : SpecialLinearGroup R V) → Matrix.SpecialLinearGroup (Module.Free.ChooseBasisIndex R V) R) g) :
              Matrix.{u_2, u_2, u_1} (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R) :
            Matrix.{u_2, u_2, u_1} (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)) ↔
    ∃ (r : R),
      r ^ Fintype.card.{u_2} (Module.Free.ChooseBasisIndex R V) = 1 ∧
        (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id
have inr : ∀ (a : R),
  a ^ Fintype.card.{u_2} (Module.Free.ChooseBasisIndex R V) = 1 ∧
      Eq (α := Matrix.{u_2, u_2, u_1} (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
        ((Matrix.scalar (Module.Free.ChooseBasisIndex R V) :
              (a : R) → Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
            a :
          Matrix.{u_2, u_2, u_1} (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
        ((↑((e : (a : SpecialLinearGroup R V) → Matrix.SpecialLinearGroup (Module.Free.ChooseBasisIndex R V) R) g) :
            Matrix.{u_2, u_2, u_1} (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R) :
          Matrix.{u_2, u_2, u_1} (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R) ↔
    a ^ Fintype.card.{u_2} (Module.Free.ChooseBasisIndex R V) = 1 ∧
      (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) a LinearMap.id
Tactic: apply exists_congr
-- 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 : SpecialLinearGroup R V
hR : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
this : Fintype (Module.Free.ChooseBasisIndex R V) := Module.Free.ChooseBasisIndex.fintype R V
e : SpecialLinearGroup R V ≃* Matrix.SpecialLinearGroup.{u_2, u_1} (Module.Free.ChooseBasisIndex R V) R :=
  MulEquiv.symm (Matrix.SpecialLinearGroup.toLin_equiv b)
⊢ ∀ (a : R),
    a ^ Fintype.card.{u_2} (Module.Free.ChooseBasisIndex R V) = 1 ∧
        Eq (α := Matrix.{u_2, u_2, u_1} (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
          ((Matrix.scalar (Module.Free.ChooseBasisIndex R V) :
                (a : R) → Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
              a :
            Matrix.{u_2, u_2, u_1} (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
          ((↑((e : (a : SpecialLinearGroup R V) → Matrix.SpecialLinearGroup (Module.Free.ChooseBasisIndex R V) R) g) :
              Matrix.{u_2, u_2, u_1} (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R) :
            Matrix.{u_2, u_2, u_1} (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R) ↔
      a ^ Fintype.card.{u_2} (Module.Free.ChooseBasisIndex R V) = 1 ∧
        (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) a LinearMap.id
have inr : ∀ (a : R),
  a ^ Fintype.card.{u_2} (Module.Free.ChooseBasisIndex R V) = 1 →
    (Eq (α := Matrix.{u_2, u_2, u_1} (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
        (Matrix.diagonal fun (x : Module.Free.ChooseBasisIndex R V) ↦ a)
        (↑((MulEquiv.symm (Matrix.SpecialLinearGroup.toLin_equiv b) :
                (a : SpecialLinearGroup R V) → Matrix.SpecialLinearGroup (Module.Free.ChooseBasisIndex R V) R)
              g) :
          Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R) ↔
      (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) a LinearMap.id)
Tactic: simp only [Matrix.scalar_apply, and_congr_right_iff, e]