-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X : Scheme
s : Set ↥X
hs : IsLocallyConstructible s
R : CommRingCat
f : X ⟶ Spec R
hf : LocallyOfFinitePresentation f
inst_1 : QuasiCompact f
this :
  ∀ {X : Scheme.{u}} {s : Set ↥X} (hs : IsLocallyConstructible s) (R : CommRingCat.{u}) (f : X ⟶ Spec R)
    [hf : LocallyOfFinitePresentation f] [QuasiCompact f] (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    IsLocallyConstructible (X := ↥(Spec R)) (⇑f '' s)
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
inst_2 : CompactSpace.{u} ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
i : 𝒰.I₀
inst : QuasiCompact (𝒰.f i ≫ f)
h :
  Eq (α := Set ↥(Spec R)) (⇑f '' (s ∩ (↑(opensRange (𝒰.f i)) : Set ↥X)))
    (Set.image (α := ↥(𝒰.X i))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            ((𝒰.f i).base ≫ f.base)) :
        (a : ↥(𝒰.X i)) → ↥(Spec R))
      (⇑(𝒰.f i) ⁻¹' s))
h₁ :
  Eq (α := Set ↥(Spec R)) ((⇑(TopCat.Hom.hom f.base) : (a : ↥X) → ↥(Spec R)) '' (s ∩ (↑(opensRange (𝒰.f i)) : Set ↥X)))
    (Set.image (α := ↥(𝒰.X i))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            ((𝒰.f i).base ≫ f.base)) :
        (a : ↥(𝒰.X i)) → ↥(Spec R))
      (⇑(𝒰.f i) ⁻¹' s))
h₂ :
  Eq (α := Set ↥(Spec R)) ((⇑(TopCat.Hom.hom f.base) : (a : ↥X) → ↥(Spec R)) '' (s ∩ (↑(opensRange (𝒰.f i)) : Set ↥X)))
    (Set.image (α := ↥(𝒰.X i)) (⇑(TopCat.Hom.hom ((𝒰.f i).base ≫ f.base)) : (a : ↥(𝒰.X i)) → ↥(Spec R))
      (⇑(𝒰.f i) ⁻¹' s))
h₃ :
  Eq (α := Set ↥(Spec R)) ((⇑(TopCat.Hom.hom f.base) : (a : ↥X) → ↥(Spec R)) '' (s ∩ (↑(opensRange (𝒰.f i)) : Set ↥X)))
    (Set.image (α := ↥(𝒰.X i))
      (⇑((TopCat.Hom.hom f.base).comp (TopCat.Hom.hom (𝒰.f i).base)) : (a : ↥(𝒰.X i)) → ↥(Spec R)) (⇑(𝒰.f i) ⁻¹' s))
h₄ :
  Eq (α := Set ↥(Spec R)) ((⇑(TopCat.Hom.hom f.base) : (a : ↥X) → ↥(Spec R)) '' (s ∩ (↑(opensRange (𝒰.f i)) : Set ↥X)))
    (Set.image (α := ↥(𝒰.X i))
      (Function.comp (β := ↥X) (⇑(TopCat.Hom.hom f.base) : (a : ↥X) → ↥(Spec R))
        (⇑(TopCat.Hom.hom (𝒰.f i).base) : (a : ↥(𝒰.X i)) → ↥X))
      (⇑(𝒰.f i) ⁻¹' s))
h₅ :
  Eq (α := Set ↥(Spec R)) ((⇑(TopCat.Hom.hom f.base) : (a : ↥X) → ↥(Spec R)) '' (s ∩ (↑(opensRange (𝒰.f i)) : Set ↥X)))
    (Set.image (α := ↥X) (⇑(TopCat.Hom.hom f.base) : (a : ↥X) → ↥(Spec R))
      (Set.image (α := ↥(𝒰.X i)) (⇑(TopCat.Hom.hom (𝒰.f i).base) : (a : ↥(𝒰.X i)) → ↥X) (⇑(𝒰.f i) ⁻¹' s)))
h₆ :
  Eq (α := Set ↥(Spec R)) ((⇑(TopCat.Hom.hom f.base) : (a : ↥X) → ↥(Spec R)) '' (s ∩ (↑(opensRange (𝒰.f i)) : Set ↥X)))
    ((⇑(TopCat.Hom.hom f.base) : (a : ↥X) → ↥(Spec R)) ''
      (s ∩ Set.range (ι := ↥(𝒰.X i)) (⇑(TopCat.Hom.hom (𝒰.f i).base) : (a : ↥(𝒰.X i)) → ↥X)))
h₇ h₈ :
  Eq (α := Set ↥(Spec R))
    ((⇑(TopCat.Hom.hom f.base) : (a : ↥X) → ↥(Spec R)) '' (s ∩ Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)))
    ((⇑(TopCat.Hom.hom f.base) : (a : ↥X) → ↥(Spec R)) ''
      (s ∩ Set.range (ι := ↥(𝒰.X i)) (⇑(TopCat.Hom.hom (𝒰.f i).base) : (a : ↥(𝒰.X i)) → ↥X)))
⊢ Eq (α := Set ↥(Spec R)) (⇑f '' (s ∩ (↑(opensRange (𝒰.f i)) : Set ↥X)))
    (Set.image (α := ↥(𝒰.X i)) (⇑(𝒰.f i ≫ f)) (⇑(𝒰.f i) ⁻¹' s))

Tactic:
rw [Scheme.Hom.comp_base, ← TopCat.Hom.hom, ← TopCat.Hom.hom, TopCat.hom_comp,
      ContinuousMap.coe_comp, Set.image_comp, Set.image_preimage_eq_inter_range, coe_opensRange]

Premises used: ContinuousMap.coe_comp, Set.image_preimage_eq_inter_range, TopCat.Hom.hom, Set.image_comp, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.hom_comp, AlgebraicGeometry.Scheme.Hom.coe_opensRange