-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
f : M →* N
h : ∀ (y : ↥S), IsUnit.{u_2} (M := N) ((f : (a : M) → N) (↑y : M) : N)
x₁ x₂ : M
y₁ y₂ : ↥S
rw :
  HMul.hMul (β := N)
        (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₁ : N)
          ((↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y₁)⁻¹ : N) : N))
        ((f : (a : M) → N) (↑y₂ : M) : N) =
      (f : (a : M) → N) x₂ ↔
    Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (x₁ * (↑y₂ : M)) : N) ((f : (a : M) → N) (x₂ * (↑y₁ : M)) : N)
rw₁ :
  HMul.hMul (α := N) ((f : (a : M) → N) x₁ : N)
        (HMul.hMul (α := N) (β := N) ((↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y₁)⁻¹ : N) : N)
          ((f : (a : M) → N) (↑y₂ : M) : N)) =
      (f : (a : M) → N) x₂ ↔
    Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (x₁ * (↑y₂ : M)) : N) ((f : (a : M) → N) (x₂ * (↑y₁ : M)) : N)
rw₂ :
  HMul.hMul (α := N) ((f : (a : M) → N) x₁ : N)
        (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑y₂ : M) : N)
          ((↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y₁)⁻¹ : N) : N)) =
      (f : (a : M) → N) x₂ ↔
    Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (x₁ * (↑y₂ : M)) : N) ((f : (a : M) → N) (x₂ * (↑y₁ : M)) : N)
rw₃ :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₁ : N) ((f : (a : M) → N) (↑y₂ : M) : N) *
        (↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y₁)⁻¹ : N) =
      (f : (a : M) → N) x₂ ↔
    Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (x₁ * (↑y₂ : M)) : N) ((f : (a : M) → N) (x₂ * (↑y₁ : M)) : N)
rw₄ :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₁ : N) ((f : (a : M) → N) (↑y₂ : M) : N) =
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑y₁ : M) : N) ((f : (a : M) → N) x₂ : N) ↔
    Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (x₁ * (↑y₂ : M)) : N) ((f : (a : M) → N) (x₂ * (↑y₁ : M)) : N)
rw₅ :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₁ : N) ((f : (a : M) → N) (↑y₂ : M) : N) =
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑y₁ : M) : N) ((f : (a : M) → N) x₂ : N) ↔
    Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (x₁ * (↑y₂ : M)) : N) ((f : (a : M) → N) ((↑y₁ : M) * x₂) : N)
rw₆ :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₁ : N) ((f : (a : M) → N) (↑y₂ : M) : N) =
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑y₁ : M) : N) ((f : (a : M) → N) x₂ : N) ↔
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₁ : N) ((f : (a : M) → N) (↑y₂ : M) : N) =
      (f : (a : M) → N) ((↑y₁ : M) * x₂)
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₁ : N)
        ((↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y₁)⁻¹ : N) : N) =
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₂ : N)
        ((↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y₂)⁻¹ : N) : N) ↔
    Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (x₁ * (↑y₂ : M)) : N) ((f : (a : M) → N) (x₂ * (↑y₁ : M)) : N)
have rw₇ : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₁ : N) ((f : (a : M) → N) (↑y₂ : M) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑y₁ : M) : N) ((f : (a : M) → N) x₂ : N) ↔
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₁ : N) ((f : (a : M) → N) (↑y₂ : M) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑y₁ : M) : N) ((f : (a : M) → N) x₂ : N)
Tactic: rw [mul_inv_right h, mul_assoc, mul_comm _ (f y₂), ← mul_assoc, mul_inv_left h, mul_comm x₂,
    f.map_mul, f.map_mul]