Local definition in section in terms of many variables

Stream: new members

[Jim Portegies]

Hi all,

What is the recommended approach in the following situation:

I'm having a section with many variables, for the example let's say they're all natural numbers, and throughout the section I would like to have access to a new constant that depends in a fixed way on these variables. Naively it would be something like this:

section many_variables

variable {a b c d e f g h : ℕ}

def σ : ℕ := a + b + c + d + e + f + g + h

lemma σ_eq : σ = a + b + c + d + e + f + g + h := by
  rfl

end many_variables

Now I get an error already in the statement of the lemma ("don't know how to synthesize implicit argument 'h'"), which I understand why I get. Yet my intended behavior is different, something that I _could_ achieve with the following code using a propositional equality, but I'm not sure if that is acceptable. The reason I would like this in the first place is that I would like to get my expressions relatively concise in computations that I'm doing. Any thoughts/recommendations?

section many_variables_2

variable {a b c d e f g h : ℕ}
variable {σ : ℕ}
variable (hσ : σ = a + b + c + d + e + f + g + h)

lemma σ_eq_again : σ = a + b + c + d + e + f + g + h := hσ

end many_variables_2

[Edward van de Meent]

use notation?

[Edward van de Meent]

you can take a look at how it is done in the #Carleson project; look for the namespace ShortVariables

[Edward van de Meent]

notice the set_option hygiene false

[Jim Portegies]

Thanks! I will follow that approach as well then

[Jim Portegies]

(as it is actually for the #Carleson project indeed)