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)
T : Submonoid P
Q : Type u_4
inst_3 : CommMonoid Q
k : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
z : N
x : M × ↥S
hx : HMul.hMul (β := N) z ((f : (a : M) → N) (↑x.2 : M) : N) = (f : (a : M) → N) x.1
v : P
hv : (k : (a : P) → M) v = x.1
w : P
hw : (k : (a : P) → M) w = (↑x.2 : M)
simp_rw : HMul.hMul (β := N) z ((f.toMonoidHom : (a : M) → N) (↑x.2 : M) : N) = (f.toMonoidHom : (a : M) → N) x.1
⊢ HMul.hMul (β := N) z
      ((f.toMonoidHom.comp k.toMonoidHom : (a : P) → N) (↑(v, Subtype.mk (p := fun (x : P) ↦ x ∈ T) w ⋯).2 : P) : N) =
    (f.toMonoidHom.comp k.toMonoidHom : (a : P) → N) (v, Subtype.mk (p := fun (x : P) ↦ x ∈ T) w ⋯).1

Tactic:
simp_rw [MonoidHom.comp_apply, MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_coe, hv, hw]

Premises used: MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_coe, MonoidHom.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
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 : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
z : N
x : M × ↥S
hx : HMul.hMul (β := N) z ((f : (a : M) → N) (↑x.2 : M) : N) = (f : (a : M) → N) x.1
v : P
hv : (k : (a : P) → M) v = x.1
w : P
hw : (k : (a : P) → M) w = (↑x.2 : M)
dsimp : HMul.hMul (β := N) z ((f : (a : M) → N) (↑x.2 : M) : N) = (f : (a : M) → N) x.1
⊢ HMul.hMul (β := N) z ((f.toMonoidHom : (a : M) → N) (↑x.2 : M) : N) = (f.toMonoidHom : (a : M) → N) x.1

Tactic:
dsimp
-- 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 : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
z : N
x : M × ↥S
hx : HMul.hMul (β := N) z ((f : (a : M) → N) (↑x.2 : M) : N) = (f : (a : M) → N) x.1
v : P
hv : (k : (a : P) → M) v = x.1
w : P
hw : (k : (a : P) → M) w = (↑x.2 : M)
rw rw₁ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x.1 : N) ((f : (a : M) → N) x.1 : N)
⊢ HMul.hMul (β := N) z ((f : (a : M) → N) (↑x.2 : M) : N) = (f : (a : M) → N) x.1

Tactic:
rw [hx]
-- 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 : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
x y : P
rw :
  (∃ (c : ↥S),
      HMul.hMul (β := M) (↑c : M) ((k : (a : P) → M) x : M) = HMul.hMul (β := M) (↑c : M) ((k : (a : P) → M) y : M)) →
    ∃ (c : ↥T), (↑c : P) * x = (↑c : P) * y
⊢ Eq.{u_2 + 1} (α := N) ((f.toMonoidHom.comp k.toMonoidHom : (a : P) → N) x : N)
      ((f.toMonoidHom.comp k.toMonoidHom : (a : P) → N) y : N) →
    ∃ (c : ↥T), (↑c : P) * x = (↑c : P) * y

Tactic:
rw [MonoidHom.comp_apply, MonoidHom.comp_apply, MulEquiv.toMonoidHom_eq_coe,
        MonoidHom.coe_coe, toMonoidHom_apply, toMonoidHom_apply, f.eq_iff_exists]

Premises used: MulEquiv.toMonoidHom_eq_coe, Submonoid.LocalizationMap.eq_iff_exists, MonoidHom.coe_coe, Submonoid.LocalizationMap.toMonoidHom_apply, MonoidHom.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
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 : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
x y : P
c : ↥S
hc : HMul.hMul (β := M) (↑c : M) ((k : (a : P) → M) x : M) = HMul.hMul (β := M) (↑c : M) ((k : (a : P) → M) y : M)
let : ∀ (d : P) (hd : (k : (a : P) → M) d = (↑c : M)), ∃ (c : ↥T), (↑c : P) * x = (↑c : P) * y
⊢ ∃ (c : ↥T), (↑c : P) * x = (↑c : P) * y

