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 y : M
h_1 : ∃ (c : ↥S), (↑c : M) * x = (↑c : M) * y
c : ↥S
h : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) ((↑c : M) * x) : N) ((f : (a : M) → N) ((↑c : M) * y) : N)
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑c : M) : N) ((f : (a : M) → N) x : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑c : M) : N) ((f : (a : M) → N) y : N)

Tactic:
rw [map_mul, map_mul] at h

Premises used: 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
x y : M
h_1 : ∃ (c : ↥S), (↑c : M) * x = (↑c : M) * y
c : ↥S
h :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑c : M) : N) ((f : (a : M) → N) x : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑c : M) : N) ((f : (a : M) → N) y : N)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)

Tactic:
(f.map_units c).mul_right_inj.mp h

Premises used: IsUnit.mul_right_inj, Iff.mp, 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
x y : M
h_1 : ∃ (c : ↥S), (↑c : M) * x = (↑c : M) * y
c : ↥S
h :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑c : M) : N) ((f : (a : M) → N) x : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑c : M) : N) ((f : (a : M) → N) y : N)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)

Tactic:
exact (f.map_units c).mul_right_inj.mp h

Premises used: IsUnit.mul_right_inj, Iff.mp, 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
z : N
⊢ HMul.hMul (β := N) z ((f : (a : M) → N) (↑(f.sec z).2 : M) : N) = (f : (a : M) → N) (f.sec z).1

Tactic:
Classical.choose_spec <| f.surj z

Premises used: Classical.choose_spec, 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
z : N
rw : (f : (a : M) → N) (f.sec z).1 = HMul.hMul (β := N) z ((f : (a : M) → N) (↑(f.sec z).2 : M) : N)
rw₁ rw₂ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (f.sec z).1 : N) ((f : (a : M) → N) (f.sec z).1 : N)
⊢ (f : (a : M) → N) (f.sec z).1 = HMul.hMul (α := N) ((f : (a : M) → N) (↑(f.sec z).2 : M) : N) z

Tactic:
rw [mul_comm, sec_spec]

Premises used: mul_comm, Submonoid.LocalizationMap.sec_spec
-- 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 : M →* N
h : ∀ (y : ↥S), IsUnit.{u_2} (M := N) ((f : (a : M) → N) (↑y : M) : N)
y : ↥S
w z : N
rw :
  (↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y)⁻¹ : N) * w = z ↔
    w = HMul.hMul (α := N) ((f : (a : M) → N) (↑y : M) : N) z
⊢ w * (↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y)⁻¹ : N) = z ↔
    w = HMul.hMul (α := N) ((f : (a : M) → N) (↑y : M) : N) z

Tactic:
rw [mul_comm]

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 : M →* N
h : ∀ (y : ↥S), IsUnit.{u_2} (M := N) ((f : (a : M) → N) (↑y : M) : N)
y : ↥S
w z : N
⊢ (↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y)⁻¹ : N) * w = z ↔
    w = HMul.hMul (α := N) ((f : (a : M) → N) (↑y : M) : N) z

Tactic:
Units.inv_mul_eq_iff_eq_mul (IsUnit.liftRight (f.restrict S) h y)

Premises used: IsUnit.liftRight, MonoidHom.restrict, Units.inv_mul_eq_iff_eq_mul, DFunLike.coe
-- 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 : M →* N
h : ∀ (y : ↥S), IsUnit.{u_2} (M := N) ((f : (a : M) → N) (↑y : M) : N)
y : ↥S
w z : N
⊢ (↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y)⁻¹ : N) * w = z ↔
    w = HMul.hMul (α := N) ((f : (a : M) → N) (↑y : M) : N) z

Tactic:
exact Units.inv_mul_eq_iff_eq_mul (IsUnit.liftRight (f.restrict S) h y)

Premises used: IsUnit.liftRight, MonoidHom.restrict, Units.inv_mul_eq_iff_eq_mul, DFunLike.coe
-- 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 : M →* N
h : ∀ (y : ↥S), IsUnit.{u_2} (M := N) ((f : (a : M) → N) (↑y : M) : N)
y : ↥S
w z : N
rw :
  w * (↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y)⁻¹ : N) = z ↔
    HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N) = w
rw₁ :
  w = HMul.hMul (α := N) ((f : (a : M) → N) (↑y : M) : N) z ↔ HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N) = w
rw₂ :
  w = HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N) ↔ HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N) = w
