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
inst_2 : IsIntegralHom f
U : (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)).1
e : pullback (Y := PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U)
    (toNormalization f)
    (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U) ≅
  (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) :=
  IsOpenImmersion.isoOfRangeEq
    (pullback.fst (toNormalization f)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U))
    (f ⁻¹ᵁ (↑U : Y.Opens)).ι ⋯
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)))
⊢ RingHom.IsIntegral (R := (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (CommRingCat.Hom.hom (app f (↑U : Y.Opens)))

Tactic:
IsIntegralHom.isIntegral_app _ _ U.2

Premises used: AlgebraicGeometry.IsIntegralHom.isIntegral_app, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
inst_2 : IsIntegralHom f
U : (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)).1
e : pullback (Y := PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U)
    (toNormalization f)
    (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U) ≅
  (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) :=
  IsOpenImmersion.isoOfRangeEq
    (pullback.fst (toNormalization f)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U))
    (f ⁻¹ᵁ (↑U : Y.Opens)).ι ⋯
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)))
⊢ RingHom.IsIntegral (R := (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (CommRingCat.Hom.hom (app f (↑U : Y.Opens)))

Tactic:
exact IsIntegralHom.isIntegral_app _ _ U.2

Premises used: AlgebraicGeometry.IsIntegralHom.isIntegral_app, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
inst_2 : IsIntegralHom f
U : (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)).1
e : pullback (Y := PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U)
    (toNormalization f)
    (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U) ≅
  (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) :=
  IsOpenImmersion.isoOfRangeEq
    (pullback.fst (toNormalization f)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U))
    (f ⁻¹ᵁ (↑U : Y.Opens)).ι ⋯
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)))
⊢ Eq.{u + 1} (α := Subalgebra (↑Γ(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)) ⊤

Tactic:
have : integralClosure Γ(Y, U.1) Γ(X, f ⁻¹ᵁ U.1) = ⊤ := by
    rw [integralClosure_eq_top_iff, ← algebraMap_isIntegral_iff, RingHom.algebraMap_toAlgebra]
    exact IsIntegralHom.isIntegral_app _ _ U.2
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
inst_2 : IsIntegralHom f
U : (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)).1
e : pullback (Y := PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U)
    (toNormalization f)
    (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U) ≅
  (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) :=
  IsOpenImmersion.isoOfRangeEq
    (pullback.fst (toNormalization f)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U))
    (f ⁻¹ᵁ (↑U : Y.Opens)).ι ⋯
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 :
  Eq.{u + 1} (α := Subalgebra (↑Γ(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)) ⊤
rw :
  IsIso.{u, u + 1} (X := Spec (CommRingCat.of (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))) (Y := Spec (CommRingCat.of ↥⊤))
    (Spec.map (CommRingCat.ofHom (AlgHom.toRingHom (Subalgebra.val ⊤))))
⊢ IsIso.{u, u + 1} (X := Spec (CommRingCat.of (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))) (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))))))

