-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : GeometricallyReduced f
inst_2 : Flat f
inst_3 : IsReduced Y
inst_4 : 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
inst :
  ∀
    (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)
⊢ IsReduced.{u_1}
    (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)))))))

Tactic:
apply +allowSynthFailures @IsReduced.of_openCover (𝒰 := sigmaOpenCover _)

Premises used: AlgebraicGeometry.IsReduced.of_openCover, AlgebraicGeometry.sigmaOpenCover