Module: Mathlib.LinearAlgebra.TensorProduct.Opposite

Goal state before:
pp: case ha
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S).symm (opLinearEquiv R).symm ≪≫ₗ opLinearEquiv S
e₂ : A ⊗[R] B ≃ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R) ≪≫ₗ opLinearEquiv S
x✝ : A
⊢ ((AlgHom.op.symm
            ((algHomOfLinearMapTensorProduct ↑e₁ ⋯ ⋯).comp
              (AlgHom.opComm (algHomOfLinearMapTensorProduct ↑e₂ ⋯ ⋯)))).comp
        includeLeft)
      x✝ =
    ((AlgHom.op.symm (AlgHom.id S (A ⊗[R] B)ᵐᵒᵖ)).comp includeLeft) x✝

pp: case hb
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S).symm (opLinearEquiv R).symm ≪≫ₗ opLinearEquiv S
e₂ : A ⊗[R] B ≃ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R) ≪≫ₗ opLinearEquiv S
x✝ : B
⊢ ((AlgHom.restrictScalars R
            (AlgHom.op.symm
              ((algHomOfLinearMapTensorProduct ↑e₁ ⋯ ⋯).comp
                (AlgHom.opComm (algHomOfLinearMapTensorProduct ↑e₂ ⋯ ⋯))))).comp
        includeRight)
      x✝ =
    ((AlgHom.restrictScalars R (AlgHom.op.symm (AlgHom.id S (A ⊗[R] B)ᵐᵒᵖ))).comp includeRight) x✝

Tactic:
<;>

Goal state after:
case ha
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S).symm (opLinearEquiv R).symm ≪≫ₗ opLinearEquiv S
e₂ : A ⊗[R] B ≃ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R) ≪≫ₗ opLinearEquiv S
x✝ : A
⊢ ((AlgHom.op.symm
            ((algHomOfLinearMapTensorProduct ↑e₁ ⋯ ⋯).comp
              (AlgHom.opComm (algHomOfLinearMapTensorProduct ↑e₂ ⋯ ⋯)))).comp
        includeLeft)
      x✝ =
    ((AlgHom.op.symm (AlgHom.id S (A ⊗[R] B)ᵐᵒᵖ)).comp includeLeft) x✝

case hb
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S).symm (opLinearEquiv R).symm ≪≫ₗ opLinearEquiv S
e₂ : A ⊗[R] B ≃ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R) ≪≫ₗ opLinearEquiv S
x✝ : B
⊢ ((AlgHom.restrictScalars R
            (AlgHom.op.symm
              ((algHomOfLinearMapTensorProduct ↑e₁ ⋯ ⋯).comp
                (AlgHom.opComm (algHomOfLinearMapTensorProduct ↑e₂ ⋯ ⋯))))).comp
        includeRight)
      x✝ =
    ((AlgHom.restrictScalars R (AlgHom.op.symm (AlgHom.id S (A ⊗[R] B)ᵐᵒᵖ))).comp includeRight) x✝