awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
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))
⊢ 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.base).comp (TopCat.Hom.hom (𝒰.f i).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))
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))
⊢ 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))
    (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))
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))
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))
⊢ 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) (⇑(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)))
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))
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)))
⊢ 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)))
  ((⇑(TopCat.Hom.hom f.base) : (a : ↥X) → ↥(Spec R)) ''
    (s ∩ Set.range (ι := ↥(𝒰.X i)) (⇑(TopCat.Hom.hom (𝒰.f i).base) : (a : ↥(𝒰.X i)) → ↥X)))
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 : QuasiCompact f
hX : ∃ (S : CommRingCat.{u}), X = Spec S
⊢ IsLocallyConstructible (X := ↥(Spec R)) (⇑f '' s)
have obtain : ∀ (S : CommRingCat.{u}) {s : Set ↥(Spec S)} (hs : IsLocallyConstructible s) (f : Spec S ⟶ Spec R)
  [hf : LocallyOfFinitePresentation f] [QuasiCompact f], IsLocallyConstructible (X := ↥(Spec R)) (⇑f '' s)
Tactic: obtain ⟨S, rfl⟩ := hX
Cleared hypotheses: X, s, hs, f, hf, inst, hX
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation (goal)
Goal:
R S : CommRingCat
s : Set ↥(Spec S)
hs : IsLocallyConstructible s
f : Spec S ⟶ Spec R
hf : LocallyOfFinitePresentation f
inst : QuasiCompact f
⊢ IsLocallyConstructible (X := ↥(Spec R)) (⇑f '' s)
have obtain : ∀ (φ : R ⟶ S) [hf : LocallyOfFinitePresentation (Spec.map φ)] [QuasiCompact (Spec.map φ)],
  IsLocallyConstructible (X := ↥(Spec R)) (⇑(Spec.map φ) '' s)
Tactic: obtain ⟨φ, rfl⟩ := Spec.map_surjective f
Cleared hypotheses: f, hf, inst
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation (hypothesis)
Goal:
R S : CommRingCat
s : Set ↥(Spec S)
hs : IsLocallyConstructible s
φ : R ⟶ S
hf : LocallyOfFinitePresentation (Spec.map φ)
inst : QuasiCompact (Spec.map φ)
⊢ IsLocallyConstructible (X := ↥(Spec R)) (⇑(Spec.map φ) '' s)
have hf₁ : (CommRingCat.Hom.hom φ).FinitePresentation
Tactic: rw [HasRingHomProperty.Spec_iff (P := @LocallyOfFinitePresentation)] at hf
Cleared hypotheses: hf, inst
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ @LocallyOfFiniteType = affineLocally fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.FiniteType
have h : ∀ ⦃X Y : Scheme.{u_1}⦄ (f : X ⟶ Y),
  LocallyOfFiniteType f ↔ affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.FiniteType) f
Tactic: ext X Y f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
⊢ LocallyOfFiniteType f ↔ affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.FiniteType) f
have h : (∀ {U : Y.Opens},
    IsAffineOpen U →
      ∀ {V : X.Opens},
        IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).FiniteType) ↔
  affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.FiniteType) f
Tactic: rw [locallyOfFiniteType_iff, affineLocally_iff_forall_isAffineOpen]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
h :
  (∀ {U : Y.Opens},
      IsAffineOpen U →
        ∀ {V : X.Opens},
          IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).FiniteType) ↔
    affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.FiniteType) f
⊢ LocallyOfFiniteType f ↔ affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.FiniteType) f
have h₁ : (∀ {U : Y.Opens},
    IsAffineOpen U →
      ∀ {V : X.Opens},
        IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).FiniteType) ↔
  ∀ {U : Y.Opens},
    IsAffineOpen U →
      ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).FiniteType
Tactic: rw [locallyOfFiniteType_iff, affineLocally_iff_forall_isAffineOpen]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
inst_1 : JacobsonSpace.{u} ↥Y
⊢ JacobsonSpace.{u} ↥X
have inr : ∀
  (this :
    ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] [JacobsonSpace.{u} ↥Y]
      (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), JacobsonSpace.{u} ↥X)
  (hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S), JacobsonSpace.{u} ↥X
