-- Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
theorem of_source_openCover [IsAffine Y]
    (𝒰 : X.OpenCover) [∀ i, IsAffine (𝒰.obj i)] (H : ∀ i, Q ((𝒰.map i ≫ f).appTop.hom)) :
    P f

Proof state:
case openCover
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
H✝ : ∀ (i : 𝒰.J), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.map i ≫ f)))
S : 𝒰.J → ↑X.affineOpens := fun i => ⟨Scheme.Hom.opensRange (𝒰.map i), ⋯⟩
U : ↑X.affineOpens
s : Finset ↑Γ(X, ↑U)
hs : Ideal.span ↑s = ⊤
H : ∀ (f_1 : { x // x ∈ s }), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(X.affineBasicOpen ↑f_1) ⋯))
⊢ ∀ (r : ↑↑s),
    ∃ T x x_1,
      ∃ (_ : IsLocalization.Away (↑r) T),
        Q ((algebraMap (↑Γ(X, ↑U)) T).comp (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)))

Tactic:
rintro r

Result:
case openCover
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
H✝ : ∀ (i : 𝒰.J), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.map i ≫ f)))
S : 𝒰.J → ↑X.affineOpens := fun i => ⟨Scheme.Hom.opensRange (𝒰.map i), ⋯⟩
U : ↑X.affineOpens
s : Finset ↑Γ(X, ↑U)
hs : Ideal.span ↑s = ⊤
H : ∀ (f_1 : { x // x ∈ s }), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(X.affineBasicOpen ↑f_1) ⋯))
r : ↑↑s
⊢ ∃ T x x_1,
    ∃ (_ : IsLocalization.Away (↑r) T),
      Q ((algebraMap (↑Γ(X, ↑U)) T).comp (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)))

Proof state:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
H : ∀ (i : 𝒰.J), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.map i ≫ f)))
U : ↑X.affineOpens
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯))

Tactic:
let S i : X.affineOpens := ⟨_, isAffineOpen_opensRange (𝒰.map i)⟩

Result:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
H : ∀ (i : 𝒰.J), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.map i ≫ f)))
U : ↑X.affineOpens
S : 𝒰.J → ↑X.affineOpens := fun i => ⟨Scheme.Hom.opensRange (𝒰.map i), ⋯⟩
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯))

Proof state:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
H : ∀ (i : 𝒰.J), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.map i ≫ f)))
U : ↑X.affineOpens
S : 𝒰.J → ↑X.affineOpens := fun i => ⟨Scheme.Hom.opensRange (𝒰.map i), ⋯⟩
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯))

Tactic:
induction U using of_affine_open_cover S 𝒰.iSup_opensRange with
| basicOpen U r H =>
  simp_rw [Scheme.affineBasicOpen_coe,
    ← f.appLE_map (U := ⊤) le_top (homOfLE (X.basicOpen_le r)).op]
  have := U.2.isLocalization_basicOpen r
  exact (isLocal_ringHomProperty P).StableUnderCompositionWithLocalizationAwayTarget _ r _ H
| openCover U s hs H =>
  apply (isLocal_ringHomProperty P).ofLocalizationSpanTarget.ofIsLocalization
    (isLocal_ringHomProperty P).respectsIso _ _ hs
  rintro r
  refine ⟨_, _, _, IsAffineOpen.isLocalization_basicOpen U.2 r, ?_⟩
  rw [RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp, Scheme.Hom.appLE_map]
  exact H r
| hU i =>
  specialize H i
  rw [← (isLocal_ringHomProperty P).respectsIso.cancel_right_isIso _
    ((IsOpenImmersion.isoOfRangeEq (𝒰.map i) (S i).1.ι
    Subtype.range_coe.symm).inv.app _), ← CommRingCat.hom_comp, ← Scheme.comp_appTop,
    IsOpenImmersion.isoOfRangeEq_inv_fac_assoc, Scheme.comp_appTop,
    Scheme.Opens.ι_appTop, Scheme.Hom.appTop, Scheme.Hom.app_eq_appLE, Scheme.Hom.appLE_map] at H
  exact (f.appLE_congr _ rfl (by simp) (fun f => Q f.hom)).mp H

Result:
no goals

Proof state:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
H : ∀ (i : 𝒰.J), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.map i ≫ f)))
⊢ P f

Tactic:
rw [HasAffineProperty.iff_of_isAffine (P := P)]

Result:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
H : ∀ (i : 𝒰.J), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.map i ≫ f)))
⊢ sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => Q) f

Proof state:
case openCover
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
H✝ : ∀ (i : 𝒰.J), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.map i ≫ f)))
S : 𝒰.J → ↑X.affineOpens := fun i => ⟨Scheme.Hom.opensRange (𝒰.map i), ⋯⟩
U : ↑X.affineOpens
s : Finset ↑Γ(X, ↑U)
hs : Ideal.span ↑s = ⊤
H : ∀ (f_1 : { x // x ∈ s }), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(X.affineBasicOpen ↑f_1) ⋯))
r : ↑↑s
⊢ ∃ T x x_1,
    ∃ (_ : IsLocalization.Away (↑r) T),
      Q ((algebraMap (↑Γ(X, ↑U)) T).comp (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)))

Tactic:
refine ⟨_, _, _, IsAffineOpen.isLocalization_basicOpen U.2 r, ?_⟩

Result:
case openCover
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
H✝ : ∀ (i : 𝒰.J), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.map i ≫ f)))
S : 𝒰.J → ↑X.affineOpens := fun i => ⟨Scheme.Hom.opensRange (𝒰.map i), ⋯⟩
U : ↑X.affineOpens
s : Finset ↑Γ(X, ↑U)
hs : Ideal.span ↑s = ⊤
H : ∀ (f_1 : { x // x ∈ s }), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(X.affineBasicOpen ↑f_1) ⋯))
r : ↑↑s
⊢ Q ((algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen ↑r)).comp (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)))

Proof state:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
H : ∀ (i : 𝒰.J), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.map i ≫ f)))
⊢ sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => Q) f

Tactic:
intro U

Result:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
H : ∀ (i : 𝒰.J), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.map i ≫ f)))
U : ↑X.affineOpens
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯))