awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst_2 : IsIntegralHom f₂
H : f = f₁ ≫ f₂
U : (directedCover Y).I₀
rw :
  Spec.map
        (appLE f₂ (↑U : Y.Opens) (f₂ ⁻¹ᵁ (↑U : Y.Opens)) ⋯ ≫
          CommRingCat.ofHom
            ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ toOpens U) ⋯)).codRestrict
              (integralClosure (↑Γ(Y, toOpens U) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u)) ⋯)) ≫
      ⋯.fromSpec =
    (normalizationGlueData f).natTrans.app U ≫ (directedCover Y).f U
⊢ CategoryStruct.comp (Y := colimit (normalizationGlueData f).functor) (colimit.ι (normalizationGlueData f).functor U)
      (colimit.desc (normalizationGlueData f).functor
          { pt := T,
            ι :=
              {
                app := fun (U : Y.AffineZariskiSite) ↦
                  Spec.map
                      (CommRingCat.ofHom
                        ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ U.toOpens) ⋯)).codRestrict
                          (integralClosure (↑Γ(Y, U.toOpens) : Type u) (↑Γ(X, f ⁻¹ᵁ U.toOpens) : Type u)) ⋯)) ≫
                    ⋯.fromSpec,
                naturality := ⋯ :
                NatTrans (normalizationGlueData f).functor (Functor.obj (Functor.const Y.AffineZariskiSite) T) } } ≫
        f₂) =
    CategoryStruct.comp (Y := colimit (normalizationGlueData f).functor)
      (colimit.ι (normalizationGlueData f).functor U :
        (normalizationGlueData f).functor.obj U ⟶ colimit (normalizationGlueData f).functor)
      ((normalizationGlueData f).toBase : (normalizationGlueData f).glued ⟶ Y)

Tactic:
rw [colimit.ι_desc_assoc, (normalizationGlueData f).ι_toBase, Category.assoc,
    ← IsAffineOpen.SpecMap_appLE_fromSpec _ U.2 _ le_rfl, ← Spec.map_comp_assoc]

Premises used: CategoryTheory.Category.assoc, le_rfl, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.ι_toBase, AlgebraicGeometry.Scheme.Hom.normalizationGlueData, AlgebraicGeometry.Spec.map_comp_assoc, CategoryTheory.Limits.colimit.ι_desc_assoc, AlgebraicGeometry.IsAffineOpen.SpecMap_appLE_fromSpec, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst_2 : IsIntegralHom f₂
H : f = f₁ ≫ f₂
U : (directedCover Y).I₀
dsimp :
  Spec.map
        (appLE f₂ (↑U : Y.Opens) (f₂ ⁻¹ᵁ (↑U : Y.Opens)) ⋯ ≫
          CommRingCat.ofHom
            ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ toOpens U) ⋯)).codRestrict
              (integralClosure (↑Γ(Y, toOpens U) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u)) ⋯)) ≫
      ⋯.fromSpec =
    (Spec.map ((normalizationDiagramMap f).app (Opposite.op (toOpens U))) ≫ ⋯.isoSpec.inv) ≫ (↑U : Y.Opens).ι
⊢ Spec.map
        (appLE f₂ (↑U : Y.Opens) (f₂ ⁻¹ᵁ (↑U : Y.Opens)) ⋯ ≫
          CommRingCat.ofHom
            ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ toOpens U) ⋯)).codRestrict
              (integralClosure (↑Γ(Y, toOpens U) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u)) ⋯)) ≫
      ⋯.fromSpec =
    (normalizationGlueData f).natTrans.app U ≫ (directedCover Y).f U

Tactic:
dsimp [normalizationGlueData, relativeGluingData, restrictIsoSpec]

Premises used: AlgebraicGeometry.Scheme.AffineZariskiSite.relativeGluingData, AlgebraicGeometry.Scheme.Hom.normalizationGlueData, AlgebraicGeometry.Scheme.AffineZariskiSite.restrictIsoSpec
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst_2 : IsIntegralHom f₂
H : f = f₁ ≫ f₂
U : (directedCover Y).I₀
rw :
  Spec.map
        (appLE f₂ (↑U : Y.Opens) (f₂ ⁻¹ᵁ (↑U : Y.Opens)) ⋯ ≫
          CommRingCat.ofHom
            ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ toOpens U) ⋯)).codRestrict
              (integralClosure (↑Γ(Y, toOpens U) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u)) ⋯)) ≫
      ⋯.fromSpec =
    Spec.map ((normalizationDiagramMap f).app (Opposite.op (toOpens U))) ≫ ⋯.isoSpec.inv ≫ (↑U : Y.Opens).ι
