awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : Semiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype m
M : Matrix m n R
x : m → R
⊢ (M.vecMulLinear : (a : m → R) → n → R) x = x ᵥ* M

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Matrix.vecMul, Finset.sum, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : Semiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype m
M : Matrix m n R
⊢ Eq (α := (a : m → R) → n → R) (⇑M.vecMulLinear : (a : m → R) → n → R) fun (v : m → R) ↦ v ᵥ* M

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Matrix.vecMul, Finset.sum, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : Semiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype m
M : Matrix m n R
this : DecidableEq m := Classical.decEq m
simp_rw :
  Eq (α := Submodule R (n → R)) (span R (Set.range fun (x : m) ↦ Pi.single (M := fun (i : m) ↦ R) x 1 ᵥ* M))
    (span R (Set.range fun (i : m) ↦ M i))
⊢ Eq (α := Submodule R (n → R)) (LinearMap.range M.vecMulLinear) (span R (Set.range M.row))

Tactic:
simp_rw [range_eq_map, ← iSup_range_single, Submodule.map_iSup, range_eq_map, ←
    Ideal.span_singleton_one, Ideal.span, Submodule.map_span, image_image, image_singleton,
    Matrix.vecMulLinear_apply, iSup_span, range_eq_iUnion, iUnion_singleton_eq_range,
    LinearMap.single, LinearMap.coe_mk, AddHom.coe_mk, row_def]

Premises used: LinearMap.coe_mk, Set.image_image, Matrix.row_def, Submodule.map_iSup, Set.image_singleton, LinearMap.iSup_range_single, Ideal.span_singleton_one, Submodule.iSup_span, Set.iUnion_singleton_eq_range, LinearMap.single, Matrix.vecMulLinear_apply, Ideal.span, LinearMap.range_eq_map, Submodule.map_span, AddHom.coe_mk, Set.range_eq_iUnion
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : Semiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype m
M : Matrix m n R
this : DecidableEq m := Classical.decEq m
simp_rw simp_rw₁ :
  Eq (α := Submodule R (n → R))
    (span R (Set.range fun (x : m) (x_1 : n) ↦ Pi.single (M := fun (i : m) ↦ R) x 1 ⬝ᵥ fun (i : m) ↦ M i x_1))
    (span R (Set.range fun (i : m) ↦ M i))
simp_rw₂ :
  Eq (α := Submodule R (n → R)) (span R (Set.range fun (x : m) (x_1 : n) ↦ 1 * M x x_1))
    (span R (Set.range fun (i : m) ↦ M i))
⊢ Eq (α := Submodule R (n → R))
    (span R
      (Set.range fun (x : m) (x_1 : n) ↦
        have j := x_1;
        Pi.single (M := fun (i : m) ↦ R) x 1 ⬝ᵥ fun (i : m) ↦ M i j))
    (span R (Set.range fun (i : m) ↦ M i))

Tactic:
simp_rw [single_dotProduct, one_mul]

Premises used: single_dotProduct, one_mul
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : Semiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype m
M : Matrix m n R
rw :
  Function.Injective (α := m → R) (β := n → R) (⇑M.vecMulLinear : (a : m → R) → n → R) ↔
    Function.Injective (α := m → R) (β := n → R) (⇑(Fintype.linearCombination R M.row) : (a : m → R) → n → R)
⊢ (Function.Injective (β := n → R) fun (v : m → R) ↦ v ᵥ* M) ↔ LinearIndependent R M.row

Tactic:
rw [← coe_vecMulLinear, linearIndependent_iff_injective_fintypeLinearCombination]

Premises used: Matrix.coe_vecMulLinear, linearIndependent_iff_injective_fintypeLinearCombination
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : Semiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype m
M : Matrix m n R
a :
  Eq (α := (m → R) → n → R) (⇑M.vecMulLinear : (a : m → R) → n → R)
    (⇑(Fintype.linearCombination R M.row) : (a : m → R) → n → R)
