awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
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
hVW' : (↑W : Set ↥(pullback f fT)) = (↑V : Set ↥(pullback f fT))ᶜ
this_1 : IsClosedImmersion V.ι
this : IsClosedImmersion W.ι
H : IsColimit (BinaryCofan.mk V.ι W.ι)
e : normalization (X := pullback f fT) (pullback.snd f fT) ≅ (↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT) :=
  Iso.trans (Y := normalization (V.ι ≫ pullback.snd f fT) ⨿ normalization (W.ι ≫ pullback.snd f fT))
    (Iso.symm (normalizationCoprodIso (pullback.snd f fT) H) :
      normalization (X := pullback f fT) (pullback.snd f fT) ≅
        normalization (V.ι ≫ pullback.snd f fT) ⨿ normalization (W.ι ≫ pullback.snd f fT))
    (coprod.mapIso (Iso.symm (asIso (toNormalization (V.ι ≫ pullback.snd f fT))))
        (Iso.refl (normalization (W.ι ≫ pullback.snd f fT))) :
      normalization (V.ι ≫ pullback.snd f fT) ⨿ normalization (W.ι ≫ pullback.snd f fT) ≅
        (↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT))
ι : (↑V : Scheme) ⟶ (↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT) := coprod.inl
Heq : toNormalization (pullback.snd f fT) ⁻¹ᵁ e.hom ⁻¹ᵁ opensRange ι = V
⊢ IsIso (X := (↑(toNormalization (pullback.snd f fT) ⁻¹ᵁ e.hom ⁻¹ᵁ opensRange ι) : Scheme))
    (CategoryStruct.comp (Y := (↑(opensRange ι) : Scheme))
        ((toNormalization (pullback.snd f fT) ≫ e.hom) ∣_ opensRange ι) (Iso.inv (isoOpensRange ι)) :
      (↑(toNormalization (pullback.snd f fT) ⁻¹ᵁ e.hom ⁻¹ᵁ opensRange ι) : Scheme) ⟶ (↑V : Scheme))
have h : CategoryStruct.comp (Y := (↑(opensRange ι) : Scheme)) ((toNormalization (pullback.snd f fT) ≫ e.hom) ∣_ opensRange ι)
    (Iso.inv (isoOpensRange ι)) =
  ((pullback f fT).isoOfEq Heq).hom
Tactic: convert! (inferInstance : IsIso (Scheme.isoOfEq _ Heq).hom)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
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
hVW' : (↑W : Set ↥(pullback f fT)) = (↑V : Set ↥(pullback f fT))ᶜ
this_1 : IsClosedImmersion V.ι
this : IsClosedImmersion W.ι
H : IsColimit (BinaryCofan.mk V.ι W.ι)
e : normalization (X := pullback f fT) (pullback.snd f fT) ≅ (↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT) :=
  Iso.trans (Y := normalization (V.ι ≫ pullback.snd f fT) ⨿ normalization (W.ι ≫ pullback.snd f fT))
    (Iso.symm (normalizationCoprodIso (pullback.snd f fT) H) :
      normalization (X := pullback f fT) (pullback.snd f fT) ≅
        normalization (V.ι ≫ pullback.snd f fT) ⨿ normalization (W.ι ≫ pullback.snd f fT))
    (coprod.mapIso (Iso.symm (asIso (toNormalization (V.ι ≫ pullback.snd f fT))))
        (Iso.refl (normalization (W.ι ≫ pullback.snd f fT))) :
      normalization (V.ι ≫ pullback.snd f fT) ⨿ normalization (W.ι ≫ pullback.snd f fT) ≅
        (↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT))
ι : (↑V : Scheme) ⟶ (↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT) := coprod.inl
Heq : toNormalization (pullback.snd f fT) ⁻¹ᵁ e.hom ⁻¹ᵁ opensRange ι = V
⊢ CategoryStruct.comp (Y := (↑(opensRange ι) : Scheme)) ((toNormalization (pullback.snd f fT) ≫ e.hom) ∣_ opensRange ι)
      (Iso.inv (isoOpensRange ι)) =
    ((pullback f fT).isoOfEq Heq).hom
have h : (((pullback f fT).isoOfEq Heq).inv ≫ (toNormalization (pullback.snd f fT) ≫ e.hom) ∣_ opensRange ι) ≫ (opensRange ι).ι =
  Iso.hom (isoOpensRange ι) ≫ (opensRange ι).ι
