Of Electromagnetic Field electric Field

lemma ofElectromagneticField_electricField {c : SpeedOfLight}    (E : Time → Space 3 → EuclideanSpace ℝ (Fin 3)) (B : Time → Space 3 → EuclideanSpace ℝ (Fin 3))    (E_contDiff : ContDiff ℝ 1 ↿E) (B_contDiff : ContDiff ℝ 2 ↿B)    (B_grad : ∀ t, ∇ ⬝ (B t) = 0) (faraday : ∀ t x, curl (E t) x = - ∂ₜ (B · x) t) :    (ofElectromagneticField c E B).electricField c = E := by  have h0 := B_contDiff.of_le (m := 1) (by simp)  ext1 t  ext1 x  suffices h : E t x + ∂ₜ (fun t => (ofElectromagneticField c E B).vectorPotential c t x) t =      - ∇ ((ofElectromagneticField c E B).scalarPotential c t) x by    simp only [electricField]    rw [sub_eq_iff_eq_add', ← h, add_comm]  convert congrFun (eq_grad_integral_of_curl_zero (fun x => E t x +      ∂ₜ (fun t => (ofElectromagneticField c E B).vectorPotential c t x) t) ?_ ?_) x  · simp [ofElectromagneticField_scalarPotential_eq_add_vectorPotential _ _ B (by fun_prop)]    rw [fun_grad_neg]    simp  · simp only [Time.deriv]    fun_prop  · rw [fun_curl_add]    ext1 x    simp [faraday]    suffices h : ∂ₜ (B · x) t = curl (fun x =>        ∂ₜ ((ofElectromagneticField c E B).vectorPotential c · x) t) x by      simp [h]    rw [← Space.time_deriv_curl_commute]    · congr      funext t      have h1 := eq_neg_curl_of_div_zero (B t) (by fun_prop) (B_grad t)      conv_lhs => rw [h1]      simp only [ofElectromagneticField_vectorPotential]      rw [fun_curl_neg]      simp only [WithLp.equiv_apply, WithLp.ofLp_smul, map_smul, LinearMap.smul_apply,        WithLp.equiv_symm_apply, WithLp.toLp_smul, Pi.neg_apply]      intro x      apply Differentiable.differentiableAt      apply ContDiff.differentiable (n := 1) _ (by simp)      apply contDiff_parametric_intervalIntegral_of_contDiff      refine contDiff_euclidean.mpr ?_      intro i      let C : (Space) × ℝ → EuclideanSpace ℝ (Fin 3) := fun p =>        let x:= p.1        let u := p.2        (u • basis.repr x) ⨯ₑ₃ B t (u • x)      suffices h : ContDiff ℝ 1 (fun x => C x i) by        convert! h        exact 1      fin_cases i      all_goals      · simp [C, crossProduct]        fun_prop    · fun_prop    · fun_prop    · simp only [Time.deriv]      fun_prop