⊢ Function.Injective (α := m → R) (β := n → R) (⇑M.vecMulLinear : (a : m → R) → n → R) ↔
    Function.Injective (α := m → R) (β := n → R) (⇑(Fintype.linearCombination R M.row) : (a : m → R) → n → R)

Tactic:
congr! 1
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : Semiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype m
M : Matrix m n R
⊢ Eq (α := (m → R) → n → R) (⇑M.vecMulLinear : (a : m → R) → n → R)
    (⇑(Fintype.linearCombination R M.row) : (a : m → R) → n → R)

Tactic:
funext fun _ => Matrix.vecMul_eq_sum _ _

Premises used: Matrix.vecMul_eq_sum, funext
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : Semiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype m
M : Matrix m n R
⊢ Eq (α := (m → R) → n → R) (⇑M.vecMulLinear : (a : m → R) → n → R)
    (⇑(Fintype.linearCombination R M.row) : (a : m → R) → n → R)

Tactic:
exact funext fun _ => Matrix.vecMul_eq_sum _ _

Premises used: Matrix.vecMul_eq_sum, funext
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : Semiring R
m : Type u_3
inst_1 : Fintype m
A : Matrix m m R
inst_2 : DecidableEq m
ha : IsUnit A
rw : Function.Injective (β := m → R) fun (v : m → R) ↦ v ᵥ* A
⊢ LinearIndependent R A.row

Tactic:
rw [← Matrix.vecMul_injective_iff]

Premises used: Matrix.vecMul_injective_iff
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : Semiring R
m : Type u_3
inst_1 : Fintype m
A : Matrix m m R
inst_2 : DecidableEq m
ha : IsUnit A
⊢ Function.Injective (β := m → R) fun (v : m → R) ↦ v ᵥ* A

Tactic:
Matrix.vecMul_injective_of_isUnit ha

Premises used: Matrix.vecMul_injective_of_isUnit
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : Semiring R
m : Type u_3
inst_1 : Fintype m
A : Matrix m m R
inst_2 : DecidableEq m
ha : IsUnit A
⊢ Function.Injective (β := m → R) fun (v : m → R) ↦ v ᵥ* A

Tactic:
exact Matrix.vecMul_injective_of_isUnit ha

