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
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)
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)
inl :
  ∀ (c : M) (hc : c ∈ (↑S : Set M)) (hc' : Membership.mem (α := P) T ((g : (a : M) → P) c : P))
    (eq :
      HMul.hMul (α := P) (β := P) ((↑(Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) c) hc') : P) : P)
          ((g : (a : M) → P) z' : P) =
        HMul.hMul (α := P) (β := P) ((↑(Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) c) hc') : P) : P)
          ((g : (a : M) → P) w' : P)),
    z = w
⊢ z = w

Tactic:
obtain ⟨c, hc, rfl⟩ := surj hc'

Premises used: rfl
-- 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)
c : M
hc : c ∈ (↑S : Set M)
hc' : Membership.mem (α := P) T ((g : (a : M) → P) c : P)
eq :
  HMul.hMul (α := P) (β := P) ((↑(Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) c) hc') : P) : P)
      ((g : (a : M) → P) z' : P) =
    HMul.hMul (α := P) (β := P) ((↑(Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) c) hc') : P) : P)
      ((g : (a : M) → P) w' : P)
⊢ c * z' = c * w'

Tactic:
simp_rw [← map_mul, hg.eq_iff] at eq

Premises used: Function.Injective.eq_iff, 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
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)
c : M
hc : c ∈ (↑S : Set M)
hc' : Membership.mem (α := P) T ((g : (a : M) → P) c : P)
eq : c * z' = c * w'
inl : ∃ (c : ↥S), (↑c : M) * z' = (↑c : M) * w'
⊢ z = w

Tactic:
rw [← (f.map_units x).mul_left_inj, hxz, hxw, f.eq_iff_exists]

Premises used: Submonoid.LocalizationMap.eq_iff_exists, IsUnit.mul_left_inj, Submonoid.LocalizationMap.map_units
-- 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)
c : M
hc : c ∈ (↑S : Set M)
hc' : Membership.mem (α := P) T ((g : (a : M) → P) c : P)
eq : c * z' = c * w'
⊢ ∃ (c : ↥S), (↑c : M) * z' = (↑c : M) * w'

Tactic:
⟨⟨c, hc⟩, eq⟩

Premises used: Subtype.mk, Exists.intro
-- 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)
c : M
hc : c ∈ (↑S : Set M)
hc' : Membership.mem (α := P) T ((g : (a : M) → P) c : P)
eq : c * z' = c * w'
⊢ ∃ (c : ↥S), (↑c : M) * z' = (↑c : M) * w'

Tactic:
exact ⟨⟨c, hc⟩, 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
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)
inj : Injective.{u_3 + 1, u_4 + 1} (α := P) (β := Q) (⇑k : (a : P) → Q)
inr : HMul.hMul (β := N) z ((f : (a : M) → N) (↑x : M) : N) = HMul.hMul (β := N) w ((f : (a : M) → N) (↑x : M) : N)
⊢ z = w

Tactic:
apply (f.map_units x).mul_right_cancel

Premises used: Submonoid.LocalizationMap.map_units, IsUnit.mul_right_cancel
-- 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)
inj : Injective.{u_3 + 1, u_4 + 1} (α := P) (β := Q) (⇑k : (a : P) → Q)
inr : (f : (a : M) → N) z' = HMul.hMul (β := N) w ((f : (a : M) → N) (↑x : M) : N)
inr₁ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) z' : N) ((f : (a : M) → N) w' : N)
inr₂ inr₃ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) w' : N) ((f : (a : M) → N) w' : N)
⊢ HMul.hMul (β := N) z ((f : (a : M) → N) (↑x : M) : N) = HMul.hMul (β := N) w ((f : (a : M) → N) (↑x : M) : N)

Tactic:
rw [hxz, hxw, hg (inj this)]
-- 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
surj : Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P)
hg : Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
z : Q
obtain :
  ∀ (y t : P) (ht : t ∈ T),
    ∃ (a : N), (f.map hy k : (a : N) → Q) a = k.mk' y (Subtype.mk (p := fun (x : P) ↦ x ∈ T) t ht)
⊢ ∃ (a : N), (f.map hy k : (a : N) → Q) a = z

Tactic:
obtain ⟨y, ⟨t, ht⟩, rfl⟩ := k.mk'_surjective z

Premises used: Submonoid.LocalizationMap.mk'_surjective, rfl
-- 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
surj : Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P)
hg : Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
y t : P
ht : t ∈ T
obtain :
  ∀ (s : M) (hs : s ∈ (↑S : Set M)) (ht : Membership.mem (α := P) T ((g : (a : M) → P) s : P)),
    ∃ (a : N), (f.map hy k : (a : N) → Q) a = k.mk' y (Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) s) ht)
⊢ ∃ (a : N), (f.map hy k : (a : N) → Q) a = k.mk' y (Subtype.mk (p := fun (x : P) ↦ x ∈ T) t ht)

Tactic:
obtain ⟨s, hs, rfl⟩ := surj ht

