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

Tactic:
simp only [CommRingCat.hom_ofHom]

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
    (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:
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 ≤ f ⁻¹ᵁ ⊤

Tactic:
simp

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
⊢ ∀ (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ Y.basicOpen r),
    P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (↑V) e))

Tactic:
intro U hU

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
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (↑U) hU))

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
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (↑U) hU))

Tactic:
have : X.basicOpen (f.appLE ⊤ U (by simp) r) = U := by
  simp only [Scheme.Hom.appLE, Opens.map_top, CommRingCat.comp_apply, RingHom.coe_comp,
    Function.comp_apply]
  rw [Scheme.basicOpen_res]
  simpa using hU

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

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),
    (fun {R S} [CommRing R] [CommRing S] => P)
      (Localization.awayMap (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) ↑r)

Tactic:
intro r

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