rw₃ rw₄ :
  HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N) = w ↔ HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N) = w
⊢ z = w * (↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y)⁻¹ : N) ↔
    HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N) = w

Tactic:
rw [eq_comm, mul_inv_left h, mul_comm, eq_comm]

Premises used: eq_comm, mul_comm, Submonoid.LocalizationMap.mul_inv_left
-- 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 : M →* N
hf : ∀ (y : ↥S), IsUnit.{u_2} (M := N) ((f : (a : M) → N) (↑y : M) : N)
y z : ↥S
h :
  Eq.{u_2 + 1} (α := Nˣ) (((IsUnit.liftRight (f.restrict S) hf : (a : ↥S) → Nˣ) y)⁻¹ : Nˣ)
    (((IsUnit.liftRight (f.restrict S) hf : (a : ↥S) → Nˣ) z)⁻¹ : Nˣ)
rw :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑z : M) : N)
      ((↑((IsUnit.liftRight (f.restrict S) hf : (a : ↥S) → Nˣ) z)⁻¹ : N) : N) =
    1
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (↑y : M) : N) ((f : (a : M) → N) (↑z : M) : N)

Tactic:
rw [← mul_one (f y), eq_comm, ← mul_inv_left hf y (f z) 1, h]

Premises used: eq_comm, Submonoid.LocalizationMap.mul_inv_left, mul_one, OfNat.ofNat, Subtype.val, DFunLike.coe
-- 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 : M →* N
hf : ∀ (y : ↥S), IsUnit.{u_2} (M := N) ((f : (a : M) → N) (↑y : M) : N)
y z : ↥S
h :
  Eq.{u_2 + 1} (α := Nˣ) (((IsUnit.liftRight (f.restrict S) hf : (a : ↥S) → Nˣ) y)⁻¹ : Nˣ)
    (((IsUnit.liftRight (f.restrict S) hf : (a : ↥S) → Nˣ) z)⁻¹ : Nˣ)
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑z : M) : N)
      ((↑((IsUnit.liftRight (f.restrict S) hf : (a : ↥S) → Nˣ) z)⁻¹ : N) : N) =
    1

Tactic:
Units.inv_mul (IsUnit.liftRight (f.restrict S) hf z)⁻¹

Premises used: IsUnit.liftRight, Units.inv_mul, MonoidHom.restrict, Inv.inv, DFunLike.coe
-- 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 : M →* N
hf : ∀ (y : ↥S), IsUnit.{u_2} (M := N) ((f : (a : M) → N) (↑y : M) : N)
y z : ↥S
h :
  Eq.{u_2 + 1} (α := Nˣ) (((IsUnit.liftRight (f.restrict S) hf : (a : ↥S) → Nˣ) y)⁻¹ : Nˣ)
    (((IsUnit.liftRight (f.restrict S) hf : (a : ↥S) → Nˣ) z)⁻¹ : Nˣ)
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑z : M) : N)
      ((↑((IsUnit.liftRight (f.restrict S) hf : (a : ↥S) → Nˣ) z)⁻¹ : N) : N) =
    1

Tactic:
exact Units.inv_mul (IsUnit.liftRight (f.restrict S) hf z)⁻¹

Premises used: IsUnit.liftRight, Units.inv_mul, MonoidHom.restrict, Inv.inv, DFunLike.coe
-- 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 : M →* N
h : ∀ (y : ↥S), IsUnit.{u_2} (M := N) ((f : (a : M) → N) (↑y : M) : N)
y : ↥S
z : N
H : HMul.hMul (α := N) ((f : (a : M) → N) (↑y : M) : N) z = 1
rw : (↑1 : N) = HMul.hMul (α := N) ((f : (a : M) → N) (↑y : M) : N) z
⊢ (↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y)⁻¹ : N) = z

Tactic:
rw [← one_mul _⁻¹, Units.val_mul, mul_inv_left]

Premises used: Inv.inv, Submonoid.LocalizationMap.mul_inv_left, Units.val_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 : M →* N
h : ∀ (y : ↥S), IsUnit.{u_2} (M := N) ((f : (a : M) → N) (↑y : M) : N)
y : ↥S
z : N
H : HMul.hMul (α := N) ((f : (a : M) → N) (↑y : M) : N) z = 1
⊢ (↑1 : N) = HMul.hMul (α := N) ((f : (a : M) → N) (↑y : M) : N) z

Tactic:
H.symm

