awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (hypothesis)
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
⊢ id (IsFinite f)
have inst : IsArtinianScheme X
Tactic: have inst : IsArtinianScheme X :=
      { toIsLocallyArtinian := .of_locallyQuasiFinite f,
        toCompactSpace := QuasiCompact.compactSpace_of_compactSpace f }
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
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
⊢ id (IsFinite f)
have obtain : ∀ (S : CommRingCat.{u}) (f : Spec S ⟶ Spec R) [LocallyQuasiFinite f] [QuasiCompact f], id (IsFinite f)
Tactic: obtain ⟨S, rfl⟩ := hX
Cleared hypotheses: X, f, inst, inst_1, hX
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
R : CommRingCat
inst : IsLocallyArtinian.{u} (Spec R)
S : CommRingCat
f : Spec S ⟶ Spec R
inst_1 : LocallyQuasiFinite f
inst_2 : QuasiCompact f
⊢ id (IsFinite f)
have obtain : ∀ (φ : R ⟶ S) [LocallyQuasiFinite (Spec.map φ)] [QuasiCompact (Spec.map φ)], id (IsFinite (Spec.map φ))
Tactic: obtain ⟨φ, rfl⟩ := Spec.map_surjective f
Cleared hypotheses: f, inst_1, inst_2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
R : CommRingCat
inst : IsLocallyArtinian.{u} (Spec R)
S : CommRingCat
φ : R ⟶ S
inst_1 : LocallyQuasiFinite (Spec.map φ)
inst_2 : QuasiCompact (Spec.map φ)
⊢ id (IsFinite (Spec.map φ))
have simp : IsArtinianRing.{u} (↑R : Type u) → (CommRingCat.Hom.hom φ).QuasiFinite → (CommRingCat.Hom.hom φ).Finite
Tactic: simp only [isLocallyArtinianScheme_Spec, HasRingHomProperty.Spec_iff, id_eq,
    IsFinite.SpecMap_iff] at *
Cleared hypotheses: inst, inst_1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (hypothesis)
Goal:
R S : CommRingCat
φ : R ⟶ S
inst : QuasiCompact (Spec.map φ)
inst_1 : IsArtinianRing.{u} (↑R : Type u)
inst_2 : (CommRingCat.Hom.hom φ).QuasiFinite
⊢ (CommRingCat.Hom.hom φ).Finite
have algebraizeInst : Algebra.QuasiFinite.{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
hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
⊢ id (LocallyQuasiFinite f)
have 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)
Tactic: wlog hY : ∃ R, Y = Spec R
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
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)
⊢ id (LocallyQuasiFinite f)
have 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)
Tactic: wlog hY : ∃ R, Y = Spec R
Cleared hypotheses: X, Y, f, hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
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)
have 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)
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 (hypothesis)
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)
⊢ 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)
have this₁ : ∀ (x : ↥Y), IsLocallyArtinian.{u} (Hom.fiber f x)
Tactic: have (x : Y) : IsLocallyArtinian (f.fiber x) :=
      .of_locallyQuasiFinite (f.fiberToSpecResidueField x)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
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)
have 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))
Tactic: refine (MorphismProperty.cancel_right_of_respectsIso @LocallyQuasiFinite _
      (Spec.map ((Y.affineCover.f i).residueFieldMap _))).mp ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (hypothesis)
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) ⋯ ⋯
⊢ 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))
have this₁ : IsClosedImmersion g
Tactic: have : IsClosedImmersion g := .of_isPreimmersion _ (isClosed_discrete _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
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 (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))
have 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)
Tactic: convert! (inferInstance : LocallyQuasiFinite <| g ≫ f.fiberToSpecResidueField _) using 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
hY : ∃ (R : CommRingCat.{u}), Y = Spec R
⊢ id (LocallyQuasiFinite f)
have obtain : ∀ (R : CommRingCat.{u}) (f : X ⟶ Spec R) (hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)),
  id (LocallyQuasiFinite f)
