awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card
Goal:
𝔽 : Type u_1
inst : Field 𝔽
inst_1 : Fintype 𝔽
n : ℕ
M : { s : Fin n → Fin n → 𝔽 // LinearIndependent 𝔽 s }
b : Basis (Fin n) 𝔽 (Fin n → 𝔽) := basisOfPiSpaceOfLinearIndependent ⋯
this :
  Invertible (α := Matrix (Fin n) (Fin n) 𝔽) (Basis.toMatrix (Pi.basisFun 𝔽 (Fin n)) (⇑b : (a : Fin n) → Fin n → 𝔽))
rw :
  IsUnit
    (det (n := Fin n)
      (Basis.toMatrix (Pi.basisFun 𝔽 (Fin n)) (⇑(basisOfPiSpaceOfLinearIndependent ⋯) : (a : Fin n) → Fin n → 𝔽)))
⊢ IsUnit (↑M : Fin n → Fin n → 𝔽)ᵀ.det

Tactic:
rw [← Basis.coePiBasisFun.toMatrix_eq_transpose,
      ← coe_basisOfPiSpaceOfLinearIndependent M.2]

Premises used: coe_basisOfPiSpaceOfLinearIndependent, Module.Basis.coePiBasisFun.toMatrix_eq_transpose, Subtype.property
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card
Goal:
𝔽 : Type u_1
inst : Field 𝔽
inst_1 : Fintype 𝔽
n : ℕ
M : { s : Fin n → Fin n → 𝔽 // LinearIndependent 𝔽 s }
b : Basis (Fin n) 𝔽 (Fin n → 𝔽) := basisOfPiSpaceOfLinearIndependent ⋯
this :
  Invertible (α := Matrix (Fin n) (Fin n) 𝔽) (Basis.toMatrix (Pi.basisFun 𝔽 (Fin n)) (⇑b : (a : Fin n) → Fin n → 𝔽))
⊢ IsUnit
    (det (n := Fin n)
      (Basis.toMatrix (Pi.basisFun 𝔽 (Fin n)) (⇑(basisOfPiSpaceOfLinearIndependent ⋯) : (a : Fin n) → Fin n → 𝔽)))

Tactic:
isUnit_det_of_invertible _

Premises used: Matrix.isUnit_det_of_invertible
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card
Goal:
𝔽 : Type u_1
inst : Field 𝔽
inst_1 : Fintype 𝔽
n : ℕ
M : { s : Fin n → Fin n → 𝔽 // LinearIndependent 𝔽 s }
b : Basis (Fin n) 𝔽 (Fin n → 𝔽) := basisOfPiSpaceOfLinearIndependent ⋯
this :
  Invertible (α := Matrix (Fin n) (Fin n) 𝔽) (Basis.toMatrix (Pi.basisFun 𝔽 (Fin n)) (⇑b : (a : Fin n) → Fin n → 𝔽))
⊢ IsUnit
    (det (n := Fin n)
      (Basis.toMatrix (Pi.basisFun 𝔽 (Fin n)) (⇑(basisOfPiSpaceOfLinearIndependent ⋯) : (a : Fin n) → Fin n → 𝔽)))

Tactic:
exact isUnit_det_of_invertible _

Premises used: Matrix.isUnit_det_of_invertible
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card
Goal:
𝔽 : Type u_1
inst : Field 𝔽
inst_1 : Fintype 𝔽
n : ℕ
M : { s : Fin n → Fin n → 𝔽 // LinearIndependent 𝔽 s }
let let₁ let₂ : IsUnit (↑M : Fin n → Fin n → 𝔽)ᵀ.det
let₃ :
  let b : Basis (Fin n) 𝔽 (Fin n → 𝔽) := basisOfPiSpaceOfLinearIndependent ⋯;
  ∀
    (this :
      Invertible (α := Matrix (Fin n) (Fin n) 𝔽)
        (Basis.toMatrix (Pi.basisFun 𝔽 (Fin n)) (⇑b : (a : Fin n) → Fin n → 𝔽))),
    IsUnit (↑M : Fin n → Fin n → 𝔽)ᵀ.det
let₄ :
  let b : Basis (Fin n) 𝔽 (Fin n → 𝔽) := basisOfPiSpaceOfLinearIndependent ⋯;
  ∀
    (this :
      Invertible (α := Matrix (Fin n) (Fin n) 𝔽)
        (Basis.toMatrix (Pi.basisFun 𝔽 (Fin n)) (⇑b : (a : Fin n) → Fin n → 𝔽))),
    IsUnit
      (det (n := Fin n)
        (Basis.toMatrix (Pi.basisFun 𝔽 (Fin n)) (⇑(basisOfPiSpaceOfLinearIndependent ⋯) : (a : Fin n) → Fin n → 𝔽)))
⊢ IsUnit (↑M : Fin n → Fin n → 𝔽)ᵀ.det

Tactic:
classical
    let b := basisOfPiSpaceOfLinearIndependent M.2
    have := (Pi.basisFun 𝔽 (Fin n)).invertibleToMatrix b
    rw [← Basis.coePiBasisFun.toMatrix_eq_transpose,
      ← coe_basisOfPiSpaceOfLinearIndependent M.2]
    exact isUnit_det_of_invertible _

Premises used: Matrix.isUnit_det_of_invertible, coe_basisOfPiSpaceOfLinearIndependent, Module.Basis.coePiBasisFun.toMatrix_eq_transpose, Subtype.property
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card
Goal:
𝔽 : Type u_1
inst : Field 𝔽
inst_1 : Fintype 𝔽
n : ℕ
⊢ Function.RightInverse
    (fun (M : { s : Fin n → Fin n → 𝔽 // LinearIndependent 𝔽 s }) ↦ GeneralLinearGroup.mk'' (↑M : Fin n → Fin n → 𝔽)ᵀ ⋯)
    fun (M : GL (Fin n) 𝔽) ↦
    Subtype.mk (p := fun (s : Fin n → Fin n → 𝔽) ↦ LinearIndependent 𝔽 s) (↑M : Matrix (Fin n) (Fin n) 𝔽).col ⋯

Tactic:
congrFun rfl

Premises used: Function.LeftInverse, congrFun, Function.RightInverse, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card
Goal:
𝔽 : Type u_1
inst : Field 𝔽
inst_1 : Fintype 𝔽
n : ℕ
⊢ Function.RightInverse
    (fun (M : { s : Fin n → Fin n → 𝔽 // LinearIndependent 𝔽 s }) ↦ GeneralLinearGroup.mk'' (↑M : Fin n → Fin n → 𝔽)ᵀ ⋯)
    fun (M : GL (Fin n) 𝔽) ↦
    Subtype.mk (p := fun (s : Fin n → Fin n → 𝔽) ↦ LinearIndependent 𝔽 s) (↑M : Matrix (Fin n) (Fin n) 𝔽).col ⋯

Tactic:
exact congrFun rfl

Premises used: congrFun, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card
Goal:
𝔽 : Type u_1
inst : Field 𝔽
inst_1 : Fintype 𝔽
n : ℕ
rw : n ≤ finrank 𝔽 (Fin n → 𝔽)
⊢ Nat.card.{u_1} (GL (Fin n) 𝔽) = ∏ i : Fin n, (q ^ n - q ^ (↑i : ℕ))

Tactic:
rw [Nat.card_congr (equiv_GL_linearindependent n), card_linearIndependent,
    Module.finrank_fintype_fun_eq_card, Fintype.card_fin]

Premises used: Fintype.card_fin, Nat.card_congr, Module.finrank_fintype_fun_eq_card, Matrix.equiv_GL_linearindependent, card_linearIndependent
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card
Goal:
𝔽 : Type u_1
inst : Field 𝔽
inst_1 : Fintype 𝔽
n : ℕ
⊢ n ≤ finrank 𝔽 (Fin n → 𝔽)

Tactic:
simp only [Module.finrank_fintype_fun_eq_card, Fintype.card_fin, le_refl]

Premises used: le_refl, Fintype.card_fin, Module.finrank_fintype_fun_eq_card
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : GL n R
rw : ((↑A : Matrix n n R) * (↑A⁻¹ : Matrix n n R)).det = 1
rw₁ : Eq.{v + 1} (α := R) (Matrix.det.{v, u} (n := n) 1) 1
rw₂ rw₃ : Eq.{v + 1} (α := R) 1 1
⊢ (↑A : Matrix n n R).det * (↑A⁻¹ : Matrix n n R).det = 1

Tactic:
rw [← det_mul, A.mul_inv, det_one]

Premises used: Units.mul_inv, Matrix.det_mul, Matrix.det_one
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : GL n R
rw : ((↑A⁻¹ : Matrix n n R) * (↑A : Matrix n n R)).det = 1
rw₁ : Eq.{v + 1} (α := R) (Matrix.det.{v, u} (n := n) 1) 1
rw₂ rw₃ : Eq.{v + 1} (α := R) 1 1
⊢ (↑A⁻¹ : Matrix n n R).det * (↑A : Matrix n n R).det = 1

Tactic:
rw [← det_mul, A.inv_mul, det_one]

Premises used: Units.inv_mul, Matrix.det_mul, Matrix.det_one
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : Nontrivial R
g : GL n R
⊢ (↑g : Matrix n n R).det ≠ 0

Tactic:
g.det.ne_zero

Premises used: Units.ne_zero, Matrix.GeneralLinearGroup.det, DFunLike.coe, Matrix.det
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
u : Rˣ
huv : (↑((det : (a : GL n R) → Rˣ) ((scalar n : (a : Rˣ) → GL n R) u)) : R) = (↑(u ^ Fintype.card n) : R)
⊢ (det : (a : GL n R) → Rˣ) ((scalar n : (a : Rˣ) → GL n R) u) = u ^ Fintype.card n

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
u : Rˣ
⊢ (↑((det : (a : GL n R) → Rˣ) ((scalar n : (a : Rˣ) → GL n R) u)) : R) = (↑(u ^ Fintype.card n) : R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
V : Type u_1
inst_3 : AddCommGroup V
inst_4 : Module R V
b : Module.Basis n R V
M : GL n R
v : V
⊢ Eq (α := V)
    ((GeneralLinearGroup.toLinearEquiv ((toLin' b : (a : GL n R) → LinearMap.GeneralLinearGroup R V) M) : (a : V) → V)
        v :
      V)
    ((Fintype.linearCombination R (⇑b : (a : n) → V) : (a : n → R) → V)
        ((↑M : Matrix n n R) *ᵥ (⇑((b.repr : (a : V) → n →₀ R) v : n →₀ R) : (a : n) → R)) :
      V)

Tactic:
simp [toLin', toLin, Fintype.linearCombination_apply, MulEquiv.trans_apply]

Premises used: Matrix.GeneralLinearGroup.toLin, Matrix.GeneralLinearGroup.toLin', MulEquiv.trans_apply, Fintype.linearCombination_apply
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A B : GL n R
⊢ A = B ↔ ∀ (i j : n), (↑A : Matrix n n R) i j = (↑B : Matrix n n R) i j

Tactic:
Units.ext_iff.trans Matrix.ext_iff.symm

Premises used: Units.ext_iff, Iff.trans, Matrix.ext_iff, Iff.symm
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A B : GL n R
h : ∀ (i j : n), (↑A : Matrix n n R) i j = (↑B : Matrix n n R) i j
⊢ A = B

Tactic:
Units.ext <| Matrix.ext h

Premises used: Units.ext, Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A B : GL n R
⊢ (↑(A * B) : Matrix n n R) = (↑A : Matrix n n R) * (↑B : Matrix n n R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
⊢ Eq (α := Matrix n n R) (↑1 : Matrix n n R) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : GL n R
⊢ (↑A⁻¹ : Matrix n n R) = (↑A : Matrix n n R)⁻¹

Tactic:
letI := A.invertible
  invOf_eq_nonsing_inv (↑A : Matrix n n R)

Premises used: Units.val, Matrix.invOf_eq_nonsing_inv
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : GL n R
⊢ Eq (α := (n → R) →ₗ[R] n → R)
    (↑((toLin : (a : GL n R) → LinearMap.GeneralLinearGroup R (n → R)) A) : (n → R) →ₗ[R] n → R)
    (↑A : Matrix n n R).mulVecLin

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : GL n R
v : n → R
⊢ Eq (α := n → R)
    (((↑((toLin : (a : GL n R) → LinearMap.GeneralLinearGroup R (n → R)) A) : (n → R) →ₗ[R] n → R) :
          (a : n → R) → n → R)
        v :
      n → R)
    (((↑A : Matrix n n R).mulVecLin : (a : n → R) → n → R) v : n → R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
⊢ Eq (α := GL n R →* GL n R) (map (RingHom.id R)) (MonoidHom.id (GL n R))

Tactic:
rfl

Premises used: MonoidHom.mk', Matrix.GeneralLinearGroup.map, Matrix.map, rfl, Units.map
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
f : R →+* S
i j : n
g : GL n R
⊢ Eq.{u_1 + 1} (α := S) ((↑((map f : (a : GL n R) → GL n S) g) : Matrix n n S) i j : S)
    ((f : (a : R) → S) ((↑g : Matrix n n R) i j) : S)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
T : Type u_2
inst_3 : CommRing S
inst_4 : CommRing T
f : T →+* R
g : R →+* S
⊢ Eq (α := GL n T →* GL n S) (map (g.comp f)) (MonoidHom.comp (map g) (map f))

Tactic:
rfl

Premises used: Matrix, Matrix.GeneralLinearGroup.map, Matrix.map, rfl, Units.map
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
T : Type u_2
inst_3 : CommRing S
inst_4 : CommRing T
f : T →+* R
g : R →+* S
x : GL n T
⊢ Eq (α := GL n S) ((MonoidHom.comp (map g) (map f) : (a : GL n T) → GL n S) x : GL n S)
    ((map g : (a : GL n R) → GL n S) ((map f : (a : GL n T) → GL n R) x) : GL n S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
f : R →+* S
⊢ Eq (α := GL n S) ((map f : (a : GL n R) → GL n S) 1) 1

Tactic:
simp only [map_one]

Premises used: map_one
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
f : R →+* S
g h : GL n R
⊢ (map f : (a : GL n R) → GL n S) (g * h) =
    HMul.hMul (α := GL n S) (β := GL n S) ((map f : (a : GL n R) → GL n S) g : GL n S)
      ((map f : (a : GL n R) → GL n S) h : GL n S)

Tactic:
simp only [map_mul]

Premises used: map_mul
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
f : R →+* S
g : GL n R
⊢ Eq (α := GL n S) ((map f : (a : GL n R) → GL n S) g⁻¹ : GL n S) (((map f : (a : GL n R) → GL n S) g)⁻¹ : GL n S)

Tactic:
simp only [map_inv]

Premises used: map_inv
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
f : R →+* S
g : GL n R
huv :
  Eq.{u_1 + 1} (α := S) (↑((det : (a : GL n S) → Sˣ) ((map f : (a : GL n R) → GL n S) g)) : S)
    (↑(((Units.map (↑f : R →* S) : MonoidHom.{v, u_1} Rˣ Sˣ) : (a : Rˣ) → Sˣ) ((det : (a : GL n R) → Rˣ) g)) : S)
⊢ Eq.{u_1 + 1} (α := Sˣ) ((det : (a : GL n S) → Sˣ) ((map f : (a : GL n R) → GL n S) g) : Sˣ)
    (((Units.map (↑f : R →* S) : MonoidHom.{v, u_1} Rˣ Sˣ) : (a : Rˣ) → Sˣ) ((det : (a : GL n R) → Rˣ) g) : Sˣ)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
f : R →+* S
g : GL n R
huv :
  Eq.{u_1 + 1} (α := S)
    (Matrix.det.{u_1, u} (n := n)
        (((↑f.mapMatrix : Matrix n n R →* Matrix n n S) : (a : Matrix n n R) → Matrix n n S) (↑g : Matrix n n R)) :
      S)
    ((f : (a : R) → S) (↑g : Matrix n n R).det : S)
⊢ Eq.{u_1 + 1} (α := S) (↑((det : (a : GL n S) → Sˣ) ((map f : (a : GL n R) → GL n S) g)) : S)
    (↑(((Units.map (↑f : R →* S) : MonoidHom.{v, u_1} Rˣ Sˣ) : (a : Rˣ) → Sˣ) ((det : (a : GL n R) → Rˣ) g)) : S)

Tactic:
simp only [map,
    Matrix.GeneralLinearGroup.val_det_apply, Units.coe_map, MonoidHom.coe_coe]

Premises used: Units.coe_map, Matrix.GeneralLinearGroup.map, MonoidHom.coe_coe, Matrix.GeneralLinearGroup.val_det_apply
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
f : R →+* S
g : GL n R
⊢ Eq.{u_1 + 1} (α := S)
    (Matrix.det.{u_1, u} (n := n)
        (((↑f.mapMatrix : Matrix n n R →* Matrix n n S) : (a : Matrix n n R) → Matrix n n S) (↑g : Matrix n n R)) :
      S)
    ((f : (a : R) → S) (↑g : Matrix n n R).det : S)

Tactic:
Eq.symm (RingHom.map_det f g.1)

Premises used: Units.val, RingHom.map_det, Eq.symm
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
f : R →+* S
g : GL n R
⊢ Eq.{u_1 + 1} (α := S)
    (Matrix.det.{u_1, u} (n := n)
        (((↑f.mapMatrix : Matrix n n R →* Matrix n n S) : (a : Matrix n n R) → Matrix n n S) (↑g : Matrix n n R)) :
      S)
    ((f : (a : R) → S) (↑g : Matrix n n R).det : S)

Tactic:
exact Eq.symm (RingHom.map_det f g.1)

Premises used: Units.val, RingHom.map_det, Eq.symm
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
f : R →+* S
g : GL n R
⊢ HMul.hMul (α := GL n S) (β := GL n S) ((map f : (a : GL n R) → GL n S) g : GL n S)
      ((map f : (a : GL n R) → GL n S) g⁻¹ : GL n S) =
    1

Tactic:
simp only [map_inv, mul_inv_cancel]

Premises used: map_inv, mul_inv_cancel
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
f : R →+* S
g : GL n R
⊢ HMul.hMul (α := GL n S) (β := GL n S) ((map f : (a : GL n R) → GL n S) g⁻¹ : GL n S)
      ((map f : (a : GL n R) → GL n S) g : GL n S) =
    1

Tactic:
simp only [map_inv, inv_mul_cancel]

Premises used: inv_mul_cancel, map_inv
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
f : R →+* S
g : GL n R
rw : Eq (α := Matrix n n S) (((↑g : Matrix n n R) * (↑g : Matrix n n R)⁻¹).map (⇑f : (a : R) → S)) 1
⊢ HMul.hMul (α := Matrix n n S) ((↑g : Matrix n n R).map (⇑f : (a : R) → S))
      ((↑g : Matrix n n R)⁻¹.map (⇑f : (a : R) → S)) =
    1

Tactic:
rw [← Matrix.map_mul]

Premises used: Matrix.map_mul
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
f : R →+* S
g : GL n R
⊢ Eq (α := Matrix n n S) (((↑g : Matrix n n R) * (↑g : Matrix n n R)⁻¹).map (⇑f : (a : R) → S)) 1

Tactic:
simp only [isUnits_det_units, mul_nonsing_inv, map_zero, map_one, Matrix.map_one]

Premises used: Matrix.isUnits_det_units, Matrix.map_one, map_zero, map_one, Matrix.mul_nonsing_inv
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
f : R →+* S
g : GL n R
rw : Eq (α := Matrix n n S) (((↑g : Matrix n n R)⁻¹ * (↑g : Matrix n n R)).map (⇑f : (a : R) → S)) 1
⊢ HMul.hMul (α := Matrix n n S) ((↑g : Matrix n n R)⁻¹.map (⇑f : (a : R) → S))
      ((↑g : Matrix n n R).map (⇑f : (a : R) → S)) =
    1

Tactic:
rw [← Matrix.map_mul]

Premises used: Matrix.map_mul
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
f : R →+* S
g : GL n R
⊢ Eq (α := Matrix n n S) (((↑g : Matrix n n R)⁻¹ * (↑g : Matrix n n R)).map (⇑f : (a : R) → S)) 1

Tactic:
simp only [isUnits_det_units, nonsing_inv_mul, map_zero, map_one, Matrix.map_one]

Premises used: Matrix.isUnits_det_units, Matrix.map_one, Matrix.nonsing_inv_mul, map_zero, map_one
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R_1 : Type v
inst_2 : CommRing R_1
S : Type u_1
T : Type u_2
inst_3 : CommRing S
inst_4 : CommRing T
f : R_1 →+* S
R : Type u_3
m : Type u_4
inst_5 : CommSemiring R
inst_6 : Fintype m
inst_7 : DecidableEq m
x : GL n R
y : GL m R
⊢ HMul.hMul (α := Matrix (n × m) (n × m) R)
      (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) (↑x : Matrix n n R) (↑y : Matrix m m R))
      (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) (↑x⁻¹ : Matrix n n R) (↑y⁻¹ : Matrix m m R)) =
    1

Tactic:
simp only [← mul_kronecker_mul, Units.mul_inv, one_kronecker_one]

Premises used: Matrix.mul_kronecker_mul, Units.mul_inv, Matrix.one_kronecker_one
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R_1 : Type v
inst_2 : CommRing R_1
S : Type u_1
T : Type u_2
inst_3 : CommRing S
inst_4 : CommRing T
f : R_1 →+* S
R : Type u_3
m : Type u_4
inst_5 : CommSemiring R
inst_6 : Fintype m
inst_7 : DecidableEq m
x : GL n R
y : GL m R
⊢ HMul.hMul (α := Matrix (n × m) (n × m) R)
      (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) (↑x⁻¹ : Matrix n n R) (↑y⁻¹ : Matrix m m R))
      (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) (↑x : Matrix n n R) (↑y : Matrix m m R)) =
    1

Tactic:
simp only [← mul_kronecker_mul, Units.inv_mul, one_kronecker_one]

Premises used: Units.inv_mul, Matrix.mul_kronecker_mul, Matrix.one_kronecker_one
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_3
m : Type u_4
inst_2 : CommSemiring R
inst_3 : Fintype m
inst_4 : DecidableEq m
x : Matrix n n R
y : Matrix m m R
hx : IsUnit x
hy : IsUnit y
⊢ IsUnit (M := Matrix (n × m) (n × m) R) (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) x y)

Tactic:
GeneralLinearGroup.kronecker hx.unit hy.unit |>.isUnit

Premises used: Matrix.GeneralLinearGroup.kronecker, Matrix.kroneckerMap, IsUnit.unit, Units.isUnit
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
g g' : SpecialLinearGroup n R
⊢ Eq (α := GL n R) ((toGL : (a : SpecialLinearGroup n R) → GL n R) g : GL n R)
      ((toGL : (a : SpecialLinearGroup n R) → GL n R) g' : GL n R) →
    g = g'

Tactic:
simpa [toGL] using fun h _ ↦ Subtype.ext h

Premises used: Matrix.SpecialLinearGroup.toGL, Subtype.ext
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
g g' : SpecialLinearGroup n R
⊢ Eq (α := GL n R) ((toGL : (a : SpecialLinearGroup n R) → GL n R) g : GL n R)
      ((toGL : (a : SpecialLinearGroup n R) → GL n R) g' : GL n R) ↔
    g = g'

Tactic:
toGL_injective.eq_iff

Premises used: Function.Injective.eq_iff, Matrix.SpecialLinearGroup.toGL_injective
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
g : SpecialLinearGroup n R
⊢ Eq.{v + 1} (α := Rˣ)
    ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) ((toGL : (a : SpecialLinearGroup n R) → GL n R) g) : Rˣ) (1 : Rˣ)

Tactic:
Units.ext g.prop

Premises used: Units.ext, Subtype.prop
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
g : SpecialLinearGroup n R
⊢ (↑((toGL : (a : SpecialLinearGroup n R) → GL n R) g) : Matrix n n R) = (↑g : Matrix n n R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FaithfulSMul R S
g g' : SpecialLinearGroup n R
⊢ Eq (α := GL n S) ((mapGL S : (a : SpecialLinearGroup n R) → GL n S) g : GL n S)
      ((mapGL S : (a : SpecialLinearGroup n R) → GL n S) g' : GL n S) ↔
    g = g'

Tactic:
simp [mapGL, ext_iff]

Premises used: Matrix.SpecialLinearGroup.ext_iff, Matrix.SpecialLinearGroup.mapGL
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FaithfulSMul R S
a b : SpecialLinearGroup n R
⊢ Eq (α := GL n S) ((mapGL S : (a : SpecialLinearGroup n R) → GL n S) a : GL n S)
      ((mapGL S : (a : SpecialLinearGroup n R) → GL n S) b : GL n S) →
    a = b

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
g : SpecialLinearGroup n R
⊢ Eq (α := Matrix n n S) (↑((mapGL S : (a : SpecialLinearGroup n R) → GL n S) g) : Matrix n n S)
    (↑((map (algebraMap R S) : (a : SpecialLinearGroup n R) → SpecialLinearGroup n S) g) : Matrix n n S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
T : Type u_2
inst_5 : CommRing T
inst_6 : Algebra R T
inst_7 : Algebra S T
inst_8 : IsScalarTower R S T
g : SpecialLinearGroup n R
huv :
  ∀ (i j : n),
    Eq.{u_2 + 1} (α := T)
      ((↑((GeneralLinearGroup.map (algebraMap S T) : (a : GL n S) → GL n T)
              ((mapGL S : (a : SpecialLinearGroup n R) → GL n S) g)) :
          Matrix n n T)
        i j)
      ((↑((mapGL T : (a : SpecialLinearGroup n R) → GL n T) g) : Matrix n n T) i j)
⊢ Eq (α := GL n T)
    ((GeneralLinearGroup.map (algebraMap S T) : (a : GL n S) → GL n T)
        ((mapGL S : (a : SpecialLinearGroup n R) → GL n S) g) :
      GL n T)
    ((mapGL T : (a : SpecialLinearGroup n R) → GL n T) g : GL n T)

Tactic:
ext