Simple theorem of + and ≤

Stream: Is there code for X?

[Iván Renison]

Hi, do you know if is there a simple way to probe this lemma?

example (a b c d : ℝ) : 0 ≤ a + b + c + d ↔ -b - c ≤ a + d := by
  sorry

Ideally a way that can easily be used inline in a rewrite. The only way I was able to probe it is with a lot of rewrites, but it is not nice

[Anthony Wang]

This works:

import Mathlib

example (a b c d : ℝ) : 0 ≤ a + b + c + d ↔ -b - c ≤ a + d := by
  grind

[Anthony Wang]

Or

import Mathlib

example (a b c d : ℝ) : 0 ≤ a + b + c + d ↔ -b - c ≤ a + d := by
  constructor <;> intro _; linarith

[Iván Renison]

Okay, and for doing it inline I should do rw [show 0 ≤ a + b + c + d ↔ -b - c ≤ a + d by grind]?

[Snir Broshi]

Iván Renison said:

Okay, and for doing it inline I should do rw [show 0 ≤ a + b + c + d ↔ -b - c ≤ a + d by grind]?

You can also suffices -b - c ≤ a + d by grind if your goal is the LHS

[Iván Renison]

Thank you