-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal S
H : ZariskisMainProperty R p
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
r : S
hrp : r ∉ p
hr : IsIntegral R r
m : (x : S) → ℕ
hm : ∀ (x : S), IsIntegral R (r ^ m x * x)
t : Set S := insert r {x : S | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (adjoin R t) x) r ⋯
this :
  LE.le (α :=
    Subalgebra R (Localization.Away (M := S) ((Subalgebra.val (adjoin R t) : (a : ↥(adjoin R t)) → S) r' : S)))
    (AlgHom.range
      (IsScalarTower.toAlgHom R S
        (Localization.Away (M := S) ((Subalgebra.val (adjoin R t) : (a : ↥(adjoin R t)) → S) r' : S))))
    (AlgHom.range (Localization.awayMapₐ (Subalgebra.val (adjoin R t)) r'))
x : S
n : ℕ
refine_3 :
  ∀ (y : Localization.Away r')
    (hy :
      Eq (α :=
        Localization.Away (M := S) ((AlgHom.toRingHom (Subalgebra.val (adjoin R t)) : (a : ↥(adjoin R t)) → S) r' : S))
        ((Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (adjoin R t))) r' :
              (a : Localization.Away r') →
                Localization.Away (((adjoin R t).val.toRingHom : (a : ↥(adjoin R t)) → S) r'))
            y :
          Localization.Away (M := S)
            ((AlgHom.toRingHom (Subalgebra.val (adjoin R t)) : (a : ↥(adjoin R t)) → S) r' : S))
        ((AlgHom.toRingHom
                (IsScalarTower.toAlgHom R S
                  (Localization.Away (M := S) ((Subalgebra.val (adjoin R t) : (a : ↥(adjoin R t)) → S) r' : S))) :
              (a : S) → Localization.Away (((adjoin R t).val : (a : ↥(adjoin R t)) → S) r'))
            x :
          Localization.Away (M := S) ((Subalgebra.val (adjoin R t) : (a : ↥(adjoin R t)) → S) r' : S))),
    ∃ (a : Localization.Away r'),
      Eq (α :=
        Localization.Away (M := S) ((AlgHom.toRingHom (Subalgebra.val (adjoin R t)) : (a : ↥(adjoin R t)) → S) r' : S))
        ((Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (adjoin R t))) r' :
              (a : Localization.Away r') →
                Localization.Away (((adjoin R t).val.toRingHom : (a : ↥(adjoin R t)) → S) r'))
            a :
          Localization.Away (M := S)
            ((AlgHom.toRingHom (Subalgebra.val (adjoin R t)) : (a : ↥(adjoin R t)) → S) r' : S))
        (IsLocalization.mk'
            (Localization.Away (M := S)
              ((AlgHom.toRingHom (Subalgebra.val (adjoin R t)) : (a : ↥(adjoin R t)) → S) r' : S))
            x
            (Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S)
                (Submonoid.powers ((AlgHom.toRingHom (Subalgebra.val (adjoin R t)) : (a : ↥(adjoin R t)) → S) r') :
                  Submonoid S)
                x)
              ((fun (x : ℕ) ↦
                  HPow.hPow (α := S) ((AlgHom.toRingHom (Subalgebra.val (adjoin R t)) : (a : ↥(adjoin R t)) → S) r' : S)
                    x)
                n)
              ⋯) :
          Localization.Away (M := S)
            ((AlgHom.toRingHom (Subalgebra.val (adjoin R t)) : (a : ↥(adjoin R t)) → S) r' : S))
⊢ ∃ (a : Localization.Away r'),
    Eq (α :=
      Localization.Away (M := S) ((AlgHom.toRingHom (Subalgebra.val (adjoin R t)) : (a : ↥(adjoin R t)) → S) r' : S))
      ((Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (adjoin R t))) r' :
            (a : Localization.Away r') → Localization.Away (((adjoin R t).val.toRingHom : (a : ↥(adjoin R t)) → S) r'))
          a :
        Localization.Away (M := S) ((AlgHom.toRingHom (Subalgebra.val (adjoin R t)) : (a : ↥(adjoin R t)) → S) r' : S))
      (IsLocalization.mk'
          (Localization.Away (M := S)
            ((AlgHom.toRingHom (Subalgebra.val (adjoin R t)) : (a : ↥(adjoin R t)) → S) r' : S))
          x
          (Subtype.mk (p := fun (x : S) ↦
            Membership.mem (γ := Submonoid S)
              (Submonoid.powers ((AlgHom.toRingHom (Subalgebra.val (adjoin R t)) : (a : ↥(adjoin R t)) → S) r') :
                Submonoid S)
              x)
            ((fun (x : ℕ) ↦
                HPow.hPow (α := S) ((AlgHom.toRingHom (Subalgebra.val (adjoin R t)) : (a : ↥(adjoin R t)) → S) r' : S)
                  x)
              n)
            ⋯) :
        Localization.Away (M := S) ((AlgHom.toRingHom (Subalgebra.val (adjoin R t)) : (a : ↥(adjoin R t)) → S) r' : S))

Tactic:
obtain ⟨y, hy : Localization.awayMap _ _ _ = _⟩ := this ⟨x, rfl⟩

Premises used: Localization.awayMap, Exists.intro, DFunLike.coe, rfl