awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_2 : DecidableEq m
M : Matrix m n α
i : m
j : n
a : HMul.hMul (α := Matrix m m α) (diagonal fun (x : m) ↦ 1) M i j = M i j
⊢ HMul.hMul (α := Matrix m m α) 1 M i j = M i j
have a₁ : 1 * M i j = M i j
Tactic: rw [← diagonal_one, diagonal_mul, one_mul]
-- 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
inst_2 : DecidableEq m
M : Matrix m n α
i : m
j : n
a : HMul.hMul (α := Matrix m m α) (diagonal fun (x : m) ↦ 1) M i j = M i j
a₁ : 1 * M i j = M i j
⊢ HMul.hMul (α := Matrix m m α) 1 M i j = M i j
have a₂ : M i j = M i j
Tactic: rw [← diagonal_one, diagonal_mul, one_mul]
-- 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
inst_2 : DecidableEq n
M : Matrix m n α
⊢ M * 1 = M
have a : ∀ (i : m) (j : n), HMul.hMul (β := Matrix n n α) M 1 i j = M i j
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 n
inst_2 : DecidableEq n
M : Matrix m n α
i : m
j : n
⊢ HMul.hMul (β := Matrix n n α) M 1 i j = M i j
have a : HMul.hMul (β := Matrix n n α) M (diagonal fun (x : n) ↦ 1) i j = M i j
Tactic: rw [← diagonal_one, mul_diagonal, mul_one]
-- 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
inst_2 : DecidableEq n
M : Matrix m n α
i : m
j : n
a : HMul.hMul (β := Matrix n n α) M (diagonal fun (x : n) ↦ 1) i j = M i j
⊢ HMul.hMul (β := Matrix n n α) M 1 i j = M i j
have a₁ : M i j * 1 = M i j
Tactic: rw [← diagonal_one, mul_diagonal, mul_one]
-- 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
inst_2 : DecidableEq n
M : Matrix m n α
i : m
j : n
a : HMul.hMul (β := Matrix n n α) M (diagonal fun (x : n) ↦ 1) i j = M i j
a₁ : M i j * 1 = M i j
⊢ HMul.hMul (β := Matrix n n α) M 1 i j = M i j
have a₂ : M i j = M i j
Tactic: rw [← diagonal_one, mul_diagonal, mul_one]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
α : Type v
inst : NonAssocSemiring α
inst_1 : DecidableEq m
a : α
⊢ HSMul.hSMul (β := Matrix m m α) a 1 = diagonal fun (x : m) ↦ a
have simp_rw : HSMul.hSMul (β := Matrix m m α) a (diagonal fun (x : m) ↦ 1) = diagonal fun (x : m) ↦ a
Tactic: simp_rw [← diagonal_one, ← diagonal_smul, Pi.smul_def, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
α : Type v
inst : NonAssocSemiring α
inst_1 : DecidableEq m
a : α
simp_rw : HSMul.hSMul (β := Matrix m m α) a (diagonal fun (x : m) ↦ 1) = diagonal fun (x : m) ↦ a
⊢ HSMul.hSMul (β := Matrix m m α) a 1 = diagonal fun (x : m) ↦ a
have simp_rw₁ : diagonal (HSMul.hSMul (β := m → α) a fun (x : m) ↦ 1) = diagonal fun (x : m) ↦ a
Tactic: simp_rw [← diagonal_one, ← diagonal_smul, Pi.smul_def, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
α : Type v
inst : NonAssocSemiring α
inst_1 : DecidableEq m
a : α
simp_rw : HSMul.hSMul (β := Matrix m m α) a (diagonal fun (x : m) ↦ 1) = diagonal fun (x : m) ↦ a
simp_rw₁ : diagonal (HSMul.hSMul (β := m → α) a fun (x : m) ↦ 1) = diagonal fun (x : m) ↦ a
⊢ HSMul.hSMul (β := Matrix m m α) a 1 = diagonal fun (x : m) ↦ a
have simp_rw₂ : Eq (α := Matrix m m α) (diagonal fun (i : m) ↦ HSMul.hSMul (β := α) a 1) (diagonal fun (x : m) ↦ a)
Tactic: simp_rw [← diagonal_one, ← diagonal_smul, Pi.smul_def, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
α : Type v
inst : NonAssocSemiring α
inst_1 : DecidableEq m
a : α
simp_rw : HSMul.hSMul (β := Matrix m m α) a (diagonal fun (x : m) ↦ 1) = diagonal fun (x : m) ↦ a
simp_rw₁ : diagonal (HSMul.hSMul (β := m → α) a fun (x : m) ↦ 1) = diagonal fun (x : m) ↦ a
simp_rw₂ : Eq (α := Matrix m m α) (diagonal fun (i : m) ↦ HSMul.hSMul (β := α) a 1) (diagonal fun (x : m) ↦ a)
⊢ HSMul.hSMul (β := Matrix m m α) a 1 = diagonal fun (x : m) ↦ a
have simp_rw₃ : Eq (α := Matrix m m α) (diagonal fun (i : m) ↦ a * 1) (diagonal fun (x : m) ↦ a)
Tactic: simp_rw [← diagonal_one, ← diagonal_smul, Pi.smul_def, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
α : Type v
inst : NonAssocSemiring α
inst_1 : DecidableEq m
a : α
⊢ HSMul.hSMul (β := Matrix m m α) (MulOpposite.op a) 1 = diagonal fun (x : m) ↦ a
have simp_rw : HSMul.hSMul (β := Matrix m m α) (MulOpposite.op a) (diagonal fun (x : m) ↦ 1) = diagonal fun (x : m) ↦ a
Tactic: simp_rw [← diagonal_one, ← diagonal_smul, Pi.smul_def, op_smul_eq_mul, one_mul]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
α : Type v
inst : NonAssocSemiring α
inst_1 : DecidableEq m
a : α
simp_rw : HSMul.hSMul (β := Matrix m m α) (MulOpposite.op a) (diagonal fun (x : m) ↦ 1) = diagonal fun (x : m) ↦ a
⊢ HSMul.hSMul (β := Matrix m m α) (MulOpposite.op a) 1 = diagonal fun (x : m) ↦ a
have simp_rw₁ : diagonal (HSMul.hSMul (β := m → α) (MulOpposite.op a) fun (x : m) ↦ 1) = diagonal fun (x : m) ↦ a
Tactic: simp_rw [← diagonal_one, ← diagonal_smul, Pi.smul_def, op_smul_eq_mul, one_mul]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
α : Type v
inst : NonAssocSemiring α
inst_1 : DecidableEq m
a : α
simp_rw : HSMul.hSMul (β := Matrix m m α) (MulOpposite.op a) (diagonal fun (x : m) ↦ 1) = diagonal fun (x : m) ↦ a
simp_rw₁ : diagonal (HSMul.hSMul (β := m → α) (MulOpposite.op a) fun (x : m) ↦ 1) = diagonal fun (x : m) ↦ a
⊢ HSMul.hSMul (β := Matrix m m α) (MulOpposite.op a) 1 = diagonal fun (x : m) ↦ a
have simp_rw₂ : Eq (α := Matrix m m α) (diagonal fun (i : m) ↦ HSMul.hSMul (β := α) (MulOpposite.op a) 1) (diagonal fun (x : m) ↦ a)
Tactic: simp_rw [← diagonal_one, ← diagonal_smul, Pi.smul_def, op_smul_eq_mul, one_mul]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
α : Type v
inst : NonAssocSemiring α
inst_1 : DecidableEq m
a : α
simp_rw : HSMul.hSMul (β := Matrix m m α) (MulOpposite.op a) (diagonal fun (x : m) ↦ 1) = diagonal fun (x : m) ↦ a
simp_rw₁ : diagonal (HSMul.hSMul (β := m → α) (MulOpposite.op a) fun (x : m) ↦ 1) = diagonal fun (x : m) ↦ a
simp_rw₂ :
  Eq (α := Matrix m m α) (diagonal fun (i : m) ↦ HSMul.hSMul (β := α) (MulOpposite.op a) 1) (diagonal fun (x : m) ↦ a)
⊢ HSMul.hSMul (β := Matrix m m α) (MulOpposite.op a) 1 = diagonal fun (x : m) ↦ a
have simp_rw₃ : Eq (α := Matrix m m α) (diagonal fun (i : m) ↦ 1 * a) (diagonal fun (x : m) ↦ a)
Tactic: simp_rw [← diagonal_one, ← diagonal_smul, Pi.smul_def, op_smul_eq_mul, one_mul]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype m
inst_2 : Fintype n
L : Matrix l m α
M : Matrix m n α
N : Matrix n o α
⊢ L * M * N = L * (M * N)
have a : ∀ (i : l) (j : o), (L * M * N) i j = (L * (M * N)) i j
Tactic: ext
-- 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 : NonUnitalNonAssocRing α
inst_1 : Fintype n
M : Matrix m n α
N : Matrix n o α
⊢ -M * N = -(M * N)
have a : ∀ (i : m) (j : o), (-M * N) i j = (-(M * N)) i j
Tactic: ext
-- 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 : NonUnitalNonAssocRing α
inst_1 : Fintype n
M : Matrix m n α
N : Matrix n o α
⊢ M * -N = -(M * N)
have a : ∀ (i : m) (j : o), (M * -N) i j = (-(M * N)) i j
Tactic: ext
-- 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 : NonUnitalNonAssocRing α
inst_1 : Fintype n
M M' : Matrix m n α
N : Matrix n o α
⊢ (M - M') * N = M * N - M' * N
have rw : (M + -M') * N = M * N - M' * N
Tactic: rw [sub_eq_add_neg, Matrix.add_mul, Matrix.neg_mul, sub_eq_add_neg]
-- 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 : NonUnitalNonAssocRing α
inst_1 : Fintype n
M M' : Matrix m n α
N : Matrix n o α
rw : (M + -M') * N = M * N - M' * N
⊢ (M - M') * N = M * N - M' * N
have rw₁ : M * N + -M' * N = M * N - M' * N
Tactic: rw [sub_eq_add_neg, Matrix.add_mul, Matrix.neg_mul, sub_eq_add_neg]
-- 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 : NonUnitalNonAssocRing α
inst_1 : Fintype n
M M' : Matrix m n α
N : Matrix n o α
rw : (M + -M') * N = M * N - M' * N
rw₁ : M * N + -M' * N = M * N - M' * N
⊢ (M - M') * N = M * N - M' * N
have rw₂ : M * N + -(M' * N) = M * N - M' * N
Tactic: rw [sub_eq_add_neg, Matrix.add_mul, Matrix.neg_mul, sub_eq_add_neg]
-- 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 : NonUnitalNonAssocRing α
inst_1 : Fintype n
M M' : Matrix m n α
N : Matrix n o α
rw : (M + -M') * N = M * N - M' * N
rw₁ : M * N + -M' * N = M * N - M' * N
rw₂ : M * N + -(M' * N) = M * N - M' * N
⊢ (M - M') * N = M * N - M' * N
have rw₃ : M * N + -(M' * N) = M * N + -(M' * N)
Tactic: rw [sub_eq_add_neg, Matrix.add_mul, Matrix.neg_mul, sub_eq_add_neg]
-- 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 : NonUnitalNonAssocRing α
inst_1 : Fintype n
M : Matrix m n α
N N' : Matrix n o α
⊢ M * (N - N') = M * N - M * N'
have rw : M * (N + -N') = M * N - M * N'
Tactic: rw [sub_eq_add_neg, Matrix.mul_add, Matrix.mul_neg, sub_eq_add_neg]
-- 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 : NonUnitalNonAssocRing α
inst_1 : Fintype n
M : Matrix m n α
N N' : Matrix n o α
rw : M * (N + -N') = M * N - M * N'
⊢ M * (N - N') = M * N - M * N'
have rw₁ : M * N + M * -N' = M * N - M * N'
Tactic: rw [sub_eq_add_neg, Matrix.mul_add, Matrix.mul_neg, sub_eq_add_neg]
-- 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 : NonUnitalNonAssocRing α
inst_1 : Fintype n
M : Matrix m n α
N N' : Matrix n o α
rw : M * (N + -N') = M * N - M * N'
rw₁ : M * N + M * -N' = M * N - M * N'
⊢ M * (N - N') = M * N - M * N'
have rw₂ : M * N + -(M * N') = M * N - M * N'
Tactic: rw [sub_eq_add_neg, Matrix.mul_add, Matrix.mul_neg, sub_eq_add_neg]
-- 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 : NonUnitalNonAssocRing α
inst_1 : Fintype n
M : Matrix m n α
N N' : Matrix n o α
rw : M * (N + -N') = M * N - M * N'
rw₁ : M * N + M * -N' = M * N - M * N'
rw₂ : M * N + -(M * N') = M * N - M * N'
⊢ M * (N - N') = M * N - M * N'
have rw₃ : M * N + -(M * N') = M * N + -(M * N')
Tactic: rw [sub_eq_add_neg, Matrix.mul_add, Matrix.mul_neg, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
n : Type u_3
α : Type v
inst : Semiring α
inst_1 : Fintype n
inst_2 : DecidableEq n
inst_3 : PartialOrder α
inst_4 : IsOrderedRing α
A : Matrix n n α
hA : ∀ (i j : n), 0 ≤ A i j
m : ℕ
ih : ∀ (i j : n), 0 ≤ (A ^ m) i j
i j : n
⊢ 0 ≤ (A ^ (m + 1)) i j
have succ : LE.le.{v} (α := α) 0 (∑ j_1 : n, (A ^ m) i j_1 * A j_1 j)
Tactic: rw [pow_succ, mul_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
n : Type u_3
α : Type v
inst : Semiring α
inst_1 : Fintype n
inst_2 : DecidableEq n
inst_3 : PartialOrder α
inst_4 : IsOrderedRing α
A : Matrix n n α
hA : ∀ (i j : n), 0 ≤ A i j
k : ℕ
⊢ ∀ (i j : n), 0 ≤ (A ^ k) i j
have zero : ∀ (i j : n), 0 ≤ HPow.hPow (β := ℕ) A 0 i j
Tactic: induction k with
  | zero => aesop (add simp one_apply)
  | succ m ih =>
    intro i j; rw [pow_succ, mul_apply]
    exact Finset.sum_nonneg fun l _ => mul_nonneg (ih i l) (hA l j)
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
n : Type u_3
α : Type v
inst : Semiring α
inst_1 : Fintype n
inst_2 : DecidableEq n
inst_3 : PartialOrder α
inst_4 : IsOrderedRing α
A : Matrix n n α
hA : ∀ (i j : n), 0 ≤ A i j
k : ℕ
zero : ∀ (i j : n), 0 ≤ HPow.hPow (β := ℕ) A 0 i j
⊢ ∀ (i j : n), 0 ≤ (A ^ k) i j
have succ : ∀ (m : ℕ) (ih : ∀ (i j : n), 0 ≤ (A ^ m) i j) (i j : n), 0 ≤ (A ^ (m + 1)) i j
Tactic: induction k with
  | zero => aesop (add simp one_apply)
  | succ m ih =>
    intro i j; rw [pow_succ, mul_apply]
    exact Finset.sum_nonneg fun l _ => mul_nonneg (ih i l) (hA l j)
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : CommSemiring α
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix m n α
a : α
⊢ a • M = HMul.hMul (β := Matrix n n α) M (diagonal fun (x : n) ↦ a)
have a₁ : ∀ (i : m) (j : n), (a • M) i j = HMul.hMul (β := Matrix n n α) M (diagonal fun (x : n) ↦ a) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
n : Type u_3
α : Type v
inst : Mul α
inst_1 : Zero α
inst_2 : NoZeroDivisors α
a b : n → α
ha : a ≠ 0
hb : b ≠ 0
h : vecMulVec a b = 0
⊢ False
have obtain : ∀ (i : n) (ha : a i ≠ 0 i), False
Tactic: obtain ⟨i, ha⟩ := Function.ne_iff.mp ha
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
n : Type u_3
α : Type v
inst : Mul α
inst_1 : Zero α
inst_2 : NoZeroDivisors α
a b : n → α
ha_1 : a ≠ 0
hb : b ≠ 0
h : vecMulVec a b = 0
i : n
ha : a i ≠ 0 i
⊢ False
have obtain : ∀ (j : n) (hb : b j ≠ 0 j), False
Tactic: obtain ⟨j, hb⟩ := Function.ne_iff.mp hb
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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 → α
⊢ Eq (α := m → α) (0 *ᵥ v) 0
have h : ∀ (x : m), (0 *ᵥ v) x = 0 x
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
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 α
⊢ (x + y) *ᵥ v = x *ᵥ v + y *ᵥ v
have h : ∀ (m_1 : m), ((x + y) *ᵥ v) m_1 = (x *ᵥ v + y *ᵥ v) m_1
Tactic: ext m
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ v ⬝ᵥ A *ᵥ w = v ᵥ* A ⬝ᵥ w
have 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))
Tactic: simp only [dotProduct, vecMul, mulVec, Finset.mul_sum, Finset.sum_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
A : Matrix m n α
⊢ A *ᵥ 0 = 0
have h : ∀ (x : m), (A *ᵥ 0) x = 0 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 : NonUnitalNonAssocSemiring α
inst_1 : Fintype m
A : Matrix m n α
⊢ 0 ᵥ* A = 0
have h : ∀ (x : n), (0 ᵥ* A) x = 0 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 : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
v : n → α
⊢ Eq (α := m → α) (0 *ᵥ v) 0
have h : ∀ (x : m), (0 *ᵥ v) x = 0 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 : NonUnitalNonAssocSemiring α
inst_1 : Fintype m
v : m → α
⊢ Eq (α := n → α) (v ᵥ* 0) 0
have h : ∀ (x : n), (v ᵥ* 0) x = 0 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 : NonUnitalNonAssocSemiring α
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 : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
A B : Matrix m n α
x : n → α
⊢ (A + B) *ᵥ x = A *ᵥ x + B *ᵥ x
have h : ∀ (x_1 : m), ((A + B) *ᵥ x) x_1 = (A *ᵥ x + B *ᵥ x) 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 : NonUnitalNonAssocSemiring α
inst_1 : Fintype m
A B : Matrix m n α
x : m → α
⊢ x ᵥ* (A + B) = x ᵥ* A + x ᵥ* B
have h : ∀ (x_1 : n), (x ᵥ* (A + B)) x_1 = (x ᵥ* A + x ᵥ* B) 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 : NonUnitalNonAssocSemiring α
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
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 → α
⊢ M *ᵥ b • v = b • M *ᵥ v
have h : ∀ (x : m), (M *ᵥ b • v) x = (b • M *ᵥ v) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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 → α
⊢ (b • M) *ᵥ v = b • M *ᵥ v
have h : ∀ (x : m), ((b • M) *ᵥ v) x = (b • M *ᵥ v) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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 α
⊢ (b • v) ᵥ* M = b • v ᵥ* M
have h : ∀ (x : n), ((b • v) ᵥ* M) x = (b • v ᵥ* M) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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 α
⊢ v ᵥ* (b • M) = b • v ᵥ* M
have h : ∀ (x : n), (v ᵥ* (b • M)) x = (b • v ᵥ* M) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ M *ᵥ Pi.single (M := fun (a : n) ↦ R) j 1 = M.col j
have h : ∀ (x : m), (M *ᵥ Pi.single (M := fun (a : n) ↦ R) j 1) x = M.col j x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ Pi.single (M := fun (a : m) ↦ R) i 1 ᵥ* M = M.row i
have h : ∀ (x : n), (Pi.single (M := fun (a : m) ↦ R) i 1 ᵥ* M) x = M.row i x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ diagonal v *ᵥ Pi.single (M := fun (a : n) ↦ R) j x = Pi.single (M := fun (j : n) ↦ R) j (v j * x)
have 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
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ (diagonal v *ᵥ Pi.single (M := fun (a : n) ↦ R) j x) i = Pi.single (M := fun (j : n) ↦ R) j (v j * x) i
have 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
Tactic: rw [mulVec_diagonal]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ Pi.single (M := fun (a : n) ↦ R) j x ᵥ* diagonal v = Pi.single (M := fun (j : n) ↦ R) j (x * v j)
have 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
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ (Pi.single (M := fun (a : n) ↦ R) j x ᵥ* diagonal v) i = Pi.single (M := fun (j : n) ↦ R) j (x * v j) i
have 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
Tactic: rw [vecMul_diagonal]
-- 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 : NonUnitalSemiring α
inst_1 : Fintype n
inst_2 : Fintype m
v : m → α
M : Matrix m n α
N : Matrix n o α
⊢ v ᵥ* M ᵥ* N = v ᵥ* (M * N)
have h : ∀ (x : o), (v ᵥ* M ᵥ* N) x = (v ᵥ* (M * N)) x
Tactic: ext
-- 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 : NonUnitalSemiring α
inst_1 : Fintype n
inst_2 : Fintype o
v : o → α
M : Matrix m n α
N : Matrix n o α
⊢ M *ᵥ N *ᵥ v = (M * N) *ᵥ v
have h : ∀ (x : m), (M *ᵥ N *ᵥ v) x = ((M * N) *ᵥ v) x
Tactic: ext
-- 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 : 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
have h : ((M * N) *ᵥ v) x = (M *ᵥ N *ᵥ v) x
Tactic: symm
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
have rw : (A * (B * C)) i j = A i ⬝ᵥ B *ᵥ Cᵀ j
Tactic: rw [Matrix.mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype m
u v : m → α
w : n → α
⊢ u ᵥ* vecMulVec v w = (u ⬝ᵥ v) • w
have h : ∀ (i : n), (u ᵥ* vecMulVec v w) i = ((u ⬝ᵥ v) • w) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype n
u : m → α
v w : n → α
⊢ vecMulVec u v *ᵥ w = MulOpposite.op (v ⬝ᵥ w) • u
have h : ∀ (i : m), (vecMulVec u v *ᵥ w) i = (MulOpposite.op (v ⬝ᵥ w) • u) i
Tactic: ext 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 : Fintype m
M : Matrix l m α
x : m → α
y : n → α
⊢ M * vecMulVec x y = vecMulVec (M *ᵥ x) y
have a : ∀ (i : l) (j : n), (M * vecMulVec x y) i j = vecMulVec (M *ᵥ x) y 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
M : Matrix l m α
x : m → α
y : n → α
i : l
j : n
⊢ (M * vecMulVec x y) i j = vecMulVec (M *ᵥ x) y i j
have a : ∑ j_1 : m, M i j_1 * vecMulVec x y j_1 j = vecMulVec (M *ᵥ x) y i 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
⊢ (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) = (M *ᵥ x) i * 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
⊢ (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) = (fun (j : m) ↦ M i j) ⬝ᵥ x * y j
Tactic: simp_rw [mul_apply, vecMulVec_apply, mulVec, dotProduct, Finset.sum_mul, mul_assoc]