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

A. Maxwell's equations in three dimensions

Maxwell's equations relate electric and magnetic fields to electric charge and current. In three spatial dimensions they can be written using the familiar divergence, curl, and time-derivative operators of vector calculus.

A.1. Main results

This module proves the four differential equations:

gaussLawElectric, relating the divergence of the electric field to charge density;

gaussLawMagnetic, stating that the magnetic field is divergence-free;

ampereLaw, including both the electric current and displacement-current terms;

faradayLaw, relating the curl of the electric field to the time derivative of the magnetic field.

A.2. Relation to the covariant formulation

The electric and magnetic fields are obtained from an electromagnetic potential. Gauss's law for the electric field and Ampère's law are derived from the covariant extremality condition IsExtrema, while the two homogeneous equations follow from the potential definitions and smoothness assumptions. The results therefore connect the tensorial backend to the standard three-dimensional presentation.

A.3. Current scope

The statements here are pointwise differential equations in free space. Integral formulations, boundary conditions, and constitutive laws for material media are outside the current scope of this module.

              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! 🐙