awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ (M * vecMulVec x y) i j = vecMulVec (M *ᵥ x) y i j
have 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
Tactic: simp_rw [mul_apply, vecMulVec_apply, mulVec, dotProduct, Finset.sum_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ (M * vecMulVec x y) i j = vecMulVec (M *ᵥ x) y i j
have 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)
Tactic: simp_rw [mul_apply, vecMulVec_apply, mulVec, dotProduct, Finset.sum_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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 α
⊢ vecMulVec x y * M = vecMulVec x (y ᵥ* M)
have a : ∀ (i : l) (j : n), (vecMulVec x y * M) i j = vecMulVec x (y ᵥ* M) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ (vecMulVec x y * M) i j = vecMulVec x (y ᵥ* M) i j
have a : ∑ j_1 : m, vecMulVec x y i j_1 * M j_1 j = vecMulVec x (y ᵥ* M) i j
Tactic: simp_rw [mul_apply, vecMulVec_apply, vecMul, dotProduct, Finset.mul_sum, mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ (vecMulVec x y * M) i j = vecMulVec x (y ᵥ* M) i j
have a₁ : ∑ x_1 : m, x i * y x_1 * M x_1 j = x i * (y ᵥ* M) j
Tactic: simp_rw [mul_apply, vecMulVec_apply, vecMul, dotProduct, Finset.mul_sum, mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ (vecMulVec x y * M) i j = vecMulVec x (y ᵥ* M) i j
have a₂ : ∑ x_1 : m, x i * y x_1 * M x_1 j = x i * y ⬝ᵥ fun (i : m) ↦ M i j
Tactic: simp_rw [mul_apply, vecMulVec_apply, vecMul, dotProduct, Finset.mul_sum, mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ (vecMulVec x y * M) i j = vecMulVec x (y ᵥ* M) i j
have a₃ : ∑ x_1 : m, x i * y x_1 * M x_1 j = x i * ∑ x : m, y x * M x j
Tactic: simp_rw [mul_apply, vecMulVec_apply, vecMul, dotProduct, Finset.mul_sum, mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ (vecMulVec x y * M) i j = vecMulVec x (y ᵥ* M) i j
have 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))
Tactic: simp_rw [mul_apply, vecMulVec_apply, vecMul, dotProduct, Finset.mul_sum, mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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 → α
⊢ vecMulVec u v * vecMulVec w x = vecMulVec u ((v ⬝ᵥ w) • x)
have rw : vecMulVec u (v ᵥ* vecMulVec w x) = vecMulVec u ((v ⬝ᵥ w) • x)
Tactic: rw [vecMulVec_mul, vecMul_vecMulVec]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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)
⊢ vecMulVec u v * vecMulVec w x = vecMulVec u ((v ⬝ᵥ w) • x)
have rw₁ : vecMulVec u ((v ⬝ᵥ w) • x) = vecMulVec u ((v ⬝ᵥ w) • x)
Tactic: rw [vecMulVec_mul, vecMul_vecMulVec]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
have refine : ∀ (ha : Function.Injective (β := Matrix l n α) fun (B : Matrix m n α) ↦ A * B) (v w : m → α) (hvw : A *ᵥ v = A *ᵥ w),
  v = w
Tactic: refine ⟨fun ha v w hvw => ?_, fun ha B C hBC => ext_col fun j => ha congr(($hBC).col j)⟩
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ v = w
have inhabit : ∀ (inhabited_h : Inhabited n), v = w
Tactic: inhabit n
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ v = w
have 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)
Tactic: suffices (of fun i j => v i) = (of fun i j => w i) from
    funext fun i => congrFun₂ this i (default : n)
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
have 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
Tactic: refine ⟨fun ha v w hvw => ?_, fun ha B C hBC => ext_row fun i => ha congr(($hBC).row i)⟩
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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)
⊢ v = w
have inhabit : ∀ (inhabited_h : Inhabited l), v = w
Tactic: inhabit l
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ v = w
have 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)
Tactic: suffices (of fun i j => v j) = (of fun i j => w j) from
    funext fun j => congrFun₂ this (default : l) j
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype m
A : Matrix m m α
⊢ IsLeftRegular A ↔ Function.Injective A.mulVec
have inl : IsEmpty m → (IsLeftRegular A ↔ Function.Injective A.mulVec)
Tactic: cases isEmpty_or_nonempty m
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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)
⊢ IsLeftRegular A ↔ Function.Injective A.mulVec
have inr : Nonempty m → (IsLeftRegular A ↔ Function.Injective A.mulVec)
Tactic: cases isEmpty_or_nonempty m
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype m
A : Matrix m m α
⊢ IsRightRegular A ↔ Function.Injective (β := m → α) fun (v : m → α) ↦ v ᵥ* A
have inl : IsEmpty m → (IsRightRegular A ↔ Function.Injective (β := m → α) fun (v : m → α) ↦ v ᵥ* A)
Tactic: cases isEmpty_or_nonempty m
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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)
⊢ IsRightRegular A ↔ Function.Injective (β := m → α) fun (v : m → α) ↦ v ᵥ* A
have inr : Nonempty m → (IsRightRegular A ↔ Function.Injective (β := m → α) fun (v : m → α) ↦ v ᵥ* A)
Tactic: cases isEmpty_or_nonempty m
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonAssocSemiring α
inst_1 : Fintype n
A : Matrix m n α
⊢ A *ᵥ 1 = ∑ j : n, Aᵀ j
have h : ∀ (x : m), (A *ᵥ 1) x = (∑ j : n, Aᵀ j) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonAssocSemiring α
inst_1 : Fintype m
A : Matrix m n α
⊢ 1 ᵥ* A = ∑ i : m, A i
have h : ∀ (x : n), (1 ᵥ* A) x = (∑ i : m, A i) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ M = N
have a : ∀ (i : m) (j : n), M i j = N i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (hypothesis)
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
⊢ M i j = N i j
have h₁ : ∀ (i : n), M.col i = N.col i
Tactic: simp_rw [mulVec_single_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ M = N
have a : ∀ (i : m) (j : n), M i j = N i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (hypothesis)
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
⊢ M i j = N i j
have h₁ : ∀ (i : m), M.row i = N.row i
Tactic: simp_rw [single_one_vecMul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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 = B
have a : ∀ (i : m) (j : n), A i j = B i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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 = B
have a : ∀ (i : m) (j : n), A i j = B i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
α : Type v
inst : NonAssocSemiring α
inst_1 : Fintype m
inst_2 : DecidableEq m
v : m → α
⊢ 1 *ᵥ v = v
have h : ∀ (x : m), (1 *ᵥ v) x = v x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
α : Type v
inst : NonAssocSemiring α
inst_1 : Fintype m
inst_2 : DecidableEq m
v : m → α
x : m
⊢ (1 *ᵥ v) x = v x
have h : ((diagonal fun (x : m) ↦ 1) *ᵥ v) x = v x
Tactic: rw [← diagonal_one, mulVec_diagonal, one_mul]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ (1 *ᵥ v) x = v x
have h₁ : 1 * v x = v x
Tactic: rw [← diagonal_one, mulVec_diagonal, one_mul]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ (1 *ᵥ v) x = v x
have h₂ : v x = v x
Tactic: rw [← diagonal_one, mulVec_diagonal, one_mul]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
α : Type v
inst : NonAssocSemiring α
inst_1 : Fintype m
inst_2 : DecidableEq m
v : m → α
⊢ v ᵥ* 1 = v
have h : ∀ (x : m), (v ᵥ* 1) x = v x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
α : Type v
inst : NonAssocSemiring α
inst_1 : Fintype m
inst_2 : DecidableEq m
v : m → α
x : m
⊢ (v ᵥ* 1) x = v x
have h : (v ᵥ* diagonal fun (x : m) ↦ 1) x = v x
Tactic: rw [← diagonal_one, vecMul_diagonal, mul_one]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ (v ᵥ* 1) x = v x
have h₁ : v x * 1 = v x
Tactic: rw [← diagonal_one, vecMul_diagonal, mul_one]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ (v ᵥ* 1) x = v x
have h₂ : v x = v x
Tactic: rw [← diagonal_one, vecMul_diagonal, mul_one]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
α : Type v
inst : NonAssocSemiring α
inst_1 : Fintype m
inst_2 : DecidableEq m
x : α
v : m → α
⊢ (diagonal fun (x_1 : m) ↦ x) *ᵥ v = x • v
have h : ∀ (x_1 : m), ((diagonal fun (x_2 : m) ↦ x) *ᵥ v) x_1 = (x • v) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
α : Type v
inst : NonAssocSemiring α
inst_1 : Fintype m
inst_2 : DecidableEq m
x : α
v : m → α
⊢ (v ᵥ* diagonal fun (x_1 : m) ↦ x) = MulOpposite.op x • v
have h : ∀ (x_1 : m), (v ᵥ* diagonal fun (x_2 : m) ↦ x) x_1 = (MulOpposite.op x • v) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocRing α
inst_1 : Fintype m
v : m → α
A : Matrix m n α
⊢ -v ᵥ* A = -(v ᵥ* A)
have h : ∀ (x : n), (-v ᵥ* A) x = (-(v ᵥ* A)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocRing α
inst_1 : Fintype m
v : m → α
A : Matrix m n α
⊢ v ᵥ* -A = -(v ᵥ* A)
have h : ∀ (x : n), (v ᵥ* -A) x = (-(v ᵥ* A)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocRing α
inst_1 : Fintype m
v : m → α
A : Matrix m n α
⊢ -v ᵥ* -A = v ᵥ* A
have rw : -(-v ᵥ* A) = v ᵥ* A
Tactic: rw [vecMul_neg, neg_vecMul, neg_neg]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ -v ᵥ* -A = v ᵥ* A
have rw₁ : - -(v ᵥ* A) = v ᵥ* A
Tactic: rw [vecMul_neg, neg_vecMul, neg_neg]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ -v ᵥ* -A = v ᵥ* A
have rw₂ : v ᵥ* A = v ᵥ* A
Tactic: rw [vecMul_neg, neg_vecMul, neg_neg]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocRing α
inst_1 : Fintype n
v : n → α
A : Matrix m n α
⊢ -A *ᵥ v = -(A *ᵥ v)
have h : ∀ (x : m), (-A *ᵥ v) x = (-(A *ᵥ v)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocRing α
inst_1 : Fintype n
v : n → α
A : Matrix m n α
⊢ A *ᵥ -v = -(A *ᵥ v)
have h : ∀ (x : m), (A *ᵥ -v) x = (-(A *ᵥ v)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocRing α
inst_1 : Fintype n
v : n → α
A : Matrix m n α
⊢ -A *ᵥ -v = A *ᵥ v
have rw : -(-A *ᵥ v) = A *ᵥ v
Tactic: rw [mulVec_neg, neg_mulVec, neg_neg]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ -A *ᵥ -v = A *ᵥ v
have rw₁ : - -(A *ᵥ v) = A *ᵥ v
Tactic: rw [mulVec_neg, neg_mulVec, neg_neg]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ -A *ᵥ -v = A *ᵥ v
have rw₂ : A *ᵥ v = A *ᵥ v
Tactic: rw [mulVec_neg, neg_mulVec, neg_neg]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocRing α
inst_1 : Fintype n
A : Matrix m n α
x y : n → α
⊢ A *ᵥ (x - y) = A *ᵥ x - A *ᵥ y
have h : ∀ (x_1 : m), (A *ᵥ (x - y)) x_1 = (A *ᵥ x - A *ᵥ y) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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 - y) ᵥ* A = x ᵥ* A - y ᵥ* A
have h : ∀ (x_1 : n), ((x - y) ᵥ* A) x_1 = (x ᵥ* A - y ᵥ* A) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalCommSemiring α
inst_1 : Fintype m
A : Matrix m n α
x : m → α
⊢ Aᵀ *ᵥ x = x ᵥ* A
have h : ∀ (x_1 : n), (Aᵀ *ᵥ x) x_1 = (x ᵥ* A) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalCommSemiring α
inst_1 : Fintype n
A : Matrix m n α
x : n → α
⊢ x ᵥ* Aᵀ = A *ᵥ x
have h : ∀ (x_1 : m), (x ᵥ* Aᵀ) x_1 = (A *ᵥ x) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
have rw : x ᵥ* Aᵀ ⬝ᵥ y = y ⬝ᵥ A *ᵥ x
Tactic: rw [dotProduct_mulVec, dotProduct_comm, vecMul_transpose]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ x ⬝ᵥ Aᵀ *ᵥ y = y ⬝ᵥ A *ᵥ x
have rw₁ : y ⬝ᵥ x ᵥ* Aᵀ = y ⬝ᵥ A *ᵥ x
Tactic: rw [dotProduct_mulVec, dotProduct_comm, vecMul_transpose]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ x ⬝ᵥ Aᵀ *ᵥ y = y ⬝ᵥ A *ᵥ x
have rw₂ : y ⬝ᵥ A *ᵥ x = y ⬝ᵥ A *ᵥ x
Tactic: rw [dotProduct_mulVec, dotProduct_comm, vecMul_transpose]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : NonUnitalCommSemiring α
inst_1 : Fintype n
inst_2 : Fintype o
A : Matrix m n α
B : Matrix o n α
x : o → α
⊢ A *ᵥ x ᵥ* B = (A * Bᵀ) *ᵥ x
have rw : A *ᵥ x ᵥ* B = A *ᵥ Bᵀ *ᵥ x
Tactic: rw [← mulVec_mulVec, mulVec_transpose]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : NonUnitalCommSemiring α
inst_1 : Fintype n
inst_2 : Fintype o
A : Matrix m n α
B : Matrix o n α
x : o → α
rw : A *ᵥ x ᵥ* B = A *ᵥ Bᵀ *ᵥ x
⊢ A *ᵥ x ᵥ* B = (A * Bᵀ) *ᵥ x
have rw₁ : A *ᵥ x ᵥ* B = A *ᵥ x ᵥ* B
Tactic: rw [← mulVec_mulVec, mulVec_transpose]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : NonUnitalCommSemiring α
inst_1 : Fintype m
inst_2 : Fintype n
A : Matrix m n α
B : Matrix m o α
x : n → α
⊢ (A *ᵥ x) ᵥ* B = x ᵥ* (Aᵀ * B)
have rw : (A *ᵥ x) ᵥ* B = x ᵥ* Aᵀ ᵥ* B
Tactic: rw [← vecMul_vecMul, vecMul_transpose]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : NonUnitalCommSemiring α
inst_1 : Fintype m
inst_2 : Fintype n
A : Matrix m n α
B : Matrix m o α
x : n → α
rw : (A *ᵥ x) ᵥ* B = x ᵥ* Aᵀ ᵥ* B
⊢ (A *ᵥ x) ᵥ* B = x ᵥ* (Aᵀ * B)
have rw₁ : (A *ᵥ x) ᵥ* B = (A *ᵥ x) ᵥ* B
Tactic: rw [← vecMul_vecMul, vecMul_transpose]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (hypothesis)
Goal:
n : Type u_3
R : Type u_7
inst : Semiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : (M ^ k).row i = 0
h' : k ≤ l
⊢ (M ^ l).row i = 0
have h'₁ : l = k + (l - k)
Tactic: replace h' : l = k + (l - k) := by lia
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
n : Type u_3
R : Type u_7
inst : Semiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : (M ^ k).row i = 0
h' : l = k + (l - k)
⊢ (M ^ l).row i = 0
have rw : ∀ (h : Pi.single (M := fun (a : n) ↦ R) i 1 ᵥ* M ^ k = 0) (h' : l = k + (l - k)),
  Pi.single (M := fun (a : n) ↦ R) i 1 ᵥ* M ^ l = 0
Tactic: rw [← single_one_vecMul] at h ⊢
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
n : Type u_3
R : Type u_7
inst : Semiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : Pi.single (M := fun (a : n) ↦ R) i 1 ᵥ* M ^ k = 0
h' : l = k + (l - k)
⊢ Pi.single (M := fun (a : n) ↦ R) i 1 ᵥ* M ^ l = 0
have rw : Pi.single (M := fun (a : n) ↦ R) i 1 ᵥ* M ^ (k + (l - k)) = 0
Tactic: rw [h', pow_add, ← vecMul_vecMul, h, zero_vecMul]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
n : Type u_3
R : Type u_7
inst : Semiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : Pi.single (M := fun (a : n) ↦ R) i 1 ᵥ* M ^ k = 0
h' : l = k + (l - k)
rw : Pi.single (M := fun (a : n) ↦ R) i 1 ᵥ* M ^ (k + (l - k)) = 0
⊢ Pi.single (M := fun (a : n) ↦ R) i 1 ᵥ* M ^ l = 0
have rw₁ : Pi.single (M := fun (a : n) ↦ R) i 1 ᵥ* (M ^ k * M ^ (l - k)) = 0
Tactic: rw [h', pow_add, ← vecMul_vecMul, h, zero_vecMul]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
n : Type u_3
R : Type u_7
inst : Semiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : Pi.single (M := fun (a : n) ↦ R) i 1 ᵥ* M ^ k = 0
h' : l = k + (l - k)
rw : Pi.single (M := fun (a : n) ↦ R) i 1 ᵥ* M ^ (k + (l - k)) = 0
rw₁ : Pi.single (M := fun (a : n) ↦ R) i 1 ᵥ* (M ^ k * M ^ (l - k)) = 0
⊢ Pi.single (M := fun (a : n) ↦ R) i 1 ᵥ* M ^ l = 0
have rw₂ : Pi.single (M := fun (a : n) ↦ R) i 1 ᵥ* M ^ k ᵥ* M ^ (l - k) = 0
Tactic: rw [h', pow_add, ← vecMul_vecMul, h, zero_vecMul]