awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : (↑Γ(X, U) : Type u)
H :
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen f))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) x (X.basicOpen f) ⋯)
    0
s : Set (↑X.affineOpens : Type u)
hs : s.Finite
e : U = ⨆ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)
h₁ : ∀ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens) ≤ U
n : (i : (↑s : Type u)) → ℕ
hn :
  ∀ (i : (↑s : Type u)),
    HMul.hMul (β := (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
        (HPow.hPow (α := (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
                (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
              f :
            (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
          (n i))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
            x :
          (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u)) =
      0
this : Finite.{u + 1} (↑s : Type u)
val : Fintype (↑s : Type u)
⊢ f ^ Finset.sup Finset.univ n * x = 0
have h : ∀ (i : (↑s : Type u)),
  Eq (α := (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (homOfLE sorry).op) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
        (f ^ Finset.sup Finset.univ n * x) :
      (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
    (0 : (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
Tactic: suffices ∀ i : s, X.presheaf.map (homOfLE (h₁ i)).op (f ^ Finset.univ.sup n * x) = 0 by
    subst e
    apply TopCat.Sheaf.eq_of_locally_eq X.sheaf fun i : s => (i : X.Opens)
    intro i
    change _ = (X.sheaf.obj.map _) 0
    rw [map_zero]
    apply this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : (↑Γ(X, U) : Type u)
H :
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen f))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) x (X.basicOpen f) ⋯)
    0
s : Set (↑X.affineOpens : Type u)
hs : s.Finite
e : U = ⨆ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)
h₁ : ∀ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens) ≤ U
n : (i : (↑s : Type u)) → ℕ
this : Finite.{u + 1} (↑s : Type u)
val : Fintype (↑s : Type u)
i : (↑s : Type u)
hn :
  (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
        (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
      (f ^ (Finset.sup Finset.univ n - n i) * (f ^ n i * x)) =
    HMul.hMul (α := (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u)) (β :=
      (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
          (f ^ (Finset.sup Finset.univ n - n i)) :
        (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
      (0 : (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
⊢ Eq (α := (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
        (f ^ Finset.sup Finset.univ n * x) :
      (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
    (0 : (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
have h : ∀
  (hn :
    Eq (α := (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X.presheaf.map (homOfLE sorry).op) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
          (f ^ (Finset.sup Finset.univ n - n i + n i) * x) :
        (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
      (0 : (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))),
  n i ≤ Finset.sup Finset.univ n
Tactic: rwa [mul_zero, ← mul_assoc, ← pow_add, tsub_add_cancel_of_le] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u)
⊢ IsNilpotent f ↔ X.basicOpen f = ⊥
have refine : ∀ (hf : X.basicOpen f = ⊥), IsNilpotent f
Tactic: refine ⟨X.basicOpen_eq_bot_of_isNilpotent U f, fun hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u)
hf : X.basicOpen f = ⊥
⊢ X.basicOpen f ≤ ⊥
have rw : LE.le.{u} (α := X.Opens) ⊥ ⊥
Tactic: rw [hf]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (hypothesis)
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u)
hf : X.basicOpen f = ⊥
⊢ Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen f))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) 1 (X.basicOpen f) ⋯)
    0
have e : X.basicOpen f ≤ ⊥
Tactic: have e : X.basicOpen f ≤ ⊥ := by rw [hf]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u)
hf : X.basicOpen f = ⊥
e : X.basicOpen f ≤ ⊥
⊢ Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen f))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) 1 (X.basicOpen f) ⋯)
    0
have rw : Eq (α :=
  ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
    (X.presheaf.obj (op (X.basicOpen f))))
  (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
    CommRingCat.carrier)
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) (V := U) 1 ⊥ sorry)
    (X.basicOpen f) e)
  0
Tactic: rw [← TopCat.Presheaf.restrict_restrict e bot_le]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u)
hf : X.basicOpen f = ⊥
e : X.basicOpen f ≤ ⊥
⊢ Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen f))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier)
      (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) (V := U) 1 ⊥ ⋯)
      (X.basicOpen f) e)
    0
have rw : Eq (α :=
  ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
    (X.presheaf.obj (op (X.basicOpen f))))
  (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
    CommRingCat.carrier) 0 (X.basicOpen f) e)
  0
Tactic: rw [Subsingleton.eq_zero (1 |_ ⊥)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u)
hf : X.basicOpen f = ⊥
e : X.basicOpen f ≤ ⊥
⊢ Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen f))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) 0 (X.basicOpen f) e)
    0
have change : Eq (α := (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X.presheaf.map (homOfLE e).op) :
        (a : (↑(X.presheaf.obj (op ⊥)) : Type u)) → (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u))
      0 :
    (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u))
  (0 : (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u))
Tactic: change X.presheaf.map _ 0 = 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u)
hf : X.basicOpen f = ⊥
e : X.basicOpen f ≤ ⊥
⊢ Eq (α := (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (homOfLE e).op) :
          (a : (↑(X.presheaf.obj (op ⊥)) : Type u)) → (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u))
        0 :
      (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u))
    (0 : (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u))
