-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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 :
  ∀ (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
a : (↑(↑s : Set R) : Type u_1)
rw :
  HMul.hMul (β := Away (↑a : R)) (f a)
      ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) ((↑a : R) ^ N) : Away (↑a : R)) =
    HMul.hMul (α := Away (↑a : R)) (β := Away (↑a : R))
      ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) ((↑a : R) ^ (N - n a)) : Away (↑a : R))
      ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) (r_1 a) : Away (↑a : R))
rw₁ :
  HMul.hMul (β := Away (↑a : R)) (f a)
      ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) ((↑a : R) ^ N) : Away (↑a : R)) =
    HMul.hMul (α := Away (↑a : R))
      ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) ((↑a : R) ^ (N - n a)) : Away (↑a : R))
      (f a * HPow.hPow (α := Away (↑a : R)) ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) (↑a : R)) (n a))
rw₂ :
  HMul.hMul (β := Away (↑a : R)) (f a)
      ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) ((↑a : R) ^ N) : Away (↑a : R)) =
    f a *
      HMul.hMul (α := Away (↑a : R))
        ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) ((↑a : R) ^ (N - n a)) : Away (↑a : R))
        (HPow.hPow (α := Away (↑a : R)) ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) (↑a : R)) (n a))
rw₃ :
  HMul.hMul (β := Away (↑a : R)) (f a)
      ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) ((↑a : R) ^ N) : Away (↑a : R)) =
    f a *
      HMul.hMul (α := Away (↑a : R)) (β := Away (↑a : R))
        ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) ((↑a : R) ^ (N - n a)) : Away (↑a : R))
        ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) ((↑a : R) ^ n a) : Away (↑a : R))
rw₄ :
  HMul.hMul (β := Away (↑a : R)) (f a)
      ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) ((↑a : R) ^ N) : Away (↑a : R)) =
    HMul.hMul (β := Away (↑a : R)) (f a)
      ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) ((↑a : R) ^ (N - n a) * (↑a : R) ^ n a) :
        Away (↑a : R))
rw₅ :
  HMul.hMul (β := Away (↑a : R)) (f a)
      ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) ((↑a : R) ^ N) : Away (↑a : R)) =
    HMul.hMul (β := Away (↑a : R)) (f a)
      ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) ((↑a : R) ^ (N - n a + n a)) : Away (↑a : R))
⊢ 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)
have rw₆ : HMul.hMul (β := Away (↑a : R)) (f a)
    ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) ((↑a : R) ^ N) : Away (↑a : R)) =
  HMul.hMul (β := Away (↑a : R)) (f a)
    ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) ((↑a : R) ^ s.attach.sup n) : Away (↑a : R))
Tactic: rw [map_mul, ← eq, mul_left_comm, ← map_pow, ← map_mul, ← pow_add,
      Nat.sub_add_cancel (Finset.le_sup <| s.mem_attach a)]