awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
inst_2 : IsReduced X
i :
  PreZeroHypercover.I₀ (S := normalization f)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
⊢ IsReduced.{u} (PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) i)
have this : _root_.IsReduced.{u} (↑((normalizationDiagram f).obj (Opposite.op (↑i : Y.Opens))) : Type u)
Tactic: have : _root_.IsReduced ((normalizationDiagram f).obj (.op i.1)) :=
      let := (f.app i.1).hom.toAlgebra
      isReduced_of_injective (Subalgebra.val _) Subtype.val_injective
-- 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 : IsReduced X
i :
  PreZeroHypercover.I₀ (S := normalization f)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
this : _root_.IsReduced.{u} (↑((normalizationDiagram f).obj (Opposite.op (↑i : Y.Opens))) : Type u)
⊢ IsReduced.{u} (PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) i)
have dsimp : IsReduced.{u} (Spec ((normalizationDiagram f).obj (Opposite.op (toOpens i))))
Tactic: dsimp [normalizationOpenCover, 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
inst_2 : IsIntegral X
⊢ IrreducibleSpace.{u} ↥(normalization f)
have rw : IsIrreducible.{u} (X := ↥(normalization f)) ⊤
Tactic: rw [irreducibleSpace_def]
-- 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 : IsIntegral X
⊢ IsIrreducible.{u} (X := ↥(normalization f)) ⊤
have h : Eq (α := Set ↥(normalization f)) ⊤ (closure (Set.image (α := ↥X) (⇑(toNormalization f)) Set.univ))
Tactic: convert!
      ((IrreducibleSpace.isIrreducible_univ X).image _
          f.toNormalization.continuous.continuousOn).closure
-- 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₂
⊢ normalization f ⟶ T
have refine_1 : ∀ (U : (directedCover Y).I₀) (x : (↑Γ(T, f₂ ⁻¹ᵁ (↑U : Y.Opens)) : Type u)),
  Membership.mem (α := (↑Γ(X, f ⁻¹ᵁ Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op U))) : Type u)) (γ :=
    Subalgebra (↑Γ(Y, Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op U))) : Type u)
      (↑Γ(X, f ⁻¹ᵁ Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op U))) : Type u))
    (integralClosure (↑Γ(Y, Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op U))) : Type u)
      (↑Γ(X, f ⁻¹ᵁ Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op U))) : Type u))
    ((CommRingCat.Hom.hom
            (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op U))) sorry) :
          (a : (↑Γ(T, f₂ ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) →
            (↑Γ(X, f ⁻¹ᵁ Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op U))) : Type u))
        x :
      (↑Γ(X, f ⁻¹ᵁ Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op U))) : Type u))
Tactic: refine colimit.desc _
    { pt := _
      ι.app U := Spec.map (CommRingCat.ofHom ((f₁.appLE _ _ (by simp [H])).hom.codRestrict _
        fun x ↦ ?_)) ≫ (U.2.preimage f₂).fromSpec,
      ι.naturality := ?_ }
-- 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₂
refine_1 :
  ∀ (U : (directedCover Y).I₀) (x : (↑Γ(T, f₂ ⁻¹ᵁ (↑U : Y.Opens)) : Type u)),
    Membership.mem (α := (↑Γ(X, f ⁻¹ᵁ Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op U))) : Type u)) (γ :=
      Subalgebra (↑Γ(Y, Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op U))) : Type u)
        (↑Γ(X, f ⁻¹ᵁ Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op U))) : Type u))
      (integralClosure (↑Γ(Y, Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op U))) : Type u)
        (↑Γ(X, f ⁻¹ᵁ Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op U))) : Type u))
      ((CommRingCat.Hom.hom
              (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op U))) ⋯) :
            (a : (↑Γ(T, f₂ ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) →
              (↑Γ(X, f ⁻¹ᵁ Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op U))) : Type u))
          x :
        (↑Γ(X, f ⁻¹ᵁ Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op U))) : Type u))
