awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Lemmas (goal)
Goal:
M : Type u_1
N : Type u_2
F : Type u_3
ι : Type u_4
inst : Finite ι
inst_1 : CommMonoid M
inst_2 : CommMonoid N
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
f : F
S : Submonoid M
hf : IsLocalizationMap.{u_1, u_2} (N := N) S (⇑f : (a : M) → N)
n : ι → N
x : (z : N) → M × ↥S
hx : ∀ (z : N), HMul.hMul (β := N) z ((f : (a : M) → N) (↑(x z).2 : M) : N) = (f : (a : M) → N) (x z).1
val : Fintype ι
i : ι
rw :
  HMul.hMul (β := N) (n i) ((f : (a : M) → N) (↑((x (n i)).2 * ∏ x_1 ∈ erase univ i, (x (n x_1)).2) : M) : N) =
    (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)
⊢ HMul.hMul (β := N) (n i) ((f : (a : M) → N) (↑(∏ i : ι, (x (n i)).2) : M) : N) =
    (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)
have rw₁ : HMul.hMul (β := N) (n i) ((f : (a : M) → N) ((↑(x (n i)).2 : M) * (↑(∏ x_1 ∈ erase univ i, (x (n x_1)).2) : M)) : N) =
  (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)
Tactic: rw [← univ.mul_prod_erase _ (mem_univ i), S.coe_mul, map_mul, ← mul_assoc, hx, map_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Lemmas (goal)
Goal:
M : Type u_1
N : Type u_2
F : Type u_3
ι : Type u_4
inst : Finite ι
inst_1 : CommMonoid M
inst_2 : CommMonoid N
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
f : F
S : Submonoid M
hf : IsLocalizationMap.{u_1, u_2} (N := N) S (⇑f : (a : M) → N)
n : ι → N
x : (z : N) → M × ↥S
hx : ∀ (z : N), HMul.hMul (β := N) z ((f : (a : M) → N) (↑(x z).2 : M) : N) = (f : (a : M) → N) (x z).1
val : Fintype ι
i : ι
rw :
  HMul.hMul (β := N) (n i) ((f : (a : M) → N) (↑((x (n i)).2 * ∏ x_1 ∈ erase univ i, (x (n x_1)).2) : M) : N) =
    (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)
rw₁ :
  HMul.hMul (β := N) (n i) ((f : (a : M) → N) ((↑(x (n i)).2 : M) * (↑(∏ x_1 ∈ erase univ i, (x (n x_1)).2) : M)) : N) =
    (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)
⊢ HMul.hMul (β := N) (n i) ((f : (a : M) → N) (↑(∏ i : ι, (x (n i)).2) : M) : N) =
    (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)
have rw₂ : n i *
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑(x (n i)).2 : M) : N)
      ((f : (a : M) → N) (↑(∏ x_1 ∈ erase univ i, (x (n x_1)).2) : M) : N) =
  (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)
Tactic: rw [← univ.mul_prod_erase _ (mem_univ i), S.coe_mul, map_mul, ← mul_assoc, hx, map_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Lemmas (goal)
Goal:
M : Type u_1
N : Type u_2
F : Type u_3
ι : Type u_4
inst : Finite ι
inst_1 : CommMonoid M
inst_2 : CommMonoid N
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
f : F
S : Submonoid M
hf : IsLocalizationMap.{u_1, u_2} (N := N) S (⇑f : (a : M) → N)
n : ι → N
x : (z : N) → M × ↥S
hx : ∀ (z : N), HMul.hMul (β := N) z ((f : (a : M) → N) (↑(x z).2 : M) : N) = (f : (a : M) → N) (x z).1
val : Fintype ι
i : ι
rw :
  HMul.hMul (β := N) (n i) ((f : (a : M) → N) (↑((x (n i)).2 * ∏ x_1 ∈ erase univ i, (x (n x_1)).2) : M) : N) =
    (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)
rw₁ :
  HMul.hMul (β := N) (n i) ((f : (a : M) → N) ((↑(x (n i)).2 : M) * (↑(∏ x_1 ∈ erase univ i, (x (n x_1)).2) : M)) : N) =
    (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)
rw₂ :
  n i *
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑(x (n i)).2 : M) : N)
        ((f : (a : M) → N) (↑(∏ x_1 ∈ erase univ i, (x (n x_1)).2) : M) : N) =
    (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)
⊢ HMul.hMul (β := N) (n i) ((f : (a : M) → N) (↑(∏ i : ι, (x (n i)).2) : M) : N) =
    (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)
