awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst_2 : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U :
  PreZeroHypercover.I₀ (S := normalization f)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
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_2 : IsAffineHom f₁
this : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
h₁ : f ⁻¹ᵁ (↑U : Y.Opens) ≤ f₀ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₁' : f ⁻¹ᵁ (↑U : Y.Opens) = toNormalization f ⁻¹ᵁ f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₂ : fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) = f₁ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₂' : fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) = f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₃ : f ⁻¹ᵁ (↑U : Y.Opens) = toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)
⊢ Spec.map
        (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))) ≫
      PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₁ =
    Spec.map (appLE (toNormalization f) (f₁ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ (↑U : Y.Opens)) h₁) ≫ ⋯.fromSpec ≫ f₁
have this₁ : appLE (toNormalization f) (f₁ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ (↑U : Y.Opens)) h₁ =
  (normalization f).presheaf.map (Quiver.Hom.op (eqToHom h₂)) ≫
    app (toNormalization f) (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom h₃))
Tactic: have : (toNormalization f).appLE (f₁ ⁻¹ᵁ g ⁻¹ᵁ U.val) (f ⁻¹ᵁ U.val) h₁ =
        f.normalization.presheaf.map (eqToHom h₂).op ≫
        (toNormalization f).app (f.fromNormalization ⁻¹ᵁ U.val) ≫
          X.presheaf.map (eqToHom h₃).op := by
        simp [app_eq_appLE]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst_2 : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U :
  PreZeroHypercover.I₀ (S := normalization f)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
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_2 : IsAffineHom f₁
this_3 : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
h₁ : f ⁻¹ᵁ (↑U : Y.Opens) ≤ f₀ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₁' : f ⁻¹ᵁ (↑U : Y.Opens) = toNormalization f ⁻¹ᵁ f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₂ : fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) = f₁ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₂' : fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) = f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₃ : f ⁻¹ᵁ (↑U : Y.Opens) = toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)
this :
  appLE (toNormalization f) (f₁ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ (↑U : Y.Opens)) h₁ =
    (normalization f).presheaf.map (Quiver.Hom.op (eqToHom h₂)) ≫
      app (toNormalization f) (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom h₃))
⊢ Spec.map
        (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))) ≫
      PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₁ =
    Spec.map (appLE (toNormalization f) (f₁ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ (↑U : Y.Opens)) h₁) ≫ ⋯.fromSpec ≫ f₁
have rw : Spec.map
      (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))) ≫
    PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₁ =
  Spec.map
      ((normalization f).presheaf.map (Quiver.Hom.op (eqToHom h₂)) ≫
        (Iso.hom (normalizationObjIso f sorry) ≫
            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)) ≫
              X.presheaf.map (Quiver.Hom.op (eqToHom sorry))) ≫
          X.presheaf.map (Quiver.Hom.op (eqToHom h₃))) ≫
    sorry.fromSpec ≫ f₁
Tactic: rw [this, f.toNormalization_app_preimage U]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst_2 : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U :
  PreZeroHypercover.I₀ (S := normalization f)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
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_2 : IsAffineHom f₁
this : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
h₁ : f ⁻¹ᵁ (↑U : Y.Opens) ≤ f₀ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₁' : f ⁻¹ᵁ (↑U : Y.Opens) = toNormalization f ⁻¹ᵁ f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₂ : fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) = f₁ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₂' : fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) = f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₃ : f ⁻¹ᵁ (↑U : Y.Opens) = toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)
⊢ Spec.map (appLE f₀ (g ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ (↑U : Y.Opens)) h₁) ≫ ⋯.fromSpec =
    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 ≫ f₂
have simp : Spec.map (appLE (toNormalization f) (f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ (↑U : Y.Opens)) sorry) ≫
    Spec.map (appLE f₂ (g ⁻¹ᵁ (↑U : Y.Opens)) (f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)) sorry) ≫ sorry.fromSpec =
  Spec.map
      (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))) ≫
    PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₂
Tactic: simp only [AlgHom.toRingHom_eq_coe, hf₀, comp_appLE, Spec.map_comp, Category.assoc,
        app_eq_appLE]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst_2 : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U :
  PreZeroHypercover.I₀ (S := normalization f)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
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_2 : IsAffineHom f₁
this : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
h₁ : f ⁻¹ᵁ (↑U : Y.Opens) ≤ f₀ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₁' : f ⁻¹ᵁ (↑U : Y.Opens) = toNormalization f ⁻¹ᵁ f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₂ : fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) = f₁ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₂' : fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) = f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₃ : f ⁻¹ᵁ (↑U : Y.Opens) = toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)
⊢ Spec.map (appLE (toNormalization f) (f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ (↑U : Y.Opens)) ⋯) ≫
      Spec.map (appLE f₂ (g ⁻¹ᵁ (↑U : Y.Opens)) (f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)) ⋯) ≫ ⋯.fromSpec =
    Spec.map
        (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))) ≫
      PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₂
have rw : Spec.map (appLE (toNormalization f) (f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ (↑U : Y.Opens)) sorry) ≫ sorry.fromSpec ≫ f₂ =
  Spec.map
      (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))) ≫
    PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₂
