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
ι : 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))
⊢ Eq.{u_1 + 1} (α := Localization S) (∏ i ∈ t, mk (f i) (s i)) (mk (∏ i ∈ t, f i) (∏ i ∈ t, s i))
have 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 a s_1, mk (f i) (s i))
        (mk (∏ i ∈ insert a s_1, f i) (∏ i ∈ insert a s_1, s i))
Tactic: induction t using Finset.induction_on
Cleared hypotheses: t
-- 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: classical
  induction t using Finset.induction_on <;> simp [mk_one, Finset.prod_insert, *, mk_mul]
Cleared hypotheses: t
-- 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
empty : Eq.{u_1 + 1} (α := Localization S) (∏ i ∈ ∅, mk (f i) (s i)) (mk (∏ i ∈ ∅, f i) (∏ i ∈ ∅, s i))
⊢ Eq.{u_1 + 1} (α := Localization S) (∏ i ∈ t, mk (f i) (s i)) (mk (∏ i ∈ t, f i) (∏ i ∈ t, s i))
have 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 a s_1, mk (f i) (s i))
        (mk (∏ i ∈ insert a s_1, f i) (∏ i ∈ insert a s_1, s i))
Tactic: classical
  induction t using Finset.induction_on <;> simp [mk_one, Finset.prod_insert, *, mk_mul]
Cleared hypotheses: t
-- 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
h : (↑y.2 : M) * x.1 = (↑x.2 : M) * y.1
⊢ (↑1 : M) * ((↑y.2 : M) * x.1) = (↑1 : M) * ((↑x.2 : M) * y.1)
have rw : (↑1 : M) * ((↑x.2 : M) * y.1) = (↑1 : M) * ((↑x.2 : M) * y.1)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
a : ↥S
⊢ mk (↑a : M) a = 1
have symm : 1 = mk (↑a : M) a
Tactic: symm
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
a : ↥S
⊢ 1 = mk (↑a : M) a
have rw : (r S : (a : M × ↥S) → M × ↥S → Prop) (1, 1) ((↑a : M), a)
Tactic: rw [← mk_one, mk_eq_mk_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
R : Type u_4
inst_1 : SMul R M
inst_2 : IsScalarTower R M M
c : R
a : M
b : ↥S
⊢ c • mk a b = mk (c • a) b
have rw : Eq (α := Localization S)
  (OreLocalization.oreNum (HSMul.hSMul (β := M) c 1) b • a /ₒ
    (OreLocalization.oreDenom (HSMul.hSMul (β := M) c 1) b * 1))
  (c • a /ₒ b)
Tactic: rw [mk, mk, ← OreLocalization.smul_one_oreDiv_one_smul, OreLocalization.oreDiv_smul_oreDiv]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
R : Type u_4
inst_1 : SMul R M
inst_2 : IsScalarTower R M M
c : R
a : M
b : ↥S
⊢ Eq (α := Localization S)
    (OreLocalization.oreNum (HSMul.hSMul (β := M) c 1) b • a /ₒ
      (OreLocalization.oreDenom (HSMul.hSMul (β := M) c 1) b * 1))
    (c • a /ₒ b)
have change : Eq (α := OreLocalization S M) (HSMul.hSMul (β := M) c 1 • a /ₒ (b * 1)) (c • a /ₒ b)
Tactic: change (c • 1) • a /ₒ (b * 1) = _
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
R : Type u_4
inst_1 : SMul R M
inst_2 : IsScalarTower R M M
c : R
a : M
b : ↥S
⊢ Eq (α := OreLocalization S M) (HSMul.hSMul (β := M) c 1 • a /ₒ (b * 1)) (c • a /ₒ b)
have rw : Eq (α := OreLocalization S M) (c • HSMul.hSMul (α := M) 1 a /ₒ (b * 1)) (c • a /ₒ b)
Tactic: rw [smul_assoc, one_smul, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
R : Type u_4
inst_1 : SMul R M
inst_2 : IsScalarTower R M M
c : R
a : M
b : ↥S
rw : Eq (α := OreLocalization S M) (c • HSMul.hSMul (α := M) 1 a /ₒ (b * 1)) (c • a /ₒ b)
⊢ Eq (α := OreLocalization S M) (HSMul.hSMul (β := M) c 1 • a /ₒ (b * 1)) (c • a /ₒ b)
have rw₁ : Eq (α := OreLocalization S M) (c • a /ₒ (b * 1)) (c • a /ₒ b)
Tactic: rw [smul_assoc, one_smul, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
R : Type u_4
inst_1 : SMul R M
inst_2 : IsScalarTower R M M
c : R
a : M
b : ↥S
rw : Eq (α := OreLocalization S M) (c • HSMul.hSMul (α := M) 1 a /ₒ (b * 1)) (c • a /ₒ b)
rw₁ : Eq (α := OreLocalization S M) (c • a /ₒ (b * 1)) (c • a /ₒ b)
⊢ Eq (α := OreLocalization S M) (HSMul.hSMul (β := M) c 1 • a /ₒ (b * 1)) (c • a /ₒ b)
have rw₂ : Eq (α := OreLocalization S M) (c • a /ₒ b) (c • a /ₒ b)
Tactic: rw [smul_assoc, one_smul, 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
F : Type u_4
inst_2 : FunLike F M N
inst_3 : MulHomClass F M N
f : F
hf : IsLocalizationMap.{u_1, u_2} (N := N) S (⇑f : (a : M) → N)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) 1 : N) (1 : N)
have rw : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑1 : M) : N) ((f : (a : M) → N) 1 : N) = (f : (a : M) → N) (↑1 : M)
Tactic: rw [← (hf.map_units 1).mul_right_inj, 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
f g : S.LocalizationMap N
⊢ f.toMonoidHom = g.toMonoidHom → f = g
have mk : ∀ (toMulHom : M →ₙ* N) (isLocalizationMap : S.IsLocalizationMap toMulHom.toFun),
  { toMulHom := toMulHom, isLocalizationMap := isLocalizationMap : S.LocalizationMap N }.toMonoidHom = g.toMonoidHom →
    { toMulHom := toMulHom, isLocalizationMap := isLocalizationMap : S.LocalizationMap N } = g
Tactic: cases f
Cleared hypotheses: f
-- 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
g : S.LocalizationMap N
toMulHom : M →ₙ* N
isLocalizationMap : S.IsLocalizationMap toMulHom.toFun
⊢ { toMulHom := toMulHom, isLocalizationMap := isLocalizationMap : S.LocalizationMap N }.toMonoidHom = g.toMonoidHom →
    { toMulHom := toMulHom, isLocalizationMap := isLocalizationMap : S.LocalizationMap N } = g
have mk : ∀
  (eq :
    { toMulHom := toMulHom, isLocalizationMap := isLocalizationMap : S.LocalizationMap N }.toMonoidHom = g.toMonoidHom),
  toMulHom = g.toMulHom
Tactic: congr! with eq
-- 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
g : S.LocalizationMap N
toMulHom : M →ₙ* N
isLocalizationMap : S.IsLocalizationMap toMulHom.toFun
eq : { toMulHom := toMulHom, isLocalizationMap := isLocalizationMap : S.LocalizationMap N }.toMonoidHom = g.toMonoidHom
⊢ toMulHom = g.toMulHom
have mk : ∀ (x : M), Eq.{u_2 + 1} (α := N) ((toMulHom : (a : M) → N) x : N) ((g.toMulHom : (a : M) → N) x : N)
Tactic: ext
-- 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
z w : N
⊢ ∃ (z' : M) (w' : M) (d : ↥S),
    HMul.hMul (β := N) z ((f : (a : M) → N) (↑d : M) : N) = (f : (a : M) → N) z' ∧
      HMul.hMul (β := N) w ((f : (a : M) → N) (↑d : M) : N) = (f : (a : M) → N) w'
have let : ∀ (a : M × ↥S) (ha : HMul.hMul (β := N) z ((f : (a : M) → N) (↑a.2 : M) : N) = (f : (a : M) → N) a.1),
  ∃ (z' : M) (w' : M) (d : ↥S),
    HMul.hMul (β := N) z ((f : (a : M) → N) (↑d : M) : N) = (f : (a : M) → N) z' ∧
      HMul.hMul (β := N) w ((f : (a : M) → N) (↑d : M) : N) = (f : (a : M) → N) w'
Tactic: let ⟨a, ha⟩ := surj f z
-- 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
z w : N
a : M × ↥S
ha : HMul.hMul (β := N) z ((f : (a : M) → N) (↑a.2 : M) : N) = (f : (a : M) → N) a.1
⊢ ∃ (z' : M) (w' : M) (d : ↥S),
    HMul.hMul (β := N) z ((f : (a : M) → N) (↑d : M) : N) = (f : (a : M) → N) z' ∧
      HMul.hMul (β := N) w ((f : (a : M) → N) (↑d : M) : N) = (f : (a : M) → N) w'
have let : ∀ (b : M × ↥S) (hb : HMul.hMul (β := N) w ((f : (a : M) → N) (↑b.2 : M) : N) = (f : (a : M) → N) b.1),
  ∃ (z' : M) (w' : M) (d : ↥S),
    HMul.hMul (β := N) z ((f : (a : M) → N) (↑d : M) : N) = (f : (a : M) → N) z' ∧
      HMul.hMul (β := N) w ((f : (a : M) → N) (↑d : M) : N) = (f : (a : M) → N) w'
Tactic: let ⟨b, hb⟩ := surj f w
-- 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
z w : N
a : M × ↥S
ha : HMul.hMul (β := N) z ((f : (a : M) → N) (↑a.2 : M) : N) = (f : (a : M) → N) a.1
b : M × ↥S
hb : HMul.hMul (β := N) w ((f : (a : M) → N) (↑b.2 : M) : N) = (f : (a : M) → N) b.1
⊢ ∃ (z' : M) (w' : M) (d : ↥S),
    HMul.hMul (β := N) z ((f : (a : M) → N) (↑d : M) : N) = (f : (a : M) → N) z' ∧
      HMul.hMul (β := N) w ((f : (a : M) → N) (↑d : M) : N) = (f : (a : M) → N) w'
have refine_1 : HMul.hMul (β := N) z ((f : (a : M) → N) (↑(a.2 * b.2) : M) : N) = (f : (a : M) → N) (a.1 * (↑b.2 : M))
Tactic: refine ⟨a.1 * b.2, a.2 * b.1, a.2 * 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
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : HMul.hMul (β := N) z ((f : (a : M) → N) (↑a.2 : M) : N) = (f : (a : M) → N) a.1
b : M × ↥S
hb : HMul.hMul (β := N) w ((f : (a : M) → N) (↑b.2 : M) : N) = (f : (a : M) → N) b.1
refine_1 : HMul.hMul (β := N) z ((f : (a : M) → N) (↑(a.2 * b.2) : M) : N) = (f : (a : M) → N) (a.1 * (↑b.2 : M))
⊢ ∃ (z' : M) (w' : M) (d : ↥S),
    HMul.hMul (β := N) z ((f : (a : M) → N) (↑d : M) : N) = (f : (a : M) → N) z' ∧
      HMul.hMul (β := N) w ((f : (a : M) → N) (↑d : M) : N) = (f : (a : M) → N) w'
have refine_2 : HMul.hMul (β := N) w ((f : (a : M) → N) (↑(a.2 * b.2) : M) : N) = (f : (a : M) → N) ((↑a.2 : M) * b.1)
Tactic: refine ⟨a.1 * b.2, a.2 * b.1, a.2 * 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
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : HMul.hMul (β := N) z ((f : (a : M) → N) (↑a.2 : M) : N) = (f : (a : M) → N) a.1
b : M × ↥S
hb : HMul.hMul (β := N) w ((f : (a : M) → N) (↑b.2 : M) : N) = (f : (a : M) → N) b.1
⊢ HMul.hMul (β := N) z ((f : (a : M) → N) (↑(a.2 * b.2) : M) : N) = (f : (a : M) → N) (a.1 * (↑b.2 : M))
have refine_1 : z * HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑a.2 : M) : N) ((f : (a : M) → N) (↑b.2 : M) : N) =
  HMul.hMul (β := N) (HMul.hMul (β := N) z ((f : (a : M) → N) (↑a.2 : M) : N)) ((f : (a : M) → N) (↑b.2 : M) : N)
