awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst : Countable ι
μ : Measure X
inst_1 : NormedAddCommGroup E
f : X → E
s : ι → Set X
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X) in s i, ‖f x‖ ∂μ
B : ∀ (i : ι), ∫⁻ (a : X) in s i, (↑‖f a‖₊ : ℝ≥0∞) ∂μ = ENNReal.ofReal (∫ (a : X) in s i, (↑‖f a‖₊ : ℝ) ∂μ)
S' : Summable (α := ℝ≥0) fun (i : ι) ↦ NNReal.mk (∫ (x : X) in s i, (↑‖f x‖₊ : ℝ) ∂μ) ⋯
⊢ ∑' (a : ι), (↑(NNReal.mk (∫ (x : X) in s a, (↑‖f x‖₊ : ℝ) ∂μ) ⋯) : ℝ≥0∞) =
    (↑(∑' (b : ι), NNReal.mk (∫ (x : X) in s b, (↑‖f x‖₊ : ℝ) ∂μ) ⋯) : ℝ≥0∞)

Tactic:
have S'' := ENNReal.tsum_coe_eq S'.hasSum
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst : Countable ι
μ : Measure X
inst_1 : NormedAddCommGroup E
f : X → E
s : ι → Set X
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X) in s i, ‖f x‖ ∂μ
B : ∀ (i : ι), ∫⁻ (a : X) in s i, (↑‖f a‖₊ : ℝ≥0∞) ∂μ = ENNReal.ofReal (∫ (a : X) in s i, (↑‖f a‖₊ : ℝ) ∂μ)
S' : Summable (α := ℝ≥0) fun (i : ι) ↦ NNReal.mk (∫ (x : X) in s i, (↑‖f x‖₊ : ℝ) ∂μ) ⋯
S'' :
  ∑' (a : ι), (↑(NNReal.mk (∫ (x : X) in s a, (↑‖f x‖₊ : ℝ) ∂μ) ⋯) : ℝ≥0∞) =
    (↑(∑' (b : ι), NNReal.mk (∫ (x : X) in s b, (↑‖f x‖₊ : ℝ) ∂μ) ⋯) : ℝ≥0∞)
⊢ ∑' (a : ι), ENNReal.ofReal (∫ (x : X) in s a, ‖f x‖ ∂μ) =
    ENNReal.ofReal (↑(∑' (b : ι), NNReal.mk (∫ (x : X) in s b, ‖f x‖ ∂μ) ⋯) : ℝ)

Tactic:
simp_rw [ENNReal.coe_nnreal_eq, NNReal.coe_mk, coe_nnnorm] at S''

Premises used: NNReal.coe_mk, coe_nnnorm, ENNReal.coe_nnreal_eq
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst : Countable ι
μ : Measure X
inst_1 : NormedAddCommGroup E
f : X → E
s : ι → Set X
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X) in s i, ‖f x‖ ∂μ
B : ∀ (i : ι), ∫⁻ (a : X) in s i, (↑‖f a‖₊ : ℝ≥0∞) ∂μ = ENNReal.ofReal (∫ (a : X) in s i, (↑‖f a‖₊ : ℝ) ∂μ)
S' : Summable (α := ℝ≥0) fun (i : ι) ↦ NNReal.mk (∫ (x : X) in s i, (↑‖f x‖₊ : ℝ) ∂μ) ⋯
S'' :
  ∑' (a : ι), ENNReal.ofReal (∫ (x : X) in s a, ‖f x‖ ∂μ) =
    ENNReal.ofReal (↑(∑' (b : ι), NNReal.mk (∫ (x : X) in s b, ‖f x‖ ∂μ) ⋯) : ℝ)
⊢ ENNReal.ofReal (↑(∑' (b : ι), NNReal.mk (∫ (x : X) in s b, ‖f x‖ ∂μ) ⋯) : ℝ) < ∞

Tactic:
ENNReal.ofReal_lt_top

Premises used: ENNReal.ofReal_lt_top
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst : Countable ι
μ : Measure X
inst_1 : NormedAddCommGroup E
f : X → E
s : ι → Set X
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X) in s i, ‖f x‖ ∂μ
B : ∀ (i : ι), ∫⁻ (a : X) in s i, (↑‖f a‖₊ : ℝ≥0∞) ∂μ = ENNReal.ofReal (∫ (a : X) in s i, (↑‖f a‖₊ : ℝ) ∂μ)
S' : Summable (α := ℝ≥0) fun (i : ι) ↦ NNReal.mk (∫ (x : X) in s i, (↑‖f x‖₊ : ℝ) ∂μ) ⋯
S'' :
  ∑' (a : ι), ENNReal.ofReal (∫ (x : X) in s a, ‖f x‖ ∂μ) =
    ENNReal.ofReal (↑(∑' (b : ι), NNReal.mk (∫ (x : X) in s b, ‖f x‖ ∂μ) ⋯) : ℝ)
⊢ LT.lt (α := ℝ≥0∞) (∑' (b : ι), ENNReal.ofReal (∫ (a : X) in s b, (↑‖f a‖₊ : ℝ) ∂μ)) ∞

Tactic:
convert! ENNReal.ofReal_lt_top

Premises used: ENNReal.ofReal_lt_top
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst : Countable ι
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : TopologicalSpace X
inst_3 : BorelSpace X
inst_4 : T2Space X
inst_5 : IsLocallyFiniteMeasure μ
f : C(X, E)
s : ι → Compacts X
hf : Summable (α := ℝ) fun (i : ι) ↦ ‖ContinuousMap.restrict (↑(s i) : Set X) f‖ * μ.real (↑(s i) : Set X)
⊢ IntegrableOn.{u_1, u_3} (ε := E) (⇑f : (a : X) → E) (⋃ (i : ι), (↑(s i) : Set X)) μ

Tactic:
integrableOn_iUnion_of_summable_integral_norm
      (fun i => (map_continuous f).continuousOn.integrableOn_compact (s i).isCompact)
      (.of_nonneg_of_le (fun ι => integral_nonneg fun x => norm_nonneg _) (fun i => ?_) hf)

Premises used: MeasureTheory.integral_nonneg, Continuous.continuousOn, Summable.of_nonneg_of_le, TopologicalSpace.Compacts.isCompact, MeasureTheory.integrableOn_iUnion_of_summable_integral_norm, ContinuousMapClass.map_continuous, ContinuousOn.integrableOn_compact, DFunLike.coe, norm_nonneg
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst : Countable ι
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : TopologicalSpace X
inst_3 : BorelSpace X
inst_4 : T2Space X
inst_5 : IsLocallyFiniteMeasure μ
f : C(X, E)
s : ι → Compacts X
hf : Summable (α := ℝ) fun (i : ι) ↦ ‖ContinuousMap.restrict (↑(s i) : Set X) f‖ * μ.real (↑(s i) : Set X)
i :
  ∀ (i : ι),
    ∫ (x : X) in (↑(s i) : Set X), norm.{u_3} (E := E) ((f : (a : X) → E) x : E) ∂μ ≤
      ‖ContinuousMap.restrict (↑(s i) : Set X) f‖ * μ.real (↑(s i) : Set X)
⊢ IntegrableOn.{u_1, u_3} (ε := E) (⇑f : (a : X) → E) (⋃ (i : ι), (↑(s i) : Set X)) μ

Tactic:
refine
    integrableOn_iUnion_of_summable_integral_norm
      (fun i => (map_continuous f).continuousOn.integrableOn_compact (s i).isCompact)
      (.of_nonneg_of_le (fun ι => integral_nonneg fun x => norm_nonneg _) (fun i => ?_) hf)

Premises used: MeasureTheory.integral_nonneg, Continuous.continuousOn, Summable.of_nonneg_of_le, TopologicalSpace.Compacts.isCompact, MeasureTheory.integrableOn_iUnion_of_summable_integral_norm, ContinuousMapClass.map_continuous, ContinuousOn.integrableOn_compact, DFunLike.coe, norm_nonneg
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst : Countable ι
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : TopologicalSpace X
inst_3 : BorelSpace X
inst_4 : T2Space X
inst_5 : IsLocallyFiniteMeasure μ
f : C(X, E)
s : ι → Compacts X
hf : Summable (α := ℝ) fun (i : ι) ↦ ‖ContinuousMap.restrict (↑(s i) : Set X) f‖ * μ.real (↑(s i) : Set X)
i : ι
rw :
  norm (E := ℝ) (∫ (x : X) in (↑(s i) : Set X), norm.{u_3} (E := E) ((f : (a : X) → E) x : E) ∂μ) ≤
    ‖ContinuousMap.restrict (↑(s i) : Set X) f‖ * μ.real (↑(s i) : Set X)
⊢ ∫ (x : X) in (↑(s i) : Set X), norm.{u_3} (E := E) ((f : (a : X) → E) x : E) ∂μ ≤
    ‖ContinuousMap.restrict (↑(s i) : Set X) f‖ * μ.real (↑(s i) : Set X)

Tactic:
rw [← (Real.norm_of_nonneg (integral_nonneg fun x => norm_nonneg _) : ‖_‖ = ∫ x in s i, ‖f x‖ ∂μ)]

Premises used: MeasureTheory.integral_nonneg, DFunLike.coe, norm_nonneg, Real.norm_of_nonneg
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst : Countable ι
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : TopologicalSpace X
inst_3 : BorelSpace X
inst_4 : T2Space X
inst_5 : IsLocallyFiniteMeasure μ
f : C(X, E)
s : ι → Compacts X
hf : Summable (α := ℝ) fun (i : ι) ↦ ‖ContinuousMap.restrict (↑(s i) : Set X) f‖ * μ.real (↑(s i) : Set X)
i : ι
⊢ norm (E := ℝ) (∫ (x : X) in (↑(s i) : Set X), norm.{u_3} (E := E) ((f : (a : X) → E) x : E) ∂μ) ≤
    ‖ContinuousMap.restrict (↑(s i) : Set X) f‖ * μ.real (↑(s i) : Set X)

Tactic:
norm_setIntegral_le_of_norm_le_const (s i).isCompact.measure_lt_top
      fun x hx => (norm_norm (f x)).symm ▸ (f.restrict (s i : Set X)).norm_coe_le_norm ⟨x, hx⟩

Premises used: ContinuousMap.norm_coe_le_norm, Eq.rec, MeasureTheory.norm_setIntegral_le_of_norm_le_const, norm_norm, Subtype.mk, SetLike.coe, IsCompact.measure_lt_top, TopologicalSpace.Compacts.isCompact, Eq.symm, DFunLike.coe, ContinuousMap.restrict
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst : Countable ι
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : TopologicalSpace X
inst_3 : BorelSpace X
inst_4 : T2Space X
inst_5 : IsLocallyFiniteMeasure μ
f : C(X, E)
s : ι → Compacts X
hf : Summable (α := ℝ) fun (i : ι) ↦ ‖ContinuousMap.restrict (↑(s i) : Set X) f‖ * μ.real (↑(s i) : Set X)
i : ι
⊢ norm (E := ℝ) (∫ (x : X) in (↑(s i) : Set X), norm.{u_3} (E := E) ((f : (a : X) → E) x : E) ∂μ) ≤
    ‖ContinuousMap.restrict (↑(s i) : Set X) f‖ * μ.real (↑(s i) : Set X)

Tactic:
exact
    norm_setIntegral_le_of_norm_le_const (s i).isCompact.measure_lt_top
      fun x hx => (norm_norm (f x)).symm ▸ (f.restrict (s i : Set X)).norm_coe_le_norm ⟨x, hx⟩

Premises used: MeasureTheory.norm_setIntegral_le_of_norm_le_const, IsCompact.measure_lt_top, TopologicalSpace.Compacts.isCompact
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst : Countable ι
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : TopologicalSpace X
inst_3 : BorelSpace X
inst_4 : T2Space X
inst_5 : IsLocallyFiniteMeasure μ
f : C(X, E)
s : ι → Compacts X
hf : Summable (α := ℝ) fun (i : ι) ↦ ‖ContinuousMap.restrict (↑(s i) : Set X) f‖ * μ.real (↑(s i) : Set X)
hs : Eq.{u_1 + 1} (α := Set X) (⋃ (i : ι), (↑(s i) : Set X)) univ
⊢ Integrable.{u_3, u_1} (ε := E) (⇑f : (a : X) → E) μ

Tactic:
simpa only [hs, integrableOn_univ] using integrableOn_iUnion_of_summable_norm_restrict hf

Premises used: MeasureTheory.integrableOn_iUnion_of_summable_norm_restrict, MeasureTheory.integrableOn_univ
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
h :
  (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) =ᶠ[ae (μ.restrict s)]
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) :
      X → E)
⊢ MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯ =
    MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯

Tactic:
ext1
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
⊢ (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) =ᶠ[ae (μ.restrict s)]
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) :
      X → E)

Tactic:
(ae_restrict_of_ae (Lp.coeFn_add f g)).mp ?_

Premises used: MeasureTheory.Lp.coeFn_add, Filter.EventuallyEq, MeasureTheory.ae_restrict_of_ae, Filter.Eventually.mp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
h :
  ∀ᵐ (x : X) ∂μ.restrict s,
    (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x = ((↑(↑f : X →ₘ[μ] E) : X → E) + (↑(↑g : X →ₘ[μ] E) : X → E)) x →
      (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
        (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) :
                X →ₘ[μ.restrict s] E) :
            X → E)
          x
⊢ (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) =ᶠ[ae (μ.restrict s)]
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) :
      X → E)

Tactic:
refine (ae_restrict_of_ae (Lp.coeFn_add f g)).mp ?_

Premises used: MeasureTheory.Lp.coeFn_add, MeasureTheory.ae_restrict_of_ae, Filter.Eventually.mp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
⊢ ∀ᵐ (x : X) ∂μ.restrict s,
    (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x = ((↑(↑f : X →ₘ[μ] E) : X → E) + (↑(↑g : X →ₘ[μ] E) : X → E)) x →
      (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
        (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) :
                X →ₘ[μ.restrict s] E) :
            X → E)
          x

Tactic:
(Lp.coeFn_add (MemLp.toLp f ((Lp.memLp f).restrict s))
          (MemLp.toLp g ((Lp.memLp g).restrict s))).mp ?_

Premises used: MeasureTheory.Lp.coeFn_add, MeasureTheory.Lp.memLp, MeasureTheory.AEEqFun.cast, Filter.Eventually.mp, MeasureTheory.MemLp.toLp, MeasureTheory.MemLp.restrict, Subtype.val
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
h :
  ∀ᵐ (x : X) ∂μ.restrict s,
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) :
            X → E)
          x =
        ((↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) +
            (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E))
          x →
      (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x = ((↑(↑f : X →ₘ[μ] E) : X → E) + (↑(↑g : X →ₘ[μ] E) : X → E)) x →
        (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
          (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) :
                  X →ₘ[μ.restrict s] E) :
              X → E)
            x
⊢ ∀ᵐ (x : X) ∂μ.restrict s,
    (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x = ((↑(↑f : X →ₘ[μ] E) : X → E) + (↑(↑g : X →ₘ[μ] E) : X → E)) x →
      (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
        (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) :
                X →ₘ[μ.restrict s] E) :
            X → E)
          x

Tactic:
refine
    (Lp.coeFn_add (MemLp.toLp f ((Lp.memLp f).restrict s))
          (MemLp.toLp g ((Lp.memLp g).restrict s))).mp ?_

Premises used: MeasureTheory.Lp.coeFn_add, MeasureTheory.Lp.memLp, MeasureTheory.AEEqFun.cast, Filter.Eventually.mp, MeasureTheory.MemLp.toLp, MeasureTheory.MemLp.restrict, Subtype.val
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
⊢ ∀ᵐ (x : X) ∂μ.restrict s,
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) :
            X → E)
          x =
        ((↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) +
            (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E))
          x →
      (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x = ((↑(↑f : X →ₘ[μ] E) : X → E) + (↑(↑g : X →ₘ[μ] E) : X → E)) x →
        (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
          (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) :
                  X →ₘ[μ.restrict s] E) :
              X → E)
            x