Tactic: rw [IsAffineOpen.SpecMap_appLE_fromSpec _ _ ((U.2.preimage _).preimage _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst_2 : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U :
  PreZeroHypercover.I₀ (S := normalization f)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
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_2 : IsAffineHom f₁
this : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
h₁ : f ⁻¹ᵁ (↑U : Y.Opens) ≤ f₀ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₁' : f ⁻¹ᵁ (↑U : Y.Opens) = toNormalization f ⁻¹ᵁ f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₂ : fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) = f₁ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₂' : fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) = f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₃ : f ⁻¹ᵁ (↑U : Y.Opens) = toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)
⊢ Spec.map (appLE (toNormalization f) (f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ (↑U : Y.Opens)) ⋯) ≫ ⋯.fromSpec ≫ f₂ =
    Spec.map
        (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))) ≫
      PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₂
have this₁ : appLE (toNormalization f) (f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ (↑U : Y.Opens)) sorry =
  (normalization f).presheaf.map (Quiver.Hom.op (eqToHom h₂')) ≫
    app (toNormalization f) (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom h₃))
Tactic: have : (toNormalization f).appLE (f₂ ⁻¹ᵁ g ⁻¹ᵁ U.1) (f ⁻¹ᵁ U.1) h₁'.le =
        f.normalization.presheaf.map (eqToHom h₂').op ≫
        (toNormalization f).app (f.fromNormalization ⁻¹ᵁ U.1) ≫
          X.presheaf.map (eqToHom h₃).op := by
        simp [app_eq_appLE]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst_2 : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U :
  PreZeroHypercover.I₀ (S := normalization f)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
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_2 : IsAffineHom f₁
this_3 : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
h₁ : f ⁻¹ᵁ (↑U : Y.Opens) ≤ f₀ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₁' : f ⁻¹ᵁ (↑U : Y.Opens) = toNormalization f ⁻¹ᵁ f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₂ : fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) = f₁ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₂' : fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) = f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₃ : f ⁻¹ᵁ (↑U : Y.Opens) = toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)
this :
  appLE (toNormalization f) (f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ (↑U : Y.Opens)) ⋯ =
    (normalization f).presheaf.map (Quiver.Hom.op (eqToHom h₂')) ≫
      app (toNormalization f) (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom h₃))
⊢ Spec.map (appLE (toNormalization f) (f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ (↑U : Y.Opens)) ⋯) ≫ ⋯.fromSpec ≫ f₂ =
    Spec.map
        (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))) ≫
      PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₂
have rw : Spec.map
      ((normalization f).presheaf.map (Quiver.Hom.op (eqToHom h₂')) ≫
        (Iso.hom (normalizationObjIso f sorry) ≫
            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)) ≫
              X.presheaf.map (Quiver.Hom.op (eqToHom sorry))) ≫
          X.presheaf.map (Quiver.Hom.op (eqToHom h₃))) ≫
    sorry.fromSpec ≫ f₂ =
  Spec.map
      (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))) ≫
    PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₂
Tactic: rw [this, f.toNormalization_app_preimage 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 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
⊢ f =
    CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ 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)))
have simp : Eq (α := Cocone.pt (F := pair U V) (colimit.cocone (pair U V)) ⟶ Y)
  (Iso.inv (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))) ≫ f)
  (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
    (coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f)))
    (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))))
Tactic: simp only [← Iso.inv_comp_eq, Category.assoc]
-- 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)) ⟶ Y)
    (Iso.inv (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))) ≫ f)
    (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
      (coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f)))
      (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))))
have h₁ : CategoryStruct.comp (Y := U ⨿ V) coprod.inl (Iso.inv (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))) ≫ f) =
  CategoryStruct.comp (Y := U ⨿ V) coprod.inl
    (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
      (coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f)))
      (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))))
Tactic: apply coprod.hom_ext
-- 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
h₁ :
  CategoryStruct.comp (Y := U ⨿ V) coprod.inl
      (Iso.inv (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))) ≫ f) =
    CategoryStruct.comp (Y := U ⨿ V) coprod.inl
      (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
        (coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f)))
        (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))))
⊢ Eq (α := Cocone.pt (F := pair U V) (colimit.cocone (pair U V)) ⟶ Y)
    (Iso.inv (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))) ≫ f)
    (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
      (coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f)))
      (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))))
have h₂ : CategoryStruct.comp (Y := U ⨿ V) coprod.inr (Iso.inv (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))) ≫ f) =
  CategoryStruct.comp (Y := U ⨿ V) coprod.inr
    (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
      (coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f)))
      (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))))
Tactic: apply coprod.hom_ext
-- 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 (α := normalization (iU ≫ f) ⨿ normalization (iV ≫ f) ⟶ normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
    (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))) ⋯) :
      normalization (iU ≫ f) ⨿ normalization (iV ≫ f) ⟶ normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
    (𝟙 (normalization (iU ≫ f) ⨿ normalization (iV ≫ f)) :
      normalization (iU ≫ f) ⨿ normalization (iV ≫ f) ⟶ normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
have h₁ : 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)) =
  coprod.inl ≫ 𝟙 (normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
Tactic: ext
-- 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
h₁ :
  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))
⊢ Eq (α := normalization (iU ≫ f) ⨿ normalization (iV ≫ f) ⟶ normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
    (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))) ⋯) :
      normalization (iU ≫ f) ⨿ normalization (iV ≫ f) ⟶ normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
    (𝟙 (normalization (iU ≫ f) ⨿ normalization (iV ≫ f)) :
      normalization (iU ≫ f) ⨿ normalization (iV ≫ f) ⟶ normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
have h₂ : 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)) =
  coprod.inr ≫ 𝟙 (normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
Tactic: ext