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
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 :
  ∀ (hab : ∃ a_1 ∈ S, a_1 * ((↑b.2 : M) ^ n * a.1 ^ n) = a_1 * ((↑a.2 : M) ^ n * b.1 ^ n)),
    ∃ a_1 ∈ S, a_1 * ((↑b.2 : M) * a.1) = a_1 * ((↑a.2 : M) * b.1)
⊢ Localization.mk a.1 a.2 = Localization.mk b.1 b.2

Tactic:
simp only [mk_pow, mk_eq_mk_iff, r_iff_exists, SubmonoidClass.coe_pow, Subtype.exists,
      exists_prop] at hab ⊢

Premises used: Subtype.exists, exists_prop, Localization.r_iff_exists, Localization.mk_pow, SubmonoidClass.coe_pow, Localization.mk_eq_mk_iff
-- 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 : ∃ a_1 ∈ S, a_1 * ((↑b.2 : M) ^ n * a.1 ^ n) = a_1 * ((↑a.2 : M) ^ n * b.1 ^ n)
mk :
  ∀ (c : M) (hc : c ∈ S) (hab : c * ((↑b.2 : M) ^ n * a.1 ^ n) = c * ((↑a.2 : M) ^ n * b.1 ^ n)),
    ∃ a_1 ∈ S, a_1 * ((↑b.2 : M) * a.1) = a_1 * ((↑a.2 : M) * b.1)
⊢ ∃ a_1 ∈ S, a_1 * ((↑b.2 : M) * a.1) = a_1 * ((↑a.2 : M) * b.1)

Tactic:
obtain ⟨c, hc, hab⟩ := hab
-- 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
c : M
hc : c ∈ S
hab : c * ((↑b.2 : M) ^ n * a.1 ^ n) = c * ((↑a.2 : M) ^ n * b.1 ^ n)
⊢ ∃ a_1 ∈ S, a_1 * ((↑b.2 : M) * a.1) = a_1 * ((↑a.2 : M) * b.1)

Tactic:
⟨c, hc, pow_left_injective hn ?_⟩

Premises used: pow_left_injective, And.intro, Exists.intro
-- 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
c : M
hc : c ∈ S
hab : c * ((↑b.2 : M) ^ n * a.1 ^ n) = c * ((↑a.2 : M) ^ n * b.1 ^ n)
mk :
  Eq.{u_1 + 1} (α := M) ((fun (a : M) ↦ a ^ n) (c * ((↑b.2 : M) * a.1)))
    ((fun (a : M) ↦ a ^ n) (c * ((↑a.2 : M) * b.1)))
⊢ ∃ a_1 ∈ S, a_1 * ((↑b.2 : M) * a.1) = a_1 * ((↑a.2 : M) * b.1)

Tactic:
refine ⟨c, hc, pow_left_injective hn ?_⟩
-- 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
c : M
hc : c ∈ S
hab : c * ((↑b.2 : M) ^ n * a.1 ^ n) = c * ((↑a.2 : M) ^ n * b.1 ^ n)
mk :
  ∀ (hn : Ne (α := ℕ) 0 0)
    (hab :
      c * (HPow.hPow (β := ℕ) (↑b.2 : M) 0 * HPow.hPow (β := ℕ) a.1 0) =
        c * (HPow.hPow (β := ℕ) (↑a.2 : M) 0 * HPow.hPow (β := ℕ) b.1 0)),
    Eq.{u_1 + 1} (α := M) ((fun (a : M) ↦ HPow.hPow (β := ℕ) a 0) (c * ((↑b.2 : M) * a.1)))
      ((fun (a : M) ↦ HPow.hPow (β := ℕ) a 0) (c * ((↑a.2 : M) * b.1)))
mk₁ :
  ∀ (n : ℕ) (hn : n + 1 ≠ 0)
    (hab : c * ((↑b.2 : M) ^ (n + 1) * a.1 ^ (n + 1)) = c * ((↑a.2 : M) ^ (n + 1) * b.1 ^ (n + 1))),
    Eq.{u_1 + 1} (α := M) ((fun (a : M) ↦ a ^ (n + 1)) (c * ((↑b.2 : M) * a.1)))
      ((fun (a : M) ↦ a ^ (n + 1)) (c * ((↑a.2 : M) * b.1)))
⊢ Eq.{u_1 + 1} (α := M) ((fun (a : M) ↦ a ^ n) (c * ((↑b.2 : M) * a.1)))
    ((fun (a : M) ↦ a ^ n) (c * ((↑a.2 : M) * b.1)))

Tactic:
obtain _ | n := 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
P : Type u_3
inst_2 : CommMonoid P
inst_3 : IsMulTorsionFree M
a₁ : Localization S
a : M × ↥S
a₂ : Localization S
b : M × ↥S
c : M
hc : c ∈ S
hn : Ne (α := ℕ) 0 0
hab :
  c * (HPow.hPow (β := ℕ) (↑b.2 : M) 0 * HPow.hPow (β := ℕ) a.1 0) =
    c * (HPow.hPow (β := ℕ) (↑a.2 : M) 0 * HPow.hPow (β := ℕ) b.1 0)
⊢ Eq.{u_1 + 1} (α := M) ((fun (a : M) ↦ HPow.hPow (β := ℕ) a 0) (c * ((↑b.2 : M) * a.1)))
    ((fun (a : M) ↦ HPow.hPow (β := ℕ) a 0) (c * ((↑a.2 : M) * b.1)))

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
P : Type u_3
inst_2 : CommMonoid P
inst_3 : IsMulTorsionFree M
a₁ : Localization S
a : M × ↥S
a₂ : Localization S
b : M × ↥S
c : M
hc : c ∈ S
n : ℕ
hn : n + 1 ≠ 0
hab : c * ((↑b.2 : M) ^ (n + 1) * a.1 ^ (n + 1)) = c * ((↑a.2 : M) ^ (n + 1) * b.1 ^ (n + 1))
⊢ Eq.{u_1 + 1} (α := M) ((fun (a : M) ↦ a ^ (n + 1)) (c * ((↑b.2 : M) * a.1)))
    ((fun (a : M) ↦ a ^ (n + 1)) (c * ((↑a.2 : M) * b.1)))

Tactic:
simp [mul_pow, pow_succ c, mul_assoc, hab]

Premises used: pow_succ, mul_assoc, mul_pow
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Submonoid α
b : ↥s
c d : α
h : Eq.{u_1 + 1} (α := Localization s) ((fun (a : α) ↦ mk a b) c) ((fun (a : α) ↦ mk a b) d)
⊢ c = d

Tactic:
simpa [mk_eq_mk_iff, r_iff_exists] using h

Premises used: Localization.r_iff_exists, Localization.mk_eq_mk_iff
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
simp_rw : (r s : (a : α × ↥s) → α × ↥s → Prop) (a₁, a₂) (b₁, b₂) ↔ (↑b₂ : α) * a₁ = (↑a₂ : α) * b₁
simp_rw₁ : (∃ (c : ↥s), (↑c : α) * ((↑b₂ : α) * a₁) = (↑c : α) * ((↑a₂ : α) * b₁)) ↔ (↑b₂ : α) * a₁ = (↑a₂ : α) * b₁
simp_rw₂ : (∃ (c : ↥s), (↑b₂ : α) * a₁ = (↑a₂ : α) * b₁) ↔ (↑b₂ : α) * a₁ = (↑a₂ : α) * b₁
⊢ mk a₁ a₂ = mk b₁ b₂ ↔ (↑b₂ : α) * a₁ = (↑a₂ : α) * b₁

Tactic:
simp_rw [mk_eq_mk_iff, r_iff_exists, mul_left_cancel_iff, exists_const]

Premises used: Localization.r_iff_exists, exists_const, mul_left_cancel_iff, Localization.mk_eq_mk_iff
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
G : Type u_2
F : Type u_3
inst : CommMonoid M
inst_1 : CommGroup G
S : Submonoid G
inst_2 : FunLike F G M
inst_3 : MulHomClass F G M
f : F
h : IsLocalizationMap.{u_2, u_1} (M := G) (N := M) S (⇑f : (a : G) → M)
⊢ Bijective.{u_2 + 1, u_1 + 1} (α := G) (β := M) (⇑f : (a : G) → M)

