awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
l : Type u_3
m : Type u_4
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
inst_3 : Fintype m
inst_4 : DecidableEq m
M : Matrix l m R
N : Matrix m n R
x : n → R
rw :
  Eq (α := l → R)
    (((toLin' : (a : Matrix l m R) → (m → R) →ₗ[R] l → R) M ∘ₗ (toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) N :
          (a : n → R) → l → R)
        x :
      l → R)
    ((((toLin' : (a : Matrix l m R) → (m → R) →ₗ[R] l → R) M : (m → R) →ₗ[R] l → R) : (a : m → R) → l → R)
        ((((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) N : (n → R) →ₗ[R] m → R) : (a : n → R) → m → R) x :
          m → R) :
      l → R)
rw₁ rw₂ :
  Eq (α := l → R)
    ((((toLin' : (a : Matrix l m R) → (m → R) →ₗ[R] l → R) M : (m → R) →ₗ[R] l → R) : (a : m → R) → l → R)
        ((((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) N : (n → R) →ₗ[R] m → R) : (a : n → R) → m → R) x :
          m → R) :
      l → R)
    ((((toLin' : (a : Matrix l m R) → (m → R) →ₗ[R] l → R) M : (m → R) →ₗ[R] l → R) : (a : m → R) → l → R)
        ((((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) N : (n → R) →ₗ[R] m → R) : (a : n → R) → m → R) x :
          m → R) :
      l → R)
⊢ Eq (α := l → R)
    ((((toLin' : (a : Matrix l n R) → (n → R) →ₗ[R] l → R) (M * N) : (n → R) →ₗ[R] l → R) : (a : n → R) → l → R) x :
      l → R)
    ((((toLin' : (a : Matrix l m R) → (m → R) →ₗ[R] l → R) M : (m → R) →ₗ[R] l → R) : (a : m → R) → l → R)
        ((((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) N : (n → R) →ₗ[R] m → R) : (a : n → R) → m → R) x :
          m → R) :
      l → R)

Tactic:
rw [Matrix.toLin'_mul, LinearMap.comp_apply]

Premises used: LinearMap.comp_apply, Matrix.toLin'_mul
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
l : Type u_3
m : Type u_4
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
inst_3 : Fintype l
inst_4 : DecidableEq l
f : (n → R) →ₗ[R] m → R
g : (l → R) →ₗ[R] n → R
this :
  f ∘ₗ g =
    (toLin' : (a : Matrix m l R) → (l → R) →ₗ[R] m → R)
      (HMul.hMul (α := Matrix m n R) (β := Matrix n l R)
        ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R) f : Matrix m n R)
        ((toMatrix' : (a : (l → R) →ₗ[R] n → R) → Matrix n l R) g : Matrix n l R))
rw :
  (toMatrix' : (a : (l → R) →ₗ[R] m → R) → Matrix m l R)
      ((toLin' : (a : Matrix m l R) → (l → R) →ₗ[R] m → R)
        (HMul.hMul (α := Matrix m n R) (β := Matrix n l R)
          ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R) f : Matrix m n R)
          ((toMatrix' : (a : (l → R) →ₗ[R] n → R) → Matrix n l R) g : Matrix n l R))) =
    HMul.hMul (α := Matrix m n R) (β := Matrix n l R)
      ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R) f : Matrix m n R)
      ((toMatrix' : (a : (l → R) →ₗ[R] n → R) → Matrix n l R) g : Matrix n l R)
rw₁ rw₂ :
  HMul.hMul (α := Matrix m n R) (β := Matrix n l R)
      ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R) f : Matrix m n R)
      ((toMatrix' : (a : (l → R) →ₗ[R] n → R) → Matrix n l R) g : Matrix n l R) =
    HMul.hMul (α := Matrix m n R) (β := Matrix n l R)
      ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R) f : Matrix m n R)
      ((toMatrix' : (a : (l → R) →ₗ[R] n → R) → Matrix n l R) g : Matrix n l R)
⊢ (toMatrix' : (a : (l → R) →ₗ[R] m → R) → Matrix m l R) (f ∘ₗ g) =
    HMul.hMul (α := Matrix m n R) (β := Matrix n l R)
      ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R) f : Matrix m n R)
      ((toMatrix' : (a : (l → R) →ₗ[R] n → R) → Matrix n l R) g : Matrix n l R)

Tactic:
rw [this, LinearMap.toMatrix'_toLin']

Premises used: LinearMap.toMatrix'_toLin'
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
l : Type u_3
m : Type u_4
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
inst_3 : Fintype l
inst_4 : DecidableEq l
f : (n → R) →ₗ[R] m → R
g : (l → R) →ₗ[R] n → R
suffices :
  f ∘ₗ g =
    (toLin' : (a : Matrix m l R) → (l → R) →ₗ[R] m → R)
      (HMul.hMul (α := Matrix m n R) (β := Matrix n l R)
        ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R) f : Matrix m n R)
        ((toMatrix' : (a : (l → R) →ₗ[R] n → R) → Matrix n l R) g : Matrix n l R))
⊢ (toMatrix' : (a : (l → R) →ₗ[R] m → R) → Matrix m l R) (f ∘ₗ g) =
    HMul.hMul (α := Matrix m n R) (β := Matrix n l R)
      ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R) f : Matrix m n R)
      ((toMatrix' : (a : (l → R) →ₗ[R] n → R) → Matrix n l R) g : Matrix n l R)

Tactic:
suffices f.comp g = Matrix.toLin' (LinearMap.toMatrix' f * LinearMap.toMatrix' g) by
    rw [this, LinearMap.toMatrix'_toLin']
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
l : Type u_3
m : Type u_4
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
inst_3 : Fintype l
inst_4 : DecidableEq l
f : (n → R) →ₗ[R] m → R
g : (l → R) →ₗ[R] n → R
rw :
  f ∘ₗ g =
    (toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R) f) ∘ₗ
      (toLin' : (a : Matrix n l R) → (l → R) →ₗ[R] n → R) ((toMatrix' : (a : (l → R) →ₗ[R] n → R) → Matrix n l R) g)
rw₁ :
  f ∘ₗ g =
    f ∘ₗ (toLin' : (a : Matrix n l R) → (l → R) →ₗ[R] n → R) ((toMatrix' : (a : (l → R) →ₗ[R] n → R) → Matrix n l R) g)
rw₂ rw₃ : f ∘ₗ g = f ∘ₗ g
⊢ f ∘ₗ g =
    (toLin' : (a : Matrix m l R) → (l → R) →ₗ[R] m → R)
      (HMul.hMul (α := Matrix m n R) (β := Matrix n l R)
        ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R) f : Matrix m n R)
        ((toMatrix' : (a : (l → R) →ₗ[R] n → R) → Matrix n l R) g : Matrix n l R))

Tactic:
rw [Matrix.toLin'_mul, Matrix.toLin'_toMatrix', Matrix.toLin'_toMatrix']

Premises used: Matrix.toLin'_mul, Matrix.toLin'_toMatrix'
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
m : Type u_4
inst_1 : Fintype m
inst_2 : DecidableEq m
f g : (m → R) →ₗ[R] m → R
⊢ (toMatrix' : (a : (m → R) →ₗ[R] m → R) → Matrix m m R) (f * g) =
    HMul.hMul (α := Matrix m m R) (β := Matrix m m R)
      ((toMatrix' : (a : (m → R) →ₗ[R] m → R) → Matrix m m R) f : Matrix m m R)
      ((toMatrix' : (a : (m → R) →ₗ[R] m → R) → Matrix m m R) g : Matrix m m R)

Tactic:
LinearMap.toMatrix'_comp f g

Premises used: LinearMap.toMatrix'_comp
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
x : R
⊢ Eq (α := Matrix n n R)
    ((toMatrix' : (a : (n → R) →ₗ[R] n → R) → Matrix n n R)
        ((algebraMap R (End R (n → R)) : (a : R) → End R (n → R)) x) :
      Matrix n n R)
    ((scalar n : (a : R) → Matrix n n R) x : Matrix n n R)

Tactic:
simp [Module.algebraMap_end_eq_smul_id, smul_eq_diagonal_mul]

Premises used: Module.algebraMap_end_eq_smul_id, Matrix.smul_eq_diagonal_mul
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
⊢ Eq (α := Submodule R (n → R))
      (ker (R₂ := R) (M₂ := n → R) (τ₁₂ := RingHom.id R) ((toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) M)) ⊥ ↔
    ∀ (v : n → R), M *ᵥ v = 0 → v = 0

Tactic:
Matrix.ker_mulVecLin_eq_bot_iff

Premises used: Matrix.ker_mulVecLin_eq_bot_iff
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
m : Type u_4
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix m n R
⊢ Eq (α := Submodule R (m → R))
    (LinearMap.range (R := R) (M := n → R) (τ₁₂ := RingHom.id R)
      ((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) M))
    (span R (Set.range M.col))

Tactic:
Matrix.range_mulVecLin _

Premises used: Matrix.range_mulVecLin
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
inst_3 : Fintype m
inst_4 : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : m → R
rw : (((toLin' : (a : Matrix m m R) → (m → R) →ₗ[R] m → R) (M * M') : (m → R) →ₗ[R] m → R) : (a : m → R) → m → R) x = x
rw₁ : ((toLin' : (a : Matrix m m R) → (m → R) →ₗ[R] m → R) 1 : (a : m → R) → m → R) x = x
rw₂ : (LinearMap.id : (a : m → R) → m → R) x = x
rw₃ rw₄ : x = x
⊢ (((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) M : (n → R) →ₗ[R] m → R) : (a : n → R) → m → R)
      ((((toLin' : (a : Matrix n m R) → (m → R) →ₗ[R] n → R) M' : (m → R) →ₗ[R] n → R) : (a : m → R) → n → R) x :
        n → R) =
    x

Tactic:
rw [← Matrix.toLin'_mul_apply, hMM', Matrix.toLin'_one, id_apply]

Premises used: LinearMap.id_apply, Matrix.toLin'_mul_apply, Matrix.toLin'_one
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
inst_3 : Fintype m
inst_4 : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : n → R
rw : (((toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (M' * M) : (n → R) →ₗ[R] n → R) : (a : n → R) → n → R) x = x
rw₁ : ((toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) 1 : (a : n → R) → n → R) x = x
rw₂ : (LinearMap.id : (a : n → R) → n → R) x = x
rw₃ rw₄ : x = x
⊢ (((toLin' : (a : Matrix n m R) → (m → R) →ₗ[R] n → R) M' : (m → R) →ₗ[R] n → R) : (a : m → R) → n → R)
      ((((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) M : (n → R) →ₗ[R] m → R) : (a : n → R) → m → R) x :
        m → R) =
    x

Tactic:
rw [← Matrix.toLin'_mul_apply, hM'M, Matrix.toLin'_one, id_apply]

Premises used: LinearMap.id_apply, Matrix.toLin'_mul_apply, Matrix.toLin'_one
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
⊢ Eq (α := Matrix n n R ≃ₐ[R] (n → R) →ₗ[R] n → R) (AlgEquiv.symm toMatrixAlgEquiv') toLinAlgEquiv'

Tactic:
rfl

Premises used: Matrix.toLinAlgEquiv', rfl
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
⊢ Eq (α := ((n → R) →ₗ[R] n → R) ≃ₐ[R] Matrix n n R) (AlgEquiv.symm toLinAlgEquiv') toMatrixAlgEquiv'

Tactic:
rfl

Premises used: AlgEquiv.symm, LinearMap.toMatrixAlgEquiv', AlgEquiv.ofLinearEquiv, Equiv.symm, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
⊢ (toMatrixAlgEquiv' : (a : (n → R) →ₗ[R] n → R) → Matrix n n R)
      ((toLinAlgEquiv' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) M) =
    M

Tactic:
LinearMap.toMatrixAlgEquiv'.apply_symm_apply M

Premises used: LinearMap.toMatrixAlgEquiv', AlgEquiv.apply_symm_apply
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
f : (n → R) →ₗ[R] n → R
⊢ (toLinAlgEquiv' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R)
      ((toMatrixAlgEquiv' : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) f) =
    f

Tactic:
Matrix.toLinAlgEquiv'.apply_symm_apply f

Premises used: AlgEquiv.apply_symm_apply, Matrix.toLinAlgEquiv'
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
f : (n → R) →ₗ[R] n → R
i j : n
⊢ Eq.{u_1 + 1} (α := R) ((toMatrixAlgEquiv' : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) f i j : R)
    ((f : (a : n → R) → n → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
v : n → R
⊢ (((toLinAlgEquiv' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) M : (n → R) →ₗ[R] n → R) : (a : n → R) → n → R) v =
    M *ᵥ v

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Matrix.mulVec, Finset.sum, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
⊢ Eq (α := (n → R) →ₗ[R] n → R) ((toLinAlgEquiv' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) 1) LinearMap.id

Tactic:
Matrix.toLin'_one

Premises used: Matrix.toLin'_one
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
⊢ Eq (α := Matrix n n R) ((toMatrixAlgEquiv' : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) id : Matrix n n R)
    (1 : Matrix n n R)

Tactic:
LinearMap.toMatrix'_id

Premises used: Function.update, Pi.single, dite, LinearMap.toMatrix'_id
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
f g : (n → R) →ₗ[R] n → R
⊢ (toMatrixAlgEquiv' : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) (f ∘ₗ g) =
    HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
      ((toMatrixAlgEquiv' : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) f : Matrix n n R)
      ((toMatrixAlgEquiv' : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) g : Matrix n n R)

Tactic:
LinearMap.toMatrix'_comp _ _

Premises used: LinearMap.toMatrix'_comp
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
f g : (n → R) →ₗ[R] n → R
⊢ (toMatrixAlgEquiv' : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) (f * g) =
    HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
      ((toMatrixAlgEquiv' : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) f : Matrix n n R)
      ((toMatrixAlgEquiv' : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) g : Matrix n n R)

Tactic:
LinearMap.toMatrixAlgEquiv'_comp f g

Premises used: LinearMap.toMatrixAlgEquiv'_comp
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
f : (n → R) →ₗ[R] n → R
⊢ IsUnit (M := Matrix n n R) ((toMatrix' : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) f : Matrix n n R) ↔ IsUnit f

Tactic:
isUnit_map_iff LinearMap.toMatrixAlgEquiv' f

Premises used: LinearMap.toMatrixAlgEquiv', isUnit_map_iff
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
⊢ IsUnit (M := (n → R) →ₗ[R] n → R) ((toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) M : (n → R) →ₗ[R] n → R) ↔
    IsUnit M

Tactic:
isUnit_map_iff LinearMap.toMatrixAlgEquiv'.symm M

Premises used: AlgEquiv.symm, LinearMap.toMatrixAlgEquiv', isUnit_map_iff
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
⊢ Eq (α := ((n → R) →ₗ[R] n → R) ≃ₗ[R] Matrix n n R) (toMatrix (Pi.basisFun R n) (Pi.basisFun R n)) toMatrix'

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Function.update, dotProduct, LinearMap.toMatrix', Pi.single, dite, Matrix.mulVec, LinearEquiv.trans, Finset.sum, rfl, LinearMap.toMatrix
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : Finite m
inst_3 : DecidableEq n
⊢ Eq (α := Matrix m n R ≃ₗ[R] (n → R) →ₗ[R] m → R) (toLin (Pi.basisFun R n) (Pi.basisFun R m)) toLin'

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Matrix.toLin, Function.update, dotProduct, Matrix.toLin', LinearMap.toMatrix', Pi.single, dite, Matrix.mulVec, LinearEquiv.trans, Finset.sum, rfl, LinearMap.toMatrix
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
⊢ (toMatrix v₁ v₂).symm = toLin v₁ v₂

Tactic:
rfl

Premises used: Matrix.toLin, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
⊢ (toLin v₁ v₂).symm = toMatrix v₁ v₂

Tactic:
rfl

Premises used: LinearEquiv.symm, LinearEquiv.trans, rfl, LinearMap.toMatrix
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
rw : (toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) (((toLin v₁ v₂).symm : (a : M₁ →ₗ[R] M₂) → Matrix m n R) f) = f
rw₁ rw₂ : f = f
⊢ (toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) ((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) f) = f

Tactic:
rw [← Matrix.toLin_symm, LinearEquiv.apply_symm_apply]

Premises used: Matrix.toLin_symm, LinearEquiv.apply_symm_apply
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M : Matrix m n R
rw : ((toLin v₁ v₂).symm : (a : M₁ →ₗ[R] M₂) → Matrix m n R) ((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) M) = M
rw₁ rw₂ : M = M
⊢ (toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) ((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) M) = M

Tactic:
rw [← Matrix.toLin_symm, LinearEquiv.symm_apply_apply]

Premises used: Matrix.toLin_symm, LinearEquiv.symm_apply_apply
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
i : m
j : n
⊢ Eq.{u_1 + 1} (α := R) ((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) f i j : R)
    ((((v₂.repr : (a : M₂) → m →₀ R) ((f : (a : M₁) → M₂) ((v₁ : (a : n) → M₁) j : M₁)) : m →₀ R) : (a : m) → R) i : R)

Tactic:
simp [toMatrix]

Premises used: LinearMap.toMatrix
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
j : n
⊢ Eq (α := m → R) (((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) f)ᵀ j)
    (⇑((v₂.repr : (a : M₂) → m →₀ R) ((f : (a : M₁) → M₂) ((v₁ : (a : n) → M₁) j : M₁)) : m →₀ R) : (a : m) → R)

Tactic:
funext fun i ↦ f.toMatrix_apply _ _ i j

Premises used: funext, LinearMap.toMatrix_apply
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
i : m
j : n
⊢ Eq.{u_1 + 1} (α := R) ((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) f i j : R)
    ((((v₂.repr : (a : M₂) → m →₀ R) ((f : (a : M₁) → M₂) ((v₁ : (a : n) → M₁) j : M₁)) : m →₀ R) : (a : m) → R) i : R)

Tactic:
LinearMap.toMatrix_apply v₁ v₂ f i j

Premises used: LinearMap.toMatrix_apply
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
j : n
⊢ Eq (α := m → R) (((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) f)ᵀ j)
    (⇑((v₂.repr : (a : M₂) → m →₀ R) ((f : (a : M₁) → M₂) ((v₁ : (a : n) → M₁) j : M₁)) : m →₀ R) : (a : m) → R)

Tactic:
LinearMap.toMatrix_transpose_apply v₁ v₂ f j

Premises used: LinearMap.toMatrix_transpose_apply
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
a : ∀ (i j : n), Eq.{u_1 + 1} (α := R) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) id i j : R) (1 i j : R)
⊢ Eq (α := Matrix n n R) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) id : Matrix n n R) (1 : Matrix n n R)

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
i j : n
⊢ Eq.{u_1 + 1} (α := R) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) id i j : R) (1 i j : R)

Tactic:
simp [LinearMap.toMatrix_apply, Matrix.one_apply, Finsupp.single_apply, eq_comm]

Premises used: Matrix.one_apply, eq_comm, Finsupp.single_apply, LinearMap.toMatrix_apply
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
⊢ Eq (α := Matrix n n R) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) 1) 1

Tactic:
LinearMap.toMatrix_id v₁

Premises used: LinearMap.toMatrix_id
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_7
inst_1 : Unique ι
f : R →ₗ[R] R
i j : ι
⊢ Eq.{u_1 + 1} (α := R)
    ((toMatrix (Basis.singleton ι R) (Basis.singleton ι R) : (a : R →ₗ[R] R) → Matrix ι ι R) f i j : R)
    ((f : (a : R) → R) 1 : R)

Tactic:
simp [toMatrix, Subsingleton.elim j default]

Premises used: Inhabited.default, Subsingleton.elim, LinearMap.toMatrix
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
rw :
  Eq.{u_5 + 1} (α := M₁ →ₗ[R] M₁)
    ((toLin v₁ v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁)
        ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) LinearMap.id) :
      M₁ →ₗ[R] M₁)
    (LinearMap.id : M₁ →ₗ[R] M₁)
rw₁ rw₂ : Eq.{u_5 + 1} (α := M₁ →ₗ[R] M₁) LinearMap.id LinearMap.id
⊢ Eq.{u_5 + 1} (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) 1) LinearMap.id

Tactic:
rw [← LinearMap.toMatrix_id v₁, Matrix.toLin_toMatrix]

Premises used: LinearMap.toMatrix_id, Matrix.toLin_toMatrix
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
r : R
⊢ Eq (α := Matrix n n R)
    ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R)
        ((toLin v₁ v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) ((scalar n : (a : R) → Matrix n n R) r)) :
      Matrix n n R)
    ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (HSMul.hSMul (β := M₁ →ₗ[R] M₁) r LinearMap.id) : Matrix n n R)

Tactic:
simp [toMatrix_id, smul_one_eq_diagonal]

Premises used: Matrix.smul_one_eq_diagonal, LinearMap.toMatrix_id
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
x : R
⊢ Eq (α := Matrix n n R)
    ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) ((algebraMap R (End R M₁) : (a : R) → End R M₁) x) :
      Matrix n n R)
    ((scalar n : (a : R) → Matrix n n R) x : Matrix n n R)

Tactic:
simp [Module.algebraMap_end_eq_smul_id, LinearMap.toMatrix_id, smul_eq_diagonal_mul]

Premises used: LinearMap.toMatrix_id, Module.algebraMap_end_eq_smul_id, Matrix.smul_eq_diagonal_mul