awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Matrix.Basic
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α_1 : Type u_11
β : Type u_12
γ : Type u_13
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonAssocSemiring α_1
inst_3 : NonAssocSemiring β
inst_4 : NonAssocSemiring γ
α : Type u_14
inst_5 : Mul α
inst_6 : AddCommMonoid α
x : (Matrix m m α)ᵐᵒᵖ
⊢ (fun (M : Matrix.{u_2, u_2, u_14} m m αᵐᵒᵖ) ↦ op (Mᵀ.map unop)) ((fun (M : (Matrix m m α)ᵐᵒᵖ) ↦ (unop M)ᵀ.map op) x) =
    x

Tactic:
aesop
-- Module: Mathlib.Data.Matrix.Basic
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α_1 : Type u_11
β : Type u_12
γ : Type u_13
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonAssocSemiring α_1
inst_3 : NonAssocSemiring β
inst_4 : NonAssocSemiring γ
α : Type u_14
inst_5 : Mul α
inst_6 : AddCommMonoid α
x x_1 : Matrix.{u_2, u_2, u_14} m m αᵐᵒᵖ
a : ∀ (i j : m), unop (op ((x * x_1)ᵀ.map unop)) i j = unop (op (xᵀ.map unop) * op (x_1ᵀ.map unop)) i j
⊢ unop (op ((x * x_1)ᵀ.map unop)) = unop (op (xᵀ.map unop) * op (x_1ᵀ.map unop))

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Basic
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α_1 : Type u_11
β : Type u_12
γ : Type u_13
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonAssocSemiring α_1
inst_3 : NonAssocSemiring β
inst_4 : NonAssocSemiring γ
α : Type u_14
inst_5 : Mul α
inst_6 : AddCommMonoid α
x x_1 : Matrix.{u_2, u_2, u_14} m m αᵐᵒᵖ
i j : m
⊢ unop (op ((x * x_1)ᵀ.map unop)) i j = unop (op (xᵀ.map unop) * op (x_1ᵀ.map unop)) i j

Tactic:
simp [transpose, mul_apply]

Premises used: Matrix.mul_apply, Matrix.transpose
-- Module: Mathlib.Data.Matrix.Basic
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α_1 : Type u_11
β : Type u_12
γ : Type u_13
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonAssocSemiring α_1
inst_3 : NonAssocSemiring β
inst_4 : NonAssocSemiring γ
α : Type u_14
inst_5 : Mul α
inst_6 : AddCommMonoid α
x x_1 : Matrix.{u_2, u_2, u_14} m m αᵐᵒᵖ
⊢ op ((x + x_1)ᵀ.map unop) = op (xᵀ.map unop) + op (x_1ᵀ.map unop)

Tactic:
aesop
-- Module: Mathlib.Data.Matrix.Basic
Goal:
l : Type u_1
m : Type u_2
n_1 : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α_1 : Type u_11
β : Type u_12
γ : Type u_13
α : Type u_14
inst : MulOne α
inst_1 : AddCommMonoid α
inst_2 : IsStablyFiniteRing α
n : ℕ
⊢ Eq.{u_14 + 1} (α := (Matrix (Fin n) (Fin n) α)ᵐᵒᵖ)
    ((RingEquiv.mopMatrix : (a : Matrix (Fin n) (Fin n) αᵐᵒᵖ) → (Matrix (Fin n) (Fin n) α)ᵐᵒᵖ) 1 :
      (Matrix (Fin n) (Fin n) α)ᵐᵒᵖ)
    (1 : (Matrix (Fin n) (Fin n) α)ᵐᵒᵖ)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Basic
Goal:
α : Type u_14
inst : MulOne α
inst_1 : AddCommMonoid α
h : IsStablyFiniteRing.{u_14} αᵐᵒᵖ
n : ℕ
⊢ Eq.{u_14 + 1} (α := Matrix (Fin n) (Fin n) αᵐᵒᵖᵐᵒᵖ) ((fun (M : Matrix (Fin n) (Fin n) α) ↦ M.map (op ∘ op)) 1) 1

