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
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)
z : N
h :
  HMul.hMul (α := R) (β := R) ((j : (a : A) → R) ((l : (a : P) → A) (k.sec ((f.map hy k : (a : N) → Q) z)).1 : A) : R)
      ((↑((IsUnit.liftRight ((j.toMonoidHom.comp l).restrict T) ⋯ : (a : ↥T) → Rˣ)
                (k.sec ((f.map hy k : (a : N) → Q) z)).2)⁻¹ :
          R) :
        R) =
    HMul.hMul (α := R) (β := R) ((j : (a : A) → R) ((l : (a : P) → A) ((g : (a : M) → P) (f.sec z).1 : P) : A) : R)
      ((↑((IsUnit.liftRight ((j.toMonoidHom.comp (l.comp g)).restrict S) ⋯ : (a : ↥S) → Rˣ) (f.sec z).2)⁻¹ : R) : R)
⊢ 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)

Tactic:
change j _ * _ = j (l _) * _

Premises used: 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
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)
z : N
h :
  HMul.hMul (α := R) (β := R) ((j : (a : A) → R) ((l : (a : P) → A) (k.sec ((f.map hy k : (a : N) → Q) z)).1 : A) : R)
      ((j.toMonoidHom.comp (l.comp g) : (a : M) → R) (↑(f.sec z).2 : M) : R) =
    HMul.hMul (α := R) (β := R)
      ((j.toMonoidHom.comp l : (a : P) → R) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) : R)
      ((j : (a : A) → R) ((l : (a : P) → A) ((g : (a : M) → P) (f.sec z).1 : P) : A) : R)
⊢ HMul.hMul (α := R) (β := R) ((j : (a : A) → R) ((l : (a : P) → A) (k.sec ((f.map hy k : (a : N) → Q) z)).1 : A) : R)
      ((↑((IsUnit.liftRight ((j.toMonoidHom.comp l).restrict T) ⋯ : (a : ↥T) → Rˣ)
                (k.sec ((f.map hy k : (a : N) → Q) z)).2)⁻¹ :
          R) :
        R) =
    HMul.hMul (α := R) (β := R) ((j : (a : A) → R) ((l : (a : P) → A) ((g : (a : M) → P) (f.sec z).1 : P) : A) : R)
      ((↑((IsUnit.liftRight ((j.toMonoidHom.comp (l.comp g)).restrict S) ⋯ : (a : ↥S) → Rˣ) (f.sec z).2)⁻¹ : R) : R)

Tactic:
rw [mul_inv_left, ← mul_assoc, mul_inv_right]

Premises used: mul_assoc, Submonoid.LocalizationMap.mul_inv_right, 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
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)
z : N
h :
  HMul.hMul (α := R) (β := R) ((j : (a : A) → R) ((l : (a : P) → A) (k.sec ((f.map hy k : (a : N) → Q) z)).1 : A) : R)
      ((j : (a : A) → R) ((l : (a : P) → A) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) : A) : R) =
    HMul.hMul (α := R) (β := R)
      ((j : (a : A) → R) ((l : (a : P) → A) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) : A) : R)
      ((j : (a : A) → R) ((l : (a : P) → A) ((g : (a : M) → P) (f.sec z).1 : P) : A) : R)
⊢ HMul.hMul (α := R) (β := R) ((j : (a : A) → R) ((l : (a : P) → A) (k.sec ((f.map hy k : (a : N) → Q) z)).1 : A) : R)
      ((j.toMonoidHom.comp (l.comp g) : (a : M) → R) (↑(f.sec z).2 : M) : R) =
    HMul.hMul (α := R) (β := R)
      ((j.toMonoidHom.comp l : (a : P) → R) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) : R)
      ((j : (a : A) → R) ((l : (a : P) → A) ((g : (a : M) → P) (f.sec z).1 : P) : A) : R)

Tactic:
change j _ * j (l (g _)) = j (l _) * _

