-- 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 :=
  ⋯
refine :
  ∀
    (i :
      { 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) }),
    Eq (α :=
      Ideal
        (↑Γ(Y,
              (↑((fun
                        (U :
                          { 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) }) ↦
                      Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens)
                        (↑U : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1)).1 ⋯)
                    i) :
                Y.Opens)) :
          Type u_1))
      ((Scheme.Hom.ker (X := pullback f g) (pullback.snd f g)).ideal
        ((fun
              (U :
                { 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) }) ↦
            Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens)
              (↑U : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1)).1 ⋯)
          i))
      (Scheme.IdealSheafData.ideal ⊥
        ((fun
              (U :
                { 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) }) ↦
            Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens)
              (↑U : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1)).1 ⋯)
          i))
⊢ Scheme.Hom.ker (X := pullback f g) (pullback.snd f g) = ⊥

Tactic:
refine Scheme.IdealSheafData.ext_of_iSup_eq_top (fun U ↦ ⟨_, by exact U.2.1⟩) h𝒰 ?_

Premises used: Subtype.mk, AlgebraicGeometry.Scheme.IdealSheafData.ext_of_iSup_eq_top