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
α : 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
inhabited_h : Inhabited n
suffices :
  Eq (α := Matrix m n α) ((of : (a : m → n → α) → Matrix m n α) fun (i : m) (j : n) ↦ v i)
    ((of : (a : m → n → α) → Matrix m n α) fun (i : m) (j : n) ↦ w i)
⊢ v = w

Tactic:
suffices (of fun i j => v i) = (of fun i j => w i) from
    funext fun i => congrFun₂ this i (default : n)
-- 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
inhabited_h : Inhabited n
⊢ Eq (α := Matrix m n α) ((of : (a : m → n → α) → Matrix m n α) fun (i : m) (j : n) ↦ v i)
    ((of : (a : m → n → α) → Matrix m n α) fun (i : m) (j : n) ↦ w i)

Tactic:
ha <| ext fun _ _ => congrFun hvw _

Premises used: congrFun, Matrix.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
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
inhabited_h : Inhabited n
⊢ Eq (α := Matrix m n α) ((of : (a : m → n → α) → Matrix m n α) fun (i : m) (j : n) ↦ v i)
    ((of : (a : m → n → α) → Matrix m n α) fun (i : m) (j : n) ↦ w i)

Tactic:
exact ha <| ext fun _ _ => congrFun hvw _

Premises used: congrFun, Matrix.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 : Nonempty l
inst_2 : Fintype m
A : Matrix m n α
⊢ (Function.Injective (β := Matrix l n α) fun (B : Matrix l m α) ↦ B * A) ↔
    Function.Injective (β := n → α) fun (v : m → α) ↦ v ᵥ* A

Tactic:
⟨fun ha v w hvw => ?_, fun ha B C hBC => ext_row fun i => ha congr(($hBC).row i)⟩

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

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

Tactic:
inhabit l
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalSemiring α
inst_1 : Nonempty l
inst_2 : Fintype m
A : Matrix m n α
ha : Function.Injective (β := Matrix l n α) fun (B : Matrix l m α) ↦ B * A
v w : m → α
hvw : Eq (α := n → α) ((fun (v : m → α) ↦ v ᵥ* A) v) ((fun (v : m → α) ↦ v ᵥ* A) w)
inhabited_h : Inhabited l
suffices :
  Eq (α := Matrix l m α) ((of : (a : l → m → α) → Matrix l m α) fun (i : l) (j : m) ↦ v j)
    ((of : (a : l → m → α) → Matrix l m α) fun (i : l) (j : m) ↦ w j)
⊢ v = w

Tactic:
suffices (of fun i j => v j) = (of fun i j => w j) from
    funext fun j => congrFun₂ this (default : l) 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 : Nonempty l
inst_2 : Fintype m
A : Matrix m n α
ha : Function.Injective (β := Matrix l n α) fun (B : Matrix l m α) ↦ B * A
v w : m → α
hvw : Eq (α := n → α) ((fun (v : m → α) ↦ v ᵥ* A) v) ((fun (v : m → α) ↦ v ᵥ* A) w)
inhabited_h : Inhabited l
⊢ Eq (α := Matrix l m α) ((of : (a : l → m → α) → Matrix l m α) fun (i : l) (j : m) ↦ v j)
    ((of : (a : l → m → α) → Matrix l m α) fun (i : l) (j : m) ↦ w j)

Tactic:
ha <| ext fun _ _ => congrFun hvw _

Premises used: congrFun, Matrix.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 : Nonempty l
inst_2 : Fintype m
A : Matrix m n α
ha : Function.Injective (β := Matrix l n α) fun (B : Matrix l m α) ↦ B * A
v w : m → α
hvw : Eq (α := n → α) ((fun (v : m → α) ↦ v ᵥ* A) v) ((fun (v : m → α) ↦ v ᵥ* A) w)
inhabited_h : Inhabited l
⊢ Eq (α := Matrix l m α) ((of : (a : l → m → α) → Matrix l m α) fun (i : l) (j : m) ↦ v j)
    ((of : (a : l → m → α) → Matrix l m α) fun (i : l) (j : m) ↦ w j)

Tactic:
exact ha <| ext fun _ _ => congrFun hvw _

Premises used: congrFun, Matrix.ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype m
A : Matrix m m α
inl : IsEmpty m → (IsLeftRegular A ↔ Function.Injective A.mulVec)
inr : Nonempty m → (IsLeftRegular A ↔ Function.Injective A.mulVec)
⊢ IsLeftRegular A ↔ Function.Injective A.mulVec

