awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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
h₇ h₈ : Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) x.1 : P) ((g : (a : M) → P) x.1 : P)
⊢ HMul.hMul (β := P) v ((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]

Premises used: Iff.mpr, mul_assoc, MonoidHom.restrict, MonoidHom.restrict_apply, IsUnit.mul_liftRight_inv, Submonoid.LocalizationMap.lift_mk', mul_comm, Submonoid.LocalizationMap.eq_mk'_iff_mul_eq, mul_one, Subtype.val, Prod.snd, DFunLike.coe
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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
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
⊢ ∃ (a : N), (f.lift hg : (a : N) → P) a = v

Tactic:
obtain ⟨x, hx⟩ := H v
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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 : (f.lift hg : (a : N) → P) (f.mk' x.1 x.2) = v
⊢ ∃ (a : N), (f.lift hg : (a : N) → P) a = v

Tactic:
use f.mk' x.1 x.2

Premises used: Submonoid.LocalizationMap.mk', Prod.fst, Prod.snd
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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)
h₃ 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)
⊢ (f.lift hg : (a : N) → P) (f.mk' x.1 x.2) = v

Tactic:
rw [lift_mk', mul_inv_left hg, mul_comm, ← hx]

Premises used: Submonoid.LocalizationMap.lift_mk', mul_comm, Submonoid.LocalizationMap.mul_inv_left
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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)
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)
⊢ 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
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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
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)
mp₁ :
  Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) x : P) ((g : (a : M) → P) y : P) →
    Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
⊢ 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
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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)

Tactic:
f.eq_of_eq hg

Premises used: Submonoid.LocalizationMap.eq_of_eq
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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)

Tactic:
exact f.eq_of_eq hg

Premises used: Submonoid.LocalizationMap.eq_of_eq
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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
h : Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) x : P) ((g : (a : M) → P) y : P)
⊢ Eq.{u_3 + 1} (α := P) ((f.lift hg : (a : N) → P) ((f : (a : M) → N) x : N) : P)
    ((f.lift hg : (a : N) → P) ((f : (a : M) → N) y : N) : P)

Tactic:
rw [← f.lift_eq hg, ← f.lift_eq hg] at h

Premises used: Submonoid.LocalizationMap.lift_eq
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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
h :
  Eq.{u_3 + 1} (α := P) ((f.lift hg : (a : N) → P) ((f : (a : M) → N) x : N) : P)
    ((f.lift hg : (a : N) → P) ((f : (a : M) → N) y : N) : P)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)

Tactic:
H h
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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
h :
  Eq.{u_3 + 1} (α := P) ((f.lift hg : (a : N) → P) ((f : (a : M) → N) x : N) : P)
    ((f.lift hg : (a : N) → P) ((f : (a : M) → N) y : N) : P)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)

Tactic:
exact H h
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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 :
  ∀ (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)
z w : N
h : Eq.{u_3 + 1} (α := P) ((f.lift hg : (a : N) → P) z : P) ((f.lift hg : (a : N) → P) w : P)
mpr : ∀ (w_1 : M × ↥S), HMul.hMul (β := N) z ((f : (a : M) → N) (↑w_1.2 : M) : N) = (f : (a : M) → N) w_1.1 → z = w
⊢ z = w

Tactic:
obtain ⟨_, _⟩ := f.surj z

Premises used: Submonoid.LocalizationMap.surj
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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 :
  ∀ (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)
z w : N
h : Eq.{u_3 + 1} (α := P) ((f.lift hg : (a : N) → P) z : P) ((f.lift hg : (a : N) → P) w : P)
w_1 : M × ↥S
h_1 : HMul.hMul (β := N) z ((f : (a : M) → N) (↑w_1.2 : M) : N) = (f : (a : M) → N) w_1.1
mpr : ∀ (w_2 : M × ↥S), HMul.hMul (β := N) w ((f : (a : M) → N) (↑w_2.2 : M) : N) = (f : (a : M) → N) w_2.1 → z = w
⊢ z = w

Tactic:
obtain ⟨_, _⟩ := f.surj w

Premises used: Submonoid.LocalizationMap.surj
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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 :
  ∀ (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)
