awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
n : Type u_11
m : Type u_12
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 m'
inst_6 : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
f : (m' → R) →ₗ[R] m → 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₁₂ id f) =
    HMul.hMul (α := Matrix n m R) (β := Matrix m 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 ∘ₗ id) :
        Matrix n m R)
      ((toMatrix' : (a : (m' → R) →ₗ[R] m → R) → Matrix m m' R) f : Matrix m 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.compl₂ f) =
    HMul.hMul (α := Matrix n m R) (β := Matrix m 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 :
        Matrix n m R)
      ((toMatrix' : (a : (m' → R) →ₗ[R] m → R) → Matrix m m' R) f : Matrix m m' R)

Tactic:
rw [← LinearMap.comp_id B, ← LinearMap.compl₁₂]

Premises used: LinearMap.comp_id, LinearMap.compl₁₂
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
n : Type u_11
m : Type u_12
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 m'
inst_6 : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
f : (m' → R) →ₗ[R] 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.compl₁₂ id f) =
    HMul.hMul (α := Matrix n m R) (β := Matrix m 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 ∘ₗ id) :
        Matrix n m R)
      ((toMatrix' : (a : (m' → R) →ₗ[R] m → R) → Matrix m m' R) f : Matrix m m' R)

Tactic:
simp
-- 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
M : Matrix n' n R
N : Matrix m m' R
⊢ HMul.hMul (β := Matrix n m R) 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 :
          Matrix n m R) *
      N =
    ((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₁₂ ((toLin' : (a : Matrix n n' R) → (n' → R) →ₗ[R] n → R) Mᵀ)
        ((toLin' : (a : Matrix m m' R) → (m' → R) →ₗ[R] m → R) N))

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
M : Matrix n' n R
⊢ HMul.hMul (β := Matrix n m R) 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 :
        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 ∘ₗ (toLin' : (a : Matrix n n' R) → (n' → R) →ₗ[R] n → R) Mᵀ)

Tactic:
simp only [B.toMatrix₂'_comp, transpose_transpose, toMatrix'_toLin']

Premises used: Matrix.transpose_transpose, LinearMap.toMatrix'_toLin', LinearMap.toMatrix₂'_comp
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
n : Type u_11
m : Type u_12
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 m'
inst_6 : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
M : Matrix m m' R
⊢ HMul.hMul (α := 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 :
        Matrix n m R)
      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₂ (σ₄₂ := RingHom.id R) ((toLin' : (a : Matrix m m' R) → (m' → R) →ₗ[R] m → R) M))

Tactic:
simp only [B.toMatrix₂'_compl₂, toMatrix'_toLin']

Premises used: LinearMap.toMatrix'_toLin', LinearMap.toMatrix₂'_compl₂
-- 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'
M : Matrix n m R
P : Matrix n n' R
Q : Matrix m m' R
⊢ Eq (α := 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)
        (compl₁₂ (Mₗ := n → R) (N := m → R)
          (((toLinearMap₂' R : Matrix n m R ≃ₗ[R] (n → R) →ₗ[R] (m → R) →ₗ[R] R) :
              (a : Matrix n m R) → (n → R) →ₗ[R] (m → R) →ₗ[R] R)
            M)
          ((toLin' : (a : Matrix n n' R) → (n' → R) →ₗ[R] n → R) P)
          ((toLin' : (a : Matrix m m' R) → (m' → R) →ₗ[R] m → R) Q)) :
      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)
        (((toLinearMap₂' R : Matrix n' m' R ≃ₗ[R] (n' → R) →ₗ[R] (m' → R) →ₗ[R] R) :
            (a : Matrix n' m' R) → (n' → R) →ₗ[R] (m' → R) →ₗ[R] R)
          (Pᵀ * M * Q)) :
      Matrix n' m' R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
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 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₂
σ₁ σ₂ : R →+* R
inst_7 : Fintype n
inst_8 : Fintype m
inst_9 : DecidableEq m
inst_10 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
B : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂
i : n
j : m
⊢ Eq.{u_10 + 1} (α := N₂) ((toMatrix₂ b₁ b₂ : (a : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂) → Matrix n m N₂) B i j : N₂)
    ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] N₂) ((b₁ : (a : n) → M₁) i) : M₂ →ₛₗ[σ₂] N₂) : (a : M₂) → N₂)
        ((b₂ : (a : m) → M₂) j : M₂) :
      N₂)

Tactic:
simp only [toMatrix₂, LinearEquiv.trans_apply, toMatrixₛₗ₂'_apply, LinearEquiv.arrowCongr_apply,
    Basis.equivFun_symm_apply, Pi.single_apply, ite_smul, one_smul, zero_smul, sum_ite_eq',
    mem_univ, ↓reduceIte, LinearEquiv.refl_apply]

Premises used: Finset.mem_univ, Module.Basis.equivFun_symm_apply, Finset.sum_ite_eq', Pi.single_apply, LinearMap.toMatrix₂, LinearEquiv.trans_apply, LinearEquiv.arrowCongr_apply, one_smul, zero_smul, LinearEquiv.refl_apply, reduceIte, ite_smul, LinearMap.toMatrixₛₗ₂'_apply
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
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 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₂
σ₁ : R →+* R
inst_7 : Fintype n
inst_8 : Fintype m
inst_9 : DecidableEq m
inst_10 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
M : Matrix n m N₂
x : M₁
y : M₂
⊢ Eq.{u_10 + 1} (α := N₂)
    ((((((toLinearMapₛₗ₂ σ₁ b₁ b₂ : (a : Matrix n m N₂) → M₁ →ₛₗ[σ₁] M₂ →ₗ[R] N₂) M : M₁ →ₛₗ[σ₁] M₂ →ₗ[R] N₂) :
                (a : M₁) → M₂ →ₗ[R] N₂)
              x :
            M₂ →ₗ[R] N₂) :
          (a : M₂) → N₂)
        y :
      N₂)
    (∑ i : n,
        ∑ j : m,
          ((σ₁ : (a : R) → R) ((((b₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) i : R) : R) •>
            ((((b₂.repr : (a : M₂) → m →₀ R) y : m →₀ R) : (a : m) → R) j : R) •> M i j :
      N₂)

Tactic:
Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ =>
    smul_algebra_smul_comm (σ₁ ((Basis.equivFun b₁) x _))
    ((RingHom.id R) ((Basis.equivFun b₂) y _)) (M _ _)

Premises used: Multiset.sum, Multiset.foldr, smul_algebra_smul_comm, RingHom.id, DFunLike.coe, Finset.sum_congr, Finset.sum, rfl, Module.Basis.equivFun
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
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 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₂
inst_7 : Fintype n
inst_8 : Fintype m
inst_9 : DecidableEq m
inst_10 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
M : Matrix n m N₂
x : M₁
y : M₂
⊢ Eq.{u_10 + 1} (α := N₂)
    ((((((toLinearMap₂ b₁ b₂ : (a : Matrix n m N₂) → M₁ →ₗ[R] M₂ →ₗ[R] N₂) M : M₁ →ₗ[R] M₂ →ₗ[R] N₂) :
                (a : M₁) → M₂ →ₗ[R] N₂)
              x :
            M₂ →ₗ[R] N₂) :
          (a : M₂) → N₂)
        y :
      N₂)
    (∑ i : n,
        ∑ j : m,
          ((((b₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) i : R) •>
            ((((b₂.repr : (a : M₂) → m →₀ R) y : m →₀ R) : (a : m) → R) j : R) •> M i j :
      N₂)

Tactic:
Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ =>
    smul_algebra_smul_comm ((RingHom.id R) ((Basis.equivFun b₁) x _))
    ((RingHom.id R) ((Basis.equivFun b₂) y _)) (M _ _)

Premises used: Multiset.sum, Multiset.foldr, smul_algebra_smul_comm, RingHom.id, DFunLike.coe, Finset.sum_congr, Finset.sum, rfl, Module.Basis.equivFun
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
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 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₂
σ₁ : R →+* R
inst_7 : Fintype n
inst_8 : Fintype m
inst_9 : DecidableEq m
inst_10 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
M : Matrix n m N₂
i : n
j : m
simp :
  ∑ x : n,
      ∑ x_1 : m,
        ((σ₁ : (a : R) → R) ((Finsupp.single i 1 : (a : n) → R) x : R) : R) •>
          ((Finsupp.single j 1 : (a : m) → R) x_1 : R) •> M x x_1 =
    M i j
⊢ (((((toLinearMapₛₗ₂ σ₁ b₁ b₂ : (a : Matrix n m N₂) → M₁ →ₛₗ[σ₁] M₂ →ₗ[R] N₂) M : M₁ →ₛₗ[σ₁] M₂ →ₗ[R] N₂) :
              (a : M₁) → M₂ →ₗ[R] N₂)
            ((b₁ : (a : n) → M₁) i) :
          M₂ →ₗ[R] N₂) :
        (a : M₂) → N₂)
      ((b₂ : (a : m) → M₂) j : M₂) =
    M i j

Tactic:
simp only [toLinearMapₛₗ₂_apply, Basis.repr_self]

Premises used: Matrix.toLinearMapₛₗ₂_apply, Module.Basis.repr_self
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
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 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₂
σ₁ : R →+* R
inst_7 : Fintype n
inst_8 : Fintype m
inst_9 : DecidableEq m
inst_10 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
M : Matrix n m N₂
i : n
j : m
⊢ Membership.mem (γ := Finset n) univ i

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
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 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₂
σ₁ : R →+* R
inst_7 : Fintype n
inst_8 : Fintype m
inst_9 : DecidableEq m
inst_10 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
M : Matrix n m N₂
i : n
j : m
k : n
h : Membership.mem (γ := Finset n) univ k
hk : k ≠ i
⊢ Eq.{u_10 + 1} (α := N₂)
    (∑ x : m,
      ((σ₁ : (a : R) → R) ((Finsupp.single i 1 : (a : n) → R) k : R) : R) •>
        ((Finsupp.single j 1 : (a : m) → R) x : R) •> M k x)
    0

Tactic:
simp [hk]
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
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 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₂
σ₁ : R →+* R
inst_7 : Fintype n
inst_8 : Fintype m
inst_9 : DecidableEq m
inst_10 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
M : Matrix n m N₂
i : n
j : m
⊢ Membership.mem (γ := Finset m) univ j

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
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 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₂
σ₁ : R →+* R
inst_7 : Fintype n
inst_8 : Fintype m
inst_9 : DecidableEq m
inst_10 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
M : Matrix n m N₂
i : n
j k : m
h : Membership.mem (γ := Finset m) univ k
hk : k ≠ j
⊢ ((σ₁ : (a : R) → R) ((Finsupp.single i 1 : (a : n) → R) i : R) : R) •>
      ((Finsupp.single j 1 : (a : m) → R) k : R) •> M i k =
    0

Tactic:
simp [hk]
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
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 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₂
σ₁ : R →+* R
inst_7 : Fintype n
inst_8 : Fintype m
inst_9 : DecidableEq m
inst_10 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
M : Matrix n m N₂
i : n
j : m
rw :
  ((σ₁ : (a : R) → R) ((Finsupp.single i 1 : (a : n) → R) i : R) : R) •>
      ((Finsupp.single j 1 : (a : m) → R) j : R) •> M i j =
    M i j
⊢ ∑ x : n,
      ∑ x_1 : m,
        ((σ₁ : (a : R) → R) ((Finsupp.single i 1 : (a : n) → R) x : R) : R) •>
          ((Finsupp.single j 1 : (a : m) → R) x_1 : R) •> M x x_1 =
    M i j

Tactic:
rw [Finset.sum_eq_single_of_mem i (by simp) fun k _ hk ↦ by simp [hk],
    Finset.sum_eq_single_of_mem j (by simp) fun k _ hk ↦ by simp [hk]]

Premises used: Finset.sum_eq_single_of_mem
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
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 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₂
σ₁ : R →+* R
inst_7 : Fintype n
inst_8 : Fintype m
inst_9 : DecidableEq m
inst_10 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
M : Matrix n m N₂
i : n
j : m
⊢ ((σ₁ : (a : R) → R) ((Finsupp.single i 1 : (a : n) → R) i : R) : R) •>
      ((Finsupp.single j 1 : (a : m) → R) j : R) •> M i j =
    M i j

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
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 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₂
inst_7 : Fintype n
inst_8 : Fintype m
inst_9 : DecidableEq m
inst_10 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
M : Matrix n m N₂
i : n
j : m
⊢ (((((toLinearMap₂ b₁ b₂ : (a : Matrix n m N₂) → M₁ →ₗ[R] M₂ →ₗ[R] N₂) M : M₁ →ₗ[R] M₂ →ₗ[R] N₂) :
              (a : M₁) → M₂ →ₗ[R] N₂)
            ((b₁ : (a : n) → M₁) i) :
          M₂ →ₗ[R] N₂) :
        (a : M₂) → N₂)
      ((b₂ : (a : m) → M₂) j : M₂) =
    M i j

Tactic:
toLinearMapₛₗ₂_apply_basis ..

Premises used: Matrix.toLinearMapₛₗ₂_apply_basis
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
σ₁ σ₂ : R →+* R
inst_5 : Fintype n
inst_6 : Fintype m
inst_7 : DecidableEq m
inst_8 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
B : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R
x : n → R
y : m → R
simp :
  Eq.{u_1 + 1} (α := R)
    (∑ x_1 : n,
      ∑ i : m,
        HMul.hMul (α := R) ((σ₁ : (a : R) → R) (x x_1) : R)
          (HMul.hMul (α := R) (β := R) ((σ₂ : (a : R) → R) (y i) : R)
            ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) x_1) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
                ((b₂ : (a : m) → M₂) i : M₂) :
              R)))
    (∑ x_1 : m,
      ∑ i : n,
        HMul.hMul (α := R) ((σ₂ : (a : R) → R) (y x_1) : R)
          (HMul.hMul (α := R) (β := R) ((σ₁ : (a : R) → R) (x i) : R)
            ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) i) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
                ((b₂ : (a : m) → M₂) x_1 : M₂) :
              R)))
⊢ Eq (α := R)
    ((⇑σ₁ : (a : R) → R) ∘ x ⬝ᵥ
        (toMatrix₂ b₁ b₂ : (a : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R) → Matrix n m R) B *ᵥ (⇑σ₂ : (a : R) → R) ∘ y :
      R)
    ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁.equivFun.symm : (a : n → R) → M₁) x) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
        ((b₂.equivFun.symm : (a : m → R) → M₂) y : M₂) :
      R)

Tactic:
simp only [dotProduct, Function.comp_apply, Function.comp_def, mulVec_eq_sum, op_smul_eq_smul,
    Finset.sum_apply, Pi.smul_apply, transpose_apply, toMatrix₂_apply, smul_eq_mul, mul_sum,
    Basis.equivFun_symm_apply, map_sum, map_smulₛₗ, coe_sum, LinearMap.smul_apply]

Premises used: Finset.mul_sum, Module.Basis.equivFun_symm_apply, dotProduct, LinearMap.smul_apply, Finset.sum_apply, MulActionSemiHomClass.map_smulₛₗ, LinearMap.coe_sum, map_sum, Function.comp_def, Matrix.mulVec_eq_sum, LinearMap.toMatrix₂_apply, Function.comp_apply, smul_eq_mul, Matrix.transpose_apply, IsCentralScalar.op_smul_eq_smul, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
σ₁ σ₂ : R →+* R
inst_5 : Fintype n
inst_6 : Fintype m
inst_7 : DecidableEq m
inst_8 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
B : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R
x : n → R
y : m → R
rw :
  Eq.{u_1 + 1} (α := R)
    (∑ y_1 : m,
      ∑ x_1 : n,
        HMul.hMul (α := R) ((σ₁ : (a : R) → R) (x x_1) : R)
          (HMul.hMul (α := R) (β := R) ((σ₂ : (a : R) → R) (y y_1) : R)
            ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) x_1) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
                ((b₂ : (a : m) → M₂) y_1 : M₂) :
              R)))
    (∑ x_1 : m,
      ∑ i : n,
        HMul.hMul (α := R) ((σ₂ : (a : R) → R) (y x_1) : R)
          (HMul.hMul (α := R) (β := R) ((σ₁ : (a : R) → R) (x i) : R)
            ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) i) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
                ((b₂ : (a : m) → M₂) x_1 : M₂) :
              R)))
⊢ Eq.{u_1 + 1} (α := R)
    (∑ x_1 : n,
      ∑ i : m,
        HMul.hMul (α := R) ((σ₁ : (a : R) → R) (x x_1) : R)
          (HMul.hMul (α := R) (β := R) ((σ₂ : (a : R) → R) (y i) : R)
            ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) x_1) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
                ((b₂ : (a : m) → M₂) i : M₂) :
              R)))
    (∑ x_1 : m,
      ∑ i : n,
        HMul.hMul (α := R) ((σ₂ : (a : R) → R) (y x_1) : R)
          (HMul.hMul (α := R) (β := R) ((σ₁ : (a : R) → R) (x i) : R)
            ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) i) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
                ((b₂ : (a : m) → M₂) x_1 : M₂) :
              R)))

