awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyQuasiFinite f
inst_1 : IsLocallyArtinian Y
hY : ∃ (R : CommRingCat.{u}), Y = Spec R
hX : ∃ (S : CommRingCat.{u}), X = Spec S
obtain :
  ∀ (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyQuasiFinite f] [IsLocallyArtinian.{u} (Spec R)],
    id (IsLocallyArtinian X)
⊢ id (IsLocallyArtinian X)

Tactic:
obtain ⟨R, rfl⟩ := hY

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X : Scheme
hX : ∃ (S : CommRingCat.{u}), X = Spec S
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyQuasiFinite f
inst_1 : IsLocallyArtinian.{u} (Spec R)
obtain : ∀ (S : CommRingCat.{u}) (f : Spec S ⟶ Spec R) [LocallyQuasiFinite f], id (IsLocallyArtinian.{u} (Spec S))
⊢ id (IsLocallyArtinian X)

Tactic:
obtain ⟨S, rfl⟩ := hX

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
R : CommRingCat
inst : IsLocallyArtinian.{u} (Spec R)
S : CommRingCat
f : Spec S ⟶ Spec R
inst_1 : LocallyQuasiFinite f
obtain : ∀ (φ : R ⟶ S) [LocallyQuasiFinite (Spec.map φ)], id (IsLocallyArtinian.{u} (Spec S))
⊢ id (IsLocallyArtinian.{u} (Spec S))

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

Premises used: AlgebraicGeometry.Spec.map_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
R : CommRingCat
inst : IsLocallyArtinian.{u} (Spec R)
S : CommRingCat
φ : R ⟶ S
inst_1 : LocallyQuasiFinite (Spec.map φ)
simp : IsArtinianRing.{u} (↑R : Type u) → (CommRingCat.Hom.hom φ).QuasiFinite → IsArtinianRing.{u} (↑S : Type u)
⊢ id (IsLocallyArtinian.{u} (Spec S))

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

Premises used: AlgebraicGeometry.HasRingHomProperty.Spec_iff, AlgebraicGeometry.Scheme.isLocallyArtinianScheme_Spec, id_eq
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
R S : CommRingCat
φ : R ⟶ S
inst : IsArtinianRing.{u} (↑R : Type u)
inst_1 : (CommRingCat.Hom.hom φ).QuasiFinite
⊢ Algebra.QuasiFinite.{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
inst : IsArtinianRing.{u} (↑R : Type u)
inst_1 : (CommRingCat.Hom.hom φ).QuasiFinite
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Algebra.QuasiFinite.{u, u} (↑R : Type u) (↑S : Type u)
⊢ Module.Finite.{u, u} (↑R : Type u) (↑S : Type u)

Tactic:
have : Module.Finite R S := .of_quasiFinite
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
R S : CommRingCat
φ : R ⟶ S
inst : IsArtinianRing.{u} (↑R : Type u)
inst_1 : (CommRingCat.Hom.hom φ).QuasiFinite
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Algebra.QuasiFinite.{u, u} (↑R : Type u) (↑S : Type u)
this : Module.Finite.{u, u} (↑R : Type u) (↑S : Type u)
⊢ IsArtinianRing.{u} (↑S : Type u)

Tactic:
.of_finite R S

Premises used: CommRingCat.carrier, IsArtinianRing.of_finite
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
R S : CommRingCat
φ : R ⟶ S
inst : IsArtinianRing.{u} (↑R : Type u)
inst_1 : (CommRingCat.Hom.hom φ).QuasiFinite
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Algebra.QuasiFinite.{u, u} (↑R : Type u) (↑S : Type u)
this : Module.Finite.{u, u} (↑R : Type u) (↑S : Type u)
⊢ IsArtinianRing.{u} (↑S : Type u)

Tactic:
exact .of_finite R S
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyQuasiFinite f
y : ↥Y
⊢ IsLocallyArtinian.{u} (Hom.fiber f y)

Tactic:
.of_locallyQuasiFinite (pullback.snd _ _)

Premises used: CategoryTheory.Limits.pullback.snd, AlgebraicGeometry.IsLocallyArtinian.of_locallyQuasiFinite
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyQuasiFinite f
y : ↥Y
⊢ IsDiscrete (X := ↥X) (Set.preimage (β := ↥Y) ⇑f {y})

Tactic:
simpa [Scheme.Hom.range_fiberι] using
    (isDiscrete_univ_iff.mpr inferInstance).image (f.fiberι y).isEmbedding.toIsInducing

Premises used: Iff.mpr, AlgebraicGeometry.Scheme.Hom.range_fiberι, inferInstance, isDiscrete_univ_iff, AlgebraicGeometry.Scheme.Hom.fiberι, AlgebraicGeometry.Scheme.Hom.isEmbedding, IsDiscrete.image, Topology.IsEmbedding.toIsInducing
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyQuasiFinite f
s : Set ↥Y
hs : IsDiscrete s
⊢ IsDiscrete (X := ↥X) (⇑f ⁻¹' s)

Tactic:
hs.preimage' f.continuous.continuousOn f.isDiscrete_preimage_singleton

Premises used: Continuous.continuousOn, AlgebraicGeometry.Scheme.Hom.isDiscrete_preimage_singleton, AlgebraicGeometry.Scheme.Hom.continuous, IsDiscrete.preimage'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyQuasiFinite f
inst_1 : QuasiCompact f
y : ↥Y
⊢ Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {y})

Tactic:
simpa [Scheme.Hom.range_fiberι] using Set.finite_univ.image (f.fiberι y)

Premises used: AlgebraicGeometry.Scheme.Hom.range_fiberι, CategoryTheory.ConcreteCategory.hom, Set.Finite.image, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.Scheme.Hom.fiberι, Set.finite_univ, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyQuasiFinite f
inst_1 : QuasiCompact f
s : Set ↥Y
hs : s.Finite
⊢ Set.Finite (α := ↥X) (⇑f ⁻¹' s)

Tactic:
hs.preimage' fun _ _ ↦ f.finite_preimage_singleton _

Premises used: AlgebraicGeometry.Scheme.Hom.finite_preimage_singleton, Set.Finite.preimage'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyQuasiFinite f
inst_1 : QuasiCompact f
⊢ Filter.Tendsto (α := ↥X) (β := ↥Y) (⇑f) Filter.cofinite Filter.cofinite

Tactic:
.cofinite_of_finite_preimage_singleton f.finite_preimage_singleton

Premises used: Filter.Tendsto.cofinite_of_finite_preimage_singleton, AlgebraicGeometry.Scheme.Hom.finite_preimage_singleton
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyQuasiFinite f
inst_1 : QuasiCompact f
inst_2 : IsLocallyArtinian Y
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyQuasiFinite f] [QuasiCompact f] [IsLocallyArtinian Y]
        (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), id (IsFinite f))
    (hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R), id (IsFinite f)
