awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
b' : Basis ι' R M
inst_3 : Fintype ι
inst_4 : Finite ι'
m : M
intro :
  ∀ (val : Fintype ι'),
    mulVec.{u_5, u_2, u_1} (n := ι) (b'.toMatrix (⇑b : (a : ι) → M))
        (⇑((b.repr : (a : M) → ι →₀ R) m : ι →₀ R) : (a : ι) → R) =
      (⇑((b'.repr : (a : M) → ι' →₀ R) m : ι' →₀ R) : (a : ι') → R)
⊢ mulVec.{u_5, u_2, u_1} (n := ι) (b'.toMatrix (⇑b : (a : ι) → M))
      (⇑((b.repr : (a : M) → ι →₀ R) m : ι →₀ R) : (a : ι) → R) =
    (⇑((b'.repr : (a : M) → ι' →₀ R) m : ι' →₀ R) : (a : ι') → R)

Tactic:
cases nonempty_fintype ι'

Premises used: nonempty_fintype
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
b' : Basis ι' R M
inst_3 : Fintype ι
inst_4 : Finite ι'
m : M
val : Fintype ι'
⊢ mulVec.{u_5, u_2, u_1} (n := ι) (b'.toMatrix (⇑b : (a : ι) → M))
      (⇑((b.repr : (a : M) → ι →₀ R) m : ι →₀ R) : (a : ι) → R) =
    (⇑((b'.repr : (a : M) → ι' →₀ R) m : ι' →₀ R) : (a : ι') → R)

Tactic:
simp [← LinearMap.toMatrix_id_eq_basis_toMatrix, LinearMap.toMatrix_mulVec_repr]

Premises used: LinearMap.toMatrix_mulVec_repr, LinearMap.toMatrix_id_eq_basis_toMatrix
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
b' : Basis ι' R M
inst_3 : Fintype ι
inst_4 : Finite ι'
m : M
intro :
  ∀ (val : Fintype ι'),
    mulVec.{u_5, u_2, u_1} (n := ι) (b'.toMatrix (⇑b : (a : ι) → M))
        (⇑((b.repr : (a : M) → ι →₀ R) m : ι →₀ R) : (a : ι) → R) =
      (⇑((b'.repr : (a : M) → ι' →₀ R) m : ι' →₀ R) : (a : ι') → R)
⊢ mulVec.{u_5, u_2, u_1} (n := ι) (b'.toMatrix (⇑b : (a : ι) → M))
      (⇑((b.repr : (a : M) → ι →₀ R) m : ι →₀ R) : (a : ι) → R) =
    (⇑((b'.repr : (a : M) → ι' →₀ R) m : ι' →₀ R) : (a : ι') → R)

Tactic:
classical
  cases nonempty_fintype ι'
  simp [← LinearMap.toMatrix_id_eq_basis_toMatrix, LinearMap.toMatrix_mulVec_repr]

Premises used: LinearMap.toMatrix_mulVec_repr, nonempty_fintype, LinearMap.toMatrix_id_eq_basis_toMatrix
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
b' : Basis ι' R M
ι'' : Type u_10
inst_3 : Fintype ι'
b'' : ι'' → M
haveI :
  ∀ (this : DecidableEq ι),
    HMul.hMul (α := Matrix ι ι' R) (b.toMatrix (⇑b' : (a : ι') → M)) (b'.toMatrix b'') = b.toMatrix b''
⊢ HMul.hMul (α := Matrix ι ι' R) (b.toMatrix (⇑b' : (a : ι') → M)) (b'.toMatrix b'') = b.toMatrix b''

Tactic:
haveI := Classical.decEq ι
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
b' : Basis ι' R M
ι'' : Type u_10
inst_3 : Fintype ι'
b'' : ι'' → M
this : DecidableEq ι
haveI :
  ∀ (this : DecidableEq ι'),
    HMul.hMul (α := Matrix ι ι' R) (b.toMatrix (⇑b' : (a : ι') → M)) (b'.toMatrix b'') = b.toMatrix b''
⊢ HMul.hMul (α := Matrix ι ι' R) (b.toMatrix (⇑b' : (a : ι') → M)) (b'.toMatrix b'') = b.toMatrix b''

Tactic:
haveI := Classical.decEq ι'
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
b' : Basis ι' R M
ι'' : Type u_10
inst_3 : Fintype ι'
b'' : ι'' → M
this_1 : DecidableEq ι
this : DecidableEq ι'
haveI :
  ∀ (this : DecidableEq ι''),
    HMul.hMul (α := Matrix ι ι' R) (b.toMatrix (⇑b' : (a : ι') → M)) (b'.toMatrix b'') = b.toMatrix b''
⊢ HMul.hMul (α := Matrix ι ι' R) (b.toMatrix (⇑b' : (a : ι') → M)) (b'.toMatrix b'') = b.toMatrix b''

Tactic:
haveI := Classical.decEq ι''
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
b' : Basis ι' R M
ι'' : Type u_10
inst_3 : Fintype ι'
b'' : ι'' → M
this_1 : DecidableEq ι
this_2 : DecidableEq ι'
this : DecidableEq ι''
a :
  ∀ (i : ι) (j : ι''),
    HMul.hMul (α := Matrix ι ι' R) (b.toMatrix (⇑b' : (a : ι') → M)) (b'.toMatrix b'') i j = b.toMatrix b'' i j
⊢ HMul.hMul (α := Matrix ι ι' R) (b.toMatrix (⇑b' : (a : ι') → M)) (b'.toMatrix b'') = b.toMatrix b''

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
b' : Basis ι' R M
ι'' : Type u_10
inst_3 : Fintype ι'
b'' : ι'' → M
this_1 : DecidableEq ι
this_2 : DecidableEq ι'
this : DecidableEq ι''
i : ι
j : ι''
⊢ HMul.hMul (α := Matrix ι ι' R) (b.toMatrix (⇑b' : (a : ι') → M)) (b'.toMatrix b'') i j = b.toMatrix b'' i j

Tactic:
simp only [Matrix.mul_apply, toMatrix_apply, sum_repr_mul_repr]

Premises used: Matrix.mul_apply, Module.Basis.sum_repr_mul_repr, Module.Basis.toMatrix_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
b' : Basis ι' R M
inst_3 : DecidableEq ι
inst_4 : Fintype ι'
rw : Eq (α := Matrix ι ι R) (b.toMatrix (⇑b : (a : ι) → M)) 1
rw₁ rw₂ : Eq (α := Matrix ι ι R) 1 1
⊢ HMul.hMul (α := Matrix ι ι' R) (β := Matrix ι' ι R) (b.toMatrix (⇑b' : (a : ι') → M))
      (b'.toMatrix (⇑b : (a : ι) → M)) =
    1

Tactic:
rw [toMatrix_mul_toMatrix, toMatrix_self]

Premises used: Module.Basis.toMatrix_self, Module.Basis.toMatrix_mul_toMatrix
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
a : ∀ (i j : ι'), (b.reindex e).toMatrix v i j = (b.toMatrix v).submatrix (⇑e.symm : (a : ι') → ι) _root_.id i j
⊢ (b.reindex e).toMatrix v = (b.toMatrix v).submatrix (⇑e.symm : (a : ι') → ι) _root_.id

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
i j : ι'
⊢ (b.reindex e).toMatrix v i j = (b.toMatrix v).submatrix (⇑e.symm : (a : ι') → ι) _root_.id i j

Tactic:
simp only [toMatrix_apply, repr_reindex, Matrix.submatrix_apply, _root_.id,
    Finsupp.mapDomain_equiv_apply]

Premises used: id, Module.Basis.repr_reindex, Module.Basis.toMatrix_apply, Finsupp.mapDomain_equiv_apply, Matrix.submatrix_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
b : Basis ι R M
f : M ≃ₗ[R] N
v : ι → N
a : ∀ (i j : ι), (b.map f).toMatrix v i j = b.toMatrix ((⇑f.symm : (a : N) → M) ∘ v) i j
⊢ (b.map f).toMatrix v = b.toMatrix ((⇑f.symm : (a : N) → M) ∘ v)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
b : Basis ι R M
f : M ≃ₗ[R] N
v : ι → N
i j : ι
⊢ (b.map f).toMatrix v i j = b.toMatrix ((⇑f.symm : (a : N) → M) ∘ v) i j

Tactic:
simp only [toMatrix_apply, Basis.map, LinearEquiv.trans_apply, (· ∘ ·)]

Premises used: Module.Basis.map, Function.comp, LinearEquiv.trans_apply, Module.Basis.toMatrix_apply
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
inst : CommSemiring R₁
n : Type u_5
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R₁
i j : n
⊢ (((M.toBilin'Aux : (a : n → R₁) → (n → R₁) →ₗ[R₁] R₁) (Pi.single (M := fun (a : n) ↦ R₁) i 1) : (n → R₁) →ₗ[R₁] R₁) :
        (a : n → R₁) → R₁)
      (Pi.single (M := fun (a : n) ↦ R₁) j 1) =
    M i j

Tactic:
Matrix.toLinearMap₂'Aux_single _ _ _ _ _

Premises used: Matrix.toLinearMap₂'Aux_single
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
M₁ : Type u_2
inst : CommSemiring R₁
inst_1 : AddCommMonoid M₁
inst_2 : Module R₁ M₁
n : Type u_5
B : BilinForm R₁ M₁
b : n → M₁
i j : n
⊢ Eq.{u_1 + 1} (α := R₁) ((toMatrixAux b : (a : BilinForm R₁ M₁) → Matrix n n R₁) B i j : R₁)
    ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁) (b i) : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) (b j) : R₁)

Tactic:
LinearMap.toMatrix₂Aux_apply R₁ B _ _ _ _

Premises used: LinearMap.toMatrix₂Aux_apply
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
inst : CommSemiring R₁
n : Type u_5
inst_1 : Fintype n
inst_2 : DecidableEq n
B₂ : BilinForm R₁ (n → R₁)
rw :
  toBilin'Aux
      (((toMatrix₂Aux R₁ (fun (j : n) ↦ Pi.single (M := fun (j : n) ↦ R₁) j 1) fun (j : n) ↦
              Pi.single (M := fun (j : n) ↦ R₁) j 1 :
            (((j : n) → R₁) →ₗ[R₁] ((j : n) → R₁) →ₗ[R₁] R₁) →ₗ[R₁] Matrix n n R₁) :
          (a : BilinForm R₁ ((j : n) → R₁)) → Matrix n n R₁)
        B₂) =
    B₂
rw₁ :
  toLinearMap₂'Aux (RingHom.id R₁) (RingHom.id R₁)
      (((toMatrix₂Aux R₁ (fun (j : n) ↦ Pi.single (M := fun (j : n) ↦ R₁) j 1) fun (j : n) ↦
              Pi.single (M := fun (j : n) ↦ R₁) j 1 :
            (((j : n) → R₁) →ₗ[R₁] ((j : n) → R₁) →ₗ[R₁] R₁) →ₗ[R₁] Matrix n n R₁) :
          (a : BilinForm R₁ ((j : n) → R₁)) → Matrix n n R₁)
        B₂) =
    B₂
rw₂ rw₃ : B₂ = B₂
⊢ toBilin'Aux
      ((BilinForm.toMatrixAux fun (j : n) ↦ Pi.single (M := fun (j : n) ↦ R₁) j 1 :
          (a : BilinForm R₁ ((j : n) → R₁)) → Matrix n n R₁)
        B₂) =
    B₂

Tactic:
rw [BilinForm.toMatrixAux, Matrix.toBilin'Aux, toLinearMap₂'Aux_toMatrix₂Aux]

Premises used: LinearMap.BilinForm.toMatrixAux, Matrix.toBilin'Aux, LinearMap.toLinearMap₂'Aux_toMatrix₂Aux
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
inst : CommSemiring R₁
n : Type u_5
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R₁
⊢ Eq (α := BilinForm R₁ (n → R₁)) M.toBilin'Aux ((toBilin' : (a : Matrix n n R₁) → BilinForm R₁ (n → R₁)) M)

Tactic:
rfl

Premises used: LinearMap.mk₂'ₛₗ, Matrix.toLinearMap₂'Aux, rfl, Matrix.toBilin'Aux
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
inst : CommSemiring R₁
n : Type u_5
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R₁
x y : n → R₁
⊢ Eq.{u_1 + 1} (α := R₁) (∑ i : n, ∑ j : n, x i • y j • M i j) (∑ i : n, ∑ j : n, x i * M i j * y j)

Tactic:
simp only [smul_eq_mul, mul_comm, mul_left_comm]

Premises used: mul_left_comm, mul_comm, smul_eq_mul
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
inst : CommSemiring R₁
n : Type u_5
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R₁
v w : n → R₁
⊢ (((((toBilin' : (a : Matrix n n R₁) → BilinForm R₁ (n → R₁)) M : BilinForm R₁ (n → R₁)) :
              (a : n → R₁) → (n → R₁) →ₗ[R₁] R₁)
            v :
          (n → R₁) →ₗ[R₁] R₁) :
        (a : n → R₁) → R₁)
      w =
    v ⬝ᵥ M *ᵥ w

Tactic:
Matrix.toLinearMap₂'_apply' _ _ _

Premises used: Matrix.toLinearMap₂'_apply'
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
inst : CommSemiring R₁
n : Type u_5
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R₁
i j : n
⊢ (((((toBilin' : (a : Matrix n n R₁) → BilinForm R₁ (n → R₁)) M : BilinForm R₁ (n → R₁)) :
              (a : n → R₁) → (n → R₁) →ₗ[R₁] R₁)
            (Pi.single (M := fun (a : n) ↦ R₁) i 1) :
          (n → R₁) →ₗ[R₁] R₁) :
        (a : n → R₁) → R₁)
      (Pi.single (M := fun (a : n) ↦ R₁) j 1) =
    M i j

Tactic:
simp [Matrix.toBilin'_apply, Pi.single_apply]

Premises used: Pi.single_apply, Matrix.toBilin'_apply
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
inst : CommSemiring R₁
n : Type u_5
inst_1 : Fintype n
inst_2 : DecidableEq n
⊢ Eq (α := Matrix n n R₁ ≃ₗ[R₁] BilinForm R₁ (n → R₁)) (LinearEquiv.symm toMatrix') toBilin'

Tactic:
rfl

Premises used: Matrix.toBilin', rfl
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
inst : CommSemiring R₁
n : Type u_5
inst_1 : Fintype n
inst_2 : DecidableEq n
⊢ Eq (α := BilinForm R₁ (n → R₁) ≃ₗ[R₁] Matrix n n R₁) (LinearEquiv.symm toBilin') BilinForm.toMatrix'

Tactic:
BilinForm.toMatrix'.symm_symm

Premises used: Matrix.toBilin', LinearEquiv.symm_symm, LinearMap.BilinForm.toMatrix'
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
inst : CommSemiring R₁
n : Type u_5
inst_1 : Fintype n
inst_2 : DecidableEq n
B : BilinForm R₁ (n → R₁)
⊢ (toBilin' : (a : Matrix n n R₁) → BilinForm R₁ (n → R₁))
      ((BilinForm.toMatrix' : (a : BilinForm R₁ (n → R₁)) → Matrix n n R₁) B) =
    B

Tactic:
Matrix.toBilin'.apply_symm_apply B

Premises used: Matrix.toBilin', LinearEquiv.apply_symm_apply
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
inst : CommSemiring R₁
n : Type u_5
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R₁
⊢ (toMatrix' : (a : BilinForm R₁ (n → R₁)) → Matrix n n R₁)
      ((toBilin' : (a : Matrix n n R₁) → BilinForm R₁ (n → R₁)) M) =
    M

Tactic:
(LinearMap.toMatrix₂' R₁).apply_symm_apply M

Premises used: LinearMap.toMatrix₂', LinearEquiv.apply_symm_apply
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
inst : CommSemiring R₁
n : Type u_5
inst_1 : Fintype n
inst_2 : DecidableEq n
B : BilinForm R₁ (n → R₁)
i j : n
⊢ Eq.{u_1 + 1} (α := R₁) ((toMatrix' : (a : BilinForm R₁ (n → R₁)) → Matrix n n R₁) B i j : R₁)
    ((((B : (a : n → R₁) → (n → R₁) →ₗ[R₁] R₁) (Pi.single (M := fun (a : n) ↦ R₁) i 1) : (n → R₁) →ₗ[R₁] R₁) :
          (a : n → R₁) → R₁)
        (Pi.single (M := fun (a : n) ↦ R₁) j 1) :
      R₁)

Tactic:
LinearMap.toMatrix₂'_apply _ _ _

Premises used: LinearMap.toMatrix₂'_apply
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
inst : CommSemiring R₁
n : Type u_5
o : Type u_6
inst_1 : Fintype n
inst_2 : Fintype o
inst_3 : DecidableEq n
inst_4 : DecidableEq o
B : BilinForm R₁ (n → R₁)
l r : (o → R₁) →ₗ[R₁] n → R₁
⊢ (toMatrix' : (a : BilinForm R₁ (o → R₁)) → Matrix o o R₁) (B.comp l r) =
    HMul.hMul (β := Matrix n o R₁)
      (HMul.hMul (α := Matrix o n R₁) (β := Matrix n n R₁)
        ((LinearMap.toMatrix' : (a : (o → R₁) →ₗ[R₁] n → R₁) → Matrix n o R₁) l)ᵀ
        ((toMatrix' : (a : BilinForm R₁ (n → R₁)) → Matrix n n R₁) B : Matrix n n R₁))
      ((LinearMap.toMatrix' : (a : (o → R₁) →ₗ[R₁] n → R₁) → Matrix n o R₁) r : Matrix n o R₁)

Tactic:
B.toMatrix₂'_compl₁₂ _ _

Premises used: LinearMap.toMatrix₂'_compl₁₂
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
inst : CommSemiring R₁
n : Type u_5
inst_1 : Fintype n
inst_2 : DecidableEq n
B : BilinForm R₁ (n → R₁)
f : (n → R₁) →ₗ[R₁] n → R₁
⊢ (toMatrix' : (a : BilinForm R₁ (n → R₁)) → Matrix n n R₁) (B.compLeft f) =
    HMul.hMul (α := Matrix n n R₁) (β := Matrix n n R₁)
      ((LinearMap.toMatrix' : (a : (n → R₁) →ₗ[R₁] n → R₁) → Matrix n n R₁) f)ᵀ
      ((toMatrix' : (a : BilinForm R₁ (n → R₁)) → Matrix n n R₁) B : Matrix n n R₁)

Tactic:
B.toMatrix₂'_comp _

Premises used: Function.update, Pi.single, dite, LinearMap.toMatrix₂'_comp
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
inst : CommSemiring R₁
n : Type u_5
inst_1 : Fintype n
inst_2 : DecidableEq n
B : BilinForm R₁ (n → R₁)
f : (n → R₁) →ₗ[R₁] n → R₁
⊢ (toMatrix' : (a : BilinForm R₁ (n → R₁)) → Matrix n n R₁) (B.compRight f) =
    HMul.hMul (α := Matrix n n R₁) (β := Matrix n n R₁)
      ((toMatrix' : (a : BilinForm R₁ (n → R₁)) → Matrix n n R₁) B : Matrix n n R₁)
      ((LinearMap.toMatrix' : (a : (n → R₁) →ₗ[R₁] n → R₁) → Matrix n n R₁) f : Matrix n n R₁)

Tactic:
B.toMatrix₂'_compl₂ _

Premises used: Function.update, Pi.single, dite, LinearMap.toMatrix₂'_compl₂
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
inst : CommSemiring R₁
n : Type u_5
o : Type u_6
inst_1 : Fintype n
inst_2 : Fintype o
inst_3 : DecidableEq n
inst_4 : DecidableEq o
B : BilinForm R₁ (n → R₁)
M : Matrix o n R₁
N : Matrix n o R₁
⊢ HMul.hMul (β := Matrix n n R₁) M ((toMatrix' : (a : BilinForm R₁ (n → R₁)) → Matrix n n R₁) B : Matrix n n R₁) * N =
    (toMatrix' : (a : BilinForm R₁ (o → R₁)) → Matrix o o R₁)
      (B.comp ((toLin' : (a : Matrix n o R₁) → (o → R₁) →ₗ[R₁] n → R₁) Mᵀ)
        ((toLin' : (a : Matrix n o R₁) → (o → R₁) →ₗ[R₁] n → R₁) N))

Tactic:
B.mul_toMatrix₂'_mul _ _

Premises used: LinearMap.mul_toMatrix₂'_mul
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
inst : CommSemiring R₁
n : Type u_5
inst_1 : Fintype n
inst_2 : DecidableEq n
B : BilinForm R₁ (n → R₁)
M : Matrix n n R₁
⊢ HMul.hMul (β := Matrix n n R₁) M ((toMatrix' : (a : BilinForm R₁ (n → R₁)) → Matrix n n R₁) B : Matrix n n R₁) =
    (toMatrix' : (a : BilinForm R₁ (n → R₁)) → Matrix n n R₁)
      (B.compLeft ((toLin' : (a : Matrix n n R₁) → (n → R₁) →ₗ[R₁] n → R₁) Mᵀ))

Tactic:
LinearMap.mul_toMatrix' B _

Premises used: Function.update, Pi.single, LinearMap.mul_toMatrix', dite
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
inst : CommSemiring R₁
n : Type u_5
inst_1 : Fintype n
inst_2 : DecidableEq n
B : BilinForm R₁ (n → R₁)
M : Matrix n n R₁
⊢ HMul.hMul (α := Matrix n n R₁) ((toMatrix' : (a : BilinForm R₁ (n → R₁)) → Matrix n n R₁) B : Matrix n n R₁) M =
    (toMatrix' : (a : BilinForm R₁ (n → R₁)) → Matrix n n R₁)
      (B.compRight ((toLin' : (a : Matrix n n R₁) → (n → R₁) →ₗ[R₁] n → R₁) M))

Tactic:
B.toMatrix₂'_mul _

Premises used: Function.update, Pi.single, dite, LinearMap.toMatrix₂'_mul
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
inst : CommSemiring R₁
n : Type u_5
o : Type u_6
inst_1 : Fintype n
inst_2 : Fintype o
inst_3 : DecidableEq n
inst_4 : DecidableEq o
M : Matrix n n R₁
P Q : Matrix n o R₁
⊢ Eq (α := Matrix o o R₁)
    ((BilinForm.toMatrix' : (a : BilinForm R₁ (o → R₁)) → Matrix o o R₁)
        (BilinForm.comp (M' := n → R₁) ((toBilin' : (a : Matrix n n R₁) → BilinForm R₁ (n → R₁)) M)
          ((toLin' : (a : Matrix n o R₁) → (o → R₁) →ₗ[R₁] n → R₁) P)
          ((toLin' : (a : Matrix n o R₁) → (o → R₁) →ₗ[R₁] n → R₁) Q)) :
      Matrix o o R₁)
    ((BilinForm.toMatrix' : (a : BilinForm R₁ (o → R₁)) → Matrix o o R₁)
        ((toBilin' : (a : Matrix o o R₁) → BilinForm R₁ (o → R₁)) (Pᵀ * M * Q)) :
      Matrix o o R₁)

Tactic:
simp only [BilinForm.toMatrix'_comp, BilinForm.toMatrix'_toBilin', toMatrix'_toLin']

Premises used: LinearMap.toMatrix'_toLin', LinearMap.BilinForm.toMatrix'_comp, LinearMap.BilinForm.toMatrix'_toBilin'
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
M₁ : Type u_2
inst : CommSemiring R₁
inst_1 : AddCommMonoid M₁
inst_2 : Module R₁ M₁
n : Type u_5
inst_3 : Fintype n
inst_4 : DecidableEq n
b : Basis n R₁ M₁
B : BilinForm R₁ M₁
i j : n
⊢ Eq.{u_1 + 1} (α := R₁) ((toMatrix b : (a : BilinForm R₁ M₁) → Matrix n n R₁) B i j : R₁)
    ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁) ((b : (a : n) → M₁) i) : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁)
        ((b : (a : n) → M₁) j : M₁) :
      R₁)

Tactic:
LinearMap.toMatrix₂_apply _ _ B _ _

Premises used: LinearMap.toMatrix₂_apply
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
M₁ : Type u_2
inst : CommSemiring R₁
inst_1 : AddCommMonoid M₁
inst_2 : Module R₁ M₁
n : Type u_5
inst_3 : Fintype n
inst_4 : DecidableEq n
b : Basis n R₁ M₁
B : BilinForm R₁ M₁
x y : n → R₁
⊢ x ⬝ᵥ (toMatrix b : (a : BilinForm R₁ M₁) → Matrix n n R₁) B *ᵥ y =
    (((B : (a : M₁) → M₁ →ₗ[R₁] R₁) ((b.equivFun.symm : (a : n → R₁) → M₁) x) : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁)
      ((b.equivFun.symm : (a : n → R₁) → M₁) y : M₁)

Tactic:
dotProduct_toMatrix₂_mulVec b b B x y

Premises used: dotProduct_toMatrix₂_mulVec
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
M₁ : Type u_2
inst : CommSemiring R₁
inst_1 : AddCommMonoid M₁
inst_2 : Module R₁ M₁
n : Type u_5
inst_3 : Fintype n
inst_4 : DecidableEq n
b : Basis n R₁ M₁
B : BilinForm R₁ M₁
x y : M₁
⊢ Eq.{u_1 + 1} (α := R₁) ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁) x : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) y : R₁)
    (dotProduct.{u_1, u_5} (m := n) (⇑((b.repr : (a : M₁) → n →₀ R₁) x : n →₀ R₁) : (a : n) → R₁)
        (mulVec (n := n) ((toMatrix b : (a : BilinForm R₁ M₁) → Matrix n n R₁) B)
          (⇑((b.repr : (a : M₁) → n →₀ R₁) y : n →₀ R₁) : (a : n) → R₁)) :
      R₁)

Tactic:
apply_eq_dotProduct_toMatrix₂_mulVec b b B x y

Premises used: apply_eq_dotProduct_toMatrix₂_mulVec
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
M₁ : Type u_2
inst : CommSemiring R₁
inst_1 : AddCommMonoid M₁
inst_2 : Module R₁ M₁
n : Type u_5
inst_3 : Fintype n
inst_4 : DecidableEq n
b : Basis n R₁ M₁
M : Matrix n n R₁
x y : M₁
⊢ Eq.{u_1 + 1} (α := R₁)
    (∑ i : n,
      ∑ j : n,
        HSMul.hSMul (α := R₁) ((((b.repr : (a : M₁) → n →₀ R₁) x : n →₀ R₁) : (a : n) → R₁) i : R₁)
          (HSMul.hSMul (α := R₁) ((((b.repr : (a : M₁) → n →₀ R₁) y : n →₀ R₁) : (a : n) → R₁) j : R₁) (M i j)))
    (∑ i : n,
      ∑ j : n,
        HMul.hMul (β := R₁)
          (HMul.hMul (α := R₁) ((((b.repr : (a : M₁) → n →₀ R₁) x : n →₀ R₁) : (a : n) → R₁) i : R₁) (M i j))
          ((((b.repr : (a : M₁) → n →₀ R₁) y : n →₀ R₁) : (a : n) → R₁) j : R₁))

Tactic:
simp only [smul_eq_mul, mul_comm, mul_left_comm]

Premises used: mul_left_comm, mul_comm, smul_eq_mul
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
M₁ : Type u_2
inst : CommSemiring R₁
inst_1 : AddCommMonoid M₁
inst_2 : Module R₁ M₁
n : Type u_5
inst_3 : Fintype n
inst_4 : DecidableEq n
b : Basis n R₁ M₁
B : BilinForm R₁ M₁
⊢ Eq (α := Matrix n n R₁) ((toMatrixAux (⇑b : (a : n) → M₁) : (a : BilinForm R₁ M₁) → Matrix n n R₁) B : Matrix n n R₁)
    ((toMatrix b : (a : BilinForm R₁ M₁) → Matrix n n R₁) B : Matrix n n R₁)

Tactic:
LinearMap.toMatrix₂Aux_eq _ _ B

Premises used: LinearMap.toMatrix₂Aux_eq
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
M₁ : Type u_2
inst : CommSemiring R₁
inst_1 : AddCommMonoid M₁
inst_2 : Module R₁ M₁
n : Type u_5
inst_3 : Fintype n
inst_4 : DecidableEq n
b : Basis n R₁ M₁
⊢ (toMatrix b).symm = toBilin b

Tactic:
rfl

Premises used: Matrix.toBilin, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
M₁ : Type u_2
inst : CommSemiring R₁
inst_1 : AddCommMonoid M₁
inst_2 : Module R₁ M₁
n : Type u_5
inst_3 : Fintype n
inst_4 : DecidableEq n
b : Basis n R₁ M₁
⊢ (toBilin b).symm = LinearMap.BilinForm.toMatrix b

Tactic:
(LinearMap.BilinForm.toMatrix b).symm_symm

Premises used: LinearMap.BilinForm.toMatrix, LinearEquiv.symm_symm, Matrix.toBilin
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
inst : CommSemiring R₁
n : Type u_5
inst_1 : Fintype n
inst_2 : DecidableEq n
h :
  ∀ (M : Matrix n n R₁) (i i_1 : n),
    Eq (α := R₁)
      ((((((toBilin (Pi.basisFun R₁ n) : (a : Matrix n n R₁) → BilinForm R₁ (n → R₁)) M ∘ₗ
                        LinearMap.single R₁ (fun (i : n) ↦ R₁) i :
                      R₁ →ₗ[R₁] (n → R₁) →ₗ[R₁] R₁) :
                    (a : R₁) → (n → R₁) →ₗ[R₁] R₁)
                  1 ∘ₗ
                LinearMap.single R₁ (fun (i : n) ↦ R₁) i_1 :
              R₁ →ₗ[R₁] R₁) :
            (a : R₁) → R₁)
          1 :
        R₁)
      ((((((toBilin' : (a : Matrix n n R₁) → BilinForm R₁ (n → R₁)) M ∘ₗ LinearMap.single R₁ (fun (i : n) ↦ R₁) i :
                      R₁ →ₗ[R₁] (n → R₁) →ₗ[R₁] R₁) :
                    (a : R₁) → (n → R₁) →ₗ[R₁] R₁)
                  1 ∘ₗ
                LinearMap.single R₁ (fun (i : n) ↦ R₁) i_1 :
              R₁ →ₗ[R₁] R₁) :
            (a : R₁) → R₁)
          1 :
        R₁)
⊢ Eq (α := Matrix n n R₁ ≃ₗ[R₁] BilinForm R₁ (n → R₁)) (toBilin (Pi.basisFun R₁ n)) toBilin'

Tactic:
ext M