Physlib.SpaceAndTime.Space.CrossProduct

Physlib
SpaceAndTime
Space
CrossProduct

Imports

/-
Copyright (c) 2025 Zhi Kai Pong. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Zhi Kai Pong, Joseph Tooby-Smith
-/
module

public import Mathlib.LinearAlgebra.CrossProduct
public import Physlib.SpaceAndTime.Time.Derivatives

The cross product on Euclidean vectors in three dimensions

i. Overview

In this module we define the cross product on EuclideanSpace ℝ (Fin 3), and prove various properties about it related to time derivatives and inner products.

ii. Key results

⨯ₑ₃ : The cross product on EuclideanSpace ℝ (Fin 3).

time_deriv_cross_commute : Time derivatives move out of cross products.

inner_cross_self : Inner product of a vector with the cross product of another vector and itself is zero.

inner_self_cross : Inner product of a vector with the cross product of itself and another vector is zero.

iii. Table of contents

A. The notation for the cross product

B. Time derivatives move out of cross products

C. Inner product of vectors with cross products involving themselves

iv. References

@[expose] public section

A. The notation for the cross product

Cross product in EuclideanSpace ℝ (Fin 3). Uses ⨯ which is typed using \X or \vectorproduct or \crossproduct.

set_option quotPrecheck false in

infixl:70 " ⨯ₑ₃ " => fun a b => (WithLp.equiv 2 (Fin 3 → ℝ)).symm
    (WithLp.equiv 2 (Fin 3 → ℝ) a ⨯₃ WithLp.equiv 2 (Fin 3 → ℝ) b)

B. Time derivatives move out of cross products

Cross product and fderiv commute.


