awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
inst : CommRing R
inst_1 : DecidableEq n
inst_2 : Fintype n
inst_3 : IsDomain R
M : Matrix n n R
h : M.det ≠ 0
⊢ SeparatingLeft (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := n → R) (M₂ := n → R) (I₁ := RingHom.id R) (I₂ :=
    RingHom.id R)
    (((toLinearMap₂' R : Matrix n n R ≃ₗ[R] (n → R) →ₗ[R] (n → R) →ₗ[R] R) :
        (a : Matrix n n R) → (n → R) →ₗ[R] (n → R) →ₗ[R] R)
      M)

Tactic:
separatingLeft_toLinearMap₂'_iff_det_ne_zero.mpr h

Premises used: Iff.mpr, LinearMap.separatingLeft_toLinearMap₂'_iff_det_ne_zero
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
inst : CommRing R
inst_1 : DecidableEq n
inst_2 : Fintype n
inst_3 : IsDomain R
M : Matrix n n R
h : M.det ≠ 0
⊢ SeparatingRight (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := n → R) (M₂ := n → R) (I₁ := RingHom.id R) (I₂ :=
    RingHom.id R)
    (((toLinearMap₂' R : Matrix n n R ≃ₗ[R] (n → R) →ₗ[R] (n → R) →ₗ[R] R) :
        (a : Matrix n n R) → (n → R) →ₗ[R] (n → R) →ₗ[R] R)
      M)

Tactic:
separatingRight_toLinearMap₂'_iff_det_ne_zero.mpr h

Premises used: Iff.mpr, LinearMap.separatingRight_toLinearMap₂'_iff_det_ne_zero
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
inst : CommRing R
inst_1 : DecidableEq n
inst_2 : Fintype n
inst_3 : IsDomain R
M : Matrix n n R
h : M.det ≠ 0
⊢ Nondegenerate (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := n → R) (M₂ := n → R) (I₁ := RingHom.id R) (I₂ :=
    RingHom.id R)
    (((toLinearMap₂' R : Matrix n n R ≃ₗ[R] (n → R) →ₗ[R] (n → R) →ₗ[R] R) :
        (a : Matrix n n R) → (n → R) →ₗ[R] (n → R) →ₗ[R] R)
      M)

Tactic:
nondegenerate_toLinearMap₂'_iff_det_ne_zero.mpr h

Premises used: Iff.mpr, LinearMap.nondegenerate_toLinearMap₂'_iff_det_ne_zero
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : IsDomain R
inst_4 : AddCommMonoid M₁
inst_5 : Module R M₁
b : Basis m R M₁
B : M₁ →ₗ[R] M₁ →ₗ[R] R
rw :
  B.SeparatingLeft ↔
    Matrix.SeparatingLeft.{u_12, u_12, u_1} (m := m) (n := m) (R := R)
      ((toMatrix₂ b b : (a : M₁ →ₗ[R] M₁ →ₗ[R] R) → Matrix m m R) B)
rw₁ rw₂ : B.SeparatingLeft ↔ B.SeparatingLeft
⊢ B.SeparatingLeft ↔
    Ne.{u_1 + 1} (α := R) (det.{u_1, u_12} (n := m) ((toMatrix₂ b b : (a : M₁ →ₗ[R] M₁ →ₗ[R] R) → Matrix m m R) B)) 0

Tactic:
rw [← Matrix.separatingLeft_iff_det_ne_zero, separatingLeft_toMatrix₂_iff]

Premises used: Matrix.separatingLeft_iff_det_ne_zero, LinearMap.separatingLeft_toMatrix₂_iff
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : IsDomain R
inst_4 : AddCommMonoid M₁
inst_5 : Module R M₁
b : Basis m R M₁
B : M₁ →ₗ[R] M₁ →ₗ[R] R
h : Ne.{u_1 + 1} (α := R) (det.{u_1, u_12} (n := m) ((toMatrix₂ b b : (a : M₁ →ₗ[R] M₁ →ₗ[R] R) → Matrix m m R) B)) 0
⊢ B.SeparatingLeft

Tactic:
(separatingLeft_iff_det_ne_zero b).mpr h

Premises used: Iff.mpr, LinearMap.separatingLeft_iff_det_ne_zero
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : IsDomain R
inst_4 : AddCommMonoid M₁
inst_5 : Module R M₁
b : Basis m R M₁
B : M₁ →ₗ[R] M₁ →ₗ[R] R
rw :
  B.SeparatingRight ↔
    Matrix.SeparatingRight.{u_12, u_12, u_1} (m := m) (n := m) (R := R)
      ((toMatrix₂ b b : (a : M₁ →ₗ[R] M₁ →ₗ[R] R) → Matrix m m R) B)
rw₁ rw₂ : B.SeparatingRight ↔ B.SeparatingRight
⊢ B.SeparatingRight ↔
    Ne.{u_1 + 1} (α := R) (det.{u_1, u_12} (n := m) ((toMatrix₂ b b : (a : M₁ →ₗ[R] M₁ →ₗ[R] R) → Matrix m m R) B)) 0

Tactic:
rw [← Matrix.separatingRight_iff_det_ne_zero, separatingRight_toMatrix₂_iff]

Premises used: Matrix.separatingRight_iff_det_ne_zero, LinearMap.separatingRight_toMatrix₂_iff
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : IsDomain R
inst_4 : AddCommMonoid M₁
inst_5 : Module R M₁
b : Basis m R M₁
B : M₁ →ₗ[R] M₁ →ₗ[R] R
h : Ne.{u_1 + 1} (α := R) (det.{u_1, u_12} (n := m) ((toMatrix₂ b b : (a : M₁ →ₗ[R] M₁ →ₗ[R] R) → Matrix m m R) B)) 0
⊢ B.SeparatingRight

Tactic:
(separatingRight_iff_det_ne_zero b).mpr h

Premises used: Iff.mpr, LinearMap.separatingRight_iff_det_ne_zero
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : IsDomain R
inst_4 : AddCommMonoid M₁
inst_5 : Module R M₁
b : Basis m R M₁
B : M₁ →ₗ[R] M₁ →ₗ[R] R
rw :
  B.Nondegenerate ↔
    Matrix.Nondegenerate.{u_12, u_12, u_1} (m := m) (n := m) (R := R)
      ((toMatrix₂ b b : (a : M₁ →ₗ[R] M₁ →ₗ[R] R) → Matrix m m R) B)
rw₁ rw₂ : B.Nondegenerate ↔ B.Nondegenerate
⊢ B.Nondegenerate ↔
    Ne.{u_1 + 1} (α := R) (det.{u_1, u_12} (n := m) ((toMatrix₂ b b : (a : M₁ →ₗ[R] M₁ →ₗ[R] R) → Matrix m m R) B)) 0

Tactic:
rw [← Matrix.nondegenerate_iff_det_ne_zero, nondegenerate_toMatrix₂_iff]

Premises used: LinearMap.nondegenerate_toMatrix₂_iff, Matrix.nondegenerate_iff_det_ne_zero
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : IsDomain R
inst_4 : AddCommMonoid M₁
inst_5 : Module R M₁
b : Basis m R M₁
B : M₁ →ₗ[R] M₁ →ₗ[R] R
h : Ne.{u_1 + 1} (α := R) (det.{u_1, u_12} (n := m) ((toMatrix₂ b b : (a : M₁ →ₗ[R] M₁ →ₗ[R] R) → Matrix m m R) B)) 0
⊢ B.Nondegenerate

Tactic:
(nondegenerate_iff_det_ne_zero b).mpr h

Premises used: Iff.mpr, LinearMap.nondegenerate_iff_det_ne_zero
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A B : SpecialLinearGroup n R
⊢ A = B ↔ ∀ (i j : n), (↑A : Matrix n n R) i j = (↑B : Matrix n n R) i j

Tactic:
Subtype.ext_iff.trans Matrix.ext_iff.symm

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

Tactic:
(SpecialLinearGroup.ext_iff A B).mpr

Premises used: Iff.mpr, Matrix.SpecialLinearGroup.ext_iff
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : Subsingleton n
⊢ Subsingleton (SpecialLinearGroup n R)

Tactic:
⟨fun ⟨A, hA⟩ ⟨B, hB⟩ ↦ ?_⟩

Premises used: _private.0.Matrix.SpecialLinearGroup.subsingleton_of_subsingleton.match_1, Subtype.mk, Subsingleton.intro, Eq
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : Subsingleton n
refine :
  ∀ (x x : SpecialLinearGroup n R) (A : Matrix n n R) (hA : A.det = 1) (B : Matrix n n R) (hB : B.det = 1),
    Eq (α := SpecialLinearGroup n R) (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) A hA)
      (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) B hB)
⊢ Subsingleton (SpecialLinearGroup n R)

Tactic:
refine ⟨fun ⟨A, hA⟩ ⟨B, hB⟩ ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : Subsingleton n
x x_1 : SpecialLinearGroup n R
A : Matrix n n R
hA : A.det = 1
B : Matrix n n R
hB : B.det = 1
a :
  ∀ (i j : n),
    (↑(Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) A hA) : Matrix n n R) i j =
      (↑(Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) B hB) : Matrix n n R) i j
