awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Matrix.Basis
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : Fintype m
inst_4 : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
k : n
d : α
a : l
b : n
pos :
  ∀ (h₁ : i = a),
    Eq.{u_7 + 1} (α := α)
      (∑ j_1 : m,
          HMul.hMul (α := α) (β := α)
            ((of : (a : l → m → α) → Matrix l m α) (fun (i' : l) (j' : m) ↦ if i = i' ∧ j = j' then c else 0) a j_1 : α)
            ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if j = i' ∧ k = j' then d else 0) j_1 b :
              α) :
        α)
      ((of : (a : l → n → α) → Matrix l n α) (fun (i' : l) (j' : n) ↦ if i = i' ∧ k = j' then c * d else 0) a b : α)
neg :
  ∀ (h₁ : ¬i = a),
    Eq.{u_7 + 1} (α := α)
      (∑ j_1 : m,
          HMul.hMul (α := α) (β := α)
            ((of : (a : l → m → α) → Matrix l m α) (fun (i' : l) (j' : m) ↦ if i = i' ∧ j = j' then c else 0) a j_1 : α)
            ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if j = i' ∧ k = j' then d else 0) j_1 b :
              α) :
        α)
      ((of : (a : l → n → α) → Matrix l n α) (fun (i' : l) (j' : n) ↦ if i = i' ∧ k = j' then c * d else 0) a b : α)
⊢ Eq.{u_7 + 1} (α := α)
    (∑ j_1 : m,
        HMul.hMul (α := α) (β := α)
          ((of : (a : l → m → α) → Matrix l m α) (fun (i' : l) (j' : m) ↦ if i = i' ∧ j = j' then c else 0) a j_1 : α)
          ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if j = i' ∧ k = j' then d else 0) j_1 b : α) :
      α)
    ((of : (a : l → n → α) → Matrix l n α) (fun (i' : l) (j' : n) ↦ if i = i' ∧ k = j' then c * d else 0) a b : α)

Tactic:
by_cases h₁ : i = a
-- Module: Mathlib.Data.Matrix.Basis
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : Fintype m
inst_4 : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
k : n
d : α
a : l
b : n
h₁ : i = a
pos :
  ∀ (h₂ : k = b),
    Eq.{u_7 + 1} (α := α)
      (∑ j_1 : m,
          HMul.hMul (α := α) (β := α)
            ((of : (a : l → m → α) → Matrix l m α) (fun (i' : l) (j' : m) ↦ if i = i' ∧ j = j' then c else 0) a j_1 : α)
            ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if j = i' ∧ k = j' then d else 0) j_1 b :
              α) :
        α)
      ((of : (a : l → n → α) → Matrix l n α) (fun (i' : l) (j' : n) ↦ if i = i' ∧ k = j' then c * d else 0) a b : α)
neg :
  ∀ (h₂ : ¬k = b),
    Eq.{u_7 + 1} (α := α)
      (∑ j_1 : m,
          HMul.hMul (α := α) (β := α)
            ((of : (a : l → m → α) → Matrix l m α) (fun (i' : l) (j' : m) ↦ if i = i' ∧ j = j' then c else 0) a j_1 : α)
            ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if j = i' ∧ k = j' then d else 0) j_1 b :
              α) :
        α)
      ((of : (a : l → n → α) → Matrix l n α) (fun (i' : l) (j' : n) ↦ if i = i' ∧ k = j' then c * d else 0) a b : α)
⊢ Eq.{u_7 + 1} (α := α)
    (∑ j_1 : m,
        HMul.hMul (α := α) (β := α)
          ((of : (a : l → m → α) → Matrix l m α) (fun (i' : l) (j' : m) ↦ if i = i' ∧ j = j' then c else 0) a j_1 : α)
          ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if j = i' ∧ k = j' then d else 0) j_1 b : α) :
      α)
    ((of : (a : l → n → α) → Matrix l n α) (fun (i' : l) (j' : n) ↦ if i = i' ∧ k = j' then c * d else 0) a b : α)

