awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
f : S.LocalizationMap N
P : Type u_4
inst_2 : Monoid P
j k : N →* P
n : N
m : M
s : ↥S
hn : HMul.hMul (β := N) n ((f : (a : M) → N) (↑s : M) : N) = (f : (a : M) → N) m
h :
  ∀ (a : M),
    Eq.{u_4 + 1} (α := P) ((j : (a : N) → P) ((f : (a : M) → N) a : N) : P)
      ((k : (a : N) → P) ((f : (a : M) → N) a : N) : P)
rw :
  (j : (a : N) → P) (HMul.hMul (β := N) n ((f : (a : M) → N) (↑s : M) : N)) =
    HMul.hMul (α := P) (β := P) ((k : (a : N) → P) n : P) ((j : (a : N) → P) ((f : (a : M) → N) (↑s : M) : N) : P)
rw₁ :
  (j : (a : N) → P) (HMul.hMul (β := N) n ((f : (a : M) → N) (↑s : M) : N)) =
    HMul.hMul (α := P) (β := P) ((k : (a : N) → P) n : P) ((k : (a : N) → P) ((f : (a : M) → N) (↑s : M) : N) : P)
rw₂ :
  Eq.{u_4 + 1} (α := P) ((j : (a : N) → P) (HMul.hMul (β := N) n ((f : (a : M) → N) (↑s : M) : N)) : P)
    ((k : (a : N) → P) (HMul.hMul (β := N) n ((f : (a : M) → N) (↑s : M) : N)) : P)
rw₃ :
  Eq.{u_4 + 1} (α := P) ((j : (a : N) → P) ((f : (a : M) → N) m : N) : P)
    ((k : (a : N) → P) ((f : (a : M) → N) m : N) : P)
⊢ HMul.hMul (α := P) (β := P) ((j : (a : N) → P) n : P) ((j : (a : N) → P) ((f : (a : M) → N) (↑s : M) : N) : P) =
    HMul.hMul (α := P) (β := P) ((k : (a : N) → P) n : P) ((j : (a : N) → P) ((f : (a : M) → N) (↑s : M) : N) : P)
have rw₄ : Eq.{u_4 + 1} (α := P) ((k : (a : N) → P) ((f : (a : M) → N) m : N) : P)
  ((k : (a : N) → P) ((f : (a : M) → N) m : N) : P)
