awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_5
inst_1 : Fintype n
inst_2 : DecidableEq n
h :
  ∀ (i x : n),
    Eq.{u_1 + 1} (α := R) ((mulVecLin 1 ∘ₗ LinearMap.single R (fun (i : n) ↦ R) i : (a : R) → n → R) 1 x : R)
      (((LinearMap.id ∘ₗ LinearMap.single R (fun (i : n) ↦ R) i : R →ₗ[R] n → R) : (a : R) → n → R) 1 x : R)
⊢ Eq (α := (n → R) →ₗ[R] n → R) (mulVecLin 1) LinearMap.id

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_5
inst_1 : Fintype n
inst_2 : DecidableEq n
i x : n
⊢ Eq.{u_1 + 1} (α := R) ((mulVecLin 1 ∘ₗ LinearMap.single R (fun (i : n) ↦ R) i : (a : R) → n → R) 1 x : R)
    (((LinearMap.id ∘ₗ LinearMap.single R (fun (i : n) ↦ R) i : R →ₗ[R] n → R) : (a : R) → n → R) 1 x : R)

Tactic:
simp [Matrix.one_apply, Pi.single_apply, eq_comm]

Premises used: Matrix.one_apply, Pi.single_apply, eq_comm
-- 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 : Fintype n
inst_2 : Fintype m
M : Matrix l m R
N : Matrix m n R
⊢ (M * N).mulVecLin = M.mulVecLin ∘ₗ N.mulVecLin

Tactic:
LinearMap.ext fun _ ↦ (mulVec_mulVec _ _ _).symm

Premises used: LinearMap.ext, Eq.symm, Matrix.mulVec_mulVec
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
m : Type u_4
n : Type u_5
inst_1 : Fintype n
M : Matrix m n R
⊢ Eq (α := Submodule R (n → R)) (ker M.mulVecLin) ⊥ ↔ ∀ (v : n → R), M *ᵥ v = 0 → v = 0

Tactic:
simp only [Submodule.eq_bot_iff, LinearMap.mem_ker, Matrix.mulVecLin_apply]

Premises used: Matrix.mulVecLin_apply, LinearMap.mem_ker, Submodule.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 : Fintype n
M : Matrix m n R
rw : Eq (α := Submodule R (m → R)) (LinearMap.range Mᵀ.vecMulLinear) (span R (Set.range M.col))
rw₁ : Eq (α := Submodule R (m → R)) (span R (Set.range Mᵀ.row)) (span R (Set.range M.col))
rw₂ rw₃ : Eq (α := Submodule R (m → R)) (span R (Set.range M.col)) (span R (Set.range M.col))
⊢ Eq (α := Submodule R (m → R)) (LinearMap.range M.mulVecLin) (span R (Set.range M.col))

Tactic:
rw [← vecMulLinear_transpose, range_vecMulLinear, row_transpose]

Premises used: range_vecMulLinear, Matrix.row_transpose, Matrix.vecMulLinear_transpose
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
m : Type u_4
n : Type u_5
inst_1 : Fintype n
M : Matrix m n R
simp_rw : (Function.Injective (β := m → R) fun (x : n → R) ↦ x ᵥ* Mᵀ) ↔ LinearIndependent R M.col
simp_rw₁ : LinearIndependent R Mᵀ.row ↔ LinearIndependent R M.col
⊢ (Function.Injective (β := m → R) fun (x : n → R) ↦ M *ᵥ x) ↔ LinearIndependent R M.col

Tactic:
simp_rw [← M.vecMul_transpose, vecMul_injective_iff, row_transpose]

Premises used: Matrix.row_transpose, Matrix.vecMul_transpose, Matrix.vecMul_injective_iff
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
m : Type u_4
inst_1 : Fintype m
A : Matrix m m R
inst_2 : DecidableEq m
ha : IsUnit A
rw : Function.Injective A.mulVec
⊢ LinearIndependent R A.col

Tactic:
rw [← Matrix.mulVec_injective_iff]

Premises used: Matrix.mulVec_injective_iff
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
m : Type u_4
inst_1 : Fintype m
A : Matrix m m R
inst_2 : DecidableEq m
ha : IsUnit A
⊢ Function.Injective A.mulVec

Tactic:
Matrix.mulVec_injective_of_isUnit ha