Tactic:
⟨fun g g' eq ↦ ?_, fun m ↦ ?_⟩

Premises used: And.intro, Function.Bijective
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
G : Type u_2
F : Type u_3
inst : CommMonoid M
inst_1 : CommGroup G
S : Submonoid G
inst_2 : FunLike F G M
inst_3 : MulHomClass F G M
f : F
h : IsLocalizationMap.{u_2, u_1} (M := G) (N := M) S (⇑f : (a : G) → M)
refine_1 : ∀ (g g' : G) (eq : Eq.{u_1 + 1} (α := M) ((f : (a : G) → M) g : M) ((f : (a : G) → M) g' : M)), g = g'
refine_2 : ∀ (m : M), ∃ (a : G), (f : (a : G) → M) a = m
⊢ Bijective.{u_2 + 1, u_1 + 1} (α := G) (β := M) (⇑f : (a : G) → M)

Tactic:
refine ⟨fun g g' eq ↦ ?_, fun m ↦ ?_⟩
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
G : Type u_2
F : Type u_3
inst : CommMonoid M
inst_1 : CommGroup G
S : Submonoid G
inst_2 : FunLike F G M
inst_3 : MulHomClass F G M
f : F
h : IsLocalizationMap.{u_2, u_1} (M := G) (N := M) S (⇑f : (a : G) → M)
g g' : G
eq : Eq.{u_1 + 1} (α := M) ((f : (a : G) → M) g : M) ((f : (a : G) → M) g' : M)
refine_1 : ∀ (c : ↥S) (eq : (↑c : G) * g = (↑c : G) * g'), g = g'
⊢ g = g'

Tactic:
have ⟨c, eq⟩ := h.exists_of_eq eq
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
G : Type u_2
F : Type u_3
inst : CommMonoid M
inst_1 : CommGroup G
S : Submonoid G
inst_2 : FunLike F G M
inst_3 : MulHomClass F G M
f : F
h : IsLocalizationMap.{u_2, u_1} (M := G) (N := M) S (⇑f : (a : G) → M)
g g' : G
eq_1 : Eq.{u_1 + 1} (α := M) ((f : (a : G) → M) g : M) ((f : (a : G) → M) g' : M)
c : ↥S
eq : (↑c : G) * g = (↑c : G) * g'
⊢ g = g'

Tactic:
mul_left_cancel eq

Premises used: mul_left_cancel
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
G : Type u_2
F : Type u_3
inst : CommMonoid M
inst_1 : CommGroup G
S : Submonoid G
inst_2 : FunLike F G M
inst_3 : MulHomClass F G M
f : F
h : IsLocalizationMap.{u_2, u_1} (M := G) (N := M) S (⇑f : (a : G) → M)
g g' : G
eq_1 : Eq.{u_1 + 1} (α := M) ((f : (a : G) → M) g : M) ((f : (a : G) → M) g' : M)
c : ↥S
eq : (↑c : G) * g = (↑c : G) * g'
⊢ g = g'

Tactic:
exact mul_left_cancel eq

Premises used: mul_left_cancel
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
G : Type u_2
F : Type u_3
inst : CommMonoid M
inst_1 : CommGroup G
S : Submonoid G
inst_2 : FunLike F G M
inst_3 : MulHomClass F G M
f : F
h : IsLocalizationMap.{u_2, u_1} (M := G) (N := M) S (⇑f : (a : G) → M)
m : M
refine_2 :
  ∀ (x : G × ↥S) (eq : HMul.hMul (β := M) m ((f : (a : G) → M) (↑x.2 : G) : M) = (f : (a : G) → M) x.1),
    ∃ (a : G), (f : (a : G) → M) a = m
⊢ ∃ (a : G), (f : (a : G) → M) a = m

Tactic:
have ⟨x, eq⟩ := h.surj m
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
G : Type u_2
F : Type u_3
inst : CommMonoid M
inst_1 : CommGroup G
S : Submonoid G
inst_2 : FunLike F G M
inst_3 : MulHomClass F G M
f : F
h : IsLocalizationMap.{u_2, u_1} (M := G) (N := M) S (⇑f : (a : G) → M)
m : M
x : G × ↥S
eq : HMul.hMul (β := M) m ((f : (a : G) → M) (↑x.2 : G) : M) = (f : (a : G) → M) x.1
h₁ : (f : (a : G) → M) (x.1 / (↑x.2 : G)) = m
⊢ ∃ (a : G), (f : (a : G) → M) a = m

Tactic:
use x.1 / x.2

Premises used: Prod.fst, Prod.snd
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
G : Type u_2
F : Type u_3
inst : CommMonoid M
inst_1 : CommGroup G
S : Submonoid G
inst_2 : FunLike F G M
inst_3 : MulHomClass F G M
f : F
h : IsLocalizationMap.{u_2, u_1} (M := G) (N := M) S (⇑f : (a : G) → M)
m : M
x : G × ↥S
eq : HMul.hMul (β := M) m ((f : (a : G) → M) (↑x.2 : G) : M) = (f : (a : G) → M) x.1
h₁ : (f : (a : G) → M) (x.1 * (↑x.2 : G)⁻¹) = m
h₂ : HMul.hMul (α := M) (β := M) ((f : (a : G) → M) x.1 : M) ((f : (a : G) → M) (↑x.2 : G)⁻¹ : M) = m
h₃ :
  HMul.hMul (β := M) (HMul.hMul (β := M) m ((f : (a : G) → M) (↑x.2 : G) : M)) ((f : (a : G) → M) (↑x.2 : G)⁻¹ : M) = m
h₄ : m * HMul.hMul (α := M) (β := M) ((f : (a : G) → M) (↑x.2 : G) : M) ((f : (a : G) → M) (↑x.2 : G)⁻¹ : M) = m
h₅ : HMul.hMul (β := M) m ((f : (a : G) → M) ((↑x.2 : G) * (↑x.2 : G)⁻¹) : M) = m
h₆ : HMul.hMul (β := M) m ((f : (a : G) → M) 1 : M) = m
h₇ : m * 1 = m
h₈ h₉ : m = m
⊢ (f : (a : G) → M) (x.1 / (↑x.2 : G)) = m

Tactic:
rw [div_eq_mul_inv, map_mul, ← eq, mul_assoc, ← map_mul, mul_inv_cancel, h.map_one, mul_one]

Premises used: Submonoid.IsLocalizationMap.map_one, mul_assoc, div_eq_mul_inv, map_mul, mul_inv_cancel, mul_one
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
G : Type u_2
F : Type u_3
inst : CommMonoid M
inst_1 : CommGroup G
S : Submonoid G
inst_2 : FunLike F G M
inst_3 : MulHomClass F G M
f : F
h : Bijective.{u_2 + 1, u_1 + 1} (α := G) (β := M) (⇑f : (a : G) → M)
e : G ≃* M := { toEquiv := Equiv.ofBijective (⇑f : (a : G) → M) h, map_mul' := ⋯ }
x y : G
eq : Eq.{u_1 + 1} (α := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y : M)
⊢ ∃ (c : ↥S), (↑c : G) * x = (↑c : G) * y

Tactic:
simp [h.1 eq]

Premises used: And.left
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
G : Type u_2
inst : CommGroup G
S : Submonoid G
⊢ IsLocalizationMap.{u_2, u_2} (M := G) S id

Tactic:
S.isLocalizationMap_iff_bijective (f := MulHom.id _).mpr bijective_id

Premises used: Iff.mpr, Function.bijective_id, Submonoid.isLocalizationMap_iff_bijective
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
G : Type u_2
inst : CommMonoid M
inst_1 : CommGroup G
S : Submonoid M
f : M → G
hf : Injective f
surj : ∀ (g : G), ∃ (x : M), ∃ y ∈ S, g = f x / f y
g : G
x y : M
hy : y ∈ S
eq : g = f x / f y
⊢ g * f (↑(x, Subtype.mk (p := fun (x : M) ↦ x ∈ S) y hy).2 : M) = f (x, Subtype.mk (p := fun (x : M) ↦ x ∈ S) y hy).1

Tactic:
simp [eq]
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
G : Type u_2
inst : CommMonoid M
inst_1 : CommGroup G
S : Submonoid M
f : M → G
hf : Injective f
surj : ∀ (g : G), ∃ (x : M), ∃ y ∈ S, g = f x / f y
x y : M
eq : f x = f y
⊢ ∃ (c : ↥S), (↑c : M) * x = (↑c : M) * y

Tactic:
simp [hf eq]
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
S : AddSubmonoid ℕ
hS : S ≠ ⊥
z : ℤ
inl : ∀ (z : ℕ), ∃ (x : ℕ), ∃ y ∈ S, (↑z : ℤ) = HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)
inr : ∀ (z : ℕ), ∃ (x : ℕ), ∃ y ∈ S, -(↑z : ℤ) = HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)
⊢ ∃ (x : ℕ), ∃ y ∈ S, z = HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)

Tactic:
obtain ⟨z, rfl | rfl⟩ := z.eq_nat_or_neg

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
S : AddSubmonoid ℕ
hS : S ≠ ⊥
z : ℕ
⊢ (↑z : ℤ) = HSub.hSub (α := ℤ) (↑z : ℤ) (↑0 : ℤ)

Tactic:
lia
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
S : AddSubmonoid ℕ
hS : S ≠ ⊥
z : ℕ
⊢ ∃ (x : ℕ), ∃ y ∈ S, (↑z : ℤ) = HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)

Tactic:
exact ⟨z, 0, zero_mem _, by lia⟩
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
S : AddSubmonoid ℕ
hS : S ≠ ⊥
z : ℕ
inr : ∀ (n : ℕ) (hnS : n ∈ S) (hn0 : n ≠ 0), ∃ (x : ℕ), ∃ y ∈ S, -(↑z : ℤ) = HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)
⊢ ∃ (x : ℕ), ∃ y ∈ S, -(↑z : ℤ) = HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)

