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)
mp :
  Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := P) (⇑(f.lift hg) : (a : N) → P) →
    ∀ (v : P), ∃ (x : M × ↥S), HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1
⊢ Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := P) (⇑(f.lift hg) : (a : N) → P) ↔
    ∀ (v : P), ∃ (x : M × ↥S), HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1
have mpr : (∀ (v : P), ∃ (x : M × ↥S), HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1) →
  Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := P) (⇑(f.lift hg) : (a : N) → P)
Tactic: constructor
-- 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)
H : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := P) (⇑(f.lift hg) : (a : N) → P)
v : P
⊢ ∃ (x : M × ↥S), HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1
have mp : ∀ (z : N) (hz : (f.lift hg : (a : N) → P) z = v),
  ∃ (x : M × ↥S), HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1
Tactic: obtain ⟨z, hz⟩ := H v
-- 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)
H : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := P) (⇑(f.lift hg) : (a : N) → P)
v : P
z : N
hz : (f.lift hg : (a : N) → P) z = v
⊢ ∃ (x : M × ↥S), HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1
have mp : ∀ (x : M × ↥S) (hx : HMul.hMul (β := N) z ((f : (a : M) → N) (↑x.2 : M) : N) = (f : (a : M) → N) x.1),
  ∃ (x : M × ↥S), HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1
Tactic: obtain ⟨x, hx⟩ := f.surj z
-- 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)
H : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := P) (⇑(f.lift hg) : (a : N) → P)
v : P
z : N
hz : (f.lift hg : (a : N) → P) z = v
x : M × ↥S
hx : HMul.hMul (β := N) z ((f : (a : M) → N) (↑x.2 : M) : N) = (f : (a : M) → N) x.1
⊢ ∃ (x : M × ↥S), HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1
have h : HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1
Tactic: use x
-- 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)
H : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := P) (⇑(f.lift hg) : (a : N) → P)
v : P
z : N
hz : (f.lift hg : (a : N) → P) z = v
x : M × ↥S
hx : HMul.hMul (β := N) z ((f : (a : M) → N) (↑x.2 : M) : N) = (f : (a : M) → N) x.1
⊢ HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1
have h : HMul.hMul (α := P) (β := P) ((f.lift hg : (a : N) → P) z : P) ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1
Tactic: rw [← hz, f.eq_mk'_iff_mul_eq.2 hx, lift_mk', mul_assoc, mul_comm _ (g ↑x.2),
      ← MonoidHom.restrict_apply, IsUnit.mul_liftRight_inv (g.restrict S) hg, 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)
H : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := P) (⇑(f.lift hg) : (a : N) → P)
v : P
z : N
hz : (f.lift hg : (a : N) → P) z = v
x : M × ↥S
hx : HMul.hMul (β := N) z ((f : (a : M) → N) (↑x.2 : M) : N) = (f : (a : M) → N) x.1
h :
  HMul.hMul (α := P) (β := P) ((f.lift hg : (a : N) → P) z : P) ((g : (a : M) → P) (↑x.2 : M) : P) =
    (g : (a : M) → P) x.1
⊢ HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1
have h₁ : HMul.hMul (α := P) (β := P) ((f.lift hg : (a : N) → P) (f.mk' x.1 x.2) : P) ((g : (a : M) → P) (↑x.2 : M) : P) =
  (g : (a : M) → P) x.1
Tactic: rw [← hz, f.eq_mk'_iff_mul_eq.2 hx, lift_mk', mul_assoc, mul_comm _ (g ↑x.2),
      ← MonoidHom.restrict_apply, IsUnit.mul_liftRight_inv (g.restrict S) hg, 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)
H : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := P) (⇑(f.lift hg) : (a : N) → P)
v : P
z : N
hz : (f.lift hg : (a : N) → P) z = v
x : M × ↥S
hx : HMul.hMul (β := N) z ((f : (a : M) → N) (↑x.2 : M) : N) = (f : (a : M) → N) x.1
h :
  HMul.hMul (α := P) (β := P) ((f.lift hg : (a : N) → P) z : P) ((g : (a : M) → P) (↑x.2 : M) : P) =
    (g : (a : M) → P) x.1
h₁ :
  HMul.hMul (α := P) (β := P) ((f.lift hg : (a : N) → P) (f.mk' x.1 x.2) : P) ((g : (a : M) → P) (↑x.2 : M) : P) =
    (g : (a : M) → P) x.1
⊢ HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1
have h₂ : HMul.hMul (β := P)
    (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) x.1 : P)
      ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) x.2)⁻¹ : P) : P))
    ((g : (a : M) → P) (↑x.2 : M) : P) =
  (g : (a : M) → P) x.1
Tactic: rw [← hz, f.eq_mk'_iff_mul_eq.2 hx, lift_mk', mul_assoc, mul_comm _ (g ↑x.2),
      ← MonoidHom.restrict_apply, IsUnit.mul_liftRight_inv (g.restrict S) hg, 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)
H : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := P) (⇑(f.lift hg) : (a : N) → P)
v : P
z : N
hz : (f.lift hg : (a : N) → P) z = v
x : M × ↥S
hx : HMul.hMul (β := N) z ((f : (a : M) → N) (↑x.2 : M) : N) = (f : (a : M) → N) x.1
h :
  HMul.hMul (α := P) (β := P) ((f.lift hg : (a : N) → P) z : P) ((g : (a : M) → P) (↑x.2 : M) : P) =
    (g : (a : M) → P) x.1
h₁ :
  HMul.hMul (α := P) (β := P) ((f.lift hg : (a : N) → P) (f.mk' x.1 x.2) : P) ((g : (a : M) → P) (↑x.2 : M) : P) =
    (g : (a : M) → P) x.1
h₂ :
  HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) x.1 : P)
        ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) x.2)⁻¹ : P) : P))
      ((g : (a : M) → P) (↑x.2 : M) : P) =
    (g : (a : M) → P) x.1
⊢ HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1
have h₃ : HMul.hMul (α := P) ((g : (a : M) → P) x.1 : P)
    (HMul.hMul (α := P) (β := P) ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) x.2)⁻¹ : P) : P)
      ((g : (a : M) → P) (↑x.2 : M) : P)) =
  (g : (a : M) → P) x.1
Tactic: rw [← hz, f.eq_mk'_iff_mul_eq.2 hx, lift_mk', mul_assoc, mul_comm _ (g ↑x.2),
      ← MonoidHom.restrict_apply, IsUnit.mul_liftRight_inv (g.restrict S) hg, 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)
H : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := P) (⇑(f.lift hg) : (a : N) → P)
v : P
z : N
hz : (f.lift hg : (a : N) → P) z = v
x : M × ↥S
hx : HMul.hMul (β := N) z ((f : (a : M) → N) (↑x.2 : M) : N) = (f : (a : M) → N) x.1
h :
  HMul.hMul (α := P) (β := P) ((f.lift hg : (a : N) → P) z : P) ((g : (a : M) → P) (↑x.2 : M) : P) =
    (g : (a : M) → P) x.1
h₁ :
  HMul.hMul (α := P) (β := P) ((f.lift hg : (a : N) → P) (f.mk' x.1 x.2) : P) ((g : (a : M) → P) (↑x.2 : M) : P) =
    (g : (a : M) → P) x.1
h₂ :
  HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) x.1 : P)
        ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) x.2)⁻¹ : P) : P))
      ((g : (a : M) → P) (↑x.2 : M) : P) =
    (g : (a : M) → P) x.1
h₃ :
  HMul.hMul (α := P) ((g : (a : M) → P) x.1 : P)
      (HMul.hMul (α := P) (β := P) ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) x.2)⁻¹ : P) : P)
        ((g : (a : M) → P) (↑x.2 : M) : P)) =
    (g : (a : M) → P) x.1
