-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight (goal)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.FaithfullyFlat R S
left :
  Function.Injective (α := R) (β :=
    (↑(CategoryTheory.Limits.Cone.pt (F :=
          CategoryTheory.Limits.parallelPair (X := CommRingCat.of S) (Y :=
            CategoryTheory.Limits.Cocone.pt (F :=
              CategoryTheory.Limits.span (X := CommRingCat.of R) (Y := CommRingCat.of S) (Z := CommRingCat.of S)
                (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)))
              (CommRingCat.pushoutCocone R S S))
            (CategoryTheory.Limits.PushoutCocone.inl (CommRingCat.pushoutCocone R S S))
            (CategoryTheory.Limits.PushoutCocone.inr (CommRingCat.pushoutCocone R S S)))
          (CommRingCat.equalizerFork (CategoryTheory.Limits.PushoutCocone.inl (CommRingCat.pushoutCocone R S S))
            (CategoryTheory.Limits.PushoutCocone.inr (CommRingCat.pushoutCocone R S S)))) :
      Type u))
    (⇑(codRestrictEqLocusPushoutCocone R S) :
      (a : R) →
        (↑(CommRingCat.equalizerFork (CommRingCat.pushoutCocone R S S).inl (CommRingCat.pushoutCocone R S S).inr).pt :
          Type u))
⊢ Function.Bijective (α := R) (β :=
    (↑(CategoryTheory.Limits.Cone.pt (F :=
          CategoryTheory.Limits.parallelPair (X := CommRingCat.of S) (Y :=
            CategoryTheory.Limits.Cocone.pt (F :=
              CategoryTheory.Limits.span (X := CommRingCat.of R) (Y := CommRingCat.of S) (Z := CommRingCat.of S)
                (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)))
              (CommRingCat.pushoutCocone R S S))
            (CategoryTheory.Limits.PushoutCocone.inl (CommRingCat.pushoutCocone R S S))
            (CategoryTheory.Limits.PushoutCocone.inr (CommRingCat.pushoutCocone R S S)))
          (CommRingCat.equalizerFork (CategoryTheory.Limits.PushoutCocone.inl (CommRingCat.pushoutCocone R S S))
            (CategoryTheory.Limits.PushoutCocone.inr (CommRingCat.pushoutCocone R S S)))) :
      Type u))
    (⇑(codRestrictEqLocusPushoutCocone R S) :
      (a : R) →
        (↑(CommRingCat.equalizerFork (CommRingCat.pushoutCocone R S S).inl (CommRingCat.pushoutCocone R S S).inr).pt :
          Type u))
have right : Function.Surjective (α := R) (β :=
  (↑(CategoryTheory.Limits.Cone.pt (F :=
        CategoryTheory.Limits.parallelPair (X := CommRingCat.of S) (Y :=
          CategoryTheory.Limits.Cocone.pt (F :=
            CategoryTheory.Limits.span (X := CommRingCat.of R) (Y := CommRingCat.of S) (Z := CommRingCat.of S)
              (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)))
            (CommRingCat.pushoutCocone R S S))
          (CategoryTheory.Limits.PushoutCocone.inl (CommRingCat.pushoutCocone R S S))
          (CategoryTheory.Limits.PushoutCocone.inr (CommRingCat.pushoutCocone R S S)))
        (CommRingCat.equalizerFork (CategoryTheory.Limits.PushoutCocone.inl (CommRingCat.pushoutCocone R S S))
          (CategoryTheory.Limits.PushoutCocone.inr (CommRingCat.pushoutCocone R S S)))) :
    Type u))
  (⇑(codRestrictEqLocusPushoutCocone R S) :
    (a : R) →
      (↑(CommRingCat.equalizerFork (CommRingCat.pushoutCocone R S S).inl (CommRingCat.pushoutCocone R S S).inr).pt :
        Type u))
Tactic: constructor