awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : QuasiCompact f
inst_2 : QuasiSeparated f
U : Y.AffineZariskiSite
r : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
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 : Algebra (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (app f (↑(U.basicOpen r) : Y.Opens)))
this_3 : Algebra ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
  ↥(integralClosure (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)) :=
  (CommRingCat.Hom.hom ((normalizationDiagram f).map (homOfLE ⋯).op)).toAlgebra
inst : Algebra (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
this_4 : IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u)
this_5 :
  IsLocalization.Away (R := (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    ((algebraMap (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) :
          (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
        r :
      (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)
this_6 : Algebra (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u) :=
  (CommRingCat.Hom.hom (appLE f (↑U : Y.Opens) (f ⁻¹ᵁ Y.basicOpen r) ⋯)).toAlgebra
this_7 :
  IsScalarTower.{u, u, u} (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)
    (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)
this_8 :
  IsScalarTower.{u, u, u} (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, Y.basicOpen r) : Type u)
    (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)
this :
  IsScalarTower.{u, u, u} ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    ↥(integralClosure (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u))
    (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)
⊢ IsScalarTower.{u, u, u} (↑Γ(Y, (↑U : Y.Opens)) : Type u)
    ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    ↥(integralClosure (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u))

Tactic:
have : IsScalarTower Γ(Y, U.1) (integralClosure Γ(Y, U.1) Γ(X, f ⁻¹ᵁ U.1))
    (integralClosure Γ(Y, Y.basicOpen r) Γ(X, f ⁻¹ᵁ Y.basicOpen r)) := .of_algebraMap_eq' rfl
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : QuasiCompact f
inst_2 : QuasiSeparated f
U : Y.AffineZariskiSite
r : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
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 : Algebra (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (app f (↑(U.basicOpen r) : Y.Opens)))
this_3 : Algebra ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
  ↥(integralClosure (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)) :=
  (CommRingCat.Hom.hom ((normalizationDiagram f).map (homOfLE ⋯).op)).toAlgebra
inst : Algebra (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
this_4 : IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u)
this_5 :
  IsLocalization.Away (R := (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    ((algebraMap (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) :
          (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
        r :
      (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)
this_6 : Algebra (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u) :=
  (CommRingCat.Hom.hom (appLE f (↑U : Y.Opens) (f ⁻¹ᵁ Y.basicOpen r) ⋯)).toAlgebra
this_7 :
  IsScalarTower.{u, u, u} (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)
    (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)
this_8 :
  IsScalarTower.{u, u, u} (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, Y.basicOpen r) : Type u)
    (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)
this_9 :
  IsScalarTower.{u, u, u} ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    ↥(integralClosure (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u))
    (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)
this :
  IsScalarTower.{u, u, u} (↑Γ(Y, (↑U : Y.Opens)) : Type u)
    ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    ↥(integralClosure (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u))
⊢ IsLocalization.Away (R := ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))
    ((algebraMap (↑Γ(Y, (↑U : Y.Opens)) : Type u)
            ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) :
          (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) →
            ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))
        r :
      ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))
    ↥(integralClosure (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u))

Tactic:
IsLocalization.Away.integralClosure r

Premises used: IsLocalization.Away.integralClosure
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : QuasiCompact f
inst_2 : QuasiSeparated f
U : Y.AffineZariskiSite
r : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
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 : Algebra (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (app f (↑(U.basicOpen r) : Y.Opens)))
this_3 : Algebra ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
  ↥(integralClosure (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)) :=
  (CommRingCat.Hom.hom ((normalizationDiagram f).map (homOfLE ⋯).op)).toAlgebra
inst : Algebra (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
this_4 : IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u)
this_5 :
  IsLocalization.Away (R := (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    ((algebraMap (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) :
          (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
        r :
      (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)
this_6 : Algebra (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u) :=
  (CommRingCat.Hom.hom (appLE f (↑U : Y.Opens) (f ⁻¹ᵁ Y.basicOpen r) ⋯)).toAlgebra
this_7 :
  IsScalarTower.{u, u, u} (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)
    (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)
this_8 :
  IsScalarTower.{u, u, u} (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, Y.basicOpen r) : Type u)
    (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)
this_9 :
  IsScalarTower.{u, u, u} ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    ↥(integralClosure (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u))
    (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)
this :
  IsScalarTower.{u, u, u} (↑Γ(Y, (↑U : Y.Opens)) : Type u)
    ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    ↥(integralClosure (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u))
⊢ IsLocalization.Away (R := ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))
    ((algebraMap (↑Γ(Y, (↑U : Y.Opens)) : Type u)
            ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) :
          (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) →
            ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))
        r :
      ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))
    ↥(integralClosure (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u))

Tactic:
exact IsLocalization.Away.integralClosure r

Premises used: IsLocalization.Away.integralClosure
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
⊢ ((normalizationGlueData f).functor ⋙ forget).IsLocallyDirected

Tactic:
Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin ..

Premises used: AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U V : Y.AffineZariskiSite
i : U ⟶ V
rw :
  (Iso.inv (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫
        Cover.trans (P := IsOpenImmersion) (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)) i ≫
          Iso.hom (pullbackRestrictIsoRestrict f (↑V : Y.Opens))) ≫
      (f ⁻¹ᵁ (↑V : Y.Opens)).ι =
    X.homOfLE ⋯ ≫ (f ⁻¹ᵁ (↑V : Y.Opens)).ι
⊢ Iso.inv (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫
      Cover.trans (P := IsOpenImmersion) (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)) i ≫
        Iso.hom (pullbackRestrictIsoRestrict f (↑V : Y.Opens)) =
    X.homOfLE ⋯

Tactic:
rw [← cancel_mono (Scheme.Opens.ι _)]

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U V : Y.AffineZariskiSite
i : U ⟶ V
⊢ (Iso.inv (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫
        Cover.trans (P := IsOpenImmersion) (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)) i ≫
          Iso.hom (pullbackRestrictIsoRestrict f (↑V : Y.Opens))) ≫
      (f ⁻¹ᵁ (↑V : Y.Opens)).ι =
    X.homOfLE ⋯ ≫ (f ⁻¹ᵁ (↑V : Y.Opens)).ι

Tactic:
simp +instances [Cover.trans, Cover.locallyDirectedPullbackCover]

Premises used: AlgebraicGeometry.Scheme.Cover.locallyDirectedPullbackCover, AlgebraicGeometry.Scheme.Cover.trans
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U V : Y.AffineZariskiSite
i : U ⟶ V
⊢ Iso.inv (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫
      Cover.trans (P := IsOpenImmersion) (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)) i ≫
        Iso.hom (pullbackRestrictIsoRestrict f (↑V : Y.Opens)) =
    X.homOfLE ⋯

Tactic:
have : (pullbackRestrictIsoRestrict f U.1).inv ≫
      Cover.trans ((directedCover Y).pullback₁ f) i ≫
      (pullbackRestrictIsoRestrict f V.1).hom = X.homOfLE
        (f.preimage_mono (toOpens_mono i.1.1)) := by
    rw [← cancel_mono (Scheme.Opens.ι _)]
    simp +instances [Cover.trans, Cover.locallyDirectedPullbackCover]
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U V : Y.AffineZariskiSite
i : U ⟶ V
this :
  Iso.inv (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫
      Cover.trans (P := IsOpenImmersion) (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)) i ≫
        Iso.hom (pullbackRestrictIsoRestrict f (↑V : Y.Opens)) =
    X.homOfLE ⋯
rw :
  Eq (α := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ⟶ normalization f)
    ((f ⁻¹ᵁ U.toOpens).toSpecΓ ≫
      Spec.map
          (CommRingCat.ofHom
              (↑(Subalgebra.val
                    (integralClosure (↑Γ(Y, (↑V : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u))) :
                ↥(integralClosure (↑Γ(Y, (↑V : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u)) →+*
                  (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u)) ≫
            X.presheaf.map (homOfLE ⋯).op) ≫
        colimit.ι (normalizationGlueData f).functor V)
    ((f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫
      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))) ≫
        (normalizationGlueData f).functor.map i ≫ colimit.ι (normalizationGlueData f).functor V)
⊢ Eq (α := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ⟶ normalization f)
    ((f ⁻¹ᵁ U.toOpens).toSpecΓ ≫
      Spec.map
          (CommRingCat.ofHom
              (↑(Subalgebra.val
                    (integralClosure (↑Γ(Y, (↑V : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u))) :
                ↥(integralClosure (↑Γ(Y, (↑V : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u)) →+*
                  (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u)) ≫
            X.presheaf.map (homOfLE ⋯).op) ≫
        colimit.ι (normalizationGlueData f).functor V)
    ((f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫
      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))) ≫
        colimit.ι (normalizationGlueData f).functor U)

Tactic:
rw [← colimit.w f.normalizationGlueData.functor i]

Premises used: AlgebraicGeometry.Scheme.Hom.normalizationGlueData, CategoryTheory.Limits.colimit.w, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.functor
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U V : Y.AffineZariskiSite
i : U ⟶ V
this :
  Iso.inv (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫
      Cover.trans (P := IsOpenImmersion) (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)) i ≫
        Iso.hom (pullbackRestrictIsoRestrict f (↑V : Y.Opens)) =
    X.homOfLE ⋯
dsimp :
  Eq (α := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ⟶ normalization f)
    ((f ⁻¹ᵁ U.toOpens).toSpecΓ ≫
      Spec.map
          (CommRingCat.ofHom
              (↑(Subalgebra.val
                    (integralClosure (↑Γ(Y, (↑V : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u))) :
                ↥(integralClosure (↑Γ(Y, (↑V : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u)) →+*
                  (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u)) ≫
            X.presheaf.map (homOfLE ⋯).op) ≫
        colimit.ι (((toOpensFunctor Y).op ⋙ normalizationDiagram f).rightOp ⋙ Scheme.Spec) V)
    ((f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫
      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))) ≫
        Spec.map ((normalizationDiagram f).map ((toOpensFunctor Y).map i).op) ≫
          colimit.ι (((toOpensFunctor Y).op ⋙ normalizationDiagram f).rightOp ⋙ Scheme.Spec) V)
⊢ Eq (α := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ⟶ normalization f)
    ((f ⁻¹ᵁ U.toOpens).toSpecΓ ≫
      Spec.map
          (CommRingCat.ofHom
              (↑(Subalgebra.val
                    (integralClosure (↑Γ(Y, (↑V : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u))) :
                ↥(integralClosure (↑Γ(Y, (↑V : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u)) →+*
                  (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u)) ≫
            X.presheaf.map (homOfLE ⋯).op) ≫
        colimit.ι (normalizationGlueData f).functor V)
    ((f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫
      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))) ≫
        (normalizationGlueData f).functor.map i ≫ colimit.ι (normalizationGlueData f).functor V)

Tactic:
dsimp [normalizationGlueData, relativeGluingData]

Premises used: AlgebraicGeometry.Scheme.AffineZariskiSite.relativeGluingData, AlgebraicGeometry.Scheme.Hom.normalizationGlueData
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U V : Y.AffineZariskiSite
i : U ⟶ V
this :
  Iso.inv (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫
      Cover.trans (P := IsOpenImmersion) (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)) i ≫
        Iso.hom (pullbackRestrictIsoRestrict f (↑V : Y.Opens)) =
    X.homOfLE ⋯
rw :
  Eq (α := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ⟶ normalization f)
    ((f ⁻¹ᵁ U.toOpens).toSpecΓ ≫
      Spec.map
          (CommRingCat.ofHom
              (↑(Subalgebra.val
                    (integralClosure (↑Γ(Y, (↑V : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u))) :
                ↥(integralClosure (↑Γ(Y, (↑V : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u)) →+*
                  (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u)) ≫
            X.presheaf.map (homOfLE ⋯).op) ≫
        colimit.ι (((toOpensFunctor Y).op ⋙ normalizationDiagram f).rightOp ⋙ Scheme.Spec) V)
    ((f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫
      Spec.map
          ((normalizationDiagram f).map ((toOpensFunctor Y).map i).op ≫
            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))) ≫
        colimit.ι (((toOpensFunctor Y).op ⋙ normalizationDiagram f).rightOp ⋙ Scheme.Spec) V)
⊢ Eq (α := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ⟶ normalization f)
    ((f ⁻¹ᵁ U.toOpens).toSpecΓ ≫
      Spec.map
          (CommRingCat.ofHom
              (↑(Subalgebra.val
                    (integralClosure (↑Γ(Y, (↑V : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u))) :
                ↥(integralClosure (↑Γ(Y, (↑V : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u)) →+*
                  (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u)) ≫
            X.presheaf.map (homOfLE ⋯).op) ≫
        colimit.ι (((toOpensFunctor Y).op ⋙ normalizationDiagram f).rightOp ⋙ Scheme.Spec) V)
    ((f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫
      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))) ≫
        Spec.map ((normalizationDiagram f).map ((toOpensFunctor Y).map i).op) ≫
          colimit.ι (((toOpensFunctor Y).op ⋙ normalizationDiagram f).rightOp ⋙ Scheme.Spec) V)

Tactic:
rw [← Spec.map_comp_assoc]

Premises used: AlgebraicGeometry.Spec.map_comp_assoc
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U V : Y.AffineZariskiSite
i : U ⟶ V
this :
  Iso.inv (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫
      Cover.trans (P := IsOpenImmersion) (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)) i ≫
        Iso.hom (pullbackRestrictIsoRestrict f (↑V : Y.Opens)) =
    X.homOfLE ⋯
⊢ Eq (α := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ⟶ normalization f)
    ((f ⁻¹ᵁ U.toOpens).toSpecΓ ≫
      Spec.map
          (CommRingCat.ofHom
              (↑(Subalgebra.val
                    (integralClosure (↑Γ(Y, (↑V : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u))) :
                ↥(integralClosure (↑Γ(Y, (↑V : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u)) →+*
                  (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u)) ≫
            X.presheaf.map (homOfLE ⋯).op) ≫
        colimit.ι (((toOpensFunctor Y).op ⋙ normalizationDiagram f).rightOp ⋙ Scheme.Spec) V)
    ((f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫
      Spec.map
          ((normalizationDiagram f).map ((toOpensFunctor Y).map i).op ≫
            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))) ≫
        colimit.ι (((toOpensFunctor Y).op ⋙ normalizationDiagram f).rightOp ⋙ Scheme.Spec) V)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : Type u)
rw :
  Eq (α := pullback f (↑U : Y.Opens).ι ⟶ normalization f)
    ((Iso.hom (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫ (f ⁻¹ᵁ (↑U : Y.Opens)).ι) ≫ toNormalization f)
    (Iso.hom (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫
      (f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫
        CategoryStruct.comp (Y :=
          Spec
            (CommRingCat.of ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))
          (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))
⊢ Eq (α := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ⟶ normalization f) ((f ⁻¹ᵁ (↑U : Y.Opens)).ι ≫ toNormalization f)
    ((f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫
      CategoryStruct.comp (Y :=
        Spec
          (CommRingCat.of ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))
        (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))

Tactic:
rw [← cancel_epi (pullbackRestrictIsoRestrict f U.1).hom, ← Category.assoc]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.pullbackRestrictIsoRestrict, Subtype.val, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom