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
A : SpecialLinearGroup R V
v : V
⊢ Eq (α := V) ((LinearEquiv.symm ((toLinearEquiv : (a : SpecialLinearGroup R V) → V ≃ₗ[R] V) A) : (a : V) → V) v : V)
    ((fun (x : V) ↦ (((↑A⁻¹ : V ≃ₗ[R] V) : (a : V) → V) x : V)) v : V)

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
A : SpecialLinearGroup R V
⊢ (↑(LinearEquiv.symm ((toLinearEquiv : (a : SpecialLinearGroup R V) → V ≃ₗ[R] V) A)) : V →ₗ[R] V) =
    (↑(↑A⁻¹ : V ≃ₗ[R] V) : V →ₗ[R] V)

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
⊢ Function.Injective.{u_2 + 1, u_2 + 1} (α := SpecialLinearGroup R V) (β := V ≃ₗ[R] V)
    (⇑toLinearEquiv : (a : SpecialLinearGroup R V) → V ≃ₗ[R] V)

Tactic:
Subtype.val_injective

Premises used: Subtype.val_injective
-- 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
u : SpecialLinearGroup R V
⊢ Eq.{u_2 + 1} (α := V ≃ₗ[R] V)
    (LinearMap.GeneralLinearGroup.toLinearEquiv
      ((toGeneralLinearGroup : (a : SpecialLinearGroup R V) → LinearMap.GeneralLinearGroup R V) u))
    ((toLinearEquiv : (a : SpecialLinearGroup R V) → V ≃ₗ[R] V) u)

Tactic:
rfl

Premises used: LinearMap.GeneralLinearGroup.toLinearEquiv, 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
u : SpecialLinearGroup R V
⊢ Eq.{u_2 + 1} (α := V →ₗ[R] V)
    (↑((toGeneralLinearGroup : (a : SpecialLinearGroup R V) → LinearMap.GeneralLinearGroup R V) u) : V →ₗ[R] V)
    (↑((toLinearEquiv : (a : SpecialLinearGroup R V) → V ≃ₗ[R] V) u) : V →ₗ[R] V)

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
⊢ Function.Injective.{u_2 + 1, u_2 + 1} (α := SpecialLinearGroup R V) (β := LinearMap.GeneralLinearGroup R V)
    (⇑toGeneralLinearGroup : (a : SpecialLinearGroup R V) → LinearMap.GeneralLinearGroup R V)

Tactic:
simp [toGeneralLinearGroup, toLinearEquiv_injective]

Premises used: SpecialLinearGroup.toGeneralLinearGroup, SpecialLinearGroup.toLinearEquiv_injective
-- 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
u : LinearMap.GeneralLinearGroup R V
mp :
  Membership.mem (γ := Set (LinearMap.GeneralLinearGroup R V))
      (Set.range (ι := SpecialLinearGroup R V)
        (⇑toGeneralLinearGroup : (a : SpecialLinearGroup R V) → LinearMap.GeneralLinearGroup R V))
      u →
    Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) u.toLinearEquiv : Rˣ) (1 : Rˣ)
mpr :
  Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) u.toLinearEquiv : Rˣ) (1 : Rˣ) →
    Membership.mem (γ := Set (LinearMap.GeneralLinearGroup R V))
      (Set.range (ι := SpecialLinearGroup R V)
        (⇑toGeneralLinearGroup : (a : SpecialLinearGroup R V) → LinearMap.GeneralLinearGroup R V))
      u
⊢ Membership.mem (γ := Set (LinearMap.GeneralLinearGroup R V))
      (Set.range (ι := SpecialLinearGroup R V)
        (⇑toGeneralLinearGroup : (a : SpecialLinearGroup R V) → LinearMap.GeneralLinearGroup R V))
      u ↔
    Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) u.toLinearEquiv : Rˣ) (1 : Rˣ)

Tactic:
constructor
-- 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
u : LinearMap.GeneralLinearGroup R V
v : SpecialLinearGroup R V
hv : (toGeneralLinearGroup : (a : SpecialLinearGroup R V) → LinearMap.GeneralLinearGroup R V) v = u
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ˣ)
⊢ Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) u.toLinearEquiv : Rˣ) (1 : Rˣ)

Tactic:
rw [← hv, toGeneralLinearGroup_toLinearEquiv_apply]

Premises used: SpecialLinearGroup.toGeneralLinearGroup_toLinearEquiv_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
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ˣ) ((toLinearEquiv : (a : SpecialLinearGroup R V) → V ≃ₗ[R] V) v) : Rˣ)
    (1 : Rˣ)

Tactic:
v.prop

