[GOAL]
M₀ : Type ?u.8
inst✝ : MonoidWithZero M₀
⊢ 1 ∈
    { carrier := {x | ∀ (y : M₀), y * x = 0 → y = 0},
        mul_mem' :=
          (_ :
            ∀ {x y : M₀},
              x ∈ {x | ∀ (y : M₀), y * x = 0 → y = 0} →
                y ∈ {x | ∀ (y : M₀), y * x = 0 → y = 0} → ∀ (z : M₀), z * (x * y) = 0 → z = 0) }.carrier
[PROOFSTEP]
simp
[GOAL]
M₀ : Type ?u.2171
inst✝ : MonoidWithZero M₀
⊢ 1 ∈
    { carrier := {x | ∀ (y : M₀), x * y = 0 → y = 0},
        mul_mem' :=
          (_ :
            ∀ {x y : M₀},
              x ∈ {x | ∀ (y : M₀), x * y = 0 → y = 0} →
                y ∈ {x | ∀ (y : M₀), x * y = 0 → y = 0} → ∀ (z : M₀), x * y * z = 0 → z = 0) }.carrier
[PROOFSTEP]
simp
[GOAL]
M₀✝ : Type ?u.4317
inst✝¹ : MonoidWithZero M₀✝
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
⊢ nonZeroDivisorsLeft M₀ = nonZeroDivisorsRight M₀
[PROOFSTEP]
ext x
[GOAL]
case h
M₀✝ : Type ?u.4317
inst✝¹ : MonoidWithZero M₀✝
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
x : M₀
⊢ x ∈ nonZeroDivisorsLeft M₀ ↔ x ∈ nonZeroDivisorsRight M₀
[PROOFSTEP]
simp [mul_comm x]
[GOAL]
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
⊢ ↑(nonZeroDivisorsLeft M₀) = {x | x ≠ 0}
[PROOFSTEP]
ext x
[GOAL]
case h
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
⊢ x ∈ ↑(nonZeroDivisorsLeft M₀) ↔ x ∈ {x | x ≠ 0}
[PROOFSTEP]
simp only [SetLike.mem_coe, mem_nonZeroDivisorsLeft_iff, mul_eq_zero, forall_eq_or_imp, true_and, Set.mem_setOf_eq]
[GOAL]
case h
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
⊢ (∀ (a : M₀), x = 0 → a = 0) ↔ x ≠ 0
[PROOFSTEP]
refine' ⟨fun h ↦ _, fun hx y hx' ↦ by contradiction⟩
[GOAL]
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
hx : x ≠ 0
y : M₀
hx' : x = 0
⊢ y = 0
[PROOFSTEP]
contradiction
[GOAL]
case h
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
h : ∀ (a : M₀), x = 0 → a = 0
⊢ x ≠ 0
[PROOFSTEP]
contrapose! h
[GOAL]
case h
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
h : x = 0
⊢ ∃ a, x = 0 ∧ a ≠ 0
[PROOFSTEP]
exact ⟨1, h, one_ne_zero⟩
[GOAL]
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
⊢ ↑(nonZeroDivisorsRight M₀) = {x | x ≠ 0}
[PROOFSTEP]
ext x
[GOAL]
case h
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
⊢ x ∈ ↑(nonZeroDivisorsRight M₀) ↔ x ∈ {x | x ≠ 0}
[PROOFSTEP]
simp only [SetLike.mem_coe, mem_nonZeroDivisorsRight_iff, mul_eq_zero, Set.mem_setOf_eq]
[GOAL]
case h
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
⊢ (∀ (y : M₀), x = 0 ∨ y = 0 → y = 0) ↔ x ≠ 0
[PROOFSTEP]
refine' ⟨fun h ↦ _, fun hx y hx' ↦ by aesop⟩
[GOAL]
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
hx : x ≠ 0
y : M₀
hx' : x = 0 ∨ y = 0
⊢ y = 0
[PROOFSTEP]
aesop
[GOAL]
case h
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
h : ∀ (y : M₀), x = 0 ∨ y = 0 → y = 0
⊢ x ≠ 0
[PROOFSTEP]
contrapose! h
[GOAL]
case h
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
h : x = 0
⊢ ∃ y, (x = 0 ∨ y = 0) ∧ y ≠ 0
[PROOFSTEP]
exact ⟨1, Or.inl h, one_ne_zero⟩
