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)
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)))
⊢ 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 ⋯)))
have 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 sorry)) ≫
      Iso.hom
          (appIso
            (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
              (Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) (↑U : Y.Opens) sorry))
            ⊤) ≫
        Iso.hom
          (ΓSpecIso
            ((normalizationDiagram f).obj
              (Opposite.op (toOpens (Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) (↑U : Y.Opens) sorry))))))
    (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 sorry)))
Tactic: dsimp [normalizationObjIso]
-- 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)
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)))
⊢ 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 ⋯)))
have change : Eq (α :=
  (normalization f).presheaf.obj (Opposite.op (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens))) ⟶
    Γ(X, toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)))
  (app (toNormalization f) (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)))
  ((normalization f).presheaf.map (Quiver.Hom.op (eqToHom sorry)) ≫
    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 sorry))))
Tactic: change _ = f.normalization.presheaf.map (eqToHom (by simp [fromNormalization_preimage])).op ≫
      ((f.normalizationOpenCover.f U).appIso _).hom ≫
      (Scheme.ΓSpecIso _).hom ≫
      CommRingCat.ofHom (integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val.toRingHom ≫
      X.presheaf.map (eqToHom (by simp [← Scheme.Hom.comp_preimage])).op
-- 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)
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).presheaf.obj (Opposite.op (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens))) ⟶
      Γ(X, toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)))
    (app (toNormalization f) (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)))
    ((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 ⋯))))
have H : 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]
-- 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)
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)
⊢ Eq (α :=
    (normalization f).presheaf.obj (Opposite.op (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens))) ⟶
      Γ(X, toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)))
    (app (toNormalization f) (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)))
    ((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 ⋯))))
have h : 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: convert! congr($(Scheme.Hom.congr_app (f.ι_toNormalization U) (f.fromNormalization ⁻¹ᵁ U)) ≫
    X.presheaf.map (eqToHom H).op) using 1
-- 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)
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)
⊢ (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))
have h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: dsimp
-- 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)
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)
have h : 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]
-- 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)
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)
have h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: congr 1
-- 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)
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)
have h : 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]
-- 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)
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)
have h : 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 _)]
-- 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.Opens
hU : IsAffineOpen U
this : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u) := (CommRingCat.Hom.hom (app f U)).toAlgebra
⊢ Eq (α := Γ(Y, U) ⟶ Γ(normalization f, fromNormalization f ⁻¹ᵁ U)) (app (fromNormalization f) U)
    (CommRingCat.ofHom
        (algebraMap (↑(Y.presheaf.1 (Opposite.op U)) : Type u)
          ↥(integralClosure (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u))) ≫
      Iso.inv (normalizationObjIso f hU))
have 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))
Tactic: have : IsIso (((normalizationOpenCover f).f ⟨U, hU⟩).app (f.fromNormalization ⁻¹ᵁ U)) :=
    Scheme.Hom.isIso_app _ _ (by simp [← fromNormalization_preimage])
-- 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.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)
have rw : ⊤ =
  (Spec.map
        ((normalizationDiagramMap f).app
          (Opposite.op (↑(Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) U hU) : Y.Opens))) ≫
      IsAffineOpen.fromSpec sorry) ⁻¹ᵁ
    U
Tactic: rw [f.ι_fromNormalization]
-- 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.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 (α := Γ(Y, U) ⟶ Γ(normalization f, fromNormalization f ⁻¹ᵁ U)) (app (fromNormalization f) U)
    (CommRingCat.ofHom
        (algebraMap (↑(Y.presheaf.1 (Opposite.op U)) : Type u)
          ↥(integralClosure (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u))) ≫
      Iso.inv (normalizationObjIso f hU))
have 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)
Tactic: have H : ⊤ = ((normalizationOpenCover f).f ⟨U, hU⟩ ≫ fromNormalization f) ⁻¹ᵁ U := by
    rw [f.ι_fromNormalization]; simp
-- 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.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)
have simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: simp [Scheme.Hom.appLE, ← ΓSpecIso_inv_naturality]
-- 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.Opens
hU : IsAffineOpen 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)))))
    (appLE (toNormalization f) (fromNormalization f ⁻¹ᵁ U) (f ⁻¹ᵁ U) ⋯)
have 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 sorry) ≫
    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 sorry)))
      (X.presheaf.map (Quiver.Hom.op (homOfLE sorry))))
Tactic: rw [appLE, f.toNormalization_app_preimage ⟨U, hU⟩, Category.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 : Y.Opens
hU : IsAffineOpen 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 ⋯))))
have 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))
Tactic: simp [← Functor.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
inst_2 : IsIntegralHom f
⊢ IsIso (Y := normalization f) (toNormalization f)
have 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)
Tactic: refine (IsZariskiLocalAtTarget.iff_of_openCover (P := .isomorphisms _)
    f.normalizationOpenCover).mpr fun U ↦ ?_