have rw₃ : HMul.hMul (β := N) (HMul.hMul (β := N) (n i) ((f : (a : M) → N) (↑(x (n i)).2 : M) : N))
    ((f : (a : M) → N) (↑(∏ x_1 ∈ erase univ i, (x (n x_1)).2) : M) : N) =
  (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)
Tactic: rw [← univ.mul_prod_erase _ (mem_univ i), S.coe_mul, map_mul, ← mul_assoc, hx, map_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Lemmas (goal)
Goal:
M : Type u_1
N : Type u_2
F : Type u_3
ι : Type u_4
inst : Finite ι
inst_1 : CommMonoid M
inst_2 : CommMonoid N
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
f : F
S : Submonoid M
hf : IsLocalizationMap.{u_1, u_2} (N := N) S (⇑f : (a : M) → N)
n : ι → N
x : (z : N) → M × ↥S
hx : ∀ (z : N), HMul.hMul (β := N) z ((f : (a : M) → N) (↑(x z).2 : M) : N) = (f : (a : M) → N) (x z).1
val : Fintype ι
i : ι
rw :
  HMul.hMul (β := N) (n i) ((f : (a : M) → N) (↑((x (n i)).2 * ∏ x_1 ∈ erase univ i, (x (n x_1)).2) : M) : N) =
    (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)
rw₁ :
  HMul.hMul (β := N) (n i) ((f : (a : M) → N) ((↑(x (n i)).2 : M) * (↑(∏ x_1 ∈ erase univ i, (x (n x_1)).2) : M)) : N) =
    (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)
rw₂ :
  n i *
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑(x (n i)).2 : M) : N)
        ((f : (a : M) → N) (↑(∏ x_1 ∈ erase univ i, (x (n x_1)).2) : M) : N) =
    (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)
rw₃ :
  HMul.hMul (β := N) (HMul.hMul (β := N) (n i) ((f : (a : M) → N) (↑(x (n i)).2 : M) : N))
      ((f : (a : M) → N) (↑(∏ x_1 ∈ erase univ i, (x (n x_1)).2) : M) : N) =
    (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)
⊢ HMul.hMul (β := N) (n i) ((f : (a : M) → N) (↑(∏ i : ι, (x (n i)).2) : M) : N) =
    (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)
have rw₄ : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (x (n i)).1 : N)
    ((f : (a : M) → N) (↑(∏ x_1 ∈ erase univ i, (x (n x_1)).2) : M) : N) =
  (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)
Tactic: rw [← univ.mul_prod_erase _ (mem_univ i), S.coe_mul, map_mul, ← mul_assoc, hx, map_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Lemmas (goal)
Goal:
M : Type u_1
N : Type u_2
F : Type u_3
ι : Type u_4
inst : Finite ι
inst_1 : CommMonoid M
inst_2 : CommMonoid N
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
f : F
S : Submonoid M
hf : IsLocalizationMap.{u_1, u_2} (N := N) S (⇑f : (a : M) → N)
n : ι → N
x : (z : N) → M × ↥S
hx : ∀ (z : N), HMul.hMul (β := N) z ((f : (a : M) → N) (↑(x z).2 : M) : N) = (f : (a : M) → N) (x z).1
val : Fintype ι
i : ι
rw :
  HMul.hMul (β := N) (n i) ((f : (a : M) → N) (↑((x (n i)).2 * ∏ x_1 ∈ erase univ i, (x (n x_1)).2) : M) : N) =
    (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)
rw₁ :
  HMul.hMul (β := N) (n i) ((f : (a : M) → N) ((↑(x (n i)).2 : M) * (↑(∏ x_1 ∈ erase univ i, (x (n x_1)).2) : M)) : N) =
    (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)
rw₂ :
  n i *
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑(x (n i)).2 : M) : N)
        ((f : (a : M) → N) (↑(∏ x_1 ∈ erase univ i, (x (n x_1)).2) : M) : N) =
    (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)
rw₃ :
  HMul.hMul (β := N) (HMul.hMul (β := N) (n i) ((f : (a : M) → N) (↑(x (n i)).2 : M) : N))
      ((f : (a : M) → N) (↑(∏ x_1 ∈ erase univ i, (x (n x_1)).2) : M) : N) =
    (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)
rw₄ :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (x (n i)).1 : N)
      ((f : (a : M) → N) (↑(∏ x_1 ∈ erase univ i, (x (n x_1)).2) : M) : N) =
    (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)
⊢ HMul.hMul (β := N) (n i) ((f : (a : M) → N) (↑(∏ i : ι, (x (n i)).2) : M) : N) =
    (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)
