m n : Nat
x✝ : ↑m ∣ ↑n
a : Int
ae : ↑n = ↑m * a
⊢ m ∣ n
m n : Nat
⊢ ↑m ∣ ↑n ↔ m ∣ n
refine ⟨fun ⟨a, ae⟩ => ?_, fun ⟨k, e⟩ => ⟨k, by rw [e, Int.ofNat_mul]⟩⟩
no goals
m n : Nat
x✝ : ↑m ∣ ↑n
a : Int
ae : ↑n = ↑m * a
⊢ m ∣ n
match Int.le_total a 0 with
| .inl h =>
  have := ae.symm ▸ Int.mul_nonpos_of_nonneg_of_nonpos (ofNat_zero_le _) h
  rw [Nat.le_antisymm (ofNat_le.1 this) (Nat.zero_le _)]
  apply Nat.dvd_zero
| .inr h => match a, eq_ofNat_of_zero_le h with
  | _, ⟨k, rfl⟩ => exact ⟨k, Int.ofNat.inj ae⟩
no goals
m n : Nat
x✝ : m ∣ n
k : Nat
e : n = m * k
⊢ ↑n = ↑m * ↑k
rw [e, Int.ofNat_mul]
m n : Nat
x✝ : ↑m ∣ ↑n
a : Int
ae : ↑n = ↑m * a
h : a ≤ 0
this : ↑n ≤ 0
⊢ m ∣ n
m n : Nat
x✝ : ↑m ∣ ↑n
a : Int
ae : ↑n = ↑m * a
h : a ≤ 0
⊢ m ∣ n
have := ae.symm ▸ Int.mul_nonpos_of_nonneg_of_nonpos (ofNat_zero_le _) h
m n : Nat
x✝ : ↑m ∣ ↑n
a : Int
ae : ↑n = ↑m * a
h : a ≤ 0
this : ↑n ≤ 0
⊢ m ∣ 0
m n : Nat
x✝ : ↑m ∣ ↑n
a : Int
ae : ↑n = ↑m * a
h : a ≤ 0
this : ↑n ≤ 0
⊢ m ∣ n
rw [Nat.le_antisymm (ofNat_le.1 this) (Nat.zero_le _)]
no goals
m n : Nat
x✝ : ↑m ∣ ↑n
a : Int
ae : ↑n = ↑m * a
h : a ≤ 0
this : ↑n ≤ 0
⊢ m ∣ 0
apply Nat.dvd_zero
no goals
m n : Nat
x✝ : ↑m ∣ ↑n
a : Int
ae : ↑n = ↑m * a
h : 0 ≤ a
⊢ m ∣ n
match a, eq_ofNat_of_zero_le h with
| _, ⟨k, rfl⟩ => exact ⟨k, Int.ofNat.inj ae⟩
no goals
m n : Nat
x✝ : ↑m ∣ ↑n
a : Int
k : Nat
ae : ↑n = ↑m * ↑k
h : 0 ≤ ↑k
⊢ m ∣ n
exact ⟨k, Int.ofNat.inj ae⟩