awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
α : Type u_7
inst : DecidableEq m
inst_1 : AddCommMonoidWithOne α
inst_2 : Fintype m
n : ℕ
inst_3 : n.AtLeastTwo
⊢ Eq (α := Matrix m m α) (∑ i : m, single i i (OfNat.ofNat n)) (OfNat.ofNat n)

Tactic:
sum_single_eq_diagonal _

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

Tactic:
sum_single_eq_diagonal _

Premises used: Matrix.sum_single_eq_diagonal
-- 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 : AddCommMonoid α
inst_3 : Fintype m
inst_4 : Fintype n
x : m → n → α
a :
  ∀ (i : m) (j : n),
    Eq.{u_7 + 1} (α := α) ((∑ i : m, ∑ j : n, single i j (x i j)) i j : α)
      ((of : (a : m → n → α) → Matrix m n α) x i j : α)
⊢ Eq (α := Matrix m n α) (∑ i : m, ∑ j : n, single i j (x i j) : Matrix m n α)
    ((of : (a : m → n → α) → Matrix m n α) x : Matrix m n α)

Tactic:
ext i j
-- 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 : AddCommMonoid α
inst_3 : Fintype m
inst_4 : Fintype n
x : m → n → α
i : m
j : n
a :
  Eq.{u_7 + 1} (α := α) ((∑ x_1 : m × n, single x_1.1 x_1.2 (x x_1.1 x_1.2)) i j : α)
    ((of : (a : m → n → α) → Matrix m n α) x i j : α)
⊢ Eq.{u_7 + 1} (α := α) ((∑ i : m, ∑ j : n, single i j (x i j)) i j : α)
    ((of : (a : m → n → α) → Matrix m n α) x i j : α)

Tactic:
rw [← Fintype.sum_prod_type']

Premises used: Fintype.sum_prod_type'
-- 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 : AddCommMonoid α
inst_3 : Fintype m
inst_4 : Fintype n
x : m → n → α
i : m
j : n
⊢ Eq.{u_7 + 1} (α := α) ((∑ x_1 : m × n, single x_1.1 x_1.2 (x x_1.1 x_1.2)) i j : α)
    ((of : (a : m → n → α) → Matrix m n α) x i j : α)

Tactic:
simp [single, Matrix.sum_apply, Matrix.of_apply, ← Prod.mk_inj]

Premises used: Matrix.sum_apply, Prod.mk_inj, 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 : AddCommMonoid α
inst_3 : Fintype m
inst_4 : Fintype n
x : Matrix m n α
⊢ x = ∑ i : m, ∑ j : n, single i j (x i j)

Tactic:
sum_sum_single _ |>.symm

Premises used: Matrix.sum_sum_single, Eq.symm
-- 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 : MulZeroOneClass α
i : m
j : n
⊢ Eq (α := Matrix m n α) (single i j 1)
    (vecMulVec (Pi.single (M := fun (a : m) ↦ α) i 1) (Pi.single (M := fun (a : n) ↦ α) j 1))

Tactic:
simp [-mul_ite, single, vecMulVec, ite_and, Pi.single_apply, eq_comm]

Premises used: Pi.single_apply, mul_ite, eq_comm, ite_and, Matrix.vecMulVec, 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 : AddCommMonoid α
inst_3 : Finite m
inst_4 : Finite n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)
intro : ∀ (val : Fintype m), P M
⊢ P M

Tactic:
cases nonempty_fintype m

Premises used: nonempty_fintype
-- 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 : AddCommMonoid α
inst_3 : Finite m
inst_4 : Finite n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)
val : Fintype m
intro : ∀ (val : Fintype n), P M
⊢ P M

Tactic:
cases nonempty_fintype n

Premises used: nonempty_fintype
-- 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 : AddCommMonoid α
inst_3 : Finite m
inst_4 : Finite n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)
val : Fintype m
val_1 : Fintype n
intro : P (∑ x ∈ SProd.sprod (α := Finset m) (β := Finset n) Finset.univ Finset.univ, single x.1 x.2 (M x.1 x.2))
⊢ P M