Tactic:
have ⟨n, hnS, hn0⟩ := S.bot_or_exists_ne_zero.resolve_left hS
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
S : AddSubmonoid ℕ
hS : S ≠ ⊥
z n : ℕ
hnS : n ∈ S
hn0 : n ≠ 0
⊢ z < n * (z / n + 1)

Tactic:
have key : z < n * (z / n + 1) := Nat.lt_mul_div_succ _ <| Nat.pos_of_ne_zero hn0
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
S : AddSubmonoid ℕ
hS : S ≠ ⊥
z n : ℕ
hnS : n ∈ S
hn0 : n ≠ 0
key : z < n * (z / n + 1)
⊢ -(↑z : ℤ) = HSub.hSub (α := ℤ) (↑((z / n + 1) * n - z) : ℤ) (↑((z / n + 1) * n) : ℤ)

Tactic:
lia
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
S : AddSubmonoid ℕ
hS : S ≠ ⊥
z n : ℕ
hnS : n ∈ S
hn0 : n ≠ 0
key : z < n * (z / n + 1)
⊢ ∃ (x : ℕ), ∃ y ∈ S, -(↑z : ℤ) = HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)

Tactic:
exact ⟨(z / n + 1) * n - z, (z / n + 1) * n, nsmul_mem hnS _, by lia⟩
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
⊢ IsLocalizationMap (N := ℤ) ⊤ Nat.cast