Tactic:
by_cases h₂ : k = b
-- Module: Mathlib.Data.Matrix.Basis
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : Fintype m
inst_4 : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
k : n
d : α
a : l
b : n
h₁ : ¬i = a
pos :
  ∀ (h₂ : k = b),
    Eq.{u_7 + 1} (α := α)
      (∑ j_1 : m,
          HMul.hMul (α := α) (β := α)
            ((of : (a : l → m → α) → Matrix l m α) (fun (i' : l) (j' : m) ↦ if i = i' ∧ j = j' then c else 0) a j_1 : α)
            ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if j = i' ∧ k = j' then d else 0) j_1 b :
              α) :
        α)
      ((of : (a : l → n → α) → Matrix l n α) (fun (i' : l) (j' : n) ↦ if i = i' ∧ k = j' then c * d else 0) a b : α)
neg :
  ∀ (h₂ : ¬k = b),
    Eq.{u_7 + 1} (α := α)
      (∑ j_1 : m,
          HMul.hMul (α := α) (β := α)
            ((of : (a : l → m → α) → Matrix l m α) (fun (i' : l) (j' : m) ↦ if i = i' ∧ j = j' then c else 0) a j_1 : α)
            ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if j = i' ∧ k = j' then d else 0) j_1 b :
              α) :
        α)
      ((of : (a : l → n → α) → Matrix l n α) (fun (i' : l) (j' : n) ↦ if i = i' ∧ k = j' then c * d else 0) a b : α)
⊢ Eq.{u_7 + 1} (α := α)
    (∑ j_1 : m,
        HMul.hMul (α := α) (β := α)
          ((of : (a : l → m → α) → Matrix l m α) (fun (i' : l) (j' : m) ↦ if i = i' ∧ j = j' then c else 0) a j_1 : α)
          ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if j = i' ∧ k = j' then d else 0) j_1 b : α) :
      α)
    ((of : (a : l → n → α) → Matrix l n α) (fun (i' : l) (j' : n) ↦ if i = i' ∧ k = j' then c * d else 0) a b : α)

Tactic:
by_cases h₂ : k = b
-- Module: Mathlib.Data.Matrix.Basis
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : Fintype m
inst_4 : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
k : n
d : α
a : l
b : n
h₁ : i = a
h₂ : k = b
⊢ Eq.{u_7 + 1} (α := α)
    (∑ j_1 : m,
        HMul.hMul (α := α) (β := α)
          ((of : (a : l → m → α) → Matrix l m α) (fun (i' : l) (j' : m) ↦ if i = i' ∧ j = j' then c else 0) a j_1 : α)
          ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if j = i' ∧ k = j' then d else 0) j_1 b : α) :
      α)
    ((of : (a : l → n → α) → Matrix l n α) (fun (i' : l) (j' : n) ↦ if i = i' ∧ k = j' then c * d else 0) a b : α)

Tactic:
simp [h₁, h₂]
-- Module: Mathlib.Data.Matrix.Basis
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : Fintype m
inst_4 : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
k : n
d : α
a : l
b : n
h₁ : i = a
h₂ : ¬k = b
⊢ Eq.{u_7 + 1} (α := α)
    (∑ j_1 : m,
        HMul.hMul (α := α) (β := α)
          ((of : (a : l → m → α) → Matrix l m α) (fun (i' : l) (j' : m) ↦ if i = i' ∧ j = j' then c else 0) a j_1 : α)
          ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if j = i' ∧ k = j' then d else 0) j_1 b : α) :
      α)
    ((of : (a : l → n → α) → Matrix l n α) (fun (i' : l) (j' : n) ↦ if i = i' ∧ k = j' then c * d else 0) a b : α)

Tactic:
simp [h₁, h₂]
-- Module: Mathlib.Data.Matrix.Basis
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : Fintype m
inst_4 : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
k : n
d : α
a : l
b : n
h₁ : ¬i = a
h₂ : k = b
⊢ Eq.{u_7 + 1} (α := α)
    (∑ j_1 : m,
        HMul.hMul (α := α) (β := α)
          ((of : (a : l → m → α) → Matrix l m α) (fun (i' : l) (j' : m) ↦ if i = i' ∧ j = j' then c else 0) a j_1 : α)
          ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if j = i' ∧ k = j' then d else 0) j_1 b : α) :
      α)
    ((of : (a : l → n → α) → Matrix l n α) (fun (i' : l) (j' : n) ↦ if i = i' ∧ k = j' then c * d else 0) a b : α)