⊢ Eq (α := SpecialLinearGroup n R) (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) A hA)
    (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) B hB)

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : Subsingleton n
x x_1 : SpecialLinearGroup n R
A : Matrix n n R
hA : A.det = 1
B : Matrix n n R
hB : B.det = 1
i j : n
a :
  ∀ (hn : IsEmpty n),
    (↑(Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) A hA) : Matrix n n R) i j =
      (↑(Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) B hB) : Matrix n n R) i j
a₁ :
  ∀ (hn : Nonempty n),
    (↑(Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) A hA) : Matrix n n R) i j =
      (↑(Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) B hB) : Matrix n n R) i j
⊢ (↑(Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) A hA) : Matrix n n R) i j =
    (↑(Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) B hB) : Matrix n n R) i j

Tactic:
rcases isEmpty_or_nonempty n with hn | hn

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : Subsingleton n
x x_1 : SpecialLinearGroup n R
A : Matrix n n R
hA : A.det = 1
B : Matrix n n R
hB : B.det = 1
i j : n
hn : IsEmpty n
a : False
⊢ (↑(Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) A hA) : Matrix n n R) i j =
    (↑(Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) B hB) : Matrix n n R) i j

Tactic:
exfalso
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : Subsingleton n
x x_1 : SpecialLinearGroup n R
A : Matrix n n R
hA : A.det = 1
B : Matrix n n R
hB : B.det = 1
i j : n
hn : IsEmpty n
⊢ False

