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
U : (↑Y.affineOpens : Type u)
⊢ Function.Injective (α :=
    (↑(CommRingCat.of ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))) :
      Type u))
    (β := (↑(CommRingCat.of (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X :=
          CommRingCat.of ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))
          (Y := CommRingCat.of (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : 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)))) :
      (a :
          (↑(CommRingCat.of
                ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))) :
            Type u)) →
        (↑(CommRingCat.of (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) : Type u))

Tactic:
exact Subtype.val_injective

Premises used: Subtype.val_injective
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
⊢ (↑(IdealSheafData.support (ker (toNormalization f))) : Set ↥(normalization f)) =
    (↑(IdealSheafData.support ⊥) : Set ↥(normalization f))

Tactic:
have := congr(($(f.ker_toNormalization).support : Set f.normalization))
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
this :
  (↑(IdealSheafData.support (ker (toNormalization f))) : Set ↥(normalization f)) =
    (↑(IdealSheafData.support ⊥) : Set ↥(normalization f))
⊢ Eq (α := Set ↥(normalization f)) (closure (Set.range (ι := ↥X) ⇑(toNormalization f))) Set.univ

Tactic:
rw [IdealSheafData.support_bot, Scheme.Hom.support_ker, TopologicalSpace.Closeds.coe_top] at this

Premises used: TopologicalSpace.Closeds.coe_top, AlgebraicGeometry.Scheme.Hom.support_ker, AlgebraicGeometry.Scheme.IdealSheafData.support_bot
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
this : Eq (α := Set ↥(normalization f)) (closure (Set.range (ι := ↥X) ⇑(toNormalization f))) Set.univ
⊢ IsDominant (Y := normalization f) (toNormalization f)

Tactic:
⟨dense_iff_closure_eq.mpr this⟩

Premises used: Iff.mpr, dense_iff_closure_eq, AlgebraicGeometry.IsDominant.mk
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
this : Eq (α := Set ↥(normalization f)) (closure (Set.range (ι := ↥X) ⇑(toNormalization f))) Set.univ
⊢ IsDominant (Y := normalization f) (toNormalization f)

Tactic:
exact ⟨dense_iff_closure_eq.mpr this⟩
-- Module: Mathlib.AlgebraicGeometry.Normalization
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))
⊢ _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
-- Module: Mathlib.AlgebraicGeometry.Normalization
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)
dsimp : IsReduced.{u} (Spec ((normalizationDiagram f).obj (Opposite.op (toOpens i))))
⊢ IsReduced.{u} (PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) i)

Tactic:
dsimp [normalizationOpenCover, normalizationGlueData, relativeGluingData]

Premises used: AlgebraicGeometry.Scheme.AffineZariskiSite.relativeGluingData, AlgebraicGeometry.Scheme.Hom.normalizationGlueData, AlgebraicGeometry.Scheme.Hom.normalizationOpenCover
-- Module: Mathlib.AlgebraicGeometry.Normalization
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} (Spec ((normalizationDiagram f).obj (Opposite.op (toOpens i))))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
inst_2 : IsIntegral X
rw : IsIrreducible.{u} (X := ↥(normalization f)) ⊤
⊢ IrreducibleSpace.{u} ↥(normalization f)

Tactic:
rw [irreducibleSpace_def]

Premises used: irreducibleSpace_def
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
inst_2 : IsIntegral X
⊢ IsIrreducible (X := ↥(normalization f)) (closure (Set.image (α := ↥X) (⇑(toNormalization f)) Set.univ))

Tactic:
((IrreducibleSpace.isIrreducible_univ X).image _
          f.toNormalization.continuous.continuousOn).closure

Premises used: Continuous.continuousOn, AlgebraicGeometry.PresheafedSpace.carrier, IrreducibleSpace.isIrreducible_univ, IsIrreducible.image, IsIrreducible.closure, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.Scheme.Hom.toNormalization, TopCat.carrier, AlgebraicGeometry.Scheme.Hom.continuous, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
inst_2 : IsIntegral X
h : Eq (α := Set ↥(normalization f)) ⊤ (closure (Set.image (α := ↥X) (⇑(toNormalization f)) Set.univ))
⊢ IsIrreducible.{u} (X := ↥(normalization f)) ⊤

