awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_2 : ∀ (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) ⋯ ⋯
this : IsClosedImmersion g
⊢ LocallyQuasiFinite (g ≫ Hom.fiberToSpecResidueField f ((Y.affineCover.f i) x))

Tactic:
(inferInstance : LocallyQuasiFinite <| g ≫ f.fiberToSpecResidueField _)

Premises used: inferInstance
-- 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_2 : ∀ (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) ⋯ ⋯
this : IsClosedImmersion g
h :
  Hom.fiberToSpecResidueField (pullback.snd f (Y.affineCover.f i)) x ≫
      Spec.map (Hom.residueFieldMap (Y.affineCover.f i) x) =
    g ≫ Hom.fiberToSpecResidueField f ((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 ≫
      Spec.map (Hom.residueFieldMap (Y.affineCover.f i) x))

Tactic:
convert! (inferInstance : LocallyQuasiFinite <| g ≫ f.fiberToSpecResidueField _) using 1

Premises used: inferInstance
-- 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_2 : ∀ (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) ⋯ ⋯
this : IsClosedImmersion g
⊢ Hom.fiberToSpecResidueField (pullback.snd f (Y.affineCover.f i)) x ≫
      Spec.map (Hom.residueFieldMap (Y.affineCover.f i) x) =
    g ≫ Hom.fiberToSpecResidueField f ((Y.affineCover.f i) x)

Tactic:
simp [g, Hom.fiberToSpecResidueField]

Premises used: AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
hY : ∃ (R : CommRingCat.{u}), Y = Spec R
obtain :
  ∀ (R : CommRingCat.{u}) (f : X ⟶ Spec R)
    (hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField 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
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
inr :
  ∀
    (this :
      ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R)
        (hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField 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)
    (hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField 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
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R)
    (hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField 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 ↦ ?_) ⟨_, rfl⟩

Premises used: Iff.mpr, CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover, Exists.intro, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.Scheme.affineCover._proof_7, Classical.choose, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R)
    (hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x))
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), id (LocallyQuasiFinite f)
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
inr :
  ∀ (i : X.affineCover.I₀) (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField (X.affineCover.f i ≫ f) x)
⊢ id (LocallyQuasiFinite f)

Tactic:
refine (IsZariskiLocalAtSource.iff_of_openCover X.affineCover).mpr fun i ↦
      this _ _ (fun x ↦ ?_) ⟨_, rfl⟩

Premises used: Iff.mpr, CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover, Exists.intro, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.Scheme.affineCover._proof_7, Classical.choose, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R)
    (hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x))
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), id (LocallyQuasiFinite f)
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
i : X.affineCover.I₀
x : ↥(Spec R)
⊢ ∀ (x : ↥(Spec R)), IsLocallyArtinian.{u} (Hom.fiber f x)

Tactic:
have (x : _) : IsLocallyArtinian (f.fiber x) :=
      .of_locallyQuasiFinite (f.fiberToSpecResidueField x)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
this_1 :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R)
    (hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x))
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), id (LocallyQuasiFinite f)
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
i : X.affineCover.I₀
x : ↥(Spec R)
this : ∀ (x : ↥(Spec R)), IsLocallyArtinian.{u} (Hom.fiber f x)
⊢ (X.affineCover.f i ≫ f) ≫ 𝟙 (Spec R) = X.affineCover.f i ≫ f

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
this_1 :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R)
    (hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x))
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), id (LocallyQuasiFinite f)
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
i : X.affineCover.I₀
x : ↥(Spec R)
this : ∀ (x : ↥(Spec R)), IsLocallyArtinian.{u} (Hom.fiber f x)
⊢ (Spec R).fromSpecResidueField x ≫ 𝟙 (Spec R) = 𝟙 (Spec ((Spec R).residueField x)) ≫ (Spec R).fromSpecResidueField x

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
this_1 :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R)
    (hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x))
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), id (LocallyQuasiFinite f)
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
i : X.affineCover.I₀
x : ↥(Spec R)
this : ∀ (x : ↥(Spec R)), IsLocallyArtinian.{u} (Hom.fiber f x)
g : Hom.fiber (X.affineCover.f i ≫ f) x ⟶ Hom.fiber f x :=
  pullback.map (X.affineCover.f i ≫ f) ((Spec R).fromSpecResidueField x) f ((Spec R).fromSpecResidueField x)
    (X.affineCover.f i) (𝟙 (Spec ((Spec R).residueField x))) (𝟙 (Spec R)) ⋯ ⋯
⊢ IsClosedImmersion g

