case intro
α : Type u_1
β : Type ?u.86920
γ : Type ?u.86923
δ : Type ?u.86926
inst✝ : Monoid α
p : α
hp : Irreducible p
q' : α
hq : Irreducible (p * q')
⊢ p * q' ∣ p
α : Type u_1
β : Type ?u.86920
γ : Type ?u.86923
δ : Type ?u.86926
inst✝ : Monoid α
p q : α
hp : Irreducible p
hq : Irreducible q
⊢ p ∣ q → q ∣ p
rintro ⟨q', rfl⟩
no goals
case intro
α : Type u_1
β : Type ?u.86920
γ : Type ?u.86923
δ : Type ?u.86926
inst✝ : Monoid α
p : α
hp : Irreducible p
q' : α
hq : Irreducible (p * q')
⊢ p * q' ∣ p
rw [IsUnit.mul_right_dvd (Or.resolve_left (of_irreducible_mul hq) hp.not_unit)]