awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
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 : M ≃ₗ[R] P
g : N ≃ₗ[R] Q
⊢ rTensor N f ≪≫ₗ lTensor P g = TensorProduct.congr f g

Tactic:
toLinearMap_injective <| LinearMap.lTensor_comp_rTensor M _ _

Premises used: LinearEquiv.toLinearMap_injective, LinearMap.lTensor_comp_rTensor
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
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 : M ≃ₗ[R] P
g : N ≃ₗ[R] Q
⊢ lTensor M g ≪≫ₗ rTensor Q f = TensorProduct.congr f g

Tactic:
toLinearMap_injective <| LinearMap.rTensor_comp_lTensor M _ _

Premises used: LinearMap.rTensor_comp_lTensor, LinearEquiv.toLinearMap_injective
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : AddCommMonoid S
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R S
inst_9 : Module R P
inst_10 : Module R Q
f : M ≃ₗ[R] P
g : N ≃ₗ[R] Q
f' : S ≃ₗ[R] M
⊢ rTensor N f' ≪≫ₗ TensorProduct.congr f g = TensorProduct.congr (f' ≪≫ₗ f) g

Tactic:
toLinearMap_injective <| LinearMap.map_comp_rTensor M _ _ _

Premises used: LinearEquiv.toLinearMap_injective, LinearMap.map_comp_rTensor
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : AddCommMonoid S
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R S
inst_9 : Module R P
inst_10 : Module R Q
f : M ≃ₗ[R] P
g : N ≃ₗ[R] Q
g' : S ≃ₗ[R] N
⊢ lTensor M g' ≪≫ₗ TensorProduct.congr f g = TensorProduct.congr f (g' ≪≫ₗ g)

Tactic:
toLinearMap_injective <| LinearMap.map_comp_lTensor M _ _ _

Premises used: LinearEquiv.toLinearMap_injective, LinearMap.map_comp_lTensor
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : AddCommMonoid S
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R S
inst_9 : Module R P
inst_10 : Module R Q
f' : P ≃ₗ[R] S
f : M ≃ₗ[R] P
g : N ≃ₗ[R] Q
⊢ TensorProduct.congr f g ≪≫ₗ rTensor Q f' = TensorProduct.congr (f ≪≫ₗ f') g

Tactic:
toLinearMap_injective <| LinearMap.rTensor_comp_map M _ _ _

Premises used: LinearMap.rTensor_comp_map, LinearEquiv.toLinearMap_injective
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : AddCommMonoid S
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R S
inst_9 : Module R P
inst_10 : Module R Q
g' : Q ≃ₗ[R] S
f : M ≃ₗ[R] P
g : N ≃ₗ[R] Q
⊢ TensorProduct.congr f g ≪≫ₗ lTensor P g' = TensorProduct.congr f (g ≪≫ₗ g')

Tactic:
toLinearMap_injective <| LinearMap.lTensor_comp_map M _ _ _

Premises used: LinearEquiv.toLinearMap_injective, LinearMap.lTensor_comp_map
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
f : M ≃ₗ[R] M
n : ℕ
⊢ HPow.hPow (α := M ⊗[R] N ≃ₗ[R] M ⊗[R] N) (rTensor N f) n = rTensor N (f ^ n)

Tactic:
simpa only [one_pow] using TensorProduct.congr_pow f (1 : N ≃ₗ[R] N) n

Premises used: one_pow, TensorProduct.congr_pow, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
f : M ≃ₗ[R] M
n : ℤ
⊢ HPow.hPow (α := M ⊗[R] N ≃ₗ[R] M ⊗[R] N) (rTensor N f) n = rTensor N (f ^ n)

Tactic:
simpa only [one_zpow] using TensorProduct.congr_zpow f (1 : N ≃ₗ[R] N) n

Premises used: TensorProduct.congr_zpow, one_zpow, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
f : N ≃ₗ[R] N
n : ℕ
⊢ HPow.hPow (α := M ⊗[R] N ≃ₗ[R] M ⊗[R] N) (lTensor M f) n = lTensor M (f ^ n)