Tactic:
have : IsClosedImmersion g := .of_isPreimmersion _ (isClosed_discrete _)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
this_1 :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R)
    (hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x))
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), id (LocallyQuasiFinite f)
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
i : X.affineCover.I₀
x : ↥(Spec R)
this_2 : ∀ (x : ↥(Spec R)), IsLocallyArtinian.{u} (Hom.fiber f x)
g : Hom.fiber (X.affineCover.f i ≫ f) x ⟶ Hom.fiber f x :=
  pullback.map (X.affineCover.f i ≫ f) ((Spec R).fromSpecResidueField x) f ((Spec R).fromSpecResidueField x)
    (X.affineCover.f i) (𝟙 (Spec ((Spec R).residueField x))) (𝟙 (Spec R)) ⋯ ⋯
this : IsClosedImmersion g
⊢ LocallyQuasiFinite (g ≫ Hom.fiberToSpecResidueField f x)

Tactic:
(inferInstance : LocallyQuasiFinite <| g ≫ f.fiberToSpecResidueField _)

Premises used: inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
this_1 :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R)
    (hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x))
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), id (LocallyQuasiFinite f)
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
i : X.affineCover.I₀
x : ↥(Spec R)
this_2 : ∀ (x : ↥(Spec R)), IsLocallyArtinian.{u} (Hom.fiber f x)
g : Hom.fiber (X.affineCover.f i ≫ f) x ⟶ Hom.fiber f x :=
  pullback.map (X.affineCover.f i ≫ f) ((Spec R).fromSpecResidueField x) f ((Spec R).fromSpecResidueField x)
    (X.affineCover.f i) (𝟙 (Spec ((Spec R).residueField x))) (𝟙 (Spec R)) ⋯ ⋯
this : IsClosedImmersion g
h : Hom.fiberToSpecResidueField (X.affineCover.f i ≫ f) x = g ≫ Hom.fiberToSpecResidueField f x
⊢ LocallyQuasiFinite (Hom.fiberToSpecResidueField (X.affineCover.f i ≫ f) x)

Tactic:
convert! (inferInstance : LocallyQuasiFinite <| g ≫ f.fiberToSpecResidueField _) using 1

Premises used: inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
this_1 :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R)
    (hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x))
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), id (LocallyQuasiFinite f)
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
i : X.affineCover.I₀
x : ↥(Spec R)
this_2 : ∀ (x : ↥(Spec R)), IsLocallyArtinian.{u} (Hom.fiber f x)
g : Hom.fiber (X.affineCover.f i ≫ f) x ⟶ Hom.fiber f x :=
  pullback.map (X.affineCover.f i ≫ f) ((Spec R).fromSpecResidueField x) f ((Spec R).fromSpecResidueField x)
    (X.affineCover.f i) (𝟙 (Spec ((Spec R).residueField x))) (𝟙 (Spec R)) ⋯ ⋯
this : IsClosedImmersion g
⊢ Hom.fiberToSpecResidueField (X.affineCover.f i ≫ f) x = g ≫ Hom.fiberToSpecResidueField f x

Tactic:
simp [g, Hom.fiberToSpecResidueField]

