Physlib.Electromagnetism.Current.InfiniteWire

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.Dynamics.IsExtrema
public import Physlib.SpaceAndTime.Space.Norm.Basic
public import Physlib.SpaceAndTime.Space.ConstantSliceDist

The magnetic field around a infinite wire

i. Overview

In this module we verify the electromagnetic properties of an infinite wire carrying a steady current along the x-axis.

ii. Key results

wireCurrentDensity : The current density associated with an infinite wire carrying a current I along the x-axis.

infiniteWire : The electromagnetic potential associated with an infinite wire carrying a current I along the x-axis.

infiniteWire_isExterma : The electromagnetic potential of an infinite wire carrying a current I along the x-axis satisfies Maxwell's equations.

iii. Table of contents

A. The current density

B. The electromagnetic potential

B.1. The scalar potential

B.2. The vector potential

C. The electric field

D. Maxwell's equations

iv. References

@[expose] public section

A. The current density

The 4-current density of an infinite wire carrying a current I along the x-axis is given by

$$J(t, x, y, z) = (0, I δ((y, z)), 0, 0).$$

              @[simp]
lemma wireCurrentDensity_chargeDesnity (c : SpeedOfLight) (I : ℝ) :
    (wireCurrentDensity c I).chargeDensity c = 0 := byc:SpeedOfLightI:ℝ⊢ (DistLorentzCurrentDensity.chargeDensity c) ((wireCurrentDensity c) I) = 0
  ext ηc:SpeedOfLightI:ℝη:𝓢(Time × Space, ℝ)⊢ ((DistLorentzCurrentDensity.chargeDensity c) ((wireCurrentDensity c) I)) η = 0 η
  simp [DistLorentzCurrentDensity.chargeDensity, wireCurrentDensity, constantTime_apply,
  constantSliceDist_apply]All goals completed! 🐙lemma wireCurrentDensity_currentDensity_fst (c : SpeedOfLight) (I : ℝ)
    (η : 𝓢(Time × Space 3, ℝ)) :
    (wireCurrentDensity c I).currentDensity c η 0 =
    (constantTime <|
    constantSliceDist 0 <|
    I • diracDelta ℝ 0) η := byc:SpeedOfLightI:ℝη:𝓢(Time × Space, ℝ)⊢ (((DistLorentzCurrentDensity.currentDensity c) ((wireCurrentDensity c) I)) η).ofLp 0 =
  (constantTime ((constantSliceDist 0) (I • diracDelta ℝ 0))) η
  simp [wireCurrentDensity, DistLorentzCurrentDensity.currentDensity,
    constantTime_apply, constantSliceDist_apply, diracDelta'_apply]All goals completed! 🐙@[simp]
lemma wireCurrentDensity_currentDensity_snd (c : SpeedOfLight) (I : ℝ)
    (ε : 𝓢(Time × Space 3, ℝ)) :
    (wireCurrentDensity c I).currentDensity c ε 1 = 0 := byc:SpeedOfLightI:ℝε:𝓢(Time × Space, ℝ)⊢ (((DistLorentzCurrentDensity.currentDensity c) ((wireCurrentDensity c) I)) ε).ofLp 1 = 0
  simp [wireCurrentDensity, DistLorentzCurrentDensity.currentDensity,
    constantTime_apply, constantSliceDist_apply]All goals completed! 🐙@[simp]
lemma wireCurrentDensity_currentDensity_thrd (c : SpeedOfLight) (I : ℝ)
    (ε : 𝓢(Time × Space 3, ℝ)) :
    (wireCurrentDensity c I).currentDensity c ε 2 = 0 := byc:SpeedOfLightI:ℝε:𝓢(Time × Space, ℝ)⊢ (((DistLorentzCurrentDensity.currentDensity c) ((wireCurrentDensity c) I)) ε).ofLp 2 = 0
  simp [wireCurrentDensity, DistLorentzCurrentDensity.currentDensity,
    constantTime_apply, constantSliceDist_apply, diracDelta'_apply]All goals completed! 🐙

B. The electromagnetic potential

The electromagnetic potential of an infinite wire carrying a current I along the x-axis is given by

$$A(t, x, y, z) = \left(0, -\frac{μ_0 I}{2\pi} \log (\sqrt{y^2 + z^2}), 0, 0\right).$$

B.1. The scalar potential

THe scalar potential of an infinite wire carrying a current I along the x-axis is zero:

$$V(t, x, y, z) = 0.$$

@[simp]
lemma infiniteWire_scalarPotential (𝓕 : FreeSpace) (I : ℝ) :
    (infiniteWire 𝓕 I).scalarPotential 𝓕.c = 0 := by𝓕:FreeSpaceI:ℝ⊢ (scalarPotential 𝓕.c) (infiniteWire 𝓕 I) = 0
  ext η𝓕:FreeSpaceI:ℝη:𝓢(Time × Space, ℝ)⊢ ((scalarPotential 𝓕.c) (infiniteWire 𝓕 I)) η = 0 η
  simp [scalarPotential, Lorentz.Vector.temporalCLM,
  infiniteWire, constantTime_apply, constantSliceDist_apply, distOfFunction_vector_eval]All goals completed! 🐙

B.2. The vector potential

The vector potential of an infinite wire carrying a current I along the x-axis is given by $$\vec A(t, x, y, z) = \left(-\frac{μ_0 I}{2\pi} \log (\sqrt{y^2 + z^2}), 0, 0\right).$$

The time derivative $\partial_t \vec A$ is zero, as expected for a steady current, and the spatial derivative $\partial_x \vec A$ is also zero, as expected for a system with translational symmetry along the x-axis.

              lemma infiniteWire_vectorPotential (𝓕 : FreeSpace) (I : ℝ) :
    (infiniteWire 𝓕 I).vectorPotential 𝓕.c =
    (constantTime <|
    constantSliceDist 0
    ((- I * 𝓕.μ₀ / (2 * Real.pi)) • distOfFunction (fun (x : Space 2) =>
      Real.log ‖x‖ • EuclideanSpace.single 0 (1 : ℝ))
    (by𝓕:FreeSpaceI:ℝ⊢ IsDistBounded fun x => Real.log ‖x‖ • EuclideanSpace.single 0 1 apply (IsDistBounded.log_norm (by𝓕:FreeSpaceI:ℝ⊢ 2 ≤ 2 norm_numAll goals completed! 🐙)).smul_const))) := by𝓕:FreeSpaceI:ℝ⊢ (vectorPotential 𝓕.c) (infiniteWire 𝓕 I) =
  constantTime
    ((constantSliceDist 0)
      ((-I * 𝓕.μ₀ / (2 * Real.pi)) • distOfFunction (fun x => Real.log ‖x‖ • EuclideanSpace.single 0 1) ⋯))
  ext η i𝓕:FreeSpaceI:ℝη:𝓢(Time × Space, ℝ)i:Fin 3⊢ (((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)) η).ofLp i =
  ((constantTime
          ((constantSliceDist 0)
            ((-I * 𝓕.μ₀ / (2 * Real.pi)) • distOfFunction (fun x => Real.log ‖x‖ • EuclideanSpace.single 0 1) ⋯)))
        η).ofLp
    i
  simp [vectorPotential, infiniteWire, constantTime_apply,
  constantSliceDist_apply, Lorentz.Vector.spatialCLM, distOfFunction_vector_eval,
  distOfFunction_eculid_eval, eq_comm]All goals completed! 🐙lemma infiniteWire_vectorPotential_fst (𝓕 : FreeSpace) (I : ℝ)(η : 𝓢(Time × Space 3, ℝ)) :
    (infiniteWire 𝓕 I).vectorPotential 𝓕.c η 0 =
    (constantTime <|
    constantSliceDist 0 <|
    (- I * 𝓕.μ₀ / (2 * Real.pi)) • distOfFunction (fun (x : Space 2) => Real.log ‖x‖)
    (IsDistBounded.log_norm)) η := by𝓕:FreeSpaceI:ℝη:𝓢(Time × Space, ℝ)⊢ (((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)) η).ofLp 0 =
  (constantTime ((constantSliceDist 0) ((-I * 𝓕.μ₀ / (2 * Real.pi)) • distOfFunction (fun x => Real.log ‖x‖) ⋯))) η
  simp [infiniteWire_vectorPotential 𝓕 I, constantTime_apply,
    constantSliceDist_apply, distOfFunction_eculid_eval]All goals completed! 🐙@[simp]
lemma infiniteWire_vectorPotential_snd (𝓕 : FreeSpace) (I : ℝ) :
    (infiniteWire 𝓕 I).vectorPotential 𝓕.c η 1 = 0 := byη:𝓢(Time × Space, ℝ)𝓕:FreeSpaceI:ℝ⊢ (((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)) η).ofLp 1 = 0
  simp [infiniteWire_vectorPotential 𝓕 I, constantTime_apply,
    constantSliceDist_apply, distOfFunction_eculid_eval]All goals completed! 🐙@[simp]
lemma infiniteWire_vectorPotential_thrd (𝓕 : FreeSpace) (I : ℝ) :
    (infiniteWire 𝓕 I).vectorPotential 𝓕.c η 2 = 0 := byη:𝓢(Time × Space, ℝ)𝓕:FreeSpaceI:ℝ⊢ (((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)) η).ofLp 2 = 0
  simp [infiniteWire_vectorPotential 𝓕 I, constantTime_apply,
    constantSliceDist_apply, distOfFunction_eculid_eval]All goals completed! 🐙

@[simp]
lemma infiniteWire_vectorPotential_distTimeDeriv (𝓕 : FreeSpace) (I : ℝ) :
    distTimeDeriv ((infiniteWire 𝓕 I).vectorPotential 𝓕.c) = 0 := by𝓕:FreeSpaceI:ℝ⊢ distTimeDeriv ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)) = 0
  ext1 η𝓕:FreeSpaceI:ℝη:𝓢(Time × Space, ℝ)⊢ (distTimeDeriv ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I))) η = 0 η
  ext i𝓕:FreeSpaceI:ℝη:𝓢(Time × Space, ℝ)i:Fin 3⊢ ((distTimeDeriv ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I))) η).ofLp i = (0 η).ofLp i
  rw [infiniteWire_vectorPotential _ I,𝓕:FreeSpaceI:ℝη:𝓢(Time × Space, ℝ)i:Fin 3⊢ ((distTimeDeriv
          (constantTime
            ((constantSliceDist 0)
              ((-I * 𝓕.μ₀ / (2 * Real.pi)) • distOfFunction (fun x => Real.log ‖x‖ • EuclideanSpace.single 0 1) ⋯))))
        η).ofLp
    i =
  (0 η).ofLp iAll goals completed! 🐙 constantTime_distTimeDeriv𝓕:FreeSpaceI:ℝη:𝓢(Time × Space, ℝ)i:Fin 3⊢ (0 η).ofLp i = (0 η).ofLp iAll goals completed! 🐙]All goals completed! 🐙@[simp]
