-- 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
s : (↑(CommRingCat.of S) : Type u)
hs :
  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))))
    s
obtain :
  ∀ (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)))))
⊢ ∃ (a : R),
    (codRestrictEqLocusPushoutCocone R S :
          (a : R) →
            (↑(CommRingCat.equalizerFork (CommRingCat.pushoutCocone R S S).inl
                    (CommRingCat.pushoutCocone R S S).inr).pt :
              Type u))
        a =
      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)
        s hs

Tactic:
obtain ⟨t, rfl⟩ := Set.mem_range.mp <|
    Algebra.IsEffective.eqLocus_includeLeft_includeRight hf ▸ SetLike.mem_coe.mpr hs

Premises used: Set.mem_range, Iff.mp, rfl