case mp
k m : ℕ+
h : k ∣ m
⊢ ↑k ∣ ↑m

case mpr
k m : ℕ+
h : ↑k ∣ ↑m
⊢ k ∣ m
k m : ℕ+
⊢ k ∣ m ↔ ↑k ∣ ↑m
constructor <;> intro h
case mp.intro
k w✝ : ℕ+
⊢ ↑k ∣ ↑(k * w✝)
case mp
k m : ℕ+
h : k ∣ m
⊢ ↑k ∣ ↑m
rcases h with ⟨_, rfl⟩
no goals
case mp.intro
k w✝ : ℕ+
⊢ ↑k ∣ ↑(k * w✝)
apply dvd_mul_right
case mpr.intro
k m : ℕ+
a : ℕ
h : ↑m = ↑k * a
⊢ k ∣ m
case mpr
k m : ℕ+
h : ↑k ∣ ↑m
⊢ k ∣ m
rcases h with ⟨a, h⟩
no goals
case mpr.intro
k m : ℕ+
a : ℕ
h : ↑m = ↑k * a
⊢ k ∣ m
cases a with
| zero =>
  contrapose h
  apply ne_zero
| succ n =>
  use ⟨n.succ, n.succ_pos⟩
  rw [← coe_inj, h, mul_coe, mk_coe]
case mpr.intro.zero
k m : ℕ+
h : ¬k ∣ m
⊢ ¬↑m = ↑k * zero
case mpr.intro.zero
k m : ℕ+
h : ↑m = ↑k * zero
⊢ k ∣ m
contrapose h
no goals
case mpr.intro.zero
k m : ℕ+
h : ¬k ∣ m
⊢ ¬↑m = ↑k * zero
apply ne_zero
case mpr.intro.succ
k m : ℕ+
n : ℕ
h : ↑m = ↑k * succ n
⊢ m = k * { val := succ n, property := (_ : 0 < succ n) }
case mpr.intro.succ
k m : ℕ+
n : ℕ
h : ↑m = ↑k * succ n
⊢ k ∣ m
use ⟨n.succ, n.succ_pos⟩
no goals
case mpr.intro.succ
k m : ℕ+
n : ℕ
h : ↑m = ↑k * succ n
⊢ m = k * { val := succ n, property := (_ : 0 < succ n) }
rw [← coe_inj, h, mul_coe, mk_coe]