-- 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
⊢ Q ((algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen ↑r)).comp (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)))

Tactic:
rw [RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp, Scheme.Hom.appLE_map]

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

Proof state:
case hU
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)
S : 𝒰.J → ↑X.affineOpens := fun i => ⟨Scheme.Hom.opensRange (𝒰.map i), ⋯⟩
i : 𝒰.J
H : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.map i ≫ f)))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(S i) ⋯))

Tactic:
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

Result:
case hU
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)
S : 𝒰.J → ↑X.affineOpens := fun i => ⟨Scheme.Hom.opensRange (𝒰.map i), ⋯⟩
i : 𝒰.J
H : Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ((↑(S i)).ι ''ᵁ ⊤) ⋯))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(S i) ⋯))

Proof state:
case hU
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), ⋯⟩
i : 𝒰.J
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(S i) ⋯))

Tactic:
specialize H i

Result:
case hU
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)
S : 𝒰.J → ↑X.affineOpens := fun i => ⟨Scheme.Hom.opensRange (𝒰.map i), ⋯⟩
i : 𝒰.J
H : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.map i ≫ f)))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(S i) ⋯))

Proof state:
case hU
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)
S : 𝒰.J → ↑X.affineOpens := fun i => ⟨Scheme.Hom.opensRange (𝒰.map i), ⋯⟩
i : 𝒰.J
H : Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ((↑(S i)).ι ''ᵁ ⊤) ⋯))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(S i) ⋯))

Tactic:
exact (f.appLE_congr _ rfl (by simp) (fun f => Q f.hom)).mp H

Result:
no goals

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

Tactic:
exact H r

Result:
no goals

Proof state:
case basicOpen
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
r : ↑Γ(X, ↑U)
H : Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯))
this : IsLocalization.Away r ↑Γ(X, X.basicOpen r)
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯ ≫ X.presheaf.map (homOfLE ⋯).op))

Tactic:
exact (isLocal_ringHomProperty P).StableUnderCompositionWithLocalizationAwayTarget _ r _ H

Result:
no goals

Proof state:
case basicOpen
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
r : ↑Γ(X, ↑U)
H : Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(X.affineBasicOpen r) ⋯))

Tactic:
simp_rw [Scheme.affineBasicOpen_coe,
  ← f.appLE_map (U := ⊤) le_top (homOfLE (X.basicOpen_le r)).op]

Result:
case basicOpen
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
r : ↑Γ(X, ↑U)
H : Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯ ≫ X.presheaf.map (homOfLE ⋯).op))