Tactic: simp_rw [mul_def, map_mul, ← ha]
-- 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
z w : N
a : M × ↥S
ha : HMul.hMul (β := N) z ((f : (a : M) → N) (↑a.2 : M) : N) = (f : (a : M) → N) a.1
b : M × ↥S
hb : HMul.hMul (β := N) w ((f : (a : M) → N) (↑b.2 : M) : N) = (f : (a : M) → N) b.1
⊢ HMul.hMul (β := N) w ((f : (a : M) → N) (↑(a.2 * b.2) : M) : N) = (f : (a : M) → N) ((↑a.2 : M) * b.1)
have refine_2 : w * HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑a.2 : M) : N) ((f : (a : M) → N) (↑b.2 : M) : N) =
  HMul.hMul (α := N) ((f : (a : M) → N) (↑a.2 : M) : N) (HMul.hMul (β := N) w ((f : (a : M) → N) (↑b.2 : M) : N))
Tactic: simp_rw [mul_def, map_mul, ← hb]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (hypothesis)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
f : S.LocalizationMap N
x y : M
h_1 : ∃ (c : ↥S), (↑c : M) * x = (↑c : M) * y
c : ↥S
h : (↑c : M) * x = (↑c : M) * y
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
have h₁ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) ((↑c : M) * x) : N) ((f : (a : M) → N) ((↑c : M) * y) : N)
Tactic: replace h := congr_arg f h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (hypothesis)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
f : S.LocalizationMap N
x y : M
h_1 : ∃ (c : ↥S), (↑c : M) * x = (↑c : M) * y
c : ↥S
h : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) ((↑c : M) * x) : N) ((f : (a : M) → N) ((↑c : M) * y) : N)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
have h₁ : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑c : M) : N) ((f : (a : M) → N) x : N) =
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑c : M) : N) ((f : (a : M) → N) y : N)
Tactic: rw [map_mul, map_mul] at h
Cleared hypotheses: 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
f : S.LocalizationMap N
z : N
⊢ (f : (a : M) → N) (f.sec z).1 = HMul.hMul (α := N) ((f : (a : M) → N) (↑(f.sec z).2 : M) : N) z
have rw : (f : (a : M) → N) (f.sec z).1 = HMul.hMul (β := N) z ((f : (a : M) → N) (↑(f.sec z).2 : M) : N)
Tactic: rw [mul_comm, sec_spec]
-- 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
z : N
rw : (f : (a : M) → N) (f.sec z).1 = HMul.hMul (β := N) z ((f : (a : M) → N) (↑(f.sec z).2 : M) : N)
⊢ (f : (a : M) → N) (f.sec z).1 = HMul.hMul (α := N) ((f : (a : M) → N) (↑(f.sec z).2 : M) : N) z
have rw₁ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (f.sec z).1 : N) ((f : (a : M) → N) (f.sec z).1 : N)
Tactic: rw [mul_comm, sec_spec]
-- 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 : M →* N
h : ∀ (y : ↥S), IsUnit.{u_2} (M := N) ((f : (a : M) → N) (↑y : M) : N)
y : ↥S
w z : N
⊢ w * (↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y)⁻¹ : N) = z ↔
    w = HMul.hMul (α := N) ((f : (a : M) → N) (↑y : M) : N) z
