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.Opens
hU : IsAffineOpen U
this_1 : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u) := (CommRingCat.Hom.hom (app f U)).toAlgebra
this :
  IsIso (X := Γ(normalization f, fromNormalization f ⁻¹ᵁ U)) (Y :=
    Γ((normalizationOpenCover f).X ⟨U, hU⟩,
      PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
          (Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) U hU) ⁻¹ᵁ
        fromNormalization f ⁻¹ᵁ U))
    (app
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
        (Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) U hU))
      (fromNormalization f ⁻¹ᵁ U))
⊢ ⊤ =
    (Spec.map
          ((normalizationDiagramMap f).app
            (Opposite.op (↑(Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) U hU) : Y.Opens))) ≫
        IsAffineOpen.fromSpec ⋯) ⁻¹ᵁ
      U

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : Y.Opens
hU : IsAffineOpen U
this_1 : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u) := (CommRingCat.Hom.hom (app f U)).toAlgebra
this :
  IsIso (X := Γ(normalization f, fromNormalization f ⁻¹ᵁ U)) (Y :=
    Γ((normalizationOpenCover f).X ⟨U, hU⟩,
      PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
          (Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) U hU) ⁻¹ᵁ
        fromNormalization f ⁻¹ᵁ U))
    (app
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
        (Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) U hU))
      (fromNormalization f ⁻¹ᵁ U))
⊢ Eq (α :=
    (PreZeroHypercover.X (S := normalization f)
        (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
        (Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) U hU)).Opens)
    ⊤
    ((PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
          (Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) U hU) ≫
        fromNormalization f) ⁻¹ᵁ
      U)

Tactic:
have H : ⊤ = ((normalizationOpenCover f).f ⟨U, hU⟩ ≫ fromNormalization f) ⁻¹ᵁ U := by
    rw [f.ι_fromNormalization]; simp
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : Y.Opens
hU : IsAffineOpen U
this_1 : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u) := (CommRingCat.Hom.hom (app f U)).toAlgebra
this :
  IsIso (X := Γ(normalization f, fromNormalization f ⁻¹ᵁ U)) (Y :=
    Γ((normalizationOpenCover f).X ⟨U, hU⟩,
      PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
          (Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) U hU) ⁻¹ᵁ
        fromNormalization f ⁻¹ᵁ U))
    (app
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
        (Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) U hU))
      (fromNormalization f ⁻¹ᵁ U))
H :
  Eq (α :=
    (PreZeroHypercover.X (S := normalization f)
        (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
        (Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) U hU)).Opens)
    ⊤
    ((PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
          (Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) U hU) ≫
        fromNormalization f) ⁻¹ᵁ
      U)
simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp [Scheme.Hom.appLE, ← ΓSpecIso_inv_naturality]

Premises used: AlgebraicGeometry.Scheme.Hom.appLE, AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : Y.Opens
hU : IsAffineOpen U
this_1 : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u) := (CommRingCat.Hom.hom (app f U)).toAlgebra
this :
  IsIso (X := Γ(normalization f, fromNormalization f ⁻¹ᵁ U)) (Y :=
    Γ((normalizationOpenCover f).X ⟨U, hU⟩,
      PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
          (Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) U hU) ⁻¹ᵁ
        fromNormalization f ⁻¹ᵁ U))
    (app
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
        (Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) U hU))
      (fromNormalization f ⁻¹ᵁ U))
H :
  Eq (α :=
    (PreZeroHypercover.X (S := normalization f)
        (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
        (Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) U hU)).Opens)
    ⊤
    ((PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
          (Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) U hU) ≫
        fromNormalization f) ⁻¹ᵁ
      U)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : Y.Opens
hU : IsAffineOpen U
this : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u) := (CommRingCat.Hom.hom (app f U)).toAlgebra
⊢ f ⁻¹ᵁ U ≤ toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ U

Tactic:
simp [← Scheme.Hom.comp_preimage]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_preimage
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : Y.Opens
hU : IsAffineOpen U
rw :
  Eq (α := Γ(normalization f, fromNormalization f ⁻¹ᵁ U) ⟶ CommRingCat.of (↑Γ(X, f ⁻¹ᵁ U) : Type u))
    (Iso.hom (normalizationObjIso f hU) ≫
      CommRingCat.ofHom
        (AlgHom.toRingHom (Subalgebra.val (integralClosure (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u)))))
    (Iso.hom (normalizationObjIso f ⋯) ≫
      CategoryStruct.comp (Y := Γ(X, toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ U))
        (CommRingCat.ofHom
            (↑(Subalgebra.val
                  (integralClosure
                    (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)) : Type u)
                    (↑Γ(X, f ⁻¹ᵁ (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)) :
                      Type u))) :
              ↥(integralClosure (↑Γ(Y, (↑⟨U, hU⟩ : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑⟨U, hU⟩ : Y.Opens)) : Type u)) →+*
                (↑Γ(X, f ⁻¹ᵁ (↑⟨U, hU⟩ : Y.Opens)) : Type u)) ≫
          X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
        (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))))
⊢ Eq (α := Γ(normalization f, fromNormalization f ⁻¹ᵁ U) ⟶ CommRingCat.of (↑Γ(X, f ⁻¹ᵁ U) : Type u))
    (Iso.hom (normalizationObjIso f hU) ≫
      CommRingCat.ofHom
        (AlgHom.toRingHom (Subalgebra.val (integralClosure (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u)))))
    (appLE (toNormalization f) (fromNormalization f ⁻¹ᵁ U) (f ⁻¹ᵁ U) ⋯)

Tactic:
rw [appLE, f.toNormalization_app_preimage ⟨U, hU⟩, Category.assoc]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Hom.toNormalization_app_preimage, AlgebraicGeometry.Scheme.Hom.appLE, Subtype.mk
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : Y.Opens
hU : IsAffineOpen U
simp :
  Eq (α :=
    CommRingCat.of ↥(integralClosure (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u)) ⟶
      CommRingCat.of (↑Γ(X, f ⁻¹ᵁ U) : Type u))
    (CommRingCat.ofHom
      (↑(Subalgebra.val (integralClosure (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u))) :
        ↥(integralClosure (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u)) →+* (↑Γ(X, f ⁻¹ᵁ U) : Type u)))
    (CommRingCat.ofHom
        (↑(Subalgebra.val (integralClosure (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u))) :
          ↥(integralClosure (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u)) →+* (↑Γ(X, f ⁻¹ᵁ U) : Type u)) ≫
      𝟙 Γ(X, f ⁻¹ᵁ U))
⊢ Eq (α := Γ(normalization f, fromNormalization f ⁻¹ᵁ U) ⟶ CommRingCat.of (↑Γ(X, f ⁻¹ᵁ U) : Type u))
    (Iso.hom (normalizationObjIso f hU) ≫
      CommRingCat.ofHom
        (AlgHom.toRingHom (Subalgebra.val (integralClosure (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u)))))
    (Iso.hom (normalizationObjIso f ⋯) ≫
      CategoryStruct.comp (Y := Γ(X, toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ U))
        (CommRingCat.ofHom
            (↑(Subalgebra.val
                  (integralClosure
                    (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)) : Type u)
                    (↑Γ(X, f ⁻¹ᵁ (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)) :
                      Type u))) :
              ↥(integralClosure (↑Γ(Y, (↑⟨U, hU⟩ : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑⟨U, hU⟩ : Y.Opens)) : Type u)) →+*
                (↑Γ(X, f ⁻¹ᵁ (↑⟨U, hU⟩ : Y.Opens)) : Type u)) ≫
          X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
        (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))))

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : Y.Opens
hU : IsAffineOpen U
⊢ Eq (α :=
    CommRingCat.of ↥(integralClosure (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u)) ⟶
      CommRingCat.of (↑Γ(X, f ⁻¹ᵁ U) : Type u))
    (CommRingCat.ofHom
      (↑(Subalgebra.val (integralClosure (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u))) :
        ↥(integralClosure (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u)) →+* (↑Γ(X, f ⁻¹ᵁ U) : Type u)))
    (CommRingCat.ofHom
        (↑(Subalgebra.val (integralClosure (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u))) :
          ↥(integralClosure (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u)) →+* (↑Γ(X, f ⁻¹ᵁ U) : Type u)) ≫
      𝟙 Γ(X, f ⁻¹ᵁ U))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
inst_2 : IsIntegralHom f
⊢ IsIso (Y := normalization f) (toNormalization f)

Tactic:
(IsZariskiLocalAtTarget.iff_of_openCover (P := .isomorphisms _)
    f.normalizationOpenCover).mpr fun U ↦ ?_

