Cancelling terms in inequality

Stream: new members

[Li Xuanji]

Is there a tactic or proof steps that can change the goal state in false_inequality to b ≤ d? I've added a sample of one way to do it manually. I realise this may be a weird request since false_inequality is not true (if it were true, e.g. if we add (h : b ≤ d) as a hypothesis, linarith would solve it) but I sometimes end up in a goal state similar to this due to typos or missing hypotheses (e.g. positivity), and a cancellation tactic would be nice to make the error / missing hypothesis more clear

import Mathlib
-- Note: this theorem is not true!
theorem false_inequality (a b c d e f: ℝ): a + b + c + e + f ≤ a + c + d + e + f := by
  simp
  rw [show a + b + c = b + (a + c) by ac_rfl]
  rw [show a + c + d = d + (a + c) by ac_rfl]
  simp
  -- goal is now: b ≤ d

[Ruben Van de Velde]

gcongr leaves b ≤ c and c ≤ d as goals

[Kevin Buzzard]

theorem false_inequality (a b c d e f: ℝ): a + b + c + e + f ≤ a + c + d + e + f := by
  gcongr ?_ + _ + _
  -- ⊢ a + b + c ≤ a + c + d

goes not quite far enough (as opposed to gcongr which goes too far)