have rw : Eq.{u + 1} (α := (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u)) 0 0
Tactic: rw [map_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (hypothesis)
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u)
hf : X.basicOpen f = ⊥
⊢ IsNilpotent f
have h : Eq (α :=
  ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
    (X.presheaf.obj (op (X.basicOpen f))))
  (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
    CommRingCat.carrier) 1 (X.basicOpen f) sorry)
  0
Tactic: have h : (1 : Γ(X, U)) |_ (X.basicOpen f) = 0 := by
    have e : X.basicOpen f ≤ ⊥ := by rw [hf]
    rw [← TopCat.Presheaf.restrict_restrict e bot_le]
    rw [Subsingleton.eq_zero (1 |_ ⊥)]
    change X.presheaf.map _ 0 = 0
    rw [map_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u)
hf : X.basicOpen f = ⊥
h :
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen f))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) 1 (X.basicOpen f) ⋯)
    0
⊢ IsNilpotent f
have obtain : ∀ (n : ℕ) (hn : f ^ n * 1 = 0), IsNilpotent f
Tactic: obtain ⟨n, hn⟩ := exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact X hU 1 f h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (hypothesis)
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u)
hf : X.basicOpen f = ⊥
h :
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen f))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) 1 (X.basicOpen f) ⋯)
    0
n : ℕ
hn : f ^ n * 1 = 0
⊢ IsNilpotent f
have hn₁ : f ^ n = 0
Tactic: rw [mul_one] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ @LocallyQuasiFinite = affineLocally fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.QuasiFinite
have h : ∀ ⦃X Y : Scheme.{u_1}⦄ (f : X ⟶ Y),
  LocallyQuasiFinite f ↔ affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.QuasiFinite) f
Tactic: ext X Y f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsFinite f
⊢ LocallyQuasiFinite f
have inst : targetAffineLocally
  (fun (X x : Scheme.{u}) (f : X ⟶ x) (x_1 : IsAffine x) ↦ IsAffine X ∧ (CommRingCat.Hom.hom (Hom.appTop f)).Finite) f
Tactic: rw [HasAffineProperty.eq_targetAffineLocally @IsFinite] at ‹IsFinite f›
Cleared hypotheses: inst
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst :
  targetAffineLocally
    (fun (X x : Scheme.{u}) (f : X ⟶ x) (x_1 : IsAffine x) ↦ IsAffine X ∧ (CommRingCat.Hom.hom (Hom.appTop f)).Finite) f
⊢ LocallyQuasiFinite f
have rw : affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.QuasiFinite) f
Tactic: rw [HasRingHomProperty.eq_affineLocally @LocallyQuasiFinite]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst :
  targetAffineLocally
    (fun (X x : Scheme.{u}) (f : X ⟶ x) (x_1 : IsAffine x) ↦ IsAffine X ∧ (CommRingCat.Hom.hom (Hom.appTop f)).Finite) f
⊢ affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.QuasiFinite) f
have refine : targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.QuasiFinite) f
Tactic: refine ((targetAffineLocally_affineAnd_eq_affineLocally
    RingHom.QuasiFinite.propertyIsLocal).le f ?_).2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
⊢ LocallyQuasiFinite f
have rw : LocallyQuasiFinite (Hom.liftCoborder f ≫ (Hom.coborderRange f).ι)
Tactic: rw [← f.liftCoborder_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
⊢ LocallyQuasiFinite (Hom.liftCoborder f ≫ (Hom.coborderRange f).ι)
have this : LocallyQuasiFinite (Hom.coborderRange f).ι
Tactic: have := HasRingHomProperty.of_isOpenImmersion (P := @LocallyQuasiFinite)
    RingHom.QuasiFinite.holdsForLocalizationAway.containsIdentities (f := f.coborderRange.ι)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyQuasiFinite f
inst_1 : IsLocallyArtinian Y
⊢ id (IsLocallyArtinian X)
have inr : ∀
  (this :
    ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyQuasiFinite f] [IsLocallyArtinian Y]
      (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), id (IsLocallyArtinian X))
  (hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R), id (IsLocallyArtinian X)
Tactic: wlog hY : ∃ R, Y = Spec R
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyQuasiFinite f
inst_1 : IsLocallyArtinian Y
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyQuasiFinite f] [IsLocallyArtinian Y]
        (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), id (IsLocallyArtinian X))
    (hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R), id (IsLocallyArtinian X)
⊢ id (IsLocallyArtinian X)
have wlog : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyQuasiFinite f] [IsLocallyArtinian Y]
  (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), id (IsLocallyArtinian X)
