-- 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 = ⊤
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)

Tactic:
have := hs' r ⟨X.basicOpen (f.appLE ⊤ U le_top r.1), U.2.basicOpen (f.appLE ⊤ U le_top r.1)⟩
  (by simp [Scheme.Hom.appLE])

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))
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)

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
⊢ (sourceAffineLocally fun {R S} [CommRing R] [CommRing S] => P).IsLocal

Tactic:
constructor

Result:
case respectsIso
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
⊢ (sourceAffineLocally fun {R S} [CommRing R] [CommRing S] => P).toProperty.RespectsIso

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, ⊤)),
    sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => P) f →
      sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => P) (f ∣_ Y.basicOpen r)

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

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
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯))

Tactic:
apply h₃ _ _ 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 = ⊤
hs' : ∀ (r : { x // x ∈ s }), sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => P) (f ∣_ Y.basicOpen ↑r)
U : ↑X.affineOpens
⊢ ∀ (r : ↑↑s),
    (fun {R S} [CommRing R] [CommRing S] => P)
      (Localization.awayMap (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) ↑r)

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
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))
⊢ ↑⟨X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) ↑r), ⋯⟩ ≤ f ⁻¹ᵁ Y.basicOpen ↑r

Tactic:
simp [Scheme.Hom.appLE]

Result:
no goals

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
⊢ X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) r) = ↑U

Tactic:
simp only [Scheme.Hom.appLE, Opens.map_top, CommRingCat.comp_apply, RingHom.coe_comp,
  Function.comp_apply]

Result:
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
⊢ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) r)) =
    ↑U