awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
R S : CommRingCat
φ : R ⟶ S
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField (Spec.map φ) x)
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
x : ↥(Spec R)
hP : x.asIdeal.IsPrime
refine_1 : Spec.map φ ≫ 𝟙 (Spec R) = 𝟙 (Spec S) ≫ Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))
⊢ (Arrow.mk (Hom.fiberToSpecResidueField (Spec.map φ) x)).left ≅
    (Arrow.mk (X := Spec (CommRingCat.of (x.asIdeal.Fiber (↑S : Type u)))) (Y :=
        Spec (CommRingCat.of x.asIdeal.ResidueField))
        (Spec.map (CommRingCat.ofHom (algebraMap x.asIdeal.ResidueField (x.asIdeal.Fiber (↑S : Type u)))))).left
have refine_1₁ : (Spec R).fromSpecResidueField x ≫ 𝟙 (Spec R) =
  Spec.map (Spec.residueFieldIso R x).inv ≫
    Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) x.asIdeal.ResidueField))
Tactic: refine asIso (pullback.map _ _ _ _ (𝟙 _) (Spec.map (Spec.residueFieldIso _ x).inv) (𝟙 _)
      ?_ ?_) ≪≫ pullbackSymmetry _ _ ≪≫ pullbackSpecIso ..
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
R S : CommRingCat
φ : R ⟶ S
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField (Spec.map φ) x)
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
x : ↥(Spec R)
hP : x.asIdeal.IsPrime
⊢ Spec.map φ ≫ 𝟙 (Spec R) = 𝟙 (Spec S) ≫ Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))
have refine_1 : Spec.map φ = Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))
Tactic: simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsPreimmersion f
⊢ LocallyQuasiFinite f
have refine : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
Tactic: refine .of_fiberToSpecResidueField _ fun x ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsPreimmersion f
x : ↥Y
⊢ LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
have this : IsClosedImmersion (Hom.fiberToSpecResidueField f x)
Tactic: have : IsClosedImmersion (f.fiberToSpecResidueField x) :=
    .of_isPreimmersion (pullback.snd _ _) (isClosed_discrete _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
⊢ LocallyQuasiFinite f ↔ ∀ (x : ↥Y), IsDiscrete (X := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})
have refine : ∀ (H : ∀ (x : ↥Y), IsDiscrete (X := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})), LocallyQuasiFinite f
Tactic: refine ⟨fun _ ↦ f.isDiscrete_preimage_singleton, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
H : ∀ (x : ↥Y), IsDiscrete (X := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})
⊢ id (LocallyQuasiFinite f)
have inr : ∀
  (this :
    ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} [LocallyOfFiniteType f]
      (H : ∀ (x : ↥Y), IsDiscrete (X := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
      id (LocallyQuasiFinite f))
  (hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R), id (LocallyQuasiFinite f)
Tactic: wlog hY : ∃ R, Y = Spec R
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
H : ∀ (x : ↥Y), IsDiscrete (X := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} [LocallyOfFiniteType f]
        (H : ∀ (x : ↥Y), IsDiscrete (X := ↥X) (Set.preimage (β := ↥Y) ⇑f {x}))
        (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), id (LocallyQuasiFinite f))
    (hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R), id (LocallyQuasiFinite f)
