-- 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
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
⊢ ∃ (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
have 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)))))
Tactic: obtain ⟨t, rfl⟩ := Set.mem_range.mp <|
    Algebra.IsEffective.eqLocus_includeLeft_includeRight hf ▸ SetLike.mem_coe.mpr hs
Cleared hypotheses: s, hs