awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Away (goal)
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 : Type u_4
inst_3 : AddCommMonoid A
x : A
B : Type u_5
inst_4 : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst_5 : AddCommMonoid C
g : A →+ C
y : A
G : AwayMap (x + y) C
rw :
  mk' G (x + y)
      (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := AddSubmonoid A) (multiples (x + y)) x_1) (x + y) ⋯) =
    0
⊢ HAdd.hAdd (α := C) ((G : (a : A) → C) x : C)
      (mk' G y
        (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := AddSubmonoid A) (multiples (x + y)) x_1) (x + y) ⋯)) =
    0
have rw₁ : Eq.{u_6 + 1} (α := C) 0 0
Tactic: rw [add_mk'_eq_mk'_of_add, mk'_self]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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
⊢ Con (M × ↥S)
have refine_1 : ∀ {x y z : M × ↥S},
  (∃ (c : ↥S), (↑c : M) * ((↑y.2 : M) * x.1) = (↑c : M) * ((↑x.2 : M) * y.1)) →
    (∃ (c : ↥S), (↑c : M) * ((↑z.2 : M) * y.1) = (↑c : M) * ((↑y.2 : M) * z.1)) →
      ∃ (c : ↥S), (↑c : M) * ((↑z.2 : M) * x.1) = (↑c : M) * ((↑x.2 : M) * z.1)
Tactic: refine
    { r := fun a b : M × S ↦ ∃ c : S, ↑c * (↑b.2 * a.1) = c * (a.2 * b.1)
      iseqv := ⟨fun a ↦ ⟨1, rfl⟩, fun ⟨c, hc⟩ ↦ ⟨c, hc.symm⟩, ?_⟩
      mul' := ?_ }
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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
refine_1 :
  ∀ {x y z : M × ↥S},
    (∃ (c : ↥S), (↑c : M) * ((↑y.2 : M) * x.1) = (↑c : M) * ((↑x.2 : M) * y.1)) →
      (∃ (c : ↥S), (↑c : M) * ((↑z.2 : M) * y.1) = (↑c : M) * ((↑y.2 : M) * z.1)) →
        ∃ (c : ↥S), (↑c : M) * ((↑z.2 : M) * x.1) = (↑c : M) * ((↑x.2 : M) * z.1)
⊢ Con (M × ↥S)
have refine_2 : ∀ {w x y z : M × ↥S},
  (∃ (c : ↥S), (↑c : M) * ((↑x.2 : M) * w.1) = (↑c : M) * ((↑w.2 : M) * x.1)) →
    (∃ (c : ↥S), (↑c : M) * ((↑z.2 : M) * y.1) = (↑c : M) * ((↑y.2 : M) * z.1)) →
      ∃ (c : ↥S), (↑c : M) * ((↑(x * z).2 : M) * (w * y).1) = (↑c : M) * ((↑(w * y).2 : M) * (x * z).1)
Tactic: refine
    { r := fun a b : M × S ↦ ∃ c : S, ↑c * (↑b.2 * a.1) = c * (a.2 * b.1)
      iseqv := ⟨fun a ↦ ⟨1, rfl⟩, fun ⟨c, hc⟩ ↦ ⟨c, hc.symm⟩, ?_⟩
      mul' := ?_ }
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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)
⊢ ∃ (c_1 : ↥S), (↑c_1 : M) * ((↑c.2 : M) * a.1) = (↑c_1 : M) * ((↑a.2 : M) * c.1)
have h : (↑(t₂ * t₁ * b.2) : M) * ((↑c.2 : M) * a.1) = (↑(t₂ * t₁ * b.2) : M) * ((↑a.2 : M) * c.1)
Tactic: use t₂ * t₁ * b.2
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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₁ * b.2) : M) * ((↑c.2 : M) * a.1) = (↑(t₂ * t₁ * b.2) : M) * ((↑a.2 : M) * c.1)
have h : (↑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: simp only [Submonoid.coe_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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) * ((↑b.2 : M) * a.1)) = (↑t₁ : M) * (↑a.2 : M) * ((↑t₂ : M) * ((↑c.2 : M) * b.1))
have rw : (↑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: rw [ht₁]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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) * ((↑c.2 : M) * b.1)) = (↑t₂ : M) * (↑t₁ : M) * (↑b.2 : M) * ((↑a.2 : M) * c.1)
have 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)
Tactic: rw [ht₂]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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) * (↑t₁ : M) * (↑b.2 : M) * ((↑c.2 : M) * a.1) = (↑t₂ : M) * (↑t₁ : M) * (↑b.2 : M) * ((↑a.2 : M) * c.1)
have 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))
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
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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₂ : M) * (↑t₁ : M) * (↑b.2 : M) * ((↑c.2 : M) * a.1) = (↑t₂ : M) * (↑t₁ : M) * (↑b.2 : M) * ((↑a.2 : M) * c.1)
have 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))
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
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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₂ : M) * (↑t₁ : M) * (↑b.2 : M) * ((↑c.2 : M) * a.1) = (↑t₂ : M) * (↑t₁ : M) * (↑b.2 : M) * ((↑a.2 : M) * c.1)
have 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)
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
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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)
⊢ ∃ (c_1 : ↥S), (↑c_1 : M) * ((↑(b * d).2 : M) * (a * c).1) = (↑c_1 : M) * ((↑(a * c).2 : M) * (b * d).1)
have h : (↑(t₂ * t₁) : M) * ((↑(b * d).2 : M) * (a * c).1) = (↑(t₂ * t₁) : M) * ((↑(a * c).2 : M) * (b * d).1)
Tactic: use t₂ * t₁
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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) * ((↑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))
have 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))
Tactic: rw [ht₁, ht₂]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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) * ((↑(b * d).2 : M) * (a * c).1) = (↑(t₂ * t₁) : M) * ((↑(a * c).2 : M) * (b * d).1)
have 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))
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
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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) * ((↑(b * d).2 : M) * (a * c).1) = (↑(t₂ * t₁) : M) * ((↑(a * c).2 : M) * (b * d).1)
have 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))
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
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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) (p, q) (x, y)
have rw : (b : (a : M × ↥S) → M × ↥S → Prop) (1 * (p, q)) (1 * (x, y))
Tactic: rw [← one_mul (p, q), ← one_mul (x, y)]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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))
have refine : (b : (a : M × ↥S) → M × ↥S → Prop) (((↑(t * y) : M), t * y) * (p, q)) (1 * (x, y))
Tactic: refine b.trans (b.mul (H (t * y)) (b.refl _)) ?_
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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 * y) : M), t * y) * (p, q)) (1 * (x, y))
have h : ((↑(t * y) : M), t * y) * (p, q) = ((↑(t * q) : M), t * q) * (x, y)
Tactic: convert! b.symm (b.mul (H (t * q)) (b.refl (x, y))) using 1
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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)
⊢ ((↑(t * y) : M), t * y) * (p, q) = ((↑(t * q) : M), t * q) * (x, y)
have h : ((↑t : M) * (↑y : M) * p, t * y * q) = ((↑t : M) * (↑q : M) * x, t * q * y)
Tactic: dsimp only [Prod.mk_mul_mk, Submonoid.coe_mul] at ht ⊢
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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) * ((↑y : M) * p) = (↑t : M) * ((↑q : M) * x)
⊢ ((↑t : M) * (↑y : M) * p, t * y * q) = ((↑t : M) * (↑q : M) * x, t * q * y)
have h : ((↑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]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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))
⊢ ((↑t : M) * (↑y : M) * p, t * y * q) = ((↑t : M) * (↑q : M) * x, t * q * y)
have h₁ : ((↑t : M) * ((↑q : M) * x), t * (y * q)) = ((↑t : M) * ((↑q : M) * x), t * (q * y))
Tactic: simp_rw [mul_assoc, ht, mul_comm y q]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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 ↔ (OreLocalization.oreEqv S M : M × ↥S → M × ↥S → Prop) x y
have 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)
Tactic: simp +instances only [r_iff_exists, Subtype.exists, exists_prop, OreLocalization.oreEqv,
    smul_eq_mul, Submonoid.mk_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x y : M × ↥S
⊢ (∃ 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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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)
⊢ (∃ 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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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)
⊢ u * (↑x.2 : M) * y.1 = u * (↑y.2 : M) * x.1
have rw : u * ((↑x.2 : M) * y.1) = u * (↑y.2 : M) * x.1
Tactic: rw [mul_assoc, mul_assoc, ← e]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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
⊢ u * (↑x.2 : M) * y.1 = u * (↑y.2 : M) * x.1
have rw₁ : u * ((↑x.2 : M) * y.1) = u * ((↑y.2 : M) * x.1)
Tactic: rw [mul_assoc, mul_assoc, ← e]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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)
⊢ u * (↑x.2 : M) * y.1 = u * (↑y.2 : M) * x.1
have rw₂ : u * ((↑y.2 : M) * x.1) = u * ((↑y.2 : M) * x.1)
Tactic: rw [mul_assoc, mul_assoc, ← e]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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)
⊢ u * ((↑y.2 : M) * x.1) = u * ((↑x.2 : M) * y.1)
have rw : 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]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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)
⊢ u * ((↑y.2 : M) * x.1) = u * ((↑x.2 : M) * y.1)
have rw₁ : v * (↑x.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]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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)
⊢ u * ((↑y.2 : M) * x.1) = u * ((↑x.2 : M) * y.1)
have rw₂ : v * x.1 * (↑x.2 : M) = u * ((↑x.2 : M) * y.1)
Tactic: rw [← mul_assoc, e₂, mul_right_comm, ← e₁, mul_assoc, mul_comm y.1]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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)
⊢ u * ((↑y.2 : M) * x.1) = u * ((↑x.2 : M) * y.1)
have rw₃ : u * y.1 * (↑x.2 : M) = u * ((↑x.2 : M) * y.1)
Tactic: rw [← mul_assoc, e₂, mul_right_comm, ← e₁, mul_assoc, mul_comm y.1]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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)
⊢ u * ((↑y.2 : M) * x.1) = u * ((↑x.2 : M) * y.1)
have rw₄ : u * (y.1 * (↑x.2 : M)) = u * ((↑x.2 : M) * y.1)
Tactic: rw [← mul_assoc, e₂, mul_right_comm, ← e₁, mul_assoc, mul_comm y.1]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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)
⊢ u * ((↑y.2 : M) * x.1) = u * ((↑x.2 : M) * y.1)
have rw₅ : u * ((↑x.2 : M) * y.1) = u * ((↑x.2 : M) * y.1)
Tactic: rw [← mul_assoc, e₂, mul_right_comm, ← e₁, mul_assoc, mul_comm y.1]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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 z : M × ↥S
h : (OreLocalization.oreEqv S M : M × ↥S → M × ↥S → Prop) y z
⊢ 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) ⋯
have 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) sorry) sorry =
    Eq.ndrec (motive := p) (f z.1 z.2) sorry
