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 : NonUnitalNonAssocSemiring α
inst_1 : Fintype m
L M : Matrix l m α
N : Matrix m n α
i : l
j : n
⊢ ((L + M) * N) i j = (L * N + M * N) i j

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
inst_2 : DecidableEq m
d : m → α
M : Matrix m n α
i : m
j : n
⊢ (diagonal d * M) i j = d i * M i j

Tactic:
diagonal_dotProduct _ _ _

Premises used: diagonal_dotProduct
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
inst_2 : DecidableEq n
d : n → α
M : Matrix m n α
i : m
j : n
rw : (M * (diagonal d)ᵀ) i j = M i j * d j
⊢ (M * diagonal d) i j = M i j * d j

Tactic:
rw [← diagonal_transpose]

Premises used: Matrix.diagonal_transpose
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
inst_2 : DecidableEq n
d : n → α
M : Matrix m n α
i : m
j : n
⊢ (M * (diagonal d)ᵀ) i j = M i j * d j

Tactic:
apply dotProduct_diagonal

Premises used: dotProduct_diagonal
-- Module: Mathlib.Data.Matrix.Mul
Goal:
n : Type u_3
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
inst_2 : DecidableEq n
d₁ d₂ : n → α
a : ∀ (i j : n), (diagonal d₁ * diagonal d₂) i j = diagonal (fun (i : n) ↦ d₁ i * d₂ i) i j
⊢ diagonal d₁ * diagonal d₂ = diagonal fun (i : n) ↦ d₁ i * d₂ i

Tactic:
ext i j
-- Module: Mathlib.Data.Matrix.Mul
Goal:
n : Type u_3
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
inst_2 : DecidableEq n
d₁ d₂ : n → α
i j : n
pos : ∀ (h : i = j), (diagonal d₁ * diagonal d₂) i j = diagonal (fun (i : n) ↦ d₁ i * d₂ i) i j
neg : ∀ (h : ¬i = j), (diagonal d₁ * diagonal d₂) i j = diagonal (fun (i : n) ↦ d₁ i * d₂ i) i j
⊢ (diagonal d₁ * diagonal d₂) i j = diagonal (fun (i : n) ↦ d₁ i * d₂ i) i j

Tactic:
by_cases h : i = j
-- Module: Mathlib.Data.Matrix.Mul
Goal:
n : Type u_3
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
inst_2 : DecidableEq n
d₁ d₂ : n → α
i j : n
h : i = j
⊢ (diagonal d₁ * diagonal d₂) i j = diagonal (fun (i : n) ↦ d₁ i * d₂ i) i j

Tactic:
simp [h]
-- Module: Mathlib.Data.Matrix.Mul
Goal:
n : Type u_3
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
inst_2 : DecidableEq n
d₁ d₂ : n → α
i j : n
h : ¬i = j
⊢ (diagonal d₁ * diagonal d₂) i j = diagonal (fun (i : n) ↦ d₁ i * d₂ i) i j

Tactic:
simp [h]
-- Module: Mathlib.Data.Matrix.Mul
Goal:
n : Type u_3
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
inst_2 : DecidableEq n
d₁ d₂ : n → α
⊢ diagonal d₁ * diagonal d₂ = diagonal fun (i : n) ↦ d₁ i * d₂ i

Tactic:
diagonal_mul_diagonal _ _

Premises used: Matrix.diagonal_mul_diagonal
-- Module: Mathlib.Data.Matrix.Mul
Goal:
n : Type u_3
α : Type u_10
inst : NonUnitalNonAssocCommSemiring α
inst_1 : Fintype n
inst_2 : DecidableEq n
d₁ d₂ : n → α
simp_rw : diagonal d₁ * diagonal d₂ = diagonal d₂ * diagonal d₁
simp_rw₁ : Eq (α := Matrix n n α) (diagonal fun (i : n) ↦ d₁ i * d₂ i) (diagonal fun (i : n) ↦ d₂ i * d₁ i)
⊢ Commute (diagonal d₁) (diagonal d₂)

Tactic:
simp_rw [commute_iff_eq, diagonal_mul_diagonal, mul_comm]