Tactic:
AddSubmonoid.isLocalizationMap_nat_int _ top_ne_bot

Premises used: top_ne_bot, AddSubmonoid.isLocalizationMap_nat_int
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoid M
S : Submonoid M
inst_1 : CommMonoid N
f : S.LocalizationMap N
simp_rw :
  (∀ ⦃a₁ a₂ : M⦄ (a : M) (b : a ∈ S), a * a₁ = a * a₂ → a₁ = a₂) ↔
    ∀ ⦃x : M⦄, x ∈ S → ∀ ⦃a₁ a₂ : M⦄, x * a₁ = x * a₂ → a₁ = a₂
⊢ Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ↔ ∀ ⦃x : M⦄, x ∈ S → IsRegular x

Tactic:
simp_rw [Commute.isRegular_iff (Commute.all _), IsLeftRegular,
    Injective, LocalizationMap.eq_iff_exists, exists_imp, Subtype.forall]

Premises used: Submonoid.LocalizationMap.eq_iff_exists, Subtype.forall, IsLeftRegular, Commute.isRegular_iff, Function.Injective, exists_imp, Commute.all
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoid M
S : Submonoid M
inst_1 : CommMonoid N
f : S.LocalizationMap N
⊢ (∀ ⦃a₁ a₂ : M⦄ (a : M) (b : a ∈ S), a * a₁ = a * a₂ → a₁ = a₂) ↔
    ∀ ⦃x : M⦄, x ∈ S → ∀ ⦃a₁ a₂ : M⦄, x * a₁ = x * a₂ → a₁ = a₂

