n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → coprime n m
m : ℕ
mlt : m < n
mdvd : m ∣ n
⊢ m = 1
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → coprime n m
⊢ Prime n
refine' prime_def_lt.mpr ⟨h1, fun m mlt mdvd => _⟩
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → coprime n m
m : ℕ
mlt : m < n
mdvd : m ∣ n
hm : m ≠ 0
⊢ m = 1
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → coprime n m
m : ℕ
mlt : m < n
mdvd : m ∣ n
⊢ m = 1
have hm : m ≠ 0 := by
  rintro rfl
  rw [zero_dvd_iff] at mdvd
  exact mlt.ne' mdvd
no goals
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → coprime n m
m : ℕ
mlt : m < n
mdvd : m ∣ n
hm : m ≠ 0
⊢ m = 1
exact (h m mlt hm).symm.eq_one_of_dvd mdvd
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → coprime n m
mlt : 0 < n
mdvd : 0 ∣ n
⊢ False
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → coprime n m
m : ℕ
mlt : m < n
mdvd : m ∣ n
⊢ m ≠ 0
rintro rfl
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → coprime n m
mlt : 0 < n
mdvd : n = 0
⊢ False
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → coprime n m
mlt : 0 < n
mdvd : 0 ∣ n
⊢ False
rw [zero_dvd_iff] at mdvd
no goals
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → coprime n m
mlt : 0 < n
mdvd : n = 0
⊢ False
exact mlt.ne' mdvd