Tactic:
IsEmpty.false i

Premises used: IsEmpty.false
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : Subsingleton n
x x_1 : SpecialLinearGroup n R
A : Matrix n n R
hA : A.det = 1
B : Matrix n n R
hB : B.det = 1
i j : n
hn : IsEmpty n
⊢ False

Tactic:
exact IsEmpty.false i

Premises used: IsEmpty.false
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : Subsingleton n
x x_1 : SpecialLinearGroup n R
A : Matrix n n R
hA : A.det = 1
B : Matrix n n R
hB : B.det = 1
i j : n
hn : Nonempty n
a :
  ∀ (hB_1 : B i i = 1) (hA_1 : A i i = 1) (j : n) (hn : Nonempty n),
    (↑(Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) A hA) : Matrix n n R) i j =
      (↑(Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) B hB) : Matrix n n R) i j
⊢ (↑(Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) A hA) : Matrix n n R) i j =
    (↑(Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) B hB) : Matrix n n R) i j

Tactic:
rw [det_eq_elem_of_subsingleton _ i] at hA hB

Premises used: Matrix.det_eq_elem_of_subsingleton
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : Subsingleton n
x x_1 : SpecialLinearGroup n R
A : Matrix n n R
hA_1 : A.det = 1
B : Matrix n n R
hB_1 : B.det = 1
i : n
hB : B i i = 1
hA : A i i = 1
j : n
hn : Nonempty n
⊢ (↑(Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) A hA_1) : Matrix n n R) i j =
    (↑(Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) B hB_1) : Matrix n n R) i j

Tactic:
simp only [Subsingleton.elim j i, hA, hB]

Premises used: Subsingleton.elim
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
rw : (↑A : Matrix n n R).det ^ (Fintype.card n - 1) = 1
rw₁ : HPow.hPow (α := R) 1 (Fintype.card n - 1) = 1
rw₂ rw₃ : Eq.{v + 1} (α := R) 1 1
⊢ (↑A : Matrix n n R).adjugate.det = 1

Tactic:
rw [det_adjugate, A.prop, one_pow]

Premises used: one_pow, Matrix.det_adjugate, Subtype.prop
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A B : SpecialLinearGroup n R
rw : (↑A : Matrix n n R).det * (↑B : Matrix n n R).det = 1
rw₁ : 1 * (↑B : Matrix n n R).det = 1
rw₂ : HMul.hMul (α := R) 1 1 = 1
rw₃ rw₄ : Eq.{v + 1} (α := R) 1 1
⊢ ((↑A : Matrix n n R) * (↑B : Matrix n n R)).det = 1

Tactic:
rw [det_mul, A.prop, B.prop, one_mul]

