-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U_1 : ι → (↑Y.affineOpens : Type u)
hU : Eq.{u + 1} (α := Y.Opens) (⨆ (i : ι), (↑(U_1 i) : Y.Opens)) ⊤
hU' : ∀ (i : ι), Q (X := (↑(f ⁻¹ᵁ (↑(U_1 i) : Y.Opens)) : Scheme)) (f ∣_ (↑(U_1 i) : Y.Opens))
this : Q.IsLocal := ⋯
U : (↑Y.affineOpens : Type u)
s : Finset (↑Γ(Y, (↑U : Y.Opens)) : Type u)
hs : Eq (α := Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, (↑U : Y.Opens)) : Type u))) ⊤
H :
  ∀ (f_1 : ↥s),
    Q (X := (↑(f ⁻¹ᵁ (↑(Y.affineBasicOpen (↑f_1 : (↑Γ(Y, (↑U : Y.Opens)) : Type u))) : Y.Opens)) : Scheme))
      (f ∣_ (↑(Y.affineBasicOpen (↑f_1 : (↑Γ(Y, (↑U : Y.Opens)) : Type u))) : Y.Opens))
r : (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u)
hr :
  Membership.mem (γ := Finset (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
    (Finset.image
      (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (↑U : Y.Opens).topIso.inv) :
        (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
      s)
    r
openCover :
  ∀ (r : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (hr' : r ∈ s)
    (hr :
      Membership.mem (α := (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u)) (γ :=
        Finset (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
        (Finset.image
          (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (↑U : Y.Opens).topIso.inv) :
            (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
          s)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (↑U : Y.Opens).topIso.inv :
              (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
            r :
          (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))),
    Q (X :=
      (↑((f ∣_ (↑U : Y.Opens)) ⁻¹ᵁ
            (↑(↑U : Y.Opens) : Scheme).basicOpen (U := ⊤)
              (↑(Subtype.mk (p := fun (x : (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u)) ↦
                    Membership.mem (γ := Finset (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
                      (Finset.image
                        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                              (CC := CommRingCat.carrier) (↑U : Y.Opens).topIso.inv) :
                          (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
                        s)
                      x)
                    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                          CommRingCat.carrier) (↑U : Y.Opens).topIso.inv :
                        (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
                      r)
                    hr) :
                (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))) :
        Scheme))
      (f ∣_ (↑U : Y.Opens) ∣_
        (↑(↑U : Y.Opens) : Scheme).basicOpen (U := ⊤)
          (↑(Subtype.mk (p := fun (x : (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u)) ↦
                Membership.mem (γ := Finset (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
                  (Finset.image
                    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                          CommRingCat.carrier) (↑U : Y.Opens).topIso.inv) :
                      (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
                    s)
                  x)
                ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier) (↑U : Y.Opens).topIso.inv :
                    (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
                  r)
                hr) :
            (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u)))
⊢ Q (X :=
    (↑((f ∣_ (↑U : Y.Opens)) ⁻¹ᵁ
          (↑(↑U : Y.Opens) : Scheme).basicOpen
            (↑(Subtype.mk (p := fun (x : (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u)) ↦
                  Membership.mem (γ := Finset (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
                    (Finset.image
                      (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                            (CC := CommRingCat.carrier) (↑U : Y.Opens).topIso.inv) :
                        (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
                      s)
                    x)
                  r hr) :
              (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))) :
      Scheme))
    (f ∣_ (↑U : Y.Opens) ∣_
      (↑(↑U : Y.Opens) : Scheme).basicOpen
        (↑(Subtype.mk (p := fun (x : (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u)) ↦
              Membership.mem (γ := Finset (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
                (Finset.image
                  (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        CommRingCat.carrier) (↑U : Y.Opens).topIso.inv) :
                    (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
                  s)
                x)
              r hr) :
          (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u)))

Tactic:
obtain ⟨r, hr', rfl⟩ := Finset.mem_image.mp hr

Premises used: Finset.mem_image, Iff.mp, rfl