awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ∃ (c : ↥S), (↑c : M) * (m * (ms₁.1 * (↑ms₂.2 : M))) = (↑c : M) * (m * (ms₂.1 * (↑ms₁.2 : M)))
⊢ ∃ (c : ↥S), m * ((↑c : M) * (ms₁.1 * (↑ms₂.2 : M))) = m * ((↑c : M) * (ms₂.1 * (↑ms₁.2 : M)))

Tactic:
simp_rw [mul_left_comm _ m] at eq

Premises used: mul_left_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 : ∃ (c : ↥S), m * ((↑c : M) * (ms₁.1 * (↑ms₂.2 : M))) = m * ((↑c : M) * (ms₂.1 * (↑ms₁.2 : M)))
⊢ ∃ (c : ↥S), (↑c : M) * (ms₁.1 * (↑ms₂.2 : M)) = (↑c : M) * (ms₂.1 * (↑ms₁.2 : M))

Tactic:
eq.imp fun _ ↦ (hm.1 ·)

Premises used: Exists.imp, IsRegular.left
-- 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 : ∃ (c : ↥S), m * ((↑c : M) * (ms₁.1 * (↑ms₂.2 : M))) = m * ((↑c : M) * (ms₂.1 * (↑ms₁.2 : M)))
⊢ ∃ (c : ↥S), (↑c : M) * (ms₁.1 * (↑ms₂.2 : M)) = (↑c : M) * (ms₂.1 * (↑ms₁.2 : M))

Tactic:
exact eq.imp fun _ ↦ (hm.1 ·)

Premises used: Exists.imp, IsRegular.left
-- 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
inst_2 : IsCancelMul M
simp_rw : ∀ (r : N), IsRightRegular r
⊢ IsCancelMul N

Tactic:
simp_rw [isCancelMul_iff_forall_isRegular, Commute.isRegular_iff (Commute.all _),
    ← Commute.isRightRegular_iff (Commute.all _)]

Premises used: isCancelMul_iff_forall_isRegular, Commute.isRightRegular_iff, 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
inst_2 : IsCancelMul M
n : N
have :
  ∀ (ms : M × ↥S) (eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) ms.1),
    IsRightRegular n
⊢ IsRightRegular 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
inst_2 : IsCancelMul M
n : N
ms : M × ↥S
eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) ms.1
⊢ IsRightRegular n

Tactic:
exact (eq ▸ f.map_isRegular (isCancelMul_iff_forall_isRegular.mp ‹_› ms.1)).2.of_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
inst_2 : IsCancelMul M
⊢ IsCancelMul.{u_1} (Localization S)

Tactic:
(Localization.monoidOf S).isCancelMul

Premises used: Submonoid.LocalizationMap.isCancelMul, Localization.monoidOf
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoid M
S : Submonoid M
inst_1 : CommMonoid N
inst_2 : IsCancelMul M
inst_3 : Nontrivial M
⊢ Nontrivial.{u_1} (Localization S)

Tactic:
(injective_iff <| Localization.monoidOf S).mpr (fun _ _ ↦ .all _) |>.nontrivial

Premises used: Iff.mpr, Submonoid.LocalizationMap.injective_iff, IsRegular.all, Function.Injective.nontrivial, Localization.monoidOf
-- 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
inst_2 : Subsingleton M
x y : N
obtain : ∀ (mx : M) (sx : ↥S), f.mk' mx sx = y
⊢ x = y

Tactic:
obtain ⟨mx, sx, rfl⟩ := f.mk'_surjective x

Premises used: Submonoid.LocalizationMap.mk'_surjective, rfl
-- 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
inst_2 : Subsingleton M
y : N
mx : M
sx : ↥S
obtain : ∀ (my : M) (sy : ↥S), f.mk' mx sx = f.mk' my sy
⊢ f.mk' mx sx = y

Tactic:
obtain ⟨my, sy, rfl⟩ := f.mk'_surjective y

Premises used: Submonoid.LocalizationMap.mk'_surjective, rfl
-- 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
inst_2 : Subsingleton M
mx : M
sx : ↥S
my : M
sy : ↥S
⊢ f.mk' mx sx = f.mk' my sy

Tactic:
congr(f.mk' $(Subsingleton.elim ..) $(Subsingleton.elim ..))

Premises used: congrArg, Submonoid.LocalizationMap.mk', id, congr, Subsingleton.elim
-- 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
inst_2 : Subsingleton M
mx : M
sx : ↥S
my : M
sy : ↥S
⊢ f.mk' mx sx = f.mk' my sy

Tactic:
exact congr(f.mk' $(Subsingleton.elim ..) $(Subsingleton.elim ..))
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoid M
S : Submonoid M
inst_1 : CommMonoid N
inst_2 : Subsingleton M
⊢ Subsingleton.{u_1 + 1} (Localization S)

Tactic:
(Localization.monoidOf S).subsingleton_of_subsingleton

Premises used: Localization.monoidOf, Submonoid.LocalizationMap.subsingleton_of_subsingleton
-- Module: Mathlib.GroupTheory.MonoidLocalization.Cardinality
Goal:
M : Type u
inst : CommMonoid M
S : Submonoid M
⊢ #(Localization S) ≤ #M

Tactic:
OreLocalization.cardinalMk_le S

Premises used: OreLocalization.cardinalMk_le
-- Module: Mathlib.GroupTheory.MonoidLocalization.DivPairs
Goal:
M : Type u_1
G : Type u_2
inst : CommMonoid M
inst_1 : CommGroup G
f : LocalizationMap.{u_1, u_2} (M := M) ⊤ G
s : Submonoid G
x : M × M
⊢ x ∈ divPairs f s ↔ HDiv.hDiv (α := G) (β := G) ((f : (a : M) → G) x.1 : G) ((f : (a : M) → G) x.2 : G) ∈ s

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.GroupTheory.MonoidLocalization.DivPairs
Goal:
M : Type u_1
G : Type u_2
H : Type u_3
inst : CommMonoid M
inst_1 : CommGroup G
inst_2 : CommGroup H
f : LocalizationMap.{u_1, u_2} (M := M) ⊤ G
g : LocalizationMap.{u_1, u_3} (M := M) ⊤ H
s : Submonoid G
h : ∀ (x : M × M), x ∈ divPairs g (comap (g.mulEquivOfLocalizations f).toMonoidHom s) ↔ x ∈ divPairs f s
⊢ divPairs g (comap (g.mulEquivOfLocalizations f).toMonoidHom s) = divPairs f s

Tactic:
ext
-- Module: Mathlib.GroupTheory.MonoidLocalization.DivPairs
Goal:
M : Type u_1
G : Type u_2
H : Type u_3
inst : CommMonoid M
inst_1 : CommGroup G
inst_2 : CommGroup H
f : LocalizationMap.{u_1, u_2} (M := M) ⊤ G
g : LocalizationMap.{u_1, u_3} (M := M) ⊤ H
s : Submonoid G
x : M × M
⊢ x ∈ divPairs g (comap (g.mulEquivOfLocalizations f).toMonoidHom s) ↔ x ∈ divPairs f s

Tactic:
simp
-- Module: Mathlib.GroupTheory.MonoidLocalization.Finite
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
inst_1 : Monoid.FG M
hS : S.FG
⊢ Monoid.FG.{u_1} ↥S

Tactic:
rw [← Monoid.fg_iff_submonoid_fg] at hS

Premises used: Monoid.fg_iff_submonoid_fg
-- Module: Mathlib.GroupTheory.MonoidLocalization.Finite
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
inst_1 : Monoid.FG M
hS : Monoid.FG.{u_1} ↥S
⊢ Monoid.FG.{u_1} (Localization S)

Tactic:
Monoid.fg_of_surjective mkHom mkHom_surjective

Premises used: Localization.mkHom_surjective, Localization.mkHom, Monoid.fg_of_surjective
-- Module: Mathlib.GroupTheory.MonoidLocalization.Finite
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
inst_1 : Monoid.FG M
hS : Monoid.FG.{u_1} ↥S
⊢ Monoid.FG.{u_1} (Localization S)

Tactic:
exact Monoid.fg_of_surjective mkHom mkHom_surjective

Premises used: Monoid.fg_of_surjective
-- Module: Mathlib.GroupTheory.MonoidLocalization.Finite
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
inst_1 : Monoid.FG M
⊢ Monoid.FG.{u_1} (GrothendieckGroup M)

Tactic:
fg Monoid.FG.fg_top

Premises used: Monoid.FG.fg_top, Localization.fg
-- Module: Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : IsCancelMul M
m₁ m₂ : M
⊢ Eq (α := GrothendieckGroup M) ((of : (a : M) → GrothendieckGroup M) m₁ : GrothendieckGroup M)
      ((of : (a : M) → GrothendieckGroup M) m₂ : GrothendieckGroup M) →
    m₁ = m₂

Tactic:
simp [of, ← mk_one_eq_monoidOf_mk, mk_eq_mk_iff']

Premises used: Localization.mk_one_eq_monoidOf_mk, Algebra.GrothendieckGroup.of, Localization.mk_eq_mk_iff'
-- Module: Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Goal:
M : Type u_1
G : Type u_2
inst : CommMonoid M
inst_1 : CommGroup G
m₁ m₂ : M
s₁ s₂ : ↥⊤
h : (r ⊤ : (a : M × ↥⊤) → M × ↥⊤ → Prop) (m₁, s₁) (m₂, s₂)
⊢ Eq (α := GrothendieckGroup M)
    (Eq.ndrec (a := mk m₁ s₁) (motive := fun (x : Localization (M := M) ⊤) ↦ GrothendieckGroup M)
      (mk (↑s₁ : M) (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) ⊤ x) m₁ ⋯) :
        Localization (M := M) ⊤)
      ⋯)
    (mk (↑s₂ : M) (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) ⊤ x) m₂ ⋯))

