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_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 : M₁
y : M₂
nth_rw :
  Eq (α := R)
    (((B : (a : M₁) → M₂ →ₛₗ[σ₂] R)
            (∑ i : n,
              ((((b₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) i : R) •> ((b₁ : (a : n) → M₁) i : M₁)) :
          (a : M₂) → R)
        (∑ i : m, ((((b₂.repr : (a : M₂) → m →₀ R) y : m →₀ R) : (a : m) → R) i : R) •> ((b₂ : (a : m) → M₂) i : M₂)) :
      R)
    (dotProduct.{u_1, u_11} (m := n)
        (Function.comp (β := R) (⇑σ₁ : (a : R) → R) (⇑((b₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R))
        (mulVec.{u_1, u_11, u_12} (n := m) ((toMatrix₂ b₁ b₂ : (a : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R) → Matrix n m R) B)
          (Function.comp (β := R) (⇑σ₂ : (a : R) → R) (⇑((b₂.repr : (a : M₂) → m →₀ R) y : m →₀ R) : (a : m) → R))) :
      R)
⊢ Eq (α := R) ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) x : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R) y : R)
    (dotProduct.{u_1, u_11} (m := n)
        (Function.comp (β := R) (⇑σ₁ : (a : R) → R) (⇑((b₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R))
        (mulVec.{u_1, u_11, u_12} (n := m) ((toMatrix₂ b₁ b₂ : (a : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R) → Matrix n m R) B)
          (Function.comp (β := R) (⇑σ₂ : (a : R) → R) (⇑((b₂.repr : (a : M₂) → m →₀ R) y : m →₀ R) : (a : m) → R))) :
      R)

Tactic:
nth_rw 1 [← b₁.sum_repr x, ← b₂.sum_repr y]

Premises used: Module.Basis.sum_repr
-- 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 : M₁
y : M₂
this :
  Eq.{u_1 + 1} (α := R)
    (∑ j : m,
      ∑ i : n,
        HMul.hMul (β := R)
          (HMul.hMul (α := R) (β := R)
            ((σ₂ : (a : R) → R) ((((b₂.repr : (a : M₂) → m →₀ R) y : m →₀ R) : (a : m) → R) j : R) : R)
            ((σ₁ : (a : R) → R) ((((b₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) i : R) : R))
          ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) i) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
              ((b₂ : (a : m) → M₂) j : M₂) :
            R))
    (∑ i : n,
      ∑ j : m,
        HMul.hMul (β := R)
          (HMul.hMul (α := R) (β := R)
            ((σ₁ : (a : R) → R) ((((b₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) i : R) : R)
            ((σ₂ : (a : R) → R) ((((b₂.repr : (a : M₂) → m →₀ R) y : m →₀ R) : (a : m) → R) j : R) : R))
          ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) i) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
              ((b₂ : (a : m) → M₂) j : M₂) :
            R))
⊢ Eq (α := R)
    (((B : (a : M₁) → M₂ →ₛₗ[σ₂] R)
            (∑ i : n,
              ((((b₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) i : R) •> ((b₁ : (a : n) → M₁) i : M₁)) :
          (a : M₂) → R)
        (∑ i : m, ((((b₂.repr : (a : M₂) → m →₀ R) y : m →₀ R) : (a : m) → R) i : R) •> ((b₂ : (a : m) → M₂) i : M₂)) :
      R)
    (dotProduct.{u_1, u_11} (m := n)
        (Function.comp (β := R) (⇑σ₁ : (a : R) → R) (⇑((b₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R))
        (mulVec.{u_1, u_11, u_12} (n := m) ((toMatrix₂ b₁ b₂ : (a : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R) → Matrix n m R) B)
          (Function.comp (β := R) (⇑σ₂ : (a : R) → R) (⇑((b₂.repr : (a : M₂) → m →₀ R) y : m →₀ R) : (a : m) → R))) :
      R)

Tactic:
simpa [dotProduct, Matrix.mulVec_eq_sum, Finset.mul_sum, -Basis.sum_repr, ← mul_assoc]

Premises used: Finset.mul_sum, dotProduct, mul_assoc, Matrix.mulVec_eq_sum, Module.Basis.sum_repr
-- 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 : M₁
y : M₂
suffices :
  Eq.{u_1 + 1} (α := R)
    (∑ j : m,
      ∑ i : n,
        HMul.hMul (β := R)
          (HMul.hMul (α := R) (β := R)
            ((σ₂ : (a : R) → R) ((((b₂.repr : (a : M₂) → m →₀ R) y : m →₀ R) : (a : m) → R) j : R) : R)
            ((σ₁ : (a : R) → R) ((((b₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) i : R) : R))
          ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) i) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
              ((b₂ : (a : m) → M₂) j : M₂) :
            R))
    (∑ i : n,
      ∑ j : m,
        HMul.hMul (β := R)
          (HMul.hMul (α := R) (β := R)
            ((σ₁ : (a : R) → R) ((((b₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) i : R) : R)
            ((σ₂ : (a : R) → R) ((((b₂.repr : (a : M₂) → m →₀ R) y : m →₀ R) : (a : m) → R) j : R) : R))
          ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) i) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
              ((b₂ : (a : m) → M₂) j : M₂) :
            R))
⊢ Eq (α := R)
    (((B : (a : M₁) → M₂ →ₛₗ[σ₂] R)
            (∑ i : n,
              ((((b₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) i : R) •> ((b₁ : (a : n) → M₁) i : M₁)) :
          (a : M₂) → R)
        (∑ i : m, ((((b₂.repr : (a : M₂) → m →₀ R) y : m →₀ R) : (a : m) → R) i : R) •> ((b₂ : (a : m) → M₂) i : M₂)) :
      R)
    (dotProduct.{u_1, u_11} (m := n)
        (Function.comp (β := R) (⇑σ₁ : (a : R) → R) (⇑((b₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R))
        (mulVec.{u_1, u_11, u_12} (n := m) ((toMatrix₂ b₁ b₂ : (a : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R) → Matrix n m R) B)
          (Function.comp (β := R) (⇑σ₂ : (a : R) → R) (⇑((b₂.repr : (a : M₂) → m →₀ R) y : m →₀ R) : (a : m) → R))) :
      R)

Tactic:
suffices ∑ j, ∑ i, σ₂ (b₂.repr y j) * σ₁ (b₁.repr x i) * B (b₁ i) (b₂ j) =
           ∑ i, ∑ j, σ₁ (b₁.repr x i) * σ₂ (b₂.repr y j) * B (b₁ i) (b₂ j) by
    simpa [dotProduct, Matrix.mulVec_eq_sum, Finset.mul_sum, -Basis.sum_repr, ← mul_assoc]
-- 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 : M₁
y : M₂
simp_rw :
  Eq.{u_1 + 1} (α := R)
    (∑ x_1 : m,
      ∑ x_2 : n,
        HMul.hMul (β := R)
          (HMul.hMul (α := R) (β := R)
            ((σ₁ : (a : R) → R) ((((b₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) x_2 : R) : R)
            ((σ₂ : (a : R) → R) ((((b₂.repr : (a : M₂) → m →₀ R) y : m →₀ R) : (a : m) → R) x_1 : R) : R))
          ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) x_2) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
              ((b₂ : (a : m) → M₂) x_1 : M₂) :
            R))
    (∑ i : n,
      ∑ j : m,
        HMul.hMul (β := R)
          (HMul.hMul (α := R) (β := R)
            ((σ₁ : (a : R) → R) ((((b₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) i : R) : R)
            ((σ₂ : (a : R) → R) ((((b₂.repr : (a : M₂) → m →₀ R) y : m →₀ R) : (a : m) → R) j : R) : R))
          ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) i) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
              ((b₂ : (a : m) → M₂) j : M₂) :
            R))
⊢ Eq.{u_1 + 1} (α := R)
    (∑ j : m,
      ∑ i : n,
        HMul.hMul (β := R)
          (HMul.hMul (α := R) (β := R)
            ((σ₂ : (a : R) → R) ((((b₂.repr : (a : M₂) → m →₀ R) y : m →₀ R) : (a : m) → R) j : R) : R)
            ((σ₁ : (a : R) → R) ((((b₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) i : R) : R))
          ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) i) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
              ((b₂ : (a : m) → M₂) j : M₂) :
            R))
    (∑ i : n,
      ∑ j : m,
        HMul.hMul (β := R)
          (HMul.hMul (α := R) (β := R)
            ((σ₁ : (a : R) → R) ((((b₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) i : R) : R)
            ((σ₂ : (a : R) → R) ((((b₂.repr : (a : M₂) → m →₀ R) y : m →₀ R) : (a : m) → R) j : R) : R))
          ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) i) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
              ((b₂ : (a : m) → M₂) j : M₂) :
            R))

Tactic:
simp_rw [mul_comm (σ₂ _)]

Premises used: mul_comm, DFunLike.coe
-- 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 : M₁
y : M₂
⊢ Eq.{u_1 + 1} (α := R)
    (∑ x_1 : m,
      ∑ x_2 : n,
        HMul.hMul (β := R)
          (HMul.hMul (α := R) (β := R)
            ((σ₁ : (a : R) → R) ((((b₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) x_2 : R) : R)
            ((σ₂ : (a : R) → R) ((((b₂.repr : (a : M₂) → m →₀ R) y : m →₀ R) : (a : m) → R) x_1 : R) : R))
          ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) x_2) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
              ((b₂ : (a : m) → M₂) x_1 : M₂) :
            R))
    (∑ i : n,
      ∑ j : m,
        HMul.hMul (β := R)
          (HMul.hMul (α := R) (β := R)
            ((σ₁ : (a : R) → R) ((((b₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) i : R) : R)
            ((σ₂ : (a : R) → R) ((((b₂.repr : (a : M₂) → m →₀ R) y : m →₀ R) : (a : m) → R) j : R) : R))
          ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) i) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
              ((b₂ : (a : m) → M₂) j : M₂) :
            R))

Tactic:
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 : M₁
y : M₂
⊢ Eq.{u_1 + 1} (α := R)
    (∑ x_1 : m,
      ∑ x_2 : n,
        HMul.hMul (β := R)
          (HMul.hMul (α := R) (β := R)
            ((σ₁ : (a : R) → R) ((((b₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) x_2 : R) : R)
            ((σ₂ : (a : R) → R) ((((b₂.repr : (a : M₂) → m →₀ R) y : m →₀ R) : (a : m) → R) x_1 : R) : R))
          ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) x_2) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
              ((b₂ : (a : m) → M₂) x_1 : M₂) :
            R))
    (∑ i : n,
      ∑ j : m,
        HMul.hMul (β := R)
          (HMul.hMul (α := R) (β := R)
            ((σ₁ : (a : R) → R) ((((b₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) i : R) : R)
            ((σ₂ : (a : R) → R) ((((b₂.repr : (a : M₂) → m →₀ R) y : m →₀ R) : (a : m) → R) j : R) : R))
          ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) i) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
              ((b₂ : (a : m) → M₂) j : M₂) :
            R))

