Please move the other variables to this section, and also don't break lines immediately after the keyword variable.

I don't know what you mean here. If I move the other global(?) variables into this section then they are not visible in the other sections. I have not broken lines by doing this

variable {B : Type*}
  {E : B → Type*}
  [∀ x, NormedAddCommGroup (E x)]

section tangentSpaceEquiv

variable [∀ x, NormedSpace ℝ (E x)]

Maybe there is a formatter for Lean to avoid problems like this?

What I mean is that
instead of

variable
  [∀ x, NormedSpace ℝ (E x)]

it must be:

variable [∀ x, NormedSpace ℝ (E x)]

That bit is done :-)

Can you explain what does this structure do? Preferably as a doc comment.

Can you rename this section or remove the name entirely?

Can you please explain a bit what the proof strategy here is? Why do you need this lemma? It is a bit unclear at the moment.

The idea is that there are two equivalent ways of defining a bilinear positive definite form: 1) pull back the inner product on $\mathbb{R}^n$ via the inverse trivialisation 2) push forward vectors and then apply the inner product on $\mathbb{R}^n$.

It turns out that using (1) makes proving smoothness straightforward and g_bilin_1_smooth_on_chart proves that locally g_bilini_1 is smooth (the trick is to make the set on which this is true small enough hence the intersection ((trivializationAt F E i).baseSet ∩ (chartAt HB i).source)). This can then be used to prove global smoothness via a partition of unity.

However it is not so clear (to me at any rate) how one uses (1) to prove positive definiteness. This is where (2) comes in. With this definition, it is straightforward to prove positivity, definiteness and symmetry.

I then prove that the two definitions are equal which allows me to prove that (1) is symmetric positive and definite.

But one is still not done. Mathlib's definition requires von Neumann boundedness which is true for finite dimensional manifolds.

I should add a lot of the code, and you comment tangentially (pun intended) about this, is to do with the fact that we have two norms and Mathlib via type classes only allows one so I created a structure VectorSpaceAux with its own norm and showed that they are equivalent (generate the same topology). It is well known that all norms on finite dimensional metric spaces are equivalent but it seems Mathlib does things differently.

Here's a bit more detail:

Mathlib's type class system doesn't support having multiple norm structures on the same type.
As the mathlib documentation states (Analysis.NormedSpace.FiniteDimension):

"The fact that all norms are equivalent is not written explicitly, as it would mean having
two norms on a single space, which is not the way type classes work. However, if one has a
finite-dimensional vector space E with a norm, and a copy E' of this type with another
norm, then the identities from E to E' and from E' to E are continuous thanks to
LinearMap.continuous_of_finiteDimensional. This gives the desired norm equivalence."

See
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Normed/Module/FiniteDimension.html

What this description elides is that "this gives the desired norm equivalence" requires
creating this auxiliary type plus substantial additional work (see tangentSpaceEquiv,
withSeminormsOfBilinearForm, and aux_tvs) to establish the equivalence and derive the needed
WithSeminorms and IsVonNBounded properties.

In classical mathematics, "all norms on a finite-dimensional space are equivalent" is a
one-line citation. In Mathlib, making this work requires explicit construction and proof.

I did toy with the idea of a blog post on the whole proof but I wanted feedback on it first (for which I am very grateful) and I am now distracted with trying to proved that the exponential map on Lie algebras is smooth.

I fear I am in danger of writing a blog post here and will stop now but please ask anything if I have been insufficiently clear.

This seems out of scope of this file, can you move it to a different file? Perhaps a file related to ContinuousLinearMap? All lemmas related to this also need to be moved.

These need to be let instead of letIs since this is not a definition.