awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : QuasiCompact f
inst_2 : QuasiSeparated f
U : Y.AffineZariskiSite
r : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
this_1 : Algebra (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (app f (↑U : Y.Opens)))
this_2 : Algebra (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (app f (↑(U.basicOpen r) : Y.Opens)))
this_3 : Algebra ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
  ↥(integralClosure (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)) :=
  (CommRingCat.Hom.hom ((normalizationDiagram f).map (homOfLE ⋯).op)).toAlgebra
inst : Algebra (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
this_4 : IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u)
this_5 :
  IsLocalization.Away (R := (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    ((algebraMap (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) :
          (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
        r :
      (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)
this_6 : Algebra (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u) :=
  (CommRingCat.Hom.hom (appLE f (↑U : Y.Opens) (f ⁻¹ᵁ Y.basicOpen r) ⋯)).toAlgebra
this :
  IsScalarTower.{u, u, u} (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)
    (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)
⊢ IsLocalization.Away (R := ↥(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)) :
          (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) →
            ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))
        r :
      ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))
    ↥(integralClosure (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u))
have this₁ : IsScalarTower.{u, u, u} (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, Y.basicOpen r) : Type u)
  (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)
Tactic: have : IsScalarTower Γ(Y, U.1) Γ(Y, Y.basicOpen r) Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
    .of_algebraMap_eq' <| by
      simp only [RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp, Scheme.Hom.app_eq_appLE,
        Scheme.Hom.map_appLE, AffineZariskiSite.basicOpen]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : QuasiCompact f
inst_2 : QuasiSeparated f
U : Y.AffineZariskiSite
r : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
this_1 : Algebra (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (app f (↑U : Y.Opens)))
this_2 : Algebra (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (app f (↑(U.basicOpen r) : Y.Opens)))
this_3 : Algebra ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
  ↥(integralClosure (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)) :=
  (CommRingCat.Hom.hom ((normalizationDiagram f).map (homOfLE ⋯).op)).toAlgebra
inst : Algebra (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
this_4 : IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u)
this_5 :
  IsLocalization.Away (R := (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    ((algebraMap (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) :
          (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
        r :
      (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)
this_6 : Algebra (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u) :=
  (CommRingCat.Hom.hom (appLE f (↑U : Y.Opens) (f ⁻¹ᵁ Y.basicOpen r) ⋯)).toAlgebra
this_7 :
  IsScalarTower.{u, u, u} (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)
    (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)
this :
  IsScalarTower.{u, u, u} (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, Y.basicOpen r) : Type u)
    (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)
⊢ IsLocalization.Away (R := ↥(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)) :
          (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) →
            ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))
        r :
      ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))
    ↥(integralClosure (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u))
have this₁ : IsScalarTower.{u, u, u} ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
  ↥(integralClosure (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u))
  (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)
Tactic: have : IsScalarTower (integralClosure Γ(Y, U.1) Γ(X, f ⁻¹ᵁ U.1))
    (integralClosure Γ(Y, Y.basicOpen r) Γ(X, f ⁻¹ᵁ Y.basicOpen r))
    Γ(X, f ⁻¹ᵁ Y.basicOpen r) := .of_algebraMap_eq' rfl
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : QuasiCompact f
inst_2 : QuasiSeparated f
U : Y.AffineZariskiSite
r : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
this_1 : Algebra (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (app f (↑U : Y.Opens)))
this_2 : Algebra (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (app f (↑(U.basicOpen r) : Y.Opens)))
this_3 : Algebra ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
  ↥(integralClosure (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)) :=
  (CommRingCat.Hom.hom ((normalizationDiagram f).map (homOfLE ⋯).op)).toAlgebra
inst : Algebra (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
this_4 : IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u)
this_5 :
  IsLocalization.Away (R := (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    ((algebraMap (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) :
          (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
        r :
      (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)
this_6 : Algebra (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u) :=
  (CommRingCat.Hom.hom (appLE f (↑U : Y.Opens) (f ⁻¹ᵁ Y.basicOpen r) ⋯)).toAlgebra
this_7 :
  IsScalarTower.{u, u, u} (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)
    (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)
this_8 :
  IsScalarTower.{u, u, u} (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, Y.basicOpen r) : Type u)
    (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)
this :
  IsScalarTower.{u, u, u} ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    ↥(integralClosure (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u))
    (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)
⊢ IsLocalization.Away (R := ↥(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)) :
          (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) →
            ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))
        r :
      ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))
    ↥(integralClosure (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u))
have this₁ : IsScalarTower.{u, u, u} (↑Γ(Y, (↑U : Y.Opens)) : Type u)
  ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
  ↥(integralClosure (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u))