Tactic: wlog hY : ∃ S, Y = Spec S
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
inst_1 : JacobsonSpace.{u} ↥Y
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] [JacobsonSpace.{u} ↥Y]
        (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), JacobsonSpace.{u} ↥X)
    (hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S), JacobsonSpace.{u} ↥X
⊢ JacobsonSpace.{u} ↥X
have wlog : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] [JacobsonSpace.{u} ↥Y]
  (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), JacobsonSpace.{u} ↥X
Tactic: wlog hY : ∃ S, Y = Spec S
Cleared hypotheses: X, Y, f, inst, inst_1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
inst_1 : JacobsonSpace.{u} ↥Y
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] [JacobsonSpace.{u} ↥Y]
    (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), JacobsonSpace.{u} ↥X
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
⊢ JacobsonSpace.{u} ↥X
have inr : ∀ (i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀),
  JacobsonSpace.{u} ↥(Scheme.Hom.opensRange ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i))
Tactic: rw [(Scheme.OpenCover.isOpenCover_opensRange (Y.affineCover.pullback₁ f)).jacobsonSpace_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
inst_1 : JacobsonSpace.{u} ↥Y
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] [JacobsonSpace.{u} ↥Y]
    (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), JacobsonSpace.{u} ↥X
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
⊢ JacobsonSpace.{u} ↥(Scheme.Hom.opensRange ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i))
have inst : LocallyOfFiniteType (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
  (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
    (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
Tactic: have inst : LocallyOfFiniteType (Y.affineCover.pullbackHom f i) :=
      MorphismProperty.pullback_snd _ _ inferInstance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : LocallyOfFiniteType f
inst_2 : JacobsonSpace.{u} ↥Y
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] [JacobsonSpace.{u} ↥Y]
    (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), JacobsonSpace.{u} ↥X
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
inst_3 :
  LocallyOfFiniteType (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
inst : JacobsonSpace.{u} ↥Y
⊢ JacobsonSpace.{u} ↥(Scheme.Hom.opensRange ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i))
have inst₁ : JacobsonSpace.{u} ↥(Y.affineCover.X i)
Tactic: have inst : JacobsonSpace (Y.affineCover.X i) :=
      .of_isOpenEmbedding (Y.affineCover.f i).isOpenEmbedding
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : LocallyOfFiniteType f
inst_2 : JacobsonSpace.{u} ↥Y
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] [JacobsonSpace.{u} ↥Y]
    (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), JacobsonSpace.{u} ↥X
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
inst_3 :
  LocallyOfFiniteType (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
inst_4 : JacobsonSpace.{u} ↥Y
inst : JacobsonSpace.{u} ↥(Y.affineCover.X i)
e : ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i) ≃ₜ
  (↑(Set.range (ι := ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i))
        ⇑((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i)) :
    Type u) :=
  ⋯.toHomeomorph
⊢ JacobsonSpace.{u} ↥(Scheme.Hom.opensRange ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i))
have this₁ : JacobsonSpace.{u} ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
Tactic: have := this (Y.affineCover.pullbackHom f i) ⟨_, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
inst_1 : JacobsonSpace.{u} ↥Y
hY : ∃ (S : CommRingCat.{u}), Y = Spec S
⊢ JacobsonSpace.{u} ↥X
have obtain : ∀ (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyOfFiniteType f] [JacobsonSpace.{u} ↥(Spec R)], JacobsonSpace.{u} ↥X
Tactic: obtain ⟨R, rfl⟩ := hY
Cleared hypotheses: Y, f, inst, inst_1, hY
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (goal)
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFiniteType f
inst_1 : JacobsonSpace.{u} ↥(Spec R)
⊢ JacobsonSpace.{u} ↥X
have inr : ∀
  (this :
    ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyOfFiniteType f] [JacobsonSpace.{u} ↥(Spec R)]
      (hX : ∃ (S : CommRingCat.{u}), X = Spec S), JacobsonSpace.{u} ↥X)
  (hX : ¬∃ (S : CommRingCat.{u}), X = Spec S), JacobsonSpace.{u} ↥X
