# Zulip Chat Archive

## Stream: new members

### Topic: best way to split into cases

#### Jack J Garzella (Jul 10 2020 at 02:54):

I am trying to prove a theorem which splits into cases based on the degree of a polynomial. In particular, if `f`

is my polynomial, I have seperate cases for if `degree f`

is `⊥`

, `0`

, `1`

, or `2`

, and `n+3`

, the final case requiring an induction. I have tried a few different approaches and haven't figured out a good way:

- the
`cases`

tactic replaces the instances of`degree f`

in my goal, instead of giving me a term of type`degree f = ⊥`

or`degree f = 0`

, etc. I really need the term of type`degree f = ...`

, so I tried hacking it in there with a variable (e.g.`let n = degree f, have n = degree f, by simp [f], cases ...`

) but I still wasn't able to figure out how to finish the proof this way - the
`by_cases`

tactic gives me the proposition I want, but at the end I am left with a bunch of`¬degree f = ...`

assumptions, making for a messy proof by induction - if I try to switch into term mode and using a match statement like
`exact match ... end`

then Lean can't figure out any of the placeholders

Overall, it just feels clunky to not be able to match in tactic mode, instead having to eliminate on the `option`

type and then three times in the match--is there a better way to do this?

#### Jalex Stark (Jul 10 2020 at 03:05):

Jack J Garzella said:

- the
`by_cases`

tactic gives me the proposition I want, but at the end I am left with a bunch of`¬degree f = ...`

assumptions, making for a messy proof by induction

you can probably prove `3 \le degree f`

by `omega`

#### Jalex Stark (Jul 10 2020 at 03:05):

posting your code would help a lot here

#### Scott Morrison (Jul 10 2020 at 03:28):

perhaps `by_cases h : degree f \le 2`

, and then `interval_cases h`

?

#### Scott Morrison (Jul 10 2020 at 03:29):

You might also find it helpful to introduce a new `n:nat`

, with `h : n = degree f`

, and then do induction on `n`

.

#### Kevin Buzzard (Jul 10 2020 at 14:07):

Possibly with some `unfreezingI`

magic

Last updated: Dec 20 2023 at 11:08 UTC