awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
x : ↥S
⊢ mk 0 x = 0

Tactic:
OreLocalization.zero_oreDiv' _

Premises used: Localization.mk, OreLocalization.zero_oreDiv'
-- 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
x : Localization S
y : M × ↥S
⊢ 0 * mk y.1 y.2 = 0

Tactic:
simp only [← Localization.mk_zero y.2, mk_mul, mk_eq_mk_iff, mul_zero, zero_mul, r_of_eq]

Premises used: MulZeroClass.zero_mul, Localization.r_of_eq, MulZeroClass.mul_zero, Localization.mk_mul, Prod.snd, Localization.mk_zero, Localization.mk_eq_mk_iff
-- 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
x : Localization S
y : M × ↥S
⊢ mk y.1 y.2 * 0 = 0

Tactic:
simp only [← Localization.mk_zero y.2, mk_mul, mk_eq_mk_iff, mul_zero, r_of_eq]

Premises used: Localization.r_of_eq, MulZeroClass.mul_zero, Localization.mk_mul, Prod.snd, Localization.mk_zero, Localization.mk_eq_mk_iff
-- Module: Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
Goal:
M : Type u_1
inst : CommMonoidWithZero M
S : Submonoid M
p : Type u_4
f : M → ↥S → p
H : ∀ {a c : M} {b d : ↥S}, (r S : (a : M × ↥S) → M × ↥S → Prop) (a, b) (c, d) → f a b = f c d
rw : liftOn (mk 0 1) f @H = f 0 1
rw₁ rw₂ : f 0 1 = f 0 1
⊢ liftOn 0 f @H = f 0 1

Tactic:
rw [← mk_zero 1, liftOn_mk]

Premises used: Localization.liftOn_mk, OfNat.ofNat, Localization.mk_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
f : S.LocalizationMap N
rw : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑(f.sec 0).2 : M) : N) (0 : N) = 0
rw₁ rw₂ : Eq.{u_2 + 1} (α := N) 0 0
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (f.sec 0).1 : N) (0 : N)

Tactic:
rw [LocalizationMap.sec_spec', mul_zero]

Premises used: MulZeroClass.mul_zero, Submonoid.LocalizationMap.sec_spec'
-- 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
g : M →*₀ P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
dsimp : Eq.{u_3 + 1} (α := P) ((f.lift (g := (↑g : M →* P)) hg : (a : N) → P) 0 : P) (0 : P)
⊢ Eq.{u_3 + 1} (α := P) (OneHom.toFun (↑(f.lift (g := (↑g : M →* P)) hg) : OneHom N P) 0) 0

Tactic:
dsimp only [OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe]

Premises used: MonoidHom.toOneHom_coe, OneHom.toFun_eq_coe
-- 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
g : M →*₀ P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
rw : ((↑g : M →* P) : (a : M) → P) (f.sec 0).1 = (↑(↑g : M →* P) : OneHom M P).toFun 0
⊢ Eq.{u_3 + 1} (α := P) ((f.lift (g := (↑g : M →* P)) hg : (a : N) → P) 0 : P) (0 : P)

Tactic:
rw [LocalizationMap.lift_spec f hg 0 0, mul_zero, ← map_zero g, ← g.toMonoidHom_coe]

Premises used: Submonoid.LocalizationMap.lift_spec, map_zero, MulZeroClass.mul_zero, MonoidWithZeroHom.toMonoidHom_coe, OfNat.ofNat
-- 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
g : M →*₀ P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
⊢ ((↑g : M →* P) : (a : M) → P) (f.sec 0).1 = (↑(↑g : M →* P) : OneHom M P).toFun 0

Tactic:
f.eq_of_eq hg ?_

Premises used: Submonoid.LocalizationMap.eq_of_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
P : Type u_3
inst_2 : CommMonoidWithZero P
f : S.LocalizationMap N
g : M →*₀ P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
refine : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (f.sec 0).1 : N) ((f : (a : M) → N) 0 : N)
⊢ ((↑g : M →* P) : (a : M) → P) (f.sec 0).1 = (↑(↑g : M →* P) : OneHom M P).toFun 0

Tactic:
refine f.eq_of_eq hg ?_

Premises used: Submonoid.LocalizationMap.eq_of_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
P : Type u_3
inst_2 : CommMonoidWithZero P
f : S.LocalizationMap N
g : M →*₀ P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
rw : Eq.{u_2 + 1} (α := N) (0 : N) ((f : (a : M) → N) 0 : N)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (f.sec 0).1 : N) ((f : (a : M) → N) 0 : N)

