simp match question

Stream: lean4

[Chris B]

I'm a bit confused about when arguments to a match will/won't be reduced during an invocation of simp. The case I originally got stuck on involves a pattern match that's expecting (ofNat x, ofNat y), but is given (ofNat x, nat lit):

/-
Unfolds to (Int.ofNat (n / 0)) and closes the goal since the denominator fits the match's structure of
(ofNat n, ofNat m) => (ofNat (n / d))
-/
example (n : Nat) : Int.div (Int.ofNat n) (Int.ofNat 0) = (Int.ofNat (n / 0)) := by
simp [Int.div]

/-
Doesn't unfold, seems to be because of the literal `0` becoming (@OfNat.ofNat Int 0 (@Int.instOfNatInt 0)),
which isn't immediately of the shape Int.ofNat _
-/
example (n : Nat) : Int.div (Int.ofNat n) 0 = (Int.ofNat (n / 0)) := by
simp [Int.div]
rfl

But the same set of circumstances passed to Nat.mul reduces in both cases despite the match also requiring the shape (OfNat x, OfNat y):

example (n : Nat) : Int.mul (Int.ofNat n) (Int.ofNat 0) = Int.ofNat (n * 0) := by
simp [Int.mul]

/-
lit 0 becomes  (@OfNat.ofNat.{0} Int 0 (@Int.instOfNatInt 0)) but still reduces and solves
-/
example (n : Nat) : Int.mul (Int.ofNat n) 0 = (Int.ofNat (n * 0)) := by
simp [Int.mul]
rfl

Also, when a match is reduced to the RHS of some arm, is there any way to get the goal view to display the RHS of the arm that hit instead of continuing to display the whole match?