PhyslibAlpha.ClassicalFieldTheory.Local.JetPointFiber

Imports

/-
Copyright (c) 2026 Juan Jose Fernandez Morales. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Juan Jose Fernandez Morales
-/
module

public import PhyslibAlpha.ClassicalFieldTheory.Local.JetPoint

Fiber directions on jet points

i. Overview

This module adds the affine fiber-direction structure on coordinate-level jet points.

At this stage, it introduces:

fiber-coordinate data on jet points,

affine translation and line maps in the jet fiber,

and the jet-fiber direction determined by a field.

ii. Key results

ClassicalFieldTheory.Local.JetFiberData

ClassicalFieldTheory.Local.JetPoint.addFiber

ClassicalFieldTheory.Local.JetPoint.lineMap

ClassicalFieldTheory.Local.jetDirectionAt

iii. Table of contents

A. Fiber-coordinate data

B. Affine fiber structure on jet points

C. Fiber directions determined by fields

iv. References

@[expose] public section

A. Fiber-coordinate data

Fiber-coordinate data for jet points of order k. This records only the coordinates u^a_I, not the base point in Space d.

The fiber coordinates indexed by all derivative indices of order at most k.

structure JetFiberData (d m k : ℕ) where coord : JetCoordinates d m k

instance : CoeFun (JetFiberData d m k) (fun _ => DerivativeIndex d k → Fin m → ℝ) where
  coe V := V.coord



@[ext]
lemma ext (V W : JetFiberData d m k) (hcoord : ∀ I a, V.coord I a = W.coord I a) : V = W := byd:ℕm:ℕk:ℕV:JetFiberData d m kW:JetFiberData d m khcoord:∀ (I : DerivativeIndex d k) (a : Fin m), V.coord I a = W.coord I a⊢ V = W
  cases V with
  | mk coordV =>mkd:ℕm:ℕk:ℕW:JetFiberData d m kcoordV:JetCoordinates d m khcoord:∀ (I : DerivativeIndex d k) (a : Fin m), { coord := coordV }.coord I a = W.coord I a⊢ { coord := coordV } = W
  cases W with
  | mk coordW =>mk.mkd:ℕm:ℕk:ℕcoordV:JetCoordinates d m kcoordW:JetCoordinates d m khcoord:∀ (I : DerivativeIndex d k) (a : Fin m), { coord := coordV }.coord I a = { coord := coordW }.coord I a⊢ { coord := coordV } = { coord := coordW }
  have h : coordV = coordW := byd:ℕm:ℕk:ℕV:JetFiberData d m kW:JetFiberData d m khcoord:∀ (I : DerivativeIndex d k) (a : Fin m), V.coord I a = W.coord I a⊢ V = Wmk.mkd:ℕm:ℕk:ℕcoordV:JetCoordinates d m kcoordW:JetCoordinates d m khcoord:∀ (I : DerivativeIndex d k) (a : Fin m), { coord := coordV }.coord I a = { coord := coordW }.coord I ah:coordV = coordW⊢ { coord := coordV } = { coord := coordW }
    funext Id:ℕm:ℕk:ℕcoordV:JetCoordinates d m kcoordW:JetCoordinates d m khcoord:∀ (I : DerivativeIndex d k) (a : Fin m), { coord := coordV }.coord I a = { coord := coordW }.coord I aI:DerivativeIndex d k⊢ coordV I = coordW Imk.mkd:ℕm:ℕk:ℕcoordV:JetCoordinates d m kcoordW:JetCoordinates d m khcoord:∀ (I : DerivativeIndex d k) (a : Fin m), { coord := coordV }.coord I a = { coord := coordW }.coord I ah:coordV = coordW⊢ { coord := coordV } = { coord := coordW }
    funext ad:ℕm:ℕk:ℕcoordV:JetCoordinates d m kcoordW:JetCoordinates d m khcoord:∀ (I : DerivativeIndex d k) (a : Fin m), { coord := coordV }.coord I a = { coord := coordW }.coord I aI:DerivativeIndex d ka:Fin m⊢ coordV I a = coordW I amk.mkd:ℕm:ℕk:ℕcoordV:JetCoordinates d m kcoordW:JetCoordinates d m khcoord:∀ (I : DerivativeIndex d k) (a : Fin m), { coord := coordV }.coord I a = { coord := coordW }.coord I ah:coordV = coordW⊢ { coord := coordV } = { coord := coordW }
    exact hcoord I amk.mkd:ℕm:ℕk:ℕcoordV:JetCoordinates d m kcoordW:JetCoordinates d m khcoord:∀ (I : DerivativeIndex d k) (a : Fin m), { coord := coordV }.coord I a = { coord := coordW }.coord I ah:coordV = coordW⊢ { coord := coordV } = { coord := coordW }mk.mkd:ℕm:ℕk:ℕcoordV:JetCoordinates d m kcoordW:JetCoordinates d m khcoord:∀ (I : DerivativeIndex d k) (a : Fin m), { coord := coordV }.coord I a = { coord := coordW }.coord I ah:coordV = coordW⊢ { coord := coordV } = { coord := coordW }
  cases hmk.mk.refld:ℕm:ℕk:ℕcoordV:JetCoordinates d m khcoord:∀ (I : DerivativeIndex d k) (a : Fin m), { coord := coordV }.coord I a = { coord := coordV }.coord I a⊢ { coord := coordV } = { coord := coordV }
  rflAll goals completed! 🐙

