-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Module.Finite R S
inst_6 : q.LiesOver p
hRS : Ideal.FG (RingHom.ker (F := R →+* S) (algebraMap R S))
H_1 :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
s : Finset S
hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤
a b : (x : S) → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S : (a : R) → S) (a x) = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : S)
r : R
hrp : r ∉ p
hr :
  ∀ (r' : R),
    r ∣ r' →
      Function.Injective.{u_1 + 1, u_2 + 1} (α := Away r') (β := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
        (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
r' : R
hr' : r * ∏ i ∈ s, b i ∣ r'
H :
  LE.le (α := Subalgebra R (Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S)))
    (AlgHom.range (IsScalarTower.toAlgHom R S (Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))))
    (AlgHom.range (awayMapₐ (Algebra.ofId R S) r'))
x : S
n : ℕ
obtain :
  ∀ (y : Away r')
    (hy :
      Eq.{u_2 + 1} (α := Away (M := S) ((AlgHom.toRingHom (Algebra.ofId R S) : (a : R) → S) r' : S))
        (((awayMap (AlgHom.toRingHom (Algebra.ofId R S)) r' :
                RingHom.{u_1, u_2} (Away r')
                  (Away (M := S) ((AlgHom.toRingHom (Algebra.ofId R S) : (a : R) → S) r' : S))) :
              (a : Away r') → Away (((Algebra.ofId R S).toRingHom : (a : R) → S) r'))
            y :
          Away (M := S) ((AlgHom.toRingHom (Algebra.ofId R S) : (a : R) → S) r' : S))
        ((AlgHom.toRingHom (IsScalarTower.toAlgHom R S (Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))) :
              (a : S) → Away ((Algebra.ofId R S : (a : R) → S) r'))
            x :
          Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))),
    ∃ (a : Away r'),
      Eq (α := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
        (((awayMap (algebraMap R S) r' :
                RingHom.{u_1, u_2} (Away r') (Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))) :
              (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
            a :
          Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
        (IsLocalization.mk' (Away (M := S) ((algebraMap R S : (a : R) → S) r' : S)) x
            (Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.powers ((algebraMap R S : (a : R) → S) r') : Submonoid S) x)
              ((fun (x : ℕ) ↦ HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r' : S) x) n) ⋯) :
          Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
⊢ ∃ (a : Away r'),
    Eq (α := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
      (((awayMap (algebraMap R S) r' :
              RingHom.{u_1, u_2} (Away r') (Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))) :
            (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
          a :
        Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
      (IsLocalization.mk' (Away (M := S) ((algebraMap R S : (a : R) → S) r' : S)) x
          (Subtype.mk (p := fun (x : S) ↦
            Membership.mem (γ := Submonoid S) (Submonoid.powers ((algebraMap R S : (a : R) → S) r') : Submonoid S) x)
            ((fun (x : ℕ) ↦ HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r' : S) x) n) ⋯) :
        Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))

Tactic:
obtain ⟨y, hy : awayMap _ _ _ = _⟩ := H ⟨x, rfl⟩

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