awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)
⊢ 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]
-- 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)
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)
⊢ 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 ⊓ 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 (hypothesis)
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 (Y := Γ(normalization (pullback.snd f g), normalizationPullback f g ⁻¹ᵁ W)) (app (normalizationPullback f g) W)
have this : IsIso (X :=
  pushout (Y := Γ(normalization f, fromNormalization f ⁻¹ᵁ U))
    (appLE (fromNormalization f) U (fromNormalization f ⁻¹ᵁ U) sorry) (appLE g U V hVU))
  (Y := Γ(pullback (fromNormalization f) g, W)) (pushoutSection sorry hVU sorry sorry)
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
-- 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
this :
  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 ⋯ ⋯)
⊢ IsIso (Y := Γ(normalization (pullback.snd f g), normalizationPullback f g ⁻¹ᵁ W)) (app (normalizationPullback f g) W)
have rw : IsIso (X :=
  pushout (Y := Γ(normalization f, fromNormalization f ⁻¹ᵁ U)) (app (fromNormalization f) U) (appLE g U V hVU)) (Y :=
  Γ(normalization (pullback.snd f g), normalizationPullback f g ⁻¹ᵁ W))
  (Iso.hom (pushout.congrHom sorry sorry) ≫ pushoutSection sorry hVU sorry sorry ≫ app (normalizationPullback f g) W)
Tactic: rw [← @isIso_comp_left_iff _ _ _ _ _ _ _ this,
    ← isIso_comp_left_iff (pushout.congrHom f.fromNormalization.app_eq_appLE rfl).hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (hypothesis)
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
this :
  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 ⋯ ⋯)
⊢ IsIso (X :=
    pushout (Y := Γ(normalization f, fromNormalization f ⁻¹ᵁ U)) (app (fromNormalization f) U) (appLE g U V hVU)) (Y :=
    Γ(normalization (pullback.snd f g), normalizationPullback f g ⁻¹ᵁ W))
    (Iso.hom (pushout.congrHom ⋯ ⋯) ≫ pushoutSection ⋯ hVU ⋯ ⋯ ≫ app (normalizationPullback f g) W)
have this₁ : (CommRingCat.Hom.hom (appLE g U V hVU)).Smooth
Tactic: have : (g.appLE U V hVU).hom.Smooth := g.smooth_appLE hU hV hVU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (hypothesis)
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
this_1 :
  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 ⋯ ⋯)
this : (CommRingCat.Hom.hom (appLE g U V hVU)).Smooth
⊢ IsIso (X :=
    pushout (Y := Γ(normalization f, fromNormalization f ⁻¹ᵁ U)) (app (fromNormalization f) U) (appLE g U V hVU)) (Y :=
    Γ(normalization (pullback.snd f g), normalizationPullback f g ⁻¹ᵁ W))
    (Iso.hom (pushout.congrHom ⋯ ⋯) ≫ pushoutSection ⋯ hVU ⋯ ⋯ ≫ app (normalizationPullback f g) W)
have algebraizeInst : Algebra.Smooth.{u, u} (↑Γ(S, U) : Type u) (↑Γ(Y, V) : Type u)
Tactic: algebraize [(f.app U).hom, (g.appLE U V hVU).hom, ((pullback.snd f g).app V).hom]
-- 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
this_1 :
  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 ⋯ ⋯)
