Splitting min or max into cases for inequalities?

Stream: Is there code for X?

[Rowan Williams]

I'm trying to prove this theorem from the Mathematics in Lean C02S04

theorem aux : min a b + c ≤ min (a + c) (b + c) := by
-- I want to have a goal that looks something like
-- min a b + c ≤ (a + c) ∨ min a b + c ≤ (b + c)
-- essentially splitting the min function into the two cases

I know there is a more elegant way to do it without cases, but for my edification, how would I do it in cases? I've tried apply?, but came up empty-handed and apply min_choice only seems to work for direct equality

[Notification Bot]

This topic was moved here from #Is there code for X? > Splitting min or max into cases? by Rowan Williams.

[Andrew Yang]

does rw [min_def (a+c)]; split work?

[Rowan Williams]

Andrew Yang said:

does rw [min_def (a+c)]; split work?

It does! I was trying to apply min_def earlier which probably doesn't work for a much more base-level conceptual lean implementation reason :sweat_smile: Thank you!

[Kevin Buzzard]

You apply implications and rw iff statements.