Tactic:
forall₂_comm

Premises used: forall₂_comm
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoid M
S : Submonoid M
inst_1 : CommMonoid N
f : S.LocalizationMap N
⊢ (∀ ⦃a₁ a₂ : M⦄ (a : M) (b : a ∈ S), a * a₁ = a * a₂ → a₁ = a₂) ↔
    ∀ ⦃x : M⦄, x ∈ S → ∀ ⦃a₁ a₂ : M⦄, x * a₁ = x * a₂ → a₁ = a₂

Tactic:
exact forall₂_comm

Premises used: forall₂_comm
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoid M
inst_1 : CommMonoid N
f : LocalizationMap.{u_1, u_2} (M := M) ⊤ N
⊢ Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ↔ IsCancelMul M

Tactic:
simp [injective_iff, isCancelMul_iff_forall_isRegular]

Premises used: Submonoid.LocalizationMap.injective_iff, isCancelMul_iff_forall_isRegular
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoid M
S : Submonoid M
inst_1 : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
⊢ IsRegular.{u_2} (R := N) ((f : (a : M) → N) m : N)

Tactic:
(Commute.isRegular_iff (Commute.all _)).mpr fun n₁ n₂ eq ↦ ?_

Premises used: Iff.mpr, Commute.isRegular_iff, Commute.all
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoid M
S : Submonoid M
inst_1 : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
refine :
  ∀ (n₁ n₂ : N)
    (eq :
      Eq.{u_2 + 1} (α := N) ((fun (x : N) ↦ HMul.hMul (α := N) ((f : (a : M) → N) m : N) x) n₁)
        ((fun (x : N) ↦ HMul.hMul (α := N) ((f : (a : M) → N) m : N) x) n₂)),
    n₁ = n₂
⊢ IsRegular.{u_2} (R := N) ((f : (a : M) → N) m : N)

Tactic:
refine (Commute.isRegular_iff (Commute.all _)).mpr fun n₁ n₂ eq ↦ ?_

Premises used: Iff.mpr, Commute.isRegular_iff, Commute.all
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoid M
S : Submonoid M
inst_1 : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
eq :
  Eq.{u_2 + 1} (α := N) ((fun (x : N) ↦ HMul.hMul (α := N) ((f : (a : M) → N) m : N) x) n₁)
    ((fun (x : N) ↦ HMul.hMul (α := N) ((f : (a : M) → N) m : N) x) n₂)
have :
  ∀ (ms₁ : M × ↥S) (eq₁ : HMul.hMul (β := N) n₁ ((f : (a : M) → N) (↑ms₁.2 : M) : N) = (f : (a : M) → N) ms₁.1), n₁ = n₂
⊢ n₁ = n₂

Tactic:
have ⟨ms₁, eq₁⟩ := f.surj n₁
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoid M
S : Submonoid M
inst_1 : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
eq :
  Eq.{u_2 + 1} (α := N) ((fun (x : N) ↦ HMul.hMul (α := N) ((f : (a : M) → N) m : N) x) n₁)
    ((fun (x : N) ↦ HMul.hMul (α := N) ((f : (a : M) → N) m : N) x) n₂)
ms₁ : M × ↥S
eq₁ : HMul.hMul (β := N) n₁ ((f : (a : M) → N) (↑ms₁.2 : M) : N) = (f : (a : M) → N) ms₁.1
have :
  ∀ (ms₂ : M × ↥S) (eq₂ : HMul.hMul (β := N) n₂ ((f : (a : M) → N) (↑ms₂.2 : M) : N) = (f : (a : M) → N) ms₂.1), n₁ = n₂
⊢ n₁ = n₂