Tactic: rw [Iso.comp_inv_eq, ← Iso.inv_comp_eq, ← cancel_mono (Scheme.Opens.ι _)]
-- 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
hVW' : (↑W : Set ↥(pullback f fT)) = (↑V : Set ↥(pullback f fT))ᶜ
this_1 : IsClosedImmersion V.ι
this : IsClosedImmersion W.ι
H : IsColimit (BinaryCofan.mk V.ι W.ι)
e : normalization (X := pullback f fT) (pullback.snd f fT) ≅ (↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT) :=
  Iso.trans (Y := normalization (V.ι ≫ pullback.snd f fT) ⨿ normalization (W.ι ≫ pullback.snd f fT))
    (Iso.symm (normalizationCoprodIso (pullback.snd f fT) H) :
      normalization (X := pullback f fT) (pullback.snd f fT) ≅
        normalization (V.ι ≫ pullback.snd f fT) ⨿ normalization (W.ι ≫ pullback.snd f fT))
    (coprod.mapIso (Iso.symm (asIso (toNormalization (V.ι ≫ pullback.snd f fT))))
        (Iso.refl (normalization (W.ι ≫ pullback.snd f fT))) :
      normalization (V.ι ≫ pullback.snd f fT) ⨿ normalization (W.ι ≫ pullback.snd f fT) ≅
        (↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT))
ι : (↑V : Scheme) ⟶ (↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT) := coprod.inl
Heq : toNormalization (pullback.snd f fT) ⁻¹ᵁ e.hom ⁻¹ᵁ opensRange ι = V
⊢ (((pullback f fT).isoOfEq Heq).inv ≫ (toNormalization (pullback.snd f fT) ≫ e.hom) ∣_ opensRange ι) ≫
      (opensRange ι).ι =
    Iso.hom (isoOpensRange ι) ≫ (opensRange ι).ι
have this₁ : Eq (α :=
  (↑V : Scheme) ⟶ Cocone.pt (F := pair (↑V : Scheme) (↑W : Scheme)) (colimit.cocone (pair (↑V : Scheme) (↑W : Scheme))))
  (V.ι ≫ Iso.hom (H.coconePointUniqueUpToIso (colimit.isColimit (pair (↑V : Scheme) (↑W : Scheme))))) coprod.inl
Tactic: have : V.ι ≫ (H.coconePointUniqueUpToIso (colimit.isColimit _)).hom = coprod.inl :=
      H.comp_coconePointUniqueUpToIso_hom _ ⟨.left⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
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' := ⋯ }
⊢ Eq (α := ↥(normalization f))
    (fTn
        ((toNormalization (pullback.snd f fT)) (↑v : ↥(pullback f fT)) :
          ↥(normalization (X := pullback f fT) (pullback.snd f fT))) :
      ↥(normalization f))
    ((toNormalization f) x : ↥(normalization f))
have simp : Eq (α := ↥(normalization f)) ((toNormalization (pullback.snd f fT) ≫ fTn) (↑v : ↥(pullback f fT)) : ↥(normalization f))
  ((pullback.fst f fT ≫ toNormalization f) (↑v : ↥(pullback f fT)) : ↥(normalization f))