Tactic:
rw [Finset.sum_comm]

Premises used: Finset.sum_comm
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
σ₁ σ₂ : R →+* R
inst_5 : Fintype n
inst_6 : Fintype m
inst_7 : DecidableEq m
inst_8 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
B : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R
x : n → R
y : m → R
⊢ Eq.{u_1 + 1} (α := R)
    (∑ y_1 : m,
      ∑ x_1 : n,
        HMul.hMul (α := R) ((σ₁ : (a : R) → R) (x x_1) : R)
          (HMul.hMul (α := R) (β := R) ((σ₂ : (a : R) → R) (y y_1) : R)
            ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) x_1) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
                ((b₂ : (a : m) → M₂) y_1 : M₂) :
              R)))
    (∑ x_1 : m,
      ∑ i : n,
        HMul.hMul (α := R) ((σ₂ : (a : R) → R) (y x_1) : R)
          (HMul.hMul (α := R) (β := R) ((σ₁ : (a : R) → R) (x i) : R)
            ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) i) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
                ((b₂ : (a : m) → M₂) x_1 : M₂) :
              R)))

Tactic:
Finset.sum_congr rfl (fun i _ ↦ Finset.sum_congr rfl fun j _ ↦ ?_)

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
σ₁ σ₂ : R →+* R
inst_5 : Fintype n
inst_6 : Fintype m
inst_7 : DecidableEq m
inst_8 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
B : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R
x : n → R
y : m → R
refine :
  ∀ (i : m),
    Membership.mem (γ := Finset m) univ i →
      ∀ (j : n),
        Membership.mem (γ := Finset n) univ j →
          HMul.hMul (α := R) ((σ₁ : (a : R) → R) (x j) : R)
              (HMul.hMul (α := R) (β := R) ((σ₂ : (a : R) → R) (y i) : R)
                ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) j) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
                    ((b₂ : (a : m) → M₂) i : M₂) :
                  R)) =
            HMul.hMul (α := R) ((σ₂ : (a : R) → R) (y i) : R)
              (HMul.hMul (α := R) (β := R) ((σ₁ : (a : R) → R) (x j) : R)
                ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) j) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
                    ((b₂ : (a : m) → M₂) i : M₂) :
                  R))