⊢ HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1
have h₄ : HMul.hMul (α := P) ((g : (a : M) → P) x.1 : P)
    (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (↑x.2 : M) : P)
      ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) x.2)⁻¹ : P) : P)) =
  (g : (a : M) → P) x.1
Tactic: rw [← hz, f.eq_mk'_iff_mul_eq.2 hx, lift_mk', mul_assoc, mul_comm _ (g ↑x.2),
      ← MonoidHom.restrict_apply, IsUnit.mul_liftRight_inv (g.restrict S) hg, 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)
H : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := P) (⇑(f.lift hg) : (a : N) → P)
v : P
z : N
hz : (f.lift hg : (a : N) → P) z = v
x : M × ↥S
hx : HMul.hMul (β := N) z ((f : (a : M) → N) (↑x.2 : M) : N) = (f : (a : M) → N) x.1
h :
  HMul.hMul (α := P) (β := P) ((f.lift hg : (a : N) → P) z : P) ((g : (a : M) → P) (↑x.2 : M) : P) =
    (g : (a : M) → P) x.1
h₁ :
  HMul.hMul (α := P) (β := P) ((f.lift hg : (a : N) → P) (f.mk' x.1 x.2) : P) ((g : (a : M) → P) (↑x.2 : M) : P) =
    (g : (a : M) → P) x.1
h₂ :
  HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) x.1 : P)
        ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) x.2)⁻¹ : P) : P))
      ((g : (a : M) → P) (↑x.2 : M) : P) =
    (g : (a : M) → P) x.1
h₃ :
  HMul.hMul (α := P) ((g : (a : M) → P) x.1 : P)
      (HMul.hMul (α := P) (β := P) ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) x.2)⁻¹ : P) : P)
        ((g : (a : M) → P) (↑x.2 : M) : P)) =
    (g : (a : M) → P) x.1
h₄ :
  HMul.hMul (α := P) ((g : (a : M) → P) x.1 : P)
      (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (↑x.2 : M) : P)
        ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) x.2)⁻¹ : P) : P)) =
    (g : (a : M) → P) x.1
⊢ HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1
have h₅ : HMul.hMul (α := P) ((g : (a : M) → P) x.1 : P)
    (HMul.hMul (α := P) (β := P) ((g.restrict S : (a : ↥S) → P) x.2 : P)
      ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) x.2)⁻¹ : P) : P)) =
  (g : (a : M) → P) x.1
Tactic: rw [← hz, f.eq_mk'_iff_mul_eq.2 hx, lift_mk', mul_assoc, mul_comm _ (g ↑x.2),
      ← MonoidHom.restrict_apply, IsUnit.mul_liftRight_inv (g.restrict S) hg, 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)
H : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := P) (⇑(f.lift hg) : (a : N) → P)
v : P
z : N
hz : (f.lift hg : (a : N) → P) z = v
x : M × ↥S
hx : HMul.hMul (β := N) z ((f : (a : M) → N) (↑x.2 : M) : N) = (f : (a : M) → N) x.1
h :
  HMul.hMul (α := P) (β := P) ((f.lift hg : (a : N) → P) z : P) ((g : (a : M) → P) (↑x.2 : M) : P) =
    (g : (a : M) → P) x.1
h₁ :
  HMul.hMul (α := P) (β := P) ((f.lift hg : (a : N) → P) (f.mk' x.1 x.2) : P) ((g : (a : M) → P) (↑x.2 : M) : P) =
    (g : (a : M) → P) x.1
h₂ :
  HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) x.1 : P)
        ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) x.2)⁻¹ : P) : P))
      ((g : (a : M) → P) (↑x.2 : M) : P) =
    (g : (a : M) → P) x.1
h₃ :
  HMul.hMul (α := P) ((g : (a : M) → P) x.1 : P)
      (HMul.hMul (α := P) (β := P) ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) x.2)⁻¹ : P) : P)
        ((g : (a : M) → P) (↑x.2 : M) : P)) =
    (g : (a : M) → P) x.1
