case inl
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ sqrt p → ¬m ∣ p
this : ∀ {m k : ℕ}, m ≤ k → 1 < m → p ≠ m * k
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ : m ∣ p
k : ℕ
e : p = m * k
mk : m ≤ k
⊢ False

case inr
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ sqrt p → ¬m ∣ p
this : ∀ {m k : ℕ}, m ≤ k → 1 < m → p ≠ m * k
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ : m ∣ p
k : ℕ
e : p = m * k
km : k ≤ m
⊢ False
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ sqrt p → ¬m ∣ p
this : ∀ {m k : ℕ}, m ≤ k → 1 < m → p ≠ m * k
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ : m ∣ p
k : ℕ
e : p = m * k
⊢ False
cases' le_total m k with mk km
no goals
case inl
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ sqrt p → ¬m ∣ p
this : ∀ {m k : ℕ}, m ≤ k → 1 < m → p ≠ m * k
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ : m ∣ p
k : ℕ
e : p = m * k
mk : m ≤ k
⊢ False
exact this mk m2 e
case inr
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ sqrt p → ¬m ∣ p
this : ∀ {m k : ℕ}, m ≤ k → 1 < m → p ≠ m * k
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ : m ∣ p
k : ℕ
e : p = k * m
km : k ≤ m
⊢ False
case inr
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ sqrt p → ¬m ∣ p
this : ∀ {m k : ℕ}, m ≤ k → 1 < m → p ≠ m * k
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ : m ∣ p
k : ℕ
e : p = m * k
km : k ≤ m
⊢ False
rw [mul_comm] at e
case inr
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ sqrt p → ¬m ∣ p
this : ∀ {m k : ℕ}, m ≤ k → 1 < m → p ≠ m * k
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ : m ∣ p
k : ℕ
e : p = k * m
km : k ≤ m
⊢ 1 * m < k * m
case inr
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ sqrt p → ¬m ∣ p
this : ∀ {m k : ℕ}, m ≤ k → 1 < m → p ≠ m * k
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ : m ∣ p
k : ℕ
e : p = k * m
km : k ≤ m
⊢ False
refine' this km (lt_of_mul_lt_mul_right _ (zero_le m)) e
no goals
case inr
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ sqrt p → ¬m ∣ p
this : ∀ {m k : ℕ}, m ≤ k → 1 < m → p ≠ m * k
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ : m ∣ p
k : ℕ
e : p = k * m
km : k ≤ m
⊢ 1 * m < k * m
rwa [one_mul, ← e]