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
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₂
refine_1 :
  (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₁) ⁻¹ᵁ
      g ⁻¹ᵁ (↑U : Y.Opens) =
    ⊤
refine_2 :
  (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₂) ⁻¹ᵁ
      g ⁻¹ᵁ (↑U : Y.Opens) =
    ⊤
⊢ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₁ =
    PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₂
have refine_3 : Eq (α := Spec (CommRingCat.of (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) ⟶ T)
  (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₁)
  (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₂)
Tactic: refine eq_of_SpecMap_comp_eq_of_isAffineOpen
    (CommRingCat.ofHom (integralClosure Γ(Y, U.1) Γ(X, f ⁻¹ᵁ U.1)).val.toRingHom)
    Subtype.val_injective _ (U.2.preimage g) ?_ ?_ ?_
-- 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₂
⊢ (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₁) ⁻¹ᵁ
      g ⁻¹ᵁ (↑U : Y.Opens) =
    ⊤
have refine_1 : (Spec.map ((normalizationDiagramMap f).app (Opposite.op (↑U : Y.Opens))) ≫ IsAffineOpen.fromSpec sorry) ⁻¹ᵁ (↑U : Y.Opens) =
  ⊤
Tactic: simp only [← Scheme.Hom.comp_preimage, Category.assoc, hf₁, ι_fromNormalization]
-- 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₂
⊢ (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₂) ⁻¹ᵁ
      g ⁻¹ᵁ (↑U : Y.Opens) =
    ⊤
have refine_2 : (Spec.map ((normalizationDiagramMap f).app (Opposite.op (↑U : Y.Opens))) ≫ IsAffineOpen.fromSpec sorry) ⁻¹ᵁ (↑U : Y.Opens) =
  ⊤
Tactic: simp only [← Scheme.Hom.comp_preimage, Category.assoc, hf₂, ι_fromNormalization]
-- 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₂
⊢ f ⁻¹ᵁ (↑U : Y.Opens) ≤ f₀ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
have simp : f ⁻¹ᵁ (↑U : Y.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)
Tactic: simp only [← Scheme.Hom.comp_preimage, f₀, Category.assoc,
        hf₁, toNormalization_fromNormalization]
-- 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₂
⊢ Eq (α := Spec (CommRingCat.of (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) ⟶ T)
    (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₁)
    (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 h₁ : f ⁻¹ᵁ (↑U : Y.Opens) ≤ f₀ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
Tactic: have h₁ : f ⁻¹ᵁ U.1 ≤ f₀ ⁻¹ᵁ g ⁻¹ᵁ U.1 := by
      simp only [← Scheme.Hom.comp_preimage, f₀, Category.assoc,
        hf₁, toNormalization_fromNormalization]; rfl
-- 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)
⊢ Eq (α := Spec (CommRingCat.of (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) ⟶ T)
    (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₁)
    (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 h₁' : f ⁻¹ᵁ (↑U : Y.Opens) = toNormalization f ⁻¹ᵁ f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
Tactic: have h₁' : f ⁻¹ᵁ U.1 = toNormalization f ⁻¹ᵁ f₂ ⁻¹ᵁ g ⁻¹ᵁ U.1 := by
      simp only [← Scheme.Hom.comp_preimage, hf₂, toNormalization_fromNormalization]
-- 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)
⊢ Eq (α := Spec (CommRingCat.of (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) ⟶ T)
    (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₁)
    (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 h₂ : fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) = f₁ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
Tactic: have h₂ : fromNormalization f ⁻¹ᵁ U.1 = f₁ ⁻¹ᵁ g ⁻¹ᵁ U.1 := by
      simp only [← Scheme.Hom.comp_preimage, hf₁]
-- 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)
⊢ Eq (α := Spec (CommRingCat.of (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) ⟶ T)
    (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₁)
    (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 h₂' : fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) = f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
Tactic: have h₂' : fromNormalization f ⁻¹ᵁ U.1 = f₂ ⁻¹ᵁ g ⁻¹ᵁ U.1 := by
      simp only [← Scheme.Hom.comp_preimage, hf₂]
-- 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)
⊢ Eq (α := Spec (CommRingCat.of (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) ⟶ T)
    (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₁)
    (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 h₃ : f ⁻¹ᵁ (↑U : Y.Opens) = toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)
Tactic: have h₃ : f ⁻¹ᵁ U.1 = toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ U.1 := by
      simp [← Scheme.Hom.comp_preimage]
-- 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)
⊢ Eq (α := Spec (CommRingCat.of (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) ⟶ T)
    (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₁)
    (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 trans : 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₁ =
  Spec.map (appLE f₀ (g ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ (↑U : Y.Opens)) h₁) ≫ sorry.fromSpec
Tactic: trans Spec.map (f₀.appLE (g ⁻¹ᵁ U.val) (f ⁻¹ᵁ U.val) h₁) ≫ (U.prop.preimage g).fromSpec
-- 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)
trans :
  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₁ =
    Spec.map (appLE f₀ (g ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ (↑U : Y.Opens)) h₁) ≫ ⋯.fromSpec
⊢ Eq (α := Spec (CommRingCat.of (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) ⟶ T)
    (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₁)
    (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 trans₁ : Spec.map (appLE f₀ (g ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ (↑U : Y.Opens)) h₁) ≫ sorry.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₂
Tactic: trans Spec.map (f₀.appLE (g ⁻¹ᵁ U.val) (f ⁻¹ᵁ U.val) h₁) ≫ (U.prop.preimage g).fromSpec
-- 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
        (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₁ =
    Spec.map (appLE f₀ (g ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ (↑U : Y.Opens)) h₁) ≫ ⋯.fromSpec
have simp : 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₁) ≫
    Spec.map (app f₁ (g ⁻¹ᵁ (↑U : Y.Opens))) ≫ sorry.fromSpec
Tactic: simp only [AlgHom.toRingHom_eq_coe, comp_appLE, Spec.map_comp, Category.assoc, f₀]
-- 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
        (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₁) ≫
      Spec.map (app f₁ (g ⁻¹ᵁ (↑U : Y.Opens))) ≫ ⋯.fromSpec
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 (appLE (toNormalization f) (f₁ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ (↑U : Y.Opens)) h₁) ≫ sorry.fromSpec ≫ f₁
Tactic: rw [app_eq_appLE, IsAffineOpen.SpecMap_appLE_fromSpec _ _ ((U.2.preimage _).preimage _)]