Tactic:
have ⟨ms₂, eq₂⟩ := f.surj n₂
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoid M
S : Submonoid M
inst_1 : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
eq :
  Eq.{u_2 + 1} (α := N) ((fun (x : N) ↦ HMul.hMul (α := N) ((f : (a : M) → N) m : N) x) n₁)
    ((fun (x : N) ↦ HMul.hMul (α := N) ((f : (a : M) → N) m : N) x) n₂)
ms₁ : M × ↥S
eq₁ : HMul.hMul (β := N) n₁ ((f : (a : M) → N) (↑ms₁.2 : M) : N) = (f : (a : M) → N) ms₁.1
ms₂ : M × ↥S
eq₂ : HMul.hMul (β := N) n₂ ((f : (a : M) → N) (↑ms₂.2 : M) : N) = (f : (a : M) → N) ms₂.1
rw :
  HMul.hMul (β := N) n₁ ((f : (a : M) → N) ((↑ms₁.2 : M) * (↑ms₂.2 : M)) : N) =
    HMul.hMul (β := N) n₂ ((f : (a : M) → N) ((↑ms₁.2 : M) * (↑ms₂.2 : M)) : N)
⊢ n₁ = n₂

Tactic:
rw [← (f.map_units (ms₁.2 * ms₂.2)).mul_left_inj, Submonoid.coe_mul]

Premises used: HMul.hMul, IsUnit.mul_left_inj, Submonoid.LocalizationMap.map_units, Prod.snd, Submonoid.coe_mul
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoid M
S : Submonoid M
inst_1 : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
eq :
  Eq.{u_2 + 1} (α := N) ((fun (x : N) ↦ HMul.hMul (α := N) ((f : (a : M) → N) m : N) x) n₁)
    ((fun (x : N) ↦ HMul.hMul (α := N) ((f : (a : M) → N) m : N) x) n₂)
ms₁ : M × ↥S
eq₁ : HMul.hMul (β := N) n₁ ((f : (a : M) → N) (↑ms₁.2 : M) : N) = (f : (a : M) → N) ms₁.1
ms₂ : M × ↥S
eq₂ : HMul.hMul (β := N) n₂ ((f : (a : M) → N) (↑ms₂.2 : M) : N) = (f : (a : M) → N) ms₂.1
⊢ HMul.hMul (α := N) (β := N) ((fun (x : N) ↦ HMul.hMul (α := N) ((f : (a : M) → N) m : N) x) n₁ : N)
      ((f : (a : M) → N) ((↑ms₁.2 : M) * (↑ms₂.2 : M)) : N) =
    HMul.hMul (α := N) (β := N) ((fun (x : N) ↦ HMul.hMul (α := N) ((f : (a : M) → N) m : N) x) n₂ : N)
      ((f : (a : M) → N) ((↑ms₁.2 : M) * (↑ms₂.2 : M)) : N)

Tactic:
replace eq := congr($eq * f (ms₁.2 * ms₂.2))
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoid M
S : Submonoid M
inst_1 : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
ms₁ : M × ↥S
eq₁ : HMul.hMul (β := N) n₁ ((f : (a : M) → N) (↑ms₁.2 : M) : N) = (f : (a : M) → N) ms₁.1
ms₂ : M × ↥S
eq₂ : HMul.hMul (β := N) n₂ ((f : (a : M) → N) (↑ms₂.2 : M) : N) = (f : (a : M) → N) ms₂.1
eq :
  HMul.hMul (α := N) (β := N) ((fun (x : N) ↦ HMul.hMul (α := N) ((f : (a : M) → N) m : N) x) n₁ : N)
      ((f : (a : M) → N) ((↑ms₁.2 : M) * (↑ms₂.2 : M)) : N) =
    HMul.hMul (α := N) (β := N) ((fun (x : N) ↦ HMul.hMul (α := N) ((f : (a : M) → N) m : N) x) n₂ : N)
      ((f : (a : M) → N) ((↑ms₁.2 : M) * (↑ms₂.2 : M)) : N)
