[Merged by Bors] - feat: Finset.nsmul_inf'

[madvorak]

---

I didn't really know where to put it.

When I paste

lemma Finset.nsmul_inf' {α β : Type*} [LinearOrderedAddCommMonoid β] {s : Finset α}
    (hs : s.Nonempty) (f : α → β) (n : ℕ) :
    s.inf' hs (fun a => n • f a) = n • s.inf' hs f := by
  if nz : n = 0 then
    rw [nz]
    simp_rw [zero_smul]
    apply Finset.inf'_const
  else
    obtain ⟨d, hd, hfd⟩ := Finset.exists_mem_eq_inf' hs f
    obtain ⟨dₙ, hnₙ, hfdₙ⟩ := Finset.exists_mem_eq_inf' hs (fun a => n • f a)
    have key : n • f dₙ = n • f d
    · apply eq_of_ge_of_not_gt
      · rw [← hfd]
        exact nsmul_le_nsmul_right (Finset.inf'_le f hnₙ) n
      · rw [not_lt, ← hfdₙ]
        exact Finset.inf'_le (fun a => n • f a) hd
    rw [hfd, hfdₙ, key]

into the root then #find_home gives me:

[Mathlib.Algebra.BigOperators.Finprod,
 Mathlib.Algebra.Periodic,
 Mathlib.SetTheory.Cardinal.Basic,
 Mathlib.Dynamics.BirkhoffSum.Average,
 Mathlib.GroupTheory.Submonoid.Pointwise,
 Mathlib.Order.Filter.Pointwise,
 Mathlib.Algebra.Module.BigOperators,
 Mathlib.RingTheory.Multiplicity,
 Mathlib.Algebra.Tropical.BigOperators,
 Mathlib.Algebra.BigOperators.Intervals,
 Mathlib.Algebra.Module.Submodule.Basic,
 Mathlib.Deprecated.Subgroup,
 Mathlib.Order.Filter.Germ,
 Mathlib.Topology.Support,
 Mathlib.Data.Finsupp.Basic,
 Mathlib.Topology.Bornology.Absorbs,
 Mathlib.Algebra.Order.Rearrangement,
 Mathlib.MeasureTheory.MeasurableSpace.Basic,
 Mathlib.Data.Rat.Star,
 Mathlib.Algebra.GroupWithZero.NonZeroDivisors,
 Mathlib.CategoryTheory.Galois.Basic,
 Mathlib.Data.DFinsupp.Basic,
 Mathlib.Data.Set.Pointwise.Finite,
 Mathlib.GroupTheory.Subgroup.Finite,
 Mathlib.Combinatorics.SimpleGraph.Regularity.Energy,
 Mathlib.Data.Finsupp.Pointwise,
 Mathlib.RingTheory.NonUnitalSubring.Basic,
 Mathlib.GroupTheory.Coprod.Basic,
 Mathlib.Data.Holor,
 Mathlib.CategoryTheory.Preadditive.Basic,
 Mathlib.RingTheory.Subsemiring.Basic]

[eric-wieser]

I think with the new proof you can probably find a better home for the lemma.

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style