-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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)
⊢ 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))
have 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) sorry sorry)
      (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))
Tactic: refine @quasiSeparatedSpace_of_quasiSeparated _ _ ?_
    (HasAffineProperty.of_isPullback (.of_hasPullback _ (Z.affineCover.f i)) ‹_›) ?_