Premises used: Eq.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 : M →* N
h : ∀ (y : ↥S), IsUnit.{u_2} (M := N) ((f : (a : M) → N) (↑y : M) : N)
y : ↥S
z : N
H : HMul.hMul (α := N) ((f : (a : M) → N) (↑y : M) : N) z = 1
⊢ (↑1 : N) = HMul.hMul (α := N) ((f : (a : M) → N) (↑y : M) : N) z

Tactic:
exact H.symm

Premises used: Eq.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 y : M
c : ↥S
h : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) ((↑c : M) * x) : N) ((f : (a : M) → N) ((↑c : M) * y) : N)
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑c : M) : N) ((f : (a : M) → N) x : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑c : M) : N) ((f : (a : M) → N) y : N)

Tactic:
rw [map_mul, map_mul] at h

Premises used: 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
x y : M
c : ↥S
h :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑c : M) : N) ((f : (a : M) → N) x : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑c : M) : N) ((f : (a : M) → N) y : N)
let :
  ∀ (u : Nˣ) (hu : (↑u : N) = (f : (a : M) → N) (↑c : M)),
    Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)

Tactic:
let ⟨u, hu⟩ := f.map_units c
-- 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 y : M
c : ↥S
h :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑c : M) : N) ((f : (a : M) → N) x : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑c : M) : N) ((f : (a : M) → N) y : N)
u : Nˣ
hu : (↑u : N) = (f : (a : M) → N) (↑c : M)
⊢ HMul.hMul (β := N) (↑u : N) ((f : (a : M) → N) x : N) = HMul.hMul (β := N) (↑u : N) ((f : (a : M) → N) y : N)

Tactic:
rw [← hu] at h
-- 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 y : M
c : ↥S
h :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑c : M) : N) ((f : (a : M) → N) x : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑c : M) : N) ((f : (a : M) → N) y : N)
u : Nˣ
hu : (↑u : N) = (f : (a : M) → N) (↑c : M)
h₁ : HMul.hMul (β := N) (↑u : N) ((f : (a : M) → N) x : N) = HMul.hMul (β := N) (↑u : N) ((f : (a : M) → N) y : N)
⊢ (↑u : N) = (f : (a : M) → N) (↑c : M)

Tactic:
rw [← hu] at h
-- 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 y : M
c : ↥S
u : Nˣ
h : HMul.hMul (β := N) (↑u : N) ((f : (a : M) → N) x : N) = HMul.hMul (β := N) (↑u : N) ((f : (a : M) → N) y : N)
hu : (↑u : N) = (f : (a : M) → N) (↑c : M)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)

Tactic:
(Units.mul_right_inj u).1 h

Premises used: Iff.mp, Units.mul_right_inj
-- 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 y : M
c : ↥S
u : Nˣ
h : HMul.hMul (β := N) (↑u : N) ((f : (a : M) → N) x : N) = HMul.hMul (β := N) (↑u : N) ((f : (a : M) → N) y : N)
hu : (↑u : N) = (f : (a : M) → N) (↑c : M)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)

Tactic:
exact (Units.mul_right_inj u).1 h

Premises used: Iff.mp, Units.mul_right_inj
-- 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 y : M
c : ↥S
h : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (x * (↑c : M)) : N) ((f : (a : M) → N) (y * (↑c : M)) : N)
rw : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (x * (↑c : M)) : N) ((f : (a : M) → N) ((↑c : M) * y) : N)
rw₁ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (x * (↑c : M)) : N) ((f : (a : M) → N) (y * (↑c : M)) : N)
rw₂ rw₃ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (y * (↑c : M)) : N) ((f : (a : M) → N) (y * (↑c : M)) : N)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) ((↑c : M) * x) : N) ((f : (a : M) → N) ((↑c : M) * y) : N)