Tactic:
simpa [r_iff_exists, mk_eq_mk_iff, eq_comm, mul_comm] using h

Premises used: eq_comm, Localization.r_iff_exists, mul_comm, Localization.mk_eq_mk_iff
-- Module: Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Goal:
M : Type u_1
inst : CommMonoid M
m : M
s : ↥⊤
⊢ (mk m s)⁻¹ = mk (↑s : M) (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) ⊤ x) m ⋯)

Tactic:
rfl

Premises used: Localization.mk, Localization.rec, Quotient.mk', OreLocalization.oreDiv, rfl
-- Module: Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Goal:
M : Type u_1
G : Type u_2
inst : CommMonoid M
inst_1 : CommGroup G
a : GrothendieckGroup M
H : ∀ (y : M × ↥⊤), (mk y.1 y.2)⁻¹ * mk y.1 y.2 = 1
⊢ a⁻¹ * a = 1

Tactic:
cases a using ind
-- Module: Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Goal:
M : Type u_1
G : Type u_2
inst : CommMonoid M
inst_1 : CommGroup G
y : M × ↥⊤
H :
  Submonoid.LocalizationMap.mk' (monoidOf ⊤) ((↑y.2 : M) * y.1)
      (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) ⊤ x) y.1 ⋯ * y.2) =
    1
⊢ (mk y.1 y.2)⁻¹ * mk y.1 y.2 = 1

Tactic:
rw [inv_mk, mk_eq_monoidOf_mk', ← Submonoid.LocalizationMap.mk'_mul]

Premises used: Localization.mk_eq_monoidOf_mk', Algebra.GrothendieckGroup.inv_mk, Submonoid.LocalizationMap.mk'_mul
-- Module: Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Goal:
M : Type u_1
G : Type u_2
inst : CommMonoid M
inst_1 : CommGroup G
y : M × ↥⊤
⊢ Submonoid.LocalizationMap.mk' (monoidOf ⊤)
      (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) ⊤ x) y.1 ⋯ * y.2) : M)
      (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) ⊤ x) y.1 ⋯ * y.2) =
    1

Tactic:
Submonoid.LocalizationMap.mk'_self' _ _

Premises used: Submonoid.LocalizationMap.mk'_self'
-- Module: Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Goal:
M : Type u_1
G : Type u_2
inst : CommMonoid M
inst_1 : CommGroup G
y : M × ↥⊤
h : (↑y.2 : M) * y.1 = (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) ⊤ x) y.1 ⋯ * y.2) : M)
⊢ Submonoid.LocalizationMap.mk' (monoidOf ⊤) ((↑y.2 : M) * y.1)
      (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) ⊤ x) y.1 ⋯ * y.2) =
    1

Tactic:
convert! Submonoid.LocalizationMap.mk'_self' _ _