Tactic:
rw [matrix_eq_sum_single M, ← Finset.sum_product']

Premises used: Matrix.matrix_eq_sum_single, Finset.sum_product'
-- 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 : AddCommMonoid α
inst_3 : Finite m
inst_4 : Finite n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)
val : Fintype m
val_1 : Fintype n
intro : ∀ x ∈ SProd.sprod (α := Finset m) (β := Finset n) Finset.univ Finset.univ, P (single x.1 x.2 (M x.1 x.2))
⊢ P (∑ x ∈ SProd.sprod (α := Finset m) (β := Finset n) Finset.univ Finset.univ, single x.1 x.2 (M x.1 x.2))

Tactic:
apply Finset.sum_induction _ _ h_add h_zero

Premises used: Finset.sum_induction
-- 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 : AddCommMonoid α
inst_3 : Finite m
inst_4 : Finite n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)
val : Fintype m
val_1 : Fintype n
x : m × n
h : x ∈ SProd.sprod (α := Finset m) (β := Finset n) Finset.univ Finset.univ
⊢ P (single x.1 x.2 (M x.1 x.2))

Tactic:
apply h_std_basis
-- 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 : AddCommMonoid α
inst_3 : Finite m
inst_4 : Finite n
inst_5 : Nonempty m
inst_6 : Nonempty n
P : Matrix m n α → Prop
M : Matrix m n α
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)
inhabit : ∀ (inhabited_h : Inhabited m), P 0
⊢ P 0

Tactic:
inhabit m
-- 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 : AddCommMonoid α
inst_3 : Finite m
inst_4 : Finite n
inst_5 : Nonempty m
inst_6 : Nonempty n
P : Matrix m n α → Prop
M : Matrix m n α
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)
inhabited_h : Inhabited m
inhabit : ∀ (inhabited_h : Inhabited n), P 0
⊢ P 0

Tactic:
inhabit n
-- 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 : AddCommMonoid α
inst_3 : Finite m
inst_4 : Finite n
inst_5 : Nonempty m
inst_6 : Nonempty n
P : Matrix m n α → Prop
M : Matrix m n α
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)
inhabited_h_1 : Inhabited m
inhabited_h : Inhabited n
⊢ P 0

Tactic:
simpa using h_std_basis default default 0

Premises used: Inhabited.default, OfNat.ofNat
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
β : Type u_8
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Finite m
inst_3 : Finite n
inst_4 : AddCommMonoid α
inst_5 : AddCommMonoid β
f g : Matrix m n α →+ β
h : ∀ (i : m) (j : n), f.comp (singleAddMonoidHom i j) = g.comp (singleAddMonoidHom i j)
intro : ∀ (val : Fintype m), f = g
⊢ f = g

Tactic:
cases nonempty_fintype m

Premises used: nonempty_fintype
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
β : Type u_8
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Finite m
inst_3 : Finite n
inst_4 : AddCommMonoid α
inst_5 : AddCommMonoid β
f g : Matrix m n α →+ β
h : ∀ (i : m) (j : n), f.comp (singleAddMonoidHom i j) = g.comp (singleAddMonoidHom i j)
val : Fintype m
intro : ∀ (val : Fintype n), f = g
⊢ f = g

Tactic:
cases nonempty_fintype n

