-- Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
theorem of_iSup_eq_top [IsAffine Y] {ι : Type*}
    (U : ι → X.affineOpens) (hU : ⨆ i, (U i : Opens X) = ⊤)
    (H : ∀ i, Q (f.appLE ⊤ (U i).1 le_top).hom) :
    P f

Proof state:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
ι : Type u_1
U : ι → ↑X.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
H : ∀ (i : ι), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(U i) ⋯))
this :
  ∀ (i : (X.openCoverOfISupEqTop (fun i => ↑(U i)) hU).J),
    IsAffine ((X.openCoverOfISupEqTop (fun i => ↑(U i)) hU).obj i)
⊢ P f

Tactic:
refine of_source_openCover (X.openCoverOfISupEqTop _ hU) fun i ↦ ?_

Result:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
ι : Type u_1
U : ι → ↑X.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
H : ∀ (i : ι), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(U i) ⋯))
this :
  ∀ (i : (X.openCoverOfISupEqTop (fun i => ↑(U i)) hU).J),
    IsAffine ((X.openCoverOfISupEqTop (fun i => ↑(U i)) hU).obj i)
i : (X.openCoverOfISupEqTop (fun i => ↑(U i)) hU).J
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop ((X.openCoverOfISupEqTop (fun i => ↑(U i)) hU).map i ≫ f)))

Proof state:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
ι : Type u_1
U : ι → ↑X.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
H : ∀ (i : ι), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(U i) ⋯))
this :
  ∀ (i : (X.openCoverOfISupEqTop (fun i => ↑(U i)) hU).J),
    IsAffine ((X.openCoverOfISupEqTop (fun i => ↑(U i)) hU).obj i)
i : (X.openCoverOfISupEqTop (fun i => ↑(U i)) hU).J
⊢ ↑(U i) = (↑(U i)).ι ''ᵁ ⊤

Tactic:
simp

Result:
no goals

Proof state:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
ι : Type u_1
U : ι → ↑X.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
H : ∀ (i : ι), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(U i) ⋯))
⊢ P f

Tactic:
have (i) : IsAffine ((X.openCoverOfISupEqTop _ hU).obj i) := (U i).2

Result:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
ι : Type u_1
U : ι → ↑X.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
H : ∀ (i : ι), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(U i) ⋯))
this :
  ∀ (i : (X.openCoverOfISupEqTop (fun i => ↑(U i)) hU).J),
    IsAffine ((X.openCoverOfISupEqTop (fun i => ↑(U i)) hU).obj i)
⊢ P f

Proof state:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
ι : Type u_1
U : ι → ↑X.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
H : ∀ (i : ι), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(U i) ⋯))
this :
  ∀ (i : (X.openCoverOfISupEqTop (fun i => ↑(U i)) hU).J),
    IsAffine ((X.openCoverOfISupEqTop (fun i => ↑(U i)) hU).obj i)
i : (X.openCoverOfISupEqTop (fun i => ↑(U i)) hU).J
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop ((X.openCoverOfISupEqTop (fun i => ↑(U i)) hU).map i ≫ f)))

Tactic:
simpa [Scheme.Hom.app_eq_appLE] using (f.appLE_congr _ rfl (by simp) (fun f => Q f.hom)).mp (H i)

Result:
no goals