Tactic:
simpa only [one_pow] using TensorProduct.congr_pow (1 : M ≃ₗ[R] M) f n

Premises used: one_pow, TensorProduct.congr_pow, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
f : N ≃ₗ[R] N
n : ℤ
⊢ HPow.hPow (α := M ⊗[R] N ≃ₗ[R] M ⊗[R] N) (lTensor M f) n = lTensor M (f ^ n)

Tactic:
simpa only [one_zpow] using TensorProduct.congr_zpow (1 : M ≃ₗ[R] M) f n

Premises used: TensorProduct.congr_zpow, one_zpow, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
inst_1 : AddCommGroup M
inst_2 : AddCommMonoid N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f g : N →ₗ[R] P
⊢ (lTensorHom M : (a : N →ₗ[R] P) → TensorProduct R M N →ₗ[R] TensorProduct R M P) (f - g) =
    HSub.hSub (α := TensorProduct R M N →ₗ[R] TensorProduct R M P) (β := TensorProduct R M N →ₗ[R] TensorProduct R M P)
      ((lTensorHom M : (a : N →ₗ[R] P) → TensorProduct R M N →ₗ[R] TensorProduct R M P) f :
        TensorProduct R M N →ₗ[R] TensorProduct R M P)
      ((lTensorHom M : (a : N →ₗ[R] P) → TensorProduct R M N →ₗ[R] TensorProduct R M P) g :
        TensorProduct R M N →ₗ[R] TensorProduct R M P)

Tactic:
(lTensorHom (R := R) (N := N) (P := P) M).map_sub f g

Premises used: LinearMap.lTensorHom, LinearMap.map_sub
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
inst_1 : AddCommGroup M
inst_2 : AddCommMonoid N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f g : N →ₗ[R] P
⊢ (lTensorHom M : (a : N →ₗ[R] P) → TensorProduct R M N →ₗ[R] TensorProduct R M P) (f - g) =
    HSub.hSub (α := TensorProduct R M N →ₗ[R] TensorProduct R M P) (β := TensorProduct R M N →ₗ[R] TensorProduct R M P)
      ((lTensorHom M : (a : N →ₗ[R] P) → TensorProduct R M N →ₗ[R] TensorProduct R M P) f :
        TensorProduct R M N →ₗ[R] TensorProduct R M P)
      ((lTensorHom M : (a : N →ₗ[R] P) → TensorProduct R M N →ₗ[R] TensorProduct R M P) g :
        TensorProduct R M N →ₗ[R] TensorProduct R M P)

Tactic:
exact (lTensorHom (R := R) (N := N) (P := P) M).map_sub f g

Premises used: LinearMap.lTensorHom, LinearMap.map_sub
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommGroup P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
f g : N →ₗ[R] P
⊢ (rTensorHom Q : (a : N →ₗ[R] P) → TensorProduct R N Q →ₗ[R] TensorProduct R P Q) (f - g) =
    HSub.hSub (α := TensorProduct R N Q →ₗ[R] TensorProduct R P Q) (β := TensorProduct R N Q →ₗ[R] TensorProduct R P Q)
      ((rTensorHom Q : (a : N →ₗ[R] P) → TensorProduct R N Q →ₗ[R] TensorProduct R P Q) f :
        TensorProduct R N Q →ₗ[R] TensorProduct R P Q)
      ((rTensorHom Q : (a : N →ₗ[R] P) → TensorProduct R N Q →ₗ[R] TensorProduct R P Q) g :
        TensorProduct R N Q →ₗ[R] TensorProduct R P Q)

Tactic:
(rTensorHom (R := R) (N := N) (P := P) Q).map_sub f g

