[GOAL]
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)ᵐᵒᵖ :=
  LinearEquiv.trans
    (TensorProduct.AlgebraTensorModule.congr (LinearEquiv.symm (opLinearEquiv S)) (LinearEquiv.symm (opLinearEquiv R)))
    (opLinearEquiv S)
e₂ : A ⊗[R] B ≃ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ :=
  LinearEquiv.trans (TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R)) (opLinearEquiv S)
⊢ ↑AlgHom.op.symm
      (AlgHom.comp
        (algHomOfLinearMapTensorProduct ↑e₁
          (_ :
            ∀ (a₁ a₂ : Aᵐᵒᵖ) (b₁ b₂ : Bᵐᵒᵖ), ↑↑e₁ ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = ↑↑e₁ (a₁ ⊗ₜ[R] b₁) * ↑↑e₁ (a₂ ⊗ₜ[R] b₂))
          (_ : ∀ (r : S), ↑↑e₁ (↑(algebraMap S Aᵐᵒᵖ) r ⊗ₜ[R] 1) = ↑(algebraMap S (A ⊗[R] B)ᵐᵒᵖ) r))
        (↑AlgHom.opComm
          (algHomOfLinearMapTensorProduct ↑e₂
            (_ : ∀ (a₁ a₂ : A) (b₁ b₂ : B), ↑↑e₂ ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = ↑↑e₂ (a₁ ⊗ₜ[R] b₁) * ↑↑e₂ (a₂ ⊗ₜ[R] b₂))
            (_ : ∀ (r : S), ↑↑e₂ (↑(algebraMap S A) r ⊗ₜ[R] 1) = ↑(algebraMap S (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) r)))) =
    ↑AlgHom.op.symm (AlgHom.id S (A ⊗[R] B)ᵐᵒᵖ)
[PROOFSTEP]
ext
[GOAL]
case ha.H
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)ᵐᵒᵖ :=
  LinearEquiv.trans
    (TensorProduct.AlgebraTensorModule.congr (LinearEquiv.symm (opLinearEquiv S)) (LinearEquiv.symm (opLinearEquiv R)))
    (opLinearEquiv S)
e₂ : A ⊗[R] B ≃ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ :=
  LinearEquiv.trans (TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R)) (opLinearEquiv S)
x✝ : A
⊢ ↑(AlgHom.comp
          (↑AlgHom.op.symm
            (AlgHom.comp
              (algHomOfLinearMapTensorProduct ↑e₁
                (_ :
                  ∀ (a₁ a₂ : Aᵐᵒᵖ) (b₁ b₂ : Bᵐᵒᵖ),
                    ↑↑e₁ ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = ↑↑e₁ (a₁ ⊗ₜ[R] b₁) * ↑↑e₁ (a₂ ⊗ₜ[R] b₂))
                (_ : ∀ (r : S), ↑↑e₁ (↑(algebraMap S Aᵐᵒᵖ) r ⊗ₜ[R] 1) = ↑(algebraMap S (A ⊗[R] B)ᵐᵒᵖ) r))
              (↑AlgHom.opComm
                (algHomOfLinearMapTensorProduct ↑e₂
                  (_ :
                    ∀ (a₁ a₂ : A) (b₁ b₂ : B),
                      ↑↑e₂ ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = ↑↑e₂ (a₁ ⊗ₜ[R] b₁) * ↑↑e₂ (a₂ ⊗ₜ[R] b₂))
                  (_ : ∀ (r : S), ↑↑e₂ (↑(algebraMap S A) r ⊗ₜ[R] 1) = ↑(algebraMap S (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) r)))))
          includeLeft)
      x✝ =
    ↑(AlgHom.comp (↑AlgHom.op.symm (AlgHom.id S (A ⊗[R] B)ᵐᵒᵖ)) includeLeft) x✝
[PROOFSTEP]
rfl
[GOAL]
case hb.H
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)ᵐᵒᵖ :=
  LinearEquiv.trans
    (TensorProduct.AlgebraTensorModule.congr (LinearEquiv.symm (opLinearEquiv S)) (LinearEquiv.symm (opLinearEquiv R)))
    (opLinearEquiv S)
e₂ : A ⊗[R] B ≃ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ :=
  LinearEquiv.trans (TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R)) (opLinearEquiv S)
x✝ : B
⊢ ↑(AlgHom.comp
          (AlgHom.restrictScalars R
            (↑AlgHom.op.symm
              (AlgHom.comp
                (algHomOfLinearMapTensorProduct ↑e₁
                  (_ :
                    ∀ (a₁ a₂ : Aᵐᵒᵖ) (b₁ b₂ : Bᵐᵒᵖ),
                      ↑↑e₁ ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = ↑↑e₁ (a₁ ⊗ₜ[R] b₁) * ↑↑e₁ (a₂ ⊗ₜ[R] b₂))
                  (_ : ∀ (r : S), ↑↑e₁ (↑(algebraMap S Aᵐᵒᵖ) r ⊗ₜ[R] 1) = ↑(algebraMap S (A ⊗[R] B)ᵐᵒᵖ) r))
                (↑AlgHom.opComm
                  (algHomOfLinearMapTensorProduct ↑e₂
                    (_ :
                      ∀ (a₁ a₂ : A) (b₁ b₂ : B),
                        ↑↑e₂ ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = ↑↑e₂ (a₁ ⊗ₜ[R] b₁) * ↑↑e₂ (a₂ ⊗ₜ[R] b₂))
                    (_ : ∀ (r : S), ↑↑e₂ (↑(algebraMap S A) r ⊗ₜ[R] 1) = ↑(algebraMap S (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) r))))))
          includeRight)
      x✝ =
    ↑(AlgHom.comp (AlgHom.restrictScalars R (↑AlgHom.op.symm (AlgHom.id S (A ⊗[R] B)ᵐᵒᵖ))) includeRight) x✝
[PROOFSTEP]
rfl
[GOAL]
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)ᵐᵒᵖ :=
  LinearEquiv.trans
    (TensorProduct.AlgebraTensorModule.congr (LinearEquiv.symm (opLinearEquiv S)) (LinearEquiv.symm (opLinearEquiv R)))
    (opLinearEquiv S)
