awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
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 R).fromSpecResidueField x ≫ 𝟙 (Spec R) =
    Spec.map (Spec.residueFieldIso R x).inv ≫
      Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) x.asIdeal.ResidueField))

Tactic:
simp [← Spec.map_comp, fromSpecResidueField, Spec.fromSpecStalk_eq]

Premises used: AlgebraicGeometry.Scheme.fromSpecResidueField, AlgebraicGeometry.Spec.map_comp, AlgebraicGeometry.Spec.fromSpecStalk_eq
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
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
⊢ (Arrow.mk (Hom.fiberToSpecResidueField (Spec.map φ) x)).right ≅
    (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)))))).right

Tactic:
exact asIso (Spec.map (Spec.residueFieldIso _ x).inv)

Premises used: AlgebraicGeometry.Spec.map, AlgebraicGeometry.Scheme.Spec.residueFieldIso, CategoryTheory.Iso.inv, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
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
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp [Hom.fiberToSpecResidueField]

Premises used: AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
⊢ LocallyQuasiFinite f ↔ ∀ (x : ↥Y), IsFinite (Hom.fiberToSpecResidueField f x)

Tactic:
⟨fun _ ↦ inferInstance, fun _ ↦ .of_fiberToSpecResidueField f fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro, AlgebraicGeometry.LocallyQuasiFinite.of_fiberToSpecResidueField
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsPreimmersion f
⊢ LocallyQuasiFinite f

Tactic:
.of_fiberToSpecResidueField _ fun x ↦ ?_

Premises used: AlgebraicGeometry.LocallyQuasiFinite.of_fiberToSpecResidueField
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsPreimmersion f
refine : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
⊢ LocallyQuasiFinite f

Tactic:
refine .of_fiberToSpecResidueField _ fun x ↦ ?_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsPreimmersion f
x : ↥Y
⊢ IsClosedImmersion (Hom.fiberToSpecResidueField f x)

Tactic:
have : IsClosedImmersion (f.fiberToSpecResidueField x) :=
    .of_isPreimmersion (pullback.snd _ _) (isClosed_discrete _)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsPreimmersion f
x : ↥Y
this : IsClosedImmersion (Hom.fiberToSpecResidueField f x)
⊢ LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
⊢ LocallyQuasiFinite f ↔ ∀ (x : ↥Y), IsDiscrete (X := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})

Tactic:
⟨fun _ ↦ f.isDiscrete_preimage_singleton, fun H ↦ ?_⟩

Premises used: AlgebraicGeometry.Scheme.Hom.isDiscrete_preimage_singleton, Iff.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
refine : ∀ (H : ∀ (x : ↥Y), IsDiscrete (X := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})), LocallyQuasiFinite f
⊢ LocallyQuasiFinite f ↔ ∀ (x : ↥Y), IsDiscrete (X := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})

Tactic:
refine ⟨fun _ ↦ f.isDiscrete_preimage_singleton, fun H ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
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)
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)
⊢ id (LocallyQuasiFinite f)

Tactic:
wlog hY : ∃ R, Y = Spec R
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
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)

Tactic:
(IsZariskiLocalAtTarget.iff_of_openCover Y.affineCover).mpr fun i ↦
      this (f := pullback.snd _ _) (fun x ↦ ?_) ⟨_, rfl⟩

Premises used: Iff.mpr, Exists.intro, AlgebraicGeometry.Scheme.affineCover._proof_7, Classical.choose, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
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
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})
⊢ id (LocallyQuasiFinite f)

Tactic:
refine (IsZariskiLocalAtTarget.iff_of_openCover Y.affineCover).mpr fun i ↦
      this (f := pullback.snd _ _) (fun x ↦ ?_) ⟨_, rfl⟩

Premises used: Iff.mpr, Exists.intro, AlgebraicGeometry.Scheme.affineCover._proof_7, Classical.choose, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
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 (β := ↥X) (⇑(pullback.fst f (Y.affineCover.f i)))
      (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) ((Y.affineCover.f i) x : ↥Y))))

Tactic:
(H (Y.affineCover.f i x)).preimage ((pullback.fst f _).continuous.continuousOn)
        (pullback.fst f (Y.affineCover.f i)).isOpenEmbedding.injective

Premises used: CategoryTheory.PreZeroHypercover.f, Continuous.continuousOn, Topology.IsOpenEmbedding.toIsEmbedding, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, CategoryTheory.Limits.pullback.fst, Topology.IsEmbedding.injective, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.Hom.continuous, IsDiscrete.preimage, AlgebraicGeometry.Scheme.affineCover, DFunLike.coe, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
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)
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))))
⊢ IsDiscrete (X := ↥(pullback f (Y.affineCover.f i)))
    (Set.preimage (β := ↥(Y.affineCover.X i)) ⇑(pullback.snd f (Y.affineCover.f i)) {x})

Tactic:
convert!
      (H (Y.affineCover.f i x)).preimage ((pullback.fst f _).continuous.continuousOn)
        (pullback.fst f (Y.affineCover.f i)).isOpenEmbedding.injective

Premises used: CategoryTheory.PreZeroHypercover.f, Continuous.continuousOn, Topology.IsOpenEmbedding.toIsEmbedding, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, CategoryTheory.Limits.pullback.fst, Topology.IsEmbedding.injective, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.Hom.continuous, IsDiscrete.preimage, AlgebraicGeometry.Scheme.affineCover, DFunLike.coe, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
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)
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
⊢ 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:
ext
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
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)
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:
simp [← (Y.affineCover.f i).isOpenEmbedding.injective.eq_iff, ← Scheme.Hom.comp_apply,
      -Hom.comp_base, pullback.condition]

