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
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst_2 : IsIntegralHom f₂
H : f = f₁ ≫ f₂
U :
  (X.openCoverOfIsOpenCover
      (fun (k : (↑Y.affineOpens : Type u)) ↦
        (TopologicalSpace.Opens.comap (TopCat.Hom.hom f.base) :
            (a : TopologicalSpace.Opens ↥Y) → TopologicalSpace.Opens ↥X)
          (↑k : Y.Opens))
      ⋯).I₀
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)))
⊢ (X.openCoverOfIsOpenCover
            (fun (k : (↑Y.affineOpens : Type u)) ↦
              (TopologicalSpace.Opens.comap (TopCat.Hom.hom f.base) :
                  (a : TopologicalSpace.Opens ↥Y) → TopologicalSpace.Opens ↥X)
                (↑k : Y.Opens))
            ⋯).f
        U ≫
      CategoryStruct.comp (Y := normalization f) (toNormalization f) (normalizationDesc f f₁ f₂ H) =
    (X.openCoverOfIsOpenCover
            (fun (k : (↑Y.affineOpens : Type u)) ↦
              (TopologicalSpace.Opens.comap (TopCat.Hom.hom f.base) :
                  (a : TopologicalSpace.Opens ↥Y) → TopologicalSpace.Opens ↥X)
                (↑k : Y.Opens))
            ⋯).f
        U ≫
      f₁
have refine : (f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫
    CategoryStruct.comp (Y :=
      Spec (CommRingCat.of ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))
      (Spec.map
        (CommRingCat.ofHom
          (AlgHom.toRingHom
            (Subalgebra.val
              (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))))
      (CategoryStruct.comp (Y := normalization f)
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U)
        (normalizationDesc f f₁ f₂ H)) =
  (X.openCoverOfIsOpenCover
          (fun (k : (↑Y.affineOpens : Type u)) ↦
            (TopologicalSpace.Opens.comap (TopCat.Hom.hom f.base) :
                (a : TopologicalSpace.Opens ↥Y) → TopologicalSpace.Opens ↥X)
              (↑k : Y.Opens))
          sorry).f
      U ≫
    f₁
Tactic: refine (Scheme.Hom.ι_toNormalization_assoc ..).trans ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst_2 : IsIntegralHom f₂
H : f = f₁ ≫ f₂
U :
  (X.openCoverOfIsOpenCover
      (fun (k : (↑Y.affineOpens : Type u)) ↦
        (TopologicalSpace.Opens.comap (TopCat.Hom.hom f.base) :
            (a : TopologicalSpace.Opens ↥Y) → TopologicalSpace.Opens ↥X)
          (↑k : Y.Opens))
      ⋯).I₀
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)))
⊢ (f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫
      Spec.map
          (CategoryStruct.comp (Y :=
            CommRingCat.of ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))
            (CommRingCat.ofHom
              ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ toOpens U) ⋯)).codRestrict
                (integralClosure (↑Γ(Y, toOpens U) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u)) ⋯))
            (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)))) ≫
        ⋯.fromSpec =
    Opens.ι
        ((TopologicalSpace.Opens.comap (TopCat.Hom.hom f.base) :
            (a : TopologicalSpace.Opens ↥Y) → TopologicalSpace.Opens ↥X)
          (↑U : Y.Opens)) ≫
      f₁
have change : (f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫ Spec.map (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ (↑U : Y.Opens)) sorry) ≫ sorry.fromSpec =
  (f ⁻¹ᵁ (↑U : Y.Opens)).ι ≫ f₁
Tactic: change (f ⁻¹ᵁ U.1).toSpecΓ ≫ Spec.map (f₁.appLE (f₂ ⁻¹ᵁ U.1) (f ⁻¹ᵁ U.1) (by simp [H])) ≫
    (U.2.preimage f₂).fromSpec = (f ⁻¹ᵁ U.1).ι ≫ f₁
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst_2 : IsIntegralHom f₂
H : f = f₁ ≫ f₂
⊢ Eq (α := normalization f ⟶ Y) (normalizationDesc f f₁ f₂ H ≫ f₂) (fromNormalization f)
have refine : ∀ (U : (directedCover Y).I₀),
  colimit.ι (normalizationGlueData f).functor U ≫ normalizationDesc f f₁ f₂ H ≫ f₂ =
    colimit.ι (normalizationGlueData f).functor U ≫ fromNormalization f