Premises used: Subtype.prop
-- 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
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ˣ) ((toLinearEquiv : (a : SpecialLinearGroup R V) → V ≃ₗ[R] V) v) : Rˣ)
    (1 : Rˣ)

Tactic:
exact v.prop

Premises used: Subtype.prop
-- 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
u : LinearMap.GeneralLinearGroup R V
hu : Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) u.toLinearEquiv : Rˣ) (1 : Rˣ)
⊢ Membership.mem (γ := Set (LinearMap.GeneralLinearGroup R V))
    (Set.range (ι := SpecialLinearGroup R V)
      (⇑toGeneralLinearGroup : (a : SpecialLinearGroup R V) → LinearMap.GeneralLinearGroup R V))
    u

Tactic:
⟨⟨u.toLinearEquiv, hu⟩, rfl⟩

Premises used: Set.Mem, setOf, LinearMap.GeneralLinearGroup.toLinearEquiv, Subtype.mk, Exists.intro, Set.range, 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
u : LinearMap.GeneralLinearGroup R V
hu : Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) u.toLinearEquiv : Rˣ) (1 : Rˣ)
⊢ Membership.mem (γ := Set (LinearMap.GeneralLinearGroup R V))
    (Set.range (ι := SpecialLinearGroup R V)
      (⇑toGeneralLinearGroup : (a : SpecialLinearGroup R V) → LinearMap.GeneralLinearGroup R V))
    u

Tactic:
refine ⟨⟨u.toLinearEquiv, hu⟩, 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
g : SpecialLinearGroup R V
v : V
⊢ g • v = HSMul.hSMul (α := V ≃ₗ[R] V) ((toLinearEquiv : (a : SpecialLinearGroup R V) → V ≃ₗ[R] V) g : V ≃ₗ[R] V) v

Tactic:
rfl

Premises used: SMul.comp.smul, 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
g : SpecialLinearGroup R V
⊢ (toLinearEquiv : (a : SpecialLinearGroup R V) → V ≃ₗ[R] V) g = (↑g : V ≃ₗ[R] V)

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
g : SpecialLinearGroup R V
a : R
v : V
⊢ g • a • v = a • g • v

Tactic:
simp [SpecialLinearGroup.smul_def]

Premises used: SpecialLinearGroup.smul_def
-- 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
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
rw₂ rw₃ : Eq.{u_3 + 1} (α := 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ˣ)

Tactic:
rw [LinearEquiv.det_baseChange, g.prop, map_one]

Premises used: LinearEquiv.det_baseChange, map_one, Subtype.prop
-- 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
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
⊢ Eq (α := S ⊗[R] V ≃ₗ[S] S ⊗[R] V)
    (↑(Subtype.mk (p := fun (u : S ⊗[R] V ≃ₗ[S] S ⊗[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ˣ)
                u :
              Sˣ)
            (1 : Sˣ))
          (LinearEquiv.baseChange R S V V (↑1 : V ≃ₗ[R] V)) ⋯) :
      S ⊗[R] V ≃ₗ[S] S ⊗[R] V)
    (↑1 : S ⊗[R] V ≃ₗ[S] S ⊗[R] V)

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
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
x y : SpecialLinearGroup R V
⊢ (↑(Subtype.mk (p := fun (u : S ⊗[R] V ≃ₗ[S] S ⊗[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ˣ)
                u :
              Sˣ)
            (1 : Sˣ))
          (LinearEquiv.baseChange R S V V (↑(x * y) : V ≃ₗ[R] V)) ⋯) :
      S ⊗[R] V ≃ₗ[S] S ⊗[R] V) =
    (↑(HMul.hMul (α := SpecialLinearGroup S (S ⊗[R] V))
          (Subtype.mk (p := fun (u : S ⊗[R] V ≃ₗ[S] S ⊗[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ˣ)
                  u :
                Sˣ)
              (1 : Sˣ))
            (LinearEquiv.baseChange R S V V (↑x : V ≃ₗ[R] V)) ⋯)
          (Subtype.mk (p := fun (u : S ⊗[R] V ≃ₗ[S] S ⊗[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ˣ)
                  u :
                Sˣ)
              (1 : Sˣ))
            (LinearEquiv.baseChange R S V V (↑y : V ≃ₗ[R] V)) ⋯)) :
      S ⊗[R] V ≃ₗ[S] S ⊗[R] V)

Tactic:
simp [LinearEquiv.baseChange_mul]

