[GOAL]
α : Type u_1
inst✝ : SemigroupWithZero α
a : α
h : a = 0
⊢ 0 ∣ a
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
inst✝ : SemigroupWithZero α
a : α
h : a = 0
⊢ 0 ∣ 0
[PROOFSTEP]
exact ⟨0, by simp⟩
[GOAL]
α : Type u_1
inst✝ : SemigroupWithZero α
a : α
h : a = 0
⊢ 0 = 0 * 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : SemigroupWithZero α
a✝ a : α
⊢ a * 0 = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : CancelMonoidWithZero α
a b c : α
ha : a ≠ 0
d : α
⊢ a * c = a * b * d ↔ c = b * d
[PROOFSTEP]
rw [mul_assoc, mul_right_inj' ha]
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a b c : α
hc : c ≠ 0
d : α
⊢ b * c = a * c * d ↔ b = a * d
[PROOFSTEP]
rw [mul_right_comm, mul_left_inj' hc]
[GOAL]
α : Type u_1
inst✝ : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
⊢ DvdNotUnit a b
[PROOFSTEP]
constructor
[GOAL]
case left
α : Type u_1
inst✝ : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
⊢ a ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case left
α : Type u_1
inst✝ : CommMonoidWithZero α
b : α
hd : 0 ∣ b
hnd : ¬b ∣ 0
⊢ False
[PROOFSTEP]
exact hnd (dvd_zero _)
[GOAL]
case right
α : Type u_1
inst✝ : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
⊢ ∃ x, ¬IsUnit x ∧ b = a * x
[PROOFSTEP]
rcases hd with ⟨c, rfl⟩
[GOAL]
case right.intro
α : Type u_1
inst✝ : CommMonoidWithZero α
a c : α
hnd : ¬a * c ∣ a
⊢ ∃ x, ¬IsUnit x ∧ a * c = a * x
[PROOFSTEP]
refine' ⟨c, _, rfl⟩
[GOAL]
case right.intro
α : Type u_1
inst✝ : CommMonoidWithZero α
a c : α
hnd : ¬a * c ∣ a
⊢ ¬IsUnit c
[PROOFSTEP]
rintro ⟨u, rfl⟩
[GOAL]
case right.intro.intro
α : Type u_1
inst✝ : CommMonoidWithZero α
a : α
u : αˣ
hnd : ¬a * ↑u ∣ a
⊢ False
[PROOFSTEP]
simp at hnd 
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
x y : α
x✝ : x ∣ y ∧ ¬y ∣ x
d : α
hd : y = x * d
hyx : ¬y ∣ x
hx0 : x = 0
⊢ False
[PROOFSTEP]
simp [hx0] at hyx 
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
x y : α
x✝¹ : x ∣ y ∧ ¬y ∣ x
d : α
hd : y = x * d
hyx : ¬y ∣ x
x✝ : d ∣ 1
e : α
he : 1 = d * e
⊢ x = y * e
[PROOFSTEP]
rw [hd, mul_assoc, ← he, mul_one]
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
x y : α
x✝¹ : DvdNotUnit x y
hx0 : x ≠ 0
d : α
hdu : ¬IsUnit d
hdx : y = x * d
x✝ : y ∣ x
e : α
he : x = y * e
⊢ x * 1 = x * (d * e)
[PROOFSTEP]
conv =>
  lhs
  rw [he, hdx]
  simp [mul_assoc]
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
x y : α
x✝¹ : DvdNotUnit x y
hx0 : x ≠ 0
d : α
hdu : ¬IsUnit d
hdx : y = x * d
x✝ : y ∣ x
e : α
he : x = y * e
| x * 1 = x * (d * e)
[PROOFSTEP]
  lhs
  rw [he, hdx]
  simp [mul_assoc]
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
x y : α
x✝¹ : DvdNotUnit x y
hx0 : x ≠ 0
d : α
hdu : ¬IsUnit d
hdx : y = x * d
x✝ : y ∣ x
e : α
he : x = y * e
| x * 1 = x * (d * e)
[PROOFSTEP]
  lhs
  rw [he, hdx]
  simp [mul_assoc]
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
x y : α
x✝¹ : DvdNotUnit x y
hx0 : x ≠ 0
d : α
hdu : ¬IsUnit d
hdx : y = x * d
x✝ : y ∣ x
e : α
he : x = y * e
| x * 1 = x * (d * e)
[PROOFSTEP]
lhs
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
x y : α
x✝¹ : DvdNotUnit x y
hx0 : x ≠ 0
d : α
hdu : ¬IsUnit d
hdx : y = x * d
x✝ : y ∣ x
e : α
he : x = y * e
| x * 1
[PROOFSTEP]
rw [he, hdx]
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
x y : α
x✝¹ : DvdNotUnit x y
hx0 : x ≠ 0
d : α
hdu : ¬IsUnit d
hdx : y = x * d
x✝ : y ∣ x
e : α
he : x = y * e
| x * d * e * 1
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
α : Type u_1
inst✝ : MonoidWithZero α
p q : α
h₁ : q ≠ 0
h₂ : p ∣ q
⊢ p ≠ 0
[PROOFSTEP]
rcases h₂ with ⟨u, rfl⟩
[GOAL]
case intro
α : Type u_1
inst✝ : MonoidWithZero α
p u : α
h₁ : p * u ≠ 0
⊢ p ≠ 0
[PROOFSTEP]
exact left_ne_zero_of_mul h₁
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Subsingleton αˣ
a b : α
⊢ a ∣ b → b ∣ a → a = b
[PROOFSTEP]
rintro ⟨c, rfl⟩ ⟨d, hcd⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Subsingleton αˣ
a c d : α
hcd : a = a * c * d
⊢ a = a * c
[PROOFSTEP]
rw [mul_assoc, eq_comm, mul_right_eq_self₀, mul_eq_one] at hcd 
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Subsingleton αˣ
a c d : α
hcd : c = 1 ∧ d = 1 ∨ a = 0
⊢ a = a * c
[PROOFSTEP]
obtain ⟨rfl, -⟩ | rfl := hcd
[GOAL]
case intro.intro.inl.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Subsingleton αˣ
a d : α
⊢ a = a * 1
[PROOFSTEP]
simp
[GOAL]
case intro.intro.inr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Subsingleton αˣ
c d : α
⊢ 0 = 0 * c
[PROOFSTEP]
simp