⊢ Spec.map
        (appLE f₂ (↑U : Y.Opens) (f₂ ⁻¹ᵁ (↑U : Y.Opens)) ⋯ ≫
          CommRingCat.ofHom
            ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ toOpens U) ⋯)).codRestrict
              (integralClosure (↑Γ(Y, toOpens U) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u)) ⋯)) ≫
      ⋯.fromSpec =
    (Spec.map ((normalizationDiagramMap f).app (Opposite.op (toOpens U))) ≫ ⋯.isoSpec.inv) ≫ (↑U : Y.Opens).ι

Tactic:
rw [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst_2 : IsIntegralHom f₂
H : f = f₁ ≫ f₂
U : (directedCover Y).I₀
e_a :
  Eq (α :=
    Γ(Y, (↑U : Y.Opens)) ⟶
      CommRingCat.of ↥(integralClosure (↑Γ(Y, toOpens U) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u)))
    (appLE f₂ (↑U : Y.Opens) (f₂ ⁻¹ᵁ (↑U : Y.Opens)) ⋯ ≫
      CommRingCat.ofHom
        ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ toOpens U) ⋯)).codRestrict
          (integralClosure (↑Γ(Y, toOpens U) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u)) ⋯))
    ((normalizationDiagramMap f).app (Opposite.op (toOpens U)))
⊢ Spec.map
        (appLE f₂ (↑U : Y.Opens) (f₂ ⁻¹ᵁ (↑U : Y.Opens)) ⋯ ≫
          CommRingCat.ofHom
            ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ toOpens U) ⋯)).codRestrict
              (integralClosure (↑Γ(Y, toOpens U) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u)) ⋯)) ≫
      ⋯.fromSpec =
    Spec.map ((normalizationDiagramMap f).app (Opposite.op (toOpens U))) ≫ ⋯.isoSpec.inv ≫ (↑U : Y.Opens).ι

Tactic:
congr 2
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst_2 : IsIntegralHom f₂
H : f = f₁ ≫ f₂
U : (directedCover Y).I₀
e_a :
  ∀ (i : (↑Γ(Y, (↑U : Y.Opens)) : Type u)),
    Eq.{u + 1} (α := (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
      (↑((CommRingCat.Hom.hom
                (appLE f₂ (↑U : Y.Opens) (f₂ ⁻¹ᵁ (↑U : Y.Opens)) ⋯ ≫
                  CommRingCat.ofHom
                    ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ toOpens U) ⋯)).codRestrict
                      (integralClosure (↑Γ(Y, toOpens U) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u)) ⋯)) :
              (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) →
                (↑(CommRingCat.of ↥(integralClosure (↑Γ(Y, toOpens U) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))) :
                  Type u))
            i) :
        (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
      (↑((CommRingCat.Hom.hom ((normalizationDiagramMap f).app (Opposite.op (toOpens U))) :
              (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) →
                (↑(CommRingCat.of ↥(integralClosure (↑Γ(Y, toOpens U) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))) :
                  Type u))
            i) :
        (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
⊢ Eq (α :=
    Γ(Y, (↑U : Y.Opens)) ⟶
      CommRingCat.of ↥(integralClosure (↑Γ(Y, toOpens U) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u)))
    (appLE f₂ (↑U : Y.Opens) (f₂ ⁻¹ᵁ (↑U : Y.Opens)) ⋯ ≫
      CommRingCat.ofHom
        ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ toOpens U) ⋯)).codRestrict
          (integralClosure (↑Γ(Y, toOpens U) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u)) ⋯))
    ((normalizationDiagramMap f).app (Opposite.op (toOpens U)))

