Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV✝ : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
this✝ : IsIso (toNormalization f ∣_ ⨆ x, V x)
x : ↥X
y : ↑{x | QuasiFiniteAt f x}
hxVy : (toNormalization f) x ∈ V y
U : Y.Opens
r : ↑Γ(normalization f, fromNormalization f ⁻¹ᵁ U)
hU : IsAffineOpen U
hr : IsAffineOpen (toNormalization f ⁻¹ᵁ (normalization f).basicOpen r)
hxV : x ∈ toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
hrV : (normalization f).basicOpen r ≤ V y
W : X.Opens := toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
H✝ : W ≤ f ⁻¹ᵁ U
H' :
  appLE (fromNormalization f) U ((normalization f).basicOpen r) ⋯ ≫
      app (toNormalization f) ((normalization f).basicOpen r) =
    appLE f U W H✝
H : (toNormalization f ∣_ V y) ⁻¹ᵁ (V y).ι ⁻¹ᵁ (normalization f).basicOpen r = opensRange (X.homOfLE ⋯)
this :
  IsIso
    (appLE (toNormalization f) ((V y).ι ''ᵁ opensRange ((normalization f).homOfLE hrV))
      ((toNormalization f ⁻¹ᵁ V y).ι ''ᵁ (toNormalization f ∣_ V y) ⁻¹ᵁ opensRange ((normalization f).homOfLE hrV)) ⋯)
⊢ IsIso
    (appLE (toNormalization f) ((normalization f).basicOpen r) (toNormalization f ⁻¹ᵁ (normalization f).basicOpen r) ⋯)

Tactic:
convert! this

Goal state after:
case e'_3
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV✝ : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
this✝ : IsIso (toNormalization f ∣_ ⨆ x, V x)
x : ↥X
y : ↑{x | QuasiFiniteAt f x}
hxVy : (toNormalization f) x ∈ V y
U : Y.Opens
r : ↑Γ(normalization f, fromNormalization f ⁻¹ᵁ U)
hU : IsAffineOpen U
hr : IsAffineOpen (toNormalization f ⁻¹ᵁ (normalization f).basicOpen r)
hxV : x ∈ toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
hrV : (normalization f).basicOpen r ≤ V y
W : X.Opens := toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
H✝ : W ≤ f ⁻¹ᵁ U
H' :
  appLE (fromNormalization f) U ((normalization f).basicOpen r) ⋯ ≫
      app (toNormalization f) ((normalization f).basicOpen r) =
    appLE f U W H✝
H : (toNormalization f ∣_ V y) ⁻¹ᵁ (V y).ι ⁻¹ᵁ (normalization f).basicOpen r = opensRange (X.homOfLE ⋯)
this :
  IsIso
    (appLE (toNormalization f) ((V y).ι ''ᵁ opensRange ((normalization f).homOfLE hrV))
      ((toNormalization f ⁻¹ᵁ V y).ι ''ᵁ (toNormalization f ∣_ V y) ⁻¹ᵁ opensRange ((normalization f).homOfLE hrV)) ⋯)
⊢ (normalization f).basicOpen r = (V y).ι ''ᵁ opensRange ((normalization f).homOfLE hrV)

case e'_4
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV✝ : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
this✝ : IsIso (toNormalization f ∣_ ⨆ x, V x)
x : ↥X
y : ↑{x | QuasiFiniteAt f x}
hxVy : (toNormalization f) x ∈ V y
U : Y.Opens
r : ↑Γ(normalization f, fromNormalization f ⁻¹ᵁ U)
hU : IsAffineOpen U
hr : IsAffineOpen (toNormalization f ⁻¹ᵁ (normalization f).basicOpen r)
hxV : x ∈ toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
hrV : (normalization f).basicOpen r ≤ V y
W : X.Opens := toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
H✝ : W ≤ f ⁻¹ᵁ U
H' :
  appLE (fromNormalization f) U ((normalization f).basicOpen r) ⋯ ≫
      app (toNormalization f) ((normalization f).basicOpen r) =
    appLE f U W H✝
H : (toNormalization f ∣_ V y) ⁻¹ᵁ (V y).ι ⁻¹ᵁ (normalization f).basicOpen r = opensRange (X.homOfLE ⋯)
this :
  IsIso
    (appLE (toNormalization f) ((V y).ι ''ᵁ opensRange ((normalization f).homOfLE hrV))
      ((toNormalization f ⁻¹ᵁ V y).ι ''ᵁ (toNormalization f ∣_ V y) ⁻¹ᵁ opensRange ((normalization f).homOfLE hrV)) ⋯)