Tactic:
let ⟨d, hd⟩ := k.surjective c
-- 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 : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
x y : P
c : ↥S
hc : HMul.hMul (β := M) (↑c : M) ((k : (a : P) → M) x : M) = HMul.hMul (β := M) (↑c : M) ((k : (a : P) → M) y : M)
d : P
hd : (k : (a : P) → M) d = (↑c : M)
⊢ ∃ (c : ↥T), (↑c : P) * x = (↑c : P) * y

Tactic:
⟨⟨d, H' ▸ show k d ∈ S from hd.symm ▸ c.2⟩, ?_⟩

Premises used: Eq.rec, Subtype.mk, Exists.intro, Eq.symm, Subtype.property
-- 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 : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
x y : P
c : ↥S
hc : HMul.hMul (β := M) (↑c : M) ((k : (a : P) → M) x : M) = HMul.hMul (β := M) (↑c : M) ((k : (a : P) → M) y : M)
d : P
hd : (k : (a : P) → M) d = (↑c : M)
refine : (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ T) d ⋯) : P) * x = (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ T) d ⋯) : P) * y
⊢ ∃ (c : ↥T), (↑c : P) * x = (↑c : P) * y

Tactic:
refine ⟨⟨d, H' ▸ show k d ∈ S from hd.symm ▸ c.2⟩, ?_⟩
-- 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 : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
x y : P
c : ↥S
hc : HMul.hMul (β := M) (↑c : M) ((k : (a : P) → M) x : M) = HMul.hMul (β := M) (↑c : M) ((k : (a : P) → M) y : M)
d : P
hd : (k : (a : P) → M) d = (↑c : M)
rw :
  ∀ (hc : Eq.{u_1 + 1} (α := M) ((k : (a : P) → M) (d * x) : M) ((k : (a : P) → M) (d * y) : M))
    (hd : (k : (a : P) → M) d = (↑c : M)),
    (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ T) d ⋯) : P) * x = (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ T) d ⋯) : P) * y
⊢ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ T) d ⋯) : P) * x = (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ T) d ⋯) : P) * y

Tactic:
rw [← hd, ← map_mul k, ← map_mul k] at hc

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
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 : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
x y : P
c : ↥S
d : P
hc : Eq.{u_1 + 1} (α := M) ((k : (a : P) → M) (d * x) : M) ((k : (a : P) → M) (d * y) : M)
hd : (k : (a : P) → M) d = (↑c : M)
⊢ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ T) d ⋯) : P) * x = (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ T) d ⋯) : P) * y

Tactic:
k.injective hc

Premises used: MulEquiv.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
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 : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
x y : P
c : ↥S
d : P
hc : Eq.{u_1 + 1} (α := M) ((k : (a : P) → M) (d * x) : M) ((k : (a : P) → M) (d * y) : M)
hd : (k : (a : P) → M) d = (↑c : M)
⊢ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ T) d ⋯) : P) * x = (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ T) d ⋯) : P) * y

Tactic:
exact k.injective hc

