-- Module: Mathlib.Algebra.Algebra.Subalgebra.Centralizer
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
B : Type u_3
inst_3 : Semiring B
inst_4 : Algebra R B
S : Set B
inst_5 : Module.Free R A
eq1 :
  Eq (α := Subalgebra R (A ⊗[R] B))
    (comap (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
      (centralizer R ((⇑includeLeft : (a : B) → B ⊗[R] A) '' S)))
    (comap (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
      (AlgHom.range (A := TensorProduct.{u_1, u_3, u_2} R (↥(centralizer R S)) A)
        (Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R A) :
          TensorProduct.{u_1, u_3, u_2} R (↥(centralizer R S)) A →ₐ[R] B ⊗[R] A)))
x : A ⊗[R] B
y : TensorProduct.{u_1, u_3, u_2} R (↥(centralizer R S)) A
hy :
  Eq (α := B ⊗[R] A)
    (((Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R A) :
            TensorProduct.{u_1, u_3, u_2} R (↥(centralizer R S)) A →ₐ[R] B ⊗[R] A) :
          (a : ↥(centralizer R S) ⊗[R] A) → B ⊗[R] A)
        y :
      B ⊗[R] A)
    ((Algebra.TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) x : B ⊗[R] A)
h :
  Eq (α := B ⊗[R] A)
    ((Algebra.TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A)
        (((Algebra.TensorProduct.map (AlgHom.id R A) (val (centralizer R S)) :
              TensorProduct.{u_1, u_2, u_3} R A ↥(centralizer R S) →ₐ[R] A ⊗[R] B) :
            (a : A ⊗[R] ↥(centralizer R S)) → A ⊗[R] B)
          ((Algebra.TensorProduct.comm R (↥(centralizer R S)) A :
              (a : ↥(centralizer R S) ⊗[R] A) → A ⊗[R] ↥(centralizer R S))
            y)) :
      B ⊗[R] A)
    (((Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R A) :
            TensorProduct.{u_1, u_3, u_2} R (↥(centralizer R S)) A →ₐ[R] B ⊗[R] A) :
          (a : ↥(centralizer R S) ⊗[R] A) → B ⊗[R] A)
        y :
      B ⊗[R] A)
h₁ :
  Eq (α := B ⊗[R] A)
    (((Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R A) :
            TensorProduct.{u_1, u_3, u_2} R (↥(centralizer R S)) A →ₐ[R] B ⊗[R] A) :
          (a : ↥(centralizer R S) ⊗[R] A) → B ⊗[R] A)
        ((Algebra.TensorProduct.comm R A ↥(centralizer R S) :
            (a : A ⊗[R] ↥(centralizer R S)) → ↥(centralizer R S) ⊗[R] A)
          ((Algebra.TensorProduct.comm R (↥(centralizer R S)) A :
              (a : ↥(centralizer R S) ⊗[R] A) → A ⊗[R] ↥(centralizer R S))
            y)) :
      B ⊗[R] A)
    (((Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R A) :
            TensorProduct.{u_1, u_3, u_2} R (↥(centralizer R S)) A →ₐ[R] B ⊗[R] A) :
          (a : ↥(centralizer R S) ⊗[R] A) → B ⊗[R] A)
        y :
      B ⊗[R] A)
h₂ :
  Eq (α := B ⊗[R] A)
    (((Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R A) :
            TensorProduct.{u_1, u_3, u_2} R (↥(centralizer R S)) A →ₐ[R] B ⊗[R] A) :
          (a : ↥(centralizer R S) ⊗[R] A) → B ⊗[R] A)
        ((AlgEquiv.symm (Algebra.TensorProduct.comm R (↥(centralizer R S)) A) :
            (a : A ⊗[R] ↥(centralizer R S)) → ↥(centralizer R S) ⊗[R] A)
          ((Algebra.TensorProduct.comm R (↥(centralizer R S)) A :
              (a : ↥(centralizer R S) ⊗[R] A) → A ⊗[R] ↥(centralizer R S))
            y)) :
      B ⊗[R] A)
    (((Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R A) :
            TensorProduct.{u_1, u_3, u_2} R (↥(centralizer R S)) A →ₐ[R] B ⊗[R] A) :
          (a : ↥(centralizer R S) ⊗[R] A) → B ⊗[R] A)
        y :
      B ⊗[R] A)
h₃ h₄ :
  Eq (α := B ⊗[R] A)
    (((Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R A) :
            TensorProduct.{u_1, u_3, u_2} R (↥(centralizer R S)) A →ₐ[R] B ⊗[R] A) :
          (a : ↥(centralizer R S) ⊗[R] A) → B ⊗[R] A)
        y :
      B ⊗[R] A)
    (((Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R A) :
            TensorProduct.{u_1, u_3, u_2} R (↥(centralizer R S)) A →ₐ[R] B ⊗[R] A) :
          (a : ↥(centralizer R S) ⊗[R] A) → B ⊗[R] A)
        y :
      B ⊗[R] A)
⊢ Eq (α := B ⊗[R] A)
    ((Algebra.TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A)
        (((Algebra.TensorProduct.map (AlgHom.id R A) (val (centralizer R S)) :
              TensorProduct.{u_1, u_2, u_3} R A ↥(centralizer R S) →ₐ[R] A ⊗[R] B) :
            (a : A ⊗[R] ↥(centralizer R S)) → A ⊗[R] B)
          ((Algebra.TensorProduct.comm R (↥(centralizer R S)) A :
              (a : ↥(centralizer R S) ⊗[R] A) → A ⊗[R] ↥(centralizer R S))
            y)) :
      B ⊗[R] A)
    ((Algebra.TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) x : B ⊗[R] A)

Tactic:
rw [← hy, comm_comp_map_apply, ← Algebra.TensorProduct.comm_symm, AlgEquiv.symm_apply_apply]

Premises used: Algebra.TensorProduct.comm_comp_map_apply, AlgEquiv.symm_apply_apply, Algebra.TensorProduct.comm_symm