Tactic: refine colimit.hom_ext fun U ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst_2 : IsIntegralHom f₂
H : f = f₁ ≫ f₂
U : (directedCover Y).I₀
⊢ colimit.ι (normalizationGlueData f).functor U ≫ normalizationDesc f f₁ f₂ H ≫ f₂ =
    colimit.ι (normalizationGlueData f).functor U ≫ fromNormalization f
have dsimp : CategoryStruct.comp (Y := colimit (normalizationGlueData f).functor) (colimit.ι (normalizationGlueData f).functor U)
    (colimit.desc (normalizationGlueData f).functor
        { pt := T,
          ι :=
            {
              app := fun (U : Y.AffineZariskiSite) ↦
                Spec.map
                    (CommRingCat.ofHom
                      ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ U.toOpens) sorry)).codRestrict
                        (integralClosure (↑Γ(Y, U.toOpens) : Type u) (↑Γ(X, f ⁻¹ᵁ U.toOpens) : Type u)) sorry)) ≫
                  sorry.fromSpec,
              naturality := sorry :
              NatTrans (normalizationGlueData f).functor (Functor.obj (Functor.const Y.AffineZariskiSite) T) } } ≫
      f₂) =
  CategoryStruct.comp (Y := colimit (normalizationGlueData f).functor)
    (colimit.ι (normalizationGlueData f).functor U :
      (normalizationGlueData f).functor.obj U ⟶ colimit (normalizationGlueData f).functor)
    ((normalizationGlueData f).toBase : (normalizationGlueData f).glued ⟶ Y)
Tactic: dsimp [normalizationDesc, fromNormalization]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst_2 : IsIntegralHom f₂
H : f = f₁ ≫ f₂
U : (directedCover Y).I₀
⊢ CategoryStruct.comp (Y := colimit (normalizationGlueData f).functor) (colimit.ι (normalizationGlueData f).functor U)
      (colimit.desc (normalizationGlueData f).functor
          { pt := T,
            ι :=
              {
                app := fun (U : Y.AffineZariskiSite) ↦
                  Spec.map
                      (CommRingCat.ofHom
                        ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ U.toOpens) ⋯)).codRestrict
                          (integralClosure (↑Γ(Y, U.toOpens) : Type u) (↑Γ(X, f ⁻¹ᵁ U.toOpens) : Type u)) ⋯)) ≫
                    ⋯.fromSpec,
                naturality := ⋯ :
                NatTrans (normalizationGlueData f).functor (Functor.obj (Functor.const Y.AffineZariskiSite) T) } } ≫
        f₂) =
    CategoryStruct.comp (Y := colimit (normalizationGlueData f).functor)
      (colimit.ι (normalizationGlueData f).functor U :
        (normalizationGlueData f).functor.obj U ⟶ colimit (normalizationGlueData f).functor)
      ((normalizationGlueData f).toBase : (normalizationGlueData f).glued ⟶ Y)
have rw : Spec.map
      (appLE f₂ (↑U : Y.Opens) (f₂ ⁻¹ᵁ (↑U : Y.Opens)) sorry ≫
        CommRingCat.ofHom
          ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ toOpens U) sorry)).codRestrict
            (integralClosure (↑Γ(Y, toOpens U) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u)) sorry)) ≫
    sorry.fromSpec =
  (normalizationGlueData f).natTrans.app U ≫ (directedCover Y).f U