Tactic:
ext i
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst_2 : IsIntegralHom f₂
H : f = f₁ ≫ f₂
U : (directedCover Y).I₀
i : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
e_a :
  Eq (α := (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
    ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ toOpens U) ⋯) :
          (a : (↑(T.presheaf.1 (Opposite.op (f₂ ⁻¹ᵁ (↑U : Y.Opens)))) : Type u)) → (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
        ((CommRingCat.Hom.hom (appLE f₂ (↑U : Y.Opens) (f₂ ⁻¹ᵁ (↑U : Y.Opens)) ⋯) :
              (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑(T.presheaf.1 (Opposite.op (f₂ ⁻¹ᵁ (↑U : Y.Opens)))) : Type u))
            i :
          (↑(T.presheaf.1 (Opposite.op (f₂ ⁻¹ᵁ (↑U : Y.Opens)))) : Type u)) :
      (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
    ((CommRingCat.Hom.hom (app f (toOpens U)) :
          (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
        i :
      (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
⊢ Eq.{u + 1} (α := (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
    (↑((CommRingCat.Hom.hom
              (appLE f₂ (↑U : Y.Opens) (f₂ ⁻¹ᵁ (↑U : Y.Opens)) ⋯ ≫
                CommRingCat.ofHom
                  ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ toOpens U) ⋯)).codRestrict
                    (integralClosure (↑Γ(Y, toOpens U) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u)) ⋯)) :
            (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) →
              (↑(CommRingCat.of ↥(integralClosure (↑Γ(Y, toOpens U) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))) :
                Type u))
          i) :
      (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
    (↑((CommRingCat.Hom.hom ((normalizationDiagramMap f).app (Opposite.op (toOpens U))) :
            (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) →
              (↑(CommRingCat.of ↥(integralClosure (↑Γ(Y, toOpens U) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))) :
                Type u))
          i) :
      (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))

Tactic:
dsimp [normalizationDiagram, normalizationDiagramMap, RingHom.algebraMap_toAlgebra]

Premises used: AlgebraicGeometry.Scheme.Hom.normalizationDiagram, RingHom.algebraMap_toAlgebra, AlgebraicGeometry.Scheme.Hom.normalizationDiagramMap
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst_2 : IsIntegralHom f₂
H : f = f₁ ≫ f₂
U : (directedCover Y).I₀
i : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
e_a :
  Eq (α := (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (appLE (f₁ ≫ f₂) (↑U : Y.Opens) (f ⁻¹ᵁ toOpens U) ⋯) :
          (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
        i :
      (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
    ((CommRingCat.Hom.hom (appLE f (toOpens U) (f ⁻¹ᵁ toOpens U) ⋯) :
          (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
        i :
      (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
⊢ Eq (α := (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
    ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ toOpens U) ⋯) :
          (a : (↑(T.presheaf.1 (Opposite.op (f₂ ⁻¹ᵁ (↑U : Y.Opens)))) : Type u)) → (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
        ((CommRingCat.Hom.hom (appLE f₂ (↑U : Y.Opens) (f₂ ⁻¹ᵁ (↑U : Y.Opens)) ⋯) :
              (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑(T.presheaf.1 (Opposite.op (f₂ ⁻¹ᵁ (↑U : Y.Opens)))) : Type u))
            i :
          (↑(T.presheaf.1 (Opposite.op (f₂ ⁻¹ᵁ (↑U : Y.Opens)))) : Type u)) :
      (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
    ((CommRingCat.Hom.hom (app f (toOpens U)) :
          (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
        i :
      (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))

Tactic:
rw [← CommRingCat.comp_apply, Hom.appLE_comp_appLE, app_eq_appLE]

Premises used: AlgebraicGeometry.Scheme.Hom.app_eq_appLE, CommRingCat.comp_apply, AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst_2 : IsIntegralHom f₂
H : f = f₁ ≫ f₂
U : (directedCover Y).I₀
i : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
e_a e_a₁ :
  Eq (α := (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (appLE (f₁ ≫ f₂) (↑U : Y.Opens) (f ⁻¹ᵁ toOpens U) ⋯) :
          (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
        i :
      (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
    ((CommRingCat.Hom.hom (appLE f (toOpens U) (f ⁻¹ᵁ toOpens U) ⋯) :
          (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
        i :
      (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
⊢ Eq (α := (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (appLE (f₁ ≫ f₂) (↑U : Y.Opens) (f ⁻¹ᵁ toOpens U) ⋯) :
          (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
        i :
      (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
    ((CommRingCat.Hom.hom (appLE f (toOpens U) (f ⁻¹ᵁ toOpens U) ⋯) :
          (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))
        i :
      (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u))

Tactic:
simp_rw [H]
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst_2 : IsIntegralHom f₂
H : f = f₁ ≫ f₂
rw : IsIntegralHom (X := normalization f) (fromNormalization f)
⊢ IsIntegralHom (X := normalization f) (normalizationDesc f f₁ f₂ H ≫ f₂)

Tactic:
rw [f.normalizationDesc_comp]

Premises used: AlgebraicGeometry.Scheme.Hom.normalizationDesc_comp
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst_2 : IsIntegralHom f₂
H : f = f₁ ≫ f₂
⊢ IsIntegralHom (X := normalization f) (fromNormalization f)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst_2 : IsIntegralHom f₂
H : f = f₁ ≫ f₂
⊢ IsIntegralHom (X := normalization f) (normalizationDesc f f₁ f₂ H ≫ f₂)

Tactic:
have : IsIntegralHom (f.normalizationDesc f₁ f₂ H ≫ f₂) := by
    rw [f.normalizationDesc_comp]; infer_instance
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst_2 : IsIntegralHom f₂
H : f = f₁ ≫ f₂
this : IsIntegralHom (X := normalization f) (normalizationDesc f f₁ f₂ H ≫ f₂)
⊢ IsIntegralHom (X := normalization f) (normalizationDesc f f₁ f₂ H)

Tactic:
.of_comp _ f₂

Premises used: AlgebraicGeometry.IsIntegralHom.of_comp
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst_2 : IsIntegralHom f₂
H : f = f₁ ≫ f₂
this : IsIntegralHom (X := normalization f) (normalizationDesc f f₁ f₂ H ≫ f₂)
⊢ IsIntegralHom (X := normalization f) (normalizationDesc f f₁ f₂ H)

Tactic:
exact .of_comp _ f₂
-- Module: Mathlib.AlgebraicGeometry.Normalization
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
apply :
  ∀
    (U :
      PreZeroHypercover.I₀ (S := normalization f)
        (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))),
    PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₁ =
      PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₂
⊢ f₁ = f₂

Tactic:
apply f.normalizationOpenCover.hom_ext _ _ fun U ↦ ?_

Premises used: AlgebraicGeometry.Scheme.Cover.hom_ext, AlgebraicGeometry.Scheme.Hom.normalizationOpenCover
-- Module: Mathlib.AlgebraicGeometry.Normalization
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 : Algebra (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (app f (↑U : Y.Opens)))
⊢ IsAffineHom f₁

Tactic:
have : IsAffineHom f₁ := have : IsAffineHom (f₁ ≫ g) := hf₁ ▸ inferInstance; .of_comp _ g
-- Module: Mathlib.AlgebraicGeometry.Normalization
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 : IsAffineHom f₁
⊢ IsAffineHom f₂

Tactic:
have : IsAffineHom f₂ := have : IsAffineHom (f₂ ≫ g) := hf₂ ▸ inferInstance; .of_comp _ g
-- Module: Mathlib.AlgebraicGeometry.Normalization
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₁
⊢ f₀ = toNormalization f ≫ f₂

Tactic:
have hf₀ : f₀ = toNormalization f ≫ f₂ := H₁
-- Module: Mathlib.AlgebraicGeometry.Normalization
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₁ =
    PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₂

Tactic:
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) ?_ ?_ ?_

Premises used: AlgebraicGeometry.Spec, CommRingCat.carrier, Set.Mem, Subtype.val_injective, Subalgebra.val, setOf, CommRingCat.ofHom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgHom.toRingHom, integralClosure, Opposite.op, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, AlgebraicGeometry.eq_of_SpecMap_comp_eq_of_isAffineOpen, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Subtype.val, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace, Subtype.property, AlgebraicGeometry.IsAffineOpen.preimage
-- Module: Mathlib.AlgebraicGeometry.Normalization
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) =
    ⊤
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₂)
⊢ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₁ =
    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) ?_ ?_ ?_

Premises used: CommRingCat.carrier, Subtype.val_injective, Subalgebra.val, CommRingCat.ofHom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgHom.toRingHom, integralClosure, Opposite.op, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, AlgebraicGeometry.eq_of_SpecMap_comp_eq_of_isAffineOpen, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Subtype.val, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace, Subtype.property, AlgebraicGeometry.IsAffineOpen.preimage
-- Module: Mathlib.AlgebraicGeometry.Normalization
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 :
  (Spec.map ((normalizationDiagramMap f).app (Opposite.op (↑U : Y.Opens))) ≫ IsAffineOpen.fromSpec ⋯) ⁻¹ᵁ
      (↑U : Y.Opens) =
    ⊤
⊢ (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₁) ⁻¹ᵁ
      g ⁻¹ᵁ (↑U : Y.Opens) =
    ⊤

Tactic:
simp only [← Scheme.Hom.comp_preimage, Category.assoc, hf₁, ι_fromNormalization]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Hom.comp_preimage, AlgebraicGeometry.Scheme.Hom.ι_fromNormalization