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
refine :
  ∀ (U : Y.AffineZariskiSite) (r : (↑Γ(Y, (↑U : Y.Opens)) : Type u)),
    IsLocalization.Away (R := (↑(((toOpensFunctor Y).op ⋙ normalizationDiagram f).obj (Opposite.op U)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := ((toOpensFunctor Y).op ⋙ Y.presheaf).obj (Opposite.op U))
              (((toOpensFunctor Y).op.whiskerLeft (normalizationDiagramMap f)).app (Opposite.op U)) :
            (a : (↑(((toOpensFunctor Y).op ⋙ Y.presheaf).obj (Opposite.op U)) : Type u)) →
              (↑(((toOpensFunctor Y).op ⋙ normalizationDiagram f).obj (Opposite.op U)) : Type u))
          r :
        (↑(((toOpensFunctor Y).op ⋙ normalizationDiagram f).obj (Opposite.op U)) : Type u))
      (↑(((toOpensFunctor Y).op ⋙ normalizationDiagram f).obj (Opposite.op (U.basicOpen r))) : Type u)
⊢ NatTrans.Coequifibered ((toOpensFunctor Y).op.whiskerLeft (normalizationDiagramMap f))

Tactic:
refine coequifibered_iff_forall_isLocalizationAway.mpr fun U r ↦ ?_

Premises used: Iff.mpr, AlgebraicGeometry.Scheme.AffineZariskiSite.coequifibered_iff_forall_isLocalizationAway
-- 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 : 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
⊢ IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u)

Tactic:
have : IsLocalization.Away r Γ(Y, Y.basicOpen r) :=
    U.2.isLocalization_basicOpen _
-- 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 : Algebra (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)
  (↑Γ(X,
        X.basicOpen (U := f ⁻¹ᵁ (↑U : Y.Opens))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(Y, (↑U : Y.Opens))) (app f (↑U : Y.Opens)) :
              (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
            r)) :
    Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))))
dsimp :
  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)
⊢ 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)

Tactic:
dsimp +instances [inst]
-- 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 : Algebra (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)
  (↑Γ(X,
        X.basicOpen (U := f ⁻¹ᵁ (↑U : Y.Opens))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(Y, (↑U : Y.Opens))) (app f (↑U : Y.Opens)) :
              (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
            r)) :
    Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))))
rw! :
  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,
          X.basicOpen (U := f ⁻¹ᵁ (↑U : Y.Opens))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (X := Γ(Y, (↑U : Y.Opens))) (app f (↑U : Y.Opens)) :
                (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
              r)) :
      Type u)
⊢ 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)

Tactic:
rw! (castMode := .all) [f.preimage_basicOpen r]

Premises used: AlgebraicGeometry.Scheme.Hom.preimage_basicOpen
-- 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 : Algebra (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)
  (↑Γ(X,
        X.basicOpen (U := f ⁻¹ᵁ (↑U : Y.Opens))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(Y, (↑U : Y.Opens))) (app f (↑U : Y.Opens)) :
              (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
            r)) :
    Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))))
⊢ 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,
          X.basicOpen (U := f ⁻¹ᵁ (↑U : Y.Opens))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (X := Γ(Y, (↑U : Y.Opens))) (app f (↑U : Y.Opens)) :
                (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
              r)) :
      Type u)

Tactic:
isLocalization_basicOpen_of_qcqs (f.isCompact_preimage U.2.isCompact)
        (f.isQuasiSeparated_preimage U.2.isQuasiSeparated) (f.app _ r)

Premises used: AlgebraicGeometry.IsAffineOpen.isCompact, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.Hom.app, AlgebraicGeometry.Scheme.Hom.isCompact_preimage, AlgebraicGeometry.IsAffineOpen.isQuasiSeparated, DFunLike.coe, AlgebraicGeometry.isLocalization_basicOpen_of_qcqs, AlgebraicGeometry.Scheme.Hom.isQuasiSeparated_preimage, Subtype.property
-- 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 : Algebra (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)
  (↑Γ(X,
        X.basicOpen (U := f ⁻¹ᵁ (↑U : Y.Opens))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(Y, (↑U : Y.Opens))) (app f (↑U : Y.Opens)) :
              (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
            r)) :
    Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))))
