awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
h :
  ValuativeCriterion.Uniqueness f ∧
      QuasiSeparated f ∧ ValuativeCriterion.Existence f ∧ QuasiCompact f ∧ LocallyOfFiniteType f →
    ValuativeCriterion.Existence f ∧
      ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f
h₁ :
  ValuativeCriterion.Existence f ∧
      ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f →
    ValuativeCriterion.Uniqueness f ∧
      QuasiSeparated f ∧ ValuativeCriterion.Existence f ∧ QuasiCompact f ∧ LocallyOfFiniteType f
h₂ h₃ :
  ValuativeCriterion.Uniqueness f →
    QuasiSeparated f →
      ValuativeCriterion.Existence f →
        QuasiCompact f →
          LocallyOfFiniteType f →
            ValuativeCriterion.Existence f ∧
              ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f
h₄ :
  ValuativeCriterion.Uniqueness f →
    QuasiSeparated f →
      ValuativeCriterion.Existence f → QuasiCompact f → LocallyOfFiniteType f → ValuativeCriterion.Existence f
h₅ :
  ValuativeCriterion.Uniqueness f →
    QuasiSeparated f →
      ValuativeCriterion.Existence f → QuasiCompact f → LocallyOfFiniteType f → ValuativeCriterion.Uniqueness f
h₆ :
  ValuativeCriterion.Uniqueness f →
    QuasiSeparated f → ValuativeCriterion.Existence f → QuasiCompact f → LocallyOfFiniteType f → QuasiCompact f
h₇ :
  ValuativeCriterion.Uniqueness f →
    QuasiSeparated f → ValuativeCriterion.Existence f → QuasiCompact f → LocallyOfFiniteType f → QuasiSeparated f
h₈ :
  ValuativeCriterion.Uniqueness f →
    QuasiSeparated f → ValuativeCriterion.Existence f → QuasiCompact f → LocallyOfFiniteType f → LocallyOfFiniteType f
h₉ h₁₀ :
  ValuativeCriterion.Existence f →
    ValuativeCriterion.Uniqueness f →
      QuasiCompact f →
        QuasiSeparated f →
          LocallyOfFiniteType f →
            ValuativeCriterion.Uniqueness f ∧
              QuasiSeparated f ∧ ValuativeCriterion.Existence f ∧ QuasiCompact f ∧ LocallyOfFiniteType f
h₁₁ :
  ValuativeCriterion.Existence f →
    ValuativeCriterion.Uniqueness f →
      QuasiCompact f → QuasiSeparated f → LocallyOfFiniteType f → ValuativeCriterion.Uniqueness f
h₁₂ :
  ValuativeCriterion.Existence f →
    ValuativeCriterion.Uniqueness f → QuasiCompact f → QuasiSeparated f → LocallyOfFiniteType f → QuasiSeparated f
h₁₃ :
  ValuativeCriterion.Existence f →
    ValuativeCriterion.Uniqueness f →
      QuasiCompact f → QuasiSeparated f → LocallyOfFiniteType f → ValuativeCriterion.Existence f
h₁₄ :
  ValuativeCriterion.Existence f →
    ValuativeCriterion.Uniqueness f → QuasiCompact f → QuasiSeparated f → LocallyOfFiniteType f → QuasiCompact f
h₁₅ :
  ValuativeCriterion.Existence f →
    ValuativeCriterion.Uniqueness f → QuasiCompact f → QuasiSeparated f → LocallyOfFiniteType f → LocallyOfFiniteType f
⊢ ValuativeCriterion.Uniqueness f ∧
      QuasiSeparated f ∧ ValuativeCriterion.Existence f ∧ QuasiCompact f ∧ LocallyOfFiniteType f ↔
    ValuativeCriterion.Existence f ∧
      ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f

