Help me find a home for this lemma about ENNReal and enorm

Stream: mathlib4

[Michael Rothgang]

I'm struggling to find a home for this lemma. find_home is not helpful. Any ideas?

import Mathlib
-- TODO: where is a good home for this lemma? minimal imports are
-- Mathlib.Analysis.Normed.{Group.Continuity, Ring.Basic}; #find_home! is not helpful
lemma enorm_ofReal_of_nonneg {a : ℝ} (ha : 0 ≤ a) : ‖ENNReal.ofReal a‖ₑ = ‖a‖ₑ:= by
  simpa using (Real.enorm_of_nonneg ha).symm

[Floris van Doorn]

Mathlib.Analysis.Normed.Group.Basic. This works:

import Mathlib.Analysis.Normed.Group.Basic

lemma enorm_ofReal_of_nonneg {a : ℝ} (ha : 0 ≤ a) : ‖ENNReal.ofReal a‖ₑ = ‖a‖ₑ:= by
  simpa using (Real.enorm_of_nonneg ha).symm

Presumably yoursimp used a later lemma that wasn't needed.

[Floris van Doorn]

(Note: simp [Real.enorm_of_nonneg, ha] or simp_rw [enorm_eq_self, Real.enorm_of_nonneg ha] are also valid proofs)

[Floris van Doorn]

Oh, the issue with #min_imports is that if you import more, the statement uses the instance docs#Real.normedCommRing, even though there are other ways to get an instance...

[Yaël Dillies]

Maybe we are missing a shortcut instance on ℝ?

[Damiano Testa]

This issue of alternative paths found by instance-searches is recurring, but I do not really have a good way of avoiding it. Maybe, adding a flag that computes the LUB of all constants contained in a declarations that do not correspond to instances could be useful?

[Yaël Dillies]

I've just convinced myself that the correct fix to have more shortcut instances. Let me check my prediction...

[Floris van Doorn]

Just brainstorming:

• it might be helpful to also have a command that does #min_imports but ignores all used instances. This will be an underestimate of the imports needed, but will often be right (it's not that common to use an instance from a file without using any lemma from it).
• If it also prints a list of used instances (+ the file they are declared in) that are not imported with this smaller set of imports, it's easy to add imports back.
• You could even imagine automatically going over all places where these now unimported instances are used, and run type-class inference trying to find an instance with the smaller set of imports.

I'm not convinced that it's actually a good investment of time to write this, but that could be a way to deal with this.
I can imagine that it's not just type-class inference that causes #min_imports to overestimate the needed imports, but also something like simp, which could use lemmas that are not actually needed to simplify an expression.

[Michael Rothgang]

Thanks for all the answers, that was really helpful. (My PR is updated now.)