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 : 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)
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)
⊢ 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) (β := N) ((f : (a : M) → N) x₁ : N) ((f : (a : M) → N) (↑y₂ : M) : N) *
      (↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y₁)⁻¹ : 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)
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)
rw₃ :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₁ : N) ((f : (a : M) → N) (↑y₂ : M) : N) *
        (↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y₁)⁻¹ : 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) (β := N) ((f : (a : M) → N) x₁ : N) ((f : (a : M) → N) (↑y₂ : M) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑y₁ : M) : N) ((f : (a : M) → N) x₂ : N) ↔
  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)
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)
rw₃ :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₁ : N) ((f : (a : M) → N) (↑y₂ : M) : N) *
        (↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y₁)⁻¹ : 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) (β := N) ((f : (a : M) → N) x₁ : N) ((f : (a : M) → N) (↑y₂ : M) : N) =
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑y₁ : M) : N) ((f : (a : M) → N) x₂ : N) ↔
    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) (β := N) ((f : (a : M) → N) x₁ : N) ((f : (a : M) → N) (↑y₂ : M) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑y₁ : M) : N) ((f : (a : M) → N) x₂ : N) ↔
  Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (x₁ * (↑y₂ : M)) : N) ((f : (a : M) → N) ((↑y₁ : M) * x₂) : 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)
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)
rw₃ :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₁ : N) ((f : (a : M) → N) (↑y₂ : M) : N) *
        (↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y₁)⁻¹ : 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) (β := N) ((f : (a : M) → N) x₁ : N) ((f : (a : M) → N) (↑y₂ : M) : N) =
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑y₁ : M) : N) ((f : (a : M) → N) x₂ : N) ↔
    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) (β := N) ((f : (a : M) → N) x₁ : N) ((f : (a : M) → N) (↑y₂ : M) : N) =
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑y₁ : M) : N) ((f : (a : M) → N) x₂ : N) ↔
    Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (x₁ * (↑y₂ : M)) : N) ((f : (a : M) → N) ((↑y₁ : M) * x₂) : 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) (β := N) ((f : (a : M) → N) x₁ : N) ((f : (a : M) → N) (↑y₂ : M) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑y₁ : M) : N) ((f : (a : M) → N) x₂ : N) ↔
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₁ : N) ((f : (a : M) → N) (↑y₂ : M) : N) =
    (f : (a : M) → N) ((↑y₁ : M) * x₂)
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
hf : ∀ (y : ↥S), IsUnit.{u_2} (M := N) ((f : (a : M) → N) (↑y : M) : N)
y z : ↥S
h :
  Eq.{u_2 + 1} (α := Nˣ) (((IsUnit.liftRight (f.restrict S) hf : (a : ↥S) → Nˣ) y)⁻¹ : Nˣ)
    (((IsUnit.liftRight (f.restrict S) hf : (a : ↥S) → Nˣ) z)⁻¹ : Nˣ)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (↑y : M) : N) ((f : (a : M) → N) (↑z : M) : N)
have rw : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑z : M) : N)
    ((↑((IsUnit.liftRight (f.restrict S) hf : (a : ↥S) → Nˣ) z)⁻¹ : N) : N) =
  1
Tactic: rw [← mul_one (f y), eq_comm, ← mul_inv_left hf y (f z) 1, 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 : M →* N
h : ∀ (y : ↥S), IsUnit.{u_2} (M := N) ((f : (a : M) → N) (↑y : M) : N)
y : ↥S
z : N
H : HMul.hMul (α := N) ((f : (a : M) → N) (↑y : M) : N) z = 1
⊢ (↑((IsUnit.liftRight (f.restrict S) h : (a : ↥S) → Nˣ) y)⁻¹ : N) = z
have rw : (↑1 : N) = HMul.hMul (α := N) ((f : (a : M) → N) (↑y : M) : N) z
Tactic: rw [← one_mul _⁻¹, Units.val_mul, mul_inv_left]
-- 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
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
x y : M
c : ↥S
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)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
have let : ∀ (u : Nˣ) (hu : (↑u : N) = (f : (a : M) → N) (↑c : M)),
  Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