Tactic: wlog hX : ∃ S, X = Spec S
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (goal)
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFiniteType f
inst_1 : JacobsonSpace.{u} ↥(Spec R)
inr :
  ∀
    (this :
      ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyOfFiniteType f] [JacobsonSpace.{u} ↥(Spec R)]
        (hX : ∃ (S : CommRingCat.{u}), X = Spec S), JacobsonSpace.{u} ↥X)
    (hX : ¬∃ (S : CommRingCat.{u}), X = Spec S), JacobsonSpace.{u} ↥X
⊢ JacobsonSpace.{u} ↥X
have wlog : ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyOfFiniteType f] [JacobsonSpace.{u} ↥(Spec R)]
  (hX : ∃ (S : CommRingCat.{u}), X = Spec S), JacobsonSpace.{u} ↥X
Tactic: wlog hX : ∃ S, X = Spec S
Cleared hypotheses: X, R, f, inst, inst_1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (goal)
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst_1 : LocallyOfFiniteType f
inst_2 : JacobsonSpace.{u} ↥(Spec R)
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyOfFiniteType f] [JacobsonSpace.{u} ↥(Spec R)]
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), JacobsonSpace.{u} ↥X
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
inst : JacobsonSpace.{u} ↥(Spec R)
⊢ JacobsonSpace.{u} ↥X
have inr : ∀ (i : X.affineCover.I₀), JacobsonSpace.{u} ↥(Scheme.Hom.opensRange (X.affineCover.f i))
Tactic: rw [X.affineCover.isOpenCover_opensRange.jacobsonSpace_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (hypothesis)
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst_1 : LocallyOfFiniteType f
inst_2 : JacobsonSpace.{u} ↥(Spec R)
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyOfFiniteType f] [JacobsonSpace.{u} ↥(Spec R)]
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), JacobsonSpace.{u} ↥X
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
inst : JacobsonSpace.{u} ↥(Spec R)
i : X.affineCover.I₀
⊢ JacobsonSpace.{u} ↥(Scheme.Hom.opensRange (X.affineCover.f i))
have this₁ : JacobsonSpace.{u} ↥(X.affineCover.X i)
Tactic: have := this _ (X.affineCover.f i ≫ f) ⟨_, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (goal)
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFiniteType f
inst_1 : JacobsonSpace.{u} ↥(Spec R)
hX : ∃ (S : CommRingCat.{u}), X = Spec S
⊢ JacobsonSpace.{u} ↥X
have obtain : ∀ (S : CommRingCat.{u}) (f : Spec S ⟶ Spec R) [LocallyOfFiniteType f], JacobsonSpace.{u} ↥(Spec S)
Tactic: obtain ⟨S, rfl⟩ := hX
Cleared hypotheses: X, f, inst, hX
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (goal)
Goal:
R : CommRingCat
inst : JacobsonSpace.{u} ↥(Spec R)
S : CommRingCat
f : Spec S ⟶ Spec R
inst_1 : LocallyOfFiniteType f
⊢ JacobsonSpace.{u} ↥(Spec S)
have obtain : ∀ (φ : R ⟶ S) [LocallyOfFiniteType (Spec.map φ)], JacobsonSpace.{u} ↥(Spec S)
Tactic: obtain ⟨φ, rfl : Spec.map φ = f⟩ := Spec.homEquiv.symm.surjective f
Cleared hypotheses: f, inst_1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (hypothesis)
Goal:
R : CommRingCat
inst : JacobsonSpace.{u} ↥(Spec R)
S : CommRingCat
φ : R ⟶ S
inst_1 : LocallyOfFiniteType (Spec.map φ)
⊢ JacobsonSpace.{u} ↥(Spec S)
have this : (CommRingCat.Hom.hom φ).FiniteType
Tactic: have : RingHom.FiniteType φ.hom := HasRingHomProperty.Spec_iff.mp ‹_›
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (hypothesis)
Goal:
R : CommRingCat
inst : JacobsonSpace.{u} ↥(Spec R)
S : CommRingCat
φ : R ⟶ S
inst_1 : LocallyOfFiniteType (Spec.map φ)
this : (CommRingCat.Hom.hom φ).FiniteType
⊢ JacobsonSpace.{u} ↥(Spec S)
have algebraizeInst : Algebra.FiniteType.{u, u} (↑R : Type u) (↑S : Type u)
Tactic: algebraize [φ.hom]