Premises used: Iff.mpr, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.Scheme.Hom.normalizationOpenCover
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
inst_2 : IsIntegralHom f
refine :
  ∀ (U : (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)).1),
    MorphismProperty.isomorphisms Scheme (X :=
      (Precoverage.ZeroHypercover.pullback₁ (T := normalization f) (toNormalization f) (normalizationOpenCover f)).X U)
      (Cover.pullbackHom (P := IsOpenImmersion) (normalizationOpenCover f) (toNormalization f) U :
        (Precoverage.ZeroHypercover.pullback₁ (T := normalization f) (toNormalization f) (normalizationOpenCover f)).X
            U ⟶
          PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U)
⊢ IsIso (Y := normalization f) (toNormalization f)

Tactic:
refine (IsZariskiLocalAtTarget.iff_of_openCover (P := .isomorphisms _)
    f.normalizationOpenCover).mpr fun U ↦ ?_

Premises used: Iff.mpr, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.Scheme.Hom.normalizationOpenCover
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
inst_2 : IsIntegralHom f
U : (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)).1
⊢ Eq (α := Set ↥X)
    (Set.range (ι :=
      ↥(pullback (Y :=
          PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U)
          (toNormalization f)
          (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U)))
      ⇑(pullback.fst (toNormalization f)
          (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U)))
    (Set.range (ι := ↥(↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) ⇑(f ⁻¹ᵁ (↑U : Y.Opens)).ι)

Tactic:
simp [← Hom.coe_opensRange,
      Hom.opensRange_pullbackFst, ← f.fromNormalization_preimage, ← Scheme.Hom.comp_preimage]

Premises used: AlgebraicGeometry.Scheme.Hom.fromNormalization_preimage, AlgebraicGeometry.Scheme.Hom.opensRange_pullbackFst, AlgebraicGeometry.Scheme.Hom.comp_preimage, AlgebraicGeometry.Scheme.Hom.coe_opensRange
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
inst_2 : IsIntegralHom f
U : (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)).1
e : pullback (Y := PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U)
    (toNormalization f)
    (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U) ≅
  (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) :=
  IsOpenImmersion.isoOfRangeEq
    (pullback.fst (toNormalization f)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U))
    (f ⁻¹ᵁ (↑U : Y.Opens)).ι ⋯
rw :
  MorphismProperty.isomorphisms Scheme
    ((e ≪≫ ⋯.isoSpec).inv ≫ Cover.pullbackHom (P := IsOpenImmersion) (normalizationOpenCover f) (toNormalization f) U)
⊢ MorphismProperty.isomorphisms Scheme (X :=
    (Precoverage.ZeroHypercover.pullback₁ (T := normalization f) (toNormalization f) (normalizationOpenCover f)).X U)
    (Cover.pullbackHom (P := IsOpenImmersion) (normalizationOpenCover f) (toNormalization f) U :
      (Precoverage.ZeroHypercover.pullback₁ (T := normalization f) (toNormalization f) (normalizationOpenCover f)).X U ⟶
        PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U)

Tactic:
rw [← MorphismProperty.cancel_left_of_respectsIso (.isomorphisms _)
    (e ≪≫ (U.2.preimage f).isoSpec).inv]

Premises used: AlgebraicGeometry.IsAffineOpen.isoSpec, CategoryTheory.MorphismProperty.isomorphisms, CategoryTheory.Iso.trans, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Iso.inv, Subtype.property, AlgebraicGeometry.IsAffineOpen.preimage
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
inst_2 : IsIntegralHom f
U : (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)).1
e : pullback (Y := PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U)
    (toNormalization f)
    (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U) ≅
  (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) :=
  IsOpenImmersion.isoOfRangeEq
    (pullback.fst (toNormalization f)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U))
    (f ⁻¹ᵁ (↑U : Y.Opens)).ι ⋯
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)))
h :
  Spec Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) = Spec (CommRingCat.of (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) →
    PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U =
        Spec
          (CommRingCat.of ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))) →
      (e ≪≫ ⋯.isoSpec).inv ≫ Cover.pullbackHom (P := IsOpenImmersion) (normalizationOpenCover f) (toNormalization f) U =
        Spec.map
          (CommRingCat.ofHom
            (AlgHom.toRingHom
              (Subalgebra.val
                (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))))
convert_to :
  IsIso.{u, u + 1} (X := Spec (CommRingCat.of (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))) (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))))))