Tactic:
rw [LocalizationMap.sec_zero_fst]

Premises used: Submonoid.LocalizationMap.sec_zero_fst
-- 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
g : M →*₀ P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
⊢ Eq.{u_2 + 1} (α := N) (0 : N) ((f : (a : M) → N) 0 : N)

Tactic:
(map_zero f).symm

Premises used: map_zero, Eq.symm
-- 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
g : M →*₀ P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
⊢ Eq.{u_2 + 1} (α := N) (0 : N) ((f : (a : M) → N) 0 : N)

Tactic:
exact (map_zero f).symm

Premises used: map_zero, Eq.symm
-- 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
g : M →*₀ P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
⊢ Eq (α := (a : N) → P) (⇑(f.lift₀ g hg) : (a : N) → P) (⇑(f.lift (g := (↑g : M →* P)) hg) : (a : N) → P)

Tactic:
rfl

Premises used: rfl
-- 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
g : M →*₀ P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
x : N
⊢ (f.lift₀ g hg : (a : N) → P) x =
    HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec x).1 : P)
      ((↑((IsUnit.liftRight ((↑g : M →* P).restrict S) hg : (a : ↥S) → Pˣ) (f.sec x).2)⁻¹ : P) : P)

Tactic:
rfl

Premises used: rfl
-- 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
inst_2 : IsCancelMulZero M
simp_rw : ∀ {a : N}, a ≠ 0 → IsRightRegular a
⊢ IsCancelMulZero N

Tactic:
simp_rw [isCancelMulZero_iff_forall_isRegular, Commute.isRegular_iff (Commute.all _),
    ← Commute.isRightRegular_iff (Commute.all _)]

Premises used: Commute.isRightRegular_iff, Commute.isRegular_iff, Commute.all, isCancelMulZero_iff_forall_isRegular
-- 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
inst_2 : IsCancelMulZero M
n : N
hn : n ≠ 0
have :
  ∀ (ms : M × ↥S) (eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) ms.1),
    IsRightRegular n
⊢ IsRightRegular n

Tactic:
have ⟨ms, eq⟩ := f.surj n
-- 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
inst_2 : IsCancelMulZero M
n : N
hn : n ≠ 0
ms : M × ↥S
eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) ms.1
refine : ms.1 ≠ 0
⊢ IsRightRegular n

Tactic:
refine (eq ▸ f.map_isRegular (isCancelMulZero_iff_forall_isRegular.mp ‹_› ?_)).2.of_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
inst_2 : IsCancelMulZero M
n : N
hn : n ≠ 0
ms : M × ↥S
eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) ms.1
⊢ ms.1 ≠ 0

Tactic:
fun h ↦ hn ?_

Premises used: Not
-- 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
inst_2 : IsCancelMulZero M
n : N
hn : n ≠ 0
ms : M × ↥S
eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) ms.1
refine : ∀ (h : ms.1 = 0), n = 0
⊢ ms.1 ≠ 0

Tactic:
refine fun h ↦ hn ?_
-- 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
inst_2 : IsCancelMulZero M
n : N
hn : n ≠ 0
ms : M × ↥S
eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) ms.1
h : ms.1 = 0
rwa : ∀ (eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) 0) (h : ms.1 = 0), n = 0
rwa₁ : ∀ (eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = 0) (h : ms.1 = 0), n = 0
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (eq : n = 0) (h : ms.1 = 0), n = 0
⊢ n = 0

Tactic:
rwa [h, map_zero, (f.map_units _).mul_left_eq_zero] at eq

Premises used: IsUnit.mul_left_eq_zero, map_zero, Submonoid.LocalizationMap.map_units
-- 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
m : M
simp_rw : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) m : N) ((f : (a : M) → N) 0 : N) ↔ ∃ (s : ↥S), (↑s : M) * m = 0
simp_rw₁ : (∃ (c : ↥S), (↑c : M) * m = (↑c : M) * 0) ↔ ∃ (s : ↥S), (↑s : M) * m = 0
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) m : N) (0 : N) ↔ ∃ (s : ↥S), (↑s : M) * m = 0

Tactic:
simp_rw [← f.map_zero, eq_iff_exists, mul_zero]

Premises used: Submonoid.LocalizationMap.eq_iff_exists, MulZeroClass.mul_zero, 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
f : S.LocalizationMap N
m : M
s : ↥S
rw :
  HMul.hMul (β := N) (f.mk' m s) ((f : (a : M) → N) (↑s : M) : N) =
      HMul.hMul (α := N) (β := N) (0 : N) ((f : (a : M) → N) (↑s : M) : N) ↔
    ∃ (s : ↥S), (↑s : M) * m = 0
rw₁ :
  (f : (a : M) → N) m = HMul.hMul (α := N) (β := N) (0 : N) ((f : (a : M) → N) (↑s : M) : N) ↔
    ∃ (s : ↥S), (↑s : M) * m = 0
rw₂ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) m : N) (0 : N) ↔ ∃ (s : ↥S), (↑s : M) * m = 0
rw₃ rw₄ : (∃ (s : ↥S), (↑s : M) * m = 0) ↔ ∃ (s : ↥S), (↑s : M) * m = 0
⊢ f.mk' m s = 0 ↔ ∃ (s : ↥S), (↑s : M) * m = 0

Tactic:
rw [← (f.map_units s).mul_left_inj, mk'_spec, zero_mul, map_eq_zero_iff]

Premises used: MulZeroClass.zero_mul, Submonoid.LocalizationMap.map_eq_zero_iff, IsUnit.mul_left_inj, Submonoid.LocalizationMap.map_units, Submonoid.LocalizationMap.mk'_spec
-- 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
s : ↥S
rw : 0 = f.mk' 0 s
rw₁ : HMul.hMul (α := N) (β := N) (0 : N) ((f : (a : M) → N) (↑s : M) : N) = (f : (a : M) → N) 0
rw₂ : Eq.{u_2 + 1} (α := N) (0 : N) ((f : (a : M) → N) 0 : N)
rw₃ rw₄ : Eq.{u_2 + 1} (α := N) 0 0
⊢ f.mk' 0 s = 0

Tactic:
rw [eq_comm, eq_mk'_iff_mul_eq, zero_mul, f.map_zero]

Premises used: MulZeroClass.zero_mul, eq_comm, Submonoid.LocalizationMap.map_zero, Submonoid.LocalizationMap.eq_mk'_iff_mul_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
⊢ LE.le (α := Submonoid M) (nonZeroDivisors M) (comap f (nonZeroDivisors N))

Tactic:
fun m hm ↦ nonZeroDivisorsRight_eq_nonZeroDivisors (M₀ := N) ▸ fun n h0 ↦ ?_

Premises used: Eq.rec, nonZeroDivisorsRight_eq_nonZeroDivisors
-- 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
refine :
  ∀ (m : M) (hm : Membership.mem (γ := Submonoid M) (nonZeroDivisors M) m) (n : N)
    (h0 : HMul.hMul (β := N) n ((f : (a : M) → N) m : N) = 0), n = 0
⊢ LE.le (α := Submonoid M) (nonZeroDivisors M) (comap f (nonZeroDivisors N))

Tactic:
refine fun m hm ↦ nonZeroDivisorsRight_eq_nonZeroDivisors (M₀ := N) ▸ fun n h0 ↦ ?_
-- 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
m : M
hm : Membership.mem (γ := Submonoid M) (nonZeroDivisors M) m
n : N
h0 : HMul.hMul (β := N) n ((f : (a : M) → N) m : N) = 0
have : ∀ (ms : M × ↥S) (eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) ms.1), n = 0
⊢ n = 0

Tactic:
have ⟨ms, eq⟩ := f.surj n
-- 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
m : M
hm : Membership.mem (γ := Submonoid M) (nonZeroDivisors M) m
n : N
h0 : HMul.hMul (β := N) n ((f : (a : M) → N) m : N) = 0
ms : M × ↥S
eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) ms.1
⊢ ∃ (s : ↥S), (↑s : M) * (ms.1 * m) = 0

Tactic:
rw [← (f.map_units ms.2).mul_left_eq_zero, mul_right_comm, eq, ← map_mul, map_eq_zero_iff] at h0

Premises used: IsUnit.mul_left_eq_zero, Submonoid.LocalizationMap.map_eq_zero_iff, map_mul, mul_right_comm, Submonoid.LocalizationMap.map_units, Prod.snd
-- 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
m : M
hm : Membership.mem (γ := Submonoid M) (nonZeroDivisors M) m
n : N
h0 : HMul.hMul (β := N) n ((f : (a : M) → N) m : N) = 0
ms : M × ↥S
eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) ms.1
h0₁ : ∃ (s : ↥S), (↑s : M) * (ms.1 * m) = 0
⊢ HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) ms.1

