How to use `only` with any_goals and different hypotheses

Stream: new members

[Jakub Nowak]

import Mathlib

example {a b : ℚ} (le : a ≤ b) : True := by
  rcases lt_trichotomy 0 a with ha | rfl | ha
  <;> rcases lt_trichotomy 0 b with hb | rfl | hb

  -- linarith can remove 3 out of 9 cases that are obviously invalid
  -- e.g.
  --   le : a ≤ 0
  --   ha : 0 < a
  -- any_goals linarith

  -- This only removes one goal:
  --   le : a ≤ b
  --   ha : 0 < a
  --   hb : b < 0
  any_goals linarith only [le, ha, hb]

I'm using any_goals linarith to solve some of the hypotheses. Now, in my code I have hundreds of cases and it's painfully slow. I wanted to speed it up with linarith only, but I have a problem as described in the code commends. Any help? Maybe I could write this type of code differently?

[Jakub Nowak]

I know I can make it work, by making sure the names of the hypotheses are the same in every subgoal, e.g. like this:

  rcases lt_trichotomy 0 a with ha | ha | ha
  <;> rcases lt_trichotomy 0 b with hb | hb | hb

Are there other workarounds or proper way?

[Jakub Nowak]

Super ugly, but that works:

import Mathlib

example {a b : ℚ} (le : a ≤ b) : True := by
  have ha := trivial
  have hb := trivial
  rcases lt_trichotomy 0 a with ha | rfl | ha
  <;> rcases lt_trichotomy 0 b with hb | rfl | hb
  any_goals linarith only [le, ha, hb]