-- Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
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))
refine :
  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))
⊢ Membership.mem (γ := Submodule (↑Γ(Y, V) : Type u_1) (↑Γ(Y, V) : Type u_1)) ⊥ x

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) ?_

Premises used: le_rfl, CommRingCat.inr_injective_of_flat, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.Scheme.Hom.appLE, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, AlgebraicGeometry.Scheme.Hom.flat_appLE, CategoryTheory.Functor.obj