awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
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 :
  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 - 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:
apply Finset.le_sup (Finset.mem_univ i)

Premises used: Finset.mem_univ, Finset.le_sup
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u)
⊢ IsNilpotent f ↔ X.basicOpen f = ⊥

Tactic:
⟨X.basicOpen_eq_bot_of_isNilpotent U f, fun hf ↦ ?_⟩

Premises used: Iff.intro, AlgebraicGeometry.LocallyRingedSpace.basicOpen_eq_bot_of_isNilpotent, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u)
refine : ∀ (hf : X.basicOpen f = ⊥), IsNilpotent f
⊢ IsNilpotent f ↔ X.basicOpen f = ⊥

Tactic:
refine ⟨X.basicOpen_eq_bot_of_isNilpotent U f, fun hf ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u)
hf : X.basicOpen f = ⊥
rw rw₁ : LE.le.{u} (α := X.Opens) ⊥ ⊥
⊢ X.basicOpen f ≤ ⊥

Tactic:
rw [hf]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u)
hf : X.basicOpen f = ⊥
⊢ X.basicOpen f ≤ ⊥

Tactic:
have e : X.basicOpen f ≤ ⊥ := by rw [hf]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u)
hf : X.basicOpen f = ⊥
e : X.basicOpen f ≤ ⊥
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 ⊥ ⋯)
      (X.basicOpen f) e)
    0
⊢ 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

Tactic:
rw [← TopCat.Presheaf.restrict_restrict e bot_le]

Premises used: TopCat.Presheaf.restrict_restrict, bot_le
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u)
hf : X.basicOpen f = ⊥
e : X.basicOpen f ≤ ⊥
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
⊢ 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

Tactic:
rw [Subsingleton.eq_zero (1 |_ ⊥)]

Premises used: TopCat.Presheaf.restrictOpen, Bot.bot, Subsingleton.eq_zero, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u)
hf : X.basicOpen f = ⊥
e : X.basicOpen f ≤ ⊥
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))
⊢ 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:
change X.presheaf.map _ 0 = 0

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Functor.map, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, OfNat.ofNat, DFunLike.coe, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u)
hf : X.basicOpen f = ⊥
e : X.basicOpen f ≤ ⊥
rw rw₁ : Eq.{u + 1} (α := (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u)) 0 0
⊢ 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:
rw [map_zero]

Premises used: map_zero
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
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

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]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
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
obtain : ∀ (n : ℕ) (hn : f ^ n * 1 = 0), IsNilpotent f
⊢ IsNilpotent f

Tactic:
obtain ⟨n, hn⟩ := exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact X hU 1 f h

Premises used: AlgebraicGeometry.exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
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
⊢ f ^ n = 0

Tactic:
rw [mul_one] at hn

Premises used: mul_one
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
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 = 0
w : ℕ
h₁ : f ^ n = 0
⊢ IsNilpotent f

Tactic:
use n
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
inst : CompactSpace.{u} ↥X
f : (↑Γ(X, ⊤) : Type u)
⊢ IsNilpotent f ↔ X.basicOpen f = ⊥

Tactic:
isNilpotent_iff_basicOpen_eq_bot_of_isCompact (U := ⊤) (CompactSpace.isCompact_univ) f

Premises used: CompactSpace.isCompact_univ, AlgebraicGeometry.Scheme.isNilpotent_iff_basicOpen_eq_bot_of_isCompact
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
s : Set (↑Γ(X, U) : Type u)
⊢ X.zeroLocus s = Set.univ ↔ s ⊆ (↑(nilradical (↑Γ(X, U) : Type u)) : Set (↑Γ(X, U) : Type u))

Tactic:
simp [Scheme.zeroLocus_def, ← Scheme.isNilpotent_iff_basicOpen_eq_bot_of_isCompact hU,
    ← mem_nilradical, Set.subset_def]

Premises used: Set.subset_def, AlgebraicGeometry.Scheme.zeroLocus_def, AlgebraicGeometry.Scheme.isNilpotent_iff_basicOpen_eq_bot_of_isCompact, mem_nilradical
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
inst : CompactSpace.{u} ↥X
s : Set (↑Γ(X, ⊤) : Type u)
⊢ X.zeroLocus s = Set.univ ↔ s ⊆ (↑(nilradical (↑Γ(X, ⊤) : Type u)) : Set (↑Γ(X, ⊤) : Type u))

