awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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)
rw₅ 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)

Tactic:
rw [map_mul f, map_mul f, f.mk'_eq_iff_eq_mul.1 H, ← mul_assoc, mk'_spec', mul_comm (f x₂)]

Premises used: mul_assoc, map_mul, Submonoid.LocalizationMap.mk'_spec', Iff.mp, mul_comm, DFunLike.coe, Submonoid.LocalizationMap.mk'_eq_iff_eq_mul
-- 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
⊢ f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔
    Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (x₁ * (↑y₂ : M)) : N) ((f : (a : M) → N) (x₂ * (↑y₁ : M)) : N)

Tactic:
simp only [f.mk'_eq_iff_eq, mul_comm]

Premises used: Submonoid.LocalizationMap.mk'_eq_iff_eq, mul_comm
-- 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
a₁ b₁ : M
a₂ b₂ : ↥S
⊢ f.mk' a₁ a₂ = f.mk' b₁ b₂ ↔ ∃ (c : ↥S), (↑c : M) * ((↑b₂ : M) * a₁) = (↑c : M) * ((↑a₂ : M) * b₁)

Tactic:
f.mk'_eq_iff_eq.trans <| f.eq_iff_exists

Premises used: Submonoid.LocalizationMap.mk'_eq_iff_eq, Submonoid.LocalizationMap.eq_iff_exists, Iff.trans
-- 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
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₂)
rw₁ 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)
⊢ f.mk' a₁ a₂ = f.mk' b₁ b₂ ↔ (Localization.r S : (a : M × ↥S) → M × ↥S → Prop) (a₁, a₂) (b₁, b₂)

Tactic:
rw [f.eq, Localization.r_iff_exists]

Premises used: Localization.r_iff_exists, Submonoid.LocalizationMap.eq
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
f : S.LocalizationMap N
g : S.LocalizationMap P
x y : M
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N) ↔
    Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) x : P) ((g : (a : M) → P) y : P)

Tactic:
f.eq_iff_exists.trans g.eq_iff_exists.symm

Premises used: Submonoid.LocalizationMap.eq_iff_exists, Iff.trans, Iff.symm
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
f : S.LocalizationMap N
g : S.LocalizationMap P
x₁ x₂ : M
y₁ y₂ : ↥S
⊢ f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ g.mk' x₁ y₁ = g.mk' x₂ y₂

Tactic:
f.eq'.trans g.eq'.symm

Premises used: Submonoid.LocalizationMap.eq', Iff.trans, Iff.symm
-- 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 : M
y : ↥S
⊢ ∃ (c : ↥S), (↑c : M) * ((↑(f.sec (f.mk' x y)).2 : M) * x) = (↑c : M) * ((↑y : M) * (f.sec (f.mk' x y)).1)

Tactic:
f.eq_iff_exists.1 <| f.mk'_eq_iff_eq.1 <| (mk'_sec _ _).symm

Premises used: Submonoid.LocalizationMap.mk'_eq_iff_eq, Submonoid.LocalizationMap.eq_iff_exists, Iff.mp, Eq.symm, Submonoid.LocalizationMap.mk'_sec
-- 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
a₁ b₁ : M
a₂ b₂ : ↥S
H : (↑a₂ : M) * b₁ = (↑b₂ : M) * a₁
⊢ f.mk' a₁ a₂ = f.mk' b₁ b₂

Tactic:
f.mk'_eq_iff_eq.2 <| H ▸ rfl

Premises used: Iff.mpr, Submonoid.LocalizationMap.mk'_eq_iff_eq, Eq.rec, rfl
-- 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
a₁ b₁ : M
a₂ b₂ : ↥S
H : b₁ * (↑a₂ : M) = a₁ * (↑b₂ : M)
⊢ (↑a₂ : M) * b₁ = (↑b₂ : M) * a₁

Tactic:
simpa only [mul_comm] using H

Premises used: mul_comm
-- 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
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)
rw₂ rw₃ : a * ((↑c : M) * (↑b : M)) = a * ((↑c : M) * (↑b : M))
⊢ a * (↑(b * c) : M) = a * (↑c : M) * (↑b : M)

Tactic:
rw [Submonoid.coe_mul, mul_comm (b : M), mul_assoc]

Premises used: mul_assoc, mul_comm, Subtype.val, Submonoid.coe_mul
-- 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
a b : M
d : ↥S
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)
⊢ f.mk' a d = f.mk' b d ↔ ∃ (c : ↥S), (↑c : M) * a = (↑c : M) * b

