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
a b c : M × ↥S
t₁ : ↥S
ht₁ : (↑t₁ : M) * ((↑b.2 : M) * a.1) = (↑t₁ : M) * ((↑a.2 : M) * b.1)
t₂ : ↥S
ht₂ : (↑t₂ : M) * ((↑c.2 : M) * b.1) = (↑t₂ : M) * ((↑b.2 : M) * c.1)
⊢ (↑t₂ : M) * (↑c.2 : M) * ((↑t₁ : M) * ((↑a.2 : M) * b.1)) = (↑t₁ : M) * (↑a.2 : M) * ((↑t₂ : M) * ((↑c.2 : M) * b.1))

Tactic:
ac_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
P : Type u_3
inst_2 : CommMonoid P
a b c : M × ↥S
t₁ : ↥S
ht₁ : (↑t₁ : M) * ((↑b.2 : M) * a.1) = (↑t₁ : M) * ((↑a.2 : M) * b.1)
t₂ : ↥S
ht₂ : (↑t₂ : M) * ((↑c.2 : M) * b.1) = (↑t₂ : M) * ((↑b.2 : M) * c.1)
rw : (↑t₁ : M) * (↑a.2 : M) * ((↑t₂ : M) * ((↑b.2 : M) * c.1)) = (↑t₂ : M) * (↑t₁ : M) * (↑b.2 : M) * ((↑a.2 : M) * c.1)
⊢ (↑t₁ : M) * (↑a.2 : M) * ((↑t₂ : M) * ((↑c.2 : M) * b.1)) = (↑t₂ : M) * (↑t₁ : M) * (↑b.2 : M) * ((↑a.2 : M) * c.1)

Tactic:
rw [ht₂]
-- 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
a b c : M × ↥S
t₁ : ↥S
ht₁ : (↑t₁ : M) * ((↑b.2 : M) * a.1) = (↑t₁ : M) * ((↑a.2 : M) * b.1)
t₂ : ↥S
ht₂ : (↑t₂ : M) * ((↑c.2 : M) * b.1) = (↑t₂ : M) * ((↑b.2 : M) * c.1)
⊢ (↑t₁ : M) * (↑a.2 : M) * ((↑t₂ : M) * ((↑b.2 : M) * c.1)) = (↑t₂ : M) * (↑t₁ : M) * (↑b.2 : M) * ((↑a.2 : M) * c.1)

Tactic:
ac_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
P : Type u_3
inst_2 : CommMonoid P
a b c : M × ↥S
t₁ : ↥S
ht₁ : (↑t₁ : M) * ((↑b.2 : M) * a.1) = (↑t₁ : M) * ((↑a.2 : M) * b.1)
t₂ : ↥S
ht₂ : (↑t₂ : M) * ((↑c.2 : M) * b.1) = (↑t₂ : M) * ((↑b.2 : M) * c.1)
t₃ : (↑t₂ : M) * (↑t₁ : M) * (↑b.2 : M) * ((↑c.2 : M) * a.1) = (↑t₂ : M) * (↑c.2 : M) * ((↑t₁ : M) * ((↑b.2 : M) * a.1))
t₄ :
  (↑t₂ : M) * (↑c.2 : M) * ((↑t₁ : M) * ((↑b.2 : M) * a.1)) = (↑t₁ : M) * (↑a.2 : M) * ((↑t₂ : M) * ((↑c.2 : M) * b.1))
t₅ : (↑t₁ : M) * (↑a.2 : M) * ((↑t₂ : M) * ((↑c.2 : M) * b.1)) = (↑t₂ : M) * (↑t₁ : M) * (↑b.2 : M) * ((↑a.2 : M) * c.1)
⊢ (↑t₂ : M) * (↑t₁ : M) * (↑b.2 : M) * ((↑c.2 : M) * a.1) = (↑t₂ : M) * (↑t₁ : M) * (↑b.2 : M) * ((↑a.2 : M) * c.1)

