case hn
m n : ℤ
hn : n ≠ 0
⊢ ↑n ≠ 0

m n : ℤ
hn : ↑n ≠ 0
⊢ (↑m / ↑n).den = 1 ↔ n ∣ m
m n : ℤ
hn : n ≠ 0
⊢ (↑m / ↑n).den = 1 ↔ n ∣ m
replace hn : (n : ℚ) ≠ 0
case mp
m n : ℤ
hn : ↑n ≠ 0
⊢ (↑m / ↑n).den = 1 → n ∣ m

case mpr
m n : ℤ
hn : ↑n ≠ 0
⊢ n ∣ m → (↑m / ↑n).den = 1
m n : ℤ
hn : ↑n ≠ 0
⊢ (↑m / ↑n).den = 1 ↔ n ∣ m
constructor
no goals
case hn
m n : ℤ
hn : n ≠ 0
⊢ ↑n ≠ 0
rwa [Ne.def, ← Int.cast_zero, coe_int_inj]
case mp
m n : ℤ
hn : ↑n ≠ 0
h : (↑m / ↑n).den = 1
⊢ n ∣ m
case mp
m n : ℤ
hn : ↑n ≠ 0
⊢ (↑m / ↑n).den = 1 → n ∣ m
intro h
case mp
m n : ℤ
hn : ↑n ≠ 0
h : (↑m / ↑n).den = 1
⊢ m = n * (↑m / ↑n).num
case mp
m n : ℤ
hn : ↑n ≠ 0
h : (↑m / ↑n).den = 1
⊢ n ∣ m
use ((m : ℚ) / n).num
case mp
m n : ℤ
hn : ↑n ≠ 0
h : (↑m / ↑n).den = 1
hk : ↑(↑m / ↑n).num = ↑m / ↑n
⊢ m = n * (↑m / ↑n).num
case mp
m n : ℤ
hn : ↑n ≠ 0
h : (↑m / ↑n).den = 1
⊢ m = n * (↑m / ↑n).num
have hk := Rat.coe_int_num_of_den_eq_one h
case mp
m n : ℤ
hn : ↑n ≠ 0
h : (↑m / ↑n).den = 1
hk : ↑((↑m / ↑n).num * n) = ↑m
⊢ m = n * (↑m / ↑n).num
case mp
m n : ℤ
hn : ↑n ≠ 0
h : (↑m / ↑n).den = 1
hk : ↑(↑m / ↑n).num = ↑m / ↑n
⊢ m = n * (↑m / ↑n).num
simp_rw [eq_div_iff_mul_eq hn, ← Int.cast_mul] at hk
no goals
case mp
m n : ℤ
hn : ↑n ≠ 0
h : (↑m / ↑n).den = 1
hk : ↑((↑m / ↑n).num * n) = ↑m
⊢ m = n * (↑m / ↑n).num
rwa [mul_comm, eq_comm, coe_int_inj] at hk
case mpr.intro
n : ℤ
hn : ↑n ≠ 0
d : ℤ
⊢ (↑(n * d) / ↑n).den = 1
case mpr
m n : ℤ
hn : ↑n ≠ 0
⊢ n ∣ m → (↑m / ↑n).den = 1
rintro ⟨d, rfl⟩
no goals
case mpr.intro
n : ℤ
hn : ↑n ≠ 0
d : ℤ
⊢ (↑(n * d) / ↑n).den = 1
rw [Int.cast_mul, mul_comm, mul_div_cancel _ hn, Rat.coe_int_den]