What to do with small, self-contained lemmas?

Stream: new members

[Calvin Lee]

Hello! I'm working on some localized module proofs that I'd like to upstream into mathlib. In particular that a localized module is a tensor product, which I just finished.
However, I'm not sure if all of the dependencies of my proofs should be upstreamed. For example, I wrote this small lemma about certain tensor products (they also occur if N is a cyclic group) that I'm not sure would be useful to others. Should I try to inline it into my proof? or make it private somehow within the file?
This is the lemma:

section tensor_product
variables {R M N : Type*} [comm_semiring R]  [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N]
lemma tensor_product.every_element_pure_if_absorbing_add
  (x : tensor_product R M N) (h : ∀ (m₁ m₂ : M) (n₁ n₂ : N), (∃ m n, m₁ ⊗ₜ n₁ + m₂ ⊗ₜ n₂ = m ⊗ₜ[R] n)) : (∃ m n, x = m ⊗ₜ n) :=
    tensor_product.induction_on x
    begin
      use [0, 0],
      symmetry,
      exact tensor_product.zero_tmul M 0,
    end
    begin
      intros m n,
      use [m, n],
    end
    begin
      rintros x y ⟨m₁, n₁, h₁⟩ ⟨m₂, n₂, h₂⟩,
      rw [h₁, h₂],
      exact h m₁ m₂ n₁ n₂,
    end
end tensor_product

[Kevin Buzzard]

More smaller proofs is always better than fewer larger ones, surely!

[Kevin Buzzard]

That proof looks so golfable :-)