Physlib.Electromagnetism.ThreeDimension.MaxwellEquations

Imports

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

public import Physlib.Electromagnetism.ThreeDimension.Basic
public import Physlib.Electromagnetism.Dynamics.IsExtrema

Maxwell equations in three dimensions

This file states Maxwell's equations in the familiar vector-calculus language and connects them to the tensorial backend formulation.

              local notation "φ" => V.scalarPotential 𝓕.clocal notation "A" => V.vectorPotential 𝓕.clocal notation "E" => V.electricField 𝓕.clocal notation "B" => V.magneticField 𝓕.clocal notation "ρ" => J₄.chargeDensity 𝓕.clocal notation "J" => J₄.currentDensity 𝓕.clocal notation "ε₀" => 𝓕.ε₀local notation "μ₀" => 𝓕.μ₀

Gauss's law for the electric field.

theorem gaussLawElectric (t : Time) (x : Space)
    (h : IsExtrema 𝓕 V J₄) (hV : ContDiff ℝ ∞ V) (hJ : ContDiff ℝ ∞ J₄) :
    (∇ ⬝ E t) x = ρ t x / ε₀ := by𝓕:FreeSpaceV:ElectromagneticPotentialJ₄:LorentzCurrentDensityt:Timex:Spaceh:IsExtrema 𝓕 V J₄hV:ContDiff ℝ ∞ (V.val 3)hJ:ContDiff ℝ ∞ J₄⊢ Space.div (electricField 𝓕.c V t) x = LorentzCurrentDensity.chargeDensity 𝓕.c J₄ t x / 𝓕.ε₀
  exact ((isExtrema_iff_gauss_ampere_magneticFieldMatrix hV J₄ hJ (𝓕 := 𝓕)).mp h t x).1All goals completed! 🐙

Gauss's law for the magnetic field.