Tactic:
rw [mul_comm _ x, mul_comm _ y, 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
x₁ x₂ : M
y₁ y₂ : ↥S
⊢ f.mk' (x₁ * x₂) (y₁ * y₂) = f.mk' x₁ y₁ * f.mk' x₂ y₂

Tactic:
(mul_inv_left f.map_units _ _ _).2 ?_

Premises used: Iff.mpr, Submonoid.LocalizationMap.mk', Submonoid.LocalizationMap.mul_inv_left, 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
x₁ x₂ : M
y₁ y₂ : ↥S
refine :
  (f : (a : M) → N) (x₁ * x₂) =
    HMul.hMul (α := N) ((f.toMonoidHom : (a : M) → N) (↑(y₁ * y₂) : M) : N) (f.mk' x₁ y₁ * f.mk' x₂ y₂)
⊢ f.mk' (x₁ * x₂) (y₁ * y₂) = f.mk' x₁ y₁ * f.mk' x₂ y₂

Tactic:
refine (mul_inv_left f.map_units _ _ _).2 ?_

Premises used: Iff.mpr, Submonoid.LocalizationMap.mul_inv_left, 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
x₁ x₂ : M
y₁ y₂ : ↥S
simp :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₁ : N) ((f : (a : M) → N) x₂ : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑y₁ : M) : N) ((f : (a : M) → N) (↑y₂ : M) : N) *
      (HMul.hMul (α := N) ((f : (a : M) → N) x₁ : N) (↑(IsUnit.unit (a := (f : (a : M) → N) (↑y₁ : M)) ⋯)⁻¹ : N) *
        HMul.hMul (α := N) ((f : (a : M) → N) x₂ : N) (↑(IsUnit.unit (a := (f : (a : M) → N) (↑y₂ : M)) ⋯)⁻¹ : N))
⊢ (f : (a : M) → N) (x₁ * x₂) =
    HMul.hMul (α := N) ((f.toMonoidHom : (a : M) → N) (↑(y₁ * y₂) : M) : N) (f.mk' x₁ y₁ * f.mk' x₂ y₂)

Tactic:
simp only [map_mul, coe_mul, toMonoidHom_apply, mk', IsUnit.liftRight, Units.liftRight,
    MonoidHom.restrict_apply, MonoidHom.coe_mk, OneHom.coe_mk]

Premises used: IsUnit.liftRight, Submonoid.LocalizationMap.mk', OneHom.coe_mk, MonoidHom.restrict_apply, map_mul, MonoidHom.coe_mk, Units.liftRight, Submonoid.LocalizationMap.toMonoidHom_apply, 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
x₁ x₂ : M
y₁ y₂ : ↥S
rw :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₁ : N) ((f : (a : M) → N) x₂ : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₁ : N) ((f : (a : M) → N) x₂ : N) *
      (HMul.hMul (α := N) ((f : (a : M) → N) (↑y₁ : M) : N)
          (↑(IsUnit.unit (a := (f : (a : M) → N) (↑y₁ : M)) ⋯)⁻¹ : N) *
        HMul.hMul (α := N) ((f : (a : M) → N) (↑y₂ : M) : N)
          (↑(IsUnit.unit (a := (f : (a : M) → N) (↑y₂ : M)) ⋯)⁻¹ : N))
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₁ : N) ((f : (a : M) → N) x₂ : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑y₁ : M) : N) ((f : (a : M) → N) (↑y₂ : M) : N) *
      (HMul.hMul (α := N) ((f : (a : M) → N) x₁ : N) (↑(IsUnit.unit (a := (f : (a : M) → N) (↑y₁ : M)) ⋯)⁻¹ : N) *
        HMul.hMul (α := N) ((f : (a : M) → N) x₂ : N) (↑(IsUnit.unit (a := (f : (a : M) → N) (↑y₂ : M)) ⋯)⁻¹ : N))

Tactic:
rw [mul_mul_mul_comm (f x₁), mul_left_comm, mul_mul_mul_comm (f y₁)]

Premises used: mul_mul_mul_comm, mul_left_comm, Subtype.val, DFunLike.coe
-- 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
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₁ : N) ((f : (a : M) → N) x₂ : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₁ : N) ((f : (a : M) → N) x₂ : N) *
      (HMul.hMul (α := N) ((f : (a : M) → N) (↑y₁ : M) : N)
          (↑(IsUnit.unit (a := (f : (a : M) → N) (↑y₁ : M)) ⋯)⁻¹ : N) *
        HMul.hMul (α := N) ((f : (a : M) → N) (↑y₂ : M) : N)
          (↑(IsUnit.unit (a := (f : (a : M) → N) (↑y₂ : M)) ⋯)⁻¹ : N))

Tactic:
simp
-- 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
rw : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((↑1⁻¹ : N) : N) = (f : (a : M) → N) x
⊢ f.mk' x 1 = (f : (a : M) → N) x