Premises used: commute_iff_eq, mul_comm, Matrix.diagonal_mul_diagonal
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype m
inst_2 : DecidableEq m
M : Matrix m n α
a : α
a₁ : ∀ (i : m) (j : n), (a • M) i j = HMul.hMul (α := Matrix m m α) (diagonal fun (x : m) ↦ a) M i j
⊢ a • M = HMul.hMul (α := Matrix m m α) (diagonal fun (x : m) ↦ a) M

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype m
inst_2 : DecidableEq m
M : Matrix m n α
a : α
i : m
j : n
⊢ (a • M) i j = HMul.hMul (α := Matrix m m α) (diagonal fun (x : m) ↦ a) M i j

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix m n α
a : α
a₁ : ∀ (i : m) (j : n), (MulOpposite.op a • M) i j = HMul.hMul (β := Matrix n n α) M (diagonal fun (x : n) ↦ a) i j
⊢ MulOpposite.op a • M = HMul.hMul (β := Matrix n n α) M (diagonal fun (x : n) ↦ a)

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix m n α
a : α
i : m
j : n
⊢ (MulOpposite.op a • M) i j = HMul.hMul (β := Matrix n n α) M (diagonal fun (x : n) ↦ a) i j

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
β : Type w
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype m
s : Finset β
f : β → Matrix l m α
M : Matrix m n α
⊢ (∑ a ∈ s, f a) * M = ∑ a ∈ s, f a * M

Tactic:
map_sum (addMonoidHomMulRight M) f s

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Matrix.addMonoidHomMulRight, map_sum, Finset.sum
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
β : Type w
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype m
s : Finset β
f : β → Matrix m n α
M : Matrix l m α
⊢ M * ∑ a ∈ s, f a = ∑ a ∈ s, M * f a

Tactic:
map_sum (addMonoidHomMulLeft M) f s

Premises used: Multiset.sum, Multiset.foldr, dotProduct, map_sum, Matrix.addMonoidHomMulLeft, Finset.sum
-- 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
inst_2 : Monoid R
inst_3 : DistribMulAction R α
inst_4 : IsScalarTower R α α
⊢ IsScalarTower R (Matrix n n α) (Matrix n n α)

Tactic:
⟨fun r m n => Matrix.smul_mul r m n⟩

Premises used: Matrix.smul_mul, IsScalarTower.mk
-- 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
inst_2 : Monoid R
inst_3 : DistribMulAction R α
inst_4 : SMulCommClass R α α
⊢ SMulCommClass R (Matrix n n α) (Matrix n n α)

Tactic:
⟨fun r m n => (Matrix.mul_smul m r n).symm⟩

Premises used: Matrix.mul_smul, SMulCommClass.mk, Eq.symm
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
β : Type w
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
L : Matrix m n α
M : Matrix n o α
inst_2 : NonUnitalNonAssocSemiring β
F : Type u_10
inst_3 : FunLike F α β
inst_4 : NonUnitalRingHomClass F α β
f : F
a :
  ∀ (i : m) (j : o),
    (L * M).map (⇑f : (a : α) → β) i j =
      HMul.hMul (α := Matrix m n β) (β := Matrix n o β) (L.map (⇑f : (a : α) → β)) (M.map (⇑f : (a : α) → β)) i j
⊢ (L * M).map (⇑f : (a : α) → β) =
    HMul.hMul (α := Matrix m n β) (β := Matrix n o β) (L.map (⇑f : (a : α) → β)) (M.map (⇑f : (a : α) → β))

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
β : Type w
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
L : Matrix m n α
M : Matrix n o α
inst_2 : NonUnitalNonAssocSemiring β
F : Type u_10
inst_3 : FunLike F α β
inst_4 : NonUnitalRingHomClass F α β
f : F
i : m
j : o
⊢ (L * M).map (⇑f : (a : α) → β) i j =
    HMul.hMul (α := Matrix m n β) (β := Matrix n o β) (L.map (⇑f : (a : α) → β)) (M.map (⇑f : (a : α) → β)) i j

Tactic:
simp [mul_apply, map_sum]

Premises used: Matrix.mul_apply, map_sum
-- Module: Mathlib.Data.Matrix.Mul
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 α
a : ∀ (i : m) (j : n), HMul.hMul (α := Matrix m m α) 1 M i j = M i j
⊢ 1 * M = M

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
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
a₂ a₃ : M i j = M i j
⊢ HMul.hMul (α := Matrix m m α) 1 M i j = M i j

Tactic:
rw [← diagonal_one, diagonal_mul, one_mul]

Premises used: Matrix.diagonal_mul, Matrix.diagonal_one, one_mul
-- Module: Mathlib.Data.Matrix.Mul
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 α
a : ∀ (i : m) (j : n), HMul.hMul (β := Matrix n n α) M 1 i j = M i j
⊢ M * 1 = M

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
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
a₂ a₃ : M i j = M i j
⊢ HMul.hMul (β := Matrix n n α) M 1 i j = M i j

Tactic:
rw [← diagonal_one, mul_diagonal, mul_one]

