awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact mul_comm _ _

Premises used: mul_comm
-- Module: Mathlib.LinearAlgebra.TensorProduct.Matrix
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_7
κ : Type u_8
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : CommRing R
inst_5 : AddCommGroup M
inst_6 : AddCommGroup N
inst_7 : Module R M
inst_8 : Module R N
bM : Basis ι R M
bN : Basis κ R N
a :
  ∀ (i : κ) (j i' : ι) (j' : κ),
    Eq.{u_1 + 1} (α := R)
      (((toMatrix (bM.tensorProduct bN) (bN.tensorProduct bM) :
              (M ⊗[R] N →ₗ[R] N ⊗[R] M) ≃ₗ[R] Matrix (κ × ι) (ι × κ) R) :
            (a : M ⊗[R] N →ₗ[R] N ⊗[R] M) → Matrix (κ × ι) (ι × κ) R)
          (↑(TensorProduct.comm R M N) : M ⊗[R] N →ₗ[R] N ⊗[R] M) (i, j) (i', j') :
        R)
      (submatrix 1 Prod.swap _root_.id (i, j) (i', j') : R)
⊢ Eq (α := Matrix (κ × ι) (ι × κ) R)
    (((toMatrix (bM.tensorProduct bN) (bN.tensorProduct bM) :
            (M ⊗[R] N →ₗ[R] N ⊗[R] M) ≃ₗ[R] Matrix (κ × ι) (ι × κ) R) :
          (a : M ⊗[R] N →ₗ[R] N ⊗[R] M) → Matrix (κ × ι) (ι × κ) R)
        (↑(TensorProduct.comm R M N) : M ⊗[R] N →ₗ[R] N ⊗[R] M) :
      Matrix (κ × ι) (ι × κ) R)
    (submatrix 1 Prod.swap _root_.id : 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
ι : Type u_7
κ : Type u_8
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : CommRing R
inst_5 : AddCommGroup M
inst_6 : AddCommGroup N
inst_7 : Module R M
inst_8 : Module R N
bM : Basis ι R M
bN : Basis κ R N
i : κ
j i' : ι
j' : κ
⊢ Eq.{u_1 + 1} (α := R)
    (((toMatrix (bM.tensorProduct bN) (bN.tensorProduct bM) :
            (M ⊗[R] N →ₗ[R] N ⊗[R] M) ≃ₗ[R] Matrix (κ × ι) (ι × κ) R) :
          (a : M ⊗[R] N →ₗ[R] N ⊗[R] M) → Matrix (κ × ι) (ι × κ) R)
        (↑(TensorProduct.comm R M N) : M ⊗[R] N →ₗ[R] N ⊗[R] M) (i, j) (i', j') :
      R)
    (submatrix 1 Prod.swap _root_.id (i, j) (i', j') : R)

Tactic:
simp only [toMatrix_apply, Basis.tensorProduct_apply, LinearEquiv.coe_coe, comm_tmul,
    Basis.tensorProduct_repr_tmul_apply, Basis.repr_self, Finsupp.single_apply, @eq_comm _ i',
    @eq_comm _ j', smul_eq_mul, mul_ite, mul_one, mul_zero, ← ite_and, and_comm, submatrix_apply,
    Matrix.one_apply, Prod.swap_prod_mk, id_eq, Prod.mk.injEq]

Premises used: Module.Basis.tensorProduct_apply, Matrix.one_apply, mul_ite, Prod.swap_prod_mk, and_comm, eq_comm, MulZeroClass.mul_zero, Prod.mk.injEq, Finsupp.single_apply, Matrix.submatrix_apply, TensorProduct.comm_tmul, smul_eq_mul, mul_one, ite_and, Module.Basis.tensorProduct_repr_tmul_apply, Module.Basis.repr_self, LinearMap.toMatrix_apply, LinearEquiv.coe_coe, id_eq
-- Module: Mathlib.LinearAlgebra.TensorProduct.Matrix
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
ι : Type u_7
κ : Type u_8
τ : Type u_9
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : DecidableEq τ
inst_3 : Fintype ι
inst_4 : Fintype κ
inst_5 : Fintype τ
inst_6 : CommRing R
inst_7 : AddCommGroup M
inst_8 : AddCommGroup N
inst_9 : AddCommGroup P
inst_10 : Module R M
inst_11 : Module R N
inst_12 : Module R P
bM : Basis ι R M
bN : Basis κ R N
bP : Basis τ R P
a :
  ∀ (i : ι) (j : κ) (k k' : τ) (i' : ι) (j' : κ),
    Eq.{u_1 + 1} (α := R)
      (((toMatrix (Basis.tensorProduct (bM.tensorProduct bN) bP) (bM.tensorProduct (bN.tensorProduct bP)) :
              (M ⊗[R] N ⊗[R] P →ₗ[R] M ⊗[R] (N ⊗[R] P)) ≃ₗ[R] Matrix (ι × κ × τ) ((ι × κ) × τ) R) :
            (a : M ⊗[R] N ⊗[R] P →ₗ[R] M ⊗[R] (N ⊗[R] P)) → Matrix (ι × κ × τ) ((ι × κ) × τ) R)
          (↑(TensorProduct.assoc R M N P) : M ⊗[R] N ⊗[R] P →ₗ[R] M ⊗[R] (N ⊗[R] P)) (i, j, k) ((i', j'), k') :
        R)
      (submatrix (n := ι × κ × τ) 1 _root_.id (⇑(Equiv.prodAssoc ι κ τ) : (a : (ι × κ) × τ) → ι × κ × τ) (i, j, k)
          ((i', j'), k') :
        R)
⊢ Eq (α := Matrix (ι × κ × τ) ((ι × κ) × τ) R)
    (((toMatrix (Basis.tensorProduct (bM.tensorProduct bN) bP) (bM.tensorProduct (bN.tensorProduct bP)) :
            (M ⊗[R] N ⊗[R] P →ₗ[R] M ⊗[R] (N ⊗[R] P)) ≃ₗ[R] Matrix (ι × κ × τ) ((ι × κ) × τ) R) :
          (a : M ⊗[R] N ⊗[R] P →ₗ[R] M ⊗[R] (N ⊗[R] P)) → Matrix (ι × κ × τ) ((ι × κ) × τ) R)
        (↑(TensorProduct.assoc R M N P) : M ⊗[R] N ⊗[R] P →ₗ[R] M ⊗[R] (N ⊗[R] P)) :
      Matrix (ι × κ × τ) ((ι × κ) × τ) R)
    (submatrix (n := ι × κ × τ) 1 _root_.id (⇑(Equiv.prodAssoc ι κ τ) : (a : (ι × κ) × τ) → ι × κ × τ) :
      Matrix (ι × κ × τ) ((ι × κ) × τ) R)

Tactic:
ext ⟨i, j, k⟩ ⟨⟨i', j'⟩, k'⟩
-- Module: Mathlib.LinearAlgebra.TensorProduct.Matrix
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
ι : Type u_7
κ : Type u_8
τ : Type u_9
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : DecidableEq τ
inst_3 : Fintype ι
inst_4 : Fintype κ
inst_5 : Fintype τ
inst_6 : CommRing R
inst_7 : AddCommGroup M
inst_8 : AddCommGroup N
inst_9 : AddCommGroup P
inst_10 : Module R M
inst_11 : Module R N
inst_12 : Module R P
bM : Basis ι R M
bN : Basis κ R N
bP : Basis τ R P
i : ι
j : κ
k k' : τ
i' : ι
j' : κ
⊢ Eq.{u_1 + 1} (α := R)
    (((toMatrix (Basis.tensorProduct (bM.tensorProduct bN) bP) (bM.tensorProduct (bN.tensorProduct bP)) :
            (M ⊗[R] N ⊗[R] P →ₗ[R] M ⊗[R] (N ⊗[R] P)) ≃ₗ[R] Matrix (ι × κ × τ) ((ι × κ) × τ) R) :
          (a : M ⊗[R] N ⊗[R] P →ₗ[R] M ⊗[R] (N ⊗[R] P)) → Matrix (ι × κ × τ) ((ι × κ) × τ) R)
        (↑(TensorProduct.assoc R M N P) : M ⊗[R] N ⊗[R] P →ₗ[R] M ⊗[R] (N ⊗[R] P)) (i, j, k) ((i', j'), k') :
      R)
    (submatrix (n := ι × κ × τ) 1 _root_.id (⇑(Equiv.prodAssoc ι κ τ) : (a : (ι × κ) × τ) → ι × κ × τ) (i, j, k)
        ((i', j'), k') :
      R)

Tactic:
simp only [toMatrix_apply, Basis.tensorProduct_apply, LinearEquiv.coe_coe, assoc_tmul,
    Basis.tensorProduct_repr_tmul_apply, Basis.repr_self, Finsupp.single_apply, @eq_comm _ k',
    @eq_comm _ j', smul_eq_mul, mul_ite, mul_one, mul_zero, ← ite_and, @eq_comm _ i',
    submatrix_apply, Matrix.one_apply, id_eq, Equiv.prodAssoc_apply, Prod.mk.injEq]

Premises used: Module.Basis.tensorProduct_apply, Matrix.one_apply, Equiv.prodAssoc_apply, mul_ite, TensorProduct.assoc_tmul, eq_comm, MulZeroClass.mul_zero, Prod.mk.injEq, Finsupp.single_apply, Matrix.submatrix_apply, smul_eq_mul, mul_one, ite_and, Module.Basis.tensorProduct_repr_tmul_apply, Module.Basis.repr_self, LinearMap.toMatrix_apply, LinearEquiv.coe_coe, id_eq
-- Module: Mathlib.LinearAlgebra.TensorProduct.Opposite
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra S A
inst_8 : IsScalarTower R S A
e₁ : TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ :=
  (TensorProduct.AlgebraTensorModule.congr (LinearEquiv.symm (opLinearEquiv S)) (LinearEquiv.symm (opLinearEquiv R)) :
      TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ ≃ₗ[S] A ⊗[R] B) ≪≫ₗ
    (opLinearEquiv S : A ⊗[R] B ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ)
e₂ : A ⊗[R] B ≃ₗ[S] (TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)ᵐᵒᵖ :=
  (TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R) :
      A ⊗[R] B ≃ₗ[S] TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ) ≪≫ₗ
    (opLinearEquiv S : TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ ≃ₗ[S] (TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)ᵐᵒᵖ)
a₁ a₂ : Aᵐᵒᵖ
b₁ b₂ : Bᵐᵒᵖ
⊢ unop
      (((↑e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ →ₗ[S] (A ⊗[R] B)ᵐᵒᵖ) : (a : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ) → (A ⊗[R] B)ᵐᵒᵖ)
        ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂))) =
    unop
      (HMul.hMul (α := (A ⊗[R] B)ᵐᵒᵖ) (β := (A ⊗[R] B)ᵐᵒᵖ)
        (((↑e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ →ₗ[S] (A ⊗[R] B)ᵐᵒᵖ) : (a : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ) → (A ⊗[R] B)ᵐᵒᵖ) (a₁ ⊗ₜ[R] b₁) :
          (A ⊗[R] B)ᵐᵒᵖ)
        (((↑e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ →ₗ[S] (A ⊗[R] B)ᵐᵒᵖ) : (a : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ) → (A ⊗[R] B)ᵐᵒᵖ) (a₂ ⊗ₜ[R] b₂) :
          (A ⊗[R] B)ᵐᵒᵖ))

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Opposite
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra S A
inst_8 : IsScalarTower R S A
e₁ : TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ :=
  (TensorProduct.AlgebraTensorModule.congr (LinearEquiv.symm (opLinearEquiv S)) (LinearEquiv.symm (opLinearEquiv R)) :
      TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ ≃ₗ[S] A ⊗[R] B) ≪≫ₗ
    (opLinearEquiv S : A ⊗[R] B ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ)
e₂ : A ⊗[R] B ≃ₗ[S] (TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)ᵐᵒᵖ :=
  (TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R) :
      A ⊗[R] B ≃ₗ[S] TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ) ≪≫ₗ
    (opLinearEquiv S : TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ ≃ₗ[S] (TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)ᵐᵒᵖ)
a₁ a₂ : Aᵐᵒᵖ
b₁ b₂ : Bᵐᵒᵖ
⊢ unop
      (((↑e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ →ₗ[S] (A ⊗[R] B)ᵐᵒᵖ) : (a : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ) → (A ⊗[R] B)ᵐᵒᵖ)
        ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂))) =
    unop
      (HMul.hMul (α := (A ⊗[R] B)ᵐᵒᵖ) (β := (A ⊗[R] B)ᵐᵒᵖ)
        (((↑e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ →ₗ[S] (A ⊗[R] B)ᵐᵒᵖ) : (a : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ) → (A ⊗[R] B)ᵐᵒᵖ) (a₁ ⊗ₜ[R] b₁) :
          (A ⊗[R] B)ᵐᵒᵖ)
        (((↑e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ →ₗ[S] (A ⊗[R] B)ᵐᵒᵖ) : (a : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ) → (A ⊗[R] B)ᵐᵒᵖ) (a₂ ⊗ₜ[R] b₂) :
          (A ⊗[R] B)ᵐᵒᵖ))

