awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
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)).ι ⋯
⊢ MorphismProperty.isomorphisms Scheme (X :=
    (Precoverage.ZeroHypercover.pullback₁ (T := normalization f) (toNormalization f) (normalizationOpenCover f)).X U)
    (Cover.pullbackHom (P := IsOpenImmersion) (normalizationOpenCover f) (toNormalization f) U :
      (Precoverage.ZeroHypercover.pullback₁ (T := normalization f) (toNormalization f) (normalizationOpenCover f)).X U ⟶
        PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U)
have rw : MorphismProperty.isomorphisms Scheme
  ((e ≪≫ sorry.isoSpec).inv ≫ Cover.pullbackHom (P := IsOpenImmersion) (normalizationOpenCover f) (toNormalization f) U)
Tactic: rw [← MorphismProperty.cancel_left_of_respectsIso (.isomorphisms _)
    (e ≪≫ (U.2.preimage f).isoSpec).inv]
-- 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 : 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)))
⊢ MorphismProperty.isomorphisms Scheme
    ((e ≪≫ ⋯.isoSpec).inv ≫ Cover.pullbackHom (P := IsOpenImmersion) (normalizationOpenCover f) (toNormalization f) U)
have h : Spec Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) = Spec (CommRingCat.of (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) →
  PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U =
      Spec (CommRingCat.of ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))) →
    (e ≪≫ sorry.isoSpec).inv ≫ Cover.pullbackHom (P := IsOpenImmersion) (normalizationOpenCover f) (toNormalization f) U =
      Spec.map
        (CommRingCat.ofHom
          (AlgHom.toRingHom
            (Subalgebra.val (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))))
Tactic: convert_to IsIso (Spec.map (CommRingCat.ofHom
      (integralClosure Γ(Y, U.1) Γ(X, f ⁻¹ᵁ U.1)).val.toRingHom))
-- 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 : 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)))
h :
  Spec Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) = Spec (CommRingCat.of (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) →
    PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U =
        Spec
          (CommRingCat.of ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))) →
      (e ≪≫ ⋯.isoSpec).inv ≫ Cover.pullbackHom (P := IsOpenImmersion) (normalizationOpenCover f) (toNormalization f) U =
        Spec.map
          (CommRingCat.ofHom
            (AlgHom.toRingHom
              (Subalgebra.val
                (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))))
⊢ MorphismProperty.isomorphisms Scheme
    ((e ≪≫ ⋯.isoSpec).inv ≫ Cover.pullbackHom (P := IsOpenImmersion) (normalizationOpenCover f) (toNormalization f) U)
have convert_to : 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: convert_to IsIso (Spec.map (CommRingCat.ofHom
      (integralClosure Γ(Y, U.1) Γ(X, f ⁻¹ᵁ U.1)).val.toRingHom))
