-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
s : Finset R
f : (a : (↑(↑s : Set R) : Type u_1)) → Away (↑a : R)
h :
  ∀ (a b : (↑(↑s : Set R) : Type u_1)),
    Eq (α := Away ((↑a : R) * (↑b : R)))
      ((Away.awayToAwayRight (↑a : R) (↑b : R) : (a_1 : Away (↑a : R)) → Away ((↑a : R) * (↑b : R))) (f a) :
        Away ((↑a : R) * (↑b : R)))
      ((Away.awayToAwayLeft (↑b : R) (↑a : R) : (a_1 : Away (↑b : R)) → Away ((↑a : R) * (↑b : R))) (f b) :
        Away ((↑a : R) * (↑b : R)))
mem : Membership.mem (γ := Ideal R) (Ideal.span (↑s : Set R)) 1
span_eq : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
n : (a : (↑(↑s : Set R) : Type u_1)) → ℕ
r_1 : (a : (↑(↑s : Set R) : Type u_1)) → R
eq_1 :
  ∀ (a : (↑(↑s : Set R) : Type u_1)),
    f a * HPow.hPow (α := Away (↑a : R)) ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) (↑a : R)) (n a) =
      (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) (r_1 a)
N : ℕ := s.attach.sup n
r : (a : (↑(↑s : Set R) : Type u_1)) → R := fun (a : (↑(↑s : Set R) : Type u_1)) ↦ (↑a : R) ^ (N - n a) * r_1 a
eq :
  ∀ (a : (↑(↑s : Set R) : Type u_1)),
    HMul.hMul (β := Away (↑a : R)) (f a)
        ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) ((↑a : R) ^ N) : Away (↑a : R)) =
      (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) (r a)
N'_1 : (a b : (↑(↑s : Set R) : Type u_1)) → ℕ
hN' :
  ∀ (a b : (↑(↑s : Set R) : Type u_1)),
    ((↑a : R) * (↑b : R)) ^ N'_1 a b * (r a * (↑b : R) ^ N) = ((↑a : R) * (↑b : R)) ^ N'_1 a b * (r b * (↑a : R) ^ N)
N' : ℕ :=
  (s ×ˢ s).attach.sup fun (a : ↥(s ×ˢ s)) ↦
    N'_1 (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R)) (↑a : R × R).1 ⋯)
      (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R)) (↑a : R × R).2 ⋯)
a b : (↑(↑s : Set R) : Type u_1)
rw :
  ((↑a : R) * (↑b : R)) ^
        (((s ×ˢ s).attach.sup fun (a : ↥(s ×ˢ s)) ↦
              N'_1 (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R)) (↑a : R × R).1 ⋯)
                (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R)) (↑a : R × R).2 ⋯)) -
            N'_1
              (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
                (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).1 ⋯)
              (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
                (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).2 ⋯) +
          N'_1
            (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
              (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).1 ⋯)
            (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
              (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).2 ⋯)) *
      (r a * (↑b : R) ^ N) =
    ((↑a : R) * (↑b : R)) ^
        (((s ×ˢ s).attach.sup fun (a : ↥(s ×ˢ s)) ↦
              N'_1 (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R)) (↑a : R × R).1 ⋯)
                (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R)) (↑a : R × R).2 ⋯)) -
            N'_1
              (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
                (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).1 ⋯)
              (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
                (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).2 ⋯) +
          N'_1
            (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
              (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).1 ⋯)
            (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
              (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).2 ⋯)) *
      (r b * (↑a : R) ^ N)
rw₁ :
  ((↑a : R) * (↑b : R)) ^
          (((s ×ˢ s).attach.sup fun (a : ↥(s ×ˢ s)) ↦
              N'_1 (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R)) (↑a : R × R).1 ⋯)
                (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R)) (↑a : R × R).2 ⋯)) -
            N'_1
              (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
                (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).1 ⋯)
              (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
                (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).2 ⋯)) *
        ((↑a : R) * (↑b : R)) ^
          N'_1
            (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
              (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).1 ⋯)
            (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
              (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).2 ⋯) *
      (r a * (↑b : R) ^ N) =
    ((↑a : R) * (↑b : R)) ^
          (((s ×ˢ s).attach.sup fun (a : ↥(s ×ˢ s)) ↦
              N'_1 (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R)) (↑a : R × R).1 ⋯)
                (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R)) (↑a : R × R).2 ⋯)) -
            N'_1
              (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
                (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).1 ⋯)
              (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
                (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).2 ⋯)) *
        ((↑a : R) * (↑b : R)) ^
          N'_1
            (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
              (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).1 ⋯)
            (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
              (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).2 ⋯) *
      (r b * (↑a : R) ^ N)
