awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂
⊢ (toMatrix₂ b₁ b₂ : (a : M₁ →ₛₗ[σ₁] M₂ →ₗ[R] N₂) → Matrix n m N₂)
      ((toLinearMapₛₗ₂ σ₁ b₁ b₂ : (a : Matrix n m N₂) → M₁ →ₛₗ[σ₁] M₂ →ₗ[R] N₂) M) =
    M

Tactic:
(LinearMap.toMatrix₂ b₁ b₂).apply_symm_apply M

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

Tactic:
(LinearMap.toMatrix₂ b₁ b₂).apply_symm_apply M

Premises used: LinearMap.toMatrix₂, LinearEquiv.apply_symm_apply
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
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₂
inst_9 : AddCommMonoid M₁'
inst_10 : Module R M₁'
inst_11 : AddCommMonoid M₂'
inst_12 : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst_13 : Fintype n'
inst_14 : Fintype m'
inst_15 : DecidableEq n'
inst_16 : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
a :
  ∀ (i : n') (j : m'),
    (toMatrix₂ b₁' b₂' : (a : M₁' →ₗ[R] M₂' →ₗ[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 b₁' b₁ : (a : M₁' →ₗ[R] M₁) → Matrix n n' R) l)ᵀ
          ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R))
        ((toMatrix b₂' b₂ : (a : M₂' →ₗ[R] M₂) → Matrix m m' R) r : Matrix m m' R) i j
