Wkp U deriv To Lp sub

lemma WkpU.derivToLp_sub    (f g : WkpU d k p U hU)    (n : ℕ+) (hn : n ≤ k) (s : Fin n → Fin d) :    WkpU.derivtoLp (f - g) n hn s =      WkpU.derivtoLp f n hn s - WkpU.derivtoLp g n hn s := by  apply Lp.ext  obtain ⟨h_neg, eq_neg⟩ := WeakmultiDerivU_smul U hU s g.val (-1) (WkpU.hasWeakDeriv g n hn s)  obtain ⟨h_add, eq_add⟩ := WeakmultiDerivU_add U hU s f.val _ (WkpU.hasWeakDeriv f n hn s) h_neg  have his : IsWeakMultiDerivU U s (f - g).val      (WeakmultiderivU U (f.val + (-1 : ℝ) • g.val) s h_add) := by      have hfg : (f - g).val = f.val + (-1 : ℝ) • g.val := by        ext1; simp [sub_eq_add_neg]      rw [hfg]; exact Classical.choose_spec h_add  have key : (WkpU.weakDeriv (f - g) n hn s : (Fin d → ℝ) → ℝ) =ᵐ[μU d U]      (WkpU.weakDeriv f n hn s : (Fin d → ℝ) → ℝ) - WkpU.weakDeriv g n hn s := by      have step := WeakmultiderivU_unique hU s _ (WkpU.hasWeakDeriv (f - g) n hn s) _ his      filter_upwards [step, eq_add, eq_neg,        AEEqFun.coeFn_add (WeakmultiderivU U f.val s (WkpU.hasWeakDeriv f n hn s) : (Fin d → ℝ) →ₘ[μU d U] ℝ)                          (WeakmultiderivU U ((-1 : ℝ) • g.val) s h_neg : (Fin d → ℝ) →ₘ[μU d U] ℝ),        AEEqFun.coeFn_smul (-1 : ℝ) (WeakmultiderivU U g.val s (WkpU.hasWeakDeriv g n hn s) : (Fin d → ℝ) →ₘ[μU d U] ℝ),        AEEqFun.coeFn_sub (WkpU.weakDeriv f n hn s : (Fin d → ℝ) →ₘ[μU d U] ℝ)                          (WkpU.weakDeriv g n hn s : (Fin d → ℝ) →ₘ[μU d U] ℝ)]        with x h1 h2 h3 h4 h5 h6      simp only [Pi.add_apply, Pi.smul_apply, smul_eq_mul, Pi.sub_apply, WkpU.weakDeriv] at *      linarith  filter_upwards [    (WkpU.weakDeriv_memLp (f - g) n hn s).coeFn_toLp,    (WkpU.weakDeriv_memLp f n hn s).coeFn_toLp,    (WkpU.weakDeriv_memLp g n hn s).coeFn_toLp,    Lp.coeFn_sub (WkpU.weakDeriv_memLp f n hn s).toLp                 (WkpU.weakDeriv_memLp g n hn s).toLp,    key] with x h1 h2 h3 h4 h5  simp only [WkpU.derivtoLp, Pi.sub_apply] at *  linarith