Tactic:
rw [mk', map_one]

Premises used: Submonoid.LocalizationMap.mk', map_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
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((↑1⁻¹ : N) : N) = (f : (a : M) → N) x

Tactic:
mul_one _

Premises used: 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
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((↑1⁻¹ : N) : N) = (f : (a : M) → N) x

Tactic:
exact mul_one _

Premises used: 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
z : N
rw :
  HMul.hMul (α := N) ((f : (a : M) → N) (↑(f.sec z).2 : M) : N) z =
    HMul.hMul (α := N) ((f.toMonoidHom : (a : M) → N) (↑(f.sec z).2 : M) : N) z
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (f.sec z).1 : N)
      ((↑((IsUnit.liftRight (f.toMonoidHom.restrict S) ⋯ : (a : ↥S) → Nˣ) (f.sec z).2)⁻¹ : N) : N) =
    z

Tactic:
rw [← sec_spec, mul_inv_left, mul_comm]

Premises used: mul_comm, Submonoid.LocalizationMap.mul_inv_left, Submonoid.LocalizationMap.sec_spec
-- 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
z : N
⊢ HMul.hMul (α := N) ((f : (a : M) → N) (↑(f.sec z).2 : M) : N) z =
    HMul.hMul (α := N) ((f.toMonoidHom : (a : M) → N) (↑(f.sec z).2 : M) : N) z

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
z : N
⊢ ∃ (x : M) (y : ↥S), f.mk' x y = z

Tactic:
⟨(f.sec z).1, (f.sec z).2, f.mk'_sec z⟩

Premises used: Submonoid.LocalizationMap.sec, Prod.fst, Exists.intro, Submonoid.LocalizationMap.mk'_sec, Prod.snd
-- 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) (β := N) ((f : (a : M) → N) (↑y : M) : N) ((f : (a : M) → N) x : N) =
    HMul.hMul (α := N) (β := N) ((f.toMonoidHom : (a : M) → N) (↑y : M) : N) ((f : (a : M) → N) x : N)
⊢ 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 : (a : M) → N) x

Tactic:
rw [mul_assoc, mul_comm _ (f y), ← mul_assoc, mul_inv_left, mul_comm]

Premises used: mul_assoc, mul_comm, Submonoid.LocalizationMap.mul_inv_left, Subtype.val, DFunLike.coe
-- 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
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑y : M) : N) ((f : (a : M) → N) x : N) =
    HMul.hMul (α := N) (β := N) ((f.toMonoidHom : (a : M) → N) (↑y : M) : N) ((f : (a : M) → N) x : 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
y : ↥S
rw : HMul.hMul (β := N) (f.mk' x y) ((f : (a : M) → N) (↑y : M) : 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)
⊢ HMul.hMul (α := N) ((f : (a : M) → N) (↑y : M) : N) (f.mk' x y) = (f : (a : M) → N) x

Tactic:
rw [mul_comm, mk'_spec]

Premises used: mul_comm, Submonoid.LocalizationMap.mk'_spec
-- 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
z : N
H : z = f.mk' x y
rw : HMul.hMul (β := N) (f.mk' x y) ((f : (a : M) → N) (↑y : M) : 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)
⊢ HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N) = (f : (a : M) → N) x

Tactic:
rw [H, mk'_spec]

Premises used: Submonoid.LocalizationMap.mk'_spec
-- 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
z : N
H : HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N) = (f : (a : M) → N) x
rwa :
  z =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N)
      ((↑((IsUnit.liftRight (f.toMonoidHom.restrict S) ⋯ : (a : ↥S) → Nˣ) y)⁻¹ : N) : N)
rwa₁ rwa₂ rwa₃ rwa₄ : HMul.hMul (β := N) z ((f.toMonoidHom : (a : M) → N) (↑y : M) : N) = (f : (a : M) → N) x
⊢ z = f.mk' x y

Tactic:
rwa [mk', mul_inv_right]

Premises used: Submonoid.LocalizationMap.mk', Submonoid.LocalizationMap.mul_inv_right
-- 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
z : N
rw : z = f.mk' x y ↔ (f : (a : M) → N) x = HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N)
rw₁ :
  HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N) = (f : (a : M) → N) x ↔
    (f : (a : M) → N) x = HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N)
rw₂ rw₃ :
  (f : (a : M) → N) x = HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N) ↔
    (f : (a : M) → N) x = HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N)
⊢ f.mk' x y = z ↔ (f : (a : M) → N) x = HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N)

Tactic:
rw [eq_comm, eq_mk'_iff_mul_eq, eq_comm]

Premises used: eq_comm, Submonoid.LocalizationMap.eq_mk'_iff_mul_eq