-- 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))
⊢ Membership.mem (γ := Submodule (↑Γ(Y, V) : Type u_1) (↑Γ(Y, V) : Type u_1)) ⊥ x
have refine : Eq (α := (↑(pushout (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) sorry) (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) 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))
  ((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))
Tactic: refine CommRingCat.inr_injective_of_flat (f.appLE U (f ⁻¹ᵁ U) le_rfl) (g.appLE U V hVU)
    (by simpa [Scheme.Hom.appLE] using f.app_injective U) (g.flat_appLE hU hV hVU) ?_