-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : QuasiSeparated (f ≫ g)
𝒰 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover Y :=
  (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind
    fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
    ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover
this : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
i : Z.affineCover.I₀
j :
  PreZeroHypercover.I₀ (S := pullback g (Z.affineCover.f i))
    (Precoverage.ZeroHypercover.toPreZeroHypercover (pullback g (Z.affineCover.f i)).affineCover)
refine_1 :
  (Precoverage.ZeroHypercover.pullback₁ f
          ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind
            fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
            ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover)).X
      (Sigma.mk (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
        PreZeroHypercover.I₀ (C := Scheme) (S := (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)
          ((fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
              (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                  ((fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                      (((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover :
                        ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).OpenCover))
                    i) :
                PreZeroHypercover ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)))
            i))
        i j) ⟶
    pullback (f ≫ g) (Z.affineCover.f i)
refine_2 :
  QuasiSeparated (X :=
    (Precoverage.ZeroHypercover.pullback₁ f
          ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind
            fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
            ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover)).X
      (Sigma.mk (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
        PreZeroHypercover.I₀ (C := Scheme) (S := (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)
          ((fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
              (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                  ((fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                      (((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover :
                        ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).OpenCover))
                    i) :
                PreZeroHypercover ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)))
            i))
        i j))
    (Y := pullback (f ≫ g) (Z.affineCover.f i))
    (CategoryStruct.comp (Y :=
        pullback (Y :=
          (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X
            (Sigma.fst (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
              PreZeroHypercover.I₀ (C := Scheme) (S := (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)
                ((fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                    (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                        ((fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                            (((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover :
                              ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).OpenCover))
                          i) :
                      PreZeroHypercover ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)))
                  i))
              (Sigma.mk (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                PreZeroHypercover.I₀ (C := Scheme) (S := (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)
                  ((fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                          ((fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                              (((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover :
                                ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).OpenCover))
                            i) :
                        PreZeroHypercover ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)))
                    i))
                i j)))
          f
          ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).f
            (Sigma.fst (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
              PreZeroHypercover.I₀ (C := Scheme) (S := (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)
                ((fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                    (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                        ((fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                            (((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover :
                              ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).OpenCover))
                          i) :
                      PreZeroHypercover ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)))
                  i))
              (Sigma.mk (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                PreZeroHypercover.I₀ (C := Scheme) (S := (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)
                  ((fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                          ((fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                              (((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover :
                                ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).OpenCover))
                            i) :
                        PreZeroHypercover ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)))
                    i))
                i j))))
        (pullback.map f
          (((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind
                fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover).f
            (Sigma.mk (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
              PreZeroHypercover.I₀ (C := Scheme) (S := (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)
                ((fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                    (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                        ((fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                            (((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover :
                              ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).OpenCover))
                          i) :
                      PreZeroHypercover ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)))
                  i))
              i j))
          f
          ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).f
            (Sigma.fst (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
              PreZeroHypercover.I₀ (C := Scheme) (S := (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)
                ((fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                    (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                        ((fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                            (((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover :
                              ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).OpenCover))
                          i) :
                      PreZeroHypercover ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)))
                  i))
              (Sigma.mk (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                PreZeroHypercover.I₀ (C := Scheme) (S := (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)
                  ((fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                          ((fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                              (((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover :
                                ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).OpenCover))
                            i) :
                        PreZeroHypercover ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)))
                    i))
                i j)))
          (𝟙 X)
          (PreZeroHypercover.f
            ((fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                    ((fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                        (((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover :
                          ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).OpenCover))
                      i) :
                  PreZeroHypercover ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)))
              (Sigma.fst (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                PreZeroHypercover.I₀ (C := Scheme) (S := (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)
                  ((fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                          ((fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                              (((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover :
                                ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).OpenCover))
                            i) :
                        PreZeroHypercover ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)))
                    i))
                (Sigma.mk (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                  PreZeroHypercover.I₀ (C := Scheme) (S := (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)
                    ((fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                            ((fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                                (((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover :
                                  ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).OpenCover))
                              i) :
                          PreZeroHypercover ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)))
                      i))
                  i j)))
            (Sigma.snd (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
              PreZeroHypercover.I₀ (C := Scheme) (S := (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)
                ((fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                    (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                        ((fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                            (((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover :
                              ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).OpenCover))
                          i) :
                      PreZeroHypercover ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)))
                  i))
              (Sigma.mk (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                PreZeroHypercover.I₀ (C := Scheme) (S := (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)
                  ((fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                          ((fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                              (((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover :
                                ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).OpenCover))
                            i) :
                        PreZeroHypercover ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)))
                    i))
                i j)))
          (𝟙 Y) ⋯ ⋯)
        (Iso.hom (pullbackRightPullbackFstIso g (Z.affineCover.f i) f)) :
      (Precoverage.ZeroHypercover.pullback₁ f
              ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind
                fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover)).X
          (Sigma.mk (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
            PreZeroHypercover.I₀ (C := Scheme) (S := (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)
              ((fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                      ((fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                          (((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover :
                            ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).OpenCover))
                        i) :
                    PreZeroHypercover ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)))
                i))
            i j) ⟶
        pullback (f ≫ g) (Z.affineCover.f i))
⊢ QuasiSeparatedSpace.{u}
    ↥((Precoverage.ZeroHypercover.pullback₁ f
            ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind
              fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
              ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover)).X
        (Sigma.mk (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
          PreZeroHypercover.I₀ (C := Scheme) (S := (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)
            ((fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                    ((fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                        (((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover :
                          ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).OpenCover))
                      i) :
                  PreZeroHypercover ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)))
              i))
          i j))

Tactic:
refine @quasiSeparatedSpace_of_quasiSeparated _ _ ?_
    (HasAffineProperty.of_isPullback (.of_hasPullback _ (Z.affineCover.f i)) ‹_›) ?_

Premises used: AlgebraicGeometry.quasiSeparatedSpace_of_quasiSeparated