-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
f : S.LocalizationMap N
x₁ x₂ : M
y₁ y₂ : ↥S
H : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) ((↑y₂ : M) * x₁) : N) ((f : (a : M) → N) ((↑y₁ : M) * x₂) : N)
rw : (f : (a : M) → N) x₁ = HMul.hMul (β := N) (f.mk' x₂ y₂) ((f : (a : M) → N) (↑y₁ : M) : N)
rw₁ :
  (f : (a : M) → N) x₁ =
    HMul.hMul (β := N)
      (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₂ : N)
        ((↑((IsUnit.liftRight (f.toMonoidHom.restrict S) ⋯ : (a : ↥S) → Nˣ) y₂)⁻¹ : N) : N))
      ((f : (a : M) → N) (↑y₁ : M) : N)
rw₂ :
  (f : (a : M) → N) x₁ =
    HMul.hMul (α := N) ((f : (a : M) → N) x₂ : N)
      (HMul.hMul (α := N) (β := N) ((↑((IsUnit.liftRight (f.toMonoidHom.restrict S) ⋯ : (a : ↥S) → Nˣ) y₂)⁻¹ : N) : N)
        ((f : (a : M) → N) (↑y₁ : M) : N))
rw₃ :
  (f : (a : M) → N) x₁ =
    HMul.hMul (α := N) ((f : (a : M) → N) x₂ : N)
      (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑y₁ : M) : N)
        ((↑((IsUnit.liftRight (f.toMonoidHom.restrict S) ⋯ : (a : ↥S) → Nˣ) y₂)⁻¹ : N) : N))
rw₄ :
  (f : (a : M) → N) x₁ =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₂ : N) ((f : (a : M) → N) (↑y₁ : M) : N) *
      (↑((IsUnit.liftRight (f.toMonoidHom.restrict S) ⋯ : (a : ↥S) → Nˣ) y₂)⁻¹ : N)
rw₅ :
  (f : (a : M) → N) x₁ =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (x₂ * (↑y₁ : M)) : N)
      ((↑((IsUnit.liftRight (f.toMonoidHom.restrict S) ⋯ : (a : ↥S) → Nˣ) y₂)⁻¹ : N) : N)
rw₆ :
  (f : (a : M) → N) x₁ =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) ((↑y₁ : M) * x₂) : N)
      ((↑((IsUnit.liftRight (f.toMonoidHom.restrict S) ⋯ : (a : ↥S) → Nˣ) y₂)⁻¹ : N) : N)
rw₇ :
  (f : (a : M) → N) x₁ =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) ((↑y₂ : M) * x₁) : N)
      ((↑((IsUnit.liftRight (f.toMonoidHom.restrict S) ⋯ : (a : ↥S) → Nˣ) y₂)⁻¹ : N) : N)
rw₈ :
  (f : (a : M) → N) x₁ =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (x₁ * (↑y₂ : M)) : N)
      ((↑((IsUnit.liftRight (f.toMonoidHom.restrict S) ⋯ : (a : ↥S) → Nˣ) y₂)⁻¹ : N) : N)
rw₉ :
  (f : (a : M) → N) x₁ =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₁ : N) ((f : (a : M) → N) (↑y₂ : M) : N) *
      (↑((IsUnit.liftRight (f.toMonoidHom.restrict S) ⋯ : (a : ↥S) → Nˣ) y₂)⁻¹ : N)
rw₁₀ :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₁ : N) ((f.toMonoidHom : (a : M) → N) (↑y₂ : M) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₁ : N) ((f : (a : M) → N) (↑y₂ : M) : N)
rw₁₁ 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) x₁ : N) ((f : (a : M) → N) (↑y₂ : M) : N)
⊢ f.mk' x₁ y₁ = f.mk' x₂ y₂

Tactic:
rw [mk'_eq_iff_eq_mul, mk', mul_assoc, mul_comm _ (f y₁), ← mul_assoc, ← map_mul f, mul_comm x₂,
      ← H, ← mul_comm x₁, map_mul f, mul_inv_right f.map_units, toMonoidHom_apply]

Premises used: Submonoid.LocalizationMap.mk', mul_assoc, map_mul, mul_comm, Submonoid.LocalizationMap.mul_inv_right, Submonoid.LocalizationMap.map_units, Subtype.val, DFunLike.coe, Submonoid.LocalizationMap.mk'_eq_iff_eq_mul, Submonoid.LocalizationMap.toMonoidHom_apply