-- Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
lemma of_iSup_eq_top {ι} (U : ι → Y.Opens) (hU : iSup U = ⊤)
    (H : ∀ i, P (f ∣_ U i)) : P f

Proof state:
P : MorphismProperty Scheme
hP : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (f ∣_ U i)
⊢ P f

Tactic:
refine (IsLocalAtTarget.iff_of_openCover' f
  (Y.openCoverOfISupEqTop (s := Set.range U) Subtype.val (by ext; simp [← hU]))).mpr fun i ↦ ?_

Result:
P : MorphismProperty Scheme
hP : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (f ∣_ U i)
i : (Y.openCoverOfISupEqTop Subtype.val ⋯).1
⊢ P (Scheme.Cover.pullbackHom (Y.openCoverOfISupEqTop Subtype.val ⋯) f i)

Proof state:
P : MorphismProperty Scheme
hP : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (f ∣_ U i)
i : (Y.openCoverOfISupEqTop Subtype.val ⋯).1
⊢ P (Scheme.Cover.pullbackHom (Y.openCoverOfISupEqTop Subtype.val ⋯) f i)

Tactic:
obtain ⟨_, i, rfl⟩ := i

Result:
case mk.intro
P : MorphismProperty Scheme
hP : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (f ∣_ U i)
i : ι
⊢ P (Scheme.Cover.pullbackHom (Y.openCoverOfISupEqTop Subtype.val ⋯) f ⟨U i, ⋯⟩)

Proof state:
case mk.intro
P : MorphismProperty Scheme
hP : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (f ∣_ U i)
i : ι
⊢ P (Scheme.Cover.pullbackHom (Y.openCoverOfISupEqTop Subtype.val ⋯) f ⟨U i, ⋯⟩)

Tactic:
refine (P.arrow_mk_iso_iff (morphismRestrictOpensRange f _)).mp ?_

Result:
case mk.intro
P : MorphismProperty Scheme
hP : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (f ∣_ U i)
i : ι
⊢ P (f ∣_ Scheme.Hom.opensRange ((Y.openCoverOfISupEqTop Subtype.val ⋯).map ⟨U i, ⋯⟩))

Proof state:
case mk.intro
P : MorphismProperty Scheme
hP : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (f ∣_ U i)
i : ι
⊢ P (f ∣_ Scheme.Hom.opensRange (U i).ι)

Tactic:
rw [Scheme.Opens.opensRange_ι]

Result:
case mk.intro
P : MorphismProperty Scheme
hP : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (f ∣_ U i)
i : ι
⊢ P (f ∣_ U i)

Proof state:
case mk.intro
P : MorphismProperty Scheme
hP : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (f ∣_ U i)
i : ι
⊢ P (f ∣_ Scheme.Hom.opensRange ((Y.openCoverOfISupEqTop Subtype.val ⋯).map ⟨U i, ⋯⟩))

Tactic:
show P (f ∣_ (U i).ι.opensRange)

Result:
case mk.intro
P : MorphismProperty Scheme
hP : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (f ∣_ U i)
i : ι
⊢ P (f ∣_ Scheme.Hom.opensRange (U i).ι)

Proof state:
case mk.intro
P : MorphismProperty Scheme
hP : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (f ∣_ U i)
i : ι
⊢ P (f ∣_ U i)

Tactic:
exact H i

Result:
no goals

Proof state:
P : MorphismProperty Scheme
hP : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (f ∣_ U i)
⊢ ⨆ i, ↑i = ⊤

Tactic:
ext

Result:
case h.h
P : MorphismProperty Scheme
hP : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (f ∣_ U i)
x✝ : ↑↑Y.toPresheafedSpace
⊢ x✝ ∈ ↑(⨆ i, ↑i) ↔ x✝ ∈ ↑⊤

Proof state:
case h.h
P : MorphismProperty Scheme
hP : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (f ∣_ U i)
x✝ : ↑↑Y.toPresheafedSpace
⊢ x✝ ∈ ↑(⨆ i, ↑i) ↔ x✝ ∈ ↑⊤

Tactic:
simp [← hU]

Result:
no goals