wlog :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyQuasiFinite f] [QuasiCompact f] [IsLocallyArtinian Y]
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), id (IsFinite f)
⊢ id (IsFinite f)

Tactic:
wlog hY : ∃ R, Y = Spec R
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyQuasiFinite f
inst_1 : QuasiCompact f
inst_2 : IsLocallyArtinian Y
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyQuasiFinite f] [QuasiCompact f] [IsLocallyArtinian Y]
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), id (IsFinite f)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
⊢ id (IsFinite f)

Tactic:
(IsZariskiLocalAtTarget.iff_of_openCover Y.affineCover).mpr fun i ↦
      this (pullback.snd _ _) ⟨_, 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 : LocallyQuasiFinite f
inst_1 : QuasiCompact f
inst_2 : IsLocallyArtinian Y
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyQuasiFinite f] [QuasiCompact f] [IsLocallyArtinian Y]
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), id (IsFinite f)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
⊢ id (IsFinite f)

Tactic:
exact (IsZariskiLocalAtTarget.iff_of_openCover Y.affineCover).mpr fun i ↦
      this (pullback.snd _ _) ⟨_, 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 : LocallyQuasiFinite f
inst_1 : QuasiCompact f
inst_2 : IsLocallyArtinian Y
hY : ∃ (R : CommRingCat.{u}), Y = Spec R
obtain :
  ∀ (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyQuasiFinite f] [QuasiCompact f] [IsLocallyArtinian.{u} (Spec R)],
    id (IsFinite f)
⊢ id (IsFinite f)

Tactic:
obtain ⟨R, rfl⟩ := hY

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyQuasiFinite f
inst_1 : QuasiCompact f
inst_2 : IsLocallyArtinian.{u} (Spec R)
inr :
  ∀
    (this :
      ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyQuasiFinite f] [QuasiCompact f]
        [IsLocallyArtinian.{u} (Spec R)] (hX : ∃ (S : CommRingCat.{u}), X = Spec S), id (IsFinite f))
    (hX : ¬∃ (S : CommRingCat.{u}), X = Spec S), id (IsFinite f)
wlog :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyQuasiFinite f] [QuasiCompact f]
    [IsLocallyArtinian.{u} (Spec R)] (hX : ∃ (S : CommRingCat.{u}), X = Spec S), id (IsFinite f)
⊢ id (IsFinite f)

Tactic:
wlog hX : ∃ S, X = Spec S
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyQuasiFinite f
inst_1 : QuasiCompact f
inst_2 : IsLocallyArtinian.{u} (Spec R)
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyQuasiFinite f] [QuasiCompact f]
    [IsLocallyArtinian.{u} (Spec R)] (hX : ∃ (S : CommRingCat.{u}), X = Spec S), id (IsFinite f)
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
⊢ IsArtinianScheme X