Tactic:
simp [h₁, h₂]
-- Module: Mathlib.Data.Matrix.Basis
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : Fintype m
inst_4 : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
k : n
d : α
a : l
b : n
h₁ : ¬i = a
h₂ : ¬k = b
⊢ Eq.{u_7 + 1} (α := α)
    (∑ j_1 : m,
        HMul.hMul (α := α) (β := α)
          ((of : (a : l → m → α) → Matrix l m α) (fun (i' : l) (j' : m) ↦ if i = i' ∧ j = j' then c else 0) a j_1 : α)
          ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if j = i' ∧ k = j' then d else 0) j_1 b : α) :
      α)
    ((of : (a : l → n → α) → Matrix l n α) (fun (i' : l) (j' : n) ↦ if i = i' ∧ k = j' then c * d else 0) a b : α)

Tactic:
simp [h₁, h₂]
-- Module: Mathlib.Data.Matrix.Basis
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_7
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : DecidableEq o
inst_4 : Fintype m
inst_5 : NonUnitalNonAssocSemiring α
inst_6 : Fintype n
i : l
i' : m
j' : n
j : o
a : α
x : Matrix m n α
b : α
a₁ : ∀ (i'' : l) (j'' : o), (single i i' a * x * single j' j b) i'' j'' = single i j (a * x i' j' * b) i'' j''
⊢ single i i' a * x * single j' j b = single i j (a * x i' j' * b)

