Physlib.Electromagnetism.Distributional.Dynamics.KineticTerm

Imports

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

public import Physlib.Electromagnetism.Distributional.MagneticField
public import Physlib.Electromagnetism.Dynamics.Basic
public import Physlib.Mathematics.VariationalCalculus.HasVarGradient

The kinetic term

i. Overview

The kinetic term of the electromagnetic field is - 1/(4 μ₀) F_μν F^μν. We define this, show it is invariant under Lorentz transformations, and show properties of its variational gradient.

In particular the variational gradient gradKineticTerm of the kinetic term is directly related to Gauss's law and the Ampere law.

In this implementation we have set μ₀ = 1. It is a TODO to introduce this constant.

ii. Key results

DistElectromagneticPotential.gradKineticTerm is the variational gradient of the kinetic term for distributional electromagnetic potentials.

iii. Table of contents

A. The gradient of the kinetic term for distributions

A.1. The gradient of the kinetic term as a tensor

iv. References

https://quantummechanics.ucsd.edu/ph130a/130_notes/node452.html

@[expose] public section

A. The gradient of the kinetic term for distributions

For distributions we define the gradient of the kinetic term directly using ElectromagneticPotential.gradKineticTerm_eq_sum_sum as the defining formula.

              attribute [-simp] Fintype.sum_sum_typeattribute [-simp] Nat.succ_eq_add_onelemma gradKineticTerm_eq_sum_sum {d} {𝓕 : FreeSpace}
    (A : DistElectromagneticPotential d) (ε : 𝓢(SpaceTime d, ℝ)) :
    A.gradKineticTerm 𝓕 ε = ∑ ν, ∑ μ,
        (1 / (𝓕.μ₀) * (η μ μ * η ν ν * distDeriv μ (distDeriv μ A) ε ν -
        distDeriv μ (distDeriv ν A) ε μ)) • Lorentz.Vector.basis ν := rfl

lemma gradKineticTerm_eq_fieldStrength {d} {𝓕 : FreeSpace} (A : DistElectromagneticPotential d)
    (ε : 𝓢(SpaceTime d, ℝ)) :
    A.gradKineticTerm 𝓕 ε = ∑ ν, (1/𝓕.μ₀ * η ν ν) •
    (∑ μ, ((Vector.basis.tensorProduct Vector.basis).repr
      (distDeriv μ (A.fieldStrength) ε) (μ, ν))) • Lorentz.Vector.basis ν := byd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)⊢ ((gradKineticTerm 𝓕) A) ε =
  ∑ ν,
    (1 / 𝓕.μ₀ * η ν ν) •
      (∑ μ, ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, ν)) •
        Vector.basis ν
  rw [gradKineticTerm_eq_sum_sum Ad:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)⊢ ∑ ν,
    ∑ μ,
      (1 / 𝓕.μ₀ * (η μ μ * η ν ν * ((distDeriv μ) ((distDeriv μ) A)) ε ν - ((distDeriv μ) ((distDeriv ν) A)) ε μ)) •
        Vector.basis ν =
  ∑ ν,
    (1 / 𝓕.μ₀ * η ν ν) •
      (∑ μ, ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, ν)) •
        Vector.basis νd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)⊢ ∑ ν,
    ∑ μ,
      (1 / 𝓕.μ₀ * (η μ μ * η ν ν * ((distDeriv μ) ((distDeriv μ) A)) ε ν - ((distDeriv μ) ((distDeriv ν) A)) ε μ)) •
        Vector.basis ν =
  ∑ ν,
    (1 / 𝓕.μ₀ * η ν ν) •
      (∑ μ, ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, ν)) •
        Vector.basis ν]d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)⊢ ∑ ν,
    ∑ μ,
      (1 / 𝓕.μ₀ * (η μ μ * η ν ν * ((distDeriv μ) ((distDeriv μ) A)) ε ν - ((distDeriv μ) ((distDeriv ν) A)) ε μ)) •
        Vector.basis ν =
  ∑ ν,
    (1 / 𝓕.μ₀ * η ν ν) •
      (∑ μ, ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, ν)) •
        Vector.basis ν
  apply Finset.sum_congr rfl (fun ν _ => ?_)d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ ∑ μ,
    (1 / 𝓕.μ₀ * (η μ μ * η ν ν * ((distDeriv μ) ((distDeriv μ) A)) ε ν - ((distDeriv μ) ((distDeriv ν) A)) ε μ)) •
      Vector.basis ν =
  (1 / 𝓕.μ₀ * η ν ν) •
    (∑ μ, ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, ν)) •
      Vector.basis ν
  rw [smul_smul,d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ ∑ μ,
    (1 / 𝓕.μ₀ * (η μ μ * η ν ν * ((distDeriv μ) ((distDeriv μ) A)) ε ν - ((distDeriv μ) ((distDeriv ν) A)) ε μ)) •
      Vector.basis ν =
  (1 / 𝓕.μ₀ * η ν ν *
      ∑ μ, ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, ν)) •
    Vector.basis νd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ (1 / 𝓕.μ₀ * ∑ i, (η i i * η ν ν * ((distDeriv i) ((distDeriv i) A)) ε ν - ((distDeriv i) ((distDeriv ν) A)) ε i)) •
    Vector.basis ν =
  (1 / 𝓕.μ₀ *
      (η ν ν * ∑ μ, ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, ν))) •
    Vector.basis ν ← Finset.sum_smul,d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ (∑ i, 1 / 𝓕.μ₀ * (η i i * η ν ν * ((distDeriv i) ((distDeriv i) A)) ε ν - ((distDeriv i) ((distDeriv ν) A)) ε i)) •
    Vector.basis ν =
  (1 / 𝓕.μ₀ * η ν ν *
      ∑ μ, ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, ν)) •
    Vector.basis νd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ (1 / 𝓕.μ₀ * ∑ i, (η i i * η ν ν * ((distDeriv i) ((distDeriv i) A)) ε ν - ((distDeriv i) ((distDeriv ν) A)) ε i)) •
    Vector.basis ν =
  (1 / 𝓕.μ₀ *
      (η ν ν * ∑ μ, ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, ν))) •
    Vector.basis ν ← Finset.mul_sum,d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ (1 / 𝓕.μ₀ * ∑ i, (η i i * η ν ν * ((distDeriv i) ((distDeriv i) A)) ε ν - ((distDeriv i) ((distDeriv ν) A)) ε i)) •
    Vector.basis ν =
  (1 / 𝓕.μ₀ * η ν ν *
      ∑ μ, ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, ν)) •
    Vector.basis νd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ (1 / 𝓕.μ₀ * ∑ i, (η i i * η ν ν * ((distDeriv i) ((distDeriv i) A)) ε ν - ((distDeriv i) ((distDeriv ν) A)) ε i)) •
    Vector.basis ν =
  (1 / 𝓕.μ₀ *
      (η ν ν * ∑ μ, ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, ν))) •
    Vector.basis ν mul_assocd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ (1 / 𝓕.μ₀ * ∑ i, (η i i * η ν ν * ((distDeriv i) ((distDeriv i) A)) ε ν - ((distDeriv i) ((distDeriv ν) A)) ε i)) •
    Vector.basis ν =
  (1 / 𝓕.μ₀ *
      (η ν ν * ∑ μ, ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, ν))) •
    Vector.basis νd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ (1 / 𝓕.μ₀ * ∑ i, (η i i * η ν ν * ((distDeriv i) ((distDeriv i) A)) ε ν - ((distDeriv i) ((distDeriv ν) A)) ε i)) •
    Vector.basis ν =
  (1 / 𝓕.μ₀ *
      (η ν ν * ∑ μ, ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, ν))) •
    Vector.basis ν]d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ (1 / 𝓕.μ₀ * ∑ i, (η i i * η ν ν * ((distDeriv i) ((distDeriv i) A)) ε ν - ((distDeriv i) ((distDeriv ν) A)) ε i)) •
    Vector.basis ν =
  (1 / 𝓕.μ₀ *
      (η ν ν * ∑ μ, ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, ν))) •
    Vector.basis ν
  congr 2e_a.e_ad:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ ∑ i, (η i i * η ν ν * ((distDeriv i) ((distDeriv i) A)) ε ν - ((distDeriv i) ((distDeriv ν) A)) ε i) =
  η ν ν * ∑ μ, ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, ν)
  rw [Finset.mul_sume_a.e_ad:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ ∑ i, (η i i * η ν ν * ((distDeriv i) ((distDeriv i) A)) ε ν - ((distDeriv i) ((distDeriv ν) A)) ε i) =
  ∑ i, η ν ν * ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv i) (fieldStrength A)) ε)) (i, ν)e_a.e_ad:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ ∑ i, (η i i * η ν ν * ((distDeriv i) ((distDeriv i) A)) ε ν - ((distDeriv i) ((distDeriv ν) A)) ε i) =
  ∑ i, η ν ν * ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv i) (fieldStrength A)) ε)) (i, ν)]e_a.e_ad:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ ∑ i, (η i i * η ν ν * ((distDeriv i) ((distDeriv i) A)) ε ν - ((distDeriv i) ((distDeriv ν) A)) ε i) =
  ∑ i, η ν ν * ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv i) (fieldStrength A)) ε)) (i, ν)
  apply Finset.sum_congr rfl (fun μ _ => ?_)d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dx✝¹:ν ∈ Finset.univμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univ⊢ η μ μ * η ν ν * ((distDeriv μ) ((distDeriv μ) A)) ε ν - ((distDeriv μ) ((distDeriv ν) A)) ε μ =
  η ν ν * ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, ν)
  conv_rhs =>
    rw [distDeriv_apply, Distribution.fderivD_apply, map_neg]d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dx✝¹:ν ∈ Finset.univμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univ| η ν ν *
  (-(Vector.basis.tensorProduct Vector.basis).repr
        ((fieldStrength A)
          ((SchwartzMap.evalCLM ℝ (SpaceTime d) ℝ (Vector.basis μ)) ((fderivCLM ℝ (SpaceTime d) ℝ) ε))))
    (μ, ν)
    simp only [Finsupp.coe_neg, Pi.neg_apply, mul_neg]d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dx✝¹:ν ∈ Finset.univμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univ| -(η ν ν *
    ((Vector.basis.tensorProduct Vector.basis).repr
        ((fieldStrength A)
          ((SchwartzMap.evalCLM ℝ (SpaceTime d) ℝ (Vector.basis μ)) ((fderivCLM ℝ (SpaceTime d) ℝ) ε))))
      (μ, ν))
    rw [fieldStrength_basis_repr_eq_single]d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dx✝¹:ν ∈ Finset.univμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univ| -(η ν ν *
    (η (μ, ν).1 (μ, ν).1 *
        ((distDeriv (μ, ν).1) A)
          ((SchwartzMap.evalCLM ℝ (SpaceTime d) ℝ (Vector.basis μ)) ((fderivCLM ℝ (SpaceTime d) ℝ) ε)) (μ, ν).2 -
      η (μ, ν).2 (μ, ν).2 *
        ((distDeriv (μ, ν).2) A)
          ((SchwartzMap.evalCLM ℝ (SpaceTime d) ℝ (Vector.basis μ)) ((fderivCLM ℝ (SpaceTime d) ℝ) ε)) (μ, ν).1))
    simp onlyd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dx✝¹:ν ∈ Finset.univμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univ| -(η ν ν *
    (η μ μ *
        ((distDeriv μ) A) ((SchwartzMap.evalCLM ℝ (SpaceTime d) ℝ (Vector.basis μ)) ((fderivCLM ℝ (SpaceTime d) ℝ) ε))
          ν -
      η ν ν *
        ((distDeriv ν) A) ((SchwartzMap.evalCLM ℝ (SpaceTime d) ℝ (Vector.basis μ)) ((fderivCLM ℝ (SpaceTime d) ℝ) ε))
          μ))
    rw [SpaceTime.apply_fderiv_eq_distDeriv, SpaceTime.apply_fderiv_eq_distDeriv]d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dx✝¹:ν ∈ Finset.univμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univ| -(η ν ν * (η μ μ * (-((distDeriv μ) ((distDeriv μ) A)) ε) ν - η ν ν * (-((distDeriv μ) ((distDeriv ν) A)) ε) μ))
    simpd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dx✝¹:ν ∈ Finset.univμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univ| -(η ν ν * (-(η μ μ * ((distDeriv μ) ((distDeriv μ) A)) ε ν) + η ν ν * ((distDeriv μ) ((distDeriv ν) A)) ε μ))
  ring_nfd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dx✝¹:ν ∈ Finset.univμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univ⊢ η μ μ * η ν ν * ((distDeriv μ) ((distDeriv μ) A)) ε ν - ((distDeriv μ) ((distDeriv ν) A)) ε μ =
  η μ μ * η ν ν * ((distDeriv μ) ((distDeriv μ) A)) ε ν - η ν ν ^ 2 * ((distDeriv μ) ((distDeriv ν) A)) ε μ
  simpAll goals completed! 🐙

