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 V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst_2 : QuasiCompact iU
inst_3 : QuasiSeparated iU
inst_4 : QuasiCompact iV
inst_5 : QuasiSeparated iV
rw :
  Eq (α := Cocone.pt (F := pair U V) (colimit.cocone (pair U V)) ⟶ normalization f)
    (Iso.inv (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))) ≫
      CategoryStruct.comp (Y := normalization f) (toNormalization f)
        (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
          (normalizationDesc f
              (CategoryStruct.comp (Y := Cocone.pt (F := pair U V) (colimit.cocone (pair U V)))
                (Iso.hom (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))))
                (coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f))))
              (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))) ⋯ :
            normalization f ⟶ normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
          (coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
              (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization f) ⋯) :
            normalization (iU ≫ f) ⨿ normalization (iV ≫ f) ⟶ normalization f)))
    (Iso.inv (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))) ≫ toNormalization f ≫ 𝟙 (normalization f))
⊢ CategoryStruct.comp (Y := normalization f) (toNormalization f)
      (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
        (normalizationDesc f
            (CategoryStruct.comp (Y := Cocone.pt (F := pair U V) (colimit.cocone (pair U V)))
              (Iso.hom (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))))
              (coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f))))
            (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))) ⋯ :
          normalization f ⟶ normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
        (coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
            (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization f) ⋯) :
          normalization (iU ≫ f) ⨿ normalization (iV ≫ f) ⟶ normalization f)) =
    toNormalization f ≫ 𝟙 (normalization f)

Tactic:
rw [← cancel_epi (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).inv]

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.pair, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst_2 : QuasiCompact iU
inst_3 : QuasiSeparated iU
inst_4 : QuasiCompact iV
inst_5 : QuasiSeparated iV
⊢ CategoryStruct.comp (Y := U ⨿ V) coprod.inl
      (Iso.inv (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))) ≫
        CategoryStruct.comp (Y := normalization f) (toNormalization f)
          (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
            (normalizationDesc f
                (CategoryStruct.comp (Y := Cocone.pt (F := pair U V) (colimit.cocone (pair U V)))
                  (Iso.hom (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))))
                  (coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f))))
                (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))) ⋯ :
              normalization f ⟶ normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
            (coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
                (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization f) ⋯) :
              normalization (iU ≫ f) ⨿ normalization (iV ≫ f) ⟶ normalization f))) =
    CategoryStruct.comp (Y := U ⨿ V) coprod.inl
      (Iso.inv (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))) ≫ toNormalization f ≫ 𝟙 (normalization f))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst_2 : QuasiCompact iU
inst_3 : QuasiSeparated iU
inst_4 : QuasiCompact iV
inst_5 : QuasiSeparated iV
⊢ CategoryStruct.comp (Y := U ⨿ V) coprod.inr
      (Iso.inv (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))) ≫
        CategoryStruct.comp (Y := normalization f) (toNormalization f)
          (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
            (normalizationDesc f
                (CategoryStruct.comp (Y := Cocone.pt (F := pair U V) (colimit.cocone (pair U V)))
                  (Iso.hom (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))))
                  (coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f))))
                (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))) ⋯ :
              normalization f ⟶ normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
            (coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
                (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization f) ⋯) :
              normalization (iU ≫ f) ⨿ normalization (iV ≫ f) ⟶ normalization f))) =
    CategoryStruct.comp (Y := U ⨿ V) coprod.inr
      (Iso.inv (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))) ≫ toNormalization f ≫ 𝟙 (normalization f))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst_2 : QuasiCompact iU