Tactic:
cases isEmpty_or_nonempty m

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype m
A : Matrix m m α
h : IsEmpty m
⊢ IsLeftRegular A ↔ Function.Injective A.mulVec

Tactic:
simp [IsLeftRegular, Function.injective_of_subsingleton]

Premises used: Function.injective_of_subsingleton, IsLeftRegular
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype m
A : Matrix m m α
h : Nonempty m
⊢ IsLeftRegular A ↔ Function.Injective A.mulVec

Tactic:
mul_right_injective_iff_mulVec_injective

Premises used: Matrix.mul_right_injective_iff_mulVec_injective
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype m
A : Matrix m m α
h : Nonempty m
⊢ IsLeftRegular A ↔ Function.Injective A.mulVec

Tactic:
exact mul_right_injective_iff_mulVec_injective

Premises used: Matrix.mul_right_injective_iff_mulVec_injective
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype m
A : Matrix m m α
inl : IsEmpty m → (IsRightRegular A ↔ Function.Injective (β := m → α) fun (v : m → α) ↦ v ᵥ* A)
inr : Nonempty m → (IsRightRegular A ↔ Function.Injective (β := m → α) fun (v : m → α) ↦ v ᵥ* A)
⊢ IsRightRegular A ↔ Function.Injective (β := m → α) fun (v : m → α) ↦ v ᵥ* A

Tactic:
cases isEmpty_or_nonempty m

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype m
A : Matrix m m α
h : IsEmpty m
⊢ IsRightRegular A ↔ Function.Injective (β := m → α) fun (v : m → α) ↦ v ᵥ* A

Tactic:
simp [IsRightRegular, Function.injective_of_subsingleton]

Premises used: Function.injective_of_subsingleton, IsRightRegular
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype m
A : Matrix m m α
h : Nonempty m
⊢ IsRightRegular A ↔ Function.Injective (β := m → α) fun (v : m → α) ↦ v ᵥ* A

Tactic:
mul_left_injective_iff_vecMul_injective

Premises used: Matrix.mul_left_injective_iff_vecMul_injective
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype m
A : Matrix m m α
h : Nonempty m
⊢ IsRightRegular A ↔ Function.Injective (β := m → α) fun (v : m → α) ↦ v ᵥ* A

Tactic:
exact mul_left_injective_iff_vecMul_injective

Premises used: Matrix.mul_left_injective_iff_vecMul_injective
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonAssocSemiring α
inst_1 : Fintype n
A : Matrix m n α
h : ∀ (x : m), (A *ᵥ 1) x = (∑ j : n, Aᵀ j) x
⊢ A *ᵥ 1 = ∑ j : n, Aᵀ j

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonAssocSemiring α
inst_1 : Fintype n
A : Matrix m n α
x : m
⊢ (A *ᵥ 1) x = (∑ j : n, Aᵀ j) x

Tactic:
simp [mulVec, dotProduct]

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

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

Tactic:
simp [vecMul, dotProduct]

Premises used: dotProduct, Matrix.vecMul
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonAssocSemiring α
inst_1 : DecidableEq n
inst_2 : Fintype n
M N : Matrix m n α
h : ∀ (i : n), M *ᵥ Pi.single (M := fun (a : n) ↦ α) i 1 = N *ᵥ Pi.single (M := fun (a : n) ↦ α) i 1
a : ∀ (i : m) (j : n), M i j = N i j
⊢ M = N

Tactic:
ext i j
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonAssocSemiring α
inst_1 : DecidableEq n
inst_2 : Fintype n
M N : Matrix m n α
h : ∀ (i : n), M *ᵥ Pi.single (M := fun (a : n) ↦ α) i 1 = N *ᵥ Pi.single (M := fun (a : n) ↦ α) i 1
i : m
j : n
⊢ ∀ (i : n), M.col i = N.col i

Tactic:
simp_rw [mulVec_single_one] at h

Premises used: Matrix.mulVec_single_one
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonAssocSemiring α
inst_1 : DecidableEq n
inst_2 : Fintype n
M N : Matrix m n α
i : m
j : n
h : ∀ (i : n), M.col i = N.col i
⊢ M i j = N i j

Tactic:
congrFun (h j) i

