-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
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 : ℕ
⊢ ∃ (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))
have 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) sorry) :
        Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
Tactic: obtain ⟨y, hy : awayMap _ _ _ = _⟩ := H ⟨x, rfl⟩