lemma infiniteWire_vectorPotential_distSpaceDeriv_0 (𝓕 : FreeSpace) (I : ℝ) :
    distSpaceDeriv 0 ((infiniteWire 𝓕 I).vectorPotential 𝓕.c) = 0 := by𝓕:FreeSpaceI:ℝ⊢ (distSpaceDeriv 0) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)) = 0
  ext1 η𝓕:FreeSpaceI:ℝη:𝓢(Time × Space, ℝ)⊢ ((distSpaceDeriv 0) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I))) η = 0 η
  simp [infiniteWire_vectorPotential _ I, constantTime_distSpaceDeriv,
    distDeriv_constantSliceDist_same]All goals completed! 🐙

C. The electric field

The electric field of an infinite wire carrying a current I along the x-axis is zero: $$\vec E(t, x, y, z) = 0.$$

@[simp]
lemma infiniteWire_electricField (𝓕 : FreeSpace) (I : ℝ) :
    (infiniteWire 𝓕 I).electricField 𝓕.c = 0 := by𝓕:FreeSpaceI:ℝ⊢ (electricField 𝓕.c) (infiniteWire 𝓕 I) = 0
  ext1 η𝓕:FreeSpaceI:ℝη:𝓢(Time × Space, ℝ)⊢ ((electricField 𝓕.c) (infiniteWire 𝓕 I)) η = 0 η
  ext i𝓕:FreeSpaceI:ℝη:𝓢(Time × Space, ℝ)i:Fin 3⊢ (((electricField 𝓕.c) (infiniteWire 𝓕 I)) η).ofLp i = (0 η).ofLp i
  simp [electricField]All goals completed! 🐙

D. Maxwell's equations



lemma infiniteWire_isExterma {𝓕 : FreeSpace} {I : ℝ} :
    IsExtrema 𝓕 (infiniteWire 𝓕 I) (wireCurrentDensity 𝓕.c I) := by𝓕:FreeSpaceI:ℝ⊢ IsExtrema 𝓕 (infiniteWire 𝓕 I) ((wireCurrentDensity 𝓕.c) I)
  simp only [isExtrema_iff_vectorPotential, infiniteWire_electricField, map_zero,
    _root_.zero_apply, one_div, wireCurrentDensity_chargeDesnity, mul_zero,
    implies_true, PiLp.zero_apply, zero_sub, true_and]𝓕:FreeSpaceI:ℝ⊢ ∀ (ε : 𝓢(Time × Space, ℝ)) (i : Fin 3),
  -∑ x,
          -((((distSpaceDeriv x) ((distSpaceDeriv x) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp i -
              (((distSpaceDeriv x) ((distSpaceDeriv i) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp x) +
      𝓕.μ₀ * (((DistLorentzCurrentDensity.currentDensity 𝓕.c) ((wireCurrentDensity 𝓕.c) I)) ε).ofLp i =
    0
  intro ε i𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)i:Fin 3⊢ -∑ x,
        -((((distSpaceDeriv x) ((distSpaceDeriv x) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp i -
            (((distSpaceDeriv x) ((distSpaceDeriv i) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp x) +
    𝓕.μ₀ * (((DistLorentzCurrentDensity.currentDensity 𝓕.c) ((wireCurrentDensity 𝓕.c) I)) ε).ofLp i =
  0
  rw [neg_add_eq_zero𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)i:Fin 3⊢ ∑ x,
    -((((distSpaceDeriv x) ((distSpaceDeriv x) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp i -
        (((distSpaceDeriv x) ((distSpaceDeriv i) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp x) =
  𝓕.μ₀ * (((DistLorentzCurrentDensity.currentDensity 𝓕.c) ((wireCurrentDensity 𝓕.c) I)) ε).ofLp i𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)i:Fin 3⊢ ∑ x,
    -((((distSpaceDeriv x) ((distSpaceDeriv x) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp i -
        (((distSpaceDeriv x) ((distSpaceDeriv i) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp x) =
  𝓕.μ₀ * (((DistLorentzCurrentDensity.currentDensity 𝓕.c) ((wireCurrentDensity 𝓕.c) I)) ε).ofLp i]𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)i:Fin 3⊢ ∑ x,
    -((((distSpaceDeriv x) ((distSpaceDeriv x) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp i -
        (((distSpaceDeriv x) ((distSpaceDeriv i) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp x) =
  𝓕.μ₀ * (((DistLorentzCurrentDensity.currentDensity 𝓕.c) ((wireCurrentDensity 𝓕.c) I)) ε).ofLp i
  fin_cases i«0»𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ ∑ x,
    -((((distSpaceDeriv x) ((distSpaceDeriv x) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp
          ((fun i => i) ⟨0, ⋯⟩) -
        (((distSpaceDeriv x) ((distSpaceDeriv ((fun i => i) ⟨0, ⋯⟩)) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I))))
              ε).ofLp
          x) =
  𝓕.μ₀ * (((DistLorentzCurrentDensity.currentDensity 𝓕.c) ((wireCurrentDensity 𝓕.c) I)) ε).ofLp ((fun i => i) ⟨0, ⋯⟩)«1»𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ ∑ x,
    -((((distSpaceDeriv x) ((distSpaceDeriv x) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp
          ((fun i => i) ⟨1, ⋯⟩) -
        (((distSpaceDeriv x) ((distSpaceDeriv ((fun i => i) ⟨1, ⋯⟩)) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I))))
              ε).ofLp
          x) =
  𝓕.μ₀ * (((DistLorentzCurrentDensity.currentDensity 𝓕.c) ((wireCurrentDensity 𝓕.c) I)) ε).ofLp ((fun i => i) ⟨1, ⋯⟩)«2»𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ ∑ x,
    -((((distSpaceDeriv x) ((distSpaceDeriv x) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp
          ((fun i => i) ⟨2, ⋯⟩) -
        (((distSpaceDeriv x) ((distSpaceDeriv ((fun i => i) ⟨2, ⋯⟩)) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I))))
              ε).ofLp
          x) =
  𝓕.μ₀ * (((DistLorentzCurrentDensity.currentDensity 𝓕.c) ((wireCurrentDensity 𝓕.c) I)) ε).ofLp ((fun i => i) ⟨2, ⋯⟩)
  ·«0»𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ ∑ x,
    -((((distSpaceDeriv x) ((distSpaceDeriv x) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp
          ((fun i => i) ⟨0, ⋯⟩) -
        (((distSpaceDeriv x) ((distSpaceDeriv ((fun i => i) ⟨0, ⋯⟩)) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I))))
              ε).ofLp
          x) =
  𝓕.μ₀ * (((DistLorentzCurrentDensity.currentDensity 𝓕.c) ((wireCurrentDensity 𝓕.c) I)) ε).ofLp ((fun i => i) ⟨0, ⋯⟩) simp [Fin.sum_univ_three]«0»𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ -(((distSpaceDeriv 2) ((distSpaceDeriv 2) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp 0 +
    -(((distSpaceDeriv 1) ((distSpaceDeriv 1) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp 0 =
  𝓕.μ₀ * (((DistLorentzCurrentDensity.currentDensity 𝓕.c) ((wireCurrentDensity 𝓕.c) I)) ε).ofLp 0
    simp [distSpaceDeriv_apply', infiniteWire_vectorPotential_fst]«0»𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ -(-(I * 𝓕.μ₀) / (2 * Real.pi) *
        (constantTime ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯)))
          ((SchwartzMap.evalCLM ℝ (Time × Space) ℝ (0, basis 2))
            ((fderivCLM ℝ (Time × Space) ℝ)
              ((SchwartzMap.evalCLM ℝ (Time × Space) ℝ (0, basis 2)) ((fderivCLM ℝ (Time × Space) ℝ) ε))))) +
    -(-(I * 𝓕.μ₀) / (2 * Real.pi) *
        (constantTime ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯)))
          ((SchwartzMap.evalCLM ℝ (Time × Space) ℝ (0, basis 1))
            ((fderivCLM ℝ (Time × Space) ℝ)
              ((SchwartzMap.evalCLM ℝ (Time × Space) ℝ (0, basis 1)) ((fderivCLM ℝ (Time × Space) ℝ) ε))))) =
  𝓕.μ₀ * (((DistLorentzCurrentDensity.currentDensity 𝓕.c) ((wireCurrentDensity 𝓕.c) I)) ε).ofLp 0
    simp [apply_fderiv_eq_distSpaceDeriv, wireCurrentDensity_currentDensity_fst]«0»𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ -(-(I * 𝓕.μ₀) / (2 * Real.pi) *
        ((distSpaceDeriv 2)
            ((distSpaceDeriv 2) (constantTime ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯)))))
          ε) +
    -(-(I * 𝓕.μ₀) / (2 * Real.pi) *
        ((distSpaceDeriv 1)
            ((distSpaceDeriv 1) (constantTime ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯)))))
          ε) =
  𝓕.μ₀ * (I * (constantTime ((constantSliceDist 0) (diracDelta ℝ 0))) ε)
    field_simp«0»𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ I *
    (((distSpaceDeriv 2)
          ((distSpaceDeriv 2) (constantTime ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯)))))
        ε +
      ((distSpaceDeriv 1)
          ((distSpaceDeriv 1) (constantTime ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯)))))
        ε) =
  I * 2 * Real.pi * (constantTime ((constantSliceDist 0) (diracDelta ℝ 0))) ε
    simp only [constantTime_distSpaceDeriv, mul_assoc]«0»𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ I *
    ((constantTime ((distDeriv 2) ((distDeriv 2) ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯)))))
        ε +
      (constantTime ((distDeriv 1) ((distDeriv 1) ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯)))))
        ε) =
  I * (2 * (Real.pi * (constantTime ((constantSliceDist 0) (diracDelta ℝ 0))) ε))
    congr«0».e_a𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (constantTime ((distDeriv 2) ((distDeriv 2) ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯))))) ε +
    (constantTime ((distDeriv 1) ((distDeriv 1) ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯)))))
      ε =
  2 * (Real.pi * (constantTime ((constantSliceDist 0) (diracDelta ℝ 0))) ε)
    rw [← _root_.add_apply,«0».e_a𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (constantTime ((distDeriv 2) ((distDeriv 2) ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯)))) +
      constantTime ((distDeriv 1) ((distDeriv 1) ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯)))))
    ε =
  2 * (Real.pi * (constantTime ((constantSliceDist 0) (diracDelta ℝ 0))) ε)«0».e_a𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (constantTime
      ((distDeriv 2) ((distDeriv 2) ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) +
        (distDeriv 1) ((distDeriv 1) ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯)))))
    ε =
  2 * (Real.pi * (constantTime ((constantSliceDist 0) (diracDelta ℝ 0))) ε) ← map_add constantTime«0».e_a𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (constantTime
      ((distDeriv 2) ((distDeriv 2) ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) +
        (distDeriv 1) ((distDeriv 1) ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯)))))
    ε =
  2 * (Real.pi * (constantTime ((constantSliceDist 0) (diracDelta ℝ 0))) ε)«0».e_a𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (constantTime
      ((distDeriv 2) ((distDeriv 2) ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) +
        (distDeriv 1) ((distDeriv 1) ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯)))))
    ε =
  2 * (Real.pi * (constantTime ((constantSliceDist 0) (diracDelta ℝ 0))) ε)]«0».e_a𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (constantTime
      ((distDeriv 2) ((distDeriv 2) ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) +
        (distDeriv 1) ((distDeriv 1) ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯)))))
    ε =
  2 * (Real.pi * (constantTime ((constantSliceDist 0) (diracDelta ℝ 0))) ε)
    trans (constantTime ((constantSliceDist 0) ((2 * Real.pi) • diracDelta ℝ 0))) ε𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (constantTime
      ((distDeriv 2) ((distDeriv 2) ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) +
        (distDeriv 1) ((distDeriv 1) ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯)))))
    ε =
  (constantTime ((constantSliceDist 0) ((2 * Real.pi) • diracDelta ℝ 0))) ε𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (constantTime ((constantSliceDist 0) ((2 * Real.pi) • diracDelta ℝ 0))) ε =
  2 * (Real.pi * (constantTime ((constantSliceDist 0) (diracDelta ℝ 0))) ε);swap𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (constantTime ((constantSliceDist 0) ((2 * Real.pi) • diracDelta ℝ 0))) ε =
  2 * (Real.pi * (constantTime ((constantSliceDist 0) (diracDelta ℝ 0))) ε)𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (constantTime
      ((distDeriv 2) ((distDeriv 2) ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) +
        (distDeriv 1) ((distDeriv 1) ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯)))))
    ε =
  (constantTime ((constantSliceDist 0) ((2 * Real.pi) • diracDelta ℝ 0))) ε
    ·𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (constantTime ((constantSliceDist 0) ((2 * Real.pi) • diracDelta ℝ 0))) ε =
  2 * (Real.pi * (constantTime ((constantSliceDist 0) (diracDelta ℝ 0))) ε) simp𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ 2 * Real.pi * (constantTime ((constantSliceDist 0) (diracDelta ℝ 0))) ε =
  2 * (Real.pi * (constantTime ((constantSliceDist 0) (diracDelta ℝ 0))) ε)
      ringAll goals completed! 🐙
    congre_6𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (distDeriv 2) ((distDeriv 2) ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) +
    (distDeriv 1) ((distDeriv 1) ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) =
  (constantSliceDist 0) ((2 * Real.pi) • diracDelta ℝ 0)
    rw [show (2 : Fin 3) = Fin.succAbove (0 : Fin 3) 1 by𝓕:FreeSpaceI:ℝ⊢ IsExtrema 𝓕 (infiniteWire 𝓕 I) ((wireCurrentDensity 𝓕.c) I)e_6𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (distDeriv (Fin.succAbove 0 1))
      ((distDeriv (Fin.succAbove 0 1)) ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) +
    (distDeriv (Fin.succAbove 0 0))
      ((distDeriv (Fin.succAbove 0 0)) ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) =
  (constantSliceDist 0) ((2 * Real.pi) • diracDelta ℝ 0) simpAll goals completed! 🐙e_6𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (distDeriv (Fin.succAbove 0 1))
      ((distDeriv (Fin.succAbove 0 1)) ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) +
    (distDeriv (Fin.succAbove 0 0))
      ((distDeriv (Fin.succAbove 0 0)) ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) =
  (constantSliceDist 0) ((2 * Real.pi) • diracDelta ℝ 0),
      show (1 : Fin 3) = Fin.succAbove (0 : Fin 3) 0 by𝓕:FreeSpaceI:ℝ⊢ IsExtrema 𝓕 (infiniteWire 𝓕 I) ((wireCurrentDensity 𝓕.c) I)e_6𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (distDeriv (Fin.succAbove 0 1))
      ((distDeriv (Fin.succAbove 0 1)) ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) +
    (distDeriv (Fin.succAbove 0 0))
      ((distDeriv (Fin.succAbove 0 0)) ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) =
  (constantSliceDist 0) ((2 * Real.pi) • diracDelta ℝ 0) simpAll goals completed! 🐙e_6𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (distDeriv (Fin.succAbove 0 1))
      ((distDeriv (Fin.succAbove 0 1)) ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) +
    (distDeriv (Fin.succAbove 0 0))
      ((distDeriv (Fin.succAbove 0 0)) ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) =
  (constantSliceDist 0) ((2 * Real.pi) • diracDelta ℝ 0)]e_6𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (distDeriv (Fin.succAbove 0 1))
      ((distDeriv (Fin.succAbove 0 1)) ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) +
    (distDeriv (Fin.succAbove 0 0))
      ((distDeriv (Fin.succAbove 0 0)) ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) =
  (constantSliceDist 0) ((2 * Real.pi) • diracDelta ℝ 0)
    repeat rw [distDeriv_constantSliceDist_succAbove,e_6𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (distDeriv (Fin.succAbove 0 1)) ((constantSliceDist 0) ((distDeriv 1) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) +
    (distDeriv (Fin.succAbove 0 0))
      ((distDeriv (Fin.succAbove 0 0)) ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) =
  (constantSliceDist 0) ((2 * Real.pi) • diracDelta ℝ 0)e_6𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (constantSliceDist 0) ((distDeriv 1) ((distDeriv 1) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) +
    (constantSliceDist 0) ((distDeriv 0) ((distDeriv 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) =
  (constantSliceDist 0) ((2 * Real.pi) • diracDelta ℝ 0) distDeriv_constantSliceDist_succAbovee_6𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (constantSliceDist 0) ((distDeriv 1) ((distDeriv 1) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) +
    (distDeriv (Fin.succAbove 0 0))
      ((distDeriv (Fin.succAbove 0 0)) ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) =
  (constantSliceDist 0) ((2 * Real.pi) • diracDelta ℝ 0)e_6𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (constantSliceDist 0) ((distDeriv 1) ((distDeriv 1) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) +
    (constantSliceDist 0) ((distDeriv 0) ((distDeriv 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) =
  (constantSliceDist 0) ((2 * Real.pi) • diracDelta ℝ 0)]e_6𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (constantSliceDist 0) ((distDeriv 1) ((distDeriv 1) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) +
    (distDeriv (Fin.succAbove 0 0))
      ((distDeriv (Fin.succAbove 0 0)) ((constantSliceDist 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) =
  (constantSliceDist 0) ((2 * Real.pi) • diracDelta ℝ 0)e_6𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (constantSliceDist 0) ((distDeriv 1) ((distDeriv 1) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) +
    (constantSliceDist 0) ((distDeriv 0) ((distDeriv 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) =
  (constantSliceDist 0) ((2 * Real.pi) • diracDelta ℝ 0)e_6𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (constantSliceDist 0) ((distDeriv 1) ((distDeriv 1) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) +
    (constantSliceDist 0) ((distDeriv 0) ((distDeriv 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) =
  (constantSliceDist 0) ((2 * Real.pi) • diracDelta ℝ 0)
    rw [← map_add (constantSliceDist 0)e_6𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (constantSliceDist 0)
    ((distDeriv 1) ((distDeriv 1) (distOfFunction (fun x => Real.log ‖x‖) ⋯)) +
      (distDeriv 0) ((distDeriv 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) =
  (constantSliceDist 0) ((2 * Real.pi) • diracDelta ℝ 0)e_6𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (constantSliceDist 0)
    ((distDeriv 1) ((distDeriv 1) (distOfFunction (fun x => Real.log ‖x‖) ⋯)) +
      (distDeriv 0) ((distDeriv 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) =
  (constantSliceDist 0) ((2 * Real.pi) • diracDelta ℝ 0)]e_6𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (constantSliceDist 0)
    ((distDeriv 1) ((distDeriv 1) (distOfFunction (fun x => Real.log ‖x‖) ⋯)) +
      (distDeriv 0) ((distDeriv 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) =
  (constantSliceDist 0) ((2 * Real.pi) • diracDelta ℝ 0)
    congre_6.e_6𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (distDeriv 1) ((distDeriv 1) (distOfFunction (fun x => Real.log ‖x‖) ⋯)) +
    (distDeriv 0) ((distDeriv 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯)) =
  (2 * Real.pi) • diracDelta ℝ 0
    trans distDiv (distGrad (distOfFunction (fun (x : Space 2) => Real.log ‖x‖)
      (IsDistBounded.log_norm)))𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (distDeriv 1) ((distDeriv 1) (distOfFunction (fun x => Real.log ‖x‖) ⋯)) +
    (distDeriv 0) ((distDeriv 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯)) =
  distDiv (∇ᵈ (distOfFunction (fun x => Real.log ‖x‖) ⋯))𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ distDiv (∇ᵈ (distOfFunction (fun x => Real.log ‖x‖) ⋯)) = (2 * Real.pi) • diracDelta ℝ 0
    ·𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (distDeriv 1) ((distDeriv 1) (distOfFunction (fun x => Real.log ‖x‖) ⋯)) +
    (distDeriv 0) ((distDeriv 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯)) =
  distDiv (∇ᵈ (distOfFunction (fun x => Real.log ‖x‖) ⋯)) ext ε𝓕:FreeSpaceI:ℝε✝:𝓢(Time × Space, ℝ)ε:𝓢(Space 2, ℝ)⊢ ((distDeriv 1) ((distDeriv 1) (distOfFunction (fun x => Real.log ‖x‖) ⋯)) +
      (distDeriv 0) ((distDeriv 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯)))
    ε =
  (distDiv (∇ᵈ (distOfFunction (fun x => Real.log ‖x‖) ⋯))) ε
      simp [distDiv_apply_eq_sum_distDeriv]𝓕:FreeSpaceI:ℝε✝:𝓢(Time × Space, ℝ)ε:𝓢(Space 2, ℝ)⊢ ((distDeriv 1) ((distDeriv 1) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) ε +
    ((distDeriv 0) ((distDeriv 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) ε =
  (((distDeriv 0) (∇ᵈ (distOfFunction (fun x => Real.log ‖x‖) ⋯))) ε).ofLp 0 +
    (((distDeriv 1) (∇ᵈ (distOfFunction (fun x => Real.log ‖x‖) ⋯))) ε).ofLp 1
      rw [add_comm𝓕:FreeSpaceI:ℝε✝:𝓢(Time × Space, ℝ)ε:𝓢(Space 2, ℝ)⊢ ((distDeriv 0) ((distDeriv 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) ε +
    ((distDeriv 1) ((distDeriv 1) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) ε =
  (((distDeriv 0) (∇ᵈ (distOfFunction (fun x => Real.log ‖x‖) ⋯))) ε).ofLp 0 +
    (((distDeriv 1) (∇ᵈ (distOfFunction (fun x => Real.log ‖x‖) ⋯))) ε).ofLp 1𝓕:FreeSpaceI:ℝε✝:𝓢(Time × Space, ℝ)ε:𝓢(Space 2, ℝ)⊢ ((distDeriv 0) ((distDeriv 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) ε +
    ((distDeriv 1) ((distDeriv 1) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) ε =
  (((distDeriv 0) (∇ᵈ (distOfFunction (fun x => Real.log ‖x‖) ⋯))) ε).ofLp 0 +
    (((distDeriv 1) (∇ᵈ (distOfFunction (fun x => Real.log ‖x‖) ⋯))) ε).ofLp 1]𝓕:FreeSpaceI:ℝε✝:𝓢(Time × Space, ℝ)ε:𝓢(Space 2, ℝ)⊢ ((distDeriv 0) ((distDeriv 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) ε +
    ((distDeriv 1) ((distDeriv 1) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) ε =
  (((distDeriv 0) (∇ᵈ (distOfFunction (fun x => Real.log ‖x‖) ⋯))) ε).ofLp 0 +
    (((distDeriv 1) (∇ᵈ (distOfFunction (fun x => Real.log ‖x‖) ⋯))) ε).ofLp 1
      congr 1e_a𝓕:FreeSpaceI:ℝε✝:𝓢(Time × Space, ℝ)ε:𝓢(Space 2, ℝ)⊢ ((distDeriv 0) ((distDeriv 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) ε =
  (((distDeriv 0) (∇ᵈ (distOfFunction (fun x => Real.log ‖x‖) ⋯))) ε).ofLp 0e_a𝓕:FreeSpaceI:ℝε✝:𝓢(Time × Space, ℝ)ε:𝓢(Space 2, ℝ)⊢ ((distDeriv 1) ((distDeriv 1) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) ε =
  (((distDeriv 1) (∇ᵈ (distOfFunction (fun x => Real.log ‖x‖) ⋯))) ε).ofLp 1 <;>e_a𝓕:FreeSpaceI:ℝε✝:𝓢(Time × Space, ℝ)ε:𝓢(Space 2, ℝ)⊢ ((distDeriv 0) ((distDeriv 0) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) ε =
  (((distDeriv 0) (∇ᵈ (distOfFunction (fun x => Real.log ‖x‖) ⋯))) ε).ofLp 0e_a𝓕:FreeSpaceI:ℝε✝:𝓢(Time × Space, ℝ)ε:𝓢(Space 2, ℝ)⊢ ((distDeriv 1) ((distDeriv 1) (distOfFunction (fun x => Real.log ‖x‖) ⋯))) ε =
  (((distDeriv 1) (∇ᵈ (distOfFunction (fun x => Real.log ‖x‖) ⋯))) ε).ofLp 1
        simp [distDeriv_apply, fderivD_apply, distGrad_apply]All goals completed! 🐙
    rw [distGrad_distOfFunction_log_norm𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ distDiv (distOfFunction (fun x => ‖x‖ ^ (-2) • basis.repr x) ⋯) = (2 * Real.pi) • diracDelta ℝ 0𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ distDiv (distOfFunction (fun x => ‖x‖ ^ (-2) • basis.repr x) ⋯) = (2 * Real.pi) • diracDelta ℝ 0]𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ distDiv (distOfFunction (fun x => ‖x‖ ^ (-2) • basis.repr x) ⋯) = (2 * Real.pi) • diracDelta ℝ 0
    simpa using distDiv_inv_pow_eq_dim (d := 2)All goals completed! 🐙
  all_goals
    simp only [Fin.mk_one, Fin.reduceFinMk, Fin.isValue, neg_sub, Finset.sum_sub_distrib,
      Fin.sum_univ_three, infiniteWire_vectorPotential_distSpaceDeriv_0, map_zero,
      _root_.zero_apply, PiLp.zero_apply, zero_add, add_sub_add_right_eq_sub,
      wireCurrentDensity_currentDensity_snd, wireCurrentDensity_currentDensity_thrd, mul_zero]«2»𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (((distSpaceDeriv 0) ((distSpaceDeriv 2) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp 0 +
      (((distSpaceDeriv 1) ((distSpaceDeriv 2) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp 1 -
    (((distSpaceDeriv 1) ((distSpaceDeriv 1) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp 2 =
  0
    ring_nf«2»𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (((distSpaceDeriv 0) ((distSpaceDeriv 2) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp 0 +
      (((distSpaceDeriv 1) ((distSpaceDeriv 2) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp 1 -
    (((distSpaceDeriv 1) ((distSpaceDeriv 1) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp 2 =
  0
    rw [distSpaceDeriv_commute«1»𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (((distSpaceDeriv 1) ((distSpaceDeriv 0) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp 0 +
      (((distSpaceDeriv 2) ((distSpaceDeriv 1) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp 2 -
    (((distSpaceDeriv 2) ((distSpaceDeriv 2) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp 1 =
  0«2»𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (((distSpaceDeriv 2) ((distSpaceDeriv 0) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp 0 +
      (((distSpaceDeriv 1) ((distSpaceDeriv 2) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp 1 -
    (((distSpaceDeriv 1) ((distSpaceDeriv 1) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp 2 =
  0]«1»𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (((distSpaceDeriv 1) ((distSpaceDeriv 0) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp 0 +
      (((distSpaceDeriv 2) ((distSpaceDeriv 1) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp 2 -
    (((distSpaceDeriv 2) ((distSpaceDeriv 2) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp 1 =
  0«2»𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (((distSpaceDeriv 2) ((distSpaceDeriv 0) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp 0 +
      (((distSpaceDeriv 1) ((distSpaceDeriv 2) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp 1 -
    (((distSpaceDeriv 1) ((distSpaceDeriv 1) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp 2 =
  0«2»𝓕:FreeSpaceI:ℝε:𝓢(Time × Space, ℝ)⊢ (((distSpaceDeriv 2) ((distSpaceDeriv 0) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp 0 +
      (((distSpaceDeriv 1) ((distSpaceDeriv 2) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp 1 -
    (((distSpaceDeriv 1) ((distSpaceDeriv 1) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)))) ε).ofLp 2 =
  0
    simp [distSpaceDeriv_apply']All goals completed! 🐙