awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : S.LocalizationMap N
x₁ x₂ : M
y₁ y₂ : ↥S
H : f.mk' x₁ y₁ = f.mk' x₂ y₂
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) ((↑y₂ : M) * x₁) : N) ((f : (a : M) → N) ((↑y₁ : M) * x₂) : N)
have rw : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑y₂ : M) : N) ((f : (a : M) → N) x₁ : N) =
  (f : (a : M) → N) ((↑y₁ : M) * x₂)
Tactic: rw [map_mul f, map_mul f, f.mk'_eq_iff_eq_mul.1 H, ← mul_assoc, mk'_spec', mul_comm (f x₂)]
-- 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 : S.LocalizationMap N
x₁ x₂ : M
y₁ y₂ : ↥S
H : f.mk' x₁ y₁ = f.mk' x₂ y₂
rw :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑y₂ : M) : N) ((f : (a : M) → N) x₁ : N) =
    (f : (a : M) → N) ((↑y₁ : M) * x₂)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) ((↑y₂ : M) * x₁) : N) ((f : (a : M) → N) ((↑y₁ : M) * x₂) : N)
have rw₁ : 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) (↑y₁ : M) : N) ((f : (a : M) → N) x₂ : N)
Tactic: rw [map_mul f, map_mul f, f.mk'_eq_iff_eq_mul.1 H, ← mul_assoc, mk'_spec', mul_comm (f x₂)]
-- 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 : S.LocalizationMap N
x₁ x₂ : M
y₁ y₂ : ↥S
H : f.mk' x₁ y₁ = f.mk' x₂ y₂
rw :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑y₂ : M) : N) ((f : (a : M) → N) x₁ : N) =
    (f : (a : M) → N) ((↑y₁ : M) * x₂)
rw₁ :
  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) (↑y₁ : M) : N) ((f : (a : M) → N) x₂ : N)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) ((↑y₂ : M) * x₁) : N) ((f : (a : M) → N) ((↑y₁ : M) * x₂) : N)
have rw₂ : HMul.hMul (α := N) ((f : (a : M) → N) (↑y₂ : M) : N)
    (HMul.hMul (β := N) (f.mk' x₂ y₂) ((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 [map_mul f, map_mul f, f.mk'_eq_iff_eq_mul.1 H, ← mul_assoc, mk'_spec', mul_comm (f x₂)]
-- 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 : S.LocalizationMap N
x₁ x₂ : M
y₁ y₂ : ↥S
H : f.mk' x₁ y₁ = f.mk' x₂ y₂
rw :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑y₂ : M) : N) ((f : (a : M) → N) x₁ : N) =
    (f : (a : M) → N) ((↑y₁ : M) * x₂)
rw₁ :
  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) (↑y₁ : M) : N) ((f : (a : M) → N) x₂ : N)
