-- Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
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))
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))
⊢ 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))

Tactic:
constructor