Premises used: CategoryTheory.PreZeroHypercover.f, Topology.IsOpenEmbedding.toIsEmbedding, Function.Injective.eq_iff, AlgebraicGeometry.Scheme.Hom.comp_apply, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, Topology.IsEmbedding.injective, AlgebraicGeometry.Scheme.Hom.comp_base, CategoryTheory.Limits.pullback.condition, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
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
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)
⊢ id (LocallyQuasiFinite f)

Tactic:
obtain ⟨R, rfl⟩ := hY

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
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)
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)
⊢ id (LocallyQuasiFinite f)

Tactic:
wlog hX : ∃ S, X = Spec S
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
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})
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:
(IsZariskiLocalAtSource.iff_of_openCover X.affineCover).mpr fun i ↦
      this _ (fun x ↦ (H x).preimage (X.affineCover.f _).continuous.continuousOn
      (X.affineCover.f _).isOpenEmbedding.injective) ⟨_, rfl⟩

Premises used: Iff.mpr, CategoryTheory.PreZeroHypercover.f, Continuous.continuousOn, Topology.IsOpenEmbedding.toIsEmbedding, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover, Topology.IsEmbedding.injective, Exists.intro, AlgebraicGeometry.Scheme.affineCover._proof_7, Classical.choose, AlgebraicGeometry.Scheme.Hom.continuous, IsDiscrete.preimage, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
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})
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:
exact (IsZariskiLocalAtSource.iff_of_openCover X.affineCover).mpr fun i ↦
      this _ (fun x ↦ (H x).preimage (X.affineCover.f _).continuous.continuousOn
      (X.affineCover.f _).isOpenEmbedding.injective) ⟨_, rfl⟩

Premises used: Iff.mpr, CategoryTheory.PreZeroHypercover.f, Continuous.continuousOn, Topology.IsOpenEmbedding.toIsEmbedding, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover, Topology.IsEmbedding.injective, Exists.intro, AlgebraicGeometry.Scheme.affineCover._proof_7, Classical.choose, AlgebraicGeometry.Scheme.Hom.continuous, IsDiscrete.preimage, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
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
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)
⊢ id (LocallyQuasiFinite f)

Tactic:
obtain ⟨S, rfl⟩ := hX

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
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})
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 φ))
⊢ id (LocallyQuasiFinite f)

Tactic:
obtain ⟨φ, rfl⟩ := Spec.map_surjective f

Premises used: AlgebraicGeometry.Spec.map_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
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})
simp : (CommRingCat.Hom.hom φ).FiniteType → (CommRingCat.Hom.hom φ).QuasiFinite
⊢ id (LocallyQuasiFinite (Spec.map φ))

Tactic:
simp only [HasRingHomProperty.Spec_iff, id_eq] at *

Premises used: AlgebraicGeometry.HasRingHomProperty.Spec_iff, id_eq
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
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
⊢ Algebra.FiniteType.{u, u} (↑R : Type u) (↑S : Type u)

Tactic:
algebraize [φ.hom]

Premises used: CommRingCat.Hom.hom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
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
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Algebra.FiniteType.{u, u} (↑R : Type u) (↑S : Type u)
⊢ (CommRingCat.Hom.hom φ).QuasiFinite

Tactic:
(Algebra.QuasiFinite.iff_finite_comap_preimage_singleton).mpr fun x ↦
    ((Spec.map φ).isCompact_preimage_singleton _).finite (H _)

Premises used: Iff.mpr, AlgebraicGeometry.Scheme.Hom.isCompact_preimage_singleton, AlgebraicGeometry.Spec.map, Algebra.QuasiFinite.iff_finite_comap_preimage_singleton, RingHom.QuasiFinite, IsCompact.finite
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
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
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Algebra.FiniteType.{u, u} (↑R : Type u) (↑S : Type u)
⊢ (CommRingCat.Hom.hom φ).QuasiFinite

Tactic:
exact (Algebra.QuasiFinite.iff_finite_comap_preimage_singleton).mpr fun x ↦
    ((Spec.map φ).isCompact_preimage_singleton _).finite (H _)

Premises used: Iff.mpr, AlgebraicGeometry.Scheme.Hom.isCompact_preimage_singleton, AlgebraicGeometry.Spec.map, Algebra.QuasiFinite.iff_finite_comap_preimage_singleton, IsCompact.finite
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
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)
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)
⊢ id (LocallyQuasiFinite f)

Tactic:
wlog hY : ∃ R, Y = Spec R
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
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)

Tactic:
(IsZariskiLocalAtTarget.iff_of_openCover Y.affineCover).mpr fun i ↦
      this (f := pullback.snd _ _) (fun x ↦ ?_) ⟨_, rfl⟩

Premises used: Iff.mpr, CategoryTheory.PreZeroHypercover.f, CategoryTheory.Limits.pullback.snd, Exists.intro, AlgebraicGeometry.Scheme.affineCover._proof_7, Classical.choose, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
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
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})
⊢ id (LocallyQuasiFinite f)

Tactic:
refine (IsZariskiLocalAtTarget.iff_of_openCover Y.affineCover).mpr fun i ↦
      this (f := pullback.snd _ _) (fun x ↦ ?_) ⟨_, rfl⟩

Premises used: Iff.mpr, CategoryTheory.PreZeroHypercover.f, CategoryTheory.Limits.pullback.snd, Exists.intro, AlgebraicGeometry.Scheme.affineCover._proof_7, Classical.choose, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl