conflicting imports

Stream: general

[Sebastien Gouezel]

When I import two unrelated files (that are not yet in mathlib, so giving a MWE is complicated), I get the error

invalid import: topology.metric_space.closeds
invalid object declaration, environment already has an object named 'metric.metric_space._proof_1'

So it seems my two files define an object with the same name, but of course I never gave this name to anything. In the two files, #check metric.metric_space._proof_1 gives respectively

metric.metric_space._proof_1 : ∀ (x y : nonempty_compacts ?M_1), emetric.Hausdorff_edist (x.val) (y.val) ≠ ⊤

and

metric.metric_space._proof_1 :
  ∀ (x y : completion ?M_1),
    ennreal.of_real
        ((λ (x y : completion ?M_1),
            completion.extension (λ (p : ?M_1 × ?M_1), dist (p.fst) (p.snd)) (completion.prod (x, y)))
           x
           y) =
      ennreal.of_real
        ((λ (x y : completion ?M_1),
            completion.extension (λ (p : ?M_1 × ?M_1), dist (p.fst) (p.snd)) (completion.prod (x, y)))
           x
           y)

These two statements come from instance proofs in the two files. For instance, the first one comes from

instance : metric_space (nonempty_compacts α) :=
emetric_space.to_metric_space $ λx y, Hausdorff_edist_ne_top_of_ne_empty_of_bounded x.2.1 y.2.1
  (bounded_of_compact x.2.2) (bounded_of_compact y.2.2)

If I give a name to the instance, then the problem disappears. Does this mean that one should always give a name to instances, or is there a better way to solve the issue?

[Mario Carneiro]

you should name your instance if it gets a dumb name

[Mario Carneiro]

you can learn the naming algorithm with some trial and error, and predict the dumb names

[Kenny Lau]

like is_ring_hom.is_ring_hom? :P

[Mario Carneiro]

Usually you just notice this stuff when someone (or you) complains about it

[Kenny Lau]

import algebra.field_power
import algebra.group
import category_theory.fully_faithful
import category_theory.instances.measurable_space
import category_theory.instances.topological_spaces

#check int.has_pow
#check units.is_group_hom
#check units.is_monoid_hom
#check category_theory.category_theory.faithful
#check category_theory.category_theory.fully_faithful
#check category_theory.instances.Meas.category_theory.concrete_category
#check category_theory.instances.Top.category_theory.concrete_category