awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
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 B : SpecialLinearGroup n R
⊢ Eq (α := (n → R) ≃ₗ[R] n → R)
    ((fun
          (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 : (n → R) ≃ₗ[R] 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 * B)) ⋯))
    ((fun
          (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 : (n → R) ≃ₗ[R] n → R))
      (HMul.hMul (α := _root_.SpecialLinearGroup R (n → R)) (β := _root_.SpecialLinearGroup R (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ˣ) })
        (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) B) ⋯ :
          { 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ˣ) })))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
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
g : SpecialLinearGroup n R
⊢ Eq.{u_2 + 1} (α := V →ₗ[R] V)
    (↑(↑((toLin_equiv b : (a : SpecialLinearGroup n R) → _root_.SpecialLinearGroup R V) g) : V ≃ₗ[R] V) : V →ₗ[R] V)
    ((toLin b b : (a : Matrix n n R) → V →ₗ[R] V) (↑g : Matrix n n R))

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Matrix.mulVec, Finset.sum, rfl
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
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
g : _root_.SpecialLinearGroup R V
⊢ Eq (α := Matrix n n R)
    ((↑((MulEquiv.symm (toLin_equiv b) : (a : _root_.SpecialLinearGroup R V) → SpecialLinearGroup n R) g) :
        Matrix n n R) :
      Matrix n n R)
    ((LinearMap.toMatrix b b : (a : V →ₗ[R] V) → Matrix n n R) (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) : Matrix n n R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
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
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
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
rwa₁ : Fintype.card.{u_2} (Module.Free.ChooseBasisIndex R V) ≤ 1
rwa₂ rwa₃ rwa₄ rwa₅ : Module.finrank R V ≤ 1
⊢ Subsingleton.{u_2 + 1} (Module.Free.ChooseBasisIndex R V)

Tactic:
rwa [← Finite.card_le_one_iff_subsingleton,
      Nat.card_eq_fintype_card, ← Module.finrank_eq_card_basis b]

Premises used: Module.finrank_eq_card_basis, Finite.card_le_one_iff_subsingleton, Nat.card_eq_fintype_card
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
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)

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]
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
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)
⊢ Subsingleton ↥(Subgroup.center (Matrix.SpecialLinearGroup.{u_2, u_1} (Module.Free.ChooseBasisIndex R V) R))

Tactic:
infer_instance
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
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)
⊢ 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
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
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))
⊢ Subsingleton.{u_2 + 1} ↥(Subgroup.center (SpecialLinearGroup R V))

Tactic:
rw [Equiv.subsingleton_congr
    (Subgroup.centerCongr (Matrix.SpecialLinearGroup.toLin_equiv b)).toEquiv] at this

Premises used: Matrix.SpecialLinearGroup.toLin_equiv, Equiv.subsingleton_congr, MulEquiv.toEquiv, Subgroup.centerCongr
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
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.{u_2 + 1} ↥(Subgroup.center (SpecialLinearGroup R V))
⊢ Eq.{u_2 + 1} (α := Subgroup (SpecialLinearGroup R V)) (Subgroup.center (SpecialLinearGroup R V)) ⊥

Tactic:
Subgroup.eq_bot_of_subsingleton _

Premises used: Subgroup.eq_bot_of_subsingleton
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
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.{u_2 + 1} ↥(Subgroup.center (SpecialLinearGroup R V))
⊢ Eq.{u_2 + 1} (α := Subgroup (SpecialLinearGroup R V)) (Subgroup.center (SpecialLinearGroup R V)) ⊥

Tactic:
exact Subgroup.eq_bot_of_subsingleton _

Premises used: Subgroup.eq_bot_of_subsingleton
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
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
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
⊢ 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

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
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
⊢ Subsingleton.{u_2 + 1} (SpecialLinearGroup R V)

Tactic:
have : Subsingleton (SpecialLinearGroup R V) := inferInstance
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
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
this : Subsingleton.{u_2 + 1} (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

Tactic:
simp [Subsingleton.eq_one g]

Premises used: Subsingleton.eq_one
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
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
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
⊢ 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:
rw [Module.finrank_eq_card_basis b]

Premises used: Module.finrank_eq_card_basis
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
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)
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
⊢ 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 [← show e g ∈ Subgroup.center _ ↔ g ∈ Subgroup.center _ from
    MulEquivClass.apply_mem_center_iff e]

Premises used: MulEquivClass.apply_mem_center_iff
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
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)
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
⊢ 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 [Matrix.SpecialLinearGroup.mem_center_iff]

Premises used: Matrix.SpecialLinearGroup.mem_center_iff
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
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)
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
⊢ (∃ (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:
apply exists_congr

Premises used: exists_congr
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
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)
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)
⊢ ∀ (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:
simp only [Matrix.scalar_apply, and_congr_right_iff, e]

Premises used: and_congr_right_iff, Matrix.scalar_apply
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
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_1 : 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
hr : r ^ Fintype.card.{u_2} (Module.Free.ChooseBasisIndex R V) = 1
this :
  Eq (α := Matrix.{u_2, u_2, u_1} (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
    (↑((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)
    ((Matrix.of :
        (a : Module.Free.ChooseBasisIndex R V → Module.Free.ChooseBasisIndex R V → R) →
          Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
      fun (i j : Module.Free.ChooseBasisIndex R V) ↦
      ((b.repr : (a : V) → Module.Free.ChooseBasisIndex R V →₀ R)
            ((fun (x : V) ↦ (((↑g : V ≃ₗ[R] V) : (a : V) → V) x : V))
              ((b : (a : Module.Free.ChooseBasisIndex R V) → V) j)) :
          (a : Module.Free.ChooseBasisIndex R V) → R)
        i)
simp :
  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) ↦ r)
      ((Matrix.of :
          (a : Module.Free.ChooseBasisIndex R V → Module.Free.ChooseBasisIndex R V → R) →
            Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
        fun (i j : Module.Free.ChooseBasisIndex R V) ↦
        (((b.repr : (a : V) → Module.Free.ChooseBasisIndex R V →₀ R)
                (((↑g : V ≃ₗ[R] V) : (a : V) → V) ((b : (a : Module.Free.ChooseBasisIndex R V) → V) j : V)) :
              Finsupp.{u_2, u_1} (Module.Free.ChooseBasisIndex R V) R) :
            (a : Module.Free.ChooseBasisIndex R V) → R)
          i) ↔
    (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) = HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id
⊢ 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) ↦ r)
      (↑((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) r LinearMap.id

Tactic:
simp only [this]