How do I find a file that imports a list of files?

Stream: mathlib4

[Rémy Degenne]

I want to add that lemma to Mathlib but I don't know where I should put it:

lemma AnalyticAt.re_ofReal {f : ℂ → ℂ} {x : ℝ} (hf : AnalyticAt ℂ f x) :
    AnalyticAt ℝ (fun x : ℝ ↦ (f x).re) x :=
  (Complex.reCLM.analyticAt _).comp (hf.restrictScalars.comp (Complex.ofRealCLM.analyticAt _))

If I import Mathlib in a file and use #find_home! it suggests weird files that seem to import way too much. In order to understand why, I used #min_imports, and it believes that my lemma needs inner product spaces and C* algebras... probably because when you import those files some instances are generated through them instead of through other ways?

By inspecting the proof, I can tell that it in fact needs only Mathlib.Analysis.Analytic.Constructions and Mathlib.Analysis.Complex.Basic (and I checked that it works with those imports). How do I find files that import both, but not much more?

[Damiano Testa]

I have no current solution, but two comments.

1. The various versions of #min_imports rely on the final version of the declaration, so, once typeclass search commits to a path, they do not see if other paths may yield smaller imports.
2. I have observed as well that sometimes there are unnecessary imports reported by #min_imports, but did not get to the bottom of where/why they show up.

[Rémy Degenne]

Thanks for those comments. I think that 1. is what is happening here.
I found a file by looking at "imported by" sections in the documentation and trying to guess a good path (which is not a very robust solution). For this lemma I found the file Mathlib.Analysis.SpecialFunctions.Complex.Analytic.

[Damiano Testa]

Here is a quick implementation of a slow command that finds least upper bounds among imports:

import Mathlib

/--
info: import Mathlib.Analysis.Analytic.Constructions
import Mathlib.Analysis.CStarAlgebra.Classes
import Mathlib.Analysis.InnerProductSpace.Basic
import Init.Data.List.Nat.Pairwise
import Init.Data.List.Sort.Lemmas
-/
#guard_msgs in
#min_imports in
lemma AnalyticAt.re_ofReal {f : ℂ → ℂ} {x : ℝ} (hf : AnalyticAt ℂ f x) :
    AnalyticAt ℝ (fun x : ℝ ↦ (f x).re) x :=
  (Complex.reCLM.analyticAt _).comp (hf.restrictScalars.comp (Complex.ofRealCLM.analyticAt _))

namespace Mathlib.Tactic
open Lean Elab Command
/--
Returns the `NameSet` of modules that
* import all entries of `required` and
* are minimal with respect to this property.

Note.
The imports must all be from `Mathlib`.
-/
-- extracted from `Lean.Name.findHome`
def findOverImports (env : Environment) (required : Array Name) : NameSet := Id.run do
  let imports := env.importGraph.transitiveClosure
  let mut candidates : NameSet := {}
  for (n, i) in imports do
    if required.all fun r => n == r || i.contains r then
      candidates := candidates.insert n
  for c in candidates do
    for i in candidates do
      if imports.find? i |>.getD {} |>.contains c then
        candidates := candidates.erase i
  return candidates

@[inherit_doc findOverImports]
elab "#find_over_imports " ids:ident+ : command => do
  let imports := ids.map (·.getId)
  logInfo m!"{(findOverImports (← getEnv) imports).toArray}"

end Mathlib.Tactic

/--
info: [Mathlib.MeasureTheory.Integral.FundThmCalculus,
 Mathlib.Analysis.Calculus.ParametricIntegral,
 Mathlib.Geometry.Manifold.Instances.Real,
 Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith,
 Mathlib.Topology.MetricSpace.HausdorffDimension,
 Mathlib.Analysis.Complex.UpperHalfPlane.Manifold,
 Mathlib.Analysis.Calculus.ContDiff.WithLp,
 Mathlib.Analysis.Calculus.BumpFunction.Normed,
 Mathlib.Analysis.Complex.RealDeriv,
 Mathlib.Analysis.SpecialFunctions.Exponential]
-/
#guard_msgs in
#find_over_imports
  Mathlib.Analysis.Analytic.Constructions
  Mathlib.Analysis.Complex.Basic

/--
info: [Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances, Mathlib.Analysis.CStarAlgebra.Spectrum]
-/
#guard_msgs in
#find_over_imports
  Mathlib.Analysis.Analytic.Constructions
  Mathlib.Analysis.CStarAlgebra.Classes
  Mathlib.Analysis.InnerProductSpace.Basic
  --Init.Data.List.Nat.Pairwise
  --Init.Data.List.Sort.Lemmas

[Damiano Testa]

I have observed sometimes inconsistencies in how importGraph reports dependencies, so I would not trust the outcome of this command too much, since it is a quick implementation that certainly contains bugs, using something that I am not fully convinced is completely robust.

[Jon Eugster]

@Damiano Testa if you report these inconsistencies in an issue on the importGraph repo, I might take some time at some point to look at it. iirc this part of the code was a quick and dirty hack by Kim and the code even says that its not capturing everything.

[Damiano Testa]

Sorry, I did not mean to blame anyone: it is great that code is available for doing this!

[Damiano Testa]

Sorry, I did not mean to blame anyone: it is great that code is available for doing this!

[Damiano Testa]

I don't have a clear bug report, but it looked now as if cross-repository dependencies might confuse import graph. I'll keep an eye out for something concrete.

[Jon Eugster]

I didnt perceive anything as blame, I just wanted to point out that I'd be interested in looking at such problems, but it's easier to start from something which isn't working even if it's vague or not fully reproducible :)