Premises used: Submonoid.LocalizationMap.mk'_self'
-- Module: Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Goal:
M : Type u_1
G : Type u_2
inst : CommMonoid M
inst_1 : CommGroup G
y : M × ↥⊤
h : y.1 * (↑y.2 : M) = (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) ⊤ x) y.1 ⋯ * y.2) : M)
h₁ h₂ :
  y.1 * (↑y.2 : M) = (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) ⊤ x) y.1 ⋯) : M) * (↑y.2 : M)
⊢ (↑y.2 : M) * y.1 = (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) ⊤ x) y.1 ⋯ * y.2) : M)

Tactic:
rw [mul_comm, Submonoid.coe_mul]

Premises used: mul_comm, Submonoid.coe_mul
-- Module: Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Goal:
M : Type u_1
inst : CommMonoid M
m₁ m₂ : M
s₁ s₂ : ↥⊤
simp :
  mk (m₁ * (↑s₂ : M)) (s₁ * Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) ⊤ x) m₂ ⋯) =
    mk (m₁ * (↑s₂ : M)) (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) ⊤ x) ((↑s₁ : M) * m₂) ⋯)
⊢ mk m₁ s₁ / mk m₂ s₂ =
    mk (m₁ * (↑s₂ : M)) (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) ⊤ x) ((↑s₁ : M) * m₂) ⋯)

Tactic:
simp [div_eq_mul_inv, mk_mul]

Premises used: div_eq_mul_inv, Localization.mk_mul
-- Module: Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Goal:
M : Type u_1
inst : CommMonoid M
m₁ m₂ : M
s₁ s₂ : ↥⊤
⊢ mk (m₁ * (↑s₂ : M)) (s₁ * Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) ⊤ x) m₂ ⋯) =
    mk (m₁ * (↑s₂ : M)) (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) ⊤ x) ((↑s₁ : M) * m₂) ⋯)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Goal:
M : Type u_1
G : Type u_2
inst : CommMonoid M
inst_1 : CommGroup G
f : M →* G
h :
  ∀ (x : M),
    Eq.{u_2 + 1} (α := G)
      (((fun (f : MonoidHom.{u_1, u_2} (GrothendieckGroup M) G) ↦ f.comp of)
              ((fun (f : M →* G) ↦
                  (Submonoid.LocalizationMap.lift (monoidOf ⊤) (g := f) ⋯ :
                    MonoidHom.{u_1, u_2} (Localization (M := M) ⊤) G))
                f) :
            (a : M) → G)
          x :
        G)
      ((f : (a : M) → G) x : G)
⊢ (fun (f : MonoidHom.{u_1, u_2} (GrothendieckGroup M) G) ↦ f.comp of)
      ((fun (f : M →* G) ↦
          (Submonoid.LocalizationMap.lift (monoidOf ⊤) (g := f) ⋯ : MonoidHom.{u_1, u_2} (Localization (M := M) ⊤) G))
        f) =
    f

Tactic:
ext
-- Module: Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Goal:
M : Type u_1
G : Type u_2
inst : CommMonoid M
inst_1 : CommGroup G
f : M →* G
x : M
⊢ Eq.{u_2 + 1} (α := G)
    (((fun (f : MonoidHom.{u_1, u_2} (GrothendieckGroup M) G) ↦ f.comp of)
            ((fun (f : M →* G) ↦
                (Submonoid.LocalizationMap.lift (monoidOf ⊤) (g := f) ⋯ :
                  MonoidHom.{u_1, u_2} (Localization (M := M) ⊤) G))
              f) :
          (a : M) → G)
        x :
      G)
    ((f : (a : M) → G) x : G)

Tactic:
simp
-- Module: Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Goal:
M : Type u_1
G : Type u_2
inst : CommMonoid M
inst_1 : CommGroup G
f : MonoidHom.{u_1, u_2} (GrothendieckGroup M) G
h :
  ∀ (x : Localization (M := M) ⊤),
    Eq.{u_2 + 1} (α := G)
      (((fun (f : M →* G) ↦
                (Submonoid.LocalizationMap.lift (monoidOf ⊤) (g := f) ⋯ :
                  MonoidHom.{u_1, u_2} (Localization (M := M) ⊤) G))
              ((fun (f : MonoidHom.{u_1, u_2} (GrothendieckGroup M) G) ↦ f.comp of) f) :
            (a : Localization ⊤) → G)
          x :
        G)
      ((f : (a : Localization ⊤) → G) x : G)
