Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
⊢ ∃ U, IsIso (toNormalization f ∣_ U) ∧ (toNormalization f ⁻¹ᵁ U).carrier = {x | QuasiFiniteAt f x}

Tactic:
choose V hxV hV using fun x : { x // f.QuasiFiniteAt x } ↦
    f.exists_mem_and_isIso_morphismRestrict_toNormalization x x.2
  let 𝒰 := Opens.iSupOpenCover V
  have : IsIso (f.toNormalization ∣_ ⨆ x, V x) := by
    refine (IsZariskiLocalAtTarget.iff_of_openCover (P := .isomorphisms _) 𝒰).mpr fun x ↦ ?_
    refine (MorphismProperty.arrow_mk_iso_iff (.isomorphisms _)
      ((morphismRestrictRestrict ..).symm ≪≫ morphismRestrictOpensRange ..)).mp ?_
    have : Opens.ι _ ''ᵁ (𝒰.f x).opensRange = V x := by
      simp only [Opens.iSupOpenCover, 𝒰, ← opensRange_comp, homOfLE_ι, Opens.opensRange_ι]
    convert! hV x
  refine ⟨⨆ x : { x | f.QuasiFiniteAt x }, V x, this, ?_⟩
  ext x
  suffices (∃ i : { x | f.QuasiFiniteAt x }, toNormalization f x ∈ V i) ↔ f.QuasiFiniteAt x by
    simpa
  refine ⟨?_, fun h ↦ ⟨⟨x, h⟩, hxV _⟩⟩
  rintro ⟨y, hxVy⟩
  obtain ⟨U, r, hU, hr, hxV, hrV⟩ :
      ∃ (U : Y.Opens) (r : Γ(f.normalization, f.fromNormalization ⁻¹ᵁ U)),
      IsAffineOpen U ∧ IsAffineOpen (f.toNormalization ⁻¹ᵁ f.normalization.basicOpen r) ∧
      x ∈ f.toNormalization ⁻¹ᵁ f.normalization.basicOpen r ∧ Scheme.basicOpen _ r ≤ V y := by
    obtain ⟨_, ⟨W, hW, rfl⟩, hxW, hWV : W ≤ _⟩ := X.isBasis_affineOpens.exists_subset_of_mem_open
      hxVy (f.toNormalization ⁻¹ᵁ V y).isOpen
    have : IsAffine W := hW
    let V' := (X.homOfLE hWV ≫ f.toNormalization ∣_ V y ≫ (V y).ι).opensRange
    have hV' : IsAffineOpen V' := isAffineOpen_opensRange _
    have hV'V : V' ≤ V y := by
      simp_rw [V', ← Category.assoc, opensRange_comp]
      exact (image_le_opensRange _ _).trans (by simp)
    have hV'W : f.toNormalization ⁻¹ᵁ V' = W := by
      have : (f.toNormalization ⁻¹ᵁ V y).ι ⁻¹ᵁ f.toNormalization ⁻¹ᵁ V' =
          (f.toNormalization ⁻¹ᵁ V y).ι ⁻¹ᵁ W := by
        rw [← Scheme.Hom.comp_preimage, ← morphismRestrict_ι]
        simp only [V', opensRange_comp, Scheme.Hom.preimage_image_eq, opensRange_homOfLE]
      simpa only [image_preimage_eq_opensRange_inf, Opens.opensRange_ι, ← preimage_inf,
        inf_eq_right.mpr, hV'V, hWV] using congr((f.toNormalization ⁻¹ᵁ V y).ι ''ᵁ $this)
    obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ := Y.isBasis_affineOpens.exists_subset_of_mem_open
      (Set.mem_univ (f x)) isOpen_univ
    obtain ⟨f₁, f₂, e, hxf⟩ := exists_basicOpen_le_affine_inter (hU.preimage f.fromNormalization)
      hV' (f.toNormalization x) ⟨by simpa [← Scheme.Hom.comp_apply], hV'W.ge hxW⟩
    refine ⟨U, f₁, hU, ?_, hxf, (e.trans_le (f.normalization.basicOpen_le _)).trans hV'V⟩
    rw [e, preimage_basicOpen]
    exact IsAffineOpen.basicOpen (hV'W ▸ hW) _
  let W := f.toNormalization ⁻¹ᵁ f.normalization.basicOpen r
  have H : W ≤ f ⁻¹ᵁ U := by
    unfold W
    grw [Scheme.basicOpen_le, ← Scheme.Hom.comp_preimage, f.toNormalization_fromNormalization]
  have H' : f.fromNormalization.appLE _ _ ((normalization f).basicOpen_le _) ≫
    f.toNormalization.app _ = f.appLE U W H := by
    simp only [app_eq_appLE]
    exact (appLE_comp_appLE _ _ _ _ _ _ _).trans (by simp [W])
  have : IsIso ((toNormalization f).app ((normalization f).basicOpen r)) := by
    have H : (f.toNormalization ∣_ V y) ⁻¹ᵁ (V y).ι ⁻¹ᵁ (normalization f).basicOpen r =
        (Scheme.homOfLE _ (f.toNormalization.preimage_mono hrV)).opensRange := by
      apply Scheme.Hom.image_injective (f.toNormalization ∣_ V y)
      simp only [opensRange_homOfLE, image_preimage_eq_opensRange_inf]
      rw [← Scheme.Hom.comp_preimage, ← morphismRestrict_ι, Scheme.Hom.comp_preimage,
        image_preimage_eq_opensRange_inf]
    have := (inferInstance : IsIso ((toNormalization f ∣_ V y).app
      (Scheme.homOfLE _ hrV).opensRange))
    simp only [Opens.toScheme_presheaf_obj, app_eq_appLE, morphismRestrict_appLE] at this ⊢
    convert! this <;>
      simp [Scheme.Hom.image_preimage_eq_opensRange_inf, -Scheme.preimage_basicOpen,
        f.toNormalization.preimage_mono, hrV, H]
  have : (f.appLE U W H).hom.QuasiFinite := by
    have : (f.appLE U W H).hom.FiniteType := f.finiteType_appLE hU hr H
    rw [← H', CommRingCat.hom_comp, RingHom.finiteType_respectsIso.cancel_right_isIso] at this
    rw [← H', CommRingCat.hom_comp, RingHom.QuasiFinite.respectsIso.cancel_right_isIso]
    exact .of_isIntegral_of_finiteType (IsIntegralHom.isIntegral_app f.fromNormalization _ hU)
      ⟨r, (hU.preimage f.fromNormalization).isLocalization_basicOpen _⟩ this
  have hxU : f x ∈ U := by
    convert! show _ ∈ U from (normalization f).basicOpen_le _ hxV
    rw [← Scheme.Hom.comp_apply, f.toNormalization_fromNormalization]
  refine .of_comp (g := (Y.presheaf.germ U _ hxU).hom) ?_
  rw [← CommRingCat.hom_comp, f.germ_stalkMap, ← X.presheaf.germ_res (homOfLE H) _ hxV,
    app_eq_appLE, appLE_map_assoc, CommRingCat.hom_comp]
  refine .comp ?_ this
  have := hr.isLocalization_stalk ⟨x, hxV⟩
  let := X.presheaf.algebra_section_stalk ⟨x, hxV⟩
  rw [← RingHom.algebraMap_toAlgebra (X.presheaf.germ _ _ _).hom, @RingHom.quasiFinite_algebraMap]
  exact .of_isLocalization (hr.primeIdealOf ⟨x, hxV⟩).asIdeal.primeCompl

Goal state after: