p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
⊢ Prime p
p : ℕ
⊢ Prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
refine' ⟨fun h => ⟨h.two_le, h.eq_one_or_self_of_dvd⟩, fun h => _⟩
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
⊢ Prime p
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
⊢ Prime p
have h1 := (@one_lt_two ℕ ..).trans_le h.1
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
a b : ℕ
hab : p = a * b
⊢ IsUnit a ∨ IsUnit b
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
⊢ Prime p
refine' ⟨mt Nat.isUnit_iff.mp h1.ne', fun a b hab => _⟩
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
a b : ℕ
hab : p = a * b
⊢ a = 1 ∨ b = 1
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
a b : ℕ
hab : p = a * b
⊢ IsUnit a ∨ IsUnit b
simp only [Nat.isUnit_iff]
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
a b : ℕ
hab : p = a * b
⊢ a = p → b = 1

p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
a b : ℕ
hab : p = a * b
⊢ a ∣ p
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
a b : ℕ
hab : p = a * b
⊢ a = 1 ∨ b = 1
apply Or.imp_right _ (h.2 a _)
a b : ℕ
h : 2 ≤ a ∧ ∀ (m : ℕ), m ∣ a → m = 1 ∨ m = a
h1 : 1 < a
hab : a = a * b
⊢ b = 1
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
a b : ℕ
hab : p = a * b
⊢ a = p → b = 1
rintro rfl
no goals
a b : ℕ
h : 2 ≤ a ∧ ∀ (m : ℕ), m ∣ a → m = 1 ∨ m = a
h1 : 1 < a
hab : a = a * b
⊢ b = 1
rw [← mul_right_inj' (pos_of_gt h1).ne', ← hab, mul_one]
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
a b : ℕ
hab : p = a * b
⊢ a ∣ a * b
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
a b : ℕ
hab : p = a * b
⊢ a ∣ p
rw [hab]
no goals
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
a b : ℕ
hab : p = a * b
⊢ a ∣ a * b
exact dvd_mul_right _ _