-- Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
lemma locally_of_iff (hQl : LocalizationAwayPreserves Q)
    (hQa : StableUnderCompositionWithLocalizationAway Q)
    (h : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y), P f ↔
      ∀ (x : X), ∃ (U : Y.affineOpens) (V : X.affineOpens) (_ : x ∈ V.1) (e : V.1 ≤ f ⁻¹ᵁ U.1),
      Q (f.appLE U V e).hom) : HasRingHomProperty P (Locally Q) where
  isLocal_ringHomProperty := locally_propertyIsLocal hQl hQa
  eq_affineLocally'

Proof state:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => Q
hQa : StableUnderCompositionWithLocalizationAway fun {R S} [CommRing R] [CommRing S] => Q
h :
  ∀ {X Y : Scheme} (f : X ⟶ Y),
    P f ↔
      ∀ (x : ↑↑X.toPresheafedSpace),
        ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
⊢ P = affineLocally fun {R S} [CommRing R] [CommRing S] => Locally fun {R S} [CommRing R] [CommRing S] => Q

Tactic:
haveI : HasRingHomProperty (affineLocally (Locally Q)) (Locally Q) :=
  ⟨locally_propertyIsLocal hQl hQa, rfl⟩

Result:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => Q
hQa : StableUnderCompositionWithLocalizationAway fun {R S} [CommRing R] [CommRing S] => Q
h :
  ∀ {X Y : Scheme} (f : X ⟶ Y),
    P f ↔
      ∀ (x : ↑↑X.toPresheafedSpace),
        ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
this :
  HasRingHomProperty
    (affineLocally fun {R S} [CommRing R] [CommRing S] => Locally fun {R S} [CommRing R] [CommRing S] => Q)
    fun {R S} [CommRing R] [CommRing S] => Locally fun {R S} [CommRing R] [CommRing S] => Q
⊢ P = affineLocally fun {R S} [CommRing R] [CommRing S] => Locally fun {R S} [CommRing R] [CommRing S] => Q

Proof state:
case h
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => Q
hQa : StableUnderCompositionWithLocalizationAway fun {R S} [CommRing R] [CommRing S] => Q
h :
  ∀ {X Y : Scheme} (f : X ⟶ Y),
    P f ↔
      ∀ (x : ↑↑X.toPresheafedSpace),
        ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
this :
  HasRingHomProperty
    (affineLocally fun {R S} [CommRing R] [CommRing S] => Locally fun {R S} [CommRing R] [CommRing S] => Q)
    fun {R S} [CommRing R] [CommRing S] => Locally fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
f : X ⟶ Y
⊢ P f ↔ affineLocally (fun {R S} [CommRing R] [CommRing S] => Locally fun {R S} [CommRing R] [CommRing S] => Q) f

Tactic:
rw [h, iff_exists_appLE_locally (P := affineLocally (Locally Q)) hQa.left hQa.respectsIso]

Result:
no goals

Proof state:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => Q
hQa : StableUnderCompositionWithLocalizationAway fun {R S} [CommRing R] [CommRing S] => Q
h :
  ∀ {X Y : Scheme} (f : X ⟶ Y),
    P f ↔
      ∀ (x : ↑↑X.toPresheafedSpace),
        ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
this :
  HasRingHomProperty
    (affineLocally fun {R S} [CommRing R] [CommRing S] => Locally fun {R S} [CommRing R] [CommRing S] => Q)
    fun {R S} [CommRing R] [CommRing S] => Locally fun {R S} [CommRing R] [CommRing S] => Q
⊢ P = affineLocally fun {R S} [CommRing R] [CommRing S] => Locally fun {R S} [CommRing R] [CommRing S] => Q

Tactic:
ext X Y f

Result:
case h
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => Q
hQa : StableUnderCompositionWithLocalizationAway fun {R S} [CommRing R] [CommRing S] => Q
h :
  ∀ {X Y : Scheme} (f : X ⟶ Y),
    P f ↔
      ∀ (x : ↑↑X.toPresheafedSpace),
        ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
this :
  HasRingHomProperty
    (affineLocally fun {R S} [CommRing R] [CommRing S] => Locally fun {R S} [CommRing R] [CommRing S] => Q)
    fun {R S} [CommRing R] [CommRing S] => Locally fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
f : X ⟶ Y
⊢ P f ↔ affineLocally (fun {R S} [CommRing R] [CommRing S] => Locally fun {R S} [CommRing R] [CommRing S] => Q) f