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.opComm (algHomOfLinearMapTensorProduct ↑e₂ ⋯ ⋯)).comp (algHomOfLinearMapTensorProduct ↑e₁ ⋯ ⋯)).comp
        includeLeft)
      x✝ =
    ((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.opComm (algHomOfLinearMapTensorProduct ↑e₂ ⋯ ⋯)).comp
              (algHomOfLinearMapTensorProduct ↑e₁ ⋯ ⋯))).comp
        includeRight)
      x✝ =
    ((AlgHom.restrictScalars R (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.opComm (algHomOfLinearMapTensorProduct ↑e₂ ⋯ ⋯)).comp (algHomOfLinearMapTensorProduct ↑e₁ ⋯ ⋯)).comp
        includeLeft)
      x✝ =
    ((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.opComm (algHomOfLinearMapTensorProduct ↑e₂ ⋯ ⋯)).comp
              (algHomOfLinearMapTensorProduct ↑e₁ ⋯ ⋯))).comp
        includeRight)
      x✝ =
    ((AlgHom.restrictScalars R (AlgHom.id S (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ))).comp includeRight) x✝