-- 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 : ℕ
y : Away r'
hy :
  Eq.{u_2 + 1} (α := 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'))
        y :
      Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
    ((algebraMap S (Away (M := S) ((algebraMap R S : (a : R) → S) r' : S)) :
          (a : S) → Away ((algebraMap R S : (a : R) → S) r'))
        x :
      Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
⊢ HMul.hMul (α := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S)) (β :=
      Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
      ((algebraMap S (Away (M := S) ((algebraMap R S : (a : R) → S) r' : S)) :
            (a : S) → Away ((algebraMap R S : (a : R) → S) r'))
          x :
        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'))
          (HPow.hPow (α := Away r') (Away.invSelf r') n) :
        Away (M := S) ((algebraMap R S : (a : R) → S) r' : S)) =
    IsLocalization.mk' (M := Submonoid.powers ((algebraMap R S : (a : R) → S) r'))
      (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)
        (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r' : S) n) ⋯)

Tactic:
simp [Away.invSelf, Localization.mk_eq_mk', awayMap, IsLocalization.Away.map,
    IsLocalization.map_mk', ← Algebra.smul_def, IsLocalization.smul_mk', ← IsLocalization.mk'_pow]

Premises used: IsLocalization.map_mk', Localization.mk_eq_mk', IsLocalization.mk'_pow, IsLocalization.smul_mk', Localization.Away.invSelf, IsLocalization.Away.map, Localization.awayMap, Algebra.smul_def