Tactic:
rw [mk'_eq_iff_eq', map_mul, map_mul, ← eq_iff_exists f]

Premises used: Submonoid.LocalizationMap.eq_iff_exists, map_mul, Submonoid.LocalizationMap.mk'_eq_iff_eq'
-- 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
a b : M
d : ↥S
⊢ 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:
(map_units f d).mul_left_inj

Premises used: IsUnit.mul_left_inj, Submonoid.LocalizationMap.map_units
-- 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
a b : M
d : ↥S
⊢ 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:
exact (map_units f d).mul_left_inj

Premises used: IsUnit.mul_left_inj, Submonoid.LocalizationMap.map_units
-- 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
y : ↥S
rw : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (↑y : M) : N) ((f.toMonoidHom : (a : M) → N) (↑y : M) : N)
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑y : M) : N)
      ((↑((IsUnit.liftRight (f.toMonoidHom.restrict S) ⋯ : (a : ↥S) → Nˣ) y)⁻¹ : N) : N) =
    1

Tactic:
rw [mul_inv_left, mul_one]

Premises used: Submonoid.LocalizationMap.mul_inv_left, mul_one
-- 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
y : ↥S
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (↑y : M) : N) ((f.toMonoidHom : (a : M) → N) (↑y : M) : N)

Tactic:
dsimp
-- 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 : M
H : x ∈ S
⊢ f.mk' x (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x H) = 1

Tactic:
mk'_self' f ⟨x, H⟩

Premises used: Subtype.mk, Submonoid.LocalizationMap.mk'_self'
-- 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 : ↥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
rw₂ rw₃ : f.mk' (x₁ * 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

Tactic:
rw [← mk'_one, ← mk'_mul, one_mul]

Premises used: Submonoid.LocalizationMap.mk'_one, Submonoid.LocalizationMap.mk'_mul, one_mul
-- 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 : ↥S
rw : HMul.hMul (α := N) ((f : (a : M) → N) x₁ : N) (f.mk' x₂ y) = f.mk' (x₁ * x₂) y
rw₁ rw₂ : f.mk' (x₁ * 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

Tactic:
rw [mul_comm, mul_mk'_eq_mk'_of_mul]

Premises used: Submonoid.LocalizationMap.mul_mk'_eq_mk'_of_mul, mul_comm
-- 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 : M
y : ↥S
rw : f.mk' (x * 1) y = f.mk' x y
rw₁ rw₂ : f.mk' x y = f.mk' x y
⊢ HMul.hMul (α := N) ((f : (a : M) → N) x : N) (f.mk' 1 y) = f.mk' x y

Tactic:
rw [mul_mk'_eq_mk'_of_mul, mul_one]

Premises used: Submonoid.LocalizationMap.mul_mk'_eq_mk'_of_mul, mul_one
-- 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 : 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
rw₅ rw₆ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) x : N)
⊢ f.mk' (x * (↑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]

Premises used: mul_assoc, map_mul, Submonoid.LocalizationMap.mul_mk'_one_eq_mk', mul_one, Submonoid.LocalizationMap.mk'_self'
-- 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 : M
y : ↥S
rw : f.mk' (x * (↑y : M)) y = (f : (a : M) → N) x
rw₁ rw₂ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) x : N)
⊢ f.mk' ((↑y : M) * x) y = (f : (a : M) → N) x

Tactic:
rw [mul_comm, mk'_mul_cancel_right]

Premises used: Submonoid.LocalizationMap.mk'_mul_cancel_right, mul_comm
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
f : S.LocalizationMap N
j : N →* P
y : ↥S
⊢ IsUnit.{u_3} (M := P) ((j.comp f.toMonoidHom : (a : M) → P) (↑y : M) : P)

Tactic:
⟨Units.map j <| IsUnit.liftRight (f.toMonoidHom.restrict S) f.map_units y,
    show j _ = j _ from congr_arg j (IsUnit.coe_liftRight (f.toMonoidHom.restrict S) f.map_units _)⟩

Premises used: IsUnit.liftRight, IsUnit, MonoidHom.restrict, IsUnit.coe_liftRight, Submonoid.LocalizationMap.toMonoidHom, congr_arg, Exists.intro, Submonoid.LocalizationMap.map_units, DFunLike.coe, Units.map
-- 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
P : Type u_4
inst_2 : Monoid P
j k : N →* P
h : j.comp f.toMonoidHom = k.comp f.toMonoidHom
h₁ : ∀ (n : N), Eq.{u_4 + 1} (α := P) ((j : (a : N) → P) n : P) ((k : (a : N) → P) n : P)
⊢ j = k

Tactic:
ext n
-- 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
P : Type u_4
inst_2 : Monoid P
j k : N →* P
h : j.comp f.toMonoidHom = k.comp f.toMonoidHom
n : N
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)
⊢ 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

Premises used: Submonoid.LocalizationMap.surj
-- 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
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
⊢ ∀ (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)
-- 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
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)
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)
rw₄ rw₅ :
  Eq.{u_4 + 1} (α := P) ((k : (a : N) → P) ((f : (a : M) → N) m : N) : P)
    ((k : (a : N) → P) ((f : (a : M) → N) 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)

Tactic:
rw [← j.map_mul, h, ← k.map_mul, hn, h m]

Premises used: MonoidHom.map_mul
-- 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
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)
⊢ Eq.{u_4 + 1} (α := P) ((j : (a : N) → P) n : P) ((k : (a : N) → P) n : P)

Tactic:
exact ((f.map_units s).map j).mul_left_inj.mp <| by rw [← j.map_mul, h, ← k.map_mul, hn, h m]

Premises used: Iff.mp, IsUnit.map, IsUnit.mul_left_inj, Submonoid.LocalizationMap.map_units
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
x y : M
rw : mk (x * y) 1 = mk (x * y) (HMul.hMul (α := ↥S) 1 1)
rw₁ rw₂ : Eq (α := Localization S) (mk (x * y) 1) (mk (x * y) 1)
⊢ mk (x * y) 1 = HMul.hMul (α := Localization S) (mk x 1) (mk y 1)

Tactic:
rw [mk_mul, mul_one]

Premises used: Localization.mk_mul, mul_one
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
y : ↥S
rw : mk ((↑y : M) * 1) (1 * y) = 1
rw₁ : mk (↑y : M) (1 * y) = 1
rw₂ : mk (↑y : M) y = 1
rw₃ rw₄ : Eq.{u_1 + 1} (α := Localization S) 1 1
⊢ mk (↑y : M) 1 * mk 1 y = 1

Tactic:
rw [mk_mul, mul_one, one_mul, mk_self]

Premises used: Localization.mk_self, Localization.mk_mul, mul_one, one_mul
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
z : Localization S
x : M × ↥S
rw : mk (x.1 * (↑x.2 : M)) (x.2 * 1) = mk x.1 1
rw₁ : mk ((↑x.2 : M) * x.1) (x.2 * 1) = mk x.1 1
rw₂ : mk (↑x.2 : M) x.2 * mk x.1 1 = mk x.1 1
rw₃ : HMul.hMul (α := Localization S) 1 (mk x.1 1) = mk x.1 1
rw₄ rw₅ : Eq (α := Localization S) (mk x.1 1) (mk x.1 1)
⊢ mk x.1 x.2 * mk (↑x.2 : M) 1 = mk x.1 1

Tactic:
rw [mk_mul, mul_comm x.fst, ← mk_mul, mk_self, one_mul]

Premises used: Prod.fst, Localization.mk_self, mul_comm, Localization.mk_mul, one_mul
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
x y : M
⊢ (∃ (c : ↥S), (↑c : M) * ((↑(y, 1).2 : M) * (x, 1).1) = (↑c : M) * ((↑(x, 1).2 : M) * (y, 1).1)) ↔
    ∃ (c : ↥S), (↑c : M) * x = (↑c : M) * y

Tactic:
simp
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x : M
⊢ Eq (α := Localization S) (mk x 1) ((monoidOf S : (a : M) → Localization S) x)

Tactic:
rfl

Premises used: Localization.mk, Quotient.mk', OreLocalization.oreDiv, rfl
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x : M
y : ↥S
rw : mk (x * (↑y : M)) (1 * y) = mk x 1
⊢ HMul.hMul (β := Localization S) (mk x y) ((monoidOf S : (a : M) → Localization S) (↑y : M) : Localization S) =
    (monoidOf S : (a : M) → Localization S) x

Tactic:
rw [← mk_one_eq_monoidOf_mk, ← mk_one_eq_monoidOf_mk, mk_mul x y y 1, mul_comm y 1]

Premises used: Localization.mk_one_eq_monoidOf_mk, mul_comm, Localization.mk_mul, OfNat.ofNat, Subtype.val
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x : M
y : ↥S
rhs : mk x 1
| mk (x * (↑y : M)) (1 * y) = mk x 1

Tactic:
rhs
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x : M
y : ↥S
rw : mk x (HMul.hMul (α := ↥S) 1 1)
| mk x 1

