awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (goal)
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
have refine : (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ T) d sorry) : P) * x = (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ T) d sorry) : P) * y
Tactic: refine ⟨⟨d, H' ▸ show k d ∈ S from hd.symm ▸ c.2⟩, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (goal)
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)
⊢ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ T) d ⋯) : P) * x = (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ T) d ⋯) : P) * y
have 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 sorry) : P) * x = (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ T) d sorry) : P) * y
Tactic: rw [← hd, ← map_mul k, ← map_mul k] at hc
Cleared hypotheses: hc, hd
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
f : S.LocalizationMap N
⊢ f.ofMulEquivOfDom (k := MulEquiv.refl M) ⋯ = f
have h : ∀ (x : M),
  Eq.{u_2 + 1} (α := N) ((f.ofMulEquivOfDom (k := MulEquiv.refl M) sorry : (a : M) → N) x : N) ((f : (a : M) → N) x : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (goal)
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) (mk x y) = f.mk' x y
have rw : (mulEquivOfQuotient f : (a : Localization S) → N) ((monoidOf S).mk' x y) = f.mk' x y
Tactic: rw [mk_eq_monoidOf_mk'_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (goal)
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) = mk x y
have rw : ((mulEquivOfQuotient f).symm : (a : N) → Localization S) (f.mk' x y) = (monoidOf S).mk' x y
Tactic: rw [mk_eq_monoidOf_mk'_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
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
⊢ a = b
have 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)
Tactic: rw [← f.mk'_sec a, ← f.mk'_sec b, f.eq]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (hypothesis)
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 ∈ S
have eq₁ : 0 = (↑c : M)
Tactic: rw [mul_zero, mul_one] at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
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
⊢ Nontrivial N
have rwa : ¬Subsingleton N
Tactic: rwa [← not_subsingleton_iff_nontrivial, f.subsingleton_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoidWithZero N
f : S.LocalizationMap N
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) 0 : N) (0 : N)
have 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)
Tactic: have ⟨ms, eq⟩ := f.surj 0
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
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
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) 0 : N) (0 : N)
have rw : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (0 * ms.1) : N) (0 : N)
Tactic: rw [← zero_mul, map_mul, ← eq, zero_mul, mul_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
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)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) 0 : N) (0 : N)
have rw₁ : M
Tactic: rw [← zero_mul, map_mul, ← eq, zero_mul, mul_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
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
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) 0 : N) (0 : N)
have rw₂ : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) 0 : N) ((f : (a : M) → N) ms.1 : N) = 0
Tactic: rw [← zero_mul, map_mul, ← eq, zero_mul, mul_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
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
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) 0 : N) (0 : N)
have 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
Tactic: rw [← zero_mul, map_mul, ← eq, zero_mul, mul_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
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
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) 0 : N) (0 : N)
have rw₄ : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) 0 : N) (0 : N) = 0
Tactic: rw [← zero_mul, map_mul, ← eq, zero_mul, mul_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
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
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) 0 : N) (0 : N)
have rw₅ : Eq.{u_2 + 1} (α := N) 0 0
Tactic: rw [← zero_mul, map_mul, ← eq, zero_mul, mul_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
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
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) 0 : N) (0 : N)
have 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)
Tactic: have ⟨ms, eq⟩ := f.surj 0
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
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
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) 0 : N) (0 : N)
have rw : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (0 * ms.1) : N) (0 : N)
Tactic: rw [← zero_mul, map_mul, ← eq, zero_mul, mul_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
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)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) 0 : N) (0 : N)
have rw₁ : M
Tactic: rw [← zero_mul, map_mul, ← eq, zero_mul, mul_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
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
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) 0 : N) (0 : N)
have rw₂ : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) 0 : N) ((f : (a : M) → N) ms.1 : N) = 0
Tactic: rw [← zero_mul, map_mul, ← eq, zero_mul, mul_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
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
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) 0 : N) (0 : N)
have 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
Tactic: rw [← zero_mul, map_mul, ← eq, zero_mul, mul_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
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
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) 0 : N) (0 : N)
have rw₄ : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) 0 : N) (0 : N) = 0
Tactic: rw [← zero_mul, map_mul, ← eq, zero_mul, mul_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
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
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) 0 : N) (0 : N)
have rw₅ : Eq.{u_2 + 1} (α := N) 0 0
Tactic: rw [← zero_mul, map_mul, ← eq, zero_mul, mul_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
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
⊢ liftOn 0 f @H = f 0 1
have rw : liftOn (mk 0 1) f @H = f 0 1
Tactic: rw [← mk_zero 1, liftOn_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
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
⊢ liftOn 0 f @H = f 0 1
have rw₁ : f 0 1 = f 0 1
Tactic: rw [← mk_zero 1, liftOn_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoidWithZero N
f : S.LocalizationMap N
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (f.sec 0).1 : N) (0 : N)
have rw : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑(f.sec 0).2 : M) : N) (0 : N) = 0
Tactic: rw [LocalizationMap.sec_spec', mul_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
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
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (f.sec 0).1 : N) (0 : N)
have rw₁ : Eq.{u_2 + 1} (α := N) 0 0
Tactic: rw [LocalizationMap.sec_spec', mul_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
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_3 + 1} (α := P) (OneHom.toFun (↑(f.lift (g := (↑g : M →* P)) hg) : OneHom N P) 0) 0
have dsimp : Eq.{u_3 + 1} (α := P) ((f.lift (g := (↑g : M →* P)) hg : (a : N) → P) 0 : P) (0 : P)
Tactic: dsimp only [OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
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_3 + 1} (α := P) ((f.lift (g := (↑g : M →* P)) hg : (a : N) → P) 0 : P) (0 : P)
have rw : ((↑g : M →* P) : (a : M) → P) (f.sec 0).1 = (↑(↑g : M →* P) : OneHom M P).toFun 0
Tactic: rw [LocalizationMap.lift_spec f hg 0 0, mul_zero, ← map_zero g, ← g.toMonoidHom_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
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
have refine : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (f.sec 0).1 : N) ((f : (a : M) → N) 0 : N)
Tactic: refine f.eq_of_eq hg ?_
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
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) ((f : (a : M) → N) (f.sec 0).1 : N) ((f : (a : M) → N) 0 : N)
have rw : Eq.{u_2 + 1} (α := N) (0 : N) ((f : (a : M) → N) 0 : N)
Tactic: rw [LocalizationMap.sec_zero_fst]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
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
⊢ IsCancelMulZero N
have simp_rw : ∀ {a : N}, a ≠ 0 → IsRightRegular a
Tactic: simp_rw [isCancelMulZero_iff_forall_isRegular, Commute.isRegular_iff (Commute.all _),
    ← Commute.isRightRegular_iff (Commute.all _)]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
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
⊢ IsRightRegular n
have 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
Tactic: have ⟨ms, eq⟩ := f.surj n
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
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
⊢ IsRightRegular n
have refine : ms.1 ≠ 0
Tactic: refine (eq ▸ f.map_isRegular (isCancelMulZero_iff_forall_isRegular.mp ‹_› ?_)).2.of_mul
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
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
have refine : ∀ (h : ms.1 = 0), n = 0
Tactic: refine fun h ↦ hn ?_
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
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
⊢ n = 0
have 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
Tactic: rwa [h, map_zero, (f.map_units _).mul_left_eq_zero] at eq
Cleared hypotheses: eq, h
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
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
⊢ n = 0
have rwa₁ : ∀ (eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = 0) (h : ms.1 = 0), n = 0
Tactic: rwa [h, map_zero, (f.map_units _).mul_left_eq_zero] at eq
Cleared hypotheses: eq, h
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
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
⊢ n = 0
have rwa₂ : ∀ (eq : n = 0) (h : ms.1 = 0), n = 0
Tactic: rwa [h, map_zero, (f.map_units _).mul_left_eq_zero] at eq
Cleared hypotheses: eq, h
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
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
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) m : N) (0 : N) ↔ ∃ (s : ↥S), (↑s : M) * m = 0
have 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
Tactic: simp_rw [← f.map_zero, eq_iff_exists, mul_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
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
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) m : N) (0 : N) ↔ ∃ (s : ↥S), (↑s : M) * m = 0
have simp_rw₁ : (∃ (c : ↥S), (↑c : M) * m = (↑c : M) * 0) ↔ ∃ (s : ↥S), (↑s : M) * m = 0
Tactic: simp_rw [← f.map_zero, eq_iff_exists, mul_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
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
⊢ f.mk' m s = 0 ↔ ∃ (s : ↥S), (↑s : M) * m = 0
have 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
Tactic: rw [← (f.map_units s).mul_left_inj, mk'_spec, zero_mul, map_eq_zero_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
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
⊢ f.mk' m s = 0 ↔ ∃ (s : ↥S), (↑s : M) * m = 0
have 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
Tactic: rw [← (f.map_units s).mul_left_inj, mk'_spec, zero_mul, map_eq_zero_iff]