awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
hf : affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FinitePresentation) f
⊢ affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FiniteType) f

Tactic:
affineLocally_le (fun hf ↦ ?_) f hf

Premises used: AlgebraicGeometry.affineLocally_le
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
hf : affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FinitePresentation) f
refine :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S} (hf : f.FinitePresentation), f.FiniteType
⊢ affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FiniteType) f

Tactic:
refine affineLocally_le (fun hf ↦ ?_) f hf

Premises used: AlgebraicGeometry.affineLocally_le
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
hf_1 : affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FinitePresentation) f
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f_2 : R →+* S
hf : f_2.FinitePresentation
⊢ f_2.FiniteType

Tactic:
RingHom.FiniteType.of_finitePresentation hf

Premises used: RingHom.FiniteType.of_finitePresentation
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
hf_1 : affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FinitePresentation) f
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f_2 : R →+* S
hf : f_2.FinitePresentation
⊢ f_2.FiniteType

Tactic:
exact RingHom.FiniteType.of_finitePresentation hf

Premises used: RingHom.FiniteType.of_finitePresentation
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X}
        (hs : IsLocallyConstructible s) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
        IsLocallyConstructible (X := ↥Y) (⇑f '' s))
    (hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R), IsLocallyConstructible (X := ↥Y) (⇑f '' s)
wlog :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X}
    (hs : IsLocallyConstructible s) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsLocallyConstructible (X := ↥Y) (⇑f '' s)
⊢ IsLocallyConstructible (X := ↥Y) (⇑f '' s)

Tactic:
wlog hY : ∃ R, Y = Spec R
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X}
    (hs : IsLocallyConstructible s) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsLocallyConstructible (X := ↥Y) (⇑f '' s)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
⊢ IsLocallyConstructible (X := ↥Y) (⇑f '' s)

Tactic:
.of_isOpenCover Y.affineCover.isOpenCover_opensRange fun i ↦ ?_

Premises used: AlgebraicGeometry.Scheme.OpenCover.isOpenCover_opensRange, Topology.IsLocallyConstructible.of_isOpenCover, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X}
    (hs : IsLocallyConstructible s) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsLocallyConstructible (X := ↥Y) (⇑f '' s)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
inr :
  ∀ (i : Y.affineCover.I₀),
    IsLocallyConstructible (X := (↑(↑(opensRange (Y.affineCover.f i)) : Set ↥Y) : Type u))
      (Subtype.val (p := fun (x : ↥Y) ↦ x ∈ (↑(opensRange (Y.affineCover.f i)) : Set ↥Y)) ⁻¹' ⇑f '' s)
⊢ IsLocallyConstructible (X := ↥Y) (⇑f '' s)

Tactic:
refine .of_isOpenCover Y.affineCover.isOpenCover_opensRange fun i ↦ ?_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X}
    (hs : IsLocallyConstructible s) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsLocallyConstructible (X := ↥Y) (⇑f '' s)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.I₀
⊢ LocallyOfFinitePresentation (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)

Tactic:
have inst : LocallyOfFinitePresentation (Y.affineCover.pullbackHom f i) :=
      MorphismProperty.pullback_snd _ _ inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst_1 : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X}
    (hs : IsLocallyConstructible s) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsLocallyConstructible (X := ↥Y) (⇑f '' s)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.I₀
inst :
  LocallyOfFinitePresentation (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
⊢ QuasiCompact (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)

Tactic:
have inst : QuasiCompact (Y.affineCover.pullbackHom f i) :=
      MorphismProperty.pullback_snd _ _ inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst_1 : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X}
    (hs : IsLocallyConstructible s) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsLocallyConstructible (X := ↥Y) (⇑f '' s)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.I₀
