Implicit argument inclusion

Stream: new members

[Frédéric Dupuis]

I'm trying to write the following lemma:

variables {α K : Type*}
  [nondiscrete_normed_field K] [algebra ℝ K] [is_R_or_C K]
  [inner_product_space K α]

lemma parallelogram_law_with_norm {x y : α} :
  ∥x + y∥ * ∥x + y∥ + ∥x - y∥ * ∥x - y∥ = 2 * (∥x∥ * ∥x∥ + ∥y∥ * ∥y∥) := sorry

The problem is that the norm comes from the inner product, but K never shows up in the lemma statement, which means that Lean never finds the relevant has_norm instance. Is there any way to feed that information in manually?

[Frédéric Dupuis]

The reason I'm hoping there's a way to do this without just recopying all the implicit arguments manually is that I have also defined lots of notation for that inner product that I would like to be available here.

[Ruben Van de Velde]

Is this what include K is for?

[Kenny Lau]

yes

[Frédéric Dupuis]

Thanks! Is there also a way to also stop the inclusion after this lemma?

[Bryan Gin-ge Chen]

omit K

[Scott Morrison]

Alternatively, you can just embed the include within a section ... end; it only lasts for that scope. This has the added bonus that sections are helpful for the reader anyway, while omit adds a burden of keeping track of more things.