inst_3 : QuasiSeparated iU
inst_4 : QuasiCompact iV
inst_5 : QuasiSeparated iV
⊢ Eq (α := U ⟶ normalization f)
    (CategoryStruct.comp (Y := normalization (iU ≫ f)) (toNormalization (iU ≫ f) : U ⟶ normalization (iU ≫ f))
      (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
          (coprod.inl : normalization (iU ≫ f) ⟶ normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
          (Iso.hom (normalizationCoprodIso f e) : normalization (iU ≫ f) ⨿ normalization (iV ≫ f) ⟶ normalization f) :
        normalization (iU ≫ f) ⟶ normalization f))
    (iU ≫ toNormalization f)

Tactic:
simp [Scheme.Hom.normalizationCoprodIso]

Premises used: AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst_2 : QuasiCompact iU
inst_3 : QuasiSeparated iU
inst_4 : QuasiCompact iV
inst_5 : QuasiSeparated iV
⊢ Eq (α := V ⟶ normalization f)
    (CategoryStruct.comp (Y := normalization (iV ≫ f)) (toNormalization (iV ≫ f) : V ⟶ normalization (iV ≫ f))
      (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
          (coprod.inr : normalization (iV ≫ f) ⟶ normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
          (Iso.hom (normalizationCoprodIso f e) : normalization (iU ≫ f) ⨿ normalization (iV ≫ f) ⟶ normalization f) :
        normalization (iV ≫ f) ⟶ normalization f))
    (iV ≫ toNormalization f)

Tactic:
simp [Scheme.Hom.normalizationCoprodIso]

Premises used: AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst_2 : QuasiCompact iU
inst_3 : QuasiSeparated iU
inst_4 : QuasiCompact iV
inst_5 : QuasiSeparated iV
⊢ Eq (α := U ⟶ normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
    (iU ≫ CategoryStruct.comp (Y := normalization f) (toNormalization f) (Iso.inv (normalizationCoprodIso f e)) :
      U ⟶ normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
    (toNormalization (iU ≫ f) ≫ coprod.inl : U ⟶ normalization (iU ≫ f) ⨿ normalization (iV ≫ f))

Tactic:
simp [← toNormalization_inl_normalizationCoprodIso_hom_assoc f e]

Premises used: AlgebraicGeometry.Scheme.Hom.toNormalization_inl_normalizationCoprodIso_hom_assoc
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst_2 : QuasiCompact iU
inst_3 : QuasiSeparated iU
inst_4 : QuasiCompact iV
inst_5 : QuasiSeparated iV
⊢ Eq (α := V ⟶ normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
    (iV ≫ CategoryStruct.comp (Y := normalization f) (toNormalization f) (Iso.inv (normalizationCoprodIso f e)) :
      V ⟶ normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
    (toNormalization (iV ≫ f) ≫ coprod.inr : V ⟶ normalization (iU ≫ f) ⨿ normalization (iV ≫ f))

Tactic:
simp [← toNormalization_inr_normalizationCoprodIso_hom_assoc f e]

Premises used: AlgebraicGeometry.Scheme.Hom.toNormalization_inr_normalizationCoprodIso_hom_assoc
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst_2 : QuasiCompact iU
inst_3 : QuasiSeparated iU
inst_4 : QuasiCompact iV
inst_5 : QuasiSeparated iV
⊢ Eq (α := normalization (iU ≫ f) ⟶ Y)
    (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
        (coprod.inl : normalization (iU ≫ f) ⟶ normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
        (CategoryStruct.comp (Y := normalization f) (Iso.hom (normalizationCoprodIso f e)) (fromNormalization f) :
          normalization (iU ≫ f) ⨿ normalization (iV ≫ f) ⟶ Y) :
      normalization (iU ≫ f) ⟶ Y)
    (fromNormalization (iU ≫ f) : normalization (iU ≫ f) ⟶ Y)

Tactic:
simp [Scheme.Hom.normalizationCoprodIso]

Premises used: AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst_2 : QuasiCompact iU
inst_3 : QuasiSeparated iU
inst_4 : QuasiCompact iV
inst_5 : QuasiSeparated iV
⊢ Eq (α := normalization (iV ≫ f) ⟶ Y)
    (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
        (coprod.inr : normalization (iV ≫ f) ⟶ normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
        (CategoryStruct.comp (Y := normalization f) (Iso.hom (normalizationCoprodIso f e)) (fromNormalization f) :
          normalization (iU ≫ f) ⨿ normalization (iV ≫ f) ⟶ Y) :
      normalization (iV ≫ f) ⟶ Y)
    (fromNormalization (iV ≫ f) : normalization (iV ≫ f) ⟶ Y)

Tactic:
simp [Scheme.Hom.normalizationCoprodIso]

Premises used: AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst_2 : QuasiCompact iU
inst_3 : QuasiSeparated iU
inst_4 : QuasiCompact iV
inst_5 : QuasiSeparated iV
⊢ Eq (α := normalization f ⟶ Y)
    (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
      (Iso.inv (normalizationCoprodIso f e) : normalization f ⟶ normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
      (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f)) :
        normalization (iU ≫ f) ⨿ normalization (iV ≫ f) ⟶ Y))
    (fromNormalization f)

Tactic:
simp [Scheme.Hom.normalizationCoprodIso]

Premises used: AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
inst : QuasiCompact f_1
inst_1 : QuasiSeparated f_1
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_2 : QuasiCompact f
inst_3 : QuasiSeparated f
⊢ f ≫ 𝟙 S = CategoryStruct.comp (Y := normalization f) (toNormalization f) (fromNormalization f)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
inst : QuasiCompact f_1
inst_1 : QuasiSeparated f_1
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_2 : QuasiCompact f
inst_3 : QuasiSeparated f
⊢ g ≫ 𝟙 S = 𝟙 Y ≫ g

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
inst : QuasiCompact f_1
inst_1 : QuasiSeparated f_1
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_2 : QuasiCompact f
inst_3 : QuasiSeparated f
⊢ Eq (α := pullback f g ⟶ Y) (pullback.snd f g)
    (CategoryStruct.comp (Y := pullback (X := normalization f) (fromNormalization f) g)
      (pullback.map f g (fromNormalization f) g (toNormalization f) (𝟙 Y) (𝟙 S) ⋯ ⋯)
      (pullback.snd (fromNormalization f) g))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : QuasiCompact f
inst_1 : QuasiSeparated f
⊢ Eq (α := normalization (X := pullback f g) (pullback.snd f g) ⟶ Y)
    (CategoryStruct.comp (Y := pullback (X := normalization f) (fromNormalization f) g) (normalizationPullback f g)
        (pullback.snd (fromNormalization f) g) :
      normalization (X := pullback f g) (pullback.snd f g) ⟶ Y)
    (fromNormalization (pullback.snd f g) : normalization (X := pullback f g) (pullback.snd f g) ⟶ Y)

Tactic:
(pullback.snd f g).normalizationDesc_comp ..

Premises used: CategoryTheory.Limits.pullback.snd, AlgebraicGeometry.Scheme.Hom.normalizationDesc_comp
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
inst : QuasiCompact f_1
inst_1 : QuasiSeparated f_1
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_2 : QuasiCompact f
inst_3 : QuasiSeparated f
inst_4 : Smooth g
apply :
  ∀ (x : ↥(pullback (X := normalization f) (fromNormalization f) g)),
    ∃ (U : (pullback (X := normalization f) (fromNormalization f) g).Opens),
      x ∈ U ∧
        MorphismProperty.isomorphisms Scheme (X := (↑(normalizationPullback f g ⁻¹ᵁ U) : Scheme))
          (normalizationPullback f g ∣_ U)
⊢ IsIso (X := normalization (X := pullback f g) (pullback.snd f g)) (Y :=
    pullback (X := normalization f) (fromNormalization f) g) (normalizationPullback f g)

Tactic:
apply IsZariskiLocalAtTarget.of_forall_exists_morphismRestrict (P := .isomorphisms _) fun x ↦ ?_

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.of_forall_exists_morphismRestrict
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
inst : QuasiCompact f_1
inst_1 : QuasiSeparated f_1
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_2 : QuasiCompact f
inst_3 : QuasiSeparated f
inst_4 : Smooth g
x : ↥(pullback (X := normalization f) (fromNormalization f) g)
obtain :
  ∀ (U : TopologicalSpace.Opens ↥S) (hU : U ∈ S.affineOpens)
    (hxU : Membership.mem (α := ↥S) (↑U : Set ↥S) ((pullback.snd (fromNormalization f) g ≫ g) x : ↥S)),
    ∃ (U : (pullback (X := normalization f) (fromNormalization f) g).Opens),
      x ∈ U ∧
        MorphismProperty.isomorphisms Scheme (X := (↑(normalizationPullback f g ⁻¹ᵁ U) : Scheme))
          (normalizationPullback f g ∣_ U)
⊢ ∃ (U : (pullback (X := normalization f) (fromNormalization f) g).Opens),
    x ∈ U ∧
      MorphismProperty.isomorphisms Scheme (X := (↑(normalizationPullback f g ⁻¹ᵁ U) : Scheme))
        (normalizationPullback f g ∣_ U)

Tactic:
obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ := S.isBasis_affineOpens.exists_subset_of_mem_open
    (Set.mem_univ ((pullback.snd _ g ≫ g) x)) isOpen_univ

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.pullback.snd, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', isOpen_univ, CategoryTheory.CategoryStruct.comp, Set.mem_univ, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.isBasis_affineOpens, DFunLike.coe, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
inst : QuasiCompact f_1
inst_1 : QuasiSeparated f_1
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_2 : QuasiCompact f
inst_3 : QuasiSeparated f
inst_4 : Smooth g
x : ↥(pullback (X := normalization f) (fromNormalization f) g)
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : Membership.mem (α := ↥S) (↑U : Set ↥S) ((pullback.snd (fromNormalization f) g ≫ g) x : ↥S)
obtain :
  ∀ (V : TopologicalSpace.Opens ↥Y) (hV : V ∈ Y.affineOpens)
    (hxV : Membership.mem (α := ↥Y) (↑V : Set ↥Y) ((pullback.snd (fromNormalization f) g) x : ↥Y)) (hVU : V ≤ g ⁻¹ᵁ U),
    ∃ (U : (pullback (X := normalization f) (fromNormalization f) g).Opens),
      x ∈ U ∧
        MorphismProperty.isomorphisms Scheme (X := (↑(normalizationPullback f g ⁻¹ᵁ U) : Scheme))
          (normalizationPullback f g ∣_ U)
⊢ ∃ (U : (pullback (X := normalization f) (fromNormalization f) g).Opens),
    x ∈ U ∧
      MorphismProperty.isomorphisms Scheme (X := (↑(normalizationPullback f g ⁻¹ᵁ U) : Scheme))
        (normalizationPullback f g ∣_ U)

Tactic:
obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU : V ≤ g ⁻¹ᵁ U⟩ :=
    Y.isBasis_affineOpens.exists_subset_of_mem_open (a := pullback.snd _ g x) hxU (g ⁻¹ᵁ U).2

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, TopologicalSpace.Opens.is_open', AlgebraicGeometry.Scheme.isBasis_affineOpens, CategoryTheory.Functor.obj, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
inst : QuasiCompact f_1
inst_1 : QuasiSeparated f_1
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_2 : QuasiCompact f
inst_3 : QuasiSeparated f
inst_4 : Smooth g
x : ↥(pullback (X := normalization f) (fromNormalization f) g)
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : Membership.mem (α := ↥S) (↑U : Set ↥S) ((pullback.snd (fromNormalization f) g ≫ g) x : ↥S)
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : Membership.mem (α := ↥Y) (↑V : Set ↥Y) ((pullback.snd (fromNormalization f) g) x : ↥Y)
hVU : V ≤ g ⁻¹ᵁ U
W : (pullback (X := normalization f) (fromNormalization f) g).Opens := pullback.snd (fromNormalization f) g ⁻¹ᵁ V
⊢ ∃ (U : (pullback (X := normalization f) (fromNormalization f) g).Opens),
    x ∈ U ∧
      MorphismProperty.isomorphisms Scheme (X := (↑(normalizationPullback f g ⁻¹ᵁ U) : Scheme))
        (normalizationPullback f g ∣_ U)

Tactic:
⟨W, hxV, (isIso_morphismRestrict_iff_isIso_app _ (U := W) (hV.preimage _)).mpr ?_⟩

Premises used: Iff.mpr, AlgebraicGeometry.isIso_morphismRestrict_iff_isIso_app, And.intro, Exists.intro, AlgebraicGeometry.IsAffineOpen.preimage
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
inst : QuasiCompact f_1
inst_1 : QuasiSeparated f_1
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_2 : QuasiCompact f
inst_3 : QuasiSeparated f
inst_4 : Smooth g
x : ↥(pullback (X := normalization f) (fromNormalization f) g)
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : Membership.mem (α := ↥S) (↑U : Set ↥S) ((pullback.snd (fromNormalization f) g ≫ g) x : ↥S)
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : Membership.mem (α := ↥Y) (↑V : Set ↥Y) ((pullback.snd (fromNormalization f) g) x : ↥Y)
hVU : V ≤ g ⁻¹ᵁ U
W : (pullback (X := normalization f) (fromNormalization f) g).Opens := pullback.snd (fromNormalization f) g ⁻¹ᵁ V
refine :
  IsIso (Y := Γ(normalization (pullback.snd f g), normalizationPullback f g ⁻¹ᵁ W)) (app (normalizationPullback f g) W)
⊢ ∃ (U : (pullback (X := normalization f) (fromNormalization f) g).Opens),
    x ∈ U ∧
      MorphismProperty.isomorphisms Scheme (X := (↑(normalizationPullback f g ⁻¹ᵁ U) : Scheme))
        (normalizationPullback f g ∣_ U)

Tactic:
refine ⟨W, hxV, (isIso_morphismRestrict_iff_isIso_app _ (U := W) (hV.preimage _)).mpr ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
inst : QuasiCompact f_1
inst_1 : QuasiSeparated f_1
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_2 : QuasiCompact f
inst_3 : QuasiSeparated f
inst_4 : Smooth g
x : ↥(pullback (X := normalization f) (fromNormalization f) g)
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : Membership.mem (α := ↥S) (↑U : Set ↥S) ((pullback.snd (fromNormalization f) g ≫ g) x : ↥S)
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : Membership.mem (α := ↥Y) (↑V : Set ↥Y) ((pullback.snd (fromNormalization f) g) x : ↥Y)
hVU : V ≤ g ⁻¹ᵁ U
W : (pullback (X := normalization f) (fromNormalization f) g).Opens := pullback.snd (fromNormalization f) g ⁻¹ᵁ V
simp_rw :
  Eq (α := (pullback (X := normalization f) (fromNormalization f) g).Opens) (pullback.snd (fromNormalization f) g ⁻¹ᵁ V)
    (pullback.fst (fromNormalization f) g ⁻¹ᵁ fromNormalization f ⁻¹ᵁ U ⊓ pullback.snd (fromNormalization f) g ⁻¹ᵁ V)
simp_rw₁ :
  Eq (α := (pullback (X := normalization f) (fromNormalization f) g).Opens) (pullback.snd (fromNormalization f) g ⁻¹ᵁ V)
    ((pullback.fst (fromNormalization f) g ≫ fromNormalization f) ⁻¹ᵁ U ⊓ pullback.snd (fromNormalization f) g ⁻¹ᵁ V)
simp_rw₂ :
  Eq (α := (pullback (X := normalization f) (fromNormalization f) g).Opens) (pullback.snd (fromNormalization f) g ⁻¹ᵁ V)
    ((pullback.snd (fromNormalization f) g ≫ g) ⁻¹ᵁ U ⊓ pullback.snd (fromNormalization f) g ⁻¹ᵁ V)
simp_rw₃ :
  Eq (α := (pullback (X := normalization f) (fromNormalization f) g).Opens) (pullback.snd (fromNormalization f) g ⁻¹ᵁ V)
    (pullback.snd (fromNormalization f) g ⁻¹ᵁ g ⁻¹ᵁ U ⊓ pullback.snd (fromNormalization f) g ⁻¹ᵁ V)
simp_rw₄ :
  Eq (α := (pullback (X := normalization f) (fromNormalization f) g).Opens) (pullback.snd (fromNormalization f) g ⁻¹ᵁ V)
    (pullback.snd (fromNormalization f) g ⁻¹ᵁ (g ⁻¹ᵁ U ⊓ V))
⊢ W = pullback.fst (fromNormalization f) g ⁻¹ᵁ fromNormalization f ⁻¹ᵁ U ⊓ pullback.snd (fromNormalization f) g ⁻¹ᵁ V

Tactic:
simp_rw [W, ← Scheme.Hom.comp_preimage, pullback.condition, Scheme.Hom.comp_preimage,
      ← Scheme.Hom.preimage_inf, inf_eq_right.mpr hVU]

Premises used: Iff.mpr, AlgebraicGeometry.Scheme.Hom.comp_preimage, AlgebraicGeometry.Scheme.Hom.preimage_inf, CategoryTheory.Limits.pullback.condition, inf_eq_right
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
inst : QuasiCompact f_1
inst_1 : QuasiSeparated f_1
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_2 : QuasiCompact f
inst_3 : QuasiSeparated f
inst_4 : Smooth g
x : ↥(pullback (X := normalization f) (fromNormalization f) g)
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : Membership.mem (α := ↥S) (↑U : Set ↥S) ((pullback.snd (fromNormalization f) g ≫ g) x : ↥S)
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : Membership.mem (α := ↥Y) (↑V : Set ↥Y) ((pullback.snd (fromNormalization f) g) x : ↥Y)
hVU : V ≤ g ⁻¹ᵁ U
W : (pullback (X := normalization f) (fromNormalization f) g).Opens := pullback.snd (fromNormalization f) g ⁻¹ᵁ V
⊢ IsIso (X :=
    pushout (Y := Γ(normalization f, fromNormalization f ⁻¹ᵁ U))
      (appLE (fromNormalization f) U (fromNormalization f ⁻¹ᵁ U) ⋯) (appLE g U V hVU))
    (Y := Γ(pullback (fromNormalization f) g, W)) (pushoutSection ⋯ hVU ⋯ ⋯)

Tactic:
have := isIso_pushoutSection_of_isQuasiSeparated_of_flat_right
    (.of_hasPullback f.fromNormalization g) hVU le_rfl (UY := W)
    (by simp_rw [W, ← Scheme.Hom.comp_preimage, pullback.condition, Scheme.Hom.comp_preimage,
      ← Scheme.Hom.preimage_inf, inf_eq_right.mpr hVU]) hU hV
    (hU.preimage f.fromNormalization).isCompact (hU.preimage f.fromNormalization).isQuasiSeparated