Tactic:
rw [← (f.map_units ms.2).mul_left_eq_zero, mul_right_comm, eq, ← map_mul, map_eq_zero_iff] at h0

Premises used: IsUnit.mul_left_eq_zero, Submonoid.LocalizationMap.map_eq_zero_iff, map_mul, mul_right_comm, Submonoid.LocalizationMap.map_units, Prod.snd
-- 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
m : M
hm : Membership.mem (γ := Submonoid M) (nonZeroDivisors M) m
n : N
ms : M × ↥S
h0 : ∃ (s : ↥S), (↑s : M) * (ms.1 * m) = 0
eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) ms.1
⊢ ∃ (s : ↥S), (↑s : M) * ms.1 = 0

Tactic:
simp_rw [← mul_assoc, mul_right_mem_nonZeroDivisorsRight_eq_zero_iff hm.2] at h0

Premises used: mul_assoc, mul_right_mem_nonZeroDivisorsRight_eq_zero_iff, And.right
-- 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
m : M
hm : Membership.mem (γ := Submonoid M) (nonZeroDivisors M) m
n : N
ms : M × ↥S
eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) ms.1
h0 : ∃ (s : ↥S), (↑s : M) * ms.1 = 0
rwa : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = 0
rwa₁ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) ms.1 : N) (0 : N)
rwa₂ rwa₃ rwa₄ rwa₅ : ∃ (s : ↥S), (↑s : M) * ms.1 = 0
⊢ n = 0

Tactic:
rwa [← (f.map_units ms.2).mul_left_eq_zero, eq, map_eq_zero_iff]

Premises used: IsUnit.mul_left_eq_zero, Submonoid.LocalizationMap.map_eq_zero_iff, Submonoid.LocalizationMap.map_units, Prod.snd
-- 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
⊢ LE.le (α := Submonoid N) (Submonoid.map f (nonZeroDivisors M)) (nonZeroDivisors N)

Tactic:
map_le_iff_le_comap.mpr f.nonZeroDivisors_le_comap

Premises used: Iff.mpr, Submonoid.map_le_iff_le_comap, Submonoid.LocalizationMap.nonZeroDivisors_le_comap
-- 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
inst_2 : NoZeroDivisors M
⊢ NoZeroDivisors N

Tactic:
noZeroDivisors_iff_forall_mem_nonZeroDivisors.mpr fun n hn ↦ ?_

Premises used: Iff.mpr, noZeroDivisors_iff_forall_mem_nonZeroDivisors
-- 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
inst_2 : NoZeroDivisors M
refine : ∀ (n : N) (hn : n ≠ 0), Membership.mem (γ := Submonoid N) (nonZeroDivisors N) n
⊢ NoZeroDivisors N

Tactic:
refine noZeroDivisors_iff_forall_mem_nonZeroDivisors.mpr fun n hn ↦ ?_

Premises used: Iff.mpr, noZeroDivisors_iff_forall_mem_nonZeroDivisors
-- 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
inst_2 : NoZeroDivisors M
n : N
hn : n ≠ 0
have :
  ∀ (ms : M × ↥S) (eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) ms.1),
    Membership.mem (γ := Submonoid N) (nonZeroDivisors N) n
⊢ Membership.mem (γ := Submonoid N) (nonZeroDivisors N) n

Tactic:
have ⟨ms, eq⟩ := f.surj n
-- 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
inst_2 : NoZeroDivisors M
n : N
hn : n ≠ 0
ms : M × ↥S
eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) ms.1
h : ms.1 = 0
rwa : ∀ (eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) 0) (h : ms.1 = 0), n = 0
rwa₁ : ∀ (eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = 0) (h : ms.1 = 0), n = 0
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (eq : n = 0) (h : ms.1 = 0), n = 0
⊢ n = 0

Tactic:
rwa [h, f.map_zero, (f.map_units _).mul_left_eq_zero] at eq

Premises used: IsUnit.mul_left_eq_zero, Submonoid.LocalizationMap.map_zero, Submonoid.LocalizationMap.map_units
-- 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
inst_2 : NoZeroDivisors M
n : N
hn : n ≠ 0
ms : M × ↥S
eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) ms.1
⊢ ms.1 ≠ 0

