awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v : m → α
x : α
i : m
this : ∀ (j : m), j ≠ i → HMul.hMul (α := α) (Pi.single (M := fun (a : m) ↦ α) i x j : α) (v j) = 0
h : x * v i = HMul.hMul (α := α) (Pi.single (M := fun (a : m) ↦ α) i x i : α) (v i)
convert_2 : i ∉ Finset.univ → HMul.hMul (α := α) (Pi.single (M := fun (a : m) ↦ α) i x i : α) (v i) = 0
⊢ Pi.single (M := fun (a : m) ↦ α) i x ⬝ᵥ v = x * v i

Tactic:
convert! Finset.sum_eq_single i (fun j _ => this j) _ using 1

Premises used: Finset.sum_eq_single
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v : m → α
x : α
i : m
this : ∀ (j : m), j ≠ i → HMul.hMul (α := α) (Pi.single (M := fun (a : m) ↦ α) i x j : α) (v j) = 0
⊢ x * v i = HMul.hMul (α := α) (Pi.single (M := fun (a : m) ↦ α) i x i : α) (v i)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v : m → α
x : α
i : m
this : ∀ (j : m), j ≠ i → HMul.hMul (α := α) (Pi.single (M := fun (a : m) ↦ α) i x j : α) (v j) = 0
⊢ i ∉ Finset.univ → HMul.hMul (α := α) (Pi.single (M := fun (a : m) ↦ α) i x i : α) (v i) = 0

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v : m → α
x : α
i j : m
hij : j ≠ i
⊢ HMul.hMul (β := α) (v j) (Pi.single (M := fun (a : m) ↦ α) i x j : α) = 0

Tactic:
simp [Pi.single_eq_of_ne hij]

Premises used: Pi.single_eq_of_ne
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v : m → α
x : α
i : m
⊢ ∀ (j : m), j ≠ i → HMul.hMul (β := α) (v j) (Pi.single (M := fun (a : m) ↦ α) i x j : α) = 0

Tactic:
have : ∀ j ≠ i, v j * (Pi.single i x : m → α) j = 0 := fun j hij => by
    simp [Pi.single_eq_of_ne hij]
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v : m → α
x : α
i : m
this : ∀ (j : m), j ≠ i → HMul.hMul (β := α) (v j) (Pi.single (M := fun (a : m) ↦ α) i x j : α) = 0
⊢ ∑ x_1 : m, HMul.hMul (β := α) (v x_1) (Pi.single (M := fun (a : m) ↦ α) i x x_1 : α) =
    HMul.hMul (β := α) (v i) (Pi.single (M := fun (a : m) ↦ α) i x i : α)

Tactic:
Finset.sum_eq_single i (fun j _ => this j) _

Premises used: Finset.sum_eq_single
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v : m → α
x : α
i : m
this : ∀ (j : m), j ≠ i → HMul.hMul (β := α) (v j) (Pi.single (M := fun (a : m) ↦ α) i x j : α) = 0
h : v i * x = HMul.hMul (β := α) (v i) (Pi.single (M := fun (a : m) ↦ α) i x i : α)
convert_2 : i ∉ Finset.univ → HMul.hMul (β := α) (v i) (Pi.single (M := fun (a : m) ↦ α) i x i : α) = 0
⊢ v ⬝ᵥ Pi.single (M := fun (a : m) ↦ α) i x = v i * x

Tactic:
convert! Finset.sum_eq_single i (fun j _ => this j) _ using 1

Premises used: Finset.sum_eq_single
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v : m → α
x : α
i : m
this : ∀ (j : m), j ≠ i → HMul.hMul (β := α) (v j) (Pi.single (M := fun (a : m) ↦ α) i x j : α) = 0
⊢ v i * x = HMul.hMul (β := α) (v i) (Pi.single (M := fun (a : m) ↦ α) i x i : α)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v : m → α
x : α
i : m
this : ∀ (j : m), j ≠ i → HMul.hMul (β := α) (v j) (Pi.single (M := fun (a : m) ↦ α) i x j : α) = 0
⊢ i ∉ Finset.univ → HMul.hMul (β := α) (v i) (Pi.single (M := fun (a : m) ↦ α) i x i : α) = 0

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Mul
Goal:
n : Type u_3
α : Type v
inst : Fintype n
inst_1 : NonAssocSemiring α
⊢ Eq.{v + 1} (α := α) (dotProduct.{v, u_3} (m := n) 1 1) (↑(Fintype.card n) : α)

