-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
𝒰 : Scheme.OpenCover.{u_1, u} X
inst_2 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
H : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
U : (↑X.affineOpens : Type u)
S : (i : 𝒰.I₀) → (↑X.affineOpens : Type u) :=
  fun (i : 𝒰.I₀) ↦ Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (Scheme.Hom.opensRange (𝒰.f i)) ⋯
basicOpen :
  ∀ (U : (↑X.affineOpens : Type u)) (r : (↑Γ(X, (↑U : X.Opens)) : Type u))
    (H :
      Q (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, (↑U : X.Opens)) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯))),
    Q (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, (↑(X.affineBasicOpen r) : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑(X.affineBasicOpen r) : X.Opens) ⋯))
openCover :
  ∀ (U : (↑X.affineOpens : Type u)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u))
    (hs : Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u))) ⊤)
    (H :
      ∀ (f_1 : ↥s),
        Q (R := (↑Γ(Y, ⊤) : Type u)) (S :=
          (↑Γ(X, (↑(X.affineBasicOpen (↑f_1 : (↑Γ(X, (↑U : X.Opens)) : Type u))) : X.Opens)) : Type u))
          (CommRingCat.Hom.hom
            (Scheme.Hom.appLE f ⊤ (↑(X.affineBasicOpen (↑f_1 : (↑Γ(X, (↑U : X.Opens)) : Type u))) : X.Opens) ⋯))),
    Q (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, (↑U : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯))
hU :
  ∀ (i : 𝒰.I₀),
    Q (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, (↑(S i) : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑(S i) : X.Opens) ⋯))
⊢ Q (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, (↑U : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯))

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 (𝒰.f i) (S i).1.ι
      Subtype.range_coe.symm).inv.app _), ← CommRingCat.hom_comp, ← Scheme.Hom.comp_appTop,
      IsOpenImmersion.isoOfRangeEq_inv_fac_assoc, Scheme.Hom.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

Premises used: AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_inv_fac_assoc, AlgebraicGeometry.Scheme.Hom.appTop, CommRingCat.hom_comp, AlgebraicGeometry.Scheme.Opens.ι_appTop, AlgebraicGeometry.Scheme.Hom.app_eq_appLE, AlgebraicGeometry.Scheme.affineBasicOpen_coe, AlgebraicGeometry.Scheme.Hom.comp_appTop, RingHom.algebraMap_toAlgebra, AlgebraicGeometry.Scheme.Hom.appLE_map