awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
v : n → α
x y : Matrix m n α
h : ∀ (m_1 : m), ((x + y) *ᵥ v) m_1 = (x *ᵥ v + y *ᵥ v) m_1
⊢ (x + y) *ᵥ v = x *ᵥ v + y *ᵥ v

Tactic:
ext m
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m_1 : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
v : n → α
x y : Matrix m_1 n α
m : m_1
⊢ ((x + y) *ᵥ v) m = (x *ᵥ v + y *ᵥ v) m

Tactic:
apply add_dotProduct

Premises used: add_dotProduct
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
A : Matrix m n α
B : Matrix n o α
i : m
⊢ (A * B) i = A i ᵥ* B

Tactic:
rfl

Premises used: Matrix.vecMul, rfl
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype m
v : m → α
M : Matrix m n α
⊢ v ᵥ* M = ∑ i : m, v i • M i

Tactic:
(Finset.sum_fn ..).symm

Premises used: dotProduct, Matrix.vecMul, Finset.sum_fn, Eq.symm
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
v : n → α
M : Matrix m n α
⊢ M *ᵥ v = ∑ i : n, MulOpposite.op (v i) • Mᵀ i

Tactic:
(Finset.sum_fn ..).symm

Premises used: dotProduct, Matrix.transpose, MulOpposite.unop, Finset.sum_fn, Eq.symm, Matrix.mulVec
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype m
inst_2 : DecidableEq m
v w : m → α
x : m
⊢ (diagonal v *ᵥ w) x = v x * w x

Tactic:
diagonal_dotProduct v w x

Premises used: diagonal_dotProduct, Matrix.mulVec
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype m
inst_2 : DecidableEq m
v w : m → α
x : m
⊢ (v ᵥ* diagonal w) x = v x * w x

Tactic:
dotProduct_diagonal' v w x

Premises used: Matrix.vecMul, dotProduct_diagonal'
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
inst : Fintype n
inst_1 : Fintype m
inst_2 : NonUnitalSemiring R
v : m → R
A : Matrix m n R
w : n → R
simp : Eq.{u_7 + 1} (α := R) (∑ x : m, ∑ i : n, v x * (A x i * w i)) (∑ x : n, ∑ x_1 : m, v x_1 * (A x_1 x * w x))
⊢ v ⬝ᵥ A *ᵥ w = v ᵥ* A ⬝ᵥ w

Tactic:
simp only [dotProduct, vecMul, mulVec, Finset.mul_sum, Finset.sum_mul, mul_assoc]

Premises used: Finset.mul_sum, dotProduct, mul_assoc, Matrix.vecMul, Matrix.mulVec, Finset.sum_mul
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
inst : Fintype n
inst_1 : Fintype m
inst_2 : NonUnitalSemiring R
v : m → R
A : Matrix m n R
w : n → R
⊢ Eq.{u_7 + 1} (α := R) (∑ x : m, ∑ i : n, v x * (A x i * w i)) (∑ x : n, ∑ x_1 : m, v x_1 * (A x_1 x * w x))

Tactic:
Finset.sum_comm

Premises used: Finset.sum_comm
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
inst : Fintype n
inst_1 : Fintype m
inst_2 : NonUnitalSemiring R
v : m → R
A : Matrix m n R
w : n → R
⊢ Eq.{u_7 + 1} (α := R) (∑ x : m, ∑ i : n, v x * (A x i * w i)) (∑ x : n, ∑ x_1 : m, v x_1 * (A x_1 x * w x))

Tactic:
exact Finset.sum_comm

Premises used: Finset.sum_comm
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
A : Matrix m n α
h : ∀ (x : m), (A *ᵥ 0) x = 0 x
⊢ A *ᵥ 0 = 0

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
A : Matrix m n α
x : m
⊢ (A *ᵥ 0) x = 0 x

Tactic:
simp [mulVec]

Premises used: Matrix.mulVec
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype m
A : Matrix m n α
h : ∀ (x : n), (0 ᵥ* A) x = 0 x
⊢ 0 ᵥ* A = 0

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype m
A : Matrix m n α
x : n
⊢ (0 ᵥ* A) x = 0 x

Tactic:
simp [vecMul]