Tactic: rw [← j.map_mul, h, ← k.map_mul, hn, h m]
-- 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
x y : M
⊢ mk (x * y) 1 = HMul.hMul (α := Localization S) (mk x 1) (mk y 1)
have rw : mk (x * y) 1 = mk (x * y) (HMul.hMul (α := ↥S) 1 1)
Tactic: rw [mk_mul, mul_one]
-- 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
x y : M
rw : mk (x * y) 1 = mk (x * y) (HMul.hMul (α := ↥S) 1 1)
⊢ mk (x * y) 1 = HMul.hMul (α := Localization S) (mk x 1) (mk y 1)
have rw₁ : Eq (α := Localization S) (mk (x * y) 1) (mk (x * y) 1)
Tactic: rw [mk_mul, mul_one]
-- 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
y : ↥S
⊢ mk (↑y : M) 1 * mk 1 y = 1
have rw : mk ((↑y : M) * 1) (1 * y) = 1
Tactic: rw [mk_mul, mul_one, one_mul, 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
y : ↥S
rw : mk ((↑y : M) * 1) (1 * y) = 1
⊢ mk (↑y : M) 1 * mk 1 y = 1
have rw₁ : mk (↑y : M) (1 * y) = 1
Tactic: rw [mk_mul, mul_one, one_mul, 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
y : ↥S
rw : mk ((↑y : M) * 1) (1 * y) = 1
rw₁ : mk (↑y : M) (1 * y) = 1
⊢ mk (↑y : M) 1 * mk 1 y = 1
have rw₂ : mk (↑y : M) y = 1
Tactic: rw [mk_mul, mul_one, one_mul, 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
y : ↥S
rw : mk ((↑y : M) * 1) (1 * y) = 1
rw₁ : mk (↑y : M) (1 * y) = 1
rw₂ : mk (↑y : M) y = 1
⊢ mk (↑y : M) 1 * mk 1 y = 1
have rw₃ : Eq.{u_1 + 1} (α := Localization S) 1 1
Tactic: rw [mk_mul, mul_one, one_mul, 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
z : Localization S
x : M × ↥S
⊢ mk x.1 x.2 * mk (↑x.2 : M) 1 = mk x.1 1
have rw : mk (x.1 * (↑x.2 : M)) (x.2 * 1) = mk x.1 1
Tactic: rw [mk_mul, mul_comm x.fst, ← mk_mul, mk_self, one_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
z : Localization S
x : M × ↥S
rw : mk (x.1 * (↑x.2 : M)) (x.2 * 1) = mk x.1 1
⊢ mk x.1 x.2 * mk (↑x.2 : M) 1 = mk x.1 1
have rw₁ : mk ((↑x.2 : M) * x.1) (x.2 * 1) = mk x.1 1
Tactic: rw [mk_mul, mul_comm x.fst, ← mk_mul, mk_self, one_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
z : Localization S
x : M × ↥S
rw : mk (x.1 * (↑x.2 : M)) (x.2 * 1) = mk x.1 1
rw₁ : mk ((↑x.2 : M) * x.1) (x.2 * 1) = mk x.1 1
⊢ mk x.1 x.2 * mk (↑x.2 : M) 1 = mk x.1 1
have rw₂ : mk (↑x.2 : M) x.2 * mk x.1 1 = mk x.1 1
Tactic: rw [mk_mul, mul_comm x.fst, ← mk_mul, mk_self, one_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
z : Localization S
x : M × ↥S
rw : mk (x.1 * (↑x.2 : M)) (x.2 * 1) = mk x.1 1
rw₁ : mk ((↑x.2 : M) * x.1) (x.2 * 1) = mk x.1 1
rw₂ : mk (↑x.2 : M) x.2 * mk x.1 1 = mk x.1 1
⊢ mk x.1 x.2 * mk (↑x.2 : M) 1 = mk x.1 1
have rw₃ : HMul.hMul (α := Localization S) 1 (mk x.1 1) = mk x.1 1
Tactic: rw [mk_mul, mul_comm x.fst, ← mk_mul, mk_self, one_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
z : Localization S
x : M × ↥S
rw : mk (x.1 * (↑x.2 : M)) (x.2 * 1) = mk x.1 1
rw₁ : mk ((↑x.2 : M) * x.1) (x.2 * 1) = mk x.1 1
rw₂ : mk (↑x.2 : M) x.2 * mk x.1 1 = mk x.1 1
rw₃ : HMul.hMul (α := Localization S) 1 (mk x.1 1) = mk x.1 1
⊢ mk x.1 x.2 * mk (↑x.2 : M) 1 = mk x.1 1
have rw₄ : Eq (α := Localization S) (mk x.1 1) (mk x.1 1)
Tactic: rw [mk_mul, mul_comm x.fst, ← mk_mul, mk_self, one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x : M
y : ↥S
⊢ HMul.hMul (β := Localization S) (mk x y) ((monoidOf S : (a : M) → Localization S) (↑y : M) : Localization S) =
    (monoidOf S : (a : M) → Localization S) x
have rw : mk (x * (↑y : M)) (1 * y) = mk x 1
Tactic: rw [← mk_one_eq_monoidOf_mk, ← mk_one_eq_monoidOf_mk, mk_mul x y y 1, 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 : M
y : ↥S
| mk (x * (↑y : M)) (1 * y) = mk x 1
have rhs : mk x 1
Tactic: rhs
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x : M
y : ↥S
| mk x 1
have rw : mk x (HMul.hMul (α := ↥S) 1 1)
Tactic: rw [← mul_one 1]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x : M
y : ↥S
| mk x (HMul.hMul (α := ↥S) 1 1)
have rw : mk (x * 1) (HMul.hMul (α := ↥S) 1 1)
Tactic: rw [← mul_one x]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x : M
y : ↥S
| mk (x * (↑y : M)) (1 * y) = mk x 1
have rw : mk (x * 1) (HMul.hMul (α := ↥S) 1 1)
Tactic: rhs; rw [← mul_one 1]; rw [← mul_one x]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x : M
y : ↥S
⊢ mk (x * (↑y : M)) (1 * y) = mk x 1
have conv : mk (x * (↑y : M)) (1 * y) = mk (x * 1) (HMul.hMul (α := ↥S) 1 1)
Tactic: conv => rhs; rw [← mul_one 1]; rw [← mul_one x]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
p : Sort u
f : M → ↥S → p
H : ∀ {a c : M} {b d : ↥S}, (r S : (a : M × ↥S) → M × ↥S → Prop) (a, b) (c, d) → f a b = f c d
a : M
b : ↥S
⊢ ((monoidOf S).mk' a b).liftOn f @H = f a b
have rw : (mk a b).liftOn f @H = f a b
Tactic: rw [← mk_eq_monoidOf_mk', liftOn_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
p : Sort u
f : M → ↥S → p
H : ∀ {a c : M} {b d : ↥S}, (r S : (a : M × ↥S) → M × ↥S → Prop) (a, b) (c, d) → f a b = f c d
a : M
b : ↥S
rw : (mk a b).liftOn f @H = f a b
⊢ ((monoidOf S).mk' a b).liftOn f @H = f a b
have rw₁ : f a b = f a b
Tactic: rw [← mk_eq_monoidOf_mk', liftOn_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
p : Sort u_4
f : M → ↥S → M → ↥S → p
H :
  ∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥S},
    (r S : (a : M × ↥S) → M × ↥S → Prop) (a, b) (a', b') →
      (r S : (a : M × ↥S) → M × ↥S → Prop) (c, d) (c', d') → f a b c d = f a' b' c' d'
a c : M
b d : ↥S
⊢ ((monoidOf S).mk' a b).liftOn₂ ((monoidOf S).mk' c d) f @H = f a b c d
have rw : (mk a b).liftOn₂ (mk c d) f @H = f a b c d
Tactic: rw [← mk_eq_monoidOf_mk', liftOn₂_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
p : Sort u_4
f : M → ↥S → M → ↥S → p
H :
  ∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥S},
    (r S : (a : M × ↥S) → M × ↥S → Prop) (a, b) (a', b') →
      (r S : (a : M × ↥S) → M × ↥S → Prop) (c, d) (c', d') → f a b c d = f a' b' c' d'
a c : M
b d : ↥S
rw : (mk a b).liftOn₂ (mk c d) f @H = f a b c d
⊢ ((monoidOf S).mk' a b).liftOn₂ ((monoidOf S).mk' c d) f @H = f a b c d
have rw₁ : f a b c d = f a b c d
Tactic: rw [← mk_eq_monoidOf_mk', liftOn₂_mk]
-- 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
inst_3 : IsMulTorsionFree M
n : ℕ
hn : n ≠ 0
a₁ : Localization S
a : M × ↥S
a₂ : Localization S
b : M × ↥S
hab : mk a.1 a.2 ^ n = mk b.1 b.2 ^ n
⊢ Eq (α := Localization S) (Quot.mk (⇑(OreLocalization.oreEqv S M) : M × ↥S → M × ↥S → Prop) a)
    (Quot.mk (⇑(OreLocalization.oreEqv S M) : M × ↥S → M × ↥S → Prop) b)
have mk : mk a.1 a.2 = mk b.1 b.2
Tactic: change mk a.1 a.2 = mk b.1 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
inst_3 : IsMulTorsionFree M
n : ℕ
hn : n ≠ 0
a₁ : Localization S
a : M × ↥S
a₂ : Localization S
b : M × ↥S
hab : mk a.1 a.2 ^ n = mk b.1 b.2 ^ n
⊢ mk a.1 a.2 = mk b.1 b.2
have 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)
Tactic: simp only [mk_pow, mk_eq_mk_iff, r_iff_exists, SubmonoidClass.coe_pow, Subtype.exists,
      exists_prop] at hab ⊢
Cleared hypotheses: hab
-- 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
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)
⊢ ∃ a_1 ∈ S, a_1 * ((↑b.2 : M) * a.1) = a_1 * ((↑a.2 : M) * b.1)
have 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)
Tactic: obtain ⟨c, hc, hab⟩ := hab
Cleared hypotheses: hab
-- 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
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)
have 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)))
Tactic: refine ⟨c, hc, pow_left_injective hn ?_⟩
-- 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
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)
⊢ 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)))
have 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)))
Tactic: obtain _ | n := n
Cleared hypotheses: n, hn, hab
-- 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
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)))
⊢ 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)))
have 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)))
Tactic: obtain _ | n := n
Cleared hypotheses: n, hn, hab
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
⊢ mk a₁ a₂ = mk b₁ b₂ ↔ (↑b₂ : α) * a₁ = (↑a₂ : α) * b₁
have simp_rw : (r s : (a : α × ↥s) → α × ↥s → Prop) (a₁, a₂) (b₁, b₂) ↔ (↑b₂ : α) * a₁ = (↑a₂ : α) * b₁
Tactic: simp_rw [mk_eq_mk_iff, r_iff_exists, mul_left_cancel_iff, exists_const]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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₁
⊢ mk a₁ a₂ = mk b₁ b₂ ↔ (↑b₂ : α) * a₁ = (↑a₂ : α) * b₁
have simp_rw₁ : (∃ (c : ↥s), (↑c : α) * ((↑b₂ : α) * a₁) = (↑c : α) * ((↑a₂ : α) * b₁)) ↔ (↑b₂ : α) * a₁ = (↑a₂ : α) * b₁
Tactic: simp_rw [mk_eq_mk_iff, r_iff_exists, mul_left_cancel_iff, exists_const]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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₁
⊢ mk a₁ a₂ = mk b₁ b₂ ↔ (↑b₂ : α) * a₁ = (↑a₂ : α) * b₁
have simp_rw₂ : (∃ (c : ↥s), (↑b₂ : α) * a₁ = (↑a₂ : α) * b₁) ↔ (↑b₂ : α) * a₁ = (↑a₂ : α) * b₁
Tactic: simp_rw [mk_eq_mk_iff, r_iff_exists, mul_left_cancel_iff, exists_const]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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)
have 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'
Tactic: refine ⟨fun g g' eq ↦ ?_, fun m ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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'
⊢ Bijective.{u_2 + 1, u_1 + 1} (α := G) (β := M) (⇑f : (a : G) → M)
have refine_2 : ∀ (m : M), ∃ (a : G), (f : (a : G) → M) a = m
Tactic: refine ⟨fun g g' eq ↦ ?_, fun m ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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)
⊢ g = g'
have refine_1 : ∀ (c : ↥S) (eq : (↑c : G) * g = (↑c : G) * g'), g = g'
Tactic: have ⟨c, eq⟩ := h.exists_of_eq eq
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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
⊢ ∃ (a : G), (f : (a : G) → M) a = m
have 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
Tactic: have ⟨x, eq⟩ := h.surj m
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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
⊢ ∃ (a : G), (f : (a : G) → M) a = m
have h₁ : (f : (a : G) → M) (x.1 / (↑x.2 : G)) = m
Tactic: use x.1 / x.2
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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
⊢ (f : (a : G) → M) (x.1 / (↑x.2 : G)) = m
have h₁ : (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]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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
⊢ (f : (a : G) → M) (x.1 / (↑x.2 : G)) = m
have h₂ : HMul.hMul (α := M) (β := M) ((f : (a : G) → M) x.1 : M) ((f : (a : G) → M) (↑x.2 : G)⁻¹ : M) = m
Tactic: rw [div_eq_mul_inv, map_mul, ← eq, mul_assoc, ← map_mul, mul_inv_cancel, h.map_one, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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
⊢ (f : (a : G) → M) (x.1 / (↑x.2 : G)) = m
have 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
Tactic: rw [div_eq_mul_inv, map_mul, ← eq, mul_assoc, ← map_mul, mul_inv_cancel, h.map_one, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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
⊢ (f : (a : G) → M) (x.1 / (↑x.2 : G)) = m
have h₄ : m * HMul.hMul (α := M) (β := M) ((f : (a : G) → M) (↑x.2 : G) : M) ((f : (a : G) → M) (↑x.2 : G)⁻¹ : M) = m
Tactic: rw [div_eq_mul_inv, map_mul, ← eq, mul_assoc, ← map_mul, mul_inv_cancel, h.map_one, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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
⊢ (f : (a : G) → M) (x.1 / (↑x.2 : G)) = m
have h₅ : HMul.hMul (β := M) m ((f : (a : G) → M) ((↑x.2 : G) * (↑x.2 : G)⁻¹) : M) = m
Tactic: rw [div_eq_mul_inv, map_mul, ← eq, mul_assoc, ← map_mul, mul_inv_cancel, h.map_one, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
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
⊢ (f : (a : G) → M) (x.1 / (↑x.2 : G)) = m
have h₆ : HMul.hMul (β := M) m ((f : (a : G) → M) 1 : M) = m
Tactic: rw [div_eq_mul_inv, map_mul, ← eq, mul_assoc, ← map_mul, mul_inv_cancel, h.map_one, mul_one]