-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B : CommRingCat
s : BinaryCofan A B
m : (↑A : Type u) ⊗[ℤ] (↑B : Type u) →+* (↑s.pt : Type u)
hm : ∀ (j : Discrete WalkingPair), (A.coproductCocone B).ι.app j ≫ { hom' := m } = s.ι.app j
hf :
  Eq.{u + 1} (α := (↑A : Type u) →ₐ[ℤ] (↑s.pt : Type u))
      (AlgHom.comp (B := (↑A : Type u) ⊗[ℤ] (↑B : Type u))
        (RingHom.toIntAlgHom (Hom.hom { hom' := m }) : (↑(A.coproductCocone B).pt : Type u) →ₐ[ℤ] (↑s.pt : Type u))
        Algebra.TensorProduct.includeLeft)
      (((Equiv.symm Algebra.TensorProduct.liftEquiv :
                ((↑A : Type u) ⊗[ℤ] (↑B : Type u) →ₐ[ℤ] (↑s.pt : Type u)) ≃
                  { fg : ((↑A : Type u) →ₐ[ℤ] (↑s.pt : Type u)) × ((↑B : Type u) →ₐ[ℤ] (↑s.pt : Type u)) //
                    ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
                      Commute (S := (↑s.pt : Type u))
                        ((fg.1 : (a : (↑A : Type u)) → (↑s.pt : Type u)) x : (↑s.pt : Type u))
                        ((fg.2 : (a : (↑B : Type u)) → (↑s.pt : Type u)) y : (↑s.pt : Type u)) }) :
              (a : (↑A : Type u) ⊗[ℤ] (↑B : Type u) →ₐ[ℤ] (↑s.pt : Type u)) →
                { fg : ((↑A : Type u) →ₐ[ℤ] (↑s.pt : Type u)) × ((↑B : Type u) →ₐ[ℤ] (↑s.pt : Type u)) //
                  ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
                    Commute ((fg.1 : (a : (↑A : Type u)) → (↑s.pt : Type u)) x)
                      ((fg.2 : (a : (↑B : Type u)) → (↑s.pt : Type u)) y) })
            (Hom.hom
                (ofHom
                  (AlgHom.toRingHom
                    (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯ :
                      (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u) ⊗[ℤ]
                          (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u) →ₐ[ℤ]
                        (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) s.pt)
                              { as := WalkingPair.left : Discrete WalkingPair }) :
                          Type u))))).toIntAlgHom).1.1 ∧
    Eq.{u + 1} (α := (↑B : Type u) →ₐ[ℤ] (↑s.pt : Type u))
      (AlgHom.comp (B := (↑A : Type u) ⊗[ℤ] (↑B : Type u))
        (AlgHom.restrictScalars ℤ (S := ℤ) (RingHom.toIntAlgHom (Hom.hom { hom' := m })) :
          (↑A : Type u) ⊗[ℤ] (↑B : Type u) →ₐ[ℤ] (↑s.pt : Type u))
        (Algebra.TensorProduct.includeRight : (↑B : Type u) →ₐ[ℤ] (↑A : Type u) ⊗[ℤ] (↑B : Type u)))
      (((Equiv.symm Algebra.TensorProduct.liftEquiv :
                ((↑A : Type u) ⊗[ℤ] (↑B : Type u) →ₐ[ℤ] (↑s.pt : Type u)) ≃
                  { fg : ((↑A : Type u) →ₐ[ℤ] (↑s.pt : Type u)) × ((↑B : Type u) →ₐ[ℤ] (↑s.pt : Type u)) //
                    ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
                      Commute (S := (↑s.pt : Type u))
                        ((fg.1 : (a : (↑A : Type u)) → (↑s.pt : Type u)) x : (↑s.pt : Type u))
                        ((fg.2 : (a : (↑B : Type u)) → (↑s.pt : Type u)) y : (↑s.pt : Type u)) }) :
              (a : (↑A : Type u) ⊗[ℤ] (↑B : Type u) →ₐ[ℤ] (↑s.pt : Type u)) →
                { fg : ((↑A : Type u) →ₐ[ℤ] (↑s.pt : Type u)) × ((↑B : Type u) →ₐ[ℤ] (↑s.pt : Type u)) //
                  ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
                    Commute ((fg.1 : (a : (↑A : Type u)) → (↑s.pt : Type u)) x)
                      ((fg.2 : (a : (↑B : Type u)) → (↑s.pt : Type u)) y) })
            (Hom.hom
                (ofHom
                  (AlgHom.toRingHom
                    (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯ :
                      (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u) ⊗[ℤ]
                          (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u) →ₐ[ℤ]
                        (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) s.pt)
                              { as := WalkingPair.left : Discrete WalkingPair }) :
                          Type u))))).toIntAlgHom).1.2
⊢ Eq.{u + 1} (α := ((↑A : Type u) →ₐ[ℤ] (↑s.pt : Type u)) × ((↑B : Type u) →ₐ[ℤ] (↑s.pt : Type u)))
    (↑(((Equiv.symm Algebra.TensorProduct.liftEquiv :
              ((↑A : Type u) ⊗[ℤ] (↑B : Type u) →ₐ[ℤ] (↑s.pt : Type u)) ≃
                { fg : ((↑A : Type u) →ₐ[ℤ] (↑s.pt : Type u)) × ((↑B : Type u) →ₐ[ℤ] (↑s.pt : Type u)) //
                  ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
                    Commute (S := (↑s.pt : Type u))
                      ((fg.1 : (a : (↑A : Type u)) → (↑s.pt : Type u)) x : (↑s.pt : Type u))
                      ((fg.2 : (a : (↑B : Type u)) → (↑s.pt : Type u)) y : (↑s.pt : Type u)) }) :
            (a : (↑A : Type u) ⊗[ℤ] (↑B : Type u) →ₐ[ℤ] (↑s.pt : Type u)) →
              { fg : ((↑A : Type u) →ₐ[ℤ] (↑s.pt : Type u)) × ((↑B : Type u) →ₐ[ℤ] (↑s.pt : Type u)) //
                ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
                  Commute ((fg.1 : (a : (↑A : Type u)) → (↑s.pt : Type u)) x)
                    ((fg.2 : (a : (↑B : Type u)) → (↑s.pt : Type u)) y) })
          (RingHom.toIntAlgHom (Hom.hom { hom' := m }))) :
      ((↑A : Type u) →ₐ[ℤ] (↑s.pt : Type u)) × ((↑B : Type u) →ₐ[ℤ] (↑s.pt : Type u)))
    (↑(((Equiv.symm Algebra.TensorProduct.liftEquiv :
              ((↑A : Type u) ⊗[ℤ] (↑B : Type u) →ₐ[ℤ] (↑s.pt : Type u)) ≃
                { fg : ((↑A : Type u) →ₐ[ℤ] (↑s.pt : Type u)) × ((↑B : Type u) →ₐ[ℤ] (↑s.pt : Type u)) //
                  ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
                    Commute (S := (↑s.pt : Type u))
                      ((fg.1 : (a : (↑A : Type u)) → (↑s.pt : Type u)) x : (↑s.pt : Type u))
                      ((fg.2 : (a : (↑B : Type u)) → (↑s.pt : Type u)) y : (↑s.pt : Type u)) }) :
            (a : (↑A : Type u) ⊗[ℤ] (↑B : Type u) →ₐ[ℤ] (↑s.pt : Type u)) →
              { fg : ((↑A : Type u) →ₐ[ℤ] (↑s.pt : Type u)) × ((↑B : Type u) →ₐ[ℤ] (↑s.pt : Type u)) //
                ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
                  Commute ((fg.1 : (a : (↑A : Type u)) → (↑s.pt : Type u)) x)
                    ((fg.2 : (a : (↑B : Type u)) → (↑s.pt : Type u)) y) })
          (Hom.hom
              (ofHom
                (AlgHom.toRingHom
                  (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯ :
                    (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u) ⊗[ℤ]
                        (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u) →ₐ[ℤ]
                      (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) s.pt)
                            { as := WalkingPair.left : Discrete WalkingPair }) :
                        Type u))))).toIntAlgHom) :
      ((↑A : Type u) →ₐ[ℤ] (↑s.pt : Type u)) × ((↑B : Type u) →ₐ[ℤ] (↑s.pt : Type u)))

Tactic:
rw [Algebra.TensorProduct.liftEquiv_symm_apply_coe, Prod.mk.injEq]

Premises used: Prod.mk.injEq, Algebra.TensorProduct.liftEquiv_symm_apply_coe