Premises used: Matrix.mulVec_injective_of_isUnit
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
m : Type u_4
inst_1 : Fintype m
A : Matrix m m R
inst_2 : DecidableEq m
ha : IsUnit A
⊢ Function.Injective A.mulVec

Tactic:
exact Matrix.mulVec_injective_of_isUnit ha

Premises used: Matrix.mulVec_injective_of_isUnit
-- 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
f g : (n → R) →ₗ[R] m → R
a :
  ∀ (i : m) (j : n),
    (of : (a : m → n → R) → Matrix m n R)
        (fun (i : m) (j : n) ↦ (f + g : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i) i j =
      HAdd.hAdd (α := Matrix m n R) (β := Matrix m n R)
        ((of : (a : m → n → R) → Matrix m n R) fun (i : m) (j : n) ↦
          (f : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i)
        ((of : (a : m → n → R) → Matrix m n R) fun (i : m) (j : n) ↦
          (g : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i)
        i j
⊢ ((of : (a : m → n → R) → Matrix m n R) fun (i : m) (j : n) ↦
      (f + g : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i) =
    HAdd.hAdd (α := Matrix m n R)
      ((of : (a : m → n → R) → Matrix m n R) fun (i : m) (j : n) ↦
        (f : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i)
      ((of : (a : m → n → R) → Matrix m n R) fun (i : m) (j : n) ↦
        (g : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i)

Tactic:
ext i j
-- 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
f g : (n → R) →ₗ[R] m → R
i : m
j : n
⊢ (of : (a : m → n → R) → Matrix m n R)
      (fun (i : m) (j : n) ↦ (f + g : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i) i j =
    HAdd.hAdd (α := Matrix m n R) (β := Matrix m n R)
      ((of : (a : m → n → R) → Matrix m n R) fun (i : m) (j : n) ↦
        (f : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i)
      ((of : (a : m → n → R) → Matrix m n R) fun (i : m) (j : n) ↦
        (g : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i)
      i j

Tactic:
simp only [Pi.add_apply, LinearMap.add_apply, of_apply, Matrix.add_apply]

Premises used: Matrix.add_apply, LinearMap.add_apply, Matrix.of_apply, Pi.add_apply
-- 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
c : R
f : (n → R) →ₗ[R] m → R
a :
  ∀ (i : m) (j : n),
    (of : (a : m → n → R) → Matrix m n R)
        (fun (i : m) (j : n) ↦ (c • f : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i) i j =
      HSMul.hSMul (α := R) (β := Matrix m n R) ((RingHom.id R : (a : R) → R) c : R)
        ((of : (a : m → n → R) → Matrix m n R) fun (i : m) (j : n) ↦
          (f : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i)
        i j
⊢ ((of : (a : m → n → R) → Matrix m n R) fun (i : m) (j : n) ↦
      (c • f : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i) =
    HSMul.hSMul (α := R) (β := Matrix m n R) ((RingHom.id R : (a : R) → R) c : R)
      ((of : (a : m → n → R) → Matrix m n R) fun (i : m) (j : n) ↦
        (f : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i)

Tactic:
ext i j
-- 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
c : R
f : (n → R) →ₗ[R] m → R
i : m
j : n
⊢ (of : (a : m → n → R) → Matrix m n R)
      (fun (i : m) (j : n) ↦ (c • f : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i) i j =
    HSMul.hSMul (α := R) (β := Matrix m n R) ((RingHom.id R : (a : R) → R) c : R)
      ((of : (a : m → n → R) → Matrix m n R) fun (i : m) (j : n) ↦
        (f : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i)
      i j

Tactic:
simp only [Pi.smul_apply, LinearMap.smul_apply, RingHom.id_apply, of_apply, Matrix.smul_apply]

Premises used: RingHom.id_apply, LinearMap.smul_apply, Matrix.smul_apply, Matrix.of_apply, Pi.smul_apply
-- 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
f : (n → R) →ₗ[R] m → R
apply :
  ∀ (i : n),
    Eq (α := m → R)
      ((mulVecLin
              ((fun (f : (n → R) →ₗ[R] m → R) ↦
                  ((of : (a : m → n → R) → Matrix m n R) fun (i : m) (j : n) ↦
                      (f : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i :
                    Matrix m n R))
                f) :
            (a : n → R) → m → R)
          ((Pi.basisFun R n : (a : n) → n → R) i : n → R) :
        m → R)
      ((f : (a : n → R) → m → R) ((Pi.basisFun R n : (a : n) → n → R) i : n → R) : m → R)
⊢ mulVecLin
      ((fun (f : (n → R) →ₗ[R] m → R) ↦
          ((of : (a : m → n → R) → Matrix m n R) fun (i : m) (j : n) ↦
              (f : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i :
            Matrix m n R))
        f) =
    f

Tactic:
apply (Pi.basisFun R n).ext

Premises used: Pi.basisFun, Module.Basis.ext
-- 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
f : (n → R) →ₗ[R] m → R
j : n
h :
  ∀ (i : m),
    Eq.{u_1 + 1} (α := R)
      ((mulVecLin
              ((fun (f : (n → R) →ₗ[R] m → R) ↦
                  ((of : (a : m → n → R) → Matrix m n R) fun (i : m) (j : n) ↦
                      (f : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i :
                    Matrix m n R))
                f) :
            (a : n → R) → m → R)
          ((Pi.basisFun R n : (a : n) → n → R) j : n → R) i :
        R)
      ((f : (a : n → R) → m → R) ((Pi.basisFun R n : (a : n) → n → R) j : n → R) i : R)
⊢ Eq (α := m → R)
    ((mulVecLin
            ((fun (f : (n → R) →ₗ[R] m → R) ↦
                ((of : (a : m → n → R) → Matrix m n R) fun (i : m) (j : n) ↦
                    (f : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i :
                  Matrix m n R))
              f) :
          (a : n → R) → m → R)
        ((Pi.basisFun R n : (a : n) → n → R) j : n → R) :
      m → R)
    ((f : (a : n → R) → m → R) ((Pi.basisFun R n : (a : n) → n → R) j : n → R) : m → R)

Tactic:
ext i
-- 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
f : (n → R) →ₗ[R] m → R
j : n
i : m
⊢ Eq.{u_1 + 1} (α := R)
    ((mulVecLin
            ((fun (f : (n → R) →ₗ[R] m → R) ↦
                ((of : (a : m → n → R) → Matrix m n R) fun (i : m) (j : n) ↦
                    (f : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i :
                  Matrix m n R))
              f) :
          (a : n → R) → m → R)
        ((Pi.basisFun R n : (a : n) → n → R) j : n → R) i :
      R)
    ((f : (a : n → R) → m → R) ((Pi.basisFun R n : (a : n) → n → R) j : n → R) i : R)

Tactic:
simp only [Pi.basisFun_apply, Matrix.mulVec_single_one, col_apply,
      Matrix.mulVecLin_apply, of_apply]

Premises used: Matrix.col_apply, Matrix.mulVec_single_one, Matrix.mulVecLin_apply, Matrix.of_apply, Pi.basisFun_apply
-- 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
M : Matrix m n R
a :
  ∀ (i : m) (j : n),
    (fun (f : (n → R) →ₗ[R] m → R) ↦
          ((of : (a : m → n → R) → Matrix m n R) fun (i : m) (j : n) ↦
              (f : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i :
            Matrix m n R))
        M.mulVecLin i j =
      M i j
⊢ (fun (f : (n → R) →ₗ[R] m → R) ↦
        ((of : (a : m → n → R) → Matrix m n R) fun (i : m) (j : n) ↦
            (f : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i :
          Matrix m n R))
      M.mulVecLin =
    M

Tactic:
ext i j
-- 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
M : Matrix m n R
i : m
j : n
⊢ (fun (f : (n → R) →ₗ[R] m → R) ↦
        ((of : (a : m → n → R) → Matrix m n R) fun (i : m) (j : n) ↦
            (f : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i :
          Matrix m n R))
      M.mulVecLin i j =
    M i j

Tactic:
simp only [Matrix.mulVec_single_one, col_apply, Matrix.mulVecLin_apply, of_apply]

Premises used: Matrix.col_apply, Matrix.mulVec_single_one, Matrix.mulVecLin_apply, Matrix.of_apply
-- 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 (α := (n → R) →ₗ[R] m → R) ((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) M : (n → R) →ₗ[R] m → R)
    (M.mulVecLin : (n → R) →ₗ[R] m → R)

Tactic:
rfl

Premises used: rfl
-- 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
⊢ Eq (α := Matrix m n R ≃ₗ[R] (n → R) →ₗ[R] m → R) (LinearEquiv.symm toMatrix') toLin'

Tactic:
rfl

Premises used: Matrix.toLin', rfl
-- 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
⊢ Eq (α := ((n → R) →ₗ[R] m → R) ≃ₗ[R] Matrix m n R) (LinearEquiv.symm toLin') toMatrix'

Tactic:
rfl

Premises used: LinearEquiv.symm, LinearMap.toMatrix', rfl
-- 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
⊢ (toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R) ((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) M) = M

Tactic:
LinearMap.toMatrix'.apply_symm_apply M

Premises used: LinearMap.toMatrix', LinearEquiv.apply_symm_apply
-- 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
f : (n → R) →ₗ[R] m → R
⊢ (toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R) f) = f

Tactic:
Matrix.toLin'.apply_symm_apply f

Premises used: Matrix.toLin', LinearEquiv.apply_symm_apply
-- 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
f : (n → R) →ₗ[R] m → R
i : m
j : n
⊢ Eq.{u_1 + 1} (α := R) ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R) f i j : R)
    ((f : (a : n → R) → m → 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
m : Type u_4
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix m n R
v : n → R
⊢ (((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) M : (n → R) →ₗ[R] m → R) : (a : n → R) → m → 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
m : Type u_4
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
f : (n → R) →ₗ[R] m → R
v : n → R
rw :
  Eq (α := m → R)
    ((((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R) f) :
            (n → R) →ₗ[R] m → R) :
          (a : n → R) → m → R)
        v :
      m → R)
    ((f : (a : n → R) → m → R) v : m → R)
rw₁ rw₂ : Eq (α := m → R) ((f : (a : n → R) → m → R) v : m → R) ((f : (a : n → R) → m → R) v : m → R)
⊢ Eq (α := m → R) ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R) f *ᵥ v) ((f : (a : n → R) → m → R) v)

Tactic:
rw [← toLin'_apply, toLin'_toMatrix']

Premises used: Matrix.toLin'_apply, Matrix.toLin'_toMatrix'
-- 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) ((toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) 1) LinearMap.id

Tactic:
Matrix.mulVecLin_one

Premises used: Matrix.mulVecLin_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
a : ∀ (i j : n), Eq.{u_1 + 1} (α := R) ((toMatrix' : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) id i j : R) (1 i j : R)
⊢ Eq (α := Matrix n n R) ((toMatrix' : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) id : Matrix n n R) (1 : Matrix n n R)

Tactic:
ext
-- 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
i j : n
a :
  Eq.{u_1 + 1} (α := R) ((toMatrix' : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) id i j : R) (if i = j then 1 else 0 : R)
a₁ :
  Eq.{u_1 + 1} (α := R) ((id : (a : n → R) → n → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i : R)
    (if i = j then 1 else 0 : R)
a₂ : Eq.{u_1 + 1} (α := R) (Pi.single (M := fun (a : n) ↦ R) j 1 i : R) (if i = j then 1 else 0 : R)
a₃ a₄ : Eq.{u_1 + 1} (α := R) (if i = j then 1 else 0) (if i = j then 1 else 0)
⊢ Eq.{u_1 + 1} (α := R) ((toMatrix' : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) id i j : R) (1 i j : R)

Tactic:
rw [Matrix.one_apply, LinearMap.toMatrix'_apply, id_apply, Pi.single_apply]

Premises used: Matrix.one_apply, LinearMap.id_apply, Pi.single_apply, LinearMap.toMatrix'_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
⊢ Eq (α := Matrix n n R) ((toMatrix' : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) 1) 1

Tactic:
LinearMap.toMatrix'_id

Premises used: LinearMap.toMatrix'_id
-- 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
⊢ Eq (α := (n → R) →ₗ[R] l → R) ((toLin' : (a : Matrix l n R) → (n → R) →ₗ[R] l → R) (M * N) : (n → R) →ₗ[R] 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 :
      (n → R) →ₗ[R] l → R)

Tactic:
Matrix.mulVecLin_mul _ _

Premises used: Matrix.mulVecLin_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
⊢ (toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (HPow.hPow (β := ℕ) M 0) =
    HPow.hPow (α := (n → R) →ₗ[R] n → R) (β := ℕ)
      ((toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) M : (n → R) →ₗ[R] n → R) 0

Tactic:
simp [End.one_eq_id]

Premises used: Module.End.one_eq_id
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n_1 : Type u_5
inst_1 : DecidableEq n_1
inst_2 : Fintype n_1
M : Matrix n_1 n_1 R
n : ℕ
ih :
  (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) (M ^ n) =
    HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
      ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) n
succ :
  (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) (M ^ n * M) =
    HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
      ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) (n + 1)
succ₁ :
  (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) (M ^ n * M) =
    HMul.hMul (β := (n_1 → R) →ₗ[R] n_1 → R)
      (HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
        ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) n)
      ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R)
succ₂ :
  (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) (M ^ n) ∘ₗ
      (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M =
    HMul.hMul (β := (n_1 → R) →ₗ[R] n_1 → R)
      (HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
        ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) n)
      ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R)
succ₃ :
  HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
        ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) n ∘ₗ
      (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M =
    HMul.hMul (β := (n_1 → R) →ₗ[R] n_1 → R)
      (HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
        ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) n)
      ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R)
succ₄ succ₅ :
  Eq (α := (n_1 → R) →ₗ[R] n_1 → R)
    (HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
        ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) n ∘ₗ
      (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M)
    (HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
        ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) n ∘ₗ
      (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M)
⊢ (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) (M ^ (n + 1)) =
    HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
      ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) (n + 1)

Tactic:
rw [pow_succ, pow_succ, toLin'_mul, ih, Module.End.mul_eq_comp]

Premises used: Module.End.mul_eq_comp, pow_succ, Matrix.toLin'_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
k : ℕ
zero :
  (toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (HPow.hPow (β := ℕ) M 0) =
    HPow.hPow (α := (n → R) →ₗ[R] n → R) (β := ℕ)
      ((toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) M : (n → R) →ₗ[R] n → R) 0
succ :
  ∀ (n_1 : ℕ)
    (ih :
      (toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (M ^ n_1) =
        HPow.hPow (α := (n → R) →ₗ[R] n → R)
          ((toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) M : (n → R) →ₗ[R] n → R) n_1),
    (toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (M ^ (n_1 + 1)) =
      HPow.hPow (α := (n → R) →ₗ[R] n → R) ((toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) M : (n → R) →ₗ[R] n → R)
        (n_1 + 1)
⊢ (toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (M ^ k) =
    HPow.hPow (α := (n → R) →ₗ[R] n → R) ((toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) M : (n → R) →ₗ[R] n → R) k

Tactic:
induction k with
  | zero => simp [End.one_eq_id]
  | succ n ih => rw [pow_succ, pow_succ, toLin'_mul, ih, Module.End.mul_eq_comp]

Premises used: Module.End.mul_eq_comp, Module.End.one_eq_id, pow_succ, Matrix.toLin'_mul, Matrix.zero
-- 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 l
inst_4 : DecidableEq l
f₁ : m → k
e₂ : n ≃ l
M : Matrix k l R
⊢ Eq (α := (n → R) →ₗ[R] m → R)
    ((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) (M.submatrix f₁ (⇑e₂ : (a : n) → l)) : (n → R) →ₗ[R] m → R)
    (funLeft R R f₁ ∘ₗ (toLin' : (a : Matrix k l R) → (l → R) →ₗ[R] k → R) M ∘ₗ funLeft R R (⇑e₂.symm : (a : l) → n) :
      (n → R) →ₗ[R] m → R)

Tactic:
Matrix.mulVecLin_submatrix _ _ _

Premises used: Matrix.mulVecLin_submatrix
-- 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 l
inst_4 : DecidableEq l
e₁ : k ≃ m
e₂ : l ≃ n
M : Matrix k l R
⊢ Eq (α := (n → R) →ₗ[R] m → R)
    ((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) ((reindex e₁ e₂ : (a : Matrix k l R) → Matrix m n R) M) :
      (n → R) →ₗ[R] m → R)
    ((↑(LinearEquiv.funCongrLeft R R e₁.symm) : (k → R) →ₗ[R] m → R) ∘ₗ
        (toLin' : (a : Matrix k l R) → (l → R) →ₗ[R] k → R) M ∘ₗ
          (↑(LinearEquiv.funCongrLeft R R e₂) : (n → R) →ₗ[R] l → R) :
      (n → R) →ₗ[R] m → R)

Tactic:
Matrix.mulVecLin_reindex _ _ _

Premises used: Matrix.mulVecLin_reindex