⊢ MorphismProperty.isomorphisms Scheme
    ((e ≪≫ ⋯.isoSpec).inv ≫ Cover.pullbackHom (P := IsOpenImmersion) (normalizationOpenCover f) (toNormalization f) U)

Tactic:
convert_to IsIso (Spec.map (CommRingCat.ofHom
      (integralClosure Γ(Y, U.1) Γ(X, f ⁻¹ᵁ U.1)).val.toRingHom))

Premises used: CategoryTheory.IsIso, CommRingCat.carrier, Subalgebra.val, CommRingCat.ofHom, AlgebraicGeometry.Spec.map, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgHom.toRingHom, integralClosure, Opposite.op, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.PresheafedSpace.Hom.base, 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
inst_2 : IsIntegralHom f
U : (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)).1
e : pullback (Y := PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U)
    (toNormalization f)
    (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U) ≅
  (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) :=
  IsOpenImmersion.isoOfRangeEq
    (pullback.fst (toNormalization f)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U))
    (f ⁻¹ᵁ (↑U : Y.Opens)).ι ⋯
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)))
e_3 : Spec Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) = Spec (CommRingCat.of (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
e_4 :
  PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U =
    Spec (CommRingCat.of ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))
h :
  ⋯.isoSpec.hom ≫
      ((e ≪≫ ⋯.isoSpec).inv ≫
          Cover.pullbackHom (P := IsOpenImmersion) (normalizationOpenCover f) (toNormalization f) U) ≫
        PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U =
    ⋯.isoSpec.hom ≫
      CategoryStruct.comp (Y :=
        PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) 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)
⊢ (e ≪≫ ⋯.isoSpec).inv ≫ Cover.pullbackHom (P := IsOpenImmersion) (normalizationOpenCover f) (toNormalization f) U =
    Spec.map
      (CommRingCat.ofHom
        (AlgHom.toRingHom
          (Subalgebra.val (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))))

Tactic:
rw [← cancel_mono (f.normalizationOpenCover.f U), ← cancel_epi (U.2.preimage f).isoSpec.hom]

Premises used: AlgebraicGeometry.IsAffineOpen.isoSpec, CategoryTheory.PreZeroHypercover.f, CategoryTheory.cancel_mono, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, AlgebraicGeometry.Scheme.Hom.normalizationOpenCover, Subtype.property, AlgebraicGeometry.IsAffineOpen.preimage
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
inst_2 : IsIntegralHom f
U : (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)).1
e : pullback (Y := PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U)
    (toNormalization f)
    (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U) ≅
  (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) :=
  IsOpenImmersion.isoOfRangeEq
    (pullback.fst (toNormalization f)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U))
    (f ⁻¹ᵁ (↑U : Y.Opens)).ι ⋯
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)))
e_3 : Spec Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) = Spec (CommRingCat.of (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
e_4 :
  PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U =
    Spec (CommRingCat.of ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))
⊢ ⋯.isoSpec.hom ≫
      ((e ≪≫ ⋯.isoSpec).inv ≫
          Cover.pullbackHom (P := IsOpenImmersion) (normalizationOpenCover f) (toNormalization f) U) ≫
        PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U =
    ⋯.isoSpec.hom ≫
      CategoryStruct.comp (Y :=
        PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) 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:
simp [e, -Iso.cancel_iso_hom_left, IsAffineOpen.isoSpec_hom,
      Hom.ι_toNormalization]

Premises used: AlgebraicGeometry.Scheme.Hom.ι_toNormalization, CategoryTheory.Iso.cancel_iso_hom_left, AlgebraicGeometry.IsAffineOpen.isoSpec_hom
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
inst_2 : IsIntegralHom f
U : (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)).1
e : pullback (Y := PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U)
    (toNormalization f)
    (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U) ≅
  (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) :=
  IsOpenImmersion.isoOfRangeEq
    (pullback.fst (toNormalization f)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U))
    (f ⁻¹ᵁ (↑U : Y.Opens)).ι ⋯
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)))
rw : RingHom.IsIntegral (R := (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (CommRingCat.Hom.hom (app f (↑U : Y.Opens)))
⊢ Eq.{u + 1} (α := Subalgebra (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) ⊤

Tactic:
rw [integralClosure_eq_top_iff, ← algebraMap_isIntegral_iff, RingHom.algebraMap_toAlgebra]

Premises used: integralClosure_eq_top_iff, algebraMap_isIntegral_iff, RingHom.algebraMap_toAlgebra