Tactic:
tauto
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
inst_2 : LocallyOfFiniteType f
H : ValuativeCriterion f
rw : (ValuativeCriterion ⊓ @QuasiCompact ⊓ @QuasiSeparated ⊓ @LocallyOfFiniteType) f
⊢ IsProper f

Tactic:
rw [eq_valuativeCriterion]

Premises used: AlgebraicGeometry.IsProper.eq_valuativeCriterion
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
inst_2 : LocallyOfFiniteType f
H : ValuativeCriterion f
⊢ (ValuativeCriterion ⊓ @QuasiCompact ⊓ @QuasiSeparated ⊓ @LocallyOfFiniteType) f

Tactic:
⟨⟨⟨‹_›, ‹_›⟩, ‹_›⟩, ‹_›⟩

Premises used: And.intro
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
inst_2 : LocallyOfFiniteType f
H : ValuativeCriterion f
⊢ (ValuativeCriterion ⊓ @QuasiCompact ⊓ @QuasiSeparated ⊓ @LocallyOfFiniteType) f

Tactic:
exact ⟨⟨⟨‹_›, ‹_›⟩, ‹_›⟩, ‹_›⟩
-- 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
obtain :
  ∀ (T : Scheme.{u}) (fT : T ⟶ Y),
    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),
        IsFinite (V.ι ≫ pullback.snd f fT) →
          ∀ (hv₂ : (pullback.fst f fT) (↑v : ↥(pullback f fT)) = x),
            ∃ (V : (normalization f).Opens),
              Membership.mem (α := ↥(normalization f)) V ((toNormalization f) x : ↥(normalization f)) ∧
                IsIso (X := (↑(toNormalization f ⁻¹ᵁ V) : Scheme)) (toNormalization f ∣_ V)
⊢ ∃ (V : (normalization f).Opens),
    Membership.mem (α := ↥(normalization f)) V ((toNormalization f) x : ↥(normalization f)) ∧
      IsIso (X := (↑(toNormalization f ⁻¹ᵁ V) : Scheme)) (toNormalization f ∣_ V)

Tactic:
obtain ⟨T, fT, _, ⟨u, hu⟩, V, W, v, hVW, _, hv₂⟩ := exists_etale_isCompl_of_quasiFiniteAt _ rfl hx

Premises used: rfl, AlgebraicGeometry.exists_etale_isCompl_of_quasiFiniteAt
-- 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
⊢ (↑W : Set ↥(pullback f fT)) = (↑V : Set ↥(pullback f fT))ᶜ

Tactic:
have hVW' : (W : Set ↑(pullback f fT)) = (↑V)ᶜ :=
      eq_compl_iff_isCompl.mpr (hVW.map TopologicalSpace.Opens.frameHom).symm
-- 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))ᶜ
⊢ IsClosed (X := ↥(pullback f fT)) (Set.range (ι := ↥(↑V : Scheme)) ⇑V.ι)

Tactic:
simp [eq_compl_comm.mp hVW', W.isOpen]

Premises used: TopologicalSpace.Opens.isOpen, Iff.mp, eq_compl_comm
-- 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))ᶜ
⊢ IsClosedImmersion V.ι

Tactic:
have : IsClosedImmersion V.ι := .of_isPreimmersion _ (by simp [eq_compl_comm.mp hVW', W.isOpen])
-- 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 : IsClosedImmersion V.ι
⊢ IsClosed (X := ↥(pullback f fT)) (Set.range (ι := ↥(↑W : Scheme)) ⇑W.ι)

Tactic:
simpa [hVW'] using V.2

Premises used: TopologicalSpace.Opens.is_open'
-- 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 : IsClosedImmersion V.ι
⊢ IsClosedImmersion W.ι

Tactic:
have : IsClosedImmersion W.ι := .of_isPreimmersion _ (by simpa [hVW'] using V.2)
-- 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.ι
⊢ IsCompl (opensRange V.ι) (opensRange W.ι)

Tactic:
simpa
-- 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.ι
obtain :
  ∀ (H : IsColimit (BinaryCofan.mk V.ι W.ι)),
    ∃ (U : (normalization (X := pullback f fT) (pullback.snd f fT)).Opens),
      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))) ∧
        IsIso (X := (↑(toNormalization (pullback.snd f fT) ⁻¹ᵁ U) : Scheme)) (toNormalization (pullback.snd f fT) ∣_ U)
⊢ ∃ (U : (normalization (X := pullback f fT) (pullback.snd f fT)).Opens),
    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))) ∧
      IsIso (X := (↑(toNormalization (pullback.snd f fT) ⁻¹ᵁ U) : Scheme)) (toNormalization (pullback.snd f fT) ∣_ U)

