awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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 : α)
⊢ v ⬝ᵥ Pi.single (M := fun (a : m) ↦ α) i x = v i * x
have convert_2 : i ∉ Finset.univ → HMul.hMul (β := α) (v i) (Pi.single (M := fun (a : m) ↦ α) i x i : α) = 0
Tactic: convert! Finset.sum_eq_single i (fun j _ => this j) _ using 1
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
n : Type u_3
α : Type v
inst : Fintype n
inst_1 : NonAssocSemiring α
inst_2 : DecidableEq n
v : n → α
i : n
⊢ v ⬝ᵥ Pi.single (M := fun (a : n) ↦ α) i 1 = v i
have rw : v i * 1 = v i
Tactic: rw [dotProduct_single, mul_one]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ v ⬝ᵥ Pi.single (M := fun (a : n) ↦ α) i 1 = v i
have rw₁ : v i = v i
Tactic: rw [dotProduct_single, mul_one]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
n : Type u_3
α : Type v
inst : Fintype n
inst_1 : NonAssocSemiring α
inst_2 : DecidableEq n
i : n
v : n → α
⊢ Pi.single (M := fun (a : n) ↦ α) i 1 ⬝ᵥ v = v i
have rw : 1 * v i = v i
Tactic: rw [single_dotProduct, one_mul]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ Pi.single (M := fun (a : n) ↦ α) i 1 ⬝ᵥ v = v i
have rw₁ : v i = v i
Tactic: rw [single_dotProduct, one_mul]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : NonUnitalNonAssocRing α
v w : m → α
⊢ -v ⬝ᵥ -w = v ⬝ᵥ w
have rw : -(v ⬝ᵥ -w) = v ⬝ᵥ w
Tactic: rw [neg_dotProduct, dotProduct_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : NonUnitalNonAssocRing α
v w : m → α
rw : -(v ⬝ᵥ -w) = v ⬝ᵥ w
⊢ -v ⬝ᵥ -w = v ⬝ᵥ w
have rw₁ : - -(v ⬝ᵥ w) = v ⬝ᵥ w
Tactic: rw [neg_dotProduct, dotProduct_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ -v ⬝ᵥ -w = v ⬝ᵥ w
have rw₂ : v ⬝ᵥ w = v ⬝ᵥ w
Tactic: rw [neg_dotProduct, dotProduct_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : CommRing α
inst_2 : Nontrivial m
inst_3 : Nontrivial α
a : m → α
⊢ ∃ (b : m → α), b ≠ 0 ∧ b ⬝ᵥ a = 0
have obtain : ∀ (i j : m) (hij : i ≠ j), ∃ (b : m → α), b ≠ 0 ∧ b ⬝ᵥ a = 0
Tactic: obtain ⟨i, j, hij⟩ : ∃ i j : m, i ≠ j := nontrivial_iff.mp ‹_›
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ ∃ (b : m → α), b ≠ 0 ∧ b ⬝ᵥ a = 0
have 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
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
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ 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
have 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
Tactic: split_ifs with h h2
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ 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
have 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
Tactic: split_ifs with h h2
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ 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
have 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
Tactic: split_ifs with h h2
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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 → α) (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
have neg : (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]⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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 → α
⊢ ∃ (b : m → α), b ≠ 0 ∧ b ⬝ᵥ a = 0
have 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
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)]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ ∃ (b : m → α), b ≠ 0 ∧ b ⬝ᵥ a = 0
have 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
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)]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ ∃ (b : m → α), b ≠ 0 ∧ b ⬝ᵥ a = 0
have 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
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)]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ ∃ (b : m → α), b ≠ 0 ∧ b ⬝ᵥ a = 0
have 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
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)]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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)
⊢ False
have obtain : ∀ (b : m → α) (hb : b ≠ 0) (hba : b ⬝ᵥ a = 0), False
Tactic: obtain ⟨b, hb, hba⟩ := exists_ne_zero_dotProduct_eq_zero a
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ False
have obtain : ∀ (b : m → α) (hb : b ≠ 0) (hba : b ⬝ᵥ a = 0), False
Tactic: obtain ⟨b, hb, hba⟩ := exists_ne_zero_dotProduct_eq_zero a
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
have refine_1 : (A * B) 0 0 = A 0 0 * B 0 0 + A 0 1 * B 1 0
Tactic: refine ⟨?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ (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
have refine_2 : (A * B) 0 1 = A 0 0 * B 0 1 + A 0 1 * B 1 1
Tactic: refine ⟨?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ (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
have refine_3 : (A * B) 1 0 = A 1 0 * B 0 0 + A 1 1 * B 1 0
Tactic: refine ⟨?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ (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
have refine_4 : (A * B) 1 1 = A 1 0 * B 0 1 + A 1 1 * B 1 1
Tactic: refine ⟨?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
have 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
Tactic: rw [Matrix.mul_apply, Finset.sum_fin_eq_sum_range, Finset.sum_range_succ, Finset.sum_range_succ]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
R : Type u_10
inst : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (A * B) 0 1 = A 0 0 * B 0 1 + A 0 1 * B 1 1
have 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
Tactic: rw [Matrix.mul_apply, Finset.sum_fin_eq_sum_range, Finset.sum_range_succ, Finset.sum_range_succ]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
R : Type u_10
inst : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (A * B) 1 0 = A 1 0 * B 0 0 + A 1 1 * B 1 0
have 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
Tactic: rw [Matrix.mul_apply, Finset.sum_fin_eq_sum_range, Finset.sum_range_succ, Finset.sum_range_succ]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
R : Type u_10
inst : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (A * B) 1 1 = A 1 0 * B 0 1 + A 1 1 * B 1 1
have 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
Tactic: rw [Matrix.mul_apply, Finset.sum_fin_eq_sum_range, Finset.sum_range_succ, Finset.sum_range_succ]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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 • M * N = a • (M * N)
have a₁ : ∀ (i : m) (j : l), (a • M * N) i j = (a • (M * N)) 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
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 α
⊢ M * a • N = a • (M * N)
have a₁ : ∀ (i : m) (j : l), (M * a • N) i j = (a • (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 : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
M : Matrix m n α
⊢ M * 0 = 0
have a : ∀ (i : m) (j : o), HMul.hMul (β := Matrix n o α) M 0 i j = 0 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 : NonUnitalNonAssocSemiring α
inst_1 : Fintype m
M : Matrix m n α
⊢ 0 * M = 0
have a : ∀ (i : l) (j : n), HMul.hMul (α := Matrix l m α) 0 M i j = 0 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 : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
L : Matrix m n α
M N : Matrix n o α
⊢ L * (M + N) = L * M + L * N
have a : ∀ (i : m) (j : o), (L * (M + N)) i j = (L * M + L * N) 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 : NonUnitalNonAssocSemiring α
inst_1 : Fintype m
L M : Matrix l m α
N : Matrix m n α
⊢ (L + M) * N = L * N + M * N
have a : ∀ (i : l) (j : n), ((L + M) * N) i j = (L * N + 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
α : 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
have rw : (M * (diagonal d)ᵀ) i j = M i j * d j
Tactic: rw [← diagonal_transpose]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
have a : ∀ (i j : n), (diagonal d₁ * diagonal d₂) i j = diagonal (fun (i : n) ↦ d₁ i * d₂ i) i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
n : Type u_3
α : Type v
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
inst_2 : DecidableEq n
d₁ d₂ : n → α
i j : n
⊢ (diagonal d₁ * diagonal d₂) i j = diagonal (fun (i : n) ↦ d₁ i * d₂ i) i j
have pos : ∀ (h : i = j), (diagonal d₁ * diagonal d₂) i j = diagonal (fun (i : n) ↦ d₁ i * d₂ i) i j
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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
⊢ (diagonal d₁ * diagonal d₂) i j = diagonal (fun (i : n) ↦ d₁ i * d₂ i) i j
have neg : ∀ (h : ¬i = j), (diagonal d₁ * diagonal d₂) i j = diagonal (fun (i : n) ↦ d₁ i * d₂ i) i j
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
n : Type u_3
α : Type u_10
inst : NonUnitalNonAssocCommSemiring α
inst_1 : Fintype n
inst_2 : DecidableEq n
d₁ d₂ : n → α
⊢ Commute (diagonal d₁) (diagonal d₂)
have simp_rw : diagonal d₁ * diagonal d₂ = diagonal d₂ * diagonal d₁
Tactic: simp_rw [commute_iff_eq, diagonal_mul_diagonal, mul_comm]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
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₁
⊢ Commute (diagonal d₁) (diagonal d₂)
have simp_rw₁ : Eq (α := Matrix n n α) (diagonal fun (i : n) ↦ d₁ i * d₂ i) (diagonal fun (i : n) ↦ d₂ i * d₁ i)
Tactic: simp_rw [commute_iff_eq, diagonal_mul_diagonal, mul_comm]
-- 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
inst_2 : DecidableEq m
M : Matrix m n α
a : α
⊢ a • M = HMul.hMul (α := Matrix m m α) (diagonal fun (x : m) ↦ a) M
have a₁ : ∀ (i : m) (j : n), (a • M) i j = HMul.hMul (α := Matrix m m α) (diagonal fun (x : m) ↦ a) 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 : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix m n α
a : α
⊢ MulOpposite.op a • M = HMul.hMul (β := Matrix n n α) M (diagonal fun (x : n) ↦ a)
have 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: 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
β : 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
⊢ (L * M).map (⇑f : (a : α) → β) =
    HMul.hMul (α := Matrix m n β) (β := Matrix n o β) (L.map (⇑f : (a : α) → β)) (M.map (⇑f : (a : α) → β))
have 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
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
inst_2 : DecidableEq m
M : Matrix m n α
⊢ 1 * M = M
have a : ∀ (i : m) (j : n), HMul.hMul (α := Matrix m m α) 1 M 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 m
inst_2 : DecidableEq m
M : Matrix m n α
i : m
j : n
⊢ HMul.hMul (α := Matrix m m α) 1 M i j = M i j
have a : HMul.hMul (α := Matrix m m α) (diagonal fun (x : m) ↦ 1) M i j = M i j
Tactic: rw [← diagonal_one, diagonal_mul, one_mul]