Tactic:
calc
      (t₂ * t₁ * b.2 : M) * (c.2 * a.1) = t₂ * c.2 * (t₁ * (b.2 * a.1)) := by ac_rfl
      _ = t₁ * a.2 * (t₂ * (c.2 * b.1)) := by rw [ht₁]; ac_rfl
      _ = t₂ * t₁ * b.2 * (a.2 * c.1) := by rw [ht₂]; ac_rfl

Premises used: HMul.hMul, Prod.fst, Subtype.val, 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
P : Type u_3
inst_2 : CommMonoid P
a b c d : M × ↥S
t₁ : ↥S
ht₁ : (↑t₁ : M) * ((↑b.2 : M) * a.1) = (↑t₁ : M) * ((↑a.2 : M) * b.1)
t₂ : ↥S
ht₂ : (↑t₂ : M) * ((↑d.2 : M) * c.1) = (↑t₂ : M) * ((↑c.2 : M) * d.1)
h : (↑(t₂ * t₁) : M) * ((↑(b * d).2 : M) * (a * c).1) = (↑(t₂ * t₁) : M) * ((↑(a * c).2 : M) * (b * d).1)
⊢ ∃ (c_1 : ↥S), (↑c_1 : M) * ((↑(b * d).2 : M) * (a * c).1) = (↑c_1 : M) * ((↑(a * c).2 : M) * (b * d).1)

Tactic:
use t₂ * t₁
-- 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
a b c d : M × ↥S
t₁ : ↥S
ht₁ : (↑t₁ : M) * ((↑b.2 : M) * a.1) = (↑t₁ : M) * ((↑a.2 : M) * b.1)
t₂ : ↥S
ht₂ : (↑t₂ : M) * ((↑d.2 : M) * c.1) = (↑t₂ : M) * ((↑c.2 : M) * d.1)
⊢ (↑t₂ : M) * (↑t₁ : M) * ((↑b.2 : M) * (↑d.2 : M) * (a.1 * c.1)) =
    (↑t₂ : M) * ((↑d.2 : M) * c.1) * ((↑t₁ : M) * ((↑b.2 : M) * a.1))

Tactic:
ac_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
P : Type u_3
inst_2 : CommMonoid P
a b c d : M × ↥S
t₁ : ↥S
ht₁ : (↑t₁ : M) * ((↑b.2 : M) * a.1) = (↑t₁ : M) * ((↑a.2 : M) * b.1)
t₂ : ↥S
ht₂ : (↑t₂ : M) * ((↑d.2 : M) * c.1) = (↑t₂ : M) * ((↑c.2 : M) * d.1)
rw :
  (↑t₂ : M) * ((↑c.2 : M) * d.1) * ((↑t₁ : M) * ((↑a.2 : M) * b.1)) =
    (↑t₂ : M) * (↑t₁ : M) * ((↑a.2 : M) * (↑c.2 : M) * (b.1 * d.1))
⊢ (↑t₂ : M) * ((↑d.2 : M) * c.1) * ((↑t₁ : M) * ((↑b.2 : M) * a.1)) =
    (↑t₂ : M) * (↑t₁ : M) * ((↑a.2 : M) * (↑c.2 : M) * (b.1 * d.1))

Tactic:
rw [ht₁, ht₂]
-- 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
a b c d : M × ↥S
t₁ : ↥S
ht₁ : (↑t₁ : M) * ((↑b.2 : M) * a.1) = (↑t₁ : M) * ((↑a.2 : M) * b.1)
t₂ : ↥S
ht₂ : (↑t₂ : M) * ((↑d.2 : M) * c.1) = (↑t₂ : M) * ((↑c.2 : M) * d.1)
⊢ (↑t₂ : M) * ((↑c.2 : M) * d.1) * ((↑t₁ : M) * ((↑a.2 : M) * b.1)) =
    (↑t₂ : M) * (↑t₁ : M) * ((↑a.2 : M) * (↑c.2 : M) * (b.1 * d.1))

