cases b with
| mk nb db =>
  simp at *
  exact And.intro hnum hdenom
case mk
b : Fraction
na da : ℤ
denom_Neq_zero✝ : da ≠ 0
hnum : { num := na, denom := da, denom_Neq_zero := denom_Neq_zero✝ }.num = b.num
hdenom : { num := na, denom := da, denom_Neq_zero := denom_Neq_zero✝ }.denom = b.denom
⊢ { num := na, denom := da, denom_Neq_zero := denom_Neq_zero✝ } = b
no goals