Derivative of transition map is in GL

Stream: Is there code for X?

[Dominic Steinitz]

So far I have this but maybe there is better way of approaching it

import Mathlib

open SmoothManifoldWithCorners
open scoped Manifold

noncomputable
def GLBundle {n : ℕ} : FiberBundleCore
  (atlas (EuclideanSpace ℝ (Fin n)) (Metric.sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1))
  (Metric.sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1)
  (GL (Fin n) ℝ)
  where

  baseSet i := i.1.source
  isOpen_baseSet i := i.1.open_source
  indexAt := achart (EuclideanSpace ℝ (Fin n))
  mem_baseSet_at := mem_chart_source (EuclideanSpace ℝ (Fin n))

  coordChange i j x v := by
    let ii := i.1
    have h1 : i.1 ∈ atlas (EuclideanSpace ℝ (Fin n)) ↑(Metric.sphere 0 1) := i.2
    have h2 : j.1 ∈ atlas (EuclideanSpace ℝ (Fin n)) ↑(Metric.sphere 0 1) := j.2
    have h3 : (i.1).symm ≫ₕ j.1 ∈ ((contDiffGroupoid ⊤) (𝓡 n)) := HasGroupoid.compatible h1 h2
    have h4 : (j.1).symm ≫ₕ i.1 ∈ ((contDiffGroupoid ⊤) (𝓡 n)) := HasGroupoid.compatible h2 h1

    let tl := (fderiv ℝ (j.1 ∘ (i.1).symm) (i.1 x)).toLinearMap
    let B := Pi.basisFun ℝ (Fin n)
    let tm := LinearMap.toMatrix B B tl
    let (ntm : Matrix (Fin n) (Fin n) ℝ) := (tm * v)
    -- We need a proof that ntm has non-zero determinant
    exact (sorry : GL (Fin n) ℝ)

  coordChange_self := sorry

  continuousOn_coordChange := sorry

  coordChange_comp := sorry