Premises used: rfl
-- 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
surj : Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P)
hg : Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
y : P
s : M
hs : s ∈ (↑S : Set M)
ht : Membership.mem (α := P) T ((g : (a : M) → P) s : P)
obtain :
  ∀ (x : M),
    ∃ (a : N),
      (f.map hy k : (a : N) → Q) a =
        k.mk' ((g : (a : M) → P) x) (Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) s) ht)
⊢ ∃ (a : N), (f.map hy k : (a : N) → Q) a = k.mk' y (Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) s) ht)

Tactic:
obtain ⟨x, rfl⟩ := hg y

Premises used: rfl
-- 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
surj : Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P)
hg : Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
s : M
hs : s ∈ (↑S : Set M)
ht : Membership.mem (α := P) T ((g : (a : M) → P) s : P)
x : M
h :
  (f.map hy k : (a : N) → Q) (f.mk' x (Subtype.mk (p := fun (x : M) ↦ x ∈ S) s hs)) =
    k.mk' ((g : (a : M) → P) x) (Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) s) ht)
⊢ ∃ (a : N),
    (f.map hy k : (a : N) → Q) a =
      k.mk' ((g : (a : M) → P) x) (Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) s) ht)

Tactic:
use f.mk' x ⟨s, hs⟩

Premises used: Submonoid.LocalizationMap.mk', Subtype.mk
-- 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
surj : Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P)
hg : Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
s : M
hs : s ∈ (↑S : Set M)
ht : Membership.mem (α := P) T ((g : (a : M) → P) s : P)
x : M
h h₁ :
  k.mk' ((g : (a : M) → P) x)
      (Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ S) s hs) : M))
        ⋯) =
    k.mk' ((g : (a : M) → P) x) (Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) s) ht)
⊢ (f.map hy k : (a : N) → Q) (f.mk' x (Subtype.mk (p := fun (x : M) ↦ x ∈ S) s hs)) =
    k.mk' ((g : (a : M) → P) x) (Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) s) ht)

Tactic:
rw [map_mk']

Premises used: Submonoid.LocalizationMap.map_mk'
-- 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
Q : Type u_4
inst_3 : CommMonoid Q
hg : Injective.{u_1 + 1, u_3 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
k : LocalizationMap (Submonoid.map g S) Q
⊢ Injective.{u_2 + 1, u_4 + 1} (α := N) (β := Q) (⇑(f.map ⋯ k) : (a : N) → Q)

Tactic:
f.map_injective_of_surjOn_or_injective _ (.inl <| Set.surjOn_image ..) hg

Premises used: Set.surjOn_image, Or.inl, Submonoid.LocalizationMap.map_injective_of_surjOn_or_injective
-- 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
Q : Type u_4
inst_3 : CommMonoid Q
hg : Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
k : LocalizationMap (Submonoid.map g S) Q
⊢ Surjective.{u_2 + 1, u_4 + 1} (α := N) (β := Q) (⇑(f.map ⋯ k) : (a : N) → Q)

Tactic:
f.map_surjective_of_surjOn _ (Set.surjOn_image ..) hg

Premises used: Set.surjOn_image, Submonoid.LocalizationMap.map_surjective_of_surjOn
-- 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
k : S.LocalizationMap P
x : N
⊢ Eq.{u_3 + 1} (α := P) ((f.mulEquivOfLocalizations k : (a : N) → P) x : P) ((f.lift ⋯ : (a : N) → P) x : P)

Tactic:
rfl

Premises used: rfl
-- 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
k : S.LocalizationMap P
x : P
⊢ Eq.{u_2 + 1} (α := N) (((f.mulEquivOfLocalizations k).symm : (a : P) → N) x : N) ((k.lift ⋯ : (a : P) → N) x : N)

Tactic:
rfl

Premises used: rfl
-- 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
k : S.LocalizationMap P
⊢ (k.mulEquivOfLocalizations f).symm = f.mulEquivOfLocalizations k

Tactic:
rfl

Premises used: Submonoid.LocalizationMap.mulEquivOfLocalizations, Equiv.symm, MulEquiv.symm, rfl
-- 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)
T : Submonoid P
Q : Type u_4
inst_3 : CommMonoid Q
k : N ≃* P
v : P
z : N
hz : (k : (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
rw :
  HMul.hMul (β := P) v ((k : (a : N) → P) ((f : (a : M) → N) (↑x.2 : M) : N) : P) =
    (k : (a : N) → P) (HMul.hMul (β := N) z ((f : (a : M) → N) (↑x.2 : M) : N))
rw₁ :
  HMul.hMul (β := P) v ((k : (a : N) → P) ((f : (a : M) → N) (↑x.2 : M) : N) : P) =
    HMul.hMul (α := P) (β := P) ((k : (a : N) → P) z : P) ((k : (a : N) → P) ((f : (a : M) → N) (↑x.2 : M) : N) : P)
rw₂ rw₃ :
  HMul.hMul (α := P) (β := P) ((k : (a : N) → P) z : P) ((k : (a : N) → P) ((f : (a : M) → N) (↑x.2 : M) : N) : P) =
    HMul.hMul (α := P) (β := P) ((k : (a : N) → P) z : P) ((k : (a : N) → P) ((f : (a : M) → N) (↑x.2 : M) : N) : P)
⊢ HMul.hMul (β := P) v ((k : (a : N) → P) ((f : (a : M) → N) (↑x.2 : M) : N) : P) =
    (k : (a : N) → P) ((f : (a : M) → N) x.1 : N)

Tactic:
rw [← hx, map_mul, ← hz]

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
k : N ≃* P
x : M
⊢ Eq.{u_3 + 1} (α := P) ((f.ofMulEquivOfLocalizations k : (a : M) → P) x : P)
    ((k : (a : N) → P) ((f : (a : M) → N) x : N) : P)

Tactic:
rfl

Premises used: rfl
-- 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
k : N ≃* P
⊢ (f.ofMulEquivOfLocalizations k).toMonoidHom = k.toMonoidHom.comp f.toMonoidHom

Tactic:
rfl

Premises used: rfl
-- 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
k : N ≃* P
x : M
⊢ Eq.{u_2 + 1} (α := N) ((k.symm : (a : P) → N) ((f.ofMulEquivOfLocalizations k : (a : M) → P) x : P) : N)
    ((f : (a : M) → N) x : N)

Tactic:
k.symm_apply_apply (f x)

Premises used: DFunLike.coe, MulEquiv.symm_apply_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
k : P ≃* N
x : M
⊢ Eq.{u_2 + 1} (α := N) ((k : (a : P) → N) ((f.ofMulEquivOfLocalizations k.symm : (a : M) → P) x : P) : N)
    ((f : (a : M) → N) x : N)

Tactic:
k.apply_symm_apply (f x)

Premises used: DFunLike.coe, MulEquiv.apply_symm_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
k : N ≃* P
x : M
y : P
⊢ (f.ofMulEquivOfLocalizations k : (a : M) → P) x = y ↔
    Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((k.symm : (a : P) → N) y : N)

Tactic:
k.toEquiv.eq_symm_apply.symm

Premises used: MulEquiv.toEquiv, Iff.symm, Equiv.eq_symm_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
k : S.LocalizationMap P
⊢ f.ofMulEquivOfLocalizations (f.mulEquivOfLocalizations k) = k

Tactic:
toMonoidHom_injective <| f.lift_comp k.map_units

Premises used: Submonoid.LocalizationMap.lift_comp, Submonoid.LocalizationMap.map_units, Submonoid.LocalizationMap.toMonoidHom_injective
-- 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
k : S.LocalizationMap P
x : M
⊢ Eq.{u_3 + 1} (α := P) ((f.ofMulEquivOfLocalizations (f.mulEquivOfLocalizations k) : (a : M) → P) x : P)
    ((k : (a : M) → P) x : P)

Tactic:
simp
-- 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
k : N ≃* P
⊢ f.mulEquivOfLocalizations (f.ofMulEquivOfLocalizations k) = k

Tactic:
DFunLike.ext _ _ fun x ↦ DFunLike.ext_iff.1 (f.lift_of_comp k.toMonoidHom) x

Premises used: Submonoid.LocalizationMap.lift_of_comp, DFunLike.ext, DFunLike.ext_iff, MulEquiv.toMonoidHom, Iff.mp
-- 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
k : N ≃* P
x : N
⊢ Eq.{u_3 + 1} (α := P) ((f.mulEquivOfLocalizations (f.ofMulEquivOfLocalizations k) : (a : N) → P) x : P)
    ((k : (a : N) → P) x : P)

Tactic:
simp
-- 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
h :
  ∀ (x : M),
    Eq.{u_2 + 1} (α := N) ((f.ofMulEquivOfLocalizations (MulEquiv.refl N) : (a : M) → N) x : N)
      ((f : (a : M) → N) x : N)
⊢ f.ofMulEquivOfLocalizations (MulEquiv.refl N) = f

Tactic:
ext
-- 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
x : M
⊢ Eq.{u_2 + 1} (α := N) ((f.ofMulEquivOfLocalizations (MulEquiv.refl N) : (a : M) → N) x : N) ((f : (a : M) → N) x : N)

Tactic:
rfl
-- 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
Q : Type u_4
inst_3 : CommMonoid Q
k : N ≃* P
j : P ≃* Q
h :
  ∀ (x : M),
    Eq.{u_4 + 1} (α := Q) (((f.ofMulEquivOfLocalizations (k.trans j)).toMonoidHom : (a : M) → Q) x : Q)
      ((j.toMonoidHom.comp (f.ofMulEquivOfLocalizations k).toMonoidHom : (a : M) → Q) x : Q)
⊢ (f.ofMulEquivOfLocalizations (k.trans j)).toMonoidHom = j.toMonoidHom.comp (f.ofMulEquivOfLocalizations k).toMonoidHom

Tactic:
ext
-- 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
Q : Type u_4
inst_3 : CommMonoid Q
k : N ≃* P
j : P ≃* Q
x : M
⊢ Eq.{u_4 + 1} (α := Q) (((f.ofMulEquivOfLocalizations (k.trans j)).toMonoidHom : (a : M) → Q) x : Q)
    ((j.toMonoidHom.comp (f.ofMulEquivOfLocalizations k).toMonoidHom : (a : M) → Q) x : Q)

Tactic:
rfl