⊢ (toMatrix₂ b₁' b₂' : (a : M₁' →ₗ[R] M₂' →ₗ[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 b₁' b₁ : (a : M₁' →ₗ[R] M₁) → Matrix n n' R) l)ᵀ
        ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R))
      ((toMatrix b₂' b₂ : (a : M₂' →ₗ[R] M₂) → Matrix m m' R) r : Matrix m m' R)

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
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₂
inst_9 : AddCommMonoid M₁'
inst_10 : Module R M₁'
inst_11 : AddCommMonoid M₂'
inst_12 : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst_13 : Fintype n'
inst_14 : Fintype m'
inst_15 : DecidableEq n'
inst_16 : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
a :
  Eq.{u_1 + 1} (α := R)
    ((((B : (a : M₁) → M₂ →ₗ[R] R) ((l : (a : M₁') → M₁) ((b₁' : (a : n') → M₁') i : M₁')) : M₂ →ₗ[R] R) : (a : M₂) → R)
        ((r : (a : M₂') → M₂) ((b₂' : (a : m') → M₂') j : M₂') : M₂) :
      R)
    (∑ x : m,
        ∑ i_1 : n,
          HMul.hMul (β := R)
            (HMul.hMul (α := R) (β := R)
              ((((b₁.repr : (a : M₁) → n →₀ R) ((l : (a : M₁') → M₁) ((b₁' : (a : n') → M₁') i : M₁')) : n →₀ R) :
                    (a : n) → R)
                  i_1 :
                R)
              ((((B : (a : M₁) → M₂ →ₗ[R] R) ((b₁ : (a : n) → M₁) i_1) : M₂ →ₗ[R] R) : (a : M₂) → R)
                  ((b₂ : (a : m) → M₂) x : M₂) :
                R))
            ((((b₂.repr : (a : M₂) → m →₀ R) ((r : (a : M₂') → M₂) ((b₂' : (a : m') → M₂') j : M₂')) : m →₀ R) :
                  (a : m) → R)
                x :
              R) :
      R)
⊢ (toMatrix₂ b₁' b₂' : (a : M₁' →ₗ[R] M₂' →ₗ[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 b₁' b₁ : (a : M₁' →ₗ[R] M₁) → Matrix n n' R) l)ᵀ
        ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R))
      ((toMatrix b₂' b₂ : (a : M₂' →ₗ[R] M₂) → Matrix m m' R) r : Matrix m m' R) i j

Tactic:
simp only [LinearMap.toMatrix₂_apply, compl₁₂_apply, transpose_apply, Matrix.mul_apply,
    LinearMap.toMatrix_apply, sum_mul]

Premises used: Matrix.mul_apply, LinearMap.compl₁₂_apply, LinearMap.toMatrix₂_apply, Matrix.transpose_apply, LinearMap.toMatrix_apply, Finset.sum_mul
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
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₂
inst_9 : AddCommMonoid M₁'
inst_10 : Module R M₁'
inst_11 : AddCommMonoid M₂'
inst_12 : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst_13 : Fintype n'
inst_14 : Fintype m'
inst_15 : DecidableEq n'
inst_16 : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
a :
  Eq.{u_1 + 1} (α := R)
    ((((B : (a : M₁) → M₂ →ₗ[R] R) ((l : (a : M₁') → M₁) ((b₁' : (a : n') → M₁') i : M₁')) : M₂ →ₗ[R] R) : (a : M₂) → R)
        ((r : (a : M₂') → M₂) ((b₂' : (a : m') → M₂') j : M₂') : M₂) :
      R)
    (∑ y : n,
        ∑ x : m,
          HMul.hMul (β := R)
            (HMul.hMul (α := R) (β := R)
              ((((b₁.repr : (a : M₁) → n →₀ R) ((l : (a : M₁') → M₁) ((b₁' : (a : n') → M₁') i : M₁')) : n →₀ R) :
                    (a : n) → R)
                  y :
                R)
              ((((B : (a : M₁) → M₂ →ₗ[R] R) ((b₁ : (a : n) → M₁) y) : M₂ →ₗ[R] R) : (a : M₂) → R)
                  ((b₂ : (a : m) → M₂) x : M₂) :
                R))
            ((((b₂.repr : (a : M₂) → m →₀ R) ((r : (a : M₂') → M₂) ((b₂' : (a : m') → M₂') j : M₂')) : m →₀ R) :
                  (a : m) → R)
                x :
              R) :
      R)
⊢ Eq.{u_1 + 1} (α := R)
    ((((B : (a : M₁) → M₂ →ₗ[R] R) ((l : (a : M₁') → M₁) ((b₁' : (a : n') → M₁') i : M₁')) : M₂ →ₗ[R] R) : (a : M₂) → R)
        ((r : (a : M₂') → M₂) ((b₂' : (a : m') → M₂') j : M₂') : M₂) :
      R)
    (∑ x : m,
        ∑ i_1 : n,
          HMul.hMul (β := R)
            (HMul.hMul (α := R) (β := R)
              ((((b₁.repr : (a : M₁) → n →₀ R) ((l : (a : M₁') → M₁) ((b₁' : (a : n') → M₁') i : M₁')) : n →₀ R) :
                    (a : n) → R)
                  i_1 :
                R)
              ((((B : (a : M₁) → M₂ →ₗ[R] R) ((b₁ : (a : n) → M₁) i_1) : M₂ →ₗ[R] R) : (a : M₂) → R)
                  ((b₂ : (a : m) → M₂) x : M₂) :
                R))
            ((((b₂.repr : (a : M₂) → m →₀ R) ((r : (a : M₂') → M₂) ((b₂' : (a : m') → M₂') j : M₂')) : m →₀ R) :
                  (a : m) → R)
                x :
              R) :
      R)

Tactic:
rw [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
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
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₂
inst_9 : AddCommMonoid M₁'
inst_10 : Module R M₁'
inst_11 : AddCommMonoid M₂'
inst_12 : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst_13 : Fintype n'
inst_14 : Fintype m'
inst_15 : DecidableEq n'
inst_16 : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
rw :
  Finsupp.sum ((b₁.repr : (a : M₁) → n →₀ R) ((l : (a : M₁') → M₁) ((b₁' : (a : n') → M₁') i : M₁')))
    fun (i : n) (xi : R) ↦
    Finsupp.sum ((b₂.repr : (a : M₂) → m →₀ R) ((r : (a : M₂') → M₂) ((b₂' : (a : m') → M₂') j : M₂')))
      fun (j : m) (yj : R) ↦
      xi •>
        yj •>
          ((((B : (a : M₁) → M₂ →ₗ[R] R) ((b₁ : (a : n) → M₁) i) : M₂ →ₗ[R] R) : (a : M₂) → R)
              ((b₂ : (a : m) → M₂) j : M₂) :
            R)
| ((((B : (a : M₁) → M₂ →ₗ[R] R) ((l : (a : M₁') → M₁) ((b₁' : (a : n') → M₁') i : M₁')) : M₂ →ₗ[R] R) : (a : M₂) → R)
      ((r : (a : M₂') → M₂) ((b₂' : (a : m') → M₂') j : M₂') : M₂) :
    R)

Tactic:
rw [← LinearMap.sum_repr_mul_repr_mul b₁ b₂]

Premises used: LinearMap.sum_repr_mul_repr_mul
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
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₂
inst_9 : AddCommMonoid M₁'
inst_10 : Module R M₁'
inst_11 : AddCommMonoid M₂'
inst_12 : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst_13 : Fintype n'
inst_14 : Fintype m'
inst_15 : DecidableEq n'
inst_16 : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
a :
  Eq.{u_1 + 1} (α := R)
    (Finsupp.sum ((b₁.repr : (a : M₁) → n →₀ R) ((l : (a : M₁') → M₁) ((b₁' : (a : n') → M₁') i : M₁')))
      fun (i : n) (xi : R) ↦
      Finsupp.sum ((b₂.repr : (a : M₂) → m →₀ R) ((r : (a : M₂') → M₂) ((b₂' : (a : m') → M₂') j : M₂')))
        fun (j : m) (yj : R) ↦
        xi •>
          yj •>
            ((((B : (a : M₁) → M₂ →ₗ[R] R) ((b₁ : (a : n) → M₁) i) : M₂ →ₗ[R] R) : (a : M₂) → R)
                ((b₂ : (a : m) → M₂) j : M₂) :
              R))
    (∑ y : n,
      ∑ x : m,
        HMul.hMul (β := R)
          (HMul.hMul (α := R) (β := R)
            ((((b₁.repr : (a : M₁) → n →₀ R) ((l : (a : M₁') → M₁) ((b₁' : (a : n') → M₁') i : M₁')) : n →₀ R) :
                  (a : n) → R)
                y :
              R)
            ((((B : (a : M₁) → M₂ →ₗ[R] R) ((b₁ : (a : n) → M₁) y) : M₂ →ₗ[R] R) : (a : M₂) → R)
                ((b₂ : (a : m) → M₂) x : M₂) :
              R))
          ((((b₂.repr : (a : M₂) → m →₀ R) ((r : (a : M₂') → M₂) ((b₂' : (a : m') → M₂') j : M₂')) : m →₀ R) :
                (a : m) → R)
              x :
            R))
⊢ Eq.{u_1 + 1} (α := R)
    ((((B : (a : M₁) → M₂ →ₗ[R] R) ((l : (a : M₁') → M₁) ((b₁' : (a : n') → M₁') i : M₁')) : M₂ →ₗ[R] R) : (a : M₂) → R)
        ((r : (a : M₂') → M₂) ((b₂' : (a : m') → M₂') j : M₂') : M₂) :
      R)
    (∑ y : n,
        ∑ x : m,
          HMul.hMul (β := R)
            (HMul.hMul (α := R) (β := R)
              ((((b₁.repr : (a : M₁) → n →₀ R) ((l : (a : M₁') → M₁) ((b₁' : (a : n') → M₁') i : M₁')) : n →₀ R) :
                    (a : n) → R)
                  y :
                R)
              ((((B : (a : M₁) → M₂ →ₗ[R] R) ((b₁ : (a : n) → M₁) y) : M₂ →ₗ[R] R) : (a : M₂) → R)
                  ((b₂ : (a : m) → M₂) x : M₂) :
                R))
            ((((b₂.repr : (a : M₂) → m →₀ R) ((r : (a : M₂') → M₂) ((b₂' : (a : m') → M₂') j : M₂')) : m →₀ R) :
                  (a : m) → R)
                x :
              R) :
      R)

Tactic:
conv_lhs => rw [← LinearMap.sum_repr_mul_repr_mul b₁ b₂]

Premises used: LinearMap.sum_repr_mul_repr_mul
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
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₂
inst_9 : AddCommMonoid M₁'
inst_10 : Module R M₁'
inst_11 : AddCommMonoid M₂'
inst_12 : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst_13 : Fintype n'
inst_14 : Fintype m'
inst_15 : DecidableEq n'
inst_16 : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
a :
  ∀ (x : n),
    Membership.mem (γ := Finset n) univ x →
      Eq.{u_1 + 1} (α := R)
        (Finsupp.sum ((b₂.repr : (a : M₂) → m →₀ R) ((r : (a : M₂') → M₂) ((b₂' : (a : m') → M₂') j : M₂')))
          fun (j : m) (yj : R) ↦
          ((((b₁.repr : (a : M₁) → n →₀ R) ((l : (a : M₁') → M₁) ((b₁' : (a : n') → M₁') i : M₁')) : n →₀ R) :
                  (a : n) → R)
                x :
              R) •>
            yj •>
              ((((B : (a : M₁) → M₂ →ₗ[R] R) ((b₁ : (a : n) → M₁) x) : M₂ →ₗ[R] R) : (a : M₂) → R)
                  ((b₂ : (a : m) → M₂) j : M₂) :
                R))
        (∑ x_1 : m,
          HMul.hMul (β := R)
            (HMul.hMul (α := R) (β := R)
              ((((b₁.repr : (a : M₁) → n →₀ R) ((l : (a : M₁') → M₁) ((b₁' : (a : n') → M₁') i : M₁')) : n →₀ R) :
                    (a : n) → R)
                  x :
                R)
              ((((B : (a : M₁) → M₂ →ₗ[R] R) ((b₁ : (a : n) → M₁) x) : M₂ →ₗ[R] R) : (a : M₂) → R)
                  ((b₂ : (a : m) → M₂) x_1 : M₂) :
                R))
            ((((b₂.repr : (a : M₂) → m →₀ R) ((r : (a : M₂') → M₂) ((b₂' : (a : m') → M₂') j : M₂')) : m →₀ R) :
                  (a : m) → R)
                x_1 :
              R))
⊢ Eq.{u_1 + 1} (α := R)
    (∑ i_1 : n,
      Finsupp.sum ((b₂.repr : (a : M₂) → m →₀ R) ((r : (a : M₂') → M₂) ((b₂' : (a : m') → M₂') j : M₂')))
        fun (j : m) (yj : R) ↦
        ((((b₁.repr : (a : M₁) → n →₀ R) ((l : (a : M₁') → M₁) ((b₁' : (a : n') → M₁') i : M₁')) : n →₀ R) :
                (a : n) → R)
              i_1 :
            R) •>
          yj •>
            ((((B : (a : M₁) → M₂ →ₗ[R] R) ((b₁ : (a : n) → M₁) i_1) : M₂ →ₗ[R] R) : (a : M₂) → R)
                ((b₂ : (a : m) → M₂) j : M₂) :
              R))
    (∑ y : n,
      ∑ x : m,
        HMul.hMul (β := R)
          (HMul.hMul (α := R) (β := R)
            ((((b₁.repr : (a : M₁) → n →₀ R) ((l : (a : M₁') → M₁) ((b₁' : (a : n') → M₁') i : M₁')) : n →₀ R) :
                  (a : n) → R)
                y :
              R)
            ((((B : (a : M₁) → M₂ →ₗ[R] R) ((b₁ : (a : n) → M₁) y) : M₂ →ₗ[R] R) : (a : M₂) → R)
                ((b₂ : (a : m) → M₂) x : M₂) :
              R))
          ((((b₂.repr : (a : M₂) → m →₀ R) ((r : (a : M₂') → M₂) ((b₂' : (a : m') → M₂') j : M₂')) : m →₀ R) :
                (a : m) → R)
              x :
            R))

Tactic:
apply sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
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₂
inst_9 : AddCommMonoid M₁'
inst_10 : Module R M₁'
inst_11 : AddCommMonoid M₂'
inst_12 : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst_13 : Fintype n'
inst_14 : Fintype m'
inst_15 : DecidableEq n'
inst_16 : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
i' : n
a :
  ∀ (x : m),
    Membership.mem (γ := Finset m) univ x →
      ((((b₁.repr : (a : M₁) → n →₀ R) ((l : (a : M₁') → M₁) ((b₁' : (a : n') → M₁') i : M₁')) : n →₀ R) : (a : n) → R)
              i' :
            R) •>
          ((((b₂.repr : (a : M₂) → m →₀ R) ((r : (a : M₂') → M₂) ((b₂' : (a : m') → M₂') j : M₂')) : m →₀ R) :
                  (a : m) → R)
                x :
              R) •>
            ((((B : (a : M₁) → M₂ →ₗ[R] R) ((b₁ : (a : n) → M₁) i') : M₂ →ₗ[R] R) : (a : M₂) → R)
                ((b₂ : (a : m) → M₂) x : M₂) :
              R) =
        HMul.hMul (β := R)
          (HMul.hMul (α := R) (β := R)
            ((((b₁.repr : (a : M₁) → n →₀ R) ((l : (a : M₁') → M₁) ((b₁' : (a : n') → M₁') i : M₁')) : n →₀ R) :
                  (a : n) → R)
                i' :
              R)
            ((((B : (a : M₁) → M₂ →ₗ[R] R) ((b₁ : (a : n) → M₁) i') : M₂ →ₗ[R] R) : (a : M₂) → R)
                ((b₂ : (a : m) → M₂) x : M₂) :
              R))
          ((((b₂.repr : (a : M₂) → m →₀ R) ((r : (a : M₂') → M₂) ((b₂' : (a : m') → M₂') j : M₂')) : m →₀ R) :
                (a : m) → R)
              x :
            R)
⊢ Eq.{u_1 + 1} (α := R)
    (∑ i_1 : m,
      ((((b₁.repr : (a : M₁) → n →₀ R) ((l : (a : M₁') → M₁) ((b₁' : (a : n') → M₁') i : M₁')) : n →₀ R) : (a : n) → R)
            i' :
          R) •>
        ((((b₂.repr : (a : M₂) → m →₀ R) ((r : (a : M₂') → M₂) ((b₂' : (a : m') → M₂') j : M₂')) : m →₀ R) :
                (a : m) → R)
              i_1 :
            R) •>
          ((((B : (a : M₁) → M₂ →ₗ[R] R) ((b₁ : (a : n) → M₁) i') : M₂ →ₗ[R] R) : (a : M₂) → R)
              ((b₂ : (a : m) → M₂) i_1 : M₂) :
            R))
    (∑ x : m,
      HMul.hMul (β := R)
        (HMul.hMul (α := R) (β := R)
          ((((b₁.repr : (a : M₁) → n →₀ R) ((l : (a : M₁') → M₁) ((b₁' : (a : n') → M₁') i : M₁')) : n →₀ R) :
                (a : n) → R)
              i' :
            R)
          ((((B : (a : M₁) → M₂ →ₗ[R] R) ((b₁ : (a : n) → M₁) i') : M₂ →ₗ[R] R) : (a : M₂) → R)
              ((b₂ : (a : m) → M₂) x : M₂) :
            R))
        ((((b₂.repr : (a : M₂) → m →₀ R) ((r : (a : M₂') → M₂) ((b₂' : (a : m') → M₂') j : M₂')) : m →₀ R) :
              (a : m) → R)
            x :
          R))

Tactic:
apply sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
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₂
inst_9 : AddCommMonoid M₁'
inst_10 : Module R M₁'
inst_11 : AddCommMonoid M₂'
inst_12 : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst_13 : Fintype n'
inst_14 : Fintype m'
inst_15 : DecidableEq n'
inst_16 : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
i' : n
j' : m
⊢ ((((b₁.repr : (a : M₁) → n →₀ R) ((l : (a : M₁') → M₁) ((b₁' : (a : n') → M₁') i : M₁')) : n →₀ R) : (a : n) → R) i' :
        R) •>
      ((((b₂.repr : (a : M₂) → m →₀ R) ((r : (a : M₂') → M₂) ((b₂' : (a : m') → M₂') j : M₂')) : m →₀ R) : (a : m) → R)
            j' :
          R) •>
        ((((B : (a : M₁) → M₂ →ₗ[R] R) ((b₁ : (a : n) → M₁) i') : M₂ →ₗ[R] R) : (a : M₂) → R)
            ((b₂ : (a : m) → M₂) j' : M₂) :
          R) =
    HMul.hMul (β := R)
      (HMul.hMul (α := R) (β := R)
        ((((b₁.repr : (a : M₁) → n →₀ R) ((l : (a : M₁') → M₁) ((b₁' : (a : n') → M₁') i : M₁')) : n →₀ R) :
              (a : n) → R)
            i' :
          R)
        ((((B : (a : M₁) → M₂ →ₗ[R] R) ((b₁ : (a : n) → M₁) i') : M₂ →ₗ[R] R) : (a : M₂) → R)
            ((b₂ : (a : m) → M₂) j' : M₂) :
          R))
      ((((b₂.repr : (a : M₂) → m →₀ R) ((r : (a : M₂') → M₂) ((b₂' : (a : m') → M₂') j : M₂')) : m →₀ R) : (a : m) → R)
          j' :
        R)

Tactic:
simp only [smul_eq_mul, mul_assoc, mul_comm,
        mul_left_comm]

Premises used: mul_assoc, mul_left_comm, mul_comm, smul_eq_mul
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
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₂
inst_9 : AddCommMonoid M₁'
inst_10 : Module R M₁'
inst_11 : AddCommMonoid M₂'
inst_12 : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst_13 : Fintype n'
inst_14 : Fintype m'
inst_15 : DecidableEq n'
inst_16 : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
i' : n
i_1 : m
⊢ ((((b₁.repr : (a : M₁) → n →₀ R) ((l : (a : M₁') → M₁) ((b₁' : (a : n') → M₁') i : M₁')) : n →₀ R) : (a : n) → R) i' :
        R) •>
      0 •>
        ((((B : (a : M₁) → M₂ →ₗ[R] R) ((b₁ : (a : n) → M₁) i') : M₂ →ₗ[R] R) : (a : M₂) → R)
            ((b₂ : (a : m) → M₂) i_1 : M₂) :
          R) =
    0

Tactic:
simp only [zero_smul, smul_zero]

Premises used: smul_zero, zero_smul
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
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₂
inst_9 : AddCommMonoid M₁'
inst_10 : Module R M₁'
inst_11 : AddCommMonoid M₂'
inst_12 : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst_13 : Fintype n'
inst_14 : Fintype m'
inst_15 : DecidableEq n'
inst_16 : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
i_1 : n
⊢ Eq.{u_1 + 1} (α := R)
    (Finsupp.sum ((b₂.repr : (a : M₂) → m →₀ R) ((r : (a : M₂') → M₂) ((b₂' : (a : m') → M₂') j : M₂')))
      fun (j : m) (yj : R) ↦
      0 •>
        yj •>
          ((((B : (a : M₁) → M₂ →ₗ[R] R) ((b₁ : (a : n) → M₁) i_1) : M₂ →ₗ[R] R) : (a : M₂) → R)
              ((b₂ : (a : m) → M₂) j : M₂) :
            R))
    0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
n : Type u_11
m : Type u_12
n' : Type u_13
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
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₂
inst_9 : AddCommMonoid M₁'
inst_10 : Module R M₁'
b₁' : Basis n' R M₁'
inst_11 : Fintype n'
inst_12 : DecidableEq n'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
f : M₁' →ₗ[R] M₁
rw :
  HMul.hMul (β := Matrix m m R)
      (HMul.hMul (α := Matrix n' n R) (β := Matrix n m R) ((toMatrix b₁' b₁ : (a : M₁' →ₗ[R] M₁) → Matrix n n' R) f)ᵀ
        ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R))
      ((toMatrix b₂ b₂ : (a : M₂ →ₗ[R] M₂) → Matrix m m R) id : Matrix m m R) =
    HMul.hMul (α := Matrix n' n R) (β := Matrix n m R) ((toMatrix b₁' b₁ : (a : M₁' →ₗ[R] M₁) → Matrix n n' R) f)ᵀ
      ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R)
⊢ (toMatrix₂ b₁' b₂ : (a : M₁' →ₗ[R] M₂ →ₗ[R] R) → Matrix n' m R) (B ∘ₗ f) =
    HMul.hMul (α := Matrix n' n R) (β := Matrix n m R) ((toMatrix b₁' b₁ : (a : M₁' →ₗ[R] M₁) → Matrix n n' R) f)ᵀ
      ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R)

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

Premises used: LinearMap.toMatrix₂_compl₁₂, LinearMap.comp, LinearMap.compl₂_id, LinearMap.compl₁₂