Premises used: LinearEquiv.baseChange_mul
-- 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
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
f : SpecialLinearGroup R V
⊢ Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : W ≃ₗ[R] W) → Rˣ) (e.symm ≪≫ₗ (↑f : V ≃ₗ[R] V) ≪≫ₗ e) : Rˣ) (1 : Rˣ)

Tactic:
simp [f.prop]

Premises used: Subtype.prop
-- 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
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
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ˣ)
⊢ Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) (e ≪≫ₗ (↑g : W ≃ₗ[R] W) ≪≫ₗ e.symm) : Rˣ) (1 : Rˣ)

Tactic:
nth_rewrite 1 [← LinearEquiv.symm_symm e]

Premises used: LinearEquiv.symm_symm
-- 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
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ˣ)
rw₁ rw₂ : Eq.{u_1 + 1} (α := Rˣ) 1 1
⊢ 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:
rw [LinearEquiv.det_conj g e.symm, g.prop]

Premises used: LinearEquiv.symm, LinearEquiv.det_conj, Subtype.prop
-- 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
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
f : SpecialLinearGroup R V
⊢ Eq.{u_2 + 1} (α := V ≃ₗ[R] V)
    ((fun (a : { u : V ≃ₗ[R] V // Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) u : Rˣ) (1 : Rˣ) }) ↦
        (↑a : V ≃ₗ[R] V))
      ((fun (g : SpecialLinearGroup R W) ↦
          (Subtype.mk (p := fun (u : V ≃ₗ[R] V) ↦
              Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) u : Rˣ) (1 : Rˣ))
              (e ≪≫ₗ (↑g : W ≃ₗ[R] W) ≪≫ₗ e.symm) ⋯ :
            { u : V ≃ₗ[R] V // Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) u : Rˣ) (1 : Rˣ) }))
        ((fun (f : SpecialLinearGroup R V) ↦
            (Subtype.mk (p := fun (u : W ≃ₗ[R] W) ↦
                Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : W ≃ₗ[R] W) → Rˣ) u : Rˣ) (1 : Rˣ))
                (e.symm ≪≫ₗ (↑f : V ≃ₗ[R] V) ≪≫ₗ e) ⋯ :
              { u : W ≃ₗ[R] W // Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : W ≃ₗ[R] W) → Rˣ) u : Rˣ) (1 : Rˣ) }))
          f)))
    ((fun (a : { u : V ≃ₗ[R] V // Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) u : Rˣ) (1 : Rˣ) }) ↦
        (↑a : V ≃ₗ[R] V))
      f)

Tactic:
aesop
-- 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
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_3 + 1} (α := W ≃ₗ[R] W)
    ((fun (a : { u : W ≃ₗ[R] W // Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : W ≃ₗ[R] W) → Rˣ) u : Rˣ) (1 : Rˣ) }) ↦
        (↑a : W ≃ₗ[R] W))
      ((fun (f : SpecialLinearGroup R V) ↦
          (Subtype.mk (p := fun (u : W ≃ₗ[R] W) ↦
              Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : W ≃ₗ[R] W) → Rˣ) u : Rˣ) (1 : Rˣ))
              (e.symm ≪≫ₗ (↑f : V ≃ₗ[R] V) ≪≫ₗ e) ⋯ :
            { u : W ≃ₗ[R] W // Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : W ≃ₗ[R] W) → Rˣ) u : Rˣ) (1 : Rˣ) }))
        ((fun (g : SpecialLinearGroup R W) ↦
            (Subtype.mk (p := fun (u : V ≃ₗ[R] V) ↦
                Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) u : Rˣ) (1 : Rˣ))
                (e ≪≫ₗ (↑g : W ≃ₗ[R] W) ≪≫ₗ e.symm) ⋯ :
              { u : V ≃ₗ[R] V // Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) u : Rˣ) (1 : Rˣ) }))
          g)))
    ((fun (a : { u : W ≃ₗ[R] W // Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : W ≃ₗ[R] W) → Rˣ) u : Rˣ) (1 : Rˣ) }) ↦
        (↑a : W ≃ₗ[R] W))
      g)

Tactic:
aesop
-- 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
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
f g : SpecialLinearGroup R V
⊢ Eq.{u_3 + 1} (α := W ≃ₗ[R] W)
    ((fun (a : { u : W ≃ₗ[R] W // Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : W ≃ₗ[R] W) → Rˣ) u : Rˣ) (1 : Rˣ) }) ↦
        (↑a : W ≃ₗ[R] W))
      (Subtype.mk (p := fun (u : W ≃ₗ[R] W) ↦
        Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : W ≃ₗ[R] W) → Rˣ) u : Rˣ) (1 : Rˣ))
        (e.symm ≪≫ₗ (↑(f * g) : V ≃ₗ[R] V) ≪≫ₗ e) ⋯))
    ((fun (a : { u : W ≃ₗ[R] W // Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : W ≃ₗ[R] W) → Rˣ) u : Rˣ) (1 : Rˣ) }) ↦
        (↑a : W ≃ₗ[R] W))
      (HMul.hMul (α := SpecialLinearGroup R W)
        (Subtype.mk (p := fun (u : W ≃ₗ[R] W) ↦
          Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : W ≃ₗ[R] W) → Rˣ) u : Rˣ) (1 : Rˣ))
          (e.symm ≪≫ₗ (↑f : V ≃ₗ[R] V) ≪≫ₗ e) ⋯)
        (Subtype.mk (p := fun (u : W ≃ₗ[R] W) ↦
          Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : W ≃ₗ[R] W) → Rˣ) u : Rˣ) (1 : Rˣ))
          (e.symm ≪≫ₗ (↑g : V ≃ₗ[R] V) ≪≫ₗ e) ⋯)))

Tactic:
aesop
-- 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
W : Type u_3
inst_3 : AddCommGroup W
inst_4 : Module R W
e : V ≃ₗ[R] W
f : SpecialLinearGroup R V
⊢ Eq (α := W ≃ₗ[R] W) (↑((congr_linearEquiv e : (a : SpecialLinearGroup R V) → SpecialLinearGroup R W) f) : W ≃ₗ[R] W)
    (e.symm ≪≫ₗ (↑f : V ≃ₗ[R] V) ≪≫ₗ e)

Tactic:
rfl

Premises used: LinearEquiv.trans, 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
W : Type u_3
inst_3 : AddCommGroup W
inst_4 : Module R W
e : V ≃ₗ[R] W
f : SpecialLinearGroup R V
x : W
⊢ Eq.{u_3 + 1} (α := W)
    ((fun (x : W) ↦
          (((↑((congr_linearEquiv e : (a : SpecialLinearGroup R V) → SpecialLinearGroup R W) f) : W ≃ₗ[R] W) :
                (a : W) → W)
              x :
            W))
        x :
      W)
    ((e : (a : V) → W) ((fun (x : V) ↦ (((↑f : V ≃ₗ[R] V) : (a : V) → V) x : V)) ((e.symm : (a : W) → V) x)) : W)

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
W : Type u_3
inst_3 : AddCommGroup W
inst_4 : Module R W
e : V ≃ₗ[R] W
⊢ (congr_linearEquiv e).symm = congr_linearEquiv e.symm

Tactic:
rfl

Premises used: LinearEquiv.symm, SpecialLinearGroup.congr_linearEquiv, Equiv.symm, MulEquiv.symm, 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
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
f : W ≃ₗ[R] X
⊢ (congr_linearEquiv e).trans (congr_linearEquiv f) = congr_linearEquiv (e ≪≫ₗ f)

Tactic:
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
⊢ Eq (α := SpecialLinearGroup R V ≃* SpecialLinearGroup R V) (congr_linearEquiv (LinearEquiv.refl R V))
    (MulEquiv.refl (SpecialLinearGroup R V))

Tactic:
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
A : SpecialLinearGroup 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ˣ)
        ((toLin' : (a : SpecialLinearGroup n R) → (n → R) ≃ₗ[R] n → R) A) :
      Rˣ)
    (1 : Rˣ)

Tactic:
simp [← Units.val_inj, LinearEquiv.coe_det, Units.val_one,
        Matrix.SpecialLinearGroup.toLin'_to_linearMap]

Premises used: Units.val_inj, Matrix.SpecialLinearGroup.toLin'_to_linearMap, Units.val_one, LinearEquiv.coe_det
-- 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
u : _root_.SpecialLinearGroup R (n → R)
⊢ Eq.{u_1 + 1} (α := R)
    (det.{u_1, u_3} (n := n)
      ((LinearMap.toMatrix' : (a : (n → R) →ₗ[R] n → R) → Matrix n n R)
        (↑(↑u : (n → R) ≃ₗ[R] n → R) : (n → R) →ₗ[R] n → R)))
    1

Tactic:
simp [← LinearEquiv.coe_det, u.prop]

Premises used: Subtype.prop, LinearEquiv.coe_det
-- 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
u : _root_.SpecialLinearGroup R (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))
      ((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ˣ) }))
        ((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 }))
          u)))
    ((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))
      u)

Tactic:
simp [← LinearEquiv.toLinearMap_inj, Matrix.SpecialLinearGroup.toLin']

Premises used: LinearEquiv.toLinearMap_inj, Matrix.SpecialLinearGroup.toLin'