Tactic: let ⟨u, hu⟩ := f.map_units c
-- 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
c : ↥S
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)
u : Nˣ
hu : (↑u : N) = (f : (a : M) → N) (↑c : M)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
have h₁ : HMul.hMul (β := N) (↑u : N) ((f : (a : M) → N) x : N) = HMul.hMul (β := N) (↑u : N) ((f : (a : M) → N) y : N)
Tactic: rw [← hu] at h
Cleared hypotheses: h, hu
-- 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
x y : M
c : ↥S
h : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (x * (↑c : M)) : N) ((f : (a : M) → N) (y * (↑c : M)) : N)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) ((↑c : M) * x) : N) ((f : (a : M) → N) ((↑c : M) * y) : N)
have rw : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (x * (↑c : M)) : N) ((f : (a : M) → N) ((↑c : M) * y) : N)
Tactic: rw [mul_comm _ x, mul_comm _ y, h]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
f : S.LocalizationMap N
x y : M
c : ↥S
h : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (x * (↑c : M)) : N) ((f : (a : M) → N) (y * (↑c : M)) : N)
rw : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (x * (↑c : M)) : N) ((f : (a : M) → N) ((↑c : M) * y) : N)
rw₁ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (x * (↑c : M)) : N) ((f : (a : M) → N) (y * (↑c : M)) : N)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) ((↑c : M) * x) : N) ((f : (a : M) → N) ((↑c : M) * y) : N)
have rw₂ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (y * (↑c : M)) : N) ((f : (a : M) → N) (y * (↑c : M)) : N)
Tactic: rw [mul_comm _ x, mul_comm _ y, h]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
f : S.LocalizationMap N
x₁ x₂ : M
y₁ y₂ : ↥S
⊢ f.mk' (x₁ * x₂) (y₁ * y₂) = f.mk' x₁ y₁ * f.mk' x₂ y₂
have refine : (f : (a : M) → N) (x₁ * x₂) =
  HMul.hMul (α := N) ((f.toMonoidHom : (a : M) → N) (↑(y₁ * y₂) : M) : N) (f.mk' x₁ y₁ * f.mk' x₂ y₂)
Tactic: refine (mul_inv_left f.map_units _ _ _).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
x₁ x₂ : M
y₁ y₂ : ↥S
⊢ (f : (a : M) → N) (x₁ * x₂) =
    HMul.hMul (α := N) ((f.toMonoidHom : (a : M) → N) (↑(y₁ * y₂) : M) : N) (f.mk' x₁ y₁ * f.mk' x₂ y₂)
have simp : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₁ : N) ((f : (a : M) → N) x₂ : N) =
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑y₁ : M) : N) ((f : (a : M) → N) (↑y₂ : M) : N) *
    (HMul.hMul (α := N) ((f : (a : M) → N) x₁ : N) (↑(IsUnit.unit (a := (f : (a : M) → N) (↑y₁ : M)) sorry)⁻¹ : N) *
      HMul.hMul (α := N) ((f : (a : M) → N) x₂ : N) (↑(IsUnit.unit (a := (f : (a : M) → N) (↑y₂ : M)) sorry)⁻¹ : N))
Tactic: simp only [map_mul, coe_mul, toMonoidHom_apply, mk', IsUnit.liftRight, Units.liftRight,
    MonoidHom.restrict_apply, MonoidHom.coe_mk, OneHom.coe_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
f : S.LocalizationMap N
x₁ x₂ : M
y₁ y₂ : ↥S
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₁ : N) ((f : (a : M) → N) x₂ : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑y₁ : M) : N) ((f : (a : M) → N) (↑y₂ : M) : N) *
      (HMul.hMul (α := N) ((f : (a : M) → N) x₁ : N) (↑(IsUnit.unit (a := (f : (a : M) → N) (↑y₁ : M)) ⋯)⁻¹ : N) *
        HMul.hMul (α := N) ((f : (a : M) → N) x₂ : N) (↑(IsUnit.unit (a := (f : (a : M) → N) (↑y₂ : M)) ⋯)⁻¹ : N))
have rw : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₁ : N) ((f : (a : M) → N) x₂ : N) =
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x₁ : N) ((f : (a : M) → N) x₂ : N) *
    (HMul.hMul (α := N) ((f : (a : M) → N) (↑y₁ : M) : N) (↑(IsUnit.unit (a := (f : (a : M) → N) (↑y₁ : M)) sorry)⁻¹ : N) *
      HMul.hMul (α := N) ((f : (a : M) → N) (↑y₂ : M) : N) (↑(IsUnit.unit (a := (f : (a : M) → N) (↑y₂ : M)) sorry)⁻¹ : N))
Tactic: rw [mul_mul_mul_comm (f x₁), mul_left_comm, mul_mul_mul_comm (f y₁)]
-- 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
x : M
⊢ f.mk' x 1 = (f : (a : M) → N) x
have rw : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((↑1⁻¹ : N) : N) = (f : (a : M) → N) x
Tactic: rw [mk', map_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 : S.LocalizationMap N
z : N
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (f.sec z).1 : N)
      ((↑((IsUnit.liftRight (f.toMonoidHom.restrict S) ⋯ : (a : ↥S) → Nˣ) (f.sec z).2)⁻¹ : N) : N) =
    z