have rw₅ : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (x (n i)).1 : N)
    ((f : (a : M) → N) (↑(∏ x_1 ∈ erase univ i, (x (n x_1)).2) : M) : N) =
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (x (n i)).1 : N)
    ((f : (a : M) → N) (↑(∏ j ∈ erase univ i, (x (n j)).2) : M) : N)
Tactic: rw [← univ.mul_prod_erase _ (mem_univ i), S.coe_mul, map_mul, ← mul_assoc, hx, map_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Lemmas (goal)
Goal:
M : Type u_1
N : Type u_2
F : Type u_3
ι : Type u_4
inst : Finite ι
inst_1 : CommMonoid M
inst_2 : CommMonoid N
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
f : F
S : Submonoid M
hf : IsLocalizationMap.{u_1, u_2} (N := N) S (⇑f : (a : M) → N)
n : ι → N
x : (z : N) → M × ↥S
hx : ∀ (z : N), HMul.hMul (β := N) z ((f : (a : M) → N) (↑(x z).2 : M) : N) = (f : (a : M) → N) (x z).1
val : Fintype ι
⊢ ∃ (s : ↥S) (x : ι → M), ∀ (i : ι), HMul.hMul (β := N) (n i) ((f : (a : M) → N) (↑s : M) : N) = (f : (a : M) → N) (x i)
have refine : ∀ (i : ι),
  HMul.hMul (β := N) (n i) ((f : (a : M) → N) (↑(∏ i : ι, (x (n i)).2) : M) : N) =
    (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)
Tactic: classical
  refine ⟨∏ i : ι, (x (n i)).2, fun i ↦ (x (n i)).1 * ∏ j ∈ univ.erase i, (x (n j)).2, fun i ↦ ?_⟩
  rw [← univ.mul_prod_erase _ (mem_univ i), S.coe_mul, map_mul, ← mul_assoc, hx, map_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Lemmas (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
N : ι → Type u_3
inst : (i : ι) → CommMonoid (M i)
inst_1 : (i : ι) → CommMonoid (N i)
S : (i : ι) → Submonoid (M i)
f : (i : ι) → M i → N i
hf : ∀ (i : ι), (S i).IsLocalizationMap (f i)
z : (i : ι) → N i
⊢ ∃ (x : ((i : ι) → M i) × ↥(pi (M := M) Set.univ S)),
    z * Pi.map (α := M) (β := N) f (↑x.2 : (i : ι) → M i) = Pi.map (α := M) (β := N) f x.1
have choose : ∀ (x : (i : ι) → (z : N i) → M i × ↥(S i)) (hx : ∀ (i : ι) (z : N i), z * f i (↑(x i z).2 : M i) = f i (x i z).1),
  ∃ (x : ((i : ι) → M i) × ↥(pi (M := M) Set.univ S)),
    z * Pi.map (α := M) (β := N) f (↑x.2 : (i : ι) → M i) = Pi.map (α := M) (β := N) f x.1
Tactic: choose x hx using fun i ↦ (hf i).surj
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Lemmas (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
N : ι → Type u_3
inst : (i : ι) → CommMonoid (M i)
inst_1 : (i : ι) → CommMonoid (N i)
S : (i : ι) → Submonoid (M i)
f : (i : ι) → M i → N i
hf : ∀ (i : ι), (S i).IsLocalizationMap (f i)
x y : (i : ι) → M i
eq : Pi.map (α := M) (β := N) f x = Pi.map (α := M) (β := N) f y
⊢ ∃ (c : ↥(pi (M := M) Set.univ S)), (↑c : (i : ι) → M i) * x = (↑c : (i : ι) → M i) * y
have choose : ∀ (c : (i : ι) → ↥(S i)) (hc : ∀ (i : ι), (↑(c i) : M i) * x i = (↑(c i) : M i) * y i),
  ∃ (c : ↥(pi (M := M) Set.univ S)), (↑c : (i : ι) → M i) * x = (↑c : (i : ι) → M i) * y
Tactic: choose c hc using fun i ↦ (hf i).exists_of_eq congr($eq i)
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (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
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
x y : M
h : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
⊢ Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) x : P) ((g : (a : M) → P) y : P)
have obtain : ∀ (c : ↥S) (hc : (↑c : M) * x = (↑c : M) * y), Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) x : P) ((g : (a : M) → P) y : P)
Tactic: obtain ⟨c, hc⟩ := f.eq_iff_exists.1 h
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (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
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
x y : M
h : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
c : ↥S
hc : (↑c : M) * x = (↑c : M) * y
⊢ Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) x : P) ((g : (a : M) → P) y : P)
have rw : HMul.hMul (β := P)
    (HMul.hMul (α := P) (β := P) ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) c)⁻¹ : P) : P)
      (((g.restrict S : MonoidHom.{u_1, u_3} (↥S) P) : (a : ↥S) → P) c : P))
    ((g : (a : M) → P) x : P) =
  (g : (a : M) → P) y
