awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation (goal)
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)) : Set ↥Y) : Type u))
    (Subtype.val (p := fun (x : ↥Y) ↦ x ∈ (↑(opensRange (Y.affineCover.f i)) : Set ↥Y)) ⁻¹' ⇑f '' s)
have 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)))
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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation (goal)
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)))
have 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)))
Tactic: refine .trans ?_
      ((Scheme.homeoOfIso (Y.affineCover.f i).isoOpensRange).image_eq_preimage_symm _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation (goal)
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.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)))
have 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))))
Tactic: apply Set.image_injective.mpr Subtype.val_injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation (goal)
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 ↥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))))
have 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)
Tactic: rw [Set.image_preimage_eq_inter_range, ← Set.image_comp, ← Set.image_comp,
      Subtype.range_coe_subtype, Set.setOf_mem_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation (goal)
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)
⊢ ⇑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)
have 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))
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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
hY : ∃ (R : CommRingCat.{u}), Y = Spec R
⊢ IsLocallyConstructible (X := ↥Y) (⇑f '' s)
have obtain : ∀ (R : CommRingCat.{u}) (f : X ⟶ Spec R) [hf : LocallyOfFinitePresentation f] [QuasiCompact f],
  IsLocallyConstructible (X := ↥(Spec R)) (⇑f '' s)
Tactic: obtain ⟨R, rfl⟩ := hY
Cleared hypotheses: Y, f, hf, inst, hY
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation (goal)
Goal:
X : Scheme
s : Set ↥X
hs : IsLocallyConstructible s
R : CommRingCat
f : X ⟶ Spec R
hf : LocallyOfFinitePresentation f
inst : QuasiCompact f
⊢ IsLocallyConstructible (X := ↥(Spec R)) (⇑f '' s)
have inr : ∀
  (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), IsLocallyConstructible (X := ↥(Spec R)) (⇑f '' s)
Tactic: wlog hX : ∃ S, X = Spec S
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation (goal)
Goal:
X : Scheme
s : Set ↥X
hs : IsLocallyConstructible s
R : CommRingCat
f : X ⟶ Spec R
hf : LocallyOfFinitePresentation f
inst : QuasiCompact f
inr :
  ∀
    (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), IsLocallyConstructible (X := ↥(Spec R)) (⇑f '' s)
⊢ IsLocallyConstructible (X := ↥(Spec R)) (⇑f '' s)
have wlog : ∀ {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)
Tactic: wlog hX : ∃ S, X = Spec S
Cleared hypotheses: X, s, hs, R, f, hf, inst
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation (hypothesis)
Goal:
X : Scheme
s : Set ↥X
hs : IsLocallyConstructible s
R : CommRingCat
f : X ⟶ Spec R
hf : LocallyOfFinitePresentation f
inst : 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
⊢ IsLocallyConstructible (X := ↥(Spec R)) (⇑f '' s)
have inst : CompactSpace.{u} ↥X
Tactic: have inst : CompactSpace X := HasAffineProperty.iff_of_isAffine.mp ‹QuasiCompact f›
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation (goal)
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 : CompactSpace.{u} ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
⊢ IsLocallyConstructible (X := ↥(Spec R)) (⇑f '' s)
have inr : IsLocallyConstructible.{u} (X := ↥(Spec R)) (⋃ (i : 𝒰.I₀), ⇑f '' (s ∩ (↑(opensRange (𝒰.f i)) : Set ↥X)))
Tactic: rw [← 𝒰.isOpenCover_opensRange.iUnion_inter s, Set.image_iUnion]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation (goal)
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 : CompactSpace.{u} ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
⊢ IsLocallyConstructible.{u} (X := ↥(Spec R)) (⋃ (i : 𝒰.I₀), ⇑f '' (s ∩ (↑(opensRange (𝒰.f i)) : Set ↥X)))
have inr : ∀ (i : 𝒰.I₀), IsLocallyConstructible (X := ↥(Spec R)) (⇑f '' (s ∩ (↑(opensRange (𝒰.f i)) : Set ↥X)))
Tactic: refine .iUnion fun i ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation (hypothesis)
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 : CompactSpace.{u} ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
i : 𝒰.I₀
⊢ IsLocallyConstructible (X := ↥(Spec R)) (⇑f '' (s ∩ (↑(opensRange (𝒰.f i)) : Set ↥X)))
have inst₁ : QuasiCompact (𝒰.f i ≫ f)
Tactic: have inst : QuasiCompact (𝒰.f i ≫ f) :=
      HasAffineProperty.iff_of_isAffine.mpr (inferInstanceAs (CompactSpace (Spec _)))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation (goal)
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)
⊢ IsLocallyConstructible (X := ↥(Spec R)) (⇑f '' (s ∩ (↑(opensRange (𝒰.f i)) : Set ↥X)))
have h : Eq (α := Set ↥(Spec R)) (⇑f '' (s ∩ (↑(opensRange (𝒰.f i)) : Set ↥X)))
  (Set.image (α := ↥(𝒰.X i)) (⇑(𝒰.f i ≫ f)) (⇑(𝒰.f i) ⁻¹' s))
Tactic: convert! this (hs.preimage_of_isOpenEmbedding (𝒰.f i).isOpenEmbedding) _ (𝒰.f i ≫ f) ⟨_, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation (goal)
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)
⊢ Eq (α := Set ↥(Spec R)) (⇑f '' (s ∩ (↑(opensRange (𝒰.f i)) : Set ↥X)))
    (Set.image (α := ↥(𝒰.X i)) (⇑(𝒰.f i ≫ f)) (⇑(𝒰.f i) ⁻¹' s))
have 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))
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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation (goal)
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))
⊢ Eq (α := Set ↥(Spec R)) (⇑f '' (s ∩ (↑(opensRange (𝒰.f i)) : Set ↥X)))
    (Set.image (α := ↥(𝒰.X i)) (⇑(𝒰.f i ≫ f)) (⇑(𝒰.f i) ⁻¹' s))
have 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))
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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation (goal)
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))
⊢ Eq (α := Set ↥(Spec R)) (⇑f '' (s ∩ (↑(opensRange (𝒰.f i)) : Set ↥X)))
    (Set.image (α := ↥(𝒰.X i)) (⇑(𝒰.f i ≫ f)) (⇑(𝒰.f i) ⁻¹' s))
have 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))
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]