Tactic:
convert!
      ((IrreducibleSpace.isIrreducible_univ X).image _
          f.toNormalization.continuous.continuousOn).closure

Premises used: Continuous.continuousOn, AlgebraicGeometry.PresheafedSpace.carrier, IrreducibleSpace.isIrreducible_univ, IsIrreducible.image, IsIrreducible.closure, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.Scheme.Hom.toNormalization, TopCat.carrier, AlgebraicGeometry.Scheme.Hom.continuous, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
inst_2 : IsIntegral X
⊢ Eq (α := Set ↥(normalization f)) ⊤ (closure (Set.image (α := ↥X) (⇑(toNormalization f)) Set.univ))

Tactic:
simpa using f.toNormalization.denseRange.closure_range.symm

Premises used: AlgebraicGeometry.Scheme.Hom.denseRange, AlgebraicGeometry.Scheme.Hom.toNormalization, DenseRange.closure_range, Eq.symm
-- 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₀
⊢ f ⁻¹ᵁ Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op U)) ≤ 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₂
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))
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))) ⋯)).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))
                ⋯)) ≫
          ⋯.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))) ⋯)).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))
                ⋯)) ≫
          ⋯.fromSpec) ≫
        CategoryTheory.Functor.map (Functor.obj (Functor.const (directedCover Y).I₀) T) f_1
⊢ normalization f ⟶ T

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 := ?_ }

Premises used: CategoryTheory.Limits.Cocone.mk, CategoryTheory.NatTrans.mk, CategoryTheory.Limits.colimit.desc, CategoryTheory.CategoryStruct.comp
-- 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₀
x : (↑Γ(T, f₂ ⁻¹ᵁ (↑U : Y.Opens)) : Type u)
⊢ 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 : (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
⊢ Eq.{u + 1} (α := (↑Γ(Y, (↑U : Y.Opens)) : Type u) →+* (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    (algebraMap (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    (@RingHom.comp _ (↑Γ(T, f₂ ⁻¹ᵁ (↑U : Y.Opens)) : Type u) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (↑Γ(T, f₂ ⁻¹ᵁ (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
      (algebraMap (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(T, f₂ ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))

Tactic:
simp only [RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp,
        Hom.app_eq_appLE, Hom.appLE_comp_appLE, ← H]

Premises used: CommRingCat.hom_comp, AlgebraicGeometry.Scheme.Hom.app_eq_appLE, RingHom.algebraMap_toAlgebra, AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE
-- 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₀
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
⊢ 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]
-- 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₀
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
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)
⊢ 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))

Tactic:
.algebraMap (R := Γ(Y, U.1)) (B := Γ(X, f ⁻¹ᵁ U.1)) (f₂.isIntegral_app U.1 U.2 x)

Premises used: Set.Mem, setOf, RingHom.IsIntegralElem, IsIntegral, AlgebraicGeometry.Scheme.Hom.isIntegral_app, IsIntegral.algebraMap, Subtype.val, Subtype.property
-- 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₀
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
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)
⊢ 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))

Tactic:
exact .algebraMap (R := Γ(Y, U.1)) (B := Γ(X, f ⁻¹ᵁ U.1)) (f₂.isIntegral_app U.1 U.2 x)
-- 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 :
  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
⊢ (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

Tactic:
dsimp [normalizationGlueData, relativeGluingData]

Premises used: AlgebraicGeometry.Scheme.AffineZariskiSite.relativeGluingData, AlgebraicGeometry.Scheme.Hom.normalizationGlueData
-- 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 :
  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
⊢ 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

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]

Premises used: AlgebraicGeometry.IsAffineOpen.map_fromSpec, Quiver.Hom.op, Quiver.Hom.le, AlgebraicGeometry.Spec.map_comp_assoc, CategoryTheory.Category.comp_id, CategoryTheory.homOfLE, AlgebraicGeometry.Scheme.AffineZariskiSite.toOpens_mono, AlgebraicGeometry.Scheme.Hom.preimage_mono, 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 V : (directedCover Y).I₀
i : U ⟶ V
refine_2 :
  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)) ⋯)
⊢ 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

Tactic:
congr 2