-- 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 :
  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)
change :
  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))
⊢ 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)

Tactic:
change IsLocalization.Away ((algebraMap Γ(Y, U.1) (integralClosure Γ(Y, U.1) Γ(X, f ⁻¹ᵁ U.1))) r)
    (integralClosure Γ(Y, Y.basicOpen r) Γ(X, f ⁻¹ᵁ Y.basicOpen r))

Premises used: CommRingCat.carrier, Algebra.algebraMap, IsLocalization.Away, Membership.mem, Subtype, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, integralClosure, Opposite.op, AlgebraicGeometry.Scheme.basicOpen, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Subtype.val, DFunLike.coe, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace