-- 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 :
  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
x : S
hxs : x ∈ (↑s : Set S)
r'' : R
hr' : r' = (r * ∏ i ∈ s, b i) * r''
simp :
  Eq (α := 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'))
        (HMul.hMul (β := S)
            (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) r'' : S)
              ((algebraMap R S : (a : R) → S) r : S))
            ((algebraMap R S : (a : R) → S) (∏ i ∈ s.erase x, b i) : S) *
          HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : 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'))
        (HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) r' : S)) :
      Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
⊢ Eq.{u_2 + 1} (α := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
    (((IsLocalization.map (T := Submonoid.powers ((algebraMap R S : (a : R) → S) r'))
              (Away (M := S) ((algebraMap R S : (a : R) → S) r' : S)) (algebraMap R S) ⋯ :
            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'))
        (IsLocalization.mk' (M := Submonoid.powers r') (Away r') ((r'' * r * ∏ i ∈ s.erase x, b i) * a x)
          (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r') x)
            (HPow.hPow (β := ℕ) r' 1) ⋯)) :
      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))

Tactic:
simp only [pow_one, IsLocalization.map_mk', IsLocalization.mk'_eq_iff_eq_mul,
      ← map_mul (algebraMap S _), map_mul (algebraMap R _), e]

Premises used: IsLocalization.map_mk', Algebra.algebraMap, IsLocalization.mk'_eq_iff_eq_mul, map_mul, pow_one