awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : N
⊢ HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec (x * y)).1 : P)
      ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) (f.sec (x * y)).2)⁻¹ : P) : P) =
    HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec x).1 : P)
        ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) (f.sec x).2)⁻¹ : P) : P) *
      HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec y).1 : P)
        ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) (f.sec y).2)⁻¹ : P) : P)
have rw : HMul.hMul (β := P)
    (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec (x * y)).1 : P) ((g : (a : M) → P) (↑(f.sec y).2 : M) : P))
    ((g : (a : M) → P) (↑(f.sec x).2 : M) : P) =
  HMul.hMul (β := P)
    (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec y).1 : P) ((g : (a : M) → P) (↑(f.sec (x * y)).2 : M) : P))
    ((g : (a : M) → P) (f.sec x).1 : P)
Tactic: rw [mul_inv_left hg, ← mul_assoc, ← mul_assoc, mul_inv_right hg, mul_comm _ (g (f.sec y).1), ←
      mul_assoc, ← mul_assoc, mul_inv_right hg]
-- 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 : N
⊢ HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec (x * y)).1 : P) ((g : (a : M) → P) (↑(f.sec y).2 : M) : P))
      ((g : (a : M) → P) (↑(f.sec x).2 : M) : P) =
    HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec y).1 : P) ((g : (a : M) → P) (↑(f.sec (x * y)).2 : M) : P))
      ((g : (a : M) → P) (f.sec x).1 : P)
have rw : HMul.hMul (α := P) (β := P) ((g : (a : M) → P) ((f.sec (x * y)).1 * (↑(f.sec y).2 : M)) : P)
    ((g : (a : M) → P) (↑(f.sec x).2 : M) : P) =
  HMul.hMul (β := P)
    (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec y).1 : P) ((g : (a : M) → P) (↑(f.sec (x * y)).2 : M) : P))
    ((g : (a : M) → P) (f.sec x).1 : P)
Tactic: rw [← 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 : N
⊢ HMul.hMul (α := P) (β := P) ((g : (a : M) → P) ((f.sec (x * y)).1 * (↑(f.sec y).2 : M)) : P)
      ((g : (a : M) → P) (↑(f.sec x).2 : M) : P) =
    HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec y).1 : P) ((g : (a : M) → P) (↑(f.sec (x * y)).2 : M) : P))
      ((g : (a : M) → P) (f.sec x).1 : P)
have rw : (g : (a : M) → P) ((f.sec (x * y)).1 * (↑(f.sec y).2 : M) * (↑(f.sec x).2 : M)) =
  HMul.hMul (β := P)
    (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec y).1 : P) ((g : (a : M) → P) (↑(f.sec (x * y)).2 : M) : P))
    ((g : (a : M) → P) (f.sec x).1 : P)
Tactic: rw [← 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 : N
⊢ (g : (a : M) → P) ((f.sec (x * y)).1 * (↑(f.sec y).2 : M) * (↑(f.sec x).2 : M)) =
    HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec y).1 : P) ((g : (a : M) → P) (↑(f.sec (x * y)).2 : M) : P))
      ((g : (a : M) → P) (f.sec x).1 : P)
have rw : (g : (a : M) → P) ((f.sec (x * y)).1 * (↑(f.sec y).2 : M) * (↑(f.sec x).2 : M)) =
  HMul.hMul (α := P) (β := P) ((g : (a : M) → P) ((f.sec y).1 * (↑(f.sec (x * y)).2 : M)) : P)
    ((g : (a : M) → P) (f.sec x).1 : P)
Tactic: rw [← 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 : N
⊢ (g : (a : M) → P) ((f.sec (x * y)).1 * (↑(f.sec y).2 : M) * (↑(f.sec x).2 : M)) =
    HMul.hMul (α := P) (β := P) ((g : (a : M) → P) ((f.sec y).1 * (↑(f.sec (x * y)).2 : M)) : P)
      ((g : (a : M) → P) (f.sec x).1 : P)
have rw : Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) ((f.sec (x * y)).1 * (↑(f.sec y).2 : M) * (↑(f.sec x).2 : M)) : P)
  ((g : (a : M) → P) ((f.sec y).1 * (↑(f.sec (x * y)).2 : M) * (f.sec x).1) : P)