Premises used: nonempty_fintype
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
β : Type u_8
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Finite m
inst_3 : Finite n
inst_4 : AddCommMonoid α
inst_5 : AddCommMonoid β
f g : Matrix m n α →+ β
h : ∀ (i : m) (j : n), f.comp (singleAddMonoidHom i j) = g.comp (singleAddMonoidHom i j)
val : Fintype m
val_1 : Fintype n
intro :
  ∀ (x : Matrix m n α), Eq.{u_8 + 1} (α := β) ((f : (a : Matrix m n α) → β) x : β) ((g : (a : Matrix m n α) → β) x : β)
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
β : Type u_8
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Finite m
inst_3 : Finite n
inst_4 : AddCommMonoid α
inst_5 : AddCommMonoid β
f g : Matrix m n α →+ β
h : ∀ (i : m) (j : n), f.comp (singleAddMonoidHom i j) = g.comp (singleAddMonoidHom i j)
val : Fintype m
val_1 : Fintype n
x : Matrix m n α
intro :
  Eq.{u_8 + 1} (α := β) ((f : (a : Matrix m n α) → β) (∑ i : m, ∑ j : n, single i j (x i j)) : β)
    ((g : (a : Matrix m n α) → β) (∑ i : m, ∑ j : n, single i j (x i j)) : β)
⊢ Eq.{u_8 + 1} (α := β) ((f : (a : Matrix m n α) → β) x : β) ((g : (a : Matrix m n α) → β) x : β)

Tactic:
rw [matrix_eq_sum_single x]

Premises used: Matrix.matrix_eq_sum_single
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
β : Type u_8
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Finite m
inst_3 : Finite n
inst_4 : AddCommMonoid α
inst_5 : AddCommMonoid β
f g : Matrix m n α →+ β
h : ∀ (i : m) (j : n), f.comp (singleAddMonoidHom i j) = g.comp (singleAddMonoidHom i j)
val : Fintype m
val_1 : Fintype n
x : Matrix m n α
intro :
  Eq.{u_8 + 1} (α := β) (∑ x_1 : m, ∑ x_2 : n, (f : (a : Matrix m n α) → β) (single x_1 x_2 (x x_1 x_2)))
    (∑ x_1 : m, ∑ x_2 : n, (g : (a : Matrix m n α) → β) (single x_1 x_2 (x x_1 x_2)))
⊢ Eq.{u_8 + 1} (α := β) ((f : (a : Matrix m n α) → β) (∑ i : m, ∑ j : n, single i j (x i j)) : β)
    ((g : (a : Matrix m n α) → β) (∑ i : m, ∑ j : n, single i j (x i j)) : β)

Tactic:
simp_rw [map_sum]

Premises used: map_sum
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
β : Type u_8
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Finite m
inst_3 : Finite n
inst_4 : AddCommMonoid α
inst_5 : AddCommMonoid β
f g : Matrix m n α →+ β
h : ∀ (i : m) (j : n), f.comp (singleAddMonoidHom i j) = g.comp (singleAddMonoidHom i j)
val : Fintype m
val_1 : Fintype n
x : Matrix m n α
intro :
  ∀ (x_1 : m),
    Membership.mem (γ := Finset m) Finset.univ x_1 →
      ∀ (x_2 : n),
        Membership.mem (γ := Finset n) Finset.univ x_2 →
          Eq.{u_8 + 1} (α := β) ((f : (a : Matrix m n α) → β) (single x_1 x_2 (x x_1 x_2)) : β)
            ((g : (a : Matrix m n α) → β) (single x_1 x_2 (x x_1 x_2)) : β)
⊢ Eq.{u_8 + 1} (α := β) (∑ x_1 : m, ∑ x_2 : n, (f : (a : Matrix m n α) → β) (single x_1 x_2 (x x_1 x_2)))
    (∑ x_1 : m, ∑ x_2 : n, (g : (a : Matrix m n α) → β) (single x_1 x_2 (x x_1 x_2)))

Tactic:
congr! 2
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
β : Type u_8
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Finite m
inst_3 : Finite n
inst_4 : AddCommMonoid α
inst_5 : AddCommMonoid β
f g : Matrix m n α →+ β
h : ∀ (i : m) (j : n), f.comp (singleAddMonoidHom i j) = g.comp (singleAddMonoidHom i j)
val : Fintype m
val_1 : Fintype n
x : Matrix m n α
x_1 : m
h_1 : Membership.mem (γ := Finset m) Finset.univ x_1
x_2 : n
h_2 : Membership.mem (γ := Finset n) Finset.univ x_2
⊢ Eq.{u_8 + 1} (α := β) ((f : (a : Matrix m n α) → β) (single x_1 x_2 (x x_1 x_2)) : β)
    ((g : (a : Matrix m n α) → β) (single x_1 x_2 (x x_1 x_2)) : β)