Premises used: 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
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)
z : N
h :
  Eq.{u_6 + 1} (α := R)
    ((j : (a : A) → R)
        ((l : (a : P) → A)
            (HMul.hMul (β := P) (k.sec ((f.map hy k : (a : N) → Q) z)).1 ((g : (a : M) → P) (↑(f.sec z).2 : M) : P)) :
          A) :
      R)
    ((j : (a : A) → R)
        ((l : (a : P) → A)
            (HMul.hMul (β := P) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) ((g : (a : M) → P) (f.sec z).1 : P)) :
          A) :
      R)
⊢ HMul.hMul (α := R) (β := R) ((j : (a : A) → R) ((l : (a : P) → A) (k.sec ((f.map hy k : (a : N) → Q) z)).1 : A) : R)
      ((j : (a : A) → R) ((l : (a : P) → A) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) : A) : R) =
    HMul.hMul (α := R) (β := R)
      ((j : (a : A) → R) ((l : (a : P) → A) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) : A) : R)
      ((j : (a : A) → R) ((l : (a : P) → A) ((g : (a : M) → P) (f.sec z).1 : P) : A) : R)

Tactic:
rw [← map_mul j, ← map_mul j, ← l.map_mul, ← l.map_mul]

Premises used: map_mul, MonoidHom.map_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
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)
z : N
⊢ Eq.{u_6 + 1} (α := R)
    ((j : (a : A) → R)
        ((l : (a : P) → A)
            (HMul.hMul (β := P) (k.sec ((f.map hy k : (a : N) → Q) z)).1 ((g : (a : M) → P) (↑(f.sec z).2 : M) : P)) :
          A) :
      R)
    ((j : (a : A) → R)
        ((l : (a : P) → A)
            (HMul.hMul (β := P) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) ((g : (a : M) → P) (f.sec z).1 : P)) :
          A) :
      R)

Tactic:
k.comp_eq_of_eq hl j ?_

Premises used: Submonoid.LocalizationMap.comp_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
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)
z : N
h :
  Eq.{u_4 + 1} (α := Q)
    ((k : (a : P) → Q)
        (HMul.hMul (β := P) (k.sec ((f.map hy k : (a : N) → Q) z)).1 ((g : (a : M) → P) (↑(f.sec z).2 : M) : P)) :
      Q)
    ((k : (a : P) → Q)
        (HMul.hMul (β := P) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) ((g : (a : M) → P) (f.sec z).1 : P)) :
      Q)
⊢ Eq.{u_6 + 1} (α := R)
    ((j : (a : A) → R)
        ((l : (a : P) → A)
            (HMul.hMul (β := P) (k.sec ((f.map hy k : (a : N) → Q) z)).1 ((g : (a : M) → P) (↑(f.sec z).2 : M) : P)) :
          A) :
      R)
    ((j : (a : A) → R)
        ((l : (a : P) → A)
            (HMul.hMul (β := P) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) ((g : (a : M) → P) (f.sec z).1 : P)) :
          A) :
      R)

Tactic:
refine k.comp_eq_of_eq hl j ?_

Premises used: Submonoid.LocalizationMap.comp_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
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)
z : N
h :
  HMul.hMul (α := Q) (β := Q) ((k : (a : P) → Q) (k.sec ((f.map hy k : (a : N) → Q) z)).1 : Q)
      ((k : (a : P) → Q) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) : Q) =
    (k : (a : P) → Q)
      (HMul.hMul (β := P) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) ((g : (a : M) → P) (f.sec z).1 : P))
h₁ :
  HMul.hMul (α := Q) (β := Q) ((k : (a : P) → Q) (k.sec ((f.map hy k : (a : N) → Q) z)).1 : Q)
      ((k : (a : P) → Q) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) : Q) =
    HMul.hMul (α := Q) (β := Q) ((k : (a : P) → Q) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) : Q)
      ((k : (a : P) → Q) ((g : (a : M) → P) (f.sec z).1 : P) : Q)
h₂ :
  HMul.hMul (β := Q)
      (HMul.hMul (α := Q) (β := Q) ((k : (a : P) → Q) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) : 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) =
    HMul.hMul (α := Q) (β := Q) ((k : (a : P) → Q) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) : Q)
      ((k : (a : P) → Q) ((g : (a : M) → P) (f.sec z).1 : P) : Q)