Tactic: simp only [← hv₂, ← Scheme.Hom.comp_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
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' := ⋯ }
⊢ ∃ (V : (normalization f).Opens),
    Membership.mem (α := ↥(normalization f)) V ((toNormalization f) x : ↥(normalization f)) ∧
      IsIso (X := (↑(toNormalization f ⁻¹ᵁ V) : Scheme)) (toNormalization f ∣_ V)
have refine : IsIso (X := (↑(toNormalization f ⁻¹ᵁ U') : Scheme)) (toNormalization f ∣_ U')
Tactic: refine ⟨U', ⟨_, hU, by simp only [← hv₂, ← Scheme.Hom.comp_apply]; simp [fTn]⟩, ?_⟩
-- 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 ⋯
⊢ IsIso (X := (↑(toNormalization f ⁻¹ᵁ U') : Scheme)) (toNormalization f ∣_ U')
have this : Surjective fTnU
Tactic: have : Surjective fTnU := ⟨fun ⟨x, a, ha, e⟩ ↦ ⟨⟨a, ha⟩, Subtype.ext <| by simpa [fTnU] using e⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
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
⊢ toNormalization (pullback.snd f fT) ⁻¹ᵁ U ≤ pullback.fst f fT ⁻¹ᵁ toNormalization f ⁻¹ᵁ U'
have refine : ∀ (x : ↥(pullback f fT)) (hx : x ∈ toNormalization (pullback.snd f fT) ⁻¹ᵁ U),
  Eq (α := ↥(normalization f))
    (fTn ((toNormalization (pullback.snd f fT)) x : ↥(normalization (X := pullback f fT) (pullback.snd f fT))) :
      ↥(normalization f))
    ((toNormalization f) ((pullback.fst f fT) x : ↥X) : ↥(normalization f))
Tactic: refine fun x hx ↦ ⟨_, hx, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
inst_1 : IsSeparated f
inst_2 : QuasiCompact f
x_1 : ↥X
hx_1 : QuasiFiniteAt f x_1
T : Scheme
fT : T ⟶ Y
left : Etale fT
u : ↥T
hu : Eq (α := ↥Y) (fT u : ↥Y) (f x_1 : ↥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_1
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
x : ↥(pullback f fT)
hx : x ∈ toNormalization (pullback.snd f fT) ⁻¹ᵁ U
⊢ Eq (α := ↥(normalization f))
    (fTn ((toNormalization (pullback.snd f fT)) x : ↥(normalization (X := pullback f fT) (pullback.snd f fT))) :
      ↥(normalization f))
    ((toNormalization f) ((pullback.fst f fT) x : ↥X) : ↥(normalization f))
have simp : Eq (α := ↥(normalization f)) ((toNormalization (pullback.snd f fT) ≫ fTn) x : ↥(normalization f))
  ((pullback.fst f fT ≫ toNormalization f) x : ↥(normalization f))
Tactic: simp only [← Scheme.Hom.comp_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
inst_1 : IsSeparated f
inst_2 : QuasiCompact f
x_1 : ↥X
hx_1 : QuasiFiniteAt f x_1
T : Scheme
fT : T ⟶ Y
left : Etale fT
u : ↥T
hu : Eq (α := ↥Y) (fT u : ↥Y) (f x_1 : ↥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_1
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
x : ↥(pullback f fT)
hx : x ∈ toNormalization (pullback.snd f fT) ⁻¹ᵁ U
⊢ Eq (α := ↥(normalization f)) ((toNormalization (pullback.snd f fT) ≫ fTn) x : ↥(normalization f))
    ((pullback.fst f fT ≫ toNormalization f) x : ↥(normalization f))
have e_a : toNormalization (pullback.snd f fT) ≫ fTn = pullback.fst f fT ≫ toNormalization f
Tactic: congr 5
-- 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
⊢ IsIso (X := (↑(toNormalization f ⁻¹ᵁ U') : Scheme)) (toNormalization f ∣_ U')
have H : toNormalization (pullback.snd f fT) ⁻¹ᵁ U ≤ pullback.fst f fT ⁻¹ᵁ toNormalization f ⁻¹ᵁ U'
Tactic: have H : (pullback.snd f fT).toNormalization ⁻¹ᵁ U ≤
      pullback.fst f fT ⁻¹ᵁ f.toNormalization ⁻¹ᵁ U' := by
    refine fun x hx ↦ ⟨_, hx, ?_⟩
    simp only [← Scheme.Hom.comp_apply]
    congr 5
    simp [fTn]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
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')
have refine_1 : IsPullback (toNormalization (pullback.snd f fT) ∣_ U)
  (resLE (pullback.fst f fT) (toNormalization f ⁻¹ᵁ U') (toNormalization (pullback.snd f fT) ⁻¹ᵁ U) H ≫
    (toNormalization f ⁻¹ᵁ U').ι)
  (fTnU ≫ U'.ι) (toNormalization f)
Tactic: refine .of_bot (t := isPullback_morphismRestrict ..) ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
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'
refine_1 :
  IsPullback (toNormalization (pullback.snd f fT) ∣_ U)
    (resLE (pullback.fst f fT) (toNormalization f ⁻¹ᵁ U') (toNormalization (pullback.snd f fT) ⁻¹ᵁ U) H ≫
      (toNormalization f ⁻¹ᵁ U').ι)
    (fTnU ≫ U'.ι) (toNormalization f)
⊢ 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')
have refine_2 : 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: refine .of_bot (t := isPullback_morphismRestrict ..) ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
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 ≫
      (toNormalization f ⁻¹ᵁ U').ι)
    (fTnU ≫ U'.ι) (toNormalization f)
have refine_1 : IsPullback (toNormalization (pullback.snd f fT) ∣_ U)
  ((toNormalization (pullback.snd f fT) ⁻¹ᵁ U).ι ≫ pullback.fst f fT) (U.ι ≫ fTn) (toNormalization f)
Tactic: simp only [Scheme.Hom.resLE_comp_ι, fTnU]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
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)
    ((toNormalization (pullback.snd f fT) ⁻¹ᵁ U).ι ≫ pullback.fst f fT) (U.ι ≫ fTn) (toNormalization f)
have refine_1 : IsPullback (toNormalization (pullback.snd f fT)) (pullback.fst f fT) fTn (toNormalization f)
Tactic: refine .paste_vert (isPullback_morphismRestrict ..) ?_