-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
U : X.AffineZariskiSite
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
αU : Γ(X, U.toOpens) ⟶ F.obj (Opposite.op U) := α.app (Opposite.op U)
αUf : Γ(X, X.basicOpen f) ⟶ F.obj (Opposite.op (U.basicOpen f)) := α.app (Opposite.op (U.basicOpen f))
algInst : Algebra (↑Γ(X, U.toOpens) : Type u) (↑(F.obj (Opposite.op U)) : Type u) := (CommRingCat.Hom.hom αU).toAlgebra
algInst_1 : Algebra (↑Γ(X, X.basicOpen f) : Type u) (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u) :=
  (CommRingCat.Hom.hom αUf).toAlgebra
algInst_2 : Algebra (↑(F.obj (Opposite.op U)) : Type u) (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u) :=
  (CommRingCat.Hom.hom (F.map ⋯.hom.op)).toAlgebra
algInst_3 : Algebra (↑Γ(X, U.toOpens) : Type u) (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u) :=
  ((CommRingCat.Hom.hom (F.map ⋯.hom.op)).comp (CommRingCat.Hom.hom αU)).toAlgebra
scalarTowerInst : IsScalarTower.{u, u, u} (↑Γ(X, U.toOpens) : Type u) (↑(F.obj (Opposite.op U)) : Type u)
  (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u) :=
  ⋯
this_1 :
  IsScalarTower.{u, u, u} (↑Γ(X, U.toOpens) : Type u) (↑Γ(X, X.basicOpen f) : Type u)
    (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u)
this : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
refine :
  IsLocalization (R := (↑(F.1 (Opposite.op U)) : Type u))
      (Algebra.algebraMapSubmonoid (↑(F.1 (Opposite.op U)) : Type u) (Submonoid.powers f))
      (↑(F.1 (Opposite.op (U.basicOpen f))) : Type u) ↔
    IsLocalization.Away (R := (↑(F.obj (Opposite.op U)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) αU :
            (a : (↑(((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U)) : Type u)) →
              (↑(F.obj (Opposite.op U)) : Type u))
          f :
        (↑(F.obj (Opposite.op U)) : Type u))
      (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u)
⊢ Algebra.IsPushout.{u, u, u, u} (↑(X.presheaf.1 (Opposite.op (↑U : X.Opens))) : Type u)
      (↑(F.1 (Opposite.op U)) : Type u) (↑(X.presheaf.1 (Opposite.op (X.basicOpen f))) : Type u)
      (↑(F.1 (Opposite.op (U.basicOpen f))) : Type u) ↔
    IsLocalization.Away (R := (↑(F.obj (Opposite.op U)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) αU :
            (a : (↑(((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U)) : Type u)) →
              (↑(F.obj (Opposite.op U)) : Type u))
          f :
        (↑(F.obj (Opposite.op U)) : Type u))
      (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u)

Tactic:
refine (Algebra.isLocalization_iff_isPushout (.powers f) Γ(X, X.basicOpen f)).symm.trans ?_

Premises used: CommRingCat.carrier, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, Opposite.op, Submonoid.powers, AlgebraicGeometry.Scheme.basicOpen, AlgebraicGeometry.PresheafedSpace.presheaf, Iff.trans, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Iff.symm, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace, Algebra.isLocalization_iff_isPushout