Tactic:
with_unfolding_all rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Opposite
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra S A
inst_8 : IsScalarTower R S A
e₁ : TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ :=
  (TensorProduct.AlgebraTensorModule.congr (LinearEquiv.symm (opLinearEquiv S)) (LinearEquiv.symm (opLinearEquiv R)) :
      TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ ≃ₗ[S] A ⊗[R] B) ≪≫ₗ
    (opLinearEquiv S : A ⊗[R] B ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ)
e₂ : A ⊗[R] B ≃ₗ[S] (TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)ᵐᵒᵖ :=
  (TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R) :
      A ⊗[R] B ≃ₗ[S] TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ) ≪≫ₗ
    (opLinearEquiv S : TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ ≃ₗ[S] (TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)ᵐᵒᵖ)
a₁ a₂ : A
b₁ b₂ : B
⊢ unop
      (((↑e₂ : A ⊗[R] B →ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) : (a : A ⊗[R] B) → (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ)
        ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂))) =
    unop
      (HMul.hMul (α := (TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)ᵐᵒᵖ) (β :=
        (TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)ᵐᵒᵖ)
        (((↑e₂ : A ⊗[R] B →ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) : (a : A ⊗[R] B) → (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) (a₁ ⊗ₜ[R] b₁) :
          (TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)ᵐᵒᵖ)
        (((↑e₂ : A ⊗[R] B →ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) : (a : A ⊗[R] B) → (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) (a₂ ⊗ₜ[R] b₂) :
          (TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)ᵐᵒᵖ))

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Opposite
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra S A
inst_8 : IsScalarTower R S A
e₁ : TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ :=
  (TensorProduct.AlgebraTensorModule.congr (LinearEquiv.symm (opLinearEquiv S)) (LinearEquiv.symm (opLinearEquiv R)) :
      TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ ≃ₗ[S] A ⊗[R] B) ≪≫ₗ
    (opLinearEquiv S : A ⊗[R] B ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ)
e₂ : A ⊗[R] B ≃ₗ[S] (TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)ᵐᵒᵖ :=
  (TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R) :
      A ⊗[R] B ≃ₗ[S] TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ) ≪≫ₗ
    (opLinearEquiv S : TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ ≃ₗ[S] (TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)ᵐᵒᵖ)
a₁ a₂ : A
b₁ b₂ : B
⊢ unop
      (((↑e₂ : A ⊗[R] B →ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) : (a : A ⊗[R] B) → (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ)
        ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂))) =
    unop
      (HMul.hMul (α := (TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)ᵐᵒᵖ) (β :=
        (TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)ᵐᵒᵖ)
        (((↑e₂ : A ⊗[R] B →ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) : (a : A ⊗[R] B) → (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) (a₁ ⊗ₜ[R] b₁) :
          (TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)ᵐᵒᵖ)
        (((↑e₂ : A ⊗[R] B →ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) : (a : A ⊗[R] B) → (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) (a₂ ⊗ₜ[R] b₂) :
          (TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)ᵐᵒᵖ))

Tactic:
with_unfolding_all rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Opposite
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra S A
inst_8 : IsScalarTower R S A
e₁ : TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ :=
  (TensorProduct.AlgebraTensorModule.congr (LinearEquiv.symm (opLinearEquiv S)) (LinearEquiv.symm (opLinearEquiv R)) :
      TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ ≃ₗ[S] A ⊗[R] B) ≪≫ₗ
    (opLinearEquiv S : A ⊗[R] B ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ)
e₂ : A ⊗[R] B ≃ₗ[S] (TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)ᵐᵒᵖ :=
  (TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R) :
      A ⊗[R] B ≃ₗ[S] TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ) ≪≫ₗ
    (opLinearEquiv S : TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ ≃ₗ[S] (TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)ᵐᵒᵖ)
x : A
⊢ Eq (α := A ⊗[R] B)
    ((AlgHom.comp (B := A ⊗[R] B)
            ((Equiv.symm AlgHom.op : (a : (A ⊗[R] B)ᵐᵒᵖ →ₐ[S] (A ⊗[R] B)ᵐᵒᵖ) → A ⊗[R] B →ₐ[S] A ⊗[R] B)
              (AlgHom.comp (B := TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)
                (algHomOfLinearMapTensorProduct (↑e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ →ₗ[S] (A ⊗[R] B)ᵐᵒᵖ) ⋯ ⋯ :
                  TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ →ₐ[S] (A ⊗[R] B)ᵐᵒᵖ)
                ((AlgHom.opComm : (a : A ⊗[R] B →ₐ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) → (A ⊗[R] B)ᵐᵒᵖ →ₐ[S] Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)
                    (algHomOfLinearMapTensorProduct (↑e₂ : A ⊗[R] B →ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) ⋯ ⋯) :
                  (A ⊗[R] B)ᵐᵒᵖ →ₐ[S] TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)))
            includeLeft :
          (a : A) → A ⊗[R] B)
        x :
      A ⊗[R] B)
    ((AlgHom.comp (B := A ⊗[R] B)
            ((Equiv.symm AlgHom.op : (a : (A ⊗[R] B)ᵐᵒᵖ →ₐ[S] (A ⊗[R] B)ᵐᵒᵖ) → A ⊗[R] B →ₐ[S] A ⊗[R] B)
              (AlgHom.id S (A ⊗[R] B)ᵐᵒᵖ))
            includeLeft :
          (a : A) → A ⊗[R] B)
        x :
      A ⊗[R] B)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Opposite
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra S A
inst_8 : IsScalarTower R S A
e₁ : TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ :=
  (TensorProduct.AlgebraTensorModule.congr (LinearEquiv.symm (opLinearEquiv S)) (LinearEquiv.symm (opLinearEquiv R)) :
      TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ ≃ₗ[S] A ⊗[R] B) ≪≫ₗ
    (opLinearEquiv S : A ⊗[R] B ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ)
e₂ : A ⊗[R] B ≃ₗ[S] (TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)ᵐᵒᵖ :=
  (TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R) :
      A ⊗[R] B ≃ₗ[S] TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ) ≪≫ₗ
    (opLinearEquiv S : TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ ≃ₗ[S] (TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)ᵐᵒᵖ)
