Commit 2023-09-12 22:27 789bd510

feat(Util/Imports): add #find_home! to exclude current module (#7075) Add the ! flag to #find_home that excludes the current module as potential home. This change is analogous to #7025. This behaviour can be desirable when the lemma depends on explicit lemmas in the current file that you also want to move. There is also the possibility that the proof of the lemma you want to move uses an auto-generated lemma and that auto-generated lemma would be auto-generated also in the earlier file. Here is an example:

--  this takes place in a new file `Mathlib/Algebra/NewFile.lean`
import Mathlib.Util.Imports
import Mathlib.Algebra.Group.Prod
lemma withSimp {A} [Zero A] (a : A) (h : a = 0) :
    (a, 0) = 0 := by
  simp only [h, Prod.mk_eq_zero]
lemma withRw {A} [Zero A] (a : A) (h : a = 0) :
    (a, 0) = 0 := by
  rw [h, Prod.mk_eq_zero, eq_self, eq_self, true_and]
  trivial
#print withSimp  -- blah blah `Mathlib.Algebra.NewFile._auxLemma.1`
#print withRw    -- only "visible" lemmas
#find_home  withSimp  -- `Mathlib.Algebra.NewFile`
#find_home! withSimp  -- `Mathlib.Algebra.Group.Prod`
#find_home  withRw    -- `Mathlib.Algebra.Group.Prod`