Tactic: rw [← 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 : N
⊢ HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec (x * y)).1 : P) ((g : (a : M) → P) (↑(f.sec y).2 : M) : P))
      ((g : (a : M) → P) (↑(f.sec x).2 : M) : P) =
    HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec y).1 : P) ((g : (a : M) → P) (↑(f.sec (x * y)).2 : M) : P))
      ((g : (a : M) → P) (f.sec x).1 : P)
have repeat : Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) ((f.sec (x * y)).1 * (↑(f.sec y).2 : M) * (↑(f.sec x).2 : M)) : P)
  ((g : (a : M) → P) ((f.sec y).1 * (↑(f.sec (x * y)).2 : M) * (f.sec x).1) : P)
Tactic: repeat rw [← 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 : N
⊢ Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) ((f.sec (x * y)).1 * (↑(f.sec y).2 : M) * (↑(f.sec x).2 : M)) : P)
    ((g : (a : M) → P) ((f.sec y).1 * (↑(f.sec (x * y)).2 : M) * (f.sec x).1) : P)
have refine : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) ((f.sec (x * y)).1 * (↑(f.sec y).2 : M) * (↑(f.sec x).2 : M)) : N)
  ((f : (a : M) → N) ((f.sec y).1 * (↑(f.sec (x * y)).2 : M) * (f.sec x).1) : N)
Tactic: refine f.eq_of_eq hg ?_
-- 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 : N
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) ((f.sec (x * y)).1 * (↑(f.sec y).2 : M) * (↑(f.sec x).2 : M)) : N)
    ((f : (a : M) → N) ((f.sec y).1 * (↑(f.sec (x * y)).2 : M) * (f.sec x).1) : N)
have simp_rw : HMul.hMul (β := N)
    (HMul.hMul (β := N) (HMul.hMul (α := N) ((f.toMonoidHom : (a : M) → N) (↑(f.sec (x * y)).2 : M) : N) (x * y))
      ((f.toMonoidHom : (a : M) → N) (↑(f.sec y).2 : M) : N))
    ((f.toMonoidHom : (a : M) → N) (↑(f.sec x).2 : M) : N) =
  HMul.hMul (β := N) (HMul.hMul (α := N) ((f.toMonoidHom : (a : M) → N) (↑(f.sec y).2 : M) : N) y)
      ((f.toMonoidHom : (a : M) → N) (↑(f.sec (x * y)).2 : M) : N) *
    HMul.hMul (α := N) ((f.toMonoidHom : (a : M) → N) (↑(f.sec x).2 : M) : N) x