Tactic:
have inst : IsArtinianScheme X :=
      { toIsLocallyArtinian := .of_locallyQuasiFinite f,
        toCompactSpace := QuasiCompact.compactSpace_of_compactSpace f }
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst_1 : LocallyQuasiFinite f
inst_2 : QuasiCompact f
inst_3 : IsLocallyArtinian.{u} (Spec R)
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyQuasiFinite f] [QuasiCompact f]
    [IsLocallyArtinian.{u} (Spec R)] (hX : ∃ (S : CommRingCat.{u}), X = Spec S), id (IsFinite f)
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
inst : IsArtinianScheme X
⊢ id (IsFinite f)

Tactic:
(MorphismProperty.cancel_left_of_respectsIso _ _ _).mp
      (this _ ((Scheme.isoSpec X).inv ≫ f) ⟨_, rfl⟩)

Premises used: AlgebraicGeometry.Scheme.isoSpec, Exists.intro, CategoryTheory.CategoryStruct.comp, Iff.mp, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Iso.inv, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst_1 : LocallyQuasiFinite f
inst_2 : QuasiCompact f
inst_3 : IsLocallyArtinian.{u} (Spec R)
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyQuasiFinite f] [QuasiCompact f]
    [IsLocallyArtinian.{u} (Spec R)] (hX : ∃ (S : CommRingCat.{u}), X = Spec S), id (IsFinite f)
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
inst : IsArtinianScheme X
⊢ id (IsFinite f)

Tactic:
exact (MorphismProperty.cancel_left_of_respectsIso _ _ _).mp
      (this _ ((Scheme.isoSpec X).inv ≫ f) ⟨_, rfl⟩)

Premises used: AlgebraicGeometry.Scheme.isoSpec, Exists.intro, CategoryTheory.CategoryStruct.comp, Iff.mp, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Iso.inv, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyQuasiFinite f
inst_1 : QuasiCompact f
inst_2 : IsLocallyArtinian.{u} (Spec R)
hX : ∃ (S : CommRingCat.{u}), X = Spec S
obtain : ∀ (S : CommRingCat.{u}) (f : Spec S ⟶ Spec R) [LocallyQuasiFinite f] [QuasiCompact f], id (IsFinite f)
⊢ id (IsFinite f)

Tactic:
obtain ⟨S, rfl⟩ := hX

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
R : CommRingCat
inst : IsLocallyArtinian.{u} (Spec R)
S : CommRingCat
f : Spec S ⟶ Spec R
inst_1 : LocallyQuasiFinite f
inst_2 : QuasiCompact f
obtain : ∀ (φ : R ⟶ S) [LocallyQuasiFinite (Spec.map φ)] [QuasiCompact (Spec.map φ)], id (IsFinite (Spec.map φ))
⊢ id (IsFinite f)

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

Premises used: AlgebraicGeometry.Spec.map_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
R : CommRingCat
inst : IsLocallyArtinian.{u} (Spec R)
S : CommRingCat
φ : R ⟶ S
inst_1 : LocallyQuasiFinite (Spec.map φ)
inst_2 : QuasiCompact (Spec.map φ)
simp : IsArtinianRing.{u} (↑R : Type u) → (CommRingCat.Hom.hom φ).QuasiFinite → (CommRingCat.Hom.hom φ).Finite
⊢ id (IsFinite (Spec.map φ))

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

