awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Normalization
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)
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))
⊢ 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))

Tactic:
trans ((directedCover Y).pullback₁ f).f U ≫ f.toNormalization

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.Hom.toNormalization, AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover, CategoryTheory.Precoverage.ZeroHypercover.pullback₁, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : Type u)
e_a :
  Iso.hom (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫ (f ⁻¹ᵁ (↑U : Y.Opens)).ι =
    (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).f 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)

Tactic:
congr 1
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : Type u)
⊢ Iso.hom (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫ (f ⁻¹ᵁ (↑U : Y.Opens)).ι =
    (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).f U

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : Type u)
⊢ HasPullback f (↑U : Y.Opens).ι

Tactic:
generalize_proofs _ _ _ _ H
-- Module: Mathlib.AlgebraicGeometry.Normalization
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).ι
⊢ (precoverage IsOpenImmersion).IsStableUnderBaseChange

Tactic:
generalize_proofs _ _ _ _ H
-- Module: Mathlib.AlgebraicGeometry.Normalization
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
⊢ ∀ (i : (directedCover Y).I₀), HasPullback f ((directedCover Y).f i)

Tactic:
generalize_proofs _ _ _ _ H
-- Module: Mathlib.AlgebraicGeometry.Normalization
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)
⊢ ∀ (U : (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).I₀), HasPullback f (↑U : Y.Opens).ι

Tactic:
generalize_proofs _ _ _ _ H
-- Module: Mathlib.AlgebraicGeometry.Normalization
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)
pf₃ : ∀ (U : (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).I₀), HasPullback f (↑U : Y.Opens).ι
⊢ ∀ {i j : (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).I₀} (hij : i ⟶ j),
    Eq (α := (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).X i ⟶ normalization f)
      (Cover.trans (P := IsOpenImmersion) (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)) hij ≫
        Iso.hom (pullbackRestrictIsoRestrict f (↑j : Y.Opens)) ≫
          (f ⁻¹ᵁ (↑j : Y.Opens)).toSpecΓ ≫
            CategoryStruct.comp (Y :=
              Spec
                (CommRingCat.of
                  ↥(integralClosure (↑Γ(Y, (↑j : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑j : Y.Opens)) : Type u))))
              (Spec.map
                (CommRingCat.ofHom
                  (AlgHom.toRingHom
                    (Subalgebra.val
                      (integralClosure (↑Γ(Y, (↑j : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑j : Y.Opens)) : Type u))))))
              (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) j))
      (Iso.hom (pullbackRestrictIsoRestrict f (↑i : Y.Opens)) ≫
        (f ⁻¹ᵁ (↑i : Y.Opens)).toSpecΓ ≫
          CategoryStruct.comp (Y :=
            Spec
              (CommRingCat.of
                ↥(integralClosure (↑Γ(Y, (↑i : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑i : Y.Opens)) : Type u))))
            (Spec.map
              (CommRingCat.ofHom
                (AlgHom.toRingHom
                  (Subalgebra.val
                    (integralClosure (↑Γ(Y, (↑i : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑i : Y.Opens)) : Type u))))))
            (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) i))

Tactic:
generalize_proofs _ _ _ _ H
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : Type u)
⊢ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫
      fromNormalization f =
    Spec.map ((normalizationDiagramMap f).app (Opposite.op (↑U : Y.Opens))) ≫ IsAffineOpen.fromSpec ⋯

Tactic:
colimit.ι_desc _ _

Premises used: CategoryTheory.NatTrans.vcomp, AlgebraicGeometry.Spec, AlgebraicGeometry.Spec.topObj, Set.Mem, setOf, ContinuousMap.comp, AlgebraicGeometry.Spec.topMap, AlgebraicGeometry.StructureSheaf.comap, AlgebraicGeometry.Spec.locallyRingedSpaceMap, CategoryTheory.Limits.colimit.ι_desc, Set.preimage, AlgebraicGeometry.PresheafedSpace.comp, AlgebraicGeometry.LocallyRingedSpace.comp, PrimeSpectrum.comap
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : Type u)
⊢ Eq (α := (normalization f).Opens) (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens))
    (opensRange (X :=
      PreZeroHypercover.X (S := normalization f)
        (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U))

Tactic:
simpa using f.normalizationGlueData.toBase_preimage_eq_opensRange_ι U

Premises used: AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase_preimage_eq_opensRange_ι, AlgebraicGeometry.Scheme.Hom.normalizationGlueData
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
⊢ CategoryStruct.comp (Y := normalization f) (toNormalization f) (fromNormalization f) = f

Tactic:
Scheme.Cover.hom_ext (X.openCoverOfIsOpenCover _
    (.comap (iSup_affineOpens_eq_top Y) f.base.1)) _ _ fun U ↦ ?_

Premises used: AlgebraicGeometry.iSup_affineOpens_eq_top, AlgebraicGeometry.Scheme.openCoverOfIsOpenCover, TopologicalSpace.IsOpenCover.comap, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', TopCat.Hom.hom', AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.Cover.hom_ext
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
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))
          ⋯).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
⊢ CategoryStruct.comp (Y := normalization f) (toNormalization f) (fromNormalization f) = f

