-- Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
theorem of_iSup_eq_top
    {ι} (U : ι → Y.affineOpens) (hU : ⨆ i, (U i : Y.Opens) = ⊤)
    (hU' : ∀ i, Q (f ∣_ U i)) :
    P f

Proof state:
case basicOpen
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U✝ : ι → ↑Y.affineOpens
hU : ⨆ i, ↑(U✝ i) = ⊤
hU' : ∀ (i : ι), Q (f ∣_ ↑(U✝ i))
this : Q.IsLocal := isLocal_affineProperty P
U : ↑Y.affineOpens
r : ↑Γ(Y, ↑U)
h : Q (f ∣_ ↑U)
⊢ Q (f ∣_ ↑(Y.affineBasicOpen r))

Tactic:
haveI : IsAffine _ := U.2

Result:
case basicOpen
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U✝ : ι → ↑Y.affineOpens
hU : ⨆ i, ↑(U✝ i) = ⊤
hU' : ∀ (i : ι), Q (f ∣_ ↑(U✝ i))
this✝ : Q.IsLocal := isLocal_affineProperty P
U : ↑Y.affineOpens
r : ↑Γ(Y, ↑U)
h : Q (f ∣_ ↑U)
this : IsAffine ↑↑U
⊢ Q (f ∣_ ↑(Y.affineBasicOpen r))

Proof state:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → ↑Y.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
hU' : ∀ (i : ι), Q (f ∣_ ↑(U i))
this : Q.IsLocal := isLocal_affineProperty P
⊢ targetAffineLocally Q f

Tactic:
intro V

Result:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → ↑Y.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
hU' : ∀ (i : ι), Q (f ∣_ ↑(U i))
this : Q.IsLocal := isLocal_affineProperty P
V : ↑Y.affineOpens
⊢ Q (f ∣_ ↑V)

Proof state:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → ↑Y.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
hU' : ∀ (i : ι), Q (f ∣_ ↑(U i))
this : Q.IsLocal := isLocal_affineProperty P
⊢ P f

Tactic:
rw [eq_targetAffineLocally P]

Result:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → ↑Y.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
hU' : ∀ (i : ι), Q (f ∣_ ↑(U i))
this : Q.IsLocal := isLocal_affineProperty P
⊢ targetAffineLocally Q f

Proof state:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → ↑Y.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
hU' : ∀ (i : ι), Q (f ∣_ ↑(U i))
⊢ P f

Tactic:
letI := isLocal_affineProperty P

Result:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → ↑Y.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
hU' : ∀ (i : ι), Q (f ∣_ ↑(U i))
this : Q.IsLocal := isLocal_affineProperty P
⊢ P f

Proof state:
case openCover
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U✝ : ι → ↑Y.affineOpens
hU : ⨆ i, ↑(U✝ i) = ⊤
hU' : ∀ (i : ι), Q (f ∣_ ↑(U✝ i))
this : Q.IsLocal := isLocal_affineProperty P
U : ↑Y.affineOpens
s : Finset ↑Γ(Y, ↑U)
hs : Ideal.span ↑s = ⊤
H : ∀ (f_1 : { x // x ∈ s }), Q (f ∣_ ↑(Y.affineBasicOpen ↑f_1))
⊢ ∀ (r : { x // x ∈ Finset.image (⇑(ConcreteCategory.hom (↑U).topIso.inv)) s }), Q (f ∣_ ↑U ∣_ (↑↑U).basicOpen ↑r)

Tactic:
intro ⟨r, hr⟩

Result:
case openCover
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U✝ : ι → ↑Y.affineOpens
hU : ⨆ i, ↑(U✝ i) = ⊤
hU' : ∀ (i : ι), Q (f ∣_ ↑(U✝ i))
this : Q.IsLocal := isLocal_affineProperty P
U : ↑Y.affineOpens
s : Finset ↑Γ(Y, ↑U)
hs : Ideal.span ↑s = ⊤
H : ∀ (f_1 : { x // x ∈ s }), Q (f ∣_ ↑(Y.affineBasicOpen ↑f_1))
r : ↑Γ(↑↑U, ⊤)
hr : r ∈ Finset.image (⇑(ConcreteCategory.hom (↑U).topIso.inv)) s
⊢ Q (f ∣_ ↑U ∣_ (↑↑U).basicOpen ↑⟨r, hr⟩)

Proof state:
case openCover.intro.intro
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U✝ : ι → ↑Y.affineOpens
hU : ⨆ i, ↑(U✝ i) = ⊤
hU' : ∀ (i : ι), Q (f ∣_ ↑(U✝ i))
this : Q.IsLocal := isLocal_affineProperty P
U : ↑Y.affineOpens
s : Finset ↑Γ(Y, ↑U)
hs : Ideal.span ↑s = ⊤
H : ∀ (f_1 : { x // x ∈ s }), Q (f ∣_ ↑(Y.affineBasicOpen ↑f_1))
r : ↑Γ(Y, ↑U)
hr' : r ∈ s
hr : (ConcreteCategory.hom (↑U).topIso.inv) r ∈ Finset.image (⇑(ConcreteCategory.hom (↑U).topIso.inv)) s
⊢ Q (f ∣_ ↑U ∣_ (↑↑U).basicOpen ↑⟨(ConcreteCategory.hom (↑U).topIso.inv) r, hr⟩)

Tactic:
exact (Q.arrow_mk_iso_iff
  (morphismRestrictRestrictBasicOpen f _ r).symm).mp (H ⟨r, hr'⟩)

Result:
no goals

Proof state:
case hU
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → ↑Y.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
hU' : ∀ (i : ι), Q (f ∣_ ↑(U i))
this : Q.IsLocal := isLocal_affineProperty P
i : ι
⊢ Q (f ∣_ ↑(U i))

Tactic:
exact hU' i

Result:
no goals

Proof state:
case basicOpen
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U✝ : ι → ↑Y.affineOpens
hU : ⨆ i, ↑(U✝ i) = ⊤
hU' : ∀ (i : ι), Q (f ∣_ ↑(U✝ i))
this✝¹ : Q.IsLocal := isLocal_affineProperty P
U : ↑Y.affineOpens
r : ↑Γ(Y, ↑U)
h : Q (f ∣_ ↑U)
this✝ : IsAffine ↑↑U
this : Q (f ∣_ ↑U ∣_ (↑↑U).basicOpen ((ConcreteCategory.hom (↑U).topIso.inv) r))
⊢ Q (f ∣_ ↑(Y.affineBasicOpen r))

Tactic:
exact (Q.arrow_mk_iso_iff
  (morphismRestrictRestrictBasicOpen f _ r)).mp this

Result:
no goals

Proof state:
case openCover
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U✝ : ι → ↑Y.affineOpens
hU : ⨆ i, ↑(U✝ i) = ⊤
hU' : ∀ (i : ι), Q (f ∣_ ↑(U✝ i))
this : Q.IsLocal := isLocal_affineProperty P
U : ↑Y.affineOpens
s : Finset ↑Γ(Y, ↑U)
hs : Ideal.span ↑s = ⊤
H : ∀ (f_1 : { x // x ∈ s }), Q (f ∣_ ↑(Y.affineBasicOpen ↑f_1))
⊢ Q (f ∣_ ↑U)

Tactic:
apply AffineTargetMorphismProperty.IsLocal.of_basicOpenCover _
  (s.image (Scheme.Opens.topIso _).inv) (by simp [← Ideal.map_span, hs, Ideal.map_top])

Result:
case openCover
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U✝ : ι → ↑Y.affineOpens
hU : ⨆ i, ↑(U✝ i) = ⊤
hU' : ∀ (i : ι), Q (f ∣_ ↑(U✝ i))
this : Q.IsLocal := isLocal_affineProperty P
U : ↑Y.affineOpens
s : Finset ↑Γ(Y, ↑U)
hs : Ideal.span ↑s = ⊤
H : ∀ (f_1 : { x // x ∈ s }), Q (f ∣_ ↑(Y.affineBasicOpen ↑f_1))
⊢ ∀ (r : { x // x ∈ Finset.image (⇑(ConcreteCategory.hom (↑U).topIso.inv)) s }), Q (f ∣_ ↑U ∣_ (↑↑U).basicOpen ↑r)

Proof state:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → ↑Y.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
hU' : ∀ (i : ι), Q (f ∣_ ↑(U i))
this : Q.IsLocal := isLocal_affineProperty P
⊢ targetAffineLocally Q f

Tactic:
classical
intro V
induction V using of_affine_open_cover U hU  with
| basicOpen U r h =>
  haveI : IsAffine _ := U.2
  have := AffineTargetMorphismProperty.IsLocal.to_basicOpen (f ∣_ U.1) (U.1.topIso.inv r) h
  exact (Q.arrow_mk_iso_iff
    (morphismRestrictRestrictBasicOpen f _ r)).mp this
| openCover U s hs H =>
  apply AffineTargetMorphismProperty.IsLocal.of_basicOpenCover _
    (s.image (Scheme.Opens.topIso _).inv) (by simp [← Ideal.map_span, hs, Ideal.map_top])
  intro ⟨r, hr⟩
  obtain ⟨r, hr', rfl⟩ := Finset.mem_image.mp hr
  exact (Q.arrow_mk_iso_iff
    (morphismRestrictRestrictBasicOpen f _ r).symm).mp (H ⟨r, hr'⟩)
| hU i => exact hU' i

Result:
no goals