Tactic:
DFunLike.congr_fun (h _ _) _

Premises used: DFunLike.congr_fun, Matrix.single
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
β : Type u_8
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Finite m
inst_3 : Finite n
inst_4 : AddCommMonoid α
inst_5 : AddCommMonoid β
f g : Matrix m n α →+ β
h : ∀ (i : m) (j : n), f.comp (singleAddMonoidHom i j) = g.comp (singleAddMonoidHom i j)
val : Fintype m
val_1 : Fintype n
x : Matrix m n α
x_1 : m
h_1 : Membership.mem (γ := Finset m) Finset.univ x_1
x_2 : n
h_2 : Membership.mem (γ := Finset n) Finset.univ x_2
⊢ Eq.{u_8 + 1} (α := β) ((f : (a : Matrix m n α) → β) (single x_1 x_2 (x x_1 x_2)) : β)
    ((g : (a : Matrix m n α) → β) (single x_1 x_2 (x x_1 x_2)) : β)

Tactic:
exact DFunLike.congr_fun (h _ _) _

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
α : Type u_7
β : Type u_8
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Finite m
inst_3 : Finite n
inst_4 : Semiring R
inst_5 : AddCommMonoid α
inst_6 : AddCommMonoid β
inst_7 : Module R α
inst_8 : Module R β
f g : Matrix m n α →ₗ[R] β
h : ∀ (i : m) (j : n), f ∘ₗ singleLinearMap R i j = g ∘ₗ singleLinearMap R i j
⊢ f = g

Tactic:
LinearMap.toAddMonoidHom_injective <| ext_addMonoidHom fun i j =>
    congrArg LinearMap.toAddMonoidHom <| h i j

Premises used: LinearMap.toAddMonoidHom, congrArg, LinearMap.toAddMonoidHom_injective, Matrix.ext_addMonoidHom
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
S : Type u_6
α : Type u_7
β : Type u_8
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : Fintype n
inst_4 : Semiring R
inst_5 : Semiring S
inst_6 : AddCommMonoid α
inst_7 : AddCommMonoid β
inst_8 : Module R α
inst_9 : Module R β
inst_10 : Module S β
inst_11 : SMulCommClass R S β
f : m → n → α →ₗ[R] β
M : Matrix m n α
⊢ Eq.{u_8 + 1} (α := β)
    ((((liftLinear S : (a : m → n → α →ₗ[R] β) → Matrix m n α →ₗ[R] β) f : Matrix m n α →ₗ[R] β) :
          (a : Matrix m n α) → β)
        M :
      β)
    (∑ i : m, ∑ j : n, (f i j : (a : α) → β) (M i j) : β)

Tactic:
simp [liftLinear, map_sum, LinearEquiv.congrLeft]

Premises used: Matrix.liftLinear, map_sum, LinearEquiv.congrLeft
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
S : Type u_6
α : Type u_7
β : Type u_8
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : Fintype n
inst_4 : Semiring R
inst_5 : Semiring S
inst_6 : AddCommMonoid α
inst_7 : AddCommMonoid β
inst_8 : Module R α
inst_9 : Module R β
inst_10 : Module S β
inst_11 : SMulCommClass R S β
f : m → n → α →ₗ[R] β
i : m
j : n
a : α
dsimp :
  Eq.{u_8 + 1} (α := β)
    (((LinearMap.lsum R (fun (i : m) ↦ (i : n) → α) S :
              (a : (i : m) → ((i : n) → α) →ₗ[R] β) → ((i : m) → (i : n) → α) →ₗ[R] β)
            fun (i : m) ↦ (LinearMap.lsum R (fun (a : n) ↦ α) S : (a : n → α →ₗ[R] β) → ((i : n) → α) →ₗ[R] β) (f i) :
          (a : (i : m) → (i : n) → α) → β)
        ((Equiv.symm of : (a : Matrix m n α) → m → n → α) (single i j a) : m → n → α) :
      β)
    ((f i j : (a : α) → β) a : β)
