-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
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_1 : IsSchemeTheoreticallyDominant g
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 (⋯.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 (⋯.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 (⋯.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 (⋯.genericPoint (S := (↑i : Set ↥Y)))))
      fun (x : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦
      pullback.fst f (Y.fromSpecStalk (⋯.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 (⋯.genericPoint (S := (↑i : Set ↥Y)))))
      fun (x : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦
      pullback.snd f (Y.fromSpecStalk (⋯.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
⊢ ∀
    (i :
      PreZeroHypercover.I₀ (S :=
        ∐ 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 (⋯.genericPoint (S := (↑i : Set ↥Y)))))
        (Precoverage.ZeroHypercover.toPreZeroHypercover
            (sigmaOpenCover 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 (⋯.genericPoint (S := (↑i : Set ↥Y))))) :
          PreZeroHypercover (C := Scheme)
            (∐ 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 (⋯.genericPoint (S := (↑i : Set ↥Y))))))),
    IsReduced.{u_1}
      (PreZeroHypercover.X
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (sigmaOpenCover 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 (⋯.genericPoint (S := (↑i : Set ↥Y))))))
        i)

Tactic:
exact fun i ↦ GeometricallyReduced.geometrically_isReduced _ _ _ (.of_hasPullback _ _)

Premises used: CategoryTheory.Limits.pullback.snd, AlgebraicGeometry.GeometricallyReduced.geometrically_isReduced, CategoryTheory.Limits.pullback.fst, CategoryTheory.IsPullback.of_hasPullback