awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X_1 Y_1 S_1 : Scheme
f_1 : X_1 ⟶ S_1
inst : LocallyOfFiniteType f_1
X Y S : Scheme
f : X ⟶ Y
inst_1 : LocallyOfFiniteType f
inst_2 : IsSeparated f
inst_3 : QuasiCompact f
obtain :
  ∀ (U : (Scheme.Hom.normalization f).Opens)
    (hU : IsIso (X := (↑(Scheme.Hom.toNormalization f ⁻¹ᵁ U) : Scheme)) (Scheme.Hom.toNormalization f ∣_ U))
    (e : (Scheme.Hom.toNormalization f ⁻¹ᵁ U).carrier = {x : ↥X | Scheme.Hom.QuasiFiniteAt f x}),
    IsOpenImmersion (Y := Scheme.Hom.normalization f) ((Scheme.Hom.quasiFiniteLocus f).ι ≫ Scheme.Hom.toNormalization f)
⊢ IsOpenImmersion (Y := Scheme.Hom.normalization f) ((Scheme.Hom.quasiFiniteLocus f).ι ≫ Scheme.Hom.toNormalization f)

Tactic:
obtain ⟨U, hU, e⟩ := Scheme.Hom.exists_isIso_morphismRestrict_toNormalization f

Premises used: AlgebraicGeometry.Scheme.Hom.exists_isIso_morphismRestrict_toNormalization
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X_1 Y_1 S_1 : Scheme
f_1 : X_1 ⟶ S_1
inst : LocallyOfFiniteType f_1
X Y S : Scheme
f : X ⟶ Y
inst_1 : LocallyOfFiniteType f
inst_2 : IsSeparated f
inst_3 : QuasiCompact f
U : (Scheme.Hom.normalization f).Opens
hU : IsIso (X := (↑(Scheme.Hom.toNormalization f ⁻¹ᵁ U) : Scheme)) (Scheme.Hom.toNormalization f ∣_ U)
e : (Scheme.Hom.toNormalization f ⁻¹ᵁ U).carrier = {x : ↥X | Scheme.Hom.QuasiFiniteAt f x}
⊢ IsOpenImmersion (X := (↑(Scheme.Hom.quasiFiniteLocus f) : Scheme))
    (CategoryStruct.comp (Y := (↑(Scheme.Hom.toNormalization f ⁻¹ᵁ U) : Scheme)) (Iso.hom (X.isoOfEq ⋯))
      (Scheme.Hom.toNormalization f ∣_ U ≫ U.ι))

Tactic:
(inferInstance :
      IsOpenImmersion
        ((X.isoOfEq (U := f.quasiFiniteLocus) (SetLike.coe_injective e.symm)).hom ≫
          f.toNormalization ∣_ U ≫ U.ι))

Premises used: inferInstance
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X_1 Y_1 S_1 : Scheme
f_1 : X_1 ⟶ S_1
inst : LocallyOfFiniteType f_1
X Y S : Scheme
f : X ⟶ Y
inst_1 : LocallyOfFiniteType f
inst_2 : IsSeparated f
inst_3 : QuasiCompact f
U : (Scheme.Hom.normalization f).Opens
hU : IsIso (X := (↑(Scheme.Hom.toNormalization f ⁻¹ᵁ U) : Scheme)) (Scheme.Hom.toNormalization f ∣_ U)
e : (Scheme.Hom.toNormalization f ⁻¹ᵁ U).carrier = {x : ↥X | Scheme.Hom.QuasiFiniteAt f x}
h :
  (Scheme.Hom.quasiFiniteLocus f).ι ≫ Scheme.Hom.toNormalization f =
    CategoryStruct.comp (Y := (↑(Scheme.Hom.toNormalization f ⁻¹ᵁ U) : Scheme)) (Iso.hom (X.isoOfEq ⋯))
      (Scheme.Hom.toNormalization f ∣_ U ≫ U.ι)
⊢ IsOpenImmersion (Y := Scheme.Hom.normalization f) ((Scheme.Hom.quasiFiniteLocus f).ι ≫ Scheme.Hom.toNormalization f)

