awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst_2 : IsIntegralHom f₂
H : f = f₁ ≫ f₂
U V : (directedCover Y).I₀
i : U ⟶ V
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) ⋯)).codRestrict
                    (integralClosure (↑Γ(Y, toOpens V) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens V) : Type u)) ⋯) ≫
                (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 ⋯).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_1 :
        (↑((normalizationDiagram f).obj (Opposite.op (toOpens U))) : Type u))
⊢ 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)) ⋯)

Tactic:
ext i
-- Module: Mathlib.AlgebraicGeometry.Normalization
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)
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) ⋯)).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))
⊢ 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))

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.AlgebraicGeometry.Normalization
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)
refine_2 :
  Eq (α := (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
    ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).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) ⋯) :
              (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) ⋯) :
          (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 ⋯).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))
⊢ 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))

Tactic:
dsimp [normalizationDiagram]

Premises used: AlgebraicGeometry.Scheme.Hom.normalizationDiagram
-- Module: Mathlib.AlgebraicGeometry.Normalization
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 (α := (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
    ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).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) ⋯) :
              (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) ⋯) :
          (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 ⋯).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:
simp only [← CommRingCat.comp_apply, appLE_map, map_appLE]

Premises used: CommRingCat.comp_apply, AlgebraicGeometry.Scheme.Hom.map_appLE, AlgebraicGeometry.Scheme.Hom.appLE_map
-- Module: Mathlib.AlgebraicGeometry.Normalization
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₁

Tactic:
Scheme.Cover.hom_ext (X.openCoverOfIsOpenCover _
    (.comap (iSup_affineOpens_eq_top Y) f.base.hom)) _ _ fun U ↦ ?_

Premises used: AlgebraicGeometry.iSup_affineOpens_eq_top, AlgebraicGeometry.Scheme.openCoverOfIsOpenCover, TopologicalSpace.IsOpenCover.comap, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', TopCat.Hom.hom, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.Cover.hom_ext
-- Module: Mathlib.AlgebraicGeometry.Normalization
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 :
  ∀
    (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₀),
    (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₁
⊢ CategoryStruct.comp (Y := normalization f) (toNormalization f) (normalizationDesc f f₁ f₂ H) = f₁

Tactic:
refine Scheme.Cover.hom_ext (X.openCoverOfIsOpenCover _
    (.comap (iSup_affineOpens_eq_top Y) f.base.hom)) _ _ fun U ↦ ?_

Premises used: AlgebraicGeometry.iSup_affineOpens_eq_top, AlgebraicGeometry.Scheme.openCoverOfIsOpenCover, TopologicalSpace.IsOpenCover.comap, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', TopCat.Hom.hom, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.Cover.hom_ext
-- Module: Mathlib.AlgebraicGeometry.Normalization
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₁

Tactic:
(Scheme.Hom.ι_toNormalization_assoc ..).trans ?_

Premises used: Set.Mem, AlgebraicGeometry.Scheme.restrict, AlgebraicGeometry.Scheme.Hom.ι_toNormalization_assoc, AlgebraicGeometry.Scheme.Opens.toScheme, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.Normalization
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)))
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))
            ⋯).f
        U ≫
      f₁
⊢ (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₁

Tactic:
refine (Scheme.Hom.ι_toNormalization_assoc ..).trans ?_

Premises used: AlgebraicGeometry.Scheme.Hom.ι_toNormalization_assoc, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.Normalization
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) ≤ f₁ ⁻¹ᵁ f₂ ⁻¹ᵁ (↑U : Y.Opens)

Tactic:
simp [H]
-- Module: Mathlib.AlgebraicGeometry.Normalization
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)))
change :
  (f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫ Spec.map (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ (↑U : Y.Opens)) ⋯) ≫ ⋯.fromSpec =
    (f ⁻¹ᵁ (↑U : Y.Opens)).ι ≫ f₁
⊢ (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₁

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₁

Premises used: AlgebraicGeometry.Spec.map, AlgebraicGeometry.IsAffineOpen.fromSpec, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.Scheme.Hom.appLE, AlgebraicGeometry.Scheme.Opens.toSpecΓ, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.Opens.ι, TopologicalSpace.Opens.map, Subtype.val, CategoryTheory.Functor.obj, Subtype.property, AlgebraicGeometry.IsAffineOpen.preimage
-- Module: Mathlib.AlgebraicGeometry.Normalization
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 (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ (↑U : Y.Opens)) ⋯) ≫ ⋯.fromSpec =
    (f ⁻¹ᵁ (↑U : Y.Opens)).ι ≫ f₁

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Normalization
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)

Tactic:
colimit.hom_ext fun U ↦ ?_

Premises used: AlgebraicGeometry.Scheme.Hom.normalization, CategoryTheory.Limits.colimit.hom_ext
-- Module: Mathlib.AlgebraicGeometry.Normalization
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 :
  ∀ (U : (directedCover Y).I₀),
    colimit.ι (normalizationGlueData f).functor U ≫ normalizationDesc f f₁ f₂ H ≫ f₂ =
      colimit.ι (normalizationGlueData f).functor U ≫ fromNormalization f
⊢ Eq (α := normalization f ⟶ Y) (normalizationDesc f f₁ f₂ H ≫ f₂) (fromNormalization f)

Tactic:
refine colimit.hom_ext fun U ↦ ?_

Premises used: CategoryTheory.Limits.colimit.hom_ext
-- Module: Mathlib.AlgebraicGeometry.Normalization
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₀
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) ⋯)).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)
⊢ colimit.ι (normalizationGlueData f).functor U ≫ normalizationDesc f f₁ f₂ H ≫ f₂ =
    colimit.ι (normalizationGlueData f).functor U ≫ fromNormalization f

Tactic:
dsimp [normalizationDesc, fromNormalization]

Premises used: AlgebraicGeometry.Scheme.Hom.fromNormalization, AlgebraicGeometry.Scheme.Hom.normalizationDesc