z w : N
h : Eq.{u_3 + 1} (α := P) ((f.lift hg : (a : N) → P) z : P) ((f.lift hg : (a : N) → P) w : P)
w_1 : M × ↥S
h_1 : HMul.hMul (β := N) z ((f : (a : M) → N) (↑w_1.2 : M) : N) = (f : (a : M) → N) w_1.1
w_2 : M × ↥S
h_2 : HMul.hMul (β := N) w ((f : (a : M) → N) (↑w_2.2 : M) : N) = (f : (a : M) → N) w_2.1
mpr : f.mk' (f.sec z).1 (f.sec z).2 = f.mk' (f.sec w).1 (f.sec w).2
⊢ z = w

Tactic:
rw [← f.mk'_sec z, ← f.mk'_sec w]

Premises used: Submonoid.LocalizationMap.mk'_sec
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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 :
  ∀ (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)
z w : N
h : Eq.{u_3 + 1} (α := P) ((f.lift hg : (a : N) → P) z : P) ((f.lift hg : (a : N) → P) w : P)
w_1 : M × ↥S
h_1 : HMul.hMul (β := N) z ((f : (a : M) → N) (↑w_1.2 : M) : N) = (f : (a : M) → N) w_1.1
w_2 : M × ↥S
h_2 : HMul.hMul (β := N) w ((f : (a : M) → N) (↑w_2.2 : M) : N) = (f : (a : M) → N) w_2.1
⊢ f.mk' (f.sec z).1 (f.sec z).2 = f.mk' (f.sec w).1 (f.sec w).2

Tactic:
(mul_inv f.map_units).2 ((H _ _).2 <| (mul_inv hg).1 h)

Premises used: Iff.mpr, Submonoid.LocalizationMap.mk', Iff.mp, Submonoid.LocalizationMap.map_units, Submonoid.LocalizationMap.mul_inv
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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 :
  ∀ (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)
z w : N
h : Eq.{u_3 + 1} (α := P) ((f.lift hg : (a : N) → P) z : P) ((f.lift hg : (a : N) → P) w : P)
w_1 : M × ↥S
h_1 : HMul.hMul (β := N) z ((f : (a : M) → N) (↑w_1.2 : M) : N) = (f : (a : M) → N) w_1.1
w_2 : M × ↥S
h_2 : HMul.hMul (β := N) w ((f : (a : M) → N) (↑w_2.2 : M) : N) = (f : (a : M) → N) w_2.1
⊢ f.mk' (f.sec z).1 (f.sec z).2 = f.mk' (f.sec w).1 (f.sec w).2

Tactic:
exact (mul_inv f.map_units).2 ((H _ _).2 <| (mul_inv hg).1 h)