Tactic:
have hs : ms.1 ≠ 0 := fun h ↦ hn (by rwa [h, f.map_zero, (f.map_units _).mul_left_eq_zero] at 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
inst_2 : NoZeroDivisors M
n : N
hn : n ≠ 0
ms : M × ↥S
eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) ms.1
hs : ms.1 ≠ 0
⊢ Membership.mem (γ := Submonoid N) (nonZeroDivisors N) n

Tactic:
And.left <| mul_mem_nonZeroDivisors.mp
    (eq ▸ f.map_nonZeroDivisors_le ⟨_, mem_nonZeroDivisors_of_ne_zero hs, rfl⟩)

Premises used: And.left, Iff.mp, mul_mem_nonZeroDivisors
-- 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
inst_2 : NoZeroDivisors M
n : N
hn : n ≠ 0
ms : M × ↥S
eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) ms.1
hs : ms.1 ≠ 0
⊢ Membership.mem (γ := Submonoid N) (nonZeroDivisors N) n

Tactic:
exact And.left <| mul_mem_nonZeroDivisors.mp
    (eq ▸ f.map_nonZeroDivisors_le ⟨_, mem_nonZeroDivisors_of_ne_zero hs, rfl⟩)

Premises used: And.left, Iff.mp, mul_mem_nonZeroDivisors
-- Module: Mathlib.GroupTheory.MonoidLocalization.Order
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁_1 b₁_1 : α
a₂_1 b₂_1 : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s : (a : α × ↥s) → α × ↥s → Prop) (a₁, a₂) (b₁, b₂)
hcd : (r s : (a : α × ↥s) → α × ↥s → Prop) (c₁, c₂) (d₁, d₂)
obtain :
  ∀ (e : ↥s) (he : (↑e : α) * ((↑(b₁, b₂).2 : α) * (a₁, a₂).1) = (↑e : α) * ((↑(a₁, a₂).2 : α) * (b₁, b₂).1)),
    (fun (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s) ↦ (↑b₂ : α) * a₁ ≤ (↑a₂ : α) * b₁) a₁ a₂ c₁ c₂ ↔
      (fun (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s) ↦ (↑b₂ : α) * a₁ ≤ (↑a₂ : α) * b₁) b₁ b₂ d₁ d₂
⊢ (fun (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s) ↦ (↑b₂ : α) * a₁ ≤ (↑a₂ : α) * b₁) a₁ a₂ c₁ c₂ ↔
    (fun (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s) ↦ (↑b₂ : α) * a₁ ≤ (↑a₂ : α) * b₁) b₁ b₂ d₁ d₂

Tactic:
obtain ⟨e, he⟩ := r_iff_exists.1 hab

Premises used: Localization.r_iff_exists, Iff.mp
-- Module: Mathlib.GroupTheory.MonoidLocalization.Order
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁_1 b₁_1 : α
a₂_1 b₂_1 : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s : (a : α × ↥s) → α × ↥s → Prop) (a₁, a₂) (b₁, b₂)
hcd : (r s : (a : α × ↥s) → α × ↥s → Prop) (c₁, c₂) (d₁, d₂)
e : ↥s
he : (↑e : α) * ((↑(b₁, b₂).2 : α) * (a₁, a₂).1) = (↑e : α) * ((↑(a₁, a₂).2 : α) * (b₁, b₂).1)
obtain :
  ∀ (f : ↥s) (hf : (↑f : α) * ((↑(d₁, d₂).2 : α) * (c₁, c₂).1) = (↑f : α) * ((↑(c₁, c₂).2 : α) * (d₁, d₂).1)),
    (fun (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s) ↦ (↑b₂ : α) * a₁ ≤ (↑a₂ : α) * b₁) a₁ a₂ c₁ c₂ ↔
      (fun (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s) ↦ (↑b₂ : α) * a₁ ≤ (↑a₂ : α) * b₁) b₁ b₂ d₁ d₂
⊢ (fun (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s) ↦ (↑b₂ : α) * a₁ ≤ (↑a₂ : α) * b₁) a₁ a₂ c₁ c₂ ↔
    (fun (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s) ↦ (↑b₂ : α) * a₁ ≤ (↑a₂ : α) * b₁) b₁ b₂ d₁ d₂

Tactic:
obtain ⟨f, hf⟩ := r_iff_exists.1 hcd

Premises used: Localization.r_iff_exists, Iff.mp