e₂ : A ⊗[R] B ≃ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ :=
  LinearEquiv.trans (TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R)) (opLinearEquiv S)
⊢ AlgHom.comp
      (↑AlgHom.opComm
        (algHomOfLinearMapTensorProduct ↑e₂
          (_ : ∀ (a₁ a₂ : A) (b₁ b₂ : B), ↑↑e₂ ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = ↑↑e₂ (a₁ ⊗ₜ[R] b₁) * ↑↑e₂ (a₂ ⊗ₜ[R] b₂))
          (_ : ∀ (r : S), ↑↑e₂ (↑(algebraMap S A) r ⊗ₜ[R] 1) = ↑(algebraMap S (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) r)))
      (algHomOfLinearMapTensorProduct ↑e₁
        (_ :
          ∀ (a₁ a₂ : Aᵐᵒᵖ) (b₁ b₂ : Bᵐᵒᵖ), ↑↑e₁ ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = ↑↑e₁ (a₁ ⊗ₜ[R] b₁) * ↑↑e₁ (a₂ ⊗ₜ[R] b₂))
        (_ : ∀ (r : S), ↑↑e₁ (↑(algebraMap S Aᵐᵒᵖ) r ⊗ₜ[R] 1) = ↑(algebraMap S (A ⊗[R] B)ᵐᵒᵖ) r)) =
    AlgHom.id S (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)
[PROOFSTEP]
ext
[GOAL]
case ha.H
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)ᵐᵒᵖ :=
  LinearEquiv.trans
    (TensorProduct.AlgebraTensorModule.congr (LinearEquiv.symm (opLinearEquiv S)) (LinearEquiv.symm (opLinearEquiv R)))
    (opLinearEquiv S)
e₂ : A ⊗[R] B ≃ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ :=
  LinearEquiv.trans (TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R)) (opLinearEquiv S)
x✝ : Aᵐᵒᵖ
⊢ ↑(AlgHom.comp
          (AlgHom.comp
            (↑AlgHom.opComm
              (algHomOfLinearMapTensorProduct ↑e₂
                (_ :
                  ∀ (a₁ a₂ : A) (b₁ b₂ : B), ↑↑e₂ ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = ↑↑e₂ (a₁ ⊗ₜ[R] b₁) * ↑↑e₂ (a₂ ⊗ₜ[R] b₂))
                (_ : ∀ (r : S), ↑↑e₂ (↑(algebraMap S A) r ⊗ₜ[R] 1) = ↑(algebraMap S (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) r)))
            (algHomOfLinearMapTensorProduct ↑e₁
              (_ :
                ∀ (a₁ a₂ : Aᵐᵒᵖ) (b₁ b₂ : Bᵐᵒᵖ),
                  ↑↑e₁ ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = ↑↑e₁ (a₁ ⊗ₜ[R] b₁) * ↑↑e₁ (a₂ ⊗ₜ[R] b₂))
              (_ : ∀ (r : S), ↑↑e₁ (↑(algebraMap S Aᵐᵒᵖ) r ⊗ₜ[R] 1) = ↑(algebraMap S (A ⊗[R] B)ᵐᵒᵖ) r)))
          includeLeft)
      x✝ =
    ↑(AlgHom.comp (AlgHom.id S (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)) includeLeft) x✝
[PROOFSTEP]
rfl
[GOAL]
case hb.H
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)ᵐᵒᵖ :=
  LinearEquiv.trans
    (TensorProduct.AlgebraTensorModule.congr (LinearEquiv.symm (opLinearEquiv S)) (LinearEquiv.symm (opLinearEquiv R)))
    (opLinearEquiv S)
e₂ : A ⊗[R] B ≃ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ :=
  LinearEquiv.trans (TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R)) (opLinearEquiv S)
x✝ : Bᵐᵒᵖ
⊢ ↑(AlgHom.comp
          (AlgHom.restrictScalars R
            (AlgHom.comp
              (↑AlgHom.opComm
                (algHomOfLinearMapTensorProduct ↑e₂
                  (_ :
                    ∀ (a₁ a₂ : A) (b₁ b₂ : B),
                      ↑↑e₂ ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = ↑↑e₂ (a₁ ⊗ₜ[R] b₁) * ↑↑e₂ (a₂ ⊗ₜ[R] b₂))
                  (_ : ∀ (r : S), ↑↑e₂ (↑(algebraMap S A) r ⊗ₜ[R] 1) = ↑(algebraMap S (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) r)))
              (algHomOfLinearMapTensorProduct ↑e₁
                (_ :
                  ∀ (a₁ a₂ : Aᵐᵒᵖ) (b₁ b₂ : Bᵐᵒᵖ),
                    ↑↑e₁ ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = ↑↑e₁ (a₁ ⊗ₜ[R] b₁) * ↑↑e₁ (a₂ ⊗ₜ[R] b₂))
                (_ : ∀ (r : S), ↑↑e₁ (↑(algebraMap S Aᵐᵒᵖ) r ⊗ₜ[R] 1) = ↑(algebraMap S (A ⊗[R] B)ᵐᵒᵖ) r))))
          includeRight)
      x✝ =
    ↑(AlgHom.comp (AlgHom.restrictScalars R (AlgHom.id S (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ))) includeRight) x✝
[PROOFSTEP]
rfl
