awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
inst_1 : IsSeparated f
inst_2 : QuasiCompact f
x : ↥X
hx : QuasiFiniteAt f x
T : Scheme
fT : T ⟶ Y
left : Etale fT
u : ↥T
hu : Eq (α := ↥Y) (fT u : ↥Y) (f x : ↥Y)
V W : (pullback f fT).Opens
v : ↥V
hVW : IsCompl V W
left_1 : IsFinite (V.ι ≫ pullback.snd f fT)
hv₂ : (pullback.fst f fT) (↑v : ↥(pullback f fT)) = x
U : (normalization (X := pullback f fT) (pullback.snd f fT)).Opens
hU :
  Membership.mem (α := ↥(normalization (X := pullback f fT) (pullback.snd f fT))) U
    ((toNormalization (pullback.snd f fT)) (↑v : ↥(pullback f fT)) :
      ↥(normalization (X := pullback f fT) (pullback.snd f fT)))
right : IsIso (X := (↑(toNormalization (pullback.snd f fT) ⁻¹ᵁ U) : Scheme)) (toNormalization (pullback.snd f fT) ∣_ U)
fTn : normalization (X := pullback f fT) (pullback.snd f fT) ⟶ normalization f :=
  normalizationPullback f fT ≫ pullback.fst (fromNormalization f) fT
U' : (normalization f).Opens := { carrier := ⇑fTn '' U.carrier, is_open' := ⋯ }
fTnU : (↑U : Scheme) ⟶ (↑U' : Scheme) := resLE fTn U' U ⋯
this : Surjective fTnU
H_1 : toNormalization (pullback.snd f fT) ⁻¹ᵁ U ≤ pullback.fst f fT ⁻¹ᵁ toNormalization f ⁻¹ᵁ U'
H :
  IsPullback (P := pullback f fT) (X := pullback (X := normalization f) (fromNormalization f) fT)
    (pullback.map f fT (fromNormalization f) fT (toNormalization f) (𝟙 T) (𝟙 Y) ⋯ ⋯) (pullback.fst f fT)
    (pullback.fst (fromNormalization f) fT) (toNormalization f)
⊢ Iso.hom (Iso.refl X) ≫ toNormalization f = toNormalization f ≫ Iso.hom (Iso.refl (normalization f))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
inst_1 : IsSeparated f
inst_2 : QuasiCompact f
x : ↥X
hx : QuasiFiniteAt f x
T : Scheme
fT : T ⟶ Y
left : Etale fT
u : ↥T
hu : Eq (α := ↥Y) (fT u : ↥Y) (f x : ↥Y)
V W : (pullback f fT).Opens
v : ↥V
hVW : IsCompl V W
left_1 : IsFinite (V.ι ≫ pullback.snd f fT)
hv₂ : (pullback.fst f fT) (↑v : ↥(pullback f fT)) = x
U : (normalization (X := pullback f fT) (pullback.snd f fT)).Opens
hU :
  Membership.mem (α := ↥(normalization (X := pullback f fT) (pullback.snd f fT))) U
    ((toNormalization (pullback.snd f fT)) (↑v : ↥(pullback f fT)) :
      ↥(normalization (X := pullback f fT) (pullback.snd f fT)))
right : IsIso (X := (↑(toNormalization (pullback.snd f fT) ⁻¹ᵁ U) : Scheme)) (toNormalization (pullback.snd f fT) ∣_ U)
fTn : normalization (X := pullback f fT) (pullback.snd f fT) ⟶ normalization f :=
  normalizationPullback f fT ≫ pullback.fst (fromNormalization f) fT
U' : (normalization f).Opens := { carrier := ⇑fTn '' U.carrier, is_open' := ⋯ }
fTnU : (↑U : Scheme) ⟶ (↑U' : Scheme) := resLE fTn U' U ⋯
this : Surjective fTnU
H_1 : toNormalization (pullback.snd f fT) ⁻¹ᵁ U ≤ pullback.fst f fT ⁻¹ᵁ toNormalization f ⁻¹ᵁ U'
H :
  IsPullback (P := pullback f fT) (X := pullback (X := normalization f) (fromNormalization f) fT)
    (pullback.map f fT (fromNormalization f) fT (toNormalization f) (𝟙 T) (𝟙 Y) ⋯ ⋯) (pullback.fst f fT)
    (pullback.fst (fromNormalization f) fT) (toNormalization f)
⊢ IsPullback (toNormalization (pullback.snd f fT)) (pullback.fst f fT) fTn (toNormalization f)

Tactic:
exact .of_iso' H (.refl _) (asIso <| f.normalizationPullback fT) (.refl _) (.refl _)
        (by cat_disch) (by simp) (by simp [fTn]) (by simp)
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
inst_1 : IsSeparated f
inst_2 : QuasiCompact f
x : ↥X
hx : QuasiFiniteAt f x
T : Scheme
fT : T ⟶ Y
left : Etale fT
u : ↥T
hu : Eq (α := ↥Y) (fT u : ↥Y) (f x : ↥Y)
V W : (pullback f fT).Opens
v : ↥V
hVW : IsCompl V W
left_1 : IsFinite (V.ι ≫ pullback.snd f fT)
hv₂ : (pullback.fst f fT) (↑v : ↥(pullback f fT)) = x
U : (normalization (X := pullback f fT) (pullback.snd f fT)).Opens
hU :
  Membership.mem (α := ↥(normalization (X := pullback f fT) (pullback.snd f fT))) U
    ((toNormalization (pullback.snd f fT)) (↑v : ↥(pullback f fT)) :
      ↥(normalization (X := pullback f fT) (pullback.snd f fT)))
right : IsIso (X := (↑(toNormalization (pullback.snd f fT) ⁻¹ᵁ U) : Scheme)) (toNormalization (pullback.snd f fT) ∣_ U)
fTn : normalization (X := pullback f fT) (pullback.snd f fT) ⟶ normalization f :=
  normalizationPullback f fT ≫ pullback.fst (fromNormalization f) fT
U' : (normalization f).Opens := { carrier := ⇑fTn '' U.carrier, is_open' := ⋯ }
fTnU : (↑U : Scheme) ⟶ (↑U' : Scheme) := resLE fTn U' U ⋯
this : Surjective fTnU
H : toNormalization (pullback.snd f fT) ⁻¹ᵁ U ≤ pullback.fst f fT ⁻¹ᵁ toNormalization f ⁻¹ᵁ U'
⊢ toNormalization (pullback.snd f fT) ∣_ U ≫ fTnU =
    resLE (pullback.fst f fT) (toNormalization f ⁻¹ᵁ U') (toNormalization (pullback.snd f fT) ⁻¹ᵁ U) H ≫
      toNormalization f ∣_ U'

Tactic:
simp [← cancel_mono U'.ι, fTnU, fTn]

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
inst_1 : IsSeparated f
inst_2 : QuasiCompact f
x : ↥X
hx : QuasiFiniteAt f x
T : Scheme
fT : T ⟶ Y
left : Etale fT
u : ↥T
hu : Eq (α := ↥Y) (fT u : ↥Y) (f x : ↥Y)
V W : (pullback f fT).Opens
v : ↥V
hVW : IsCompl V W
left_1 : IsFinite (V.ι ≫ pullback.snd f fT)
hv₂ : (pullback.fst f fT) (↑v : ↥(pullback f fT)) = x
U : (normalization (X := pullback f fT) (pullback.snd f fT)).Opens
hU :
  Membership.mem (α := ↥(normalization (X := pullback f fT) (pullback.snd f fT))) U
    ((toNormalization (pullback.snd f fT)) (↑v : ↥(pullback f fT)) :
      ↥(normalization (X := pullback f fT) (pullback.snd f fT)))
right : IsIso (X := (↑(toNormalization (pullback.snd f fT) ⁻¹ᵁ U) : Scheme)) (toNormalization (pullback.snd f fT) ∣_ U)
fTn : normalization (X := pullback f fT) (pullback.snd f fT) ⟶ normalization f :=
  normalizationPullback f fT ≫ pullback.fst (fromNormalization f) fT
U' : (normalization f).Opens := { carrier := ⇑fTn '' U.carrier, is_open' := ⋯ }
fTnU : (↑U : Scheme) ⟶ (↑U' : Scheme) := resLE fTn U' U ⋯
this : Surjective fTnU
H : toNormalization (pullback.snd f fT) ⁻¹ᵁ U ≤ pullback.fst f fT ⁻¹ᵁ toNormalization f ⁻¹ᵁ U'
⊢ IsPullback (toNormalization (pullback.snd f fT) ∣_ U)
    (resLE (pullback.fst f fT) (toNormalization f ⁻¹ᵁ U') (toNormalization (pullback.snd f fT) ⁻¹ᵁ U) H) fTnU
    (toNormalization f ∣_ U')

Tactic:
have : IsPullback ((pullback.snd f fT).toNormalization ∣_ U)
      ((pullback.fst f fT).resLE _ _ H) fTnU (f.toNormalization ∣_ U') := by
    refine .of_bot (t := isPullback_morphismRestrict ..) ?_ ?_
    · simp only [Scheme.Hom.resLE_comp_ι, fTnU]
      refine .paste_vert (isPullback_morphismRestrict ..) ?_
      have H : IsPullback (pullback.map _ _ _ _ f.toNormalization (𝟙 _) (𝟙 _) (by simp) (by simp))
          (pullback.fst f fT) (pullback.fst f.fromNormalization fT) f.toNormalization :=
        .of_right (t := .flip <| .of_hasPullback ..)
          (by simpa using (.flip <| .of_hasPullback ..)) (by cat_disch)
      exact .of_iso' H (.refl _) (asIso <| f.normalizationPullback fT) (.refl _) (.refl _)
        (by cat_disch) (by simp) (by simp [fTn]) (by simp)
    · simp [← cancel_mono U'.ι, fTnU, fTn]
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
inst_1 : IsSeparated f
inst_2 : QuasiCompact f
x : ↥X
hx : QuasiFiniteAt f x
T : Scheme
fT : T ⟶ Y
left : Etale fT
u : ↥T
hu : Eq (α := ↥Y) (fT u : ↥Y) (f x : ↥Y)
V W : (pullback f fT).Opens
v : ↥V
hVW : IsCompl V W
left_1 : IsFinite (V.ι ≫ pullback.snd f fT)
hv₂ : (pullback.fst f fT) (↑v : ↥(pullback f fT)) = x
U : (normalization (X := pullback f fT) (pullback.snd f fT)).Opens
hU :
  Membership.mem (α := ↥(normalization (X := pullback f fT) (pullback.snd f fT))) U
    ((toNormalization (pullback.snd f fT)) (↑v : ↥(pullback f fT)) :
      ↥(normalization (X := pullback f fT) (pullback.snd f fT)))
right : IsIso (X := (↑(toNormalization (pullback.snd f fT) ⁻¹ᵁ U) : Scheme)) (toNormalization (pullback.snd f fT) ∣_ U)
fTn : normalization (X := pullback f fT) (pullback.snd f fT) ⟶ normalization f :=
  normalizationPullback f fT ≫ pullback.fst (fromNormalization f) fT
U' : (normalization f).Opens := { carrier := ⇑fTn '' U.carrier, is_open' := ⋯ }
fTnU : (↑U : Scheme) ⟶ (↑U' : Scheme) := resLE fTn U' U ⋯
this_1 : Surjective fTnU
H : toNormalization (pullback.snd f fT) ⁻¹ᵁ U ≤ pullback.fst f fT ⁻¹ᵁ toNormalization f ⁻¹ᵁ U'
this :
  IsPullback (toNormalization (pullback.snd f fT) ∣_ U)
    (resLE (pullback.fst f fT) (toNormalization f ⁻¹ᵁ U') (toNormalization (pullback.snd f fT) ⁻¹ᵁ U) H) fTnU
    (toNormalization f ∣_ U')
⊢ IsIso (X := (↑(toNormalization f ⁻¹ᵁ U') : Scheme)) (toNormalization f ∣_ U')

Tactic:
MorphismProperty.of_isPullback_of_descendsAlong (P := .isomorphisms _)
    (Q := @Surjective ⊓ @Flat ⊓ @LocallyOfFinitePresentation) this
    ⟨⟨‹_›, inferInstance⟩, inferInstance⟩ ‹_›

Premises used: CategoryTheory.MorphismProperty.of_isPullback_of_descendsAlong, inferInstance, And.intro
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
inst_1 : IsSeparated f
inst_2 : QuasiCompact f
x : ↥X
hx : QuasiFiniteAt f x
T : Scheme
fT : T ⟶ Y
left : Etale fT
u : ↥T
hu : Eq (α := ↥Y) (fT u : ↥Y) (f x : ↥Y)
V W : (pullback f fT).Opens
v : ↥V
hVW : IsCompl V W
left_1 : IsFinite (V.ι ≫ pullback.snd f fT)
hv₂ : (pullback.fst f fT) (↑v : ↥(pullback f fT)) = x
U : (normalization (X := pullback f fT) (pullback.snd f fT)).Opens
hU :
  Membership.mem (α := ↥(normalization (X := pullback f fT) (pullback.snd f fT))) U
    ((toNormalization (pullback.snd f fT)) (↑v : ↥(pullback f fT)) :
      ↥(normalization (X := pullback f fT) (pullback.snd f fT)))
right : IsIso (X := (↑(toNormalization (pullback.snd f fT) ⁻¹ᵁ U) : Scheme)) (toNormalization (pullback.snd f fT) ∣_ U)
fTn : normalization (X := pullback f fT) (pullback.snd f fT) ⟶ normalization f :=
  normalizationPullback f fT ≫ pullback.fst (fromNormalization f) fT
U' : (normalization f).Opens := { carrier := ⇑fTn '' U.carrier, is_open' := ⋯ }
fTnU : (↑U : Scheme) ⟶ (↑U' : Scheme) := resLE fTn U' U ⋯
this_1 : Surjective fTnU
H : toNormalization (pullback.snd f fT) ⁻¹ᵁ U ≤ pullback.fst f fT ⁻¹ᵁ toNormalization f ⁻¹ᵁ U'
this :
  IsPullback (toNormalization (pullback.snd f fT) ∣_ U)
    (resLE (pullback.fst f fT) (toNormalization f ⁻¹ᵁ U') (toNormalization (pullback.snd f fT) ⁻¹ᵁ U) H) fTnU
    (toNormalization f ∣_ U')
⊢ IsIso (X := (↑(toNormalization f ⁻¹ᵁ U') : Scheme)) (toNormalization f ∣_ U')

Tactic:
exact MorphismProperty.of_isPullback_of_descendsAlong (P := .isomorphisms _)
    (Q := @Surjective ⊓ @Flat ⊓ @LocallyOfFinitePresentation) this
    ⟨⟨‹_›, inferInstance⟩, inferInstance⟩ ‹_›

Premises used: CategoryTheory.MorphismProperty.of_isPullback_of_descendsAlong, inferInstance, And.intro
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] (H : IsAffineHom f),
        IsOpen.{u} (X := ↥X) {x : ↥X | QuasiFiniteAt f x})
    (H : ¬IsAffineHom f), IsOpen.{u} (X := ↥X) {x : ↥X | QuasiFiniteAt f x}
wlog :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] (H : IsAffineHom f),
    IsOpen.{u} (X := ↥X) {x : ↥X | QuasiFiniteAt f x}
⊢ IsOpen.{u} (X := ↥X) {x : ↥X | QuasiFiniteAt f x}

Tactic:
wlog H : IsAffineHom f

Premises used: AlgebraicGeometry.IsAffineHom
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] (H : IsAffineHom f),
    IsOpen.{u} (X := ↥X) {x : ↥X | QuasiFiniteAt f x}
H : ¬IsAffineHom f
inr :
  ∀ (x : ↥X),
    Membership.mem (γ := Set ↥X) {x : ↥X | QuasiFiniteAt f x} x → ∃ t ⊆ {x : ↥X | QuasiFiniteAt f x}, IsOpen t ∧ x ∈ t
⊢ IsOpen.{u} (X := ↥X) {x : ↥X | QuasiFiniteAt f x}

Tactic:
rw [isOpen_iff_forall_mem_open]

Premises used: isOpen_iff_forall_mem_open
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] (H : IsAffineHom f),
    IsOpen.{u} (X := ↥X) {x : ↥X | QuasiFiniteAt f x}
H : ¬IsAffineHom f
x : ↥X
hx : Membership.mem (γ := Set ↥X) {x : ↥X | QuasiFiniteAt f x} x
inr :
  ∀ (U : Y.Opens) (hU : U ∈ Y.affineOpens) (hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)),
    ∃ t ⊆ {x : ↥X | QuasiFiniteAt f x}, IsOpen t ∧ x ∈ t
⊢ ∃ t ⊆ {x : ↥X | QuasiFiniteAt f x}, IsOpen t ∧ x ∈ t

Tactic:
obtain ⟨_, ⟨U : Y.Opens, hU, rfl⟩, hxU, -⟩ := Y.isBasis_affineOpens.exists_subset_of_mem_open
      (Set.mem_univ (f x)) isOpen_univ

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', isOpen_univ, Set.mem_univ, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.isBasis_affineOpens, AlgebraicGeometry.Scheme.Opens, DFunLike.coe, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] (H : IsAffineHom f),
    IsOpen.{u} (X := ↥X) {x : ↥X | QuasiFiniteAt f x}
H : ¬IsAffineHom f
x : ↥X
hx : Membership.mem (γ := Set ↥X) {x : ↥X | QuasiFiniteAt f x} x
U : Y.Opens
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)
inr :
  ∀ (V : X.Opens) (hV : V ∈ X.affineOpens) (hxV : x ∈ (↑V : Set ↥X)) (hVU : (↑V : Set ↥X) ⊆ (f ⁻¹ᵁ U).carrier),
    ∃ t ⊆ {x : ↥X | QuasiFiniteAt f x}, IsOpen t ∧ x ∈ t
⊢ ∃ t ⊆ {x : ↥X | QuasiFiniteAt f x}, IsOpen t ∧ x ∈ t

Tactic:
obtain ⟨_, ⟨V : X.Opens, hV, rfl⟩, hxV, hVU⟩ := X.isBasis_affineOpens.exists_subset_of_mem_open
      hxU (f ⁻¹ᵁ U).2

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, TopologicalSpace.Opens.is_open', AlgebraicGeometry.Scheme.isBasis_affineOpens, AlgebraicGeometry.Scheme.Opens, CategoryTheory.Functor.obj, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] (H : IsAffineHom f),
    IsOpen.{u} (X := ↥X) {x : ↥X | QuasiFiniteAt f x}
H : ¬IsAffineHom f
x : ↥X
hx : Membership.mem (γ := Set ↥X) {x : ↥X | QuasiFiniteAt f x} x
U : Y.Opens
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)
V : X.Opens
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (f ⁻¹ᵁ U).carrier
⊢ IsAffineHom (resLE f U V hVU)

Tactic:
have inst : IsAffineHom (f.resLE U V hVU) :=
      have : IsAffine _ := hU
      have : IsAffine _ := hV
      isAffineHom_of_isAffine _
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] (H : IsAffineHom f),
    IsOpen.{u} (X := ↥X) {x : ↥X | QuasiFiniteAt f x}
H : ¬IsAffineHom f
x : ↥X
hx : Membership.mem (γ := Set ↥X) {x : ↥X | QuasiFiniteAt f x} x
U : Y.Opens
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)
V : X.Opens
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (f ⁻¹ᵁ U).carrier
inst : IsAffineHom (resLE f U V hVU)
⊢ ∃ t ⊆ {x : ↥X | QuasiFiniteAt f x}, IsOpen t ∧ x ∈ t

Tactic:
⟨_, ?_, V.2.isOpenEmbedding_subtypeVal.isOpenMap _ (this (f.resLE U V hVU) inst), ?_⟩

Premises used: IsOpen.isOpenEmbedding_subtypeVal, Topology.IsOpenEmbedding.isOpenMap, And.intro, Exists.intro, TopologicalSpace.Opens.is_open', AlgebraicGeometry.Scheme.Hom.resLE
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] (H : IsAffineHom f),
    IsOpen.{u} (X := ↥X) {x : ↥X | QuasiFiniteAt f x}
H : ¬IsAffineHom f
x : ↥X
hx : Membership.mem (γ := Set ↥X) {x : ↥X | QuasiFiniteAt f x} x
U : Y.Opens
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)
V : X.Opens
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (f ⁻¹ᵁ U).carrier
inst : IsAffineHom (resLE f U V hVU)
inr :
  Subset.{u} (α := Set ↥X)
    (Set.image (α := { x : ↥X // x ∈ V.carrier }) (Subtype.val (p := fun (x : ↥X) ↦ x ∈ V.carrier))
      {x : ↥(↑V : Scheme) | QuasiFiniteAt (resLE f U V hVU) x})
    {x : ↥X | QuasiFiniteAt f x}
inr₁ :
  Membership.mem (γ := Set ↥X)
    (Set.image (α := { x : ↥X // x ∈ V.carrier }) (Subtype.val (p := fun (x : ↥X) ↦ x ∈ V.carrier))
      {x : ↥(↑V : Scheme) | QuasiFiniteAt (resLE f U V hVU) x})
    x
⊢ ∃ t ⊆ {x : ↥X | QuasiFiniteAt f x}, IsOpen t ∧ x ∈ t

Tactic:
refine ⟨_, ?_, V.2.isOpenEmbedding_subtypeVal.isOpenMap _ (this (f.resLE U V hVU) inst), ?_⟩
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] (H : IsAffineHom f),
    IsOpen.{u} (X := ↥X) {x : ↥X | QuasiFiniteAt f x}
H : ¬IsAffineHom f
x_1 : ↥X
hx_1 : Membership.mem (γ := Set ↥X) {x : ↥X | QuasiFiniteAt f x} x_1
U : Y.Opens
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x_1 : ↥Y)
V : X.Opens
hV : V ∈ X.affineOpens
hxV : x_1 ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (f ⁻¹ᵁ U).carrier
inst : IsAffineHom (resLE f U V hVU)
x : ↥V
hx : QuasiFiniteAt (resLE f U V hVU) x
inr :
  ∀ (hx : QuasiFiniteAt (resLE f U V hVU ≫ U.ι) x), Membership.mem (γ := Set ↥X) {x : ↥X | QuasiFiniteAt f x} (↑x : ↥X)
inr₁ : ∀ (hx : QuasiFiniteAt (V.ι ≫ f) x), Membership.mem (γ := Set ↥X) {x : ↥X | QuasiFiniteAt f x} (↑x : ↥X)
inr₂ inr₃ inr₄ inr₅ :
  ∀ (hx : QuasiFiniteAt f (V.ι x)), Membership.mem (γ := Set ↥X) {x : ↥X | QuasiFiniteAt f x} (↑x : ↥X)
⊢ Membership.mem (γ := Set ↥X) {x : ↥X | QuasiFiniteAt f x} (↑x : ↥X)

Tactic:
rwa [← quasiFiniteAt_comp_iff (g := U.ι), resLE_comp_ι,
        quasiFiniteAt_comp_iff_of_isOpenImmersion] at hx

Premises used: AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_comp_iff_of_isOpenImmersion, AlgebraicGeometry.Scheme.Hom.resLE_comp_ι, AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_comp_iff
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] (H : IsAffineHom f),
    IsOpen.{u} (X := ↥X) {x : ↥X | QuasiFiniteAt f x}
H : ¬IsAffineHom f
x : ↥X
hx : Membership.mem (γ := Set ↥X) {x : ↥X | QuasiFiniteAt f x} x
U : Y.Opens
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)
V : X.Opens
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (f ⁻¹ᵁ U).carrier
inst : IsAffineHom (resLE f U V hVU)
⊢ Membership.mem (γ := Set ↥X)
    (Set.image (α := { x : ↥X // x ∈ V.carrier }) (Subtype.val (p := fun (x : ↥X) ↦ x ∈ V.carrier))
      {x : ↥(↑V : Scheme) | QuasiFiniteAt (resLE f U V hVU) x})
    x

Tactic:
⟨⟨x, hxV⟩, show (f.resLE _ _ _).QuasiFiniteAt _ from ?_, rfl⟩

Premises used: Set.Mem, setOf, Subtype.mk, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] (H : IsAffineHom f),
    IsOpen.{u} (X := ↥X) {x : ↥X | QuasiFiniteAt f x}
H : ¬IsAffineHom f
x : ↥X
hx : Membership.mem (γ := Set ↥X) {x : ↥X | QuasiFiniteAt f x} x
U : Y.Opens
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)
V : X.Opens
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (f ⁻¹ᵁ U).carrier
inst : IsAffineHom (resLE f U V hVU)
inr : QuasiFiniteAt (resLE f U V hVU) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V.carrier) x hxV)
⊢ Membership.mem (γ := Set ↥X)
    (Set.image (α := { x : ↥X // x ∈ V.carrier }) (Subtype.val (p := fun (x : ↥X) ↦ x ∈ V.carrier))
      {x : ↥(↑V : Scheme) | QuasiFiniteAt (resLE f U V hVU) x})
    x

Tactic:
refine ⟨⟨x, hxV⟩, show (f.resLE _ _ _).QuasiFiniteAt _ from ?_, rfl⟩
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] (H : IsAffineHom f),
    IsOpen.{u} (X := ↥X) {x : ↥X | QuasiFiniteAt f x}
H : ¬IsAffineHom f
x : ↥X
hx : Membership.mem (γ := Set ↥X) {x : ↥X | QuasiFiniteAt f x} x
U : Y.Opens
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)
V : X.Opens
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (f ⁻¹ᵁ U).carrier
inst : IsAffineHom (resLE f U V hVU)
inr : QuasiFiniteAt (resLE f U V hVU ≫ U.ι) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V.carrier) x hxV)
inr₁ : QuasiFiniteAt (V.ι ≫ f) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V.carrier) x hxV)
inr₂ inr₃ inr₄ inr₅ : QuasiFiniteAt f (V.ι (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V.carrier) x hxV))
⊢ QuasiFiniteAt (resLE f U V hVU) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V.carrier) x hxV)

Tactic:
rwa [← quasiFiniteAt_comp_iff (g := U.ι), resLE_comp_ι,
        quasiFiniteAt_comp_iff_of_isOpenImmersion]

Premises used: AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_comp_iff_of_isOpenImmersion, AlgebraicGeometry.Scheme.Hom.resLE_comp_ι, AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_comp_iff
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
H : IsAffineHom f
obtain :
  ∀ (U : (normalization f).Opens) (hU : IsIso (X := (↑(toNormalization f ⁻¹ᵁ U) : Scheme)) (toNormalization f ∣_ U))
    (e : (toNormalization f ⁻¹ᵁ U).carrier = {x : ↥X | QuasiFiniteAt f x}),
    IsOpen.{u} (X := ↥X) {x : ↥X | QuasiFiniteAt f x}
⊢ IsOpen.{u} (X := ↥X) {x : ↥X | QuasiFiniteAt f x}

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 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
H : IsAffineHom f
U : (normalization f).Opens
hU : IsIso (X := (↑(toNormalization f ⁻¹ᵁ U) : Scheme)) (toNormalization f ∣_ U)
e : (toNormalization f ⁻¹ᵁ U).carrier = {x : ↥X | QuasiFiniteAt f x}
⊢ IsOpen.{u} (X := ↥X) {x : ↥X | QuasiFiniteAt f x}

Tactic:
e ▸ (f.toNormalization ⁻¹ᵁ U).2

Premises used: Eq.rec, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.Scheme.Hom.toNormalization, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, TopologicalSpace.Opens.is_open', CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
H : IsAffineHom f
U : (normalization f).Opens
hU : IsIso (X := (↑(toNormalization f ⁻¹ᵁ U) : Scheme)) (toNormalization f ∣_ U)
e : (toNormalization f ⁻¹ᵁ U).carrier = {x : ↥X | QuasiFiniteAt f x}
⊢ IsOpen.{u} (X := ↥X) {x : ↥X | QuasiFiniteAt f x}

Tactic:
exact e ▸ (f.toNormalization ⁻¹ᵁ U).2
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
x : ↥X
⊢ x ∈ quasiFiniteLocus f ↔ QuasiFiniteAt f x

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt, RingHom.QuasiFinite