inst_2 :
  LocallyOfFinitePresentation (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
inst :
  QuasiCompact (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
⊢ IsLocallyConstructible (X := ↥(↑(opensRange (Y.affineCover.f i)) : Scheme))
    (Set.preimage (β := ↥(Y.affineCover.X i)) (⇑(Iso.inv (isoOpensRange (Y.affineCover.f i))))
      (Set.image (α := ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i))
        (⇑(Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i))
        (⇑((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i) ⁻¹' s)))

Tactic:
(this (Y.affineCover.pullbackHom f i)
            (hs.preimage_of_isOpenEmbedding ((Y.affineCover.pullback₁ f).f i).isOpenEmbedding)
            ⟨_, rfl⟩).preimage_of_isOpenEmbedding
        (Y.affineCover.f i).isoOpensRange.inv.isOpenEmbedding

Premises used: Topology.IsLocallyConstructible.preimage_of_isOpenEmbedding, AlgebraicGeometry.Scheme.Hom.isoOpensRange, AlgebraicGeometry.Scheme.Cover.pullbackHom, CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, Exists.intro, CategoryTheory.Precoverage.ZeroHypercover.pullback₁, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Iso.inv, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst_1 : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X}
    (hs : IsLocallyConstructible s) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsLocallyConstructible (X := ↥Y) (⇑f '' s)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.I₀
inst_2 :
  LocallyOfFinitePresentation (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
inst :
  QuasiCompact (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
h :
  (↑(↑(opensRange (Y.affineCover.f i)) : Set ↥Y) : Type u) = ↥(↑(opensRange (Y.affineCover.f i)) : Scheme) →
    Eq (α := Set (↑(↑(opensRange (Y.affineCover.f i)) : Set ↥Y) : Type u))
      (Subtype.val (p := fun (x : ↥Y) ↦ x ∈ (↑(opensRange (Y.affineCover.f i)) : Set ↥Y)) ⁻¹' ⇑f '' s)
      (Set.preimage (β := ↥(Y.affineCover.X i)) (⇑(Iso.inv (isoOpensRange (Y.affineCover.f i))))
        (Set.image (α := ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i))
          (⇑(Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i))
          (⇑((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i) ⁻¹' s)))
⊢ IsLocallyConstructible (X := (↑(↑(opensRange (Y.affineCover.f i)) : Set ↥Y) : Type u))
    (Subtype.val (p := fun (x : ↥Y) ↦ x ∈ (↑(opensRange (Y.affineCover.f i)) : Set ↥Y)) ⁻¹' ⇑f '' s)

Tactic:
convert!
      (this (Y.affineCover.pullbackHom f i)
            (hs.preimage_of_isOpenEmbedding ((Y.affineCover.pullback₁ f).f i).isOpenEmbedding)
            ⟨_, rfl⟩).preimage_of_isOpenEmbedding
        (Y.affineCover.f i).isoOpensRange.inv.isOpenEmbedding

Premises used: Topology.IsLocallyConstructible.preimage_of_isOpenEmbedding, AlgebraicGeometry.Scheme.Hom.isoOpensRange, AlgebraicGeometry.Scheme.Cover.pullbackHom, CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, Exists.intro, CategoryTheory.Precoverage.ZeroHypercover.pullback₁, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Iso.inv, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst_1 : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X}
    (hs : IsLocallyConstructible s) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsLocallyConstructible (X := ↥Y) (⇑f '' s)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.I₀
inst_2 :
  LocallyOfFinitePresentation (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
inst :
  QuasiCompact (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
e_1 : (↑(↑(opensRange (Y.affineCover.f i)) : Set ↥Y) : Type u) = ↥(↑(opensRange (Y.affineCover.f i)) : Scheme)
⊢ Eq (α := Set (↑(↑(opensRange (Y.affineCover.f i)) : Set ↥Y) : Type u))
    (Subtype.val (p := fun (x : ↥Y) ↦ x ∈ (↑(opensRange (Y.affineCover.f i)) : Set ↥Y)) ⁻¹' ⇑f '' s)
    (Set.preimage (β := ↥(Y.affineCover.X i)) (⇑(Iso.inv (isoOpensRange (Y.affineCover.f i))))
      (Set.image (α := ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i))
        (⇑(Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i))
        (⇑((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i) ⁻¹' s)))

Tactic:
.trans ?_
      ((Scheme.homeoOfIso (Y.affineCover.f i).isoOpensRange).image_eq_preimage_symm _)

Premises used: AlgebraicGeometry.Scheme.Hom.isoOpensRange, CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.homeoOfIso, Homeomorph.image_eq_preimage_symm, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst_1 : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X}
    (hs : IsLocallyConstructible s) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsLocallyConstructible (X := ↥Y) (⇑f '' s)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.I₀
inst_2 :
  LocallyOfFinitePresentation (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
inst :
  QuasiCompact (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
e_1 : (↑(↑(opensRange (Y.affineCover.f i)) : Set ↥Y) : Type u) = ↥(↑(opensRange (Y.affineCover.f i)) : Scheme)
h :
  Eq (α := Set (↑(↑(opensRange (Y.affineCover.f i)) : Set ↥Y) : Type u))
    (Subtype.val (p := fun (x : ↥Y) ↦ x ∈ (↑(opensRange (Y.affineCover.f i)) : Set ↥Y)) ⁻¹' ⇑f '' s)
    (Set.image (α := ↥(Y.affineCover.X i))
      (⇑(homeoOfIso (isoOpensRange (Y.affineCover.f i))) :
        (a : ↥(Y.affineCover.X i)) → ↥(↑(opensRange (Y.affineCover.f i)) : Scheme))
      (Set.image (α := ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i))
        (⇑(Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i))
        (⇑((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i) ⁻¹' s)))
⊢ Eq (α := Set (↑(↑(opensRange (Y.affineCover.f i)) : Set ↥Y) : Type u))
    (Subtype.val (p := fun (x : ↥Y) ↦ x ∈ (↑(opensRange (Y.affineCover.f i)) : Set ↥Y)) ⁻¹' ⇑f '' s)
    (Set.preimage (β := ↥(Y.affineCover.X i)) (⇑(Iso.inv (isoOpensRange (Y.affineCover.f i))))
      (Set.image (α := ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i))
        (⇑(Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i))
        (⇑((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i) ⁻¹' s)))

Tactic:
refine .trans ?_
      ((Scheme.homeoOfIso (Y.affineCover.f i).isoOpensRange).image_eq_preimage_symm _)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst_1 : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X}
    (hs : IsLocallyConstructible s) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsLocallyConstructible (X := ↥Y) (⇑f '' s)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.I₀
inst_2 :
  LocallyOfFinitePresentation (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
inst :
  QuasiCompact (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
e_1 : (↑(↑(opensRange (Y.affineCover.f i)) : Set ↥Y) : Type u) = ↥(↑(opensRange (Y.affineCover.f i)) : Scheme)
h :
  Eq (α := Set ↥Y)
    (Set.image (α := { x : ↥Y // x ∈ (↑(opensRange (Y.affineCover.f i)) : Set ↥Y) })
      (Subtype.val (p := fun (x : ↥Y) ↦ x ∈ (↑(opensRange (Y.affineCover.f i)) : Set ↥Y)))
      (Subtype.val (p := fun (x : ↥Y) ↦ x ∈ (↑(opensRange (Y.affineCover.f i)) : Set ↥Y)) ⁻¹' ⇑f '' s))
    (Set.image (α := { x : ↥Y // x ∈ (↑(opensRange (Y.affineCover.f i)) : Set ↥Y) })
      (Subtype.val (p := fun (x : ↥Y) ↦ x ∈ (↑(opensRange (Y.affineCover.f i)) : Set ↥Y)))
      (Set.image (α := ↥(Y.affineCover.X i))
        (⇑(homeoOfIso (isoOpensRange (Y.affineCover.f i))) :
          (a : ↥(Y.affineCover.X i)) → ↥(↑(opensRange (Y.affineCover.f i)) : Scheme))
        (Set.image (α := ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i))
          (⇑(Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i))
          (⇑((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i) ⁻¹' s))))
⊢ Eq (α := Set (↑(↑(opensRange (Y.affineCover.f i)) : Set ↥Y) : Type u))
    (Subtype.val (p := fun (x : ↥Y) ↦ x ∈ (↑(opensRange (Y.affineCover.f i)) : Set ↥Y)) ⁻¹' ⇑f '' s)
    (Set.image (α := ↥(Y.affineCover.X i))
      (⇑(homeoOfIso (isoOpensRange (Y.affineCover.f i))) :
        (a : ↥(Y.affineCover.X i)) → ↥(↑(opensRange (Y.affineCover.f i)) : Scheme))
      (Set.image (α := ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i))
        (⇑(Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i))
        (⇑((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i) ⁻¹' s)))

Tactic:
apply Set.image_injective.mpr Subtype.val_injective

Premises used: Iff.mpr, Set.image_injective, Subtype.val_injective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst_1 : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X}
    (hs : IsLocallyConstructible s) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsLocallyConstructible (X := ↥Y) (⇑f '' s)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.I₀
inst_2 :
  LocallyOfFinitePresentation (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
inst :
  QuasiCompact (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
e_1 : (↑(↑(opensRange (Y.affineCover.f i)) : Set ↥Y) : Type u) = ↥(↑(opensRange (Y.affineCover.f i)) : Scheme)
h :
  ⇑f '' s ∩ (↑(opensRange (Y.affineCover.f i)) : Set ↥Y) =
    Set.image (α := ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i))
      (Function.comp (β := ↥(Y.affineCover.X i))
        (Function.comp (β := { x : ↥Y // x ∈ (↑(opensRange (Y.affineCover.f i)) : Set ↥Y) })
          (Subtype.val (p := fun (x : ↥Y) ↦ x ∈ (↑(opensRange (Y.affineCover.f i)) : Set ↥Y)))
          (⇑(homeoOfIso (isoOpensRange (Y.affineCover.f i))) :
            (a : ↥(Y.affineCover.X i)) → ↥(↑(opensRange (Y.affineCover.f i)) : Scheme)))
        ⇑(Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i))
      (⇑((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i) ⁻¹' s)
⊢ Eq (α := Set ↥Y)
    (Set.image (α := { x : ↥Y // x ∈ (↑(opensRange (Y.affineCover.f i)) : Set ↥Y) })
      (Subtype.val (p := fun (x : ↥Y) ↦ x ∈ (↑(opensRange (Y.affineCover.f i)) : Set ↥Y)))
      (Subtype.val (p := fun (x : ↥Y) ↦ x ∈ (↑(opensRange (Y.affineCover.f i)) : Set ↥Y)) ⁻¹' ⇑f '' s))
    (Set.image (α := { x : ↥Y // x ∈ (↑(opensRange (Y.affineCover.f i)) : Set ↥Y) })
      (Subtype.val (p := fun (x : ↥Y) ↦ x ∈ (↑(opensRange (Y.affineCover.f i)) : Set ↥Y)))
      (Set.image (α := ↥(Y.affineCover.X i))
        (⇑(homeoOfIso (isoOpensRange (Y.affineCover.f i))) :
          (a : ↥(Y.affineCover.X i)) → ↥(↑(opensRange (Y.affineCover.f i)) : Scheme))
        (Set.image (α := ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i))
          (⇑(Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i))
          (⇑((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i) ⁻¹' s))))

Tactic:
rw [Set.image_preimage_eq_inter_range, ← Set.image_comp, ← Set.image_comp,
      Subtype.range_coe_subtype, Set.setOf_mem_eq]

Premises used: Subtype.range_coe_subtype, Set.image_preimage_eq_inter_range, Set.setOf_mem_eq, Set.image_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst_1 : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X}
    (hs : IsLocallyConstructible s) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsLocallyConstructible (X := ↥Y) (⇑f '' s)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.I₀
inst_2 :
  LocallyOfFinitePresentation (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
inst :
  QuasiCompact (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
e_1 : (↑(↑(opensRange (Y.affineCover.f i)) : Set ↥Y) : Type u) = ↥(↑(opensRange (Y.affineCover.f i)) : Scheme)
h :
  ⇑f '' s ∩ (↑(opensRange (Y.affineCover.f i)) : Set ↥Y) =
    (⇑(TopCat.Hom.hom f.base) : (a : ↥X) → ↥Y) ''
      (s ∩
        Set.range (ι := ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i))
          (⇑(TopCat.Hom.hom ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i).base) :
            (a : ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)) → ↥X))
⊢ ⇑f '' s ∩ (↑(opensRange (Y.affineCover.f i)) : Set ↥Y) =
    Set.image (α := ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i))
      (⇑(TopCat.Hom.hom
              (PresheafedSpace.Hom.base
                (LocallyRingedSpace.Hom.toHom
                  (toLRSHom'
                    (Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i ≫
                      Iso.hom (isoOpensRange (Y.affineCover.f i)) ≫ (opensRange (Y.affineCover.f i)).ι)))) :
            C(↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i), ↥Y)) :
        (a : ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)) → ↥Y)
      (⇑((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i) ⁻¹' s)

Tactic:
rw [Scheme.Hom.isoOpensRange_hom_ι, Cover.pullbackHom_map, Scheme.Hom.comp_base,
      TopCat.hom_comp, ContinuousMap.coe_comp, Set.image_comp, Set.image_preimage_eq_inter_range]

Premises used: ContinuousMap.coe_comp, AlgebraicGeometry.Scheme.Hom.isoOpensRange_hom_ι, Set.image_preimage_eq_inter_range, Set.image_comp, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.hom_comp, AlgebraicGeometry.Scheme.Cover.pullbackHom_map