no goals
u : Lean.Level
R✝ : Type ?u.334202
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
n : ℤ
d : ℕ
R : Type u_1
inst✝ : DivisionRing R
a : R
inv✝ : Invertible ↑d
e : a = ↑n * ⅟↑d
⊢ a = Rat.rawCast n d + 0
simp [e, div_eq_mul_inv]