-- 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 : 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)))
e_3 : Spec Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) = Spec (CommRingCat.of (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
e_4 :
  PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U =
    Spec (CommRingCat.of ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))
⊢ (e ≪≫ ⋯.isoSpec).inv ≫ Cover.pullbackHom (P := IsOpenImmersion) (normalizationOpenCover f) (toNormalization f) U =
    Spec.map
      (CommRingCat.ofHom
        (AlgHom.toRingHom
          (Subalgebra.val (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))))
have h : sorry.isoSpec.hom ≫
    ((e ≪≫ sorry.isoSpec).inv ≫ Cover.pullbackHom (P := IsOpenImmersion) (normalizationOpenCover f) (toNormalization f) U) ≫
      PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U =
  sorry.isoSpec.hom ≫
    CategoryStruct.comp (Y :=
      PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U)
      (Spec.map
        (CommRingCat.ofHom
          (AlgHom.toRingHom
            (Subalgebra.val
              (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))))
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U)
Tactic: rw [← cancel_mono (f.normalizationOpenCover.f U), ← cancel_epi (U.2.preimage f).isoSpec.hom]
-- 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 : 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)) ⊤
have rw : RingHom.IsIntegral (R := (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (CommRingCat.Hom.hom (app f (↑U : Y.Opens)))
Tactic: rw [integralClosure_eq_top_iff, ← algebraMap_isIntegral_iff, RingHom.algebraMap_toAlgebra]
-- 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 : 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)))
⊢ 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))))))
have 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)) ⊤
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
-- 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 : 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 ↥(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))))))
have 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 ⊤))))
Tactic: rw [this]
-- 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 : IsAffineHom f
⊢ IsAffineHom (Y := normalization f) (toNormalization f)
have hg : IsSeparated (X := normalization f) (fromNormalization f)
Tactic: apply MorphismProperty.of_postcomp (W := @IsAffineHom) (W' := @IsSeparated) _ f.fromNormalization
-- 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 : IsAffineHom f
hg : IsSeparated (X := normalization f) (fromNormalization f)
⊢ IsAffineHom (Y := normalization f) (toNormalization f)
have hfg : IsAffineHom (CategoryStruct.comp (Y := normalization f) (toNormalization f) (fromNormalization f))
Tactic: apply MorphismProperty.of_postcomp (W := @IsAffineHom) (W' := @IsSeparated) _ f.fromNormalization
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
⊢ QuasiCompact (Y := normalization f) (toNormalization f)
have hg : QuasiSeparated (X := normalization f) (fromNormalization f)
Tactic: apply MorphismProperty.of_postcomp (W := @QuasiCompact)
      (W' := @QuasiSeparated) _ f.fromNormalization
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
hg : QuasiSeparated (X := normalization f) (fromNormalization f)
⊢ QuasiCompact (Y := normalization f) (toNormalization f)
have hfg : QuasiCompact (CategoryStruct.comp (Y := normalization f) (toNormalization f) (fromNormalization f))
Tactic: apply MorphismProperty.of_postcomp (W := @QuasiCompact)
      (W' := @QuasiSeparated) _ f.fromNormalization
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
⊢ QuasiSeparated (Y := normalization f) (toNormalization f)
have suffices : QuasiSeparated (CategoryStruct.comp (Y := normalization f) (toNormalization f) (fromNormalization f))
Tactic: suffices QuasiSeparated (Hom.toNormalization f ≫ Hom.fromNormalization f) from
    .of_comp _ f.fromNormalization
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
⊢ Eq (α := (normalization f).IdealSheafData) (ker (toNormalization f)) ⊥
have 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)) sorry :
                      { 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)) sorry :
            { 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)) sorry :
            { x : (normalization f).Opens //
              Membership.mem (γ := Set (normalization f).Opens) (normalization f).affineOpens x }))
        U))
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 ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
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))
have 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)))))
  ⊥
Tactic: simp only [ker_apply, IdealSheafData.ideal_bot, Pi.bot_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : Type u)
⊢ 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)))))
    ⊥
have 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)))
Tactic: rw [← RingHom.injective_iff_ker_eq_bot,
    ← ConcreteCategory.mono_iff_injective_of_preservesPullback, ← MorphismProperty.monomorphisms]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : 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)))
have 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)))
Tactic: simp only [toNormalization_app_preimage,
    eqToHom_op, MorphismProperty.cancel_left_of_respectsIso,
    MorphismProperty.cancel_right_of_respectsIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : 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)))
have 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))
Tactic: rw [MorphismProperty.monomorphisms, @ConcreteCategory.mono_iff_injective_of_preservesPullback]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
⊢ IsDominant (Y := normalization f) (toNormalization f)
have this : (↑(IdealSheafData.support (ker (toNormalization f))) : Set ↥(normalization f)) =
  (↑(IdealSheafData.support ⊥) : Set ↥(normalization f))
Tactic: have := congr(($(f.ker_toNormalization).support : Set f.normalization))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (hypothesis)
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))
⊢ IsDominant (Y := normalization f) (toNormalization f)
have this₁ : 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
Cleared hypotheses: this