Bug in push_neg

Stream: mathlib4

[Yury G. Kudryashov]

Here is an #mwe:

import Mathlib.Tactic.PushNeg

example {α} [Preorder α] (m n : α) (h : ¬(∃ k : ℕ, m ≤ n)) : m ≤ n := by
  push_neg at  h

While α is not a LinearOrder, push_neg still tries to rewrite using [not_le] and fails.

[Yury G. Kudryashov]

This used to work in Lean 3 (encountered for α = Filter β in a file I'm porting).

[Yury G. Kudryashov]

@Frédéric Dupuis @Mario Carneiro you made most contributions to this file :up:

[Frédéric Dupuis]

I'll have a look right now. If I don't manage to fix it tonight, it might be a while before I have time again though.

[Jireh Loreaux]

@Frédéric Dupuis If you don't fix it tonight I'll take a look tomorrow

[Frédéric Dupuis]

!4#2095

[Notification Bot]

This topic was moved here from #lean4 > Bug in push_neg by Yury G. Kudryashov.