lemma fderiv_cross_commute {t : Time} {s : EuclideanSpace ℝ (Fin 3)}
    {f : Time → EuclideanSpace ℝ (Fin 3)} (hf : Differentiable ℝ f) :
    s ⨯ₑ₃ (fderiv ℝ (fun t' => f t') t) 1
    = fderiv ℝ (fun t' => s ⨯ₑ₃ (f t')) t 1 := byt:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ f⊢ (fun a b =>
      (WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
    s ((fderiv ℝ (fun t' => f t') t) 1) =
  (fderiv ℝ
      (fun t' =>
        (fun a b =>
            (WithLp.equiv 2 (Fin 3 → ℝ)).symm
              ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
          s (f t'))
      t)
    1
  have h (i j : Fin 3) : s i * (fderiv ℝ (fun u => f u) t) 1 j -
      s j * (fderiv ℝ (fun u => f u) t) 1 i
      = (fderiv ℝ (fun t => s i * f t j - s j * f t i) t) 1:= by
    rw [fderiv_fun_sub,t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
  (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j) t - fderiv ℝ (fun t => s.ofLp j * (f t).ofLp i) t) 1hft:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ DifferentiableAt ℝ (fun t => s.ofLp i * (f t).ofLp j) thgt:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ DifferentiableAt ℝ (fun t => s.ofLp j * (f t).ofLp i) tt:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
  (s.ofLp i • fderiv ℝ (fun t => (f t).ofLp j) t - s.ofLp j • fderiv ℝ (fun t => (f t).ofLp i) t) 1hat:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ DifferentiableAt ℝ (fun t => (f t).ofLp i) that:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ DifferentiableAt ℝ (fun t => (f t).ofLp j) thft:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ DifferentiableAt ℝ (fun t => s.ofLp i * (f t).ofLp j) thgt:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ DifferentiableAt ℝ (fun t => s.ofLp j * (f t).ofLp i) tt:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fun a b =>
      (WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
    s ((fderiv ℝ (fun t' => f t') t) 1) =
  (fderiv ℝ
      (fun t' =>
        (fun a b =>
            (WithLp.equiv 2 (Fin 3 → ℝ)).symm
              ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
          s (f t'))
      t)
    1 fderiv_const_mul,t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
  (s.ofLp i • fderiv ℝ (fun t => (f t).ofLp j) t - fderiv ℝ (fun t => s.ofLp j * (f t).ofLp i) t) 1hat:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ DifferentiableAt ℝ (fun t => (f t).ofLp j) thft:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ DifferentiableAt ℝ (fun t => s.ofLp i * (f t).ofLp j) thgt:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ DifferentiableAt ℝ (fun t => s.ofLp j * (f t).ofLp i) tt:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
  (s.ofLp i • fderiv ℝ (fun t => (f t).ofLp j) t - s.ofLp j • fderiv ℝ (fun t => (f t).ofLp i) t) 1hat:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ DifferentiableAt ℝ (fun t => (f t).ofLp i) that:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ DifferentiableAt ℝ (fun t => (f t).ofLp j) thft:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ DifferentiableAt ℝ (fun t => s.ofLp i * (f t).ofLp j) thgt:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ DifferentiableAt ℝ (fun t => s.ofLp j * (f t).ofLp i) tt:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fun a b =>
      (WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
    s ((fderiv ℝ (fun t' => f t') t) 1) =
  (fderiv ℝ
      (fun t' =>
        (fun a b =>
            (WithLp.equiv 2 (Fin 3 → ℝ)).symm
              ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
          s (f t'))
      t)
    1 fderiv_const_mult:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
  (s.ofLp i • fderiv ℝ (fun t => (f t).ofLp j) t - s.ofLp j • fderiv ℝ (fun t => (f t).ofLp i) t) 1hat:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ DifferentiableAt ℝ (fun t => (f t).ofLp i) that:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ DifferentiableAt ℝ (fun t => (f t).ofLp j) thft:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ DifferentiableAt ℝ (fun t => s.ofLp i * (f t).ofLp j) thgt:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ DifferentiableAt ℝ (fun t => s.ofLp j * (f t).ofLp i) tt:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
  (s.ofLp i • fderiv ℝ (fun t => (f t).ofLp j) t - s.ofLp j • fderiv ℝ (fun t => (f t).ofLp i) t) 1hat:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ DifferentiableAt ℝ (fun t => (f t).ofLp i) that:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ DifferentiableAt ℝ (fun t => (f t).ofLp j) thft:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ DifferentiableAt ℝ (fun t => s.ofLp i * (f t).ofLp j) thgt:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ DifferentiableAt ℝ (fun t => s.ofLp j * (f t).ofLp i) tt:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fun a b =>
      (WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
    s ((fderiv ℝ (fun t' => f t') t) 1) =
  (fderiv ℝ
      (fun t' =>
        (fun a b =>
            (WithLp.equiv 2 (Fin 3 → ℝ)).symm
              ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
          s (f t'))
      t)
    1]t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
  (s.ofLp i • fderiv ℝ (fun t => (f t).ofLp j) t - s.ofLp j • fderiv ℝ (fun t => (f t).ofLp i) t) 1hat:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ DifferentiableAt ℝ (fun t => (f t).ofLp i) that:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ DifferentiableAt ℝ (fun t => (f t).ofLp j) thft:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ DifferentiableAt ℝ (fun t => s.ofLp i * (f t).ofLp j) thgt:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ DifferentiableAt ℝ (fun t => s.ofLp j * (f t).ofLp i) tt:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fun a b =>
      (WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
    s ((fderiv ℝ (fun t' => f t') t) 1) =
  (fderiv ℝ
      (fun t' =>
        (fun a b =>
            (WithLp.equiv 2 (Fin 3 → ℝ)).symm
              ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
          s (f t'))
      t)
    1
    ·t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
  (s.ofLp i • fderiv ℝ (fun t => (f t).ofLp j) t - s.ofLp j • fderiv ℝ (fun t => (f t).ofLp i) t) 1t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fun a b =>
      (WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
    s ((fderiv ℝ (fun t' => f t') t) 1) =
  (fderiv ℝ
      (fun t' =>
        (fun a b =>
            (WithLp.equiv 2 (Fin 3 → ℝ)).symm
              ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
          s (f t'))
      t)
    1 simp only [FunLike.coe_sub, FunLike.coe_smul, Pi.sub_apply,
        Pi.smul_apply, smul_eq_mul]t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
  s.ofLp i * (fderiv ℝ (fun t => (f t).ofLp j) t) 1 - s.ofLp j * (fderiv ℝ (fun t => (f t).ofLp i) t) 1t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fun a b =>
      (WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
    s ((fderiv ℝ (fun t' => f t') t) 1) =
  (fderiv ℝ
      (fun t' =>
        (fun a b =>
            (WithLp.equiv 2 (Fin 3 → ℝ)).symm
              ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
          s (f t'))
      t)
    1
      rw [Time.fderiv_euclid,t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
  s.ofLp i * ((fderiv ℝ (fun t => f t) t) 1).ofLp j - s.ofLp j * (fderiv ℝ (fun t => (f t).ofLp i) t) 1hft:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ Differentiable ℝ fhft:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ Differentiable ℝ fhft:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ Differentiable ℝ ft:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fun a b =>
      (WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
    s ((fderiv ℝ (fun t' => f t') t) 1) =
  (fderiv ℝ
      (fun t' =>
        (fun a b =>
            (WithLp.equiv 2 (Fin 3 → ℝ)).symm
              ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
          s (f t'))
      t)
    1 Time.fderiv_euclidt:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
  s.ofLp i * ((fderiv ℝ (fun t => f t) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun t => f t) t) 1).ofLp ihft:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ Differentiable ℝ fhft:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ Differentiable ℝ fhft:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ Differentiable ℝ fhft:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ Differentiable ℝ ft:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fun a b =>
      (WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
    s ((fderiv ℝ (fun t' => f t') t) 1) =
  (fderiv ℝ
      (fun t' =>
        (fun a b =>
            (WithLp.equiv 2 (Fin 3 → ℝ)).symm
              ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
          s (f t'))
      t)
    1]hft:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ Differentiable ℝ fhft:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ Differentiable ℝ ft:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fun a b =>
      (WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
    s ((fderiv ℝ (fun t' => f t') t) 1) =
  (fderiv ℝ
      (fun t' =>
        (fun a b =>
            (WithLp.equiv 2 (Fin 3 → ℝ)).symm
              ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
          s (f t'))
      t)
    1
      ·hft:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ Differentiable ℝ ft:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fun a b =>
      (WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
    s ((fderiv ℝ (fun t' => f t') t) 1) =
  (fderiv ℝ
      (fun t' =>
        (fun a b =>
            (WithLp.equiv 2 (Fin 3 → ℝ)).symm
              ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
          s (f t'))
      t)
    1 intro ihft:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi✝:Fin 3j:Fin 3i:Time⊢ DifferentiableAt ℝ f it:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fun a b =>
      (WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
    s ((fderiv ℝ (fun t' => f t') t) 1) =
  (fderiv ℝ
      (fun t' =>
        (fun a b =>
            (WithLp.equiv 2 (Fin 3 → ℝ)).symm
              ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
          s (f t'))
      t)
    1
        repeat fun_propAll goals completed! 🐙t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fun a b =>
      (WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
    s ((fderiv ℝ (fun t' => f t') t) 1) =
  (fderiv ℝ
      (fun t' =>
        (fun a b =>
            (WithLp.equiv 2 (Fin 3 → ℝ)).symm
              ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
          s (f t'))
      t)
    1
      ·hft:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ Differentiable ℝ ft:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fun a b =>
      (WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
    s ((fderiv ℝ (fun t' => f t') t) 1) =
  (fderiv ℝ
      (fun t' =>
        (fun a b =>
            (WithLp.equiv 2 (Fin 3 → ℝ)).symm
              ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
          s (f t'))
      t)
    1 fun_propAll goals completed! 🐙t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fun a b =>
      (WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
    s ((fderiv ℝ (fun t' => f t') t) 1) =
  (fderiv ℝ
      (fun t' =>
        (fun a b =>
            (WithLp.equiv 2 (Fin 3 → ℝ)).symm
              ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
          s (f t'))
      t)
    1
    ·hat:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ DifferentiableAt ℝ (fun t => (f t).ofLp i) tt:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fun a b =>
      (WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
    s ((fderiv ℝ (fun t' => f t') t) 1) =
  (fderiv ℝ
      (fun t' =>
        (fun a b =>
            (WithLp.equiv 2 (Fin 3 → ℝ)).symm
              ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
          s (f t'))
      t)
    1 fun_propAll goals completed! 🐙t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fun a b =>
      (WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
    s ((fderiv ℝ (fun t' => f t') t) 1) =
  (fderiv ℝ
      (fun t' =>
        (fun a b =>
            (WithLp.equiv 2 (Fin 3 → ℝ)).symm
              ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
          s (f t'))
      t)
    1
    ·hat:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ DifferentiableAt ℝ (fun t => (f t).ofLp j) tt:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fun a b =>
      (WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
    s ((fderiv ℝ (fun t' => f t') t) 1) =
  (fderiv ℝ
      (fun t' =>
        (fun a b =>
            (WithLp.equiv 2 (Fin 3 → ℝ)).symm
              ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
          s (f t'))
      t)
    1 fun_propAll goals completed! 🐙t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fun a b =>
      (WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
    s ((fderiv ℝ (fun t' => f t') t) 1) =
  (fderiv ℝ
      (fun t' =>
        (fun a b =>
            (WithLp.equiv 2 (Fin 3 → ℝ)).symm
              ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
          s (f t'))
      t)
    1
    ·hft:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ DifferentiableAt ℝ (fun t => s.ofLp i * (f t).ofLp j) tt:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fun a b =>
      (WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
    s ((fderiv ℝ (fun t' => f t') t) 1) =
  (fderiv ℝ
      (fun t' =>
        (fun a b =>
            (WithLp.equiv 2 (Fin 3 → ℝ)).symm
              ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
          s (f t'))
      t)
    1 fun_propAll goals completed! 🐙t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fun a b =>
      (WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
    s ((fderiv ℝ (fun t' => f t') t) 1) =
  (fderiv ℝ
      (fun t' =>
        (fun a b =>
            (WithLp.equiv 2 (Fin 3 → ℝ)).symm
              ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
          s (f t'))
      t)
    1
    ·hgt:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fi:Fin 3j:Fin 3⊢ DifferentiableAt ℝ (fun t => s.ofLp j * (f t).ofLp i) tt:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fun a b =>
      (WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
    s ((fderiv ℝ (fun t' => f t') t) 1) =
  (fderiv ℝ
      (fun t' =>
        (fun a b =>
            (WithLp.equiv 2 (Fin 3 → ℝ)).symm
              ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
          s (f t'))
      t)
    1 fun_propt:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fun a b =>
      (WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
    s ((fderiv ℝ (fun t' => f t') t) 1) =
  (fderiv ℝ
      (fun t' =>
        (fun a b =>
            (WithLp.equiv 2 (Fin 3 → ℝ)).symm
              ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
          s (f t'))
      t)
    1t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fun a b =>
      (WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
    s ((fderiv ℝ (fun t' => f t') t) 1) =
  (fderiv ℝ
      (fun t' =>
        (fun a b =>
            (WithLp.equiv 2 (Fin 3 → ℝ)).symm
              ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
          s (f t'))
      t)
    1
  rw [crossProductt:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fun a b =>
      (WithLp.equiv 2 (Fin 3 → ℝ)).symm
        (((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]) ⋯ ⋯ ⋯ ⋯)
            ((WithLp.equiv 2 (Fin 3 → ℝ)) a))
          ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
    s ((fderiv ℝ (fun t' => f t') t) 1) =
  (fderiv ℝ
      (fun t' =>
        (fun a b =>
            (WithLp.equiv 2 (Fin 3 → ℝ)).symm
              (((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]) ⋯ ⋯
                    ⋯ ⋯)
                  ((WithLp.equiv 2 (Fin 3 → ℝ)) a))
                ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
          s (f t'))
      t)
    1t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fun a b =>
      (WithLp.equiv 2 (Fin 3 → ℝ)).symm
        (((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]) ⋯ ⋯ ⋯ ⋯)
            ((WithLp.equiv 2 (Fin 3 → ℝ)) a))
          ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
    s ((fderiv ℝ (fun t' => f t') t) 1) =
  (fderiv ℝ
      (fun t' =>
        (fun a b =>
            (WithLp.equiv 2 (Fin 3 → ℝ)).symm
              (((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]) ⋯ ⋯
                    ⋯ ⋯)
                  ((WithLp.equiv 2 (Fin 3 → ℝ)) a))
                ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
          s (f t'))
      t)
    1]t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fun a b =>
      (WithLp.equiv 2 (Fin 3 → ℝ)).symm
        (((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]) ⋯ ⋯ ⋯ ⋯)
            ((WithLp.equiv 2 (Fin 3 → ℝ)) a))
          ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
    s ((fderiv ℝ (fun t' => f t') t) 1) =
  (fderiv ℝ
      (fun t' =>
        (fun a b =>
            (WithLp.equiv 2 (Fin 3 → ℝ)).symm
              (((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]) ⋯ ⋯
                    ⋯ ⋯)
                  ((WithLp.equiv 2 (Fin 3 → ℝ)) a))
                ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
          s (f t'))
      t)
    1
  ext it:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1i:Fin 3⊢ ((fun a b =>
          (WithLp.equiv 2 (Fin 3 → ℝ)).symm
            (((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]) ⋯ ⋯ ⋯
                  ⋯)
                ((WithLp.equiv 2 (Fin 3 → ℝ)) a))
              ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
        s ((fderiv ℝ (fun t' => f t') t) 1)).ofLp
    i =
  ((fderiv ℝ
          (fun t' =>
            (fun a b =>
                (WithLp.equiv 2 (Fin 3 → ℝ)).symm
                  (((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0])
                        ⋯ ⋯ ⋯ ⋯)
                      ((WithLp.equiv 2 (Fin 3 → ℝ)) a))
                    ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
              s (f t'))
          t)
        1).ofLp
    i
  fin_cases i«0»t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ ((fun a b =>
          (WithLp.equiv 2 (Fin 3 → ℝ)).symm
            (((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]) ⋯ ⋯ ⋯
                  ⋯)
                ((WithLp.equiv 2 (Fin 3 → ℝ)) a))
              ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
        s ((fderiv ℝ (fun t' => f t') t) 1)).ofLp
    ((fun i => i) ⟨0, ⋯⟩) =
  ((fderiv ℝ
          (fun t' =>
            (fun a b =>
                (WithLp.equiv 2 (Fin 3 → ℝ)).symm
                  (((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0])
                        ⋯ ⋯ ⋯ ⋯)
                      ((WithLp.equiv 2 (Fin 3 → ℝ)) a))
                    ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
              s (f t'))
          t)
        1).ofLp
    ((fun i => i) ⟨0, ⋯⟩)«1»t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ ((fun a b =>
          (WithLp.equiv 2 (Fin 3 → ℝ)).symm
            (((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]) ⋯ ⋯ ⋯
                  ⋯)
                ((WithLp.equiv 2 (Fin 3 → ℝ)) a))
              ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
        s ((fderiv ℝ (fun t' => f t') t) 1)).ofLp
    ((fun i => i) ⟨1, ⋯⟩) =
  ((fderiv ℝ
          (fun t' =>
            (fun a b =>
                (WithLp.equiv 2 (Fin 3 → ℝ)).symm
                  (((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0])
                        ⋯ ⋯ ⋯ ⋯)
                      ((WithLp.equiv 2 (Fin 3 → ℝ)) a))
                    ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
              s (f t'))
          t)
        1).ofLp
    ((fun i => i) ⟨1, ⋯⟩)«2»t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ ((fun a b =>
          (WithLp.equiv 2 (Fin 3 → ℝ)).symm
            (((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]) ⋯ ⋯ ⋯
                  ⋯)
                ((WithLp.equiv 2 (Fin 3 → ℝ)) a))
              ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
        s ((fderiv ℝ (fun t' => f t') t) 1)).ofLp
    ((fun i => i) ⟨2, ⋯⟩) =
  ((fderiv ℝ
          (fun t' =>
            (fun a b =>
                (WithLp.equiv 2 (Fin 3 → ℝ)).symm
                  (((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0])
                        ⋯ ⋯ ⋯ ⋯)
                      ((WithLp.equiv 2 (Fin 3 → ℝ)) a))
                    ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
              s (f t'))
          t)
        1).ofLp
    ((fun i => i) ⟨2, ⋯⟩) <;>«0»t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ ((fun a b =>
          (WithLp.equiv 2 (Fin 3 → ℝ)).symm
            (((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]) ⋯ ⋯ ⋯
                  ⋯)
                ((WithLp.equiv 2 (Fin 3 → ℝ)) a))
              ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
        s ((fderiv ℝ (fun t' => f t') t) 1)).ofLp
    ((fun i => i) ⟨0, ⋯⟩) =
  ((fderiv ℝ
          (fun t' =>
            (fun a b =>
                (WithLp.equiv 2 (Fin 3 → ℝ)).symm
                  (((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0])
                        ⋯ ⋯ ⋯ ⋯)
                      ((WithLp.equiv 2 (Fin 3 → ℝ)) a))
                    ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
              s (f t'))
          t)
        1).ofLp
    ((fun i => i) ⟨0, ⋯⟩)«1»t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ ((fun a b =>
          (WithLp.equiv 2 (Fin 3 → ℝ)).symm
            (((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]) ⋯ ⋯ ⋯
                  ⋯)
                ((WithLp.equiv 2 (Fin 3 → ℝ)) a))
              ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
        s ((fderiv ℝ (fun t' => f t') t) 1)).ofLp
    ((fun i => i) ⟨1, ⋯⟩) =
  ((fderiv ℝ
          (fun t' =>
            (fun a b =>
                (WithLp.equiv 2 (Fin 3 → ℝ)).symm
                  (((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0])
                        ⋯ ⋯ ⋯ ⋯)
                      ((WithLp.equiv 2 (Fin 3 → ℝ)) a))
                    ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
              s (f t'))
          t)
        1).ofLp
    ((fun i => i) ⟨1, ⋯⟩)«2»t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ ((fun a b =>
          (WithLp.equiv 2 (Fin 3 → ℝ)).symm
            (((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]) ⋯ ⋯ ⋯
                  ⋯)
                ((WithLp.equiv 2 (Fin 3 → ℝ)) a))
              ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
        s ((fderiv ℝ (fun t' => f t') t) 1)).ofLp
    ((fun i => i) ⟨2, ⋯⟩) =
  ((fderiv ℝ
          (fun t' =>
            (fun a b =>
                (WithLp.equiv 2 (Fin 3 → ℝ)).symm
                  (((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0])
                        ⋯ ⋯ ⋯ ⋯)
                      ((WithLp.equiv 2 (Fin 3 → ℝ)) a))
                    ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
              s (f t'))
          t)
        1).ofLp
    ((fun i => i) ⟨2, ⋯⟩)
  ·«2»t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ ((fun a b =>
          (WithLp.equiv 2 (Fin 3 → ℝ)).symm
            (((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]) ⋯ ⋯ ⋯
                  ⋯)
                ((WithLp.equiv 2 (Fin 3 → ℝ)) a))
              ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
        s ((fderiv ℝ (fun t' => f t') t) 1)).ofLp
    ((fun i => i) ⟨2, ⋯⟩) =
  ((fderiv ℝ
          (fun t' =>
            (fun a b =>
                (WithLp.equiv 2 (Fin 3 → ℝ)).symm
                  (((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0])
                        ⋯ ⋯ ⋯ ⋯)
                      ((WithLp.equiv 2 (Fin 3 → ℝ)) a))
                    ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
              s (f t'))
          t)
        1).ofLp
    ((fun i => i) ⟨2, ⋯⟩) simp [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, WithLp.equiv_apply,
      LinearMap.mk₂_apply, Fin.reduceFinMk, WithLp.equiv_symm_apply,
      PiLp.toLp_apply, cons_val]«2»t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ s.ofLp 0 * ((fderiv ℝ (fun t' => f t') t) 1).ofLp 1 - s.ofLp 1 * ((fderiv ℝ (fun t' => f t') t) 1).ofLp 0 =
  ((fderiv ℝ
          (fun t' =>
            !₂[s.ofLp 1 * (f t').ofLp 2 - s.ofLp 2 * (f t').ofLp 1, s.ofLp 2 * (f t').ofLp 0 - s.ofLp 0 * (f t').ofLp 2,
              s.ofLp 0 * (f t').ofLp 1 - s.ofLp 1 * (f t').ofLp 0])
          t)
        1).ofLp
    2
    rw [h«0»t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fderiv ℝ (fun t => s.ofLp 1 * (f t).ofLp 2 - s.ofLp 2 * (f t).ofLp 1) t) 1 =
  ((fderiv ℝ
          (fun t' =>
            !₂[s.ofLp 1 * (f t').ofLp 2 - s.ofLp 2 * (f t').ofLp 1, s.ofLp 2 * (f t').ofLp 0 - s.ofLp 0 * (f t').ofLp 2,
              s.ofLp 0 * (f t').ofLp 1 - s.ofLp 1 * (f t').ofLp 0])
          t)
        1).ofLp
    0«2»t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fderiv ℝ (fun t => s.ofLp 0 * (f t).ofLp 1 - s.ofLp 1 * (f t).ofLp 0) t) 1 =
  ((fderiv ℝ
          (fun t' =>
            !₂[s.ofLp 1 * (f t').ofLp 2 - s.ofLp 2 * (f t').ofLp 1, s.ofLp 2 * (f t').ofLp 0 - s.ofLp 0 * (f t').ofLp 2,
              s.ofLp 0 * (f t').ofLp 1 - s.ofLp 1 * (f t').ofLp 0])
          t)
        1).ofLp
    2]«1»t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fderiv ℝ (fun t => s.ofLp 2 * (f t).ofLp 0 - s.ofLp 0 * (f t).ofLp 2) t) 1 =
  ((fderiv ℝ
          (fun t' =>
            !₂[s.ofLp 1 * (f t').ofLp 2 - s.ofLp 2 * (f t').ofLp 1, s.ofLp 2 * (f t').ofLp 0 - s.ofLp 0 * (f t').ofLp 2,
              s.ofLp 0 * (f t').ofLp 1 - s.ofLp 1 * (f t').ofLp 0])
          t)
        1).ofLp
    1«2»t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fderiv ℝ (fun t => s.ofLp 0 * (f t).ofLp 1 - s.ofLp 1 * (f t).ofLp 0) t) 1 =
  ((fderiv ℝ
          (fun t' =>
            !₂[s.ofLp 1 * (f t').ofLp 2 - s.ofLp 2 * (f t').ofLp 1, s.ofLp 2 * (f t').ofLp 0 - s.ofLp 0 * (f t').ofLp 2,
              s.ofLp 0 * (f t').ofLp 1 - s.ofLp 1 * (f t').ofLp 0])
          t)
        1).ofLp
    2«2»t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fderiv ℝ (fun t => s.ofLp 0 * (f t).ofLp 1 - s.ofLp 1 * (f t).ofLp 0) t) 1 =
  ((fderiv ℝ
          (fun t' =>
            !₂[s.ofLp 1 * (f t').ofLp 2 - s.ofLp 2 * (f t').ofLp 1, s.ofLp 2 * (f t').ofLp 0 - s.ofLp 0 * (f t').ofLp 2,
              s.ofLp 0 * (f t').ofLp 1 - s.ofLp 1 * (f t').ofLp 0])
          t)
        1).ofLp
    2
    simp only [Fin.isValue]«2»t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fderiv ℝ (fun t => s.ofLp 0 * (f t).ofLp 1 - s.ofLp 1 * (f t).ofLp 0) t) 1 =
  ((fderiv ℝ
          (fun t' =>
            !₂[s.ofLp 1 * (f t').ofLp 2 - s.ofLp 2 * (f t').ofLp 1, s.ofLp 2 * (f t').ofLp 0 - s.ofLp 0 * (f t').ofLp 2,
              s.ofLp 0 * (f t').ofLp 1 - s.ofLp 1 * (f t').ofLp 0])
          t)
        1).ofLp
    2
    rw [← Time.fderiv_euclid«0»t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fderiv ℝ (fun t => s.ofLp 1 * (f t).ofLp 2 - s.ofLp 2 * (f t).ofLp 1) t) 1 =
  (fderiv ℝ
      (fun t =>
        !₂[s.ofLp 1 * (f t).ofLp 2 - s.ofLp 2 * (f t).ofLp 1, s.ofLp 2 * (f t).ofLp 0 - s.ofLp 0 * (f t).ofLp 2,
              s.ofLp 0 * (f t).ofLp 1 - s.ofLp 1 * (f t).ofLp 0].ofLp
          0)
      t)
    1«0».hft:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ Differentiable ℝ fun t' =>
  !₂[s.ofLp 1 * (f t').ofLp 2 - s.ofLp 2 * (f t').ofLp 1, s.ofLp 2 * (f t').ofLp 0 - s.ofLp 0 * (f t').ofLp 2,
    s.ofLp 0 * (f t').ofLp 1 - s.ofLp 1 * (f t').ofLp 0]«2»t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fderiv ℝ (fun t => s.ofLp 0 * (f t).ofLp 1 - s.ofLp 1 * (f t).ofLp 0) t) 1 =
  (fderiv ℝ
      (fun t =>
        !₂[s.ofLp 1 * (f t).ofLp 2 - s.ofLp 2 * (f t).ofLp 1, s.ofLp 2 * (f t).ofLp 0 - s.ofLp 0 * (f t).ofLp 2,
              s.ofLp 0 * (f t).ofLp 1 - s.ofLp 1 * (f t).ofLp 0].ofLp
          2)
      t)
    1«2».hft:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ Differentiable ℝ fun t' =>
  !₂[s.ofLp 1 * (f t').ofLp 2 - s.ofLp 2 * (f t').ofLp 1, s.ofLp 2 * (f t').ofLp 0 - s.ofLp 0 * (f t').ofLp 2,
    s.ofLp 0 * (f t').ofLp 1 - s.ofLp 1 * (f t').ofLp 0]]«1»t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fderiv ℝ (fun t => s.ofLp 2 * (f t).ofLp 0 - s.ofLp 0 * (f t).ofLp 2) t) 1 =
  (fderiv ℝ
      (fun t =>
        !₂[s.ofLp 1 * (f t).ofLp 2 - s.ofLp 2 * (f t).ofLp 1, s.ofLp 2 * (f t).ofLp 0 - s.ofLp 0 * (f t).ofLp 2,
              s.ofLp 0 * (f t).ofLp 1 - s.ofLp 1 * (f t).ofLp 0].ofLp
          1)
      t)
    1«1».hft:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ Differentiable ℝ fun t' =>
  !₂[s.ofLp 1 * (f t').ofLp 2 - s.ofLp 2 * (f t').ofLp 1, s.ofLp 2 * (f t').ofLp 0 - s.ofLp 0 * (f t').ofLp 2,
    s.ofLp 0 * (f t').ofLp 1 - s.ofLp 1 * (f t').ofLp 0]«2»t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fderiv ℝ (fun t => s.ofLp 0 * (f t).ofLp 1 - s.ofLp 1 * (f t).ofLp 0) t) 1 =
  (fderiv ℝ
      (fun t =>
        !₂[s.ofLp 1 * (f t).ofLp 2 - s.ofLp 2 * (f t).ofLp 1, s.ofLp 2 * (f t).ofLp 0 - s.ofLp 0 * (f t).ofLp 2,
              s.ofLp 0 * (f t).ofLp 1 - s.ofLp 1 * (f t).ofLp 0].ofLp
          2)
      t)
    1«2».hft:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ Differentiable ℝ fun t' =>
  !₂[s.ofLp 1 * (f t').ofLp 2 - s.ofLp 2 * (f t').ofLp 1, s.ofLp 2 * (f t').ofLp 0 - s.ofLp 0 * (f t').ofLp 2,
    s.ofLp 0 * (f t').ofLp 1 - s.ofLp 1 * (f t').ofLp 0]«2»t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ (fderiv ℝ (fun t => s.ofLp 0 * (f t).ofLp 1 - s.ofLp 1 * (f t).ofLp 0) t) 1 =
  (fderiv ℝ
      (fun t =>
        !₂[s.ofLp 1 * (f t).ofLp 2 - s.ofLp 2 * (f t).ofLp 1, s.ofLp 2 * (f t).ofLp 0 - s.ofLp 0 * (f t).ofLp 2,
              s.ofLp 0 * (f t).ofLp 1 - s.ofLp 1 * (f t).ofLp 0].ofLp
          2)
      t)
    1«2».hft:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ Differentiable ℝ fun t' =>
  !₂[s.ofLp 1 * (f t').ofLp 2 - s.ofLp 2 * (f t').ofLp 1, s.ofLp 2 * (f t').ofLp 0 - s.ofLp 0 * (f t').ofLp 2,
    s.ofLp 0 * (f t').ofLp 1 - s.ofLp 1 * (f t').ofLp 0]
    simp [Fin.isValue, cons_val_zero]«2».hft:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ Differentiable ℝ fun t' =>
  !₂[s.ofLp 1 * (f t').ofLp 2 - s.ofLp 2 * (f t').ofLp 1, s.ofLp 2 * (f t').ofLp 0 - s.ofLp 0 * (f t').ofLp 2,
    s.ofLp 0 * (f t').ofLp 1 - s.ofLp 1 * (f t').ofLp 0]
    apply Time.differentiable_euclid«2».hft:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ ∀ (i : Fin 3),
  Differentiable ℝ fun t =>
    !₂[s.ofLp 1 * (f t).ofLp 2 - s.ofLp 2 * (f t).ofLp 1, s.ofLp 2 * (f t).ofLp 0 - s.ofLp 0 * (f t).ofLp 2,
          s.ofLp 0 * (f t).ofLp 1 - s.ofLp 1 * (f t).ofLp 0].ofLp
      i
    intro i«2».hft:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1i:Fin 3⊢ Differentiable ℝ fun t =>
  !₂[s.ofLp 1 * (f t).ofLp 2 - s.ofLp 2 * (f t).ofLp 1, s.ofLp 2 * (f t).ofLp 0 - s.ofLp 0 * (f t).ofLp 2,
        s.ofLp 0 * (f t).ofLp 1 - s.ofLp 1 * (f t).ofLp 0].ofLp
    i
    fin_cases i«2».hf.«0»t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ Differentiable ℝ fun t =>
  !₂[s.ofLp 1 * (f t).ofLp 2 - s.ofLp 2 * (f t).ofLp 1, s.ofLp 2 * (f t).ofLp 0 - s.ofLp 0 * (f t).ofLp 2,
        s.ofLp 0 * (f t).ofLp 1 - s.ofLp 1 * (f t).ofLp 0].ofLp
    ((fun i => i) ⟨0, ⋯⟩)«2».hf.«1»t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ Differentiable ℝ fun t =>
  !₂[s.ofLp 1 * (f t).ofLp 2 - s.ofLp 2 * (f t).ofLp 1, s.ofLp 2 * (f t).ofLp 0 - s.ofLp 0 * (f t).ofLp 2,
        s.ofLp 0 * (f t).ofLp 1 - s.ofLp 1 * (f t).ofLp 0].ofLp
    ((fun i => i) ⟨1, ⋯⟩)«2».hf.«2»t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ Differentiable ℝ fun t =>
  !₂[s.ofLp 1 * (f t).ofLp 2 - s.ofLp 2 * (f t).ofLp 1, s.ofLp 2 * (f t).ofLp 0 - s.ofLp 0 * (f t).ofLp 2,
        s.ofLp 0 * (f t).ofLp 1 - s.ofLp 1 * (f t).ofLp 0].ofLp
    ((fun i => i) ⟨2, ⋯⟩)
    ·«2».hf.«0»t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ Differentiable ℝ fun t =>
  !₂[s.ofLp 1 * (f t).ofLp 2 - s.ofLp 2 * (f t).ofLp 1, s.ofLp 2 * (f t).ofLp 0 - s.ofLp 0 * (f t).ofLp 2,
        s.ofLp 0 * (f t).ofLp 1 - s.ofLp 1 * (f t).ofLp 0].ofLp
    ((fun i => i) ⟨0, ⋯⟩) simp [Fin.zero_eta, Fin.isValue]«2».hf.«0»t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ Differentiable ℝ fun t => s.ofLp 1 * (f t).ofLp 2 - s.ofLp 2 * (f t).ofLp 1
      fun_propAll goals completed! 🐙
    ·«2».hf.«1»t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ Differentiable ℝ fun t =>
  !₂[s.ofLp 1 * (f t).ofLp 2 - s.ofLp 2 * (f t).ofLp 1, s.ofLp 2 * (f t).ofLp 0 - s.ofLp 0 * (f t).ofLp 2,
        s.ofLp 0 * (f t).ofLp 1 - s.ofLp 1 * (f t).ofLp 0].ofLp
    ((fun i => i) ⟨1, ⋯⟩) simp [Fin.isValue]«2».hf.«1»t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ Differentiable ℝ fun t => s.ofLp 2 * (f t).ofLp 0 - s.ofLp 0 * (f t).ofLp 2
      fun_propAll goals completed! 🐙
    ·«2».hf.«2»t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ Differentiable ℝ fun t =>
  !₂[s.ofLp 1 * (f t).ofLp 2 - s.ofLp 2 * (f t).ofLp 1, s.ofLp 2 * (f t).ofLp 0 - s.ofLp 0 * (f t).ofLp 2,
        s.ofLp 0 * (f t).ofLp 1 - s.ofLp 1 * (f t).ofLp 0].ofLp
    ((fun i => i) ⟨2, ⋯⟩) simp [Fin.isValue]«2».hf.«2»t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fh:∀ (i j : Fin 3),
  s.ofLp i * ((fderiv ℝ (fun u => f u) t) 1).ofLp j - s.ofLp j * ((fderiv ℝ (fun u => f u) t) 1).ofLp i =
    (fderiv ℝ (fun t => s.ofLp i * (f t).ofLp j - s.ofLp j * (f t).ofLp i) t) 1⊢ Differentiable ℝ fun t => s.ofLp 0 * (f t).ofLp 1 - s.ofLp 1 * (f t).ofLp 0
      fun_propAll goals completed! 🐙

Cross product and time derivative commute.


lemma time_deriv_cross_commute {s : EuclideanSpace ℝ (Fin 3)} {f : Time → EuclideanSpace ℝ (Fin 3)}
    (hf : Differentiable ℝ f) :
    s ⨯ₑ₃ (∂ₜ (fun t => f t) t) = ∂ₜ (fun t => s ⨯ₑ₃ (f t)) t := byt:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ f⊢ (fun a b =>
      (WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
    s (∂ₜ (fun t => f t) t) =
  ∂ₜ
    (fun t =>
      (fun a b =>
          (WithLp.equiv 2 (Fin 3 → ℝ)).symm
            ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
        s (f t))
    t
  repeat rw [Time.derivt:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ f⊢ (fun a b =>
      (WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
    s ((fderiv ℝ (fun t => f t) t) 1) =
  ∂ₜ
    (fun t =>
      (fun a b =>
          (WithLp.equiv 2 (Fin 3 → ℝ)).symm
            ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
        s (f t))
    tt:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ f⊢ (fun a b =>
      (WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
    s ((fderiv ℝ (fun t => f t) t) 1) =
  (fderiv ℝ
      (fun t =>
        (fun a b =>
            (WithLp.equiv 2 (Fin 3 → ℝ)).symm
              ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
          s (f t))
      t)
    1]t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ f⊢ (fun a b =>
      (WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
    s ((fderiv ℝ (fun t => f t) t) 1) =
  ∂ₜ
    (fun t =>
      (fun a b =>
          (WithLp.equiv 2 (Fin 3 → ℝ)).symm
            ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
        s (f t))
    tt:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ f⊢ (fun a b =>
      (WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
    s ((fderiv ℝ (fun t => f t) t) 1) =
  (fderiv ℝ
      (fun t =>
        (fun a b =>
            (WithLp.equiv 2 (Fin 3 → ℝ)).symm
              ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
          s (f t))
      t)
    1t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ f⊢ (fun a b =>
      (WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
    s ((fderiv ℝ (fun t => f t) t) 1) =
  (fderiv ℝ
      (fun t =>
        (fun a b =>
            (WithLp.equiv 2 (Fin 3 → ℝ)).symm
              ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
          s (f t))
      t)
    1
  rw [fderiv_cross_commutet:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ f⊢ (fderiv ℝ
      (fun t' =>
        (fun a b =>
            (WithLp.equiv 2 (Fin 3 → ℝ)).symm
              ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
          s (f t'))
      t)
    1 =
  (fderiv ℝ
      (fun t =>
        (fun a b =>
            (WithLp.equiv 2 (Fin 3 → ℝ)).symm
              ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
          s (f t))
      t)
    1t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ f⊢ Differentiable ℝ ft:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ f⊢ Differentiable ℝ f]t:Times:EuclideanSpace ℝ (Fin 3)f:Time → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ f⊢ Differentiable ℝ f
  fun_propAll goals completed! 🐙

C. Inner product of vectors with cross products involving themselves



lemma inner_cross_self (v w : EuclideanSpace ℝ (Fin 3)) :
    inner ℝ v (w ⨯ₑ₃ v) = 0 := byv:EuclideanSpace ℝ (Fin 3)w:EuclideanSpace ℝ (Fin 3)⊢ inner ℝ v
    ((fun a b =>
        (WithLp.equiv 2 (Fin 3 → ℝ)).symm
          ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
      w v) =
  0
  cases v using WithLp.rec with | _ v =>toLpw:EuclideanSpace ℝ (Fin 3)v:(i : Fin 3) → (fun x => ℝ) i⊢ inner ℝ (WithLp.toLp 2 v)
    ((fun a b =>
        (WithLp.equiv 2 (Fin 3 → ℝ)).symm
          ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
      w (WithLp.toLp 2 v)) =
  0
  cases w using WithLp.rec with | _ w =>toLp.toLpv:(i : Fin 3) → (fun x => ℝ) iw:(i : Fin 3) → (fun x => ℝ) i⊢ inner ℝ (WithLp.toLp 2 v)
    ((fun a b =>
        (WithLp.equiv 2 (Fin 3 → ℝ)).symm
          ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
      (WithLp.toLp 2 w) (WithLp.toLp 2 v)) =
  0
  simp only [WithLp.equiv_apply, WithLp.equiv_symm_apply]toLp.toLpv:(i : Fin 3) → (fun x => ℝ) iw:(i : Fin 3) → (fun x => ℝ) i⊢ inner ℝ (WithLp.toLp 2 v) (WithLp.toLp 2 ((crossProduct w) v)) = 0
  change (crossProduct w) v ⬝ᵥ v = _toLp.toLpv:(i : Fin 3) → (fun x => ℝ) iw:(i : Fin 3) → (fun x => ℝ) i⊢ (crossProduct w) v ⬝ᵥ v = 0
  rw [dotProduct_comm,toLp.toLpv:(i : Fin 3) → (fun x => ℝ) iw:(i : Fin 3) → (fun x => ℝ) i⊢ v ⬝ᵥ (crossProduct w) v = 0All goals completed! 🐙 dot_cross_selftoLp.toLpv:(i : Fin 3) → (fun x => ℝ) iw:(i : Fin 3) → (fun x => ℝ) i⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙



lemma inner_self_cross (v w : EuclideanSpace ℝ (Fin 3)) :
    inner ℝ v (v ⨯ₑ₃ w) = 0 := byv:EuclideanSpace ℝ (Fin 3)w:EuclideanSpace ℝ (Fin 3)⊢ inner ℝ v
    ((fun a b =>
        (WithLp.equiv 2 (Fin 3 → ℝ)).symm
          ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
      v w) =
  0
  cases v using WithLp.rec with | _ v =>toLpw:EuclideanSpace ℝ (Fin 3)v:(i : Fin 3) → (fun x => ℝ) i⊢ inner ℝ (WithLp.toLp 2 v)
    ((fun a b =>
        (WithLp.equiv 2 (Fin 3 → ℝ)).symm
          ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
      (WithLp.toLp 2 v) w) =
  0
  cases w using WithLp.rec with | _ w =>toLp.toLpv:(i : Fin 3) → (fun x => ℝ) iw:(i : Fin 3) → (fun x => ℝ) i⊢ inner ℝ (WithLp.toLp 2 v)
    ((fun a b =>
        (WithLp.equiv 2 (Fin 3 → ℝ)).symm
          ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b)))
      (WithLp.toLp 2 v) (WithLp.toLp 2 w)) =
  0
  simp only [WithLp.equiv_apply, WithLp.equiv_symm_apply, PiLp.inner_apply]toLp.toLpv:(i : Fin 3) → (fun x => ℝ) iw:(i : Fin 3) → (fun x => ℝ) i⊢ ∑ x, inner ℝ (v x) ((crossProduct v) w x) = 0
  change (crossProduct v) w ⬝ᵥ v = _toLp.toLpv:(i : Fin 3) → (fun x => ℝ) iw:(i : Fin 3) → (fun x => ℝ) i⊢ (crossProduct v) w ⬝ᵥ v = 0
  rw [dotProduct_comm,toLp.toLpv:(i : Fin 3) → (fun x => ℝ) iw:(i : Fin 3) → (fun x => ℝ) i⊢ v ⬝ᵥ (crossProduct v) w = 0All goals completed! 🐙 dot_self_crosstoLp.toLpv:(i : Fin 3) → (fun x => ℝ) iw:(i : Fin 3) → (fun x => ℝ) i⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