⊢ 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,
          X.basicOpen (U := f ⁻¹ᵁ (↑U : Y.Opens))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (X := Γ(Y, (↑U : Y.Opens))) (app f (↑U : Y.Opens)) :
                (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
              r)) :
      Type u)

Tactic:
exact isLocalization_basicOpen_of_qcqs (f.isCompact_preimage U.2.isCompact)
        (f.isQuasiSeparated_preimage U.2.isQuasiSeparated) (f.app _ r)

Premises used: AlgebraicGeometry.IsAffineOpen.isCompact, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.Hom.app, AlgebraicGeometry.Scheme.Hom.isCompact_preimage, AlgebraicGeometry.IsAffineOpen.isQuasiSeparated, DFunLike.coe, AlgebraicGeometry.isLocalization_basicOpen_of_qcqs, AlgebraicGeometry.Scheme.Hom.isQuasiSeparated_preimage, Subtype.property
-- 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 : IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u)
⊢ 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)

Tactic:
have : IsLocalization.Away ((algebraMap ↑Γ(Y, U.1) ↑Γ(X, f ⁻¹ᵁ U.1)) r)
      Γ(X, f ⁻¹ᵁ Y.basicOpen r) := by
    let : Algebra Γ(X, f ⁻¹ᵁ U.1) Γ(X, X.basicOpen (f.app _ r)) :=
      (X.presheaf.map (homOfLE (X.basicOpen_le _)).op).hom.toAlgebra
    dsimp +instances [inst]
    rw! (castMode := .all) [f.preimage_basicOpen r]
    exact isLocalization_basicOpen_of_qcqs (f.isCompact_preimage U.2.isCompact)
        (f.isQuasiSeparated_preimage U.2.isQuasiSeparated) (f.app _ r)
-- 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 : 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
⊢ IsScalarTower.{u, u, u} (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)
    (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)

Tactic:
have : IsScalarTower Γ(Y, U.1) Γ(X, f ⁻¹ᵁ U.1) Γ(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 :
  IsScalarTower.{u, u, u} (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)
    (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)
⊢ Eq.{u + 1} (α := (↑Γ(Y, (↑U : Y.Opens)) : Type u) →+* (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u))
    (algebraMap (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u))
    (@RingHom.comp _ (↑Γ(Y, Y.basicOpen r) : Type u) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u))
      (algebraMap (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, Y.basicOpen r) : Type u)))

Tactic:
simp only [RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp, Scheme.Hom.app_eq_appLE,
        Scheme.Hom.map_appLE, AffineZariskiSite.basicOpen]

Premises used: CommRingCat.hom_comp, AlgebraicGeometry.Scheme.AffineZariskiSite.basicOpen, AlgebraicGeometry.Scheme.Hom.app_eq_appLE, RingHom.algebraMap_toAlgebra, AlgebraicGeometry.Scheme.Hom.map_appLE
-- 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 :
  IsScalarTower.{u, u, u} (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)
    (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)
⊢ IsScalarTower.{u, u, u} (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, Y.basicOpen r) : Type u)
    (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)

Tactic:
have : IsScalarTower Γ(Y, U.1) Γ(Y, Y.basicOpen r) Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
    .of_algebraMap_eq' <| by
      simp only [RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp, Scheme.Hom.app_eq_appLE,
        Scheme.Hom.map_appLE, AffineZariskiSite.basicOpen]
-- 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 :
  IsScalarTower.{u, u, u} (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, Y.basicOpen r) : Type u)
    (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)
⊢ 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)

Tactic:
have : IsScalarTower (integralClosure Γ(Y, U.1) Γ(X, f ⁻¹ᵁ U.1))
    (integralClosure Γ(Y, Y.basicOpen r) Γ(X, f ⁻¹ᵁ Y.basicOpen r))
    Γ(X, f ⁻¹ᵁ Y.basicOpen r) := .of_algebraMap_eq' rfl