awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (hypothesis)
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)) (pullback.fst f fT) fTn (toNormalization f)
have 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) sorry sorry) (pullback.fst f fT)
  (pullback.fst (fromNormalization f) fT) (toNormalization f)
Tactic: 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)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (hypothesis)
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'
⊢ IsIso (X := (↑(toNormalization f ⁻¹ᵁ U') : Scheme)) (toNormalization f ∣_ U')
have 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')
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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
⊢ IsOpen.{u} (X := ↥X) {x : ↥X | QuasiFiniteAt f x}
have 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}
Tactic: wlog H : IsAffineHom f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
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}
⊢ IsOpen.{u} (X := ↥X) {x : ↥X | QuasiFiniteAt f x}
have wlog : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] (H : IsAffineHom f),
  IsOpen.{u} (X := ↥X) {x : ↥X | QuasiFiniteAt f x}
Tactic: wlog H : IsAffineHom f
Cleared hypotheses: inst
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
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
⊢ IsOpen.{u} (X := ↥X) {x : ↥X | QuasiFiniteAt f x}
have inr : ∀ (x : ↥X),
  Membership.mem (γ := Set ↥X) {x : ↥X | QuasiFiniteAt f x} x → ∃ t ⊆ {x : ↥X | QuasiFiniteAt f x}, IsOpen t ∧ x ∈ t
Tactic: rw [isOpen_iff_forall_mem_open]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
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
⊢ ∃ t ⊆ {x : ↥X | QuasiFiniteAt f x}, IsOpen t ∧ x ∈ t
have 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
Tactic: obtain ⟨_, ⟨U : Y.Opens, hU, rfl⟩, hxU, -⟩ := Y.isBasis_affineOpens.exists_subset_of_mem_open
      (Set.mem_univ (f x)) isOpen_univ
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
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)
⊢ ∃ t ⊆ {x : ↥X | QuasiFiniteAt f x}, IsOpen t ∧ x ∈ t
have 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
Tactic: obtain ⟨_, ⟨V : X.Opens, hV, rfl⟩, hxV, hVU⟩ := X.isBasis_affineOpens.exists_subset_of_mem_open
      hxU (f ⁻¹ᵁ U).2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (hypothesis)
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
⊢ ∃ t ⊆ {x : ↥X | QuasiFiniteAt f x}, IsOpen t ∧ x ∈ t
have inst : IsAffineHom (resLE f U V hVU)
Tactic: have inst : IsAffineHom (f.resLE U V hVU) :=
      have : IsAffine _ := hU
      have : IsAffine _ := hV
      isAffineHom_of_isAffine _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
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
have 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}
Tactic: refine ⟨_, ?_, V.2.isOpenEmbedding_subtypeVal.isOpenMap _ (this (f.resLE U V hVU) inst), ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
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}
⊢ ∃ t ⊆ {x : ↥X | QuasiFiniteAt f x}, IsOpen t ∧ x ∈ t
have 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
Tactic: refine ⟨_, ?_, V.2.isOpenEmbedding_subtypeVal.isOpenMap _ (this (f.resLE U V hVU) inst), ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
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
⊢ Membership.mem (γ := Set ↥X) {x : ↥X | QuasiFiniteAt f x} (↑x : ↥X)
have inr : ∀ (hx : QuasiFiniteAt (resLE f U V hVU ≫ U.ι) 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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
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)
⊢ Membership.mem (γ := Set ↥X) {x : ↥X | QuasiFiniteAt f x} (↑x : ↥X)
have inr₁ : ∀ (hx : QuasiFiniteAt (V.ι ≫ f) 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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
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)
⊢ Membership.mem (γ := Set ↥X) {x : ↥X | QuasiFiniteAt f x} (↑x : ↥X)
have inr₂ : ∀ (hx : QuasiFiniteAt f (V.ι 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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
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
have inr : QuasiFiniteAt (resLE f U V hVU) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V.carrier) x hxV)
Tactic: refine ⟨⟨x, hxV⟩, show (f.resLE _ _ _).QuasiFiniteAt _ from ?_, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
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)
⊢ QuasiFiniteAt (resLE f U V hVU) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V.carrier) x hxV)
have inr : QuasiFiniteAt (resLE f U V hVU ≫ U.ι) (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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
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)
⊢ QuasiFiniteAt (resLE f U V hVU) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V.carrier) x hxV)
have inr₁ : QuasiFiniteAt (V.ι ≫ f) (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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
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)
⊢ QuasiFiniteAt (resLE f U V hVU) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V.carrier) x hxV)
have inr₂ : QuasiFiniteAt f (V.ι (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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
H : IsAffineHom f
⊢ IsOpen.{u} (X := ↥X) {x : ↥X | QuasiFiniteAt f x}
have 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}
Tactic: obtain ⟨U, hU, e⟩ := Scheme.Hom.exists_isIso_morphismRestrict_toNormalization f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
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
⊢ IsOpenImmersion (Y := Scheme.Hom.normalization f) ((Scheme.Hom.quasiFiniteLocus f).ι ≫ Scheme.Hom.toNormalization f)
have 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)
Tactic: obtain ⟨U, hU, e⟩ := Scheme.Hom.exists_isIso_morphismRestrict_toNormalization f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
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 (Y := Scheme.Hom.normalization f) ((Scheme.Hom.quasiFiniteLocus f).ι ≫ Scheme.Hom.toNormalization f)
have h : (Scheme.Hom.quasiFiniteLocus f).ι ≫ Scheme.Hom.toNormalization f =
  CategoryStruct.comp (Y := (↑(Scheme.Hom.toNormalization f ⁻¹ᵁ U) : Scheme)) (Iso.hom (X.isoOfEq sorry))
    (Scheme.Hom.toNormalization f ∣_ U ≫ U.ι)
Tactic: convert!
    (inferInstance :
      IsOpenImmersion
        ((X.isoOfEq (U := f.quasiFiniteLocus) (SetLike.coe_injective e.symm)).hom ≫
          f.toNormalization ∣_ U ≫ U.ι)) using 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
Z : Scheme
inst : IsOpenImmersion f
g : Y ⟶ Z
inst_1 : LocallyOfFiniteType g
⊢ quasiFiniteLocus (f ≫ g) = f ⁻¹ᵁ quasiFiniteLocus g
have h : ∀ (x : ↥X), x ∈ (↑(quasiFiniteLocus (f ≫ g)) : Set ↥X) ↔ x ∈ (↑(f ⁻¹ᵁ quasiFiniteLocus g) : Set ↥X)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
⊢ quasiFiniteLocus f = ⊤ ↔ LocallyQuasiFinite f
have refine : ∀ (H : quasiFiniteLocus f = ⊤) (x : ↥Y), _root_.IsDiscrete (X := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})
Tactic: refine ⟨fun H ↦ locallyQuasiFinite_iff_isDiscrete_preimage_singleton.mpr fun x ↦ ?_,
    fun _ ↦ f.quasiFiniteLocus_eq_top⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
H : quasiFiniteLocus f = ⊤
x : ↥Y
⊢ _root_.IsDiscrete (X := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})
have rw : ∀ (a : (↑(Set.preimage (β := ↥Y) ⇑f {x}) : Type u)), IsOpen (X := (↑(Set.preimage (β := ↥Y) ⇑f {x}) : Type u)) {a}
Tactic: rw [isDiscrete_iff_discreteTopology, discreteTopology_iff_isOpen_singleton]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
H : quasiFiniteLocus f = ⊤
a : ↥X
⊢ 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 ⋯}
have 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 sorry) :
      ↥(fiber f (f a))))
Tactic: rw [← (f.fiberHomeo _).symm.isOpen_image, Set.image_singleton]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
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
⊢ LocallyQuasiFinite ((Scheme.Hom.quasiFiniteLocus f).ι ≫ f)
have rw : Scheme.Hom.quasiFiniteLocus ((Scheme.Hom.quasiFiniteLocus f).ι ≫ f) = ⊤
Tactic: rw [← Scheme.Hom.quasiFiniteLocus_eq_top_iff, Scheme.Hom.quasiFiniteLocus_comp,
    Scheme.Opens.ι_preimage_self]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
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) = ⊤
⊢ LocallyQuasiFinite ((Scheme.Hom.quasiFiniteLocus f).ι ≫ f)
have rw₁ : (Scheme.Hom.quasiFiniteLocus f).ι ⁻¹ᵁ Scheme.Hom.quasiFiniteLocus f = ⊤
Tactic: rw [← Scheme.Hom.quasiFiniteLocus_eq_top_iff, Scheme.Hom.quasiFiniteLocus_comp,
    Scheme.Opens.ι_preimage_self]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
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 = ⊤
⊢ LocallyQuasiFinite ((Scheme.Hom.quasiFiniteLocus f).ι ≫ f)
have rw₂ : Eq.{u + 1} (α := (↑(Scheme.Hom.quasiFiniteLocus f) : Scheme).Opens) ⊤ ⊤
Tactic: rw [← Scheme.Hom.quasiFiniteLocus_eq_top_iff, Scheme.Hom.quasiFiniteLocus_comp,
    Scheme.Opens.ι_preimage_self]