awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix m n R
⊢ SeparatingRight (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := m → R) (M₂ := n → R) (I₁ := RingHom.id R) (I₂ :=
      RingHom.id R)
      (((toLinearMap₂' R : Matrix m n R ≃ₗ[R] (m → R) →ₗ[R] (n → R) →ₗ[R] R) :
          (a : Matrix m n R) → (m → R) →ₗ[R] (n → R) →ₗ[R] R)
        M) ↔
    M.SeparatingRight
have refine : ∀
  (h :
    SeparatingRight (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := m → R) (M₂ := n → R) (I₁ := RingHom.id R) (I₂ :=
      RingHom.id R)
      (((toLinearMap₂' R : Matrix m n R ≃ₗ[R] (m → R) →ₗ[R] (n → R) →ₗ[R] R) :
          (a : Matrix m n R) → (m → R) →ₗ[R] (n → R) →ₗ[R] R)
        M))
  (w : n → R), (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0
Tactic: refine ⟨fun h ↦ separatingRight_def.mpr ?_, SeparatingRight.toLinearMap₂'⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix m n R
inst_5 : AddCommMonoid M₁
inst_6 : Module R M₁
inst_7 : AddCommMonoid M₂
inst_8 : Module R M₂
b₁ : Basis m R M₁
b₂ : Basis n R M₂
⊢ SeparatingLeft.{u_1, u_1, u_1, u_1, u_6, u_7} (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := M₁) (M₂ := M₂) (I₁ :=
      RingHom.id R) (I₂ := RingHom.id R) ((toLinearMap₂ b₁ b₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂ →ₗ[R] R) M) ↔
    M.SeparatingLeft
have rw : SeparatingLeft (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := m → R) (M₂ := n → R) (I₁ := RingHom.id R) (I₂ :=
    RingHom.id R)
    (((toLinearMap₂' R : Matrix m n R ≃ₗ[R] (m → R) →ₗ[R] (n → R) →ₗ[R] R) :
        (a : Matrix m n R) → (m → R) →ₗ[R] (n → R) →ₗ[R] R)
      M) ↔
  M.SeparatingLeft
Tactic: rw [← separatingLeft_toLinearMap₂'_iff_separatingLeft_toLinearMap₂,
    separatingLeft_toLinearMap₂'_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix m n R
inst_5 : AddCommMonoid M₁
inst_6 : Module R M₁
inst_7 : AddCommMonoid M₂
inst_8 : Module R M₂
b₁ : Basis m R M₁
b₂ : Basis n R M₂
rw :
  SeparatingLeft (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := m → R) (M₂ := n → R) (I₁ := RingHom.id R) (I₂ :=
      RingHom.id R)
      (((toLinearMap₂' R : Matrix m n R ≃ₗ[R] (m → R) →ₗ[R] (n → R) →ₗ[R] R) :
          (a : Matrix m n R) → (m → R) →ₗ[R] (n → R) →ₗ[R] R)
        M) ↔
    M.SeparatingLeft
⊢ SeparatingLeft.{u_1, u_1, u_1, u_1, u_6, u_7} (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := M₁) (M₂ := M₂) (I₁ :=
      RingHom.id R) (I₂ := RingHom.id R) ((toLinearMap₂ b₁ b₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂ →ₗ[R] R) M) ↔
    M.SeparatingLeft
have rw₁ : M.SeparatingLeft ↔ M.SeparatingLeft
Tactic: rw [← separatingLeft_toLinearMap₂'_iff_separatingLeft_toLinearMap₂,
    separatingLeft_toLinearMap₂'_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix m n R
inst_5 : AddCommMonoid M₁
inst_6 : Module R M₁
inst_7 : AddCommMonoid M₂
inst_8 : Module R M₂
b₁ : Basis m R M₁
b₂ : Basis n R M₂
⊢ SeparatingRight.{u_1, u_1, u_1, u_1, u_6, u_7} (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := M₁) (M₂ := M₂) (I₁ :=
      RingHom.id R) (I₂ := RingHom.id R) ((toLinearMap₂ b₁ b₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂ →ₗ[R] R) M) ↔
    M.SeparatingRight
have rw : SeparatingRight (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := m → R) (M₂ := n → R) (I₁ := RingHom.id R) (I₂ :=
    RingHom.id R)
    (((toLinearMap₂' R : Matrix m n R ≃ₗ[R] (m → R) →ₗ[R] (n → R) →ₗ[R] R) :
        (a : Matrix m n R) → (m → R) →ₗ[R] (n → R) →ₗ[R] R)
      M) ↔
  M.SeparatingRight
Tactic: rw [← separatingRight_toLinearMap₂'_iff_separatingRight_toLinearMap₂,
    separatingRight_toLinearMap₂'_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix m n R
inst_5 : AddCommMonoid M₁
inst_6 : Module R M₁
inst_7 : AddCommMonoid M₂
inst_8 : Module R M₂
b₁ : Basis m R M₁
b₂ : Basis n R M₂
rw :
  SeparatingRight (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := m → R) (M₂ := n → R) (I₁ := RingHom.id R) (I₂ :=
      RingHom.id R)
      (((toLinearMap₂' R : Matrix m n R ≃ₗ[R] (m → R) →ₗ[R] (n → R) →ₗ[R] R) :
          (a : Matrix m n R) → (m → R) →ₗ[R] (n → R) →ₗ[R] R)
        M) ↔
    M.SeparatingRight
⊢ SeparatingRight.{u_1, u_1, u_1, u_1, u_6, u_7} (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := M₁) (M₂ := M₂) (I₁ :=
      RingHom.id R) (I₂ := RingHom.id R) ((toLinearMap₂ b₁ b₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂ →ₗ[R] R) M) ↔
    M.SeparatingRight
have rw₁ : M.SeparatingRight ↔ M.SeparatingRight
Tactic: rw [← separatingRight_toLinearMap₂'_iff_separatingRight_toLinearMap₂,
    separatingRight_toLinearMap₂'_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix m n R
inst_5 : AddCommMonoid M₁
inst_6 : Module R M₁
inst_7 : AddCommMonoid M₂
inst_8 : Module R M₂
b₁ : Basis m R M₁
b₂ : Basis n R M₂
⊢ Nondegenerate.{u_1, u_1, u_1, u_1, u_6, u_7} (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := M₁) (M₂ := M₂) (I₁ :=
      RingHom.id R) (I₂ := RingHom.id R) ((toLinearMap₂ b₁ b₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂ →ₗ[R] R) M) ↔
    M.Nondegenerate
have rw : Nondegenerate (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := m → R) (M₂ := n → R) (I₁ := RingHom.id R) (I₂ :=
    RingHom.id R)
    (((toLinearMap₂' R : Matrix m n R ≃ₗ[R] (m → R) →ₗ[R] (n → R) →ₗ[R] R) :
        (a : Matrix m n R) → (m → R) →ₗ[R] (n → R) →ₗ[R] R)
      M) ↔
  M.Nondegenerate
Tactic: rw [← nondegenerate_toLinearMap₂'_iff_nondegenerate_toLinearMap₂,
    nondegenerate_toLinearMap₂'_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix m n R
inst_5 : AddCommMonoid M₁
inst_6 : Module R M₁
inst_7 : AddCommMonoid M₂
inst_8 : Module R M₂
b₁ : Basis m R M₁
b₂ : Basis n R M₂
rw :
  Nondegenerate (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := m → R) (M₂ := n → R) (I₁ := RingHom.id R) (I₂ :=
      RingHom.id R)
      (((toLinearMap₂' R : Matrix m n R ≃ₗ[R] (m → R) →ₗ[R] (n → R) →ₗ[R] R) :
          (a : Matrix m n R) → (m → R) →ₗ[R] (n → R) →ₗ[R] R)
        M) ↔
    M.Nondegenerate
⊢ Nondegenerate.{u_1, u_1, u_1, u_1, u_6, u_7} (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := M₁) (M₂ := M₂) (I₁ :=
      RingHom.id R) (I₂ := RingHom.id R) ((toLinearMap₂ b₁ b₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂ →ₗ[R] R) M) ↔
    M.Nondegenerate
have rw₁ : M.Nondegenerate ↔ M.Nondegenerate
Tactic: rw [← nondegenerate_toLinearMap₂'_iff_nondegenerate_toLinearMap₂,
    nondegenerate_toLinearMap₂'_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
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
⊢ 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) ↔
    M.det ≠ 0
have rw : M.Nondegenerate ↔ M.det ≠ 0
Tactic: rw [nondegenerate_toLinearMap₂'_iff, Matrix.nondegenerate_iff_det_ne_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
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
rw : M.Nondegenerate ↔ 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) ↔
    M.det ≠ 0
have rw₁ : M.det ≠ 0 ↔ M.det ≠ 0
Tactic: rw [nondegenerate_toLinearMap₂'_iff, Matrix.nondegenerate_iff_det_ne_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
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
⊢ 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
have 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)
Tactic: rw [← Matrix.separatingLeft_iff_det_ne_zero, separatingLeft_toMatrix₂_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
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)
⊢ 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
have rw₁ : B.SeparatingLeft ↔ B.SeparatingLeft
Tactic: rw [← Matrix.separatingLeft_iff_det_ne_zero, separatingLeft_toMatrix₂_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
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
⊢ 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
have 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)
Tactic: rw [← Matrix.separatingRight_iff_det_ne_zero, separatingRight_toMatrix₂_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
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)
⊢ 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
have rw₁ : B.SeparatingRight ↔ B.SeparatingRight
Tactic: rw [← Matrix.separatingRight_iff_det_ne_zero, separatingRight_toMatrix₂_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
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
⊢ 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
have 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)
Tactic: rw [← Matrix.nondegenerate_iff_det_ne_zero, nondegenerate_toMatrix₂_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
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)
⊢ 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
have rw₁ : B.Nondegenerate ↔ B.Nondegenerate
Tactic: rw [← Matrix.nondegenerate_iff_det_ne_zero, nondegenerate_toMatrix₂_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
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)
have 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)
Tactic: refine ⟨fun ⟨A, hA⟩ ⟨B, hB⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
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
⊢ 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)
have 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
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
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
⊢ (↑(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
have 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
Tactic: rcases isEmpty_or_nonempty n with hn | hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
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
⊢ (↑(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
have 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
Tactic: rcases isEmpty_or_nonempty n with hn | hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
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
⊢ (↑(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
have a : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
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
⊢ (↑(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
have 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
Tactic: rw [det_eq_elem_of_subsingleton _ i] at hA hB
Cleared hypotheses: j, hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
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).adjugate.det = 1
have rw : (↑A : Matrix n n R).det ^ (Fintype.card n - 1) = 1
Tactic: rw [det_adjugate, A.prop, one_pow]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
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
⊢ (↑A : Matrix n n R).adjugate.det = 1
have rw₁ : HPow.hPow (α := R) 1 (Fintype.card n - 1) = 1
Tactic: rw [det_adjugate, A.prop, one_pow]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
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
⊢ (↑A : Matrix n n R).adjugate.det = 1
have rw₂ : Eq.{v + 1} (α := R) 1 1
Tactic: rw [det_adjugate, A.prop, one_pow]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A B : SpecialLinearGroup n R
⊢ ((↑A : Matrix n n R) * (↑B : Matrix n n R)).det = 1
have rw : (↑A : Matrix n n R).det * (↑B : Matrix n n R).det = 1
Tactic: rw [det_mul, A.prop, B.prop, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
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
⊢ ((↑A : Matrix n n R) * (↑B : Matrix n n R)).det = 1
have rw₁ : 1 * (↑B : Matrix n n R).det = 1
Tactic: rw [det_mul, A.prop, B.prop, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
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
⊢ ((↑A : Matrix n n R) * (↑B : Matrix n n R)).det = 1
have rw₂ : HMul.hMul (α := R) 1 1 = 1
Tactic: rw [det_mul, A.prop, B.prop, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
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
⊢ ((↑A : Matrix n n R) * (↑B : Matrix n n R)).det = 1
have rw₃ : Eq.{v + 1} (α := R) 1 1
Tactic: rw [det_mul, A.prop, B.prop, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
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
⊢ (↑g : Matrix n n R).det ≠ 0
have rw : Ne.{v + 1} (α := R) 1 0
Tactic: rw [g.det_coe]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : SpecialLinearGroup n R
⊢ A⁻¹ * A = 1
have a : ∀ (i j : n), (↑(A⁻¹ * A) : Matrix n n R) i j = (↑1 : Matrix n n R) i j
Tactic: ext1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
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)
    ((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
have 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)
Tactic: rw [← toLin'_mul, ← coe_mul, mul_inv_cancel, coe_one, toLin'_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
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)
⊢ 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
have 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)
Tactic: rw [← toLin'_mul, ← coe_mul, mul_inv_cancel, coe_one, toLin'_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
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)
⊢ 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
have 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
Tactic: rw [← toLin'_mul, ← coe_mul, mul_inv_cancel, coe_one, toLin'_one]