-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant (goal)
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f_1 : X ⟶ S
g_1 : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
inst_2 : Flat g
h𝒰 : TopologicalSpace.IsOpenCover (X := ↥Y)
  fun
    (V :
      { x : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1) //
        x.1 ∈ Y.affineOpens ∧
          x.1 ≤
            (TopologicalSpace.Opens.comap (TopCat.Hom.hom g.base) :
                (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥Y)
              (↑x.2 : TopologicalSpace.Opens ↥S) }) ↦
  (↑V : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1)).1 :=
  ⋯
V : TopologicalSpace.Opens ↥Y
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hV : (V, Subtype.mk (p := fun (x : TopologicalSpace.Opens ↥S) ↦ x ∈ S.affineOpens) U hU).1 ∈ Y.affineOpens
hVU : V ≤ g ⁻¹ᵁ U
x : (↑Γ(Y, V) : Type u_1)
hx :
  Membership.mem (γ := Submodule (↑Γ(Y, V) : Type u_1) (↑Γ(Y, V) : Type u_1))
    (RingHom.ker (F := (↑Γ(Y, V) : Type u_1) →+* (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u_1))
      (CommRingCat.Hom.hom (Scheme.Hom.app (pullback.snd f g) V)))
    x
this :
  Function.Injective (α := (↑(pushout (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯) (Scheme.Hom.appLE g U V hVU)) : Type u_1))
    (β := (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (Y := Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V)) (pushoutSection ⋯ hVU ⋯ ⋯)) :
      (a : (↑(pushout (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯) (Scheme.Hom.appLE g U V hVU)) : Type u_1)) →
        (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u_1))
⊢ Eq (α := (↑(pushout (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯) (Scheme.Hom.appLE g U V hVU)) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := pushout (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯) (Scheme.Hom.appLE g U V hVU))
            (pushout.inr (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯) (Scheme.Hom.appLE g U V hVU)) :
          (a : (↑Γ(Y, V) : Type u_1)) →
            (↑(pushout (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯) (Scheme.Hom.appLE g U V hVU)) : Type u_1))
        x :
      (↑(pushout (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯) (Scheme.Hom.appLE g U V hVU)) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := pushout (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯) (Scheme.Hom.appLE g U V hVU))
            (pushout.inr (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯) (Scheme.Hom.appLE g U V hVU)) :
          (a : (↑Γ(Y, V) : Type u_1)) →
            (↑(pushout (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯) (Scheme.Hom.appLE g U V hVU)) : Type u_1))
        0 :
      (↑(pushout (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯) (Scheme.Hom.appLE g U V hVU)) : Type u_1))
have a : Eq (α := (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u_1))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (Y := Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V)) (pushoutSection sorry hVU sorry sorry) :
        (a : (↑(pushout (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) sorry) (Scheme.Hom.appLE g U V hVU)) : Type u_1)) →
          (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Y := pushout (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) sorry) (Scheme.Hom.appLE g U V hVU))
              (pushout.inr (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) sorry) (Scheme.Hom.appLE g U V hVU)) :
            (a : (↑Γ(Y, V) : Type u_1)) →
              (↑(pushout (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) sorry) (Scheme.Hom.appLE g U V hVU)) : Type u_1))
          x :
        (↑(pushout (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) sorry) (Scheme.Hom.appLE g U V hVU)) : Type u_1)) :
    (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u_1))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (Y := Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V)) (pushoutSection sorry hVU sorry sorry) :
        (a : (↑(pushout (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) sorry) (Scheme.Hom.appLE g U V hVU)) : Type u_1)) →
          (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Y := pushout (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) sorry) (Scheme.Hom.appLE g U V hVU))
              (pushout.inr (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) sorry) (Scheme.Hom.appLE g U V hVU)) :
            (a : (↑Γ(Y, V) : Type u_1)) →
              (↑(pushout (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) sorry) (Scheme.Hom.appLE g U V hVU)) : Type u_1))
          0 :
        (↑(pushout (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) sorry) (Scheme.Hom.appLE g U V hVU)) : Type u_1)) :
    (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u_1))
Tactic: apply this