-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.QuasiCompact (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover.{w, u} (Scheme.precoverage P) S
inst : P.RespectsLeft IsOpenImmersion
inst_1 : CompactSpace.{u} ↥S
inst_2 : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
idx : (x : ↥S) → Fin n
x : (x : ↥S) → ↥(𝒰.X (f (idx x)))
hmem : ∀ (x_1 : ↥S), Membership.mem (γ := (𝒰.X (f (idx x_1))).Opens) (V (idx x_1)) (x x_1)
hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1
refine_1 : Scheme.AffineCover.{w, u} P S
refine_2 :
  Scheme.AffineCover.cover (P := P)
      (Scheme.AffineCover.mk (P := P) (ULift.{w, 0} (Fin n))
        (fun (i : ULift.{w, 0} (Fin n)) ↦ Γ(𝒰.X (f i.down), V i.down))
        (fun (i : ULift.{w, 0} (Fin n)) ↦ IsAffineOpen.fromSpec ⋯ ≫ 𝒰.f (f i.down)) (fun (s : ↥S) ↦ { down := idx s }) ⋯
        ⋯) ⟶
    𝒰
refine_3 :
  Finite.{w + 1}
    (Scheme.AffineCover.I₀ (P := P) (S := S)
      (Scheme.AffineCover.mk (P := P) (ULift.{w, 0} (Fin n))
        (fun (i : ULift.{w, 0} (Fin n)) ↦ Γ(𝒰.X (f i.down), V i.down))
        (fun (i : ULift.{w, 0} (Fin n)) ↦ IsAffineOpen.fromSpec ⋯ ≫ 𝒰.f (f i.down)) (fun (s : ↥S) ↦ { down := idx s }) ⋯
        ⋯))
⊢ ∃ (𝒱 : Scheme.AffineCover.{w, u} P S) (f : 𝒱.cover (P := P) ⟶ 𝒰),
    Finite.{w + 1} (𝒱.I₀ (P := P)) ∧ ∀ (j : 𝒱.cover (P := P).I₀), IsOpenImmersion (f.h₀ j)
have refine_4 : ∀
  (j :
    PreZeroHypercover.I₀.{w, u, u + 1} (S := S)
      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage P)
        (Scheme.AffineCover.cover (P := P)
          (Scheme.AffineCover.mk (P := P) (ULift.{w, 0} (Fin n))
            (fun (i : ULift.{w, 0} (Fin n)) ↦ Γ(𝒰.X (f i.down), V i.down))
            (fun (i : ULift.{w, 0} (Fin n)) ↦ IsAffineOpen.fromSpec sorry ≫ 𝒰.f (f i.down))
            (fun (s : ↥S) ↦ { down := idx s }) sorry sorry)))),
  IsOpenImmersion (Y :=
    𝒰.X
      (PreZeroHypercover.Hom.s₀
        {
          s₀ :=
            fun
              (i :
                PreZeroHypercover.I₀.{w, u, u + 1} (S := S)
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage P)
                    (Scheme.AffineCover.cover (P := P)
                      (Scheme.AffineCover.mk (P := P) (ULift.{w, 0} (Fin n))
                        (fun (i : ULift.{w, 0} (Fin n)) ↦ Γ(𝒰.X (f i.down), V i.down))
                        (fun (i : ULift.{w, 0} (Fin n)) ↦ IsAffineOpen.fromSpec sorry ≫ 𝒰.f (f i.down))
                        (fun (s : ↥S) ↦ { down := idx s }) sorry sorry)))) ↦
            f i.down,
          h₀ :=
            fun
              (i :
                PreZeroHypercover.I₀.{w, u, u + 1} (S := S)
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage P)
                    (Scheme.AffineCover.cover (P := P)
                      (Scheme.AffineCover.mk (P := P) (ULift.{w, 0} (Fin n))
                        (fun (i : ULift.{w, 0} (Fin n)) ↦ Γ(𝒰.X (f i.down), V i.down))
                        (fun (i : ULift.{w, 0} (Fin n)) ↦ IsAffineOpen.fromSpec sorry ≫ 𝒰.f (f i.down))
                        (fun (s : ↥S) ↦ { down := idx s }) sorry sorry)))) ↦
            IsAffineOpen.fromSpec sorry,
          w₀ := sorry }
        j))
    (PreZeroHypercover.Hom.h₀
      {
        s₀ :=
          fun
            (i :
              PreZeroHypercover.I₀.{w, u, u + 1} (S := S)
                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage P)
                  (Scheme.AffineCover.cover (P := P)
                    (Scheme.AffineCover.mk (P := P) (ULift.{w, 0} (Fin n))
                      (fun (i : ULift.{w, 0} (Fin n)) ↦ Γ(𝒰.X (f i.down), V i.down))
                      (fun (i : ULift.{w, 0} (Fin n)) ↦ IsAffineOpen.fromSpec sorry ≫ 𝒰.f (f i.down))
                      (fun (s : ↥S) ↦ { down := idx s }) sorry sorry)))) ↦
          f i.down,
        h₀ :=
          fun
            (i :
              PreZeroHypercover.I₀.{w, u, u + 1} (S := S)
                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage P)
                  (Scheme.AffineCover.cover (P := P)
                    (Scheme.AffineCover.mk (P := P) (ULift.{w, 0} (Fin n))
                      (fun (i : ULift.{w, 0} (Fin n)) ↦ Γ(𝒰.X (f i.down), V i.down))
                      (fun (i : ULift.{w, 0} (Fin n)) ↦ IsAffineOpen.fromSpec sorry ≫ 𝒰.f (f i.down))
                      (fun (s : ↥S) ↦ { down := idx s }) sorry sorry)))) ↦
          IsAffineOpen.fromSpec sorry,
        w₀ := sorry }
      j)
Tactic: refine ⟨?_, ?_, ?_, ?_⟩