x : B
⊢ Eq (α := A ⊗[R] B)
    ((AlgHom.comp (B := A ⊗[R] B)
            (AlgHom.restrictScalars R (S := S)
              ((Equiv.symm AlgHom.op : (a : (A ⊗[R] B)ᵐᵒᵖ →ₐ[S] (A ⊗[R] B)ᵐᵒᵖ) → A ⊗[R] B →ₐ[S] A ⊗[R] B)
                (AlgHom.comp (B := TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)
                  (algHomOfLinearMapTensorProduct (↑e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ →ₗ[S] (A ⊗[R] B)ᵐᵒᵖ) ⋯ ⋯ :
                    TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ →ₐ[S] (A ⊗[R] B)ᵐᵒᵖ)
                  ((AlgHom.opComm : (a : A ⊗[R] B →ₐ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) → (A ⊗[R] B)ᵐᵒᵖ →ₐ[S] Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)
                      (algHomOfLinearMapTensorProduct (↑e₂ : A ⊗[R] B →ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) ⋯ ⋯) :
                    (A ⊗[R] B)ᵐᵒᵖ →ₐ[S] TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ))))
            includeRight :
          (a : B) → A ⊗[R] B)
        x :
      A ⊗[R] B)
    ((AlgHom.comp (B := A ⊗[R] B)
            (AlgHom.restrictScalars R (S := S)
              ((Equiv.symm AlgHom.op : (a : (A ⊗[R] B)ᵐᵒᵖ →ₐ[S] (A ⊗[R] B)ᵐᵒᵖ) → A ⊗[R] B →ₐ[S] A ⊗[R] B)
                (AlgHom.id S (A ⊗[R] B)ᵐᵒᵖ)))
            includeRight :
          (a : B) → A ⊗[R] B)
        x :
      A ⊗[R] B)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Opposite
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra S A
inst_8 : IsScalarTower R S A
e₁ : TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ :=
  (TensorProduct.AlgebraTensorModule.congr (LinearEquiv.symm (opLinearEquiv S)) (LinearEquiv.symm (opLinearEquiv R)) :
      TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ ≃ₗ[S] A ⊗[R] B) ≪≫ₗ
    (opLinearEquiv S : A ⊗[R] B ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ)