Premises used: AlgebraicGeometry.IsFinite.SpecMap_iff, AlgebraicGeometry.HasRingHomProperty.Spec_iff, AlgebraicGeometry.Scheme.isLocallyArtinianScheme_Spec, id_eq
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
R S : CommRingCat
φ : R ⟶ S
inst : QuasiCompact (Spec.map φ)
inst_1 : IsArtinianRing.{u} (↑R : Type u)
inst_2 : (CommRingCat.Hom.hom φ).QuasiFinite
⊢ Algebra.QuasiFinite.{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
inst : QuasiCompact (Spec.map φ)
inst_1 : IsArtinianRing.{u} (↑R : Type u)
inst_2 : (CommRingCat.Hom.hom φ).QuasiFinite
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Algebra.QuasiFinite.{u, u} (↑R : Type u) (↑S : Type u)
⊢ (CommRingCat.Hom.hom φ).Finite

Tactic:
.of_quasiFinite

Premises used: RingHom.Finite, Module.Finite.of_quasiFinite
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
R S : CommRingCat
φ : R ⟶ S
inst : QuasiCompact (Spec.map φ)
inst_1 : IsArtinianRing.{u} (↑R : Type u)
inst_2 : (CommRingCat.Hom.hom φ).QuasiFinite
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Algebra.QuasiFinite.{u, u} (↑R : Type u) (↑S : Type u)
⊢ (CommRingCat.Hom.hom φ).Finite

Tactic:
exact .of_quasiFinite
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f_1 f : X ⟶ Y
inst : LocallyQuasiFinite f
inst_1 : QuasiCompact f
x : ↥Y
⊢ IsFinite (Hom.fiberToSpecResidueField f x)

Tactic:
.of_locallyQuasiFinite (pullback.snd _ _)

Premises used: CategoryTheory.Limits.pullback.snd, AlgebraicGeometry.Scheme.Hom.fiber, AlgebraicGeometry.IsFinite.of_locallyQuasiFinite, AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField 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) (hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField 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
hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField 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
hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField 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)),
    LocallyQuasiFinite (X := Hom.fiber (X := pullback f (Y.affineCover.f i)) (pullback.snd f (Y.affineCover.f i)) x)
      (Hom.fiberToSpecResidueField (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
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField 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 : ↥Y), IsLocallyArtinian.{u} (Hom.fiber f x)

Tactic:
have (x : Y) : IsLocallyArtinian (f.fiber x) :=
      .of_locallyQuasiFinite (f.fiberToSpecResidueField x)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
this_1 :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField 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)
this : ∀ (x : ↥Y), IsLocallyArtinian.{u} (Hom.fiber f x)
⊢ LocallyQuasiFinite (X := Hom.fiber (X := pullback f (Y.affineCover.f i)) (pullback.snd f (Y.affineCover.f i)) x)
    (Hom.fiberToSpecResidueField (pullback.snd f (Y.affineCover.f i)) x)

Tactic:
(MorphismProperty.cancel_right_of_respectsIso @LocallyQuasiFinite _
      (Spec.map ((Y.affineCover.f i).residueFieldMap _))).mp ?_

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.Hom.residueFieldMap, AlgebraicGeometry.Spec.map, AlgebraicGeometry.LocallyQuasiFinite, Iff.mp, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
this_1 :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField 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)
this : ∀ (x : ↥Y), IsLocallyArtinian.{u} (Hom.fiber f x)
inr :
  LocallyQuasiFinite (X := Hom.fiber (X := pullback f (Y.affineCover.f i)) (pullback.snd f (Y.affineCover.f i)) x)
    (Hom.fiberToSpecResidueField (pullback.snd f (Y.affineCover.f i)) x ≫
      Spec.map (Hom.residueFieldMap (Y.affineCover.f i) x))
⊢ LocallyQuasiFinite (X := Hom.fiber (X := pullback f (Y.affineCover.f i)) (pullback.snd f (Y.affineCover.f i)) x)
    (Hom.fiberToSpecResidueField (pullback.snd f (Y.affineCover.f i)) x)

Tactic:
refine (MorphismProperty.cancel_right_of_respectsIso @LocallyQuasiFinite _
      (Spec.map ((Y.affineCover.f i).residueFieldMap _))).mp ?_

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.Hom.residueFieldMap, AlgebraicGeometry.Spec.map, AlgebraicGeometry.LocallyQuasiFinite, Iff.mp, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
this_1 :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField 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)
this : ∀ (x : ↥Y), IsLocallyArtinian.{u} (Hom.fiber f x)
⊢ Eq (α := pullback f (Y.affineCover.f i) ⟶ Y) (pullback.snd f (Y.affineCover.f i) ≫ Y.affineCover.f i)
    (pullback.fst f (Y.affineCover.f i) ≫ f)

Tactic:
simp [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
this_1 :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField 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)
this : ∀ (x : ↥Y), IsLocallyArtinian.{u} (Hom.fiber f x)
⊢ (Y.affineCover.X i).fromSpecResidueField x ≫ Y.affineCover.f i =
    Spec.map (Hom.residueFieldMap (Y.affineCover.f i) x) ≫ Y.fromSpecResidueField ((Y.affineCover.f i) x)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
this_1 :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField 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)
this : ∀ (x : ↥Y), IsLocallyArtinian.{u} (Hom.fiber f x)
g : Hom.fiber (X := pullback f (Y.affineCover.f i)) (pullback.snd f (Y.affineCover.f i)) x ⟶
  Hom.fiber f ((Y.affineCover.f i) x) :=
  pullback.map (pullback.snd f (Y.affineCover.f i)) ((Y.affineCover.X i).fromSpecResidueField x) f
    (Y.fromSpecResidueField ((Y.affineCover.f i) x)) (pullback.fst f (Y.affineCover.f i))
    (Spec.map (Hom.residueFieldMap (Y.affineCover.f i) x)) (Y.affineCover.f i) ⋯ ⋯
⊢ IsClosedImmersion g

Tactic:
have : IsClosedImmersion g := .of_isPreimmersion _ (isClosed_discrete _)