-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Opposite (goal)
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ᵐᵒᵖ)ᵐᵒᵖ)
ha :
  ∀ (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ᵐᵒᵖ)
⊢ Eq (α := TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ →ₐ[S] 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ᵐᵒᵖ)
    (AlgHom.id S (TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ) :
      TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ →ₐ[S] TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)
have hb : ∀ (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ᵐᵒᵖ)ᵐᵒᵖ) sorry sorry))
                  (algHomOfLinearMapTensorProduct (↑e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ →ₗ[S] (A ⊗[R] B)ᵐᵒᵖ) sorry sorry) :
                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: ext