Tactic:
(MemLp.coeFn_toLp ((Lp.memLp f).restrict s)).mp ?_

Premises used: MeasureTheory.Lp.memLp, Filter.Eventually.mp, MeasureTheory.MemLp.restrict, MeasureTheory.MemLp.coeFn_toLp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
h :
  ∀ᵐ (x : X) ∂μ.restrict s,
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x = (↑(↑f : X →ₘ[μ] E) : X → E) x →
      (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) :
                  X →ₘ[μ.restrict s] E) :
              X → E)
            x =
          ((↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) +
              (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E))
            x →
        (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x = ((↑(↑f : X →ₘ[μ] E) : X → E) + (↑(↑g : X →ₘ[μ] E) : X → E)) x →
          (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
            (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) :
                    X →ₘ[μ.restrict s] E) :
                X → E)
              x
⊢ ∀ᵐ (x : X) ∂μ.restrict s,
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) :
            X → E)
          x =
        ((↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) +
            (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E))
          x →
      (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x = ((↑(↑f : X →ₘ[μ] E) : X → E) + (↑(↑g : X →ₘ[μ] E) : X → E)) x →
        (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
          (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) :
                  X →ₘ[μ.restrict s] E) :
              X → E)
            x

Tactic:
refine (MemLp.coeFn_toLp ((Lp.memLp f).restrict s)).mp ?_

Premises used: MeasureTheory.Lp.memLp, Filter.Eventually.mp, MeasureTheory.MemLp.restrict, MeasureTheory.MemLp.coeFn_toLp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
⊢ ∀ᵐ (x : X) ∂μ.restrict s,
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x = (↑(↑f : X →ₘ[μ] E) : X → E) x →
      (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) :
                  X →ₘ[μ.restrict s] E) :
              X → E)
            x =
          ((↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) +
              (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E))
            x →
        (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x = ((↑(↑f : X →ₘ[μ] E) : X → E) + (↑(↑g : X →ₘ[μ] E) : X → E)) x →
          (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
            (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) :
                    X →ₘ[μ.restrict s] E) :
                X → E)
              x

Tactic:
(MemLp.coeFn_toLp ((Lp.memLp g).restrict s)).mp ?_

Premises used: MeasureTheory.Lp.memLp, Filter.Eventually.mp, MeasureTheory.MemLp.restrict, MeasureTheory.MemLp.coeFn_toLp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
h :
  ∀ᵐ (x : X) ∂μ.restrict s,
    (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x = (↑(↑g : X →ₘ[μ] E) : X → E) x →
      (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
          (↑(↑f : X →ₘ[μ] E) : X → E) x →
        (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) :
                    X →ₘ[μ.restrict s] E) :
                X → E)
              x =
            ((↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) +
                (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E))
              x →
          (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x = ((↑(↑f : X →ₘ[μ] E) : X → E) + (↑(↑g : X →ₘ[μ] E) : X → E)) x →
            (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
              (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) :
                      X →ₘ[μ.restrict s] E) :
                  X → E)
                x
⊢ ∀ᵐ (x : X) ∂μ.restrict s,
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x = (↑(↑f : X →ₘ[μ] E) : X → E) x →
      (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) :
                  X →ₘ[μ.restrict s] E) :
              X → E)
            x =
          ((↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) +
              (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E))
            x →
        (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x = ((↑(↑f : X →ₘ[μ] E) : X → E) + (↑(↑g : X →ₘ[μ] E) : X → E)) x →
          (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
            (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) :
                    X →ₘ[μ.restrict s] E) :
                X → E)
              x

Tactic:
refine (MemLp.coeFn_toLp ((Lp.memLp g).restrict s)).mp ?_

Premises used: MeasureTheory.Lp.memLp, Filter.Eventually.mp, MeasureTheory.MemLp.restrict, MeasureTheory.MemLp.coeFn_toLp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
⊢ ∀ᵐ (x : X) ∂μ.restrict s,
    (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x = (↑(↑g : X →ₘ[μ] E) : X → E) x →
      (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
          (↑(↑f : X →ₘ[μ] E) : X → E) x →
        (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) :
                    X →ₘ[μ.restrict s] E) :
                X → E)
              x =
            ((↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) +
                (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E))
              x →
          (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x = ((↑(↑f : X →ₘ[μ] E) : X → E) + (↑(↑g : X →ₘ[μ] E) : X → E)) x →
            (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
              (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) :
                      X →ₘ[μ.restrict s] E) :
                  X → E)
                x

Tactic:
(MemLp.coeFn_toLp ((Lp.memLp (f + g)).restrict s)).mono fun x hx1 hx2 hx3 hx4 hx5 => ?_

Premises used: MeasureTheory.Lp.memLp, Filter.Eventually.mono, HAdd.hAdd, MeasureTheory.MemLp.restrict, MeasureTheory.MemLp.coeFn_toLp