Premises used: Matrix.diagonal_one, mul_one, Matrix.mul_diagonal
-- Module: Mathlib.Data.Matrix.Mul
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)
simp_rw₃ : Eq (α := Matrix m m α) (diagonal fun (i : m) ↦ a * 1) (diagonal fun (x : m) ↦ a)
⊢ HSMul.hSMul (β := Matrix m m α) a 1 = diagonal fun (x : m) ↦ a

Tactic:
simp_rw [← diagonal_one, ← diagonal_smul, Pi.smul_def, smul_eq_mul, mul_one]

Premises used: Matrix.diagonal_smul, Matrix.diagonal_one, smul_eq_mul, mul_one, Pi.smul_def
-- Module: Mathlib.Data.Matrix.Mul
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)
simp_rw₃ : Eq (α := Matrix m m α) (diagonal fun (i : m) ↦ 1 * a) (diagonal fun (x : m) ↦ a)
⊢ HSMul.hSMul (β := Matrix m m α) (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]

Premises used: op_smul_eq_mul, Matrix.diagonal_smul, Matrix.diagonal_one, Pi.smul_def, one_mul
-- Module: Mathlib.Data.Matrix.Mul
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 α
a : ∀ (i : l) (j : o), (L * M * N) i j = (L * (M * N)) i j
⊢ L * M * N = L * (M * N)

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
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 α
i : l
j : o
⊢ (L * M * N) i j = (L * (M * N)) i j

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 : NonUnitalNonAssocRing α
inst_1 : Fintype n
M : Matrix m n α
N : Matrix n o α
a : ∀ (i : m) (j : o), (-M * N) i j = (-(M * N)) i j
⊢ -M * N = -(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 : NonUnitalNonAssocRing α
inst_1 : Fintype n
M : Matrix m n α
N : Matrix n o α
i : m
j : o
⊢ (-M * N) i j = (-(M * N)) i j

Tactic:
apply neg_dotProduct

Premises used: neg_dotProduct
-- Module: Mathlib.Data.Matrix.Mul
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 α
a : ∀ (i : m) (j : o), (M * -N) i j = (-(M * N)) i j
⊢ M * -N = -(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 : NonUnitalNonAssocRing α
inst_1 : Fintype n
M : Matrix m n α
N : Matrix n o α
i : m
j : o
⊢ (M * -N) i j = (-(M * N)) i j

Tactic:
apply dotProduct_neg

Premises used: dotProduct_neg
-- Module: Mathlib.Data.Matrix.Mul
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
rw₃ rw₄ : M * N + -(M' * N) = M * N + -(M' * N)
⊢ (M - M') * N = M * N - M' * N

Tactic:
rw [sub_eq_add_neg, Matrix.add_mul, Matrix.neg_mul, sub_eq_add_neg]

Premises used: sub_eq_add_neg, Matrix.add_mul, Matrix.neg_mul
-- Module: Mathlib.Data.Matrix.Mul
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'
rw₃ rw₄ : M * N + -(M * N') = M * N + -(M * N')
⊢ M * (N - N') = M * N - M * N'

Tactic:
rw [sub_eq_add_neg, Matrix.mul_add, Matrix.mul_neg, sub_eq_add_neg]

Premises used: sub_eq_add_neg, Matrix.mul_neg, Matrix.mul_add
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : Semiring α
inst_1 : Fintype n
M : Matrix m n α
N : Matrix n o α
a : α
⊢ ((of : (a : m → n → α) → Matrix m n α) fun (i : m) (j : n) ↦ a * M i j) * N = a • (M * N)

Tactic:
smul_mul a M N

Premises used: Matrix.smul_mul
-- Module: Mathlib.Data.Matrix.Mul
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
⊢ ∀ (i j : n), 0 ≤ HPow.hPow (β := ℕ) A 0 i j

Tactic:
aesop (add simp one_apply)

Premises used: Matrix.one_apply
-- Module: Mathlib.Data.Matrix.Mul
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
succ : LE.le.{v} (α := α) 0 (∑ j_1 : n, (A ^ m) i j_1 * A j_1 j)
⊢ 0 ≤ (A ^ (m + 1)) i j

Tactic:
rw [pow_succ, mul_apply]

Premises used: pow_succ, Matrix.mul_apply
-- Module: Mathlib.Data.Matrix.Mul
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
⊢ LE.le.{v} (α := α) 0 (∑ j_1 : n, (A ^ m) i j_1 * A j_1 j)

Tactic:
Finset.sum_nonneg fun l _ => mul_nonneg (ih i l) (hA l j)

Premises used: mul_nonneg, Finset.sum_nonneg
-- Module: Mathlib.Data.Matrix.Mul
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
⊢ LE.le.{v} (α := α) 0 (∑ j_1 : n, (A ^ m) i j_1 * A j_1 j)

Tactic:
exact Finset.sum_nonneg fun l _ => mul_nonneg (ih i l) (hA l j)

Premises used: mul_nonneg, Finset.sum_nonneg
-- Module: Mathlib.Data.Matrix.Mul
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
succ : ∀ (m : ℕ) (ih : ∀ (i j : n), 0 ≤ (A ^ m) i j) (i j : n), 0 ≤ (A ^ (m + 1)) i j
⊢ ∀ (i j : n), 0 ≤ (A ^ k) 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)

Premises used: Matrix.one_apply, pow_succ, Matrix.mul_apply, Matrix.zero
-- Module: Mathlib.Data.Matrix.Mul
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₁ : ∀ (i : m) (j : n), (a • M) i j = HMul.hMul (β := Matrix n n α) M (diagonal fun (x : n) ↦ a) i j
⊢ a • M = HMul.hMul (β := Matrix n n α) M (diagonal fun (x : n) ↦ a)

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
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 : α
i : m
j : n
⊢ (a • M) i j = HMul.hMul (β := Matrix n n α) M (diagonal fun (x : n) ↦ a) i j

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : CommSemiring α
inst_1 : Fintype n
M : Matrix m n α
N : Matrix n o α
a : α
⊢ (M * (of : (a : n → o → α) → Matrix n o α) fun (i : n) (j : o) ↦ a * N i j) = a • (M * N)

Tactic:
Matrix.mul_smul M a N

Premises used: Matrix.mul_smul
-- 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_1 : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
R : Type u_10
inst : NonAssocSemiring R
inst_1 : IsStablyFiniteRing R
f : R →* Matrix (Fin 1) (Fin 1) R :=
  { toFun := fun (r : R) ↦ diagonal fun (x : Fin 1) ↦ r, map_one' := ⋯, map_mul' := ⋯ }
x x_1 : R
eq :
  Eq (α := Matrix (Fin 1) (Fin 1) R) ((f : (a : R) → Matrix (Fin 1) (Fin 1) R) x : Matrix (Fin 1) (Fin 1) R)
    ((f : (a : R) → Matrix (Fin 1) (Fin 1) R) x_1 : Matrix (Fin 1) (Fin 1) R)
⊢ x = x_1

Tactic:
simpa [f] using congr($eq 0 0)
-- 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_1 : Type u_7
S_1 : Type u_8
α : Type v
β : Type w
γ : Type u_9
R : Type u_10
S_2 : Type u_11
F : Type u_12
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S_2
inst_2 : SetLike F R
inst_3 : SubsemiringClass F R
S : F
inst_4 : IsStablyFiniteRing R
⊢ IsStablyFiniteRing.{u_10} ↥S

Tactic:
.of_injective _ (Subsemiring.subtype_injective <| .ofClass S)

Premises used: Subsemiring.ofClass, Subsemiring.subtype_injective, IsStablyFiniteRing.of_injective
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Mul α
w : m → α
v : n → α
i : m
j : n
⊢ vecMulVec w v i j = w i * v j

Tactic:
rfl

Premises used: rfl, Matrix.vecMulVec
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Mul α
w : m → α
v : n → α
i : m
⊢ (vecMulVec w v).row i = w i • v

Tactic:
rfl

Premises used: Matrix.row, rfl, Matrix.vecMulVec
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Mul α
w : m → α
v : n → α
j : n
⊢ (vecMulVec w v).col j = MulOpposite.op (v j) • w

Tactic:
rfl

Premises used: Matrix.transpose, MulOpposite.unop, Matrix.col, rfl, Matrix.vecMulVec
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : MulZeroClass α
v : n → α
⊢ Eq (α := Matrix m n α) (vecMulVec 0 v) 0

Tactic:
ext fun _ _ => zero_mul _

Premises used: MulZeroClass.zero_mul, Matrix.ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : MulZeroClass α
w : m → α
⊢ Eq (α := Matrix m m α) (vecMulVec w 0) 0

Tactic:
ext fun _ _ => mul_zero _

Premises used: MulZeroClass.mul_zero, Matrix.ext
-- Module: Mathlib.Data.Matrix.Mul
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
obtain : ∀ (i : n) (ha : a i ≠ 0 i), False
⊢ False

Tactic:
obtain ⟨i, ha⟩ := Function.ne_iff.mp ha

Premises used: Function.ne_iff, Iff.mp
-- Module: Mathlib.Data.Matrix.Mul
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
obtain : ∀ (j : n) (hb : b j ≠ 0 j), False
⊢ False

Tactic:
obtain ⟨j, hb⟩ := Function.ne_iff.mp hb

Premises used: Function.ne_iff, Iff.mp
-- Module: Mathlib.Data.Matrix.Mul
Goal:
n : Type u_3
α : Type v
inst : Mul α
inst_1 : Zero α
inst_2 : NoZeroDivisors α
a b : n → α
ha_1 : a ≠ 0
hb_1 : b ≠ 0
h : vecMulVec a b = 0
i : n
ha : a i ≠ 0 i
j : n
hb : b j ≠ 0 j
⊢ False

Tactic:
mul_ne_zero ha hb congr($h i j)

Premises used: congrArg, id, mul_ne_zero
-- Module: Mathlib.Data.Matrix.Mul
Goal:
n : Type u_3
α : Type v
inst : Mul α
inst_1 : Zero α
inst_2 : NoZeroDivisors α
a b : n → α
ha_1 : a ≠ 0
hb_1 : b ≠ 0
h : vecMulVec a b = 0
i : n
ha : a i ≠ 0 i
j : n
hb : b j ≠ 0 j
⊢ False

Tactic:
exact mul_ne_zero ha hb congr($h i j)

Premises used: congrArg, id, mul_ne_zero
-- Module: Mathlib.Data.Matrix.Mul
Goal:
n : Type u_3
α : Type v
inst : MulZeroClass α
inst_1 : NoZeroDivisors α
a b : n → α
⊢ vecMulVec a b = 0 ↔ a = 0 ∨ b = 0

Tactic:
simp only [← ext_iff, vecMulVec_apply, zero_apply, mul_eq_zero, funext_iff, Pi.zero_apply,
    forall_or_left, forall_or_right]

Premises used: Matrix.zero_apply, funext_iff, Pi.zero_apply, mul_eq_zero, forall_or_right, Matrix.vecMulVec_apply, Matrix.ext_iff, forall_or_left
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Mul α
inst_1 : Add α
inst_2 : RightDistribClass α
w₁ w₂ : m → α
v : n → α
⊢ vecMulVec (w₁ + w₂) v = vecMulVec w₁ v + vecMulVec w₂ v

Tactic:
ext fun _ _ => add_mul _ _ _

Premises used: add_mul, Matrix.ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Mul α
inst_1 : Add α
inst_2 : LeftDistribClass α
w : m → α
v₁ v₂ : n → α
⊢ vecMulVec w (v₁ + v₂) = vecMulVec w v₁ + vecMulVec w v₂

Tactic:
ext fun _ _ => mul_add _ _ _

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

Tactic:
ext fun _ _ => neg_mul _ _

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

Tactic:
ext fun _ _ => mul_neg _ _

Premises used: Matrix.ext, mul_neg
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst : Mul α
inst_1 : SMul R α
inst_2 : IsScalarTower R α α
r : R
w : m → α
v : n → α
⊢ vecMulVec (r • w) v = r • vecMulVec w v

Tactic:
ext fun _ _ => smul_mul_assoc _ _ _

Premises used: smul_mul_assoc, Matrix.ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst : Mul α
inst_1 : SMul R α
inst_2 : SMulCommClass R α α
r : R
w : m → α
v : n → α
⊢ vecMulVec w (r • v) = r • vecMulVec w v

Tactic:
ext fun _ _ => mul_smul_comm _ _ _

Premises used: mul_smul_comm, Matrix.ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Semigroup α
w : m → α
r : α
v : n → α
⊢ vecMulVec w (r • v) = vecMulVec (MulOpposite.op r • w) v

Tactic:
ext fun _ _ => mul_assoc _ _ _ |>.symm

Premises used: mul_assoc, Eq.symm, Matrix.ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : CommMagma α
w : m → α
v : n → α
⊢ (vecMulVec w v)ᵀ = vecMulVec v w

Tactic:
ext fun _ _ => mul_comm _ _

Premises used: mul_comm, Matrix.ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
n : Type u_3
α : Type v
inst : Mul α
u v : n → α
⊢ (vecMulVec u v).diag = u * v

Tactic:
rfl

Premises used: Matrix.diag, rfl, Matrix.vecMulVec
-- 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 → α
h : ∀ (x : m), (0 *ᵥ v) x = 0 x
⊢ Eq (α := m → α) (0 *ᵥ v) 0

Tactic:
ext
-- 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 : m
⊢ (0 *ᵥ v) x = 0 x

Tactic:
simp [mulVec]

Premises used: Matrix.mulVec