Premises used: congrFun, Matrix.transpose, Matrix.col
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonAssocSemiring α
inst_1 : DecidableEq n
inst_2 : Fintype n
M N : Matrix m n α
i : m
j : n
h : ∀ (i : n), M.col i = N.col i
⊢ M i j = N i j

Tactic:
exact congrFun (h j) i

Premises used: congrFun
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonAssocSemiring α
inst_1 : DecidableEq m
inst_2 : Fintype m
M N : Matrix m n α
h : ∀ (i : m), Pi.single (M := fun (a : m) ↦ α) i 1 ᵥ* M = Pi.single (M := fun (a : m) ↦ α) i 1 ᵥ* N
a : ∀ (i : m) (j : n), M i j = N i j
⊢ M = N

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

Tactic:
simp_rw [single_one_vecMul] at h

Premises used: Matrix.single_one_vecMul
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonAssocSemiring α
inst_1 : DecidableEq m
inst_2 : Fintype m
M N : Matrix m n α
i : m
j : n
h : ∀ (i : m), M.row i = N.row i
⊢ M i j = N i j

Tactic:
congrFun (h i) j

Premises used: congrFun, Matrix.row
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonAssocSemiring α
inst_1 : DecidableEq m
inst_2 : Fintype m
M N : Matrix m n α
i : m
j : n
h : ∀ (i : m), M.row i = N.row i
⊢ M i j = N i j

Tactic:
exact congrFun (h i) j

Premises used: congrFun
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonAssocSemiring α
inst_1 : Fintype n
A B : Matrix m n α
h : A.mulVec = B.mulVec
a : ∀ (i : m) (j : n), A i j = B i j
⊢ A = B

Tactic:
ext i j
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonAssocSemiring α
inst_1 : Fintype n
A B : Matrix m n α
h : A.mulVec = B.mulVec
i : m
j : n
⊢ A i j = B i j

Tactic:
simpa using congrFun₂ h (Pi.single j 1) i

Premises used: congrFun₂, Pi.single, OfNat.ofNat
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonAssocSemiring α
inst_1 : Fintype n
A B : Matrix m n α
h : A.mulVec = B.mulVec
i : m
j : n
⊢ A i j = B i j

Tactic:
classical
  simpa using congrFun₂ h (Pi.single j 1) i
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonAssocSemiring α
inst_1 : Fintype n
A B : Matrix m n α
⊢ A = B ↔ ∀ (v : n → α), A *ᵥ v = B *ᵥ v

Tactic:
mulVec_injective.eq_iff.symm.trans funext_iff

Premises used: Matrix.mulVec_injective, Function.Injective.eq_iff, funext_iff, Iff.trans, Iff.symm
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonAssocSemiring α
inst_1 : Fintype m
A B : Matrix m n α
h :
  Eq (α := (v : m → α) → n → α) ((fun (x : Matrix m n α) (v : m → α) ↦ v ᵥ* x) A)
    ((fun (x : Matrix m n α) (v : m → α) ↦ v ᵥ* x) B)
a : ∀ (i : m) (j : n), A i j = B i j
⊢ A = B

Tactic:
ext i j
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonAssocSemiring α
inst_1 : Fintype m
A B : Matrix m n α
h :
  Eq (α := (v : m → α) → n → α) ((fun (x : Matrix m n α) (v : m → α) ↦ v ᵥ* x) A)
    ((fun (x : Matrix m n α) (v : m → α) ↦ v ᵥ* x) B)
i : m
j : n
⊢ A i j = B i j

Tactic:
simpa using congrFun₂ h (Pi.single i 1) j

Premises used: congrFun₂, Pi.single, OfNat.ofNat
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonAssocSemiring α
inst_1 : Fintype m
A B : Matrix m n α
h :
  Eq (α := (v : m → α) → n → α) ((fun (x : Matrix m n α) (v : m → α) ↦ v ᵥ* x) A)
    ((fun (x : Matrix m n α) (v : m → α) ↦ v ᵥ* x) B)
i : m
j : n
⊢ A i j = B i j

Tactic:
classical
  simpa using congrFun₂ h (Pi.single i 1) j
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonAssocSemiring α
inst_1 : Fintype m
A B : Matrix m n α
⊢ A = B ↔ ∀ (v : m → α), v ᵥ* A = v ᵥ* B

Tactic:
vecMul_injective.eq_iff.symm.trans funext_iff

