-- 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
⊢ 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 ⋯)
                  (Subtype.mk (p := fun (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, Subtype.mk (p := fun (x : TopologicalSpace.Opens ↥S) ↦ x ∈ S.affineOpens) U hU) ⋯)) :
              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 ⋯)
        (Subtype.mk (p := fun (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, Subtype.mk (p := fun (x : TopologicalSpace.Opens ↥S) ↦ x ∈ S.affineOpens) U hU) ⋯)))
    (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 ⋯)
        (Subtype.mk (p := fun (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, Subtype.mk (p := fun (x : TopologicalSpace.Opens ↥S) ↦ x ∈ S.affineOpens) U hU) ⋯)))
have simp : LE.le (α := Ideal (↑Γ(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)))
  ⊥
Tactic: simp only [Scheme.Hom.ker_apply, Scheme.IdealSheafData.ideal_bot, Pi.bot_apply, ← le_bot_iff]