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 : 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)
⊢ f.mk' x₁ y₁ = f.mk' x₂ y₂
have 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)
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)
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)
⊢ f.mk' x₁ y₁ = f.mk' x₂ y₂
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) x₁ : 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
a₁ b₁ : M
a₂ b₂ : ↥S
⊢ f.mk' a₁ a₂ = f.mk' b₁ b₂ ↔ (Localization.r S : (a : M × ↥S) → M × ↥S → Prop) (a₁, a₂) (b₁, b₂)
have rw : (∃ (c : ↥S), (↑c : M) * ((↑b₂ : M) * a₁) = (↑c : M) * ((↑a₂ : M) * b₁)) ↔
  (Localization.r S : (a : M × ↥S) → M × ↥S → Prop) (a₁, a₂) (b₁, b₂)
Tactic: rw [f.eq, Localization.r_iff_exists]
-- 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
a₁ b₁ : M
a₂ b₂ : ↥S
rw :
  (∃ (c : ↥S), (↑c : M) * ((↑b₂ : M) * a₁) = (↑c : M) * ((↑a₂ : M) * b₁)) ↔
    (Localization.r S : (a : M × ↥S) → M × ↥S → Prop) (a₁, a₂) (b₁, b₂)
⊢ f.mk' a₁ a₂ = f.mk' b₁ b₂ ↔ (Localization.r S : (a : M × ↥S) → M × ↥S → Prop) (a₁, a₂) (b₁, b₂)
have rw₁ : (∃ (c : ↥S), (↑c : M) * ((↑b₂ : M) * a₁) = (↑c : M) * ((↑a₂ : M) * b₁)) ↔
  ∃ (c : ↥S), (↑c : M) * ((↑(b₁, b₂).2 : M) * (a₁, a₂).1) = (↑c : M) * ((↑(a₁, a₂).2 : M) * (b₁, b₂).1)
Tactic: rw [f.eq, Localization.r_iff_exists]
-- 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
a : M
b c : ↥S
⊢ a * (↑(b * c) : M) = a * (↑c : M) * (↑b : M)
have rw : a * ((↑b : M) * (↑c : M)) = a * (↑c : M) * (↑b : M)
Tactic: rw [Submonoid.coe_mul, mul_comm (b : M), mul_assoc]
-- 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
a : M
b c : ↥S
rw : a * ((↑b : M) * (↑c : M)) = a * (↑c : M) * (↑b : M)
⊢ a * (↑(b * c) : M) = a * (↑c : M) * (↑b : M)
have rw₁ : a * ((↑c : M) * (↑b : M)) = a * (↑c : M) * (↑b : M)
Tactic: rw [Submonoid.coe_mul, mul_comm (b : M), mul_assoc]
-- 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
a : M
b c : ↥S
rw : a * ((↑b : M) * (↑c : M)) = a * (↑c : M) * (↑b : M)
rw₁ : a * ((↑c : M) * (↑b : M)) = a * (↑c : M) * (↑b : M)
⊢ a * (↑(b * c) : M) = a * (↑c : M) * (↑b : M)
have rw₂ : a * ((↑c : M) * (↑b : M)) = a * ((↑c : M) * (↑b : M))
Tactic: rw [Submonoid.coe_mul, mul_comm (b : M), mul_assoc]
-- 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
a b : M
d : ↥S
⊢ f.mk' a d = f.mk' b d ↔ ∃ (c : ↥S), (↑c : M) * a = (↑c : M) * b
have rw : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) (↑d : M) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) b : N) ((f : (a : M) → N) (↑d : M) : N) ↔
  Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N)
Tactic: rw [mk'_eq_iff_eq', map_mul, map_mul, ← eq_iff_exists f]
-- 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
y : ↥S
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑y : M) : N)
      ((↑((IsUnit.liftRight (f.toMonoidHom.restrict S) ⋯ : (a : ↥S) → Nˣ) y)⁻¹ : N) : N) =
    1