Premises used: Matrix.vecMul
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
v : n → α
h : ∀ (x : m), (0 *ᵥ v) x = 0 x
⊢ Eq (α := m → α) (0 *ᵥ v) 0

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
v : n → α
x : m
⊢ (0 *ᵥ v) x = 0 x

Tactic:
simp [mulVec]

Premises used: Matrix.mulVec
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype m
v : m → α
h : ∀ (x : n), (v ᵥ* 0) x = 0 x
⊢ Eq (α := n → α) (v ᵥ* 0) 0

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype m
v : m → α
x : n
⊢ (v ᵥ* 0) x = 0 x

Tactic:
simp [vecMul]

Premises used: Matrix.vecMul
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
A : Matrix m n α
x y : n → α
h : ∀ (x_1 : m), (A *ᵥ (x + y)) x_1 = (A *ᵥ x + A *ᵥ y) x_1
⊢ A *ᵥ (x + y) = A *ᵥ x + A *ᵥ y

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
A : Matrix m n α
x y : n → α
x_1 : m
⊢ (A *ᵥ (x + y)) x_1 = (A *ᵥ x + A *ᵥ y) x_1

Tactic:
apply dotProduct_add

Premises used: dotProduct_add
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
A B : Matrix m n α
x : n → α
h : ∀ (x_1 : m), ((A + B) *ᵥ x) x_1 = (A *ᵥ x + B *ᵥ x) x_1
⊢ (A + B) *ᵥ x = A *ᵥ x + B *ᵥ x

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
A B : Matrix m n α
x : n → α
x_1 : m
⊢ ((A + B) *ᵥ x) x_1 = (A *ᵥ x + B *ᵥ x) x_1

Tactic:
apply add_dotProduct

Premises used: add_dotProduct
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype m
A B : Matrix m n α
x : m → α
h : ∀ (x_1 : n), (x ᵥ* (A + B)) x_1 = (x ᵥ* A + x ᵥ* B) x_1
⊢ x ᵥ* (A + B) = x ᵥ* A + x ᵥ* B

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype m
A B : Matrix m n α
x : m → α
x_1 : n
⊢ (x ᵥ* (A + B)) x_1 = (x ᵥ* A + x ᵥ* B) x_1

Tactic:
apply dotProduct_add

Premises used: dotProduct_add
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype m
A : Matrix m n α
x y : m → α
h : ∀ (x_1 : n), ((x + y) ᵥ* A) x_1 = (x ᵥ* A + y ᵥ* A) x_1
⊢ (x + y) ᵥ* A = x ᵥ* A + y ᵥ* A

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype m
A : Matrix m n α
x y : m → α
x_1 : n
⊢ ((x + y) ᵥ* A) x_1 = (x ᵥ* A + y ᵥ* A) x_1

Tactic:
apply add_dotProduct

Premises used: add_dotProduct
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
inst_2 : DistribSMul R α
inst_3 : SMulCommClass R α α
M : Matrix m n α
b : R
v : n → α
h : ∀ (x : m), (M *ᵥ b • v) x = (b • M *ᵥ v) x
⊢ M *ᵥ b • v = b • M *ᵥ v

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
inst_2 : DistribSMul R α
inst_3 : SMulCommClass R α α
M : Matrix m n α
b : R
v : n → α
x : m
⊢ (M *ᵥ b • v) x = (b • M *ᵥ v) x

Tactic:
dotProduct_smul _ _ _

Premises used: dotProduct_smul, Matrix.mulVec
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
inst_2 : DistribSMul R α
inst_3 : SMulCommClass R α α
M : Matrix m n α
b : R
v : n → α
x : m
⊢ (M *ᵥ b • v) x = (b • M *ᵥ v) x

Tactic:
exact dotProduct_smul _ _ _

Premises used: dotProduct_smul
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
inst_2 : DistribSMul R α
inst_3 : IsScalarTower R α α
b : R
M : Matrix m n α
v : n → α
h : ∀ (x : m), ((b • M) *ᵥ v) x = (b • M *ᵥ v) x
⊢ (b • M) *ᵥ v = b • M *ᵥ v

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
inst_2 : DistribSMul R α
inst_3 : IsScalarTower R α α
b : R
M : Matrix m n α
v : n → α
x : m
⊢ ((b • M) *ᵥ v) x = (b • M *ᵥ v) x

Tactic:
smul_dotProduct _ _ _