have rw : (↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y)⁻¹ : N) * w = z ↔
  w = HMul.hMul (α := N) ((f : (a : M) → N) (↑y : M) : N) z
Tactic: rw [mul_comm]
-- 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 : M →* N
h : ∀ (y : ↥S), IsUnit.{u_2} (M := N) ((f : (a : M) → N) (↑y : M) : N)
y : ↥S
w z : N
⊢ z = w * (↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y)⁻¹ : N) ↔
    HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N) = w
have rw : w * (↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y)⁻¹ : N) = z ↔
  HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N) = w
Tactic: rw [eq_comm, mul_inv_left h, mul_comm, eq_comm]
-- 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 : M →* N
h : ∀ (y : ↥S), IsUnit.{u_2} (M := N) ((f : (a : M) → N) (↑y : M) : N)
y : ↥S
w z : N
rw :
  w * (↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y)⁻¹ : N) = z ↔
    HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N) = w
⊢ z = w * (↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y)⁻¹ : N) ↔
    HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N) = w
have rw₁ : w = HMul.hMul (α := N) ((f : (a : M) → N) (↑y : M) : N) z ↔ HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N) = w
Tactic: rw [eq_comm, mul_inv_left h, mul_comm, eq_comm]
-- 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 : M →* N
h : ∀ (y : ↥S), IsUnit.{u_2} (M := N) ((f : (a : M) → N) (↑y : M) : N)
y : ↥S
w z : N
rw :
  w * (↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y)⁻¹ : N) = z ↔
    HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N) = w
rw₁ :
  w = HMul.hMul (α := N) ((f : (a : M) → N) (↑y : M) : N) z ↔ HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N) = w
⊢ z = w * (↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y)⁻¹ : N) ↔
    HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N) = w
have rw₂ : w = HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N) ↔ HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N) = w
Tactic: rw [eq_comm, mul_inv_left h, mul_comm, eq_comm]
-- 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 : M →* N
h : ∀ (y : ↥S), IsUnit.{u_2} (M := N) ((f : (a : M) → N) (↑y : M) : N)
y : ↥S
w z : N
rw :
  w * (↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y)⁻¹ : N) = z ↔
    HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N) = w
rw₁ :
  w = HMul.hMul (α := N) ((f : (a : M) → N) (↑y : M) : N) z ↔ HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N) = w
rw₂ :
  w = HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N) ↔ HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N) = w
⊢ z = w * (↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y)⁻¹ : N) ↔
    HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N) = w