Tactic:
ac_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
P : Type u_3
inst_2 : CommMonoid P
a b c d : M × ↥S
t₁ : ↥S
ht₁ : (↑t₁ : M) * ((↑b.2 : M) * a.1) = (↑t₁ : M) * ((↑a.2 : M) * b.1)
t₂ : ↥S
ht₂ : (↑t₂ : M) * ((↑d.2 : M) * c.1) = (↑t₂ : M) * ((↑c.2 : M) * d.1)
t₃ :
  (↑t₂ : M) * (↑t₁ : M) * ((↑b.2 : M) * (↑d.2 : M) * (a.1 * c.1)) =
    (↑t₂ : M) * ((↑d.2 : M) * c.1) * ((↑t₁ : M) * ((↑b.2 : M) * a.1))
t₄ :
  (↑t₂ : M) * ((↑d.2 : M) * c.1) * ((↑t₁ : M) * ((↑b.2 : M) * a.1)) =
    (↑t₂ : M) * (↑t₁ : M) * ((↑a.2 : M) * (↑c.2 : M) * (b.1 * d.1))
⊢ (↑(t₂ * t₁) : M) * ((↑(b * d).2 : M) * (a * c).1) = (↑(t₂ * t₁) : M) * ((↑(a * c).2 : M) * (b * d).1)

Tactic:
calc
      (t₂ * t₁ : M) * (b.2 * d.2 * (a.1 * c.1)) = t₂ * (d.2 * c.1) * (t₁ * (b.2 * a.1)) := by ac_rfl
      _ = (t₂ * t₁ : M) * (a.2 * c.2 * (b.1 * d.1)) := by rw [ht₁, ht₂]; ac_rfl

Premises used: HMul.hMul, Prod.fst, Subtype.val, Prod.snd
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x : ↥S
⊢ (↑1 : M) * ((↑((↑x : M), x).2 : M) * 1.1) = (↑1 : M) * ((↑1.2 : M) * ((↑x : M), x).1)

Tactic:
simp
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
b : Con (M × ↥S)
H :
  Membership.mem (γ := Set (Con (M × ↥S)))
    {c : Con (M × ↥S) | ∀ (y : ↥S), (c : (a : M × ↥S) → M × ↥S → Prop) 1 ((↑y : M), y)} b