Tactic:
exact 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_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
rw :
  Eq.{u_10 + 1} (α := N₂)
    (((toMatrix₂Aux R (⇑b₁ : (a : n) → M₁) (⇑b₂ : (a : m) → M₂) : (M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂) →ₗ[R] Matrix n m N₂) :
          (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₂)
rw₁ rw₂ :
  Eq.{u_10 + 1} (α := N₂)
    ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] N₂) ((b₁ : (a : n) → M₁) i) : M₂ →ₛₗ[σ₂] N₂) : (a : M₂) → N₂)
        ((b₂ : (a : m) → M₂) j : M₂) :
      N₂)
    ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] N₂) ((b₁ : (a : n) → M₁) i) : M₂ →ₛₗ[σ₂] N₂) : (a : M₂) → N₂)
        ((b₂ : (a : m) → M₂) j : M₂) :
      N₂)
⊢ Eq.{u_10 + 1} (α := N₂)
    (((toMatrix₂Aux R (⇑b₁ : (a : n) → M₁) (⇑b₂ : (a : m) → M₂) : (M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂) →ₗ[R] Matrix n m N₂) :
          (a : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂) → Matrix n m N₂)
        B i j :
      N₂)
    ((toMatrix₂ b₁ b₂ : (a : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂) → Matrix n m N₂) B i j : N₂)

