case pos
a b : ℤ
b0 : b = 0
⊢ ↑(a /. b).den ∣ b

case neg
a b : ℤ
b0 : ¬b = 0
⊢ ↑(a /. b).den ∣ b
a b : ℤ
⊢ ↑(a /. b).den ∣ b
by_cases b0 : b = 0
case neg.mk'
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = mk' n d
⊢ ↑(mk' n d).den ∣ b
case neg
a b : ℤ
b0 : ¬b = 0
⊢ ↑(a /. b).den ∣ b
cases' e : a /. b with n d h c
case neg.mk'
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a * ↑d = n * b
⊢ ↑(mk' n d).den ∣ b
case neg.mk'
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = mk' n d
⊢ ↑(mk' n d).den ∣ b
rw [num_den', divInt_eq_iff b0 (ne_of_gt (Int.coe_nat_pos.2 (Nat.pos_of_ne_zero h)))] at e
case neg.mk'
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a * ↑d = n * b
⊢ d ∣ Int.natAbs n * Int.natAbs b
case neg.mk'
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a * ↑d = n * b
⊢ ↑(mk' n d).den ∣ b
refine' Int.dvd_natAbs.1 <| Int.coe_nat_dvd.2 <| c.symm.dvd_of_dvd_mul_left _
case neg.mk'
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a * ↑d = n * b
⊢ ↑d ∣ a * ↑d
case neg.mk'
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a * ↑d = n * b
⊢ d ∣ Int.natAbs n * Int.natAbs b
rw [← Int.natAbs_mul, ← Int.coe_nat_dvd, Int.dvd_natAbs, ← e]
no goals
case neg.mk'
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a * ↑d = n * b
⊢ ↑d ∣ a * ↑d
simp
no goals
case pos
a b : ℤ
b0 : b = 0
⊢ ↑(a /. b).den ∣ b
simp [b0]