Premises used: Matrix.det_mul, Subtype.prop, one_mul
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : Finite R
⊢ Finite (SpecialLinearGroup n R)

Tactic:
Subtype.finite

Premises used: Matrix.SpecialLinearGroup, Subtype.finite
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : Matrix n n R
h : A.det = 1
⊢ (↑(Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1) A h) : Matrix n n R) = A

Tactic:
rfl

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

Tactic:
rfl

Premises used: Matrix.adjugate, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A B : SpecialLinearGroup 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.SpecialLinearGroup
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.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
⊢ (↑A : Matrix n n R).det = 1

Tactic:
A.2

Premises used: Subtype.property
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
m : ℕ
⊢ (↑(A ^ m) : Matrix n n R) = (↑A : Matrix n n R) ^ m

Tactic:
rfl

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

Tactic:
rfl

Premises used: Matrix.transpose, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : Nontrivial R
g : SpecialLinearGroup n R
rw : Ne.{v + 1} (α := R) 1 0
⊢ (↑g : Matrix n n R).det ≠ 0

Tactic:
rw [g.det_coe]

Premises used: Matrix.SpecialLinearGroup.det_coe
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : Nontrivial R
g : SpecialLinearGroup n R
⊢ Ne.{v + 1} (α := R) 1 0

Tactic:
norm_num
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : Nontrivial R
g : SpecialLinearGroup n R
i : n
h : (↑g : Matrix n n R) i = 0
⊢ ∀ (j : n), (↑g : Matrix n n R) i j = 0

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
a : ∀ (i j : n), (↑(A⁻¹ * A) : Matrix n n R) i j = (↑1 : Matrix n n R) i j
⊢ A⁻¹ * A = 1

Tactic:
ext1
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
i j : n
⊢ (↑(A⁻¹ * A) : Matrix n n R) i j = (↑1 : Matrix n n R) i j

Tactic:
simp [adjugate_mul]

Premises used: Matrix.adjugate_mul
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
rw :
  Eq (α := (n → R) →ₗ[R] n → R)
    ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) ((↑A : Matrix n n R) * (↑A⁻¹ : Matrix n n R)) :
      (n → R) →ₗ[R] n → R)
    (LinearMap.id : (n → R) →ₗ[R] n → R)
rw₁ :
  Eq (α := (n → R) →ₗ[R] n → R)
    ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑(A * A⁻¹) : Matrix n n R) : (n → R) →ₗ[R] n → R)
    (LinearMap.id : (n → R) →ₗ[R] n → R)
rw₂ :
  Eq (α := (n → R) →ₗ[R] n → R) ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑1 : Matrix n n R))
    LinearMap.id
rw₃ : Eq (α := (n → R) →ₗ[R] n → R) ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) 1) LinearMap.id
rw₄ rw₅ : Eq (α := (n → R) →ₗ[R] n → R) LinearMap.id LinearMap.id
⊢ Eq (α := (n → R) →ₗ[R] n → R)
    ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑A : Matrix n n R) ∘ₗ
      (Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑A⁻¹ : Matrix n n R))
    LinearMap.id

Tactic:
rw [← toLin'_mul, ← coe_mul, mul_inv_cancel, coe_one, toLin'_one]

Premises used: Matrix.SpecialLinearGroup.coe_one, Matrix.toLin'_mul, Matrix.toLin'_one, mul_inv_cancel, Matrix.SpecialLinearGroup.coe_mul
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
rw :
  Eq (α := (n → R) →ₗ[R] n → R)
    ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) ((↑A⁻¹ : Matrix n n R) * (↑A : Matrix n n R)) :
      (n → R) →ₗ[R] n → R)
    (LinearMap.id : (n → R) →ₗ[R] n → R)
rw₁ :
  Eq (α := (n → R) →ₗ[R] n → R)
    ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑(A⁻¹ * A) : Matrix n n R) : (n → R) →ₗ[R] n → R)
    (LinearMap.id : (n → R) →ₗ[R] n → R)
rw₂ :
  Eq (α := (n → R) →ₗ[R] n → R) ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑1 : Matrix n n R))
    LinearMap.id
rw₃ : Eq (α := (n → R) →ₗ[R] n → R) ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) 1) LinearMap.id
rw₄ rw₅ : Eq (α := (n → R) →ₗ[R] n → R) LinearMap.id LinearMap.id
⊢ Eq (α := (n → R) →ₗ[R] n → R)
    ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑A⁻¹ : Matrix n n R) ∘ₗ
      (Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑A : Matrix n n R))
    LinearMap.id