⊢ id (LocallyQuasiFinite f)
have wlog : ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} [LocallyOfFiniteType f]
  (H : ∀ (x : ↥Y), IsDiscrete (X := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
  id (LocallyQuasiFinite f)
Tactic: wlog hY : ∃ R, Y = Spec R
Cleared hypotheses: X, Y, f, inst, H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
H : ∀ (x : ↥Y), IsDiscrete (X := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} [LocallyOfFiniteType f]
    (H : ∀ (x : ↥Y), IsDiscrete (X := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    id (LocallyQuasiFinite f)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
⊢ id (LocallyQuasiFinite f)
have inr : ∀ (i : Y.affineCover.toPreZeroHypercover.1) (x : ↥(Y.affineCover.X i)),
  IsDiscrete (X := ↥(pullback f (Y.affineCover.f i)))
    (Set.preimage (β := ↥(Y.affineCover.X i)) ⇑(pullback.snd f (Y.affineCover.f i)) {x})
Tactic: refine (IsZariskiLocalAtTarget.iff_of_openCover Y.affineCover).mpr fun i ↦
      this (f := pullback.snd _ _) (fun x ↦ ?_) ⟨_, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
H : ∀ (x : ↥Y), IsDiscrete (X := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} [LocallyOfFiniteType f]
    (H : ∀ (x : ↥Y), IsDiscrete (X := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    id (LocallyQuasiFinite f)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
x : ↥(Y.affineCover.X i)
⊢ IsDiscrete (X := ↥(pullback f (Y.affineCover.f i)))
    (Set.preimage (β := ↥(Y.affineCover.X i)) ⇑(pullback.snd f (Y.affineCover.f i)) {x})
have h : Eq (α := Set ↥(pullback f (Y.affineCover.f i)))
  (Set.preimage (β := ↥(Y.affineCover.X i)) ⇑(pullback.snd f (Y.affineCover.f i)) {x})
  (Set.preimage (β := ↥X) (⇑(pullback.fst f (Y.affineCover.f i)))
    (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) ((Y.affineCover.f i) x : ↥Y))))
Tactic: convert!
      (H (Y.affineCover.f i x)).preimage ((pullback.fst f _).continuous.continuousOn)
        (pullback.fst f (Y.affineCover.f i)).isOpenEmbedding.injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
H : ∀ (x : ↥Y), IsDiscrete (X := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} [LocallyOfFiniteType f]
    (H : ∀ (x : ↥Y), IsDiscrete (X := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    id (LocallyQuasiFinite f)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
x : ↥(Y.affineCover.X i)
⊢ Eq (α := Set ↥(pullback f (Y.affineCover.f i)))
    (Set.preimage (β := ↥(Y.affineCover.X i)) ⇑(pullback.snd f (Y.affineCover.f i)) {x})
    (Set.preimage (β := ↥X) (⇑(pullback.fst f (Y.affineCover.f i)))
      (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) ((Y.affineCover.f i) x : ↥Y))))
have h : ∀ (x_1 : ↥(pullback f (Y.affineCover.f i))),
  Membership.mem (γ := Set ↥(pullback f (Y.affineCover.f i)))
      (Set.preimage (β := ↥(Y.affineCover.X i)) ⇑(pullback.snd f (Y.affineCover.f i)) {x}) x_1 ↔
    Membership.mem (γ := Set ↥(pullback f (Y.affineCover.f i)))
      (Set.preimage (β := ↥X) (⇑(pullback.fst f (Y.affineCover.f i)))
        (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) ((Y.affineCover.f i) x : ↥Y))))
      x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
H : ∀ (x : ↥Y), IsDiscrete (X := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})
hY : ∃ (R : CommRingCat.{u}), Y = Spec R
⊢ id (LocallyQuasiFinite f)
have obtain : ∀ (R : CommRingCat.{u}) {f : X ⟶ Spec R} [LocallyOfFiniteType f]
  (H : ∀ (x : ↥(Spec R)), IsDiscrete (X := ↥X) (Set.preimage (β := ↥(Spec R)) ⇑f {x})), id (LocallyQuasiFinite f)
Tactic: obtain ⟨R, rfl⟩ := hY
Cleared hypotheses: Y, f, inst, H, hY
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFiniteType f
H : ∀ (x : ↥(Spec R)), IsDiscrete (X := ↥X) (Set.preimage (β := ↥(Spec R)) ⇑f {x})
⊢ id (LocallyQuasiFinite f)
have inr : ∀
  (this :
    ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) {f : X ⟶ Spec R} [LocallyOfFiniteType f]
      (H : ∀ (x : ↥(Spec R)), IsDiscrete (X := ↥X) (Set.preimage (β := ↥(Spec R)) ⇑f {x}))
      (hX : ∃ (S : CommRingCat.{u}), X = Spec S), id (LocallyQuasiFinite f))
  (hX : ¬∃ (S : CommRingCat.{u}), X = Spec S), id (LocallyQuasiFinite f)
