apply_fun Subtype.val at hc
case h
a b c : ℕplus
hc : b = { val := ↑a * ↑c, property := (_ : ↑a * ↑c ≠ 0) }
⊢ ↑b = ↑a * ↑c
case h
a b c : ℕplus
hc : ↑b = ↑{ val := ↑a * ↑c, property := (_ : ↑a * ↑c ≠ 0) }
⊢ ↑b = ↑a * ↑c