Infinite Wire is Exterma

lemma infiniteWire_isExterma {𝓕 : FreeSpace} {I : ℝ} :    IsExtrema 𝓕 (infiniteWire 𝓕 I) (wireCurrentDensity 𝓕.c I) := by  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]  intro ε i  rw [neg_add_eq_zero]  fin_cases i  · simp [Fin.sum_univ_three]    simp [distSpaceDeriv_apply', infiniteWire_vectorPotential_fst]    simp [apply_fderiv_eq_distSpaceDeriv, wireCurrentDensity_currentDensity_fst]    field_simp    simp only [constantTime_distSpaceDeriv, mul_assoc]    congr    rw [← _root_.add_apply, ← map_add constantTime]    trans (constantTime ((constantSliceDist 0) ((2 * Real.pi) • diracDelta ℝ 0))) ε;swap    · simp      ring    congr    rw [show (2 : Fin 3) = Fin.succAbove (0 : Fin 3) 1 by simp,      show (1 : Fin 3) = Fin.succAbove (0 : Fin 3) 0 by simp]    repeat rw [distDeriv_constantSliceDist_succAbove, distDeriv_constantSliceDist_succAbove]    rw [← map_add (constantSliceDist 0)]    congr    trans distDiv (distGrad (distOfFunction (fun (x : Space 2) => Real.log ‖x‖)      (IsDistBounded.log_norm)))    · ext ε      simp [distDiv_apply_eq_sum_distDeriv]      rw [add_comm]      congr 1 <;>        simp [distDeriv_apply, fderivD_apply, distGrad_apply]    rw [distGrad_distOfFunction_log_norm]    simpa using distDiv_inv_pow_eq_dim (d := 2)  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]    ring_nf    rw [distSpaceDeriv_commute]    simp [distSpaceDeriv_apply']