-- Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
theorem sourceAffineLocally_isLocal (h₁ : RingHom.RespectsIso P)
    (h₂ : RingHom.LocalizationAwayPreserves P) (h₃ : RingHom.OfLocalizationSpan P) :
    (sourceAffineLocally P).IsLocal

Proof state:
case of_basicOpenCover
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P
h₂ : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => P
h₃ : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => P
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hs' : ∀ (r : { x // x ∈ s }), sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => P) (f ∣_ Y.basicOpen ↑r)
U : ↑X.affineOpens
r : ↑↑s
⊢ P (Localization.awayMap (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) ↑r)

Tactic:
simp_rw [sourceAffineLocally_morphismRestrict] at hs'

Result:
case of_basicOpenCover
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P
h₂ : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => P
h₃ : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => P
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
U : ↑X.affineOpens
r : ↑↑s
hs' :
  ∀ (r : { x // x ∈ s }) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ Y.basicOpen ↑r),
    P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen ↑r) (↑V) e))
⊢ P (Localization.awayMap (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) ↑r)

Proof state:
case to_basicOpen.a
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P
h₂ : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => P
h₃ : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => P
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
r : ↑Γ(Y, ⊤)
H : sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => P) f
U : ↑X.affineOpens
hU : ↑U ≤ f ⁻¹ᵁ Y.basicOpen r
this : X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) r) = ↑U
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯))

Tactic:
exact H U

Result:
no goals

Proof state:
case to_basicOpen
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P
h₂ : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => P
h₃ : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => P
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
r : ↑Γ(Y, ⊤)
H : sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => P) f
⊢ sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => P) (f ∣_ Y.basicOpen r)

Tactic:
rw [sourceAffineLocally_morphismRestrict]

Result:
case to_basicOpen
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P
h₂ : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => P
h₃ : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => P
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
r : ↑Γ(Y, ⊤)
H : sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => P) f
⊢ ∀ (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ Y.basicOpen r),
    P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (↑V) e))

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P
h₂ : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => P
h₃ : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => P
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
r : ↑Γ(Y, ⊤)
H : sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => P) f
U : ↑X.affineOpens
hU : ↑U ≤ f ⁻¹ᵁ Y.basicOpen r
⊢ ↑U ⊓ X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) r) = ↑U

Tactic:
simpa using hU

Result:
no goals

Proof state:
case of_basicOpenCover
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P
h₂ : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => P
h₃ : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => P
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
U : ↑X.affineOpens
r : ↑↑s
hs' :
  ∀ (r : { x // x ∈ s }) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ Y.basicOpen ↑r),
    P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen ↑r) (↑V) e))
this :
  P
    (CommRingCat.Hom.hom
      (Scheme.Hom.appLE f (Y.basicOpen ↑r) ↑⟨X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) ↑r), ⋯⟩ ⋯))
⊢ P (Localization.awayMap (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) ↑r)

Tactic:
rwa [IsAffineOpen.appLE_eq_away_map f (isAffineOpen_top Y) U.2, CommRingCat.hom_ofHom,
  ← h₁.is_localization_away_iff] at this

Result:
no goals

Proof state:
case of_basicOpenCover
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P
h₂ : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => P
h₃ : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => P
⊢ ∀ {X Y : Scheme} [inst : IsAffine Y] (f : X ⟶ Y) (s : Finset ↑Γ(Y, ⊤)),
    Ideal.span ↑s = ⊤ →
      (∀ (r : { x // x ∈ s }), sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => P) (f ∣_ Y.basicOpen ↑r)) →
        sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => P) f

Tactic:
introv hs hs' U

Result:
case of_basicOpenCover
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P
h₂ : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => P
h₃ : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => P
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hs' : ∀ (r : { x // x ∈ s }), sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => P) (f ∣_ Y.basicOpen ↑r)
U : ↑X.affineOpens
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯))