awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
g : Dual R N
q : Q
x : N
⊢ Eq.{u_5 + 1} (α := P)
    ((prodMap 0 ((dualTensorHom R N Q : (a : Dual R N ⊗[R] Q) → N →ₗ[R] Q) (g ⊗ₜ[R] q)) ∘ₗ inr R M N : (a : N) → P × Q)
        x).1
    (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
              ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q : (a : Q) → P × Q) q) ∘ₗ
            inr R M N :
          (a : N) → P × Q)
        x).1

Tactic:
simp only [coe_comp, coe_inr, Function.comp_apply, prodMap_apply, dualTensorHom_apply,
      snd_apply, Prod.smul_mk, LinearMap.zero_apply, smul_zero]

Premises used: LinearMap.zero_apply, LinearMap.prodMap_apply, LinearMap.coe_inr, dualTensorHom_apply, smul_zero, LinearMap.coe_comp, Function.comp_apply, Prod.smul_mk, LinearMap.snd_apply
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
g : Dual R N
q : Q
x : N
⊢ Eq.{u_6 + 1} (α := Q)
    ((prodMap 0 ((dualTensorHom R N Q : (a : Dual R N ⊗[R] Q) → N →ₗ[R] Q) (g ⊗ₜ[R] q)) ∘ₗ inr R M N : (a : N) → P × Q)
        x).2
    (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
              ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q : (a : Q) → P × Q) q) ∘ₗ
            inr R M N :
          (a : N) → P × Q)
        x).2

Tactic:
simp only [coe_comp, coe_inr, Function.comp_apply, prodMap_apply, dualTensorHom_apply,
      snd_apply, Prod.smul_mk, LinearMap.zero_apply, smul_zero]

Premises used: LinearMap.zero_apply, LinearMap.prodMap_apply, LinearMap.coe_inr, dualTensorHom_apply, smul_zero, LinearMap.coe_comp, Function.comp_apply, Prod.smul_mk, LinearMap.snd_apply
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
f : Dual R M
p : P
g : Dual R N
q : Q
H :
  ∀ (m : M) (n : N),
    Eq (α := P ⊗[R] Q)
      ((((compr₂ₛₗ (σ₃₄ := RingHom.id R) (TensorProduct.mk R M N)
                    (TensorProduct.map ((dualTensorHom R M P : (a : Dual R M ⊗[R] P) → M →ₗ[R] P) (f ⊗ₜ[R] p))
                      ((dualTensorHom R N Q : (a : Dual R N ⊗[R] Q) → N →ₗ[R] Q) (g ⊗ₜ[R] q))) :
                  (a : M) → N →ₗ[R] P ⊗[R] Q)
                m :
              N →ₗ[R] P ⊗[R] Q) :
            (a : N) → P ⊗[R] Q)
          n :
        P ⊗[R] Q)
      ((((compr₂ₛₗ (σ₃₄ := RingHom.id R) (TensorProduct.mk R M N)
                    ((dualTensorHom R (M ⊗[R] N) (P ⊗[R] Q) :
                        (a : Dual R (M ⊗[R] N) ⊗[R] (P ⊗[R] Q)) → M ⊗[R] N →ₗ[R] P ⊗[R] Q)
                      ((dualDistrib R M N : (a : Dual R M ⊗[R] Dual R N) → Dual R (M ⊗[R] N)) (f ⊗ₜ[R] g) ⊗ₜ[R]
                        (p ⊗ₜ[R] q))) :
                  (a : M) → N →ₗ[R] P ⊗[R] Q)
                m :
              N →ₗ[R] P ⊗[R] Q) :
            (a : N) → P ⊗[R] Q)
          n :
        P ⊗[R] Q)
⊢ Eq (α := M ⊗[R] N →ₗ[R] P ⊗[R] Q)
    (TensorProduct.map ((dualTensorHom R M P : (a : Dual R M ⊗[R] P) → M →ₗ[R] P) (f ⊗ₜ[R] p))
      ((dualTensorHom R N Q : (a : Dual R N ⊗[R] Q) → N →ₗ[R] Q) (g ⊗ₜ[R] q)))
    ((dualTensorHom R (M ⊗[R] N) (P ⊗[R] Q) : (a : Dual R (M ⊗[R] N) ⊗[R] (P ⊗[R] Q)) → M ⊗[R] N →ₗ[R] P ⊗[R] Q)
      ((dualDistrib R M N : (a : Dual R M ⊗[R] Dual R N) → Dual R (M ⊗[R] N)) (f ⊗ₜ[R] g) ⊗ₜ[R] (p ⊗ₜ[R] q)))

