-- 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 : ℕ
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))
refine_3 :
  HMul.hMul (α :=
      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))
      (HPow.hPow (α :=
        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'))
            (Localization.Away.invSelf r') :
          Localization.Away (M := S)
            ((AlgHom.toRingHom (Subalgebra.val (adjoin R t)) : (a : ↥(adjoin R t)) → S) r' : S))
        n) =
    IsLocalization.mk' (M :=
      Submonoid.powers ((AlgHom.toRingHom (Subalgebra.val (adjoin R t)) : (a : ↥(adjoin R t)) → S) r'))
      (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)
        (HPow.hPow (α := S) ((AlgHom.toRingHom (Subalgebra.val (adjoin R t)) : (a : ↥(adjoin R t)) → S) r' : S) n) ⋯)
⊢ 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 * HPow.hPow (α := Localization.Away r') (Localization.Away.invSelf r') n) :
      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:
simp only [map_mul, map_pow, hy]

Premises used: map_pow, map_mul