⊢ (fun (f : M →* G) ↦
        (Submonoid.LocalizationMap.lift (monoidOf ⊤) (g := f) ⋯ : MonoidHom.{u_1, u_2} (Localization (M := M) ⊤) G))
      ((fun (f : MonoidHom.{u_1, u_2} (GrothendieckGroup M) G) ↦ f.comp of) f) =
    f

Tactic:
ext
-- Module: Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Goal:
M : Type u_1
G : Type u_2
inst : CommMonoid M
inst_1 : CommGroup G
f : MonoidHom.{u_1, u_2} (GrothendieckGroup M) G
x : Localization (M := M) ⊤
⊢ Eq.{u_2 + 1} (α := G)
    (((fun (f : M →* G) ↦
              (Submonoid.LocalizationMap.lift (monoidOf ⊤) (g := f) ⋯ :
                MonoidHom.{u_1, u_2} (Localization (M := M) ⊤) G))
            ((fun (f : MonoidHom.{u_1, u_2} (GrothendieckGroup M) G) ↦ f.comp of) f) :
          (a : Localization ⊤) → G)
        x :
      G)
    ((f : (a : Localization ⊤) → G) x : G)

Tactic:
simp
-- Module: Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Goal:
M : Type u_1
G : Type u_2
inst : CommMonoid M
inst_1 : CommGroup G
f : M →* G
x : GrothendieckGroup M
simp :
  Eq.{u_2 + 1} (α := G)
    ((↑((IsUnit.liftRight (f.restrict ⊤) ⋯ : (a : ↥⊤) → Gˣ) (Submonoid.LocalizationMap.sec (monoidOf ⊤) x).2) : G) : G)
    ((f : (a : M) → G) (↑(Submonoid.LocalizationMap.sec (monoidOf ⊤) x).2 : M) : G)
⊢ (((lift : (a : M →* G) → GrothendieckGroup M →* G) f : MonoidHom.{u_1, u_2} (GrothendieckGroup M) G) :
        (a : GrothendieckGroup M) → G)
      x =
    HDiv.hDiv (α := G) (β := G) ((f : (a : M) → G) (Submonoid.LocalizationMap.sec (monoidOf ⊤) x).1 : G)
      ((f : (a : M) → G) (↑(Submonoid.LocalizationMap.sec (monoidOf ⊤) x).2 : M) : G)

Tactic:
simp [lift, (monoidOf ⊤).lift_apply, div_eq_mul_inv]

Premises used: div_eq_mul_inv, Algebra.GrothendieckGroup.lift, Submonoid.LocalizationMap.lift_apply, Localization.monoidOf, Top.top
-- Module: Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Goal:
M : Type u_1
G : Type u_2
inst : CommMonoid M
inst_1 : CommGroup G
f : M →* G
x : GrothendieckGroup M
⊢ Eq.{u_2 + 1} (α := G)
    ((↑((IsUnit.liftRight (f.restrict ⊤) ⋯ : (a : ↥⊤) → Gˣ) (Submonoid.LocalizationMap.sec (monoidOf ⊤) x).2) : G) : G)
    ((f : (a : M) → G) (↑(Submonoid.LocalizationMap.sec (monoidOf ⊤) x).2 : M) : G)

Tactic:
congr
-- Module: Mathlib.GroupTheory.MonoidLocalization.Lemmas
Goal:
M : Type u_1
N : Type u_2
F : Type u_3
ι : Type u_4
inst : Finite ι
inst_1 : CommMonoid M
inst_2 : CommMonoid N
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
f : F
S : Submonoid M
hf : IsLocalizationMap.{u_1, u_2} (N := N) S (⇑f : (a : M) → N)
n : ι → N
choose :
  ∀ (x : (z : N) → M × ↥S)
    (hx : ∀ (z : N), HMul.hMul (β := N) z ((f : (a : M) → N) (↑(x z).2 : M) : N) = (f : (a : M) → N) (x z).1),
    ∃ (s : ↥S) (x : ι → M),
      ∀ (i : ι), HMul.hMul (β := N) (n i) ((f : (a : M) → N) (↑s : M) : N) = (f : (a : M) → N) (x i)
