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
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 := normalization (iU ≫ f) ⨿ normalization (iV ≫ f)) coprod.inl
      (CategoryStruct.comp (Y := normalization f)
        (coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
          (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization 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))) ⋯)) =
    coprod.inl ≫ 𝟙 (normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
have h₁ : CategoryStruct.comp (Y := normalization (iU ≫ f)) (toNormalization (iU ≫ f))
    (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f)) coprod.inl
      (CategoryStruct.comp (Y := normalization f)
        (coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) sorry)
          (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization f) sorry))
        (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))) sorry))) =
  toNormalization (iU ≫ f) ≫ coprod.inl ≫ 𝟙 (normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
Tactic: refine Scheme.Hom.normalization.hom_ext _ _ _
        (coprod.desc (iU ≫ f).fromNormalization (iV ≫ f).fromNormalization) ?_ (by simp) (by simp)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (hypothesis)
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 := normalization (iU ≫ f)) (toNormalization (iU ≫ f))
      (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f)) coprod.inl
        (CategoryStruct.comp (Y := normalization f)
          (coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
            (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization 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))) ⋯))) =
    toNormalization (iU ≫ f) ≫ coprod.inl ≫ 𝟙 (normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
have H : Eq (α := U ⟶ Cocone.pt (F := pair U V) (colimit.cocone (pair U V)))
  (iU ≫ Iso.hom (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V)))) coprod.inl
Tactic: have H : iU ≫ (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).hom = coprod.inl :=
        e.comp_coconePointUniqueUpToIso_hom (colimit.isColimit (pair U V)) ⟨.left⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
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 := normalization (iU ≫ f) ⨿ normalization (iV ≫ f)) coprod.inr
      (CategoryStruct.comp (Y := normalization f)
        (coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
          (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization 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))) ⋯)) =
    coprod.inr ≫ 𝟙 (normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
have h₂ : CategoryStruct.comp (Y := normalization (iV ≫ f)) (toNormalization (iV ≫ f))
    (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f)) coprod.inr
      (CategoryStruct.comp (Y := normalization f)
        (coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) sorry)
          (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization f) sorry))
        (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))) sorry))) =
  toNormalization (iV ≫ f) ≫ coprod.inr ≫ 𝟙 (normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
Tactic: refine Scheme.Hom.normalization.hom_ext _ _ _
        (coprod.desc (iU ≫ f).fromNormalization (iV ≫ f).fromNormalization) ?_ (by simp) (by simp)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (hypothesis)
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 := normalization (iV ≫ f)) (toNormalization (iV ≫ f))
      (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f)) coprod.inr
        (CategoryStruct.comp (Y := normalization f)
          (coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
            (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization 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))) ⋯))) =
    toNormalization (iV ≫ f) ≫ coprod.inr ≫ 𝟙 (normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
have H : Eq (α := V ⟶ Cocone.pt (F := pair U V) (colimit.cocone (pair U V)))
  (iV ≫ Iso.hom (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V)))) coprod.inr
Tactic: have H : iV ≫ (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).hom = coprod.inr :=
        e.comp_coconePointUniqueUpToIso_hom (colimit.isColimit (pair U V)) ⟨.right⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
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 := 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) =
    𝟙 (normalization f)
have refine : 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))) sorry :
        normalization f ⟶ normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
      (coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) sorry)
          (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization f) sorry) :
        normalization (iU ≫ f) ⨿ normalization (iV ≫ f) ⟶ normalization f)) =
  toNormalization f ≫ 𝟙 (normalization f)
Tactic: refine Scheme.Hom.normalization.hom_ext _ _ _ f.fromNormalization ?_ (by simp) (by simp)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
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 := 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)
have 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))) sorry :
          normalization f ⟶ normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
        (coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) sorry)
            (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization f) sorry) :
          normalization (iU ≫ f) ⨿ normalization (iV ≫ f) ⟶ normalization f)))
  (Iso.inv (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))) ≫ toNormalization f ≫ 𝟙 (normalization f))
Tactic: rw [← cancel_epi (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).inv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
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 (α := 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))
have h₁ : 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))) sorry :
            normalization f ⟶ normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
          (coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) sorry)
              (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization f) sorry) :
            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: apply coprod.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
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
⊢ IsIso (X := normalization (X := pullback f g) (pullback.snd f g)) (Y :=
    pullback (X := normalization f) (fromNormalization f) g) (normalizationPullback f g)
have 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)
Tactic: apply IsZariskiLocalAtTarget.of_forall_exists_morphismRestrict (P := .isomorphisms _) fun x ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
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 : (pullback (X := normalization f) (fromNormalization f) g).Opens),
    x ∈ U ∧
      MorphismProperty.isomorphisms Scheme (X := (↑(normalizationPullback f g ⁻¹ᵁ U) : Scheme))
        (normalizationPullback f g ∣_ U)
have 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)
Tactic: obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ := S.isBasis_affineOpens.exists_subset_of_mem_open
    (Set.mem_univ ((pullback.snd _ g ≫ g) x)) isOpen_univ
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
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)
⊢ ∃ (U : (pullback (X := normalization f) (fromNormalization f) g).Opens),
    x ∈ U ∧
      MorphismProperty.isomorphisms Scheme (X := (↑(normalizationPullback f g ⁻¹ᵁ U) : Scheme))
        (normalizationPullback f g ∣_ U)
have 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)
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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
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)
have refine : IsIso (Y := Γ(normalization (pullback.snd f g), normalizationPullback f g ⁻¹ᵁ W)) (app (normalizationPullback f g) W)
Tactic: refine ⟨W, hxV, (isIso_morphismRestrict_iff_isIso_app _ (U := W) (hV.preimage _)).mpr ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
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)
⊢ W = pullback.fst (fromNormalization f) g ⁻¹ᵁ fromNormalization f ⁻¹ᵁ U ⊓ pullback.snd (fromNormalization f) g ⁻¹ᵁ V
have 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)
Tactic: simp_rw [W, ← Scheme.Hom.comp_preimage, pullback.condition, Scheme.Hom.comp_preimage,
      ← Scheme.Hom.preimage_inf, inf_eq_right.mpr hVU]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
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)
⊢ W = pullback.fst (fromNormalization f) g ⁻¹ᵁ fromNormalization f ⁻¹ᵁ U ⊓ pullback.snd (fromNormalization f) g ⁻¹ᵁ V
have 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)
Tactic: simp_rw [W, ← Scheme.Hom.comp_preimage, pullback.condition, Scheme.Hom.comp_preimage,
      ← Scheme.Hom.preimage_inf, inf_eq_right.mpr hVU]