Premises used: Iff.mpr, Iff.mp, Submonoid.LocalizationMap.map_units, Submonoid.LocalizationMap.mul_inv
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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
T : Submonoid P
hy : ∀ (y : ↥S), Membership.mem (α := P) T ((g : (a : M) → P) (↑y : M) : P)
Q : Type u_4
inst_3 : CommMonoid Q
k : T.LocalizationMap Q
x : M
⊢ Eq.{u_4 + 1} (α := Q) ((f.map hy k : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
    ((k : (a : P) → Q) ((g : (a : M) → P) x : P) : Q)

Tactic:
f.lift_eq (fun y ↦ k.map_units ⟨g y, hy y⟩) x

Premises used: Submonoid.LocalizationMap.lift_eq
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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
T : Submonoid P
hy : ∀ (y : ↥S), Membership.mem (α := P) T ((g : (a : M) → P) (↑y : M) : P)
Q : Type u_4
inst_3 : CommMonoid Q
k : T.LocalizationMap Q
⊢ (f.map hy k).comp f.toMonoidHom = k.toMonoidHom.comp g

Tactic:
f.lift_comp fun y ↦ k.map_units ⟨g y, hy y⟩

Premises used: Submonoid.LocalizationMap.lift_comp, Submonoid.LocalizationMap.map
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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
T : Submonoid P
hy : ∀ (y : ↥S), Membership.mem (α := P) T ((g : (a : M) → P) (↑y : M) : P)
Q : Type u_4
inst_3 : CommMonoid Q
k : T.LocalizationMap Q
x : M
y : ↥S
rw :
  (k.toMonoidHom.comp g : (a : M) → Q) x =
    HMul.hMul (α := Q) ((k.toMonoidHom.comp g : (a : M) → Q) (↑y : M) : Q)
      (k.mk' ((g : (a : M) → P) x) (Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) (↑y : M)) ⋯))
⊢ (f.map hy k : (a : N) → Q) (f.mk' x y) =
    k.mk' ((g : (a : M) → P) x) (Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) (↑y : M)) ⋯)

Tactic:
rw [map, lift_mk', mul_inv_left]

Premises used: Submonoid.LocalizationMap.lift_mk', Submonoid.LocalizationMap.map, Submonoid.LocalizationMap.mul_inv_left
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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
T : Submonoid P
hy : ∀ (y : ↥S), Membership.mem (α := P) T ((g : (a : M) → P) (↑y : M) : P)
Q : Type u_4
inst_3 : CommMonoid Q
k : T.LocalizationMap Q
x : M
y : ↥S
change :
  (k : (a : P) → Q) ((g : (a : M) → P) x : P) =
    HMul.hMul (α := Q) ((k : (a : P) → Q) ((g : (a : M) → P) (↑y : M) : P) : Q)
      (k.mk' ((g : (a : M) → P) x) (Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) (↑y : M)) ⋯))
⊢ (k.toMonoidHom.comp g : (a : M) → Q) x =
    HMul.hMul (α := Q) ((k.toMonoidHom.comp g : (a : M) → Q) (↑y : M) : Q)
      (k.mk' ((g : (a : M) → P) x) (Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) (↑y : M)) ⋯))

Tactic:
change k (g x) = k (g y) * _

Premises used: Subtype.val, DFunLike.coe
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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
T : Submonoid P
hy : ∀ (y : ↥S), Membership.mem (α := P) T ((g : (a : M) → P) (↑y : M) : P)
Q : Type u_4
inst_3 : CommMonoid Q
k : T.LocalizationMap Q
x : M
y : ↥S
rw :
  (k : (a : P) → Q) ((g : (a : M) → P) x : P) =
    k.mk' (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (↑y : M) : P) ((g : (a : M) → P) x : P))
      (Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) (↑y : M)) ⋯)
⊢ (k : (a : P) → Q) ((g : (a : M) → P) x : P) =
    HMul.hMul (α := Q) ((k : (a : P) → Q) ((g : (a : M) → P) (↑y : M) : P) : Q)
      (k.mk' ((g : (a : M) → P) x) (Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) (↑y : M)) ⋯))

Tactic:
rw [mul_mk'_eq_mk'_of_mul]

Premises used: Submonoid.LocalizationMap.mul_mk'_eq_mk'_of_mul
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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
T : Submonoid P
hy : ∀ (y : ↥S), Membership.mem (α := P) T ((g : (a : M) → P) (↑y : M) : P)
Q : Type u_4
inst_3 : CommMonoid Q
k : T.LocalizationMap Q
x : M
y : ↥S
⊢ (k : (a : P) → Q) ((g : (a : M) → P) x : P) =
    k.mk' (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (↑y : M) : P) ((g : (a : M) → P) x : P))
      (Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) (↑y : M)) ⋯)

Tactic:
(k.mk'_mul_cancel_left (g x) ⟨g y, hy y⟩).symm

Premises used: Submonoid.LocalizationMap.mk'_mul_cancel_left, Subtype.mk, Eq.symm, Subtype.val, DFunLike.coe
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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
T : Submonoid P
hy : ∀ (y : ↥S), Membership.mem (α := P) T ((g : (a : M) → P) (↑y : M) : P)
Q : Type u_4
inst_3 : CommMonoid Q
k : T.LocalizationMap Q
x : M
y : ↥S
⊢ (k : (a : P) → Q) ((g : (a : M) → P) x : P) =
    k.mk' (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (↑y : M) : P) ((g : (a : M) → P) x : P))
      (Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) (↑y : M)) ⋯)

Tactic:
exact (k.mk'_mul_cancel_left (g x) ⟨g y, hy y⟩).symm

Premises used: Submonoid.LocalizationMap.mk'_mul_cancel_left, Subtype.mk, Eq.symm, Subtype.val, DFunLike.coe
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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
T : Submonoid P
hy : ∀ (y : ↥S), Membership.mem (α := P) T ((g : (a : M) → P) (↑y : M) : P)
Q : Type u_4
inst_3 : CommMonoid Q
k : T.LocalizationMap Q
z : N
u : Q
⊢ (f.map hy k : (a : N) → Q) z = u ↔
    (k : (a : P) → Q) ((g : (a : M) → P) (f.sec z).1 : P) =
      HMul.hMul (α := Q) ((k : (a : P) → Q) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) : Q) u

Tactic:
f.lift_spec (fun y ↦ k.map_units ⟨g y, hy y⟩) _ _

Premises used: Submonoid.LocalizationMap.lift_spec
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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
T : Submonoid P
hy : ∀ (y : ↥S), Membership.mem (α := P) T ((g : (a : M) → P) (↑y : M) : P)
Q : Type u_4
inst_3 : CommMonoid Q
k : T.LocalizationMap Q
z : N
⊢ HMul.hMul (α := Q) (β := Q) ((f.map hy k : (a : N) → Q) z : Q)
      ((k : (a : P) → Q) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) : Q) =
    (k : (a : P) → Q) ((g : (a : M) → P) (f.sec z).1 : P)

Tactic:
f.lift_mul_right (fun y ↦ k.map_units ⟨g y, hy y⟩) _

Premises used: Submonoid.LocalizationMap.lift_mul_right
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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
T : Submonoid P
hy : ∀ (y : ↥S), Membership.mem (α := P) T ((g : (a : M) → P) (↑y : M) : P)
Q : Type u_4
inst_3 : CommMonoid Q
k : T.LocalizationMap Q
z : N
rw :
  HMul.hMul (α := Q) (β := Q) ((f.map hy k : (a : N) → Q) z : Q)
      ((k : (a : P) → Q) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) : Q) =
    (k : (a : P) → Q) ((g : (a : M) → P) (f.sec z).1 : P)
rw₁ rw₂ :
  Eq.{u_4 + 1} (α := Q) ((k : (a : P) → Q) ((g : (a : M) → P) (f.sec z).1 : P) : Q)
    ((k : (a : P) → Q) ((g : (a : M) → P) (f.sec z).1 : P) : Q)
⊢ HMul.hMul (α := Q) (β := Q) ((k : (a : P) → Q) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) : Q)
      ((f.map hy k : (a : N) → Q) z : Q) =
    (k : (a : P) → Q) ((g : (a : M) → P) (f.sec z).1 : P)

Tactic:
rw [mul_comm, f.map_mul_right]

Premises used: mul_comm, Submonoid.LocalizationMap.map_mul_right
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
f : S.LocalizationMap N
z : N
⊢ (f.map (g := MonoidHom.id M) ⋯ f : (a : N) → N) z = z

Tactic:
f.lift_id z

Premises used: Submonoid.LocalizationMap.lift_id
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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
T : Submonoid P
hy : ∀ (y : ↥S), Membership.mem (α := P) T ((g : (a : M) → P) (↑y : M) : P)
Q : Type u_4
inst_3 : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst_4 : CommMonoid A
U : Submonoid A
R : Type u_6
inst_5 : CommMonoid R
j : U.LocalizationMap R
l : P →* A
hl : ∀ (w : ↥T), Membership.mem (α := A) U ((l : (a : P) → A) (↑w : P) : A)
h :
  ∀ (z : N),
    Eq.{u_6 + 1} (α := R) (((k.map hl j).comp (f.map hy k) : (a : N) → R) z : R)
      ((f.map (g := l.comp g) ⋯ j : (a : N) → R) z : R)
⊢ (k.map hl j).comp (f.map hy k) = f.map (g := l.comp g) ⋯ j

Tactic:
ext z