Mathlib.Tactic import error

Stream: new members

[Ching-Tsun Chou]

The following sequence of imports:

import Mathlib.Tactic
import Mathlib.Data.Set.Card
import Mathlib.Data.List.OfFn
import Mathlib.Data.Fin.Basic
import Mathlib.Order.Filter.ATTopBot.Basic

produced the following error:

import Mathlib.Order.Filter.ATTopBot.Basic failed, environment already
contains 'Filter.atTop_neBot_iff.match_1' from Mathlib.Order.Filter.AtTopBot.Basic

The error goes away if import Mathlib.Tactic is removed. But I need the tactic linarith, which is not available if I don't import Mathlib.Tactic. Moving import Mathlib.Tactic to last also doesn't help. What is goiing on?

[Ching-Tsun Chou]

OK, limiting the import toimport Mathlib.Tactic.Linarith fixes the problem. But it looks like some file imported by Mathlib.Tactic conflicts with Mathlib.Order.Filter.ATTopBot.Basic.

[Eric Wieser]

You have a typo, ATTopBot should be AtTopBot

[Ching-Tsun Chou]

Ah, that is weird: I've had the same erroneous import in several other files, but I haven't seen any error messages until now.