⊢ normalization f ⟶ T
have refine_2 : ∀ ⦃X_1 Y_1 : (directedCover Y).I₀⦄ (f_1 : X_1 ⟶ Y_1),
  (normalizationGlueData f).functor.map f_1 ≫
      Spec.map
          (CommRingCat.ofHom
            ((CommRingCat.Hom.hom
                  (appLE f₁ (f₂ ⁻¹ᵁ (↑Y_1 : Y.Opens))
                    (f ⁻¹ᵁ Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op Y_1))) sorry)).codRestrict
              (integralClosure (↑Γ(Y, Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op Y_1))) : Type u)
                (↑Γ(X, f ⁻¹ᵁ Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op Y_1))) : Type u))
              sorry)) ≫
        sorry.fromSpec =
    (Spec.map
          (CommRingCat.ofHom
            ((CommRingCat.Hom.hom
                  (appLE f₁ (f₂ ⁻¹ᵁ (↑X_1 : Y.Opens))
                    (f ⁻¹ᵁ Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op X_1))) sorry)).codRestrict
              (integralClosure (↑Γ(Y, Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op X_1))) : Type u)
                (↑Γ(X, f ⁻¹ᵁ Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op X_1))) : Type u))
              sorry)) ≫
        sorry.fromSpec) ≫
      CategoryTheory.Functor.map (Functor.obj (Functor.const (directedCover Y).I₀) T) f_1
Tactic: refine colimit.desc _
    { pt := _
      ι.app U := Spec.map (CommRingCat.ofHom ((f₁.appLE _ _ (by simp [H])).hom.codRestrict _
        fun x ↦ ?_)) ≫ (U.2.preimage f₂).fromSpec,
      ι.naturality := ?_ }
-- 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₂
U : (directedCover Y).I₀
x : (↑Γ(T, f₂ ⁻¹ᵁ (↑U : Y.Opens)) : Type u)
algInst : Algebra (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (app f (↑U : Y.Opens)))
algInst_1 : Algebra (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(T, f₂ ⁻¹ᵁ (↑U : Y.Opens)) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (app f₂ (↑U : Y.Opens)))
algInst_2 : Algebra (↑Γ(T, f₂ ⁻¹ᵁ (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) :=
  (CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ (↑U : Y.Opens)) ⋯)).toAlgebra
⊢ Membership.mem (α := (↑Γ(X, f ⁻¹ᵁ Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op U))) : Type u)) (γ :=
    Subalgebra (↑Γ(Y, Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op U))) : Type u)
      (↑Γ(X, f ⁻¹ᵁ Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op U))) : Type u))
    (integralClosure (↑Γ(Y, Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op U))) : Type u)
      (↑Γ(X, f ⁻¹ᵁ Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op U))) : Type u))
    ((CommRingCat.Hom.hom
            (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op U))) ⋯) :
          (a : (↑Γ(T, f₂ ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) →
            (↑Γ(X, f ⁻¹ᵁ Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op U))) : Type u))
        x :
      (↑Γ(X, f ⁻¹ᵁ Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op U))) : Type u))
have this : IsScalarTower.{u, u, u} (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(T, f₂ ⁻¹ᵁ (↑U : Y.Opens)) : Type u)
  (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)
Tactic: have : IsScalarTower Γ(Y, U.1) Γ(T, f₂ ⁻¹ᵁ U.1) Γ(X, f ⁻¹ᵁ U.1) := .of_algebraMap_eq' <| by
      simp only [RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp,
        Hom.app_eq_appLE, Hom.appLE_comp_appLE, ← H]