⊢ Eq.{u_8 + 1} (α := β)
    ((((liftLinear S : (a : m → n → α →ₗ[R] β) → Matrix m n α →ₗ[R] β) f : Matrix m n α →ₗ[R] β) :
          (a : Matrix m n α) → β)
        (single i j a) :
      β)
    ((f i j : (a : α) → β) a : β)

Tactic:
dsimp [liftLinear, -LinearMap.lsum_apply, LinearEquiv.congrLeft, LinearEquiv.piCongrRight]

Premises used: LinearMap.lsum_apply, Matrix.liftLinear, LinearEquiv.piCongrRight, LinearEquiv.congrLeft
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
S : Type u_6
α : Type u_7
β : Type u_8
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : Fintype n
inst_4 : Semiring R
inst_5 : Semiring S
inst_6 : AddCommMonoid α
inst_7 : AddCommMonoid β
inst_8 : Module R α
inst_9 : Module R β
inst_10 : Module S β
inst_11 : SMulCommClass R S β
f : m → n → α →ₗ[R] β
i : m
j : n
a : α
simp_rw :
  Eq.{u_8 + 1} (α := β)
    (((LinearMap.lsum R (fun (i : m) ↦ (i : n) → α) S :
              (a : (i : m) → ((i : n) → α) →ₗ[R] β) → ((i : m) → (i : n) → α) →ₗ[R] β)
            fun (i : m) ↦ (LinearMap.lsum R (fun (a : n) ↦ α) S : (a : n → α →ₗ[R] β) → ((i : n) → α) →ₗ[R] β) (f i) :
          (a : (i : m) → (i : n) → α) → β)
        (Pi.single (M := fun (j : m) ↦ n → α) i (Pi.single (M := fun (j : n) ↦ α) j a)) :
      β)
    ((f i j : (a : α) → β) a : β)
⊢ Eq.{u_8 + 1} (α := β)
    (((LinearMap.lsum R (fun (i : m) ↦ (i : n) → α) S :
              (a : (i : m) → ((i : n) → α) →ₗ[R] β) → ((i : m) → (i : n) → α) →ₗ[R] β)
            fun (i : m) ↦ (LinearMap.lsum R (fun (a : n) ↦ α) S : (a : n → α →ₗ[R] β) → ((i : n) → α) →ₗ[R] β) (f i) :
          (a : (i : m) → (i : n) → α) → β)
        ((Equiv.symm of : (a : Matrix m n α) → m → n → α) (single i j a) : m → n → α) :
      β)
    ((f i j : (a : α) → β) a : β)

Tactic:
simp_rw [of_symm_single, LinearMap.lsum_piSingle]

Premises used: Matrix.of_symm_single, LinearMap.lsum_piSingle
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
S : Type u_6
α : Type u_7
β : Type u_8
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : Fintype n
inst_4 : Semiring R
inst_5 : Semiring S
inst_6 : AddCommMonoid α
inst_7 : AddCommMonoid β
inst_8 : Module R α
inst_9 : Module R β
inst_10 : Module S β
inst_11 : SMulCommClass R S β
f : m → n → α →ₗ[R] β
i : m
j : n
⊢ (liftLinear S : (a : m → n → α →ₗ[R] β) → Matrix m n α →ₗ[R] β) f ∘ₗ singleLinearMap R i j = f i j

Tactic:
LinearMap.ext <| liftLinear_single S f i j