Tactic:
rw [← toLin'_mul, ← coe_mul, inv_mul_cancel, coe_one, toLin'_one]

Premises used: inv_mul_cancel, Matrix.SpecialLinearGroup.coe_one, Matrix.toLin'_mul, Matrix.toLin'_one, Matrix.SpecialLinearGroup.coe_mul
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
v : n → R
⊢ Eq (α := n → R)
    ((((toLin' : (a : SpecialLinearGroup n R) → (n → R) ≃ₗ[R] n → R) A : (n → R) ≃ₗ[R] n → R) : (a : n → R) → n → R) v :
      n → R)
    ((((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑A : Matrix n n R) : (n → R) →ₗ[R] n → R) :
          (a : n → R) → n → R)
        v :
      n → R)

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
v : n → R
⊢ Eq (α := n → R)
    ((LinearEquiv.symm ((toLin' : (a : SpecialLinearGroup n R) → (n → R) ≃ₗ[R] n → R) A) : (a : n → R) → n → R) v :
      n → R)
    ((((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑A⁻¹ : Matrix n n R) : (n → R) →ₗ[R] n → R) :
          (a : n → R) → n → R)
        v :
      n → R)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Matrix.mulVec, Finset.sum, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
⊢ Eq (α := (n → R) →ₗ[R] n → R)
    (↑(LinearEquiv.symm ((toLin' : (a : SpecialLinearGroup n R) → (n → R) ≃ₗ[R] n → R) A)) : (n → R) →ₗ[R] n → R)
    ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (↑A⁻¹ : Matrix n n R))

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Matrix.mulVec, Finset.sum, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
⊢ Function.Injective (α := SpecialLinearGroup n R) (β := (n → R) ≃ₗ[R] n → R)
    (⇑toLin' : (a : SpecialLinearGroup n R) → (n → R) ≃ₗ[R] n → R)

Tactic:
fun _ _ h =>
  Subtype.coe_injective <| Matrix.toLin'.injective <| LinearEquiv.toLinearMap_injective.eq_iff.mpr h

Premises used: Iff.mpr, Matrix.SpecialLinearGroup, Function.Injective.eq_iff, Matrix.toLin', LinearEquiv.toLinearMap_injective, Subtype.coe_injective, Function.Injective, LinearEquiv.injective
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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 : SpecialLinearGroup n R
rw : Eq.{u_1 + 1} (α := S) ((f : (a : R) → S) (↑g : Matrix n n R).det : S) (1 : S)
⊢ Eq.{u_1 + 1} (α := S) (det.{u_1, u} (n := n) ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) (↑g : Matrix n n R)))
    1

Tactic:
rw [← f.map_det]

Premises used: RingHom.map_det
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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 : SpecialLinearGroup n R
⊢ Eq.{u_1 + 1} (α := S) ((f : (a : R) → S) (↑g : Matrix n n R).det : S) (1 : S)

Tactic:
simp [g.prop]

Premises used: Subtype.prop
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : Subsingleton n
x : SpecialLinearGroup n R
h : Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) x
rw : x = 1
rw₁ rw₂ : Eq (α := SpecialLinearGroup n R) 1 1
⊢ Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) ⊥ x

Tactic:
rw [mem_bot, Subsingleton.elim x 1]

Premises used: Subsingleton.elim, OfNat.ofNat, Subgroup.mem_bot
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
hA : Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) A
i : n
t : TransvectionStruct n R
⊢ t.toMatrix.det = 1

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
hA : Membership.mem (γ := Subgroup (SpecialLinearGroup n R)) (center (SpecialLinearGroup n R)) A
i : n
obtain :
  ∀ (r : R) (hr : (scalar n : (a : R) → Matrix n n R) r = (↑A : Matrix n n R)),
    (scalar n : (a : R) → Matrix n n R) ((↑A : Matrix n n R) i i) = (↑A : Matrix n n R)
⊢ (scalar n : (a : R) → Matrix n n R) ((↑A : Matrix n n R) i i) = (↑A : Matrix n n R)

Tactic:
obtain ⟨r : R, hr : scalar n r = A⟩ := mem_range_scalar_of_commute_transvectionStruct fun t ↦
    Subtype.ext_iff.mp <| Subgroup.mem_center_iff.mp hA ⟨t.toMatrix, by simp⟩

Premises used: Matrix.TransvectionStruct.toMatrix, Subgroup.mem_center_iff, Subtype.ext_iff, Subtype.mk, Iff.mp, Matrix.mem_range_scalar_of_commute_transvectionStruct