linter bail?

Stream: general

[Johan Commelin]

#lint-
/- The `ge_or_gt` linter reports: -/
/- The following declarations use ≥/>, probably in a way where we would prefer
  to use ≤/< instead. See note [nolint_ge] for more information. -/
#print Mbar_bdd.transition_eq /- the type contains ≥/>. Use ≤/< instead. -/

#print Mbar_bdd.transition_eq
----
@[_refl_lemma]
theorem Mbar_bdd.transition_eq : ∀ {r' : ℝ≥0} {S : Fintype} {c : ℝ≥0} {M N : ℕ} (h : M ≤ N) (F : Mbar_bdd r' S c N) (s : ↥S)
(i : fin (M + 1)), (Mbar_bdd.transition r' h F).to_fun s i = F.to_fun s (⇑(fin.cast_le _) i) :=
λ {r' : ℝ≥0} {S : Fintype} {c : ℝ≥0} {M N : ℕ} (h : M ≤ N) (F : Mbar_bdd r' S c N) (s : ↥S)
(i : fin (M + 1)), rfl

[Johan Commelin]

(This is from LTE)

[Kevin Buzzard]

What does it look like with pp.all on?