-- 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 V : (directedCover Y).I₀
i : U ⟶ V
⊢ (normalizationGlueData f).functor.map i ≫
      Spec.map
          (CommRingCat.ofHom
            ((CommRingCat.Hom.hom
                  (appLE f₁ (f₂ ⁻¹ᵁ (↑V : Y.Opens)) (f ⁻¹ᵁ Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op V)))
                    ⋯)).codRestrict
              (integralClosure (↑Γ(Y, Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op V))) : Type u)
                (↑Γ(X, f ⁻¹ᵁ Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op V))) : Type u))
              ⋯)) ≫
        ⋯.fromSpec =
    (Spec.map
          (CommRingCat.ofHom
            ((CommRingCat.Hom.hom
                  (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op U)))
                    ⋯)).codRestrict
              (integralClosure (↑Γ(Y, Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op U))) : Type u)
                (↑Γ(X, f ⁻¹ᵁ Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op U))) : Type u))
              ⋯)) ≫
        ⋯.fromSpec) ≫
      CategoryTheory.Functor.map (Functor.obj (Functor.const (directedCover Y).I₀) T) i
have refine_2 : Spec.map ((normalizationDiagram f).map ((toOpensFunctor Y).map i).op) ≫
    Spec.map
        (CommRingCat.ofHom
          ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑V : Y.Opens)) (f ⁻¹ᵁ toOpens V) sorry)).codRestrict
            (integralClosure (↑Γ(Y, toOpens V) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens V) : Type u)) sorry)) ≫
      sorry.fromSpec =
  (Spec.map
        (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) ≫
    𝟙 T
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
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst_2 : IsIntegralHom f₂
H : f = f₁ ≫ f₂
U V : (directedCover Y).I₀
i : U ⟶ V
⊢ Spec.map ((normalizationDiagram f).map ((toOpensFunctor Y).map i).op) ≫
      Spec.map
          (CommRingCat.ofHom
            ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑V : Y.Opens)) (f ⁻¹ᵁ toOpens V) ⋯)).codRestrict
              (integralClosure (↑Γ(Y, toOpens V) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens V) : Type u)) ⋯)) ≫
        ⋯.fromSpec =
    (Spec.map
          (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) ≫
      𝟙 T
have refine_2 : Spec.map
      (CommRingCat.ofHom
          ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑V : Y.Opens)) (f ⁻¹ᵁ toOpens V) sorry)).codRestrict
            (integralClosure (↑Γ(Y, toOpens V) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens V) : Type u)) sorry) ≫
        (normalizationDiagram f).map ((toOpensFunctor Y).map i).op) ≫
    sorry.fromSpec =
  Spec.map
      (T.presheaf.map (homOfLE sorry).op ≫
        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
Tactic: rw [Category.comp_id, ← Spec.map_comp_assoc, ← (V.2.preimage f₂).map_fromSpec (U.2.preimage f₂)
      (homOfLE (f₂.preimage_mono (Scheme.AffineZariskiSite.toOpens_mono i.le))).op,
      ← 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 V : (directedCover Y).I₀
i : U ⟶ V
⊢ Spec.map
        (CommRingCat.ofHom
            ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑V : Y.Opens)) (f ⁻¹ᵁ toOpens V) ⋯)).codRestrict
              (integralClosure (↑Γ(Y, toOpens V) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens V) : Type u)) ⋯) ≫
          (normalizationDiagram f).map ((toOpensFunctor Y).map i).op) ≫
      ⋯.fromSpec =
    Spec.map
        (T.presheaf.map (homOfLE ⋯).op ≫
          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
have refine_2 : CommRingCat.ofHom
      ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑V : Y.Opens)) (f ⁻¹ᵁ toOpens V) sorry)).codRestrict
        (integralClosure (↑Γ(Y, toOpens V) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens V) : Type u)) sorry) ≫
    (normalizationDiagram f).map ((toOpensFunctor Y).map i).op =
  T.presheaf.map (homOfLE sorry).op ≫
    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)
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 V : (directedCover Y).I₀
i : U ⟶ V
⊢ CommRingCat.ofHom
        ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑V : Y.Opens)) (f ⁻¹ᵁ toOpens V) ⋯)).codRestrict
          (integralClosure (↑Γ(Y, toOpens V) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens V) : Type u)) ⋯) ≫
      (normalizationDiagram f).map ((toOpensFunctor Y).map i).op =
    T.presheaf.map (homOfLE ⋯).op ≫
      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)) ⋯)