Tactic: rw [← one_mul (g x), ← IsUnit.liftRight_inv_mul (g.restrict S) hg c]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (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
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
x y : M
h : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
c : ↥S
hc : (↑c : M) * x = (↑c : M) * y
⊢ HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) c)⁻¹ : P) : P)
        (((g.restrict S : MonoidHom.{u_1, u_3} (↥S) P) : (a : ↥S) → P) c : P))
      ((g : (a : M) → P) x : P) =
    (g : (a : M) → P) y
have change : HMul.hMul (β := P)
    (HMul.hMul (α := P) (β := P) ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) c)⁻¹ : P) : P)
      ((g : (a : M) → P) (↑c : M) : P))
    ((g : (a : M) → P) x : P) =
  (g : (a : M) → P) y
Tactic: change _ * g c * _ = _
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (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
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
x y : M
h : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
c : ↥S
hc : (↑c : M) * x = (↑c : M) * y
⊢ HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) c)⁻¹ : P) : P)
        ((g : (a : M) → P) (↑c : M) : P))
      ((g : (a : M) → P) x : P) =
    (g : (a : M) → P) y
have rw : (↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) c)⁻¹ : P) *
    HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (↑c : M) : P) ((g : (a : M) → P) x : P) =
  (g : (a : M) → P) y
Tactic: rw [mul_assoc, ← g.map_mul, hc, mul_comm, mul_inv_left hg, g.map_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (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
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
x y : M
h : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
c : ↥S
hc : (↑c : M) * x = (↑c : M) * y
rw :
  (↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) c)⁻¹ : P) *
      HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (↑c : M) : P) ((g : (a : M) → P) x : P) =
    (g : (a : M) → P) y
⊢ HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) c)⁻¹ : P) : P)
        ((g : (a : M) → P) (↑c : M) : P))
      ((g : (a : M) → P) x : P) =
    (g : (a : M) → P) y
have rw₁ : HMul.hMul (α := P) (β := P) ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) c)⁻¹ : P) : P)
    ((g : (a : M) → P) ((↑c : M) * x) : P) =
  (g : (a : M) → P) y
Tactic: rw [mul_assoc, ← g.map_mul, hc, mul_comm, mul_inv_left hg, g.map_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (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
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
x y : M
h : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
c : ↥S
hc : (↑c : M) * x = (↑c : M) * y
rw :
  (↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) c)⁻¹ : P) *
      HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (↑c : M) : P) ((g : (a : M) → P) x : P) =
    (g : (a : M) → P) y
rw₁ :
  HMul.hMul (α := P) (β := P) ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) c)⁻¹ : P) : P)
      ((g : (a : M) → P) ((↑c : M) * x) : P) =
    (g : (a : M) → P) y
⊢ HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) c)⁻¹ : P) : P)
        ((g : (a : M) → P) (↑c : M) : P))
      ((g : (a : M) → P) x : P) =
    (g : (a : M) → P) y
have rw₂ : HMul.hMul (α := P) (β := P) ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) c)⁻¹ : P) : P)
    ((g : (a : M) → P) ((↑c : M) * y) : P) =
  (g : (a : M) → P) y
Tactic: rw [mul_assoc, ← g.map_mul, hc, mul_comm, mul_inv_left hg, g.map_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (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
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
x y : M
h : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
c : ↥S
hc : (↑c : M) * x = (↑c : M) * y
rw :
  (↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) c)⁻¹ : P) *
      HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (↑c : M) : P) ((g : (a : M) → P) x : P) =
    (g : (a : M) → P) y
rw₁ :
  HMul.hMul (α := P) (β := P) ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) c)⁻¹ : P) : P)
      ((g : (a : M) → P) ((↑c : M) * x) : P) =
    (g : (a : M) → P) y
rw₂ :
  HMul.hMul (α := P) (β := P) ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) c)⁻¹ : P) : P)
      ((g : (a : M) → P) ((↑c : M) * y) : P) =
    (g : (a : M) → P) y
⊢ HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) c)⁻¹ : P) : P)
        ((g : (a : M) → P) (↑c : M) : P))
      ((g : (a : M) → P) x : P) =
    (g : (a : M) → P) y