⊢ HMul.hMul (α := N) ((f : (a : M) → N) m : N)
      (HMul.hMul (β := N) n₁ ((f : (a : M) → N) ((↑ms₁.2 : M) * (↑ms₂.2 : M)) : N)) =
    HMul.hMul (α := N) ((f : (a : M) → N) m : N)
      (HMul.hMul (β := N) n₂ ((f : (a : M) → N) ((↑ms₁.2 : M) * (↑ms₂.2 : M)) : N))

Tactic:
simp_rw [mul_assoc] at eq

Premises used: mul_assoc
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoid M
S : Submonoid M
inst_1 : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
ms₁ : M × ↥S
eq₁ : HMul.hMul (β := N) n₁ ((f : (a : M) → N) (↑ms₁.2 : M) : N) = (f : (a : M) → N) ms₁.1
ms₂ : M × ↥S
eq₂ : HMul.hMul (β := N) n₂ ((f : (a : M) → N) (↑ms₂.2 : M) : N) = (f : (a : M) → N) ms₂.1
eq :
  HMul.hMul (α := N) ((f : (a : M) → N) m : N)
      (HMul.hMul (β := N) n₁ ((f : (a : M) → N) ((↑ms₁.2 : M) * (↑ms₂.2 : M)) : N)) =
    HMul.hMul (α := N) ((f : (a : M) → N) m : N)
      (HMul.hMul (β := N) n₂ ((f : (a : M) → N) ((↑ms₁.2 : M) * (↑ms₂.2 : M)) : N))
rw :
  ∀
    (eq :
      HMul.hMul (α := N) ((f : (a : M) → N) m : N)
          (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) ms₁.1 : N) ((f : (a : M) → N) (↑ms₂.2 : M) : N)) =
        HMul.hMul (α := N) ((f : (a : M) → N) m : N)
          (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) ms₂.1 : N) ((f : (a : M) → N) (↑ms₁.2 : M) : N))),
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) ms₁.1 : N) ((f : (a : M) → N) (↑ms₂.2 : M) : N) =
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) ms₂.1 : N) ((f : (a : M) → N) (↑ms₁.2 : M) : N)
⊢ HMul.hMul (β := N) n₁ ((f : (a : M) → N) ((↑ms₁.2 : M) * (↑ms₂.2 : M)) : N) =
    HMul.hMul (β := N) n₂ ((f : (a : M) → N) ((↑ms₁.2 : M) * (↑ms₂.2 : M)) : N)

Tactic:
rw [map_mul, ← mul_assoc n₁, eq₁, ← mul_assoc n₂, mul_right_comm n₂, eq₂] at eq ⊢

Premises used: mul_assoc, map_mul, mul_right_comm
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoid M
S : Submonoid M
inst_1 : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
ms₁ : M × ↥S
eq₁ : HMul.hMul (β := N) n₁ ((f : (a : M) → N) (↑ms₁.2 : M) : N) = (f : (a : M) → N) ms₁.1
ms₂ : M × ↥S
eq₂ : HMul.hMul (β := N) n₂ ((f : (a : M) → N) (↑ms₂.2 : M) : N) = (f : (a : M) → N) ms₂.1
eq :
  HMul.hMul (α := N) ((f : (a : M) → N) m : N)
      (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) ms₁.1 : N) ((f : (a : M) → N) (↑ms₂.2 : M) : N)) =
    HMul.hMul (α := N) ((f : (a : M) → N) m : N)
      (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) ms₂.1 : N) ((f : (a : M) → N) (↑ms₁.2 : M) : N))
simp_rw :
  ∀ (eq : ∃ (c : ↥S), (↑c : M) * (m * (ms₁.1 * (↑ms₂.2 : M))) = (↑c : M) * (m * (ms₂.1 * (↑ms₁.2 : M)))),
    ∃ (c : ↥S), (↑c : M) * (ms₁.1 * (↑ms₂.2 : M)) = (↑c : M) * (ms₂.1 * (↑ms₁.2 : M))
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) ms₁.1 : N) ((f : (a : M) → N) (↑ms₂.2 : M) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) ms₂.1 : N) ((f : (a : M) → N) (↑ms₁.2 : M) : N)

Tactic:
simp_rw [← map_mul, eq_iff_exists] at eq ⊢

Premises used: Submonoid.LocalizationMap.eq_iff_exists, map_mul