have refine_2 : ∀ (i_1 : (↑(CommRingCat.of (↑(T.presheaf.1 (Opposite.op (f₂ ⁻¹ᵁ (↑V : Y.Opens)))) : Type u)) : Type u)),
  Eq (α := (↑((normalizationDiagram f).obj (Opposite.op (toOpens U))) : Type u))
    ((CommRingCat.Hom.hom
            (CommRingCat.ofHom
                ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑V : Y.Opens)) (f ⁻¹ᵁ toOpens V) sorry)).codRestrict
                  (integralClosure (↑Γ(Y, toOpens V) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens V) : Type u)) sorry) ≫
              (normalizationDiagram f).map ((toOpensFunctor Y).map i).op) :
          (a : (↑(CommRingCat.of (↑(T.presheaf.1 (Opposite.op (f₂ ⁻¹ᵁ (↑V : Y.Opens)))) : Type u)) : Type u)) →
            (↑((normalizationDiagram f).obj (Opposite.op (toOpens U))) : Type u))
        i_1 :
      (↑((normalizationDiagram f).obj (Opposite.op (toOpens U))) : Type u))
    ((CommRingCat.Hom.hom
            (T.presheaf.map (homOfLE sorry).op ≫
              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 : (↑(CommRingCat.of (↑(T.presheaf.1 (Opposite.op (f₂ ⁻¹ᵁ (↑V : Y.Opens)))) : Type u)) : Type u)) →
            (↑((normalizationDiagram f).obj (Opposite.op (toOpens U))) : Type u))
        i_1 :
      (↑((normalizationDiagram f).obj (Opposite.op (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 V : (directedCover Y).I₀
i_1 : U ⟶ V
i : (↑(CommRingCat.of (↑(T.presheaf.1 (Opposite.op (f₂ ⁻¹ᵁ (↑V : Y.Opens)))) : Type u)) : Type u)
⊢ Eq (α := (↑((normalizationDiagram f).obj (Opposite.op (toOpens U))) : Type u))
    ((CommRingCat.Hom.hom
            (CommRingCat.ofHom
                ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑V : Y.Opens)) (f ⁻¹ᵁ toOpens V) ⋯)).codRestrict
                  (integralClosure (↑Γ(Y, toOpens V) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens V) : Type u)) ⋯) ≫
              (normalizationDiagram f).map ((toOpensFunctor Y).map i_1).op) :
          (a : (↑(CommRingCat.of (↑(T.presheaf.1 (Opposite.op (f₂ ⁻¹ᵁ (↑V : Y.Opens)))) : Type u)) : Type u)) →
            (↑((normalizationDiagram f).obj (Opposite.op (toOpens U))) : Type u))
        i :
      (↑((normalizationDiagram f).obj (Opposite.op (toOpens U))) : Type u))
    ((CommRingCat.Hom.hom
            (T.presheaf.map (homOfLE ⋯).op ≫
              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 : (↑(CommRingCat.of (↑(T.presheaf.1 (Opposite.op (f₂ ⁻¹ᵁ (↑V : Y.Opens)))) : Type u)) : Type u)) →
            (↑((normalizationDiagram f).obj (Opposite.op (toOpens U))) : Type u))
        i :
      (↑((normalizationDiagram f).obj (Opposite.op (toOpens U))) : Type u))
have refine_2 : Eq.{u + 1} (α := (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op (toOpens U))) : Type u))
  (↑((CommRingCat.Hom.hom
            (CommRingCat.ofHom
                ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑V : Y.Opens)) (f ⁻¹ᵁ toOpens V) sorry)).codRestrict
                  (integralClosure (↑Γ(Y, toOpens V) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens V) : Type u)) sorry) ≫
              (normalizationDiagram f).map ((toOpensFunctor Y).map i_1).op) :
          (a : (↑(CommRingCat.of (↑(T.presheaf.1 (Opposite.op (f₂ ⁻¹ᵁ (↑V : Y.Opens)))) : Type u)) : Type u)) →
            (↑((normalizationDiagram f).obj (Opposite.op (toOpens U))) : Type u))
        i) :
    (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op (toOpens U))) : Type u))
  (↑((CommRingCat.Hom.hom
            (T.presheaf.map (homOfLE sorry).op ≫
              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 : (↑(CommRingCat.of (↑(T.presheaf.1 (Opposite.op (f₂ ⁻¹ᵁ (↑V : Y.Opens)))) : Type u)) : Type u)) →
            (↑((normalizationDiagram f).obj (Opposite.op (toOpens U))) : Type u))
        i) :
    (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op (toOpens U))) : Type u))
Tactic: apply Subtype.ext
-- 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 V : (directedCover Y).I₀
i_1 : U ⟶ V
i : (↑(CommRingCat.of (↑(T.presheaf.1 (Opposite.op (f₂ ⁻¹ᵁ (↑V : Y.Opens)))) : Type u)) : Type u)
⊢ Eq.{u + 1} (α := (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op (toOpens U))) : Type u))
    (↑((CommRingCat.Hom.hom
              (CommRingCat.ofHom
                  ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑V : Y.Opens)) (f ⁻¹ᵁ toOpens V) ⋯)).codRestrict
                    (integralClosure (↑Γ(Y, toOpens V) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens V) : Type u)) ⋯) ≫
                (normalizationDiagram f).map ((toOpensFunctor Y).map i_1).op) :
            (a : (↑(CommRingCat.of (↑(T.presheaf.1 (Opposite.op (f₂ ⁻¹ᵁ (↑V : Y.Opens)))) : Type u)) : Type u)) →
              (↑((normalizationDiagram f).obj (Opposite.op (toOpens U))) : Type u))
          i) :
      (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op (toOpens U))) : Type u))
    (↑((CommRingCat.Hom.hom
              (T.presheaf.map (homOfLE ⋯).op ≫
                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 : (↑(CommRingCat.of (↑(T.presheaf.1 (Opposite.op (f₂ ⁻¹ᵁ (↑V : Y.Opens)))) : Type u)) : Type u)) →
              (↑((normalizationDiagram f).obj (Opposite.op (toOpens U))) : Type u))
          i) :
      (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op (toOpens U))) : Type u))
have refine_2 : Eq (α := (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
  ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE sorry).op) :
        (a : (↑Γ(X, f ⁻¹ᵁ toOpens V) : Type u)) → (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
      ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑V : Y.Opens)) (f ⁻¹ᵁ toOpens V) sorry) :
            (a : (↑(T.presheaf.1 (Opposite.op (f₂ ⁻¹ᵁ (↑V : Y.Opens)))) : Type u)) → (↑Γ(X, f ⁻¹ᵁ toOpens V) : Type u))
          i :
        (↑Γ(X, f ⁻¹ᵁ toOpens V) : Type u)) :
    (↑Γ(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 (T.presheaf.map (homOfLE sorry).op) :
            (a : (↑(T.presheaf.1 (Opposite.op (f₂ ⁻¹ᵁ (↑V : 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))
Tactic: dsimp [normalizationDiagram]
-- 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₂
⊢ CategoryStruct.comp (Y := normalization f) (toNormalization f) (normalizationDesc f f₁ f₂ H) = f₁
have refine : ∀
  (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))
        sorry).I₀),
  (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 ≫
      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))
            sorry).f
        U ≫
      f₁
Tactic: refine Scheme.Cover.hom_ext (X.openCoverOfIsOpenCover _
    (.comap (iSup_affineOpens_eq_top Y) f.base.hom)) _ _ fun U ↦ ?_