-- 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 : (↑Γ(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:
exact (Q.arrow_mk_iso_iff
      (morphismRestrictRestrictBasicOpen f _ r).symm).mp (H ⟨r, hr'⟩)

Premises used: AlgebraicGeometry.AffineTargetMorphismProperty.arrow_mk_iso_iff, Subtype.mk, CategoryTheory.Iso.symm, Iff.mp, AlgebraicGeometry.morphismRestrictRestrictBasicOpen