The zero-th order component of a jet-fiber direction, corresponding to the field value.

def value (V : JetFiberData d m k) : EuclideanSpace ℝ (Fin m) :=
  WithLp.toLp 2 fun a => V.coord 0 a

              @[simp]
lemma value_apply (V : JetFiberData d m k) (a : Fin m) :
    V.value a = V.coord 0 a := byd:ℕm:ℕk:ℕV:JetFiberData d m ka:Fin m⊢ V.value.ofLp a = V.coord 0 a
  simp [value]All goals completed! 🐙instance : Zero (JetFiberData d m k) where
  zero := { coord := fun _ _ => 0 }instance : Add (JetFiberData d m k) where
  add V W := { coord := fun I a => V.coord I a + W.coord I a }instance : SMul ℝ (JetFiberData d m k) where
  smul c V := { coord := fun I a => c * V.coord I a }@[simp]
lemma zero_coord (I : DerivativeIndex d k) (a : Fin m) :
    (0 : JetFiberData d m k).coord I a = 0 := rfl@[simp]
lemma add_coord (V W : JetFiberData d m k) (I : DerivativeIndex d k) (a : Fin m) :
    (V + W).coord I a = V.coord I a + W.coord I a := rfl@[simp]
lemma smul_coord (c : ℝ) (V : JetFiberData d m k) (I : DerivativeIndex d k) (a : Fin m) :
    (c • V).coord I a = c * V.coord I a := rfl

B. Affine fiber structure on jet points

Translate a jet point by a fiber-direction increment.

def addFiber (J : JetPoint d m k) (V : JetFiberData d m k) : JetPoint d m k where
  base := J.base
  fiber := fun I a => J.fiber I a + V.coord I a

The affine line in jet space through J in the fiber direction V.

def lineMap (J : JetPoint d m k) (V : JetFiberData d m k) (s : ℝ) : JetPoint d m k :=
  J.addFiber (s • V)

              @[simp]
lemma addFiber_base (J : JetPoint d m k) (V : JetFiberData d m k) :
    (J.addFiber V).base = J.base := rfl@[simp]
lemma addFiber_value (J : JetPoint d m k) (V : JetFiberData d m k) :
    (J.addFiber V).value = J.value + V.value := byd:ℕm:ℕk:ℕJ:JetPoint d m kV:JetFiberData d m k⊢ (J.addFiber V).value = J.value + V.value
  ext ad:ℕm:ℕk:ℕJ:JetPoint d m kV:JetFiberData d m ka:Fin m⊢ (J.addFiber V).value.ofLp a = (J.value + V.value).ofLp a
  rflAll goals completed! 🐙@[simp]
lemma addFiber_coord (J : JetPoint d m k) (V : JetFiberData d m k)
    (I : DerivativeIndex d k) (a : Fin m) :
    (J.addFiber V).coord I a = J.coord I a + V.coord I a := rfl@[simp]
lemma lineMap_base (J : JetPoint d m k) (V : JetFiberData d m k) (s : ℝ) :
    (J.lineMap V s).base = J.base := rfl@[simp]
lemma lineMap_coord (J : JetPoint d m k) (V : JetFiberData d m k) (s : ℝ)
    (I : DerivativeIndex d k) (a : Fin m) :
    (J.lineMap V s).coord I a = J.coord I a + s * V.coord I a := rfl

