[GOAL]
α : Type u_1
inst✝ : DivisionRing α
src✝² : DivisionSemiring αᵐᵒᵖ := divisionSemiring α
src✝¹ : Ring αᵐᵒᵖ := ring α
src✝ : RatCast αᵐᵒᵖ := ratCast α
a : ℤ
b : ℕ
hb : b ≠ 0
h : Nat.coprime (Int.natAbs a) b
⊢ unop ↑(Rat.mk' a b) = unop (↑a * (↑b)⁻¹)
[PROOFSTEP]
rw [unop_ratCast, Rat.cast_def, unop_mul, unop_inv, unop_natCast, unop_intCast, Int.commute_cast, div_eq_mul_inv]
[GOAL]
α : Type ?u.3697
inst✝ : DivisionRing α
src✝² : Ring αᵃᵒᵖ := ring α
src✝¹ : GroupWithZero αᵃᵒᵖ := groupWithZero α
src✝ : RatCast αᵃᵒᵖ := ratCast α
a : ℤ
b : ℕ
hb : b ≠ 0
h : Nat.coprime (Int.natAbs a) b
⊢ unop ↑(Rat.mk' a b) = unop (↑a * (↑b)⁻¹)
[PROOFSTEP]
rw [unop_ratCast, Rat.cast_def, unop_mul, unop_inv, unop_natCast, unop_intCast, div_eq_mul_inv]