theorem gaussLawMagnetic (t : Time) (x : Space) (hV : ContDiff ℝ ∞ V) :
    (∇ ⬝ B t) x = 0 := by𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Space.div (magneticField 𝓕.c V t) x = 0
  rw [magneticField_eq_3D,𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Space.div ((fun t x => curl (vectorPotential 𝓕.c V t) x) t) x = 0All goals completed! 🐙 div_of_curl_eq_zero _ (by𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ ContDiff ℝ 2 (vectorPotential 𝓕.c V t)All goals completed! 🐙 fun_propAll goals completed! 🐙All goals completed! 🐙), Pi.zero_apply𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙

Ampère's law.


theorem ampereLaw (t : Time) (x : Space)
    (h : IsExtrema 𝓕 V J₄) (hV : ContDiff ℝ ∞ V) (hJ : ContDiff ℝ ∞ J₄) :
      (∇ ⨯ B t) x = μ₀ • J t x + μ₀ • ε₀ • ∂ₜ (fun t => E t x) t := by𝓕:FreeSpaceV:ElectromagneticPotentialJ₄:LorentzCurrentDensityt:Timex:Spaceh:IsExtrema 𝓕 V J₄hV:ContDiff ℝ ∞ (V.val 3)hJ:ContDiff ℝ ∞ J₄⊢ curl (magneticField 𝓕.c V t) x =
  𝓕.μ₀ • LorentzCurrentDensity.currentDensity 𝓕.c J₄ t x + 𝓕.μ₀ • 𝓕.ε₀ • ∂ₜ (fun t => electricField 𝓕.c V t x) t
  ext i𝓕:FreeSpaceV:ElectromagneticPotentialJ₄:LorentzCurrentDensityt:Timex:Spaceh:IsExtrema 𝓕 V J₄hV:ContDiff ℝ ∞ (V.val 3)hJ:ContDiff ℝ ∞ J₄i:Fin 3⊢ (curl (magneticField 𝓕.c V t) x).ofLp i =
  (𝓕.μ₀ • LorentzCurrentDensity.currentDensity 𝓕.c J₄ t x + 𝓕.μ₀ • 𝓕.ε₀ • ∂ₜ (fun t => electricField 𝓕.c V t x) t).ofLp
    i
  have hdE := ((isExtrema_iff_gauss_ampere_magneticFieldMatrix hV J₄ hJ (𝓕 := 𝓕)).mp h t x).2 i𝓕:FreeSpaceV:ElectromagneticPotentialJ₄:LorentzCurrentDensityt:Timex:Spaceh:IsExtrema 𝓕 V J₄hV:ContDiff ℝ ∞ (V.val 3)hJ:ContDiff ℝ ∞ J₄i:Fin 3hdE:𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c V t x) t).ofLp i =
  ∑ j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c V t x (j, i)) x -
    𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J₄ t x).ofLp i⊢ (curl (magneticField 𝓕.c V t) x).ofLp i =
  (𝓕.μ₀ • LorentzCurrentDensity.currentDensity 𝓕.c J₄ t x + 𝓕.μ₀ • 𝓕.ε₀ • ∂ₜ (fun t => electricField 𝓕.c V t x) t).ofLp
    i
  rw [← magneticField_curl_eq_magneticFieldMatrix _ (hV.of_le ENat.LEInfty.out)𝓕:FreeSpaceV:ElectromagneticPotentialJ₄:LorentzCurrentDensityt:Timex:Spaceh:IsExtrema 𝓕 V J₄hV:ContDiff ℝ ∞ (V.val 3)hJ:ContDiff ℝ ∞ J₄i:Fin 3hdE:𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c V t x) t).ofLp i =
  (curl (magneticField 𝓕.c V t) x).ofLp i - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J₄ t x).ofLp i⊢ (curl (magneticField 𝓕.c V t) x).ofLp i =
  (𝓕.μ₀ • LorentzCurrentDensity.currentDensity 𝓕.c J₄ t x + 𝓕.μ₀ • 𝓕.ε₀ • ∂ₜ (fun t => electricField 𝓕.c V t x) t).ofLp
    i𝓕:FreeSpaceV:ElectromagneticPotentialJ₄:LorentzCurrentDensityt:Timex:Spaceh:IsExtrema 𝓕 V J₄hV:ContDiff ℝ ∞ (V.val 3)hJ:ContDiff ℝ ∞ J₄i:Fin 3hdE:𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c V t x) t).ofLp i =
  (curl (magneticField 𝓕.c V t) x).ofLp i - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J₄ t x).ofLp i⊢ (curl (magneticField 𝓕.c V t) x).ofLp i =
  (𝓕.μ₀ • LorentzCurrentDensity.currentDensity 𝓕.c J₄ t x + 𝓕.μ₀ • 𝓕.ε₀ • ∂ₜ (fun t => electricField 𝓕.c V t x) t).ofLp
    i] at hdE𝓕:FreeSpaceV:ElectromagneticPotentialJ₄:LorentzCurrentDensityt:Timex:Spaceh:IsExtrema 𝓕 V J₄hV:ContDiff ℝ ∞ (V.val 3)hJ:ContDiff ℝ ∞ J₄i:Fin 3hdE:𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c V t x) t).ofLp i =
  (curl (magneticField 𝓕.c V t) x).ofLp i - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J₄ t x).ofLp i⊢ (curl (magneticField 𝓕.c V t) x).ofLp i =
  (𝓕.μ₀ • LorentzCurrentDensity.currentDensity 𝓕.c J₄ t x + 𝓕.μ₀ • 𝓕.ε₀ • ∂ₜ (fun t => electricField 𝓕.c V t x) t).ofLp
    i
  simp only [PiLp.add_apply, PiLp.smul_apply, smul_eq_mul, ← mul_assoc, hdE, add_sub_cancel]All goals completed! 🐙

Faraday's law.


