-- 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))
⊢ 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) ⋯)

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

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