Tactic:
zeroLocus_eq_univ_iff_subset_nilradical_of_isCompact (U := ⊤) (CompactSpace.isCompact_univ) s

Premises used: CompactSpace.isCompact_univ, AlgebraicGeometry.Scheme.zeroLocus_eq_univ_iff_subset_nilradical_of_isCompact
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
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
⊢ @LocallyQuasiFinite = affineLocally fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.QuasiFinite

Tactic:
ext X Y f
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
⊢ LocallyQuasiFinite f ↔ affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.QuasiFinite) f

Tactic:
simp [locallyQuasiFinite_iff, affineLocally_iff_affineOpens_le, affineOpens]

Premises used: AlgebraicGeometry.locallyQuasiFinite_iff, AlgebraicGeometry.affineLocally_iff_affineOpens_le, AlgebraicGeometry.Scheme.affineOpens
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ MorphismProperty.IsStableUnderComposition @LocallyQuasiFinite

Tactic:
HasRingHomProperty.stableUnderComposition RingHom.QuasiFinite.stableUnderComposition

Premises used: RingHom.QuasiFinite.stableUnderComposition, AlgebraicGeometry.HasRingHomProperty.stableUnderComposition
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : LocallyQuasiFinite f
inst_1 : LocallyQuasiFinite g
⊢ LocallyQuasiFinite (f ≫ g)

Tactic:
MorphismProperty.comp_mem _ f g ‹_› ‹_›

Premises used: CategoryTheory.MorphismProperty.comp_mem
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsFinite f
⊢ 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›

Premises used: AlgebraicGeometry.IsFinite, AlgebraicGeometry.HasAffineProperty.eq_targetAffineLocally
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
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
rw : affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.QuasiFinite) f
⊢ LocallyQuasiFinite f

Tactic:
rw [HasRingHomProperty.eq_affineLocally @LocallyQuasiFinite]

Premises used: AlgebraicGeometry.HasRingHomProperty.eq_affineLocally, AlgebraicGeometry.LocallyQuasiFinite
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
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

Tactic:
((targetAffineLocally_affineAnd_eq_affineLocally
    RingHom.QuasiFinite.propertyIsLocal).le f ?_).2

Premises used: RingHom.QuasiFinite.propertyIsLocal, Eq.le, AlgebraicGeometry.targetAffineLocally_affineAnd_eq_affineLocally, And.right
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
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
refine : targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.QuasiFinite) f
⊢ affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.QuasiFinite) f

Tactic:
refine ((targetAffineLocally_affineAnd_eq_affineLocally
    RingHom.QuasiFinite.propertyIsLocal).le f ?_).2

Premises used: RingHom.QuasiFinite.propertyIsLocal, Eq.le, AlgebraicGeometry.targetAffineLocally_affineAnd_eq_affineLocally, And.right
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
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
⊢ targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.QuasiFinite) f

Tactic:
targetAffineLocally_affineAnd_le (fun hf ↦ .of_finite hf) f ‹_›

Premises used: AlgebraicGeometry.targetAffineLocally_affineAnd_le
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
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
⊢ targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.QuasiFinite) f

Tactic:
exact targetAffineLocally_affineAnd_le (fun hf ↦ .of_finite hf) f ‹_›

Premises used: AlgebraicGeometry.targetAffineLocally_affineAnd_le
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
rw : LocallyQuasiFinite (Hom.liftCoborder f ≫ (Hom.coborderRange f).ι)
⊢ LocallyQuasiFinite f

Tactic:
rw [← f.liftCoborder_ι]

Premises used: AlgebraicGeometry.Scheme.Hom.liftCoborder_ι
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
⊢ LocallyQuasiFinite (Hom.coborderRange f).ι

Tactic:
have := HasRingHomProperty.of_isOpenImmersion (P := @LocallyQuasiFinite)
    RingHom.QuasiFinite.holdsForLocalizationAway.containsIdentities (f := f.coborderRange.ι)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
this : LocallyQuasiFinite (Hom.coborderRange f).ι
⊢ LocallyQuasiFinite (Hom.liftCoborder f ≫ (Hom.coborderRange f).ι)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : LocallyQuasiFinite (f ≫ g)
⊢ LocallyQuasiFinite f

