[GOAL]
R : Type u_1
inst✝ : MonoidWithZero R
a✝ b✝ : R
hx₁ : a✝ ∈ {x | ∀ (z : R), z * x = 0 → z = 0}
hx₂ : b✝ ∈ {x | ∀ (z : R), z * x = 0 → z = 0}
x✝ : R
hz : x✝ * (a✝ * b✝) = 0
⊢ x✝ = 0
[PROOFSTEP]
rw [← mul_assoc] at hz 
[GOAL]
R : Type u_1
inst✝ : MonoidWithZero R
a✝ b✝ : R
hx₁ : a✝ ∈ {x | ∀ (z : R), z * x = 0 → z = 0}
hx₂ : b✝ ∈ {x | ∀ (z : R), z * x = 0 → z = 0}
x✝ : R
hz : x✝ * a✝ * b✝ = 0
⊢ x✝ = 0
[PROOFSTEP]
exact hx₁ _ (hx₂ _ hz)
[GOAL]
R : Type u_1
inst✝ : MonoidWithZero R
x✝ : R
hz : x✝ * 1 = 0
⊢ x✝ = 0
[PROOFSTEP]
rwa [mul_one] at hz 
[GOAL]
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
x r : M
hr : r ∈ M⁰
⊢ x = 0 → x * r = 0
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
r x : M₁
hr : r ∈ M₁⁰
⊢ r * x = 0 ↔ x = 0
[PROOFSTEP]
rw [mul_comm, mul_right_mem_nonZeroDivisors_eq_zero_iff hr]
[GOAL]
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
x y r : R
hr : r ∈ R⁰
⊢ x * r = y * r ↔ x = y
[PROOFSTEP]
refine ⟨fun h ↦ ?_, congrArg (· * r)⟩
[GOAL]
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
x y r : R
hr : r ∈ R⁰
h : x * r = y * r
⊢ x = y
[PROOFSTEP]
rw [← sub_eq_zero, ← mul_right_mem_nonZeroDivisors_eq_zero_iff hr, sub_mul, h, sub_self]
[GOAL]
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
x y r : R'
hr : r ∈ R'⁰
⊢ r * x = r * y ↔ x = y
[PROOFSTEP]
simp_rw [mul_comm r, mul_cancel_right_mem_nonZeroDivisors hr]
[GOAL]
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
⊢ a * b ∈ M₁⁰ ↔ a ∈ M₁⁰ ∧ b ∈ M₁⁰
[PROOFSTEP]
constructor
[GOAL]
case mp
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
⊢ a * b ∈ M₁⁰ → a ∈ M₁⁰ ∧ b ∈ M₁⁰
[PROOFSTEP]
intro h
[GOAL]
case mp
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
h : a * b ∈ M₁⁰
⊢ a ∈ M₁⁰ ∧ b ∈ M₁⁰
[PROOFSTEP]
constructor
[GOAL]
case mp.left
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
h : a * b ∈ M₁⁰
⊢ a ∈ M₁⁰
[PROOFSTEP]
intro x h'
[GOAL]
case mp.right
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
h : a * b ∈ M₁⁰
⊢ b ∈ M₁⁰
[PROOFSTEP]
intro x h'
[GOAL]
case mp.left
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
h : a * b ∈ M₁⁰
x : M₁
h' : x * a = 0
⊢ x = 0
[PROOFSTEP]
apply h
[GOAL]
case mp.right
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
h : a * b ∈ M₁⁰
x : M₁
h' : x * b = 0
⊢ x = 0
[PROOFSTEP]
apply h
[GOAL]
case mp.left.a
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
h : a * b ∈ M₁⁰
x : M₁
h' : x * a = 0
⊢ x * (a * b) = 0
[PROOFSTEP]
rw [← mul_assoc, h', zero_mul]
[GOAL]
case mp.right.a
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
h : a * b ∈ M₁⁰
x : M₁
h' : x * b = 0
⊢ x * (a * b) = 0
[PROOFSTEP]
rw [mul_comm a b, ← mul_assoc, h', zero_mul]
[GOAL]
case mpr
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
⊢ a ∈ M₁⁰ ∧ b ∈ M₁⁰ → a * b ∈ M₁⁰
[PROOFSTEP]
rintro ⟨ha, hb⟩ x hx
[GOAL]
case mpr.intro
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
ha : a ∈ M₁⁰
hb : b ∈ M₁⁰
x : M₁
hx : x * (a * b) = 0
⊢ x = 0
[PROOFSTEP]
apply ha
[GOAL]
case mpr.intro.a
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
ha : a ∈ M₁⁰
hb : b ∈ M₁⁰
x : M₁
hx : x * (a * b) = 0
⊢ x * a = 0
[PROOFSTEP]
apply hb
[GOAL]
case mpr.intro.a.a
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
ha : a ∈ M₁⁰
hb : b ∈ M₁⁰
x : M₁
hx : x * (a * b) = 0
⊢ x * a * b = 0
[PROOFSTEP]
rw [mul_assoc, hx]
[GOAL]
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M'
inst✝ : MonoidWithZeroHomClass F M M'
f : F
hf : Function.Injective ↑f
S : Submonoid M
hS : S ≤ M⁰
⊢ Submonoid.map f S ≤ M'⁰
[PROOFSTEP]
cases subsingleton_or_nontrivial M
[GOAL]
case inl
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M'
inst✝ : MonoidWithZeroHomClass F M M'
f : F
hf : Function.Injective ↑f
S : Submonoid M
hS : S ≤ M⁰
h✝ : Subsingleton M
⊢ Submonoid.map f S ≤ M'⁰
[PROOFSTEP]
simp [Subsingleton.elim S ⊥]
[GOAL]
case inr
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M'
inst✝ : MonoidWithZeroHomClass F M M'
f : F
hf : Function.Injective ↑f
S : Submonoid M
hS : S ≤ M⁰
h✝ : Nontrivial M
⊢ Submonoid.map f S ≤ M'⁰
[PROOFSTEP]
exact
  le_nonZeroDivisors_of_noZeroDivisors fun h ↦
    let ⟨x, hx, hx0⟩ := h
    zero_ne_one (hS (hf (hx0.trans (map_zero f).symm) ▸ hx : 0 ∈ S) 1 (mul_zero 1)).symm
[GOAL]
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
s : Multiset M₁
⊢ Multiset.prod s = 0 ↔ ∃ r x, r = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
s : Multiset M₁
⊢ Multiset.prod s = 0 → ∃ r x, r = 0
case mpr
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
s : Multiset M₁
⊢ (∃ r x, r = 0) → Multiset.prod s = 0
[PROOFSTEP]
swap
[GOAL]
case mpr
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
s : Multiset M₁
⊢ (∃ r x, r = 0) → Multiset.prod s = 0
[PROOFSTEP]
rintro ⟨r, hrs, rfl⟩
[GOAL]
case mpr.intro.intro
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
s : Multiset M₁
hrs : 0 ∈ s
⊢ Multiset.prod s = 0
[PROOFSTEP]
exact Multiset.prod_eq_zero hrs
[GOAL]
case mp
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
s : Multiset M₁
⊢ Multiset.prod s = 0 → ∃ r x, r = 0
[PROOFSTEP]
induction' s using Multiset.induction_on with a s ih
[GOAL]
case mp.empty
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
⊢ Multiset.prod 0 = 0 → ∃ r x, r = 0
[PROOFSTEP]
intro habs
[GOAL]
case mp.empty
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
habs : Multiset.prod 0 = 0
⊢ ∃ r x, r = 0
[PROOFSTEP]
simp at habs 
[GOAL]
case mp.cons
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
a : M₁
s : Multiset M₁
ih : Multiset.prod s = 0 → ∃ r x, r = 0
⊢ Multiset.prod (a ::ₘ s) = 0 → ∃ r x, r = 0
[PROOFSTEP]
rw [Multiset.prod_cons]
[GOAL]
case mp.cons
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
a : M₁
s : Multiset M₁
ih : Multiset.prod s = 0 → ∃ r x, r = 0
⊢ a * Multiset.prod s = 0 → ∃ r x, r = 0
[PROOFSTEP]
intro hprod
[GOAL]
case mp.cons
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
a : M₁
s : Multiset M₁
ih : Multiset.prod s = 0 → ∃ r x, r = 0
hprod : a * Multiset.prod s = 0
⊢ ∃ r x, r = 0
[PROOFSTEP]
replace hprod := eq_zero_or_eq_zero_of_mul_eq_zero hprod
[GOAL]
case mp.cons
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
a : M₁
s : Multiset M₁
ih : Multiset.prod s = 0 → ∃ r x, r = 0
hprod : a = 0 ∨ Multiset.prod s = 0
⊢ ∃ r x, r = 0
[PROOFSTEP]
cases' hprod with ha hb
[GOAL]
case mp.cons.inl
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
a : M₁
s : Multiset M₁
ih : Multiset.prod s = 0 → ∃ r x, r = 0
ha : a = 0
⊢ ∃ r x, r = 0
[PROOFSTEP]
exact ⟨a, Multiset.mem_cons_self a s, ha⟩
[GOAL]
case mp.cons.inr
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
a : M₁
s : Multiset M₁
ih : Multiset.prod s = 0 → ∃ r x, r = 0
hb : Multiset.prod s = 0
⊢ ∃ r x, r = 0
[PROOFSTEP]
apply (ih hb).imp _
[GOAL]
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
a : M₁
s : Multiset M₁
ih : Multiset.prod s = 0 → ∃ r x, r = 0
hb : Multiset.prod s = 0
⊢ ∀ (a_1 : M₁), (∃ x, a_1 = 0) → ∃ x, a_1 = 0
[PROOFSTEP]
rintro b ⟨hb₁, hb₂⟩
[GOAL]
case intro
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
a : M₁
s : Multiset M₁
ih : Multiset.prod s = 0 → ∃ r x, r = 0
hb : Multiset.prod s = 0
b : M₁
hb₁ : b ∈ s
hb₂ : b = 0
⊢ ∃ x, b = 0
[PROOFSTEP]
exact ⟨Multiset.mem_cons_of_mem hb₁, hb₂⟩
