best way to split into cases

Stream: new members

[Jack J Garzella]

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]

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]

posting your code would help a lot here

[Scott Morrison]

perhaps by_cases h : degree f \le 2, and then interval_cases h?

[Scott Morrison]

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]

Possibly with some unfreezingI magic