Tactic:
ext m n
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
f : Dual R M
p : P
g : Dual R N
q : Q
m : M
n : N
⊢ Eq (α := P ⊗[R] Q)
    ((((compr₂ₛₗ (σ₃₄ := RingHom.id R) (TensorProduct.mk R M N)
                  (TensorProduct.map ((dualTensorHom R M P : (a : Dual R M ⊗[R] P) → M →ₗ[R] P) (f ⊗ₜ[R] p))
                    ((dualTensorHom R N Q : (a : Dual R N ⊗[R] Q) → N →ₗ[R] Q) (g ⊗ₜ[R] q))) :
                (a : M) → N →ₗ[R] P ⊗[R] Q)
              m :
            N →ₗ[R] P ⊗[R] Q) :
          (a : N) → P ⊗[R] Q)
        n :
      P ⊗[R] Q)
    ((((compr₂ₛₗ (σ₃₄ := RingHom.id R) (TensorProduct.mk R M N)
                  ((dualTensorHom R (M ⊗[R] N) (P ⊗[R] Q) :
                      (a : Dual R (M ⊗[R] N) ⊗[R] (P ⊗[R] Q)) → M ⊗[R] N →ₗ[R] P ⊗[R] Q)
                    ((dualDistrib R M N : (a : Dual R M ⊗[R] Dual R N) → Dual R (M ⊗[R] N)) (f ⊗ₜ[R] g) ⊗ₜ[R]
                      (p ⊗ₜ[R] q))) :
                (a : M) → N →ₗ[R] P ⊗[R] Q)
              m :
            N →ₗ[R] P ⊗[R] Q) :
          (a : N) → P ⊗[R] Q)
        n :
      P ⊗[R] Q)

Tactic:
simp only [compr₂ₛₗ_apply, mk_apply, map_tmul, dualTensorHom_apply, dualDistrib_apply,
    ← smul_tmul_smul]

Premises used: TensorProduct.mk_apply, dualTensorHom_apply, TensorProduct.map_tmul, TensorProduct.smul_tmul_smul, TensorProduct.dualDistrib_apply, LinearMap.compr₂ₛₗ_apply
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : Dual R M
n : N
g : Dual R N
p : P
h :
  ∀ (m : M),
    Eq.{u_5 + 1} (α := P)
      (((dualTensorHom R N P : (a : Dual R N ⊗[R] P) → N →ₗ[R] P) (g ⊗ₜ[R] p) ∘ₗ
              (dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) (f ⊗ₜ[R] n) :
            (a : M) → P)
          m :
        P)
      ((HSMul.hSMul (α := R) (β := M →ₗ[R] P) ((g : (a : N) → R) n : R)
              ((dualTensorHom R M P : (a : Dual R M ⊗[R] P) → M →ₗ[R] P) (f ⊗ₜ[R] p) : M →ₗ[R] P) :
            (a : M) → P)
          m :
        P)
⊢ (dualTensorHom R N P : (a : Dual R N ⊗[R] P) → N →ₗ[R] P) (g ⊗ₜ[R] p) ∘ₗ
      (dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) (f ⊗ₜ[R] n) =
    HSMul.hSMul (α := R) (β := M →ₗ[R] P) ((g : (a : N) → R) n : R)
      ((dualTensorHom R M P : (a : Dual R M ⊗[R] P) → M →ₗ[R] P) (f ⊗ₜ[R] p) : M →ₗ[R] P)

Tactic:
ext m
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : Dual R M
n : N
g : Dual R N
p : P
m : M
h :
  HSMul.hSMul.{u_2, u_5, u_5} (α := R) ((f : (a : M) → R) m : R)
      (HSMul.hSMul.{u_2, u_5, u_5} (α := R) ((g : (a : N) → R) n : R) p) =
    HSMul.hSMul.{u_2, u_5, u_5} (α := R) ((g : (a : N) → R) n : R)
      (HSMul.hSMul.{u_2, u_5, u_5} (α := R) ((f : (a : M) → R) m : R) p)