Tactic:
ext i'' j''
-- Module: Mathlib.Data.Matrix.Basis
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_7
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : DecidableEq o
inst_4 : Fintype m
inst_5 : NonUnitalNonAssocSemiring α
inst_6 : Fintype n
i : l
i' : m
j' : n
j : o
a : α
x : Matrix m n α
b : α
i'' : l
j'' : o
a₁ :
  Eq.{u_7 + 1} (α := α)
    (∑ x_1 : n,
        HMul.hMul (α := α) (β := α)
          (∑ j : m,
              HMul.hMul (α := α)
                ((of : (a : l → m → α) → Matrix l m α) (fun (i'_1 : l) (j' : m) ↦ if i = i'_1 ∧ i' = j' then a else 0)
                    i'' j :
                  α)
                (x j x_1) :
            α)
          ((of : (a : n → o → α) → Matrix n o α) (fun (i' : n) (j'_1 : o) ↦ if j' = i' ∧ j = j'_1 then b else 0) x_1
              j'' :
            α) :
      α)
    ((of : (a : l → o → α) → Matrix l o α)
        (fun (i'_1 : l) (j'_1 : o) ↦ if i = i'_1 ∧ j = j'_1 then a * x i' j' * b else 0) i'' j'' :
      α)
⊢ (single i i' a * x * single j' j b) i'' j'' = single i j (a * x i' j' * b) i'' j''

Tactic:
simp only [mul_apply, single]

Premises used: Matrix.mul_apply, Matrix.single
-- Module: Mathlib.Data.Matrix.Basis
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_7
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : DecidableEq o
inst_4 : Fintype m
inst_5 : NonUnitalNonAssocSemiring α
inst_6 : Fintype n
i : l
i' : m
j' : n
j : o
a : α
x : Matrix m n α
b : α
i'' : l
j'' : o
pos :
  ∀ (h₁ : i = i''),
    Eq.{u_7 + 1} (α := α)
      (∑ x_1 : n,
          HMul.hMul (α := α) (β := α)
            (∑ j : m,
                HMul.hMul (α := α)
                  ((of : (a : l → m → α) → Matrix l m α) (fun (i'_1 : l) (j' : m) ↦ if i = i'_1 ∧ i' = j' then a else 0)
                      i'' j :
                    α)
                  (x j x_1) :
              α)
            ((of : (a : n → o → α) → Matrix n o α) (fun (i' : n) (j'_1 : o) ↦ if j' = i' ∧ j = j'_1 then b else 0) x_1
                j'' :
              α) :
        α)
      ((of : (a : l → o → α) → Matrix l o α)
          (fun (i'_1 : l) (j'_1 : o) ↦ if i = i'_1 ∧ j = j'_1 then a * x i' j' * b else 0) i'' j'' :
        α)
neg :
  ∀ (h₁ : ¬i = i''),
    Eq.{u_7 + 1} (α := α)
      (∑ x_1 : n,
          HMul.hMul (α := α) (β := α)
            (∑ j : m,
                HMul.hMul (α := α)
                  ((of : (a : l → m → α) → Matrix l m α) (fun (i'_1 : l) (j' : m) ↦ if i = i'_1 ∧ i' = j' then a else 0)
                      i'' j :
                    α)
                  (x j x_1) :
              α)
            ((of : (a : n → o → α) → Matrix n o α) (fun (i' : n) (j'_1 : o) ↦ if j' = i' ∧ j = j'_1 then b else 0) x_1
                j'' :
              α) :
        α)
      ((of : (a : l → o → α) → Matrix l o α)
          (fun (i'_1 : l) (j'_1 : o) ↦ if i = i'_1 ∧ j = j'_1 then a * x i' j' * b else 0) i'' j'' :
        α)
⊢ Eq.{u_7 + 1} (α := α)
    (∑ x_1 : n,
        HMul.hMul (α := α) (β := α)
          (∑ j : m,
              HMul.hMul (α := α)
                ((of : (a : l → m → α) → Matrix l m α) (fun (i'_1 : l) (j' : m) ↦ if i = i'_1 ∧ i' = j' then a else 0)
                    i'' j :
                  α)
                (x j x_1) :
            α)
          ((of : (a : n → o → α) → Matrix n o α) (fun (i' : n) (j'_1 : o) ↦ if j' = i' ∧ j = j'_1 then b else 0) x_1
              j'' :
            α) :
      α)
    ((of : (a : l → o → α) → Matrix l o α)
        (fun (i'_1 : l) (j'_1 : o) ↦ if i = i'_1 ∧ j = j'_1 then a * x i' j' * b else 0) i'' j'' :
      α)

Tactic:
by_cases h₁ : i = i''
-- Module: Mathlib.Data.Matrix.Basis
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_7
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : DecidableEq o
inst_4 : Fintype m
inst_5 : NonUnitalNonAssocSemiring α
inst_6 : Fintype n
i : l
i' : m
j' : n
j : o
a : α
x : Matrix m n α
b : α
i'' : l
j'' : o
h₁ : i = i''
pos :
  ∀ (h₂ : j = j''),
    Eq.{u_7 + 1} (α := α)
      (∑ x_1 : n,
          HMul.hMul (α := α) (β := α)
            (∑ j : m,
                HMul.hMul (α := α)
                  ((of : (a : l → m → α) → Matrix l m α) (fun (i'_1 : l) (j' : m) ↦ if i = i'_1 ∧ i' = j' then a else 0)
                      i'' j :
                    α)
                  (x j x_1) :
              α)
            ((of : (a : n → o → α) → Matrix n o α) (fun (i' : n) (j'_1 : o) ↦ if j' = i' ∧ j = j'_1 then b else 0) x_1
                j'' :
              α) :
        α)
      ((of : (a : l → o → α) → Matrix l o α)
          (fun (i'_1 : l) (j'_1 : o) ↦ if i = i'_1 ∧ j = j'_1 then a * x i' j' * b else 0) i'' j'' :
        α)
neg :
  ∀ (h₂ : ¬j = j''),
    Eq.{u_7 + 1} (α := α)
      (∑ x_1 : n,
          HMul.hMul (α := α) (β := α)
            (∑ j : m,
                HMul.hMul (α := α)
                  ((of : (a : l → m → α) → Matrix l m α) (fun (i'_1 : l) (j' : m) ↦ if i = i'_1 ∧ i' = j' then a else 0)
                      i'' j :
                    α)
                  (x j x_1) :
              α)
            ((of : (a : n → o → α) → Matrix n o α) (fun (i' : n) (j'_1 : o) ↦ if j' = i' ∧ j = j'_1 then b else 0) x_1
                j'' :
              α) :
        α)
      ((of : (a : l → o → α) → Matrix l o α)
          (fun (i'_1 : l) (j'_1 : o) ↦ if i = i'_1 ∧ j = j'_1 then a * x i' j' * b else 0) i'' j'' :
        α)
⊢ Eq.{u_7 + 1} (α := α)
    (∑ x_1 : n,
        HMul.hMul (α := α) (β := α)
          (∑ j : m,
              HMul.hMul (α := α)
                ((of : (a : l → m → α) → Matrix l m α) (fun (i'_1 : l) (j' : m) ↦ if i = i'_1 ∧ i' = j' then a else 0)
                    i'' j :
                  α)
                (x j x_1) :
            α)
          ((of : (a : n → o → α) → Matrix n o α) (fun (i' : n) (j'_1 : o) ↦ if j' = i' ∧ j = j'_1 then b else 0) x_1
              j'' :
            α) :
      α)
    ((of : (a : l → o → α) → Matrix l o α)
        (fun (i'_1 : l) (j'_1 : o) ↦ if i = i'_1 ∧ j = j'_1 then a * x i' j' * b else 0) i'' j'' :
      α)

Tactic:
by_cases h₂ : j = j''
-- Module: Mathlib.Data.Matrix.Basis
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_7
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : DecidableEq o
inst_4 : Fintype m
inst_5 : NonUnitalNonAssocSemiring α
inst_6 : Fintype n
i : l
i' : m
j' : n
j : o
a : α
x : Matrix m n α
b : α
i'' : l
j'' : o
h₁ : ¬i = i''
pos :
  ∀ (h₂ : j = j''),
    Eq.{u_7 + 1} (α := α)
      (∑ x_1 : n,
          HMul.hMul (α := α) (β := α)
            (∑ j : m,
                HMul.hMul (α := α)
                  ((of : (a : l → m → α) → Matrix l m α) (fun (i'_1 : l) (j' : m) ↦ if i = i'_1 ∧ i' = j' then a else 0)
                      i'' j :
                    α)
                  (x j x_1) :
              α)
            ((of : (a : n → o → α) → Matrix n o α) (fun (i' : n) (j'_1 : o) ↦ if j' = i' ∧ j = j'_1 then b else 0) x_1
                j'' :
              α) :
        α)
      ((of : (a : l → o → α) → Matrix l o α)
          (fun (i'_1 : l) (j'_1 : o) ↦ if i = i'_1 ∧ j = j'_1 then a * x i' j' * b else 0) i'' j'' :
        α)
neg :
  ∀ (h₂ : ¬j = j''),
    Eq.{u_7 + 1} (α := α)
      (∑ x_1 : n,
          HMul.hMul (α := α) (β := α)
            (∑ j : m,
                HMul.hMul (α := α)
                  ((of : (a : l → m → α) → Matrix l m α) (fun (i'_1 : l) (j' : m) ↦ if i = i'_1 ∧ i' = j' then a else 0)
                      i'' j :
                    α)
                  (x j x_1) :
              α)
            ((of : (a : n → o → α) → Matrix n o α) (fun (i' : n) (j'_1 : o) ↦ if j' = i' ∧ j = j'_1 then b else 0) x_1
                j'' :
              α) :
        α)
      ((of : (a : l → o → α) → Matrix l o α)
          (fun (i'_1 : l) (j'_1 : o) ↦ if i = i'_1 ∧ j = j'_1 then a * x i' j' * b else 0) i'' j'' :
        α)
⊢ Eq.{u_7 + 1} (α := α)
    (∑ x_1 : n,
        HMul.hMul (α := α) (β := α)
          (∑ j : m,
              HMul.hMul (α := α)
                ((of : (a : l → m → α) → Matrix l m α) (fun (i'_1 : l) (j' : m) ↦ if i = i'_1 ∧ i' = j' then a else 0)
                    i'' j :
                  α)
                (x j x_1) :
            α)
          ((of : (a : n → o → α) → Matrix n o α) (fun (i' : n) (j'_1 : o) ↦ if j' = i' ∧ j = j'_1 then b else 0) x_1
              j'' :
            α) :
      α)
    ((of : (a : l → o → α) → Matrix l o α)
        (fun (i'_1 : l) (j'_1 : o) ↦ if i = i'_1 ∧ j = j'_1 then a * x i' j' * b else 0) i'' j'' :
      α)

Tactic:
by_cases h₂ : j = j''
-- Module: Mathlib.Data.Matrix.Basis
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_7
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : DecidableEq o
inst_4 : Fintype m
inst_5 : NonUnitalNonAssocSemiring α
inst_6 : Fintype n
i : l
i' : m
j' : n
j : o
a : α
x : Matrix m n α
b : α
i'' : l
j'' : o
h₁ : i = i''
h₂ : j = j''
⊢ Eq.{u_7 + 1} (α := α)
    (∑ x_1 : n,
        HMul.hMul (α := α) (β := α)
          (∑ j : m,
              HMul.hMul (α := α)
                ((of : (a : l → m → α) → Matrix l m α) (fun (i'_1 : l) (j' : m) ↦ if i = i'_1 ∧ i' = j' then a else 0)
                    i'' j :
                  α)
                (x j x_1) :
            α)
          ((of : (a : n → o → α) → Matrix n o α) (fun (i' : n) (j'_1 : o) ↦ if j' = i' ∧ j = j'_1 then b else 0) x_1
              j'' :
            α) :
      α)
    ((of : (a : l → o → α) → Matrix l o α)
        (fun (i'_1 : l) (j'_1 : o) ↦ if i = i'_1 ∧ j = j'_1 then a * x i' j' * b else 0) i'' j'' :
      α)

Tactic:
simp [h₁, h₂]
-- Module: Mathlib.Data.Matrix.Basis
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_7
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : DecidableEq o
inst_4 : Fintype m
inst_5 : NonUnitalNonAssocSemiring α
inst_6 : Fintype n
i : l
i' : m
j' : n
j : o
a : α
x : Matrix m n α
b : α
i'' : l
j'' : o
h₁ : i = i''
h₂ : ¬j = j''
⊢ Eq.{u_7 + 1} (α := α)
    (∑ x_1 : n,
        HMul.hMul (α := α) (β := α)
          (∑ j : m,
              HMul.hMul (α := α)
                ((of : (a : l → m → α) → Matrix l m α) (fun (i'_1 : l) (j' : m) ↦ if i = i'_1 ∧ i' = j' then a else 0)
                    i'' j :
                  α)
                (x j x_1) :
            α)
          ((of : (a : n → o → α) → Matrix n o α) (fun (i' : n) (j'_1 : o) ↦ if j' = i' ∧ j = j'_1 then b else 0) x_1
              j'' :
            α) :
      α)
    ((of : (a : l → o → α) → Matrix l o α)
        (fun (i'_1 : l) (j'_1 : o) ↦ if i = i'_1 ∧ j = j'_1 then a * x i' j' * b else 0) i'' j'' :
      α)

Tactic:
simp [h₁, h₂]
-- Module: Mathlib.Data.Matrix.Basis
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_7
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : DecidableEq o
inst_4 : Fintype m
inst_5 : NonUnitalNonAssocSemiring α
inst_6 : Fintype n
i : l
i' : m
j' : n
j : o
a : α
x : Matrix m n α
b : α
i'' : l
j'' : o
h₁ : ¬i = i''
h₂ : j = j''
⊢ Eq.{u_7 + 1} (α := α)
    (∑ x_1 : n,
        HMul.hMul (α := α) (β := α)
          (∑ j : m,
              HMul.hMul (α := α)
                ((of : (a : l → m → α) → Matrix l m α) (fun (i'_1 : l) (j' : m) ↦ if i = i'_1 ∧ i' = j' then a else 0)
                    i'' j :
                  α)
                (x j x_1) :
            α)
          ((of : (a : n → o → α) → Matrix n o α) (fun (i' : n) (j'_1 : o) ↦ if j' = i' ∧ j = j'_1 then b else 0) x_1
              j'' :
            α) :
      α)
    ((of : (a : l → o → α) → Matrix l o α)
        (fun (i'_1 : l) (j'_1 : o) ↦ if i = i'_1 ∧ j = j'_1 then a * x i' j' * b else 0) i'' j'' :
      α)

Tactic:
simp [h₁, h₂]
-- Module: Mathlib.Data.Matrix.Basis
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_7
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : DecidableEq o
inst_4 : Fintype m
inst_5 : NonUnitalNonAssocSemiring α
inst_6 : Fintype n
i : l
i' : m
j' : n
j : o
a : α
x : Matrix m n α
b : α
i'' : l
j'' : o
h₁ : ¬i = i''
h₂ : ¬j = j''
⊢ Eq.{u_7 + 1} (α := α)
    (∑ x_1 : n,
        HMul.hMul (α := α) (β := α)
          (∑ j : m,
              HMul.hMul (α := α)
                ((of : (a : l → m → α) → Matrix l m α) (fun (i'_1 : l) (j' : m) ↦ if i = i'_1 ∧ i' = j' then a else 0)
                    i'' j :
                  α)
                (x j x_1) :
            α)
          ((of : (a : n → o → α) → Matrix n o α) (fun (i' : n) (j'_1 : o) ↦ if j' = i' ∧ j = j'_1 then b else 0) x_1
              j'' :
            α) :
      α)
    ((of : (a : l → o → α) → Matrix l o α)
        (fun (i'_1 : l) (j'_1 : o) ↦ if i = i'_1 ∧ j = j'_1 then a * x i' j' * b else 0) i'' j'' :
      α)

Tactic:
simp [h₁, h₂]
-- Module: Mathlib.Data.Matrix.Basis
Goal:
l_1 : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq l_1
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : Fintype m
inst_4 : NonUnitalNonAssocSemiring α
c : α
i : l_1
j k : m
l : n
h : j ≠ k
d : α
a : ∀ (a : l_1) (b : n), (single i j c * single k l d) a b = 0 a b
⊢ single i j c * single k l d = 0

Tactic:
ext a b
-- Module: Mathlib.Data.Matrix.Basis
Goal:
l_1 : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq l_1
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : Fintype m
inst_4 : NonUnitalNonAssocSemiring α
c : α
i : l_1
j k : m
l : n
h : j ≠ k
d : α
a : l_1
b : n
a₁ : Eq.{u_7 + 1} (α := α) (∑ x : m, (if i = a ∧ j = x then c else 0) * if k = x ∧ l = b then d else 0) (0 a b)
⊢ (single i j c * single k l d) a b = 0 a b

Tactic:
simp only [mul_apply, single, of_apply]

Premises used: Matrix.mul_apply, Matrix.of_apply, Matrix.single
-- Module: Mathlib.Data.Matrix.Basis
Goal:
l_1 : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq l_1
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : Fintype m
inst_4 : NonUnitalNonAssocSemiring α
c : α
i : l_1
j k : m
l : n
h : j ≠ k
d : α
a : l_1
b : n
pos :
  ∀ (h₁ : i = a),
    Eq.{u_7 + 1} (α := α) (∑ x : m, (if i = a ∧ j = x then c else 0) * if k = x ∧ l = b then d else 0) (0 a b)
neg :
  ∀ (h₁ : ¬i = a),
    Eq.{u_7 + 1} (α := α) (∑ x : m, (if i = a ∧ j = x then c else 0) * if k = x ∧ l = b then d else 0) (0 a b)
⊢ Eq.{u_7 + 1} (α := α) (∑ x : m, (if i = a ∧ j = x then c else 0) * if k = x ∧ l = b then d else 0) (0 a b)

Tactic:
by_cases h₁ : i = a
-- Module: Mathlib.Data.Matrix.Basis
Goal:
l_1 : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq l_1
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : Fintype m
inst_4 : NonUnitalNonAssocSemiring α
c : α
i : l_1
j k : m
l : n
h : j ≠ k
d : α
a : l_1
b : n
h₁ : i = a
⊢ Eq.{u_7 + 1} (α := α) (∑ x : m, (if i = a ∧ j = x then c else 0) * if k = x ∧ l = b then d else 0) (0 a b)

Tactic:
simp [h₁, h, Finset.sum_eq_zero]

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.Data.Matrix.Basis
Goal:
l_1 : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq l_1
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : Fintype m
inst_4 : NonUnitalNonAssocSemiring α
c : α
i : l_1
j k : m
l : n
h : j ≠ k
d : α
a : l_1
b : n
h₁ : ¬i = a
⊢ Eq.{u_7 + 1} (α := α) (∑ x : m, (if i = a ∧ j = x then c else 0) * if k = x ∧ l = b then d else 0) (0 a b)

Tactic:
simp [h₁]
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
i j k : n
M : Matrix n n α
hM : Commute (single i j 1) M
hkj : k ≠ j
⊢ HMul.hMul (α := Matrix n n α) (single i j 1) M i k = HMul.hMul (β := Matrix n n α) M (single i j 1) i k

Tactic:
have := ext_iff.mpr hM i k