Cases does not change assumptions

Stream: mathlib4

[David Ang]

I noticed that sometimes cases does not modify assumptions - is this intentional?

import Mathlib.Data.Polynomial.Degree.Definitions

example (R : Type) [CommRing R] (f : Polynomial R) (h : f.degree = some 0) : f.degree = some 0 := by
  cases f.degree with
  | none => rfl -- fails, because `h` did not get changed
  | some n => rfl -- fails, because `h` did not get changed

I could certainly do revert h and intro h afterwards, or cases h : f.degree and rw [h] at necessary places, but both seem redundant.

[Grant Barkley]

See also https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Matching.20and.20updating.20structure.20fields/near/366563143