Premises used: Matrix.mulVec, smul_dotProduct
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
inst_2 : DistribSMul R α
inst_3 : IsScalarTower R α α
b : R
M : Matrix m n α
v : n → α
x : m
⊢ ((b • M) *ᵥ v) x = (b • M *ᵥ v) x

Tactic:
exact smul_dotProduct _ _ _

Premises used: smul_dotProduct
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype m
inst_2 : DistribSMul R α
inst_3 : IsScalarTower R α α
b : R
v : m → α
M : Matrix m n α
h : ∀ (x : n), ((b • v) ᵥ* M) x = (b • v ᵥ* M) x
⊢ (b • v) ᵥ* M = b • v ᵥ* M

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype m
inst_2 : DistribSMul R α
inst_3 : IsScalarTower R α α
b : R
v : m → α
M : Matrix m n α
x : n
⊢ ((b • v) ᵥ* M) x = (b • v ᵥ* M) x

Tactic:
smul_dotProduct _ _ _

Premises used: Matrix.vecMul, smul_dotProduct
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype m
inst_2 : DistribSMul R α
inst_3 : IsScalarTower R α α
b : R
v : m → α
M : Matrix m n α
x : n
⊢ ((b • v) ᵥ* M) x = (b • v ᵥ* M) x

Tactic:
exact smul_dotProduct _ _ _

Premises used: smul_dotProduct
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype m
inst_2 : DistribSMul R α
inst_3 : SMulCommClass R α α
v : m → α
b : R
M : Matrix m n α
h : ∀ (x : n), (v ᵥ* (b • M)) x = (b • v ᵥ* M) x
⊢ v ᵥ* (b • M) = b • v ᵥ* M

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype m
inst_2 : DistribSMul R α
inst_3 : SMulCommClass R α α
v : m → α
b : R
M : Matrix m n α
x : n
⊢ (v ᵥ* (b • M)) x = (b • v ᵥ* M) x

Tactic:
dotProduct_smul _ _ _

Premises used: Matrix.vecMul, dotProduct_smul
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype m
inst_2 : DistribSMul R α
inst_3 : SMulCommClass R α α
v : m → α
b : R
M : Matrix m n α
x : n
⊢ (v ᵥ* (b • M)) x = (b • v ᵥ* M) x

Tactic:
exact dotProduct_smul _ _ _

Premises used: dotProduct_smul
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : NonUnitalNonAssocSemiring R
M : Matrix m n R
j : n
x : R
⊢ M *ᵥ Pi.single (M := fun (a : n) ↦ R) j x = MulOpposite.op x • M.col j

Tactic:
funext fun _ => dotProduct_single _ _ _

Premises used: funext, dotProduct_single
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring R
M : Matrix m n R
i : m
x : R
⊢ Pi.single (M := fun (a : m) ↦ R) i x ᵥ* M = x • M.row i

Tactic:
funext fun _ => single_dotProduct _ _ _

Premises used: single_dotProduct, funext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : NonAssocSemiring R
M : Matrix m n R
j : n
h : ∀ (x : m), (M *ᵥ Pi.single (M := fun (a : n) ↦ R) j 1) x = M.col j x
⊢ M *ᵥ Pi.single (M := fun (a : n) ↦ R) j 1 = M.col j

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : NonAssocSemiring R
M : Matrix m n R
j : n
x : m
⊢ (M *ᵥ Pi.single (M := fun (a : n) ↦ R) j 1) x = M.col j x

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonAssocSemiring R
i : m
M : Matrix m n R
h : ∀ (x : n), (Pi.single (M := fun (a : m) ↦ R) i 1 ᵥ* M) x = M.row i x
⊢ Pi.single (M := fun (a : m) ↦ R) i 1 ᵥ* M = M.row i

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonAssocSemiring R
i : m
M : Matrix m n R
x : n
⊢ (Pi.single (M := fun (a : m) ↦ R) i 1 ᵥ* M) x = M.row i x

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Mul
Goal:
n : Type u_3
R : Type u_7
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
h : ∀ (i : n), (diagonal v *ᵥ Pi.single (M := fun (a : n) ↦ R) j x) i = Pi.single (M := fun (j : n) ↦ R) j (v j * x) i
⊢ diagonal v *ᵥ Pi.single (M := fun (a : n) ↦ R) j x = Pi.single (M := fun (j : n) ↦ R) j (v j * x)