e₂ : A ⊗[R] B ≃ₗ[S] (TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)ᵐᵒᵖ :=
  (TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R) :
      A ⊗[R] B ≃ₗ[S] TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ) ≪≫ₗ
    (opLinearEquiv S : TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ ≃ₗ[S] (TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)ᵐᵒᵖ)
x : Aᵐᵒᵖ
⊢ Eq (α := TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)
    ((AlgHom.comp (B := TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)
            (AlgHom.comp (B := (A ⊗[R] B)ᵐᵒᵖ)
                ((AlgHom.opComm : (a : A ⊗[R] B →ₐ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) → (A ⊗[R] B)ᵐᵒᵖ →ₐ[S] Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)
                  (algHomOfLinearMapTensorProduct (↑e₂ : A ⊗[R] B →ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) ⋯ ⋯))
                (algHomOfLinearMapTensorProduct (↑e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ →ₗ[S] (A ⊗[R] B)ᵐᵒᵖ) ⋯ ⋯) :
              TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ →ₐ[S] TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)
            (includeLeft : Aᵐᵒᵖ →ₐ[S] TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ) :
          (a : Aᵐᵒᵖ) → Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)
        x :
      TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)
    (((AlgHom.comp (AlgHom.id S (TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)) includeLeft :
            Aᵐᵒᵖ →ₐ[S] TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ) :
          (a : Aᵐᵒᵖ) → Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)
        x :
      TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Opposite
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra S A
inst_8 : IsScalarTower R S A
e₁ : TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ :=
  (TensorProduct.AlgebraTensorModule.congr (LinearEquiv.symm (opLinearEquiv S)) (LinearEquiv.symm (opLinearEquiv R)) :
      TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ ≃ₗ[S] A ⊗[R] B) ≪≫ₗ
    (opLinearEquiv S : A ⊗[R] B ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ)
e₂ : A ⊗[R] B ≃ₗ[S] (TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)ᵐᵒᵖ :=
  (TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R) :
      A ⊗[R] B ≃ₗ[S] TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ) ≪≫ₗ
    (opLinearEquiv S : TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ ≃ₗ[S] (TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)ᵐᵒᵖ)