Premises used: Matrix.liftLinear_single, LinearMap.ext
-- Module: Mathlib.Data.Matrix.Basis
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
S : Type u_6
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : Fintype n
inst_4 : Semiring R
inst_5 : Semiring S
inst_6 : AddCommMonoid α
inst_7 : Module R α
inst_8 : Module S α
inst_9 : SMulCommClass R S α
⊢ Eq (α := Matrix m n α →ₗ[R] Matrix m n α)
    ((liftLinear S : (a : m → n → α →ₗ[R] Matrix m n α) → Matrix m n α →ₗ[R] Matrix m n α) (singleLinearMap R) :
      Matrix m n α →ₗ[R] Matrix m n α)
    (LinearMap.id : Matrix m n α →ₗ[R] Matrix m n α)

Tactic:
ext_linearMap _ <| liftLinear_comp_singleLinearMap _ _

Premises used: Matrix.liftLinear_comp_singleLinearMap, Matrix.ext_linearMap
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Zero α
i j : n
c : α
h : i ≠ j
⊢ (single i j c).diag = 0

Tactic:
funext fun _ => if_neg fun ⟨e₁, e₂⟩ => h (e₁.trans e₂.symm)

Premises used: funext, if_neg
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Zero α
i : n
c : α
h : ∀ (j : n), (single i i c).diag j = Pi.single (M := fun (j : n) ↦ α) i c j
⊢ (single i i c).diag = Pi.single (M := fun (j : n) ↦ α) i c

Tactic:
ext j
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Zero α
i : n
c : α
j : n
pos : ∀ (hij : i = j), (single i i c).diag j = Pi.single (M := fun (j : n) ↦ α) i c j
neg : ∀ (hij : ¬i = j), (single i i c).diag j = Pi.single (M := fun (j : n) ↦ α) i c j
⊢ (single i i c).diag j = Pi.single (M := fun (j : n) ↦ α) i c j

Tactic:
by_cases hij : i = j
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Zero α
i : n
c : α
j : n
hij : i = j
pos : (single j j c).diag j = Pi.single (M := fun (j : n) ↦ α) j c j
⊢ (single i i c).diag j = Pi.single (M := fun (j : n) ↦ α) i c j

Tactic:
rw [hij]
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Zero α
i : n
c : α
j : n
hij : i = j
pos : (single j j c).diag j = Pi.single (M := fun (j : n) ↦ α) j c j
⊢ (single i i c).diag j = Pi.single (M := fun (j : n) ↦ α) i c j

Tactic:
try rw [hij]
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Zero α
i : n
c : α
j : n
hij : i = j
⊢ (single j j c).diag j = Pi.single (M := fun (j : n) ↦ α) j c j

Tactic:
simp [hij]
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Zero α
i : n
c : α
j : n
hij : ¬i = j
⊢ (single i i c).diag j = Pi.single (M := fun (j : n) ↦ α) i c j

Tactic:
simp [hij]
-- 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 : Fintype m
inst_3 : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
b : n
M : Matrix m n α
⊢ (single i j c * M) i b = c * M j b

Tactic:
simp [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
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : NonUnitalNonAssocSemiring α
c : α
i : m
j : n
a : l
M : Matrix l m α
⊢ (M * single i j c) a j = M a i * c

Tactic:
simp [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
α : Type u_7
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
a : l
b : n
h : a ≠ i
M : Matrix m n α
⊢ (single i j c * M) a b = 0

Tactic:
simp [mul_apply, h.symm]

Premises used: Matrix.mul_apply, Ne.symm
-- Module: Mathlib.Data.Matrix.Basis
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : NonUnitalNonAssocSemiring α
c : α
i : m
j : n
a : l
b : n
hbj : b ≠ j
M : Matrix l m α
⊢ (M * single i j c) a b = 0

Tactic:
simp [mul_apply, hbj.symm]

Premises used: Matrix.mul_apply, Ne.symm
-- 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 : ∀ (a : l) (b : n), (single i j c * single j k d) a b = single i k (c * d) a b
⊢ single i j c * single j k d = single i k (c * d)

Tactic:
ext a 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
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 : α)
⊢ (single i j c * single j k d) a b = single i k (c * d) a b

Tactic:
simp only [mul_apply, single]

Premises used: Matrix.mul_apply, Matrix.single