lemma gradKineticTerm_sum_inl_eq {d} {𝓕 : FreeSpace}
    (A : DistElectromagneticPotential d) (ε : 𝓢(SpaceTime d, ℝ)) :
    A.gradKineticTerm 𝓕 ε (Sum.inl 0) =
    (1/(𝓕.μ₀ * 𝓕.c) * (distTimeSlice 𝓕.c).symm (Space.distSpaceDiv (A.electricField 𝓕.c)) ε) := byd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)⊢ ((gradKineticTerm 𝓕) A) ε (Sum.inl 0) =
  1 / (𝓕.μ₀ * 𝓕.c.val) * ((distTimeSlice 𝓕.c).symm (Space.distSpaceDiv ((electricField 𝓕.c) A))) ε
  rw [gradKineticTerm_eq_fieldStrength A ε,d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)⊢ (∑ ν,
      (1 / 𝓕.μ₀ * η ν ν) •
        (∑ μ, ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, ν)) •
          Vector.basis ν)
    (Sum.inl 0) =
  1 / (𝓕.μ₀ * 𝓕.c.val) * ((distTimeSlice 𝓕.c).symm (Space.distSpaceDiv ((electricField 𝓕.c) A))) εd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)⊢ ∑ j,
    ((1 / 𝓕.μ₀ * η j j) •
        (∑ μ, ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, j)) •
          Vector.basis j)
      (Sum.inl 0) =
  ∑ i,
    1 / (𝓕.μ₀ * 𝓕.c.val) *
      (((Space.distSpaceDeriv i) ((electricField 𝓕.c) A))
            ((compCLMOfContinuousLinearEquiv ℝ (toTimeAndSpace 𝓕.c).symm) ε)).ofLp
        i Lorentz.Vector.apply_sum,d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)⊢ ∑ j,
    ((1 / 𝓕.μ₀ * η j j) •
        (∑ μ, ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, j)) •
          Vector.basis j)
      (Sum.inl 0) =
  1 / (𝓕.μ₀ * 𝓕.c.val) * ((distTimeSlice 𝓕.c).symm (Space.distSpaceDiv ((electricField 𝓕.c) A))) εd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)⊢ ∑ j,
    ((1 / 𝓕.μ₀ * η j j) •
        (∑ μ, ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, j)) •
          Vector.basis j)
      (Sum.inl 0) =
  ∑ i,
    1 / (𝓕.μ₀ * 𝓕.c.val) *
      (((Space.distSpaceDeriv i) ((electricField 𝓕.c) A))
            ((compCLMOfContinuousLinearEquiv ℝ (toTimeAndSpace 𝓕.c).symm) ε)).ofLp
        i distTimeSlice_symm_apply,d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)⊢ ∑ j,
    ((1 / 𝓕.μ₀ * η j j) •
        (∑ μ, ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, j)) •
          Vector.basis j)
      (Sum.inl 0) =
  1 / (𝓕.μ₀ * 𝓕.c.val) *
    (Space.distSpaceDiv ((electricField 𝓕.c) A)) ((compCLMOfContinuousLinearEquiv ℝ (toTimeAndSpace 𝓕.c).symm) ε)d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)⊢ ∑ j,
    ((1 / 𝓕.μ₀ * η j j) •
        (∑ μ, ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, j)) •
          Vector.basis j)
      (Sum.inl 0) =
  ∑ i,
    1 / (𝓕.μ₀ * 𝓕.c.val) *
      (((Space.distSpaceDeriv i) ((electricField 𝓕.c) A))
            ((compCLMOfContinuousLinearEquiv ℝ (toTimeAndSpace 𝓕.c).symm) ε)).ofLp
        i
    Space.distSpaceDiv_apply_eq_sum_distSpaceDeriv,d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)⊢ ∑ j,
    ((1 / 𝓕.μ₀ * η j j) •
        (∑ μ, ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, j)) •
          Vector.basis j)
      (Sum.inl 0) =
  1 / (𝓕.μ₀ * 𝓕.c.val) *
    ∑ i,
      (((Space.distSpaceDeriv i) ((electricField 𝓕.c) A))
            ((compCLMOfContinuousLinearEquiv ℝ (toTimeAndSpace 𝓕.c).symm) ε)).ofLp
        id:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)⊢ ∑ j,
    ((1 / 𝓕.μ₀ * η j j) •
        (∑ μ, ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, j)) •
          Vector.basis j)
      (Sum.inl 0) =
  ∑ i,
    1 / (𝓕.μ₀ * 𝓕.c.val) *
      (((Space.distSpaceDeriv i) ((electricField 𝓕.c) A))
            ((compCLMOfContinuousLinearEquiv ℝ (toTimeAndSpace 𝓕.c).symm) ε)).ofLp
        i Finset.mul_sumd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)⊢ ∑ j,
    ((1 / 𝓕.μ₀ * η j j) •
        (∑ μ, ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, j)) •
          Vector.basis j)
      (Sum.inl 0) =
  ∑ i,
    1 / (𝓕.μ₀ * 𝓕.c.val) *
      (((Space.distSpaceDeriv i) ((electricField 𝓕.c) A))
            ((compCLMOfContinuousLinearEquiv ℝ (toTimeAndSpace 𝓕.c).symm) ε)).ofLp
        id:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)⊢ ∑ j,
    ((1 / 𝓕.μ₀ * η j j) •
        (∑ μ, ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, j)) •
          Vector.basis j)
      (Sum.inl 0) =
  ∑ i,
    1 / (𝓕.μ₀ * 𝓕.c.val) *
      (((Space.distSpaceDeriv i) ((electricField 𝓕.c) A))
            ((compCLMOfContinuousLinearEquiv ℝ (toTimeAndSpace 𝓕.c).symm) ε)).ofLp
        i]d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)⊢ ∑ j,
    ((1 / 𝓕.μ₀ * η j j) •
        (∑ μ, ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, j)) •
          Vector.basis j)
      (Sum.inl 0) =
  ∑ i,
    1 / (𝓕.μ₀ * 𝓕.c.val) *
      (((Space.distSpaceDeriv i) ((electricField 𝓕.c) A))
            ((compCLMOfContinuousLinearEquiv ℝ (toTimeAndSpace 𝓕.c).symm) ε)).ofLp
        i
  simp [Fintype.sum_sum_type, Finset.mul_sum]d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)⊢ ∑ i,
    𝓕.μ₀⁻¹ *
      ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv (Sum.inr i)) (fieldStrength A)) ε))
        (Sum.inr i, Sum.inl 0) =
  ∑ x,
    𝓕.c.val⁻¹ * 𝓕.μ₀⁻¹ *
      (((Space.distSpaceDeriv x) ((electricField 𝓕.c) A))
            ((compCLMOfContinuousLinearEquiv ℝ (toTimeAndSpace 𝓕.c).symm) ε)).ofLp
        x
  apply Finset.sum_congr rfl (fun ν _ => ?_)d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin dx✝:ν ∈ Finset.univ⊢ 𝓕.μ₀⁻¹ *
    ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv (Sum.inr ν)) (fieldStrength A)) ε))
      (Sum.inr ν, Sum.inl 0) =
  𝓕.c.val⁻¹ * 𝓕.μ₀⁻¹ *
    (((Space.distSpaceDeriv ν) ((electricField 𝓕.c) A))
          ((compCLMOfContinuousLinearEquiv ℝ (toTimeAndSpace 𝓕.c).symm) ε)).ofLp
      ν
  rw [← distTimeSlice_symm_applyd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin dx✝:ν ∈ Finset.univ⊢ 𝓕.μ₀⁻¹ *
    ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv (Sum.inr ν)) (fieldStrength A)) ε))
      (Sum.inr ν, Sum.inl 0) =
  𝓕.c.val⁻¹ * 𝓕.μ₀⁻¹ * (((distTimeSlice 𝓕.c).symm ((Space.distSpaceDeriv ν) ((electricField 𝓕.c) A))) ε).ofLp νd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin dx✝:ν ∈ Finset.univ⊢ 𝓕.μ₀⁻¹ *
    ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv (Sum.inr ν)) (fieldStrength A)) ε))
      (Sum.inr ν, Sum.inl 0) =
  𝓕.c.val⁻¹ * 𝓕.μ₀⁻¹ * (((distTimeSlice 𝓕.c).symm ((Space.distSpaceDeriv ν) ((electricField 𝓕.c) A))) ε).ofLp ν]d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin dx✝:ν ∈ Finset.univ⊢ 𝓕.μ₀⁻¹ *
    ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv (Sum.inr ν)) (fieldStrength A)) ε))
      (Sum.inr ν, Sum.inl 0) =
  𝓕.c.val⁻¹ * 𝓕.μ₀⁻¹ * (((distTimeSlice 𝓕.c).symm ((Space.distSpaceDeriv ν) ((electricField 𝓕.c) A))) ε).ofLp ν
  conv_rhs =>
    enter [2]d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin dx✝:ν ∈ Finset.univ| (((distTimeSlice 𝓕.c).symm ((Space.distSpaceDeriv ν) ((electricField 𝓕.c) A))) ε).ofLp ν
    rw [distTimeSlice_symm_apply, Space.distSpaceDeriv_apply']d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin dx✝:ν ∈ Finset.univ| (-((electricField 𝓕.c) A)
        ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, Space.basis ν))
          ((fderivCLM ℝ (Time × Space d) ℝ) ((compCLMOfContinuousLinearEquiv ℝ (toTimeAndSpace 𝓕.c).symm) ε)))).ofLp
  ν
    simp only [PiLp.neg_apply]d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin dx✝:ν ∈ Finset.univ| -(((electricField 𝓕.c) A)
        ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, Space.basis ν))
          ((fderivCLM ℝ (Time × Space d) ℝ) ((compCLMOfContinuousLinearEquiv ℝ (toTimeAndSpace 𝓕.c).symm) ε)))).ofLp
    ν
    rw [electricField_eq_fieldStrength, distTimeSlice_apply]d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin dx✝:ν ∈ Finset.univ| -(-𝓕.c.val *
    ((Vector.basis.tensorProduct Vector.basis).repr
        ((fieldStrength A)
          ((compCLMOfContinuousLinearEquiv ℝ (toTimeAndSpace 𝓕.c))
            ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, Space.basis ν))
              ((fderivCLM ℝ (Time × Space d) ℝ) ((compCLMOfContinuousLinearEquiv ℝ (toTimeAndSpace 𝓕.c).symm) ε))))))
      (Sum.inl 0, Sum.inr ν))
    simp only [Fin.isValue, neg_mul, neg_neg]d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin dx✝:ν ∈ Finset.univ| 𝓕.c.val *
  ((Vector.basis.tensorProduct Vector.basis).repr
      ((fieldStrength A)
        ((compCLMOfContinuousLinearEquiv ℝ (toTimeAndSpace 𝓕.c))
          ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, Space.basis ν))
            ((fderivCLM ℝ (Time × Space d) ℝ) ((compCLMOfContinuousLinearEquiv ℝ (toTimeAndSpace 𝓕.c).symm) ε))))))
    (Sum.inl 0, Sum.inr ν)
    rw [fieldStrength_antisymmetric_basis]d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin dx✝:ν ∈ Finset.univ| 𝓕.c.val *
  -((Vector.basis.tensorProduct Vector.basis).repr
        ((fieldStrength A)
          ((compCLMOfContinuousLinearEquiv ℝ (toTimeAndSpace 𝓕.c))
            ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, Space.basis ν))
              ((fderivCLM ℝ (Time × Space d) ℝ) ((compCLMOfContinuousLinearEquiv ℝ (toTimeAndSpace 𝓕.c).symm) ε))))))
      (Sum.inr ν, Sum.inl 0)
    rw [← distTimeSlice_apply, Space.apply_fderiv_eq_distSpaceDeriv, ← distTimeSlice_symm_apply,
      ← distTimeSlice_distDeriv_inr]d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin dx✝:ν ∈ Finset.univ| 𝓕.c.val *
  -((Vector.basis.tensorProduct Vector.basis).repr
        (-((distTimeSlice 𝓕.c).symm ((distTimeSlice 𝓕.c) ((distDeriv (Sum.inr ν)) (fieldStrength A)))) ε))
      (Sum.inr ν, Sum.inl 0)
    simpd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin dx✝:ν ∈ Finset.univ| 𝓕.c.val *
  ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv (Sum.inr ν)) (fieldStrength A)) ε))
    (Sum.inr ν, Sum.inl 0)
  field_simpAll goals completed! 🐙lemma gradKineticTerm_sum_inr_eq {d} {𝓕 : FreeSpace}
    (A : DistElectromagneticPotential d) (ε : 𝓢(SpaceTime d, ℝ)) (i : Fin d) :
    A.gradKineticTerm 𝓕 ε (Sum.inr i) =
    (𝓕.μ₀⁻¹ * (1 / 𝓕.c ^ 2 * (distTimeSlice 𝓕.c).symm
      (Space.distTimeDeriv (A.electricField 𝓕.c)) ε i -
      ∑ j, ((PiLp.basisFun 2 ℝ (Fin d)).tensorProduct (PiLp.basisFun 2 ℝ (Fin d))).repr
        ((distTimeSlice 𝓕.c).symm (Space.distSpaceDeriv j
          (A.magneticFieldMatrix 𝓕.c)) ε) (j, i))) := byd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)i:Fin d⊢ ((gradKineticTerm 𝓕) A) ε (Sum.inr i) =
  𝓕.μ₀⁻¹ *
    (1 / 𝓕.c.val ^ 2 * (((distTimeSlice 𝓕.c).symm (Space.distTimeDeriv ((electricField 𝓕.c) A))) ε).ofLp i -
      ∑ j,
        (((PiLp.basisFun 2 ℝ (Fin d)).tensorProduct (PiLp.basisFun 2 ℝ (Fin d))).repr
            (((distTimeSlice 𝓕.c).symm ((Space.distSpaceDeriv j) ((magneticFieldMatrix 𝓕.c) A))) ε))
          (j, i))
  simp [gradKineticTerm_eq_fieldStrength A ε, Lorentz.Vector.apply_sum,
    Fintype.sum_sum_type, mul_add, sub_eq_add_neg]d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)i:Fin d⊢ -(𝓕.μ₀⁻¹ *
        ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv (Sum.inl 0)) (fieldStrength A)) ε))
          (Sum.inl 0, Sum.inr i)) +
    -(𝓕.μ₀⁻¹ *
        ∑ a₂,
          ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv (Sum.inr a₂)) (fieldStrength A)) ε))
            (Sum.inr a₂, Sum.inr i)) =
  𝓕.μ₀⁻¹ * ((𝓕.c.val ^ 2)⁻¹ * (((distTimeSlice 𝓕.c).symm (Space.distTimeDeriv ((electricField 𝓕.c) A))) ε).ofLp i) +
    -(𝓕.μ₀⁻¹ *
        ∑ j,
          (((PiLp.basisFun 2 ℝ (Fin d)).tensorProduct (PiLp.basisFun 2 ℝ (Fin d))).repr
              (((distTimeSlice 𝓕.c).symm ((Space.distSpaceDeriv j) ((magneticFieldMatrix 𝓕.c) A))) ε))
            (j, i))
  congre_ad:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)i:Fin d⊢ -(𝓕.μ₀⁻¹ *
      ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv (Sum.inl 0)) (fieldStrength A)) ε))
        (Sum.inl 0, Sum.inr i)) =
  𝓕.μ₀⁻¹ * ((𝓕.c.val ^ 2)⁻¹ * (((distTimeSlice 𝓕.c).symm (Space.distTimeDeriv ((electricField 𝓕.c) A))) ε).ofLp i)e_a.e_a.e_fd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)i:Fin d⊢ (fun a₂ =>
    ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv (Sum.inr a₂)) (fieldStrength A)) ε))
      (Sum.inr a₂, Sum.inr i)) =
  fun j =>
  (((PiLp.basisFun 2 ℝ (Fin d)).tensorProduct (PiLp.basisFun 2 ℝ (Fin d))).repr
      (((distTimeSlice 𝓕.c).symm ((Space.distSpaceDeriv j) ((magneticFieldMatrix 𝓕.c) A))) ε))
    (j, i)
  ·e_ad:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)i:Fin d⊢ -(𝓕.μ₀⁻¹ *
      ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv (Sum.inl 0)) (fieldStrength A)) ε))
        (Sum.inl 0, Sum.inr i)) =
  𝓕.μ₀⁻¹ * ((𝓕.c.val ^ 2)⁻¹ * (((distTimeSlice 𝓕.c).symm (Space.distTimeDeriv ((electricField 𝓕.c) A))) ε).ofLp i) conv_rhs =>
      enter [2, 2]d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)i:Fin d| (((distTimeSlice 𝓕.c).symm (Space.distTimeDeriv ((electricField 𝓕.c) A))) ε).ofLp i
      rw [distTimeSlice_symm_apply, Space.distTimeDeriv_apply']d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)i:Fin d| (-((electricField 𝓕.c) A)
        ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (1, 0))
          ((fderivCLM ℝ (Time × Space d) ℝ) ((compCLMOfContinuousLinearEquiv ℝ (toTimeAndSpace 𝓕.c).symm) ε)))).ofLp
  i
      simp only [PiLp.neg_apply]d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)i:Fin d| -(((electricField 𝓕.c) A)
        ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (1, 0))
          ((fderivCLM ℝ (Time × Space d) ℝ) ((compCLMOfContinuousLinearEquiv ℝ (toTimeAndSpace 𝓕.c).symm) ε)))).ofLp
    i
      rw [electricField_eq_fieldStrength, Space.apply_fderiv_eq_distTimeDeriv,
        ← distTimeSlice_symm_apply]d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)i:Fin d| -(-𝓕.c.val *
    ((Vector.basis.tensorProduct Vector.basis).repr
        (-((distTimeSlice 𝓕.c).symm (Space.distTimeDeriv ((distTimeSlice 𝓕.c) (fieldStrength A)))) ε))
      (Sum.inl 0, Sum.inr i))
      simp [distTimeSlice_symm_distTimeDeriv_eq]d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)i:Fin d| -(𝓕.c.val *
    (𝓕.c.val *
      ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv (Sum.inl 0)) (fieldStrength A)) ε))
        (Sum.inl 0, Sum.inr i)))
    field_simpAll goals completed! 🐙
  ·e_a.e_a.e_fd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)i:Fin d⊢ (fun a₂ =>
    ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv (Sum.inr a₂)) (fieldStrength A)) ε))
      (Sum.inr a₂, Sum.inr i)) =
  fun j =>
  (((PiLp.basisFun 2 ℝ (Fin d)).tensorProduct (PiLp.basisFun 2 ℝ (Fin d))).repr
      (((distTimeSlice 𝓕.c).symm ((Space.distSpaceDeriv j) ((magneticFieldMatrix 𝓕.c) A))) ε))
    (j, i) ext ke_a.e_a.e_fd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)i:Fin dk:Fin d⊢ ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv (Sum.inr k)) (fieldStrength A)) ε))
    (Sum.inr k, Sum.inr i) =
  (((PiLp.basisFun 2 ℝ (Fin d)).tensorProduct (PiLp.basisFun 2 ℝ (Fin d))).repr
      (((distTimeSlice 𝓕.c).symm ((Space.distSpaceDeriv k) ((magneticFieldMatrix 𝓕.c) A))) ε))
    (k, i)
    conv_rhs =>
      rw [distTimeSlice_symm_apply, Space.distSpaceDeriv_apply']d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)i:Fin dk:Fin d| (((PiLp.basisFun 2 ℝ (Fin d)).tensorProduct (PiLp.basisFun 2 ℝ (Fin d))).repr
    (-((magneticFieldMatrix 𝓕.c) A)
        ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, Space.basis k))
          ((fderivCLM ℝ (Time × Space d) ℝ) ((compCLMOfContinuousLinearEquiv ℝ (toTimeAndSpace 𝓕.c).symm) ε)))))
  (k, i)
      simp only [map_neg, Finsupp.coe_neg, Pi.neg_apply]d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)i:Fin dk:Fin d| -(((PiLp.basisFun 2 ℝ (Fin d)).tensorProduct (PiLp.basisFun 2 ℝ (Fin d))).repr
      (((magneticFieldMatrix 𝓕.c) A)
        ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, Space.basis k))
          ((fderivCLM ℝ (Time × Space d) ℝ) ((compCLMOfContinuousLinearEquiv ℝ (toTimeAndSpace 𝓕.c).symm) ε)))))
    (k, i)
      rw [magneticFieldMatrix_basis_repr_eq_fieldStrength, Space.apply_fderiv_eq_distSpaceDeriv,
        ← distTimeSlice_symm_apply]d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)i:Fin dk:Fin d| -((Vector.basis.tensorProduct Vector.basis).repr
      (-((distTimeSlice 𝓕.c).symm ((Space.distSpaceDeriv k) ((distTimeSlice 𝓕.c) (fieldStrength A)))) ε))
    (Sum.inr k, Sum.inr i)
    simp [← distTimeSlice_distDeriv_inr]All goals completed! 🐙

A.1. The gradient of the kinetic term as a tensor



set_option backward.isDefEq.respectTransparency false in
attribute [-simp] Nat.reduceAdd Nat.reduceSucc Fin.isValue in
lemma gradKineticTerm_eq_distTensorDeriv {d} {𝓕 : FreeSpace}
    (A : DistElectromagneticPotential d) (ε : 𝓢(SpaceTime d, ℝ)) (ν : Fin 1 ⊕ Fin d) :
    A.gradKineticTerm 𝓕 ε ν = η ν ν * ((Tensorial.toTensor (M := Lorentz.Vector d)).symm
    (permT id (IsReindexing.auto) {(1/ 𝓕.μ₀ : ℝ) •
    distTensorDeriv A.fieldStrength ε | κ κ ν'}ᵀ)) ν := byd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin d⊢ ((gradKineticTerm 𝓕) A) ε ν =
  η ν ν *
    Tensorial.toTensor.symm
      ((permT id ⋯) ((contrT 1 0 1 ⋯) (Tensorial.toTensor ((1 / 𝓕.μ₀) • (distTensorDeriv (fieldStrength A)) ε)))) ν
  trans η ν ν * (Lorentz.Vector.basis.repr
    ((Tensorial.toTensor (M := Lorentz.Vector d)).symm
    (permT id (IsReindexing.auto) {(1/ 𝓕.μ₀ : ℝ) • distTensorDeriv A.fieldStrength ε | κ κ ν'}ᵀ))) νd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin d⊢ ((gradKineticTerm 𝓕) A) ε ν =
  η ν ν *
    (Vector.basis.repr
        (Tensorial.toTensor.symm
          ((permT id ⋯) ((contrT 1 0 1 ⋯) (Tensorial.toTensor ((1 / 𝓕.μ₀) • (distTensorDeriv (fieldStrength A)) ε))))))
      νd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin d⊢ η ν ν *
    (Vector.basis.repr
        (Tensorial.toTensor.symm
          ((permT id ⋯) ((contrT 1 0 1 ⋯) (Tensorial.toTensor ((1 / 𝓕.μ₀) • (distTensorDeriv (fieldStrength A)) ε))))))
      ν =
  η ν ν *
    Tensorial.toTensor.symm
      ((permT id ⋯) ((contrT 1 0 1 ⋯) (Tensorial.toTensor ((1 / 𝓕.μ₀) • (distTensorDeriv (fieldStrength A)) ε)))) ν
  swapd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin d⊢ η ν ν *
    (Vector.basis.repr
        (Tensorial.toTensor.symm
          ((permT id ⋯) ((contrT 1 0 1 ⋯) (Tensorial.toTensor ((1 / 𝓕.μ₀) • (distTensorDeriv (fieldStrength A)) ε))))))
      ν =
  η ν ν *
    Tensorial.toTensor.symm
      ((permT id ⋯) ((contrT 1 0 1 ⋯) (Tensorial.toTensor ((1 / 𝓕.μ₀) • (distTensorDeriv (fieldStrength A)) ε)))) νd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin d⊢ ((gradKineticTerm 𝓕) A) ε ν =
  η ν ν *
    (Vector.basis.repr
        (Tensorial.toTensor.symm
          ((permT id ⋯) ((contrT 1 0 1 ⋯) (Tensorial.toTensor ((1 / 𝓕.μ₀) • (distTensorDeriv (fieldStrength A)) ε))))))
      ν
  ·d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin d⊢ η ν ν *
    (Vector.basis.repr
        (Tensorial.toTensor.symm
          ((permT id ⋯) ((contrT 1 0 1 ⋯) (Tensorial.toTensor ((1 / 𝓕.μ₀) • (distTensorDeriv (fieldStrength A)) ε))))))
      ν =
  η ν ν *
    Tensorial.toTensor.symm
      ((permT id ⋯) ((contrT 1 0 1 ⋯) (Tensorial.toTensor ((1 / 𝓕.μ₀) • (distTensorDeriv (fieldStrength A)) ε)))) ν rflAll goals completed! 🐙
  simp [Lorentz.Vector.basis_eq_map_tensor_basis]d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin d⊢ ((gradKineticTerm 𝓕) A) ε ν =
  η ν ν *
    (𝓕.μ₀⁻¹ *
      ((basis ![Color.up]).repr
          ((permT id ⋯) ((contrT 1 0 1 ⋯) (Tensorial.toTensor ((distTensorDeriv (fieldStrength A)) ε)))))
        (Vector.indexEquiv.symm ν))
  rw [permT_basis_repr_symm_apply,d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin d⊢ ((gradKineticTerm 𝓕) A) ε ν =
  η ν ν *
    (𝓕.μ₀⁻¹ *
      ((basis (Fin.append ![Color.down] (Fin.append ![Color.up] ![Color.up]) ∘ Fin.succSuccAbove 0 1)).repr
          ((contrT 1 0 1 ⋯) (Tensorial.toTensor ((distTensorDeriv (fieldStrength A)) ε))))
        fun i => (basisIdxCongr ⋯) (Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ i)))d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin d⊢ ((gradKineticTerm 𝓕) A) ε ν =
  η ν ν *
    (𝓕.μ₀⁻¹ *
      ∑ x,
        ((basis (Fin.append ![Color.down] (Fin.append ![Color.up] ![Color.up]))).repr
            (Tensorial.toTensor ((distTensorDeriv (fieldStrength A)) ε)))
          ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i =>
                (basisIdxCongr ⋯) (Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ i)))
              (x, x))) contrT_basis_repr_apply_eq_find:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin d⊢ ((gradKineticTerm 𝓕) A) ε ν =
  η ν ν *
    (𝓕.μ₀⁻¹ *
      ∑ x,
        ((basis (Fin.append ![Color.down] (Fin.append ![Color.up] ![Color.up]))).repr
            (Tensorial.toTensor ((distTensorDeriv (fieldStrength A)) ε)))
          ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i =>
                (basisIdxCongr ⋯) (Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ i)))
              (x, x)))d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin d⊢ ((gradKineticTerm 𝓕) A) ε ν =
  η ν ν *
    (𝓕.μ₀⁻¹ *
      ∑ x,
        ((basis (Fin.append ![Color.down] (Fin.append ![Color.up] ![Color.up]))).repr
            (Tensorial.toTensor ((distTensorDeriv (fieldStrength A)) ε)))
          ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i =>
                (basisIdxCongr ⋯) (Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ i)))
              (x, x)))]d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin d⊢ ((gradKineticTerm 𝓕) A) ε ν =
  η ν ν *
    (𝓕.μ₀⁻¹ *
      ∑ x,
        ((basis (Fin.append ![Color.down] (Fin.append ![Color.up] ![Color.up]))).repr
            (Tensorial.toTensor ((distTensorDeriv (fieldStrength A)) ε)))
          ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i =>
                (basisIdxCongr ⋯) (Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ i)))
              (x, x)))
  conv_lhs =>
    rw [gradKineticTerm_eq_fieldStrength A ε]d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin d| (∑ ν,
    (1 / 𝓕.μ₀ * η ν ν) •
      (∑ μ, ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, ν)) •
        Vector.basis ν)
  ν
    simp [Lorentz.Vector.apply_sum]d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin d| 𝓕.μ₀⁻¹ * η ν ν * ∑ μ, ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, ν)
  ring_nfd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin d⊢ 𝓕.μ₀⁻¹ * η ν ν * ∑ μ, ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, ν) =
  𝓕.μ₀⁻¹ * η ν ν *
    ∑ x,
      ((basis (Fin.append ![Color.down] (Fin.append ![Color.up] ![Color.up]))).repr
          (Tensorial.toTensor ((distTensorDeriv (fieldStrength A)) ε)))
        ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i =>
              (basisIdxCongr ⋯) (Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ i)))
            (x, x))
  congr 1e_ad:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin d⊢ ∑ μ, ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, ν) =
  ∑ x,
    ((basis (Fin.append ![Color.down] (Fin.append ![Color.up] ![Color.up]))).repr
        (Tensorial.toTensor ((distTensorDeriv (fieldStrength A)) ε)))
      ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i =>
            (basisIdxCongr ⋯) (Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ i)))
          (x, x))
  refine Finset.sum_congr rfl fun μ _ => ?_e_ad:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univ⊢ ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, ν) =
  ((basis (Fin.append ![Color.down] (Fin.append ![Color.up] ![Color.up]))).repr
      (Tensorial.toTensor ((distTensorDeriv (fieldStrength A)) ε)))
    ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i =>
          (basisIdxCongr ⋯) (Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ i)))
        (μ, μ))
  rw [distTensorDeriv_toTensor_basis_repre_ad:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univ⊢ ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, ν) =
  ((basis (Fin.append ![Color.up] ![Color.up])).repr
      (Tensorial.toTensor
        (((distDeriv
              (CoVector.indexEquiv
                (ComponentIdx.prod
                    ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i =>
                          (basisIdxCongr ⋯) (Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ i)))
                        (μ, μ))).1))
            (fieldStrength A))
          ε)))
    (ComponentIdx.prod
        ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i =>
              (basisIdxCongr ⋯) (Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ i)))
            (μ, μ))).2e_ad:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univ⊢ ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, ν) =
  ((basis (Fin.append ![Color.up] ![Color.up])).repr
      (Tensorial.toTensor
        (((distDeriv
              (CoVector.indexEquiv
                (ComponentIdx.prod
                    ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i =>
                          (basisIdxCongr ⋯) (Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ i)))
                        (μ, μ))).1))
            (fieldStrength A))
          ε)))
    (ComponentIdx.prod
        ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i =>
              (basisIdxCongr ⋯) (Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ i)))
            (μ, μ))).2]e_ad:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univ⊢ ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, ν) =
  ((basis (Fin.append ![Color.up] ![Color.up])).repr
      (Tensorial.toTensor
        (((distDeriv
              (CoVector.indexEquiv
                (ComponentIdx.prod
                    ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i =>
                          (basisIdxCongr ⋯) (Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ i)))
                        (μ, μ))).1))
            (fieldStrength A))
          ε)))
    (ComponentIdx.prod
        ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i =>
              (basisIdxCongr ⋯) (Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ i)))
            (μ, μ))).2
  trans (Tensor.basis _).repr (Tensorial.toTensor (distDeriv μ (A.fieldStrength) ε))
      (fun | 0 => μ | 1 => ν)d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univ⊢ ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, ν) =
  ((basis (Fin.append ![Color.up] ![Color.up])).repr (Tensorial.toTensor (((distDeriv μ) (fieldStrength A)) ε)))
    fun x =>
    match x with
    | 0 => μ
    | 1 => νd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univ⊢ (((basis (Fin.append ![Color.up] ![Color.up])).repr (Tensorial.toTensor (((distDeriv μ) (fieldStrength A)) ε))) fun x =>
    match x with
    | 0 => μ
    | 1 => ν) =
  ((basis (Fin.append ![Color.up] ![Color.up])).repr
      (Tensorial.toTensor
        (((distDeriv
              (CoVector.indexEquiv
                (ComponentIdx.prod
                    ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i =>
                          (basisIdxCongr ⋯) (Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ i)))
                        (μ, μ))).1))
            (fieldStrength A))
          ε)))
    (ComponentIdx.prod
        ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i =>
              (basisIdxCongr ⋯) (Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ i)))
            (μ, μ))).2
  ·d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univ⊢ ((Vector.basis.tensorProduct Vector.basis).repr (((distDeriv μ) (fieldStrength A)) ε)) (μ, ν) =
  ((basis (Fin.append ![Color.up] ![Color.up])).repr (Tensorial.toTensor (((distDeriv μ) (fieldStrength A)) ε)))
    fun x =>
    match x with
    | 0 => μ
    | 1 => ν generalize (distDeriv μ (A.fieldStrength) ε) = t at *d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univt:TensorProduct ℝ (Lorentz.Vector d) (Lorentz.Vector d)⊢ ((Vector.basis.tensorProduct Vector.basis).repr t) (μ, ν) =
  ((basis (Fin.append ![Color.up] ![Color.up])).repr (Tensorial.toTensor t)) fun x =>
    match x with
    | 0 => μ
    | 1 => ν
    rw [Tensorial.basis_toTensor_apply,d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univt:TensorProduct ℝ (Lorentz.Vector d) (Lorentz.Vector d)⊢ ((Vector.basis.tensorProduct Vector.basis).repr t) (μ, ν) =
  (((basis (Fin.append ![Color.up] ![Color.up])).map Tensorial.toTensor.symm).repr t) fun x =>
    match x with
    | 0 => μ
    | 1 => νd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univt:TensorProduct ℝ (Lorentz.Vector d) (Lorentz.Vector d)⊢ ((Vector.basis.tensorProduct Vector.basis).repr t) (μ, ν) =
  (((((basis ![Color.up]).map Tensorial.toTensor.symm).tensorProduct
              ((basis ![Color.up]).map Tensorial.toTensor.symm)).reindex
          ComponentIdx.prod.symm).repr
      t)
    fun x =>
    match x with
    | 0 => μ
    | 1 => ν Tensorial.basis_map_prodd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univt:TensorProduct ℝ (Lorentz.Vector d) (Lorentz.Vector d)⊢ ((Vector.basis.tensorProduct Vector.basis).repr t) (μ, ν) =
  (((((basis ![Color.up]).map Tensorial.toTensor.symm).tensorProduct
              ((basis ![Color.up]).map Tensorial.toTensor.symm)).reindex
          ComponentIdx.prod.symm).repr
      t)
    fun x =>
    match x with
    | 0 => μ
    | 1 => νd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univt:TensorProduct ℝ (Lorentz.Vector d) (Lorentz.Vector d)⊢ ((Vector.basis.tensorProduct Vector.basis).repr t) (μ, ν) =
  (((((basis ![Color.up]).map Tensorial.toTensor.symm).tensorProduct
              ((basis ![Color.up]).map Tensorial.toTensor.symm)).reindex
          ComponentIdx.prod.symm).repr
      t)
    fun x =>
    match x with
    | 0 => μ
    | 1 => ν]d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univt:TensorProduct ℝ (Lorentz.Vector d) (Lorentz.Vector d)⊢ ((Vector.basis.tensorProduct Vector.basis).repr t) (μ, ν) =
  (((((basis ![Color.up]).map Tensorial.toTensor.symm).tensorProduct
              ((basis ![Color.up]).map Tensorial.toTensor.symm)).reindex
          ComponentIdx.prod.symm).repr
      t)
    fun x =>
    match x with
    | 0 => μ
    | 1 => ν
    simp only [Basis.repr_reindex, Finsupp.mapDomain_equiv_apply,
      Equiv.symm_symm]d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univt:TensorProduct ℝ (Lorentz.Vector d) (Lorentz.Vector d)⊢ ((Vector.basis.tensorProduct Vector.basis).repr t) (μ, ν) =
  ((((basis ![Color.up]).map Tensorial.toTensor.symm).tensorProduct
          ((basis ![Color.up]).map Tensorial.toTensor.symm)).repr
      t)
    (ComponentIdx.prod fun x =>
      match x with
      | 0 => μ
      | 1 => ν)
    rw [Lorentz.Vector.tensor_basis_map_eq_basis_reindexd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univt:TensorProduct ℝ (Lorentz.Vector d) (Lorentz.Vector d)⊢ ((Vector.basis.tensorProduct Vector.basis).repr t) (μ, ν) =
  (((Vector.basis.reindex Vector.indexEquiv.symm).tensorProduct (Vector.basis.reindex Vector.indexEquiv.symm)).repr t)
    (ComponentIdx.prod fun x =>
      match x with
      | 0 => μ
      | 1 => ν)d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univt:TensorProduct ℝ (Lorentz.Vector d) (Lorentz.Vector d)⊢ ((Vector.basis.tensorProduct Vector.basis).repr t) (μ, ν) =
  (((Vector.basis.reindex Vector.indexEquiv.symm).tensorProduct (Vector.basis.reindex Vector.indexEquiv.symm)).repr t)
    (ComponentIdx.prod fun x =>
      match x with
      | 0 => μ
      | 1 => ν)]d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univt:TensorProduct ℝ (Lorentz.Vector d) (Lorentz.Vector d)⊢ ((Vector.basis.tensorProduct Vector.basis).repr t) (μ, ν) =
  (((Vector.basis.reindex Vector.indexEquiv.symm).tensorProduct (Vector.basis.reindex Vector.indexEquiv.symm)).repr t)
    (ComponentIdx.prod fun x =>
      match x with
      | 0 => μ
      | 1 => ν)
    have hb : (((Lorentz.Vector.basis (d := d)).reindex
        Lorentz.Vector.indexEquiv.symm).tensorProduct
        (Lorentz.Vector.basis.reindex Lorentz.Vector.indexEquiv.symm)) =
        ((Lorentz.Vector.basis (d := d)).tensorProduct (Lorentz.Vector.basis (d := d))).reindex
        (Lorentz.Vector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm) := byd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin d⊢ ((gradKineticTerm 𝓕) A) ε ν =
  η ν ν *
    Tensorial.toTensor.symm
      ((permT id ⋯) ((contrT 1 0 1 ⋯) (Tensorial.toTensor ((1 / 𝓕.μ₀) • (distTensorDeriv (fieldStrength A)) ε)))) νd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univt:TensorProduct ℝ (Lorentz.Vector d) (Lorentz.Vector d)hb:(Vector.basis.reindex Vector.indexEquiv.symm).tensorProduct (Vector.basis.reindex Vector.indexEquiv.symm) =
  (Vector.basis.tensorProduct Vector.basis).reindex (Vector.indexEquiv.symm.prodCongr Vector.indexEquiv.symm)⊢ ((Vector.basis.tensorProduct Vector.basis).repr t) (μ, ν) =
  (((Vector.basis.reindex Vector.indexEquiv.symm).tensorProduct (Vector.basis.reindex Vector.indexEquiv.symm)).repr t)
    (ComponentIdx.prod fun x =>
      match x with
      | 0 => μ
      | 1 => ν)
      ext ⟨i, j⟩d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univt:TensorProduct ℝ (Lorentz.Vector d) (Lorentz.Vector d)i:ComponentIdx ![Color.up]j:ComponentIdx ![Color.up]⊢ ((Vector.basis.reindex Vector.indexEquiv.symm).tensorProduct (Vector.basis.reindex Vector.indexEquiv.symm)) (i, j) =
  ((Vector.basis.tensorProduct Vector.basis).reindex (Vector.indexEquiv.symm.prodCongr Vector.indexEquiv.symm)) (i, j)d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univt:TensorProduct ℝ (Lorentz.Vector d) (Lorentz.Vector d)hb:(Vector.basis.reindex Vector.indexEquiv.symm).tensorProduct (Vector.basis.reindex Vector.indexEquiv.symm) =
  (Vector.basis.tensorProduct Vector.basis).reindex (Vector.indexEquiv.symm.prodCongr Vector.indexEquiv.symm)⊢ ((Vector.basis.tensorProduct Vector.basis).repr t) (μ, ν) =
  (((Vector.basis.reindex Vector.indexEquiv.symm).tensorProduct (Vector.basis.reindex Vector.indexEquiv.symm)).repr t)
    (ComponentIdx.prod fun x =>
      match x with
      | 0 => μ
      | 1 => ν)
      simpd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univt:TensorProduct ℝ (Lorentz.Vector d) (Lorentz.Vector d)hb:(Vector.basis.reindex Vector.indexEquiv.symm).tensorProduct (Vector.basis.reindex Vector.indexEquiv.symm) =
  (Vector.basis.tensorProduct Vector.basis).reindex (Vector.indexEquiv.symm.prodCongr Vector.indexEquiv.symm)⊢ ((Vector.basis.tensorProduct Vector.basis).repr t) (μ, ν) =
  (((Vector.basis.reindex Vector.indexEquiv.symm).tensorProduct (Vector.basis.reindex Vector.indexEquiv.symm)).repr t)
    (ComponentIdx.prod fun x =>
      match x with
      | 0 => μ
      | 1 => ν)d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univt:TensorProduct ℝ (Lorentz.Vector d) (Lorentz.Vector d)hb:(Vector.basis.reindex Vector.indexEquiv.symm).tensorProduct (Vector.basis.reindex Vector.indexEquiv.symm) =
  (Vector.basis.tensorProduct Vector.basis).reindex (Vector.indexEquiv.symm.prodCongr Vector.indexEquiv.symm)⊢ ((Vector.basis.tensorProduct Vector.basis).repr t) (μ, ν) =
  (((Vector.basis.reindex Vector.indexEquiv.symm).tensorProduct (Vector.basis.reindex Vector.indexEquiv.symm)).repr t)
    (ComponentIdx.prod fun x =>
      match x with
      | 0 => μ
      | 1 => ν)
    rw [hb,d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univt:TensorProduct ℝ (Lorentz.Vector d) (Lorentz.Vector d)hb:(Vector.basis.reindex Vector.indexEquiv.symm).tensorProduct (Vector.basis.reindex Vector.indexEquiv.symm) =
  (Vector.basis.tensorProduct Vector.basis).reindex (Vector.indexEquiv.symm.prodCongr Vector.indexEquiv.symm)⊢ ((Vector.basis.tensorProduct Vector.basis).repr t) (μ, ν) =
  (((Vector.basis.tensorProduct Vector.basis).reindex (Vector.indexEquiv.symm.prodCongr Vector.indexEquiv.symm)).repr t)
    (ComponentIdx.prod fun x =>
      match x with
      | 0 => μ
      | 1 => ν)d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univt:TensorProduct ℝ (Lorentz.Vector d) (Lorentz.Vector d)hb:(Vector.basis.reindex Vector.indexEquiv.symm).tensorProduct (Vector.basis.reindex Vector.indexEquiv.symm) =
  (Vector.basis.tensorProduct Vector.basis).reindex (Vector.indexEquiv.symm.prodCongr Vector.indexEquiv.symm)⊢ ((Vector.basis.tensorProduct Vector.basis).repr t) (μ, ν) =
  ((Vector.basis.tensorProduct Vector.basis).repr t)
    ((Vector.indexEquiv.symm.prodCongr Vector.indexEquiv.symm).symm
      (ComponentIdx.prod fun x =>
        match x with
        | 0 => μ
        | 1 => ν)) Module.Basis.repr_reindex_applyd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univt:TensorProduct ℝ (Lorentz.Vector d) (Lorentz.Vector d)hb:(Vector.basis.reindex Vector.indexEquiv.symm).tensorProduct (Vector.basis.reindex Vector.indexEquiv.symm) =
  (Vector.basis.tensorProduct Vector.basis).reindex (Vector.indexEquiv.symm.prodCongr Vector.indexEquiv.symm)⊢ ((Vector.basis.tensorProduct Vector.basis).repr t) (μ, ν) =
  ((Vector.basis.tensorProduct Vector.basis).repr t)
    ((Vector.indexEquiv.symm.prodCongr Vector.indexEquiv.symm).symm
      (ComponentIdx.prod fun x =>
        match x with
        | 0 => μ
        | 1 => ν))d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univt:TensorProduct ℝ (Lorentz.Vector d) (Lorentz.Vector d)hb:(Vector.basis.reindex Vector.indexEquiv.symm).tensorProduct (Vector.basis.reindex Vector.indexEquiv.symm) =
  (Vector.basis.tensorProduct Vector.basis).reindex (Vector.indexEquiv.symm.prodCongr Vector.indexEquiv.symm)⊢ ((Vector.basis.tensorProduct Vector.basis).repr t) (μ, ν) =
  ((Vector.basis.tensorProduct Vector.basis).repr t)
    ((Vector.indexEquiv.symm.prodCongr Vector.indexEquiv.symm).symm
      (ComponentIdx.prod fun x =>
        match x with
        | 0 => μ
        | 1 => ν))]d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univt:TensorProduct ℝ (Lorentz.Vector d) (Lorentz.Vector d)hb:(Vector.basis.reindex Vector.indexEquiv.symm).tensorProduct (Vector.basis.reindex Vector.indexEquiv.symm) =
  (Vector.basis.tensorProduct Vector.basis).reindex (Vector.indexEquiv.symm.prodCongr Vector.indexEquiv.symm)⊢ ((Vector.basis.tensorProduct Vector.basis).repr t) (μ, ν) =
  ((Vector.basis.tensorProduct Vector.basis).repr t)
    ((Vector.indexEquiv.symm.prodCongr Vector.indexEquiv.symm).symm
      (ComponentIdx.prod fun x =>
        match x with
        | 0 => μ
        | 1 => ν))
    rflAll goals completed! 🐙
  apply congrh₁d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univ⊢ ⇑((basis (Fin.append ![Color.up] ![Color.up])).repr (Tensorial.toTensor (((distDeriv μ) (fieldStrength A)) ε))) =
  ⇑((basis (Fin.append ![Color.up] ![Color.up])).repr
      (Tensorial.toTensor
        (((distDeriv
              (CoVector.indexEquiv
                (ComponentIdx.prod
                    ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i =>
                          (basisIdxCongr ⋯) (Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ i)))
                        (μ, μ))).1))
            (fieldStrength A))
          ε)))h₂d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univ⊢ (fun x =>
    match x with
    | 0 => μ
    | 1 => ν) =
  (ComponentIdx.prod
      ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i =>
            (basisIdxCongr ⋯) (Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ i)))
          (μ, μ))).2
  ·h₁d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univ⊢ ⇑((basis (Fin.append ![Color.up] ![Color.up])).repr (Tensorial.toTensor (((distDeriv μ) (fieldStrength A)) ε))) =
  ⇑((basis (Fin.append ![Color.up] ![Color.up])).repr
      (Tensorial.toTensor
        (((distDeriv
              (CoVector.indexEquiv
                (ComponentIdx.prod
                    ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i =>
                          (basisIdxCongr ⋯) (Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ i)))
                        (μ, μ))).1))
            (fieldStrength A))
          ε))) simph₁d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univ⊢ ((distDeriv μ) (fieldStrength A)) ε =
  ((distDeriv
        (CoVector.indexEquiv
          (ComponentIdx.prod
              ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i =>
                    (basisIdxCongr ⋯) (Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ i)))
                  (μ, μ))).1))
      (fieldStrength A))
    ε
    rflAll goals completed! 🐙
  funext xh₂d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univx:Fin (Nat.succ 0 + Nat.succ 0)⊢ (match x with
  | 0 => μ
  | 1 => ν) =
  (ComponentIdx.prod
        ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i =>
              (basisIdxCongr ⋯) (Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ i)))
            (μ, μ))).2
    x
  fin_cases xh₂.«0»d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univ⊢ (match (fun i => i) ⟨0, ⋯⟩ with
  | 0 => μ
  | 1 => ν) =
  (ComponentIdx.prod
        ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i =>
              (basisIdxCongr ⋯) (Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ i)))
            (μ, μ))).2
    ((fun i => i) ⟨0, ⋯⟩)h₂.«1»d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univ⊢ (match (fun i => i) ⟨1, ⋯⟩ with
  | 0 => μ
  | 1 => ν) =
  (ComponentIdx.prod
        ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i =>
              (basisIdxCongr ⋯) (Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ i)))
            (μ, μ))).2
    ((fun i => i) ⟨1, ⋯⟩) <;>h₂.«0»d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univ⊢ (match (fun i => i) ⟨0, ⋯⟩ with
  | 0 => μ
  | 1 => ν) =
  (ComponentIdx.prod
        ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i =>
              (basisIdxCongr ⋯) (Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ i)))
            (μ, μ))).2
    ((fun i => i) ⟨0, ⋯⟩)h₂.«1»d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univ⊢ (match (fun i => i) ⟨1, ⋯⟩ with
  | 0 => μ
  | 1 => ν) =
  (ComponentIdx.prod
        ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i =>
              (basisIdxCongr ⋯) (Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ i)))
            (μ, μ))).2
    ((fun i => i) ⟨1, ⋯⟩)
    simp [Function.comp_apply, ComponentIdx.prod, ComponentIdx.DropPairSection.ofFinEquiv,
      ComponentIdx.DropPairSection.ofFin]h₂.«1»d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univ⊢ ν =
  if h : Fin.natAdd (Nat.succ 0) 1 = 0 then μ
  else
    if h : Fin.natAdd (Nat.succ 0) 1 = 1 then μ
    else Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ (Fin.predPredAbove 0 1 ⋯ (Fin.natAdd (Nat.succ 0) 1) ⋯))
  ·h₂.«0»d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univ⊢ ∀ (h : ¬Fin.natAdd (Nat.succ 0) 0 = 0) (h_1 : ¬Fin.natAdd (Nat.succ 0) 0 = 1),
  μ = Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ (Fin.predPredAbove 0 1 ⋯ (Fin.natAdd (Nat.succ 0) 0) ⋯)) intro _ hh₂.«0»d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univh✝:¬Fin.natAdd (Nat.succ 0) 0 = 0h:¬Fin.natAdd (Nat.succ 0) 0 = 1⊢ μ = Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ (Fin.predPredAbove 0 1 ⋯ (Fin.natAdd (Nat.succ 0) 0) ⋯))
    exact absurd (byd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univh✝:¬Fin.natAdd (Nat.succ 0) 0 = 0h:¬Fin.natAdd (Nat.succ 0) 0 = 1⊢ Fin.natAdd (Nat.succ 0) 0 = 1 decideAll goals completed! 🐙) h
  ·h₂.«1»d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univ⊢ ν =
  if h : Fin.natAdd (Nat.succ 0) 1 = 0 then μ
  else
    if h : Fin.natAdd (Nat.succ 0) 1 = 1 then μ
    else Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ (Fin.predPredAbove 0 1 ⋯ (Fin.natAdd (Nat.succ 0) 1) ⋯)) split_ifs with h1 h2posd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univh1:Fin.natAdd (Nat.succ 0) 1 = 0⊢ ν = μposd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univh1:¬Fin.natAdd (Nat.succ 0) 1 = 0h2:Fin.natAdd (Nat.succ 0) 1 = 1⊢ ν = μnegd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univh1:¬Fin.natAdd (Nat.succ 0) 1 = 0h2:¬Fin.natAdd (Nat.succ 0) 1 = 1⊢ ν = Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ (Fin.predPredAbove 0 1 ⋯ (Fin.natAdd (Nat.succ 0) 1) ⋯))
    ·posd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univh1:Fin.natAdd (Nat.succ 0) 1 = 0⊢ ν = μ exact absurd h1 (byd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univh1:Fin.natAdd (Nat.succ 0) 1 = 0⊢ ¬Fin.natAdd (Nat.succ 0) 1 = 0 decideAll goals completed! 🐙)
    ·posd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univh1:¬Fin.natAdd (Nat.succ 0) 1 = 0h2:Fin.natAdd (Nat.succ 0) 1 = 1⊢ ν = μ exact absurd h2 (byd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univh1:¬Fin.natAdd (Nat.succ 0) 1 = 0h2:Fin.natAdd (Nat.succ 0) 1 = 1⊢ ¬Fin.natAdd (Nat.succ 0) 1 = 1 decideAll goals completed! 🐙)
    ·negd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univh1:¬Fin.natAdd (Nat.succ 0) 1 = 0h2:¬Fin.natAdd (Nat.succ 0) 1 = 1⊢ ν = Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ (Fin.predPredAbove 0 1 ⋯ (Fin.natAdd (Nat.succ 0) 1) ⋯)) rflAll goals completed! 🐙