Tactic: wlog hX : ∃ S, X = Spec S
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFiniteType f
H : ∀ (x : ↥(Spec R)), IsDiscrete (X := ↥X) (Set.preimage (β := ↥(Spec R)) ⇑f {x})
inr :
  ∀
    (this :
      ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) {f : X ⟶ Spec R} [LocallyOfFiniteType f]
        (H : ∀ (x : ↥(Spec R)), IsDiscrete (X := ↥X) (Set.preimage (β := ↥(Spec R)) ⇑f {x}))
        (hX : ∃ (S : CommRingCat.{u}), X = Spec S), id (LocallyQuasiFinite f))
    (hX : ¬∃ (S : CommRingCat.{u}), X = Spec S), id (LocallyQuasiFinite f)
⊢ id (LocallyQuasiFinite f)
have wlog : ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) {f : X ⟶ Spec R} [LocallyOfFiniteType f]
  (H : ∀ (x : ↥(Spec R)), IsDiscrete (X := ↥X) (Set.preimage (β := ↥(Spec R)) ⇑f {x}))
  (hX : ∃ (S : CommRingCat.{u}), X = Spec S), id (LocallyQuasiFinite f)
Tactic: wlog hX : ∃ S, X = Spec S
Cleared hypotheses: X, R, f, inst, H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFiniteType f
H : ∀ (x : ↥(Spec R)), IsDiscrete (X := ↥X) (Set.preimage (β := ↥(Spec R)) ⇑f {x})
hX : ∃ (S : CommRingCat.{u}), X = Spec S
⊢ id (LocallyQuasiFinite f)
have obtain : ∀ (S : CommRingCat.{u}) {f : Spec S ⟶ Spec R} [LocallyOfFiniteType f]
  (H : ∀ (x : ↥(Spec R)), IsDiscrete (X := ↥(Spec S)) (Set.preimage (β := ↥(Spec R)) ⇑f {x})), id (LocallyQuasiFinite f)
Tactic: obtain ⟨S, rfl⟩ := hX
Cleared hypotheses: X, f, inst, H, hX
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
R S : CommRingCat
f : Spec S ⟶ Spec R
inst : LocallyOfFiniteType f
H : ∀ (x : ↥(Spec R)), IsDiscrete (X := ↥(Spec S)) (Set.preimage (β := ↥(Spec R)) ⇑f {x})
⊢ id (LocallyQuasiFinite f)
have obtain : ∀ (φ : R ⟶ S) [LocallyOfFiniteType (Spec.map φ)]
  (H : ∀ (x : ↥(Spec R)), IsDiscrete (X := ↥(Spec S)) (Set.preimage (β := ↥(Spec R)) ⇑(Spec.map φ) {x})),
  id (LocallyQuasiFinite (Spec.map φ))
Tactic: obtain ⟨φ, rfl⟩ := Spec.map_surjective f
Cleared hypotheses: f, inst, H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
R S : CommRingCat
φ : R ⟶ S
inst : LocallyOfFiniteType (Spec.map φ)
H : ∀ (x : ↥(Spec R)), IsDiscrete (X := ↥(Spec S)) (Set.preimage (β := ↥(Spec R)) ⇑(Spec.map φ) {x})
⊢ id (LocallyQuasiFinite (Spec.map φ))
have simp : (CommRingCat.Hom.hom φ).FiniteType → (CommRingCat.Hom.hom φ).QuasiFinite
Tactic: simp only [HasRingHomProperty.Spec_iff, id_eq] at *
Cleared hypotheses: inst
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (hypothesis)
Goal:
R S : CommRingCat
φ : R ⟶ S
H : ∀ (x : ↥(Spec R)), IsDiscrete (X := ↥(Spec S)) (Set.preimage (β := ↥(Spec R)) ⇑(Spec.map φ) {x})
inst : (CommRingCat.Hom.hom φ).FiniteType
⊢ (CommRingCat.Hom.hom φ).QuasiFinite
have algebraizeInst : Algebra.FiniteType.{u, u} (↑R : Type u) (↑S : Type u)
Tactic: algebraize [φ.hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
hf : ∀ (x : ↥Y), Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})
⊢ id (LocallyQuasiFinite f)
have inr : ∀
  (this :
    ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f]
      (hf : ∀ (x : ↥Y), Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {x}))
      (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), id (LocallyQuasiFinite f))
  (hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R), id (LocallyQuasiFinite f)
