awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : Semiring R₁
inst_1 : Semiring S₁
inst_2 : Semiring R₂
inst_3 : Semiring S₂
inst_4 : AddCommMonoid N₂
inst_5 : Module S₁ N₂
inst_6 : Module S₂ N₂
inst_7 : SMulCommClass S₂ S₁ N₂
inst_8 : Fintype n
inst_9 : Fintype m
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst_10 : DecidableEq n
inst_11 : DecidableEq m
f : Matrix n m N₂
i : n
j : m
⊢ ∑ i' : n, ∑ j' : m, (if i = i' then 1 else 0) •> (if j = j' then 1 else 0) •> f i' j' = f i j

Tactic:
have : (∑ i', ∑ j', (if i = i' then (1 : S₁) else (0 : S₁)) •
        (if j = j' then (1 : S₂) else (0 : S₂)) • f i' j') =
      f i j := by
    simp_rw [← Finset.smul_sum]
    simp only [ite_smul, one_smul, zero_smul, sum_ite_eq, mem_univ, ↓reduceIte]
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : Semiring R₁
inst_1 : Semiring S₁
inst_2 : Semiring R₂
inst_3 : Semiring S₂
inst_4 : AddCommMonoid N₂
inst_5 : Module S₁ N₂
inst_6 : Module S₂ N₂
inst_7 : SMulCommClass S₂ S₁ N₂
inst_8 : Fintype n
inst_9 : Fintype m
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst_10 : DecidableEq n
inst_11 : DecidableEq m
f : Matrix n m N₂
i : n
j : m
this : ∑ i' : n, ∑ j' : m, (if i = i' then 1 else 0) •> (if j = j' then 1 else 0) •> f i' j' = f i j
rw :
  Eq.{u_10 + 1} (α := N₂)
    (∑ i_1 : n,
      ∑ j_1 : m,
        ((σ₂ : (a : R₂) → S₂) (Pi.single (M := fun (a : m) ↦ R₂) j 1 j_1 : R₂) : S₂) •>
          ((σ₁ : (a : R₁) → S₁) (Pi.single (M := fun (a : n) ↦ R₁) i 1 i_1 : R₁) : S₁) •> f i_1 j_1)
    (∑ i' : n, ∑ j' : m, (if i = i' then 1 else 0) •> (if j = j' then 1 else 0) •> f i' j')
⊢ ∑ i_1 : n,
      ∑ j_1 : m,
        ((σ₂ : (a : R₂) → S₂) (Pi.single (M := fun (a : m) ↦ R₂) j 1 j_1 : R₂) : S₂) •>
          ((σ₁ : (a : R₁) → S₁) (Pi.single (M := fun (a : n) ↦ R₁) i 1 i_1 : R₁) : S₁) •> f i_1 j_1 =
    f i j

Tactic:
rw [← this]
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : Semiring R₁
inst_1 : Semiring S₁
inst_2 : Semiring R₂
inst_3 : Semiring S₂
inst_4 : AddCommMonoid N₂
inst_5 : Module S₁ N₂
inst_6 : Module S₂ N₂
inst_7 : SMulCommClass S₂ S₁ N₂
inst_8 : Fintype n
inst_9 : Fintype m
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst_10 : DecidableEq n
inst_11 : DecidableEq m
f : Matrix n m N₂
i : n
j : m
this : ∑ i' : n, ∑ j' : m, (if i = i' then 1 else 0) •> (if j = j' then 1 else 0) •> f i' j' = f i j
x : n
h : Membership.mem (γ := Finset n) univ x
x_1 : m
h_1 : Membership.mem (γ := Finset m) univ x_1
⊢ ((σ₂ : (a : R₂) → S₂) (Pi.single (M := fun (a : m) ↦ R₂) j 1 x_1 : R₂) : S₂) •>
      ((σ₁ : (a : R₁) → S₁) (Pi.single (M := fun (a : n) ↦ R₁) i 1 x : R₁) : S₁) •> f x x_1 =
    (if i = x then 1 else 0) •> (if j = x_1 then 1 else 0) •> f x x_1

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : Semiring R₁
inst_1 : Semiring S₁
inst_2 : Semiring R₂
inst_3 : Semiring S₂
inst_4 : AddCommMonoid N₂
inst_5 : Module S₁ N₂
inst_6 : Module S₂ N₂
inst_7 : SMulCommClass S₂ S₁ N₂
inst_8 : Fintype n
inst_9 : Fintype m
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst_10 : DecidableEq n
inst_11 : DecidableEq m
f : Matrix n m N₂
i : n
j : m
this : ∑ i' : n, ∑ j' : m, (if i = i' then 1 else 0) •> (if j = j' then 1 else 0) •> f i' j' = f i j
⊢ Eq.{u_10 + 1} (α := N₂)
    (∑ i_1 : n,
      ∑ j_1 : m,
        ((σ₂ : (a : R₂) → S₂) (Pi.single (M := fun (a : m) ↦ R₂) j 1 j_1 : R₂) : S₂) •>
          ((σ₁ : (a : R₁) → S₁) (Pi.single (M := fun (a : n) ↦ R₁) i 1 i_1 : R₁) : S₁) •> f i_1 j_1)
    (∑ i' : n, ∑ j' : m, (if i = i' then 1 else 0) •> (if j = j' then 1 else 0) •> f i' j')

Tactic:
exact Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ => by aesop

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
M₁ : Type u_6
M₂ : Type u_7
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : Semiring R₁
inst_2 : Semiring S₁
inst_3 : Semiring R₂
inst_4 : Semiring S₂
inst_5 : AddCommMonoid M₁
inst_6 : Module R₁ M₁
inst_7 : AddCommMonoid M₂
inst_8 : Module R₂ M₂
inst_9 : AddCommMonoid N₂
inst_10 : Module R N₂
inst_11 : Module S₁ N₂
inst_12 : Module S₂ N₂
inst_13 : SMulCommClass S₁ R N₂
inst_14 : SMulCommClass S₂ R N₂
inst_15 : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
f : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂
b₁ : n → M₁
b₂ : m → M₂
i : n
j : m
⊢ Eq.{u_10 + 1} (α := N₂)
    (((toMatrix₂Aux R b₁ b₂ : (M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂) →ₗ[R] Matrix n m N₂) :
          (a : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂) → Matrix n m N₂)
        f i j :
      N₂)
    ((((f : (a : M₁) → M₂ →ₛₗ[σ₂] N₂) (b₁ i) : M₂ →ₛₗ[σ₂] N₂) : (a : M₂) → N₂) (b₂ j) : N₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : Semiring R₁
inst_2 : Semiring S₁
inst_3 : Semiring R₂
inst_4 : Semiring S₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₂
inst_7 : Module S₁ N₂
inst_8 : Module S₂ N₂
inst_9 : SMulCommClass S₁ R N₂
inst_10 : SMulCommClass S₂ R N₂
inst_11 : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst_12 : Fintype n
inst_13 : Fintype m
inst_14 : DecidableEq n
inst_15 : DecidableEq m
f : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂
⊢ toLinearMap₂'Aux σ₁ σ₂
      (((toMatrix₂Aux R (fun (i : n) ↦ Pi.single (M := fun (j : n) ↦ R₁) i 1) fun (j : m) ↦
              Pi.single (M := fun (j : m) ↦ R₂) j 1 :
            (((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) →ₗ[R] Matrix n m N₂) :
          (a : ((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) → Matrix n m N₂)
        f) =
    f

Tactic:
ext_basis (Pi.basisFun R₁ n) (Pi.basisFun R₂ m) fun i j => ?_

Premises used: LinearMap.ext_basis, Pi.basisFun
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : Semiring R₁
inst_2 : Semiring S₁
inst_3 : Semiring R₂
inst_4 : Semiring S₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₂
inst_7 : Module S₁ N₂
inst_8 : Module S₂ N₂
inst_9 : SMulCommClass S₁ R N₂
inst_10 : SMulCommClass S₂ R N₂
inst_11 : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst_12 : Fintype n
inst_13 : Fintype m
inst_14 : DecidableEq n
inst_15 : DecidableEq m
f : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂
refine :
  ∀ (i : n) (j : m),
    Eq.{u_10 + 1} (α := N₂)
      ((((toLinearMap₂'Aux σ₁ σ₂
                    (((toMatrix₂Aux R (fun (i : n) ↦ Pi.single (M := fun (j : n) ↦ R₁) i 1) fun (j : m) ↦
                            Pi.single (M := fun (j : m) ↦ R₂) j 1 :
                          (((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) →ₗ[R] Matrix n m N₂) :
                        (a : ((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) → Matrix n m N₂)
                      f) :
                  (a : n → R₁) → (m → R₂) →ₛₗ[σ₂] N₂)
                ((Pi.basisFun R₁ n : (a : n) → n → R₁) i) :
              (m → R₂) →ₛₗ[σ₂] N₂) :
            (a : m → R₂) → N₂)
          ((Pi.basisFun R₂ m : (a : m) → m → R₂) j : m → R₂) :
        N₂)
      ((((f : (a : n → R₁) → (m → R₂) →ₛₗ[σ₂] N₂) ((Pi.basisFun R₁ n : (a : n) → n → R₁) i) : (m → R₂) →ₛₗ[σ₂] N₂) :
            (a : m → R₂) → N₂)
          ((Pi.basisFun R₂ m : (a : m) → m → R₂) j : m → R₂) :
        N₂)
⊢ toLinearMap₂'Aux σ₁ σ₂
      (((toMatrix₂Aux R (fun (i : n) ↦ Pi.single (M := fun (j : n) ↦ R₁) i 1) fun (j : m) ↦
              Pi.single (M := fun (j : m) ↦ R₂) j 1 :
            (((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) →ₗ[R] Matrix n m N₂) :
          (a : ((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) → Matrix n m N₂)
        f) =
    f

Tactic:
refine ext_basis (Pi.basisFun R₁ n) (Pi.basisFun R₂ m) fun i j => ?_

Premises used: LinearMap.ext_basis, Pi.basisFun
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : Semiring R₁
inst_2 : Semiring S₁
inst_3 : Semiring R₂
inst_4 : Semiring S₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₂
inst_7 : Module S₁ N₂
inst_8 : Module S₂ N₂
inst_9 : SMulCommClass S₁ R N₂
inst_10 : SMulCommClass S₂ R N₂
inst_11 : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst_12 : Fintype n
inst_13 : Fintype m
inst_14 : DecidableEq n
inst_15 : DecidableEq m
f : Matrix n m N₂
a :
  ∀ (i : n) (j : m),
    ((toMatrix₂Aux R (fun (i : n) ↦ Pi.single (M := fun (j : n) ↦ R₁) i 1) fun (j : m) ↦
              Pi.single (M := fun (j : m) ↦ R₂) j 1 :
            (((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) →ₗ[R] Matrix n m N₂) :
          (a : ((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) → Matrix n m N₂)
        (toLinearMap₂'Aux σ₁ σ₂ f) i j =
      f i j
⊢ ((toMatrix₂Aux R (fun (i : n) ↦ Pi.single (M := fun (j : n) ↦ R₁) i 1) fun (j : m) ↦
            Pi.single (M := fun (j : m) ↦ R₂) j 1 :
          (((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) →ₗ[R] Matrix n m N₂) :
        (a : ((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) → Matrix n m N₂)
      (toLinearMap₂'Aux σ₁ σ₂ f) =
    f

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : Semiring R₁
inst_2 : Semiring S₁
inst_3 : Semiring R₂
inst_4 : Semiring S₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₂
inst_7 : Module S₁ N₂
inst_8 : Module S₂ N₂
inst_9 : SMulCommClass S₁ R N₂
inst_10 : SMulCommClass S₂ R N₂
inst_11 : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst_12 : Fintype n
inst_13 : Fintype m
inst_14 : DecidableEq n
inst_15 : DecidableEq m
f : Matrix n m N₂
i : n
j : m
a :
  (((toLinearMap₂'Aux σ₁ σ₂ f : (a : (j : n) → R₁) → ((j : m) → R₂) →ₛₗ[σ₂] N₂)
            (Pi.single (M := fun (j : n) ↦ R₁) i 1) :
          ((j : m) → R₂) →ₛₗ[σ₂] N₂) :
        (a : (j : m) → R₂) → N₂)
      (Pi.single (M := fun (j : m) ↦ R₂) j 1) =
    f i j
⊢ ((toMatrix₂Aux R (fun (i : n) ↦ Pi.single (M := fun (j : n) ↦ R₁) i 1) fun (j : m) ↦
            Pi.single (M := fun (j : m) ↦ R₂) j 1 :
          (((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) →ₗ[R] Matrix n m N₂) :
        (a : ((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) → Matrix n m N₂)
      (toLinearMap₂'Aux σ₁ σ₂ f) i j =
    f i j

Tactic:
simp_rw [LinearMap.toMatrix₂Aux_apply, Matrix.toLinearMap₂'Aux_single]

Premises used: Matrix.toLinearMap₂'Aux_single, LinearMap.toMatrix₂Aux_apply
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid N₂
inst_2 : Module R N₂
inst_3 : Semiring R₁
inst_4 : Semiring R₂
inst_5 : Semiring S₁
inst_6 : Semiring S₂
inst_7 : Module S₁ N₂
inst_8 : Module S₂ N₂
inst_9 : SMulCommClass S₁ R N₂
inst_10 : SMulCommClass S₂ R N₂
inst_11 : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst_12 : Fintype n
inst_13 : Fintype m
inst_14 : DecidableEq n
inst_15 : DecidableEq m
M : Matrix n m N₂
⊢ Eq (α := (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂) (toLinearMap₂'Aux σ₁ σ₂ M)
    (((toLinearMapₛₗ₂' R σ₁ σ₂ : Matrix n m N₂ ≃ₗ[R] (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂) :
        (a : Matrix n m N₂) → (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂)
      M)

Tactic:
rfl

Premises used: LinearMap.mk₂'ₛₗ, Matrix.toLinearMap₂'Aux, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid N₂
inst_2 : Module R N₂
inst_3 : Semiring R₁
inst_4 : Semiring R₂
inst_5 : Semiring S₁
inst_6 : Semiring S₂
inst_7 : Module S₁ N₂
inst_8 : Module S₂ N₂
inst_9 : SMulCommClass S₁ R N₂
inst_10 : SMulCommClass S₂ R N₂
inst_11 : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst_12 : Fintype n
inst_13 : Fintype m
inst_14 : DecidableEq n
inst_15 : DecidableEq m
M : Matrix n m N₂
x : n → R₁
y : m → R₂
rw :
  Eq.{u_10 + 1} (α := N₂)
    (∑ i : n, ∑ j : m, ((σ₂ : (a : R₂) → S₂) (y j) : S₂) •> ((σ₁ : (a : R₁) → S₁) (x i) : S₁) •> M i j)
    (∑ i : n, ∑ j : m, ((σ₁ : (a : R₁) → S₁) (x i) : S₁) •> ((σ₂ : (a : R₂) → S₂) (y j) : S₂) •> M i j)
⊢ Eq.{u_10 + 1} (α := N₂)
    (((((((toLinearMapₛₗ₂' R σ₁ σ₂ : Matrix n m N₂ ≃ₗ[R] (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂) :
                      (a : Matrix n m N₂) → (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂)
                    M :
                  (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂) :
                (a : n → R₁) → (m → R₂) →ₛₗ[σ₂] N₂)
              x :
            (m → R₂) →ₛₗ[σ₂] N₂) :
          (a : m → R₂) → N₂)
        y :
      N₂)
    (∑ i : n, ∑ j : m, ((σ₁ : (a : R₁) → S₁) (x i) : S₁) •> ((σ₂ : (a : R₂) → S₂) (y j) : S₂) •> M i j : N₂)

Tactic:
rw [toLinearMapₛₗ₂', toMatrixₛₗ₂', LinearEquiv.coe_symm_mk, toLinearMap₂'Aux, mk₂'ₛₗ_apply]

Premises used: Matrix.toLinearMapₛₗ₂', LinearMap.mk₂'ₛₗ_apply, LinearEquiv.coe_symm_mk, Matrix.toLinearMap₂'Aux, LinearMap.toMatrixₛₗ₂'
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid N₂
inst_2 : Module R N₂
inst_3 : Semiring R₁
inst_4 : Semiring R₂
inst_5 : Semiring S₁
inst_6 : Semiring S₂
inst_7 : Module S₁ N₂
inst_8 : Module S₂ N₂
inst_9 : SMulCommClass S₁ R N₂
inst_10 : SMulCommClass S₂ R N₂
inst_11 : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst_12 : Fintype n
inst_13 : Fintype m
inst_14 : DecidableEq n
inst_15 : DecidableEq m
M : Matrix n m N₂
x : n → R₁
y : m → R₂
x_1 : n
h : Membership.mem (γ := Finset n) univ x_1
x_2 : m
h_1 : Membership.mem (γ := Finset m) univ x_2
rw rw₁ :
  ((σ₁ : (a : R₁) → S₁) (x x_1) : S₁) •> ((σ₂ : (a : R₂) → S₂) (y x_2) : S₂) •> M x_1 x_2 =
    ((σ₁ : (a : R₁) → S₁) (x x_1) : S₁) •> ((σ₂ : (a : R₂) → S₂) (y x_2) : S₂) •> M x_1 x_2
⊢ ((σ₂ : (a : R₂) → S₂) (y x_2) : S₂) •> ((σ₁ : (a : R₁) → S₁) (x x_1) : S₁) •> M x_1 x_2 =
    ((σ₁ : (a : R₁) → S₁) (x x_1) : S₁) •> ((σ₂ : (a : R₂) → S₂) (y x_2) : S₂) •> M x_1 x_2

Tactic:
rw [smul_comm]

Premises used: SMulCommClass.smul_comm
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid N₂
inst_2 : Module R N₂
inst_3 : Semiring R₁
inst_4 : Semiring R₂
inst_5 : Semiring S₁
inst_6 : Semiring S₂
inst_7 : Module S₁ N₂
inst_8 : Module S₂ N₂
inst_9 : SMulCommClass S₁ R N₂
inst_10 : SMulCommClass S₂ R N₂
inst_11 : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst_12 : Fintype n
inst_13 : Fintype m
inst_14 : DecidableEq n
inst_15 : DecidableEq m
M : Matrix n m N₂
x : n → R₁
y : m → R₂
⊢ Eq.{u_10 + 1} (α := N₂)
    (∑ i : n, ∑ j : m, ((σ₂ : (a : R₂) → S₂) (y j) : S₂) •> ((σ₁ : (a : R₁) → S₁) (x i) : S₁) •> M i j)
    (∑ i : n, ∑ j : m, ((σ₁ : (a : R₁) → S₁) (x i) : S₁) •> ((σ₂ : (a : R₂) → S₂) (y j) : S₂) •> M i j)

Tactic:
apply Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ => by
    rw [smul_comm]

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
S₁ : Type u_3
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid N₂
inst_2 : Module R N₂
inst_3 : Semiring S₁
inst_4 : Semiring S₂
inst_5 : Module S₁ N₂
inst_6 : Module S₂ N₂
inst_7 : SMulCommClass S₁ R N₂
inst_8 : SMulCommClass S₂ R N₂
inst_9 : SMulCommClass S₂ S₁ N₂
inst_10 : Fintype n
inst_11 : Fintype m
inst_12 : DecidableEq n
inst_13 : DecidableEq m
M : Matrix n m N₂
x : n → S₁
y : m → S₂
x_1 : n
h : Membership.mem (γ := Finset n) univ x_1
x_2 : m
h_1 : Membership.mem (γ := Finset m) univ x_2
rw : y x_2 •> ((RingHom.id S₁ : (a : S₁) → S₁) (x x_1) : S₁) •> M x_1 x_2 = x x_1 •> y x_2 •> M x_1 x_2
rw₁ : y x_2 •> x x_1 •> M x_1 x_2 = x x_1 •> y x_2 •> M x_1 x_2
rw₂ rw₃ : x x_1 •> y x_2 •> M x_1 x_2 = x x_1 •> y x_2 •> M x_1 x_2
⊢ ((RingHom.id S₂ : (a : S₂) → S₂) (y x_2) : S₂) •> ((RingHom.id S₁ : (a : S₁) → S₁) (x x_1) : S₁) •> M x_1 x_2 =
    x x_1 •> y x_2 •> M x_1 x_2

Tactic:
rw [RingHom.id_apply, RingHom.id_apply, smul_comm]

Premises used: RingHom.id_apply, SMulCommClass.smul_comm
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
n : Type u_11
m : Type u_12
inst : Fintype n
inst_1 : Fintype m
inst_2 : DecidableEq n
inst_3 : DecidableEq m
T : Type u_16
inst_4 : CommSemiring T
M : Matrix n m T
v : n → T
w : m → T
simp_rw : Eq.{u_16 + 1} (α := T) (∑ i : n, ∑ j : m, v i •> w j •> M i j) (∑ x : n, v x * ∑ x_1 : m, M x x_1 * w x_1)
⊢ ((((((toLinearMap₂' T : Matrix n m T ≃ₗ[T] (n → T) →ₗ[T] (m → T) →ₗ[T] T) :
                    (a : Matrix n m T) → (n → T) →ₗ[T] (m → T) →ₗ[T] T)
                  M :
                (n → T) →ₗ[T] (m → T) →ₗ[T] T) :
              (a : n → T) → (m → T) →ₗ[T] T)
            v :
          (m → T) →ₗ[T] T) :
        (a : m → T) → T)
      w =
    v ⬝ᵥ M *ᵥ w

Tactic:
simp_rw [Matrix.toLinearMap₂'_apply, dotProduct, Matrix.mulVec, dotProduct]

Premises used: dotProduct, Matrix.toLinearMap₂'_apply, Matrix.mulVec
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
n : Type u_11
m : Type u_12
inst : Fintype n
inst_1 : Fintype m
inst_2 : DecidableEq n
inst_3 : DecidableEq m
T : Type u_16
inst_4 : CommSemiring T
M : Matrix n m T
v : n → T
w : m → T
⊢ Eq.{u_16 + 1} (α := T) (∑ i : n, ∑ j : m, v i •> w j •> M i j) (∑ x : n, v x * ∑ x_1 : m, M x x_1 * w x_1)

Tactic:
Finset.sum_congr rfl fun _ _ => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
n : Type u_11
m : Type u_12
inst : Fintype n
inst_1 : Fintype m
inst_2 : DecidableEq n
inst_3 : DecidableEq m
T : Type u_16
inst_4 : CommSemiring T
M : Matrix n m T
v : n → T
w : m → T
refine :
  ∀ (x : n), Membership.mem (γ := Finset n) univ x → ∑ j : m, v x •> w j •> M x j = v x * ∑ x_2 : m, M x x_2 * w x_2
⊢ Eq.{u_16 + 1} (α := T) (∑ i : n, ∑ j : m, v i •> w j •> M i j) (∑ x : n, v x * ∑ x_1 : m, M x x_1 * w x_1)

Tactic:
refine Finset.sum_congr rfl fun _ _ => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
n : Type u_11
m : Type u_12
inst : Fintype n
inst_1 : Fintype m
inst_2 : DecidableEq n
inst_3 : DecidableEq m
T : Type u_16
inst_4 : CommSemiring T
M : Matrix n m T
v : n → T
w : m → T
x : n
h : Membership.mem (γ := Finset n) univ x
rw : Eq.{u_16 + 1} (α := T) (∑ j : m, v x •> w j •> M x j) (∑ i : m, v x * (M x i * w i))
⊢ ∑ j : m, v x •> w j •> M x j = v x * ∑ x_1 : m, M x x_1 * w x_1

Tactic:
rw [Finset.mul_sum]

Premises used: Finset.mul_sum
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
n : Type u_11
m : Type u_12
inst : Fintype n
inst_1 : Fintype m
inst_2 : DecidableEq n
inst_3 : DecidableEq m
T : Type u_16
inst_4 : CommSemiring T
M : Matrix n m T
v : n → T
w : m → T
x : n
h : Membership.mem (γ := Finset n) univ x
⊢ Eq.{u_16 + 1} (α := T) (∑ j : m, v x •> w j •> M x j) (∑ i : m, v x * (M x i * w i))

Tactic:
Finset.sum_congr rfl fun _ _ => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
n : Type u_11
m : Type u_12
inst : Fintype n
inst_1 : Fintype m
inst_2 : DecidableEq n
inst_3 : DecidableEq m
T : Type u_16
inst_4 : CommSemiring T
M : Matrix n m T
v : n → T
w : m → T
x : n
h : Membership.mem (γ := Finset n) univ x
refine : ∀ (x_1 : m), Membership.mem (γ := Finset m) univ x_1 → v x •> w x_1 •> M x x_1 = v x * (M x x_1 * w x_1)
⊢ Eq.{u_16 + 1} (α := T) (∑ j : m, v x •> w j •> M x j) (∑ i : m, v x * (M x i * w i))

Tactic:
refine Finset.sum_congr rfl fun _ _ => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
n : Type u_11
m : Type u_12
inst : Fintype n
inst_1 : Fintype m
inst_2 : DecidableEq n
inst_3 : DecidableEq m
T : Type u_16
inst_4 : CommSemiring T
M : Matrix n m T
v : n → T
w : m → T
x : n
h : Membership.mem (γ := Finset n) univ x
x_1 : m
h_1 : Membership.mem (γ := Finset m) univ x_1
rw : v x * w x_1 •> M x x_1 = v x * (M x x_1 * w x_1)
rw₁ : v x * (w x_1 * M x x_1) = v x * (M x x_1 * w x_1)
rw₂ : v x * (M x x_1 * w x_1) = v x * (M x x_1 * w x_1)
rw₃ rw₄ : v x * M x x_1 * w x_1 = v x * M x x_1 * w x_1
⊢ v x •> w x_1 •> M x x_1 = v x * (M x x_1 * w x_1)

Tactic:
rw [smul_eq_mul, smul_eq_mul, mul_comm (w _), ← mul_assoc]

Premises used: mul_assoc, mul_comm, smul_eq_mul
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid N₂
inst_2 : Module R N₂
inst_3 : Semiring R₁
inst_4 : Semiring R₂
inst_5 : Semiring S₁
inst_6 : Semiring S₂
inst_7 : Module S₁ N₂
inst_8 : Module S₂ N₂
inst_9 : SMulCommClass S₁ R N₂
inst_10 : SMulCommClass S₂ R N₂
inst_11 : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst_12 : Fintype n
inst_13 : Fintype m
inst_14 : DecidableEq n
inst_15 : DecidableEq m
M : Matrix n m N₂
i : n
j : m
⊢ ((((((toLinearMapₛₗ₂' R σ₁ σ₂ : Matrix n m N₂ ≃ₗ[R] (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂) :
                    (a : Matrix n m N₂) → (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂)
                  M :
                (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂) :
              (a : n → R₁) → (m → R₂) →ₛₗ[σ₂] N₂)
            (Pi.single (M := fun (a : n) ↦ R₁) i 1) :
          (m → R₂) →ₛₗ[σ₂] N₂) :
        (a : m → R₂) → N₂)
      (Pi.single (M := fun (a : m) ↦ R₂) j 1) =
    M i j

Tactic:
Matrix.toLinearMap₂'Aux_single σ₁ σ₂ M i j

Premises used: Matrix.toLinearMap₂'Aux_single
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid N₂
inst_2 : Module R N₂
inst_3 : Fintype n
inst_4 : Fintype m
inst_5 : DecidableEq n
inst_6 : DecidableEq m
M : Matrix n m N₂
i : n
j : m
⊢ ((((((toLinearMap₂' R : Matrix n m N₂ ≃ₗ[R] (n → ℕ) →ₗ[ℕ] LinearMap.{0, 0, u_12, u_10} (RingHom.id ℕ) (m → ℕ) N₂) :
                    (a : Matrix n m N₂) → (n → ℕ) →ₗ[ℕ] (m → ℕ) →ₗ[ℕ] N₂)
                  M :
                (n → ℕ) →ₗ[ℕ] LinearMap.{0, 0, u_12, u_10} (RingHom.id ℕ) (m → ℕ) N₂) :
              (a : n → ℕ) → (m → ℕ) →ₗ[ℕ] N₂)
            (Pi.single (M := fun (a : n) ↦ ℕ) i 1) :
          LinearMap.{0, 0, u_12, u_10} (RingHom.id ℕ) (m → ℕ) N₂) :
        (a : m → ℕ) → N₂)
      (Pi.single (M := fun (a : m) ↦ ℕ) j 1) =
    M i j

Tactic:
Matrix.toLinearMap₂'Aux_single _ _ M i j

Premises used: Matrix.toLinearMap₂'Aux_single
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid N₂
inst_2 : Module R N₂
inst_3 : Semiring R₁
inst_4 : Semiring R₂
inst_5 : Semiring S₁
inst_6 : Semiring S₂
inst_7 : Module S₁ N₂
inst_8 : Module S₂ N₂
inst_9 : SMulCommClass S₁ R N₂
inst_10 : SMulCommClass S₂ R N₂
inst_11 : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst_12 : Fintype n
inst_13 : Fintype m
inst_14 : DecidableEq n
inst_15 : DecidableEq m
⊢ Eq (α := Matrix n m N₂ ≃ₗ[R] (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂)
    (LinearEquiv.symm (toMatrixₛₗ₂' R) : Matrix n m N₂ ≃ₗ[R] (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂)
    (toLinearMapₛₗ₂' R σ₁ σ₂ : Matrix n m N₂ ≃ₗ[R] (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂)

Tactic:
rfl

Premises used: Matrix.toLinearMapₛₗ₂', rfl