rw₂ :
  HMul.hMul (α := N) ((f : (a : M) → N) (↑y₂ : M) : N)
      (HMul.hMul (β := N) (f.mk' x₂ y₂) ((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) ((↑y₂ : M) * x₁) : N) ((f : (a : M) → N) ((↑y₁ : M) * x₂) : N)
have rw₃ : HMul.hMul (β := N) (HMul.hMul (α := N) ((f : (a : M) → N) (↑y₂ : M) : N) (f.mk' x₂ y₂))
    ((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 [map_mul f, map_mul f, f.mk'_eq_iff_eq_mul.1 H, ← mul_assoc, mk'_spec', mul_comm (f x₂)]
-- 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 : S.LocalizationMap N
x₁ x₂ : M
y₁ y₂ : ↥S
H : f.mk' x₁ y₁ = f.mk' x₂ y₂
rw :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑y₂ : M) : N) ((f : (a : M) → N) x₁ : N) =
    (f : (a : M) → N) ((↑y₁ : M) * x₂)
rw₁ :
  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) (↑y₁ : M) : N) ((f : (a : M) → N) x₂ : N)
rw₂ :
  HMul.hMul (α := N) ((f : (a : M) → N) (↑y₂ : M) : N)
      (HMul.hMul (β := N) (f.mk' x₂ y₂) ((f : (a : M) → N) (↑y₁ : M) : N)) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑y₁ : M) : N) ((f : (a : M) → N) x₂ : N)
rw₃ :
  HMul.hMul (β := N) (HMul.hMul (α := N) ((f : (a : M) → N) (↑y₂ : M) : N) (f.mk' x₂ y₂))
      ((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) ((↑y₂ : M) * x₁) : N) ((f : (a : M) → N) ((↑y₁ : M) * x₂) : 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)
Tactic: rw [map_mul f, map_mul f, f.mk'_eq_iff_eq_mul.1 H, ← mul_assoc, mk'_spec', mul_comm (f x₂)]
-- 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 : S.LocalizationMap N
x₁ x₂ : M
y₁ y₂ : ↥S
H : f.mk' x₁ y₁ = f.mk' x₂ y₂
rw :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑y₂ : M) : N) ((f : (a : M) → N) x₁ : N) =
    (f : (a : M) → N) ((↑y₁ : M) * x₂)
rw₁ :
  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) (↑y₁ : M) : N) ((f : (a : M) → N) x₂ : N)
rw₂ :
  HMul.hMul (α := N) ((f : (a : M) → N) (↑y₂ : M) : N)
      (HMul.hMul (β := N) (f.mk' x₂ y₂) ((f : (a : M) → N) (↑y₁ : M) : N)) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑y₁ : M) : N) ((f : (a : M) → N) x₂ : N)
rw₃ :
  HMul.hMul (β := N) (HMul.hMul (α := N) ((f : (a : M) → N) (↑y₂ : M) : N) (f.mk' x₂ y₂))
      ((f : (a : M) → N) (↑y₁ : M) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑y₁ : M) : N) ((f : (a : M) → N) 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)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) ((↑y₂ : M) * x₁) : N) ((f : (a : M) → N) ((↑y₁ : M) * x₂) : N)
have rw₅ : 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) (↑y₁ : M) : N) ((f : (a : M) → N) x₂ : N)
Tactic: rw [map_mul f, map_mul f, f.mk'_eq_iff_eq_mul.1 H, ← mul_assoc, mk'_spec', mul_comm (f x₂)]
-- 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 : 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)
⊢ f.mk' x₁ y₁ = f.mk' x₂ y₂
have rw : (f : (a : M) → N) x₁ = HMul.hMul (β := N) (f.mk' x₂ y₂) ((f : (a : M) → N) (↑y₁ : M) : N)
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]
-- 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 : 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)
⊢ f.mk' x₁ y₁ = f.mk' x₂ y₂
have 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) sorry : (a : ↥S) → Nˣ) y₂)⁻¹ : N) : N))
    ((f : (a : M) → N) (↑y₁ : M) : N)
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]
-- 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 : 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)
⊢ f.mk' x₁ y₁ = f.mk' x₂ y₂
have 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) sorry : (a : ↥S) → Nˣ) y₂)⁻¹ : N) : N)
      ((f : (a : M) → N) (↑y₁ : M) : N))
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]
-- 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 : 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))
⊢ f.mk' x₁ y₁ = f.mk' x₂ y₂
have 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) sorry : (a : ↥S) → Nˣ) y₂)⁻¹ : N) : N))
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]
-- 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 : 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))
⊢ f.mk' x₁ y₁ = f.mk' x₂ y₂
have 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) sorry : (a : ↥S) → Nˣ) y₂)⁻¹ : N)
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]
-- 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 : 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)
⊢ f.mk' x₁ y₁ = f.mk' x₂ y₂
have rw₅ : (f : (a : M) → N) x₁ =
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (x₂ * (↑y₁ : M)) : N)
    ((↑((IsUnit.liftRight (f.toMonoidHom.restrict S) sorry : (a : ↥S) → Nˣ) y₂)⁻¹ : N) : N)
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]
-- 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 : 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)
⊢ f.mk' x₁ y₁ = f.mk' x₂ y₂
have rw₆ : (f : (a : M) → N) x₁ =
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) ((↑y₁ : M) * x₂) : N)
    ((↑((IsUnit.liftRight (f.toMonoidHom.restrict S) sorry : (a : ↥S) → Nˣ) y₂)⁻¹ : N) : N)
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]
-- 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 : 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)
⊢ f.mk' x₁ y₁ = f.mk' x₂ y₂
have rw₇ : (f : (a : M) → N) x₁ =
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) ((↑y₂ : M) * x₁) : N)
    ((↑((IsUnit.liftRight (f.toMonoidHom.restrict S) sorry : (a : ↥S) → Nˣ) y₂)⁻¹ : N) : N)
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]
-- 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 : 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)
⊢ f.mk' x₁ y₁ = f.mk' x₂ y₂
have rw₈ : (f : (a : M) → N) x₁ =
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (x₁ * (↑y₂ : M)) : N)
    ((↑((IsUnit.liftRight (f.toMonoidHom.restrict S) sorry : (a : ↥S) → Nˣ) y₂)⁻¹ : N) : N)
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]
-- 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 : 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)
⊢ f.mk' x₁ y₁ = f.mk' x₂ y₂
have 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) sorry : (a : ↥S) → Nˣ) y₂)⁻¹ : N)
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]