Tactic: rw [colimit.ι_desc_assoc, (normalizationGlueData f).ι_toBase, Category.assoc,
    ← IsAffineOpen.SpecMap_appLE_fromSpec _ U.2 _ le_rfl, ← 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
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst_2 : IsIntegralHom f₂
H : f = f₁ ≫ f₂
U : (directedCover Y).I₀
⊢ Spec.map
        (appLE f₂ (↑U : Y.Opens) (f₂ ⁻¹ᵁ (↑U : Y.Opens)) ⋯ ≫
          CommRingCat.ofHom
            ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ toOpens U) ⋯)).codRestrict
              (integralClosure (↑Γ(Y, toOpens U) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u)) ⋯)) ≫
      ⋯.fromSpec =
    (normalizationGlueData f).natTrans.app U ≫ (directedCover Y).f U
have dsimp : Spec.map
      (appLE f₂ (↑U : Y.Opens) (f₂ ⁻¹ᵁ (↑U : Y.Opens)) sorry ≫
        CommRingCat.ofHom
          ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ toOpens U) sorry)).codRestrict
            (integralClosure (↑Γ(Y, toOpens U) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u)) sorry)) ≫
    sorry.fromSpec =
  (Spec.map ((normalizationDiagramMap f).app (Opposite.op (toOpens U))) ≫ sorry.isoSpec.inv) ≫ (↑U : Y.Opens).ι
Tactic: dsimp [normalizationGlueData, relativeGluingData, restrictIsoSpec]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst_2 : IsIntegralHom f₂
H : f = f₁ ≫ f₂
U : (directedCover Y).I₀
⊢ Spec.map
        (appLE f₂ (↑U : Y.Opens) (f₂ ⁻¹ᵁ (↑U : Y.Opens)) ⋯ ≫
          CommRingCat.ofHom
            ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ toOpens U) ⋯)).codRestrict
              (integralClosure (↑Γ(Y, toOpens U) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u)) ⋯)) ≫
      ⋯.fromSpec =
    (Spec.map ((normalizationDiagramMap f).app (Opposite.op (toOpens U))) ≫ ⋯.isoSpec.inv) ≫ (↑U : Y.Opens).ι
have rw : Spec.map
      (appLE f₂ (↑U : Y.Opens) (f₂ ⁻¹ᵁ (↑U : Y.Opens)) sorry ≫
        CommRingCat.ofHom
          ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ toOpens U) sorry)).codRestrict
            (integralClosure (↑Γ(Y, toOpens U) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u)) sorry)) ≫
    sorry.fromSpec =
  Spec.map ((normalizationDiagramMap f).app (Opposite.op (toOpens U))) ≫ sorry.isoSpec.inv ≫ (↑U : Y.Opens).ι
Tactic: rw [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
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst_2 : IsIntegralHom f₂
H : f = f₁ ≫ f₂
U : (directedCover Y).I₀
⊢ Spec.map
        (appLE f₂ (↑U : Y.Opens) (f₂ ⁻¹ᵁ (↑U : Y.Opens)) ⋯ ≫
          CommRingCat.ofHom
            ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ toOpens U) ⋯)).codRestrict
              (integralClosure (↑Γ(Y, toOpens U) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u)) ⋯)) ≫
      ⋯.fromSpec =
    Spec.map ((normalizationDiagramMap f).app (Opposite.op (toOpens U))) ≫ ⋯.isoSpec.inv ≫ (↑U : Y.Opens).ι
have e_a : Eq (α :=
  Γ(Y, (↑U : Y.Opens)) ⟶
    CommRingCat.of ↥(integralClosure (↑Γ(Y, toOpens U) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u)))
  (appLE f₂ (↑U : Y.Opens) (f₂ ⁻¹ᵁ (↑U : Y.Opens)) sorry ≫
    CommRingCat.ofHom
      ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ toOpens U) sorry)).codRestrict
        (integralClosure (↑Γ(Y, toOpens U) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u)) sorry))
  ((normalizationDiagramMap f).app (Opposite.op (toOpens U)))
Tactic: congr 2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst_2 : IsIntegralHom f₂
H : f = f₁ ≫ f₂
U : (directedCover Y).I₀
⊢ Eq (α :=
    Γ(Y, (↑U : Y.Opens)) ⟶
      CommRingCat.of ↥(integralClosure (↑Γ(Y, toOpens U) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u)))
    (appLE f₂ (↑U : Y.Opens) (f₂ ⁻¹ᵁ (↑U : Y.Opens)) ⋯ ≫
      CommRingCat.ofHom
        ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ toOpens U) ⋯)).codRestrict
          (integralClosure (↑Γ(Y, toOpens U) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u)) ⋯))
    ((normalizationDiagramMap f).app (Opposite.op (toOpens U)))
have e_a : ∀ (i : (↑Γ(Y, (↑U : Y.Opens)) : Type u)),
  Eq.{u + 1} (α := (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
    (↑((CommRingCat.Hom.hom
              (appLE f₂ (↑U : Y.Opens) (f₂ ⁻¹ᵁ (↑U : Y.Opens)) sorry ≫
                CommRingCat.ofHom
                  ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ toOpens U) sorry)).codRestrict
                    (integralClosure (↑Γ(Y, toOpens U) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u)) sorry)) :
            (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) →
              (↑(CommRingCat.of ↥(integralClosure (↑Γ(Y, toOpens U) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))) :
                Type u))
          i) :
      (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
    (↑((CommRingCat.Hom.hom ((normalizationDiagramMap f).app (Opposite.op (toOpens U))) :
            (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) →
              (↑(CommRingCat.of ↥(integralClosure (↑Γ(Y, toOpens U) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))) :
                Type u))
          i) :
      (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
Tactic: ext i
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst_2 : IsIntegralHom f₂
H : f = f₁ ≫ f₂
U : (directedCover Y).I₀
i : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
⊢ Eq.{u + 1} (α := (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
    (↑((CommRingCat.Hom.hom
              (appLE f₂ (↑U : Y.Opens) (f₂ ⁻¹ᵁ (↑U : Y.Opens)) ⋯ ≫
                CommRingCat.ofHom
                  ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ toOpens U) ⋯)).codRestrict
                    (integralClosure (↑Γ(Y, toOpens U) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u)) ⋯)) :
            (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) →
              (↑(CommRingCat.of ↥(integralClosure (↑Γ(Y, toOpens U) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))) :
                Type u))
          i) :
      (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
    (↑((CommRingCat.Hom.hom ((normalizationDiagramMap f).app (Opposite.op (toOpens U))) :
            (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) →
              (↑(CommRingCat.of ↥(integralClosure (↑Γ(Y, toOpens U) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))) :
                Type u))
          i) :
      (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
have e_a : Eq (α := (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
  ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ toOpens U) sorry) :
        (a : (↑(T.presheaf.1 (Opposite.op (f₂ ⁻¹ᵁ (↑U : Y.Opens)))) : Type u)) → (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
      ((CommRingCat.Hom.hom (appLE f₂ (↑U : Y.Opens) (f₂ ⁻¹ᵁ (↑U : Y.Opens)) sorry) :
            (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑(T.presheaf.1 (Opposite.op (f₂ ⁻¹ᵁ (↑U : Y.Opens)))) : Type u))
          i :
        (↑(T.presheaf.1 (Opposite.op (f₂ ⁻¹ᵁ (↑U : Y.Opens)))) : Type u)) :
    (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
  ((CommRingCat.Hom.hom (app f (toOpens U)) :
        (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
      i :
    (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
Tactic: dsimp [normalizationDiagram, normalizationDiagramMap, RingHom.algebraMap_toAlgebra]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst_2 : IsIntegralHom f₂
H : f = f₁ ≫ f₂
U : (directedCover Y).I₀
i : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
⊢ Eq (α := (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
    ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ toOpens U) ⋯) :
          (a : (↑(T.presheaf.1 (Opposite.op (f₂ ⁻¹ᵁ (↑U : Y.Opens)))) : Type u)) → (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
        ((CommRingCat.Hom.hom (appLE f₂ (↑U : Y.Opens) (f₂ ⁻¹ᵁ (↑U : Y.Opens)) ⋯) :
              (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑(T.presheaf.1 (Opposite.op (f₂ ⁻¹ᵁ (↑U : Y.Opens)))) : Type u))
            i :
          (↑(T.presheaf.1 (Opposite.op (f₂ ⁻¹ᵁ (↑U : Y.Opens)))) : Type u)) :
      (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
    ((CommRingCat.Hom.hom (app f (toOpens U)) :
          (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
        i :
      (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
have e_a : Eq (α := (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (appLE (f₁ ≫ f₂) (↑U : Y.Opens) (f ⁻¹ᵁ toOpens U) sorry) :
        (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
      i :
    (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
  ((CommRingCat.Hom.hom (appLE f (toOpens U) (f ⁻¹ᵁ toOpens U) sorry) :
        (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
      i :
    (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
Tactic: rw [← CommRingCat.comp_apply, Hom.appLE_comp_appLE, app_eq_appLE]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst_2 : IsIntegralHom f₂
H : f = f₁ ≫ f₂
⊢ IsIntegralHom (X := normalization f) (normalizationDesc f f₁ f₂ H ≫ f₂)
have rw : IsIntegralHom (X := normalization f) (fromNormalization f)
Tactic: rw [f.normalizationDesc_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst_2 : IsIntegralHom f₂
H : f = f₁ ≫ f₂
⊢ IsIntegralHom (X := normalization f) (normalizationDesc f f₁ f₂ H)
have this : IsIntegralHom (X := normalization f) (normalizationDesc f f₁ f₂ H ≫ f₂)
Tactic: have : IsIntegralHom (f.normalizationDesc f₁ f₂ H ≫ f₂) := by
    rw [f.normalizationDesc_comp]; infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst_2 : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
⊢ f₁ = f₂
have apply : ∀
  (U :
    PreZeroHypercover.I₀ (S := normalization f)
      (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))),
  PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₁ =
    PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₂
Tactic: apply f.normalizationOpenCover.hom_ext _ _ fun U ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst_2 : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U :
  PreZeroHypercover.I₀ (S := normalization f)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
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)))
⊢ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₁ =
    PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₂
have this₁ : IsAffineHom f₁
Tactic: have : IsAffineHom f₁ := have : IsAffineHom (f₁ ≫ g) := hf₁ ▸ inferInstance; .of_comp _ g
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst_2 : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U :
  PreZeroHypercover.I₀ (S := normalization f)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
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 : IsAffineHom f₁
⊢ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₁ =
    PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₂
have this₁ : IsAffineHom f₂
Tactic: have : IsAffineHom f₂ := have : IsAffineHom (f₂ ≫ g) := hf₂ ▸ inferInstance; .of_comp _ g
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst_2 : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U :
  PreZeroHypercover.I₀ (S := normalization f)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
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 : IsAffineHom f₁
this : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
⊢ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₁ =
    PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₂
have refine_1 : (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₁) ⁻¹ᵁ
    g ⁻¹ᵁ (↑U : Y.Opens) =
  ⊤
Tactic: refine eq_of_SpecMap_comp_eq_of_isAffineOpen
    (CommRingCat.ofHom (integralClosure Γ(Y, U.1) Γ(X, f ⁻¹ᵁ U.1)).val.toRingHom)
    Subtype.val_injective _ (U.2.preimage g) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst_2 : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U :
  PreZeroHypercover.I₀ (S := normalization f)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
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 : IsAffineHom f₁
this : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
refine_1 :
  (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₁) ⁻¹ᵁ
      g ⁻¹ᵁ (↑U : Y.Opens) =
    ⊤
⊢ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₁ =
    PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₂
have refine_2 : (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₂) ⁻¹ᵁ
    g ⁻¹ᵁ (↑U : Y.Opens) =
  ⊤
Tactic: refine eq_of_SpecMap_comp_eq_of_isAffineOpen
    (CommRingCat.ofHom (integralClosure Γ(Y, U.1) Γ(X, f ⁻¹ᵁ U.1)).val.toRingHom)
    Subtype.val_injective _ (U.2.preimage g) ?_ ?_ ?_