Premises used: MulEquiv.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
T : Submonoid P
k : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
x : P
⊢ Eq.{u_2 + 1} (α := N) ((f.ofMulEquivOfDom H : (a : P) → N) x : N) ((f : (a : M) → N) ((k : (a : P) → M) x : M) : 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
T : Submonoid P
k : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
⊢ (f.ofMulEquivOfDom H).toMonoidHom = f.toMonoidHom.comp k.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
T : Submonoid P
k : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
x : M
⊢ Eq.{u_2 + 1} (α := N) ((f.ofMulEquivOfDom H : (a : P) → N) ((k.symm : (a : M) → P) x : P) : N)
    ((f : (a : M) → N) x : N)

Tactic:
congr_arg f <| k.apply_symm_apply x

Premises used: congr_arg, 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
T : Submonoid P
k : M ≃* P
H : Submonoid.map k.symm.toMonoidHom T = S
x : M
⊢ Eq.{u_2 + 1} (α := N) ((f.ofMulEquivOfDom H : (a : P) → N) ((k : (a : M) → P) x : P) : N) ((f : (a : M) → N) x : N)

Tactic:
congr_arg f <| k.symm_apply_apply x

Premises used: congr_arg, 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
f : S.LocalizationMap N
h :
  ∀ (x : M),
    Eq.{u_2 + 1} (α := N) ((f.ofMulEquivOfDom (k := MulEquiv.refl M) ⋯ : (a : M) → N) x : N) ((f : (a : M) → N) x : N)
⊢ f.ofMulEquivOfDom (k := MulEquiv.refl M) ⋯ = 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.ofMulEquivOfDom (k := MulEquiv.refl M) ⋯ : (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
T : Submonoid P
Q : Type u_4
inst_3 : CommMonoid Q
k : T.LocalizationMap Q
j : M ≃* P
H : Submonoid.map j.toMonoidHom S = T
x : N
⊢ Eq.{u_4 + 1} (α := Q) ((f.mulEquivOfMulEquiv k H : (a : N) → Q) x : Q)
    ((f.map (g := j.toMonoidHom) ⋯ k : (a : N) → Q) x : Q)

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
T : Submonoid P
Q : Type u_4
inst_3 : CommMonoid Q
k : T.LocalizationMap Q
j : M ≃* P
H : Submonoid.map j.toMonoidHom S = T
⊢ (f.mulEquivOfMulEquiv k H).toMonoidHom = f.map (g := j.toMonoidHom) ⋯ k

Tactic:
rfl

Premises used: Submonoid.LocalizationMap.lift, MulEquiv.toMonoidHom, Submonoid.LocalizationMap.map, 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
T : Submonoid P
Q : Type u_4
inst_3 : CommMonoid Q
k : T.LocalizationMap Q
j : M ≃* P
H : Submonoid.map j.toMonoidHom S = T
x : M
⊢ Eq.{u_4 + 1} (α := Q) ((f.mulEquivOfMulEquiv k H : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
    ((k : (a : P) → Q) ((j : (a : M) → P) x : P) : Q)

Tactic:
f.map_eq (fun y : S ↦ H ▸ Set.mem_image_of_mem j y.2) _

Premises used: Submonoid.LocalizationMap.map_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
T : Submonoid P
Q : Type u_4
inst_3 : CommMonoid Q
k : T.LocalizationMap Q
j : M ≃* P
H : Submonoid.map j.toMonoidHom S = T
x : M
y : ↥S
⊢ (f.mulEquivOfMulEquiv k H : (a : N) → Q) (f.mk' x y) =
    k.mk' ((j : (a : M) → P) x) (Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((j : (a : M) → P) (↑y : M)) ⋯)

Tactic:
f.map_mk' (fun y : S ↦ H ▸ Set.mem_image_of_mem j y.2) _ _

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
T : Submonoid P
Q : Type u_4
inst_3 : CommMonoid Q
k : T.LocalizationMap Q
j : M ≃* P
H : Submonoid.map j.toMonoidHom S = T
x : M
⊢ Eq.{u_4 + 1} (α := Q) ((f.ofMulEquivOfLocalizations (f.mulEquivOfMulEquiv k H) : (a : M) → Q) x : Q)
    ((k : (a : P) → Q) ((j : (a : M) → P) x : P) : Q)

Tactic:
Submonoid.LocalizationMap.ext_iff.1 (f.mulEquivOfLocalizations_right_inv (k.ofMulEquivOfDom H)) x

Premises used: Submonoid.LocalizationMap.ofMulEquivOfDom, Submonoid.LocalizationMap.ext_iff, Iff.mp, Submonoid.LocalizationMap.mulEquivOfLocalizations_right_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
T : Submonoid P
Q : Type u_4
inst_3 : CommMonoid Q
k : T.LocalizationMap Q
j : M ≃* P
H : Submonoid.map j.toMonoidHom S = T
⊢ (f.ofMulEquivOfLocalizations (f.mulEquivOfMulEquiv k H)).toMonoidHom = k.toMonoidHom.comp j.toMonoidHom

Tactic:
MonoidHom.ext <| f.of_mulEquivOfMulEquiv_apply H

Premises used: MonoidHom.ext, Submonoid.LocalizationMap.of_mulEquivOfMulEquiv_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
f : S.LocalizationMap N
x : Localization S
⊢ Eq.{u_2 + 1} (α := N) ((mulEquivOfQuotient f : (a : Localization S) → N) x : N)
    (((monoidOf S).lift ⋯ : (a : Localization S) → 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
f : S.LocalizationMap N
x : M
y : ↥S
⊢ (mulEquivOfQuotient f : (a : Localization S) → N) ((monoidOf S).mk' x y) = f.mk' x y

Tactic:
(monoidOf S).lift_mk' _ _ _

Premises used: Submonoid.LocalizationMap.mk', Submonoid.LocalizationMap.lift_mk', Localization.monoidOf
-- 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
y : ↥S
rw : (mulEquivOfQuotient f : (a : Localization S) → N) ((monoidOf S).mk' x y) = f.mk' x y
⊢ (mulEquivOfQuotient f : (a : Localization S) → N) (mk x y) = f.mk' x y

Tactic:
rw [mk_eq_monoidOf_mk'_apply]

Premises used: Localization.mk_eq_monoidOf_mk'_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
f : S.LocalizationMap N
x : M
y : ↥S
⊢ (mulEquivOfQuotient f : (a : Localization S) → N) ((monoidOf S).mk' x y) = f.mk' x y

Tactic:
mulEquivOfQuotient_mk' _ _

Premises used: Localization.mulEquivOfQuotient_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
f : S.LocalizationMap N
x : M
y : ↥S
⊢ (mulEquivOfQuotient f : (a : Localization S) → N) ((monoidOf S).mk' x y) = f.mk' x y

Tactic:
exact mulEquivOfQuotient_mk' _ _

Premises used: Localization.mulEquivOfQuotient_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
f : S.LocalizationMap N
x : M
⊢ Eq.{u_2 + 1} (α := N)
    ((mulEquivOfQuotient f : (a : Localization S) → N) ((monoidOf S : (a : M) → Localization S) x : Localization S) : N)
    ((f : (a : M) → N) x : N)

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
x : M
y : ↥S
⊢ ((mulEquivOfQuotient f).symm : (a : N) → Localization S) (f.mk' x y) = (monoidOf S).mk' x y

Tactic:
f.lift_mk' (monoidOf S).map_units _ _

Premises used: Submonoid.LocalizationMap.mk', Submonoid.LocalizationMap.lift_mk', Submonoid.LocalizationMap.map_units, OreLocalization.liftExpand, Localization.monoidOf
-- 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
y : ↥S
rw : ((mulEquivOfQuotient f).symm : (a : N) → Localization S) (f.mk' x y) = (monoidOf S).mk' x y
⊢ ((mulEquivOfQuotient f).symm : (a : N) → Localization S) (f.mk' x y) = mk x y

Tactic:
rw [mk_eq_monoidOf_mk'_apply]

Premises used: Localization.mk_eq_monoidOf_mk'_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
f : S.LocalizationMap N
x : M
y : ↥S
⊢ ((mulEquivOfQuotient f).symm : (a : N) → Localization S) (f.mk' x y) = (monoidOf S).mk' x y

Tactic:
mulEquivOfQuotient_symm_mk' _ _

Premises used: Localization.mulEquivOfQuotient_symm_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
f : S.LocalizationMap N
x : M
y : ↥S
⊢ ((mulEquivOfQuotient f).symm : (a : N) → Localization S) (f.mk' x y) = (monoidOf S).mk' x y

Tactic:
exact mulEquivOfQuotient_symm_mk' _ _

Premises used: Localization.mulEquivOfQuotient_symm_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
f : S.LocalizationMap N
x : M
⊢ Eq.{u_1 + 1} (α := Localization S)
    (((mulEquivOfQuotient f).symm : (a : N) → Localization S) ((f : (a : M) → N) x) : Localization S)
    ((monoidOf S : (a : M) → Localization S) x : Localization S)

Tactic:
f.lift_eq (monoidOf S).map_units _

Premises used: Submonoid.LocalizationMap.lift_eq, Submonoid.LocalizationMap.map_units, OreLocalization.liftExpand, Localization.monoidOf
-- Module: Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
Goal:
M : Type u_1
inst : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoidWithZero N
f : S.LocalizationMap N
h : 0 ∈ S
a b : N
rw : ∃ (c : ↥S), (↑c : M) * ((↑(f.sec b).2 : M) * (f.sec a).1) = (↑c : M) * ((↑(f.sec a).2 : M) * (f.sec b).1)
⊢ a = b

Tactic:
rw [← f.mk'_sec a, ← f.mk'_sec b, f.eq]

Premises used: Submonoid.LocalizationMap.mk'_sec, Submonoid.LocalizationMap.eq
-- Module: Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
Goal:
M : Type u_1
inst : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoidWithZero N
f : S.LocalizationMap N
h : 0 ∈ S
a b : N
⊢ (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ S) 0 h) : M) * ((↑(f.sec b).2 : M) * (f.sec a).1) =
    (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ S) 0 h) : M) * ((↑(f.sec a).2 : M) * (f.sec b).1)

Tactic:
simp only [zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
Goal:
M : Type u_1
inst : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoidWithZero N
f : S.LocalizationMap N
h : 0 ∈ S
a b : N
⊢ ∃ (c : ↥S), (↑c : M) * ((↑(f.sec b).2 : M) * (f.sec a).1) = (↑c : M) * ((↑(f.sec a).2 : M) * (f.sec b).1)

Tactic:
exact ⟨⟨0, h⟩, by simp only [zero_mul]⟩
-- Module: Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
Goal:
M : Type u_1
inst : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoidWithZero N
f : S.LocalizationMap N
h : Subsingleton N
c : ↥S
eq : (↑c : M) * 0 = (↑c : M) * 1
⊢ 0 = (↑c : M)

Tactic:
rw [mul_zero, mul_one] at eq

Premises used: MulZeroClass.mul_zero, mul_one
-- Module: Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
Goal:
M : Type u_1
inst : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoidWithZero N
f : S.LocalizationMap N
h : Subsingleton N
c : ↥S
eq : 0 = (↑c : M)
⊢ 0 ∈ S

Tactic:
eq ▸ c.2

Premises used: Eq.rec, Eq.symm, Subtype.property
-- Module: Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
Goal:
M : Type u_1
inst : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoidWithZero N
f : S.LocalizationMap N
h : Subsingleton N
c : ↥S
eq : 0 = (↑c : M)
⊢ 0 ∈ S

Tactic:
exact eq ▸ c.2
-- Module: Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
Goal:
M : Type u_1
inst : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoidWithZero N
f : S.LocalizationMap N
h : 0 ∉ S
rwa : ¬Subsingleton N
rwa₁ rwa₂ rwa₃ rwa₄ : 0 ∉ S
⊢ Nontrivial N

Tactic:
rwa [← not_subsingleton_iff_nontrivial, f.subsingleton_iff]

Premises used: Submonoid.LocalizationMap.subsingleton_iff, not_subsingleton_iff_nontrivial
-- Module: Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
Goal:
M : Type u_1
inst : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoidWithZero N
f : S.LocalizationMap N
have :
  ∀ (ms : M × ↥S)
    (eq : HMul.hMul (α := N) (β := N) (0 : N) ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) ms.1),
    Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) 0 : N) (0 : N)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) 0 : N) (0 : N)

Tactic:
have ⟨ms, eq⟩ := f.surj 0
-- Module: Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
Goal:
M : Type u_1
inst : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoidWithZero N
f : S.LocalizationMap N
ms : M × ↥S
eq : HMul.hMul (α := N) (β := N) (0 : N) ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) ms.1
rw : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (0 * ms.1) : N) (0 : N)
rw₁ : M
rw₂ : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) 0 : N) ((f : (a : M) → N) ms.1 : N) = 0
y : M
rw₃ :
  HMul.hMul (α := N) ((f : (a : M) → N) 0 : N)
      (HMul.hMul (α := N) (β := N) (0 : N) ((f : (a : M) → N) (↑ms.2 : M) : N)) =
    0
rw₄ : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) 0 : N) (0 : N) = 0
rw₅ rw₆ : Eq.{u_2 + 1} (α := N) 0 0
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) 0 : N) (0 : N)

Tactic:
rw [← zero_mul, map_mul, ← eq, zero_mul, mul_zero]

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero, map_mul
-- Module: Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
Goal:
M : Type u_1
inst : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoidWithZero N
F : Type u_4
inst_2 : FunLike F M N
inst_3 : MulHomClass F M N
f : F
hf : IsLocalizationMap.{u_1, u_2} (N := N) S (⇑f : (a : M) → N)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) 0 : N) (0 : N)

Tactic:
LocalizationMap.map_zero ⟨MulHomClass.toMulHom f, hf⟩

Premises used: Submonoid.LocalizationMap.mk, MulHomClass.toMulHom, Submonoid.LocalizationMap.map_zero
-- Module: Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
Goal:
M : Type u_1
inst : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoidWithZero N
P : Type u_3
inst_2 : CommMonoidWithZero P
f : S.LocalizationMap N
have :
  ∀ (ms : M × ↥S)
    (eq : HMul.hMul (α := N) (β := N) (0 : N) ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) ms.1),
    Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) 0 : N) (0 : N)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) 0 : N) (0 : N)

Tactic:
have ⟨ms, eq⟩ := f.surj 0