Tactic:
rw [LinearMap.toMatrix₂_apply, LinearMap.toMatrix₂Aux_apply]

Premises used: LinearMap.toMatrix₂_apply, LinearMap.toMatrix₂Aux_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₂
⊢ Eq (α := Matrix n m N₂ ≃ₗ[R] M₁ →ₛₗ[σ₁] M₂ →ₗ[R] N₂) (LinearEquiv.symm (toMatrix₂ b₁ b₂)) (toLinearMapₛₗ₂ σ₁ b₁ b₂)

Tactic:
rfl

Premises used: Matrix.toLinearMapₛₗ₂, rfl
-- 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₂
⊢ Eq (α := Matrix n m N₂ ≃ₗ[R] M₁ →ₗ[R] M₂ →ₗ[R] N₂) (LinearEquiv.symm (toMatrix₂ b₁ b₂)) (toLinearMap₂ b₁ b₂)

Tactic:
rfl

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

Tactic:
(LinearMap.toMatrix₂ b₁ b₂).symm_symm

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

Tactic:
(LinearMap.toMatrix₂ b₁ b₂).symm_symm

Premises used: LinearMap.toMatrix₂, LinearEquiv.symm_symm, Matrix.toLinearMapₛₗ₂, Matrix.toLinearMap₂
-- 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 m
inst_6 : DecidableEq n
h :
  ∀ (M : Matrix n m N₂) (i : n) (i_1 : m),
    Eq.{u_10 + 1} (α := N₂)
      ((((((toLinearMap₂ (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix n m N₂) → (n → R) →ₗ[R] (m → R) →ₗ[R] N₂)
                          M ∘ₗ
                        LinearMap.single R (fun (i : n) ↦ R) i :
                      R →ₗ[R] (m → R) →ₗ[R] N₂) :
                    (a : R) → (m → R) →ₗ[R] N₂)
                  1 ∘ₗ
                LinearMap.single R (fun (i : m) ↦ R) i_1 :
              R →ₗ[R] N₂) :
            (a : R) → N₂)
          1 :
        N₂)
      (((((((toLinearMap₂' R : Matrix n m N₂ ≃ₗ[R] (n → R) →ₗ[R] (m → R) →ₗ[R] N₂) :
                            (a : Matrix n m N₂) → (n → R) →ₗ[R] (m → R) →ₗ[R] N₂)
                          M ∘ₗ
                        LinearMap.single R (fun (i : n) ↦ R) i :
                      R →ₗ[R] (m → R) →ₗ[R] N₂) :
                    (a : R) → (m → R) →ₗ[R] N₂)
                  1 ∘ₗ
                LinearMap.single R (fun (i : m) ↦ R) i_1 :
              R →ₗ[R] N₂) :
            (a : R) → N₂)
          1 :
        N₂)
⊢ Eq (α := Matrix n m N₂ ≃ₗ[R] (n → R) →ₗ[R] (m → R) →ₗ[R] N₂) (toLinearMap₂ (Pi.basisFun R n) (Pi.basisFun R m))
    (toLinearMap₂' R)

Tactic:
ext M
-- 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 m
inst_6 : DecidableEq n
M : Matrix n m N₂
i : n
i_1 : m
⊢ Eq.{u_10 + 1} (α := N₂)
    ((((((toLinearMap₂ (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix n m N₂) → (n → R) →ₗ[R] (m → R) →ₗ[R] N₂) M ∘ₗ
                      LinearMap.single R (fun (i : n) ↦ R) i :
                    R →ₗ[R] (m → R) →ₗ[R] N₂) :
                  (a : R) → (m → R) →ₗ[R] N₂)
                1 ∘ₗ
              LinearMap.single R (fun (i : m) ↦ R) i_1 :
            R →ₗ[R] N₂) :
          (a : R) → N₂)
        1 :
      N₂)
    (((((((toLinearMap₂' R : Matrix n m N₂ ≃ₗ[R] (n → R) →ₗ[R] (m → R) →ₗ[R] N₂) :
                          (a : Matrix n m N₂) → (n → R) →ₗ[R] (m → R) →ₗ[R] N₂)
                        M ∘ₗ
                      LinearMap.single R (fun (i : n) ↦ R) i :
                    R →ₗ[R] (m → R) →ₗ[R] N₂) :
                  (a : R) → (m → R) →ₗ[R] N₂)
                1 ∘ₗ
              LinearMap.single R (fun (i : m) ↦ R) i_1 :
            R →ₗ[R] N₂) :
          (a : R) → N₂)
        1 :
      N₂)

Tactic:
simp only [coe_comp, coe_single, Function.comp_apply, toLinearMap₂_apply, Pi.basisFun_repr,
    toLinearMap₂'_apply]

Premises used: Matrix.toLinearMap₂'_apply, LinearMap.coe_comp, LinearMap.coe_single, Matrix.toLinearMap₂_apply, Function.comp_apply, Pi.basisFun_repr
-- 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 m
inst_6 : DecidableEq n
h :
  ∀ (B : (n → R) →ₗ[R] (m → R) →ₗ[R] N₂) (i : n) (j : m),
    Eq.{u_10 + 1} (α := N₂)
      ((toMatrix₂ (Pi.basisFun R n) (Pi.basisFun R m) : (a : (n → R) →ₗ[R] (m → R) →ₗ[R] N₂) → Matrix n m N₂) B i j :
        N₂)
      (((toMatrix₂' R : ((n → R) →ₗ[R] (m → R) →ₗ[R] N₂) ≃ₗ[R] Matrix n m N₂) :
            (a : (n → R) →ₗ[R] (m → R) →ₗ[R] N₂) → Matrix n m N₂)
          B i j :
        N₂)
⊢ Eq (α := ((n → R) →ₗ[R] (m → R) →ₗ[R] N₂) ≃ₗ[R] Matrix n m N₂) (toMatrix₂ (Pi.basisFun R n) (Pi.basisFun R m))
    (toMatrix₂' R)

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

Tactic:
rw [LinearMap.toMatrix₂_apply, LinearMap.toMatrix₂'_apply, Pi.basisFun_apply, Pi.basisFun_apply]

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

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

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

Tactic:
(Matrix.toLinearMap₂ b₁ b₂).apply_symm_apply B

Premises used: LinearEquiv.apply_symm_apply, Matrix.toLinearMap₂