h₄ :
  HMul.hMul (α := P) ((g : (a : M) → P) x.1 : P)
      (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (↑x.2 : M) : P)
        ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) x.2)⁻¹ : P) : P)) =
    (g : (a : M) → P) x.1
h₅ :
  HMul.hMul (α := P) ((g : (a : M) → P) x.1 : P)
      (HMul.hMul (α := P) (β := P) ((g.restrict S : (a : ↥S) → P) x.2 : P)
        ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) x.2)⁻¹ : P) : P)) =
    (g : (a : M) → P) x.1
⊢ HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1
have h₆ : HMul.hMul (α := P) (β := P) ((g : (a : M) → P) x.1 : P) (1 : P) = (g : (a : M) → P) x.1
Tactic: rw [← hz, f.eq_mk'_iff_mul_eq.2 hx, lift_mk', mul_assoc, mul_comm _ (g ↑x.2),
      ← MonoidHom.restrict_apply, IsUnit.mul_liftRight_inv (g.restrict S) hg, 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)
H : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := P) (⇑(f.lift hg) : (a : N) → P)
v : P
z : N
hz : (f.lift hg : (a : N) → P) z = v
x : M × ↥S
hx : HMul.hMul (β := N) z ((f : (a : M) → N) (↑x.2 : M) : N) = (f : (a : M) → N) x.1
h :
  HMul.hMul (α := P) (β := P) ((f.lift hg : (a : N) → P) z : P) ((g : (a : M) → P) (↑x.2 : M) : P) =
    (g : (a : M) → P) x.1
h₁ :
  HMul.hMul (α := P) (β := P) ((f.lift hg : (a : N) → P) (f.mk' x.1 x.2) : P) ((g : (a : M) → P) (↑x.2 : M) : P) =
    (g : (a : M) → P) x.1
h₂ :
  HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) x.1 : P)
        ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) x.2)⁻¹ : P) : P))
      ((g : (a : M) → P) (↑x.2 : M) : P) =
    (g : (a : M) → P) x.1
h₃ :
  HMul.hMul (α := P) ((g : (a : M) → P) x.1 : P)
      (HMul.hMul (α := P) (β := P) ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) x.2)⁻¹ : P) : P)
        ((g : (a : M) → P) (↑x.2 : M) : P)) =
    (g : (a : M) → P) x.1
h₄ :
  HMul.hMul (α := P) ((g : (a : M) → P) x.1 : P)
      (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (↑x.2 : M) : P)
        ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) x.2)⁻¹ : P) : P)) =
    (g : (a : M) → P) x.1
h₅ :
  HMul.hMul (α := P) ((g : (a : M) → P) x.1 : P)
      (HMul.hMul (α := P) (β := P) ((g.restrict S : (a : ↥S) → P) x.2 : P)
        ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) x.2)⁻¹ : P) : P)) =
    (g : (a : M) → P) x.1
h₆ : HMul.hMul (α := P) (β := P) ((g : (a : M) → P) x.1 : P) (1 : P) = (g : (a : M) → P) x.1
⊢ HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1
have h₇ : Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) x.1 : P) ((g : (a : M) → P) x.1 : P)
Tactic: rw [← hz, f.eq_mk'_iff_mul_eq.2 hx, lift_mk', mul_assoc, mul_comm _ (g ↑x.2),
      ← MonoidHom.restrict_apply, IsUnit.mul_liftRight_inv (g.restrict S) hg, 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)
H : ∀ (v : P), ∃ (x : M × ↥S), HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1
v : P
⊢ ∃ (a : N), (f.lift hg : (a : N) → P) a = v
have mpr : ∀ (x : M × ↥S) (hx : HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1),
  ∃ (a : N), (f.lift hg : (a : N) → P) a = v
