mathlib3

c4fbb6ff - refactor(data/real/ereal): replace `.cases` with `.rec` (#9321)

refactor(data/real/ereal): replace `.cases` with `.rec` (#9321) This provides a nicer spelling than the pile of `rfl`s we use with the old `ereal.cases`, as follows: ```diff -rcases x.cases with rfl|⟨y, rfl⟩|rfl, +induction x using ereal.rec with y, ``` As a bonus, the subgoals now end up with names matching the hypotheses.