case intro
α : Type u_1
β : Type ?u.354581
γ : Type ?u.354584
δ : Type ?u.354587
inst✝ : CancelCommMonoidWithZero α
p : α
a : αˣ
h : DvdNotUnit p (p * ↑a)
⊢ False
α : Type u_1
β : Type ?u.354581
γ : Type ?u.354584
δ : Type ?u.354587
inst✝ : CancelCommMonoidWithZero α
p q : α
h : DvdNotUnit p q
⊢ ¬p ~ᵤ q
rintro ⟨a, rfl⟩
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.354581
γ : Type ?u.354584
δ : Type ?u.354587
inst✝ : CancelCommMonoidWithZero α
p : α
a : αˣ
hp : p ≠ 0
x : α
hx : ¬IsUnit x
hx' : p * ↑a = p * x
⊢ False
case intro
α : Type u_1
β : Type ?u.354581
γ : Type ?u.354584
δ : Type ?u.354587
inst✝ : CancelCommMonoidWithZero α
p : α
a : αˣ
h : DvdNotUnit p (p * ↑a)
⊢ False
obtain ⟨hp, x, hx, hx'⟩ := h
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.354581
γ : Type ?u.354584
δ : Type ?u.354587
inst✝ : CancelCommMonoidWithZero α
p : α
a : αˣ
hp : p ≠ 0
hx : ¬IsUnit ↑a
hx' : p * ↑a = p * ↑a
⊢ False
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.354581
γ : Type ?u.354584
δ : Type ?u.354587
inst✝ : CancelCommMonoidWithZero α
p : α
a : αˣ
hp : p ≠ 0
x : α
hx : ¬IsUnit x
hx' : p * ↑a = p * x
⊢ False
rcases(mul_right_inj' hp).mp hx' with rfl
no goals
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.354581
γ : Type ?u.354584
δ : Type ?u.354587
inst✝ : CancelCommMonoidWithZero α
p : α
a : αˣ
hp : p ≠ 0
hx : ¬IsUnit ↑a
hx' : p * ↑a = p * ↑a
⊢ False
exact hx a.isUnit