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)
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) ⋯
⊢ 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
-- 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 :
  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 (X := Spec ((normalizationDiagram f).obj (Opposite.op (↑U : Y.Opens))))
    (Spec.map ((normalizationDiagramMap f).app (Opposite.op (↑U : Y.Opens))))

Tactic:
IsIntegralHom.SpecMap_iff.mpr this

Premises used: Iff.mpr, AlgebraicGeometry.IsIntegralHom.SpecMap_iff
-- 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 :
  RingHom.IsIntegral (R := (↑(Y.presheaf.obj (Opposite.op (↑U : Y.Opens))) : Type u))
    (CommRingCat.Hom.hom ((normalizationDiagramMap f).app (Opposite.op (↑U : Y.Opens))))
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 ⋯).hom =
      Spec.map ((normalizationDiagramMap f).app (Opposite.op (↑U : Y.Opens)))
⊢ IsIntegralHom ((e.inv ≫ fromNormalization f ∣_ (↑U : Y.Opens)) ≫ (IsAffineOpen.isoSpec ⋯).hom)

Tactic:
convert! IsIntegralHom.SpecMap_iff.mpr this

Premises used: Iff.mpr, AlgebraicGeometry.IsIntegralHom.SpecMap_iff
-- 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 :
  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)))
h :
  ((e.inv ≫ fromNormalization f ∣_ (↑U : Y.Opens)) ≫ (IsAffineOpen.isoSpec ⋯).hom) ≫ IsAffineOpen.fromSpec ⋯ =
    Spec.map ((normalizationDiagramMap f).app (Opposite.op (↑U : Y.Opens))) ≫ IsAffineOpen.fromSpec ⋯
⊢ (e.inv ≫ fromNormalization f ∣_ (↑U : Y.Opens)) ≫ (IsAffineOpen.isoSpec ⋯).hom =
    Spec.map ((normalizationDiagramMap f).app (Opposite.op (↑U : Y.Opens)))

Tactic:
rw [← cancel_mono U.2.fromSpec]

Premises used: AlgebraicGeometry.IsAffineOpen.fromSpec, CategoryTheory.cancel_mono, 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 :
  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) ≫ IsAffineOpen.fromSpec ⋯ =
    Spec.map ((normalizationDiagramMap f).app (Opposite.op (↑U : Y.Opens))) ≫ IsAffineOpen.fromSpec ⋯

Tactic:
simp [IsAffineOpen.isoSpec_hom, e, ι_fromNormalization]

Premises used: AlgebraicGeometry.Scheme.Hom.ι_fromNormalization, AlgebraicGeometry.IsAffineOpen.isoSpec_hom
-- 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 (α := (normalization f).Opens)
    (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
        (Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) U hU) ''ᵁ
      ⊤)
    (fromNormalization f ⁻¹ᵁ U)

Tactic:
simpa using (f.fromNormalization_preimage ⟨U, hU⟩).symm

Premises used: AlgebraicGeometry.Scheme.Hom.fromNormalization_preimage, Subtype.mk, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : Type 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)))
⊢ toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) = f ⁻¹ᵁ (↑U : Y.Opens)

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.affineOpens : Type 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)))
dsimp :
  app (toNormalization f) (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) =
    CategoryStruct.comp (Y :=
      CommRingCat.of ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))
      ((normalization f).presheaf.map (Quiver.Hom.op (eqToHom ⋯)) ≫
        Iso.hom
            (appIso
              (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
                (Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) (↑U : Y.Opens) ⋯))
              ⊤) ≫
          Iso.hom
            (ΓSpecIso
              ((normalizationDiagram f).obj
                (Opposite.op (toOpens (Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) (↑U : Y.Opens) ⋯))))))
      (CommRingCat.ofHom
          (↑(Subalgebra.val (integralClosure (↑Γ(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)) →+*
              (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) ≫
        X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
⊢ let 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)));
  Eq (α :=
    Γ(normalization f, fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) ⟶
      Γ(X, toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)))
    (app (toNormalization f) (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)))
    (Iso.hom (normalizationObjIso f ⋯) ≫
      CommRingCat.ofHom
          (↑(Subalgebra.val (integralClosure (↑Γ(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)) →+*
              (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) ≫
        X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))

Tactic:
dsimp [normalizationObjIso]

Premises used: AlgebraicGeometry.Scheme.Hom.normalizationObjIso
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : Type 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)))
⊢ Eq (α := TopologicalSpace.Opens ↥(normalization f))
    (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ''ᵁ ⊤)
    (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens))

Tactic:
simp [fromNormalization_preimage]

Premises used: AlgebraicGeometry.Scheme.Hom.fromNormalization_preimage
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : Type 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)))
⊢ toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) =
    (f ⁻¹ᵁ (↑U : Y.Opens)).ι ''ᵁ
      ((f ⁻¹ᵁ (↑U : Y.Opens)).ι ≫ toNormalization f) ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)

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.affineOpens : Type 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)))
⊢ toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) =
    (f ⁻¹ᵁ (↑U : Y.Opens)).ι ''ᵁ
      ((f ⁻¹ᵁ (↑U : Y.Opens)).ι ≫ toNormalization f) ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)

Tactic:
have H : f.toNormalization ⁻¹ᵁ f.fromNormalization ⁻¹ᵁ U =
      (f ⁻¹ᵁ U).ι ''ᵁ (((f ⁻¹ᵁ U).ι ≫ f.toNormalization) ⁻¹ᵁ f.fromNormalization ⁻¹ᵁ U) := by
    simp [← Scheme.Hom.comp_preimage]
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : Type 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)))
H :
  toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) =
    (f ⁻¹ᵁ (↑U : Y.Opens)).ι ''ᵁ
      ((f ⁻¹ᵁ (↑U : Y.Opens)).ι ≫ toNormalization f) ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)
⊢ app ((f ⁻¹ᵁ (↑U : Y.Opens)).ι ≫ toNormalization f) (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) ≫
      X.presheaf.map (Quiver.Hom.op (eqToHom H)) =
    (app
          ((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))
          (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) ≫
        (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme).presheaf.map (Quiver.Hom.op (eqToHom ⋯))) ≫
      X.presheaf.map (Quiver.Hom.op (eqToHom H))

Tactic:
congr($(Scheme.Hom.congr_app (f.ι_toNormalization U) (f.fromNormalization ⁻¹ᵁ U)) ≫
    X.presheaf.map (eqToHom H).op)

Premises used: AlgebraicGeometry.Scheme.Hom.fromNormalization, congrArg, Quiver.Hom.op, CategoryTheory.eqToHom, AlgebraicGeometry.Scheme.Hom.ι_toNormalization, AlgebraicGeometry.Scheme.Hom.congr_app, id, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.Functor.map, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, CategoryTheory.CategoryStruct.comp, 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
U : (↑Y.affineOpens : Type 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)))
H :
  toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) =
    (f ⁻¹ᵁ (↑U : Y.Opens)).ι ''ᵁ
      ((f ⁻¹ᵁ (↑U : Y.Opens)).ι ≫ toNormalization f) ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)
⊢ app (toNormalization f) (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) =
    app ((f ⁻¹ᵁ (↑U : Y.Opens)).ι ≫ toNormalization f) (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) ≫
      X.presheaf.map (Quiver.Hom.op (eqToHom H))

Tactic:
simp [Hom.app_eq_appLE]

Premises used: AlgebraicGeometry.Scheme.Hom.app_eq_appLE
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : Type 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)))
H :
  toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) =
    (f ⁻¹ᵁ (↑U : Y.Opens)).ι ''ᵁ
      ((f ⁻¹ᵁ (↑U : Y.Opens)).ι ≫ toNormalization f) ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (normalization f).presheaf.map (Quiver.Hom.op (eqToHom ⋯)) ≫
      Iso.hom
          (appIso (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U)
            ⊤) ≫
        Iso.hom (ΓSpecIso (Opposite.unop (((toOpensFunctor Y).op ⋙ normalizationDiagram f).rightOp.obj U))) ≫
          CategoryStruct.comp (Y := CommRingCat.of (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
            (CommRingCat.ofHom
              (AlgHom.toRingHom
                (Subalgebra.val
                  (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))))
            (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) =
    (app
          ((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))
          (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) ≫
        (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme).presheaf.map (Quiver.Hom.op (eqToHom ⋯))) ≫
      X.presheaf.map (Quiver.Hom.op (eqToHom H))

Tactic:
dsimp
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : Type 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)))
H :
  toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) =
    (f ⁻¹ᵁ (↑U : Y.Opens)).ι ''ᵁ
      ((f ⁻¹ᵁ (↑U : Y.Opens)).ι ≫ toNormalization f) ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)
h : 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 only [eqToHom_op, Hom.appIso_hom, Category.assoc, Scheme.Hom.naturality_assoc, eqToHom_unop,
    ← Functor.map_comp_assoc, eqToHom_map (TopologicalSpace.Opens.map _), eqToHom_trans]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.eqToHom_map, AlgebraicGeometry.Scheme.Hom.naturality_assoc, CategoryTheory.eqToHom_op, CategoryTheory.Functor.map_comp_assoc, AlgebraicGeometry.Scheme.Hom.appIso_hom, TopologicalSpace.Opens.map, CategoryTheory.eqToHom_unop, CategoryTheory.eqToHom_trans
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : Type 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)))
H :
  toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) =
    (f ⁻¹ᵁ (↑U : Y.Opens)).ι ''ᵁ
      ((f ⁻¹ᵁ (↑U : Y.Opens)).ι ≫ toNormalization f) ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)
h : 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:
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)
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 :
  toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) =
    (f ⁻¹ᵁ (↑U : Y.Opens)).ι ''ᵁ
      ((f ⁻¹ᵁ (↑U : Y.Opens)).ι ≫ toNormalization f) ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)
h : 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:
rw [← IsIso.eq_inv_comp, ← Functor.map_inv, inv_eqToHom]

Premises used: CategoryTheory.IsIso.eq_inv_comp, CategoryTheory.Functor.map_inv, CategoryTheory.inv_eqToHom
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : Type 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)))
H :
  toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) =
    (f ⁻¹ᵁ (↑U : Y.Opens)).ι ''ᵁ
      ((f ⁻¹ᵁ (↑U : Y.Opens)).ι ≫ toNormalization f) ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)
h : 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 [← Functor.map_comp, Scheme.Opens.toSpecΓ_appTop,
    ΓSpecIso_naturality_assoc (CommRingCat.ofHom _)]

Premises used: CommRingCat.ofHom, AlgebraicGeometry.Scheme.Opens.toSpecΓ_appTop, CategoryTheory.Functor.map_comp, AlgebraicGeometry.Scheme.ΓSpecIso_naturality_assoc
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : Type 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)))
H :
  toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) =
    (f ⁻¹ᵁ (↑U : Y.Opens)).ι ''ᵁ
      ((f ⁻¹ᵁ (↑U : Y.Opens)).ι ≫ toNormalization f) ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)
⊢ 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
⊢ LE.le (α := (normalization f).Opens) (fromNormalization f ⁻¹ᵁ U)
    (opensRange (X :=
      PreZeroHypercover.X (S := normalization f)
        (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
        (Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) U hU))
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
        (Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) U hU)))

Tactic:
simp [← fromNormalization_preimage]

Premises used: AlgebraicGeometry.Scheme.Hom.fromNormalization_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
this : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u) := (CommRingCat.Hom.hom (app f U)).toAlgebra
⊢ 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))

Tactic:
have : IsIso (((normalizationOpenCover f).f ⟨U, hU⟩).app (f.fromNormalization ⁻¹ᵁ U)) :=
    Scheme.Hom.isIso_app _ _ (by simp [← fromNormalization_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
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))
rw :
  ⊤ =
    (Spec.map
          ((normalizationDiagramMap f).app
            (Opposite.op (↑(Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) U hU) : Y.Opens))) ≫
        IsAffineOpen.fromSpec ⋯) ⁻¹ᵁ
      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:
rw [f.ι_fromNormalization]

Premises used: AlgebraicGeometry.Scheme.Hom.ι_fromNormalization