Tactic: wlog hY : ∃ R, Y = Spec R
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
hf : ∀ (x : ↥Y), Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f]
        (hf : ∀ (x : ↥Y), Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {x}))
        (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), id (LocallyQuasiFinite f))
    (hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R), id (LocallyQuasiFinite f)
⊢ id (LocallyQuasiFinite f)
have wlog : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f]
  (hf : ∀ (x : ↥Y), Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
  id (LocallyQuasiFinite f)
Tactic: wlog hY : ∃ R, Y = Spec R
Cleared hypotheses: X, Y, f, inst, hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
hf : ∀ (x : ↥Y), Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f]
    (hf : ∀ (x : ↥Y), Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    id (LocallyQuasiFinite f)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
⊢ id (LocallyQuasiFinite f)
have inr : ∀ (i : Y.affineCover.toPreZeroHypercover.1) (x : ↥(Y.affineCover.X i)),
  Set.Finite (α := ↥(pullback f (Y.affineCover.f i)))
    (Set.preimage (β := ↥(Y.affineCover.X i)) ⇑(pullback.snd f (Y.affineCover.f i)) {x})
Tactic: refine (IsZariskiLocalAtTarget.iff_of_openCover Y.affineCover).mpr fun i ↦
      this (f := pullback.snd _ _) (fun x ↦ ?_) ⟨_, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
hf : ∀ (x : ↥Y), Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f]
    (hf : ∀ (x : ↥Y), Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    id (LocallyQuasiFinite f)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
x : ↥(Y.affineCover.X i)
⊢ Set.Finite (α := ↥(pullback f (Y.affineCover.f i)))
    (Set.preimage (β := ↥(Y.affineCover.X i)) ⇑(pullback.snd f (Y.affineCover.f i)) {x})
have h : Eq (α := Set ↥(pullback f (Y.affineCover.f i)))
  (Set.preimage (β := ↥(Y.affineCover.X i)) ⇑(pullback.snd f (Y.affineCover.f i)) {x})
  (Set.preimage (β := ↥X) (⇑(pullback.fst f (Y.affineCover.f i)))
    (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) ((Y.affineCover.f i) x : ↥Y))))
Tactic: convert!
      (hf (Y.affineCover.f i x)).preimage
        (pullback.fst f (Y.affineCover.f i)).isOpenEmbedding.injective.injOn
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
hf : ∀ (x : ↥Y), Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f]
    (hf : ∀ (x : ↥Y), Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    id (LocallyQuasiFinite f)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
x : ↥(Y.affineCover.X i)
⊢ Eq (α := Set ↥(pullback f (Y.affineCover.f i)))
    (Set.preimage (β := ↥(Y.affineCover.X i)) ⇑(pullback.snd f (Y.affineCover.f i)) {x})
    (Set.preimage (β := ↥X) (⇑(pullback.fst f (Y.affineCover.f i)))
      (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) ((Y.affineCover.f i) x : ↥Y))))
have h : ∀ (x_1 : ↥(pullback f (Y.affineCover.f i))),
  Membership.mem (γ := Set ↥(pullback f (Y.affineCover.f i)))
      (Set.preimage (β := ↥(Y.affineCover.X i)) ⇑(pullback.snd f (Y.affineCover.f i)) {x}) x_1 ↔
    Membership.mem (γ := Set ↥(pullback f (Y.affineCover.f i)))
      (Set.preimage (β := ↥X) (⇑(pullback.fst f (Y.affineCover.f i)))
        (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) ((Y.affineCover.f i) x : ↥Y))))
      x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
