-- Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
/-- If `P` is induced by `Locally Q`, it suffices to check `Q` on affine open sets locally around
points of the source. -/
lemma iff_exists_appLE_locally
    (hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource Q)
    (hQi : RespectsIso Q) [HasRingHomProperty P (Locally Q)] :
    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

Proof state:
case refine_1.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] => Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] => Locally fun {R S} [CommRing R] [CommRing S] => Q
this✝¹ : P.Respects @IsOpenImmersion
x : ↑↑X.toPresheafedSpace
U : Opens ↑↑Y.toPresheafedSpace
hU : U ∈ Y.affineOpens
hfx : (ConcreteCategory.hom f.base) x ∈ U
right✝ : U ≤ ⊤
V : Opens ↑↑X.toPresheafedSpace
hV : V ∈ X.affineOpens
hx : x ∈ V
e : V ≤ f ⁻¹ᵁ U
hf :
  ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
    ∃ s,
      ∃ (_ : Ideal.span ↑s = ⊤),
        ∀ t ∈ s,
          ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, ↑V)) Sₜ] [inst_2 : IsLocalization.Away t Sₜ],
            Q ((algebraMap (↑Γ(X, ↑V)) Sₜ).comp (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e)))
s : Finset ↑Γ(X, ↑⟨V, hV⟩)
hfs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, ↑⟨V, hV⟩)) Sₜ] [inst_2 : IsLocalization.Away t Sₜ],
      Q ((algebraMap (↑Γ(X, ↑⟨V, hV⟩)) Sₜ).comp (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑⟨U, hU⟩) (↑⟨V, hV⟩) e)))
hs : ⨆ i ∈ ↑s, X.basicOpen i = ↑⟨V, hV⟩
this✝ : x ∈ ⨆ i ∈ s, X.basicOpen i
r : ↑Γ(X, ↑⟨V, hV⟩)
hr : r ∈ s
hrs : x ∈ X.basicOpen r
this : IsLocalization.Away r ↑Γ(X, X.basicOpen r)
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e ≫ X.presheaf.map (homOfLE ⋯).op))

Tactic:
exact hfs r hr _

Result:
no goals

Proof state:
case h
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] => Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] => Locally fun {R S} [CommRing R] [CommRing S] => Q
this : P.Respects @IsOpenImmersion
hf✝ :
  ∀ (x : ↑↑X.toPresheafedSpace),
    ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
x : ↑↑X.toPresheafedSpace
U : ↑Y.affineOpens
V : ↑X.affineOpens
hxV : x ∈ ↑V
e : ↑V ≤ f ⁻¹ᵁ ↑U
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.app f ↑U ≫ X.presheaf.map (homOfLE e).op))
⊢ Locally (fun {R S} [CommRing R] [CommRing S] => Q)
    (CommRingCat.Hom.hom (Scheme.Hom.appTop (Scheme.Hom.resLE f (↑U) (↑V) e)))

Tactic:
haveI : (toMorphismProperty (Locally Q)).RespectsIso := toMorphismProperty_respectsIso_iff.mp <|
  (isLocal_ringHomProperty P).respectsIso

Result:
case h
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] => Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] => Locally fun {R S} [CommRing R] [CommRing S] => Q
this✝ : P.Respects @IsOpenImmersion
hf✝ :
  ∀ (x : ↑↑X.toPresheafedSpace),
    ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
x : ↑↑X.toPresheafedSpace
U : ↑Y.affineOpens
V : ↑X.affineOpens
hxV : x ∈ ↑V
e : ↑V ≤ f ⁻¹ᵁ ↑U
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.app f ↑U ≫ X.presheaf.map (homOfLE e).op))
this :
  (toMorphismProperty fun {R S} [CommRing R] [CommRing S] =>
      Locally fun {R S} [CommRing R] [CommRing S] => Q).RespectsIso
⊢ Locally (fun {R S} [CommRing R] [CommRing S] => Q)
    (CommRingCat.Hom.hom (Scheme.Hom.appTop (Scheme.Hom.resLE f (↑U) (↑V) e)))

Proof state:
case h
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] => Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] => Locally fun {R S} [CommRing R] [CommRing S] => Q
this✝ : P.Respects @IsOpenImmersion
hf✝ :
  ∀ (x : ↑↑X.toPresheafedSpace),
    ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
x : ↑↑X.toPresheafedSpace
U : ↑Y.affineOpens
V : ↑X.affineOpens
hxV : x ∈ ↑V
e : ↑V ≤ f ⁻¹ᵁ ↑U
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.app f ↑U ≫ X.presheaf.map (homOfLE e).op))
this :
  (toMorphismProperty fun {R S} [CommRing R] [CommRing S] =>
      Locally fun {R S} [CommRing R] [CommRing S] => Q).RespectsIso
⊢ Locally (fun {R S} [CommRing R] [CommRing S] => Q)
    (CommRingCat.Hom.hom (Scheme.Hom.appTop (Scheme.Hom.resLE f (↑U) (↑V) e)))

Tactic:
exact (MorphismProperty.arrow_mk_iso_iff (toMorphismProperty (Locally Q))
  (arrowResLEAppIso f U V e)).mpr (locally_of hQi _ hf)

Result:
no goals

Proof state:
case refine_2
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] => Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] => Locally fun {R S} [CommRing R] [CommRing S] => Q
this : P.Respects @IsOpenImmersion
hf :
  ∀ (x : ↑↑X.toPresheafedSpace),
    ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
x : ↑↑X.toPresheafedSpace
⊢ ∃ U V, ∃ (_ : x ∈ V.carrier) (e : V ≤ f ⁻¹ᵁ U), P (Scheme.Hom.resLE f U V e)

Tactic:
obtain ⟨U, V, hxV, e, hf⟩ := hf x

Result:
case refine_2.intro.intro.intro.intro
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] => Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] => Locally fun {R S} [CommRing R] [CommRing S] => Q
this : P.Respects @IsOpenImmersion
hf✝ :
  ∀ (x : ↑↑X.toPresheafedSpace),
    ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
x : ↑↑X.toPresheafedSpace
U : ↑Y.affineOpens
V : ↑X.affineOpens
hxV : x ∈ ↑V
e : ↑V ≤ f ⁻¹ᵁ ↑U
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
⊢ ∃ U V, ∃ (_ : x ∈ V.carrier) (e : V ≤ f ⁻¹ᵁ U), P (Scheme.Hom.resLE f U V e)