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
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
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))
⊢ IsIso (X := (↑(toNormalization (pullback.snd f fT) ⁻¹ᵁ e.hom ⁻¹ᵁ opensRange ι) : Scheme))
    (toNormalization (pullback.snd f fT) ∣_ e.hom ⁻¹ᵁ opensRange ι)

Tactic:
rw [← isIso_comp_right_iff _ (e.hom ∣_ ι.opensRange),
      ← morphismRestrict_comp, ← isIso_comp_right_iff _ ι.isoOpensRange.inv]

Premises used: AlgebraicGeometry.Scheme.Hom.isoOpensRange, CategoryTheory.isIso_comp_right_iff, AlgebraicGeometry.Scheme.Hom.opensRange, AlgebraicGeometry.morphismRestrict_comp, CategoryTheory.Iso.hom, AlgebraicGeometry.morphismRestrict, CategoryTheory.Iso.inv
-- 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
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
a₁ : V ≤ toNormalization (pullback.snd f fT) ⁻¹ᵁ e.hom ⁻¹ᵁ opensRange ι
⊢ toNormalization (pullback.snd f fT) ⁻¹ᵁ e.hom ⁻¹ᵁ opensRange ι = V

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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
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₁ : ∀ (h : a ∉ V), False
⊢ a ∈ V

Tactic:
by_contra h
-- 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
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
⊢ a ∈ W

Tactic:
hVW'.ge h

Premises used: Eq.ge
-- 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
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
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
⊢ False

Tactic:
lift a to W using hVW'.ge h

Premises used: Eq.ge
-- 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
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 (α :=
    (↑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⟩
-- 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
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)))

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
-- 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
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
h : (↑a : ↥(pullback f fT)) ∉ V
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)))
⊢ False

Tactic:
Set.disjoint_iff_forall_ne.mp
          (isCompl_range_inl_inr V (W.ι ≫ pullback.snd f fT).normalization).1 ⟨_, rfl⟩ ⟨_, rfl⟩ hab

Premises used: CategoryTheory.Limits.pullback.snd, AlgebraicGeometry.isCompl_range_inl_inr, Set.disjoint_iff_forall_ne, Exists.intro, CategoryTheory.CategoryStruct.comp, Iff.mp, AlgebraicGeometry.Scheme.Opens.ι, AlgebraicGeometry.Scheme.Opens.toScheme, IsCompl.disjoint, AlgebraicGeometry.Scheme.Hom.normalization, rfl
-- 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
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
h : (↑a : ↥(pullback f fT)) ∉ V
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)))
⊢ False

Tactic:
exact Set.disjoint_iff_forall_ne.mp
          (isCompl_range_inl_inr V (W.ι ≫ pullback.snd f fT).normalization).1 ⟨_, rfl⟩ ⟨_, rfl⟩ hab

Premises used: CategoryTheory.Limits.pullback.snd, AlgebraicGeometry.isCompl_range_inl_inr, Set.disjoint_iff_forall_ne, Exists.intro, CategoryTheory.CategoryStruct.comp, Iff.mp, AlgebraicGeometry.Scheme.Opens.ι, AlgebraicGeometry.Scheme.Opens.toScheme, IsCompl.disjoint, AlgebraicGeometry.Scheme.Hom.normalization, rfl
-- 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
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 :
  (↑V : Set ↥(pullback f fT)) ⊆
    (↑(toNormalization (pullback.snd f fT) ⁻¹ᵁ e.inv ''ᵁ opensRange ι) : Set ↥(pullback f fT))
⊢ V ≤ toNormalization (pullback.snd f fT) ⁻¹ᵁ e.hom ⁻¹ᵁ opensRange ι

Tactic:
rw [← Scheme.Hom.inv_image, ← SetLike.coe_subset_coe]

Premises used: SetLike.coe_subset_coe, AlgebraicGeometry.Scheme.Hom.inv_image
-- 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
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 : Set ↥(pullback f fT)) ⊆
    (↑(toNormalization (pullback.snd f fT) ⁻¹ᵁ e.inv ''ᵁ opensRange ι) : Set ↥(pullback f fT))

Tactic:
simpa [← Scheme.Hom.opensRange_comp, ι, e, Scheme.Hom.normalizationCoprodIso,
          Set.range_comp] using Set.subset_preimage_image _ _

Premises used: Set.range_comp, AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso, AlgebraicGeometry.Scheme.Hom.opensRange_comp, Set.subset_preimage_image