⊢ ∃ (s : ↥S) (x : ι → M), ∀ (i : ι), HMul.hMul (β := N) (n i) ((f : (a : M) → N) (↑s : M) : N) = (f : (a : M) → N) (x i)

Tactic:
choose x hx using hf.surj

Premises used: Submonoid.IsLocalizationMap.surj
-- Module: Mathlib.GroupTheory.MonoidLocalization.Lemmas
Goal:
M : Type u_1
N : Type u_2
F : Type u_3
ι : Type u_4
inst : Finite ι
inst_1 : CommMonoid M
inst_2 : CommMonoid N
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
f : F
S : Submonoid M
hf : IsLocalizationMap.{u_1, u_2} (N := N) S (⇑f : (a : M) → N)
n : ι → N
x : (z : N) → M × ↥S
hx : ∀ (z : N), HMul.hMul (β := N) z ((f : (a : M) → N) (↑(x z).2 : M) : N) = (f : (a : M) → N) (x z).1
have :
  ∀ (val : Fintype ι),
    ∃ (s : ↥S) (x : ι → M),
      ∀ (i : ι), HMul.hMul (β := N) (n i) ((f : (a : M) → N) (↑s : M) : N) = (f : (a : M) → N) (x i)
⊢ ∃ (s : ↥S) (x : ι → M), ∀ (i : ι), HMul.hMul (β := N) (n i) ((f : (a : M) → N) (↑s : M) : N) = (f : (a : M) → N) (x i)

Tactic:
have ⟨_⟩ := nonempty_fintype ι
-- Module: Mathlib.GroupTheory.MonoidLocalization.Lemmas
Goal:
M : Type u_1
N : Type u_2
F : Type u_3
ι : Type u_4
inst : Finite ι
inst_1 : CommMonoid M
inst_2 : CommMonoid N
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
f : F
S : Submonoid M
hf : IsLocalizationMap.{u_1, u_2} (N := N) S (⇑f : (a : M) → N)
n : ι → N
x : (z : N) → M × ↥S
hx : ∀ (z : N), HMul.hMul (β := N) z ((f : (a : M) → N) (↑(x z).2 : M) : N) = (f : (a : M) → N) (x z).1
val : Fintype ι
⊢ ∃ (s : ↥S) (x : ι → M), ∀ (i : ι), HMul.hMul (β := N) (n i) ((f : (a : M) → N) (↑s : M) : N) = (f : (a : M) → N) (x i)

Tactic:
⟨∏ i : ι, (x (n i)).2, fun i ↦ (x (n i)).1 * ∏ j ∈ univ.erase i, (x (n j)).2, fun i ↦ ?_⟩

Premises used: HMul.hMul, Finset.univ, Prod.fst, Finset.prod, Exists.intro, Finset.erase, Subtype.val, Prod.snd
-- Module: Mathlib.GroupTheory.MonoidLocalization.Lemmas
Goal:
M : Type u_1
N : Type u_2
F : Type u_3
ι : Type u_4
inst : Finite ι
inst_1 : CommMonoid M
inst_2 : CommMonoid N
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
f : F
S : Submonoid M
hf : IsLocalizationMap.{u_1, u_2} (N := N) S (⇑f : (a : M) → N)
n : ι → N
x : (z : N) → M × ↥S
hx : ∀ (z : N), HMul.hMul (β := N) z ((f : (a : M) → N) (↑(x z).2 : M) : N) = (f : (a : M) → N) (x z).1
val : Fintype ι
refine :
  ∀ (i : ι),
    HMul.hMul (β := N) (n i) ((f : (a : M) → N) (↑(∏ i : ι, (x (n i)).2) : M) : N) =
      (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)
⊢ ∃ (s : ↥S) (x : ι → M), ∀ (i : ι), HMul.hMul (β := N) (n i) ((f : (a : M) → N) (↑s : M) : N) = (f : (a : M) → N) (x i)