Tactic: simp_rw [map_mul, sec_spec', ← toMonoidHom_apply]
-- 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 : M
y : ↥S
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) ((f.sec (f.mk' x y)).1 * (↑y : M)) : N)
    ((f : (a : M) → N) (x * (↑(f.sec (f.mk' x y)).2 : M)) : N)
have simp_rw : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (f.sec (f.mk' x y)).1 : N) ((f : (a : M) → N) (↑y : M) : N) =
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) (↑(f.sec (f.mk' x y)).2 : M) : N)
Tactic: simp_rw [map_mul, sec_spec', mul_assoc, f.mk'_spec, mul_comm]
-- 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 : M
y : ↥S
simp_rw :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (f.sec (f.mk' x y)).1 : N) ((f : (a : M) → N) (↑y : M) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) (↑(f.sec (f.mk' x y)).2 : M) : N)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) ((f.sec (f.mk' x y)).1 * (↑y : M)) : N)
    ((f : (a : M) → N) (x * (↑(f.sec (f.mk' x y)).2 : M)) : N)
have simp_rw₁ : HMul.hMul (β := N) (HMul.hMul (α := N) ((f : (a : M) → N) (↑(f.sec (f.mk' x y)).2 : M) : N) (f.mk' x y))
    ((f : (a : M) → N) (↑y : M) : N) =
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) (↑(f.sec (f.mk' x y)).2 : M) : N)
Tactic: simp_rw [map_mul, sec_spec', mul_assoc, f.mk'_spec, mul_comm]
-- 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 : M
y : ↥S
simp_rw :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (f.sec (f.mk' x y)).1 : N) ((f : (a : M) → N) (↑y : M) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) (↑(f.sec (f.mk' x y)).2 : M) : N)
simp_rw₁ :
  HMul.hMul (β := N) (HMul.hMul (α := N) ((f : (a : M) → N) (↑(f.sec (f.mk' x y)).2 : M) : N) (f.mk' x y))
      ((f : (a : M) → N) (↑y : M) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) (↑(f.sec (f.mk' x y)).2 : M) : N)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) ((f.sec (f.mk' x y)).1 * (↑y : M)) : N)
    ((f : (a : M) → N) (x * (↑(f.sec (f.mk' x y)).2 : M)) : N)
have simp_rw₂ : HMul.hMul (α := N) ((f : (a : M) → N) (↑(f.sec (f.mk' x y)).2 : M) : N)
    (HMul.hMul (β := N) (f.mk' x y) ((f : (a : M) → N) (↑y : M) : N)) =
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) (↑(f.sec (f.mk' x y)).2 : M) : N)
Tactic: simp_rw [map_mul, sec_spec', mul_assoc, f.mk'_spec, mul_comm]
-- 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 : M
y : ↥S
simp_rw :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (f.sec (f.mk' x y)).1 : N) ((f : (a : M) → N) (↑y : M) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) (↑(f.sec (f.mk' x y)).2 : M) : N)
simp_rw₁ :
  HMul.hMul (β := N) (HMul.hMul (α := N) ((f : (a : M) → N) (↑(f.sec (f.mk' x y)).2 : M) : N) (f.mk' x y))
      ((f : (a : M) → N) (↑y : M) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) (↑(f.sec (f.mk' x y)).2 : M) : N)
simp_rw₂ :
  HMul.hMul (α := N) ((f : (a : M) → N) (↑(f.sec (f.mk' x y)).2 : M) : N)
      (HMul.hMul (β := N) (f.mk' x y) ((f : (a : M) → N) (↑y : M) : N)) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) (↑(f.sec (f.mk' x y)).2 : M) : N)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) ((f.sec (f.mk' x y)).1 * (↑y : M)) : N)
    ((f : (a : M) → N) (x * (↑(f.sec (f.mk' x y)).2 : M)) : N)
have simp_rw₃ : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑(f.sec (f.mk' x y)).2 : M) : N) ((f : (a : M) → N) x : N) =
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) (↑(f.sec (f.mk' x y)).2 : M) : N)
Tactic: simp_rw [map_mul, sec_spec', mul_assoc, f.mk'_spec, mul_comm]
-- 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)
z : N
w v : P
⊢ HMul.hMul (α := P) ((f.lift hg : (a : N) → P) z : P) w = v ↔
    HMul.hMul (α := P) ((g : (a : M) → P) (f.sec z).1 : P) w =
      HMul.hMul (α := P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) v
have rw : HMul.hMul (β := P) w ((f.lift hg : (a : N) → P) z : P) = v ↔
  HMul.hMul (α := P) ((g : (a : M) → P) (f.sec z).1 : P) w =
    HMul.hMul (α := P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) v
Tactic: rw [mul_comm, lift_apply, ← mul_assoc, mul_inv_left hg, mul_comm]
-- 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)
z : N
w v : P
rw :
  HMul.hMul (β := P) w ((f.lift hg : (a : N) → P) z : P) = v ↔
    HMul.hMul (α := P) ((g : (a : M) → P) (f.sec z).1 : P) w =
      HMul.hMul (α := P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) v
⊢ HMul.hMul (α := P) ((f.lift hg : (a : N) → P) z : P) w = v ↔
    HMul.hMul (α := P) ((g : (a : M) → P) (f.sec z).1 : P) w =
      HMul.hMul (α := P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) v
have rw₁ : w *
      HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec z).1 : P)
        ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) (f.sec z).2)⁻¹ : P) : P) =
    v ↔
  HMul.hMul (α := P) ((g : (a : M) → P) (f.sec z).1 : P) w =
    HMul.hMul (α := P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) v
Tactic: rw [mul_comm, lift_apply, ← mul_assoc, mul_inv_left hg, mul_comm]
-- 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)
z : N
w v : P
rw :
  HMul.hMul (β := P) w ((f.lift hg : (a : N) → P) z : P) = v ↔
    HMul.hMul (α := P) ((g : (a : M) → P) (f.sec z).1 : P) w =
      HMul.hMul (α := P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) v
rw₁ :
  w *
        HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec z).1 : P)
          ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) (f.sec z).2)⁻¹ : P) : P) =
      v ↔
    HMul.hMul (α := P) ((g : (a : M) → P) (f.sec z).1 : P) w =
      HMul.hMul (α := P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) v
⊢ HMul.hMul (α := P) ((f.lift hg : (a : N) → P) z : P) w = v ↔
    HMul.hMul (α := P) ((g : (a : M) → P) (f.sec z).1 : P) w =
      HMul.hMul (α := P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) v
have rw₂ : HMul.hMul (β := P) w ((g : (a : M) → P) (f.sec z).1 : P) *
      (↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) (f.sec z).2)⁻¹ : P) =
    v ↔
  HMul.hMul (α := P) ((g : (a : M) → P) (f.sec z).1 : P) w =
    HMul.hMul (α := P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) v
Tactic: rw [mul_comm, lift_apply, ← mul_assoc, mul_inv_left hg, mul_comm]
-- 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)
z : N
w v : P
rw :
  HMul.hMul (β := P) w ((f.lift hg : (a : N) → P) z : P) = v ↔
    HMul.hMul (α := P) ((g : (a : M) → P) (f.sec z).1 : P) w =
      HMul.hMul (α := P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) v
rw₁ :
  w *
        HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec z).1 : P)
          ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) (f.sec z).2)⁻¹ : P) : P) =
      v ↔
    HMul.hMul (α := P) ((g : (a : M) → P) (f.sec z).1 : P) w =
      HMul.hMul (α := P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) v
rw₂ :
  HMul.hMul (β := P) w ((g : (a : M) → P) (f.sec z).1 : P) *
        (↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) (f.sec z).2)⁻¹ : P) =
      v ↔
    HMul.hMul (α := P) ((g : (a : M) → P) (f.sec z).1 : P) w =
      HMul.hMul (α := P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) v
⊢ HMul.hMul (α := P) ((f.lift hg : (a : N) → P) z : P) w = v ↔
    HMul.hMul (α := P) ((g : (a : M) → P) (f.sec z).1 : P) w =
      HMul.hMul (α := P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) v
have rw₃ : HMul.hMul (β := P) w ((g : (a : M) → P) (f.sec z).1 : P) =
    HMul.hMul (α := P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) v ↔
  HMul.hMul (α := P) ((g : (a : M) → P) (f.sec z).1 : P) w =
    HMul.hMul (α := P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) v
Tactic: rw [mul_comm, lift_apply, ← mul_assoc, mul_inv_left hg, mul_comm]
-- 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)
z : N
w v : P
rw :
  HMul.hMul (β := P) w ((f.lift hg : (a : N) → P) z : P) = v ↔
    HMul.hMul (α := P) ((g : (a : M) → P) (f.sec z).1 : P) w =
      HMul.hMul (α := P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) v
rw₁ :
  w *
        HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec z).1 : P)
          ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) (f.sec z).2)⁻¹ : P) : P) =
      v ↔
    HMul.hMul (α := P) ((g : (a : M) → P) (f.sec z).1 : P) w =
      HMul.hMul (α := P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) v
rw₂ :
  HMul.hMul (β := P) w ((g : (a : M) → P) (f.sec z).1 : P) *
        (↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) (f.sec z).2)⁻¹ : P) =
      v ↔
    HMul.hMul (α := P) ((g : (a : M) → P) (f.sec z).1 : P) w =
      HMul.hMul (α := P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) v
rw₃ :
  HMul.hMul (β := P) w ((g : (a : M) → P) (f.sec z).1 : P) =
      HMul.hMul (α := P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) v ↔
    HMul.hMul (α := P) ((g : (a : M) → P) (f.sec z).1 : P) w =
      HMul.hMul (α := P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) v
⊢ HMul.hMul (α := P) ((f.lift hg : (a : N) → P) z : P) w = v ↔
    HMul.hMul (α := P) ((g : (a : M) → P) (f.sec z).1 : P) w =
      HMul.hMul (α := P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) v
have rw₄ : HMul.hMul (α := P) ((g : (a : M) → P) (f.sec z).1 : P) w =
    HMul.hMul (α := P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) v ↔
  HMul.hMul (α := P) ((g : (a : M) → P) (f.sec z).1 : P) w =
    HMul.hMul (α := P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) v
Tactic: rw [mul_comm, lift_apply, ← mul_assoc, mul_inv_left hg, mul_comm]
-- 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 : M
v : P
y : ↥S
⊢ (f.lift hg : (a : N) → P) (f.mk' x y) = v ↔
    (g : (a : M) → P) x = HMul.hMul (α := P) ((g : (a : M) → P) (↑y : M) : P) v
have rw : HMul.hMul (α := P) (β := P) ((g : (a : M) → P) x : P)
      ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) y)⁻¹ : P) : P) =
    v ↔
  (g : (a : M) → P) x = HMul.hMul (α := P) ((g : (a : M) → P) (↑y : M) : P) v
Tactic: rw [f.lift_mk' hg]
-- 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)
z : N
⊢ HMul.hMul (α := P) (β := P) ((f.lift hg : (a : N) → P) z : P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) =
    (g : (a : M) → P) (f.sec z).1
have rw : HMul.hMul (β := P)
    (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec z).1 : P)
      ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) (f.sec z).2)⁻¹ : P) : P))
    ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) =
  (g : (a : M) → P) (f.sec z).1
Tactic: rw [lift_apply, mul_assoc, ← g.restrict_apply, IsUnit.liftRight_inv_mul, 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)
z : N
rw :
  HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec z).1 : P)
        ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) (f.sec z).2)⁻¹ : P) : P))
      ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) =
    (g : (a : M) → P) (f.sec z).1