Tactic:
convert!
    (inferInstance :
      IsOpenImmersion
        ((X.isoOfEq (U := f.quasiFiniteLocus) (SetLike.coe_injective e.symm)).hom ≫
          f.toNormalization ∣_ U ≫ U.ι)) using 1

Premises used: inferInstance
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X_1 Y_1 S_1 : Scheme
f_1 : X_1 ⟶ S_1
inst : LocallyOfFiniteType f_1
X Y S : Scheme
f : X ⟶ Y
inst_1 : LocallyOfFiniteType f
inst_2 : IsSeparated f
inst_3 : QuasiCompact f
U : (Scheme.Hom.normalization f).Opens
hU : IsIso (X := (↑(Scheme.Hom.toNormalization f ⁻¹ᵁ U) : Scheme)) (Scheme.Hom.toNormalization f ∣_ U)
e : (Scheme.Hom.toNormalization f ⁻¹ᵁ U).carrier = {x : ↥X | Scheme.Hom.QuasiFiniteAt f x}
⊢ (Scheme.Hom.quasiFiniteLocus f).ι ≫ Scheme.Hom.toNormalization f =
    CategoryStruct.comp (Y := (↑(Scheme.Hom.toNormalization f ⁻¹ᵁ U) : Scheme)) (Iso.hom (X.isoOfEq ⋯))
      (Scheme.Hom.toNormalization f ∣_ U ≫ U.ι)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyQuasiFinite f
inst_1 : LocallyOfFiniteType f
⊢ quasiFiniteLocus f = ⊤

Tactic:
top_le_iff.mp fun x _ ↦ f.quasiFiniteAt x

Premises used: top_le_iff, Iff.mp, AlgebraicGeometry.Scheme.Hom.quasiFiniteAt
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
Z : Scheme
inst : IsOpenImmersion f
g : Y ⟶ Z
inst_1 : LocallyOfFiniteType g
h : ∀ (x : ↥X), x ∈ (↑(quasiFiniteLocus (f ≫ g)) : Set ↥X) ↔ x ∈ (↑(f ⁻¹ᵁ quasiFiniteLocus g) : Set ↥X)
⊢ quasiFiniteLocus (f ≫ g) = f ⁻¹ᵁ quasiFiniteLocus g

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
Z : Scheme
inst : IsOpenImmersion f
g : Y ⟶ Z
inst_1 : LocallyOfFiniteType g
x : ↥X
⊢ x ∈ (↑(quasiFiniteLocus (f ≫ g)) : Set ↥X) ↔ x ∈ (↑(f ⁻¹ᵁ quasiFiniteLocus g) : Set ↥X)

Tactic:
simp [quasiFiniteAt_comp_iff_of_isOpenImmersion]

Premises used: AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_comp_iff_of_isOpenImmersion
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
⊢ quasiFiniteLocus f = ⊤ ↔ LocallyQuasiFinite f

Tactic:
⟨fun H ↦ locallyQuasiFinite_iff_isDiscrete_preimage_singleton.mpr fun x ↦ ?_,
    fun _ ↦ f.quasiFiniteLocus_eq_top⟩

Premises used: Iff.mpr, AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus_eq_top, AlgebraicGeometry.locallyQuasiFinite_iff_isDiscrete_preimage_singleton, Iff.intro
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
refine : ∀ (H : quasiFiniteLocus f = ⊤) (x : ↥Y), _root_.IsDiscrete (X := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})
⊢ quasiFiniteLocus f = ⊤ ↔ LocallyQuasiFinite f

Tactic:
refine ⟨fun H ↦ locallyQuasiFinite_iff_isDiscrete_preimage_singleton.mpr fun x ↦ ?_,
    fun _ ↦ f.quasiFiniteLocus_eq_top⟩
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
H : quasiFiniteLocus f = ⊤
x : ↥Y
rw : ∀ (a : (↑(Set.preimage (β := ↥Y) ⇑f {x}) : Type u)), IsOpen (X := (↑(Set.preimage (β := ↥Y) ⇑f {x}) : Type u)) {a}
⊢ _root_.IsDiscrete (X := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})

Tactic:
rw [isDiscrete_iff_discreteTopology, discreteTopology_iff_isOpen_singleton]

