Dist Laplacian fundamental Solution norm zpow

lemma distLaplacian_fundamentalSolution_norm_zpow {d : ℕ} :    Δᵈ (distOfFunction (fun x : Space d => ‖x‖ ^ (- ((d : ℤ) - 2)))      (IsDistBounded.pow _ (by omega))) =      ((- ((d : ℝ) - 2)) * d *        (volume (α := Space d)).real (Metric.ball 0 1)) • diracDelta ℝ 0 := by  by_cases h : d = 0  · subst h    have hzero :        distOfFunction (fun x : Space 0 => ‖x‖ ^ 2)          (IsDistBounded.pow _ (by omega)) = 0 := by      ext η      rw [distOfFunction_apply]      refine integral_eq_zero_of_ae (ae_of_all _ fun x => ?_)      rw [Subsingleton.elim x 0]      simp [zero_zpow_eq]    simp [hzero]  · haveI : NeZero d := ⟨by omega⟩    rw [distLaplacian]    change ∇ᵈ ⬝ (∇ᵈ (distOfFunction      (fun x : Space d => ‖x‖ ^ (- ((d : ℤ) - 2)))      (IsDistBounded.pow (- ((d : ℤ) - 2)) (by omega)))) = _    rw [distGrad_distOfFunction_norm_zpow (- ((d : ℤ) - 2)) (by omega)]    simp only [neg_sub, Int.cast_sub, Int.cast_ofNat, Int.cast_natCast, sub_sub_cancel_left]    have hdist :        distOfFunction          (fun x : Space d =>            ((2 - (d : ℝ)) * ‖x‖ ^ (- (d : ℤ))) • basis.repr x)          (by            simpa [smul_smul] using              (IsDistBounded.const_fun_smul                (F := EuclideanSpace ℝ (Fin d))                (IsDistBounded.zpow_smul_repr_self (- (d : ℤ)) (by omega))                (2 - (d : ℝ)))) =          (2 - (d : ℝ)) • distOfFunction            (fun x : Space d =>              ‖x‖ ^ (- (d : ℤ)) • basis.repr x)            (IsDistBounded.zpow_smul_repr_self (- (d : ℤ)) (by omega)) := by      convert distOfFunction_smul_fun        (fun x : Space d =>          ‖x‖ ^ (- (d : ℤ)) • basis.repr x)        (IsDistBounded.zpow_smul_repr_self (- (d : ℤ)) (by omega))        (2 - (d : ℝ)) using 1      ext x      simp [smul_smul]    rw [hdist, map_smul, distDiv_inv_pow_eq_dim, smul_smul]    ring_nf