Tactic:
obtain ⟨H⟩ := nonempty_isColimit_binaryCofanMk_of_isCompl V.ι W.ι (by simpa)

Premises used: AlgebraicGeometry.Scheme.Opens.ι, AlgebraicGeometry.nonempty_isColimit_binaryCofanMk_of_isCompl
-- 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
⊢ ∃ (U : (normalization (X := pullback f fT) (pullback.snd f fT)).Opens),
    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))) ∧
      IsIso (X := (↑(toNormalization (pullback.snd f fT) ⁻¹ᵁ U) : Scheme)) (toNormalization (pullback.snd f fT) ∣_ U)

Tactic:
⟨e.hom ⁻¹ᵁ ι.opensRange, ⟨v, ?_⟩, ?_⟩

Premises used: AlgebraicGeometry.Scheme.Hom.opensRange, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', And.intro, Exists.intro, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, CategoryTheory.Iso.hom, CategoryTheory.Functor.obj
-- 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_1 :
  Eq (α := ↥((↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT)))
    (ι v : ↥((↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT)))
    (e.hom
        ((toNormalization (pullback.snd f fT)) (↑v : ↥(pullback f fT)) :
          ↥(normalization (X := pullback f fT) (pullback.snd f fT))) :
      ↥((↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT)))
refine_2 :
  IsIso (X := (↑(toNormalization (pullback.snd f fT) ⁻¹ᵁ e.hom ⁻¹ᵁ opensRange ι) : Scheme))
    (toNormalization (pullback.snd f fT) ∣_ e.hom ⁻¹ᵁ opensRange ι)
⊢ ∃ (U : (normalization (X := pullback f fT) (pullback.snd f fT)).Opens),
    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))) ∧
      IsIso (X := (↑(toNormalization (pullback.snd f fT) ⁻¹ᵁ U) : Scheme)) (toNormalization (pullback.snd f fT) ∣_ U)

Tactic:
refine ⟨e.hom ⁻¹ᵁ ι.opensRange, ⟨v, ?_⟩, ?_⟩
-- 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_1 :
  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)))
⊢ Eq (α := ↥((↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT)))
    (ι v : ↥((↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT)))
    (e.hom
        ((toNormalization (pullback.snd f fT)) (↑v : ↥(pullback f fT)) :
          ↥(normalization (X := pullback f fT) (pullback.snd f fT))) :
      ↥((↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT)))

Tactic:
rw [← V.ι_apply, ← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply, AlgebraicGeometry.Scheme.Opens.ι_apply
-- 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_1 : ι = V.ι ≫ toNormalization (pullback.snd f fT) ≫ e.hom
⊢ 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)))

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 : ↥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_1 : ι ≫ e.inv = V.ι ≫ toNormalization (pullback.snd f fT)
⊢ ι = V.ι ≫ toNormalization (pullback.snd f fT) ≫ e.hom

Tactic:
rw [← Category.assoc, ← Iso.comp_inv_eq]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.comp_inv_eq
-- 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
⊢ ι ≫ e.inv = V.ι ≫ toNormalization (pullback.snd f fT)

Tactic:
simp [ι, e, Scheme.Hom.normalizationCoprodIso]

Premises used: AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso