case intro.intro.intro
α : Type u_1
β : Type ?u.347413
γ : Type ?u.347416
δ : Type ?u.347419
inst✝ : CommMonoidWithZero α
p q : α
hq : Irreducible q
left✝ : p ≠ 0
x : α
hx : ¬IsUnit x
hx' : q = p * x
⊢ IsUnit p
α : Type u_1
β : Type ?u.347413
γ : Type ?u.347416
δ : Type ?u.347419
inst✝ : CommMonoidWithZero α
p q : α
h : DvdNotUnit p q
hq : Irreducible q
⊢ IsUnit p
obtain ⟨_, x, hx, hx'⟩ := h
no goals
case intro.intro.intro
α : Type u_1
β : Type ?u.347413
γ : Type ?u.347416
δ : Type ?u.347419
inst✝ : CommMonoidWithZero α
p q : α
hq : Irreducible q
left✝ : p ≠ 0
x : α
hx : ¬IsUnit x
hx' : q = p * x
⊢ IsUnit p
exact Or.resolve_right ((irreducible_iff.1 hq).right p x hx') hx