Tactic: obtain ⟨x, hx⟩ := H v
-- 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)
H : ∀ (v : P), ∃ (x : M × ↥S), HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1
v : P
x : M × ↥S
hx : HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1
⊢ ∃ (a : N), (f.lift hg : (a : N) → P) a = v
have h : (f.lift hg : (a : N) → P) (f.mk' x.1 x.2) = v
Tactic: use f.mk' x.1 x.2
-- 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)
H : ∀ (v : P), ∃ (x : M × ↥S), HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1
v : P
x : M × ↥S
hx : HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1
⊢ (f.lift hg : (a : N) → P) (f.mk' x.1 x.2) = v
have h : HMul.hMul (α := P) (β := P) ((g : (a : M) → P) x.1 : P)
    ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) x.2)⁻¹ : P) : P) =
  v
Tactic: rw [lift_mk', mul_inv_left hg, mul_comm, ← hx]
-- 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)
H : ∀ (v : P), ∃ (x : M × ↥S), HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1
v : P
x : M × ↥S
hx : HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1
h :
  HMul.hMul (α := P) (β := P) ((g : (a : M) → P) x.1 : P)
      ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) x.2)⁻¹ : P) : P) =
    v
⊢ (f.lift hg : (a : N) → P) (f.mk' x.1 x.2) = v
have h₁ : (g : (a : M) → P) x.1 = HMul.hMul (α := P) ((g : (a : M) → P) (↑x.2 : M) : P) v
Tactic: rw [lift_mk', mul_inv_left hg, mul_comm, ← hx]
-- 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)
H : ∀ (v : P), ∃ (x : M × ↥S), HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1
v : P
x : M × ↥S
hx : HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1
h :
  HMul.hMul (α := P) (β := P) ((g : (a : M) → P) x.1 : P)
      ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) x.2)⁻¹ : P) : P) =
    v
h₁ : (g : (a : M) → P) x.1 = HMul.hMul (α := P) ((g : (a : M) → P) (↑x.2 : M) : P) v
⊢ (f.lift hg : (a : N) → P) (f.mk' x.1 x.2) = v
have h₂ : (g : (a : M) → P) x.1 = HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P)
Tactic: rw [lift_mk', mul_inv_left hg, mul_comm, ← hx]
-- 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)
H : ∀ (v : P), ∃ (x : M × ↥S), HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1
v : P
x : M × ↥S
hx : HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1
h :
  HMul.hMul (α := P) (β := P) ((g : (a : M) → P) x.1 : P)
      ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) x.2)⁻¹ : P) : P) =
    v
h₁ : (g : (a : M) → P) x.1 = HMul.hMul (α := P) ((g : (a : M) → P) (↑x.2 : M) : P) v
h₂ : (g : (a : M) → P) x.1 = HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P)
⊢ (f.lift hg : (a : N) → P) (f.mk' x.1 x.2) = v
have h₃ : HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P)
Tactic: rw [lift_mk', mul_inv_left hg, mul_comm, ← hx]
-- 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)
⊢ Injective.{u_2 + 1, u_3 + 1} (α := N) (β := P) (⇑(f.lift hg) : (a : N) → P) ↔
    ∀ (x y : M),
      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 mp : Injective.{u_2 + 1, u_3 + 1} (α := N) (β := P) (⇑(f.lift hg) : (a : N) → P) →
  ∀ (x y : M),
    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)
Tactic: constructor
-- 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)
mp :
  Injective.{u_2 + 1, u_3 + 1} (α := N) (β := P) (⇑(f.lift hg) : (a : N) → P) →
    ∀ (x y : M),
      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)
⊢ Injective.{u_2 + 1, u_3 + 1} (α := N) (β := P) (⇑(f.lift hg) : (a : N) → P) ↔
    ∀ (x y : M),
      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 mpr : (∀ (x y : M),
    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)) →
  Injective.{u_2 + 1, u_3 + 1} (α := N) (β := P) (⇑(f.lift hg) : (a : N) → P)
Tactic: constructor
-- 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)
H : Injective.{u_2 + 1, u_3 + 1} (α := N) (β := P) (⇑(f.lift hg) : (a : N) → P)
x y : M
⊢ 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 mp : 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)
Tactic: constructor