Tactic:
HasRingHomProperty.of_comp (fun _ _ ↦ RingHom.QuasiFinite.of_comp) ‹_›

Premises used: RingHom.QuasiFinite.of_comp, AlgebraicGeometry.HasRingHomProperty.of_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : LocallyQuasiFinite g
⊢ LocallyQuasiFinite (f ≫ g) ↔ LocallyQuasiFinite f

Tactic:
⟨fun _ ↦ .of_comp f g, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro, AlgebraicGeometry.LocallyQuasiFinite.of_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ MorphismProperty.IsStableUnderBaseChange @LocallyQuasiFinite

Tactic:
HasRingHomProperty.isStableUnderBaseChange RingHom.QuasiFinite.isStableUnderBaseChange

Premises used: AlgebraicGeometry.HasRingHomProperty.isStableUnderBaseChange, RingHom.QuasiFinite.isStableUnderBaseChange
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : LocallyQuasiFinite g
⊢ LocallyQuasiFinite (X := pullback f g) (pullback.fst f g)

Tactic:
MorphismProperty.pullback_fst f g inferInstance

Premises used: inferInstance, CategoryTheory.MorphismProperty.pullback_fst
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : LocallyQuasiFinite f
⊢ LocallyQuasiFinite (X := pullback f g) (pullback.snd f g)

Tactic:
MorphismProperty.pullback_snd f g inferInstance

Premises used: inferInstance, CategoryTheory.MorphismProperty.pullback_snd
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
V : Y.Opens
inst : LocallyQuasiFinite f
⊢ LocallyQuasiFinite (f ∣_ V)

Tactic:
IsZariskiLocalAtTarget.restrict ‹_› V

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.restrict
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
inst : LocallyQuasiFinite f
⊢ LocallyQuasiFinite (X.homOfLE e ≫ f ∣_ V)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ MorphismProperty.Respects (@LocallyQuasiFinite) IsOpenImmersion

Tactic:
HasRingHomProperty.respects_isOpenImmersion
  (RingHom.QuasiFinite.stableUnderComposition.stableUnderCompositionWithLocalizationAway
    RingHom.QuasiFinite.holdsForLocalizationAway).1

Premises used: RingHom.QuasiFinite.holdsForLocalizationAway, AlgebraicGeometry.HasRingHomProperty.respects_isOpenImmersion, RingHom.QuasiFinite.stableUnderComposition, And.left, RingHom.StableUnderComposition.stableUnderCompositionWithLocalizationAway
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
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)
wlog :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyQuasiFinite f] [IsLocallyArtinian Y]
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), id (IsLocallyArtinian X)
⊢ id (IsLocallyArtinian X)

Tactic:
wlog hY : ∃ R, Y = Spec R
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyQuasiFinite f
inst_1 : IsLocallyArtinian Y
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:
(isLocallyArtinian_iff_openCover (Y.affineCover.pullback₁ f)).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.isLocallyArtinian_iff_openCover, CategoryTheory.Precoverage.ZeroHypercover.pullback₁, 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 : IsLocallyArtinian Y
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:
exact (isLocallyArtinian_iff_openCover (Y.affineCover.pullback₁ f)).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.isLocallyArtinian_iff_openCover, CategoryTheory.Precoverage.ZeroHypercover.pullback₁, 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 : 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)
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)
⊢ id (IsLocallyArtinian X)

Tactic:
wlog hX : ∃ S, X = Spec S
-- 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
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:
(isLocallyArtinian_iff_openCover X.affineCover).mpr fun i ↦
      this (X.affineCover.f i ≫ f) hY ⟨_, rfl⟩

Premises used: Iff.mpr, CategoryTheory.PreZeroHypercover.f, Exists.intro, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.Scheme.affineCover._proof_7, Classical.choose, AlgebraicGeometry.isLocallyArtinian_iff_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 : IsLocallyArtinian Y
hY : ∃ (R : CommRingCat.{u}), Y = Spec R
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:
exact (isLocallyArtinian_iff_openCover X.affineCover).mpr fun i ↦
      this (X.affineCover.f i ≫ f) hY ⟨_, rfl⟩

Premises used: Iff.mpr, CategoryTheory.PreZeroHypercover.f, Exists.intro, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.Scheme.affineCover._proof_7, Classical.choose, AlgebraicGeometry.isLocallyArtinian_iff_openCover, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl