case left
α : Type u_1
inst✝ : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
⊢ a ≠ 0

case right
α : Type u_1
inst✝ : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
⊢ ∃ x, ¬IsUnit x ∧ b = a * x
α : Type u_1
inst✝ : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
⊢ DvdNotUnit a b
constructor
case left
α : Type u_1
inst✝ : CommMonoidWithZero α
b : α
hd : 0 ∣ b
hnd : ¬b ∣ 0
⊢ False
case left
α : Type u_1
inst✝ : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
⊢ a ≠ 0
rintro rfl
no goals
case left
α : Type u_1
inst✝ : CommMonoidWithZero α
b : α
hd : 0 ∣ b
hnd : ¬b ∣ 0
⊢ False
exact hnd (dvd_zero _)
case right.intro
α : Type u_1
inst✝ : CommMonoidWithZero α
a c : α
hnd : ¬a * c ∣ a
⊢ ∃ x, ¬IsUnit x ∧ a * c = a * x
case right
α : Type u_1
inst✝ : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
⊢ ∃ x, ¬IsUnit x ∧ b = a * x
rcases hd with ⟨c, rfl⟩
case right.intro
α : Type u_1
inst✝ : CommMonoidWithZero α
a c : α
hnd : ¬a * c ∣ a
⊢ ¬IsUnit c
case right.intro
α : Type u_1
inst✝ : CommMonoidWithZero α
a c : α
hnd : ¬a * c ∣ a
⊢ ∃ x, ¬IsUnit x ∧ a * c = a * x
refine' ⟨c, _, rfl⟩
case right.intro.intro
α : Type u_1
inst✝ : CommMonoidWithZero α
a : α
u : αˣ
hnd : ¬a * ↑u ∣ a
⊢ False
case right.intro
α : Type u_1
inst✝ : CommMonoidWithZero α
a c : α
hnd : ¬a * c ∣ a
⊢ ¬IsUnit c
rintro ⟨u, rfl⟩
no goals
case right.intro.intro
α : Type u_1
inst✝ : CommMonoidWithZero α
a : α
u : αˣ
hnd : ¬a * ↑u ∣ a
⊢ False
simp at hnd