-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
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
⊢ 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)))
have 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)))
Tactic: obtain ⟨r, hr', rfl⟩ := Finset.mem_image.mp hr
Cleared hypotheses: r, hr