Premises used: LinearMap.rTensorHom, LinearMap.map_sub
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommGroup P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
f g : N →ₗ[R] P
⊢ (rTensorHom Q : (a : N →ₗ[R] P) → TensorProduct R N Q →ₗ[R] TensorProduct R P Q) (f - g) =
    HSub.hSub (α := TensorProduct R N Q →ₗ[R] TensorProduct R P Q) (β := TensorProduct R N Q →ₗ[R] TensorProduct R P Q)
      ((rTensorHom Q : (a : N →ₗ[R] P) → TensorProduct R N Q →ₗ[R] TensorProduct R P Q) f :
        TensorProduct R N Q →ₗ[R] TensorProduct R P Q)
      ((rTensorHom Q : (a : N →ₗ[R] P) → TensorProduct R N Q →ₗ[R] TensorProduct R P Q) g :
        TensorProduct R N Q →ₗ[R] TensorProduct R P Q)

Tactic:
exact (rTensorHom (R := R) (N := N) (P := P) Q).map_sub f g

Premises used: LinearMap.rTensorHom, LinearMap.map_sub
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
inst_1 : AddCommGroup M
inst_2 : AddCommMonoid N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : N →ₗ[R] P
⊢ Eq (α := TensorProduct R M N →ₗ[R] TensorProduct R M P)
    ((lTensorHom M : (a : N →ₗ[R] P) → TensorProduct R M N →ₗ[R] TensorProduct R M P) (-f) :
      TensorProduct R M N →ₗ[R] TensorProduct R M P)
    (-(lTensorHom M : (a : N →ₗ[R] P) → TensorProduct R M N →ₗ[R] TensorProduct R M P) f :
      TensorProduct R M N →ₗ[R] TensorProduct R M P)

Tactic:
(lTensorHom (R := R) (N := N) (P := P) M).map_neg f

Premises used: LinearMap.map_neg, LinearMap.lTensorHom
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
inst_1 : AddCommGroup M
inst_2 : AddCommMonoid N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : N →ₗ[R] P
⊢ Eq (α := TensorProduct R M N →ₗ[R] TensorProduct R M P)
    ((lTensorHom M : (a : N →ₗ[R] P) → TensorProduct R M N →ₗ[R] TensorProduct R M P) (-f) :
      TensorProduct R M N →ₗ[R] TensorProduct R M P)
    (-(lTensorHom M : (a : N →ₗ[R] P) → TensorProduct R M N →ₗ[R] TensorProduct R M P) f :
      TensorProduct R M N →ₗ[R] TensorProduct R M P)

Tactic:
exact (lTensorHom (R := R) (N := N) (P := P) M).map_neg f

Premises used: LinearMap.map_neg, LinearMap.lTensorHom
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommGroup P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
f : N →ₗ[R] P
⊢ Eq (α := TensorProduct R N Q →ₗ[R] TensorProduct R P Q)
    ((rTensorHom Q : (a : N →ₗ[R] P) → TensorProduct R N Q →ₗ[R] TensorProduct R P Q) (-f) :
      TensorProduct R N Q →ₗ[R] TensorProduct R P Q)
    (-(rTensorHom Q : (a : N →ₗ[R] P) → TensorProduct R N Q →ₗ[R] TensorProduct R P Q) f :
      TensorProduct R N Q →ₗ[R] TensorProduct R P Q)

Tactic:
(rTensorHom (R := R) (N := N) (P := P) Q).map_neg f

Premises used: LinearMap.rTensorHom, LinearMap.map_neg
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommGroup P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
f : N →ₗ[R] P
⊢ Eq (α := TensorProduct R N Q →ₗ[R] TensorProduct R P Q)
    ((rTensorHom Q : (a : N →ₗ[R] P) → TensorProduct R N Q →ₗ[R] TensorProduct R P Q) (-f) :
      TensorProduct R N Q →ₗ[R] TensorProduct R P Q)
    (-(rTensorHom Q : (a : N →ₗ[R] P) → TensorProduct R N Q →ₗ[R] TensorProduct R P Q) f :
      TensorProduct R N Q →ₗ[R] TensorProduct R P Q)

Tactic:
exact (rTensorHom (R := R) (N := N) (P := P) Q).map_neg f