have rw : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (↑y : M) : N) ((f.toMonoidHom : (a : M) → N) (↑y : M) : N)
Tactic: rw [mul_inv_left, mul_one]
-- 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 : ↥S
⊢ HMul.hMul (α := N) ((f : (a : M) → N) x₁ : N) (f.mk' x₂ y) = f.mk' (x₁ * x₂) y
have rw : f.mk' x₁ 1 * f.mk' x₂ y = f.mk' (x₁ * x₂) y
Tactic: rw [← mk'_one, ← mk'_mul, one_mul]
-- 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 : ↥S
rw : f.mk' x₁ 1 * f.mk' x₂ y = f.mk' (x₁ * x₂) y
⊢ HMul.hMul (α := N) ((f : (a : M) → N) x₁ : N) (f.mk' x₂ y) = f.mk' (x₁ * x₂) y
have rw₁ : f.mk' (x₁ * x₂) (1 * y) = f.mk' (x₁ * x₂) y
Tactic: rw [← mk'_one, ← mk'_mul, one_mul]
-- 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 : ↥S
rw : f.mk' x₁ 1 * f.mk' x₂ y = f.mk' (x₁ * x₂) y
rw₁ : f.mk' (x₁ * x₂) (1 * y) = f.mk' (x₁ * x₂) y
⊢ HMul.hMul (α := N) ((f : (a : M) → N) x₁ : N) (f.mk' x₂ y) = f.mk' (x₁ * x₂) y
have rw₂ : f.mk' (x₁ * x₂) y = f.mk' (x₁ * x₂) y
Tactic: rw [← mk'_one, ← mk'_mul, one_mul]
-- 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 : ↥S
⊢ HMul.hMul (β := N) (f.mk' x₂ y) ((f : (a : M) → N) x₁ : N) = f.mk' (x₁ * x₂) y
have rw : HMul.hMul (α := N) ((f : (a : M) → N) x₁ : N) (f.mk' x₂ y) = f.mk' (x₁ * x₂) y
Tactic: rw [mul_comm, mul_mk'_eq_mk'_of_mul]
-- 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 : ↥S
rw : HMul.hMul (α := N) ((f : (a : M) → N) x₁ : N) (f.mk' x₂ y) = f.mk' (x₁ * x₂) y
⊢ HMul.hMul (β := N) (f.mk' x₂ y) ((f : (a : M) → N) x₁ : N) = f.mk' (x₁ * x₂) y
have rw₁ : f.mk' (x₁ * x₂) y = f.mk' (x₁ * x₂) y
Tactic: rw [mul_comm, mul_mk'_eq_mk'_of_mul]
-- 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 : M
y : ↥S
⊢ HMul.hMul (α := N) ((f : (a : M) → N) x : N) (f.mk' 1 y) = f.mk' x y
have rw : f.mk' (x * 1) y = f.mk' x y
Tactic: rw [mul_mk'_eq_mk'_of_mul, mul_one]
-- 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 : M
y : ↥S
rw : f.mk' (x * 1) y = f.mk' x y
⊢ HMul.hMul (α := N) ((f : (a : M) → N) x : N) (f.mk' 1 y) = f.mk' x y
have rw₁ : f.mk' x y = f.mk' x y
Tactic: rw [mul_mk'_eq_mk'_of_mul, mul_one]
-- 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 : M
y : ↥S
⊢ f.mk' (x * (↑y : M)) y = (f : (a : M) → N) x
have rw : HMul.hMul (α := N) ((f : (a : M) → N) (x * (↑y : M)) : N) (f.mk' 1 y) = (f : (a : M) → N) x
Tactic: rw [← mul_mk'_one_eq_mk', map_mul, mul_assoc, mul_mk'_one_eq_mk', mk'_self', mul_one]
-- 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 : M
y : ↥S
rw : HMul.hMul (α := N) ((f : (a : M) → N) (x * (↑y : M)) : N) (f.mk' 1 y) = (f : (a : M) → N) x
⊢ f.mk' (x * (↑y : M)) y = (f : (a : M) → N) x
have rw₁ : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) (↑y : M) : N) * f.mk' 1 y = (f : (a : M) → N) x
Tactic: rw [← mul_mk'_one_eq_mk', map_mul, mul_assoc, mul_mk'_one_eq_mk', mk'_self', mul_one]
-- 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 : M
y : ↥S
rw : HMul.hMul (α := N) ((f : (a : M) → N) (x * (↑y : M)) : N) (f.mk' 1 y) = (f : (a : M) → N) x
rw₁ :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) (↑y : M) : N) * f.mk' 1 y =
    (f : (a : M) → N) x
⊢ f.mk' (x * (↑y : M)) y = (f : (a : M) → N) x
have rw₂ : HMul.hMul (α := N) ((f : (a : M) → N) x : N) (HMul.hMul (α := N) ((f : (a : M) → N) (↑y : M) : N) (f.mk' 1 y)) =
  (f : (a : M) → N) x
Tactic: rw [← mul_mk'_one_eq_mk', map_mul, mul_assoc, mul_mk'_one_eq_mk', mk'_self', mul_one]
-- 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 : M
y : ↥S
rw : HMul.hMul (α := N) ((f : (a : M) → N) (x * (↑y : M)) : N) (f.mk' 1 y) = (f : (a : M) → N) x
rw₁ :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) (↑y : M) : N) * f.mk' 1 y =
    (f : (a : M) → N) x
rw₂ :
  HMul.hMul (α := N) ((f : (a : M) → N) x : N) (HMul.hMul (α := N) ((f : (a : M) → N) (↑y : M) : N) (f.mk' 1 y)) =
    (f : (a : M) → N) x
⊢ f.mk' (x * (↑y : M)) y = (f : (a : M) → N) x
have rw₃ : HMul.hMul (α := N) ((f : (a : M) → N) x : N) (f.mk' (↑y : M) y) = (f : (a : M) → N) x
Tactic: rw [← mul_mk'_one_eq_mk', map_mul, mul_assoc, mul_mk'_one_eq_mk', mk'_self', mul_one]
-- 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 : M
y : ↥S
rw : HMul.hMul (α := N) ((f : (a : M) → N) (x * (↑y : M)) : N) (f.mk' 1 y) = (f : (a : M) → N) x
rw₁ :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) (↑y : M) : N) * f.mk' 1 y =
    (f : (a : M) → N) x
rw₂ :
  HMul.hMul (α := N) ((f : (a : M) → N) x : N) (HMul.hMul (α := N) ((f : (a : M) → N) (↑y : M) : N) (f.mk' 1 y)) =
    (f : (a : M) → N) x
rw₃ : HMul.hMul (α := N) ((f : (a : M) → N) x : N) (f.mk' (↑y : M) y) = (f : (a : M) → N) x
⊢ f.mk' (x * (↑y : M)) y = (f : (a : M) → N) x
have rw₄ : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) (1 : N) = (f : (a : M) → N) x
Tactic: rw [← mul_mk'_one_eq_mk', map_mul, mul_assoc, mul_mk'_one_eq_mk', mk'_self', mul_one]
-- 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 : M
y : ↥S
rw : HMul.hMul (α := N) ((f : (a : M) → N) (x * (↑y : M)) : N) (f.mk' 1 y) = (f : (a : M) → N) x
rw₁ :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) (↑y : M) : N) * f.mk' 1 y =
    (f : (a : M) → N) x
rw₂ :
  HMul.hMul (α := N) ((f : (a : M) → N) x : N) (HMul.hMul (α := N) ((f : (a : M) → N) (↑y : M) : N) (f.mk' 1 y)) =
    (f : (a : M) → N) x
rw₃ : HMul.hMul (α := N) ((f : (a : M) → N) x : N) (f.mk' (↑y : M) y) = (f : (a : M) → N) x
rw₄ : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) (1 : N) = (f : (a : M) → N) x
⊢ f.mk' (x * (↑y : M)) y = (f : (a : M) → N) x
have rw₅ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) x : N)
Tactic: rw [← mul_mk'_one_eq_mk', map_mul, mul_assoc, mul_mk'_one_eq_mk', mk'_self', mul_one]
-- 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 : M
y : ↥S
⊢ f.mk' ((↑y : M) * x) y = (f : (a : M) → N) x
have rw : f.mk' (x * (↑y : M)) y = (f : (a : M) → N) x
Tactic: rw [mul_comm, mk'_mul_cancel_right]
-- 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 : M
y : ↥S
rw : f.mk' (x * (↑y : M)) y = (f : (a : M) → N) x
⊢ f.mk' ((↑y : M) * x) y = (f : (a : M) → N) x
have rw₁ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) x : N)
Tactic: rw [mul_comm, mk'_mul_cancel_right]
-- 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
P : Type u_4
inst_2 : Monoid P
j k : N →* P
h : j.comp f.toMonoidHom = k.comp f.toMonoidHom
⊢ j = k
have h₁ : ∀ (n : N), Eq.{u_4 + 1} (α := P) ((j : (a : N) → P) n : P) ((k : (a : N) → P) n : P)
Tactic: ext n
-- 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
P : Type u_4
inst_2 : Monoid P
j k : N →* P
h : j.comp f.toMonoidHom = k.comp f.toMonoidHom
n : N
⊢ Eq.{u_4 + 1} (α := P) ((j : (a : N) → P) n : P) ((k : (a : N) → P) n : P)
have h₁ : ∀ (m : M) (s : ↥S) (hn : HMul.hMul (β := N) n ((f : (a : M) → N) (↑s : M) : N) = (f : (a : M) → N) m),
  Eq.{u_4 + 1} (α := P) ((j : (a : N) → P) n : P) ((k : (a : N) → P) n : P)
Tactic: obtain ⟨⟨m, s⟩, hn : n * f s = f m⟩ := f.surj n
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (hypothesis)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
f : S.LocalizationMap N
P : Type u_4
inst_2 : Monoid P
j k : N →* P
h : j.comp f.toMonoidHom = k.comp f.toMonoidHom
n : N
m : M
s : ↥S
hn : HMul.hMul (β := N) n ((f : (a : M) → N) (↑s : M) : N) = (f : (a : M) → N) m
⊢ Eq.{u_4 + 1} (α := P) ((j : (a : N) → P) n : P) ((k : (a : N) → P) n : P)
have h₁ : ∀ (a : M),
  Eq.{u_4 + 1} (α := P) ((j : (a : N) → P) ((f : (a : M) → N) a : N) : P)
    ((k : (a : N) → P) ((f : (a : M) → N) a : N) : P)
Tactic: replace h (a) : j (f a) = k (f a) := congr($h a)
Cleared hypotheses: h
-- 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
P : Type u_4
inst_2 : Monoid P
j k : N →* P
n : N
m : M
s : ↥S
hn : HMul.hMul (β := N) n ((f : (a : M) → N) (↑s : M) : N) = (f : (a : M) → N) m
h :
  ∀ (a : M),
    Eq.{u_4 + 1} (α := P) ((j : (a : N) → P) ((f : (a : M) → N) a : N) : P)
      ((k : (a : N) → P) ((f : (a : M) → N) a : N) : P)
⊢ HMul.hMul (α := P) (β := P) ((j : (a : N) → P) n : P) ((j : (a : N) → P) ((f : (a : M) → N) (↑s : M) : N) : P) =
    HMul.hMul (α := P) (β := P) ((k : (a : N) → P) n : P) ((j : (a : N) → P) ((f : (a : M) → N) (↑s : M) : N) : P)
have rw : (j : (a : N) → P) (HMul.hMul (β := N) n ((f : (a : M) → N) (↑s : M) : N)) =
  HMul.hMul (α := P) (β := P) ((k : (a : N) → P) n : P) ((j : (a : N) → P) ((f : (a : M) → N) (↑s : M) : N) : P)
Tactic: rw [← j.map_mul, h, ← k.map_mul, hn, h m]
-- 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
P : Type u_4
inst_2 : Monoid P
j k : N →* P
n : N
m : M
s : ↥S
hn : HMul.hMul (β := N) n ((f : (a : M) → N) (↑s : M) : N) = (f : (a : M) → N) m
h :
  ∀ (a : M),
    Eq.{u_4 + 1} (α := P) ((j : (a : N) → P) ((f : (a : M) → N) a : N) : P)
      ((k : (a : N) → P) ((f : (a : M) → N) a : N) : P)
rw :
  (j : (a : N) → P) (HMul.hMul (β := N) n ((f : (a : M) → N) (↑s : M) : N)) =
    HMul.hMul (α := P) (β := P) ((k : (a : N) → P) n : P) ((j : (a : N) → P) ((f : (a : M) → N) (↑s : M) : N) : P)
⊢ HMul.hMul (α := P) (β := P) ((j : (a : N) → P) n : P) ((j : (a : N) → P) ((f : (a : M) → N) (↑s : M) : N) : P) =
    HMul.hMul (α := P) (β := P) ((k : (a : N) → P) n : P) ((j : (a : N) → P) ((f : (a : M) → N) (↑s : M) : N) : P)
have rw₁ : (j : (a : N) → P) (HMul.hMul (β := N) n ((f : (a : M) → N) (↑s : M) : N)) =
  HMul.hMul (α := P) (β := P) ((k : (a : N) → P) n : P) ((k : (a : N) → P) ((f : (a : M) → N) (↑s : M) : N) : P)
Tactic: rw [← j.map_mul, h, ← k.map_mul, hn, h m]
-- 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
P : Type u_4
inst_2 : Monoid P
j k : N →* P
n : N
m : M
s : ↥S
hn : HMul.hMul (β := N) n ((f : (a : M) → N) (↑s : M) : N) = (f : (a : M) → N) m
h :
  ∀ (a : M),
    Eq.{u_4 + 1} (α := P) ((j : (a : N) → P) ((f : (a : M) → N) a : N) : P)
      ((k : (a : N) → P) ((f : (a : M) → N) a : N) : P)
rw :
  (j : (a : N) → P) (HMul.hMul (β := N) n ((f : (a : M) → N) (↑s : M) : N)) =
    HMul.hMul (α := P) (β := P) ((k : (a : N) → P) n : P) ((j : (a : N) → P) ((f : (a : M) → N) (↑s : M) : N) : P)
rw₁ :
  (j : (a : N) → P) (HMul.hMul (β := N) n ((f : (a : M) → N) (↑s : M) : N)) =
    HMul.hMul (α := P) (β := P) ((k : (a : N) → P) n : P) ((k : (a : N) → P) ((f : (a : M) → N) (↑s : M) : N) : P)
⊢ HMul.hMul (α := P) (β := P) ((j : (a : N) → P) n : P) ((j : (a : N) → P) ((f : (a : M) → N) (↑s : M) : N) : P) =
    HMul.hMul (α := P) (β := P) ((k : (a : N) → P) n : P) ((j : (a : N) → P) ((f : (a : M) → N) (↑s : M) : N) : P)
have rw₂ : Eq.{u_4 + 1} (α := P) ((j : (a : N) → P) (HMul.hMul (β := N) n ((f : (a : M) → N) (↑s : M) : N)) : P)
  ((k : (a : N) → P) (HMul.hMul (β := N) n ((f : (a : M) → N) (↑s : M) : N)) : P)
Tactic: rw [← j.map_mul, h, ← k.map_mul, hn, h m]
-- 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
P : Type u_4
inst_2 : Monoid P
j k : N →* P
n : N
m : M
s : ↥S
hn : HMul.hMul (β := N) n ((f : (a : M) → N) (↑s : M) : N) = (f : (a : M) → N) m
h :
  ∀ (a : M),
    Eq.{u_4 + 1} (α := P) ((j : (a : N) → P) ((f : (a : M) → N) a : N) : P)
      ((k : (a : N) → P) ((f : (a : M) → N) a : N) : P)
rw :
  (j : (a : N) → P) (HMul.hMul (β := N) n ((f : (a : M) → N) (↑s : M) : N)) =
    HMul.hMul (α := P) (β := P) ((k : (a : N) → P) n : P) ((j : (a : N) → P) ((f : (a : M) → N) (↑s : M) : N) : P)
rw₁ :
  (j : (a : N) → P) (HMul.hMul (β := N) n ((f : (a : M) → N) (↑s : M) : N)) =
    HMul.hMul (α := P) (β := P) ((k : (a : N) → P) n : P) ((k : (a : N) → P) ((f : (a : M) → N) (↑s : M) : N) : P)
rw₂ :
  Eq.{u_4 + 1} (α := P) ((j : (a : N) → P) (HMul.hMul (β := N) n ((f : (a : M) → N) (↑s : M) : N)) : P)
    ((k : (a : N) → P) (HMul.hMul (β := N) n ((f : (a : M) → N) (↑s : M) : N)) : P)
⊢ HMul.hMul (α := P) (β := P) ((j : (a : N) → P) n : P) ((j : (a : N) → P) ((f : (a : M) → N) (↑s : M) : N) : P) =
    HMul.hMul (α := P) (β := P) ((k : (a : N) → P) n : P) ((j : (a : N) → P) ((f : (a : M) → N) (↑s : M) : N) : P)
have rw₃ : Eq.{u_4 + 1} (α := P) ((j : (a : N) → P) ((f : (a : M) → N) m : N) : P)
  ((k : (a : N) → P) ((f : (a : M) → N) m : N) : P)
Tactic: rw [← j.map_mul, h, ← k.map_mul, hn, h m]