Premises used: isDiscrete_iff_discreteTopology, discreteTopology_iff_isOpen_singleton
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
H : quasiFiniteLocus f = ⊤
a : ↥X
rw :
  IsOpen (X := ↥(fiber f (f a)))
    (singleton (α := ↥(fiber f (f a)))
      ((Homeomorph.symm (fiberHomeo f (f a)) : (a_1 : (↑(⇑f ⁻¹' {f a}) : Type u)) → ↥(fiber f (f a)))
          (Subtype.mk (p := fun (x : ↥X) ↦
            Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f a : ↥Y))) x) a ⋯) :
        ↥(fiber f (f a))))
⊢ IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f a : ↥Y))) : Type u))
    {Subtype.mk (p := fun (x : ↥X) ↦
        Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f a : ↥Y))) x) a ⋯}

Tactic:
rw [← (f.fiberHomeo _).symm.isOpen_image, Set.image_singleton]

Premises used: Set.image_singleton, AlgebraicGeometry.Scheme.Hom.fiberHomeo, Homeomorph.symm, Homeomorph.isOpen_image
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
H : quasiFiniteLocus f = ⊤
a : ↥X
⊢ IsOpen (X := ↥(fiber f (f a)))
    (singleton (α := ↥(fiber f (f a)))
      ((Homeomorph.symm (fiberHomeo f (f a)) : (a_1 : (↑(⇑f ⁻¹' {f a}) : Type u)) → ↥(fiber f (f a)))
          (Subtype.mk (p := fun (x : ↥X) ↦
            Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f a : ↥Y))) x) a ⋯) :
        ↥(fiber f (f a))))

Tactic:
(H.ge (Set.mem_univ a)).isClopen_singleton_asFiber.isOpen

Premises used: Eq.ge, AlgebraicGeometry.Scheme.Hom.asFiber, IsClopen.isOpen, Set.mem_univ, AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt.isClopen_singleton_asFiber
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
H : quasiFiniteLocus f = ⊤
a : ↥X
⊢ IsOpen (X := ↥(fiber f (f a)))
    (singleton (α := ↥(fiber f (f a)))
      ((Homeomorph.symm (fiberHomeo f (f a)) : (a_1 : (↑(⇑f ⁻¹' {f a}) : Type u)) → ↥(fiber f (f a)))
          (Subtype.mk (p := fun (x : ↥X) ↦
            Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f a : ↥Y))) x) a ⋯) :
        ↥(fiber f (f a))))

Tactic:
exact (H.ge (Set.mem_univ a)).isClopen_singleton_asFiber.isOpen

Premises used: Eq.ge, IsClopen.isOpen, Set.mem_univ, AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt.isClopen_singleton_asFiber
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X_1 Y_1 S_1 : Scheme
f_1 : X_1 ⟶ S_1
inst : LocallyOfFiniteType f_1
X Y S : Scheme
f : X ⟶ Y
inst_1 : LocallyOfFiniteType f
rw : Scheme.Hom.quasiFiniteLocus ((Scheme.Hom.quasiFiniteLocus f).ι ≫ f) = ⊤
rw₁ : (Scheme.Hom.quasiFiniteLocus f).ι ⁻¹ᵁ Scheme.Hom.quasiFiniteLocus f = ⊤
rw₂ rw₃ : Eq.{u + 1} (α := (↑(Scheme.Hom.quasiFiniteLocus f) : Scheme).Opens) ⊤ ⊤
⊢ LocallyQuasiFinite ((Scheme.Hom.quasiFiniteLocus f).ι ≫ f)

Tactic:
rw [← Scheme.Hom.quasiFiniteLocus_eq_top_iff, Scheme.Hom.quasiFiniteLocus_comp,
    Scheme.Opens.ι_preimage_self]

Premises used: AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus_comp, AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus_eq_top_iff, AlgebraicGeometry.Scheme.Opens.ι_preimage_self
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X_1 Y_1 S_1 : Scheme
f_1 : X_1 ⟶ S_1
inst : LocallyOfFiniteType f_1
X Y S : Scheme
f : X ⟶ Y
inst_1 : LocallyQuasiFinite f
inst_2 : LocallyOfFiniteType f
inst_3 : IsSeparated f
inst_4 : QuasiCompact f
⊢ IsOpenImmersion (Y := Scheme.Hom.normalization f)
    (X.topIso.inv ≫ Iso.inv (X.isoOfEq ⋯) ≫ (Scheme.Hom.quasiFiniteLocus f).ι ≫ Scheme.Hom.toNormalization f)

Tactic:
(inferInstance :
      IsOpenImmersion
        (X.topIso.inv ≫
          (X.isoOfEq f.quasiFiniteLocus_eq_top).inv ≫
            f.quasiFiniteLocus.ι ≫ f.toNormalization))

Premises used: inferInstance
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X_1 Y_1 S_1 : Scheme
f_1 : X_1 ⟶ S_1
inst : LocallyOfFiniteType f_1
X Y S : Scheme
f : X ⟶ Y
inst_1 : LocallyQuasiFinite f
inst_2 : LocallyOfFiniteType f
inst_3 : IsSeparated f
inst_4 : QuasiCompact f
h :
  Eq (α := X ⟶ Scheme.Hom.normalization f) (Scheme.Hom.toNormalization f)
    (X.topIso.inv ≫ Iso.inv (X.isoOfEq ⋯) ≫ (Scheme.Hom.quasiFiniteLocus f).ι ≫ Scheme.Hom.toNormalization f)
⊢ IsOpenImmersion (Y := Scheme.Hom.normalization f) (Scheme.Hom.toNormalization f)

Tactic:
convert!
    (inferInstance :
      IsOpenImmersion
        (X.topIso.inv ≫
          (X.isoOfEq f.quasiFiniteLocus_eq_top).inv ≫
            f.quasiFiniteLocus.ι ≫ f.toNormalization)) using 1

Premises used: inferInstance
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X_1 Y_1 S_1 : Scheme
f_1 : X_1 ⟶ S_1
inst : LocallyOfFiniteType f_1
X Y S : Scheme
f : X ⟶ Y
inst_1 : LocallyQuasiFinite f
inst_2 : LocallyOfFiniteType f
inst_3 : IsSeparated f
inst_4 : QuasiCompact f
⊢ Eq (α := X ⟶ Scheme.Hom.normalization f) (Scheme.Hom.toNormalization f)
    (X.topIso.inv ≫ Iso.inv (X.isoOfEq ⋯) ≫ (Scheme.Hom.quasiFiniteLocus f).ι ≫ Scheme.Hom.toNormalization f)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X_1 Y_1 S_1 : Scheme
f_1 : X_1 ⟶ S_1
inst : LocallyOfFiniteType f_1
X Y S : Scheme
f : X ⟶ Y
inst_1 : QuasiSeparated f
inst_2 : UniversallyClosed f
⊢ UniversallyClosed
    (CategoryStruct.comp (Y := Scheme.Hom.normalization f) (Scheme.Hom.toNormalization f)
      (Scheme.Hom.fromNormalization f))

Tactic:
simpa
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsProper f
inst_1 : LocallyQuasiFinite f
⊢ IsIso (Y := Scheme.Hom.normalization f) (Scheme.Hom.toNormalization f)

Tactic:
have : IsIso f.toNormalization :=
    (isIso_iff_isOpenImmersion_and_surjective _).mpr ⟨inferInstance, inferInstance⟩
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsProper f
inst_1 : LocallyQuasiFinite f
this : IsIso (Y := Scheme.Hom.normalization f) (Scheme.Hom.toNormalization f)
⊢ IsFinite f

Tactic:
(IsFinite.iff_isIntegralHom_and_locallyOfFiniteType _).mpr ⟨?_, inferInstance⟩

Premises used: Iff.mpr, inferInstance, And.intro, AlgebraicGeometry.IsFinite.iff_isIntegralHom_and_locallyOfFiniteType
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsProper f
inst_1 : LocallyQuasiFinite f
this : IsIso (Y := Scheme.Hom.normalization f) (Scheme.Hom.toNormalization f)
refine : IsIntegralHom f
⊢ IsFinite f

Tactic:
refine (IsFinite.iff_isIntegralHom_and_locallyOfFiniteType _).mpr ⟨?_, inferInstance⟩

Premises used: Iff.mpr, inferInstance, And.intro, AlgebraicGeometry.IsFinite.iff_isIntegralHom_and_locallyOfFiniteType
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsProper f
inst_1 : LocallyQuasiFinite f
this : IsIso (Y := Scheme.Hom.normalization f) (Scheme.Hom.toNormalization f)
rw :
  IsIntegralHom
    (CategoryStruct.comp (Y := Scheme.Hom.normalization f) (Scheme.Hom.toNormalization f)
      (Scheme.Hom.fromNormalization f))
⊢ IsIntegralHom f

Tactic:
rw [← f.toNormalization_fromNormalization]

Premises used: AlgebraicGeometry.Scheme.Hom.toNormalization_fromNormalization
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsProper f
inst_1 : LocallyQuasiFinite f
this : IsIso (Y := Scheme.Hom.normalization f) (Scheme.Hom.toNormalization f)
⊢ IsIntegralHom
    (CategoryStruct.comp (Y := Scheme.Hom.normalization f) (Scheme.Hom.toNormalization f)
      (Scheme.Hom.fromNormalization f))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsFinite f ↔ IsProper f ∧ LocallyQuasiFinite f

Tactic:
⟨fun _ ↦ ⟨inferInstance, inferInstance⟩,
    fun ⟨_, _⟩ ↦ .of_isProper_of_locallyQuasiFinite f⟩

Premises used: AlgebraicGeometry.IsFinite.of_isProper_of_locallyQuasiFinite, AlgebraicGeometry.IsFinite, inferInstance, _private.0.AlgebraicGeometry.IsFinite.iff_isProper_and_locallyQuasiFinite.match_1, And.intro, Iff.intro
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsFinite f ↔ IsProper f ∧ LocallyQuasiFinite f

Tactic:
refine ⟨fun _ ↦ ⟨inferInstance, inferInstance⟩,
    fun ⟨_, _⟩ ↦ .of_isProper_of_locallyQuasiFinite f⟩
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
h : ∀ (x x_1 : Scheme.{u_1}) (x_2 : x ⟶ x_1), IsFinite x_2 ↔ (@IsProper ⊓ @LocallyQuasiFinite) x_2
⊢ @IsFinite = @IsProper ⊓ @LocallyQuasiFinite

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
x x_1 : Scheme
x_2 : x ⟶ x_1
⊢ IsFinite x_2 ↔ (@IsProper ⊓ @LocallyQuasiFinite) x_2

Tactic:
IsFinite.iff_isProper_and_locallyQuasiFinite ..

Premises used: AlgebraicGeometry.IsFinite.iff_isProper_and_locallyQuasiFinite
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
x x_1 : Scheme
x_2 : x ⟶ x_1
⊢ IsFinite x_2 ↔ (@IsProper ⊓ @LocallyQuasiFinite) x_2

Tactic:
exact IsFinite.iff_isProper_and_locallyQuasiFinite ..

Premises used: AlgebraicGeometry.IsFinite.iff_isProper_and_locallyQuasiFinite
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ Mono f → IsProper f → LocallyQuasiFinite f

Tactic:
have (_ : Mono f) (_ : IsProper f) : LocallyQuasiFinite f := inferInstance
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
this : Mono f → IsProper f → LocallyQuasiFinite f
rw : (IsProper f ∧ LocallyQuasiFinite f) ∧ Mono f ↔ IsProper f ∧ Mono f
⊢ IsClosedImmersion f ↔ IsProper f ∧ Mono f

Tactic:
rw [IsClosedImmersion.iff_isFinite_and_mono, IsFinite.iff_isProper_and_locallyQuasiFinite]

Premises used: AlgebraicGeometry.IsClosedImmersion.iff_isFinite_and_mono, AlgebraicGeometry.IsFinite.iff_isProper_and_locallyQuasiFinite
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
this : Mono f → IsProper f → LocallyQuasiFinite f
⊢ (IsProper f ∧ LocallyQuasiFinite f) ∧ Mono f ↔ IsProper f ∧ Mono f

Tactic:
aesop
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
h :
  ∀ (x x_1 : Scheme.{u_1}) (x_2 : x ⟶ x_1),
    IsClosedImmersion x_2 ↔ (@IsProper ⊓ MorphismProperty.monomorphisms Scheme) x_2
⊢ @IsClosedImmersion = @IsProper ⊓ MorphismProperty.monomorphisms Scheme

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
x x_1 : Scheme
x_2 : x ⟶ x_1
⊢ IsClosedImmersion x_2 ↔ (@IsProper ⊓ MorphismProperty.monomorphisms Scheme) x_2

Tactic:
IsClosedImmersion.iff_isProper_and_mono ..

Premises used: AlgebraicGeometry.IsClosedImmersion.iff_isProper_and_mono
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
x x_1 : Scheme
x_2 : x ⟶ x_1
⊢ IsClosedImmersion x_2 ↔ (@IsProper ⊓ MorphismProperty.monomorphisms Scheme) x_2

Tactic:
exact IsClosedImmersion.iff_isProper_and_mono ..

Premises used: AlgebraicGeometry.IsClosedImmersion.iff_isProper_and_mono
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsProper f
y : ↥Y
hx : Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {y})
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f) : Set ↥X)ᶜ)ᶜ, is_open' := ⋯ }
⊢ ∃ (V : Y.Opens), y ∈ V ∧ IsFinite (f ∣_ V)

