-- Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
hf : IsEffective R S
t : R
hs :
  Membership.mem (α := (↑(CommRingCat.of S) : Type u)) (γ := Subring (↑(CommRingCat.of S) : Type u))
    (RingHom.eqLocus (S :=
      (↑(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)) :
        Type u))
      (CommRingCat.Hom.hom (CategoryTheory.Limits.PushoutCocone.inl (CommRingCat.pushoutCocone R S S)))
      (CommRingCat.Hom.hom (CategoryTheory.Limits.PushoutCocone.inr (CommRingCat.pushoutCocone R S S))))
    ((algebraMap R S : (a : R) → S) t : S)
⊢ ∃ (a : R),
    Eq (α :=
      (↑(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))
          a :
        (↑(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))
      (Subtype.mk (p := fun (x : (↑(CommRingCat.of S) : Type u)) ↦
          Membership.mem (γ := Subring (↑(CommRingCat.of S) : Type u))
            (RingHom.eqLocus (S :=
              (↑(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)) :
                Type u))
              (CommRingCat.Hom.hom (CategoryTheory.Limits.PushoutCocone.inl (CommRingCat.pushoutCocone R S S)))
              (CommRingCat.Hom.hom (CategoryTheory.Limits.PushoutCocone.inr (CommRingCat.pushoutCocone R S S))))
            x)
          ((algebraMap R S : (a : R) → S) t) hs :
        ↥(RingHom.eqLocus (S :=
            (↑(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)) :
              Type u))
            (CommRingCat.Hom.hom (CategoryTheory.Limits.PushoutCocone.inl (CommRingCat.pushoutCocone R S S)))
            (CommRingCat.Hom.hom (CategoryTheory.Limits.PushoutCocone.inr (CommRingCat.pushoutCocone R S S)))))

Tactic:
⟨t, rfl⟩

Premises used: Exists.intro, rfl