h₃ :
  HMul.hMul (α := Q) ((k : (a : P) → Q) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) : Q)
      (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)) =
    HMul.hMul (α := Q) (β := Q) ((k : (a : P) → Q) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) : Q)
      ((k : (a : P) → Q) ((g : (a : M) → P) (f.sec z).1 : P) : Q)
h₄ h₅ :
  HMul.hMul (α := Q) (β := Q) ((k : (a : P) → Q) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) : Q)
      ((k : (a : P) → Q) ((g : (a : M) → P) (f.sec z).1 : P) : Q) =
    HMul.hMul (α := Q) (β := Q) ((k : (a : P) → Q) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) : Q)
      ((k : (a : P) → Q) ((g : (a : M) → P) (f.sec z).1 : P) : Q)
⊢ Eq.{u_4 + 1} (α := Q)
    ((k : (a : P) → Q)
        (HMul.hMul (β := P) (k.sec ((f.map hy k : (a : N) → Q) z)).1 ((g : (a : M) → P) (↑(f.sec z).2 : M) : P)) :
      Q)
    ((k : (a : P) → Q)
        (HMul.hMul (β := P) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) ((g : (a : M) → P) (f.sec z).1 : P)) :
      Q)

Tactic:
rw [map_mul k, map_mul k, sec_spec', mul_assoc, map_mul_right]

Premises used: mul_assoc, map_mul, Submonoid.LocalizationMap.sec_spec', 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
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)
x : N
rw :
  Eq.{u_6 + 1} (α := R) ((k.map hl j : (a : Q) → R) ((f.map hy k : (a : N) → Q) x : Q) : R)
    (((k.map hl j).comp (f.map hy k) : (a : N) → R) x : R)
⊢ Eq.{u_6 + 1} (α := R) ((k.map hl j : (a : Q) → R) ((f.map hy k : (a : N) → Q) x : Q) : R)
    ((f.map (g := l.comp g) ⋯ j : (a : N) → R) x : R)

Tactic:
rw [← f.map_comp_map (k := k) hy j hl]

Premises used: Submonoid.LocalizationMap.map_comp_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
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)
x : N
⊢ Eq.{u_6 + 1} (α := R) ((k.map hl j : (a : Q) → R) ((f.map hy k : (a : N) → Q) x : Q) : R)
    (((k.map hl j).comp (f.map hy k) : (a : N) → R) x : R)

Tactic:
simp only [MonoidHom.coe_comp, comp_apply]

Premises used: MonoidHom.coe_comp, Function.comp_apply
-- 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
or :
  Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P) ∨
    Injective.{u_3 + 1, u_4 + 1} (α := P) (β := Q) (⇑k : (a : P) → Q)
hg : Injective.{u_1 + 1, u_3 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
z w : N
hizw : Eq.{u_4 + 1} (α := Q) ((f.map hy k : (a : N) → Q) z : Q) ((f.map hy k : (a : N) → Q) w : Q)
⊢ let i := f.map hy k;
  Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) z : Q) ((i : (a : N) → Q) w : Q)

Tactic:
set i := f.map hy k

Premises used: 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
or :
  Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P) ∨
    Injective.{u_3 + 1, u_4 + 1} (α := P) (β := Q) (⇑k : (a : P) → Q)
hg : Injective.{u_1 + 1, u_3 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
z w : N
i : N →* Q := f.map hy k
hizw : Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) z : Q) ((i : (a : N) → Q) w : Q)
⊢ ∀ (a : M),
    Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) ((f : (a : M) → N) a : N) : Q)
      ((k : (a : P) → Q) ((g : (a : M) → P) a : P) : Q)

Tactic:
have ifkg (a : M) : i (f a) = k (g a) := f.map_eq hy a
-- 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
or :
  Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P) ∨
    Injective.{u_3 + 1, u_4 + 1} (α := P) (β := Q) (⇑k : (a : P) → Q)
