-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Reduced (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : GeometricallyReduced f
inst_1 : Flat f
inst_2 : IsReduced Y
inst_3 : Finite.{u_1 + 1} (↑(irreducibleComponents ↥Y) : Type u_1)
pt : (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) → CommRingCat :=
  fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Y.presheaf.stalk (⋯.genericPoint (S := (↑Z : Set ↥Y)))
hpt : ∀ (Z : (↑(irreducibleComponents ↥Y) : Type u_1)), IsField.{u_1} (↑(pt Z) : Type u_1)
this_1 : (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) → Field (↑(pt Z) : Type u_1) :=
  fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ ⋯.toField
Z : Scheme := ∐ fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Spec (pt Z)
g : Z ⟶ Y :=
  Sigma.desc fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Y.fromSpecStalk (⋯.genericPoint (S := (↑Z : Set ↥Y)))
this_2 : Finite.{u_1 + 1} ↥Z
this : QuasiCompact g
H : IsSchemeTheoreticallyDominant g
⊢ IsReduced.{u_1} (pullback f g)
have H₁ : IsPullback (P :=
  Cocone.pt (J := Discrete (↑(irreducibleComponents ↥Y) : Type u_1)) (F :=
    Discrete.functor fun (i : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦
      pullback (Y := (fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Spec.{u_1} (pt Z)) i) f
        (Y.fromSpecStalk (sorry.genericPoint (S := (↑i : Set ↥Y)))))
    (Cofan.mk
      (∐ fun (i : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦
        pullback (Y := (fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Spec.{u_1} (pt Z)) i) f
          (Y.fromSpecStalk (sorry.genericPoint (S := (↑i : Set ↥Y)))))
      (Sigma.ι fun (i : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦
        pullback (Y := (fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Spec.{u_1} (pt Z)) i) f
          (Y.fromSpecStalk (sorry.genericPoint (S := (↑i : Set ↥Y)))))))
  (Cofan.IsColimit.desc
    (coproductIsCoproduct fun (i : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦
      pullback (Y := (fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Spec.{u_1} (pt Z)) i) f
        (Y.fromSpecStalk (sorry.genericPoint (S := (↑i : Set ↥Y)))))
    fun (x : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦
    pullback.fst f (Y.fromSpecStalk (sorry.genericPoint (S := (↑x : Set ↥Y)))))
  (Cofan.IsColimit.desc
    (coproductIsCoproduct fun (i : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦
      pullback (Y := (fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Spec.{u_1} (pt Z)) i) f
        (Y.fromSpecStalk (sorry.genericPoint (S := (↑i : Set ↥Y)))))
    fun (x : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦
    pullback.snd f (Y.fromSpecStalk (sorry.genericPoint (S := (↑x : Set ↥Y)))) ≫
      Cofan.inj (C := Scheme) (f := fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Spec (pt Z))
        (Cofan.mk (∐ fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Spec (pt Z))
          (Sigma.ι fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Spec (pt Z)))
        x)
  f g
Tactic: have H := IsUniversalColimit.isPullback_of_isColimit_left
    (X := fun Z ↦ Spec (pt Z))
    (FinitaryPreExtensive.isUniversal_finiteCoproducts (coproductIsCoproduct _))
    (fun Z ↦ Y.fromSpecStalk _) g f _ _ (fun _ ↦ .of_hasPullback _ _) (coproductIsCoproduct _)