case inl
b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ 1 → p * 1 ∣ b
⊢ 1 ∣ b

case inr
a b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ a → p * a ∣ b
ha : a ≠ 1
⊢ a ∣ b
a b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ a → p * a ∣ b
⊢ a ∣ b
obtain rfl | ha := eq_or_ne a 1
case inr.intro
a b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ a → p * a ∣ b
ha : a ≠ 1
p : ℕ
hp : Prime p ∧ p ∣ a
⊢ a ∣ b
case inr
a b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ a → p * a ∣ b
ha : a ≠ 1
⊢ a ∣ b
obtain ⟨p, hp⟩ := exists_prime_and_dvd ha
no goals
case inr.intro
a b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ a → p * a ∣ b
ha : a ≠ 1
p : ℕ
hp : Prime p ∧ p ∣ a
⊢ a ∣ b
exact _root_.trans (dvd_mul_left a p) (hdvd p hp.1 hp.2)
no goals
case inl
b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ 1 → p * 1 ∣ b
⊢ 1 ∣ b
apply one_dvd