Tactic:
refine Scheme.Cover.hom_ext (X.openCoverOfIsOpenCover _
    (.comap (iSup_affineOpens_eq_top Y) f.base.1)) _ _ fun U ↦ ?_

Premises used: AlgebraicGeometry.iSup_affineOpens_eq_top, AlgebraicGeometry.Scheme.openCoverOfIsOpenCover, TopologicalSpace.IsOpenCover.comap, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', TopCat.Hom.hom', AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.Cover.hom_ext
-- Module: Mathlib.AlgebraicGeometry.Normalization
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

Tactic:
(f.ι_toNormalization_assoc _ _).trans ?_

Premises used: Set.Mem, AlgebraicGeometry.Scheme.restrict, AlgebraicGeometry.Scheme.Hom.ι_toNormalization_assoc, AlgebraicGeometry.Scheme.Opens.toScheme, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.Normalization
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₀
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))
            ⋯).f
        U ≫
      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 ≫
      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

Tactic:
refine (f.ι_toNormalization_assoc _ _).trans ?_

Premises used: AlgebraicGeometry.Scheme.Hom.ι_toNormalization_assoc, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.Normalization
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₀
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 ⋯ =
    (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
⊢ (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

Tactic:
rw [f.ι_fromNormalization, ← Spec.map_comp_assoc]

Premises used: AlgebraicGeometry.Spec.map_comp_assoc, AlgebraicGeometry.Scheme.Hom.ι_fromNormalization
-- Module: Mathlib.AlgebraicGeometry.Normalization
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₀
change :
  (f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫ Spec.map (app f (↑U : Y.Opens)) ≫ IsAffineOpen.fromSpec ⋯ =
    (f ⁻¹ᵁ (↑U : Y.Opens)).ι ≫ f
⊢ (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

Tactic:
change (f ⁻¹ᵁ U.1).toSpecΓ ≫ Spec.map (f.app _) ≫ U.2.fromSpec = (f ⁻¹ᵁ U.1).ι ≫ _

Premises used: AlgebraicGeometry.Spec.map, AlgebraicGeometry.IsAffineOpen.fromSpec, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.Scheme.Hom.app, AlgebraicGeometry.Scheme.Opens.toSpecΓ, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.Opens.ι, TopologicalSpace.Opens.map, Subtype.val, CategoryTheory.Functor.obj, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Normalization
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 (app f (↑U : Y.Opens)) ≫ IsAffineOpen.fromSpec ⋯ =
    (f ⁻¹ᵁ (↑U : Y.Opens)).ι ≫ f

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
rw :
  ∀ (i : (↑Y.affineOpens : Type u)),
    IsIntegralHom (X := (↑(fromNormalization f ⁻¹ᵁ (↑i : Y.Opens)) : Scheme)) (fromNormalization f ∣_ (↑i : Y.Opens))
⊢ IsIntegralHom (X := normalization f) (fromNormalization f)

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := @IsIntegralHom) _
    (iSup_affineOpens_eq_top _)]

Premises used: AlgebraicGeometry.iSup_affineOpens_eq_top, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_iSup_eq_top
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : Type u)
⊢ Eq (α := Set ↥(normalization f))
    (Set.range (ι := ↥(↑(fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme))
      ⇑(Opens.ι (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens))))
    (Set.range (ι :=
      ↥(PreZeroHypercover.X (S := normalization f)
          (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U))
      ⇑(PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U))

Tactic:
simpa using congr($(f.fromNormalization_preimage U).1)
-- Module: Mathlib.AlgebraicGeometry.Normalization
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) ⋯
rw : IsIntegralHom ((e.inv ≫ fromNormalization f ∣_ (↑U : Y.Opens)) ≫ (IsAffineOpen.isoSpec ⋯).hom)
⊢ IsIntegralHom (X := (↑(fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (fromNormalization f ∣_ (↑U : Y.Opens))

Tactic:
rw [← MorphismProperty.cancel_left_of_respectsIso @IsIntegralHom e.inv,
    ← MorphismProperty.cancel_right_of_respectsIso @IsIntegralHom _ U.2.isoSpec.hom]

Premises used: AlgebraicGeometry.IsIntegralHom, AlgebraicGeometry.IsAffineOpen.isoSpec, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Normalization
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)))
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)))
⊢ 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:
change (algebraMap Γ(Y, U) (integralClosure Γ(Y, U) Γ(X, f ⁻¹ᵁ U))).IsIntegral

Premises used: CommRingCat.carrier, Algebra.algebraMap, Membership.mem, Subtype, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, integralClosure, Opposite.op, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.PresheafedSpace.Hom.base, RingHom.IsIntegral, TopologicalSpace.Opens.map, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Subtype.val, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Normalization
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.{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:
algebraMap_isIntegral_iff.mpr inferInstance

Premises used: Iff.mpr, algebraMap_isIntegral_iff, inferInstance
-- Module: Mathlib.AlgebraicGeometry.Normalization
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.{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:
exact algebraMap_isIntegral_iff.mpr inferInstance

Premises used: Iff.mpr, algebraMap_isIntegral_iff, inferInstance