Tactic: have : IsScalarTower Γ(Y, U.1) (integralClosure Γ(Y, U.1) Γ(X, f ⁻¹ᵁ U.1))
    (integralClosure Γ(Y, Y.basicOpen r) Γ(X, f ⁻¹ᵁ Y.basicOpen r)) := .of_algebraMap_eq' rfl
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U V : Y.AffineZariskiSite
i : U ⟶ V
⊢ Iso.inv (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫
      Cover.trans (P := IsOpenImmersion) (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)) i ≫
        Iso.hom (pullbackRestrictIsoRestrict f (↑V : Y.Opens)) =
    X.homOfLE ⋯
have rw : (Iso.inv (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫
      Cover.trans (P := IsOpenImmersion) (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)) i ≫
        Iso.hom (pullbackRestrictIsoRestrict f (↑V : Y.Opens))) ≫
    (f ⁻¹ᵁ (↑V : Y.Opens)).ι =
  X.homOfLE sorry ≫ (f ⁻¹ᵁ (↑V : Y.Opens)).ι
Tactic: rw [← cancel_mono (Scheme.Opens.ι _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U V : Y.AffineZariskiSite
i : U ⟶ V
⊢ Eq (α := (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).X U ⟶ normalization f)
    (Cover.trans (P := IsOpenImmersion) (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)) i ≫
      (fun (U : (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).I₀) ↦
          (Iso.hom (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫
              (f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫
                CategoryStruct.comp (Y :=
                  Spec
                    (CommRingCat.of
                      ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))
                  (Spec.map
                    (CommRingCat.ofHom
                      (AlgHom.toRingHom
                        (Subalgebra.val
                          (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))))
                  (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U) :
            (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).X U ⟶ normalization f))
        V)
    ((fun (U : (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).I₀) ↦
        (Iso.hom (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫
            (f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫
              CategoryStruct.comp (Y :=
                Spec
                  (CommRingCat.of
                    ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))
                (Spec.map
                  (CommRingCat.ofHom
                    (AlgHom.toRingHom
                      (Subalgebra.val
                        (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))))
                (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U) :
          (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).X U ⟶ normalization f))
      U)
have this : Iso.inv (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫
    Cover.trans (P := IsOpenImmersion) (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)) i ≫
      Iso.hom (pullbackRestrictIsoRestrict f (↑V : Y.Opens)) =
  X.homOfLE sorry
Tactic: have : (pullbackRestrictIsoRestrict f U.1).inv ≫
      Cover.trans ((directedCover Y).pullback₁ f) i ≫
      (pullbackRestrictIsoRestrict f V.1).hom = X.homOfLE
        (f.preimage_mono (toOpens_mono i.1.1)) := by
    rw [← cancel_mono (Scheme.Opens.ι _)]
    simp +instances [Cover.trans, Cover.locallyDirectedPullbackCover]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U V : Y.AffineZariskiSite
i : U ⟶ V
this :
  Iso.inv (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫
      Cover.trans (P := IsOpenImmersion) (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)) i ≫
        Iso.hom (pullbackRestrictIsoRestrict f (↑V : Y.Opens)) =
    X.homOfLE ⋯
⊢ Eq (α := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ⟶ normalization f)
    ((f ⁻¹ᵁ U.toOpens).toSpecΓ ≫
      Spec.map
          (CommRingCat.ofHom
              (↑(Subalgebra.val
                    (integralClosure (↑Γ(Y, (↑V : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u))) :
                ↥(integralClosure (↑Γ(Y, (↑V : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u)) →+*
                  (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u)) ≫
            X.presheaf.map (homOfLE ⋯).op) ≫
        colimit.ι (normalizationGlueData f).functor V)
    ((f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫
      Spec.map
          (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))) ≫
        colimit.ι (normalizationGlueData f).functor U)
have rw : Eq (α := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ⟶ normalization f)
  ((f ⁻¹ᵁ U.toOpens).toSpecΓ ≫
    Spec.map
        (CommRingCat.ofHom
            (↑(Subalgebra.val
                  (integralClosure (↑Γ(Y, (↑V : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u))) :
              ↥(integralClosure (↑Γ(Y, (↑V : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u)) →+*
                (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u)) ≫
          X.presheaf.map (homOfLE sorry).op) ≫
      colimit.ι (normalizationGlueData f).functor V)
  ((f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫
    Spec.map
        (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))) ≫
      (normalizationGlueData f).functor.map i ≫ colimit.ι (normalizationGlueData f).functor V)
Tactic: rw [← colimit.w f.normalizationGlueData.functor i]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U V : Y.AffineZariskiSite
i : U ⟶ V
this :
  Iso.inv (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫
      Cover.trans (P := IsOpenImmersion) (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)) i ≫
        Iso.hom (pullbackRestrictIsoRestrict f (↑V : Y.Opens)) =
    X.homOfLE ⋯
⊢ Eq (α := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ⟶ normalization f)
    ((f ⁻¹ᵁ U.toOpens).toSpecΓ ≫
      Spec.map
          (CommRingCat.ofHom
              (↑(Subalgebra.val
                    (integralClosure (↑Γ(Y, (↑V : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u))) :
                ↥(integralClosure (↑Γ(Y, (↑V : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u)) →+*
                  (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u)) ≫
            X.presheaf.map (homOfLE ⋯).op) ≫
        colimit.ι (normalizationGlueData f).functor V)
    ((f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫
      Spec.map
          (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))) ≫
        (normalizationGlueData f).functor.map i ≫ colimit.ι (normalizationGlueData f).functor V)
have dsimp : Eq (α := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ⟶ normalization f)
  ((f ⁻¹ᵁ U.toOpens).toSpecΓ ≫
    Spec.map
        (CommRingCat.ofHom
            (↑(Subalgebra.val
                  (integralClosure (↑Γ(Y, (↑V : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u))) :
              ↥(integralClosure (↑Γ(Y, (↑V : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u)) →+*
                (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u)) ≫
          X.presheaf.map (homOfLE sorry).op) ≫
      colimit.ι (((toOpensFunctor Y).op ⋙ normalizationDiagram f).rightOp ⋙ Scheme.Spec) V)
  ((f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫
    Spec.map
        (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))) ≫
      Spec.map ((normalizationDiagram f).map ((toOpensFunctor Y).map i).op) ≫
        colimit.ι (((toOpensFunctor Y).op ⋙ normalizationDiagram f).rightOp ⋙ Scheme.Spec) V)
Tactic: dsimp [normalizationGlueData, relativeGluingData]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U V : Y.AffineZariskiSite
i : U ⟶ V
this :
  Iso.inv (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫
      Cover.trans (P := IsOpenImmersion) (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)) i ≫
        Iso.hom (pullbackRestrictIsoRestrict f (↑V : Y.Opens)) =
    X.homOfLE ⋯
⊢ Eq (α := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ⟶ normalization f)
    ((f ⁻¹ᵁ U.toOpens).toSpecΓ ≫
      Spec.map
          (CommRingCat.ofHom
              (↑(Subalgebra.val
                    (integralClosure (↑Γ(Y, (↑V : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u))) :
                ↥(integralClosure (↑Γ(Y, (↑V : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u)) →+*
                  (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u)) ≫
            X.presheaf.map (homOfLE ⋯).op) ≫
        colimit.ι (((toOpensFunctor Y).op ⋙ normalizationDiagram f).rightOp ⋙ Scheme.Spec) V)
    ((f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫
      Spec.map
          (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))) ≫
        Spec.map ((normalizationDiagram f).map ((toOpensFunctor Y).map i).op) ≫
          colimit.ι (((toOpensFunctor Y).op ⋙ normalizationDiagram f).rightOp ⋙ Scheme.Spec) V)
have rw : Eq (α := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ⟶ normalization f)
  ((f ⁻¹ᵁ U.toOpens).toSpecΓ ≫
    Spec.map
        (CommRingCat.ofHom
            (↑(Subalgebra.val
                  (integralClosure (↑Γ(Y, (↑V : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u))) :
              ↥(integralClosure (↑Γ(Y, (↑V : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u)) →+*
                (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u)) ≫
          X.presheaf.map (homOfLE sorry).op) ≫
      colimit.ι (((toOpensFunctor Y).op ⋙ normalizationDiagram f).rightOp ⋙ Scheme.Spec) V)
  ((f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫
    Spec.map
        ((normalizationDiagram f).map ((toOpensFunctor Y).map i).op ≫
          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))) ≫
      colimit.ι (((toOpensFunctor Y).op ⋙ normalizationDiagram f).rightOp ⋙ Scheme.Spec) V)
Tactic: rw [← Spec.map_comp_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : Type u)
⊢ Eq (α := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ⟶ normalization f) ((f ⁻¹ᵁ (↑U : Y.Opens)).ι ≫ toNormalization 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))))))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U))
have rw : 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: rw [← cancel_epi (pullbackRestrictIsoRestrict f U.1).hom, ← 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.affineOpens : Type 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))
have 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)
Tactic: trans ((directedCover Y).pullback₁ f).f U ≫ f.toNormalization