adding irrelevant hypotheses makes linarith succeed

Stream: mathlib4

[David Renshaw]

linarith is acting in a way that's surprising to me:

import Mathlib.Data.Real.Basic
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

lemma does_not_work (b : ℝ) (hb : b ≤ Real.pi / 4) : b < Real.pi / 2 := by
  linarith -- linarith failed to find a contradiction

-- Same as previous lemma, but has `a` and `haj`, which shouldn't change
-- anything.
lemma does_work (b : ℝ) (hb : b ≤ Real.pi / 4)
    (a : ℝ) (haj : 0 < a ∧ a < Real.pi / 2)
    : b < Real.pi / 2 := by
  linarith -- succeeds

I was hoping that linarith would work for the lemma does_not_work, but I guess the fractions are too fancy for it.
But then in the does_work lemma, which adds an irrelevant hypothesis, the tactic does succeed, which I find surprising.

Is this a bug?

[Scott Morrison]

Looks suspicious to me! set_option trace.linarith true might be helpful to see what is happening.

[David Renshaw]

If I add linarith[Real.pi_pos] in the first lemma, then it does succeed.

[Alex J. Best]

It looks like this is just that linarith doesn't know pi is non-zero until you tell it so (in a roundabout way). The first goal is indeed false if pi were to be zero

[David Renshaw]

ahh

[David Renshaw]

so my haj implies that pi positive