Tactic:
⟨V, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsProper f
y : ↥Y
hx : Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {y})
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f) : Set ↥X)ᶜ)ᶜ, is_open' := ⋯ }
refine_1 : y ∈ V
refine_2 : IsFinite (f ∣_ V)
⊢ ∃ (V : Y.Opens), y ∈ V ∧ IsFinite (f ∣_ V)

Tactic:
refine ⟨V, ?_, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsProper f
y : ↥Y
hx : Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {y})
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f) : Set ↥X)ᶜ)ᶜ, is_open' := ⋯ }
this : ∀ (x : ↥X), f x = y → Scheme.Hom.QuasiFiniteAt f x
⊢ y ∈ V

Tactic:
simpa [V, not_imp_not]

Premises used: not_imp_not
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsProper f
y : ↥Y
hx : Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {y})
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f) : Set ↥X)ᶜ)ᶜ, is_open' := ⋯ }
refine_1 : ∀ (x : ↥X), f x = y → Scheme.Hom.QuasiFiniteAt f x
⊢ y ∈ V

Tactic:
suffices ∀ x, f x = y → f.QuasiFiniteAt x by simpa [V, not_imp_not]
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsProper f
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f) : Set ↥X)ᶜ)ᶜ, is_open' := ⋯ }
x : ↥X
hx : Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y)))
⊢ Finite.{u + 1} ↥(Scheme.Hom.fiber f (f x))

