Inconsistent substitution behavior of `cases`

[Kha]

As noticed by @larsk21

example (h : n = 0) : n = 0 := by cases n  -- replaces all occurrences
example (h : n = 0) : n = 0 := by cases h' : n  -- replaces occurrence in target
example (h : id n = 0) : id n = 0 := by cases id n -- replaces occurrence in target
example (h : id n = 0) : id n = 0 := by cases h' : id n -- replaces occurrence in target

[leodemoura]

The last three examples use generalize, and it currently only performs the generalization on the target type. We can change this, and it would be a solid solution for the second example, but not perfect for the last two since the generalization depends on kabstract.

Not sure whether we should do the change now or wait for the Mathlib port since it will impact it.

[digama0]

The mathlib port is going to want the same behavior as lean 3, which FTR is:

example {n} (h : n = 0) : n = 0 := by cases n  -- replaces all occurrences
example {n} (h : n = 0) : n = 0 := by cases h' : n  -- replaces occurrence in target
example {n} (h : id n = 0) : id n = 0 := by cases id n -- replaces all occurrences
example {n} (h : id n = 0) : id n = 0 := by cases h' : id n -- replaces occurrence in target

So if you are considering among all the equally confusing choices, I would suggest this one.