case intro
p : ℕ
pp : Prime p
m n : ℕ
hn : p = m * n
⊢ m = 1 ∨ m = p
p : ℕ
pp : Prime p
m : ℕ
hm : m ∣ p
⊢ m = 1 ∨ m = p
obtain ⟨n, hn⟩ := hm
case intro
p : ℕ
pp : Prime p
m n : ℕ
hn : p = m * n
this : IsUnit m ∨ IsUnit n
⊢ m = 1 ∨ m = p
case intro
p : ℕ
pp : Prime p
m n : ℕ
hn : p = m * n
⊢ m = 1 ∨ m = p
have := pp.isUnit_or_isUnit hn
case intro
p : ℕ
pp : Prime p
m n : ℕ
hn : p = m * n
this : m = 1 ∨ n = 1
⊢ m = 1 ∨ m = p
case intro
p : ℕ
pp : Prime p
m n : ℕ
hn : p = m * n
this : IsUnit m ∨ IsUnit n
⊢ m = 1 ∨ m = p
rw [Nat.isUnit_iff, Nat.isUnit_iff] at this
p : ℕ
pp : Prime p
m n : ℕ
hn : p = m * n
this : m = 1 ∨ n = 1
⊢ n = 1 → m = p
case intro
p : ℕ
pp : Prime p
m n : ℕ
hn : p = m * n
this : m = 1 ∨ n = 1
⊢ m = 1 ∨ m = p
apply Or.imp_right _ this
p : ℕ
pp : Prime p
m : ℕ
hn : p = m * 1
this : m = 1 ∨ 1 = 1
⊢ m = p
p : ℕ
pp : Prime p
m n : ℕ
hn : p = m * n
this : m = 1 ∨ n = 1
⊢ n = 1 → m = p
rintro rfl
no goals
p : ℕ
pp : Prime p
m : ℕ
hn : p = m * 1
this : m = 1 ∨ 1 = 1
⊢ m = p
rw [hn, mul_one]