awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (α := ((n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂) ≃ₗ[R] Matrix n m N₂)
    (LinearEquiv.symm (toLinearMapₛₗ₂' R σ₁ σ₂) : ((n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂) ≃ₗ[R] Matrix n m N₂)
    (toMatrixₛₗ₂' R : ((n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂) ≃ₗ[R] Matrix n m N₂)

Tactic:
(LinearMap.toMatrixₛₗ₂' R).symm_symm

Premises used: Matrix.toLinearMapₛₗ₂', LinearEquiv.symm_symm, 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
B : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂
⊢ ((toLinearMapₛₗ₂' R σ₁ σ₂ : Matrix n m N₂ ≃ₗ[R] (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂) :
        (a : Matrix n m N₂) → (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂)
      (((toMatrixₛₗ₂' R : ((n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂) ≃ₗ[R] Matrix n m N₂) :
          (a : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂) → Matrix n m N₂)
        B) =
    B

Tactic:
(Matrix.toLinearMapₛₗ₂' R σ₁ σ₂).apply_symm_apply B

Premises used: Matrix.toLinearMapₛₗ₂', LinearEquiv.apply_symm_apply
-- 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
B : (n → S₁) →ₗ[S₁] (m → S₂) →ₗ[S₂] N₂
⊢ ((toLinearMap₂' R : Matrix n m N₂ ≃ₗ[R] (n → S₁) →ₗ[S₁] (m → S₂) →ₗ[S₂] N₂) :
        (a : Matrix n m N₂) → (n → S₁) →ₗ[S₁] (m → S₂) →ₗ[S₂] N₂)
      (((toMatrix₂' R : ((n → S₁) →ₗ[S₁] (m → S₂) →ₗ[S₂] N₂) ≃ₗ[R] Matrix n m N₂) :
          (a : (n → S₁) →ₗ[S₁] (m → S₂) →ₗ[S₂] N₂) → Matrix n m N₂)
        B) =
    B

Tactic:
(Matrix.toLinearMap₂' R).apply_symm_apply B

Premises used: LinearEquiv.apply_symm_apply, Matrix.toLinearMap₂'
-- 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₂
⊢ ((toMatrixₛₗ₂' R : ((n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂) ≃ₗ[R] Matrix n m N₂) :
        (a : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂) → Matrix n m N₂)
      (((toLinearMapₛₗ₂' R σ₁ σ₂ : Matrix n m N₂ ≃ₗ[R] (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂) :
          (a : Matrix n m N₂) → (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂)
        M) =
    M

Tactic:
(LinearMap.toMatrixₛₗ₂' R).apply_symm_apply M

Premises used: LinearMap.toMatrixₛₗ₂', LinearEquiv.apply_symm_apply
-- 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₂
⊢ ((toMatrix₂' R : ((n → S₁) →ₗ[S₁] (m → S₂) →ₗ[S₂] N₂) ≃ₗ[R] Matrix n m N₂) :
        (a : (n → S₁) →ₗ[S₁] (m → S₂) →ₗ[S₂] N₂) → Matrix n m N₂)
      (((toLinearMap₂' R : Matrix n m N₂ ≃ₗ[R] (n → S₁) →ₗ[S₁] (m → S₂) →ₗ[S₂] N₂) :
          (a : Matrix n m N₂) → (n → S₁) →ₗ[S₁] (m → S₂) →ₗ[S₂] N₂)
        M) =
    M

Tactic:
(LinearMap.toMatrixₛₗ₂' R).apply_symm_apply M

Premises used: LinearMap.toMatrixₛₗ₂', LinearEquiv.apply_symm_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
B : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂
i : n
j : m
⊢ Eq.{u_10 + 1} (α := N₂)
    (((toMatrixₛₗ₂' R : ((n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂) ≃ₗ[R] Matrix n m N₂) :
          (a : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂) → Matrix n m N₂)
        B i j :
      N₂)
    ((((B : (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) :
      N₂)

Tactic:
rfl

Premises used: 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
B : (n → S₁) →ₗ[S₁] (m → S₂) →ₗ[S₂] N₂
i : n
j : m
⊢ Eq.{u_10 + 1} (α := N₂)
    (((toMatrix₂' R : ((n → S₁) →ₗ[S₁] (m → S₂) →ₗ[S₂] N₂) ≃ₗ[R] Matrix n m N₂) :
          (a : (n → S₁) →ₗ[S₁] (m → S₂) →ₗ[S₂] N₂) → Matrix n m N₂)
        B i j :
      N₂)
    ((((B : (a : n → S₁) → (m → S₂) →ₗ[S₂] N₂) (Pi.single (M := fun (a : n) ↦ S₁) i 1) : (m → S₂) →ₗ[S₂] N₂) :
          (a : m → S₂) → N₂)
        (Pi.single (M := fun (a : m) ↦ S₂) j 1) :
      N₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : DecidableEq m
inst_5 : Fintype n'
inst_6 : Fintype m'
inst_7 : DecidableEq n'
inst_8 : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
a :
  ∀ (i : n') (j : m'),
    ((toMatrix₂' R : ((n' → R) →ₗ[R] (m' → R) →ₗ[R] R) ≃ₗ[R] Matrix n' m' R) :
          (a : (n' → R) →ₗ[R] (m' → R) →ₗ[R] R) → Matrix n' m' R)
        (B.compl₁₂ l r) i j =
      HMul.hMul (β := Matrix m m' R)
        (HMul.hMul (α := Matrix n' n R) (β := Matrix n m R)
          ((toMatrix' : (a : (n' → R) →ₗ[R] n → R) → Matrix n n' R) l)ᵀ
          (((toMatrix₂' R : ((n → R) →ₗ[R] (m → R) →ₗ[R] R) ≃ₗ[R] Matrix n m R) :
                (a : (n → R) →ₗ[R] (m → R) →ₗ[R] R) → Matrix n m R)
              B :
            Matrix n m R))
        ((toMatrix' : (a : (m' → R) →ₗ[R] m → R) → Matrix m m' R) r : Matrix m m' R) i j
⊢ ((toMatrix₂' R : ((n' → R) →ₗ[R] (m' → R) →ₗ[R] R) ≃ₗ[R] Matrix n' m' R) :
        (a : (n' → R) →ₗ[R] (m' → R) →ₗ[R] R) → Matrix n' m' R)
      (B.compl₁₂ l r) =
    HMul.hMul (β := Matrix m m' R)
      (HMul.hMul (α := Matrix n' n R) (β := Matrix n m R) ((toMatrix' : (a : (n' → R) →ₗ[R] n → R) → Matrix n n' R) l)ᵀ
        (((toMatrix₂' R : ((n → R) →ₗ[R] (m → R) →ₗ[R] R) ≃ₗ[R] Matrix n m R) :
              (a : (n → R) →ₗ[R] (m → R) →ₗ[R] R) → Matrix n m R)
            B :
          Matrix n m R))
      ((toMatrix' : (a : (m' → R) →ₗ[R] m → R) → Matrix m m' R) r : Matrix m m' R)

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : DecidableEq m
inst_5 : Fintype n'
inst_6 : Fintype m'
inst_7 : DecidableEq n'
inst_8 : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
a :
  Eq.{u_16 + 1} (α := R)
    ((((B : (a : n → R) → (m → R) →ₗ[R] R) ((l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) i 1)) :
            (m → R) →ₗ[R] R) :
          (a : m → R) → R)
        ((r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1) : m → R) :
      R)
    (∑ x : m,
        ∑ i_1 : n,
          HMul.hMul (β := R)
            (HMul.hMul (α := R) (β := R)
              ((of : (a : n → n' → R) → Matrix n n' R)
                  (fun (i : n) (j : n') ↦ (l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) j 1) i) i_1 i :
                R)
              ((((B : (a : n → R) → (m → R) →ₗ[R] R) (Pi.single (M := fun (a : n) ↦ R) i_1 1) : (m → R) →ₗ[R] R) :
                    (a : m → R) → R)
                  (Pi.single (M := fun (a : m) ↦ R) x 1) :
                R))
            ((of : (a : m → m' → R) → Matrix m m' R)
                (fun (i : m) (j : m') ↦ (r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1) i) x j :
              R) :
      R)
⊢ ((toMatrix₂' R : ((n' → R) →ₗ[R] (m' → R) →ₗ[R] R) ≃ₗ[R] Matrix n' m' R) :
        (a : (n' → R) →ₗ[R] (m' → R) →ₗ[R] R) → Matrix n' m' R)
      (B.compl₁₂ l r) i j =
    HMul.hMul (β := Matrix m m' R)
      (HMul.hMul (α := Matrix n' n R) (β := Matrix n m R) ((toMatrix' : (a : (n' → R) →ₗ[R] n → R) → Matrix n n' R) l)ᵀ
        (((toMatrix₂' R : ((n → R) →ₗ[R] (m → R) →ₗ[R] R) ≃ₗ[R] Matrix n m R) :
              (a : (n → R) →ₗ[R] (m → R) →ₗ[R] R) → Matrix n m R)
            B :
          Matrix n m R))
      ((toMatrix' : (a : (m' → R) →ₗ[R] m → R) → Matrix m m' R) r : Matrix m m' R) i j

Tactic:
simp only [LinearMap.toMatrix₂'_apply, LinearMap.compl₁₂_apply, transpose_apply, Matrix.mul_apply,
    LinearMap.toMatrix', LinearEquiv.coe_mk, LinearMap.coe_mk, AddHom.coe_mk, sum_mul]

Premises used: LinearMap.coe_mk, LinearEquiv.coe_mk, Matrix.mul_apply, LinearMap.toMatrix', LinearMap.compl₁₂_apply, AddHom.coe_mk, Matrix.transpose_apply, LinearMap.toMatrix₂'_apply, Finset.sum_mul
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : DecidableEq m
inst_5 : Fintype n'
inst_6 : Fintype m'
inst_7 : DecidableEq n'
inst_8 : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
a :
  Eq.{u_16 + 1} (α := R)
    ((((B : (a : n → R) → (m → R) →ₗ[R] R) ((l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) i 1)) :
            (m → R) →ₗ[R] R) :
          (a : m → R) → R)
        ((r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1) : m → R) :
      R)
    (∑ y : n,
        ∑ x : m,
          HMul.hMul (β := R)
            (HMul.hMul (α := R) (β := R)
              ((of : (a : n → n' → R) → Matrix n n' R)
                  (fun (i : n) (j : n') ↦ (l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) j 1) i) y i :
                R)
              ((((B : (a : n → R) → (m → R) →ₗ[R] R) (Pi.single (M := fun (a : n) ↦ R) y 1) : (m → R) →ₗ[R] R) :
                    (a : m → R) → R)
                  (Pi.single (M := fun (a : m) ↦ R) x 1) :
                R))
            ((of : (a : m → m' → R) → Matrix m m' R)
                (fun (i : m) (j : m') ↦ (r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1) i) x j :
              R) :
      R)
⊢ Eq.{u_16 + 1} (α := R)
    ((((B : (a : n → R) → (m → R) →ₗ[R] R) ((l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) i 1)) :
            (m → R) →ₗ[R] R) :
          (a : m → R) → R)
        ((r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1) : m → R) :
      R)
    (∑ x : m,
        ∑ i_1 : n,
          HMul.hMul (β := R)
            (HMul.hMul (α := R) (β := R)
              ((of : (a : n → n' → R) → Matrix n n' R)
                  (fun (i : n) (j : n') ↦ (l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) j 1) i) i_1 i :
                R)
              ((((B : (a : n → R) → (m → R) →ₗ[R] R) (Pi.single (M := fun (a : n) ↦ R) i_1 1) : (m → R) →ₗ[R] R) :
                    (a : m → R) → R)
                  (Pi.single (M := fun (a : m) ↦ R) x 1) :
                R))
            ((of : (a : m → m' → R) → Matrix m m' R)
                (fun (i : m) (j : m') ↦ (r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1) i) x j :
              R) :
      R)

Tactic:
rw [sum_comm]

Premises used: Finset.sum_comm
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : DecidableEq m
inst_5 : Fintype n'
inst_6 : Fintype m'
inst_7 : DecidableEq n'
inst_8 : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
rw :
  Finsupp.sum
    ((Basis.repr (Pi.basisFun R n) : (a : n → R) → n →₀ R)
      ((l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) i 1)))
    fun (i : n) (xi : R) ↦
    Finsupp.sum
      ((Basis.repr (Pi.basisFun R m) : (a : m → R) → m →₀ R)
        ((r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1)))
      fun (j : m) (yj : R) ↦
      xi •>
        yj •>
          ((((B : (a : n → R) → (m → R) →ₗ[R] R) ((Pi.basisFun R n : (a : n) → n → R) i) : (m → R) →ₗ[R] R) :
                (a : m → R) → R)
              ((Pi.basisFun R m : (a : m) → m → R) j : m → R) :
            R)
| ((((B : (a : n → R) → (m → R) →ₗ[R] R) ((l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) i 1)) :
          (m → R) →ₗ[R] R) :
        (a : m → R) → R)
      ((r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1) : m → R) :
    R)

Tactic:
rw [← LinearMap.sum_repr_mul_repr_mul (Pi.basisFun R n) (Pi.basisFun R m) (l _) (r _)]

Premises used: Pi.basisFun, DFunLike.coe, LinearMap.sum_repr_mul_repr_mul
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : DecidableEq m
inst_5 : Fintype n'
inst_6 : Fintype m'
inst_7 : DecidableEq n'
inst_8 : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
a :
  Eq.{u_16 + 1} (α := R)
    (Finsupp.sum
      ((Basis.repr (Pi.basisFun R n) : (a : n → R) → n →₀ R)
        ((l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) i 1)))
      fun (i : n) (xi : R) ↦
      Finsupp.sum
        ((Basis.repr (Pi.basisFun R m) : (a : m → R) → m →₀ R)
          ((r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1)))
        fun (j : m) (yj : R) ↦
        xi •>
          yj •>
            ((((B : (a : n → R) → (m → R) →ₗ[R] R) ((Pi.basisFun R n : (a : n) → n → R) i) : (m → R) →ₗ[R] R) :
                  (a : m → R) → R)
                ((Pi.basisFun R m : (a : m) → m → R) j : m → R) :
              R))
    (∑ y : n,
      ∑ x : m,
        HMul.hMul (β := R)
          (HMul.hMul (α := R) (β := R)
            ((of : (a : n → n' → R) → Matrix n n' R)
                (fun (i : n) (j : n') ↦ (l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) j 1) i) y i :
              R)
            ((((B : (a : n → R) → (m → R) →ₗ[R] R) (Pi.single (M := fun (a : n) ↦ R) y 1) : (m → R) →ₗ[R] R) :
                  (a : m → R) → R)
                (Pi.single (M := fun (a : m) ↦ R) x 1) :
              R))
          ((of : (a : m → m' → R) → Matrix m m' R)
              (fun (i : m) (j : m') ↦ (r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1) i) x j :
            R))
⊢ Eq.{u_16 + 1} (α := R)
    ((((B : (a : n → R) → (m → R) →ₗ[R] R) ((l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) i 1)) :
            (m → R) →ₗ[R] R) :
          (a : m → R) → R)
        ((r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1) : m → R) :
      R)
    (∑ y : n,
        ∑ x : m,
          HMul.hMul (β := R)
            (HMul.hMul (α := R) (β := R)
              ((of : (a : n → n' → R) → Matrix n n' R)
                  (fun (i : n) (j : n') ↦ (l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) j 1) i) y i :
                R)
              ((((B : (a : n → R) → (m → R) →ₗ[R] R) (Pi.single (M := fun (a : n) ↦ R) y 1) : (m → R) →ₗ[R] R) :
                    (a : m → R) → R)
                  (Pi.single (M := fun (a : m) ↦ R) x 1) :
                R))
            ((of : (a : m → m' → R) → Matrix m m' R)
                (fun (i : m) (j : m') ↦ (r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1) i) x j :
              R) :
      R)

Tactic:
conv_lhs => rw [← LinearMap.sum_repr_mul_repr_mul (Pi.basisFun R n) (Pi.basisFun R m) (l _) (r _)]

Premises used: Pi.basisFun, DFunLike.coe, LinearMap.sum_repr_mul_repr_mul
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : DecidableEq m
inst_5 : Fintype n'
inst_6 : Fintype m'
inst_7 : DecidableEq n'
inst_8 : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
i' : n
j' : m
⊢ ((((Basis.repr (Pi.basisFun R n) : (a : n → R) → n →₀ R)
                ((l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) i 1)) :
              n →₀ R) :
            (a : n) → R)
          i' :
        R) •>
      ((((Basis.repr (Pi.basisFun R m) : (a : m → R) → m →₀ R)
                  ((r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1)) :
                m →₀ R) :
              (a : m) → R)
            j' :
          R) •>
        ((((B : (a : n → R) → (m → R) →ₗ[R] R) ((Pi.basisFun R n : (a : n) → n → R) i') : (m → R) →ₗ[R] R) :
              (a : m → R) → R)
            ((Pi.basisFun R m : (a : m) → m → R) j' : m → R) :
          R) =
    HMul.hMul (β := R)
      (HMul.hMul (α := R) (β := R)
        ((of : (a : n → n' → R) → Matrix n n' R)
            (fun (i : n) (j : n') ↦ (l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) j 1) i) i' i :
          R)
        ((((B : (a : n → R) → (m → R) →ₗ[R] R) (Pi.single (M := fun (a : n) ↦ R) i' 1) : (m → R) →ₗ[R] R) :
              (a : m → R) → R)
            (Pi.single (M := fun (a : m) ↦ R) j' 1) :
          R))
      ((of : (a : m → m' → R) → Matrix m m' R)
          (fun (i : m) (j : m') ↦ (r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1) i) j' j :
        R)

Tactic:
simp only [smul_eq_mul, Pi.basisFun_repr, mul_assoc, mul_comm, mul_left_comm,
        Pi.basisFun_apply, of_apply]

Premises used: mul_assoc, mul_left_comm, Matrix.of_apply, Pi.basisFun_apply, mul_comm, smul_eq_mul, Pi.basisFun_repr
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : DecidableEq m
inst_5 : Fintype n'
inst_6 : Fintype m'
inst_7 : DecidableEq n'
inst_8 : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
i' : n
i_1 : m
⊢ ((((Basis.repr (Pi.basisFun R n) : (a : n → R) → n →₀ R)
                ((l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) i 1)) :
              n →₀ R) :
            (a : n) → R)
          i' :
        R) •>
      0 •>
        ((((B : (a : n → R) → (m → R) →ₗ[R] R) ((Pi.basisFun R n : (a : n) → n → R) i') : (m → R) →ₗ[R] R) :
              (a : m → R) → R)
            ((Pi.basisFun R m : (a : m) → m → R) i_1 : m → R) :
          R) =
    0

Tactic:
simp only [zero_smul, smul_zero]

Premises used: smul_zero, zero_smul
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : DecidableEq m
inst_5 : Fintype n'
inst_6 : Fintype m'
inst_7 : DecidableEq n'
inst_8 : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
i_1 : n
⊢ Eq.{u_16 + 1} (α := R)
    (Finsupp.sum
      ((Basis.repr (Pi.basisFun R m) : (a : m → R) → m →₀ R)
        ((r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1)))
      fun (j : m) (yj : R) ↦
      0 •>
        yj •>
          ((((B : (a : n → R) → (m → R) →ₗ[R] R) ((Pi.basisFun R n : (a : n) → n → R) i_1) : (m → R) →ₗ[R] R) :
                (a : m → R) → R)
              ((Pi.basisFun R m : (a : m) → m → R) j : m → R) :
            R))
    0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
n : Type u_11
m : Type u_12
n' : Type u_13
R : Type u_16
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : DecidableEq m
inst_5 : Fintype n'
inst_6 : DecidableEq n'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
f : (n' → R) →ₗ[R] n → R
rw :
  ((toMatrix₂' R : ((n' → R) →ₗ[R] (m → R) →ₗ[R] R) ≃ₗ[R] Matrix n' m R) :
        (a : (n' → R) →ₗ[R] (m → R) →ₗ[R] R) → Matrix n' m R)
      (B.compl₁₂ f id) =
    HMul.hMul (α := Matrix n' n R) (β := Matrix n m R) ((toMatrix' : (a : (n' → R) →ₗ[R] n → R) → Matrix n n' R) f)ᵀ
      (((toMatrix₂' R : ((n → R) →ₗ[R] (m → R) →ₗ[R] R) ≃ₗ[R] Matrix n m R) :
            (a : (n → R) →ₗ[R] (m → R) →ₗ[R] R) → Matrix n m R)
          B :
        Matrix n m R)
⊢ ((toMatrix₂' R : ((n' → R) →ₗ[R] (m → R) →ₗ[R] R) ≃ₗ[R] Matrix n' m R) :
        (a : (n' → R) →ₗ[R] (m → R) →ₗ[R] R) → Matrix n' m R)
      (B ∘ₗ f) =
    HMul.hMul (α := Matrix n' n R) (β := Matrix n m R) ((toMatrix' : (a : (n' → R) →ₗ[R] n → R) → Matrix n n' R) f)ᵀ
      (((toMatrix₂' R : ((n → R) →ₗ[R] (m → R) →ₗ[R] R) ≃ₗ[R] Matrix n m R) :
            (a : (n → R) →ₗ[R] (m → R) →ₗ[R] R) → Matrix n m R)
          B :
        Matrix n m R)

Tactic:
rw [← LinearMap.compl₂_id (B.comp f), ← LinearMap.compl₁₂]

Premises used: LinearMap.comp, LinearMap.compl₂_id, LinearMap.compl₁₂
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
n : Type u_11
m : Type u_12
n' : Type u_13
R : Type u_16
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : DecidableEq m
inst_5 : Fintype n'
inst_6 : DecidableEq n'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
f : (n' → R) →ₗ[R] n → R
⊢ ((toMatrix₂' R : ((n' → R) →ₗ[R] (m → R) →ₗ[R] R) ≃ₗ[R] Matrix n' m R) :
        (a : (n' → R) →ₗ[R] (m → R) →ₗ[R] R) → Matrix n' m R)
      (B.compl₁₂ f id) =
    HMul.hMul (α := Matrix n' n R) (β := Matrix n m R) ((toMatrix' : (a : (n' → R) →ₗ[R] n → R) → Matrix n n' R) f)ᵀ
      (((toMatrix₂' R : ((n → R) →ₗ[R] (m → R) →ₗ[R] R) ≃ₗ[R] Matrix n m R) :
            (a : (n → R) →ₗ[R] (m → R) →ₗ[R] R) → Matrix n m R)
          B :
        Matrix n m R)

Tactic:
simp