mathlib theorem suggestion to Mathlib.ModelTheory.Syntax

Stream: mathlib4

[Alex Nekrasov]

Hello, everyone! I recently was working on a side project and needed to find a theorem which connects how relabel and varFinset work together on terms. I couldn't find such theorem so I've written it by myself. I suppose that this theorem is general enough to be worth of adding into mathlib, but I don't know whether community needs it, how do add it to mathlib and whether theorem needs any changes. In any case here is the theorem with the proof that I suppose should go into https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/ModelTheory/Syntax.lean:

import Mathlib.ModelTheory.Syntax

open FirstOrder
open FirstOrder.Language

/-- The variable finset of a relabeled term is the image of the original variable finset
under the relabeling function. -/
theorem Term.varFinset_relabel {β : Type*} [DecidableEq β] {L : Language} (t : L.Term ℕ) (f : ℕ → β) :
    (t.relabel f).varFinset = Finset.image f t.varFinset := by
  induction t with
  | var i => simp [Term.relabel, Term.varFinset]
  | func fn ts ih =>
    simp [Term.relabel, Term.varFinset, Finset.biUnion_image]
    refine Finset.biUnion_congr rfl fun a _ => ih a