⊢ Eq.{u_5 + 1} (α := P)
    (((dualTensorHom R N P : (a : Dual R N ⊗[R] P) → N →ₗ[R] P) (g ⊗ₜ[R] p) ∘ₗ
            (dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) (f ⊗ₜ[R] n) :
          (a : M) → P)
        m :
      P)
    ((HSMul.hSMul (α := R) (β := M →ₗ[R] P) ((g : (a : N) → R) n : R)
            ((dualTensorHom R M P : (a : Dual R M ⊗[R] P) → M →ₗ[R] P) (f ⊗ₜ[R] p) : M →ₗ[R] P) :
          (a : M) → P)
        m :
      P)

Tactic:
simp only [coe_comp, Function.comp_apply, dualTensorHom_apply, map_smul, LinearMap.smul_apply]

Premises used: LinearMap.smul_apply, dualTensorHom_apply, LinearMap.coe_comp, Function.comp_apply, map_smul
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : Dual R M
n : N
g : Dual R N
p : P
m : M
h h₁ :
  HSMul.hSMul.{u_2, u_5, u_5} (α := R) ((g : (a : N) → R) n : R)
      (HSMul.hSMul.{u_2, u_5, u_5} (α := R) ((f : (a : M) → R) m : R) p) =
    HSMul.hSMul.{u_2, u_5, u_5} (α := R) ((g : (a : N) → R) n : R)
      (HSMul.hSMul.{u_2, u_5, u_5} (α := R) ((f : (a : M) → R) m : R) p)
⊢ HSMul.hSMul.{u_2, u_5, u_5} (α := R) ((f : (a : M) → R) m : R)
      (HSMul.hSMul.{u_2, u_5, u_5} (α := R) ((g : (a : N) → R) n : R) p) =
    HSMul.hSMul.{u_2, u_5, u_5} (α := R) ((g : (a : N) → R) n : R)
      (HSMul.hSMul.{u_2, u_5, u_5} (α := R) ((f : (a : M) → R) m : R) p)

Tactic:
rw [smul_comm]

Premises used: SMulCommClass.smul_comm
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
m : Type u_7
n : Type u_8
inst_5 : Fintype m
inst_6 : Finite n
inst_7 : DecidableEq m
inst_8 : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i : n
a :
  ∀ (i' : n) (j' : m),
    Eq.{u_2 + 1} (α := R)
      ((toMatrix bM bN : (a : M →ₗ[R] N) → Matrix n m R)
          ((dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) (bM.coord j ⊗ₜ[R] (bN : (a : n) → N) i)) i' j' :
        R)
      (Matrix.single i j 1 i' j' : R)
⊢ Eq (α := Matrix n m R)
    ((toMatrix bM bN : (a : M →ₗ[R] N) → Matrix n m R)
        ((dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) (bM.coord j ⊗ₜ[R] (bN : (a : n) → N) i)) :
      Matrix n m R)
    (Matrix.single i j 1 : Matrix n m R)

Tactic:
ext i' j'
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
m : Type u_7
n : Type u_8
inst_5 : Fintype m
inst_6 : Finite n
inst_7 : DecidableEq m
inst_8 : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
pos :
  ∀ (hij : i = i' ∧ j = j'),
    Eq.{u_2 + 1} (α := R)
      ((toMatrix bM bN : (a : M →ₗ[R] N) → Matrix n m R)
          ((dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) (bM.coord j ⊗ₜ[R] (bN : (a : n) → N) i)) i' j' :
        R)
      (Matrix.single i j 1 i' j' : R)
neg :
  ∀ (hij : ¬(i = i' ∧ j = j')),
    Eq.{u_2 + 1} (α := R)
      ((toMatrix bM bN : (a : M →ₗ[R] N) → Matrix n m R)
          ((dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) (bM.coord j ⊗ₜ[R] (bN : (a : n) → N) i)) i' j' :
        R)
      (Matrix.single i j 1 i' j' : R)
⊢ Eq.{u_2 + 1} (α := R)
    ((toMatrix bM bN : (a : M →ₗ[R] N) → Matrix n m R)
        ((dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) (bM.coord j ⊗ₜ[R] (bN : (a : n) → N) i)) i' j' :
      R)
    (Matrix.single i j 1 i' j' : R)

Tactic:
by_cases hij : i = i' ∧ j = j'
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
m : Type u_7
n : Type u_8
inst_5 : Fintype m
inst_6 : Finite n
inst_7 : DecidableEq m
inst_8 : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
hij : i = i' ∧ j = j'
⊢ Eq.{u_2 + 1} (α := R)
    ((toMatrix bM bN : (a : M →ₗ[R] N) → Matrix n m R)
        ((dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) (bM.coord j ⊗ₜ[R] (bN : (a : n) → N) i)) i' j' :
      R)
    (Matrix.single i j 1 i' j' : R)

