awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Zero α
i : m
j : n
a_1 : α
a : m
b : n
hi : ¬i = a
pos :
  ∀ (hj : j = b),
    Eq.{u_7 + 1} (α := α)
      ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a_1 else 0) a b : α)
      ((of : (a : m → n → α) → Matrix m n α)
          (Pi.single (M := fun (a : m) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j a_1)) a b :
        α)
neg :
  ∀ (hj : ¬j = b),
    Eq.{u_7 + 1} (α := α)
      ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a_1 else 0) a b : α)
      ((of : (a : m → n → α) → Matrix m n α)
          (Pi.single (M := fun (a : m) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j a_1)) a b :
        α)
⊢ Eq.{u_7 + 1} (α := α)
    ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a_1 else 0) a b : α)
    ((of : (a : m → n → α) → Matrix m n α)
        (Pi.single (M := fun (a : m) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j a_1)) a b :
      α)

Tactic:
by_cases hj : j = b
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Zero α
i : m
j : n
a_1 : α
a : m
b : n
hi : i = a
hj : j = b
⊢ Eq.{u_7 + 1} (α := α)
    ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a_1 else 0) a b : α)
    ((of : (a : m → n → α) → Matrix m n α)
        (Pi.single (M := fun (a : m) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j a_1)) a b :
      α)

Tactic:
simp [*]
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Zero α
i : m
j : n
a_1 : α
a : m
b : n
hi : i = a
hj : ¬j = b
⊢ Eq.{u_7 + 1} (α := α)
    ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a_1 else 0) a b : α)
    ((of : (a : m → n → α) → Matrix m n α)
        (Pi.single (M := fun (a : m) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j a_1)) a b :
      α)

Tactic:
simp [*]
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Zero α
i : m
j : n
a_1 : α
a : m
b : n
hi : ¬i = a
hj : j = b
⊢ Eq.{u_7 + 1} (α := α)
    ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a_1 else 0) a b : α)
    ((of : (a : m → n → α) → Matrix m n α)
        (Pi.single (M := fun (a : m) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j a_1)) a b :
      α)

Tactic:
simp [*]
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Zero α
i : m
j : n
a_1 : α
a : m
b : n
hi : ¬i = a
hj : ¬j = b
⊢ Eq.{u_7 + 1} (α := α)
    ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a_1 else 0) a b : α)
    ((of : (a : m → n → α) → Matrix m n α)
        (Pi.single (M := fun (a : m) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j a_1)) a b :
      α)

Tactic:
simp [*]
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Zero α
i : m
j : n
a : α
⊢ Eq (α := m → n → α) ((Equiv.symm of : (a : Matrix m n α) → m → n → α) (single i j a) : m → n → α)
    (Pi.single (M := fun (j : m) ↦ n → α) i (Pi.single (M := fun (j : n) ↦ α) j a) : (j : m) → n → α)

Tactic:
congr_arg of.symm <| single_eq_of_single_single i j a

