case intro
α : Type u_1
inst✝ : MonoidWithZero α
p u : α
h₁ : p * u ≠ 0
⊢ p ≠ 0
α : Type u_1
inst✝ : MonoidWithZero α
p q : α
h₁ : q ≠ 0
h₂ : p ∣ q
⊢ p ≠ 0
rcases h₂ with ⟨u, rfl⟩
no goals
case intro
α : Type u_1
inst✝ : MonoidWithZero α
p u : α
h₁ : p * u ≠ 0
⊢ p ≠ 0
exact left_ne_zero_of_mul h₁