Tactic:
ext i
-- Module: Mathlib.Data.Matrix.Mul
Goal:
n : Type u_3
R : Type u_7
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
i : n
h :
  HMul.hMul (β := R) (v i) (Pi.single (M := fun (a : n) ↦ R) j x i : R) = Pi.single (M := fun (j : n) ↦ R) j (v j * x) i
⊢ (diagonal v *ᵥ Pi.single (M := fun (a : n) ↦ R) j x) i = Pi.single (M := fun (j : n) ↦ R) j (v j * x) i

Tactic:
rw [mulVec_diagonal]

Premises used: Matrix.mulVec_diagonal
-- Module: Mathlib.Data.Matrix.Mul
Goal:
n : Type u_3
R : Type u_7
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
i : n
⊢ HMul.hMul (β := R) (v i) (Pi.single (M := fun (a : n) ↦ R) j x i : R) = Pi.single (M := fun (j : n) ↦ R) j (v j * x) i

Tactic:
Pi.apply_single (fun i x => v i * x) (fun i => mul_zero _) j x i

Premises used: HMul.hMul, Pi.apply_single, MulZeroClass.mul_zero
-- Module: Mathlib.Data.Matrix.Mul
Goal:
n : Type u_3
R : Type u_7
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
i : n
⊢ HMul.hMul (β := R) (v i) (Pi.single (M := fun (a : n) ↦ R) j x i : R) = Pi.single (M := fun (j : n) ↦ R) j (v j * x) i

Tactic:
exact Pi.apply_single (fun i x => v i * x) (fun i => mul_zero _) j x i

Premises used: HMul.hMul, Pi.apply_single, MulZeroClass.mul_zero
-- Module: Mathlib.Data.Matrix.Mul
Goal:
n : Type u_3
R : Type u_7
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
h : ∀ (i : n), (Pi.single (M := fun (a : n) ↦ R) j x ᵥ* diagonal v) i = Pi.single (M := fun (j : n) ↦ R) j (x * v j) i
⊢ Pi.single (M := fun (a : n) ↦ R) j x ᵥ* diagonal v = Pi.single (M := fun (j : n) ↦ R) j (x * v j)

Tactic:
ext i
-- Module: Mathlib.Data.Matrix.Mul
Goal:
n : Type u_3
R : Type u_7
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
i : n
h :
  HMul.hMul (α := R) (Pi.single (M := fun (a : n) ↦ R) j x i : R) (v i) = Pi.single (M := fun (j : n) ↦ R) j (x * v j) i
⊢ (Pi.single (M := fun (a : n) ↦ R) j x ᵥ* diagonal v) i = Pi.single (M := fun (j : n) ↦ R) j (x * v j) i

Tactic:
rw [vecMul_diagonal]

Premises used: Matrix.vecMul_diagonal
-- Module: Mathlib.Data.Matrix.Mul
Goal:
n : Type u_3
R : Type u_7
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
i : n
⊢ HMul.hMul (α := R) (Pi.single (M := fun (a : n) ↦ R) j x i : R) (v i) = Pi.single (M := fun (j : n) ↦ R) j (x * v j) i

Tactic:
Pi.apply_single (fun i x => x * v i) (fun i => zero_mul _) j x i

Premises used: HMul.hMul, MulZeroClass.zero_mul, Pi.apply_single
-- Module: Mathlib.Data.Matrix.Mul
Goal:
n : Type u_3
R : Type u_7
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
i : n
⊢ HMul.hMul (α := R) (Pi.single (M := fun (a : n) ↦ R) j x i : R) (v i) = Pi.single (M := fun (j : n) ↦ R) j (x * v j) i

Tactic:
exact Pi.apply_single (fun i x => x * v i) (fun i => zero_mul _) j x i

Premises used: HMul.hMul, MulZeroClass.zero_mul, Pi.apply_single
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype n
inst_2 : Fintype m
v : m → α
M : Matrix m n α
N : Matrix n o α
h : ∀ (x : o), (v ᵥ* M ᵥ* N) x = (v ᵥ* (M * N)) x
⊢ v ᵥ* M ᵥ* N = v ᵥ* (M * N)

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype n
inst_2 : Fintype m
v : m → α
M : Matrix m n α
N : Matrix n o α
x : o
⊢ (v ᵥ* M ᵥ* N) x = (v ᵥ* (M * N)) x