Premises used: Function.Injective.eq_iff, funext_iff, Matrix.vecMul_injective, Iff.trans, Iff.symm
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : NonAssocSemiring α
inst_1 : Fintype m
inst_2 : DecidableEq m
v : m → α
h : ∀ (x : m), (1 *ᵥ v) x = v x
⊢ 1 *ᵥ v = v

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : NonAssocSemiring α
inst_1 : Fintype m
inst_2 : DecidableEq m
v : m → α
x : m
h : ((diagonal fun (x : m) ↦ 1) *ᵥ v) x = v x
h₁ : 1 * v x = v x
h₂ h₃ : v x = v x
⊢ (1 *ᵥ v) x = v x

Tactic:
rw [← diagonal_one, mulVec_diagonal, one_mul]

Premises used: Matrix.diagonal_one, Matrix.mulVec_diagonal, one_mul
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : NonAssocSemiring α
inst_1 : Fintype m
inst_2 : DecidableEq m
v : m → α
h : ∀ (x : m), (v ᵥ* 1) x = v x
⊢ v ᵥ* 1 = v

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : NonAssocSemiring α
inst_1 : Fintype m
inst_2 : DecidableEq m
v : m → α
x : m
h : (v ᵥ* diagonal fun (x : m) ↦ 1) x = v x
h₁ : v x * 1 = v x
h₂ h₃ : v x = v x
⊢ (v ᵥ* 1) x = v x

Tactic:
rw [← diagonal_one, vecMul_diagonal, mul_one]

Premises used: Matrix.vecMul_diagonal, Matrix.diagonal_one, mul_one
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : NonAssocSemiring α
inst_1 : Fintype m
inst_2 : DecidableEq m
x : α
v : m → α
h : ∀ (x_1 : m), ((diagonal fun (x_2 : m) ↦ x) *ᵥ v) x_1 = (x • v) x_1
⊢ (diagonal fun (x_1 : m) ↦ x) *ᵥ v = x • v

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : NonAssocSemiring α
inst_1 : Fintype m
inst_2 : DecidableEq m
x : α
v : m → α
x_1 : m
⊢ ((diagonal fun (x_2 : m) ↦ x) *ᵥ v) x_1 = (x • v) x_1

Tactic:
simp [mulVec_diagonal]

Premises used: Matrix.mulVec_diagonal
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : NonAssocSemiring α
inst_1 : Fintype m
inst_2 : DecidableEq m
x : α
v : m → α
h : ∀ (x_1 : m), (v ᵥ* diagonal fun (x_2 : m) ↦ x) x_1 = (MulOpposite.op x • v) x_1
⊢ (v ᵥ* diagonal fun (x_1 : m) ↦ x) = MulOpposite.op x • v

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : NonAssocSemiring α
inst_1 : Fintype m
inst_2 : DecidableEq m
x : α
v : m → α
x_1 : m
⊢ (v ᵥ* diagonal fun (x_2 : m) ↦ x) x_1 = (MulOpposite.op x • v) x_1

Tactic:
simp [vecMul_diagonal]

Premises used: Matrix.vecMul_diagonal
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : NonAssocSemiring α
inst_1 : Fintype m
inst_2 : DecidableEq m
x : ℕ
v : m → α
⊢ (↑x : Matrix m m α) *ᵥ v = HSMul.hSMul (α := α) (↑x : α) v

Tactic:
diagonal_const_mulVec _ _

Premises used: Matrix.diagonal_const_mulVec
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : NonAssocSemiring α
inst_1 : Fintype m
inst_2 : DecidableEq m
x : ℕ
v : m → α
⊢ v ᵥ* (↑x : Matrix m m α) = HSMul.hSMul (α := αᵐᵒᵖ) (MulOpposite.op (↑x : α)) v

Tactic:
vecMul_diagonal_const _ _

Premises used: Matrix.vecMul_diagonal_const
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : NonAssocSemiring α
inst_1 : Fintype m
inst_2 : DecidableEq m
x : ℕ
inst_3 : x.AtLeastTwo
v : m → α
⊢ OfNat.ofNat x *ᵥ v = HSMul.hSMul (α := α) (OfNat.ofNat x) v

Tactic:
natCast_mulVec _ _

Premises used: Matrix.natCast_mulVec
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : NonAssocSemiring α
inst_1 : Fintype m
inst_2 : DecidableEq m
x : ℕ
inst_3 : x.AtLeastTwo
v : m → α
⊢ v ᵥ* OfNat.ofNat x = HSMul.hSMul (α := αᵐᵒᵖ) (MulOpposite.op (OfNat.ofNat x)) v

