linarith and ordinal file

Stream: general

[Sebastien Gouezel]

I have tried to use linarith in the file set_theory/ordinal.lean, but it doesn't work. The minimal example is as follows. Import tactic.linarith at the top of the file. In the middle of the file (Line 996), there is

theorem zero_lt_one : (0 : ordinal) < 1 :=
lt_iff_le_and_ne.2 ⟨zero_le _, ne.symm $ ordinal.one_ne_zero⟩

Now, try pasting a linarith lemma before this lemma. It works. After the lemma, it fails.

lemma works {a b : ℕ} (hab : a ≤ b) (h : b < a) : false :=
begin
  linarith,
end

theorem zero_lt_one : (0 : ordinal) < 1 :=
lt_iff_le_and_ne.2 ⟨zero_le _, ne.symm $ ordinal.one_ne_zero⟩

lemma fails {a b : ℕ} (hab : a ≤ b) (h : b < a) : false :=
begin
  linarith,
end

So I guess linarith gets confused in some way by the ordinal lemma zero_lt_one.

[Rob Lewis]

(deleted)

[Rob Lewis]

#3455

[Sebastien Gouezel]

Thanks!