Tactic:
aesop
-- Module: Mathlib.Data.Matrix.Basic
Goal:
α : Type u_14
inst : MulOne α
inst_1 : AddCommMonoid α
h : IsStablyFiniteRing.{u_14} αᵐᵒᵖ
n : ℕ
x x_1 : Matrix (Fin n) (Fin n) α
a :
  ∀ (i j : Fin n),
    OneHom.toFun { toFun := fun (M : Matrix (Fin n) (Fin n) α) ↦ M.map (op ∘ op), map_one' := ⋯ } (x * x_1) i j =
      HMul.hMul (α := Matrix (Fin n) (Fin n) αᵐᵒᵖᵐᵒᵖ) (β := Matrix (Fin n) (Fin n) αᵐᵒᵖᵐᵒᵖ)
        (OneHom.toFun
          { toFun := fun (M : Matrix (Fin n) (Fin n) α) ↦ M.map (op ∘ op), map_one' := ⋯ :
            OneHom (Matrix (Fin n) (Fin n) α) (Matrix (Fin n) (Fin n) αᵐᵒᵖᵐᵒᵖ) }
          x)
        (OneHom.toFun
          { toFun := fun (M : Matrix (Fin n) (Fin n) α) ↦ M.map (op ∘ op), map_one' := ⋯ :
            OneHom (Matrix (Fin n) (Fin n) α) (Matrix (Fin n) (Fin n) αᵐᵒᵖᵐᵒᵖ) }
          x_1)
        i j
⊢ OneHom.toFun { toFun := fun (M : Matrix (Fin n) (Fin n) α) ↦ M.map (op ∘ op), map_one' := ⋯ } (x * x_1) =
    HMul.hMul (α := Matrix (Fin n) (Fin n) αᵐᵒᵖᵐᵒᵖ)
      (OneHom.toFun
        { toFun := fun (M : Matrix (Fin n) (Fin n) α) ↦ M.map (op ∘ op), map_one' := ⋯ :
          OneHom (Matrix (Fin n) (Fin n) α) (Matrix (Fin n) (Fin n) αᵐᵒᵖᵐᵒᵖ) }
        x)
      (OneHom.toFun
        { toFun := fun (M : Matrix (Fin n) (Fin n) α) ↦ M.map (op ∘ op), map_one' := ⋯ :
          OneHom (Matrix (Fin n) (Fin n) α) (Matrix (Fin n) (Fin n) αᵐᵒᵖᵐᵒᵖ) }
        x_1)

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Basic
Goal:
α : Type u_14
inst : MulOne α
inst_1 : AddCommMonoid α
h : IsStablyFiniteRing.{u_14} αᵐᵒᵖ
n : ℕ
x x_1 : Matrix (Fin n) (Fin n) α
i j : Fin n
⊢ OneHom.toFun { toFun := fun (M : Matrix (Fin n) (Fin n) α) ↦ M.map (op ∘ op), map_one' := ⋯ } (x * x_1) i j =
    HMul.hMul (α := Matrix (Fin n) (Fin n) αᵐᵒᵖᵐᵒᵖ) (β := Matrix (Fin n) (Fin n) αᵐᵒᵖᵐᵒᵖ)
      (OneHom.toFun
        { toFun := fun (M : Matrix (Fin n) (Fin n) α) ↦ M.map (op ∘ op), map_one' := ⋯ :
          OneHom (Matrix (Fin n) (Fin n) α) (Matrix (Fin n) (Fin n) αᵐᵒᵖᵐᵒᵖ) }
        x)
      (OneHom.toFun
        { toFun := fun (M : Matrix (Fin n) (Fin n) α) ↦ M.map (op ∘ op), map_one' := ⋯ :
          OneHom (Matrix (Fin n) (Fin n) α) (Matrix (Fin n) (Fin n) αᵐᵒᵖᵐᵒᵖ) }
        x_1)
      i j

Tactic:
simp [mul_apply]

Premises used: Matrix.mul_apply
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
R : Type u_7
α : Type u_11
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : CommSemiring R
inst_3 : Semiring α
inst_4 : Algebra R α
⊢ Eq (α := Matrix m m α →ₐ[R] Matrix m m α) (mapMatrix (AlgHom.id R α)) (AlgHom.id R (Matrix m m α))

Tactic:
rfl

Premises used: AlgHom.id, AlgHom.mapMatrix, Matrix.map, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
R : Type u_7
α : Type u_11
β : Type u_12
γ : Type u_13
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : CommSemiring R
inst_3 : Semiring α
inst_4 : Semiring β
inst_5 : Semiring γ
inst_6 : Algebra R α
inst_7 : Algebra R β
inst_8 : Algebra R γ
f : β →ₐ[R] γ
g : α →ₐ[R] β
⊢ Eq (α := Matrix m m α →ₐ[R] Matrix m m γ) (comp f.mapMatrix g.mapMatrix) (f.comp g).mapMatrix

Tactic:
rfl

Premises used: AlgHom.mapMatrix, Matrix.map, AlgHom.comp, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
R : Type u_7
α : Type u_11
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : CommSemiring R
inst_3 : Semiring α
inst_4 : Algebra R α
⊢ Eq (α := Matrix m m α ≃ₐ[R] Matrix m m α) (mapMatrix refl) refl

Tactic:
rfl

Premises used: AlgEquiv.mapMatrix, Matrix.map, AlgEquiv.refl, Equiv.refl, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
R : Type u_7
α : Type u_11
β : Type u_12
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : CommSemiring R
inst_3 : Semiring α
inst_4 : Semiring β
inst_5 : Algebra R α
inst_6 : Algebra R β
f : α ≃ₐ[R] β
⊢ Eq (α := Matrix m m β ≃ₐ[R] Matrix m m α) (symm f.mapMatrix) f.symm.mapMatrix

Tactic:
rfl

Premises used: AlgEquiv.symm, AlgEquiv.mapMatrix, Matrix.map, Equiv.symm, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
R : Type u_7
α : Type u_11
β : Type u_12
γ : Type u_13
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : CommSemiring R
inst_3 : Semiring α
inst_4 : Semiring β
inst_5 : Semiring γ
inst_6 : Algebra R α
inst_7 : Algebra R β
inst_8 : Algebra R γ
f : α ≃ₐ[R] β
g : β ≃ₐ[R] γ
⊢ Eq (α := Matrix m m α ≃ₐ[R] Matrix m m γ) (trans f.mapMatrix g.mapMatrix) (f.trans g).mapMatrix

Tactic:
rfl

Premises used: Equiv.trans, AlgEquiv.mapMatrix, AlgEquiv.trans, Matrix.map, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α : Type u_11
β : Type u_12
γ : Type u_13
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : CommSemiring R
inst_3 : Semiring α
inst_4 : Semiring β
inst_5 : Semiring γ
inst_6 : Algebra R α
inst_7 : Algebra R β
inst_8 : Algebra R γ
x : R
a :
  ∀ (i j : m),
    Eq.{u_11 + 1} (α := α)
      (MulOpposite.unop
          (Equiv.toFun (RingEquiv.toEquiv RingEquiv.mopMatrix)
            ((algebraMap R (Matrix.{u_2, u_2, u_11} m m αᵐᵒᵖ) : (a : R) → Matrix m m αᵐᵒᵖ) x))
          i j :
        α)
      (MulOpposite.unop ((algebraMap R (Matrix m m α)ᵐᵒᵖ : (a : R) → (Matrix m m α)ᵐᵒᵖ) x) i j : α)
⊢ Eq (α := Matrix m m α)
    (MulOpposite.unop
      (Equiv.toFun (RingEquiv.toEquiv RingEquiv.mopMatrix)
        ((algebraMap R (Matrix.{u_2, u_2, u_11} m m αᵐᵒᵖ) : (a : R) → Matrix m m αᵐᵒᵖ) x)))
    (MulOpposite.unop ((algebraMap R (Matrix m m α)ᵐᵒᵖ : (a : R) → (Matrix m m α)ᵐᵒᵖ) x))

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Basic
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α : Type u_11
β : Type u_12
γ : Type u_13
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : CommSemiring R
inst_3 : Semiring α
inst_4 : Semiring β
inst_5 : Semiring γ
inst_6 : Algebra R α
inst_7 : Algebra R β
inst_8 : Algebra R γ
x : R
i j : m
⊢ Eq.{u_11 + 1} (α := α)
    (MulOpposite.unop
        (Equiv.toFun (RingEquiv.toEquiv RingEquiv.mopMatrix)
          ((algebraMap R (Matrix.{u_2, u_2, u_11} m m αᵐᵒᵖ) : (a : R) → Matrix m m αᵐᵒᵖ) x))
        i j :
      α)
    (MulOpposite.unop ((algebraMap R (Matrix m m α)ᵐᵒᵖ : (a : R) → (Matrix m m α)ᵐᵒᵖ) x) i j : α)

Tactic:
simp [algebraMap_matrix_apply, eq_comm, apply_ite MulOpposite.unop]

Premises used: apply_ite, eq_comm, MulOpposite.unop, Matrix.algebraMap_matrix_apply
-- Module: Mathlib.Data.Matrix.Basic
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α : Type u_11
β_1 : Type u_12
γ : Type u_13
ι : Type u_14
β : ι → Type u_15
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : (i : ι) → Mul (β i)
inst_2 : Fintype n
x x_1 : Matrix n n ((i : ι) → β i)
h :
  ∀ (x_2 : ι) (i j : n),
    Equiv.toFun (AddEquiv.toEquiv (piAddEquiv (β := β))) (x * x_1) x_2 i j =
      (Equiv.toFun (AddEquiv.toEquiv (piAddEquiv (β := β))) x *
          Equiv.toFun (AddEquiv.toEquiv (piAddEquiv (β := β))) x_1)
        x_2 i j
⊢ Equiv.toFun (AddEquiv.toEquiv (piAddEquiv (β := β))) (x * x_1) =
    Equiv.toFun (AddEquiv.toEquiv (piAddEquiv (β := β))) x * Equiv.toFun (AddEquiv.toEquiv (piAddEquiv (β := β))) x_1

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Basic
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α : Type u_11
β_1 : Type u_12
γ : Type u_13
ι : Type u_14
β : ι → Type u_15
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : (i : ι) → Mul (β i)
inst_2 : Fintype n
x x_1 : Matrix n n ((i : ι) → β i)
x_2 : ι
i j : n
⊢ Equiv.toFun (AddEquiv.toEquiv (piAddEquiv (β := β))) (x * x_1) x_2 i j =
    (Equiv.toFun (AddEquiv.toEquiv (piAddEquiv (β := β))) x * Equiv.toFun (AddEquiv.toEquiv (piAddEquiv (β := β))) x_1)
      x_2 i j

Tactic:
simp [Matrix.mul_apply]

Premises used: Matrix.mul_apply
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
inst : Add α
⊢ Eq (α := Matrix n m α ≃+ Matrix m n α) (AddEquiv.symm (transposeAddEquiv m n α)) (transposeAddEquiv n m α)

Tactic:
rfl

Premises used: Matrix.transpose, Equiv.symm, Matrix.transposeAddEquiv, rfl, AddEquiv.symm
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
inst : AddMonoid α
l : List (Matrix m n α)
⊢ l.sumᵀ = (List.map transpose l).sum

Tactic:
map_list_sum (transposeAddEquiv m n α) l

Premises used: List.sum, map_list_sum, Matrix.transpose, Matrix.transposeAddEquiv
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
inst : AddCommMonoid α
s : Multiset (Matrix m n α)
⊢ s.sumᵀ = (Multiset.map transpose s).sum

Tactic:
(transposeAddEquiv m n α).toAddMonoidHom.map_multiset_sum s

Premises used: Multiset.sum, Multiset.foldr, AddEquiv.toAddMonoidHom, Matrix.transpose, AddMonoidHom.map_multiset_sum, Matrix.transposeAddEquiv
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
inst : AddCommMonoid α
ι : Type u_14
s : Finset ι
M : ι → Matrix m n α
⊢ Eq (α := Matrix n m α) (∑ i ∈ s, M i)ᵀ (∑ i ∈ s, (M i)ᵀ)

Tactic:
map_sum (transposeAddEquiv m n α) _ s

Premises used: Multiset.sum, Multiset.foldr, map_sum, Matrix.transpose, Matrix.transposeAddEquiv, Finset.sum
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type u_11
inst : Semiring R
inst_1 : AddCommMonoid α
inst_2 : Module R α
⊢ Eq (α := Matrix n m α ≃ₗ[R] Matrix m n α) (LinearEquiv.symm (transposeLinearEquiv m n R α))
    (transposeLinearEquiv n m R α)

Tactic:
rfl

Premises used: LinearEquiv.symm, Matrix.transposeLinearEquiv, Matrix.transpose, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
α : Type u_11
inst : CommSemiring α
inst_1 : Fintype m
inst_2 : DecidableEq m
M : Matrix m m α
k : ℕ
⊢ (M ^ k)ᵀ = Mᵀ ^ k

Tactic:
MulOpposite.op_injective <| map_pow (transposeRingEquiv m α) M k

Premises used: MulOpposite.op_injective, Matrix.transposeRingEquiv, map_pow
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
α : Type u_11
inst : CommSemiring α
inst_1 : Fintype m
inst_2 : DecidableEq m
l : List (Matrix m m α)
⊢ l.prodᵀ = (List.map transpose l).reverse.prod

Tactic:
(transposeRingEquiv m α).unop_map_list_prod l

Premises used: Matrix.transposeRingEquiv, Matrix.transpose, MulOpposite.unop, RingEquiv.unop_map_list_prod, List.prod
-- Module: Mathlib.Data.Matrix.Basic
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α : Type u_11
β : Type u_12
γ : Type u_13
inst : CommSemiring R
inst_1 : CommSemiring α
inst_2 : Fintype m
inst_3 : DecidableEq m
inst_4 : Algebra R α
r : R
⊢ (RingEquiv.toEquiv (transposeRingEquiv m α)).toFun ((algebraMap R (Matrix m m α) : (a : R) → Matrix m m α) r) =
    (algebraMap R (Matrix m m α)ᵐᵒᵖ : (a : R) → (Matrix m m α)ᵐᵒᵖ) r

Tactic:
simp [algebraMap_eq_diagonal]

Premises used: Matrix.algebraMap_eq_diagonal
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
s : Finset ι
x : ι → Matrix m n α
y : n → α
h : ∀ (x_1 : m), ((∑ i ∈ s, x i) *ᵥ y) x_1 = (∑ i ∈ s, x i *ᵥ y) x_1
⊢ Eq (α := m → α) ((∑ i ∈ s, x i) *ᵥ y) (∑ i ∈ s, x i *ᵥ y)

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
s : Finset ι
x : ι → Matrix m n α
y : n → α
x_1 : m
h : Eq.{u_11 + 1} (α := α) (∑ x_2 : n, ∑ i ∈ s, x i x_1 x_2 * y x_2) (∑ x_2 ∈ s, ∑ x_3 : n, x x_2 x_1 x_3 * y x_3)
⊢ ((∑ i ∈ s, x i) *ᵥ y) x_1 = (∑ i ∈ s, x i *ᵥ y) x_1

Tactic:
simp only [mulVec, dotProduct, sum_apply, Finset.sum_mul, Finset.sum_apply]

Premises used: dotProduct, Matrix.sum_apply, Finset.sum_apply, Matrix.mulVec, Finset.sum_mul
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
s : Finset ι
x : ι → Matrix m n α
y : n → α
x_1 : m
h h₁ :
  Eq.{u_11 + 1} (α := α) (∑ y_1 ∈ s, ∑ x_2 : n, x y_1 x_1 x_2 * y x_2) (∑ x_2 ∈ s, ∑ x_3 : n, x x_2 x_1 x_3 * y x_3)
⊢ Eq.{u_11 + 1} (α := α) (∑ x_2 : n, ∑ i ∈ s, x i x_1 x_2 * y x_2) (∑ x_2 ∈ s, ∑ x_3 : n, x x_2 x_1 x_3 * y x_3)

Tactic:
rw [Finset.sum_comm]

Premises used: Finset.sum_comm
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
x : Matrix m n α
s : Finset ι
y : ι → n → α
h : ∀ (x_1 : m), (x *ᵥ ∑ i ∈ s, y i) x_1 = (∑ i ∈ s, x *ᵥ y i) x_1
⊢ x *ᵥ ∑ i ∈ s, y i = ∑ i ∈ s, x *ᵥ y i

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
x : Matrix m n α
s : Finset ι
y : ι → n → α
x_1 : m
⊢ (x *ᵥ ∑ i ∈ s, y i) x_1 = (∑ i ∈ s, x *ᵥ y i) x_1

Tactic:
simp only [mulVec, dotProduct_sum, Finset.sum_apply]

Premises used: dotProduct_sum, Finset.sum_apply, Matrix.mulVec
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
s : Finset ι
x : ι → n → α
y : Matrix n m α
h : ∀ (x_1 : m), ((∑ i ∈ s, x i) ᵥ* y) x_1 = (∑ i ∈ s, x i ᵥ* y) x_1
⊢ (∑ i ∈ s, x i) ᵥ* y = ∑ i ∈ s, x i ᵥ* y

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
s : Finset ι
x : ι → n → α
y : Matrix n m α
x_1 : m
⊢ ((∑ i ∈ s, x i) ᵥ* y) x_1 = (∑ i ∈ s, x i ᵥ* y) x_1

Tactic:
simp only [vecMul, sum_dotProduct, Finset.sum_apply]

Premises used: Finset.sum_apply, Matrix.vecMul, sum_dotProduct
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
x : n → α
s : Finset ι
y : ι → Matrix n m α
h : ∀ (x_1 : m), (x ᵥ* ∑ i ∈ s, y i) x_1 = (∑ i ∈ s, x ᵥ* y i) x_1
⊢ Eq (α := m → α) (x ᵥ* ∑ i ∈ s, y i) (∑ i ∈ s, x ᵥ* y i)

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
x : n → α
s : Finset ι
y : ι → Matrix n m α
x_1 : m
h : Eq.{u_11 + 1} (α := α) (∑ x_2 : n, ∑ i ∈ s, x x_2 * y i x_2 x_1) (∑ x_2 ∈ s, ∑ x_3 : n, x x_3 * y x_2 x_3 x_1)
⊢ (x ᵥ* ∑ i ∈ s, y i) x_1 = (∑ i ∈ s, x ᵥ* y i) x_1

Tactic:
simp only [vecMul, dotProduct, sum_apply, Finset.mul_sum, Finset.sum_apply]

Premises used: Finset.mul_sum, dotProduct, Matrix.sum_apply, Finset.sum_apply, Matrix.vecMul
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
x : n → α
s : Finset ι
y : ι → Matrix n m α
x_1 : m
h h₁ :
  Eq.{u_11 + 1} (α := α) (∑ y_1 ∈ s, ∑ x_2 : n, x x_2 * y y_1 x_2 x_1) (∑ x_2 ∈ s, ∑ x_3 : n, x x_3 * y x_2 x_3 x_1)
⊢ Eq.{u_11 + 1} (α := α) (∑ x_2 : n, ∑ i ∈ s, x x_2 * y i x_2 x_1) (∑ x_2 ∈ s, ∑ x_3 : n, x x_3 * y x_2 x_3 x_1)

Tactic:
rw [Finset.sum_comm]

Premises used: Finset.sum_comm
-- 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
c : α
⊢ single i j c i j = c

Tactic:
if_pos (And.intro rfl rfl)

Premises used: if_pos, And.intro, rfl, Matrix.single, 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
c : α
i' : m
j' : n
h : ¬(i = i' ∧ j = j')
simp : i = i' → j = j' → c = 0
⊢ single i j c i' j' = 0

Tactic:
simp only [single, and_imp, ite_eq_right_iff, of_apply]

Premises used: and_imp, Matrix.of_apply, ite_eq_right_iff, 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
c : α
i' : m
j' : n
h : ¬(i = i' ∧ j = j')
inl : i = i' → ∀ (h : ¬i = i'), j = j' → c = 0
inr inr₁ inr₂ inr₃ : i = i' → ∀ (h : ¬j = j'), j = j' → c = 0
⊢ i = i' → j = j' → c = 0

Tactic:
tauto
-- 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 i' : m
hi : i ≠ i'
j j' : n
a : α
⊢ single i j a i' j' = 0

Tactic:
simp [hi]
-- 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 i' : m
j j' : n
hj : j ≠ j'
a : α
⊢ single i j a i' j' = 0

Tactic:
simp [hj]
-- 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
c : α
i' : m
j' : n
⊢ single i j c i' j' = if i = i' ∧ j = j' then c else 0

Tactic:
rfl

Premises used: rfl, Matrix.single, 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 : α
a₁ :
  ∀ (a_1 : m) (b : n),
    single i j a a_1 b =
      (of : (a : m → n → α) → Matrix m n α)
        (Pi.single (M := fun (a : m) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j a)) a_1 b
⊢ single i j a =
    (of : (a : m → n → α) → Matrix m n α)
      (Pi.single (M := fun (a : m) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j a))

Tactic:
ext a 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
a₁ :
  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 :
      α)
⊢ single i j a_1 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:
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_1 : α
a : m
b : n
pos :
  ∀ (hi : i = a),
    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 :
  ∀ (hi : ¬i = a),
    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 hi : i = a
-- 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