Tactic:
have : Finite (f.fiber (f x)) := (f.fiberHomeo (f x)).finite_iff.mpr ‹_›
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsProper f
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f) : Set ↥X)ᶜ)ᶜ, is_open' := ⋯ }
x : ↥X
hx : Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y)))
this : Finite.{u + 1} ↥(Scheme.Hom.fiber f (f x))
⊢ Scheme.Hom.QuasiFiniteAt f x

Tactic:
Scheme.Hom.quasiFiniteAt_iff_isOpen_singleton_asFiber.mpr (isOpen_discrete _)

Premises used: Iff.mpr, isOpen_discrete, AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_iff_isOpen_singleton_asFiber
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsProper f
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f) : Set ↥X)ᶜ)ᶜ, is_open' := ⋯ }
x : ↥X
hx : Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y)))
this : Finite.{u + 1} ↥(Scheme.Hom.fiber f (f x))
⊢ Scheme.Hom.QuasiFiniteAt f x

Tactic:
exact Scheme.Hom.quasiFiniteAt_iff_isOpen_singleton_asFiber.mpr (isOpen_discrete _)

Premises used: Iff.mpr, isOpen_discrete, AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_iff_isOpen_singleton_asFiber
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsProper f
y : ↥Y
hx : Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {y})
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f) : Set ↥X)ᶜ)ᶜ, is_open' := ⋯ }
refine_2 : LocallyQuasiFinite (f ∣_ V)
⊢ IsFinite (f ∣_ V)

