Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover (Scheme.precoverage P) S
inst✝² : P.RespectsLeft IsOpenImmersion
inst✝¹ : CompactSpace ↥S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
idx : ↥S → Fin n
x : (x : ↥S) → ↥(𝒰.X (f (idx x)))
hmem : ∀ (x_1 : ↥S), x x_1 ∈ V (idx x_1)
hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1
⊢ { I₀ := ULift.{w, 0} (Fin n), X := fun i ↦ Γ(𝒰.X (f i.down), V i.down), f := fun i ↦ ⋯.fromSpec ≫ 𝒰.f (f i.down),
        idx := fun s ↦ { down := idx s }, covers := ⋯, map_prop := ⋯ }.cover ⟶
    𝒰

pp: case refine_3
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover (Scheme.precoverage P) S
inst✝² : P.RespectsLeft IsOpenImmersion
inst✝¹ : CompactSpace ↥S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
idx : ↥S → Fin n
x : (x : ↥S) → ↥(𝒰.X (f (idx x)))
hmem : ∀ (x_1 : ↥S), x x_1 ∈ V (idx x_1)
hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1
⊢ Finite
    { I₀ := ULift.{w, 0} (Fin n), X := fun i ↦ Γ(𝒰.X (f i.down), V i.down), f := fun i ↦ ⋯.fromSpec ≫ 𝒰.f (f i.down),
        idx := fun s ↦ { down := idx s }, covers := ⋯, map_prop := ⋯ }.I₀

pp: case refine_4
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover (Scheme.precoverage P) S
inst✝² : P.RespectsLeft IsOpenImmersion
inst✝¹ : CompactSpace ↥S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
idx : ↥S → Fin n
x : (x : ↥S) → ↥(𝒰.X (f (idx x)))
hmem : ∀ (x_1 : ↥S), x x_1 ∈ V (idx x_1)
hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1
⊢ ∀
    (j :
      { I₀ := ULift.{w, 0} (Fin n), X := fun i ↦ Γ(𝒰.X (f i.down), V i.down), f := fun i ↦ ⋯.fromSpec ≫ 𝒰.f (f i.down),
            idx := fun s ↦ { down := idx s }, covers := ⋯, map_prop := ⋯ }.cover.I₀),
    IsOpenImmersion (PreZeroHypercover.Hom.h₀ ?refine_2 j)

Tactic:
· exact
      { s₀ i := f i.down
        h₀ i := (hV i.down).fromSpec }

Goal state after:
case refine_3
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover (Scheme.precoverage P) S
inst✝² : P.RespectsLeft IsOpenImmersion
inst✝¹ : CompactSpace ↥S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
idx : ↥S → Fin n
x : (x : ↥S) → ↥(𝒰.X (f (idx x)))
hmem : ∀ (x_1 : ↥S), x x_1 ∈ V (idx x_1)
hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1
⊢ Finite
    { I₀ := ULift.{w, 0} (Fin n), X := fun i ↦ Γ(𝒰.X (f i.down), V i.down), f := fun i ↦ ⋯.fromSpec ≫ 𝒰.f (f i.down),
        idx := fun s ↦ { down := idx s }, covers := ⋯, map_prop := ⋯ }.I₀

case refine_4
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover (Scheme.precoverage P) S
inst✝² : P.RespectsLeft IsOpenImmersion
inst✝¹ : CompactSpace ↥S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
idx : ↥S → Fin n
x : (x : ↥S) → ↥(𝒰.X (f (idx x)))
hmem : ∀ (x_1 : ↥S), x x_1 ∈ V (idx x_1)
hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1
⊢ ∀
    (j :
      { I₀ := ULift.{w, 0} (Fin n), X := fun i ↦ Γ(𝒰.X (f i.down), V i.down), f := fun i ↦ ⋯.fromSpec ≫ 𝒰.f (f i.down),
            idx := fun s ↦ { down := idx s }, covers := ⋯, map_prop := ⋯ }.cover.I₀),
    IsOpenImmersion ({ s₀ := fun i ↦ f i.down, h₀ := fun i ↦ ⋯.fromSpec, w₀ := ⋯ }.h₀ j)