-- 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_2 : 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
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
⊢ Eq (α := ↥((↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT)))
    (ι b : ↥((↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT)))
    ((W.ι ≫
          CategoryStruct.comp (Y := normalization (X := pullback f fT) (pullback.snd f fT))
            (toNormalization (pullback.snd f fT))
            (Iso.hom
              (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)))))
        a :
      ↥((↑V : Scheme) ⨿ normalization (W.ι ≫ pullback.snd f fT)))

Tactic:
simp only [← W.ι_apply, ← Scheme.Hom.comp_apply, Category.assoc, e] at hab

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Hom.comp_apply, AlgebraicGeometry.Scheme.Opens.ι_apply