case 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).num ∣ a
a b : ℤ
b0 : b ≠ 0
⊢ (a /. b).num ∣ a
cases' e : a /. b with n d h c
case 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).num ∣ a
case 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).num ∣ a
rw [Rat.num_den', divInt_eq_iff b0 (ne_of_gt (Int.coe_nat_pos.2 (Nat.pos_of_ne_zero h)))] at e
case mk'
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a * ↑d = n * b
⊢ Int.natAbs n ∣ Int.natAbs a * d
case 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).num ∣ a
refine' Int.natAbs_dvd.1 <| Int.dvd_natAbs.1 <| Int.coe_nat_dvd.2 <| c.dvd_of_dvd_mul_right _
case mk'
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a * ↑d = n * b
this : Int.natAbs (a * ↑d) = Int.natAbs (n * b)
⊢ Int.natAbs n ∣ Int.natAbs a * d
case mk'
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a * ↑d = n * b
⊢ Int.natAbs n ∣ Int.natAbs a * d
have := congr_arg Int.natAbs e
case mk'
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a * ↑d = n * b
this : Int.natAbs a * d = Int.natAbs n * Int.natAbs b
⊢ Int.natAbs n ∣ Int.natAbs a * d
case mk'
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a * ↑d = n * b
this : Int.natAbs (a * ↑d) = Int.natAbs (n * b)
⊢ Int.natAbs n ∣ Int.natAbs a * d
simp only [Int.natAbs_mul, Int.natAbs_ofNat] at this
no goals
case mk'
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a * ↑d = n * b
this : Int.natAbs a * d = Int.natAbs n * Int.natAbs b
⊢ Int.natAbs n ∣ Int.natAbs a * d
simp [this]