q : ℚ
⊢ q.num /. ↑q.den * (↑q.den /. 1) = q.num /. 1
q : ℚ
⊢ q * ↑q.den = ↑q.num
suffices (q.num /. ↑q.den) * (↑q.den /. 1) = q.num /. 1 by
  conv => pattern (occs := 1)q ; (rw [← @num_den q])
  simp only [coe_int_eq_divInt, coe_nat_eq_divInt, num_den] at this ⊢; assumption
q : ℚ
this : ↑q.den ≠ 0
⊢ q.num /. ↑q.den * (↑q.den /. 1) = q.num /. 1
q : ℚ
⊢ q.num /. ↑q.den * (↑q.den /. 1) = q.num /. 1
have : (q.den : ℤ) ≠ 0 := ne_of_gt (by exact_mod_cast q.pos)
no goals
q : ℚ
this : ↑q.den ≠ 0
⊢ q.num /. ↑q.den * (↑q.den /. 1) = q.num /. 1
rw [Rat.mul_def' this one_ne_zero, mul_comm (q.den : ℤ) 1, divInt_mul_right this]
q : ℚ
this : q.num /. ↑q.den * (↑q.den /. 1) = q.num /. 1
⊢ q.num /. ↑q.den * ↑q.den = ↑q.num
q : ℚ
this : q.num /. ↑q.den * (↑q.den /. 1) = q.num /. 1
⊢ q * ↑q.den = ↑q.num
conv => pattern (occs := 1)q ; (rw [← @num_den q])
q : ℚ
this : q * (↑q.den /. 1) = q.num /. 1
⊢ q * (↑q.den /. 1) = q.num /. 1
q : ℚ
this : q.num /. ↑q.den * (↑q.den /. 1) = q.num /. 1
⊢ q.num /. ↑q.den * ↑q.den = ↑q.num
simp only [coe_int_eq_divInt, coe_nat_eq_divInt, num_den] at this ⊢
no goals
q : ℚ
this : q * (↑q.den /. 1) = q.num /. 1
⊢ q * (↑q.den /. 1) = q.num /. 1
assumption
no goals
q : ℚ
⊢ 0 < ↑q.den
exact_mod_cast q.pos