Tactic: cases y
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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
z : M × ↥S
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) ⋯
have 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) sorry) sorry =
    Eq.ndrec (motive := p) (f (fst_1, snd_1).1 (fst_1, snd_1).2) sorry
Tactic: cases z
Cleared hypotheses: z, h
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
n : ℕ
a : M
b : ↥S
⊢ mk a b ^ n = mk (a ^ n) (b ^ n)
have zero : HPow.hPow (β := ℕ) (mk a b) 0 = mk (HPow.hPow (β := ℕ) a 0) (HPow.hPow (β := ℕ) b 0)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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)
⊢ mk a b ^ n = mk (a ^ n) (b ^ n)
have succ : ∀ (n : ℕ), mk a b ^ n = mk (a ^ n) (b ^ n) → mk a b ^ (n + 1) = mk (a ^ (n + 1)) (b ^ (n + 1))
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
s : ι → ↥S
⊢ Eq.{u_1 + 1} (α := Localization S) (∏ i ∈ t, mk (f i) (s i)) (mk (∏ i ∈ t, f i) (∏ i ∈ t, s i))
have empty : Eq.{u_1 + 1} (α := Localization S) (∏ i ∈ ∅, mk (f i) (s i)) (mk (∏ i ∈ ∅, f i) (∏ i ∈ ∅, s i))
Tactic: induction t using Finset.induction_on
Cleared hypotheses: t