Tactic:
apply dotProduct_assoc

Premises used: dotProduct_assoc
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype n
inst_2 : Fintype o
v : o → α
M : Matrix m n α
N : Matrix n o α
h : ∀ (x : m), (M *ᵥ N *ᵥ v) x = ((M * N) *ᵥ v) x
⊢ M *ᵥ N *ᵥ v = (M * N) *ᵥ v

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype n
inst_2 : Fintype o
v : o → α
M : Matrix m n α
N : Matrix n o α
x : m
h : ((M * N) *ᵥ v) x = (M *ᵥ N *ᵥ v) x
⊢ (M *ᵥ N *ᵥ v) x = ((M * N) *ᵥ v) x

Tactic:
symm
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype n
inst_2 : Fintype o
v : o → α
M : Matrix m n α
N : Matrix n o α
x : m
⊢ ((M * N) *ᵥ v) x = (M *ᵥ N *ᵥ v) x

Tactic:
apply dotProduct_assoc

Premises used: dotProduct_assoc
-- Module: Mathlib.Data.Matrix.Mul
Goal:
n : Type u_3
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype n
A B C : Matrix n n α
i j : n
rw : (A * (B * C)) i j = A i ⬝ᵥ B *ᵥ Cᵀ j
⊢ (A * B * C) i j = A i ⬝ᵥ B *ᵥ Cᵀ j

Tactic:
rw [Matrix.mul_assoc]

Premises used: Matrix.mul_assoc
-- Module: Mathlib.Data.Matrix.Mul
Goal:
n : Type u_3
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype n
A B C : Matrix n n α
i j : n
⊢ (A * (B * C)) i j = A i ⬝ᵥ B *ᵥ Cᵀ j

Tactic:
simp [mul_apply, dotProduct, mulVec]

Premises used: dotProduct, Matrix.mul_apply, Matrix.mulVec
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype m
u v : m → α
w : n → α
h : ∀ (i : n), (u ᵥ* vecMulVec v w) i = ((u ⬝ᵥ v) • w) i
⊢ u ᵥ* vecMulVec v w = (u ⬝ᵥ v) • w

Tactic:
ext i
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype m
u v : m → α
w : n → α
i : n
⊢ (u ᵥ* vecMulVec v w) i = ((u ⬝ᵥ v) • w) i

Tactic:
simp [vecMul, dotProduct, vecMulVec, Finset.sum_mul, mul_assoc]

Premises used: dotProduct, mul_assoc, Matrix.vecMul, Finset.sum_mul, Matrix.vecMulVec
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype n
u : m → α
v w : n → α
h : ∀ (i : m), (vecMulVec u v *ᵥ w) i = (MulOpposite.op (v ⬝ᵥ w) • u) i
⊢ vecMulVec u v *ᵥ w = MulOpposite.op (v ⬝ᵥ w) • u

Tactic:
ext i
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype n
u : m → α
v w : n → α
i : m
⊢ (vecMulVec u v *ᵥ w) i = (MulOpposite.op (v ⬝ᵥ w) • u) i

Tactic:
simp [mulVec, dotProduct, vecMulVec, Finset.mul_sum, mul_assoc]

Premises used: Finset.mul_sum, dotProduct, mul_assoc, Matrix.mulVec, Matrix.vecMulVec
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype m
M : Matrix l m α
x : m → α
y : n → α
a : ∀ (i : l) (j : n), (M * vecMulVec x y) i j = vecMulVec (M *ᵥ x) y i j
⊢ M * vecMulVec x y = vecMulVec (M *ᵥ x) y

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype m
M : Matrix l m α
x : m → α
y : n → α
i : l
j : n
a : ∑ j_1 : m, M i j_1 * vecMulVec x y j_1 j = vecMulVec (M *ᵥ x) y i j
a₁ : ∑ x_1 : m, M i x_1 * (x x_1 * y j) = (M *ᵥ x) i * y j
a₂ : ∑ x_1 : m, M i x_1 * (x x_1 * y j) = (fun (j : m) ↦ M i j) ⬝ᵥ x * y j
a₃ : ∑ x_1 : m, M i x_1 * (x x_1 * y j) = (∑ x_1 : m, M i x_1 * x x_1) * y j
a₄ : Eq.{v + 1} (α := α) (∑ x_1 : m, M i x_1 * (x x_1 * y j)) (∑ i_1 : m, M i i_1 * x i_1 * y j)
⊢ (M * vecMulVec x y) i j = vecMulVec (M *ᵥ x) y i j

