-- 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 (α := 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)
⊢ Eq (α := A ⊗[R] B →ₐ[S] 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ᵐᵒᵖ)) :
      A ⊗[R] B →ₐ[S] 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)ᵐᵒᵖ) :
      A ⊗[R] B →ₐ[S] A ⊗[R] B)
have hb : ∀ (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)ᵐᵒᵖ) sorry sorry :
                    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ᵐᵒᵖ)ᵐᵒᵖ) sorry sorry) :
                    (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: ext