Tactic:
vecMul_natCast _ _

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

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

Tactic:
apply neg_dotProduct

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

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

Tactic:
apply dotProduct_neg

Premises used: dotProduct_neg
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocRing α
inst_1 : Fintype m
v : m → α
A : Matrix m n α
rw : -(-v ᵥ* A) = v ᵥ* A
rw₁ : - -(v ᵥ* A) = v ᵥ* A
rw₂ rw₃ : v ᵥ* A = v ᵥ* A
⊢ -v ᵥ* -A = v ᵥ* A

Tactic:
rw [vecMul_neg, neg_vecMul, neg_neg]

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

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

Tactic:
apply neg_dotProduct

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

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

Tactic:
apply dotProduct_neg

Premises used: dotProduct_neg
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocRing α
inst_1 : Fintype n
v : n → α
A : Matrix m n α
rw : -(-A *ᵥ v) = A *ᵥ v
rw₁ : - -(A *ᵥ v) = A *ᵥ v
rw₂ rw₃ : A *ᵥ v = A *ᵥ v
⊢ -A *ᵥ -v = A *ᵥ v

Tactic:
rw [mulVec_neg, neg_mulVec, neg_neg]

Premises used: neg_neg, Matrix.neg_mulVec, Matrix.mulVec_neg
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocRing α
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 : NonUnitalNonAssocRing α
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_sub

Premises used: dotProduct_sub
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocRing α
inst_1 : Fintype n
A B : Matrix m n α
x : n → α
⊢ (A - B) *ᵥ x = A *ᵥ x - B *ᵥ x

Tactic:
simp [sub_eq_add_neg, add_mulVec, neg_mulVec]

Premises used: Matrix.add_mulVec, sub_eq_add_neg, Matrix.neg_mulVec
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocRing α
inst_1 : Fintype m
A B : Matrix m n α
x : m → α
⊢ x ᵥ* (A - B) = x ᵥ* A - x ᵥ* B

Tactic:
simp [sub_eq_add_neg, vecMul_add, vecMul_neg]

Premises used: Matrix.vecMul_neg, sub_eq_add_neg, Matrix.vecMul_add
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocRing α
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 : NonUnitalNonAssocRing α
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 sub_dotProduct

Premises used: sub_dotProduct
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocRing α
w₁ w₂ : m → α
v : n → α
⊢ vecMulVec (w₁ - w₂) v = vecMulVec w₁ v - vecMulVec w₂ v

Tactic:
ext fun _ _ => sub_mul _ _ _

Premises used: sub_mul, Matrix.ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocRing α
w : m → α
v₁ v₂ : n → α
⊢ vecMulVec w (v₁ - v₂) = vecMulVec w v₁ - vecMulVec w v₂

Tactic:
ext fun _ _ => mul_sub _ _ _

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

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

Tactic:
apply dotProduct_comm

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

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

Tactic:
apply dotProduct_comm

Premises used: dotProduct_comm
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : NonUnitalCommSemiring α
inst_1 : Fintype m
A : Matrix m m α
x y : m → α
rw : x ᵥ* Aᵀ ⬝ᵥ y = y ⬝ᵥ A *ᵥ x
rw₁ : y ⬝ᵥ x ᵥ* Aᵀ = y ⬝ᵥ A *ᵥ x
rw₂ rw₃ : y ⬝ᵥ A *ᵥ x = y ⬝ᵥ A *ᵥ x
⊢ x ⬝ᵥ Aᵀ *ᵥ y = y ⬝ᵥ A *ᵥ x

Tactic:
rw [dotProduct_mulVec, dotProduct_comm, vecMul_transpose]

Premises used: Matrix.vecMul_transpose, dotProduct_comm, Matrix.dotProduct_mulVec
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : NonUnitalCommSemiring α
inst_1 : Fintype m
A : Matrix m m α
x y : m → α
⊢ x ᵥ* Aᵀ ⬝ᵥ y = y ᵥ* A ⬝ᵥ x

Tactic:
simpa [dotProduct_mulVec] using dotProduct_transpose_mulVec (A := A) (x := x) (y := y)

Premises used: Matrix.dotProduct_transpose_mulVec, Matrix.dotProduct_mulVec