Tactic:
refine ⟨∏ i : ι, (x (n i)).2, fun i ↦ (x (n i)).1 * ∏ j ∈ univ.erase i, (x (n j)).2, fun i ↦ ?_⟩
-- Module: Mathlib.GroupTheory.MonoidLocalization.Lemmas
Goal:
M : Type u_1
N : Type u_2
F : Type u_3
ι : Type u_4
inst : Finite ι
inst_1 : CommMonoid M
inst_2 : CommMonoid N
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
f : F
S : Submonoid M
hf : IsLocalizationMap.{u_1, u_2} (N := N) S (⇑f : (a : M) → N)
n : ι → N
x : (z : N) → M × ↥S
hx : ∀ (z : N), HMul.hMul (β := N) z ((f : (a : M) → N) (↑(x z).2 : M) : N) = (f : (a : M) → N) (x z).1
val : Fintype ι
i : ι
rw :
  HMul.hMul (β := N) (n i) ((f : (a : M) → N) (↑((x (n i)).2 * ∏ x_1 ∈ erase univ i, (x (n x_1)).2) : M) : N) =
    (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)
rw₁ :
  HMul.hMul (β := N) (n i) ((f : (a : M) → N) ((↑(x (n i)).2 : M) * (↑(∏ x_1 ∈ erase univ i, (x (n x_1)).2) : M)) : N) =
    (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)
rw₂ :
  n i *
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑(x (n i)).2 : M) : N)
        ((f : (a : M) → N) (↑(∏ x_1 ∈ erase univ i, (x (n x_1)).2) : M) : N) =
    (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)
rw₃ :
  HMul.hMul (β := N) (HMul.hMul (β := N) (n i) ((f : (a : M) → N) (↑(x (n i)).2 : M) : N))
      ((f : (a : M) → N) (↑(∏ x_1 ∈ erase univ i, (x (n x_1)).2) : M) : N) =
    (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)
rw₄ :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (x (n i)).1 : N)
      ((f : (a : M) → N) (↑(∏ x_1 ∈ erase univ i, (x (n x_1)).2) : M) : N) =
    (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)
rw₅ rw₆ :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (x (n i)).1 : N)
      ((f : (a : M) → N) (↑(∏ x_1 ∈ erase univ i, (x (n x_1)).2) : M) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (x (n i)).1 : N)
      ((f : (a : M) → N) (↑(∏ j ∈ erase univ i, (x (n j)).2) : M) : N)
⊢ HMul.hMul (β := N) (n i) ((f : (a : M) → N) (↑(∏ i : ι, (x (n i)).2) : M) : N) =
    (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)

Tactic:
rw [← univ.mul_prod_erase _ (mem_univ i), S.coe_mul, map_mul, ← mul_assoc, hx, map_mul]

Premises used: Finset.mem_univ, Finset.univ, mul_assoc, Finset.mul_prod_erase, map_mul, Submonoid.coe_mul
-- Module: Mathlib.GroupTheory.MonoidLocalization.Lemmas
Goal:
M : Type u_1
N : Type u_2
F : Type u_3
ι : Type u_4
inst : Finite ι
inst_1 : CommMonoid M
inst_2 : CommMonoid N
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
f : F
S : Submonoid M
hf : IsLocalizationMap.{u_1, u_2} (N := N) S (⇑f : (a : M) → N)
n : ι → N
x : (z : N) → M × ↥S
hx : ∀ (z : N), HMul.hMul (β := N) z ((f : (a : M) → N) (↑(x z).2 : M) : N) = (f : (a : M) → N) (x z).1
val : Fintype ι
refine :
  ∀ (i : ι),
    HMul.hMul (β := N) (n i) ((f : (a : M) → N) (↑(∏ i : ι, (x (n i)).2) : M) : N) =
      (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)
⊢ ∃ (s : ↥S) (x : ι → M), ∀ (i : ι), HMul.hMul (β := N) (n i) ((f : (a : M) → N) (↑s : M) : N) = (f : (a : M) → N) (x i)

Tactic:
classical
  refine ⟨∏ i : ι, (x (n i)).2, fun i ↦ (x (n i)).1 * ∏ j ∈ univ.erase i, (x (n j)).2, fun i ↦ ?_⟩
  rw [← univ.mul_prod_erase _ (mem_univ i), S.coe_mul, map_mul, ← mul_assoc, hx, map_mul]

Premises used: mul_assoc, map_mul, Submonoid.coe_mul