⊢ Eq.{u_1 + 1} (α := R)
    (∑ y_1 : m,
      ∑ x_1 : n,
        HMul.hMul (α := R) ((σ₁ : (a : R) → R) (x x_1) : R)
          (HMul.hMul (α := R) (β := R) ((σ₂ : (a : R) → R) (y y_1) : R)
            ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) x_1) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
                ((b₂ : (a : m) → M₂) y_1 : M₂) :
              R)))
    (∑ x_1 : m,
      ∑ i : n,
        HMul.hMul (α := R) ((σ₂ : (a : R) → R) (y x_1) : R)
          (HMul.hMul (α := R) (β := R) ((σ₁ : (a : R) → R) (x i) : R)
            ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) i) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
                ((b₂ : (a : m) → M₂) x_1 : M₂) :
              R)))

Tactic:
refine Finset.sum_congr rfl (fun i _ ↦ Finset.sum_congr rfl fun j _ ↦ ?_)

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
σ₁ σ₂ : R →+* R
inst_5 : Fintype n
inst_6 : Fintype m
inst_7 : DecidableEq m
inst_8 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
B : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R
x : n → R
y : m → R
i : m
h : Membership.mem (γ := Finset m) univ i
j : n
h_1 : Membership.mem (γ := Finset n) univ j
⊢ HMul.hMul (α := R) ((σ₁ : (a : R) → R) (x j) : R)
      (HMul.hMul (α := R) (β := R) ((σ₂ : (a : R) → R) (y i) : R)
        ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) j) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
            ((b₂ : (a : m) → M₂) i : M₂) :
          R)) =
    HMul.hMul (α := R) ((σ₂ : (a : R) → R) (y i) : R)
      (HMul.hMul (α := R) (β := R) ((σ₁ : (a : R) → R) (x j) : R)
        ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) j) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
            ((b₂ : (a : m) → M₂) i : M₂) :
          R))

Tactic:
ring