Premises used: Matrix.vecMul_injective_of_isUnit
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype m
inst_2 : DecidableEq m
f g : (m → R) →ₗ[R] n → R
a :
  ∀ (i : m) (j : n),
    (f + g : (a : m → R) → n → R)
        (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j =
      HAdd.hAdd (α := Matrix m n R) (β := Matrix m n R)
        (fun (i : m) (j : n) ↦
          (f : (a : m → R) → n → R)
            (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j)
        (fun (i : m) (j : n) ↦
          (g : (a : m → R) → n → R)
            (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j)
        i j
⊢ (fun (i : m) (j : n) ↦
      (f + g : (a : m → R) → n → R)
        (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j) =
    HAdd.hAdd (α := Matrix m n R)
      (fun (i : m) (j : n) ↦
        (f : (a : m → R) → n → R)
          (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j)
      fun (i : m) (j : n) ↦
      (g : (a : m → R) → n → R)
        (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype m
inst_2 : DecidableEq m
f g : (m → R) →ₗ[R] n → R
i : m
j : n
⊢ (f + g : (a : m → R) → n → R)
      (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j =
    HAdd.hAdd (α := Matrix m n R) (β := Matrix m n R)
      (fun (i : m) (j : n) ↦
        (f : (a : m → R) → n → R)
          (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j)
      (fun (i : m) (j : n) ↦
        (g : (a : m → R) → n → R)
          (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j)
      i j

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

Premises used: Matrix.add_apply, LinearMap.add_apply, Pi.add_apply
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype m
inst_2 : DecidableEq m
c : Rᵐᵒᵖ
f : (m → R) →ₗ[R] n → R
a :
  ∀ (i : m) (j : n),
    (c • f : (a : m → R) → n → R)
        (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j =
      HSMul.hSMul (α := Rᵐᵒᵖ) (β := Matrix m n R) ((RingHom.id Rᵐᵒᵖ : (a : Rᵐᵒᵖ) → Rᵐᵒᵖ) c : Rᵐᵒᵖ)
        (fun (i : m) (j : n) ↦
          (f : (a : m → R) → n → R)
            (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j)
        i j
⊢ (fun (i : m) (j : n) ↦
      (c • f : (a : m → R) → n → R)
        (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j) =
    HSMul.hSMul (α := Rᵐᵒᵖ) (β := Matrix m n R) ((RingHom.id Rᵐᵒᵖ : (a : Rᵐᵒᵖ) → Rᵐᵒᵖ) c : Rᵐᵒᵖ) fun (i : m) (j : n) ↦
      (f : (a : m → R) → n → R)
        (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype m
inst_2 : DecidableEq m
c : Rᵐᵒᵖ
f : (m → R) →ₗ[R] n → R
i : m
j : n
⊢ (c • f : (a : m → R) → n → R)
      (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j =
    HSMul.hSMul (α := Rᵐᵒᵖ) (β := Matrix m n R) ((RingHom.id Rᵐᵒᵖ : (a : Rᵐᵒᵖ) → Rᵐᵒᵖ) c : Rᵐᵒᵖ)
      (fun (i : m) (j : n) ↦
        (f : (a : m → R) → n → R)
          (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j)
      i j

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

Premises used: RingHom.id_apply, LinearMap.smul_apply, Matrix.smul_apply, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype m
inst_2 : DecidableEq m
f : (m → R) →ₗ[R] n → R
apply :
  ∀ (i : m),
    Eq (α := n → R)
      ((vecMulLinear
              ((fun (f : (m → R) →ₗ[R] n → R) (i : m) (j : n) ↦
                  ((f : (a : m → R) → n → R)
                      (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R)
                      j :
                    R))
                f) :
            (a : m → R) → n → R)
          ((Pi.basisFun R m : (a : m) → m → R) i : m → R) :
        n → R)
      ((f : (a : m → R) → n → R) ((Pi.basisFun R m : (a : m) → m → R) i : m → R) : n → R)
⊢ vecMulLinear
      ((fun (f : (m → R) →ₗ[R] n → R) (i : m) (j : n) ↦
          ((f : (a : m → R) → n → R)
              (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j :
            R))
        f) =
    f

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

Premises used: Pi.basisFun, Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype m
inst_2 : DecidableEq m
f : (m → R) →ₗ[R] n → R
j : m
h :
  ∀ (i : n),
    Eq.{u_1 + 1} (α := R)
      ((vecMulLinear
              ((fun (f : (m → R) →ₗ[R] n → R) (i : m) (j : n) ↦
                  ((f : (a : m → R) → n → R)
                      (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R)
                      j :
                    R))
                f) :
            (a : m → R) → n → R)
          ((Pi.basisFun R m : (a : m) → m → R) j : m → R) i :
        R)
      ((f : (a : m → R) → n → R) ((Pi.basisFun R m : (a : m) → m → R) j : m → R) i : R)
⊢ Eq (α := n → R)
    ((vecMulLinear
            ((fun (f : (m → R) →ₗ[R] n → R) (i : m) (j : n) ↦
                ((f : (a : m → R) → n → R)
                    (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j :
                  R))
              f) :
          (a : m → R) → n → R)
        ((Pi.basisFun R m : (a : m) → m → R) j : m → R) :
      n → R)
    ((f : (a : m → R) → n → R) ((Pi.basisFun R m : (a : m) → m → R) j : m → R) : n → R)

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype m
inst_2 : DecidableEq m
f : (m → R) →ₗ[R] n → R
j : m
i : n
⊢ Eq.{u_1 + 1} (α := R)
    ((vecMulLinear
            ((fun (f : (m → R) →ₗ[R] n → R) (i : m) (j : n) ↦
                ((f : (a : m → R) → n → R)
                    (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j :
                  R))
              f) :
          (a : m → R) → n → R)
        ((Pi.basisFun R m : (a : m) → m → R) j : m → R) i :
      R)
    ((f : (a : m → R) → n → R) ((Pi.basisFun R m : (a : m) → m → R) j : m → R) i : R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype m
inst_2 : DecidableEq m
M : Matrix m n R
a :
  ∀ (i : m) (j : n),
    (fun (f : (m → R) →ₗ[R] n → R) (i : m) (j : n) ↦
          ((f : (a : m → R) → n → R)
              (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j :
            R))
        M.vecMulLinear i j =
      M i j
⊢ (fun (f : (m → R) →ₗ[R] n → R) (i : m) (j : n) ↦
        ((f : (a : m → R) → n → R)
            (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j :
          R))
      M.vecMulLinear =
    M

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype m
inst_2 : DecidableEq m
M : Matrix m n R
i : m
j : n
⊢ (fun (f : (m → R) →ₗ[R] n → R) (i : m) (j : n) ↦
        ((f : (a : m → R) → n → R)
            (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j :
          R))
      M.vecMulLinear i j =
    M i j

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : Semiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype m
inst_2 : DecidableEq m
M : Matrix m n R
v : m → R
⊢ (((toLinearMapRight' : (a : Matrix m n R) → (m → R) →ₗ[R] n → R) M : (m → R) →ₗ[R] n → R) : (a : m → R) → n → R) v =
    v ᵥ* M

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Matrix.vecMul, Finset.sum, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype m
inst_2 : DecidableEq m
inst_3 : Fintype l
inst_4 : DecidableEq l
M : Matrix l m R
N : Matrix m n R
⊢ Eq (α := (l → R) →ₗ[R] n → R)
    ((toLinearMapRight' : (a : Matrix l n R) → (l → R) →ₗ[R] n → R) (M * N) : (l → R) →ₗ[R] n → R)
    ((toLinearMapRight' : (a : Matrix m n R) → (m → R) →ₗ[R] n → R) N ∘ₗ
        (toLinearMapRight' : (a : Matrix l m R) → (l → R) →ₗ[R] m → R) M :
      (l → R) →ₗ[R] n → R)

Tactic:
LinearMap.ext fun _x ↦ (vecMul_vecMul _ M N).symm

Premises used: LinearMap.ext, Matrix.vecMul_vecMul, Eq.symm
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype m
inst_2 : DecidableEq m
inst_3 : Fintype l
inst_4 : DecidableEq l
M : Matrix l m R
N : Matrix m n R
x : l → R
⊢ Eq (α := n → R)
    ((((toLinearMapRight' : (a : Matrix l n R) → (l → R) →ₗ[R] n → R) (M * N) : (l → R) →ₗ[R] n → R) :
          (a : l → R) → n → R)
        x :
      n → R)
    ((((toLinearMapRight' : (a : Matrix m n R) → (m → R) →ₗ[R] n → R) N : (m → R) →ₗ[R] n → R) : (a : m → R) → n → R)
        ((((toLinearMapRight' : (a : Matrix l m R) → (l → R) →ₗ[R] m → R) M : (l → R) →ₗ[R] m → R) :
              (a : l → R) → m → R)
            x :
          m → R) :
      n → R)

Tactic:
(vecMul_vecMul _ M N).symm

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Matrix.vecMul, Matrix.vecMul_vecMul, Eq.symm, Finset.sum
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype m
inst_2 : DecidableEq m
inst_3 : Fintype l
inst_4 : DecidableEq l
f : (l → R) →ₗ[R] m → R
g : (m → R) →ₗ[R] n → R
⊢ Eq (α := (l → R) →ₗ[R] n → R)
    ((toLinearMapRight' : (a : Matrix l n R) → (l → R) →ₗ[R] n → R)
        ((toMatrixRight' : (a : (l → R) →ₗ[R] n → R) → Matrix l n R) (g ∘ₗ f)) :
      (l → R) →ₗ[R] n → R)
    ((toLinearMapRight' : (a : Matrix l n R) → (l → R) →ₗ[R] n → R)
        (HMul.hMul (α := Matrix l m R) (β := Matrix m n R)
          ((toMatrixRight' : (a : (l → R) →ₗ[R] m → R) → Matrix l m R) f : Matrix l m R)
          ((toMatrixRight' : (a : (m → R) →ₗ[R] n → R) → Matrix m n R) g : Matrix m n R)) :
      (l → R) →ₗ[R] n → R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : Semiring R
m : Type u_3
inst_1 : Fintype m
inst_2 : DecidableEq m
h :
  ∀ (i x : m),
    Eq.{u_1 + 1} (α := R)
      ((((toLinearMapRight' : (a : Matrix m m R) → (m → R) →ₗ[R] m → R) 1 ∘ₗ LinearMap.single R (fun (i : m) ↦ R) i :
              R →ₗ[R] m → R) :
            (a : R) → m → R)
          1 x :
        R)
      (((LinearMap.id ∘ₗ LinearMap.single R (fun (i : m) ↦ R) i : R →ₗ[R] m → R) : (a : R) → m → R) 1 x : R)
⊢ Eq (α := (m → R) →ₗ[R] m → R) ((toLinearMapRight' : (a : Matrix m m R) → (m → R) →ₗ[R] m → R) 1) LinearMap.id

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

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : Semiring R
m : Type u_3
inst_1 : Fintype m
inst_2 : DecidableEq m
⊢ Eq (α := (m → R) →ₗ[R] m → R)
    ((toLinearMapRight' : (a : Matrix m m R) → (m → R) →ₗ[R] m → R)
        ((toMatrixRight' : (a : (m → R) →ₗ[R] m → R) → Matrix m m R) id) :
      (m → R) →ₗ[R] m → R)
    ((toLinearMapRight' : (a : Matrix m m R) → (m → R) →ₗ[R] m → R) 1 : (m → R) →ₗ[R] m → R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype m
inst_2 : DecidableEq m
inst_3 : Fintype n
inst_4 : DecidableEq n
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : n → R
rw :
  (((toLinearMapRight' : (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₁ : ((toLinearMapRight' : (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
⊢ (((toLinearMapRight' : (a : Matrix m n R) → (m → R) →ₗ[R] n → R) M : (m → R) →ₗ[R] n → R) : (a : m → R) → n → R)
      ((((toLinearMapRight' : (a : Matrix n m R) → (n → R) →ₗ[R] m → R) M' : (n → R) →ₗ[R] m → R) : (a : n → R) → m → R)
          x :
        m → R) =
    x

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

Premises used: LinearMap.id_apply, Matrix.toLinearMapRight'_mul_apply, Matrix.toLinearMapRight'_one
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype m
inst_2 : DecidableEq m
inst_3 : Fintype n
inst_4 : DecidableEq n
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : m → R
rw :
  (((toLinearMapRight' : (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₁ : ((toLinearMapRight' : (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
⊢ (((toLinearMapRight' : (a : Matrix n m R) → (n → R) →ₗ[R] m → R) M' : (n → R) →ₗ[R] m → R) : (a : n → R) → m → R)
      ((((toLinearMapRight' : (a : Matrix m n R) → (m → R) →ₗ[R] n → R) M : (m → R) →ₗ[R] n → R) : (a : m → R) → n → R)
          x :
        n → R) =
    x

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

Premises used: LinearMap.id_apply, Matrix.toLinearMapRight'_mul_apply, Matrix.toLinearMapRight'_one
-- 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
⊢ (⇑M.mulVecLin : (a : n → R) → m → R) = M.mulVec

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 : Fintype n
M : Matrix m n R
v : n → R
⊢ (M.mulVecLin : (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 : Fintype n
⊢ Eq (α := (n → R) →ₗ[R] m → R) (mulVecLin 0) 0

Tactic:
LinearMap.ext zero_mulVec

Premises used: Matrix.zero_mulVec, LinearMap.ext
-- 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 N : Matrix m n R
⊢ (M + N).mulVecLin = HAdd.hAdd (α := (n → R) →ₗ[R] m → R) M.mulVecLin N.mulVecLin

Tactic:
LinearMap.ext fun _ ↦ add_mulVec _ _ _

Premises used: Matrix.add_mulVec, LinearMap.ext
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
m : Type u_4
n : Type u_5
inst_1 : Fintype m
M : Matrix m n R
h :
  ∀ (x : m → R) (x_1 : n),
    Eq.{u_1 + 1} (α := R) ((Mᵀ.mulVecLin : (a : m → R) → n → R) x x_1 : R)
      ((M.vecMulLinear : (a : m → R) → n → R) x x_1 : R)
⊢ Eq (α := (m → R) →ₗ[R] n → R) Mᵀ.mulVecLin M.vecMulLinear

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
m : Type u_4
n : Type u_5
inst_1 : Fintype m
M : Matrix m n R
x : m → R
x_1 : n
⊢ Eq.{u_1 + 1} (α := R) ((Mᵀ.mulVecLin : (a : m → R) → n → R) x x_1 : R)
    ((M.vecMulLinear : (a : m → R) → n → R) x x_1 : R)

Tactic:
simp [mulVec_transpose]

Premises used: Matrix.mulVec_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
h :
  ∀ (x : n → R) (x_1 : m),
    Eq.{u_1 + 1} (α := R) ((Mᵀ.vecMulLinear : (a : n → R) → m → R) x x_1 : R)
      ((M.mulVecLin : (a : n → R) → m → R) x x_1 : R)
⊢ Eq (α := (n → R) →ₗ[R] m → R) Mᵀ.vecMulLinear M.mulVecLin

Tactic:
ext
-- 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
x : n → R
x_1 : m
⊢ Eq.{u_1 + 1} (α := R) ((Mᵀ.vecMulLinear : (a : n → R) → m → R) x x_1 : R)
    ((M.mulVecLin : (a : n → R) → m → R) x x_1 : R)

Tactic:
simp [vecMul_transpose]

Premises used: Matrix.vecMul_transpose
-- 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 : Fintype n
inst_2 : Fintype l
f₁ : m → k
e₂ : n ≃ l
M : Matrix k l R
⊢ Eq (α := (n → R) →ₗ[R] m → R) (mulVecLin (M.submatrix f₁ (⇑e₂ : (a : n) → l)))
    (funLeft R R f₁ ∘ₗ M.mulVecLin ∘ₗ funLeft R R (⇑e₂.symm : (a : l) → n))

Tactic:
LinearMap.ext fun _ ↦ submatrix_mulVec_equiv _ _ _ _

Premises used: LinearMap.ext, Matrix.submatrix_mulVec_equiv
-- 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 : Fintype n
inst_2 : Fintype l
e₁ : k ≃ m
e₂ : l ≃ n
M : Matrix k l R
⊢ mulVecLin ((reindex e₁ e₂ : (a : Matrix k l R) → Matrix m n R) M) =
    (↑(LinearEquiv.funCongrLeft R R e₁.symm) : (k → R) →ₗ[R] m → R) ∘ₗ
      M.mulVecLin ∘ₗ (↑(LinearEquiv.funCongrLeft R R e₂) : (n → R) →ₗ[R] l → R)

Tactic:
Matrix.mulVecLin_submatrix _ _ _

Premises used: Matrix.submatrix, Matrix.mulVecLin_submatrix, LinearMap.funLeft