hf : ∀ (x : ↥Y), Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})
hY : ∃ (R : CommRingCat.{u}), Y = Spec R
⊢ id (LocallyQuasiFinite f)
have obtain : ∀ (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyOfFiniteType f]
  (hf : ∀ (x : ↥(Spec R)), Set.Finite (α := ↥X) (Set.preimage (β := ↥(Spec R)) ⇑f {x})), id (LocallyQuasiFinite f)
Tactic: obtain ⟨R, rfl⟩ := hY
Cleared hypotheses: Y, f, inst, hf, hY
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFiniteType f
hf : ∀ (x : ↥(Spec R)), Set.Finite (α := ↥X) (Set.preimage (β := ↥(Spec R)) ⇑f {x})
⊢ id (LocallyQuasiFinite f)
have inr : ∀
  (this :
    ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyOfFiniteType f]
      (hf : ∀ (x : ↥(Spec R)), Set.Finite (α := ↥X) (Set.preimage (β := ↥(Spec R)) ⇑f {x}))
      (hX : ∃ (S : CommRingCat.{u}), X = Spec S), id (LocallyQuasiFinite f))
  (hX : ¬∃ (S : CommRingCat.{u}), X = Spec S), id (LocallyQuasiFinite f)
Tactic: wlog hX : ∃ S, X = Spec S
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFiniteType f
hf : ∀ (x : ↥(Spec R)), Set.Finite (α := ↥X) (Set.preimage (β := ↥(Spec R)) ⇑f {x})
inr :
  ∀
    (this :
      ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyOfFiniteType f]
        (hf : ∀ (x : ↥(Spec R)), Set.Finite (α := ↥X) (Set.preimage (β := ↥(Spec R)) ⇑f {x}))
        (hX : ∃ (S : CommRingCat.{u}), X = Spec S), id (LocallyQuasiFinite f))
    (hX : ¬∃ (S : CommRingCat.{u}), X = Spec S), id (LocallyQuasiFinite f)
⊢ id (LocallyQuasiFinite f)
have wlog : ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyOfFiniteType f]
  (hf : ∀ (x : ↥(Spec R)), Set.Finite (α := ↥X) (Set.preimage (β := ↥(Spec R)) ⇑f {x}))
  (hX : ∃ (S : CommRingCat.{u}), X = Spec S), id (LocallyQuasiFinite f)
Tactic: wlog hX : ∃ S, X = Spec S
Cleared hypotheses: X, R, f, inst, hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFiniteType f
hf : ∀ (x : ↥(Spec R)), Set.Finite (α := ↥X) (Set.preimage (β := ↥(Spec R)) ⇑f {x})
hX : ∃ (S : CommRingCat.{u}), X = Spec S
⊢ id (LocallyQuasiFinite f)
have obtain : ∀ (S : CommRingCat.{u}) (f : Spec S ⟶ Spec R) [LocallyOfFiniteType f]
  (hf : ∀ (x : ↥(Spec R)), Set.Finite (α := ↥(Spec S)) (Set.preimage (β := ↥(Spec R)) ⇑f {x})),
  id (LocallyQuasiFinite f)
Tactic: obtain ⟨S, rfl⟩ := hX
Cleared hypotheses: X, f, inst, hf, hX
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
R S : CommRingCat
f : Spec S ⟶ Spec R
inst : LocallyOfFiniteType f
hf : ∀ (x : ↥(Spec R)), Set.Finite (α := ↥(Spec S)) (Set.preimage (β := ↥(Spec R)) ⇑f {x})
⊢ id (LocallyQuasiFinite f)
have obtain : ∀ (φ : R ⟶ S) [LocallyOfFiniteType (Spec.map φ)]
  (hf : ∀ (x : ↥(Spec R)), Set.Finite (α := ↥(Spec S)) (Set.preimage (β := ↥(Spec R)) ⇑(Spec.map φ) {x})),
  id (LocallyQuasiFinite (Spec.map φ))
Tactic: obtain ⟨φ, rfl⟩ := Spec.map_surjective f
Cleared hypotheses: f, inst, hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
R S : CommRingCat
φ : R ⟶ S
inst : LocallyOfFiniteType (Spec.map φ)
hf : ∀ (x : ↥(Spec R)), Set.Finite (α := ↥(Spec S)) (Set.preimage (β := ↥(Spec R)) ⇑(Spec.map φ) {x})
⊢ id (LocallyQuasiFinite (Spec.map φ))
have simp : (CommRingCat.Hom.hom φ).FiniteType → (CommRingCat.Hom.hom φ).QuasiFinite
Tactic: simp only [HasRingHomProperty.Spec_iff, id_eq] at *
Cleared hypotheses: inst
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (hypothesis)
Goal:
R S : CommRingCat
φ : R ⟶ S
hf : ∀ (x : ↥(Spec R)), Set.Finite (α := ↥(Spec S)) (Set.preimage (β := ↥(Spec R)) ⇑(Spec.map φ) {x})
inst : (CommRingCat.Hom.hom φ).FiniteType
⊢ (CommRingCat.Hom.hom φ).QuasiFinite
have algebraizeInst : Algebra.FiniteType.{u, u} (↑R : Type u) (↑S : Type u)
Tactic: algebraize [φ.hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
hx : QuasiFiniteAt f x
V : X.Opens
hV : IsAffineOpen V
U : Y.Opens
hU : IsAffineOpen U
hVU : V ≤ f ⁻¹ᵁ U
hxV : x ∈ V.carrier
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (appLE f U V hVU)).toAlgebra
algInst_1 : Algebra (↑(Y.presheaf.obj (Opposite.op U)) : Type u) (↑(Y.presheaf.stalk (f x)) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (Y.presheaf.germ U (f x) ⋯))
⊢ RingHom.QuasiFinite (S := (↑(Y.presheaf.stalk (f x)) : Type u)) (CommRingCat.Hom.hom (Y.presheaf.germ U (f x) ⋯))
have this : IsLocalization.AtPrime (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) sorry) : ↥Y)) : Type u)
  (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) sorry)).asIdeal
Tactic: have := hU.isLocalization_stalk ⟨f x, (hVU hxV)⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
hx : QuasiFiniteAt f x
V : X.Opens
hV : IsAffineOpen V
U : Y.Opens
hU : IsAffineOpen U
hVU : V ≤ f ⁻¹ᵁ U
hxV : x ∈ V.carrier
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (appLE f U V hVU)).toAlgebra
⊢ (CommRingCat.Hom.hom (appLE f U V hVU)).QuasiFiniteAt
    (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal
have H : RingHom.QuasiFinite (S := (↑(Y.presheaf.stalk (f x)) : Type u)) (CommRingCat.Hom.hom (Y.presheaf.germ U (f x) sorry))
Tactic: have H : (Y.presheaf.germ U _ (hVU hxV)).hom.QuasiFinite := by
    algebraize [(Y.presheaf.germ U _ (hVU hxV)).hom]
    have := hU.isLocalization_stalk ⟨f x, (hVU hxV)⟩
    rw [← (Y.presheaf.germ U _ (hVU hxV)).hom.algebraMap_toAlgebra,
      RingHom.quasiFinite_algebraMap]
    exact .of_isLocalization (hU.primeIdealOf ⟨_, hVU hxV⟩).asIdeal.primeCompl
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
hx : QuasiFiniteAt f x
V : X.Opens
hV : IsAffineOpen V
U : Y.Opens
hU : IsAffineOpen U
hVU : V ≤ f ⁻¹ᵁ U
hxV : x ∈ V.carrier
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (appLE f U V hVU)).toAlgebra
H : RingHom.QuasiFinite (S := (↑(Y.presheaf.stalk (f x)) : Type u)) (CommRingCat.Hom.hom (Y.presheaf.germ U (f x) ⋯))
algInst_1 : Algebra (↑(X.presheaf.obj (Opposite.op V)) : Type u) (↑(X.presheaf.stalk x) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (X.presheaf.germ V x hxV))
⊢ (CommRingCat.Hom.hom (appLE f U V hVU)).QuasiFiniteAt
    (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal
have this : IsLocalization.AtPrime (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV) : ↥X)) : Type u)
  (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal
Tactic: have := hV.isLocalization_stalk ⟨x, hxV⟩