Tactic: obtain ⟨R, rfl⟩ := hY
Cleared hypotheses: Y, f, hf, hY
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
⊢ id (LocallyQuasiFinite f)
have 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)
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
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)
⊢ id (LocallyQuasiFinite f)
have 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)
Tactic: wlog hX : ∃ S, X = Spec S
Cleared hypotheses: X, R, f, hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
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)
have inr : ∀ (i : X.affineCover.I₀) (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField (X.affineCover.f i ≫ f) x)
Tactic: refine (IsZariskiLocalAtSource.iff_of_openCover X.affineCover).mpr fun i ↦
      this _ _ (fun x ↦ ?_) ⟨_, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (hypothesis)
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)
⊢ LocallyQuasiFinite (Hom.fiberToSpecResidueField (X.affineCover.f i ≫ f) x)
have this₁ : ∀ (x : ↥(Spec R)), IsLocallyArtinian.{u} (Hom.fiber f x)
Tactic: have (x : _) : IsLocallyArtinian (f.fiber x) :=
      .of_locallyQuasiFinite (f.fiberToSpecResidueField x)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (hypothesis)
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)) ⋯ ⋯
⊢ LocallyQuasiFinite (Hom.fiberToSpecResidueField (X.affineCover.f i ≫ f) x)
have this₁ : IsClosedImmersion g
Tactic: have : IsClosedImmersion g := .of_isPreimmersion _ (isClosed_discrete _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
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 (Hom.fiberToSpecResidueField (X.affineCover.f i ≫ f) x)
have h : Hom.fiberToSpecResidueField (X.affineCover.f i ≫ f) x = g ≫ Hom.fiberToSpecResidueField f x
Tactic: convert! (inferInstance : LocallyQuasiFinite <| g ≫ f.fiberToSpecResidueField _) using 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
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
⊢ id (LocallyQuasiFinite f)
have obtain : ∀ (S : CommRingCat.{u}) (f : Spec S ⟶ Spec R)
  (hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)), id (LocallyQuasiFinite f)
Tactic: obtain ⟨S, rfl⟩ := hX
Cleared hypotheses: X, f, hf, hX
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
R S : CommRingCat
f : Spec S ⟶ Spec R
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
⊢ id (LocallyQuasiFinite f)
have obtain : ∀ (φ : R ⟶ S) (hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField (Spec.map φ) x)),
  id (LocallyQuasiFinite (Spec.map φ))
Tactic: obtain ⟨φ, rfl⟩ := Spec.map_surjective f
Cleared hypotheses: f, hf
-- 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
⊢ id (LocallyQuasiFinite (Spec.map φ))
have simp : (CommRingCat.Hom.hom φ).QuasiFinite
Tactic: simp only [HasRingHomProperty.Spec_iff, id_eq]
-- 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
⊢ (CommRingCat.Hom.hom φ).QuasiFinite
have refine : ∀ (P : Ideal (↑R : Type u)) (hP : P.IsPrime), Module.Finite.{u, u} P.ResidueField (P.Fiber (↑S : Type u))
Tactic: refine ⟨fun P hP ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (hypothesis)
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)))))
⊢ Module.Finite.{u, u} P.ResidueField (P.Fiber (↑S : Type u))
have this₁ : 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
Cleared hypotheses: this
-- 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
P : Ideal (↑R : Type u)
hP : P.IsPrime
⊢ Module.Finite.{u, u} P.ResidueField (P.Fiber (↑S : Type u))
have 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)))))
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
-- 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
P : Ideal (↑R : Type u)
hP : P.IsPrime
⊢ 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)))))
have 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)))))
Tactic: obtain ⟨x, rfl⟩ : ∃ x : Spec R, P = x.asIdeal := ⟨⟨P, hP⟩, rfl⟩
Cleared hypotheses: P, hP
-- 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
⊢ 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)))))
have 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
Tactic: refine (MorphismProperty.arrow_mk_iso_iff _ (Arrow.isoMk ?_ ?_ ?_)).mp (hf x)
-- 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 :
  (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
⊢ 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)))))
have 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
Tactic: refine (MorphismProperty.arrow_mk_iso_iff _ (Arrow.isoMk ?_ ?_ ?_)).mp (hf x)
-- 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 :
  (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
⊢ 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)))))
have refine_3 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: refine (MorphismProperty.arrow_mk_iso_iff _ (Arrow.isoMk ?_ ?_ ?_)).mp (hf x)
-- 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
⊢ (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.map φ ≫ 𝟙 (Spec R) = 𝟙 (Spec S) ≫ Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))
Tactic: refine asIso (pullback.map _ _ _ _ (𝟙 _) (Spec.map (Spec.residueFieldIso _ x).inv) (𝟙 _)
      ?_ ?_) ≪≫ pullbackSymmetry _ _ ≪≫ pullbackSpecIso ..