theorem faradayLaw (t : Time) (x : Space) (hV : ContDiff ℝ ∞ V) :
    (∇ ⨯ E t) x = - ∂ₜ (fun t => B t x) t := by𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ curl (electricField 𝓕.c V t) x = -∂ₜ (fun t => magneticField 𝓕.c V t x) t
  rw [electricField_eq_3D,𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ curl ((fun t x => -∇ (scalarPotential 𝓕.c V t) x - ∂ₜ (fun t => vectorPotential 𝓕.c V t x) t) t) x =
  -∂ₜ (fun t => magneticField 𝓕.c V t x) t𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ (fun i => (fun i => -0 i) i - curl (fun x => ∂ₜ (fun t => vectorPotential 𝓕.c V t x) t) i) x =
  -curl (fun x => ∂ₜ (fun t => vectorPotential 𝓕.c V t x) t) xhf𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ ContDiff ℝ 2 ↿(vectorPotential 𝓕.c V)hf𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ ContDiff ℝ 2 (scalarPotential 𝓕.c V t)hf𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Differentiable ℝ (∇ (scalarPotential 𝓕.c V t))hf1𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Differentiable ℝ fun x => -∇ (scalarPotential 𝓕.c V t) xhf2𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Differentiable ℝ fun x => ∂ₜ (fun t => vectorPotential 𝓕.c V t x) t magneticField_eq_3D,𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ curl ((fun t x => -∇ (scalarPotential 𝓕.c V t) x - ∂ₜ (fun t => vectorPotential 𝓕.c V t x) t) t) x =
  -∂ₜ (fun t => (fun t x => curl (vectorPotential 𝓕.c V t) x) t x) t𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ (fun i => (fun i => -0 i) i - curl (fun x => ∂ₜ (fun t => vectorPotential 𝓕.c V t x) t) i) x =
  -curl (fun x => ∂ₜ (fun t => vectorPotential 𝓕.c V t x) t) xhf𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ ContDiff ℝ 2 ↿(vectorPotential 𝓕.c V)hf𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ ContDiff ℝ 2 (scalarPotential 𝓕.c V t)hf𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Differentiable ℝ (∇ (scalarPotential 𝓕.c V t))hf1𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Differentiable ℝ fun x => -∇ (scalarPotential 𝓕.c V t) xhf2𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Differentiable ℝ fun x => ∂ₜ (fun t => vectorPotential 𝓕.c V t x) t fun_curl_sub,𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ (fun i =>
      curl (fun x => -∇ (scalarPotential 𝓕.c V t) x) i - curl (fun x => ∂ₜ (fun t => vectorPotential 𝓕.c V t x) t) i)
    x =
  -∂ₜ (fun t => (fun t x => curl (vectorPotential 𝓕.c V t) x) t x) thf1𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Differentiable ℝ fun x => -∇ (scalarPotential 𝓕.c V t) xhf2𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Differentiable ℝ fun x => ∂ₜ (fun t => vectorPotential 𝓕.c V t x) t𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ (fun i => (fun i => -0 i) i - curl (fun x => ∂ₜ (fun t => vectorPotential 𝓕.c V t x) t) i) x =
  -curl (fun x => ∂ₜ (fun t => vectorPotential 𝓕.c V t x) t) xhf𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ ContDiff ℝ 2 ↿(vectorPotential 𝓕.c V)hf𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ ContDiff ℝ 2 (scalarPotential 𝓕.c V t)hf𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Differentiable ℝ (∇ (scalarPotential 𝓕.c V t))hf1𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Differentiable ℝ fun x => -∇ (scalarPotential 𝓕.c V t) xhf2𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Differentiable ℝ fun x => ∂ₜ (fun t => vectorPotential 𝓕.c V t x) t fun_curl_neg,𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ (fun i =>
      (fun i => -curl (∇ (scalarPotential 𝓕.c V t)) i) i - curl (fun x => ∂ₜ (fun t => vectorPotential 𝓕.c V t x) t) i)
    x =
  -∂ₜ (fun t => (fun t x => curl (vectorPotential 𝓕.c V t) x) t x) thf𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Differentiable ℝ (∇ (scalarPotential 𝓕.c V t))hf1𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Differentiable ℝ fun x => -∇ (scalarPotential 𝓕.c V t) xhf2𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Differentiable ℝ fun x => ∂ₜ (fun t => vectorPotential 𝓕.c V t x) t𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ (fun i => (fun i => -0 i) i - curl (fun x => ∂ₜ (fun t => vectorPotential 𝓕.c V t x) t) i) x =
  -curl (fun x => ∂ₜ (fun t => vectorPotential 𝓕.c V t x) t) xhf𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ ContDiff ℝ 2 ↿(vectorPotential 𝓕.c V)hf𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ ContDiff ℝ 2 (scalarPotential 𝓕.c V t)hf𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Differentiable ℝ (∇ (scalarPotential 𝓕.c V t))hf1𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Differentiable ℝ fun x => -∇ (scalarPotential 𝓕.c V t) xhf2𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Differentiable ℝ fun x => ∂ₜ (fun t => vectorPotential 𝓕.c V t x) t
    curl_of_grad_eq_zero,𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ (fun i => (fun i => -0 i) i - curl (fun x => ∂ₜ (fun t => vectorPotential 𝓕.c V t x) t) i) x =
  -∂ₜ (fun t => (fun t x => curl (vectorPotential 𝓕.c V t) x) t x) thf𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ ContDiff ℝ 2 (scalarPotential 𝓕.c V t)hf𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Differentiable ℝ (∇ (scalarPotential 𝓕.c V t))hf1𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Differentiable ℝ fun x => -∇ (scalarPotential 𝓕.c V t) xhf2𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Differentiable ℝ fun x => ∂ₜ (fun t => vectorPotential 𝓕.c V t x) t𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ (fun i => (fun i => -0 i) i - curl (fun x => ∂ₜ (fun t => vectorPotential 𝓕.c V t x) t) i) x =
  -curl (fun x => ∂ₜ (fun t => vectorPotential 𝓕.c V t x) t) xhf𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ ContDiff ℝ 2 ↿(vectorPotential 𝓕.c V)hf𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ ContDiff ℝ 2 (scalarPotential 𝓕.c V t)hf𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Differentiable ℝ (∇ (scalarPotential 𝓕.c V t))hf1𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Differentiable ℝ fun x => -∇ (scalarPotential 𝓕.c V t) xhf2𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Differentiable ℝ fun x => ∂ₜ (fun t => vectorPotential 𝓕.c V t x) t time_deriv_curl_commute𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ (fun i => (fun i => -0 i) i - curl (fun x => ∂ₜ (fun t => vectorPotential 𝓕.c V t x) t) i) x =
  -curl (fun x => ∂ₜ (fun t => vectorPotential 𝓕.c V t x) t) xhf𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ ContDiff ℝ 2 ↿(vectorPotential 𝓕.c V)hf𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ ContDiff ℝ 2 (scalarPotential 𝓕.c V t)hf𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Differentiable ℝ (∇ (scalarPotential 𝓕.c V t))hf1𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Differentiable ℝ fun x => -∇ (scalarPotential 𝓕.c V t) xhf2𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Differentiable ℝ fun x => ∂ₜ (fun t => vectorPotential 𝓕.c V t x) t𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ (fun i => (fun i => -0 i) i - curl (fun x => ∂ₜ (fun t => vectorPotential 𝓕.c V t x) t) i) x =
  -curl (fun x => ∂ₜ (fun t => vectorPotential 𝓕.c V t x) t) xhf𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ ContDiff ℝ 2 ↿(vectorPotential 𝓕.c V)hf𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ ContDiff ℝ 2 (scalarPotential 𝓕.c V t)hf𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Differentiable ℝ (∇ (scalarPotential 𝓕.c V t))hf1𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Differentiable ℝ fun x => -∇ (scalarPotential 𝓕.c V t) xhf2𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Differentiable ℝ fun x => ∂ₜ (fun t => vectorPotential 𝓕.c V t x) t]𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ (fun i => (fun i => -0 i) i - curl (fun x => ∂ₜ (fun t => vectorPotential 𝓕.c V t x) t) i) x =
  -curl (fun x => ∂ₜ (fun t => vectorPotential 𝓕.c V t x) t) xhf𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ ContDiff ℝ 2 ↿(vectorPotential 𝓕.c V)hf𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ ContDiff ℝ 2 (scalarPotential 𝓕.c V t)hf𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Differentiable ℝ (∇ (scalarPotential 𝓕.c V t))hf1𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Differentiable ℝ fun x => -∇ (scalarPotential 𝓕.c V t) xhf2𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Differentiable ℝ fun x => ∂ₜ (fun t => vectorPotential 𝓕.c V t x) t
  simp only [neg_zero, Pi.zero_apply, zero_sub]hf𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ ContDiff ℝ 2 ↿(vectorPotential 𝓕.c V)hf𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ ContDiff ℝ 2 (scalarPotential 𝓕.c V t)hf𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Differentiable ℝ (∇ (scalarPotential 𝓕.c V t))hf1𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Differentiable ℝ fun x => -∇ (scalarPotential 𝓕.c V t) xhf2𝓕:FreeSpaceV:ElectromagneticPotentialt:Timex:SpacehV:ContDiff ℝ ∞ (V.val 3)⊢ Differentiable ℝ fun x => ∂ₜ (fun t => vectorPotential 𝓕.c V t x) t
  all_goals fun_propAll goals completed! 🐙