-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Property (goal)
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f g : A ⟶ B
c : Fork f g := Under.equalizerFork f g
hc : IsLimit c := Under.equalizerForkIsLimit f g
ι : R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g)) ⟶ A :=
  AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g)))
h' : (R.tensorProd S).obj (R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ⟶ (R.tensorProd S).obj A :=
  (R.tensorProd S).map ι
w' : h' ≫ (R.tensorProd S).map f = h' ≫ (R.tensorProd S).map g
e : IsLimit ((R.tensorProd S).mapCone c) ≃ IsLimit (Fork.ofι h' w') := isLimitMapConeForkEquiv (R.tensorProd S) ⋯
⊢ PreservesLimit (parallelPair f g) (R.tensorProd S) ↔
    Function.Bijective (α := TensorProduct (↑R : Type u) (↑S : Type u) ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g)))
      (β :=
      ↥(AlgHom.equalizer (F :=
          TensorProduct (↑R : Type u) (↑S : Type u) (↑A.right : Type u) →ₐ[(↑R : Type u)]
            TensorProduct (↑R : Type u) (↑S : Type u) (↑B.right : Type u))
          (Algebra.TensorProduct.map (AlgHom.id (↑R : Type u) (↑S : Type u)) (toAlgHom f) :
            TensorProduct (↑R : Type u) (↑S : Type u) (↑A.right : Type u) →ₐ[(↑R : Type u)]
              TensorProduct (↑R : Type u) (↑S : Type u) (↑B.right : Type u))
          (Algebra.TensorProduct.map (AlgHom.id (↑R : Type u) (↑S : Type u)) (toAlgHom g) :
            TensorProduct (↑R : Type u) (↑S : Type u) (↑A.right : Type u) →ₐ[(↑R : Type u)]
              TensorProduct (↑R : Type u) (↑S : Type u) (↑B.right : Type u))))
      (⇑(AlgHom.tensorEqualizer (↑R : Type u) (↑S : Type u) (toAlgHom f) (toAlgHom g)) :
        (a : TensorProduct (↑R : Type u) (↑S : Type u) ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g))) →
          ↥(AlgHom.equalizer (Algebra.TensorProduct.map (AlgHom.id (↑R : Type u) (↑S : Type u)) (toAlgHom f))
              (Algebra.TensorProduct.map (AlgHom.id (↑R : Type u) (↑S : Type u)) (toAlgHom g))))
have rw : IsIso (IsLimit.lift (Under.equalizerForkIsLimit ((R.tensorProd S).map f) ((R.tensorProd S).map g)) (Fork.ofι h' w')) ↔
  Function.Bijective (α := TensorProduct (↑R : Type u) (↑S : Type u) ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g)))
    (β :=
    ↥(AlgHom.equalizer (F :=
        TensorProduct (↑R : Type u) (↑S : Type u) (↑A.right : Type u) →ₐ[(↑R : Type u)]
          TensorProduct (↑R : Type u) (↑S : Type u) (↑B.right : Type u))
        (Algebra.TensorProduct.map (AlgHom.id (↑R : Type u) (↑S : Type u)) (toAlgHom f) :
          TensorProduct (↑R : Type u) (↑S : Type u) (↑A.right : Type u) →ₐ[(↑R : Type u)]
            TensorProduct (↑R : Type u) (↑S : Type u) (↑B.right : Type u))
        (Algebra.TensorProduct.map (AlgHom.id (↑R : Type u) (↑S : Type u)) (toAlgHom g) :
          TensorProduct (↑R : Type u) (↑S : Type u) (↑A.right : Type u) →ₐ[(↑R : Type u)]
            TensorProduct (↑R : Type u) (↑S : Type u) (↑B.right : Type u))))
    (⇑(AlgHom.tensorEqualizer (↑R : Type u) (↑S : Type u) (toAlgHom f) (toAlgHom g)) :
      (a : TensorProduct (↑R : Type u) (↑S : Type u) ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g))) →
        ↥(AlgHom.equalizer (Algebra.TensorProduct.map (AlgHom.id (↑R : Type u) (↑S : Type u)) (toAlgHom f))
            (Algebra.TensorProduct.map (AlgHom.id (↑R : Type u) (↑S : Type u)) (toAlgHom g))))
Tactic: rw [preservesLimit_iff_isLimit_mapCone hc, e.nonempty_congr,
    (Under.equalizerForkIsLimit _ _).nonempty_isLimit_iff_isIso_lift]