have rw₃ : HMul.hMul (α := P) (β := P) ((g : (a : M) → P) ((↑c : M) * y) : P)
    ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) c)⁻¹ : P) : P) =
  (g : (a : M) → P) y
Tactic: rw [mul_assoc, ← g.map_mul, hc, mul_comm, mul_inv_left hg, g.map_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (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
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
x y : M
h : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
c : ↥S
hc : (↑c : M) * x = (↑c : M) * y
rw :
  (↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) c)⁻¹ : P) *
      HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (↑c : M) : P) ((g : (a : M) → P) x : P) =
    (g : (a : M) → P) y
rw₁ :
  HMul.hMul (α := P) (β := P) ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) c)⁻¹ : P) : P)
      ((g : (a : M) → P) ((↑c : M) * x) : P) =
    (g : (a : M) → P) y
rw₂ :
  HMul.hMul (α := P) (β := P) ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) c)⁻¹ : P) : P)
      ((g : (a : M) → P) ((↑c : M) * y) : P) =
    (g : (a : M) → P) y
rw₃ :
  HMul.hMul (α := P) (β := P) ((g : (a : M) → P) ((↑c : M) * y) : P)
      ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) c)⁻¹ : P) : P) =
    (g : (a : M) → P) y
⊢ HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) c)⁻¹ : P) : P)
        ((g : (a : M) → P) (↑c : M) : P))
      ((g : (a : M) → P) x : P) =
    (g : (a : M) → P) y
have rw₄ : (g : (a : M) → P) ((↑c : M) * y) =
  HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (↑c : M) : P) ((g : (a : M) → P) y : P)
Tactic: rw [mul_assoc, ← g.map_mul, hc, mul_comm, mul_inv_left hg, g.map_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (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
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
x y : M
h : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
c : ↥S
hc : (↑c : M) * x = (↑c : M) * y
rw :
  (↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) c)⁻¹ : P) *
      HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (↑c : M) : P) ((g : (a : M) → P) x : P) =
    (g : (a : M) → P) y
rw₁ :
  HMul.hMul (α := P) (β := P) ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) c)⁻¹ : P) : P)
      ((g : (a : M) → P) ((↑c : M) * x) : P) =
    (g : (a : M) → P) y
rw₂ :
  HMul.hMul (α := P) (β := P) ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) c)⁻¹ : P) : P)
      ((g : (a : M) → P) ((↑c : M) * y) : P) =
    (g : (a : M) → P) y
rw₃ :
  HMul.hMul (α := P) (β := P) ((g : (a : M) → P) ((↑c : M) * y) : P)
      ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) c)⁻¹ : P) : P) =
    (g : (a : M) → P) y
rw₄ :
  (g : (a : M) → P) ((↑c : M) * y) =
    HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (↑c : M) : P) ((g : (a : M) → P) y : P)
⊢ HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) c)⁻¹ : P) : P)
        ((g : (a : M) → P) (↑c : M) : P))
      ((g : (a : M) → P) x : P) =
    (g : (a : M) → P) y
have rw₅ : HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (↑c : M) : P) ((g : (a : M) → P) y : P) =
  HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (↑c : M) : P) ((g : (a : M) → P) y : P)
Tactic: rw [mul_assoc, ← g.map_mul, hc, mul_comm, mul_inv_left hg, g.map_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (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
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
⊢ HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec 1).1 : P)
      ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) (f.sec 1).2)⁻¹ : P) : P) =
    1
have rw : Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) (f.sec 1).1 : P) ((g : (a : M) → P) (↑(f.sec 1).2 : M) : P)
Tactic: rw [mul_inv_left, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (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
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (f.sec 1).1 : N) ((f : (a : M) → N) (↑(f.sec 1).2 : M) : N)
have rw : HMul.hMul (α := N) (β := N) (1 : N) ((f : (a : M) → N) (↑(f.sec 1).2 : M) : N) = (f : (a : M) → N) (↑(f.sec 1).2 : M)
Tactic: rw [← sec_spec, one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (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
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
rw :
  HMul.hMul (α := N) (β := N) (1 : N) ((f : (a : M) → N) (↑(f.sec 1).2 : M) : N) = (f : (a : M) → N) (↑(f.sec 1).2 : M)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (f.sec 1).1 : N) ((f : (a : M) → N) (↑(f.sec 1).2 : M) : N)
have rw₁ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (↑(f.sec 1).2 : M) : N) ((f : (a : M) → N) (↑(f.sec 1).2 : M) : N)
Tactic: rw [← sec_spec, one_mul]