-- Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean
theorem mk_mem_nonZeroDivisors_associates : Associates.mk a ∈ (Associates M₀)⁰ ↔ a ∈ M₀⁰

Proof state:
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
⊢ Associates.mk a ∈ (Associates M₀)⁰ ↔ a ∈ M₀⁰

Tactic:
rw [mem_nonZeroDivisors_iff, mem_nonZeroDivisors_iff, ← not_iff_not]

Result:
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
⊢ (¬∀ (x : Associates M₀), x * Associates.mk a = 0 → x = 0) ↔ ¬∀ (x : M₀), x * a = 0 → x = 0

Proof state:
case mpr
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
x✝ : ∃ x, x * a = 0 ∧ x ≠ 0
b : M₀
hb₁ : b * a = 0
hb₂ : b ≠ 0
⊢ Associates.mk b * Associates.mk a = 0

Tactic:
rw [Associates.mk_mul_mk, hb₁, Associates.mk_zero]

Result:
no goals

Proof state:
case mp.intro.mk.intro.refine_2
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
w✝ : Associates M₀
x : M₀
hx₁ : Quot.mk (⇑(Associated.setoid M₀)) x * Associates.mk a = 0
hx₂ : Quot.mk (⇑(Associated.setoid M₀)) x ≠ 0
⊢ x ≠ 0

Tactic:
rwa [← Associates.mk_ne_zero, ← Associates.quot_mk_eq_mk]

Result:
no goals

Proof state:
case mpr
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
⊢ (∃ x, x * a = 0 ∧ x ≠ 0) → ∃ x, x * Associates.mk a = 0 ∧ x ≠ 0

Tactic:
refine fun ⟨b, hb₁, hb₂⟩ ↦ ⟨Associates.mk b, ?_, by rwa [Associates.mk_ne_zero]⟩

Result:
case mpr
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
x✝ : ∃ x, x * a = 0 ∧ x ≠ 0
b : M₀
hb₁ : b * a = 0
hb₂ : b ≠ 0
⊢ Associates.mk b * Associates.mk a = 0

Proof state:
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
⊢ (∃ x, x * Associates.mk a = 0 ∧ x ≠ 0) ↔ ∃ x, x * a = 0 ∧ x ≠ 0

Tactic:
constructor

Result:
case mp
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
⊢ (∃ x, x * Associates.mk a = 0 ∧ x ≠ 0) → ∃ x, x * a = 0 ∧ x ≠ 0

case mpr
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
⊢ (∃ x, x * a = 0 ∧ x ≠ 0) → ∃ x, x * Associates.mk a = 0 ∧ x ≠ 0

Proof state:
case mp.intro.mk.intro.refine_1
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
w✝ : Associates M₀
x : M₀
hx₁ : Quot.mk (⇑(Associated.setoid M₀)) x * Associates.mk a = 0
hx₂ : Quot.mk (⇑(Associated.setoid M₀)) x ≠ 0
⊢ x * a = 0

Tactic:
rwa [← Associates.mk_eq_zero, ← Associates.mk_mul_mk, ← Associates.quot_mk_eq_mk]

Result:
no goals

Proof state:
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
x✝ : ∃ x, x * a = 0 ∧ x ≠ 0
b : M₀
hb₁ : b * a = 0
hb₂ : b ≠ 0
⊢ Associates.mk b ≠ 0

Tactic:
rwa [Associates.mk_ne_zero]

Result:
no goals

Proof state:
case mp
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
⊢ (∃ x, x * Associates.mk a = 0 ∧ x ≠ 0) → ∃ x, x * a = 0 ∧ x ≠ 0

Tactic:
rintro ⟨⟨x⟩, hx₁, hx₂⟩

Result:
case mp.intro.mk.intro
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
w✝ : Associates M₀
x : M₀
hx₁ : Quot.mk (⇑(Associated.setoid M₀)) x * Associates.mk a = 0
hx₂ : Quot.mk (⇑(Associated.setoid M₀)) x ≠ 0
⊢ ∃ x, x * a = 0 ∧ x ≠ 0

Proof state:
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
⊢ (¬∀ (x : Associates M₀), x * Associates.mk a = 0 → x = 0) ↔ ¬∀ (x : M₀), x * a = 0 → x = 0

Tactic:
push_neg

Result:
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
⊢ (∃ x, x * Associates.mk a = 0 ∧ x ≠ 0) ↔ ∃ x, x * a = 0 ∧ x ≠ 0

Proof state:
case mp.intro.mk.intro
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
w✝ : Associates M₀
x : M₀
hx₁ : Quot.mk (⇑(Associated.setoid M₀)) x * Associates.mk a = 0
hx₂ : Quot.mk (⇑(Associated.setoid M₀)) x ≠ 0
⊢ ∃ x, x * a = 0 ∧ x ≠ 0

Tactic:
refine ⟨x, ?_, ?_⟩

Result:
case mp.intro.mk.intro.refine_1
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
w✝ : Associates M₀
x : M₀
hx₁ : Quot.mk (⇑(Associated.setoid M₀)) x * Associates.mk a = 0
hx₂ : Quot.mk (⇑(Associated.setoid M₀)) x ≠ 0
⊢ x * a = 0

case mp.intro.mk.intro.refine_2
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
w✝ : Associates M₀
x : M₀
hx₁ : Quot.mk (⇑(Associated.setoid M₀)) x * Associates.mk a = 0
hx₂ : Quot.mk (⇑(Associated.setoid M₀)) x ≠ 0
⊢ x ≠ 0