-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
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
⊢ RingHom.toIntAlgHom (Hom.hom { hom' := m }) =
    (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
have hf : Eq (α :=
  { 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)) })
  (((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 })) :
    { 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)) })
  (((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 sorry :
                (↑(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 :
    { 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)) })
Tactic: apply Algebra.TensorProduct.liftEquiv.symm.injective