-- 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
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)))
⊢ ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))

Tactic:
obtain ⟨s, hs, hfs⟩ := hf ⟨U, hU⟩ ⟨V, hV⟩ e

Result:
case refine_1.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⟩)
hs : Ideal.span ↑s = ⊤
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)))
⊢ ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))

Proof state:
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
⊢ P f ↔
    ∀ (x : ↑↑X.toPresheafedSpace),
      ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))

Tactic:
have := respects_isOpenImmersion (P := P)
  (RingHom.locally_StableUnderCompositionWithLocalizationAwaySource hQ)

Result:
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
⊢ P f ↔
    ∀ (x : ↑↑X.toPresheafedSpace),
      ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))

Proof state:
case refine_1.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⟩
⊢ ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))

Tactic:
have : x ∈ (⨆ i ∈ s, X.basicOpen i) := hs.symm ▸ hx

Result:
case refine_1.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
⊢ ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))