p a : ℕ
hp : Prime p
a1 : a ≠ 1
⊢ a ∣ p → p = a
p a : ℕ
hp : Prime p
a1 : a ≠ 1
⊢ a ∣ p ↔ p = a
refine'
  ⟨_, by
    rintro rfl
    rfl⟩
case intro
a : ℕ
a1 : a ≠ 1
j : ℕ
hp : Prime (a * j)
⊢ a * j = a
p a : ℕ
hp : Prime p
a1 : a ≠ 1
⊢ a ∣ p → p = a
rintro ⟨j, rfl⟩
case intro.inl.intro
a : ℕ
a1 : a ≠ 1
left✝ : Prime a
hp : Prime (a * 1)
⊢ a * 1 = a

case intro.inr.intro
j : ℕ
left✝ : Prime j
a1 : 1 ≠ 1
hp : Prime (1 * j)
⊢ 1 * j = 1
case intro
a : ℕ
a1 : a ≠ 1
j : ℕ
hp : Prime (a * j)
⊢ a * j = a
rcases prime_mul_iff.mp hp with (⟨_, rfl⟩ | ⟨_, rfl⟩)
p : ℕ
hp : Prime p
a1 : p ≠ 1
⊢ p ∣ p
p a : ℕ
hp : Prime p
a1 : a ≠ 1
⊢ p = a → a ∣ p
rintro rfl
no goals
p : ℕ
hp : Prime p
a1 : p ≠ 1
⊢ p ∣ p
rfl
no goals
case intro.inl.intro
a : ℕ
a1 : a ≠ 1
left✝ : Prime a
hp : Prime (a * 1)
⊢ a * 1 = a
exact mul_one _
no goals
case intro.inr.intro
j : ℕ
left✝ : Prime j
a1 : 1 ≠ 1
hp : Prime (1 * j)
⊢ 1 * j = 1
exact (a1 rfl).elim