Tactic:
simp_rw [mul_apply, vecMulVec_apply, mulVec, dotProduct, Finset.sum_mul, mul_assoc]

Premises used: dotProduct, mul_assoc, Matrix.mul_apply, Matrix.vecMulVec_apply, Matrix.mulVec, Finset.sum_mul
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype m
x : l → α
y : m → α
M : Matrix m n α
a : ∀ (i : l) (j : n), (vecMulVec x y * M) i j = vecMulVec x (y ᵥ* M) i j
⊢ vecMulVec x y * M = vecMulVec x (y ᵥ* M)

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype m
x : l → α
y : m → α
M : Matrix m n α
i : l
j : n
a : ∑ j_1 : m, vecMulVec x y i j_1 * M j_1 j = vecMulVec x (y ᵥ* M) i j
a₁ : ∑ x_1 : m, x i * y x_1 * M x_1 j = x i * (y ᵥ* M) j
a₂ : ∑ x_1 : m, x i * y x_1 * M x_1 j = x i * y ⬝ᵥ fun (i : m) ↦ M i j
a₃ : ∑ x_1 : m, x i * y x_1 * M x_1 j = x i * ∑ x : m, y x * M x j
a₄ : Eq.{v + 1} (α := α) (∑ x_1 : m, x i * y x_1 * M x_1 j) (∑ i_1 : m, x i * (y i_1 * M i_1 j))
⊢ (vecMulVec x y * M) i j = vecMulVec x (y ᵥ* M) i j

Tactic:
simp_rw [mul_apply, vecMulVec_apply, vecMul, dotProduct, Finset.mul_sum, mul_assoc]

Premises used: Finset.mul_sum, dotProduct, mul_assoc, Matrix.vecMul, Matrix.mul_apply, Matrix.vecMulVec_apply
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype m
u : l → α
v w : m → α
x : n → α
rw : vecMulVec u (v ᵥ* vecMulVec w x) = vecMulVec u ((v ⬝ᵥ w) • x)
rw₁ rw₂ : vecMulVec u ((v ⬝ᵥ w) • x) = vecMulVec u ((v ⬝ᵥ w) • x)
⊢ vecMulVec u v * vecMulVec w x = vecMulVec u ((v ⬝ᵥ w) • x)

Tactic:
rw [vecMulVec_mul, vecMul_vecMulVec]

Premises used: Matrix.vecMul_vecMulVec, Matrix.vecMulVec_mul
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype m
inst_2 : Nonempty n
A : Matrix l m α
⊢ (Function.Injective (β := Matrix l n α) fun (B : Matrix m n α) ↦ A * B) ↔ Function.Injective A.mulVec

Tactic:
⟨fun ha v w hvw => ?_, fun ha B C hBC => ext_col fun j => ha congr(($hBC).col j)⟩

Premises used: Matrix.ext_col, congrArg, id, Iff.intro, Matrix.col
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype m
inst_2 : Nonempty n
A : Matrix l m α
refine :
  ∀ (ha : Function.Injective (β := Matrix l n α) fun (B : Matrix m n α) ↦ A * B) (v w : m → α) (hvw : A *ᵥ v = A *ᵥ w),
    v = w
⊢ (Function.Injective (β := Matrix l n α) fun (B : Matrix m n α) ↦ A * B) ↔ Function.Injective A.mulVec

Tactic:
refine ⟨fun ha v w hvw => ?_, fun ha B C hBC => ext_col fun j => ha congr(($hBC).col j)⟩
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype m
inst_2 : Nonempty n
A : Matrix l m α
ha : Function.Injective (β := Matrix l n α) fun (B : Matrix m n α) ↦ A * B
v w : m → α
hvw : A *ᵥ v = A *ᵥ w
inhabit : ∀ (inhabited_h : Inhabited n), v = w
⊢ v = w

Tactic:
inhabit n