Premises used: Function.update, Matrix.of, Pi.single, dite, congr_arg, Matrix.single_eq_of_single_single, Equiv.symm, DFunLike.coe
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Zero α
inst_3 : SMulZeroClass R α
r : R
i : m
j : n
a : α
unfold :
  HSMul.hSMul (β := Matrix m n α) r
      ((of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a else 0) =
    (of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then r • a else 0
⊢ r • single i j a = single i j (r • a)

Tactic:
unfold single

Premises used: Matrix.single
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Zero α
inst_3 : SMulZeroClass R α
r : R
i : m
j : n
a : α
a₁ :
  ∀ (i_1 : m) (j_1 : n),
    HSMul.hSMul (β := Matrix m n α) r
        ((of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a else 0) i_1 j_1 =
      (of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then r • a else 0) i_1 j_1
⊢ HSMul.hSMul (β := Matrix m n α) r
      ((of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a else 0) =
    (of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then r • a else 0

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Zero α
inst_3 : SMulZeroClass R α
r : R
i : m
j : n
a : α
i_1 : m
j_1 : n
⊢ HSMul.hSMul (β := Matrix m n α) r
      ((of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a else 0) i_1 j_1 =
    (of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then r • a else 0) i_1 j_1

Tactic:
simp [smul_ite]

Premises used: smul_ite
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Zero α
i : m
j : n
a :
  ∀ (i_1 : m) (j_1 : n),
    Eq.{u_7 + 1} (α := α)
      ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then 0 else 0) i_1 j_1 : α)
      (0 i_1 j_1 : α)
⊢ Eq (α := Matrix m n α)
    ((of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then 0 else 0) 0

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Zero α
i : m
j : n
i_1 : m
j_1 : n
⊢ Eq.{u_7 + 1} (α := α)
    ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then 0 else 0) i_1 j_1 : α)
    (0 i_1 j_1 : α)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Zero α
i : m
j : n
a : α
⊢ (single i j a)ᵀ = single j i a

Tactic:
aesop (add unsafe unfold single)

Premises used: Matrix.single
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Zero α
i : m
j : n
a : α
β : Type u_10
inst_3 : Zero β
F : Type u_11
inst_4 : FunLike F α β
inst_5 : ZeroHomClass F α β
f : F
⊢ Eq (α := Matrix m n β) ((single i j a).map (⇑f : (a : α) → β) : Matrix m n β)
    (single i j ((f : (a : α) → β) a) : Matrix m n β)

Tactic:
aesop (add unsafe unfold single)

Premises used: Matrix.single
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Zero α
S : Set α
hS : 0 ∈ S
i : m
j : n
a : α
simp : (∀ (i_1 : m) (j_1 : n), (if i = i_1 ∧ j = j_1 then a else 0) ∈ S) ↔ a ∈ S
⊢ Membership.mem (γ := Set (Matrix m n α)) S.matrix (single i j a) ↔ a ∈ S

Tactic:
simp only [Set.mem_matrix, single, of_apply]

Premises used: Set.mem_matrix, Matrix.of_apply, Matrix.single
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Zero α
S : Set α
hS : 0 ∈ S
i : m
j : n
a : α
i_1 : m
j_1 : n
rw : (i = i_1 ∧ j = j_1 → a ∈ S) ∧ (¬(i = i_1 ∧ j = j_1) → 0 ∈ S)
| (if i = i_1 ∧ j = j_1 then a else 0) ∈ S

Tactic:
rw [ite_mem]

Premises used: ite_mem
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Zero α
S : Set α
hS : 0 ∈ S
i : m
j : n
a : α
conv_lhs : (∀ (i_1 : m) (j_1 : n), (i = i_1 ∧ j = j_1 → a ∈ S) ∧ (¬(i = i_1 ∧ j = j_1) → 0 ∈ S)) ↔ a ∈ S
⊢ (∀ (i_1 : m) (j_1 : n), (if i = i_1 ∧ j = j_1 then a else 0) ∈ S) ↔ a ∈ S

Tactic:
conv_lhs => intro _ _; rw [ite_mem]

Premises used: ite_mem
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Zero α
S : Set α
hS : 0 ∈ S
i : m
j : n
a : α
⊢ (∀ (i_1 : m) (j_1 : n), (i = i_1 ∧ j = j_1 → a ∈ S) ∧ (¬(i = i_1 ∧ j = j_1) → 0 ∈ S)) ↔ a ∈ S

Tactic:
simp [hS]
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
α : Type u_7
inst : DecidableEq m
inst_1 : Zero α
i : m
r : α
a : ∀ (j k : m), diagonal (Pi.single (M := fun (a : m) ↦ α) i r) j k = single i i r j k
⊢ diagonal (Pi.single (M := fun (a : m) ↦ α) i r) = single i i r

Tactic:
ext j k
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
α : Type u_7
inst : DecidableEq m
inst_1 : Zero α
i : m
r : α
j k : m
a : (if j = k then Pi.single (M := fun (a : m) ↦ α) i r j else 0) = if i = j ∧ i = k then r else 0
⊢ diagonal (Pi.single (M := fun (a : m) ↦ α) i r) j k = single i i r j k

Tactic:
dsimp [diagonal, single]

Premises used: Matrix.diagonal, Matrix.single
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
α : Type u_7
inst : DecidableEq m
inst_1 : Zero α
i : m
r : α
j k : m
⊢ (if j = k then Pi.single (M := fun (a : m) ↦ α) i r j else 0) = if i = j ∧ i = k then r else 0

Tactic:
grind
-- 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 : Zero α
f : l ≃ n
g : m ≃ o
i : n
j : o
r : α
a :
  ∀ (i' : l) (j' : m),
    (single i j r).submatrix (⇑f : (a : l) → n) (⇑g : (a : m) → o) i' j' =
      single ((f.symm : (a : n) → l) i) ((g.symm : (a : o) → m) j) r i' j'
⊢ Eq (α := Matrix l m α) ((single i j r).submatrix (⇑f : (a : l) → n) (⇑g : (a : m) → o) : Matrix l m α)
    (single ((f.symm : (a : n) → l) i) ((g.symm : (a : o) → m) j) r : Matrix l m α)

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 : Zero α
f : l ≃ n
g : m ≃ o
i : n
j : o
r : α
i' : l
j' : m
a :
  single i j r ((f : (a : l) → n) i') ((g : (a : m) → o) j') =
    single ((f.symm : (a : n) → l) i) ((g.symm : (a : o) → m) j) r i' j'
⊢ (single i j r).submatrix (⇑f : (a : l) → n) (⇑g : (a : m) → o) i' j' =
    single ((f.symm : (a : n) → l) i) ((g.symm : (a : o) → m) j) r i' j'

Tactic:
dsimp
-- 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 : Zero α
f : l ≃ n
g : m ≃ o
i : n
j : o
r : α
i' : l
j' : m
a :
  ∀ (hi : (f.symm : (a : n) → l) i ≠ i'),
    single i j r ((f : (a : l) → n) i') ((g : (a : m) → o) j') =
      single ((f.symm : (a : n) → l) i) ((g.symm : (a : o) → m) j) r i' j'
a₁ :
  single i j r ((f : (a : l) → n) ((f.symm : (a : n) → l) i : l)) ((g : (a : m) → o) j') =
    single.{u_1, u_2, u_7} (m := l) ((f.symm : (a : n) → l) i : l) ((g.symm : (a : o) → m) j) r
      ((f.symm : (a : n) → l) i : l) j'
⊢ single i j r ((f : (a : l) → n) i') ((g : (a : m) → o) j') =
    single ((f.symm : (a : n) → l) i) ((g.symm : (a : o) → m) j) r i' j'

Tactic:
obtain hi | rfl := ne_or_eq (f.symm i) i'

Premises used: ne_or_eq, Equiv.symm, DFunLike.coe, rfl
-- 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 : Zero α
f : l ≃ n
g : m ≃ o
i : n
j : o
r : α
i' : l
j' : m
hi : (f.symm : (a : n) → l) i ≠ i'
a : i ≠ (f : (a : l) → n) i'
⊢ single i j r ((f : (a : l) → n) i') ((g : (a : m) → o) j') =
    single ((f.symm : (a : n) → l) i) ((g.symm : (a : o) → m) j) r i' j'

Tactic:
rw [single_apply_of_row_ne hi, single_apply_of_row_ne]

Premises used: Matrix.single_apply_of_row_ne
-- 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 : Zero α
f : l ≃ n
g : m ≃ o
i : n
j : o
r : α
i' : l
j' : m
hi : (f.symm : (a : n) → l) i ≠ i'
⊢ i ≠ (f : (a : l) → n) i'

Tactic:
f.symm_apply_eq.not.1 hi

Premises used: Equiv.symm_apply_eq, Iff.not, Iff.mp
-- 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 : Zero α
f : l ≃ n
g : m ≃ o
i : n
j : o
r : α
i' : l
j' : m
hi : (f.symm : (a : n) → l) i ≠ i'
⊢ i ≠ (f : (a : l) → n) i'

Tactic:
exact f.symm_apply_eq.not.1 hi

Premises used: Equiv.symm_apply_eq, Iff.not, Iff.mp
-- 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 : Zero α
f : l ≃ n
g : m ≃ o
i : n
j : o
r : α
j' : m
a :
  ∀ (hj : (g.symm : (a : o) → m) j ≠ j'),
    single i j r ((f : (a : l) → n) ((f.symm : (a : n) → l) i : l)) ((g : (a : m) → o) j') =
      single.{u_1, u_2, u_7} (m := l) ((f.symm : (a : n) → l) i : l) ((g.symm : (a : o) → m) j) r
        ((f.symm : (a : n) → l) i : l) j'
a₁ :
  single i j r ((f : (a : l) → n) ((f.symm : (a : n) → l) i : l)) ((g : (a : m) → o) ((g.symm : (a : o) → m) j : m)) =
    single.{u_1, u_2, u_7} (m := l) (n := m) ((f.symm : (a : n) → l) i : l) ((g.symm : (a : o) → m) j : m) r
      ((f.symm : (a : n) → l) i : l) ((g.symm : (a : o) → m) j : m)
⊢ single i j r ((f : (a : l) → n) ((f.symm : (a : n) → l) i : l)) ((g : (a : m) → o) j') =
    single.{u_1, u_2, u_7} (m := l) ((f.symm : (a : n) → l) i : l) ((g.symm : (a : o) → m) j) r
      ((f.symm : (a : n) → l) i : l) j'

Tactic:
obtain hj | rfl := ne_or_eq (g.symm j) j'

Premises used: ne_or_eq, Equiv.symm, DFunLike.coe, rfl
-- 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 : Zero α
f : l ≃ n
g : m ≃ o
i : n
j : o
r : α
j' : m
hj : (g.symm : (a : o) → m) j ≠ j'
a : j ≠ (g : (a : m) → o) j'
⊢ single i j r ((f : (a : l) → n) ((f.symm : (a : n) → l) i : l)) ((g : (a : m) → o) j') =
    single.{u_1, u_2, u_7} (m := l) ((f.symm : (a : n) → l) i : l) ((g.symm : (a : o) → m) j) r
      ((f.symm : (a : n) → l) i : l) j'

Tactic:
rw [single_apply_of_col_ne _ _ hj, single_apply_of_col_ne]

Premises used: Matrix.single_apply_of_col_ne
-- 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 : Zero α
f : l ≃ n
g : m ≃ o
i : n
j : o
r : α
j' : m
hj : (g.symm : (a : o) → m) j ≠ j'
⊢ j ≠ (g : (a : m) → o) j'

Tactic:
g.symm_apply_eq.not.1 hj

Premises used: Equiv.symm_apply_eq, Iff.not, Iff.mp
-- 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 : Zero α
f : l ≃ n
g : m ≃ o
i : n
j : o
r : α
j' : m
hj : (g.symm : (a : o) → m) j ≠ j'
⊢ j ≠ (g : (a : m) → o) j'

Tactic:
exact g.symm_apply_eq.not.1 hj

Premises used: Equiv.symm_apply_eq, Iff.not, Iff.mp
-- 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 : Zero α
f : l ≃ n
g : m ≃ o
i : n
j : o
r : α
⊢ single i j r ((f : (a : l) → n) ((f.symm : (a : n) → l) i : l)) ((g : (a : m) → o) ((g.symm : (a : o) → m) j : m)) =
    single.{u_1, u_2, u_7} (m := l) (n := m) ((f.symm : (a : n) → l) i : l) ((g.symm : (a : o) → m) j : m) r
      ((f.symm : (a : n) → l) i : l) ((g.symm : (a : o) → m) j : m)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : AddZeroClass α
i : m
j : n
a b : α
a₁ : ∀ (i_1 : m) (j_1 : n), single i j (a + b) i_1 j_1 = (single i j a + single i j b) i_1 j_1
⊢ single i j (a + b) = single i j a + single i j b

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : AddZeroClass α
i : m
j : n
a b : α
i_1 : m
j_1 : n
a₁ :
  (if i = i_1 ∧ j = j_1 then a + b else 0) =
    HAdd.hAdd (α := Matrix m n α) (β := Matrix m n α)
      ((of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a else 0)
      ((of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then b else 0) i_1 j_1
⊢ single i j (a + b) i_1 j_1 = (single i j a + single i j b) i_1 j_1

Tactic:
simp only [single, of_apply]

Premises used: Matrix.of_apply, Matrix.single
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : AddZeroClass α
i : m
j : n
a b : α
i_1 : m
j_1 : n
pos :
  ∀ (h : i = i_1 ∧ j = j_1),
    a + b =
      HAdd.hAdd (α := Matrix m n α) (β := Matrix m n α)
        ((of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a else 0)
        ((of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then b else 0) i_1 j_1
neg :
  ∀ (h : ¬(i = i_1 ∧ j = j_1)),
    0 =
      HAdd.hAdd (α := Matrix m n α) (β := Matrix m n α)
        ((of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a else 0)
        ((of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then b else 0) i_1 j_1
⊢ (if i = i_1 ∧ j = j_1 then a + b else 0) =
    HAdd.hAdd (α := Matrix m n α) (β := Matrix m n α)
      ((of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a else 0)
      ((of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then b else 0) i_1 j_1

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : AddZeroClass α
i : m
j : n
a b : α
i_1 : m
j_1 : n
h : i = i_1 ∧ j = j_1
⊢ a + b =
    HAdd.hAdd (α := Matrix m n α) (β := Matrix m n α)
      ((of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a else 0)
      ((of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then b else 0) i_1 j_1

Tactic:
simp [h]
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : AddZeroClass α
i : m
j : n
a b : α
i_1 : m
j_1 : n
h : ¬(i = i_1 ∧ j = j_1)
⊢ 0 =
    HAdd.hAdd (α := Matrix m n α) (β := Matrix m n α)
      ((of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a else 0)
      ((of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then b else 0) i_1 j_1

Tactic:
simp [h]
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : NonUnitalNonAssocSemiring α
inst_3 : Fintype m
i : n
j : m
c : α
x : m → α
h : ∀ (i' : n), (single i j c *ᵥ x) i' = Function.update (β := fun (a : n) ↦ α) 0 i (c * x j) i'
⊢ single i j c *ᵥ x = Function.update (β := fun (a : n) ↦ α) 0 i (c * x j)

Tactic:
ext i'
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : NonUnitalNonAssocSemiring α
inst_3 : Fintype m
i : n
j : m
c : α
x : m → α
i' : n
h :
  Eq.{u_7 + 1} (α := α) (∑ x_1 : m, if i = i' ∧ j = x_1 then c * x x_1 else 0 : α)
    (Function.update (β := fun (a : n) ↦ α) 0 i (c * x j) i' : α)
⊢ (single i j c *ᵥ x) i' = Function.update (β := fun (a : n) ↦ α) 0 i (c * x j) i'

Tactic:
simp only [mulVec, dotProduct, single, of_apply, ite_mul, zero_mul]

Premises used: dotProduct, MulZeroClass.zero_mul, Matrix.of_apply, ite_mul, Matrix.mulVec, Matrix.single
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : NonUnitalNonAssocSemiring α
inst_3 : Fintype m
i : n
j : m
c : α
x : m → α
i' : n
h :
  Eq.{u_7 + 1} (α := α) (∑ x_1 : m, if i = i ∧ j = x_1 then c * x x_1 else 0 : α)
    (Function.update (β := fun (a : n) ↦ α) 0 i (c * x j) i : α)
h₁ :
  ∀ (h : i ≠ i'),
    Eq.{u_7 + 1} (α := α) (∑ x_1 : m, if i = i' ∧ j = x_1 then c * x x_1 else 0 : α)
      (Function.update (β := fun (a : n) ↦ α) 0 i (c * x j) i' : α)
⊢ Eq.{u_7 + 1} (α := α) (∑ x_1 : m, if i = i' ∧ j = x_1 then c * x x_1 else 0 : α)
    (Function.update (β := fun (a : n) ↦ α) 0 i (c * x j) i' : α)

Tactic:
rcases eq_or_ne i i' with rfl | h

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : NonUnitalNonAssocSemiring α
inst_3 : Fintype m
i : n
j : m
c : α
x : m → α
⊢ Eq.{u_7 + 1} (α := α) (∑ x_1 : m, if i = i ∧ j = x_1 then c * x x_1 else 0 : α)
    (Function.update (β := fun (a : n) ↦ α) 0 i (c * x j) i : α)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : NonUnitalNonAssocSemiring α
inst_3 : Fintype m
i : n
j : m
c : α
x : m → α
i' : n
h : i ≠ i'
⊢ Eq.{u_7 + 1} (α := α) (∑ x_1 : m, if i = i' ∧ j = x_1 then c * x x_1 else 0 : α)
    (Function.update (β := fun (a : n) ↦ α) 0 i (c * x j) i' : α)

Tactic:
simp [h, h.symm]

Premises used: Ne.symm
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
α : Type u_7
inst : DecidableEq m
inst_1 : AddCommMonoid α
inst_2 : Fintype m
f : m → α
a : ∀ (j k : m), (∑ i : m, single i i (f i)) j k = diagonal f j k
⊢ ∑ i : m, single i i (f i) = diagonal f

Tactic:
ext j k
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
α : Type u_7
inst : DecidableEq m
inst_1 : AddCommMonoid α
inst_2 : Fintype m
f : m → α
j k : m
a : single j j (f j) j k = if j = k then f j else 0
a₁ : ∀ (b : m), Membership.mem (γ := Finset m) Finset.univ b → b ≠ j → single b b (f b) j k = 0
a₂ : j ∉ Finset.univ → single j j (f j) j k = 0
⊢ (∑ i : m, single i i (f i)) j k = diagonal f j k

Tactic:
rw [sum_apply, diagonal_apply, Finset.sum_eq_single j]

Premises used: Matrix.sum_apply, Finset.sum_eq_single, Matrix.diagonal_apply
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
α : Type u_7
inst : DecidableEq m
inst_1 : AddCommMonoid α
inst_2 : Fintype m
f : m → α
j k : m
⊢ single j j (f j) j k = if j = k then f j else 0

Tactic:
simp +contextual [single]

Premises used: Matrix.single
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
α : Type u_7
inst : DecidableEq m
inst_1 : AddCommMonoid α
inst_2 : Fintype m
f : m → α
j k : m
⊢ ∀ (b : m), Membership.mem (γ := Finset m) Finset.univ b → b ≠ j → single b b (f b) j k = 0

Tactic:
simp +contextual [single]

Premises used: Matrix.single
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
α : Type u_7
inst : DecidableEq m
inst_1 : AddCommMonoid α
inst_2 : Fintype m
f : m → α
j k : m
⊢ j ∉ Finset.univ → single j j (f j) j k = 0

Tactic:
simp +contextual [single]

Premises used: Matrix.single
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
α : Type u_7
inst : DecidableEq m
inst_1 : AddCommMonoid α
inst_2 : One α
inst_3 : Fintype m
⊢ Eq (α := Matrix m m α) (∑ i : m, single i i 1) 1

Tactic:
sum_single_eq_diagonal _

Premises used: Matrix.sum_single_eq_diagonal
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
α : Type u_7
inst : DecidableEq m
inst_1 : AddCommMonoidWithOne α
inst_2 : Fintype m
n : ℕ
⊢ Eq (α := Matrix m m α) (∑ i : m, single i i (↑n : α)) (↑n : Matrix m m α)

Tactic:
sum_single_eq_diagonal _

Premises used: Matrix.sum_single_eq_diagonal