this : (CommRingCat.Hom.hom (appLE g U V hVU)).Smooth
algInst : Algebra (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u) := (CommRingCat.Hom.hom (app f U)).toAlgebra
algInst_1 : Algebra (↑Γ(S, U) : Type u) (↑Γ(Y, V) : Type u) := (CommRingCat.Hom.hom (appLE g U V hVU)).toAlgebra
algInst_2 : Algebra (↑Γ(Y, V) : Type u) (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (app (pullback.snd f g) V))
algebraizeInst : Algebra.Smooth.{u, u} (↑Γ(S, U) : Type u) (↑Γ(Y, V) : Type u)
⊢ Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) (pullback.fst f g ⁻¹ᵁ f ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
have simp_rw : Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) ((pullback.fst f g ≫ f) ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
Tactic: simp_rw [← 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
this_1 :
  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 ⋯ ⋯)
this : (CommRingCat.Hom.hom (appLE g U V hVU)).Smooth
algInst : Algebra (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u) := (CommRingCat.Hom.hom (app f U)).toAlgebra
algInst_1 : Algebra (↑Γ(S, U) : Type u) (↑Γ(Y, V) : Type u) := (CommRingCat.Hom.hom (appLE g U V hVU)).toAlgebra
algInst_2 : Algebra (↑Γ(Y, V) : Type u) (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (app (pullback.snd f g) V))
algebraizeInst : Algebra.Smooth.{u, u} (↑Γ(S, U) : Type u) (↑Γ(Y, V) : Type u)
simp_rw :
  Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) ((pullback.fst f g ≫ f) ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
⊢ Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) (pullback.fst f g ⁻¹ᵁ f ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
have simp_rw₁ : Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) ((pullback.snd f g ≫ g) ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
Tactic: simp_rw [← 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
this_1 :
  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 ⋯ ⋯)
this : (CommRingCat.Hom.hom (appLE g U V hVU)).Smooth
algInst : Algebra (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u) := (CommRingCat.Hom.hom (app f U)).toAlgebra
algInst_1 : Algebra (↑Γ(S, U) : Type u) (↑Γ(Y, V) : Type u) := (CommRingCat.Hom.hom (appLE g U V hVU)).toAlgebra
algInst_2 : Algebra (↑Γ(Y, V) : Type u) (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (app (pullback.snd f g) V))
algebraizeInst : Algebra.Smooth.{u, u} (↑Γ(S, U) : Type u) (↑Γ(Y, V) : Type u)
simp_rw :
  Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) ((pullback.fst f g ≫ f) ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
simp_rw₁ :
  Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) ((pullback.snd f g ≫ g) ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
⊢ Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) (pullback.fst f g ⁻¹ᵁ f ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
have simp_rw₂ : Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) (pullback.snd f g ⁻¹ᵁ g ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
Tactic: simp_rw [← 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
this_1 :
  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 ⋯ ⋯)
this : (CommRingCat.Hom.hom (appLE g U V hVU)).Smooth
algInst : Algebra (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u) := (CommRingCat.Hom.hom (app f U)).toAlgebra
algInst_1 : Algebra (↑Γ(S, U) : Type u) (↑Γ(Y, V) : Type u) := (CommRingCat.Hom.hom (appLE g U V hVU)).toAlgebra
algInst_2 : Algebra (↑Γ(Y, V) : Type u) (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (app (pullback.snd f g) V))
algebraizeInst : Algebra.Smooth.{u, u} (↑Γ(S, U) : Type u) (↑Γ(Y, V) : Type u)
simp_rw :
  Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) ((pullback.fst f g ≫ f) ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
simp_rw₁ :
  Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) ((pullback.snd f g ≫ g) ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
simp_rw₂ :
  Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) (pullback.snd f g ⁻¹ᵁ g ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
⊢ Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) (pullback.fst f g ⁻¹ᵁ f ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
have simp_rw₃ : Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) (pullback.snd f g ⁻¹ᵁ (g ⁻¹ᵁ U ⊓ V))
Tactic: simp_rw [← 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 (hypothesis)
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
this_1 :
  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 ⋯ ⋯)
this : (CommRingCat.Hom.hom (appLE g U V hVU)).Smooth
algInst : Algebra (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u) := (CommRingCat.Hom.hom (app f U)).toAlgebra
algInst_1 : Algebra (↑Γ(S, U) : Type u) (↑Γ(Y, V) : Type u) := (CommRingCat.Hom.hom (appLE g U V hVU)).toAlgebra
algInst_2 : Algebra (↑Γ(Y, V) : Type u) (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (app (pullback.snd f g) V))
algebraizeInst : Algebra.Smooth.{u, u} (↑Γ(S, U) : Type u) (↑Γ(Y, V) : Type u)
⊢ IsIso (X :=
    pushout (Y := Γ(normalization f, fromNormalization f ⁻¹ᵁ U)) (app (fromNormalization f) U) (appLE g U V hVU)) (Y :=
    Γ(normalization (pullback.snd f g), normalizationPullback f g ⁻¹ᵁ W))
    (Iso.hom (pushout.congrHom ⋯ ⋯) ≫ pushoutSection ⋯ hVU ⋯ ⋯ ≫ app (normalizationPullback f g) W)
have this₁ : IsIso (Y := Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V)) (pushoutSection sorry hVU sorry sorry)
Tactic: have := isIso_pushoutSection_of_isQuasiSeparated_of_flat_right
    (.of_hasPullback f g) hVU le_rfl (UY := pullback.snd f g ⁻¹ᵁ V)
    (by simp_rw [← Scheme.Hom.comp_preimage, pullback.condition, Scheme.Hom.comp_preimage,
      ← Scheme.Hom.preimage_inf, inf_eq_right.mpr hVU]) hU hV (f.isCompact_preimage hU.isCompact)
    (f.isQuasiSeparated_preimage hU.isQuasiSeparated)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : LocallyRingedSpace
h :
  ∀ (x : (↑X.toTopCat : Type u)),
    ∃ (R : CommRingCat.{u}) (f : Spec.toLocallyRingedSpace.obj (op R) ⟶ X),
      Membership.mem (γ := Set (↑(↑X.toPresheafedSpace : TopCat) : Type u))
          (Set.range (ι := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                  TopCat.carrier) f.base) :
              (a : (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u)) →
                (↑(↑X.toPresheafedSpace : TopCat) : Type u)))
          x ∧
        IsOpenImmersion f
x : (↑X.toTopCat : Type u)
⊢ ∃ (U : OpenNhds x) (R : CommRingCat.{u}), Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))
have obtain : ∀ (R : CommRingCat.{u}) (f : Spec.toLocallyRingedSpace.obj (op R) ⟶ X)
  (h₁ :
    Membership.mem (γ := Set (↑(↑X.toPresheafedSpace : TopCat) : Type u))
      (Set.range (ι := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              f.base) :
          (a : (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u)) →
            (↑(↑X.toPresheafedSpace : TopCat) : Type u)))
      x)
  (h₂ : IsOpenImmersion f),
  ∃ (U : OpenNhds x) (R : CommRingCat.{u}), Nonempty.{u + 1} (X.restrict sorry ≅ Spec.toLocallyRingedSpace.obj (op R))
Tactic: obtain ⟨R, f, h₁, h₂⟩ := h x