hg : Injective.{u_1 + 1, u_3 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
z w : N
i : N →* Q := f.map hy k
hizw : Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) z : Q) ((i : (a : N) → Q) w : Q)
ifkg :
  ∀ (a : M),
    Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) ((f : (a : M) → N) a : N) : Q)
      ((k : (a : P) → Q) ((g : (a : M) → P) a : P) : Q)
have :
  ∀ (z' w' : M) (x : ↥S) (hxz : HMul.hMul (β := N) z ((f : (a : M) → N) (↑x : M) : N) = (f : (a : M) → N) z')
    (hxw : HMul.hMul (β := N) w ((f : (a : M) → N) (↑x : M) : N) = (f : (a : M) → N) w'), z = w
⊢ z = w

Tactic:
have ⟨z', w', x, hxz, hxw⟩ := surj₂ f z w
-- 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
or :
  Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P) ∨
    Injective.{u_3 + 1, u_4 + 1} (α := P) (β := Q) (⇑k : (a : P) → Q)
hg : Injective.{u_1 + 1, u_3 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
z w : N
i : N →* Q := f.map hy k
hizw : Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) z : Q) ((i : (a : N) → Q) w : Q)
ifkg :
  ∀ (a : M),
    Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) ((f : (a : M) → N) a : N) : Q)
      ((k : (a : P) → Q) ((g : (a : M) → P) a : P) : Q)