Tactic:
suffices LocallyQuasiFinite (f ∣_ V) from .of_isProper_of_locallyQuasiFinite _
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsProper f
y : ↥Y
hx : Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {y})
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f) : Set ↥X)ᶜ)ᶜ, is_open' := ⋯ }
refine_2 : Scheme.Hom.quasiFiniteLocus (f ∣_ V) = ⊤
⊢ LocallyQuasiFinite (f ∣_ V)

Tactic:
rw [← Scheme.Hom.quasiFiniteLocus_eq_top_iff]

Premises used: AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus_eq_top_iff
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsProper f
y : ↥Y
hx : Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {y})
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f) : Set ↥X)ᶜ)ᶜ, is_open' := ⋯ }
refine_2 :
  ∀ (x : ↥(↑(f ⁻¹ᵁ V) : Scheme)),
    x ∈ (↑(Scheme.Hom.quasiFiniteLocus (f ∣_ V)) : Set ↥(↑(f ⁻¹ᵁ V) : Scheme)) ↔ x ∈ (↑⊤ : Set ↥(↑(f ⁻¹ᵁ V) : Scheme))
⊢ Scheme.Hom.quasiFiniteLocus (f ∣_ V) = ⊤

Tactic:
ext x
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsProper f
y : ↥Y
hx : Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {y})
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f) : Set ↥X)ᶜ)ᶜ, is_open' := ⋯ }
x : ↥(↑(f ⁻¹ᵁ V) : Scheme)
by_contra : ∀ (H : ¬Scheme.Hom.QuasiFiniteAt f ((f ⁻¹ᵁ V).ι x)), False
⊢ Scheme.Hom.QuasiFiniteAt f ((f ⁻¹ᵁ V).ι x)