Premises used: LinearMap.rTensorHom, LinearMap.map_neg
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
B' : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid A'
inst_2 : AddCommMonoid B'
inst_3 : Module R A'
inst_4 : Module R B'
eA : A ≃ A'
eB : B ≃ B'
h :
  ∀ (x : A ⊗[R] B),
    Eq (α := B ⊗[R] A) ((TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) x : B ⊗[R] A)
      ((TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
              (TensorProduct.comm R A' B' ≪≫ₗ
                TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eA))) :
            (a : A ⊗[R] B) → B ⊗[R] A)
          x :
        B ⊗[R] A)
⊢ Eq (α := A ⊗[R] B ≃ₗ[R] B ⊗[R] A) (TensorProduct.comm R A B)
    (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
      (TensorProduct.comm R A' B' ≪≫ₗ
        TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eA))))

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
B' : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid A'
inst_2 : AddCommMonoid B'
inst_3 : Module R A'
inst_4 : Module R B'
eA : A ≃ A'
eB : B ≃ B'
x : A ⊗[R] B
h :
  Eq (α := B ⊗[R] A) ((TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) 0)
    ((TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
          (TensorProduct.comm R A' B' ≪≫ₗ
            TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eA))) :
        (a : A ⊗[R] B) → B ⊗[R] A)
      0)
h₁ :
  ∀ (x : A) (y : B),
    Eq (α := B ⊗[R] A) ((TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) (x ⊗ₜ[R] y) : B ⊗[R] A)
      ((TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
              (TensorProduct.comm R A' B' ≪≫ₗ
                TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eA))) :
            (a : A ⊗[R] B) → B ⊗[R] A)
          (x ⊗ₜ[R] y) :
        B ⊗[R] A)
h₂ :
  ∀ (x y : A ⊗[R] B),
    Eq (α := B ⊗[R] A) ((TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) x : B ⊗[R] A)
        ((TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
                (TensorProduct.comm R A' B' ≪≫ₗ
                  TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eA))) :
              (a : A ⊗[R] B) → B ⊗[R] A)
            x :
          B ⊗[R] A) →
      Eq (α := B ⊗[R] A) ((TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) y : B ⊗[R] A)
          ((TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
                  (TensorProduct.comm R A' B' ≪≫ₗ
                    TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eA))) :
                (a : A ⊗[R] B) → B ⊗[R] A)
              y :
            B ⊗[R] A) →
        Eq (α := B ⊗[R] A) ((TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) (x + y) : B ⊗[R] A)
          ((TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
                  (TensorProduct.comm R A' B' ≪≫ₗ
                    TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eA))) :
                (a : A ⊗[R] B) → B ⊗[R] A)
              (x + y) :
            B ⊗[R] A)
⊢ Eq (α := B ⊗[R] A) ((TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) x : B ⊗[R] A)
    ((TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
            (TensorProduct.comm R A' B' ≪≫ₗ
              TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eA))) :
          (a : A ⊗[R] B) → B ⊗[R] A)
        x :
      B ⊗[R] A)

Tactic:
induction x
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
B' : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid A'
inst_2 : AddCommMonoid B'
inst_3 : Module R A'
inst_4 : Module R B'
eA : A ≃ A'
eB : B ≃ B'
⊢ Eq (α := B ⊗[R] A) ((TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) 0)
    ((TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
          (TensorProduct.comm R A' B' ≪≫ₗ
            TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eA))) :
        (a : A ⊗[R] B) → B ⊗[R] A)
      0)

Tactic:
simp [*]
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
B' : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid A'
inst_2 : AddCommMonoid B'
inst_3 : Module R A'
inst_4 : Module R B'
eA : A ≃ A'
eB : B ≃ B'
x : A
y : B
⊢ Eq (α := B ⊗[R] A) ((TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) (x ⊗ₜ[R] y) : B ⊗[R] A)
    ((TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
            (TensorProduct.comm R A' B' ≪≫ₗ
              TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eA))) :
          (a : A ⊗[R] B) → B ⊗[R] A)
        (x ⊗ₜ[R] y) :
      B ⊗[R] A)

Tactic:
simp [*]
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
B' : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid A'
inst_2 : AddCommMonoid B'
inst_3 : Module R A'
inst_4 : Module R B'
eA : A ≃ A'
eB : B ≃ B'
x y : A ⊗[R] B
h :
  Eq (α := B ⊗[R] A) ((TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) x : B ⊗[R] A)
    ((TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
            (TensorProduct.comm R A' B' ≪≫ₗ
              TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eA))) :
          (a : A ⊗[R] B) → B ⊗[R] A)
        x :
      B ⊗[R] A)
h_1 :
  Eq (α := B ⊗[R] A) ((TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) y : B ⊗[R] A)
    ((TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
            (TensorProduct.comm R A' B' ≪≫ₗ
              TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eA))) :
          (a : A ⊗[R] B) → B ⊗[R] A)
        y :
      B ⊗[R] A)
⊢ Eq (α := B ⊗[R] A) ((TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) (x + y) : B ⊗[R] A)
    ((TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
            (TensorProduct.comm R A' B' ≪≫ₗ
              TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eA))) :
          (a : A ⊗[R] B) → B ⊗[R] A)
        (x + y) :
      B ⊗[R] A)

Tactic:
simp [*]
-- Module: Mathlib.LinearAlgebra.TensorProduct.Matrix
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
ι' : Type u_10
κ' : Type u_11
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : Finite ι'
inst_5 : Finite κ'
inst_6 : CommRing R
inst_7 : AddCommGroup M
inst_8 : AddCommGroup N
inst_9 : AddCommGroup M'
inst_10 : AddCommGroup N'
inst_11 : Module R M
inst_12 : Module R N
inst_13 : Module R M'
inst_14 : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bM' : Basis ι' R M'
bN' : Basis κ' R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
a :
  ∀ (i : ι') (j : κ') (i' : ι) (j' : κ),
    Eq.{u_1 + 1} (α := R)
      (((toMatrix (bM.tensorProduct bN) (bM'.tensorProduct bN') :
              (M ⊗[R] N →ₗ[R] M' ⊗[R] N') ≃ₗ[R] Matrix (ι' × κ') (ι × κ) R) :
            (a : M ⊗[R] N →ₗ[R] M' ⊗[R] N') → Matrix (ι' × κ') (ι × κ) R)
          (map f g) (i, j) (i', j') :
        R)
      (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) ((toMatrix bM bM' : (a : M →ₗ[R] M') → Matrix ι' ι R) f)
          ((toMatrix bN bN' : (a : N →ₗ[R] N') → Matrix κ' κ R) g) (i, j) (i', j') :
        R)
⊢ Eq (α := Matrix (ι' × κ') (ι × κ) R)
    (((toMatrix (bM.tensorProduct bN) (bM'.tensorProduct bN') :
            (M ⊗[R] N →ₗ[R] M' ⊗[R] N') ≃ₗ[R] Matrix (ι' × κ') (ι × κ) R) :
          (a : M ⊗[R] N →ₗ[R] M' ⊗[R] N') → Matrix (ι' × κ') (ι × κ) R)
        (map f g) :
      Matrix (ι' × κ') (ι × κ) R)
    (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) ((toMatrix bM bM' : (a : M →ₗ[R] M') → Matrix ι' ι R) f)
        ((toMatrix bN bN' : (a : N →ₗ[R] N') → Matrix κ' κ R) g) :
      Matrix (ι' × κ') (ι × κ) R)

Tactic:
ext ⟨i, j⟩ ⟨i', j'⟩
-- Module: Mathlib.LinearAlgebra.TensorProduct.Matrix
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
ι' : Type u_10
κ' : Type u_11
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : Finite ι'
inst_5 : Finite κ'
inst_6 : CommRing R
inst_7 : AddCommGroup M
inst_8 : AddCommGroup N
inst_9 : AddCommGroup M'
inst_10 : AddCommGroup N'
inst_11 : Module R M
inst_12 : Module R N
inst_13 : Module R M'
inst_14 : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bM' : Basis ι' R M'
bN' : Basis κ' R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
i : ι'
j : κ'
i' : ι
j' : κ
a :
  HSMul.hSMul (α := R) (β := R)
      ((((bN'.repr : (a : N') → κ' →₀ R) ((g : (a : N) → N') ((bN : (a : κ) → N) j' : N)) : κ' →₀ R) : (a : κ') → R) j :
        R)
      ((((bM'.repr : (a : M') → ι' →₀ R) ((f : (a : M) → M') ((bM : (a : ι) → M) i' : M)) : ι' →₀ R) : (a : ι') → R) i :
        R) =
    HMul.hMul (α := R) (β := R)
      ((((bM'.repr : (a : M') → ι' →₀ R) ((f : (a : M) → M') ((bM : (a : ι) → M) i' : M)) : ι' →₀ R) : (a : ι') → R) i :
        R)
      ((((bN'.repr : (a : N') → κ' →₀ R) ((g : (a : N) → N') ((bN : (a : κ) → N) j' : N)) : κ' →₀ R) : (a : κ') → R) j :
        R)
⊢ Eq.{u_1 + 1} (α := R)
    (((toMatrix (bM.tensorProduct bN) (bM'.tensorProduct bN') :
            (M ⊗[R] N →ₗ[R] M' ⊗[R] N') ≃ₗ[R] Matrix (ι' × κ') (ι × κ) R) :
          (a : M ⊗[R] N →ₗ[R] M' ⊗[R] N') → Matrix (ι' × κ') (ι × κ) R)
        (map f g) (i, j) (i', j') :
      R)
    (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) ((toMatrix bM bM' : (a : M →ₗ[R] M') → Matrix ι' ι R) f)
        ((toMatrix bN bN' : (a : N →ₗ[R] N') → Matrix κ' κ R) g) (i, j) (i', j') :
      R)

Tactic:
simp_rw [Matrix.kroneckerMap_apply, toMatrix_apply, Basis.tensorProduct_apply,
    TensorProduct.map_tmul, Basis.tensorProduct_repr_tmul_apply]

Premises used: Module.Basis.tensorProduct_apply, Matrix.kroneckerMap_apply, TensorProduct.map_tmul, Module.Basis.tensorProduct_repr_tmul_apply, LinearMap.toMatrix_apply
-- Module: Mathlib.LinearAlgebra.TensorProduct.Matrix
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
ι' : Type u_10
κ' : Type u_11
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : Finite ι'
inst_5 : Finite κ'
inst_6 : CommRing R
inst_7 : AddCommGroup M
inst_8 : AddCommGroup N
inst_9 : AddCommGroup M'
inst_10 : AddCommGroup N'
inst_11 : Module R M
inst_12 : Module R N
inst_13 : Module R M'
inst_14 : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bM' : Basis ι' R M'
bN' : Basis κ' R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
i : ι'
j : κ'
i' : ι
j' : κ
⊢ HSMul.hSMul (α := R) (β := R)
      ((((bN'.repr : (a : N') → κ' →₀ R) ((g : (a : N) → N') ((bN : (a : κ) → N) j' : N)) : κ' →₀ R) : (a : κ') → R) j :
        R)
      ((((bM'.repr : (a : M') → ι' →₀ R) ((f : (a : M) → M') ((bM : (a : ι) → M) i' : M)) : ι' →₀ R) : (a : ι') → R) i :
        R) =
    HMul.hMul (α := R) (β := R)
      ((((bM'.repr : (a : M') → ι' →₀ R) ((f : (a : M) → M') ((bM : (a : ι) → M) i' : M)) : ι' →₀ R) : (a : ι') → R) i :
        R)
      ((((bN'.repr : (a : N') → κ' →₀ R) ((g : (a : N) → N') ((bN : (a : κ) → N) j' : N)) : κ' →₀ R) : (a : κ') → R) j :
        R)

Tactic:
mul_comm _ _

Premises used: mul_comm