z' w' : M
x : ↥S
hxz : HMul.hMul (β := N) z ((f : (a : M) → N) (↑x : M) : N) = (f : (a : M) → N) z'
hxw : HMul.hMul (β := N) w ((f : (a : M) → N) (↑x : M) : N) = (f : (a : M) → N) w'
rw :
  Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) ((f : (a : M) → N) z' : N) : Q)
    ((k : (a : P) → Q) ((g : (a : M) → P) w' : P) : Q)
rw₁ :
  Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) ((f : (a : M) → N) z' : N) : Q)
    ((i : (a : N) → Q) ((f : (a : M) → N) w' : N) : Q)
rw₂ :
  Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) (HMul.hMul (β := N) z ((f : (a : M) → N) (↑x : M) : N)) : Q)
    ((i : (a : N) → Q) ((f : (a : M) → N) w' : N) : Q)
rw₃ :
  Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) (HMul.hMul (β := N) z ((f : (a : M) → N) (↑x : M) : N)) : Q)
    ((i : (a : N) → Q) (HMul.hMul (β := N) w ((f : (a : M) → N) (↑x : M) : N)) : Q)
rw₄ :
  HMul.hMul (α := Q) (β := Q) ((i : (a : N) → Q) z : Q) ((i : (a : N) → Q) ((f : (a : M) → N) (↑x : M) : N) : Q) =
    (i : (a : N) → Q) (HMul.hMul (β := N) w ((f : (a : M) → N) (↑x : M) : N))
rw₅ :
  HMul.hMul (α := Q) (β := Q) ((i : (a : N) → Q) z : Q) ((i : (a : N) → Q) ((f : (a : M) → N) (↑x : M) : N) : Q) =
    HMul.hMul (α := Q) (β := Q) ((i : (a : N) → Q) w : Q) ((i : (a : N) → Q) ((f : (a : M) → N) (↑x : M) : N) : Q)
rw₆ rw₇ :
  HMul.hMul (α := Q) (β := Q) ((i : (a : N) → Q) w : Q) ((i : (a : N) → Q) ((f : (a : M) → N) (↑x : M) : N) : Q) =
    HMul.hMul (α := Q) (β := Q) ((i : (a : N) → Q) w : Q) ((i : (a : N) → Q) ((f : (a : M) → N) (↑x : M) : N) : Q)
⊢ Eq.{u_4 + 1} (α := Q) ((k : (a : P) → Q) ((g : (a : M) → P) z' : P) : Q)
    ((k : (a : P) → Q) ((g : (a : M) → P) w' : P) : Q)

Tactic:
rw [← ifkg, ← ifkg, ← hxz, ← hxw, map_mul, map_mul, hizw]

Premises used: map_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
or :
  Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P) ∨
    Injective.{u_3 + 1, u_4 + 1} (α := P) (β := Q) (⇑k : (a : P) → Q)
hg : Injective.{u_1 + 1, u_3 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
z w : N
i : N →* Q := f.map hy k
hizw : Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) z : Q) ((i : (a : N) → Q) w : Q)
ifkg :
  ∀ (a : M),
    Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) ((f : (a : M) → N) a : N) : Q)
      ((k : (a : P) → Q) ((g : (a : M) → P) a : P) : Q)
z' w' : M
x : ↥S
hxz : HMul.hMul (β := N) z ((f : (a : M) → N) (↑x : M) : N) = (f : (a : M) → N) z'
hxw : HMul.hMul (β := N) w ((f : (a : M) → N) (↑x : M) : N) = (f : (a : M) → N) w'
⊢ Eq.{u_4 + 1} (α := Q) ((k : (a : P) → Q) ((g : (a : M) → P) z' : P) : Q)
    ((k : (a : P) → Q) ((g : (a : M) → P) w' : P) : Q)

Tactic:
have : k (g z') = k (g w') := by rw [← ifkg, ← ifkg, ← hxz, ← hxw, map_mul, map_mul, hizw]
-- 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
or :
  Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P) ∨
    Injective.{u_3 + 1, u_4 + 1} (α := P) (β := Q) (⇑k : (a : P) → Q)
hg : Injective.{u_1 + 1, u_3 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
z w : N
i : N →* Q := f.map hy k
hizw : Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) z : Q) ((i : (a : N) → Q) w : Q)
ifkg :
  ∀ (a : M),
    Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) ((f : (a : M) → N) a : N) : Q)
      ((k : (a : P) → Q) ((g : (a : M) → P) a : P) : Q)
z' w' : M
x : ↥S
hxz : HMul.hMul (β := N) z ((f : (a : M) → N) (↑x : M) : N) = (f : (a : M) → N) z'
hxw : HMul.hMul (β := N) w ((f : (a : M) → N) (↑x : M) : N) = (f : (a : M) → N) w'
this :
  Eq.{u_4 + 1} (α := Q) ((k : (a : P) → Q) ((g : (a : M) → P) z' : P) : Q)
    ((k : (a : P) → Q) ((g : (a : M) → P) w' : P) : Q)
inl : ∀ (surj : Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P)), z = w
inr : ∀ (inj : Injective.{u_3 + 1, u_4 + 1} (α := P) (β := Q) (⇑k : (a : P) → Q)), z = w
⊢ z = w

Tactic:
obtain surj | inj := or

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
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
hg : Injective.{u_1 + 1, u_3 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
z w : N
i : N →* Q := f.map hy k
hizw : Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) z : Q) ((i : (a : N) → Q) w : Q)
ifkg :
  ∀ (a : M),
    Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) ((f : (a : M) → N) a : N) : Q)
      ((k : (a : P) → Q) ((g : (a : M) → P) a : P) : Q)
z' w' : M
x : ↥S
hxz : HMul.hMul (β := N) z ((f : (a : M) → N) (↑x : M) : N) = (f : (a : M) → N) z'
hxw : HMul.hMul (β := N) w ((f : (a : M) → N) (↑x : M) : N) = (f : (a : M) → N) w'
this :
  Eq.{u_4 + 1} (α := Q) ((k : (a : P) → Q) ((g : (a : M) → P) z' : P) : Q)
    ((k : (a : P) → Q) ((g : (a : M) → P) w' : P) : Q)
surj : Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P)
inl :
  ∀ (c : P) (hc' : c ∈ T)
    (eq :
      HMul.hMul (β := P) (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ T) c hc') : P) ((g : (a : M) → P) z' : P) =
        HMul.hMul (β := P) (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ T) c hc') : P) ((g : (a : M) → P) w' : P)),
    z = w
⊢ z = w

Tactic:
have ⟨⟨c, hc'⟩, eq⟩ := k.exists_of_eq this