⊢ toNormalization f ⁻¹ᵁ (normalization f).basicOpen r =
    (toNormalization f ⁻¹ᵁ V y).ι ''ᵁ (toNormalization f ∣_ V y) ⁻¹ᵁ opensRange ((normalization f).homOfLE hrV)

case e'_5.e'_4
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV✝ : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
this✝ : IsIso (toNormalization f ∣_ ⨆ x, V x)
x : ↥X
y : ↑{x | QuasiFiniteAt f x}
hxVy : (toNormalization f) x ∈ V y
U : Y.Opens
r : ↑Γ(normalization f, fromNormalization f ⁻¹ᵁ U)
hU : IsAffineOpen U
hr : IsAffineOpen (toNormalization f ⁻¹ᵁ (normalization f).basicOpen r)
hxV : x ∈ toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
hrV : (normalization f).basicOpen r ≤ V y
W : X.Opens := toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
H✝ : W ≤ f ⁻¹ᵁ U
H' :
  appLE (fromNormalization f) U ((normalization f).basicOpen r) ⋯ ≫
      app (toNormalization f) ((normalization f).basicOpen r) =
    appLE f U W H✝
H : (toNormalization f ∣_ V y) ⁻¹ᵁ (V y).ι ⁻¹ᵁ (normalization f).basicOpen r = opensRange (X.homOfLE ⋯)
this :
  IsIso
    (appLE (toNormalization f) ((V y).ι ''ᵁ opensRange ((normalization f).homOfLE hrV))
      ((toNormalization f ⁻¹ᵁ V y).ι ''ᵁ (toNormalization f ∣_ V y) ⁻¹ᵁ opensRange ((normalization f).homOfLE hrV)) ⋯)
e_3✝ :
  Γ(normalization f, (normalization f).basicOpen r) =
    Γ(normalization f, (V y).ι ''ᵁ opensRange ((normalization f).homOfLE hrV))
e_4✝ :
  Γ(X, toNormalization f ⁻¹ᵁ (normalization f).basicOpen r) =
    Γ(X, (toNormalization f ⁻¹ᵁ V y).ι ''ᵁ (toNormalization f ∣_ V y) ⁻¹ᵁ opensRange ((normalization f).homOfLE hrV))
⊢ (normalization f).basicOpen r = (V y).ι ''ᵁ opensRange ((normalization f).homOfLE hrV)

case e'_5.e'_5
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV✝ : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
this✝ : IsIso (toNormalization f ∣_ ⨆ x, V x)
x : ↥X
y : ↑{x | QuasiFiniteAt f x}
hxVy : (toNormalization f) x ∈ V y
U : Y.Opens
r : ↑Γ(normalization f, fromNormalization f ⁻¹ᵁ U)
hU : IsAffineOpen U
hr : IsAffineOpen (toNormalization f ⁻¹ᵁ (normalization f).basicOpen r)
hxV : x ∈ toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
hrV : (normalization f).basicOpen r ≤ V y
W : X.Opens := toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
H✝ : W ≤ f ⁻¹ᵁ U
H' :
  appLE (fromNormalization f) U ((normalization f).basicOpen r) ⋯ ≫
      app (toNormalization f) ((normalization f).basicOpen r) =
    appLE f U W H✝
H : (toNormalization f ∣_ V y) ⁻¹ᵁ (V y).ι ⁻¹ᵁ (normalization f).basicOpen r = opensRange (X.homOfLE ⋯)
this :
  IsIso
    (appLE (toNormalization f) ((V y).ι ''ᵁ opensRange ((normalization f).homOfLE hrV))
      ((toNormalization f ⁻¹ᵁ V y).ι ''ᵁ (toNormalization f ∣_ V y) ⁻¹ᵁ opensRange ((normalization f).homOfLE hrV)) ⋯)
e_3✝ :
  Γ(normalization f, (normalization f).basicOpen r) =
    Γ(normalization f, (V y).ι ''ᵁ opensRange ((normalization f).homOfLE hrV))
e_4✝ :
  Γ(X, toNormalization f ⁻¹ᵁ (normalization f).basicOpen r) =
    Γ(X, (toNormalization f ⁻¹ᵁ V y).ι ''ᵁ (toNormalization f ∣_ V y) ⁻¹ᵁ opensRange ((normalization f).homOfLE hrV))
⊢ toNormalization f ⁻¹ᵁ (normalization f).basicOpen r =
    (toNormalization f ⁻¹ᵁ V y).ι ''ᵁ (toNormalization f ∣_ V y) ⁻¹ᵁ opensRange ((normalization f).homOfLE hrV)