a : ℤ
ha0 : 0 < a
⊢ (↑1 / ↑a).num = 1
a : ℤ
ha0 : 0 < a
⊢ (↑a)⁻¹.num = 1
rw [← ofInt_eq_cast, ofInt, mk_eq_divInt, Rat.inv_def', divInt_eq_div, Nat.cast_one]
a : ℤ
ha0 : 0 < a
⊢ Nat.coprime (Int.natAbs 1) (Int.natAbs a)
a : ℤ
ha0 : 0 < a
⊢ (↑1 / ↑a).num = 1
apply num_div_eq_of_coprime ha0
a : ℤ
ha0 : 0 < a
⊢ Nat.coprime 1 (Int.natAbs a)
a : ℤ
ha0 : 0 < a
⊢ Nat.coprime (Int.natAbs 1) (Int.natAbs a)
rw [Int.natAbs_one]
no goals
a : ℤ
ha0 : 0 < a
⊢ Nat.coprime 1 (Int.natAbs a)
exact Nat.coprime_one_left _