Tactic:
simp [LinearMap.toMatrix_apply, hij]

Premises used: LinearMap.toMatrix_apply
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
m : Type u_7
n : Type u_8
inst_5 : Fintype m
inst_6 : Finite n
inst_7 : DecidableEq m
inst_8 : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
hij : ¬(i = i' ∧ j = j')
⊢ ¬i = i' ∨ ¬j = j'

Tactic:
rw [and_iff_not_or_not, Classical.not_not] at hij

Premises used: Classical.not_not, and_iff_not_or_not
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
m : Type u_7
n : Type u_8
inst_5 : Fintype m
inst_6 : Finite n
inst_7 : DecidableEq m
inst_8 : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
hij : ¬i = i' ∨ ¬j = j'
neg :
  ∀ (hij : ¬i = i'),
    Eq.{u_2 + 1} (α := R)
      ((toMatrix bM bN : (a : M →ₗ[R] N) → Matrix n m R)
          ((dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) (bM.coord j ⊗ₜ[R] (bN : (a : n) → N) i)) i' j' :
        R)
      (Matrix.single i j 1 i' j' : R)
neg₁ :
  ∀ (hij : ¬j = j'),
    Eq.{u_2 + 1} (α := R)
      ((toMatrix bM bN : (a : M →ₗ[R] N) → Matrix n m R)
          ((dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) (bM.coord j ⊗ₜ[R] (bN : (a : n) → N) i)) i' j' :
        R)
      (Matrix.single i j 1 i' j' : R)
⊢ Eq.{u_2 + 1} (α := R)
    ((toMatrix bM bN : (a : M →ₗ[R] N) → Matrix n m R)
        ((dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) (bM.coord j ⊗ₜ[R] (bN : (a : n) → N) i)) i' j' :
      R)
    (Matrix.single i j 1 i' j' : R)

Tactic:
rcases hij with hij | hij
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
m : Type u_7
n : Type u_8
inst_5 : Fintype m
inst_6 : Finite n
inst_7 : DecidableEq m
inst_8 : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
hij : ¬i = i'
⊢ Eq.{u_2 + 1} (α := R)
    ((toMatrix bM bN : (a : M →ₗ[R] N) → Matrix n m R)
        ((dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) (bM.coord j ⊗ₜ[R] (bN : (a : n) → N) i)) i' j' :
      R)
    (Matrix.single i j 1 i' j' : R)

Tactic:
simp [LinearMap.toMatrix_apply, Finsupp.single_eq_pi_single, hij]

Premises used: Finsupp.single_eq_pi_single, LinearMap.toMatrix_apply
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
m : Type u_7
n : Type u_8
inst_5 : Fintype m
inst_6 : Finite n
inst_7 : DecidableEq m
inst_8 : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
hij : ¬j = j'
⊢ Eq.{u_2 + 1} (α := R)
    ((toMatrix bM bN : (a : M →ₗ[R] N) → Matrix n m R)
        ((dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) (bM.coord j ⊗ₜ[R] (bN : (a : n) → N) i)) i' j' :
      R)
    (Matrix.single i j 1 i' j' : R)

Tactic:
simp [LinearMap.toMatrix_apply, Finsupp.single_eq_pi_single, hij]

Premises used: Finsupp.single_eq_pi_single, LinearMap.toMatrix_apply
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
inst_9 : DecidableEq ι
inst_10 : Fintype ι
b : Basis ι R M
h :
  ∀ (f : M →ₗ[R] N) (m : M),
    Eq.{u_4 + 1} (α := N)
      ((((dualTensorHom R M N ∘ₗ
                    ∑ i : ι,
                      (TensorProduct.mk R (Dual R M) N : (a : Dual R M) → N →ₗ[R] Dual R M ⊗[R] N)
                          ((b.dualBasis : (a : ι) → Dual R M) i) ∘ₗ
                        (applyₗ : (a : M) → (M →ₗ[R] N) →ₗ[R] N) ((b : (a : ι) → M) i) :
                  (a : M →ₗ[R] N) → M →ₗ[R] N)
                f :
              M →ₗ[R] N) :
            (a : M) → N)
          m :
        N)
      ((((LinearMap.id : (a : M →ₗ[R] N) → M →ₗ[R] N) f : M →ₗ[R] N) : (a : M) → N) m : N)
⊢ Eq (α := (M →ₗ[R] N) →ₗ[R] M →ₗ[R] N)
    (dualTensorHom R M N ∘ₗ
      ∑ i : ι,
        (TensorProduct.mk R (Dual R M) N : (a : Dual R M) → N →ₗ[R] Dual R M ⊗[R] N)
            ((b.dualBasis : (a : ι) → Dual R M) i) ∘ₗ
          (applyₗ : (a : M) → (M →ₗ[R] N) →ₗ[R] N) ((b : (a : ι) → M) i))
    LinearMap.id

Tactic:
ext f m
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
inst_9 : DecidableEq ι
inst_10 : Fintype ι
b : Basis ι R M
f : M →ₗ[R] N
m : M
⊢ Eq.{u_4 + 1} (α := N)
    ((((dualTensorHom R M N ∘ₗ
                  ∑ i : ι,
                    (TensorProduct.mk R (Dual R M) N : (a : Dual R M) → N →ₗ[R] Dual R M ⊗[R] N)
                        ((b.dualBasis : (a : ι) → Dual R M) i) ∘ₗ
                      (applyₗ : (a : M) → (M →ₗ[R] N) →ₗ[R] N) ((b : (a : ι) → M) i) :
                (a : M →ₗ[R] N) → M →ₗ[R] N)
              f :
            M →ₗ[R] N) :
          (a : M) → N)
        m :
      N)
    ((((LinearMap.id : (a : M →ₗ[R] N) → M →ₗ[R] N) f : M →ₗ[R] N) : (a : M) → N) m : N)

Tactic:
simp only [applyₗ_apply_apply, coe_sum, dualTensorHom_apply, mk_apply, id_coe, _root_.id,
        Fintype.sum_apply, Function.comp_apply, Basis.coe_dualBasis, coe_comp, Basis.coord_apply, ←
        f.map_smul, _root_.map_sum (dualTensorHom R M N), ← _root_.map_sum f, b.sum_repr]

Premises used: Module.Basis.coe_dualBasis, LinearMap.id_coe, TensorProduct.mk_apply, dualTensorHom_apply, dualTensorHom, id, LinearMap.coe_sum, map_sum, LinearMap.coe_comp, LinearMap.map_smul, Function.comp_apply, Fintype.sum_apply, Module.Basis.sum_repr, Module.Basis.coord_apply, LinearMap.applyₗ_apply_apply
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
inst_9 : DecidableEq ι
inst_10 : Fintype ι
b : Basis ι R M
H :
  ∀ (f : Dual R M) (m : N),
    Eq (α := Dual R M ⊗[R] N)
      ((((compr₂ₛₗ (TensorProduct.mk R (Dual R M) N)
                    ((∑ i : ι,
                        (TensorProduct.mk R (Dual R M) N : (a : Dual R M) → N →ₗ[R] Dual R M ⊗[R] N)
                            ((b.dualBasis : (a : ι) → Dual R M) i) ∘ₗ
                          (applyₗ : (a : M) → (M →ₗ[R] N) →ₗ[R] N) ((b : (a : ι) → M) i)) ∘ₗ
                      dualTensorHom R M N) :
                  (a : Dual R M) → N →ₗ[R] Dual R M ⊗[R] N)
                f :
              N →ₗ[R] Dual R M ⊗[R] N) :
            (a : N) → Dual R M ⊗[R] N)
          m :
        Dual R M ⊗[R] N)
      ((((compr₂ₛₗ (TensorProduct.mk R (Dual R M) N) LinearMap.id : (a : Dual R M) → N →ₗ[R] Dual R M ⊗[R] N) f :
              N →ₗ[R] Dual R M ⊗[R] N) :
            (a : N) → Dual R M ⊗[R] N)
          m :
        Dual R M ⊗[R] N)
⊢ Eq (α := Dual R M ⊗[R] N →ₗ[R] Dual R M ⊗[R] N)
    ((∑ i : ι,
        (TensorProduct.mk R (Dual R M) N : (a : Dual R M) → N →ₗ[R] Dual R M ⊗[R] N)
            ((b.dualBasis : (a : ι) → Dual R M) i) ∘ₗ
          (applyₗ : (a : M) → (M →ₗ[R] N) →ₗ[R] N) ((b : (a : ι) → M) i)) ∘ₗ
      dualTensorHom R M N)
    LinearMap.id

Tactic:
ext f m
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
inst_9 : DecidableEq ι
inst_10 : Fintype ι
b : Basis ι R M
f : Dual R M
m : N
⊢ Eq (α := Dual R M ⊗[R] N)
    ((((compr₂ₛₗ (TensorProduct.mk R (Dual R M) N)
                  ((∑ i : ι,
                      (TensorProduct.mk R (Dual R M) N : (a : Dual R M) → N →ₗ[R] Dual R M ⊗[R] N)
                          ((b.dualBasis : (a : ι) → Dual R M) i) ∘ₗ
                        (applyₗ : (a : M) → (M →ₗ[R] N) →ₗ[R] N) ((b : (a : ι) → M) i)) ∘ₗ
                    dualTensorHom R M N) :
                (a : Dual R M) → N →ₗ[R] Dual R M ⊗[R] N)
              f :
            N →ₗ[R] Dual R M ⊗[R] N) :
          (a : N) → Dual R M ⊗[R] N)
        m :
      Dual R M ⊗[R] N)
    ((((compr₂ₛₗ (TensorProduct.mk R (Dual R M) N) LinearMap.id : (a : Dual R M) → N →ₗ[R] Dual R M ⊗[R] N) f :
            N →ₗ[R] Dual R M ⊗[R] N) :
          (a : N) → Dual R M ⊗[R] N)
        m :
      Dual R M ⊗[R] N)

Tactic:
simp only [applyₗ_apply_apply, coe_sum, dualTensorHom_apply, mk_apply, id_coe, _root_.id,
        Fintype.sum_apply, Function.comp_apply, Basis.coe_dualBasis, coe_comp, compr₂ₛₗ_apply,
        tmul_smul, smul_tmul', ← sum_tmul, Basis.sum_dual_apply_smul_coord]

Premises used: Module.Basis.coe_dualBasis, LinearMap.id_coe, TensorProduct.mk_apply, dualTensorHom_apply, TensorProduct.tmul_smul, id, LinearMap.coe_sum, Module.Basis.sum_dual_apply_smul_coord, TensorProduct.sum_tmul, TensorProduct.smul_tmul', LinearMap.coe_comp, Function.comp_apply, Fintype.sum_apply, LinearMap.compr₂ₛₗ_apply, LinearMap.applyₗ_apply_apply
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Fintype ι
b : Basis ι R M
x : Dual R M ⊗[R] N
h :
  ∀ (x_1 : M),
    Eq.{u_4 + 1} (α := N)
      ((((dualTensorHomEquivOfBasis b : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) x_1 : N)
      ((((dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) x_1 : N)
⊢ Eq (α := M →ₗ[R] N) ((dualTensorHomEquivOfBasis b : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) x : M →ₗ[R] N)
    ((dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) x : M →ₗ[R] N)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Fintype ι
b : Basis ι R M
x : Dual R M ⊗[R] N
x_1 : M
⊢ Eq.{u_4 + 1} (α := N)
    ((((dualTensorHomEquivOfBasis b : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) x_1 : N)
    ((((dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) x_1 : N)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Fintype ι
b : Basis ι R M
⊢ Eq (α := Dual R M ⊗[R] N →ₗ[R] M →ₗ[R] N) (↑(dualTensorHomEquivOfBasis b) : Dual R M ⊗[R] N →ₗ[R] M →ₗ[R] N)
    (dualTensorHom R M N)

Tactic:
rfl

Premises used: dualTensorHom, rfl
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Fintype ι
b : Basis ι R M
x : Dual R M ⊗[R] N
rw :
  (LinearEquiv.symm (dualTensorHomEquivOfBasis b) : (a : M →ₗ[R] N) → Dual R M ⊗[R] N)
      ((dualTensorHomEquivOfBasis b : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) x) =
    x
rw₁ rw₂ : x = x
⊢ (LinearEquiv.symm (dualTensorHomEquivOfBasis b) : (a : M →ₗ[R] N) → Dual R M ⊗[R] N)
      ((dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) x) =
    x

Tactic:
rw [← dualTensorHomEquivOfBasis_apply b,
    LinearEquiv.symm_apply_apply <| dualTensorHomEquivOfBasis (N := N) b]

Premises used: LinearEquiv.symm_apply_apply, dualTensorHomEquivOfBasis, dualTensorHomEquivOfBasis_apply