awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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
⊢ 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 : α)
have 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 : α)
Tactic: by_cases h₂ : k = b
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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 : α)
⊢ 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 : α)
have 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 : α)
Tactic: by_cases h₂ : k = b
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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
⊢ 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 : α)
have 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 : α)
Tactic: by_cases h₂ : k = b
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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 : α)
⊢ 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 : α)
have 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 : α)
Tactic: by_cases h₂ : k = b
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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 : α
⊢ single i i' a * x * single j' j b = single i j (a * x i' j' * b)
have 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''
Tactic: ext i'' j''
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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
⊢ (single i i' a * x * single j' j b) i'' j'' = single i j (a * x i' j' * b) i'' j''
have 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'' :
    α)
Tactic: simp only [mul_apply, single]
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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
⊢ 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'' :
      α)
have 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'' :
      α)
Tactic: by_cases h₁ : i = i''
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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'' :
        α)
⊢ 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'' :
      α)
have 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'' :
      α)
Tactic: by_cases h₁ : i = i''
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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''
⊢ 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'' :
      α)
have 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'' :
      α)
Tactic: by_cases h₂ : j = j''
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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'' :
        α)
⊢ 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'' :
      α)
have 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'' :
      α)
Tactic: by_cases h₂ : j = j''
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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''
⊢ 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'' :
      α)
have 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'' :
      α)
Tactic: by_cases h₂ : j = j''
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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'' :
        α)
⊢ 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'' :
      α)
have 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'' :
      α)
Tactic: by_cases h₂ : j = j''
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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 : α
⊢ single i j c * single k l d = 0
have a : ∀ (a : l_1) (b : n), (single i j c * single k l d) a b = 0 a b
Tactic: ext a b
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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
⊢ (single i j c * single k l d) a b = 0 a b
have 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 only [mul_apply, single, of_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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
⊢ 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)
have 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)
Tactic: by_cases h₁ : i = a
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases h₁ : i = a
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (hypothesis)
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
⊢ M j k = 0
have this : 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
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (hypothesis)
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
hki : k ≠ i
⊢ M k i = 0
have this : HMul.hMul (α := Matrix n n α) (single i j 1) M k j = HMul.hMul (β := Matrix n n α) M (single i j 1) k j
Tactic: have := ext_iff.mpr hM k j
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (hypothesis)
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
i j : n
M : Matrix n n α
hM : Commute (single i j 1) M
⊢ M i i = M j j
have this : HMul.hMul (α := Matrix n n α) (single i j 1) M i j = HMul.hMul (β := Matrix n n α) M (single i j 1) i j
Tactic: have := ext_iff.mpr hM i j
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
M : Matrix n n α
hM : Pairwise fun (i j : n) ↦ Commute (single i j 1) M
⊢ Membership.mem (γ := Set (Matrix n n α)) (Set.range (ι := α) (⇑(scalar n) : (a : α) → Matrix n n α)) M
have inl : IsEmpty n → Membership.mem (γ := Set (Matrix n n α)) (Set.range (ι := α) (⇑(scalar n) : (a : α) → Matrix n n α)) M
Tactic: cases isEmpty_or_nonempty n