Tactic:
by_contra H
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsProper f
y : ↥Y
hx : Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {y})
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f) : Set ↥X)ᶜ)ᶜ, is_open' := ⋯ }
x : ↥(↑(f ⁻¹ᵁ V) : Scheme)
H : ¬Scheme.Hom.QuasiFiniteAt f ((f ⁻¹ᵁ V).ι x)
⊢ Eq (α := ↥Y) (f ((f ⁻¹ᵁ V).ι x : ↥X) : ↥Y) (f (↑x : ↥X) : ↥Y)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsProper f
y : ↥Y
hx : Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {y})
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f) : Set ↥X)ᶜ)ᶜ, is_open' := ⋯ }
x : ↥(↑(f ⁻¹ᵁ V) : Scheme)
H : ¬Scheme.Hom.QuasiFiniteAt f ((f ⁻¹ᵁ V).ι x)
⊢ False

Tactic:
exact x.2 ⟨_, H, by simp⟩

Premises used: And.intro, Exists.intro, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsProper f
y : ↥Y
hx : Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {y})
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f) : Set ↥X)ᶜ)ᶜ, is_open' := ⋯ }
x : ↥(↑(f ⁻¹ᵁ V) : Scheme)
⊢ Scheme.Hom.QuasiFiniteAt f ((f ⁻¹ᵁ V).ι x)

Tactic:
have : f.QuasiFiniteAt ((f ⁻¹ᵁ V).ι x) := by by_contra H; exact x.2 ⟨_, H, by simp⟩
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsProper f
y : ↥Y
hx : Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {y})
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f) : Set ↥X)ᶜ)ᶜ, is_open' := ⋯ }
x : ↥(↑(f ⁻¹ᵁ V) : Scheme)
this : Scheme.Hom.QuasiFiniteAt f ((f ⁻¹ᵁ V).ι x)
⊢ Scheme.Hom.QuasiFiniteAt (f ∣_ V) x

Tactic:
rw [← Scheme.Hom.quasiFiniteAt_comp_iff_of_isOpenImmersion, ← morphismRestrict_ι,
      Scheme.Hom.quasiFiniteAt_comp_iff] at this

Premises used: AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_comp_iff_of_isOpenImmersion, AlgebraicGeometry.morphismRestrict_ι, AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_comp_iff
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsProper f
y : ↥Y
hx : Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {y})
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f) : Set ↥X)ᶜ)ᶜ, is_open' := ⋯ }
x : ↥(↑(f ⁻¹ᵁ V) : Scheme)
this : Scheme.Hom.QuasiFiniteAt (f ∣_ V) x
⊢ x ∈ (↑(Scheme.Hom.quasiFiniteLocus (f ∣_ V)) : Set ↥(↑(f ⁻¹ᵁ V) : Scheme)) ↔ x ∈ (↑⊤ : Set ↥(↑(f ⁻¹ᵁ V) : Scheme))

Tactic:
simpa