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

Tactic:
intro X Y _ f r H

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

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
U : ↑X.affineOpens
hU : ↑U ≤ f ⁻¹ᵁ Y.basicOpen r
this : X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) r) = ↑U
⊢ P
    (IsLocalization.Away.map (↑(Y.presheaf.toPrefunctor.1 (op (Y.basicOpen r))))
      (↑(X.presheaf.toPrefunctor.1 (op (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) r)))))
      (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) r)

Tactic:
apply (config := { allowSynthFailures := true }) h₂

Result:
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 ⋯))

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

Tactic:
rw [Scheme.basicOpen_res]

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

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
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 (Y.basicOpen r) (↑U) hU))

Tactic:
rw [← f.appLE_congr _ rfl this (fun f => P f.hom),
  IsAffineOpen.appLE_eq_away_map f (isAffineOpen_top Y) U.2 _ r]

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
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
      (CommRingCat.ofHom
        (IsLocalization.Away.map (↑(Y.presheaf.toPrefunctor.1 (op (Y.basicOpen r))))
          (↑(X.presheaf.toPrefunctor.1 (op (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) r)))))
          (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) r)))

Proof state:
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

Tactic:
exact sourceAffineLocally_respectsIso P h₁

Result:
no goals