Tactic:
rw [this]
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
inst_2 : IsIntegralHom f
U : (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)).1
e : pullback (Y := PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U)
    (toNormalization f)
    (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U) ≅
  (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) :=
  IsOpenImmersion.isoOfRangeEq
    (pullback.fst (toNormalization f)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U))
    (f ⁻¹ᵁ (↑U : Y.Opens)).ι ⋯
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 :
  Eq.{u + 1} (α := Subalgebra (↑Γ(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)) ⊤
⊢ IsIso.{u, u + 1} (X := Spec (CommRingCat.of (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))) (Y := Spec (CommRingCat.of ↥⊤))
    (Spec.map (CommRingCat.ofHom (AlgHom.toRingHom (Subalgebra.val ⊤))))

Tactic:
inferInstanceAs (IsIso (Scheme.Spec.mapIso (Subalgebra.topEquiv
    (R := Γ(Y, U.1)) (A := ↑Γ(X, f ⁻¹ᵁ U.1))).toCommRingCatIso.op).hom)

Premises used: Set.Mem, _private.0.AlgebraicGeometry.Scheme.Hom.instIsIsoToNormalizationOfIsIntegralHom._proof_1
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
inst_2 : IsIntegralHom f
U : (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)).1
e : pullback (Y := PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U)
    (toNormalization f)
    (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U) ≅
  (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) :=
  IsOpenImmersion.isoOfRangeEq
    (pullback.fst (toNormalization f)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U))
    (f ⁻¹ᵁ (↑U : Y.Opens)).ι ⋯
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 :
  Eq.{u + 1} (α := Subalgebra (↑Γ(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)) ⊤
⊢ IsIso.{u, u + 1} (X := Spec (CommRingCat.of (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))) (Y := Spec (CommRingCat.of ↥⊤))
    (Spec.map (CommRingCat.ofHom (AlgHom.toRingHom (Subalgebra.val ⊤))))

Tactic:
exact inferInstanceAs (IsIso (Scheme.Spec.mapIso (Subalgebra.topEquiv
    (R := Γ(Y, U.1)) (A := ↑Γ(X, f ⁻¹ᵁ U.1))).toCommRingCatIso.op).hom)
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
inst_2 : IsAffineHom f
hg : IsSeparated (X := normalization f) (fromNormalization f)
hfg : IsAffineHom (CategoryStruct.comp (Y := normalization f) (toNormalization f) (fromNormalization f))
⊢ IsAffineHom (Y := normalization f) (toNormalization f)

Tactic:
apply MorphismProperty.of_postcomp (W := @IsAffineHom) (W' := @IsSeparated) _ f.fromNormalization

Premises used: AlgebraicGeometry.Scheme.Hom.fromNormalization, AlgebraicGeometry.IsAffineHom, CategoryTheory.MorphismProperty.of_postcomp
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
inst_2 : IsAffineHom f
⊢ IsSeparated (X := normalization f) (fromNormalization f)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
inst_2 hfg : IsAffineHom f
⊢ IsAffineHom (CategoryStruct.comp (Y := normalization f) (toNormalization f) (fromNormalization f))

Tactic:
rw [Hom.toNormalization_fromNormalization]

Premises used: AlgebraicGeometry.Scheme.Hom.toNormalization_fromNormalization
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
inst_2 : IsAffineHom f
⊢ IsAffineHom f

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
hg : QuasiSeparated (X := normalization f) (fromNormalization f)
hfg : QuasiCompact (CategoryStruct.comp (Y := normalization f) (toNormalization f) (fromNormalization f))
⊢ QuasiCompact (Y := normalization f) (toNormalization f)

Tactic:
apply MorphismProperty.of_postcomp (W := @QuasiCompact)
      (W' := @QuasiSeparated) _ f.fromNormalization

Premises used: AlgebraicGeometry.Scheme.Hom.fromNormalization, AlgebraicGeometry.QuasiCompact, CategoryTheory.MorphismProperty.of_postcomp
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
⊢ QuasiSeparated (X := normalization f) (fromNormalization f)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
hfg : QuasiCompact f
⊢ QuasiCompact (CategoryStruct.comp (Y := normalization f) (toNormalization f) (fromNormalization f))

Tactic:
rw [Hom.toNormalization_fromNormalization]

Premises used: AlgebraicGeometry.Scheme.Hom.toNormalization_fromNormalization
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
⊢ QuasiCompact f

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
suffices : QuasiSeparated (CategoryStruct.comp (Y := normalization f) (toNormalization f) (fromNormalization f))
⊢ QuasiSeparated (Y := normalization f) (toNormalization f)

Tactic:
suffices QuasiSeparated (Hom.toNormalization f ≫ Hom.fromNormalization f) from
    .of_comp _ f.fromNormalization
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 rw : QuasiSeparated f
⊢ QuasiSeparated (CategoryStruct.comp (Y := normalization f) (toNormalization f) (fromNormalization f))

Tactic:
rw [Hom.toNormalization_fromNormalization]

Premises used: AlgebraicGeometry.Scheme.Hom.toNormalization_fromNormalization
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
⊢ QuasiSeparated f

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
⊢ Eq (α := (normalization f).IdealSheafData) (ker (toNormalization f)) ⊥

Tactic:
Scheme.IdealSheafData.ext_of_iSup_eq_top
    (fun U : Y.affineOpens ↦ ⟨f.fromNormalization ⁻¹ᵁ U.1, U.2.preimage _⟩)
    (TopologicalSpace.IsOpenCover.comap (iSup_affineOpens_eq_top _) _) fun U ↦ ?_

Premises used: AlgebraicGeometry.Scheme.Hom.fromNormalization, AlgebraicGeometry.iSup_affineOpens_eq_top, TopologicalSpace.IsOpenCover.comap, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', Subtype.mk, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.IdealSheafData.ext_of_iSup_eq_top, 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
refine :
  ∀ (U : (↑Y.affineOpens : Type u)),
    Eq (α :=
      Ideal
        (↑Γ(normalization f,
              (↑((fun (U : (↑Y.affineOpens : Type u)) ↦
                      (Subtype.mk (p := fun (x : (normalization f).Opens) ↦
                          Membership.mem (γ := Set (normalization f).Opens) (normalization f).affineOpens x)
                          (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) ⋯ :
                        { x : (normalization f).Opens //
                          Membership.mem (γ := Set (normalization f).Opens) (normalization f).affineOpens x }))
                    U) :
                (normalization f).Opens)) :
          Type u))
      (IdealSheafData.ideal (ker (toNormalization f))
        ((fun (U : (↑Y.affineOpens : Type u)) ↦
            (Subtype.mk (p := fun (x : (normalization f).Opens) ↦
                Membership.mem (γ := Set (normalization f).Opens) (normalization f).affineOpens x)
                (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) ⋯ :
              { x : (normalization f).Opens //
                Membership.mem (γ := Set (normalization f).Opens) (normalization f).affineOpens x }))
          U))
      (IdealSheafData.ideal ⊥
        ((fun (U : (↑Y.affineOpens : Type u)) ↦
            (Subtype.mk (p := fun (x : (normalization f).Opens) ↦
                Membership.mem (γ := Set (normalization f).Opens) (normalization f).affineOpens x)
                (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) ⋯ :
              { x : (normalization f).Opens //
                Membership.mem (γ := Set (normalization f).Opens) (normalization f).affineOpens x }))
          U))
⊢ Eq (α := (normalization f).IdealSheafData) (ker (toNormalization f)) ⊥

Tactic:
refine Scheme.IdealSheafData.ext_of_iSup_eq_top
    (fun U : Y.affineOpens ↦ ⟨f.fromNormalization ⁻¹ᵁ U.1, U.2.preimage _⟩)
    (TopologicalSpace.IsOpenCover.comap (iSup_affineOpens_eq_top _) _) fun U ↦ ?_

Premises used: AlgebraicGeometry.Scheme.Hom.fromNormalization, AlgebraicGeometry.iSup_affineOpens_eq_top, TopologicalSpace.IsOpenCover.comap, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', Subtype.mk, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.IdealSheafData.ext_of_iSup_eq_top, 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
U : (↑Y.affineOpens : Type u)
simp :
  Eq (α := Ideal (↑Γ(normalization f, fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    (RingHom.ker (F :=
      (↑Γ(normalization f, fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) →+*
        (↑Γ(X, toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
      (CommRingCat.Hom.hom (app (toNormalization f) (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)))))
    ⊥
⊢ Eq (α :=
    Ideal
      (↑Γ(normalization f,
            (↑((fun (U : (↑Y.affineOpens : Type u)) ↦
                    (Subtype.mk (p := fun (x : (normalization f).Opens) ↦
                        Membership.mem (γ := Set (normalization f).Opens) (normalization f).affineOpens x)
                        (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) ⋯ :
                      { x : (normalization f).Opens //
                        Membership.mem (γ := Set (normalization f).Opens) (normalization f).affineOpens x }))
                  U) :
              (normalization f).Opens)) :
        Type u))
    (IdealSheafData.ideal (ker (toNormalization f))
      ((fun (U : (↑Y.affineOpens : Type u)) ↦
          (Subtype.mk (p := fun (x : (normalization f).Opens) ↦
              Membership.mem (γ := Set (normalization f).Opens) (normalization f).affineOpens x)
              (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) ⋯ :
            { x : (normalization f).Opens //
              Membership.mem (γ := Set (normalization f).Opens) (normalization f).affineOpens x }))
        U))
    (IdealSheafData.ideal ⊥
      ((fun (U : (↑Y.affineOpens : Type u)) ↦
          (Subtype.mk (p := fun (x : (normalization f).Opens) ↦
              Membership.mem (γ := Set (normalization f).Opens) (normalization f).affineOpens x)
              (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) ⋯ :
            { x : (normalization f).Opens //
              Membership.mem (γ := Set (normalization f).Opens) (normalization f).affineOpens x }))
        U))

Tactic:
simp only [ker_apply, IdealSheafData.ideal_bot, Pi.bot_apply]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.ideal_bot, Pi.bot_apply, AlgebraicGeometry.Scheme.Hom.ker_apply
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : Type u)
rw :
  MorphismProperty.monomorphisms CommRingCat (X := Γ(normalization f, fromNormalization f ⁻¹ᵁ (↑U : Y.Opens))) (Y :=
    Γ(X, toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)))
    (app (toNormalization f) (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)))
⊢ Eq (α := Ideal (↑Γ(normalization f, fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    (RingHom.ker (F :=
      (↑Γ(normalization f, fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) →+*
        (↑Γ(X, toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
      (CommRingCat.Hom.hom (app (toNormalization f) (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)))))
    ⊥

Tactic:
rw [← RingHom.injective_iff_ker_eq_bot,
    ← ConcreteCategory.mono_iff_injective_of_preservesPullback, ← MorphismProperty.monomorphisms]

Premises used: CategoryTheory.MorphismProperty.monomorphisms, RingHom.injective_iff_ker_eq_bot, CategoryTheory.ConcreteCategory.mono_iff_injective_of_preservesPullback
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : Type u)
simp :
  MorphismProperty.monomorphisms CommRingCat (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)))
⊢ MorphismProperty.monomorphisms CommRingCat (X := Γ(normalization f, fromNormalization f ⁻¹ᵁ (↑U : Y.Opens))) (Y :=
    Γ(X, toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)))
    (app (toNormalization f) (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)))

Tactic:
simp only [toNormalization_app_preimage,
    eqToHom_op, MorphismProperty.cancel_left_of_respectsIso,
    MorphismProperty.cancel_right_of_respectsIso]

Premises used: AlgebraicGeometry.Scheme.Hom.toNormalization_app_preimage, CategoryTheory.eqToHom_op, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : Type u)
rw :
  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))
⊢ MorphismProperty.monomorphisms CommRingCat (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)))

Tactic:
rw [MorphismProperty.monomorphisms, @ConcreteCategory.mono_iff_injective_of_preservesPullback]

Premises used: CategoryTheory.MorphismProperty.monomorphisms, CategoryTheory.ConcreteCategory.mono_iff_injective_of_preservesPullback
-- 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:
Subtype.val_injective

Premises used: Subtype.val_injective