Command to find a place for lemmas in Mathlib

Stream: mathlib4

[Vasily Ilin]

Is there a command that I can run on a piece of Lean code that would tell me where in Mathlib this piece of code can go? For example, I tried to put this in Mathlib/Analysis/Normed/Module/Basic.lean but it causes a cycle of imports.

import Mathlib

variable {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G] [Nontrivial G]

lemma Metric.diam_sphere_eq (x : G) {r : ℝ} (hr : 0 ≤ r) :
    diam (sphere x r) = 2 * r := by
  apply le_antisymm
    (diam_mono sphere_subset_closedBall isBounded_closedBall |>.trans <| diam_closedBall hr)
  obtain ⟨y, hy⟩ := exists_ne (0 : G)
  rw [← norm_ne_zero_iff] at hy
  calc
    2 * r = dist (x + r • ‖y‖⁻¹ • y) (x - r • ‖y‖⁻¹ • y) := by
      simp [dist_eq_norm, ← two_nsmul, ← smul_assoc, norm_smul, abs_of_nonneg hr, mul_assoc, hy]
    _ ≤ diam (sphere x r) := by
      apply dist_le_diam_of_mem isBounded_sphere <;> simp [norm_smul, hy, abs_of_nonneg hr]

lemma Metric.diam_closedBall_eq (x : G) {r : ℝ} (hr : 0 ≤ r) :
    diam (closedBall x r) = 2 * r :=
  le_antisymm (diam_closedBall hr) <|
    diam_sphere_eq x hr |>.symm.le.trans <| diam_mono sphere_subset_closedBall isBounded_closedBall

lemma Metric.diam_ball_eq (x : G) {r : ℝ} (hr : 0 < r) :
    diam (ball x r) = 2 * r := by
  rw [← diam_closure, closure_ball _ hr.ne', diam_closedBall_eq _ hr.le]

[Chris Henson]

https://leanprover-community.github.io/mathlib4_docs/ImportGraph/Meta.html#%C2%ABcommand#find_home!_%C2%BB

[Damiano Testa]

As Chris says, #find_home! is a good choice. However, it has not been revised after the change to the module system and I do not know if it still works as intended.

[Damiano Testa]

Actually, looking at the blame, it seems that Kim did commit a change after the module system, so if it does not work as intended, please report it! :slight_smile: