diff --git a/Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean b/Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
index 1766a15fd5def4..93c6d2e2923832 100644
--- a/Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
+++ b/Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
@@ -440,7 +440,9 @@ theorem condExpL1CLM_of_aestronglyMeasurable' (f : α →₁[μ] F') (hfm : AESt
 
 /-- Conditional expectation of a function, in L1. Its value is 0 if the function is not
 integrable. The function-valued `condExp` should be used instead in most cases. -/
-def condExpL1 (hm : m ≤ m0) (μ : Measure α) [SigmaFinite (μ.trim hm)] (f : α → F') : α →₁[μ] F' :=
+@[nolint unusedArguments] -- TODO: drop the completeness assumption in the definition, and fix
+def condExpL1 [CompleteSpace F'] (hm : m ≤ m0) (μ : Measure α) [SigmaFinite (μ.trim hm)]
+    (f : α → F') : α →₁[μ] F' :=
   setToFun μ (condExpInd F' hm μ) (dominatedFinMeasAdditive_condExpInd F' hm μ) f
 
 theorem condExpL1_undef (hf : ¬Integrable f μ) : condExpL1 hm μ f = 0 :=
diff --git a/Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean b/Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean
index 7c815018f6cfea..0f039ac6ec4586 100644
--- a/Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean
+++ b/Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean
@@ -213,6 +213,10 @@ theorem norm_toL1_eq_lintegral_norm (f : α → β) (hf : Integrable f μ) :
     ‖hf.toL1 f‖ = ENNReal.toReal (∫⁻ a, ENNReal.ofReal ‖f a‖ ∂μ) := by
   rw [norm_toL1, lintegral_norm_eq_lintegral_edist]
 
+theorem norm_toL1_eq_lintegral_enorm (f : α → β) (hf : Integrable f μ) :
+    ‖hf.toL1 f‖ = (∫⁻ a, ‖f a‖ₑ ∂μ).toReal := by
+  simp_rw [norm_toL1, edist_zero_right]
+
 @[simp]
 theorem edist_toL1_toL1 (f g : α → β) (hf : Integrable f μ) (hg : Integrable g μ) :
     edist (hf.toL1 f) (hg.toL1 g) = ∫⁻ a, edist (f a) (g a) ∂μ := by
diff --git a/Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean b/Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
index 3a8fe0b9fb25ee..3ac718ef4842d6 100644
--- a/Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
+++ b/Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
@@ -364,6 +364,8 @@ end SimpleFuncProperties
 
 end SimpleFunc
 
+open SimpleFunc
+
 /-! Construction of the space of `Lp` simple functions, and its dense embedding into `Lp`. -/
 
 
@@ -466,7 +468,7 @@ attribute [local instance] simpleFunc.module simpleFunc.normedSpace simpleFunc.i
 section ToLp
 
 /-- Construct the equivalence class `[f]` of a simple function `f` satisfying `MemLp`. -/
-abbrev toLp (f : α →ₛ E) (hf : MemLp f p μ) : Lp.simpleFunc E p μ :=
+abbrev _root_.MeasureTheory.SimpleFunc.toLp (f : α →ₛ E) (hf : MemLp f p μ) : Lp.simpleFunc E p μ :=
   ⟨hf.toLp f, ⟨f, rfl⟩⟩
 
 theorem toLp_eq_toLp (f : α →ₛ E) (hf : MemLp f p μ) : (toLp f hf : Lp E p μ) = hf.toLp f :=
@@ -621,8 +623,8 @@ protected theorem induction (hp_pos : p ≠ 0) (hp_ne_top : p ≠ ∞) {P : Lp.s
         ∀ hf : MemLp f p μ,
           ∀ hg : MemLp g p μ,
             Disjoint (support f) (support g) →
-              P (Lp.simpleFunc.toLp f hf) →
-                P (Lp.simpleFunc.toLp g hg) → P (Lp.simpleFunc.toLp f hf + Lp.simpleFunc.toLp g hg))
+              P (toLp f hf) →
+                P (toLp g hg) → P (toLp f hf + toLp g hg))
     (f : Lp.simpleFunc E p μ) : P f := by
   suffices ∀ f : α →ₛ E, ∀ hf : MemLp f p μ, P (toLp f hf) by
     rw [← toLp_toSimpleFunc f]
@@ -691,7 +693,7 @@ variable (α E 𝕜)
 /-- The embedding of Lp simple functions into Lp functions, as a continuous linear map. -/
 def coeToLp : Lp.simpleFunc E p μ →L[𝕜] Lp E p μ :=
   { AddSubgroup.subtype (Lp.simpleFunc E p μ) with
-    map_smul' _ _ := rfl }
+    map_smul' := fun _ _ => rfl }
 
 end CoeToLp
 
@@ -907,7 +909,7 @@ section Integrable
 notation:25 α " →₁ₛ[" μ "] " E => @MeasureTheory.Lp.simpleFunc α E _ _ 1 μ
 
 theorem L1.SimpleFunc.toLp_one_eq_toL1 (f : α →ₛ E) (hf : Integrable f μ) :
-    (Lp.simpleFunc.toLp f (memLp_one_iff_integrable.2 hf) : α →₁[μ] E) = hf.toL1 f :=
+    (toLp f (memLp_one_iff_integrable.2 hf) : α →₁[μ] E) = hf.toL1 f :=
   rfl
 
 @[fun_prop]
diff --git a/Mathlib/MeasureTheory/Integral/Bochner/Basic.lean b/Mathlib/MeasureTheory/Integral/Bochner/Basic.lean
index 3694203559cb08..f7d635f4f3f771 100644
--- a/Mathlib/MeasureTheory/Integral/Bochner/Basic.lean
+++ b/Mathlib/MeasureTheory/Integral/Bochner/Basic.lean
@@ -194,7 +194,7 @@ theorem integral_eq (f : α → E) (hf : Integrable f μ) : ∫ a, f a ∂μ = L
 
 theorem integral_eq_setToFun (f : α → E) :
     ∫ a, f a ∂μ = setToFun μ (weightedSMul μ) (dominatedFinMeasAdditive_weightedSMul μ) f := by
-  simp only [integral, hE, L1.integral]; rfl
+  simp only [integral, hE, ↓reduceDIte, L1.integral, setToFun]; rfl
 
 theorem L1.integral_eq_integral (f : α →₁[μ] E) : L1.integral f = ∫ a, f a ∂μ := by
   simp only [integral, L1.integral, integral_eq_setToFun]
@@ -217,7 +217,7 @@ variable (α G)
 @[simp]
 theorem integral_zero : ∫ _ : α, (0 : G) ∂μ = 0 := by
   by_cases hG : CompleteSpace G
-  · simp only [integral, hG, L1.integral]
+  · simp only [integral_eq_setToFun]
     exact setToFun_zero (dominatedFinMeasAdditive_weightedSMul μ)
   · simp [integral, hG]
 
@@ -237,7 +237,7 @@ theorem integrable_of_integral_eq_one {f : α → ℝ} (h : ∫ x, f x ∂μ = 1
 theorem integral_add {f g : α → G} (hf : Integrable f μ) (hg : Integrable g μ) :
     ∫ a, f a + g a ∂μ = ∫ a, f a ∂μ + ∫ a, g a ∂μ := by
   by_cases hG : CompleteSpace G
-  · simp only [integral, hG, L1.integral]
+  · simp only [integral_eq_setToFun]
     exact setToFun_add (dominatedFinMeasAdditive_weightedSMul μ) hf hg
   · simp [integral, hG]
 
@@ -248,7 +248,7 @@ theorem integral_add' {f g : α → G} (hf : Integrable f μ) (hg : Integrable g
 theorem integral_finsetSum {ι} (s : Finset ι) {f : ι → α → G} (hf : ∀ i ∈ s, Integrable (f i) μ) :
     ∫ a, ∑ i ∈ s, f i a ∂μ = ∑ i ∈ s, ∫ a, f i a ∂μ := by
   by_cases hG : CompleteSpace G
-  · simp only [integral, hG, L1.integral]
+  · simp only [integral_eq_setToFun]
     exact setToFun_finsetSum (dominatedFinMeasAdditive_weightedSMul _) s hf
   · simp [integral, hG]
 
@@ -257,7 +257,7 @@ theorem integral_finsetSum {ι} (s : Finset ι) {f : ι → α → G} (hf : ∀
 @[integral_simps]
 theorem integral_neg (f : α → G) : ∫ a, -f a ∂μ = -∫ a, f a ∂μ := by
   by_cases hG : CompleteSpace G
-  · simp only [integral, hG, L1.integral]
+  · simp only [integral_eq_setToFun]
     exact setToFun_neg (dominatedFinMeasAdditive_weightedSMul μ) f
   · simp [integral, hG]
 
@@ -267,7 +267,7 @@ theorem integral_neg' (f : α → G) : ∫ a, (-f) a ∂μ = -∫ a, f a ∂μ :
 theorem integral_sub {f g : α → G} (hf : Integrable f μ) (hg : Integrable g μ) :
     ∫ a, f a - g a ∂μ = ∫ a, f a ∂μ - ∫ a, g a ∂μ := by
   by_cases hG : CompleteSpace G
-  · simp only [integral, hG, L1.integral]
+  · simp only [integral_eq_setToFun]
     exact setToFun_sub (dominatedFinMeasAdditive_weightedSMul μ) hf hg
   · simp [integral, hG]
 
@@ -283,7 +283,7 @@ statement for more general rings with an *a priori* integrability assumption on
 theorem integral_smul [Module 𝕜 G] [NormSMulClass 𝕜 G] [SMulCommClass ℝ 𝕜 G] (c : 𝕜) (f : α → G) :
     ∫ a, c • f a ∂μ = c • ∫ a, f a ∂μ := by
   by_cases hG : CompleteSpace G
-  · simp only [integral, hG, L1.integral]
+  · simp only [integral_eq_setToFun]
     exact setToFun_smul (dominatedFinMeasAdditive_weightedSMul μ) weightedSMul_smul c f
   · simp [integral, hG]
 
@@ -308,7 +308,7 @@ theorem integral_div {L : Type*} [RCLike L] (r : L) (f : α → L) :
 
 theorem integral_congr_ae {f g : α → G} (h : f =ᵐ[μ] g) : ∫ a, f a ∂μ = ∫ a, g a ∂μ := by
   by_cases hG : CompleteSpace G
-  · simp only [integral, hG, L1.integral]
+  · simp only [integral_eq_setToFun]
     exact setToFun_congr_ae (dominatedFinMeasAdditive_weightedSMul μ) h
   · simp [integral, hG]
 
@@ -324,7 +324,7 @@ lemma integral_congr_ae₂ {β : Type*} {_ : MeasurableSpace β} {ν : Measure 
 theorem L1.integral_of_fun_eq_integral' {f : α → G} (hf : Integrable f μ) :
     ∫ a, (AEEqFun.mk f hf.aestronglyMeasurable) a ∂μ = ∫ a, f a ∂μ := by
   by_cases hG : CompleteSpace G
-  · simp only [MeasureTheory.integral, hG, L1.integral]
+  · simp only [integral_eq_setToFun]
     exact setToFun_toL1 (dominatedFinMeasAdditive_weightedSMul μ) hf
   · simp [MeasureTheory.integral, hG]
 
@@ -335,7 +335,7 @@ theorem L1.integral_of_fun_eq_integral {f : α → G} (hf : Integrable f μ) :
 @[continuity]
 theorem continuous_integral : Continuous fun f : α →₁[μ] G => ∫ a, f a ∂μ := by
   by_cases hG : CompleteSpace G
-  · simp only [integral, hG, L1.integral]
+  · simp only [integral_eq_setToFun]
     exact continuous_setToFun (dominatedFinMeasAdditive_weightedSMul μ)
   · simp [integral, hG, continuous_const]
 
@@ -401,8 +401,9 @@ theorem tendsto_integral_of_L1 {ι} (f : α → G) (hfi : Integrable f μ) {F :
     (hF : Tendsto (fun i => ∫⁻ x, ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)) :
     Tendsto (fun i => ∫ x, F i x ∂μ) l (𝓝 <| ∫ x, f x ∂μ) := by
   by_cases hG : CompleteSpace G
-  · simp only [integral, hG, L1.integral]
-    exact tendsto_setToFun_of_L1 (dominatedFinMeasAdditive_weightedSMul μ) f hfi hFi hF
+  · simp only [integral_eq_setToFun]
+    exact tendsto_setToFun_of_L1 (dominatedFinMeasAdditive_weightedSMul μ)
+      f hfi.aestronglyMeasurable hFi hF
   · simp [integral, hG, tendsto_const_nhds]
 
 /-- If `F i → f` in `L1`, then `∫ x, F i x ∂μ → ∫ x, f x ∂μ`. -/
@@ -443,7 +444,7 @@ theorem continuousWithinAt_of_dominated {F : X → α → G} {x₀ : X} {bound :
     (h_cont : ∀ᵐ a ∂μ, ContinuousWithinAt (fun x => F x a) s x₀) :
     ContinuousWithinAt (fun x => ∫ a, F x a ∂μ) s x₀ := by
   by_cases hG : CompleteSpace G
-  · simp only [integral, hG, L1.integral]
+  · simp only [integral_eq_setToFun]
     exact continuousWithinAt_setToFun_of_dominated (dominatedFinMeasAdditive_weightedSMul μ)
       hF_meas h_bound bound_integrable h_cont
   · simp [integral, hG, continuousWithinAt_const]
@@ -454,7 +455,7 @@ theorem continuousAt_of_dominated {F : X → α → G} {x₀ : X} {bound : α 
     (h_cont : ∀ᵐ a ∂μ, ContinuousAt (fun x => F x a) x₀) :
     ContinuousAt (fun x => ∫ a, F x a ∂μ) x₀ := by
   by_cases hG : CompleteSpace G
-  · simp only [integral, hG, L1.integral]
+  · simp only [integral_eq_setToFun]
     exact continuousAt_setToFun_of_dominated (dominatedFinMeasAdditive_weightedSMul μ)
       hF_meas h_bound bound_integrable h_cont
   · simp [integral, hG, continuousAt_const]
@@ -465,7 +466,7 @@ theorem continuousOn_of_dominated {F : X → α → G} {bound : α → ℝ} {s :
     (h_cont : ∀ᵐ a ∂μ, ContinuousOn (fun x => F x a) s) :
     ContinuousOn (fun x => ∫ a, F x a ∂μ) s := by
   by_cases hG : CompleteSpace G
-  · simp only [integral, hG, L1.integral]
+  · simp only [integral_eq_setToFun]
     exact continuousOn_setToFun_of_dominated (dominatedFinMeasAdditive_weightedSMul μ)
       hF_meas h_bound bound_integrable h_cont
   · simp [integral, hG, continuousOn_const]
@@ -475,7 +476,7 @@ theorem continuous_of_dominated {F : X → α → G} {bound : α → ℝ}
     (bound_integrable : Integrable bound μ) (h_cont : ∀ᵐ a ∂μ, Continuous fun x => F x a) :
     Continuous fun x => ∫ a, F x a ∂μ := by
   by_cases hG : CompleteSpace G
-  · simp only [integral, hG, L1.integral]
+  · simp only [integral_eq_setToFun]
     exact continuous_setToFun_of_dominated (dominatedFinMeasAdditive_weightedSMul μ)
       hF_meas h_bound bound_integrable h_cont
   · simp [integral, hG, continuous_const]
@@ -560,7 +561,7 @@ theorem tendsto_integral_approxOn_of_measurable [MeasurableSpace E] [BorelSpace
     Tendsto (fun n => (SimpleFunc.approxOn f hfm s y₀ h₀ n).integral μ)
       atTop (𝓝 <| ∫ x, f x ∂μ) := by
   have hfi' := SimpleFunc.integrable_approxOn hfm hfi h₀ h₀i
-  simp only [SimpleFunc.integral_eq_integral _ (hfi' _), integral, hE, L1.integral]
+  simp only [SimpleFunc.integral_eq_integral _ (hfi' _), integral, L1.integral]
   exact tendsto_setToFun_approxOn_of_measurable (dominatedFinMeasAdditive_weightedSMul μ)
     hfi hfm hs h₀ h₀i
 
@@ -971,7 +972,7 @@ theorem norm_integral_le_of_norm_le {f : α → G} {g : α → ℝ} (hg : Integr
 @[simp]
 theorem integral_const (c : E) : ∫ _ : α, c ∂μ = μ.real univ • c := by
   by_cases hμ : IsFiniteMeasure μ
-  · simp only [integral, hE, L1.integral]
+  · simp only [integral_eq_setToFun]
     exact setToFun_const (dominatedFinMeasAdditive_weightedSMul _) _
   by_cases hc : c = 0
   · simp [hc, integral_zero]
@@ -1013,7 +1014,7 @@ theorem integral_add_measure {f : α → G} (hμ : Integrable f μ) (hν : Integ
 theorem integral_zero_measure {m : MeasurableSpace α} (f : α → G) :
     (∫ x, f x ∂(0 : Measure α)) = 0 := by
   by_cases hG : CompleteSpace G
-  · simp only [integral, hG, L1.integral]
+  · simp only [integral_eq_setToFun]
     exact setToFun_measure_zero (dominatedFinMeasAdditive_weightedSMul _) rfl
   · simp [integral, hG]
 
diff --git a/Mathlib/MeasureTheory/Integral/DominatedConvergence.lean b/Mathlib/MeasureTheory/Integral/DominatedConvergence.lean
index dd0e6832f08439..2515789dde32af 100644
--- a/Mathlib/MeasureTheory/Integral/DominatedConvergence.lean
+++ b/Mathlib/MeasureTheory/Integral/DominatedConvergence.lean
@@ -61,7 +61,7 @@ theorem tendsto_integral_of_dominated_convergence {F : ℕ → α → G} {f : α
     (h_lim : ∀ᵐ a ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))) :
     Tendsto (fun n => ∫ a, F n a ∂μ) atTop (𝓝 <| ∫ a, f a ∂μ) := by
   by_cases hG : CompleteSpace G
-  · simp only [integral, hG, L1.integral]
+  · simp only [integral_eq_setToFun]
     exact tendsto_setToFun_of_dominated_convergence (dominatedFinMeasAdditive_weightedSMul μ)
       bound F_measurable bound_integrable h_bound h_lim
   · simp [integral, hG]
@@ -73,7 +73,7 @@ theorem tendsto_integral_filter_of_dominated_convergence {ι} {l : Filter ι} [l
     (h_lim : ∀ᵐ a ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))) :
     Tendsto (fun n => ∫ a, F n a ∂μ) l (𝓝 <| ∫ a, f a ∂μ) := by
   by_cases hG : CompleteSpace G
-  · simp only [integral, hG, L1.integral]
+  · simp only [integral_eq_setToFun]
     exact tendsto_setToFun_filter_of_dominated_convergence (dominatedFinMeasAdditive_weightedSMul μ)
       bound hF_meas h_bound bound_integrable h_lim
   · simp [integral, hG, tendsto_const_nhds]
diff --git a/Mathlib/MeasureTheory/Integral/SetToL1.lean b/Mathlib/MeasureTheory/Integral/SetToL1.lean
index fb257b16c4850e..ef5286cfbd74a0 100644
--- a/Mathlib/MeasureTheory/Integral/SetToL1.lean
+++ b/Mathlib/MeasureTheory/Integral/SetToL1.lean
@@ -17,9 +17,11 @@ with finite measure, then to integrable functions, which are limits of integrabl
 
 The main result is a continuous linear map `(α →₁[μ] E) →L[ℝ] F`.
 This extension process is used to define the Bochner integral
-in the `Mathlib/MeasureTheory/Integral/Bochner/Basic.lean` file
-and the conditional expectation of an integrable function
-in `Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean`.
+in the `Mathlib/MeasureTheory/Integral/Bochner/Basic.lean` file,
+the conditional expectation of an integrable function
+in `Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean`,
+and the integral with respect to a vector measure
+in `Mathlib/MeasureTheory/VectorMeasure/Integral.lean`.
 
 ## Main definitions
 
@@ -74,7 +76,7 @@ namespace MeasureTheory
 
 variable {α E F F' G 𝕜 : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
   [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup F'] [NormedSpace ℝ F']
-  [NormedAddCommGroup G] {m : MeasurableSpace α} {μ : Measure α}
+  [NormedAddCommGroup G] {m : MeasurableSpace α} {μ μ' μ'' : Measure α}
 
 namespace L1
 
@@ -618,28 +620,34 @@ end L1
 
 section Function
 
-variable [CompleteSpace F] {T T' T'' : Set α → E →L[ℝ] F} {C C' C'' : ℝ} {f g : α → E}
+variable {T T' T'' : Set α → E →L[ℝ] F} {C C' C'' : ℝ} {f g : α → E}
 variable (μ T)
 
 open Classical in
 /-- Extend `T : Set α → E →L[ℝ] F` to `(α → E) → F` (for integrable functions `α → E`). We set it to
-0 if the function is not integrable. -/
+0 if the function is not integrable or if the target space is not complete. -/
 def setToFun (hT : DominatedFinMeasAdditive μ T C) (f : α → E) : F :=
-  if hf : Integrable f μ then L1.setToL1 hT (hf.toL1 f) else 0
+  if _hF : CompleteSpace F then
+    if hf : Integrable f μ then L1.setToL1 hT (hf.toL1 f) else 0
+  else 0
 
 variable {μ T}
 
-theorem setToFun_eq (hT : DominatedFinMeasAdditive μ T C) (hf : Integrable f μ) :
-    setToFun μ T hT f = L1.setToL1 hT (hf.toL1 f) :=
-  dif_pos hf
+theorem setToFun_eq [hF : CompleteSpace F]
+    (hT : DominatedFinMeasAdditive μ T C) (hf : Integrable f μ) :
+    setToFun μ T hT f = L1.setToL1 hT (hf.toL1 f) := by
+  simp [setToFun, hF, hf]
 
-theorem L1.setToFun_eq_setToL1 (hT : DominatedFinMeasAdditive μ T C) (f : α →₁[μ] E) :
+theorem L1.setToFun_eq_setToL1 [CompleteSpace F]
+    (hT : DominatedFinMeasAdditive μ T C) (f : α →₁[μ] E) :
     setToFun μ T hT f = L1.setToL1 hT f := by
   rw [setToFun_eq hT (L1.integrable_coeFn f), Integrable.toL1_coeFn]
 
 theorem setToFun_undef (hT : DominatedFinMeasAdditive μ T C) (hf : ¬Integrable f μ) :
-    setToFun μ T hT f = 0 :=
-  dif_neg hf
+    setToFun μ T hT f = 0 := by
+  by_cases hF : CompleteSpace F
+  · simp [setToFun, hF, hf]
+  · simp [setToFun, hF]
 
 theorem setToFun_non_aestronglyMeasurable (hT : DominatedFinMeasAdditive μ T C)
     (hf : ¬AEStronglyMeasurable f μ) : setToFun μ T hT f = 0 :=
@@ -648,6 +656,8 @@ theorem setToFun_non_aestronglyMeasurable (hT : DominatedFinMeasAdditive μ T C)
 theorem setToFun_congr_left (hT : DominatedFinMeasAdditive μ T C)
     (hT' : DominatedFinMeasAdditive μ T' C') (h : T = T') (f : α → E) :
     setToFun μ T hT f = setToFun μ T' hT' f := by
+  by_cases hF : CompleteSpace F; swap
+  · simp [setToFun, hF]
   by_cases hf : Integrable f μ
   · simp_rw [setToFun_eq _ hf, L1.setToL1_congr_left T T' hT hT' h]
   · simp_rw [setToFun_undef _ hf]
@@ -655,6 +665,8 @@ theorem setToFun_congr_left (hT : DominatedFinMeasAdditive μ T C)
 theorem setToFun_congr_left' (hT : DominatedFinMeasAdditive μ T C)
     (hT' : DominatedFinMeasAdditive μ T' C') (h : ∀ s, MeasurableSet s → μ s < ∞ → T s = T' s)
     (f : α → E) : setToFun μ T hT f = setToFun μ T' hT' f := by
+  by_cases hF : CompleteSpace F; swap
+  · simp [setToFun, hF]
   by_cases hf : Integrable f μ
   · simp_rw [setToFun_eq _ hf, L1.setToL1_congr_left' T T' hT hT' h]
   · simp_rw [setToFun_undef _ hf]
@@ -662,20 +674,28 @@ theorem setToFun_congr_left' (hT : DominatedFinMeasAdditive μ T C)
 theorem setToFun_add_left (hT : DominatedFinMeasAdditive μ T C)
     (hT' : DominatedFinMeasAdditive μ T' C') (f : α → E) :
     setToFun μ (T + T') (hT.add hT') f = setToFun μ T hT f + setToFun μ T' hT' f := by
+  by_cases hF : CompleteSpace F; swap
+  · simp [setToFun, hF]
   by_cases hf : Integrable f μ
   · simp_rw [setToFun_eq _ hf, L1.setToL1_add_left hT hT']
   · simp_rw [setToFun_undef _ hf, add_zero]
 
+/-- `setToFun` applied to the sum `T + T'` of two operators is the sum of the corresponding
+`setToFun`. See also `setToFun_add_left'` for a version varying the reference measures. -/
 theorem setToFun_add_left' (hT : DominatedFinMeasAdditive μ T C)
     (hT' : DominatedFinMeasAdditive μ T' C') (hT'' : DominatedFinMeasAdditive μ T'' C'')
     (h_add : ∀ s, MeasurableSet s → μ s < ∞ → T'' s = T s + T' s) (f : α → E) :
     setToFun μ T'' hT'' f = setToFun μ T hT f + setToFun μ T' hT' f := by
+  by_cases hF : CompleteSpace F; swap
+  · simp [setToFun, hF]
   by_cases hf : Integrable f μ
   · simp_rw [setToFun_eq _ hf, L1.setToL1_add_left' hT hT' hT'' h_add]
   · simp_rw [setToFun_undef _ hf, add_zero]
 
 theorem setToFun_smul_left (hT : DominatedFinMeasAdditive μ T C) (c : ℝ) (f : α → E) :
     setToFun μ (fun s => c • T s) (hT.smul c) f = c • setToFun μ T hT f := by
+  by_cases hF : CompleteSpace F; swap
+  · simp [setToFun, hF]
   by_cases hf : Integrable f μ
   · simp_rw [setToFun_eq _ hf, L1.setToL1_smul_left hT c]
   · simp_rw [setToFun_undef _ hf, smul_zero]
@@ -684,12 +704,16 @@ theorem setToFun_smul_left' (hT : DominatedFinMeasAdditive μ T C)
     (hT' : DominatedFinMeasAdditive μ T' C') (c : ℝ)
     (h_smul : ∀ s, MeasurableSet s → μ s < ∞ → T' s = c • T s) (f : α → E) :
     setToFun μ T' hT' f = c • setToFun μ T hT f := by
+  by_cases hF : CompleteSpace F; swap
+  · simp [setToFun, hF]
   by_cases hf : Integrable f μ
   · simp_rw [setToFun_eq _ hf, L1.setToL1_smul_left' hT hT' c h_smul]
   · simp_rw [setToFun_undef _ hf, smul_zero]
 
 @[simp]
 theorem setToFun_zero (hT : DominatedFinMeasAdditive μ T C) : setToFun μ T hT (0 : α → E) = 0 := by
+  by_cases hF : CompleteSpace F; swap
+  · simp [setToFun, hF]
   rw [Pi.zero_def, setToFun_eq hT (integrable_zero _ _ _)]
   simp only [← Pi.zero_def]
   rw [Integrable.toL1_zero, map_zero]
@@ -697,18 +721,24 @@ theorem setToFun_zero (hT : DominatedFinMeasAdditive μ T C) : setToFun μ T hT
 @[simp]
 theorem setToFun_zero_left {hT : DominatedFinMeasAdditive μ (0 : Set α → E →L[ℝ] F) C} :
     setToFun μ 0 hT f = 0 := by
+  by_cases hF : CompleteSpace F; swap
+  · simp [setToFun, hF]
   by_cases hf : Integrable f μ
   · rw [setToFun_eq hT hf]; exact L1.setToL1_zero_left hT _
   · exact setToFun_undef hT hf
 
 theorem setToFun_zero_left' (hT : DominatedFinMeasAdditive μ T C)
     (h_zero : ∀ s, MeasurableSet s → μ s < ∞ → T s = 0) : setToFun μ T hT f = 0 := by
+  by_cases hF : CompleteSpace F; swap
+  · simp [setToFun, hF]
   by_cases hf : Integrable f μ
   · rw [setToFun_eq hT hf]; exact L1.setToL1_zero_left' hT h_zero _
   · exact setToFun_undef hT hf
 
 theorem setToFun_add (hT : DominatedFinMeasAdditive μ T C) (hf : Integrable f μ)
     (hg : Integrable g μ) : setToFun μ T hT (f + g) = setToFun μ T hT f + setToFun μ T hT g := by
+  by_cases hF : CompleteSpace F; swap
+  · simp [setToFun, hF]
   rw [setToFun_eq hT (hf.add hg), setToFun_eq hT hf, setToFun_eq hT hg, Integrable.toL1_add,
     (L1.setToL1 hT).map_add]
 
@@ -738,6 +768,8 @@ theorem setToFun_finsetSum (hT : DominatedFinMeasAdditive μ T C) {ι} (s : Fins
 
 theorem setToFun_neg (hT : DominatedFinMeasAdditive μ T C) (f : α → E) :
     setToFun μ T hT (-f) = -setToFun μ T hT f := by
+  by_cases hF : CompleteSpace F; swap
+  · simp [setToFun, hF]
   by_cases hf : Integrable f μ
   · rw [setToFun_eq hT hf, setToFun_eq hT hf.neg, Integrable.toL1_neg,
       (L1.setToL1 hT).map_neg]
@@ -752,6 +784,8 @@ theorem setToFun_smul [NormedDivisionRing 𝕜] [Module 𝕜 E] [NormSMulClass 
     [Module 𝕜 F] [NormSMulClass 𝕜 F]
     (hT : DominatedFinMeasAdditive μ T C) (h_smul : ∀ c : 𝕜, ∀ s x, T s (c • x) = c • T s x) (c : 𝕜)
     (f : α → E) : setToFun μ T hT (c • f) = c • setToFun μ T hT f := by
+  by_cases hF : CompleteSpace F; swap
+  · simp [setToFun, hF]
   by_cases hf : Integrable f μ
   · rw [setToFun_eq hT hf, setToFun_eq hT (hf.smul c), Integrable.toL1_smul' f hf,
       L1.setToL1_smul hT h_smul c]
@@ -762,6 +796,8 @@ theorem setToFun_smul [NormedDivisionRing 𝕜] [Module 𝕜 E] [NormSMulClass 
 
 theorem setToFun_congr_ae (hT : DominatedFinMeasAdditive μ T C) (h : f =ᵐ[μ] g) :
     setToFun μ T hT f = setToFun μ T hT g := by
+  by_cases hF : CompleteSpace F; swap
+  · simp [setToFun, hF]
   by_cases hfi : Integrable f μ
   · have hgi : Integrable g μ := hfi.congr h
     rw [setToFun_eq hT hfi, setToFun_eq hT hgi, (Integrable.toL1_eq_toL1_iff f g hfi hgi).2 h]
@@ -781,30 +817,43 @@ theorem setToFun_toL1 (hT : DominatedFinMeasAdditive μ T C) (hf : Integrable f
     setToFun μ T hT (hf.toL1 f) = setToFun μ T hT f :=
   setToFun_congr_ae hT hf.coeFn_toL1
 
-theorem setToFun_indicator_const (hT : DominatedFinMeasAdditive μ T C) {s : Set α}
+theorem setToFun_indicator_const [CompleteSpace F] (hT : DominatedFinMeasAdditive μ T C) {s : Set α}
     (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x : E) :
     setToFun μ T hT (s.indicator fun _ => x) = T s x := by
   rw [setToFun_congr_ae hT (@indicatorConstLp_coeFn _ _ _ 1 _ _ _ hs hμs x).symm]
   rw [L1.setToFun_eq_setToL1 hT]
   exact L1.setToL1_indicatorConstLp hT hs hμs x
 
-theorem setToFun_const [IsFiniteMeasure μ] (hT : DominatedFinMeasAdditive μ T C) (x : E) :
+theorem setToFun_const [CompleteSpace F] [IsFiniteMeasure μ]
+    (hT : DominatedFinMeasAdditive μ T C) (x : E) :
     (setToFun μ T hT fun _ => x) = T univ x := by
   have : (fun _ : α => x) = Set.indicator univ fun _ => x := (indicator_univ _).symm
   rw [this]
   exact setToFun_indicator_const hT MeasurableSet.univ (measure_ne_top _ _) x
 
+theorem setToFun_simpleFunc [CompleteSpace F] (hT : DominatedFinMeasAdditive μ T C)
+    (f : SimpleFunc α E) (hf : Integrable f μ) :
+    setToFun μ T hT f = ∑ x ∈ f.range, T (f ⁻¹' {x}) x := by
+  have h'f : MemLp f 1 μ := memLp_one_iff_integrable.mpr hf
+  let g := f.toLp h'f
+  have A : f =ᵐ[μ] g := h'f.coeFn_toLp.symm
+  rw [setToFun_congr_ae hT A, L1.setToFun_eq_setToL1 hT, L1.setToL1_eq_setToL1SCLM]
+  apply (SimpleFunc.setToSimpleFunc_congr T (fun s ↦ hT.eq_zero_of_measure_zero) hT.1 hf _).symm
+  grw [A, Lp.simpleFunc.toSimpleFunc_eq_toFun]
+
 section Order
 
 variable {G' G'' : Type*}
   [NormedAddCommGroup G''] [PartialOrder G''] [IsOrderedAddMonoid G'']
-  [NormedSpace ℝ G''] [CompleteSpace G'']
+  [NormedSpace ℝ G'']
   [NormedAddCommGroup G'] [PartialOrder G'] [NormedSpace ℝ G']
 
 theorem setToFun_mono_left' [OrderClosedTopology G''] {T T' : Set α → E →L[ℝ] G''} {C C' : ℝ}
     (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C')
     (hTT' : ∀ s, MeasurableSet s → μ s < ∞ → ∀ x, T s x ≤ T' s x) (f : α → E) :
     setToFun μ T hT f ≤ setToFun μ T' hT' f := by
+  by_cases hG'' : CompleteSpace G''; swap
+  · simp [setToFun, hG'']
   by_cases hf : Integrable f μ
   · simp_rw [setToFun_eq _ hf]; exact L1.setToL1_mono_left' hT hT' hTT' _
   · simp_rw [setToFun_undef _ hf, le_rfl]
@@ -818,6 +867,8 @@ theorem setToFun_nonneg [ClosedIciTopology G''] {T : Set α → G' →L[ℝ] G''
     (hT : DominatedFinMeasAdditive μ T C)
     (hT_nonneg : ∀ s, MeasurableSet s → μ s < ∞ → ∀ x, 0 ≤ x → 0 ≤ T s x) {f : α → G'}
     (hf : 0 ≤ᵐ[μ] f) : 0 ≤ setToFun μ T hT f := by
+  by_cases hG'' : CompleteSpace G''; swap
+  · simp [setToFun, hG'']
   by_cases hfi : Integrable f μ
   · simp_rw [setToFun_eq _ hfi]
     exact L1.setToL1_nonneg hT hT_nonneg hf
@@ -838,32 +889,43 @@ end Order
 @[continuity]
 theorem continuous_setToFun (hT : DominatedFinMeasAdditive μ T C) :
     Continuous fun f : α →₁[μ] E => setToFun μ T hT f := by
+  by_cases hF : CompleteSpace F; swap
+  · simp [setToFun, hF, continuous_const]
   simp_rw [L1.setToFun_eq_setToL1 hT]; exact ContinuousLinearMap.continuous _
 
 /-- If `F i → f` in `L1`, then `setToFun μ T hT (F i) → setToFun μ T hT f`. -/
 theorem tendsto_setToFun_of_L1 (hT : DominatedFinMeasAdditive μ T C) {ι} (f : α → E)
-    (hfi : Integrable f μ) {fs : ι → α → E} {l : Filter ι} (hfsi : ∀ᶠ i in l, Integrable (fs i) μ)
+    (hf : AEStronglyMeasurable f μ) {fs : ι → α → E} {l : Filter ι}
+    (hfsi : ∀ᶠ i in l, Integrable (fs i) μ)
     (hfs : Tendsto (fun i => ∫⁻ x, ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)) :
     Tendsto (fun i => setToFun μ T hT (fs i)) l (𝓝 <| setToFun μ T hT f) := by
   classical
-    let f_lp := hfi.toL1 f
-    let F_lp i := if hFi : Integrable (fs i) μ then hFi.toL1 (fs i) else 0
-    have tendsto_L1 : Tendsto F_lp l (𝓝 f_lp) := by
-      rw [Lp.tendsto_Lp_iff_tendsto_eLpNorm']
-      simp_rw [eLpNorm_one_eq_lintegral_enorm, Pi.sub_apply]
-      refine (tendsto_congr' ?_).mp hfs
-      filter_upwards [hfsi] with i hi
-      refine lintegral_congr_ae ?_
-      filter_upwards [hi.coeFn_toL1, hfi.coeFn_toL1] with x hxi hxf
-      simp_rw [F_lp, dif_pos hi, hxi, f_lp, hxf]
-    suffices Tendsto (fun i => setToFun μ T hT (F_lp i)) l (𝓝 (setToFun μ T hT f)) by
-      refine (tendsto_congr' ?_).mp this
-      filter_upwards [hfsi] with i hi
-      suffices h_ae_eq : F_lp i =ᵐ[μ] fs i from setToFun_congr_ae hT h_ae_eq
-      simp_rw [F_lp, dif_pos hi]
-      exact hi.coeFn_toL1
-    rw [setToFun_congr_ae hT hfi.coeFn_toL1.symm]
-    exact ((continuous_setToFun hT).tendsto f_lp).comp tendsto_L1
+  rcases eq_or_neBot l with rfl | hl
+  · simp
+  have hfi : Integrable f μ := by
+    obtain ⟨i, hi, h'i⟩ : ∃ i, ∫⁻ x, ‖fs i x - f x‖ₑ ∂μ < 1 ∧ Integrable (fs i) μ :=
+      (((tendsto_order.1 hfs).2 _ zero_lt_one).and hfsi).exists
+    have : Integrable (fs i - f) μ := ⟨h'i.aestronglyMeasurable.sub hf, hi.trans one_lt_top⟩
+    convert h'i.sub this
+    abel
+  let f_lp := hfi.toL1 f
+  let F_lp i := if hFi : Integrable (fs i) μ then hFi.toL1 (fs i) else 0
+  have tendsto_L1 : Tendsto F_lp l (𝓝 f_lp) := by
+    rw [Lp.tendsto_Lp_iff_tendsto_eLpNorm']
+    simp_rw [eLpNorm_one_eq_lintegral_enorm, Pi.sub_apply]
+    refine (tendsto_congr' ?_).mp hfs
+    filter_upwards [hfsi] with i hi
+    refine lintegral_congr_ae ?_
+    filter_upwards [hi.coeFn_toL1, hfi.coeFn_toL1] with x hxi hxf
+    simp_rw [F_lp, dif_pos hi, hxi, f_lp, hxf]
+  suffices Tendsto (fun i => setToFun μ T hT (F_lp i)) l (𝓝 (setToFun μ T hT f)) by
+    refine (tendsto_congr' ?_).mp this
+    filter_upwards [hfsi] with i hi
+    suffices h_ae_eq : F_lp i =ᵐ[μ] fs i from setToFun_congr_ae hT h_ae_eq
+    simp_rw [F_lp, dif_pos hi]
+    exact hi.coeFn_toL1
+  rw [setToFun_congr_ae hT hfi.coeFn_toL1.symm]
+  exact ((continuous_setToFun hT).tendsto f_lp).comp tendsto_L1
 
 theorem tendsto_setToFun_approxOn_of_measurable (hT : DominatedFinMeasAdditive μ T C)
     [MeasurableSpace E] [BorelSpace E] {f : α → E} {s : Set E} [SeparableSpace s]
@@ -871,7 +933,7 @@ theorem tendsto_setToFun_approxOn_of_measurable (hT : DominatedFinMeasAdditive 
     (h₀ : y₀ ∈ s) (h₀i : Integrable (fun _ => y₀) μ) :
     Tendsto (fun n => setToFun μ T hT (SimpleFunc.approxOn f hfm s y₀ h₀ n)) atTop
       (𝓝 <| setToFun μ T hT f) :=
-  tendsto_setToFun_of_L1 hT _ hfi
+  tendsto_setToFun_of_L1 hT _ hfi.aestronglyMeasurable
     (Eventually.of_forall (SimpleFunc.integrable_approxOn hfm hfi h₀ h₀i))
     (SimpleFunc.tendsto_approxOn_L1_enorm hfm _ hs (hfi.sub h₀i).2)
 
@@ -884,6 +946,52 @@ theorem tendsto_setToFun_approxOn_of_measurable_of_range_subset
   refine tendsto_setToFun_approxOn_of_measurable hT hf fmeas ?_ _ (integrable_zero _ _ _)
   exact Eventually.of_forall fun x => subset_closure (hs (Set.mem_union_left _ (mem_range_self _)))
 
+theorem setToFun_of_le_map_of_stronglyMeasurable
+    (hT : DominatedFinMeasAdditive μ T C) {β : Type*} {_ : MeasurableSpace β}
+    {μ' : Measure β} {φ : α → β} {T' : Set β → E →L[ℝ] F} (hT' : DominatedFinMeasAdditive μ' T' C')
+    {f : β → E} (hf : Integrable (f ∘ φ) μ) (hfm : StronglyMeasurable f) (hφ : Measurable φ)
+    (hμ' : μ' ≤ μ.map φ)
+    (h : ∀ (s : Set β) (x : E), MeasurableSet s → T' s x = T (φ ⁻¹' s) x) :
+    setToFun μ' T' hT' f = setToFun μ T hT (f ∘ φ) := by
+  by_cases hF : CompleteSpace F; swap
+  · simp [setToFun, hF]
+  have hfi' : Integrable f μ' :=
+    ((integrable_map_measure hfm.aestronglyMeasurable hφ.aemeasurable).2 hf).mono_measure hμ'
+  borelize E
+  have : SeparableSpace (range f ∪ {0} : Set E) := hfm.separableSpace_range_union_singleton
+  refine tendsto_nhds_unique
+    (tendsto_setToFun_approxOn_of_measurable_of_range_subset
+      hT' hfm.measurable hfi' _ Subset.rfl) ?_
+  convert tendsto_setToFun_approxOn_of_measurable_of_range_subset
+    hT (hfm.measurable.comp hφ) hf (range f ∪ {0})
+    (union_subset_union_left {0} (range_comp_subset_range φ f)) using 1
+  ext i : 1
+  rw [setToFun_simpleFunc _ _ (SimpleFunc.integrable_approxOn_range _ hfi' _),
+    setToFun_simpleFunc, SimpleFunc.approxOn_comp hfm.measurable hφ]; swap
+  · apply SimpleFunc.integrable_approxOn _ hf (by simp) (by simp)
+  simp only [union_singleton, SimpleFunc.measurableSet_preimage, h, ← preimage_comp,
+    SimpleFunc.coe_comp]
+  refine (Finset.sum_subset (SimpleFunc.range_comp_subset_range _ hφ) fun y _ hy => ?_).symm
+  rw [SimpleFunc.mem_range, ← Set.preimage_singleton_eq_empty, SimpleFunc.coe_comp] at hy
+  simp [hy, hT.1.map_empty_eq_zero]
+
+theorem setToFun_of_le_map
+    (hT : DominatedFinMeasAdditive μ T C) {β : Type*} {_ : MeasurableSpace β}
+    {μ' : Measure β} {φ : α → β} {T' : Set β → E →L[ℝ] F} (hT' : DominatedFinMeasAdditive μ' T' C')
+    {f : β → E} (hf : Integrable (f ∘ φ) μ) (hfm : AEStronglyMeasurable f (μ.map φ))
+    (hφ : Measurable φ) (hμ' : μ' ≤ μ.map φ)
+    (h : ∀ (s : Set β) (x : E), MeasurableSet s → T' s x = T (φ ⁻¹' s) x) :
+    setToFun μ' T' hT' f = setToFun μ T hT (f ∘ φ) := by
+  let g := hfm.mk
+  have A : setToFun μ' T' hT' f = setToFun μ' T' hT' g :=
+    setToFun_congr_ae _ (ae_mono hμ' hfm.ae_eq_mk)
+  have B : setToFun μ T hT (f ∘ φ) = setToFun μ T hT (g ∘ φ) := by
+    apply setToFun_congr_ae
+    exact ae_of_ae_map hφ.aemeasurable hfm.ae_eq_mk
+  rw [A, B]
+  exact setToFun_of_le_map_of_stronglyMeasurable _ _
+    (hf.congr (ae_of_ae_map hφ.aemeasurable hfm.ae_eq_mk)) hfm.stronglyMeasurable_mk hφ hμ' h
+
 /-- Auxiliary lemma for `setToFun_congr_measure`: the function sending `f : α →₁[μ] G` to
 `f : α →₁[μ'] G` is continuous when `μ' ≤ c' • μ` for `c' ≠ ∞`. -/
 theorem continuous_L1_toL1 {μ' : Measure α} (c' : ℝ≥0∞) (hc' : c' ≠ ∞) (hμ'_le : μ' ≤ c' • μ) :
@@ -928,6 +1036,8 @@ theorem setToFun_congr_measure_of_integrable {μ' : Measure α} (c' : ℝ≥0∞
     (hμ'_le : μ' ≤ c' • μ) (hT : DominatedFinMeasAdditive μ T C)
     (hT' : DominatedFinMeasAdditive μ' T C') (f : α → E) (hfμ : Integrable f μ) :
     setToFun μ T hT f = setToFun μ' T hT' f := by
+  by_cases hF : CompleteSpace F; swap
+  · simp [setToFun, hF]
   -- integrability for `μ` implies integrability for `μ'`.
   have h_int : ∀ g : α → E, Integrable g μ → Integrable g μ' := fun g hg =>
     Integrable.of_measure_le_smul hc' hμ'_le hg
@@ -1000,21 +1110,92 @@ theorem setToFun_congr_smul_measure (c : ℝ≥0∞) (hc_ne_top : c ≠ ∞)
   · simp [hc0]
   · rw [smul_smul, ENNReal.inv_mul_cancel hc0 hc_ne_top, one_smul]
 
+theorem setToFun_congr_smul_measure' (c : ℝ≥0)
+    (hT : DominatedFinMeasAdditive μ T C) (hT_smul : DominatedFinMeasAdditive (c • μ) T C')
+    (f : α → E) : setToFun μ T hT f = setToFun (c • μ) T hT_smul f := by
+  rw! [ENNReal.smul_def]
+  apply setToFun_congr_smul_measure _ (by simp)
+
+/-- `setToFun` applied to the sum `T + T'` of two operators is the sum of the corresponding
+`setToFun`. -/
+theorem setToFun_add_left'' {hT : DominatedFinMeasAdditive μ T C}
+    {hT' : DominatedFinMeasAdditive μ' T' C'} {hT'' : DominatedFinMeasAdditive μ'' T'' C''}
+    (h : ∀ s, MeasurableSet s → (μ + μ') s < ∞ → T'' s = T s + T' s)
+    (hf : Integrable f μ) (hf' : Integrable f μ') (hμ : μ'' ≤ μ + μ')
+    (hC : 0 ≤ C) (hC' : 0 ≤ C') (hC'' : 0 ≤ C'') :
+    setToFun μ'' T'' hT'' f = setToFun μ T hT f + setToFun μ' T' hT' f := by
+  have I : DominatedFinMeasAdditive (μ + μ') T C := .add_measure_right _ _ hT hC
+  have A : setToFun (μ + μ') T I f = setToFun μ T hT f :=
+    setToFun_congr_measure_of_add_right _ _ _ (hf.add_measure hf')
+  have I' : DominatedFinMeasAdditive (μ + μ') T' C' := .add_measure_left _ _ hT' hC'
+  have A' : setToFun (μ + μ') T' I' f = setToFun μ' T' hT' f :=
+    setToFun_congr_measure_of_add_left _ _ _ (hf.add_measure hf')
+  have I'' : DominatedFinMeasAdditive (μ + μ') T'' C'' := .of_measure_le hμ hT'' hC''
+  have A'' : setToFun (μ + μ') T'' I'' f = setToFun μ'' T'' hT'' f := by
+    apply setToFun_congr_measure_of_integrable (c' := 1) (by simp) (by simpa using hμ)
+    apply hf.add_measure hf'
+  rw [← A, ← A', ← A'']
+  apply setToFun_add_left' _ _ _ h
+
 theorem norm_setToFun_le_mul_norm (hT : DominatedFinMeasAdditive μ T C) (f : α →₁[μ] E)
     (hC : 0 ≤ C) : ‖setToFun μ T hT f‖ ≤ C * ‖f‖ := by
-  rw [L1.setToFun_eq_setToL1]; exact L1.norm_setToL1_le_mul_norm hT hC f
+  by_cases hF : CompleteSpace F; swap
+  · simp only [setToFun, hF, ↓reduceDIte, norm_zero]
+    positivity
+  rw [L1.setToFun_eq_setToL1]
+  exact L1.norm_setToL1_le_mul_norm hT hC f
 
 theorem norm_setToFun_le_mul_norm' (hT : DominatedFinMeasAdditive μ T C) (f : α →₁[μ] E) :
     ‖setToFun μ T hT f‖ ≤ max C 0 * ‖f‖ := by
-  rw [L1.setToFun_eq_setToL1]; exact L1.norm_setToL1_le_mul_norm' hT f
+  by_cases hF : CompleteSpace F; swap
+  · simp only [setToFun, hF, ↓reduceDIte, norm_zero]
+    positivity
+  rw [L1.setToFun_eq_setToL1]
+  exact L1.norm_setToL1_le_mul_norm' hT f
 
 theorem norm_setToFun_le (hT : DominatedFinMeasAdditive μ T C) (hf : Integrable f μ) (hC : 0 ≤ C) :
     ‖setToFun μ T hT f‖ ≤ C * ‖hf.toL1 f‖ := by
-  rw [setToFun_eq hT hf]; exact L1.norm_setToL1_le_mul_norm hT hC _
+  by_cases hF : CompleteSpace F; swap
+  · simp only [setToFun, hF, ↓reduceDIte, norm_zero]
+    positivity
+  rw [setToFun_eq hT hf]
+  exact L1.norm_setToL1_le_mul_norm hT hC _
 
 theorem norm_setToFun_le' (hT : DominatedFinMeasAdditive μ T C) (hf : Integrable f μ) :
     ‖setToFun μ T hT f‖ ≤ max C 0 * ‖hf.toL1 f‖ := by
-  rw [setToFun_eq hT hf]; exact L1.norm_setToL1_le_mul_norm' hT _
+  by_cases hF : CompleteSpace F; swap
+  · simp only [setToFun, hF, ↓reduceDIte, norm_zero]
+    positivity
+  rw [setToFun_eq hT hf]
+  exact L1.norm_setToL1_le_mul_norm' hT _
+
+theorem enorm_setToFun_le (hT : DominatedFinMeasAdditive μ T C) (hC : 0 ≤ C) :
+    ‖setToFun μ T hT f‖ₑ ≤ NNReal.mk C hC * ∫⁻ x, ‖f x‖ₑ ∂μ := by
+  by_cases hF : CompleteSpace F; swap
+  · simp [setToFun, hF]
+  by_cases hf : Integrable f μ; swap
+  · simp [setToFun_undef _ hf]
+  apply (ENNReal.toReal_le_toReal (by simp)
+    (ENNReal.mul_ne_top (by simp) hf.hasFiniteIntegral.ne)).1
+  simp only [toReal_enorm, toReal_mul, coe_toReal, NNReal.coe_mk]
+  apply (norm_setToFun_le hT hf hC).trans
+  gcongr
+  apply le_of_eq
+  rw [Integrable.norm_toL1_eq_lintegral_enorm]
+
+theorem norm_setToFun_le_toReal (hT : DominatedFinMeasAdditive μ T C) (hC : 0 ≤ C) :
+    ‖setToFun μ T hT f‖ ≤ NNReal.mk C hC * ENNReal.toReal (∫⁻ a, ENNReal.ofReal ‖f a‖ ∂μ) := by
+  by_cases hF : CompleteSpace F; swap
+  · simp only [setToFun, hF, ↓reduceDIte, norm_zero, NNReal.coe_mk, ofReal_norm]
+    positivity
+  by_cases hf : Integrable f μ; swap
+  · simp only [setToFun_undef _ hf, norm_zero, NNReal.coe_mk, ofReal_norm]
+    positivity
+  apply (norm_setToFun_le hT hf hC).trans
+  gcongr
+  · simp
+  rw [Integrable.norm_toL1_eq_lintegral_enorm]
+  simp
 
 /-- Lebesgue dominated convergence theorem provides sufficient conditions under which almost
   everywhere convergence of a sequence of functions implies the convergence of their image by
@@ -1028,6 +1209,8 @@ theorem tendsto_setToFun_of_dominated_convergence (hT : DominatedFinMeasAdditive
     (h_bound : ∀ n, ∀ᵐ a ∂μ, ‖fs n a‖ ≤ bound a)
     (h_lim : ∀ᵐ a ∂μ, Tendsto (fun n => fs n a) atTop (𝓝 (f a))) :
     Tendsto (fun n => setToFun μ T hT (fs n)) atTop (𝓝 <| setToFun μ T hT f) := by
+  by_cases hF : CompleteSpace F; swap
+  · simp [setToFun, hF]
   -- `f` is a.e.-measurable, since it is the a.e.-pointwise limit of a.e.-measurable functions.
   have f_measurable : AEStronglyMeasurable f μ :=
     aestronglyMeasurable_of_tendsto_ae _ fs_measurable h_lim