Tactic: wlog hY : ∃ R, Y = Spec R
Cleared hypotheses: X, Y, f, inst, inst_1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyQuasiFinite f
inst_1 : IsLocallyArtinian Y
hY : ∃ (R : CommRingCat.{u}), Y = Spec R
⊢ id (IsLocallyArtinian X)
have inr : ∀
  (this :
    ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyQuasiFinite f] [IsLocallyArtinian Y]
      (hY : ∃ (R : CommRingCat.{u}), Y = Spec R) (hX : ∃ (S : CommRingCat.{u}), X = Spec S), id (IsLocallyArtinian X))
  (hX : ¬∃ (S : CommRingCat.{u}), X = Spec S), id (IsLocallyArtinian X)
Tactic: wlog hX : ∃ S, X = Spec S
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyQuasiFinite f
inst_1 : IsLocallyArtinian Y
hY : ∃ (R : CommRingCat.{u}), Y = Spec R
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyQuasiFinite f] [IsLocallyArtinian Y]
        (hY : ∃ (R : CommRingCat.{u}), Y = Spec R) (hX : ∃ (S : CommRingCat.{u}), X = Spec S), id (IsLocallyArtinian X))
    (hX : ¬∃ (S : CommRingCat.{u}), X = Spec S), id (IsLocallyArtinian X)
⊢ id (IsLocallyArtinian X)
have wlog : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyQuasiFinite f] [IsLocallyArtinian Y] (hY : ∃ (R : CommRingCat.{u}), Y = Spec R)
  (hX : ∃ (S : CommRingCat.{u}), X = Spec S), id (IsLocallyArtinian X)
Tactic: wlog hX : ∃ S, X = Spec S
Cleared hypotheses: X, Y, f, inst, inst_1, hY
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
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
⊢ id (IsLocallyArtinian X)
have obtain : ∀ (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyQuasiFinite f] [IsLocallyArtinian.{u} (Spec R)],
  id (IsLocallyArtinian X)
Tactic: obtain ⟨R, rfl⟩ := hY
Cleared hypotheses: Y, f, inst, inst_1, hY
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
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)
⊢ id (IsLocallyArtinian X)
have obtain : ∀ (S : CommRingCat.{u}) (f : Spec S ⟶ Spec R) [LocallyQuasiFinite f], id (IsLocallyArtinian.{u} (Spec S))
Tactic: obtain ⟨S, rfl⟩ := hX
Cleared hypotheses: X, hX, f, inst
-- 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
⊢ id (IsLocallyArtinian.{u} (Spec S))
have obtain : ∀ (φ : R ⟶ S) [LocallyQuasiFinite (Spec.map φ)], id (IsLocallyArtinian.{u} (Spec S))
Tactic: obtain ⟨φ, rfl⟩ := Spec.map_surjective f
Cleared hypotheses: f, inst_1
-- 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 φ)
⊢ id (IsLocallyArtinian.{u} (Spec S))
have simp : IsArtinianRing.{u} (↑R : Type u) → (CommRingCat.Hom.hom φ).QuasiFinite → IsArtinianRing.{u} (↑S : Type u)
Tactic: simp only [isLocallyArtinianScheme_Spec, HasRingHomProperty.Spec_iff, id_eq] at *
Cleared hypotheses: inst, inst_1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (hypothesis)
Goal:
R S : CommRingCat
φ : R ⟶ S
inst : IsArtinianRing.{u} (↑R : Type u)
inst_1 : (CommRingCat.Hom.hom φ).QuasiFinite
⊢ IsArtinianRing.{u} (↑S : Type u)
have algebraizeInst : Algebra.QuasiFinite.{u, u} (↑R : Type u) (↑S : Type u)
Tactic: algebraize [φ.hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (hypothesis)
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)
⊢ IsArtinianRing.{u} (↑S : Type u)
have this : Module.Finite.{u, u} (↑R : Type u) (↑S : Type u)
Tactic: have : Module.Finite R S := .of_quasiFinite
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyQuasiFinite f
inst_1 : QuasiCompact f
inst_2 : IsLocallyArtinian Y
⊢ id (IsFinite f)
have 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)
Tactic: wlog hY : ∃ R, Y = Spec R
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : 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)
⊢ id (IsFinite f)
have wlog : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyQuasiFinite f] [QuasiCompact f] [IsLocallyArtinian Y]
  (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), id (IsFinite f)
Tactic: wlog hY : ∃ R, Y = Spec R
Cleared hypotheses: X, Y, f, inst, inst_1, inst_2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
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
⊢ id (IsFinite f)
have obtain : ∀ (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyQuasiFinite f] [QuasiCompact f] [IsLocallyArtinian.{u} (Spec R)],
  id (IsFinite f)
Tactic: obtain ⟨R, rfl⟩ := hY
Cleared hypotheses: Y, f, inst, inst_1, inst_2, hY
-- 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)
⊢ id (IsFinite f)
have 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)
Tactic: wlog hX : ∃ S, X = Spec S
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : 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)
⊢ id (IsFinite f)
have 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)
Tactic: wlog hX : ∃ S, X = Spec S
Cleared hypotheses: X, R, f, inst, inst_1, inst_2