⊢ HMul.hMul (α := P) (β := P) ((f.lift hg : (a : N) → P) z : P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) =
    (g : (a : M) → P) (f.sec z).1
have rw₁ : HMul.hMul (α := P) ((g : (a : M) → P) (f.sec z).1 : P)
    (HMul.hMul (α := P) (β := P) ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) (f.sec z).2)⁻¹ : P) : P)
      ((g : (a : M) → P) (↑(f.sec z).2 : M) : P)) =
  (g : (a : M) → P) (f.sec z).1
Tactic: rw [lift_apply, mul_assoc, ← g.restrict_apply, IsUnit.liftRight_inv_mul, 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)
z : N
rw :
  HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec z).1 : P)
        ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) (f.sec z).2)⁻¹ : P) : P))
      ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) =
    (g : (a : M) → P) (f.sec z).1
rw₁ :
  HMul.hMul (α := P) ((g : (a : M) → P) (f.sec z).1 : P)
      (HMul.hMul (α := P) (β := P) ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) (f.sec z).2)⁻¹ : P) : P)
        ((g : (a : M) → P) (↑(f.sec z).2 : M) : P)) =
    (g : (a : M) → P) (f.sec z).1
⊢ HMul.hMul (α := P) (β := P) ((f.lift hg : (a : N) → P) z : P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) =
    (g : (a : M) → P) (f.sec z).1
have rw₂ : HMul.hMul (α := P) ((g : (a : M) → P) (f.sec z).1 : P)
    (HMul.hMul (α := P) (β := P) ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) (f.sec z).2)⁻¹ : P) : P)
      ((g.restrict S : (a : ↥S) → P) (f.sec z).2 : P)) =
  (g : (a : M) → P) (f.sec z).1
Tactic: rw [lift_apply, mul_assoc, ← g.restrict_apply, IsUnit.liftRight_inv_mul, mul_one]