rw₂ :
  ((↑a : R) * (↑b : R)) ^
        (((s ×ˢ s).attach.sup fun (a : ↥(s ×ˢ s)) ↦
            N'_1 (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R)) (↑a : R × R).1 ⋯)
              (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R)) (↑a : R × R).2 ⋯)) -
          N'_1
            (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
              (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).1 ⋯)
            (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
              (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).2 ⋯)) *
      (((↑a : R) * (↑b : R)) ^
          N'_1
            (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
              (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).1 ⋯)
            (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
              (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).2 ⋯) *
        (r a * (↑b : R) ^ N)) =
    ((↑a : R) * (↑b : R)) ^
          (((s ×ˢ s).attach.sup fun (a : ↥(s ×ˢ s)) ↦
              N'_1 (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R)) (↑a : R × R).1 ⋯)
                (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R)) (↑a : R × R).2 ⋯)) -
            N'_1
              (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
                (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).1 ⋯)
              (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
                (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).2 ⋯)) *
        ((↑a : R) * (↑b : R)) ^
          N'_1
            (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
              (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).1 ⋯)
            (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
              (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).2 ⋯) *
      (r b * (↑a : R) ^ N)
rw₃ :
  ((↑a : R) * (↑b : R)) ^
        (((s ×ˢ s).attach.sup fun (a : ↥(s ×ˢ s)) ↦
            N'_1 (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R)) (↑a : R × R).1 ⋯)
              (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R)) (↑a : R × R).2 ⋯)) -
          N'_1
            (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
              (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).1 ⋯)
            (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
              (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).2 ⋯)) *
      (((↑a : R) * (↑b : R)) ^ N'_1 a b * (r b * (↑a : R) ^ N)) =
    ((↑a : R) * (↑b : R)) ^
          (((s ×ˢ s).attach.sup fun (a : ↥(s ×ˢ s)) ↦
              N'_1 (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R)) (↑a : R × R).1 ⋯)
                (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R)) (↑a : R × R).2 ⋯)) -
            N'_1
              (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
                (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).1 ⋯)
              (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
                (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).2 ⋯)) *
        ((↑a : R) * (↑b : R)) ^
          N'_1
            (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
              (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).1 ⋯)
            (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
              (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).2 ⋯) *
      (r b * (↑a : R) ^ N)
rw₄ rw₅ :
  ((↑a : R) * (↑b : R)) ^
          (((s ×ˢ s).attach.sup fun (a : ↥(s ×ˢ s)) ↦
              N'_1 (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R)) (↑a : R × R).1 ⋯)
                (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R)) (↑a : R × R).2 ⋯)) -
            N'_1
              (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
                (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).1 ⋯)
              (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
                (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).2 ⋯)) *
        ((↑a : R) * (↑b : R)) ^ N'_1 a b *
      (r b * (↑a : R) ^ N) =
    ((↑a : R) * (↑b : R)) ^
          (((s ×ˢ s).attach.sup fun (a : ↥(s ×ˢ s)) ↦
              N'_1 (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R)) (↑a : R × R).1 ⋯)
                (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R)) (↑a : R × R).2 ⋯)) -
            N'_1
              (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
                (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).1 ⋯)
              (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
                (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).2 ⋯)) *
        ((↑a : R) * (↑b : R)) ^
          N'_1
            (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
              (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).1 ⋯)
            (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R))
              (↑(Subtype.mk (p := fun (x : R × R) ↦ x ∈ s ×ˢ s) ((↑a : R), (↑b : R)) ⋯) : R × R).2 ⋯) *
      (r b * (↑a : R) ^ N)
⊢ HPow.hPow (β := ℕ) ((↑a : R) * (↑b : R))
        ((s ×ˢ s).attach.sup fun (a : ↥(s ×ˢ s)) ↦
          N'_1 (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R)) (↑a : R × R).1 ⋯)
            (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R)) (↑a : R × R).2 ⋯)) *
      (r a * (↑b : R) ^ N) =
    HPow.hPow (β := ℕ) ((↑a : R) * (↑b : R))
        ((s ×ˢ s).attach.sup fun (a : ↥(s ×ˢ s)) ↦
          N'_1 (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R)) (↑a : R × R).1 ⋯)
            (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R)) (↑a : R × R).2 ⋯)) *
      (r b * (↑a : R) ^ N)

Tactic:
rw [← Nat.sub_add_cancel (Finset.le_sup <| (Finset.mem_attach _ ⟨⟨a, b⟩,
      Finset.mk_mem_product a.2 b.2⟩)), pow_add, mul_assoc, hN', ← mul_assoc]

Premises used: mul_assoc, Finset.mem_attach, pow_add, Subtype.mk, Nat.sub_add_cancel, Finset.le_sup