Tactic:
simp [dotProduct]

Premises used: dotProduct
-- Module: Mathlib.Data.Matrix.Mul
Goal:
n : Type u_3
α : Type v
inst : Fintype n
inst_1 : NonAssocSemiring α
inst_2 : DecidableEq n
v : n → α
i : n
rw : v i * 1 = v i
rw₁ rw₂ : v i = v i
⊢ v ⬝ᵥ Pi.single (M := fun (a : n) ↦ α) i 1 = v i

Tactic:
rw [dotProduct_single, mul_one]

Premises used: dotProduct_single, mul_one
-- Module: Mathlib.Data.Matrix.Mul
Goal:
n : Type u_3
α : Type v
inst : Fintype n
inst_1 : NonAssocSemiring α
inst_2 : DecidableEq n
i : n
v : n → α
rw : 1 * v i = v i
rw₁ rw₂ : v i = v i
⊢ Pi.single (M := fun (a : n) ↦ α) i 1 ⬝ᵥ v = v i

Tactic:
rw [single_dotProduct, one_mul]

Premises used: single_dotProduct, one_mul
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : NonUnitalNonAssocRing α
v w : m → α
⊢ -v ⬝ᵥ w = -(v ⬝ᵥ w)

Tactic:
simp [dotProduct]

Premises used: dotProduct
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : NonUnitalNonAssocRing α
v w : m → α
⊢ v ⬝ᵥ -w = -(v ⬝ᵥ w)

Tactic:
simp [dotProduct]

Premises used: dotProduct
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : NonUnitalNonAssocRing α
v w : m → α
rw : -(v ⬝ᵥ -w) = v ⬝ᵥ w
rw₁ : - -(v ⬝ᵥ w) = v ⬝ᵥ w
rw₂ rw₃ : v ⬝ᵥ w = v ⬝ᵥ w
⊢ -v ⬝ᵥ -w = v ⬝ᵥ w

Tactic:
rw [neg_dotProduct, dotProduct_neg, neg_neg]

Premises used: neg_neg, neg_dotProduct, dotProduct_neg
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : NonUnitalNonAssocRing α
u v w : m → α
⊢ (u - v) ⬝ᵥ w = u ⬝ᵥ w - v ⬝ᵥ w

Tactic:
simp [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : NonUnitalNonAssocRing α
u v w : m → α
⊢ u ⬝ᵥ (v - w) = u ⬝ᵥ v - u ⬝ᵥ w

Tactic:
simp [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
R : Type u_7
α : Type v
inst : Fintype m
inst_1 : Mul α
inst_2 : AddCommMonoid α
inst_3 : DistribSMul R α
inst_4 : IsScalarTower R α α
x : R
v w : m → α
⊢ x • v ⬝ᵥ w = x • (v ⬝ᵥ w)

Tactic:
simp [dotProduct, Finset.smul_sum, smul_mul_assoc]

Premises used: dotProduct, smul_mul_assoc, Finset.smul_sum
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
R : Type u_7
α : Type v
inst : Fintype m
inst_1 : Mul α
inst_2 : AddCommMonoid α
inst_3 : DistribSMul R α
inst_4 : SMulCommClass R α α
x : R
v w : m → α
⊢ v ⬝ᵥ x • w = x • (v ⬝ᵥ w)

Tactic:
simp [dotProduct, Finset.smul_sum, mul_smul_comm]

Premises used: dotProduct, Finset.smul_sum, mul_smul_comm
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : CommRing α
inst_2 : Nontrivial m
inst_3 : Nontrivial α
a : m → α
⊢ ∃ (i : m) (j : m), i ≠ j

Tactic:
nontrivial_iff.mp ‹_›

Premises used: nontrivial_iff, Iff.mp
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : CommRing α
inst_2 : Nontrivial m
inst_3 : Nontrivial α
a : m → α
obtain : ∀ (i j : m) (hij : i ≠ j), ∃ (b : m → α), b ≠ 0 ∧ b ⬝ᵥ a = 0
⊢ ∃ (b : m → α), b ≠ 0 ∧ b ⬝ᵥ a = 0

Tactic:
obtain ⟨i, j, hij⟩ : ∃ i j : m, i ≠ j := nontrivial_iff.mp ‹_›

Premises used: nontrivial_iff, Iff.mp
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : CommRing α
inst_2 : Nontrivial m
inst_3 : Nontrivial α
a : m → α
i j : m
hij : i ≠ j
h :
  Ne (α := m → α)
      (if a i = 0 then Pi.single (M := fun (a : m) ↦ α) i 1
      else
        if a j = 0 then Pi.single (M := fun (a : m) ↦ α) j 1
        else fun (k : m) ↦ if k = i then a j else if k = j then -a i else 0)
      0 ∧
    (if a i = 0 then Pi.single (M := fun (a : m) ↦ α) i 1
        else
          if a j = 0 then Pi.single (M := fun (a : m) ↦ α) j 1
          else fun (k : m) ↦ if k = i then a j else if k = j then -a i else 0) ⬝ᵥ
        a =
      0
⊢ ∃ (b : m → α), b ≠ 0 ∧ b ⬝ᵥ a = 0

Tactic:
use if a i = 0 then Pi.single i 1 else if a j = 0 then Pi.single j 1 else
    fun k => if k = i then a j else if k = j then - a i else 0

Premises used: Pi.single, OfNat.ofNat, Eq, Neg.neg, ite
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : CommRing α
inst_2 : Nontrivial m
inst_3 : Nontrivial α
a : m → α
i j : m
hij : i ≠ j
pos :
  ∀ (h : a i = 0),
    Ne (α := m → α) (Pi.single (M := fun (a : m) ↦ α) i 1) 0 ∧ Pi.single (M := fun (a : m) ↦ α) i 1 ⬝ᵥ a = 0
pos₁ :
  ∀ (h : ¬a i = 0) (h2 : a j = 0),
    Ne (α := m → α) (Pi.single (M := fun (a : m) ↦ α) j 1) 0 ∧ Pi.single (M := fun (a : m) ↦ α) j 1 ⬝ᵥ a = 0
neg :
  ∀ (h : ¬a i = 0) (h2 : ¬a j = 0),
    Ne (α := m → α) (fun (k : m) ↦ if k = i then a j else if k = j then -a i else 0) 0 ∧
      (fun (k : m) ↦ if k = i then a j else if k = j then -a i else 0) ⬝ᵥ a = 0
⊢ Ne (α := m → α)
      (if a i = 0 then Pi.single (M := fun (a : m) ↦ α) i 1
      else
        if a j = 0 then Pi.single (M := fun (a : m) ↦ α) j 1
        else fun (k : m) ↦ if k = i then a j else if k = j then -a i else 0)
      0 ∧
    (if a i = 0 then Pi.single (M := fun (a : m) ↦ α) i 1
        else
          if a j = 0 then Pi.single (M := fun (a : m) ↦ α) j 1
          else fun (k : m) ↦ if k = i then a j else if k = j then -a i else 0) ⬝ᵥ
        a =
      0

Tactic:
split_ifs with h h2
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : CommRing α
inst_2 : Nontrivial m
inst_3 : Nontrivial α
a : m → α
i j : m
hij : i ≠ j
h : a i = 0
⊢ Ne (α := m → α) (Pi.single (M := fun (a : m) ↦ α) i 1) 0 ∧ Pi.single (M := fun (a : m) ↦ α) i 1 ⬝ᵥ a = 0

Tactic:
simp [h]
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : CommRing α
inst_2 : Nontrivial m
inst_3 : Nontrivial α
a : m → α
i j : m
hij : i ≠ j
h : ¬a i = 0
h2 : a j = 0
⊢ Ne (α := m → α) (Pi.single (M := fun (a : m) ↦ α) j 1) 0 ∧ Pi.single (M := fun (a : m) ↦ α) j 1 ⬝ᵥ a = 0

Tactic:
simp [h2]
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : CommRing α
inst_2 : Nontrivial m
inst_3 : Nontrivial α
a : m → α
i j : m
hij : i ≠ j
h : ¬a i = 0
h2 : ¬a j = 0
⊢ (if i = i then a j else if i = j then -a i else 0) ≠ 0 i

Tactic:
simp [h2]
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : CommRing α
inst_2 : Nontrivial m
inst_3 : Nontrivial α
a : m → α
i j : m
hij : i ≠ j
h : ¬a i = 0
h2 : ¬a j = 0
neg : (fun (k : m) ↦ if k = i then a j else if k = j then -a i else 0) ⬝ᵥ a = 0
⊢ Ne (α := m → α) (fun (k : m) ↦ if k = i then a j else if k = j then -a i else 0) 0 ∧
    (fun (k : m) ↦ if k = i then a j else if k = j then -a i else 0) ⬝ᵥ a = 0

Tactic:
refine ⟨Function.ne_iff.mpr ⟨i, by simp [h2]⟩, ?_⟩
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : CommRing α
inst_2 : Nontrivial m
inst_3 : Nontrivial α
a : m → α
i j : m
hij : i ≠ j
h : ¬a i = 0
h2 : ¬a j = 0
⊢ (fun (k : m) ↦ if k = i then a j else if k = j then -a i else 0) ⬝ᵥ a = 0

Tactic:
simp [dotProduct, Finset.sum_ite, Finset.sum_eq_ite i, hij.symm, mul_comm (a i)]

Premises used: dotProduct, Ne.symm, mul_comm, Finset.sum_ite, Finset.sum_eq_ite
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : CommRing α
inst_2 : Nontrivial m
inst_3 : Nontrivial α
a : m → α
i j : m
hij : i ≠ j
w : m → α
h h₁ :
  Ne (α := m → α)
      (if a i = 0 then Pi.single (M := fun (a : m) ↦ α) i 1
      else
        if a j = 0 then Pi.single (M := fun (a : m) ↦ α) j 1
        else fun (k : m) ↦ if k = i then a j else if k = j then -a i else 0)
      0 ∧
    (if a i = 0 then Pi.single (M := fun (a : m) ↦ α) i 1
        else
          if a j = 0 then Pi.single (M := fun (a : m) ↦ α) j 1
          else fun (k : m) ↦ if k = i then a j else if k = j then -a i else 0) ⬝ᵥ
        a =
      0
pos :
  ∀ (h : a i = 0),
    Ne (α := m → α) (Pi.single (M := fun (a : m) ↦ α) i 1) 0 ∧ Pi.single (M := fun (a : m) ↦ α) i 1 ⬝ᵥ a = 0
pos₁ :
  ∀ (h : ¬a i = 0) (h2 : a j = 0),
    Ne (α := m → α) (Pi.single (M := fun (a : m) ↦ α) j 1) 0 ∧ Pi.single (M := fun (a : m) ↦ α) j 1 ⬝ᵥ a = 0
neg :
  ∀ (h : ¬a i = 0) (h2 : ¬a j = 0),
    Ne (α := m → α) (fun (k : m) ↦ if k = i then a j else if k = j then -a i else 0) 0 ∧
      (fun (k : m) ↦ if k = i then a j else if k = j then -a i else 0) ⬝ᵥ a = 0
pos₂ :
  ∀ (h : ¬a i = 0) (h2 : a j = 0),
    Ne (α := m → α) (Pi.single (M := fun (a : m) ↦ α) j 1) 0 ∧ Pi.single (M := fun (a : m) ↦ α) j 1 ⬝ᵥ a = 0
neg₁ neg₂ :
  ∀ (h : ¬a i = 0) (h2 : ¬a j = 0),
    Ne (α := m → α) (fun (k : m) ↦ if k = i then a j else if k = j then -a i else 0) 0 ∧
      (fun (k : m) ↦ if k = i then a j else if k = j then -a i else 0) ⬝ᵥ a = 0
⊢ ∃ (b : m → α), b ≠ 0 ∧ b ⬝ᵥ a = 0

Tactic:
classical
  use if a i = 0 then Pi.single i 1 else if a j = 0 then Pi.single j 1 else
    fun k => if k = i then a j else if k = j then - a i else 0
  split_ifs with h h2
  · simp [h]
  · simp [h2]
  · refine ⟨Function.ne_iff.mpr ⟨i, by simp [h2]⟩, ?_⟩
    simp [dotProduct, Finset.sum_ite, Finset.sum_eq_ite i, hij.symm, mul_comm (a i)]

Premises used: dotProduct, Ne.symm, mul_comm, Finset.sum_ite
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : CommRing α
inst_2 : Nontrivial m
inst_3 : Nontrivial α
a : m → α
h : Function.Injective (dotProduct a)
obtain : ∀ (b : m → α) (hb : b ≠ 0) (hba : b ⬝ᵥ a = 0), False
⊢ False

Tactic:
obtain ⟨b, hb, hba⟩ := exists_ne_zero_dotProduct_eq_zero a

Premises used: exists_ne_zero_dotProduct_eq_zero
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : CommRing α
inst_2 : Nontrivial m
inst_3 : Nontrivial α
a : m → α
h : Function.Injective (dotProduct a)
b : m → α
hb : b ≠ 0
hba : b ⬝ᵥ a = 0
⊢ False

Tactic:
simpa [dotProduct_comm a b, hba, hb] using @h b 0

Premises used: dotProduct_comm
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : CommRing α
inst_2 : Nontrivial m
inst_3 : Nontrivial α
a : m → α
h : Function.Injective (β := α) fun (x : m → α) ↦ x ⬝ᵥ a
obtain : ∀ (b : m → α) (hb : b ≠ 0) (hba : b ⬝ᵥ a = 0), False
⊢ False

Tactic:
obtain ⟨b, hb, hba⟩ := exists_ne_zero_dotProduct_eq_zero a

Premises used: exists_ne_zero_dotProduct_eq_zero
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : CommRing α
inst_2 : Nontrivial m
inst_3 : Nontrivial α
a : m → α
h : Function.Injective (β := α) fun (x : m → α) ↦ x ⬝ᵥ a
b : m → α
hb : b ≠ 0
hba : b ⬝ᵥ a = 0
⊢ False

Tactic:
simpa [hba, hb] using @h b 0
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst : Fintype m
inst_1 : Mul α
inst_2 : AddCommMonoid α
M : Matrix l m α
N : Matrix m n α
i : l
k : n
⊢ (M * N) i k = ∑ j : m, M i j * N j k

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Finset.sum, rfl
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst : Fintype m
inst_1 : Mul α
inst_2 : AddCommMonoid α
M : Matrix l m α
N : Matrix m n α
i : l
k : n
⊢ (M * N) i k = M i ⬝ᵥ fun (j : m) ↦ N j k

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Matrix.Mul
Goal:
R : Type u_10
inst : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (A * B) 0 0 = A 0 0 * B 0 0 + A 0 1 * B 1 0 ∧
    (A * B) 0 1 = A 0 0 * B 0 1 + A 0 1 * B 1 1 ∧
      (A * B) 1 0 = A 1 0 * B 0 0 + A 1 1 * B 1 0 ∧ (A * B) 1 1 = A 1 0 * B 0 1 + A 1 1 * B 1 1

Tactic:
⟨?_, ?_, ?_, ?_⟩

Premises used: And.intro
-- Module: Mathlib.Data.Matrix.Mul
Goal:
R : Type u_10
inst : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
refine_1 : (A * B) 0 0 = A 0 0 * B 0 0 + A 0 1 * B 1 0
refine_2 : (A * B) 0 1 = A 0 0 * B 0 1 + A 0 1 * B 1 1
refine_3 : (A * B) 1 0 = A 1 0 * B 0 0 + A 1 1 * B 1 0
refine_4 : (A * B) 1 1 = A 1 0 * B 0 1 + A 1 1 * B 1 1
⊢ (A * B) 0 0 = A 0 0 * B 0 0 + A 0 1 * B 1 0 ∧
    (A * B) 0 1 = A 0 0 * B 0 1 + A 0 1 * B 1 1 ∧
      (A * B) 1 0 = A 1 0 * B 0 0 + A 1 1 * B 1 0 ∧ (A * B) 1 1 = A 1 0 * B 0 1 + A 1 1 * B 1 1

Tactic:
refine ⟨?_, ?_, ?_, ?_⟩
-- Module: Mathlib.Data.Matrix.Mul
Goal:
R : Type u_10
inst : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
refine_1 :
  (HAdd.hAdd (α := R) (∑ x ∈ Finset.range 0, if h : x < 2 then A 0 (⟨x, h⟩ : Fin 2) * B (⟨x, h⟩ : Fin 2) 0 else 0)
        (if h : LT.lt (α := ℕ) 0 2 then A 0 (⟨0, h⟩ : Fin 2) * B (⟨0, h⟩ : Fin 2) 0 else 0) +
      if h : LT.lt (α := ℕ) 1 2 then A 0 (⟨1, h⟩ : Fin 2) * B (⟨1, h⟩ : Fin 2) 0 else 0) =
    A 0 0 * B 0 0 + A 0 1 * B 1 0
⊢ (A * B) 0 0 = A 0 0 * B 0 0 + A 0 1 * B 1 0

Tactic:
rw [Matrix.mul_apply, Finset.sum_fin_eq_sum_range, Finset.sum_range_succ, Finset.sum_range_succ]

Premises used: Finset.sum_fin_eq_sum_range, Matrix.mul_apply, Finset.sum_range_succ
-- Module: Mathlib.Data.Matrix.Mul
Goal:
R : Type u_10
inst : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (HAdd.hAdd (α := R) (∑ x ∈ Finset.range 0, if h : x < 2 then A 0 (⟨x, h⟩ : Fin 2) * B (⟨x, h⟩ : Fin 2) 0 else 0)
        (if h : LT.lt (α := ℕ) 0 2 then A 0 (⟨0, h⟩ : Fin 2) * B (⟨0, h⟩ : Fin 2) 0 else 0) +
      if h : LT.lt (α := ℕ) 1 2 then A 0 (⟨1, h⟩ : Fin 2) * B (⟨1, h⟩ : Fin 2) 0 else 0) =
    A 0 0 * B 0 0 + A 0 1 * B 1 0

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Mul
Goal:
R : Type u_10
inst : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
refine_2 :
  (HAdd.hAdd (α := R) (∑ x ∈ Finset.range 0, if h : x < 2 then A 0 (⟨x, h⟩ : Fin 2) * B (⟨x, h⟩ : Fin 2) 1 else 0)
        (if h : LT.lt (α := ℕ) 0 2 then A 0 (⟨0, h⟩ : Fin 2) * B (⟨0, h⟩ : Fin 2) 1 else 0) +
      if h : LT.lt (α := ℕ) 1 2 then A 0 (⟨1, h⟩ : Fin 2) * B (⟨1, h⟩ : Fin 2) 1 else 0) =
    A 0 0 * B 0 1 + A 0 1 * B 1 1
⊢ (A * B) 0 1 = A 0 0 * B 0 1 + A 0 1 * B 1 1

Tactic:
rw [Matrix.mul_apply, Finset.sum_fin_eq_sum_range, Finset.sum_range_succ, Finset.sum_range_succ]

Premises used: Finset.sum_fin_eq_sum_range, Matrix.mul_apply, Finset.sum_range_succ
-- Module: Mathlib.Data.Matrix.Mul
Goal:
R : Type u_10
inst : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (HAdd.hAdd (α := R) (∑ x ∈ Finset.range 0, if h : x < 2 then A 0 (⟨x, h⟩ : Fin 2) * B (⟨x, h⟩ : Fin 2) 1 else 0)
        (if h : LT.lt (α := ℕ) 0 2 then A 0 (⟨0, h⟩ : Fin 2) * B (⟨0, h⟩ : Fin 2) 1 else 0) +
      if h : LT.lt (α := ℕ) 1 2 then A 0 (⟨1, h⟩ : Fin 2) * B (⟨1, h⟩ : Fin 2) 1 else 0) =
    A 0 0 * B 0 1 + A 0 1 * B 1 1

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Mul
Goal:
R : Type u_10
inst : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
refine_3 :
  (HAdd.hAdd (α := R) (∑ x ∈ Finset.range 0, if h : x < 2 then A 1 (⟨x, h⟩ : Fin 2) * B (⟨x, h⟩ : Fin 2) 0 else 0)
        (if h : LT.lt (α := ℕ) 0 2 then A 1 (⟨0, h⟩ : Fin 2) * B (⟨0, h⟩ : Fin 2) 0 else 0) +
      if h : LT.lt (α := ℕ) 1 2 then A 1 (⟨1, h⟩ : Fin 2) * B (⟨1, h⟩ : Fin 2) 0 else 0) =
    A 1 0 * B 0 0 + A 1 1 * B 1 0
⊢ (A * B) 1 0 = A 1 0 * B 0 0 + A 1 1 * B 1 0

Tactic:
rw [Matrix.mul_apply, Finset.sum_fin_eq_sum_range, Finset.sum_range_succ, Finset.sum_range_succ]

Premises used: Finset.sum_fin_eq_sum_range, Matrix.mul_apply, Finset.sum_range_succ
-- Module: Mathlib.Data.Matrix.Mul
Goal:
R : Type u_10
inst : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (HAdd.hAdd (α := R) (∑ x ∈ Finset.range 0, if h : x < 2 then A 1 (⟨x, h⟩ : Fin 2) * B (⟨x, h⟩ : Fin 2) 0 else 0)
        (if h : LT.lt (α := ℕ) 0 2 then A 1 (⟨0, h⟩ : Fin 2) * B (⟨0, h⟩ : Fin 2) 0 else 0) +
      if h : LT.lt (α := ℕ) 1 2 then A 1 (⟨1, h⟩ : Fin 2) * B (⟨1, h⟩ : Fin 2) 0 else 0) =
    A 1 0 * B 0 0 + A 1 1 * B 1 0

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Mul
Goal:
R : Type u_10
inst : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
refine_4 :
  (HAdd.hAdd (α := R) (∑ x ∈ Finset.range 0, if h : x < 2 then A 1 (⟨x, h⟩ : Fin 2) * B (⟨x, h⟩ : Fin 2) 1 else 0)
        (if h : LT.lt (α := ℕ) 0 2 then A 1 (⟨0, h⟩ : Fin 2) * B (⟨0, h⟩ : Fin 2) 1 else 0) +
      if h : LT.lt (α := ℕ) 1 2 then A 1 (⟨1, h⟩ : Fin 2) * B (⟨1, h⟩ : Fin 2) 1 else 0) =
    A 1 0 * B 0 1 + A 1 1 * B 1 1
⊢ (A * B) 1 1 = A 1 0 * B 0 1 + A 1 1 * B 1 1

Tactic:
rw [Matrix.mul_apply, Finset.sum_fin_eq_sum_range, Finset.sum_range_succ, Finset.sum_range_succ]

Premises used: Finset.sum_fin_eq_sum_range, Matrix.mul_apply, Finset.sum_range_succ
-- Module: Mathlib.Data.Matrix.Mul
Goal:
R : Type u_10
inst : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (HAdd.hAdd (α := R) (∑ x ∈ Finset.range 0, if h : x < 2 then A 1 (⟨x, h⟩ : Fin 2) * B (⟨x, h⟩ : Fin 2) 1 else 0)
        (if h : LT.lt (α := ℕ) 0 2 then A 1 (⟨0, h⟩ : Fin 2) * B (⟨0, h⟩ : Fin 2) 1 else 0) +
      if h : LT.lt (α := ℕ) 1 2 then A 1 (⟨1, h⟩ : Fin 2) * B (⟨1, h⟩ : Fin 2) 1 else 0) =
    A 1 0 * B 0 1 + A 1 1 * B 1 1

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst : AddCommMonoid α
inst_1 : Mul α
inst_2 : Fintype n
inst_3 : Monoid R
inst_4 : DistribMulAction R α
inst_5 : IsScalarTower R α α
a : R
M : Matrix m n α
N : Matrix n l α
a₁ : ∀ (i : m) (j : l), (a • M * N) i j = (a • (M * N)) i j
⊢ a • M * N = a • (M * N)

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst : AddCommMonoid α
inst_1 : Mul α
inst_2 : Fintype n
inst_3 : Monoid R
inst_4 : DistribMulAction R α
inst_5 : IsScalarTower R α α
a : R
M : Matrix m n α
N : Matrix n l α
i : m
j : l
⊢ (a • M * N) i j = (a • (M * N)) i j

Tactic:
apply smul_dotProduct a

Premises used: smul_dotProduct
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst : AddCommMonoid α
inst_1 : Mul α
inst_2 : Fintype n
inst_3 : Monoid R
inst_4 : DistribMulAction R α
inst_5 : SMulCommClass R α α
M : Matrix m n α
a : R
N : Matrix n l α
a₁ : ∀ (i : m) (j : l), (M * a • N) i j = (a • (M * N)) i j
⊢ M * a • N = a • (M * N)

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst : AddCommMonoid α
inst_1 : Mul α
inst_2 : Fintype n
inst_3 : Monoid R
inst_4 : DistribMulAction R α
inst_5 : SMulCommClass R α α
M : Matrix m n α
a : R
N : Matrix n l α
i : m
j : l
⊢ (M * a • N) i j = (a • (M * N)) i j

Tactic:
apply dotProduct_smul

Premises used: dotProduct_smul
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
M : Matrix m n α
a : ∀ (i : m) (j : o), HMul.hMul (β := Matrix n o α) M 0 i j = 0 i j
⊢ M * 0 = 0

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
M : Matrix m n α
i : m
j : o
⊢ HMul.hMul (β := Matrix n o α) M 0 i j = 0 i j

Tactic:
apply dotProduct_zero

Premises used: dotProduct_zero
-- 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
M : Matrix m n α
a : ∀ (i : l) (j : n), HMul.hMul (α := Matrix l m α) 0 M i j = 0 i j
⊢ 0 * M = 0

Tactic:
ext
-- 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
M : Matrix m n α
i : l
j : n
⊢ HMul.hMul (α := Matrix l m α) 0 M i j = 0 i j

Tactic:
apply zero_dotProduct

Premises used: zero_dotProduct
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
L : Matrix m n α
M N : Matrix n o α
a : ∀ (i : m) (j : o), (L * (M + N)) i j = (L * M + L * N) i j
⊢ L * (M + N) = L * M + L * N

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
L : Matrix m n α
M N : Matrix n o α
i : m
j : o
⊢ (L * (M + N)) i j = (L * M + L * N) i j

Tactic:
apply dotProduct_add

Premises used: dotProduct_add
-- 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 α
a : ∀ (i : l) (j : n), ((L + M) * N) i j = (L * N + M * N) i j
⊢ (L + M) * N = L * N + M * N

Tactic:
ext