case intro.intro.intro
α : Type u_1
β : Type ?u.348267
γ : Type ?u.348270
δ : Type ?u.348273
inst✝ : CommMonoidWithZero α
p x : α
hx : ¬IsUnit x
⊢ ¬IsUnit (p * x)
α : Type u_1
β : Type ?u.348267
γ : Type ?u.348270
δ : Type ?u.348273
inst✝ : CommMonoidWithZero α
p q : α
hp : DvdNotUnit p q
⊢ ¬IsUnit q
obtain ⟨-, x, hx, rfl⟩ := hp
no goals
case intro.intro.intro
α : Type u_1
β : Type ?u.348267
γ : Type ?u.348270
δ : Type ?u.348273
inst✝ : CommMonoidWithZero α
p x : α
hx : ¬IsUnit x
⊢ ¬IsUnit (p * x)
exact fun hc => hx (isUnit_iff_dvd_one.mpr (dvd_of_mul_left_dvd (isUnit_iff_dvd_one.mp hc)))