have rw₃ : HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N) = w ↔ HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N) = w
Tactic: rw [eq_comm, mul_inv_left h, mul_comm, eq_comm]
-- 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 : M →* N
h : ∀ (y : ↥S), IsUnit.{u_2} (M := N) ((f : (a : M) → N) (↑y : M) : N)
x₁ x₂ : M
y₁ y₂ : ↥S
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₁ : N)
        ((↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y₁)⁻¹ : N) : N) =
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₂ : N)
        ((↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y₂)⁻¹ : N) : N) ↔
    Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (x₁ * (↑y₂ : M)) : N) ((f : (a : M) → N) (x₂ * (↑y₁ : M)) : N)
have rw : HMul.hMul (β := N)
      (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₁ : N)
        ((↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y₁)⁻¹ : N) : N))
      ((f : (a : M) → N) (↑y₂ : M) : N) =
    (f : (a : M) → N) x₂ ↔
  Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (x₁ * (↑y₂ : M)) : N) ((f : (a : M) → N) (x₂ * (↑y₁ : M)) : N)
Tactic: rw [mul_inv_right h, mul_assoc, mul_comm _ (f y₂), ← mul_assoc, mul_inv_left h, mul_comm x₂,
    f.map_mul, f.map_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
f : M →* N
h : ∀ (y : ↥S), IsUnit.{u_2} (M := N) ((f : (a : M) → N) (↑y : M) : N)
x₁ x₂ : M
y₁ y₂ : ↥S
rw :
  HMul.hMul (β := N)
        (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₁ : N)
          ((↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y₁)⁻¹ : N) : N))
        ((f : (a : M) → N) (↑y₂ : M) : N) =
      (f : (a : M) → N) x₂ ↔
    Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (x₁ * (↑y₂ : M)) : N) ((f : (a : M) → N) (x₂ * (↑y₁ : M)) : N)
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₁ : N)
        ((↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y₁)⁻¹ : N) : N) =
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₂ : N)
        ((↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y₂)⁻¹ : N) : N) ↔
    Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (x₁ * (↑y₂ : M)) : N) ((f : (a : M) → N) (x₂ * (↑y₁ : M)) : N)
have rw₁ : HMul.hMul (α := N) ((f : (a : M) → N) x₁ : N)
      (HMul.hMul (α := N) (β := N) ((↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y₁)⁻¹ : N) : N)
        ((f : (a : M) → N) (↑y₂ : M) : N)) =
    (f : (a : M) → N) x₂ ↔
  Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (x₁ * (↑y₂ : M)) : N) ((f : (a : M) → N) (x₂ * (↑y₁ : M)) : N)
Tactic: rw [mul_inv_right h, mul_assoc, mul_comm _ (f y₂), ← mul_assoc, mul_inv_left h, mul_comm x₂,
    f.map_mul, f.map_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
f : M →* N
h : ∀ (y : ↥S), IsUnit.{u_2} (M := N) ((f : (a : M) → N) (↑y : M) : N)
x₁ x₂ : M
y₁ y₂ : ↥S
rw :
  HMul.hMul (β := N)
        (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₁ : N)
          ((↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y₁)⁻¹ : N) : N))
        ((f : (a : M) → N) (↑y₂ : M) : N) =
      (f : (a : M) → N) x₂ ↔
    Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (x₁ * (↑y₂ : M)) : N) ((f : (a : M) → N) (x₂ * (↑y₁ : M)) : N)
rw₁ :
  HMul.hMul (α := N) ((f : (a : M) → N) x₁ : N)
        (HMul.hMul (α := N) (β := N) ((↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y₁)⁻¹ : N) : N)
          ((f : (a : M) → N) (↑y₂ : M) : N)) =
      (f : (a : M) → N) x₂ ↔
    Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (x₁ * (↑y₂ : M)) : N) ((f : (a : M) → N) (x₂ * (↑y₁ : M)) : N)
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₁ : N)
        ((↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y₁)⁻¹ : N) : N) =
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₂ : N)
        ((↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y₂)⁻¹ : N) : N) ↔
    Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (x₁ * (↑y₂ : M)) : N) ((f : (a : M) → N) (x₂ * (↑y₁ : M)) : N)
have rw₂ : HMul.hMul (α := N) ((f : (a : M) → N) x₁ : N)
      (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑y₂ : M) : N)
        ((↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y₁)⁻¹ : N) : N)) =
    (f : (a : M) → N) x₂ ↔
  Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (x₁ * (↑y₂ : M)) : N) ((f : (a : M) → N) (x₂ * (↑y₁ : M)) : N)
Tactic: rw [mul_inv_right h, mul_assoc, mul_comm _ (f y₂), ← mul_assoc, mul_inv_left h, mul_comm x₂,
    f.map_mul, f.map_mul]