m n : ℕ
x✝ : ↑m ∣ ↑n
a : ℤ
m0 : m = 0
ae : n = 0
⊢ m ∣ n
m n : ℕ
x✝ : ↑m ∣ ↑n
a : ℤ
ae : ↑n = ↑m * a
m0 : m = 0
⊢ m ∣ n
simp [m0] at ae
no goals
m n : ℕ
x✝ : ↑m ∣ ↑n
a : ℤ
m0 : m = 0
ae : n = 0
⊢ m ∣ n
simp [ae, m0]
case intro
m n : ℕ
x✝ : ↑m ∣ ↑n
a : ℤ
ae : ↑n = ↑m * a
m0l : m > 0
k : ℕ
e : a = ↑k
⊢ m ∣ n
m n : ℕ
x✝ : ↑m ∣ ↑n
a : ℤ
ae : ↑n = ↑m * a
m0l : m > 0
⊢ m ∣ n
cases'
  eq_ofNat_of_zero_le
    (@nonneg_of_mul_nonneg_right ℤ _ m a (by simp [ae.symm]) (by simpa using m0l)) with
  k e
case intro
m n : ℕ
x✝ : ↑m ∣ ↑n
m0l : m > 0
k : ℕ
ae : ↑n = ↑m * ↑k
⊢ m ∣ n
case intro
m n : ℕ
x✝ : ↑m ∣ ↑n
a : ℤ
ae : ↑n = ↑m * a
m0l : m > 0
k : ℕ
e : a = ↑k
⊢ m ∣ n
subst a
no goals
case intro
m n : ℕ
x✝ : ↑m ∣ ↑n
m0l : m > 0
k : ℕ
ae : ↑n = ↑m * ↑k
⊢ m ∣ n
exact ⟨k, Int.ofNat.inj ae⟩
no goals
m n : ℕ
x✝ : ↑m ∣ ↑n
a : ℤ
ae : ↑n = ↑m * a
m0l : m > 0
⊢ 0 ≤ ↑m * a
simp [ae.symm]
no goals
m n : ℕ
x✝ : ↑m ∣ ↑n
a : ℤ
ae : ↑n = ↑m * a
m0l : m > 0
⊢ 0 < ↑m
simpa using m0l
no goals
m n : ℕ
x✝ : m ∣ n
k : ℕ
e : n = m * k
⊢ ↑m * ↑k = ↑n
rw [e, Int.ofNat_mul]