Tactic:
rw [← mul_one 1]

Premises used: mul_one, OfNat.ofNat
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x : M
y : ↥S
rw : mk (x * 1) (HMul.hMul (α := ↥S) 1 1)
| mk x (HMul.hMul (α := ↥S) 1 1)

Tactic:
rw [← mul_one x]

Premises used: mul_one
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x : M
y : ↥S
rw : mk (x * 1) (HMul.hMul (α := ↥S) 1 1)
| mk (x * (↑y : M)) (1 * y) = mk x 1

Tactic:
rhs; rw [← mul_one 1]; rw [← mul_one x]

Premises used: mul_one, OfNat.ofNat
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x : M
y : ↥S
conv : mk (x * (↑y : M)) (1 * y) = mk (x * 1) (HMul.hMul (α := ↥S) 1 1)
⊢ mk (x * (↑y : M)) (1 * y) = mk x 1

Tactic:
conv => rhs; rw [← mul_one 1]; rw [← mul_one x]

Premises used: mul_one, OfNat.ofNat
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x : M
y : ↥S
⊢ mk (x * (↑y : M)) (1 * y) = mk (x * 1) (HMul.hMul (α := ↥S) 1 1)

Tactic:
mk_eq_mk_iff.2 (Con.symm _ <| (Localization.r S).mul (Con.refl _ (x, 1)) <| one_rel _)

Premises used: Iff.mpr, Localization.one_rel, Con.mul, Localization.r, Con.refl, Prod.mk, Con.symm, OfNat.ofNat, Localization.mk_eq_mk_iff
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x : M
y : ↥S
⊢ mk (x * (↑y : M)) (1 * y) = mk (x * 1) (HMul.hMul (α := ↥S) 1 1)

Tactic:
exact mk_eq_mk_iff.2 (Con.symm _ <| (Localization.r S).mul (Con.refl _ (x, 1)) <| one_rel _)

Premises used: Iff.mpr, Localization.one_rel, Con.mul, Localization.r, Con.refl, Prod.mk, Con.symm, OfNat.ofNat, Localization.mk_eq_mk_iff
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
⊢ mk = (monoidOf S).mk'

Tactic:
funext fun _ ↦ funext fun _ ↦ mk_eq_monoidOf_mk'_apply _ _

Premises used: Localization.mk_eq_monoidOf_mk'_apply, funext
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
p : Sort u
f : M → ↥S → p
H : ∀ {a c : M} {b d : ↥S}, (r S : (a : M × ↥S) → M × ↥S → Prop) (a, b) (c, d) → f a b = f c d
a : M
b : ↥S
rw : (mk a b).liftOn f @H = f a b
rw₁ rw₂ : f a b = f a b
⊢ ((monoidOf S).mk' a b).liftOn f @H = f a b

Tactic:
rw [← mk_eq_monoidOf_mk', liftOn_mk]

Premises used: Localization.mk_eq_monoidOf_mk', Localization.liftOn_mk
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
p : Sort u_4
f : M → ↥S → M → ↥S → p
H :
  ∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥S},
    (r S : (a : M × ↥S) → M × ↥S → Prop) (a, b) (a', b') →
      (r S : (a : M × ↥S) → M × ↥S → Prop) (c, d) (c', d') → f a b c d = f a' b' c' d'
a c : M
b d : ↥S
rw : (mk a b).liftOn₂ (mk c d) f @H = f a b c d
rw₁ rw₂ : f a b c d = f a b c d
⊢ ((monoidOf S).mk' a b).liftOn₂ ((monoidOf S).mk' c d) f @H = f a b c d

Tactic:
rw [← mk_eq_monoidOf_mk', liftOn₂_mk]

Premises used: Localization.mk_eq_monoidOf_mk', Localization.liftOn₂_mk
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
inst_3 : IsMulTorsionFree M
n : ℕ
hn : n ≠ 0
a₁ : Localization S
a : M × ↥S
a₂ : Localization S
b : M × ↥S
hab : Localization.mk a.1 a.2 ^ n = Localization.mk b.1 b.2 ^ n
mk : Localization.mk a.1 a.2 = Localization.mk b.1 b.2
⊢ Eq (α := Localization S) (Quot.mk (⇑(OreLocalization.oreEqv S M) : M × ↥S → M × ↥S → Prop) a)
    (Quot.mk (⇑(OreLocalization.oreEqv S M) : M × ↥S → M × ↥S → Prop) b)

Tactic:
change mk a.1 a.2 = mk b.1 b.2

Premises used: Localization.mk, Prod.fst, Prod.snd