x_1 x_2 : M × ↥S
p : M
q : ↥S
x : M
y : ↥S
h : (r' S : (a : M × ↥S) → M × ↥S → Prop) (p, q) (x, y)
t : ↥S
ht : (↑t : M) * ((↑(x, y).2 : M) * (p, q).1) = (↑t : M) * ((↑(p, q).2 : M) * (x, y).1)
rw : (b : (a : M × ↥S) → M × ↥S → Prop) (1 * (p, q)) (1 * (x, y))
⊢ (b : (a : M × ↥S) → M × ↥S → Prop) (p, q) (x, y)

Tactic:
rw [← one_mul (p, q), ← one_mul (x, y)]

Premises used: Prod.mk, one_mul
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
b : Con (M × ↥S)
H :
  Membership.mem (γ := Set (Con (M × ↥S)))
    {c : Con (M × ↥S) | ∀ (y : ↥S), (c : (a : M × ↥S) → M × ↥S → Prop) 1 ((↑y : M), y)} b
x_1 x_2 : M × ↥S
p : M
q : ↥S
x : M
y : ↥S
h : (r' S : (a : M × ↥S) → M × ↥S → Prop) (p, q) (x, y)
t : ↥S
ht : (↑t : M) * ((↑(x, y).2 : M) * (p, q).1) = (↑t : M) * ((↑(p, q).2 : M) * (x, y).1)
⊢ (b : (a : M × ↥S) → M × ↥S → Prop) (1 * (p, q)) (1 * (x, y))

Tactic:
b.trans (b.mul (H (t * y)) (b.refl _)) ?_

Premises used: Con.mul, HMul.hMul, Con.trans, Con.refl
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
b : Con (M × ↥S)
H :
  Membership.mem (γ := Set (Con (M × ↥S)))
    {c : Con (M × ↥S) | ∀ (y : ↥S), (c : (a : M × ↥S) → M × ↥S → Prop) 1 ((↑y : M), y)} b
x_1 x_2 : M × ↥S
p : M
q : ↥S
x : M
y : ↥S
h : (r' S : (a : M × ↥S) → M × ↥S → Prop) (p, q) (x, y)
t : ↥S
ht : (↑t : M) * ((↑(x, y).2 : M) * (p, q).1) = (↑t : M) * ((↑(p, q).2 : M) * (x, y).1)
refine : (b : (a : M × ↥S) → M × ↥S → Prop) (((↑(t * y) : M), t * y) * (p, q)) (1 * (x, y))
⊢ (b : (a : M × ↥S) → M × ↥S → Prop) (1 * (p, q)) (1 * (x, y))

Tactic:
refine b.trans (b.mul (H (t * y)) (b.refl _)) ?_

Premises used: Con.mul, HMul.hMul, Con.trans, Con.refl
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
b : Con (M × ↥S)
H :
  Membership.mem (γ := Set (Con (M × ↥S)))
    {c : Con (M × ↥S) | ∀ (y : ↥S), (c : (a : M × ↥S) → M × ↥S → Prop) 1 ((↑y : M), y)} b
x_1 x_2 : M × ↥S
p : M
q : ↥S
x : M
y : ↥S
h : (r' S : (a : M × ↥S) → M × ↥S → Prop) (p, q) (x, y)
t : ↥S
ht : (↑t : M) * ((↑(x, y).2 : M) * (p, q).1) = (↑t : M) * ((↑(p, q).2 : M) * (x, y).1)
⊢ (b : (a : M × ↥S) → M × ↥S → Prop) (((↑(t * q) : M), t * q) * (x, y)) (1 * (x, y))

Tactic:
b.symm (b.mul (H (t * q)) (b.refl (x, y)))

Premises used: Con.mul, HMul.hMul, Con.refl, Prod.mk, Con.symm
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
b : Con (M × ↥S)
H :
  Membership.mem (γ := Set (Con (M × ↥S)))
    {c : Con (M × ↥S) | ∀ (y : ↥S), (c : (a : M × ↥S) → M × ↥S → Prop) 1 ((↑y : M), y)} b
x_1 x_2 : M × ↥S
p : M
q : ↥S
x : M
y : ↥S
h_1 : (r' S : (a : M × ↥S) → M × ↥S → Prop) (p, q) (x, y)
t : ↥S
ht : (↑t : M) * ((↑(x, y).2 : M) * (p, q).1) = (↑t : M) * ((↑(p, q).2 : M) * (x, y).1)
h : ((↑(t * y) : M), t * y) * (p, q) = ((↑(t * q) : M), t * q) * (x, y)
⊢ (b : (a : M × ↥S) → M × ↥S → Prop) (((↑(t * y) : M), t * y) * (p, q)) (1 * (x, y))

Tactic:
convert! b.symm (b.mul (H (t * q)) (b.refl (x, y))) using 1

Premises used: Con.mul, HMul.hMul, Con.refl, Prod.mk, Con.symm
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
b : Con (M × ↥S)
H :
  Membership.mem (γ := Set (Con (M × ↥S)))
    {c : Con (M × ↥S) | ∀ (y : ↥S), (c : (a : M × ↥S) → M × ↥S → Prop) 1 ((↑y : M), y)} b
x_1 x_2 : M × ↥S
p : M
q : ↥S
x : M
y : ↥S
h_1 : (r' S : (a : M × ↥S) → M × ↥S → Prop) (p, q) (x, y)
t : ↥S
ht : (↑t : M) * ((↑(x, y).2 : M) * (p, q).1) = (↑t : M) * ((↑(p, q).2 : M) * (x, y).1)
h : ((↑t : M) * (↑y : M) * p, t * y * q) = ((↑t : M) * (↑q : M) * x, t * q * y)
⊢ ((↑(t * y) : M), t * y) * (p, q) = ((↑(t * q) : M), t * q) * (x, y)

Tactic:
dsimp only [Prod.mk_mul_mk, Submonoid.coe_mul] at ht ⊢

Premises used: Prod.mk_mul_mk, Submonoid.coe_mul
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
b : Con (M × ↥S)
H :
  Membership.mem (γ := Set (Con (M × ↥S)))
    {c : Con (M × ↥S) | ∀ (y : ↥S), (c : (a : M × ↥S) → M × ↥S → Prop) 1 ((↑y : M), y)} b
x_1 x_2 : M × ↥S
p : M
q : ↥S
x : M
y : ↥S
h_1 : (r' S : (a : M × ↥S) → M × ↥S → Prop) (p, q) (x, y)
t : ↥S
ht : (↑t : M) * ((↑y : M) * p) = (↑t : M) * ((↑q : M) * x)
h : ((↑t : M) * ((↑y : M) * p), t * (y * q)) = ((↑t : M) * ((↑q : M) * x), t * (q * y))
h₁ : ((↑t : M) * ((↑q : M) * x), t * (y * q)) = ((↑t : M) * ((↑q : M) * x), t * (q * y))
⊢ ((↑t : M) * (↑y : M) * p, t * y * q) = ((↑t : M) * (↑q : M) * x, t * q * y)

Tactic:
simp_rw [mul_assoc, ht, mul_comm y q]

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x y : M × ↥S
⊢ (r S : (a : M × ↥S) → M × ↥S → Prop) x y ↔ ∃ (c : ↥S), (↑c : M) * ((↑y.2 : M) * x.1) = (↑c : M) * ((↑x.2 : M) * y.1)

Tactic:
simp only [r_eq_r' S, r', Con.rel_mk]

Premises used: Localization.r_eq_r', Con.rel_mk, Localization.r'
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x y : M × ↥S
simp :
  (∃ a ∈ S, a * ((↑y.2 : M) * x.1) = a * ((↑x.2 : M) * y.1)) ↔
    ∃ a ∈ S, ∃ (v : M), a * y.1 = v * x.1 ∧ a * (↑y.2 : M) = v * (↑x.2 : M)
⊢ (r S : (a : M × ↥S) → M × ↥S → Prop) x y ↔ (OreLocalization.oreEqv S M : M × ↥S → M × ↥S → Prop) x y

Tactic:
simp +instances only [r_iff_exists, Subtype.exists, exists_prop, OreLocalization.oreEqv,
    smul_eq_mul, Submonoid.mk_smul]

Premises used: Subtype.exists, Submonoid.mk_smul, exists_prop, Localization.r_iff_exists, smul_eq_mul, OreLocalization.oreEqv
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x y : M × ↥S
mp :
  (∃ a ∈ S, a * ((↑y.2 : M) * x.1) = a * ((↑x.2 : M) * y.1)) →
    ∃ a ∈ S, ∃ (v : M), a * y.1 = v * x.1 ∧ a * (↑y.2 : M) = v * (↑x.2 : M)
mpr :
  (∃ a ∈ S, ∃ (v : M), a * y.1 = v * x.1 ∧ a * (↑y.2 : M) = v * (↑x.2 : M)) →
    ∃ a ∈ S, a * ((↑y.2 : M) * x.1) = a * ((↑x.2 : M) * y.1)
⊢ (∃ a ∈ S, a * ((↑y.2 : M) * x.1) = a * ((↑x.2 : M) * y.1)) ↔
    ∃ a ∈ S, ∃ (v : M), a * y.1 = v * x.1 ∧ a * (↑y.2 : M) = v * (↑x.2 : M)

Tactic:
constructor
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x y : M × ↥S
u : M
hu : u ∈ S
e : u * ((↑y.2 : M) * x.1) = u * ((↑x.2 : M) * y.1)
rw : u * ((↑x.2 : M) * y.1) = u * (↑y.2 : M) * x.1
rw₁ : u * ((↑x.2 : M) * y.1) = u * ((↑y.2 : M) * x.1)
rw₂ rw₃ : u * ((↑y.2 : M) * x.1) = u * ((↑y.2 : M) * x.1)
⊢ u * (↑x.2 : M) * y.1 = u * (↑y.2 : M) * x.1

Tactic:
rw [mul_assoc, mul_assoc, ← e]

Premises used: mul_assoc
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x y : M × ↥S
u : M
hu : u ∈ S
e : u * ((↑y.2 : M) * x.1) = u * ((↑x.2 : M) * y.1)
⊢ ∃ a ∈ S, ∃ (v : M), a * y.1 = v * x.1 ∧ a * (↑y.2 : M) = v * (↑x.2 : M)

Tactic:
exact ⟨_, mul_mem hu x.2.2, u * y.2, by rw [mul_assoc, mul_assoc, ← e], mul_right_comm _ _ _⟩
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x y : M × ↥S
u : M
hu : u ∈ S
v : M
e₁ : u * y.1 = v * x.1
e₂ : u * (↑y.2 : M) = v * (↑x.2 : M)
rw : u * (↑y.2 : M) * x.1 = u * ((↑x.2 : M) * y.1)
rw₁ : v * (↑x.2 : M) * x.1 = u * ((↑x.2 : M) * y.1)
rw₂ : v * x.1 * (↑x.2 : M) = u * ((↑x.2 : M) * y.1)
rw₃ : u * y.1 * (↑x.2 : M) = u * ((↑x.2 : M) * y.1)
rw₄ : u * (y.1 * (↑x.2 : M)) = u * ((↑x.2 : M) * y.1)
rw₅ rw₆ : u * ((↑x.2 : M) * y.1) = u * ((↑x.2 : M) * y.1)
⊢ u * ((↑y.2 : M) * x.1) = u * ((↑x.2 : M) * y.1)

Tactic:
rw [← mul_assoc, e₂, mul_right_comm, ← e₁, mul_assoc, mul_comm y.1]

Premises used: mul_assoc, Prod.fst, mul_right_comm, mul_comm
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x y : M × ↥S
u : M
hu : u ∈ S
v : M
e₁ : u * y.1 = v * x.1
e₂ : u * (↑y.2 : M) = v * (↑x.2 : M)
⊢ ∃ a ∈ S, a * ((↑y.2 : M) * x.1) = a * ((↑x.2 : M) * y.1)

Tactic:
exact ⟨u, hu, by rw [← mul_assoc, e₂, mul_right_comm, ← e₁, mul_assoc, mul_comm y.1]⟩
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
a c : M
b d : ↥S
⊢ mk a b = mk c d ↔ (r S : (a : M × ↥S) → M × ↥S → Prop) (a, b) (c, d)

Tactic:
simp +instances only [mk, OreLocalization.oreDiv_eq_iff, r_iff_oreEqv_r, OreLocalization.oreEqv]

Premises used: OreLocalization.oreDiv_eq_iff, Localization.mk, Localization.r_iff_oreEqv_r, OreLocalization.oreEqv
-- 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
p : Localization S → Sort u
f : (a : M) → (b : ↥S) → p (mk a b)
H :
  ∀ {a c : M} {b d : ↥S} (h : (r S : (a : M × ↥S) → M × ↥S → Prop) (a, b) (c, d)),
    Eq.ndrec (motive := p) (f a b) ⋯ = f c d
x : Localization S
y : M × ↥S
⊢ mk y.1 y.2 = Quot.mk (⇑(OreLocalization.oreEqv S M) : M × ↥S → M × ↥S → Prop) y

Tactic:
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
P : Type u_3
inst_2 : CommMonoid P
p : Localization S → Sort u
f : (a : M) → (b : ↥S) → p (Localization.mk a b)
H :
  ∀ {a c : M} {b d : ↥S} (h : (r S : (a : M × ↥S) → M × ↥S → Prop) (a, b) (c, d)),
    Eq.ndrec (motive := p) (f a b) ⋯ = f c d
x : Localization S
y z : M × ↥S
h : (OreLocalization.oreEqv S M : M × ↥S → M × ↥S → Prop) y z
mk :
  ∀ (fst : M) (snd : ↥S) (h : (OreLocalization.oreEqv S M : M × ↥S → M × ↥S → Prop) (fst, snd) z),
    Eq.ndrec (motive := fun (x : Localization S) ↦ p x) (Eq.ndrec (motive := p) (f (fst, snd).1 (fst, snd).2) ⋯) ⋯ =
      Eq.ndrec (motive := p) (f z.1 z.2) ⋯
⊢ Eq.ndrec (motive := fun (x : Localization S) ↦ p x) (Eq.ndrec (motive := p) (f y.1 y.2) ⋯) ⋯ =
    Eq.ndrec (motive := p) (f z.1 z.2) ⋯

Tactic:
cases y
-- 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
p : Localization S → Sort u
f : (a : M) → (b : ↥S) → p (Localization.mk a b)
H :
  ∀ {a c : M} {b d : ↥S} (h : (r S : (a : M × ↥S) → M × ↥S → Prop) (a, b) (c, d)),
    Eq.ndrec (motive := p) (f a b) ⋯ = f c d
x : Localization S
z : M × ↥S
fst : M
snd : ↥S
h : (OreLocalization.oreEqv S M : M × ↥S → M × ↥S → Prop) (fst, snd) z
mk :
  ∀ (fst_1 : M) (snd_1 : ↥S) (h : (OreLocalization.oreEqv S M : M × ↥S → M × ↥S → Prop) (fst, snd) (fst_1, snd_1)),
    Eq.ndrec (motive := fun (x : Localization S) ↦ p x) (Eq.ndrec (motive := p) (f (fst, snd).1 (fst, snd).2) ⋯) ⋯ =
      Eq.ndrec (motive := p) (f (fst_1, snd_1).1 (fst_1, snd_1).2) ⋯
⊢ Eq.ndrec (motive := fun (x : Localization S) ↦ p x) (Eq.ndrec (motive := p) (f (fst, snd).1 (fst, snd).2) ⋯) ⋯ =
    Eq.ndrec (motive := p) (f z.1 z.2) ⋯

Tactic:
cases z
-- 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
p : Localization S → Sort u
f : (a : M) → (b : ↥S) → p (mk a b)
H :
  ∀ {a c : M} {b d : ↥S} (h : (r S : (a : M × ↥S) → M × ↥S → Prop) (a, b) (c, d)),
    Eq.ndrec (motive := p) (f a b) ⋯ = f c d
x : Localization S
fst : M
snd : ↥S
fst_1 : M
snd_1 : ↥S
h : (OreLocalization.oreEqv S M : M × ↥S → M × ↥S → Prop) (fst, snd) (fst_1, snd_1)
⊢ Eq.ndrec (motive := fun (x : Localization S) ↦ p x) (Eq.ndrec (motive := p) (f (fst, snd).1 (fst, snd).2) ⋯) ⋯ =
    Eq.ndrec (motive := p) (f (fst_1, snd_1).1 (fst_1, snd_1).2) ⋯

Tactic:
H (r_iff_oreEqv_r.mpr h)

Premises used: Iff.mpr, Localization.mk, OreLocalization, Quotient, Quotient.mk', Localization.r_iff_oreEqv_r, OreLocalization.oreDiv
-- 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
p : Localization S → Sort u
f : (a : M) → (b : ↥S) → p (mk a b)
H :
  ∀ {a c : M} {b d : ↥S} (h : (r S : (a : M × ↥S) → M × ↥S → Prop) (a, b) (c, d)),
    Eq.ndrec (motive := p) (f a b) ⋯ = f c d
x : Localization S
fst : M
snd : ↥S
fst_1 : M
snd_1 : ↥S
h : (OreLocalization.oreEqv S M : M × ↥S → M × ↥S → Prop) (fst, snd) (fst_1, snd_1)
⊢ Eq.ndrec (motive := fun (x : Localization S) ↦ p x) (Eq.ndrec (motive := p) (f (fst, snd).1 (fst, snd).2) ⋯) ⋯ =
    Eq.ndrec (motive := p) (f (fst_1, snd_1).1 (fst_1, snd_1).2) ⋯

Tactic:
exact H (r_iff_oreEqv_r.mpr h)

Premises used: Iff.mpr, Localization.r_iff_oreEqv_r
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
a c : M
b d : ↥S
⊢ mk a b * mk c d = mk (a * c) (b * d)

Tactic:
mul_comm b d ▸ OreLocalization.oreDiv_mul_oreDiv

Premises used: OreLocalization.oreDiv_mul_oreDiv, Eq.rec, mul_comm, Eq.symm
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
⊢ Eq.{u_1 + 1} (α := Localization S) (mk 1 1) 1

Tactic:
OreLocalization.one_def

Premises used: Localization.mk, OreLocalization.one, Quotient.mk', OreLocalization.one_def, OreLocalization.oreDiv
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
n : ℕ
a : M
b : ↥S
zero : HPow.hPow (β := ℕ) (mk a b) 0 = mk (HPow.hPow (β := ℕ) a 0) (HPow.hPow (β := ℕ) b 0)
succ : ∀ (n : ℕ), mk a b ^ n = mk (a ^ n) (b ^ n) → mk a b ^ (n + 1) = mk (a ^ (n + 1)) (b ^ (n + 1))
⊢ mk a b ^ n = mk (a ^ n) (b ^ n)

Tactic:
induction n
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
a : M
b : ↥S
⊢ HPow.hPow (β := ℕ) (mk a b) 0 = mk (HPow.hPow (β := ℕ) a 0) (HPow.hPow (β := ℕ) b 0)

Tactic:
simp [pow_succ, *, ← mk_mul, ← mk_one]

Premises used: pow_succ, Localization.mk_one, Localization.mk_mul
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
a : M
b : ↥S
n : ℕ
h : mk a b ^ n = mk (a ^ n) (b ^ n)
⊢ mk a b ^ (n + 1) = mk (a ^ (n + 1)) (b ^ (n + 1))

Tactic:
simp [pow_succ, *, ← mk_mul, ← mk_one]

Premises used: pow_succ, Localization.mk_one, Localization.mk_mul
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
s : ι → ↥S
empty : Eq.{u_1 + 1} (α := Localization S) (∏ i ∈ ∅, mk (f i) (s i)) (mk (∏ i ∈ ∅, f i) (∏ i ∈ ∅, s i))
insert :
  ∀ (a : ι) (s_1 : Finset ι),
    a ∉ s_1 →
      Eq.{u_1 + 1} (α := Localization S) (∏ i ∈ s_1, mk (f i) (s i)) (mk (∏ i ∈ s_1, f i) (∏ i ∈ s_1, s i)) →
        Eq.{u_1 + 1} (α := Localization S) (∏ i ∈ Insert.insert a s_1, mk (f i) (s i))
          (mk (∏ i ∈ Insert.insert a s_1, f i) (∏ i ∈ Insert.insert a s_1, s i))
⊢ Eq.{u_1 + 1} (α := Localization S) (∏ i ∈ t, mk (f i) (s i)) (mk (∏ i ∈ t, f i) (∏ i ∈ t, s i))

Tactic:
induction t using Finset.induction_on
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
ι : Type u_4
f : ι → M
s : ι → ↥S
⊢ Eq.{u_1 + 1} (α := Localization S) (∏ i ∈ ∅, mk (f i) (s i)) (mk (∏ i ∈ ∅, f i) (∏ i ∈ ∅, s i))

Tactic:
simp [mk_one, Finset.prod_insert, *, mk_mul]

Premises used: Finset.prod_insert, Localization.mk_one, Localization.mk_mul
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
ι : Type u_4
f : ι → M
s : ι → ↥S
a : ι
s_1 : Finset ι
h : a ∉ s_1
h_1 : Eq.{u_1 + 1} (α := Localization S) (∏ i ∈ s_1, mk (f i) (s i)) (mk (∏ i ∈ s_1, f i) (∏ i ∈ s_1, s i))
⊢ Eq.{u_1 + 1} (α := Localization S) (∏ i ∈ insert a s_1, mk (f i) (s i))
    (mk (∏ i ∈ insert a s_1, f i) (∏ i ∈ insert a s_1, s i))

Tactic:
simp [mk_one, Finset.prod_insert, *, mk_mul]

Premises used: Finset.prod_insert, Localization.mk_one, Localization.mk_mul