Premises used: AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
hX : ∃ (S : CommRingCat.{u}), X = Spec S
obtain :
  ∀ (S : CommRingCat.{u}) (f : Spec S ⟶ Spec R)
    (hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField 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
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
obtain :
  ∀ (φ : R ⟶ S) (hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField (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
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField (Spec.map φ) x)
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
simp : (CommRingCat.Hom.hom φ).QuasiFinite
⊢ id (LocallyQuasiFinite (Spec.map φ))

Tactic:
simp only [HasRingHomProperty.Spec_iff, id_eq]

Premises used: AlgebraicGeometry.HasRingHomProperty.Spec_iff, id_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
⊢ (CommRingCat.Hom.hom φ).QuasiFinite

Tactic:
⟨fun P hP ↦ ?_⟩

Premises used: Algebra.QuasiFinite.mk, RingHom.QuasiFinite
-- 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
refine : ∀ (P : Ideal (↑R : Type u)) (hP : P.IsPrime), Module.Finite.{u, u} P.ResidueField (P.Fiber (↑S : Type u))
⊢ (CommRingCat.Hom.hom φ).QuasiFinite

Tactic:
refine ⟨fun P hP ↦ ?_⟩
-- 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
P : Ideal (↑R : Type u)
hP : P.IsPrime
this :
  LocallyQuasiFinite.{u} (X := Spec (CommRingCat.of (P.Fiber (↑S : Type u)))) (Y :=
    Spec (CommRingCat.of P.ResidueField))
    (Spec.map (CommRingCat.ofHom (algebraMap P.ResidueField (P.Fiber (↑S : Type u)))))
⊢ Algebra.QuasiFinite.{u, u} P.ResidueField (P.Fiber (↑S : Type u))

Tactic:
simp only [HasRingHomProperty.Spec_iff (P := @LocallyQuasiFinite), CommRingCat.hom_ofHom,
      RingHom.quasiFinite_algebraMap] at this

Premises used: RingHom.quasiFinite_algebraMap, CommRingCat.hom_ofHom, AlgebraicGeometry.HasRingHomProperty.Spec_iff
-- 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
P : Ideal (↑R : Type u)
hP : P.IsPrime
this : Algebra.QuasiFinite.{u, u} P.ResidueField (P.Fiber (↑S : Type u))
⊢ Module.Finite.{u, u} P.ResidueField (P.Fiber (↑S : Type u))

Tactic:
.of_quasiFinite

Premises used: Module.Finite.of_quasiFinite
-- 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
P : Ideal (↑R : Type u)
hP : P.IsPrime
this : Algebra.QuasiFinite.{u, u} P.ResidueField (P.Fiber (↑S : Type u))
⊢ Module.Finite.{u, u} P.ResidueField (P.Fiber (↑S : Type u))

Tactic:
exact .of_quasiFinite
-- 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
P : Ideal (↑R : Type u)
hP : P.IsPrime
suffices :
  LocallyQuasiFinite.{u} (X := Spec (CommRingCat.of (P.Fiber (↑S : Type u)))) (Y :=
    Spec (CommRingCat.of P.ResidueField))
    (Spec.map (CommRingCat.ofHom (algebraMap P.ResidueField (P.Fiber (↑S : Type u)))))
⊢ Module.Finite.{u, u} P.ResidueField (P.Fiber (↑S : Type u))

Tactic:
suffices LocallyQuasiFinite (Spec.map <|
      CommRingCat.ofHom <| algebraMap P.ResidueField (P.Fiber S)) by
    simp only [HasRingHomProperty.Spec_iff (P := @LocallyQuasiFinite), CommRingCat.hom_ofHom,
      RingHom.quasiFinite_algebraMap] at this
    exact .of_quasiFinite
-- 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
P : Ideal (↑R : Type u)
hP : P.IsPrime
⊢ ∃ (x : ↥(Spec R)), P = x.asIdeal

Tactic:
⟨⟨P, hP⟩, rfl⟩

Premises used: PrimeSpectrum.mk, Exists.intro, rfl
-- 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
P : Ideal (↑R : Type u)
hP : P.IsPrime
obtain :
  ∀ (x : ↥(Spec R)) (hP : x.asIdeal.IsPrime),
    LocallyQuasiFinite.{u} (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)))))
⊢ LocallyQuasiFinite.{u} (X := Spec (CommRingCat.of (P.Fiber (↑S : Type u)))) (Y :=
    Spec (CommRingCat.of P.ResidueField))
    (Spec.map (CommRingCat.ofHom (algebraMap P.ResidueField (P.Fiber (↑S : Type u)))))

Tactic:
obtain ⟨x, rfl⟩ : ∃ x : Spec R, P = x.asIdeal := ⟨⟨P, hP⟩, rfl⟩

Premises used: AlgebraicGeometry.Spec, rfl
-- 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
⊢ LocallyQuasiFinite.{u} (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)))))

Tactic:
(MorphismProperty.arrow_mk_iso_iff _ (Arrow.isoMk ?_ ?_ ?_)).mp (hf x)

Premises used: CategoryTheory.MorphismProperty.arrow_mk_iso_iff, Iff.mp, CategoryTheory.Arrow.isoMk
-- 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
refine_1 :
  (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
refine_2 :
  (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
refine_3 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ LocallyQuasiFinite.{u} (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)))))

Tactic:
refine (MorphismProperty.arrow_mk_iso_iff _ (Arrow.isoMk ?_ ?_ ?_)).mp (hf x)

Premises used: CategoryTheory.MorphismProperty.arrow_mk_iso_iff, Iff.mp, CategoryTheory.Arrow.isoMk
-- 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
refine_1 : Spec.map φ ≫ 𝟙 (Spec R) = 𝟙 (Spec S) ≫ Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))
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))
⊢ (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

Tactic:
refine asIso (pullback.map _ _ _ _ (𝟙 _) (Spec.map (Spec.residueFieldIso _ x).inv) (𝟙 _)
      ?_ ?_) ≪≫ pullbackSymmetry _ _ ≪≫ pullbackSpecIso ..

Premises used: CategoryTheory.Limits.pullbackSymmetry, AlgebraicGeometry.pullbackSpecIso, AlgebraicGeometry.Spec.map, CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.pullback.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
refine_1 : Spec.map φ = Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))
⊢ Spec.map φ ≫ 𝟙 (Spec R) = 𝟙 (Spec S) ≫ Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))

Tactic:
simp
-- 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.map φ = Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))

Tactic:
rfl