awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : Type u)
trans :
  Eq (α := pullback f (↑U : Y.Opens).ι ⟶ normalization f)
    ((Iso.hom (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫ (f ⁻¹ᵁ (↑U : Y.Opens)).ι) ≫ toNormalization f)
    ((Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).f U ≫ toNormalization f)
⊢ Eq (α := pullback f (↑U : Y.Opens).ι ⟶ normalization f)
    ((Iso.hom (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫ (f ⁻¹ᵁ (↑U : Y.Opens)).ι) ≫ toNormalization f)
    (Iso.hom (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫
      (f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫
        CategoryStruct.comp (Y :=
          Spec
            (CommRingCat.of ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))
          (Spec.map
            (CommRingCat.ofHom
              (AlgHom.toRingHom
                (Subalgebra.val
                  (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))))
          (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U))
have trans₁ : Eq (α := pullback f (↑U : Y.Opens).ι ⟶ normalization f)
  ((Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).f U ≫ toNormalization f)
  (Iso.hom (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫
    (f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫
      CategoryStruct.comp (Y :=
        Spec
          (CommRingCat.of ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))
        (Spec.map
          (CommRingCat.ofHom
            (AlgHom.toRingHom
              (Subalgebra.val
                (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U))
Tactic: trans ((directedCover Y).pullback₁ f).f U ≫ f.toNormalization
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : Type u)
⊢ Eq (α := pullback f (↑U : Y.Opens).ι ⟶ normalization f)
    ((Iso.hom (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫ (f ⁻¹ᵁ (↑U : Y.Opens)).ι) ≫ toNormalization f)
    ((Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).f U ≫ toNormalization f)
have e_a : Iso.hom (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫ (f ⁻¹ᵁ (↑U : Y.Opens)).ι =
  (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).f U
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : Type u)
⊢ Eq (α := pullback f (↑U : Y.Opens).ι ⟶ normalization f)
    ((Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).f U ≫
      OpenCover.glueMorphismsOfLocallyDirected (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y))
        (fun (U : (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).I₀) ↦
          Iso.hom (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫
            (f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫
              CategoryStruct.comp (Y :=
                Spec
                  (CommRingCat.of
                    ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))
                (Spec.map
                  (CommRingCat.ofHom
                    (AlgHom.toRingHom
                      (Subalgebra.val
                        (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))))
                (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U))
        ⋯)
    (Iso.hom (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫
      (f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫
        CategoryStruct.comp (Y :=
          Spec
            (CommRingCat.of ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))
          (Spec.map
            (CommRingCat.ofHom
              (AlgHom.toRingHom
                (Subalgebra.val
                  (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))))
          (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U))
have pf : HasPullback f (↑U : Y.Opens).ι
Tactic: generalize_proofs _ _ _ _ H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : Type u)
pf : HasPullback f (↑U : Y.Opens).ι
⊢ Eq (α := pullback f (↑U : Y.Opens).ι ⟶ normalization f)
    ((Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).f U ≫
      OpenCover.glueMorphismsOfLocallyDirected (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y))
        (fun (U : (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).I₀) ↦
          Iso.hom (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫
            (f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫
              CategoryStruct.comp (Y :=
                Spec
                  (CommRingCat.of
                    ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))
                (Spec.map
                  (CommRingCat.ofHom
                    (AlgHom.toRingHom
                      (Subalgebra.val
                        (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))))
                (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U))
        ⋯)
    (Iso.hom (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫
      (f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫
        CategoryStruct.comp (Y :=
          Spec
            (CommRingCat.of ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))
          (Spec.map
            (CommRingCat.ofHom
              (AlgHom.toRingHom
                (Subalgebra.val
                  (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))))
          (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U))
have pf₁ : (precoverage IsOpenImmersion).IsStableUnderBaseChange
Tactic: generalize_proofs _ _ _ _ H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : Type u)
pf : HasPullback f (↑U : Y.Opens).ι
pf₁ : (precoverage IsOpenImmersion).IsStableUnderBaseChange
⊢ Eq (α := pullback f (↑U : Y.Opens).ι ⟶ normalization f)
    ((Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).f U ≫
      OpenCover.glueMorphismsOfLocallyDirected (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y))
        (fun (U : (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).I₀) ↦
          Iso.hom (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫
            (f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫
              CategoryStruct.comp (Y :=
                Spec
                  (CommRingCat.of
                    ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))
                (Spec.map
                  (CommRingCat.ofHom
                    (AlgHom.toRingHom
                      (Subalgebra.val
                        (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))))
                (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U))
        ⋯)
    (Iso.hom (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫
      (f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫
        CategoryStruct.comp (Y :=
          Spec
            (CommRingCat.of ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))
          (Spec.map
            (CommRingCat.ofHom
              (AlgHom.toRingHom
                (Subalgebra.val
                  (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))))
          (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U))
have pf₂ : ∀ (i : (directedCover Y).I₀), HasPullback f ((directedCover Y).f i)
Tactic: generalize_proofs _ _ _ _ H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : Type u)
pf : HasPullback f (↑U : Y.Opens).ι
pf₁ : (precoverage IsOpenImmersion).IsStableUnderBaseChange
pf₂ : ∀ (i : (directedCover Y).I₀), HasPullback f ((directedCover Y).f i)
⊢ Eq (α := pullback f (↑U : Y.Opens).ι ⟶ normalization f)
    ((Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).f U ≫
      OpenCover.glueMorphismsOfLocallyDirected (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y))
        (fun (U : (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).I₀) ↦
          Iso.hom (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫
            (f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫
              CategoryStruct.comp (Y :=
                Spec
                  (CommRingCat.of
                    ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))
                (Spec.map
                  (CommRingCat.ofHom
                    (AlgHom.toRingHom
                      (Subalgebra.val
                        (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))))
                (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U))
        ⋯)
    (Iso.hom (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫
      (f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫
        CategoryStruct.comp (Y :=
          Spec
            (CommRingCat.of ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))
          (Spec.map
            (CommRingCat.ofHom
              (AlgHom.toRingHom
                (Subalgebra.val
                  (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))))
          (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U))
have pf₃ : ∀ (U : (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).I₀), HasPullback f (↑U : Y.Opens).ι
Tactic: generalize_proofs _ _ _ _ H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
⊢ CategoryStruct.comp (Y := normalization f) (toNormalization f) (fromNormalization f) = f
have refine : ∀
  (U :
    (X.openCoverOfIsOpenCover
        (fun (k : (↑Y.affineOpens : Type u)) ↦
          (TopologicalSpace.Opens.comap f.base.hom' : (a : TopologicalSpace.Opens ↥Y) → TopologicalSpace.Opens ↥X)
            (↑k : Y.Opens))
        sorry).I₀),
  (X.openCoverOfIsOpenCover
            (fun (k : (↑Y.affineOpens : Type u)) ↦
              (TopologicalSpace.Opens.comap f.base.hom' : (a : TopologicalSpace.Opens ↥Y) → TopologicalSpace.Opens ↥X)
                (↑k : Y.Opens))
            sorry).f
        U ≫
      CategoryStruct.comp (Y := normalization f) (toNormalization f) (fromNormalization f) =
    (X.openCoverOfIsOpenCover
            (fun (k : (↑Y.affineOpens : Type u)) ↦
              (TopologicalSpace.Opens.comap f.base.hom' : (a : TopologicalSpace.Opens ↥Y) → TopologicalSpace.Opens ↥X)
                (↑k : Y.Opens))
            sorry).f
        U ≫
      f
Tactic: refine Scheme.Cover.hom_ext (X.openCoverOfIsOpenCover _
    (.comap (iSup_affineOpens_eq_top Y) f.base.1)) _ _ fun U ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U :
  (X.openCoverOfIsOpenCover
      (fun (k : (↑Y.affineOpens : Type u)) ↦
        (TopologicalSpace.Opens.comap f.base.hom' : (a : TopologicalSpace.Opens ↥Y) → TopologicalSpace.Opens ↥X)
          (↑k : Y.Opens))
      ⋯).I₀
⊢ (X.openCoverOfIsOpenCover
            (fun (k : (↑Y.affineOpens : Type u)) ↦
              (TopologicalSpace.Opens.comap f.base.hom' : (a : TopologicalSpace.Opens ↥Y) → TopologicalSpace.Opens ↥X)
                (↑k : Y.Opens))
            ⋯).f
        U ≫
      CategoryStruct.comp (Y := normalization f) (toNormalization f) (fromNormalization f) =
    (X.openCoverOfIsOpenCover
            (fun (k : (↑Y.affineOpens : Type u)) ↦
              (TopologicalSpace.Opens.comap f.base.hom' : (a : TopologicalSpace.Opens ↥Y) → TopologicalSpace.Opens ↥X)
                (↑k : Y.Opens))
            ⋯).f
        U ≫
      f
have refine : (f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫
    CategoryStruct.comp (Y :=
      Spec (CommRingCat.of ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))
      (Spec.map
        (CommRingCat.ofHom
          (AlgHom.toRingHom
            (Subalgebra.val
              (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))))
      (CategoryStruct.comp (Y := normalization f)
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U)
        (fromNormalization f)) =
  (X.openCoverOfIsOpenCover
          (fun (k : (↑Y.affineOpens : Type u)) ↦
            (TopologicalSpace.Opens.comap f.base.hom' : (a : TopologicalSpace.Opens ↥Y) → TopologicalSpace.Opens ↥X)
              (↑k : Y.Opens))
          sorry).f
      U ≫
    f
Tactic: refine (f.ι_toNormalization_assoc _ _).trans ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U :
  (X.openCoverOfIsOpenCover
      (fun (k : (↑Y.affineOpens : Type u)) ↦
        (TopologicalSpace.Opens.comap f.base.hom' : (a : TopologicalSpace.Opens ↥Y) → TopologicalSpace.Opens ↥X)
          (↑k : Y.Opens))
      ⋯).I₀
⊢ (f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫
      CategoryStruct.comp (Y :=
        Spec
          (CommRingCat.of ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))
        (Spec.map
          (CommRingCat.ofHom
            (AlgHom.toRingHom
              (Subalgebra.val
                (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))))
        (CategoryStruct.comp (Y := normalization f)
          (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U)
          (fromNormalization f)) =
    (X.openCoverOfIsOpenCover
            (fun (k : (↑Y.affineOpens : Type u)) ↦
              (TopologicalSpace.Opens.comap f.base.hom' : (a : TopologicalSpace.Opens ↥Y) → TopologicalSpace.Opens ↥X)
                (↑k : Y.Opens))
            ⋯).f
        U ≫
      f
have rw : (f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫
    Spec.map
        ((normalizationDiagramMap f).app (Opposite.op (↑U : Y.Opens)) ≫
          CommRingCat.ofHom
            (AlgHom.toRingHom
              (Subalgebra.val
                (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))) ≫
      IsAffineOpen.fromSpec sorry =
  (X.openCoverOfIsOpenCover
          (fun (k : (↑Y.affineOpens : Type u)) ↦
            (TopologicalSpace.Opens.comap f.base.hom' : (a : TopologicalSpace.Opens ↥Y) → TopologicalSpace.Opens ↥X)
              (↑k : Y.Opens))
          sorry).f
      U ≫
    f
Tactic: rw [f.ι_fromNormalization, ← Spec.map_comp_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U :
  (X.openCoverOfIsOpenCover
      (fun (k : (↑Y.affineOpens : Type u)) ↦
        (TopologicalSpace.Opens.comap f.base.hom' : (a : TopologicalSpace.Opens ↥Y) → TopologicalSpace.Opens ↥X)
          (↑k : Y.Opens))
      ⋯).I₀
⊢ (f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫
      Spec.map
          ((normalizationDiagramMap f).app (Opposite.op (↑U : Y.Opens)) ≫
            CommRingCat.ofHom
              (AlgHom.toRingHom
                (Subalgebra.val
                  (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))) ≫
        IsAffineOpen.fromSpec ⋯ =
    (X.openCoverOfIsOpenCover
            (fun (k : (↑Y.affineOpens : Type u)) ↦
              (TopologicalSpace.Opens.comap f.base.hom' : (a : TopologicalSpace.Opens ↥Y) → TopologicalSpace.Opens ↥X)
                (↑k : Y.Opens))
            ⋯).f
        U ≫
      f
have change : (f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫ Spec.map (app f (↑U : Y.Opens)) ≫ IsAffineOpen.fromSpec sorry =
  (f ⁻¹ᵁ (↑U : Y.Opens)).ι ≫ f
Tactic: change (f ⁻¹ᵁ U.1).toSpecΓ ≫ Spec.map (f.app _) ≫ U.2.fromSpec = (f ⁻¹ᵁ U.1).ι ≫ _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
⊢ IsIntegralHom (X := normalization f) (fromNormalization f)
have rw : ∀ (i : (↑Y.affineOpens : Type u)),
  IsIntegralHom (X := (↑(fromNormalization f ⁻¹ᵁ (↑i : Y.Opens)) : Scheme)) (fromNormalization f ∣_ (↑i : Y.Opens))
Tactic: rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := @IsIntegralHom) _
    (iSup_affineOpens_eq_top _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : Type u)
e : (↑(fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ≅
  PreZeroHypercover.X (S := normalization f) (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
    U :=
  IsOpenImmersion.isoOfRangeEq (Opens.ι (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)))
    (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U) ⋯
⊢ IsIntegralHom (X := (↑(fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (fromNormalization f ∣_ (↑U : Y.Opens))
have rw : IsIntegralHom ((e.inv ≫ fromNormalization f ∣_ (↑U : Y.Opens)) ≫ (IsAffineOpen.isoSpec sorry).hom)
Tactic: rw [← MorphismProperty.cancel_left_of_respectsIso @IsIntegralHom e.inv,
    ← MorphismProperty.cancel_right_of_respectsIso @IsIntegralHom _ U.2.isoSpec.hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : Type u)
e : (↑(fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ≅
  PreZeroHypercover.X (S := normalization f) (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
    U :=
  IsOpenImmersion.isoOfRangeEq (Opens.ι (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)))
    (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U) ⋯
this : Algebra (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (app f (↑U : Y.Opens)))
⊢ RingHom.IsIntegral (R := (↑(Y.presheaf.obj (Opposite.op (↑U : Y.Opens))) : Type u))
    (CommRingCat.Hom.hom ((normalizationDiagramMap f).app (Opposite.op (↑U : Y.Opens))))
have change : RingHom.IsIntegral.{u, u} (R := (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (A :=
  ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))
  (algebraMap (↑Γ(Y, (↑U : Y.Opens)) : Type u)
    ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))
Tactic: change (algebraMap Γ(Y, U) (integralClosure Γ(Y, U) Γ(X, f ⁻¹ᵁ U))).IsIntegral
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : Type u)
e : (↑(fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ≅
  PreZeroHypercover.X (S := normalization f) (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
    U :=
  IsOpenImmersion.isoOfRangeEq (Opens.ι (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)))
    (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U) ⋯
⊢ IsIntegralHom ((e.inv ≫ fromNormalization f ∣_ (↑U : Y.Opens)) ≫ (IsAffineOpen.isoSpec ⋯).hom)
have this : RingHom.IsIntegral (R := (↑(Y.presheaf.obj (Opposite.op (↑U : Y.Opens))) : Type u))
  (CommRingCat.Hom.hom ((normalizationDiagramMap f).app (Opposite.op (↑U : Y.Opens))))
Tactic: have : (f.normalizationDiagramMap.app (.op U)).hom.IsIntegral := by
    letI := (f.app U).hom.toAlgebra
    change (algebraMap Γ(Y, U) (integralClosure Γ(Y, U) Γ(X, f ⁻¹ᵁ U))).IsIntegral
    exact algebraMap_isIntegral_iff.mpr inferInstance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : Type u)
e : (↑(fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ≅
  PreZeroHypercover.X (S := normalization f) (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
    U :=
  IsOpenImmersion.isoOfRangeEq (Opens.ι (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)))
    (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U) ⋯
this :
  RingHom.IsIntegral (R := (↑(Y.presheaf.obj (Opposite.op (↑U : Y.Opens))) : Type u))
    (CommRingCat.Hom.hom ((normalizationDiagramMap f).app (Opposite.op (↑U : Y.Opens))))
⊢ IsIntegralHom ((e.inv ≫ fromNormalization f ∣_ (↑U : Y.Opens)) ≫ (IsAffineOpen.isoSpec ⋯).hom)
have h : PreZeroHypercover.X (S := normalization f) (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
      U =
    Spec ((normalizationDiagram f).obj (Opposite.op (↑U : Y.Opens))) →
  (e.inv ≫ fromNormalization f ∣_ (↑U : Y.Opens)) ≫ (IsAffineOpen.isoSpec sorry).hom =
    Spec.map ((normalizationDiagramMap f).app (Opposite.op (↑U : Y.Opens)))
Tactic: convert! IsIntegralHom.SpecMap_iff.mpr this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : Type u)
e : (↑(fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ≅
  PreZeroHypercover.X (S := normalization f) (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
    U :=
  IsOpenImmersion.isoOfRangeEq (Opens.ι (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)))
    (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U) ⋯
this :
  RingHom.IsIntegral (R := (↑(Y.presheaf.obj (Opposite.op (↑U : Y.Opens))) : Type u))
    (CommRingCat.Hom.hom ((normalizationDiagramMap f).app (Opposite.op (↑U : Y.Opens))))
e_1 :
  PreZeroHypercover.X (S := normalization f) (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
      U =
    Spec ((normalizationDiagram f).obj (Opposite.op (↑U : Y.Opens)))
⊢ (e.inv ≫ fromNormalization f ∣_ (↑U : Y.Opens)) ≫ (IsAffineOpen.isoSpec ⋯).hom =
    Spec.map ((normalizationDiagramMap f).app (Opposite.op (↑U : Y.Opens)))
have h : ((e.inv ≫ fromNormalization f ∣_ (↑U : Y.Opens)) ≫ (IsAffineOpen.isoSpec sorry).hom) ≫ IsAffineOpen.fromSpec sorry =
  Spec.map ((normalizationDiagramMap f).app (Opposite.op (↑U : Y.Opens))) ≫ IsAffineOpen.fromSpec sorry
Tactic: rw [← cancel_mono U.2.fromSpec]