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
⊢ Eq (α := ↥((↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT)))
    (ι v : ↥((↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT)))
    ((V.ι ≫ toNormalization (pullback.snd f fT) ≫ e.hom) v : ↥((↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT)))
have refine_1 : ι = V.ι ≫ toNormalization (pullback.snd f fT) ≫ e.hom
Tactic: congr 5
-- 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
⊢ ι = V.ι ≫ toNormalization (pullback.snd f fT) ≫ e.hom
have refine_1 : ι ≫ e.inv = V.ι ≫ toNormalization (pullback.snd f fT)
Tactic: rw [← Category.assoc, ← Iso.comp_inv_eq]
-- 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
⊢ IsIso (X := (↑(toNormalization (pullback.snd f fT) ⁻¹ᵁ e.hom ⁻¹ᵁ opensRange ι) : Scheme))
    (toNormalization (pullback.snd f fT) ∣_ e.hom ⁻¹ᵁ opensRange ι)
have refine_2 : 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))
Tactic: rw [← isIso_comp_right_iff _ (e.hom ∣_ ι.opensRange),
      ← morphismRestrict_comp, ← isIso_comp_right_iff _ ι.isoOpensRange.inv]
-- 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
⊢ toNormalization (pullback.snd f fT) ⁻¹ᵁ e.hom ⁻¹ᵁ opensRange ι = V
have a : toNormalization (pullback.snd f fT) ⁻¹ᵁ e.hom ⁻¹ᵁ opensRange ι ≤ V
Tactic: apply le_antisymm
-- 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
a : toNormalization (pullback.snd f fT) ⁻¹ᵁ e.hom ⁻¹ᵁ opensRange ι ≤ V
⊢ toNormalization (pullback.snd f fT) ⁻¹ᵁ e.hom ⁻¹ᵁ opensRange ι = V
have a₁ : V ≤ toNormalization (pullback.snd f fT) ⁻¹ᵁ e.hom ⁻¹ᵁ opensRange ι
Tactic: apply le_antisymm
-- 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
a : ↥(pullback f fT)
b : ↥(↑V : Scheme)
hab :
  Eq (α := ↥((↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT)))
    (ι b : ↥((↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT)))
    (e.hom ((toNormalization (pullback.snd f fT)) a : ↥(normalization (X := pullback f fT) (pullback.snd f fT))) :
      ↥((↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT)))
⊢ a ∈ V
have a₁ : ∀ (h : a ∉ V), False
Tactic: by_contra h
-- 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
a : ↥(pullback f fT)
b : ↥(↑V : Scheme)
hab :
  Eq (α := ↥((↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT)))
    (ι b : ↥((↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT)))
    (e.hom ((toNormalization (pullback.snd f fT)) a : ↥(normalization (X := pullback f fT) (pullback.snd f fT))) :
      ↥((↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT)))
h : a ∉ V
⊢ False
have a₁ : ∀ (a : ↥W)
  (hab :
    Eq (α := ↥((↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT)))
      (ι b : ↥((↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT)))
      (e.hom
          ((toNormalization (pullback.snd f fT)) (↑a : ↥(pullback f fT)) :
            ↥(normalization (X := pullback f fT) (pullback.snd f fT))) :
        ↥((↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT))))
  (h : (↑a : ↥(pullback f fT)) ∉ V), False
Tactic: lift a to W using hVW'.ge h
Cleared hypotheses: a, hab, h
-- 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
b : ↥(↑V : Scheme)
a : ↥W
hab :
  Eq (α := ↥((↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT)))
    (ι b : ↥((↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT)))
    (e.hom
        ((toNormalization (pullback.snd f fT)) (↑a : ↥(pullback f fT)) :
          ↥(normalization (X := pullback f fT) (pullback.snd f fT))) :
      ↥((↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT)))
h : (↑a : ↥(pullback f fT)) ∉ V
⊢ Eq (α := ↥((↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT)))
    (ι b : ↥((↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT)))
    ((toNormalization (W.ι ≫ pullback.snd f fT) ≫ coprod.inr) a :
      ↥((↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT)))
have this₁ : Eq (α :=
  (↑W : Scheme) ⟶ Cocone.pt (F := pair (↑V : Scheme) (↑W : Scheme)) (colimit.cocone (pair (↑V : Scheme) (↑W : Scheme))))
  (W.ι ≫ Iso.hom (H.coconePointUniqueUpToIso (colimit.isColimit (pair (↑V : Scheme) (↑W : Scheme))))) coprod.inr
Tactic: have : W.ι ≫ (H.coconePointUniqueUpToIso (colimit.isColimit _)).hom = coprod.inr :=
            H.comp_coconePointUniqueUpToIso_hom _ ⟨.right⟩
-- 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
b : ↥(↑V : Scheme)
a : ↥W
hab :
  Eq (α := ↥((↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT)))
    (ι b : ↥((↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT)))
    (e.hom
        ((toNormalization (pullback.snd f fT)) (↑a : ↥(pullback f fT)) :
          ↥(normalization (X := pullback f fT) (pullback.snd f fT))) :
      ↥((↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT)))
h : (↑a : ↥(pullback f fT)) ∉ V
⊢ False
have hab₁ : Eq (α := ↥((↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT)))
  (ι b : ↥((↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT)))
  ((toNormalization (W.ι ≫ pullback.snd f fT) ≫ coprod.inr) a :
    ↥((↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT)))
Tactic: replace hab : ι b = ((W.ι ≫ pullback.snd f fT).toNormalization ≫ coprod.inr) a := by
          have : W.ι ≫ (H.coconePointUniqueUpToIso (colimit.isColimit _)).hom = coprod.inr :=
            H.comp_coconePointUniqueUpToIso_hom _ ⟨.right⟩
          simp only [← W.ι_apply, ← Scheme.Hom.comp_apply, Category.assoc, e] at hab
          simpa [-Scheme.Hom.comp_base, Scheme.Hom.normalizationCoprodIso,
            reassoc_of% this] using hab
Cleared hypotheses: hab
-- 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
⊢ V ≤ toNormalization (pullback.snd f fT) ⁻¹ᵁ e.hom ⁻¹ᵁ opensRange ι
have a : (↑V : Set ↥(pullback f fT)) ⊆ (↑(toNormalization (pullback.snd f fT) ⁻¹ᵁ e.inv ''ᵁ opensRange ι) : Set ↥(pullback f fT))
Tactic: rw [← Scheme.Hom.inv_image, ← SetLike.coe_subset_coe]
-- 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
⊢ 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 Heq : toNormalization (pullback.snd f fT) ⁻¹ᵁ e.hom ⁻¹ᵁ opensRange ι = V
Tactic: have Heq : (pullback.snd f fT).toNormalization ⁻¹ᵁ e.hom ⁻¹ᵁ Scheme.Hom.opensRange ι = V := by
      apply le_antisymm
      · rintro a ⟨b, hab⟩
        by_contra h
        lift a to W using hVW'.ge h
        replace hab : ι b = ((W.ι ≫ pullback.snd f fT).toNormalization ≫ coprod.inr) a := by
          have : W.ι ≫ (H.coconePointUniqueUpToIso (colimit.isColimit _)).hom = coprod.inr :=
            H.comp_coconePointUniqueUpToIso_hom _ ⟨.right⟩
          simp only [← W.ι_apply, ← Scheme.Hom.comp_apply, Category.assoc, e] at hab
          simpa [-Scheme.Hom.comp_base, Scheme.Hom.normalizationCoprodIso,
            reassoc_of% this] using hab
        exact Set.disjoint_iff_forall_ne.mp
          (isCompl_range_inl_inr V (W.ι ≫ pullback.snd f fT).normalization).1 ⟨_, rfl⟩ ⟨_, rfl⟩ hab
      · rw [← Scheme.Hom.inv_image, ← SetLike.coe_subset_coe]
        simpa [← Scheme.Hom.opensRange_comp, ι, e, Scheme.Hom.normalizationCoprodIso,
          Set.range_comp] using Set.subset_preimage_image _ _