have rw : HMul.hMul (α := N) ((f : (a : M) → N) (↑(f.sec z).2 : M) : N) z =
  HMul.hMul (α := N) ((f.toMonoidHom : (a : M) → N) (↑(f.sec z).2 : M) : N) z
Tactic: rw [← sec_spec, mul_inv_left, 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 : S.LocalizationMap N
x : M
y : ↥S
⊢ HMul.hMul (β := N)
      (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N)
        ((↑((IsUnit.liftRight (f.toMonoidHom.restrict S) ⋯ : (a : ↥S) → Nˣ) y)⁻¹ : N) : N))
      ((f : (a : M) → N) (↑y : M) : N) =
    (f : (a : M) → N) x
have rw : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑y : M) : N) ((f : (a : M) → N) x : N) =
  HMul.hMul (α := N) (β := N) ((f.toMonoidHom : (a : M) → N) (↑y : M) : N) ((f : (a : M) → N) x : N)
Tactic: rw [mul_assoc, mul_comm _ (f y), ← mul_assoc, mul_inv_left, 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 : S.LocalizationMap N
x : M
y : ↥S
⊢ HMul.hMul (α := N) ((f : (a : M) → N) (↑y : M) : N) (f.mk' x y) = (f : (a : M) → N) x
have rw : HMul.hMul (β := N) (f.mk' x y) ((f : (a : M) → N) (↑y : M) : N) = (f : (a : M) → N) x
Tactic: rw [mul_comm, mk'_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
x : M
y : ↥S
rw : HMul.hMul (β := N) (f.mk' x y) ((f : (a : M) → N) (↑y : M) : N) = (f : (a : M) → N) x
⊢ HMul.hMul (α := N) ((f : (a : M) → N) (↑y : M) : N) (f.mk' x y) = (f : (a : M) → N) x
have rw₁ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) x : N)
Tactic: rw [mul_comm, mk'_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
x : M
y : ↥S
z : N
H : z = f.mk' x y
⊢ HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N) = (f : (a : M) → N) x
have rw : HMul.hMul (β := N) (f.mk' x y) ((f : (a : M) → N) (↑y : M) : N) = (f : (a : M) → N) x
Tactic: rw [H, mk'_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
x : M
y : ↥S
z : N
H : z = f.mk' x y
rw : HMul.hMul (β := N) (f.mk' x y) ((f : (a : M) → N) (↑y : M) : N) = (f : (a : M) → N) x
⊢ HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N) = (f : (a : M) → N) x
have rw₁ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) x : N)
Tactic: rw [H, mk'_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
x : M
y : ↥S
z : N
H : HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N) = (f : (a : M) → N) x
⊢ z = f.mk' x y
have rwa : z =
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N)
    ((↑((IsUnit.liftRight (f.toMonoidHom.restrict S) sorry : (a : ↥S) → Nˣ) y)⁻¹ : N) : N)
Tactic: rwa [mk', mul_inv_right]
-- 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
x : M
y : ↥S
z : N
H : HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N) = (f : (a : M) → N) x
rwa :
  z =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N)
      ((↑((IsUnit.liftRight (f.toMonoidHom.restrict S) ⋯ : (a : ↥S) → Nˣ) y)⁻¹ : N) : N)
⊢ z = f.mk' x y
have rwa₁ : HMul.hMul (β := N) z ((f.toMonoidHom : (a : M) → N) (↑y : M) : N) = (f : (a : M) → N) x
Tactic: rwa [mk', mul_inv_right]
-- 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
x : M
y : ↥S
z : N
⊢ f.mk' x y = z ↔ (f : (a : M) → N) x = HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N)
have rw : z = f.mk' x y ↔ (f : (a : M) → N) x = HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N)
Tactic: rw [eq_comm, eq_mk'_iff_mul_eq, 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 : S.LocalizationMap N
x : M
y : ↥S
z : N
rw : z = f.mk' x y ↔ (f : (a : M) → N) x = HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N)
⊢ f.mk' x y = z ↔ (f : (a : M) → N) x = HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N)
have rw₁ : HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N) = (f : (a : M) → N) x ↔
  (f : (a : M) → N) x = HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N)
Tactic: rw [eq_comm, eq_mk'_iff_mul_eq, 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 : S.LocalizationMap N
x : M
y : ↥S
z : N
rw : z = f.mk' x y ↔ (f : (a : M) → N) x = HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N)
rw₁ :
  HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N) = (f : (a : M) → N) x ↔
    (f : (a : M) → N) x = HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N)
⊢ f.mk' x y = z ↔ (f : (a : M) → N) x = HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N)
have rw₂ : (f : (a : M) → N) x = HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N) ↔
  (f : (a : M) → N) x = HMul.hMul (β := N) z ((f : (a : M) → N) (↑y : M) : N)
Tactic: rw [eq_comm, eq_mk'_iff_mul_eq, eq_comm]