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_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
simp :
  Eq (α := ↥(normalization f)) ((toNormalization (pullback.snd f fT) ≫ fTn) x : ↥(normalization f))
    ((pullback.fst f fT ≫ toNormalization f) x : ↥(normalization f))
⊢ 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:
simp only [← Scheme.Hom.comp_apply]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
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
e_a : toNormalization (pullback.snd f fT) ≫ fTn = pullback.fst f fT ≫ toNormalization f
⊢ Eq (α := ↥(normalization f)) ((toNormalization (pullback.snd f fT) ≫ fTn) x : ↥(normalization f))
    ((pullback.fst f fT ≫ toNormalization f) x : ↥(normalization f))

Tactic:
congr 5
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
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
⊢ toNormalization (pullback.snd f fT) ≫ fTn = pullback.fst f fT ≫ toNormalization f

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

Tactic:
.of_bot (t := isPullback_morphismRestrict ..) ?_ ?_

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

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

Tactic:
.paste_vert (isPullback_morphismRestrict ..) ?_

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

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

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

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

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

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

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

Tactic:
simp [fTn]