C. Fiber directions determined by fields

              @[simp]
lemma jetDirectionAt_coord (k : ℕ) (g : Space d → EuclideanSpace ℝ (Fin m)) (x : Space d)
    (I : DerivativeIndex d k) (a : Fin m) :
    (jetDirectionAt k g x).coord I a = ∂^[I.1] (fun y => (g y) a) x := rfllemma jetDirectionAt_coord_zero (k : ℕ) (g : Space d → EuclideanSpace ℝ (Fin m))
    (x : Space d) (a : Fin m) :
    (jetDirectionAt k g x).coord 0 a = (g x) a := byd:ℕm:ℕk:ℕg:Space d → EuclideanSpace ℝ (Fin m)x:Space da:Fin m⊢ (jetDirectionAt k g x).coord 0 a = (g x).ofLp a
  simp [jetDirectionAt_coord]All goals completed! 🐙

lemma jetCoordinatesAt_add_smul (k : ℕ) (f g : Space d → EuclideanSpace ℝ (Fin m))
    (x : Space d) (s : ℝ)
    (hf : ContDiff ℝ ∞ f) (hg : ContDiff ℝ ∞ g) :
    jetCoordinatesAt k (fun y => f y + s • g y) x =
      jetCoordinatesAt k f x + s • jetCoordinatesAt k g x := byd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ g⊢ jetCoordinatesAt k (fun y => f y + s • g y) x = jetCoordinatesAt k f x + s • jetCoordinatesAt k g x
  funext Id:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d k⊢ jetCoordinatesAt k (fun y => f y + s • g y) x I = (jetCoordinatesAt k f x + s • jetCoordinatesAt k g x) I
  funext ad:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin m⊢ jetCoordinatesAt k (fun y => f y + s • g y) x I a = (jetCoordinatesAt k f x + s • jetCoordinatesAt k g x) I a
  have hfa : ContDiff ℝ ∞ (fun y => (f y) a) := byd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ g⊢ jetCoordinatesAt k (fun y => f y + s • g y) x = jetCoordinatesAt k f x + s • jetCoordinatesAt k g xd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp a⊢ jetCoordinatesAt k (fun y => f y + s • g y) x I a = (jetCoordinatesAt k f x + s • jetCoordinatesAt k g x) I a
    exact (contDiff_piLp_apply (𝕜 := ℝ) (n := ∞) (p := 2)
      (E := fun _ : Fin m => ℝ) (i := a)).comp hfd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp a⊢ jetCoordinatesAt k (fun y => f y + s • g y) x I a = (jetCoordinatesAt k f x + s • jetCoordinatesAt k g x) I ad:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp a⊢ jetCoordinatesAt k (fun y => f y + s • g y) x I a = (jetCoordinatesAt k f x + s • jetCoordinatesAt k g x) I a
  have hga : ContDiff ℝ ∞ (fun y => (g y) a) := byd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ g⊢ jetCoordinatesAt k (fun y => f y + s • g y) x = jetCoordinatesAt k f x + s • jetCoordinatesAt k g xd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp a⊢ jetCoordinatesAt k (fun y => f y + s • g y) x I a = (jetCoordinatesAt k f x + s • jetCoordinatesAt k g x) I a
    exact (contDiff_piLp_apply (𝕜 := ℝ) (n := ∞) (p := 2)
      (E := fun _ : Fin m => ℝ) (i := a)).comp hgd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp a⊢ jetCoordinatesAt k (fun y => f y + s • g y) x I a = (jetCoordinatesAt k f x + s • jetCoordinatesAt k g x) I ad:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp a⊢ jetCoordinatesAt k (fun y => f y + s • g y) x I a = (jetCoordinatesAt k f x + s • jetCoordinatesAt k g x) I a
  have hadd :
      (fun y => (f y + s • g y) a) = (fun y => (f y) a) + s • fun y => (g y) a := byd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ g⊢ jetCoordinatesAt k (fun y => f y + s • g y) x = jetCoordinatesAt k f x + s • jetCoordinatesAt k g xd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp ahadd:(fun y => (f y + s • g y).ofLp a) = (fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a⊢ jetCoordinatesAt k (fun y => f y + s • g y) x I a = (jetCoordinatesAt k f x + s • jetCoordinatesAt k g x) I a
    funext yd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp ay:Space d⊢ (f y + s • g y).ofLp a = ((fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a) yd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp ahadd:(fun y => (f y + s • g y).ofLp a) = (fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a⊢ jetCoordinatesAt k (fun y => f y + s • g y) x I a = (jetCoordinatesAt k f x + s • jetCoordinatesAt k g x) I a
    simp [smul_eq_mul]d:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp ahadd:(fun y => (f y + s • g y).ofLp a) = (fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a⊢ jetCoordinatesAt k (fun y => f y + s • g y) x I a = (jetCoordinatesAt k f x + s • jetCoordinatesAt k g x) I ad:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp ahadd:(fun y => (f y + s • g y).ofLp a) = (fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a⊢ jetCoordinatesAt k (fun y => f y + s • g y) x I a = (jetCoordinatesAt k f x + s • jetCoordinatesAt k g x) I a
  have hsg : ContDiff ℝ ∞ (s • fun y => (g y) a) := byd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ g⊢ jetCoordinatesAt k (fun y => f y + s • g y) x = jetCoordinatesAt k f x + s • jetCoordinatesAt k g xd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp ahadd:(fun y => (f y + s • g y).ofLp a) = (fun y => (f y).ofLp a) + s • fun y => (g y).ofLp ahsg:ContDiff ℝ ∞ (s • fun y => (g y).ofLp a)⊢ jetCoordinatesAt k (fun y => f y + s • g y) x I a = (jetCoordinatesAt k f x + s • jetCoordinatesAt k g x) I a
    exact hga.const_smul sd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp ahadd:(fun y => (f y + s • g y).ofLp a) = (fun y => (f y).ofLp a) + s • fun y => (g y).ofLp ahsg:ContDiff ℝ ∞ (s • fun y => (g y).ofLp a)⊢ jetCoordinatesAt k (fun y => f y + s • g y) x I a = (jetCoordinatesAt k f x + s • jetCoordinatesAt k g x) I ad:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp ahadd:(fun y => (f y + s • g y).ofLp a) = (fun y => (f y).ofLp a) + s • fun y => (g y).ofLp ahsg:ContDiff ℝ ∞ (s • fun y => (g y).ofLp a)⊢ jetCoordinatesAt k (fun y => f y + s • g y) x I a = (jetCoordinatesAt k f x + s • jetCoordinatesAt k g x) I a
  simp [jetCoordinatesAt]d:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp ahadd:(fun y => (f y + s • g y).ofLp a) = (fun y => (f y).ofLp a) + s • fun y => (g y).ofLp ahsg:ContDiff ℝ ∞ (s • fun y => (g y).ofLp a)⊢ Space.iteratedDeriv (↑I) (fun y => (f y).ofLp a + s * (g y).ofLp a) x =
  Space.iteratedDeriv (↑I) (fun y => (f y).ofLp a) x + s * Space.iteratedDeriv (↑I) (fun y => (g y).ofLp a) x
  have hsum := congrFun (Space.iteratedDeriv_add I.1 hfa hsg) xd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp ahadd:(fun y => (f y + s • g y).ofLp a) = (fun y => (f y).ofLp a) + s • fun y => (g y).ofLp ahsg:ContDiff ℝ ∞ (s • fun y => (g y).ofLp a)hsum:Space.iteratedDeriv (↑I) ((fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a) x =
  ((Space.iteratedDeriv ↑I fun y => (f y).ofLp a) + Space.iteratedDeriv (↑I) (s • fun y => (g y).ofLp a)) x⊢ Space.iteratedDeriv (↑I) (fun y => (f y).ofLp a + s * (g y).ofLp a) x =
  Space.iteratedDeriv (↑I) (fun y => (f y).ofLp a) x + s * Space.iteratedDeriv (↑I) (fun y => (g y).ofLp a) x
  have hsmul := congrFun (Space.iteratedDeriv_const_smul I.1 s hga) xd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp ahadd:(fun y => (f y + s • g y).ofLp a) = (fun y => (f y).ofLp a) + s • fun y => (g y).ofLp ahsg:ContDiff ℝ ∞ (s • fun y => (g y).ofLp a)hsum:Space.iteratedDeriv (↑I) ((fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a) x =
  ((Space.iteratedDeriv ↑I fun y => (f y).ofLp a) + Space.iteratedDeriv (↑I) (s • fun y => (g y).ofLp a)) xhsmul:Space.iteratedDeriv (↑I) (s • fun y => (g y).ofLp a) x = (s • Space.iteratedDeriv ↑I fun y => (g y).ofLp a) x⊢ Space.iteratedDeriv (↑I) (fun y => (f y).ofLp a + s * (g y).ofLp a) x =
  Space.iteratedDeriv (↑I) (fun y => (f y).ofLp a) x + s * Space.iteratedDeriv (↑I) (fun y => (g y).ofLp a) x
  calc
    ∂^[I.1] ((fun y => (f y) a) + s • fun y => (g y) a) x
      = (∂^[I.1] (fun y => (f y) a) + ∂^[I.1] (s • fun y => (g y) a)) x := byd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp ahadd:(fun y => (f y + s • g y).ofLp a) = (fun y => (f y).ofLp a) + s • fun y => (g y).ofLp ahsg:ContDiff ℝ ∞ (s • fun y => (g y).ofLp a)hsum:Space.iteratedDeriv (↑I) ((fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a) x =
  ((Space.iteratedDeriv ↑I fun y => (f y).ofLp a) + Space.iteratedDeriv (↑I) (s • fun y => (g y).ofLp a)) xhsmul:Space.iteratedDeriv (↑I) (s • fun y => (g y).ofLp a) x = (s • Space.iteratedDeriv ↑I fun y => (g y).ofLp a) x⊢ Space.iteratedDeriv (↑I) ((fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a) x =
  ((Space.iteratedDeriv ↑I fun y => (f y).ofLp a) + Space.iteratedDeriv (↑I) (s • fun y => (g y).ofLp a)) x
          simpa using hsumAll goals completed! 🐙
    _ = ∂^[I.1] (fun y => (f y) a) x + s * ∂^[I.1] (fun y => (g y) a) x := byd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp ahadd:(fun y => (f y + s • g y).ofLp a) = (fun y => (f y).ofLp a) + s • fun y => (g y).ofLp ahsg:ContDiff ℝ ∞ (s • fun y => (g y).ofLp a)hsum:Space.iteratedDeriv (↑I) ((fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a) x =
  ((Space.iteratedDeriv ↑I fun y => (f y).ofLp a) + Space.iteratedDeriv (↑I) (s • fun y => (g y).ofLp a)) xhsmul:Space.iteratedDeriv (↑I) (s • fun y => (g y).ofLp a) x = (s • Space.iteratedDeriv ↑I fun y => (g y).ofLp a) x⊢ ((Space.iteratedDeriv ↑I fun y => (f y).ofLp a) + Space.iteratedDeriv (↑I) (s • fun y => (g y).ofLp a)) x =
  Space.iteratedDeriv (↑I) (fun y => (f y).ofLp a) x + s * Space.iteratedDeriv (↑I) (fun y => (g y).ofLp a) x
          simp [Pi.add_apply, Pi.smul_apply, smul_eq_mul, hsmul]All goals completed! 🐙

lemma jetAt_add_smul (k : ℕ) (f g : Space d → EuclideanSpace ℝ (Fin m))
    (x : Space d) (s : ℝ)
    (hf : ContDiff ℝ ∞ f) (hg : ContDiff ℝ ∞ g) :
    jetAt k (fun y => f y + s • g y) x = (jetAt k f x).lineMap (jetDirectionAt k g x) s := byd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ g⊢ jetAt k (fun y => f y + s • g y) x = (jetAt k f x).lineMap (jetDirectionAt k g x) s
  apply JetPoint.exthbased:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ g⊢ (jetAt k (fun y => f y + s • g y) x).base = ((jetAt k f x).lineMap (jetDirectionAt k g x) s).basehcoordd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ g⊢ ∀ (I : DerivativeIndex d k) (a : Fin m),
  (jetAt k (fun y => f y + s • g y) x).coord I a = ((jetAt k f x).lineMap (jetDirectionAt k g x) s).coord I a
  ·hbased:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ g⊢ (jetAt k (fun y => f y + s • g y) x).base = ((jetAt k f x).lineMap (jetDirectionAt k g x) s).base simp [JetPoint.lineMap]All goals completed! 🐙
  ·hcoordd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ g⊢ ∀ (I : DerivativeIndex d k) (a : Fin m),
  (jetAt k (fun y => f y + s • g y) x).coord I a = ((jetAt k f x).lineMap (jetDirectionAt k g x) s).coord I a intro I ahcoordd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin m⊢ (jetAt k (fun y => f y + s • g y) x).coord I a = ((jetAt k f x).lineMap (jetDirectionAt k g x) s).coord I a
    have hfa : ContDiff ℝ ∞ (fun y => (f y) a) := byd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ g⊢ jetAt k (fun y => f y + s • g y) x = (jetAt k f x).lineMap (jetDirectionAt k g x) shcoordd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp a⊢ (jetAt k (fun y => f y + s • g y) x).coord I a = ((jetAt k f x).lineMap (jetDirectionAt k g x) s).coord I a
      exact (contDiff_piLp_apply (𝕜 := ℝ) (n := ∞) (p := 2)
        (E := fun _ : Fin m => ℝ) (i := a)).comp hfhcoordd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp a⊢ (jetAt k (fun y => f y + s • g y) x).coord I a = ((jetAt k f x).lineMap (jetDirectionAt k g x) s).coord I ahcoordd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp a⊢ (jetAt k (fun y => f y + s • g y) x).coord I a = ((jetAt k f x).lineMap (jetDirectionAt k g x) s).coord I a
    have hga : ContDiff ℝ ∞ (fun y => (g y) a) := byd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ g⊢ jetAt k (fun y => f y + s • g y) x = (jetAt k f x).lineMap (jetDirectionAt k g x) shcoordd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp a⊢ (jetAt k (fun y => f y + s • g y) x).coord I a = ((jetAt k f x).lineMap (jetDirectionAt k g x) s).coord I a
      exact (contDiff_piLp_apply (𝕜 := ℝ) (n := ∞) (p := 2)
        (E := fun _ : Fin m => ℝ) (i := a)).comp hghcoordd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp a⊢ (jetAt k (fun y => f y + s • g y) x).coord I a = ((jetAt k f x).lineMap (jetDirectionAt k g x) s).coord I ahcoordd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp a⊢ (jetAt k (fun y => f y + s • g y) x).coord I a = ((jetAt k f x).lineMap (jetDirectionAt k g x) s).coord I a
    have hadd :
        (fun y => (f y + s • g y) a) = (fun y => (f y) a) + s • fun y => (g y) a := byd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ g⊢ jetAt k (fun y => f y + s • g y) x = (jetAt k f x).lineMap (jetDirectionAt k g x) shcoordd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp ahadd:(fun y => (f y + s • g y).ofLp a) = (fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a⊢ (jetAt k (fun y => f y + s • g y) x).coord I a = ((jetAt k f x).lineMap (jetDirectionAt k g x) s).coord I a
      funext yd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp ay:Space d⊢ (f y + s • g y).ofLp a = ((fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a) yhcoordd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp ahadd:(fun y => (f y + s • g y).ofLp a) = (fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a⊢ (jetAt k (fun y => f y + s • g y) x).coord I a = ((jetAt k f x).lineMap (jetDirectionAt k g x) s).coord I a
      simp [smul_eq_mul]hcoordd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp ahadd:(fun y => (f y + s • g y).ofLp a) = (fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a⊢ (jetAt k (fun y => f y + s • g y) x).coord I a = ((jetAt k f x).lineMap (jetDirectionAt k g x) s).coord I ahcoordd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp ahadd:(fun y => (f y + s • g y).ofLp a) = (fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a⊢ (jetAt k (fun y => f y + s • g y) x).coord I a = ((jetAt k f x).lineMap (jetDirectionAt k g x) s).coord I a
    change ∂^[I.1] (fun y => (f y + s • g y) a) x =
      ((jetAt k f x).lineMap (jetDirectionAt k g x) s).coord I ahcoordd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp ahadd:(fun y => (f y + s • g y).ofLp a) = (fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a⊢ Space.iteratedDeriv (↑I) (fun y => (f y + s • g y).ofLp a) x =
  ((jetAt k f x).lineMap (jetDirectionAt k g x) s).coord I a
    rw [JetPoint.lineMap_coord,hcoordd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp ahadd:(fun y => (f y + s • g y).ofLp a) = (fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a⊢ Space.iteratedDeriv (↑I) (fun y => (f y + s • g y).ofLp a) x =
  (jetAt k f x).coord I a + s * (jetDirectionAt k g x).coord I ahcoordd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp ahadd:(fun y => (f y + s • g y).ofLp a) = (fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a⊢ Space.iteratedDeriv (↑I) (fun y => (f y + s • g y).ofLp a) x =
  Space.iteratedDeriv (↑I) (fun y => (f y).ofLp a) x + s * Space.iteratedDeriv (↑I) (fun y => (g y).ofLp a) x jetAt_coord,hcoordd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp ahadd:(fun y => (f y + s • g y).ofLp a) = (fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a⊢ Space.iteratedDeriv (↑I) (fun y => (f y + s • g y).ofLp a) x =
  Space.iteratedDeriv (↑I) (fun y => (f y).ofLp a) x + s * (jetDirectionAt k g x).coord I ahcoordd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp ahadd:(fun y => (f y + s • g y).ofLp a) = (fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a⊢ Space.iteratedDeriv (↑I) (fun y => (f y + s • g y).ofLp a) x =
  Space.iteratedDeriv (↑I) (fun y => (f y).ofLp a) x + s * Space.iteratedDeriv (↑I) (fun y => (g y).ofLp a) x jetDirectionAt_coordhcoordd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp ahadd:(fun y => (f y + s • g y).ofLp a) = (fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a⊢ Space.iteratedDeriv (↑I) (fun y => (f y + s • g y).ofLp a) x =
  Space.iteratedDeriv (↑I) (fun y => (f y).ofLp a) x + s * Space.iteratedDeriv (↑I) (fun y => (g y).ofLp a) xhcoordd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp ahadd:(fun y => (f y + s • g y).ofLp a) = (fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a⊢ Space.iteratedDeriv (↑I) (fun y => (f y + s • g y).ofLp a) x =
  Space.iteratedDeriv (↑I) (fun y => (f y).ofLp a) x + s * Space.iteratedDeriv (↑I) (fun y => (g y).ofLp a) x]hcoordd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp ahadd:(fun y => (f y + s • g y).ofLp a) = (fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a⊢ Space.iteratedDeriv (↑I) (fun y => (f y + s • g y).ofLp a) x =
  Space.iteratedDeriv (↑I) (fun y => (f y).ofLp a) x + s * Space.iteratedDeriv (↑I) (fun y => (g y).ofLp a) x
    rw [haddhcoordd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp ahadd:(fun y => (f y + s • g y).ofLp a) = (fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a⊢ Space.iteratedDeriv (↑I) ((fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a) x =
  Space.iteratedDeriv (↑I) (fun y => (f y).ofLp a) x + s * Space.iteratedDeriv (↑I) (fun y => (g y).ofLp a) xhcoordd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp ahadd:(fun y => (f y + s • g y).ofLp a) = (fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a⊢ Space.iteratedDeriv (↑I) ((fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a) x =
  Space.iteratedDeriv (↑I) (fun y => (f y).ofLp a) x + s * Space.iteratedDeriv (↑I) (fun y => (g y).ofLp a) x]hcoordd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp ahadd:(fun y => (f y + s • g y).ofLp a) = (fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a⊢ Space.iteratedDeriv (↑I) ((fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a) x =
  Space.iteratedDeriv (↑I) (fun y => (f y).ofLp a) x + s * Space.iteratedDeriv (↑I) (fun y => (g y).ofLp a) x
    have hsg : ContDiff ℝ ∞ (s • fun y => (g y) a) := byd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ g⊢ jetAt k (fun y => f y + s • g y) x = (jetAt k f x).lineMap (jetDirectionAt k g x) shcoordd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp ahadd:(fun y => (f y + s • g y).ofLp a) = (fun y => (f y).ofLp a) + s • fun y => (g y).ofLp ahsg:ContDiff ℝ ∞ (s • fun y => (g y).ofLp a)⊢ Space.iteratedDeriv (↑I) ((fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a) x =
  Space.iteratedDeriv (↑I) (fun y => (f y).ofLp a) x + s * Space.iteratedDeriv (↑I) (fun y => (g y).ofLp a) x
      exact hga.const_smul shcoordd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp ahadd:(fun y => (f y + s • g y).ofLp a) = (fun y => (f y).ofLp a) + s • fun y => (g y).ofLp ahsg:ContDiff ℝ ∞ (s • fun y => (g y).ofLp a)⊢ Space.iteratedDeriv (↑I) ((fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a) x =
  Space.iteratedDeriv (↑I) (fun y => (f y).ofLp a) x + s * Space.iteratedDeriv (↑I) (fun y => (g y).ofLp a) xhcoordd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp ahadd:(fun y => (f y + s • g y).ofLp a) = (fun y => (f y).ofLp a) + s • fun y => (g y).ofLp ahsg:ContDiff ℝ ∞ (s • fun y => (g y).ofLp a)⊢ Space.iteratedDeriv (↑I) ((fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a) x =
  Space.iteratedDeriv (↑I) (fun y => (f y).ofLp a) x + s * Space.iteratedDeriv (↑I) (fun y => (g y).ofLp a) x
    have hsum := congrFun (Space.iteratedDeriv_add I.1 hfa hsg) xhcoordd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp ahadd:(fun y => (f y + s • g y).ofLp a) = (fun y => (f y).ofLp a) + s • fun y => (g y).ofLp ahsg:ContDiff ℝ ∞ (s • fun y => (g y).ofLp a)hsum:Space.iteratedDeriv (↑I) ((fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a) x =
  ((Space.iteratedDeriv ↑I fun y => (f y).ofLp a) + Space.iteratedDeriv (↑I) (s • fun y => (g y).ofLp a)) x⊢ Space.iteratedDeriv (↑I) ((fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a) x =
  Space.iteratedDeriv (↑I) (fun y => (f y).ofLp a) x + s * Space.iteratedDeriv (↑I) (fun y => (g y).ofLp a) x
    have hsmul := congrFun (Space.iteratedDeriv_const_smul I.1 s hga) xhcoordd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp ahadd:(fun y => (f y + s • g y).ofLp a) = (fun y => (f y).ofLp a) + s • fun y => (g y).ofLp ahsg:ContDiff ℝ ∞ (s • fun y => (g y).ofLp a)hsum:Space.iteratedDeriv (↑I) ((fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a) x =
  ((Space.iteratedDeriv ↑I fun y => (f y).ofLp a) + Space.iteratedDeriv (↑I) (s • fun y => (g y).ofLp a)) xhsmul:Space.iteratedDeriv (↑I) (s • fun y => (g y).ofLp a) x = (s • Space.iteratedDeriv ↑I fun y => (g y).ofLp a) x⊢ Space.iteratedDeriv (↑I) ((fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a) x =
  Space.iteratedDeriv (↑I) (fun y => (f y).ofLp a) x + s * Space.iteratedDeriv (↑I) (fun y => (g y).ofLp a) x
    calc
      ∂^[I.1] ((fun y => (f y) a) + s • fun y => (g y) a) x
        = (∂^[I.1] (fun y => (f y) a) + ∂^[I.1] (s • fun y => (g y) a)) x := hsum
      _ = ∂^[I.1] (fun y => (f y) a) x + s * ∂^[I.1] (fun y => (g y) a) x := byd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)g:Space d → EuclideanSpace ℝ (Fin m)x:Space ds:ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhfa:ContDiff ℝ ∞ fun y => (f y).ofLp ahga:ContDiff ℝ ∞ fun y => (g y).ofLp ahadd:(fun y => (f y + s • g y).ofLp a) = (fun y => (f y).ofLp a) + s • fun y => (g y).ofLp ahsg:ContDiff ℝ ∞ (s • fun y => (g y).ofLp a)hsum:Space.iteratedDeriv (↑I) ((fun y => (f y).ofLp a) + s • fun y => (g y).ofLp a) x =
  ((Space.iteratedDeriv ↑I fun y => (f y).ofLp a) + Space.iteratedDeriv (↑I) (s • fun y => (g y).ofLp a)) xhsmul:Space.iteratedDeriv (↑I) (s • fun y => (g y).ofLp a) x = (s • Space.iteratedDeriv ↑I fun y => (g y).ofLp a) x⊢ ((Space.iteratedDeriv ↑I fun y => (f y).ofLp a) + Space.iteratedDeriv (↑I) (s • fun y => (g y).ofLp a)) x =
  Space.iteratedDeriv (↑I) (fun y => (f y).ofLp a) x + s * Space.iteratedDeriv (↑I) (fun y => (g y).ofLp a) x
          simp [Pi.add_apply, Pi.smul_apply, smul_eq_mul, hsmul]All goals completed! 🐙