x : Bᵐᵒᵖ
⊢ Eq (α := TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)
    ((AlgHom.comp (B := TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)
            (AlgHom.restrictScalars R (S := S)
              (AlgHom.comp (B := (A ⊗[R] B)ᵐᵒᵖ)
                  ((AlgHom.opComm : (a : A ⊗[R] B →ₐ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) → (A ⊗[R] B)ᵐᵒᵖ →ₐ[S] Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)
                    (algHomOfLinearMapTensorProduct (↑e₂ : A ⊗[R] B →ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) ⋯ ⋯))
                  (algHomOfLinearMapTensorProduct (↑e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ →ₗ[S] (A ⊗[R] B)ᵐᵒᵖ) ⋯ ⋯) :
                TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ →ₐ[S] TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ))
            includeRight :
          (a : Bᵐᵒᵖ) → Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)
        x :
      TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)
    (((AlgHom.comp (AlgHom.restrictScalars R (AlgHom.id S (TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ))) includeRight :
            Bᵐᵒᵖ →ₐ[R] TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ) :
          (a : Bᵐᵒᵖ) → Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)
        x :
      TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Opposite
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra S A
inst_8 : IsScalarTower R S A
x : TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ
⊢ Eq (α := (A ⊗[R] B)ᵐᵒᵖ)
    (((opAlgEquiv R S A B : TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ ≃ₐ[S] (A ⊗[R] B)ᵐᵒᵖ) :
          (a : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ) → (A ⊗[R] B)ᵐᵒᵖ)
        x :
      (A ⊗[R] B)ᵐᵒᵖ)
    (op
        ((_root_.TensorProduct.map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)
              (↑(LinearEquiv.symm (opLinearEquiv R)) : Bᵐᵒᵖ →ₗ[R] B) :
            (a : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ) → A ⊗[R] B)
          x) :
      (A ⊗[R] B)ᵐᵒᵖ)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, rfl, MulOpposite.op
-- Module: Mathlib.LinearAlgebra.TensorProduct.Opposite
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra S A
inst_8 : IsScalarTower R S A
x : (A ⊗[R] B)ᵐᵒᵖ
⊢ Eq (α := TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)
    (((AlgEquiv.symm (opAlgEquiv R S A B) : (A ⊗[R] B)ᵐᵒᵖ ≃ₐ[S] TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ) :
          (a : (A ⊗[R] B)ᵐᵒᵖ) → Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)
        x :
      TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)
    ((_root_.TensorProduct.map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (↑(opLinearEquiv R) : B →ₗ[R] Bᵐᵒᵖ) :
          (a : A ⊗[R] B) → Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)
        (unop x) :
      TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, MulOpposite.unop, TensorProduct.tmul, AddCon.toQuotient, rfl