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
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
h :
  ∀ (x : X)
    (hx1 :
      (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
        (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x)
    (hx2 :
      (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x = (↑(↑g : X →ₘ[μ] E) : X → E) x)
    (hx3 :
      (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x = (↑(↑f : X →ₘ[μ] E) : X → E) x)
    (hx4 :
      (↑(↑(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)
    (hx5 : (↑(↑(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 (↑(↑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:
refine (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
-- 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
hx1 :
  (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
    (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x
hx2 : (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x = (↑(↑g : X →ₘ[μ] E) : X → E) x
hx3 : (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x = (↑(↑f : X →ₘ[μ] E) : X → E) x
hx4 :
  (↑(↑(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
hx5 : (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x = ((↑(↑f : X →ₘ[μ] E) : X → E) + (↑(↑g : X →ₘ[μ] E) : X → E)) x
h :
  (↑(↑(MemLp.toLp (↑(↑(f + 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
h₁ :
  (↑(↑(f + g) : X →ₘ[μ] 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
h₂ :
  (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x =
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x +
      (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x
h₃ :
  (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x =
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x + (↑(↑g : X →ₘ[μ] E) : X → E) x
h₄ : (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x = (↑(↑f : X →ₘ[μ] E) : X → E) x + (↑(↑g : X →ₘ[μ] E) : X → E) x
h₅ :
  ((↑(↑f : X →ₘ[μ] E) : X → E) + (↑(↑g : X →ₘ[μ] E) : X → E)) x =
    (↑(↑f : X →ₘ[μ] E) : X → E) x + (↑(↑g : X →ₘ[μ] E) : X → E) x
h₆ h₇ :
  (↑(↑f : X →ₘ[μ] E) : X → E) x + (↑(↑g : X →ₘ[μ] E) : X → E) x =
    (↑(↑f : X →ₘ[μ] E) : X → E) x + (↑(↑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:
rw [hx4, hx1, Pi.add_apply, hx2, hx3, hx5, Pi.add_apply]

Premises used: Pi.add_apply
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
F : Type u_4
mX : MeasurableSpace X
𝕜 : Type u_5
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : Module 𝕜 F
inst_3 : IsBoundedSMul 𝕜 F
p : ℝ≥0∞
μ : Measure X
c : 𝕜
f : ↥(Lp F p μ)
s : Set X
h :
  (↑(↑(MemLp.toLp (↑(↑(c • f) : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) =ᶠ[ae (μ.restrict s)]
    (↑(↑(c • MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F)
⊢ MemLp.toLp (↑(↑(c • f) : X →ₘ[μ] F) : X → F) ⋯ = c • MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯

Tactic:
ext1
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
F : Type u_4
mX : MeasurableSpace X
𝕜 : Type u_5
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : Module 𝕜 F
inst_3 : IsBoundedSMul 𝕜 F
p : ℝ≥0∞
μ : Measure X
c : 𝕜
f : ↥(Lp F p μ)
s : Set X
⊢ (↑(↑(MemLp.toLp (↑(↑(c • f) : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) =ᶠ[ae (μ.restrict s)]
    (↑(↑(c • MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F)

Tactic:
(ae_restrict_of_ae (Lp.coeFn_smul c f)).mp ?_

Premises used: MeasureTheory.Lp.coeFn_smul, Filter.EventuallyEq, MeasureTheory.ae_restrict_of_ae, Filter.Eventually.mp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
F : Type u_4
mX : MeasurableSpace X
𝕜 : Type u_5
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : Module 𝕜 F
inst_3 : IsBoundedSMul 𝕜 F
p : ℝ≥0∞
μ : Measure X
c : 𝕜
f : ↥(Lp F p μ)
s : Set X
h :
  ∀ᵐ (x : X) ∂μ.restrict s,
    (↑(↑(c • f) : X →ₘ[μ] F) : X → F) x = (c • (↑(↑f : X →ₘ[μ] F) : X → F)) x →
      (↑(↑(MemLp.toLp (↑(↑(c • f) : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x =
        (↑(↑(c • MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x
⊢ (↑(↑(MemLp.toLp (↑(↑(c • f) : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) =ᶠ[ae (μ.restrict s)]
    (↑(↑(c • MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F)

Tactic:
refine (ae_restrict_of_ae (Lp.coeFn_smul c f)).mp ?_

Premises used: MeasureTheory.Lp.coeFn_smul, MeasureTheory.ae_restrict_of_ae, Filter.Eventually.mp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
F : Type u_4
mX : MeasurableSpace X
𝕜 : Type u_5
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : Module 𝕜 F
inst_3 : IsBoundedSMul 𝕜 F
p : ℝ≥0∞
μ : Measure X
c : 𝕜
f : ↥(Lp F p μ)
s : Set X
⊢ ∀ᵐ (x : X) ∂μ.restrict s,
    (↑(↑(c • f) : X →ₘ[μ] F) : X → F) x = (c • (↑(↑f : X →ₘ[μ] F) : X → F)) x →
      (↑(↑(MemLp.toLp (↑(↑(c • f) : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x =
        (↑(↑(c • MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) 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
F : Type u_4
mX : MeasurableSpace X
𝕜 : Type u_5
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : Module 𝕜 F
inst_3 : IsBoundedSMul 𝕜 F
p : ℝ≥0∞
μ : Measure X
c : 𝕜
f : ↥(Lp F p μ)
s : Set X
h :
  ∀ᵐ (x : X) ∂μ.restrict s,
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x = (↑(↑f : X →ₘ[μ] F) : X → F) x →
      (↑(↑(c • f) : X →ₘ[μ] F) : X → F) x = (c • (↑(↑f : X →ₘ[μ] F) : X → F)) x →
        (↑(↑(MemLp.toLp (↑(↑(c • f) : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x =
          (↑(↑(c • MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x
⊢ ∀ᵐ (x : X) ∂μ.restrict s,
    (↑(↑(c • f) : X →ₘ[μ] F) : X → F) x = (c • (↑(↑f : X →ₘ[μ] F) : X → F)) x →
      (↑(↑(MemLp.toLp (↑(↑(c • f) : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x =
        (↑(↑(c • MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) 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
F : Type u_4
mX : MeasurableSpace X
𝕜 : Type u_5
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : Module 𝕜 F
inst_3 : IsBoundedSMul 𝕜 F
p : ℝ≥0∞
μ : Measure X
c : 𝕜
f : ↥(Lp F p μ)
s : Set X
⊢ ∀ᵐ (x : X) ∂μ.restrict s,
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x = (↑(↑f : X →ₘ[μ] F) : X → F) x →
      (↑(↑(c • f) : X →ₘ[μ] F) : X → F) x = (c • (↑(↑f : X →ₘ[μ] F) : X → F)) x →
        (↑(↑(MemLp.toLp (↑(↑(c • f) : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x =
          (↑(↑(c • MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x

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

Premises used: MeasureTheory.Lp.memLp, Filter.Eventually.mp, MeasureTheory.MemLp.restrict, MeasureTheory.MemLp.coeFn_toLp, HSMul.hSMul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
F : Type u_4
mX : MeasurableSpace X
𝕜 : Type u_5
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : Module 𝕜 F
inst_3 : IsBoundedSMul 𝕜 F
p : ℝ≥0∞
μ : Measure X
c : 𝕜
f : ↥(Lp F p μ)
s : Set X
h :
  ∀ᵐ (x : X) ∂μ.restrict s,
    (↑(↑(MemLp.toLp (↑(↑(c • f) : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x =
        (↑(↑(c • f) : X →ₘ[μ] F) : X → F) x →
      (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x =
          (↑(↑f : X →ₘ[μ] F) : X → F) x →
        (↑(↑(c • f) : X →ₘ[μ] F) : X → F) x = (c • (↑(↑f : X →ₘ[μ] F) : X → F)) x →
          (↑(↑(MemLp.toLp (↑(↑(c • f) : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x =
            (↑(↑(c • MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x
⊢ ∀ᵐ (x : X) ∂μ.restrict s,
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x = (↑(↑f : X →ₘ[μ] F) : X → F) x →
      (↑(↑(c • f) : X →ₘ[μ] F) : X → F) x = (c • (↑(↑f : X →ₘ[μ] F) : X → F)) x →
        (↑(↑(MemLp.toLp (↑(↑(c • f) : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x =
          (↑(↑(c • MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x

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

Premises used: MeasureTheory.Lp.memLp, Filter.Eventually.mp, MeasureTheory.MemLp.restrict, MeasureTheory.MemLp.coeFn_toLp, HSMul.hSMul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
F : Type u_4
mX : MeasurableSpace X
𝕜 : Type u_5
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : Module 𝕜 F
inst_3 : IsBoundedSMul 𝕜 F
p : ℝ≥0∞
μ : Measure X
c : 𝕜
f : ↥(Lp F p μ)
s : Set X
⊢ ∀ᵐ (x : X) ∂μ.restrict s,
    (↑(↑(MemLp.toLp (↑(↑(c • f) : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x =
        (↑(↑(c • f) : X →ₘ[μ] F) : X → F) x →
      (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x =
          (↑(↑f : X →ₘ[μ] F) : X → F) x →
        (↑(↑(c • f) : X →ₘ[μ] F) : X → F) x = (c • (↑(↑f : X →ₘ[μ] F) : X → F)) x →
          (↑(↑(MemLp.toLp (↑(↑(c • f) : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x =
            (↑(↑(c • MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x

Tactic:
(Lp.coeFn_smul c (MemLp.toLp f ((Lp.memLp f).restrict s))).mono fun x hx1 hx2 hx3 hx4 => ?_

Premises used: MeasureTheory.Lp.memLp, MeasureTheory.AEEqFun.cast, MeasureTheory.Lp.coeFn_smul, Filter.Eventually.mono, MeasureTheory.MemLp.toLp, MeasureTheory.MemLp.restrict, Subtype.val
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
F : Type u_4
mX : MeasurableSpace X
𝕜 : Type u_5
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : Module 𝕜 F
inst_3 : IsBoundedSMul 𝕜 F
p : ℝ≥0∞
μ : Measure X
c : 𝕜
f : ↥(Lp F p μ)
s : Set X
h :
  ∀ (x : X)
    (hx1 :
      (↑(↑(c • MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x =
        (c • (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F)) x)
    (hx2 :
      (↑(↑(MemLp.toLp (↑(↑(c • f) : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x =
        (↑(↑(c • f) : X →ₘ[μ] F) : X → F) x)
    (hx3 :
      (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x = (↑(↑f : X →ₘ[μ] F) : X → F) x)
    (hx4 : (↑(↑(c • f) : X →ₘ[μ] F) : X → F) x = (c • (↑(↑f : X →ₘ[μ] F) : X → F)) x),
    (↑(↑(MemLp.toLp (↑(↑(c • f) : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x =
      (↑(↑(c • MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x
⊢ ∀ᵐ (x : X) ∂μ.restrict s,
    (↑(↑(MemLp.toLp (↑(↑(c • f) : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x =
        (↑(↑(c • f) : X →ₘ[μ] F) : X → F) x →
      (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x =
          (↑(↑f : X →ₘ[μ] F) : X → F) x →
        (↑(↑(c • f) : X →ₘ[μ] F) : X → F) x = (c • (↑(↑f : X →ₘ[μ] F) : X → F)) x →
          (↑(↑(MemLp.toLp (↑(↑(c • f) : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x =
            (↑(↑(c • MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x

Tactic:
refine
    (Lp.coeFn_smul c (MemLp.toLp f ((Lp.memLp f).restrict s))).mono fun x hx1 hx2 hx3 hx4 => ?_

Premises used: MeasureTheory.Lp.memLp, MeasureTheory.AEEqFun.cast, MeasureTheory.Lp.coeFn_smul, Filter.Eventually.mono, MeasureTheory.MemLp.toLp, MeasureTheory.MemLp.restrict, Subtype.val
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
F : Type u_4
mX : MeasurableSpace X
𝕜 : Type u_5
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : Module 𝕜 F
inst_3 : IsBoundedSMul 𝕜 F
p : ℝ≥0∞
μ : Measure X
c : 𝕜
f : ↥(Lp F p μ)
s : Set X
x : X
hx1 :
  (↑(↑(c • MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x =
    (c • (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F)) x
hx2 :
  (↑(↑(MemLp.toLp (↑(↑(c • f) : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x =
    (↑(↑(c • f) : X →ₘ[μ] F) : X → F) x
hx3 : (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x = (↑(↑f : X →ₘ[μ] F) : X → F) x
hx4 : (↑(↑(c • f) : X →ₘ[μ] F) : X → F) x = (c • (↑(↑f : X →ₘ[μ] F) : X → F)) x
⊢ (↑(↑(MemLp.toLp (↑(↑(c • f) : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x =
    (↑(↑(c • MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x

Tactic:
simp only [hx2, hx1, hx3, hx4, Pi.smul_apply]

Premises used: Pi.smul_apply
-- 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
s : Set X
f : ↥(Lp E p μ)
rw : (eLpNorm (↑(↑f : X →ₘ[μ] E) : X → E) p (μ.restrict s)).toReal ≤ (eLpNorm (↑(↑f : X →ₘ[μ] E) : X → E) p μ).toReal
⊢ ‖MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯‖ ≤ ‖f‖

Tactic:
rw [Lp.norm_def, Lp.norm_def, eLpNorm_congr_ae (MemLp.coeFn_toLp _)]

Premises used: MeasureTheory.MemLp.coeFn_toLp, MeasureTheory.eLpNorm_congr_ae, MeasureTheory.Lp.norm_def
-- 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
s : Set X
f : ↥(Lp E p μ)
⊢ (eLpNorm (↑(↑f : X →ₘ[μ] E) : X → E) p (μ.restrict s)).toReal ≤ (eLpNorm (↑(↑f : X →ₘ[μ] E) : X → E) p μ).toReal

Tactic:
ENNReal.toReal_mono (Lp.eLpNorm_ne_top _) ?_

Premises used: ENNReal.toReal_mono, MeasureTheory.Lp.eLpNorm_ne_top
-- 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
s : Set X
f : ↥(Lp E p μ)
refine : eLpNorm (↑(↑f : X →ₘ[μ] E) : X → E) p (μ.restrict s) ≤ eLpNorm (↑(↑f : X →ₘ[μ] E) : X → E) p μ
⊢ (eLpNorm (↑(↑f : X →ₘ[μ] E) : X → E) p (μ.restrict s)).toReal ≤ (eLpNorm (↑(↑f : X →ₘ[μ] E) : X → E) p μ).toReal

Tactic:
refine ENNReal.toReal_mono (Lp.eLpNorm_ne_top _) ?_

Premises used: ENNReal.toReal_mono, MeasureTheory.Lp.eLpNorm_ne_top
-- 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
s : Set X
f : ↥(Lp E p μ)
⊢ eLpNorm (↑(↑f : X →ₘ[μ] E) : X → E) p (μ.restrict s) ≤ eLpNorm (↑(↑f : X →ₘ[μ] E) : X → E) p μ

Tactic:
eLpNorm_mono_measure _ Measure.restrict_le_self

Premises used: MeasureTheory.Measure.restrict_le_self, MeasureTheory.eLpNorm_mono_measure
-- 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
s : Set X
f : ↥(Lp E p μ)
⊢ eLpNorm (↑(↑f : X →ₘ[μ] E) : X → E) p (μ.restrict s) ≤ eLpNorm (↑(↑f : X →ₘ[μ] E) : X → E) p μ

Tactic:
exact eLpNorm_mono_measure _ Measure.restrict_le_self

Premises used: MeasureTheory.Measure.restrict_le_self, MeasureTheory.eLpNorm_mono_measure
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
Y : Type u_2
E : Type u_3
F : Type u_4
mX : MeasurableSpace X
inst : NormedAddCommGroup E
𝕜 : Type u_5
inst_1 : NormedRing 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : Module 𝕜 F
inst_4 : IsBoundedSMul 𝕜 F
p_1 : ℝ≥0∞
μ_1 μ : Measure X
p : ℝ≥0∞
hp : Fact (1 ≤ p)
s : Set X
f : ↥(Lp F p μ)
rw :
  norm (E := ↥(Lp F p (μ.restrict s)))
      (({ toFun := fun (f : ↥(Lp F p μ)) ↦ MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯, map_add' := ⋯, map_smul' := ⋯ :
              ↥(Lp F p μ) →ₗ[𝕜] ↥(Lp F p (μ.restrict s)) } :
            (a : ↥(Lp F p μ)) → ↥(Lp F p (μ.restrict s)))
          f :
        ↥(Lp F p (μ.restrict s))) ≤
    ‖f‖
⊢ norm (E := ↥(Lp F p (μ.restrict s)))
      (({ toFun := fun (f : ↥(Lp F p μ)) ↦ MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯, map_add' := ⋯, map_smul' := ⋯ :
              ↥(Lp F p μ) →ₗ[𝕜] ↥(Lp F p (μ.restrict s)) } :
            (a : ↥(Lp F p μ)) → ↥(Lp F p (μ.restrict s)))
          f :
        ↥(Lp F p (μ.restrict s))) ≤
    1 * ‖f‖

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
Y : Type u_2
E : Type u_3
F : Type u_4
mX : MeasurableSpace X
inst : NormedAddCommGroup E
𝕜 : Type u_5
inst_1 : NormedRing 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : Module 𝕜 F
inst_4 : IsBoundedSMul 𝕜 F
p_1 : ℝ≥0∞
μ_1 μ : Measure X
p : ℝ≥0∞
hp : Fact (1 ≤ p)
s : Set X
f : ↥(Lp F p μ)
⊢ norm (E := ↥(Lp F p (μ.restrict s)))
      (({ toFun := fun (f : ↥(Lp F p μ)) ↦ MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯, map_add' := ⋯, map_smul' := ⋯ :
              ↥(Lp F p μ) →ₗ[𝕜] ↥(Lp F p (μ.restrict s)) } :
            (a : ↥(Lp F p μ)) → ↥(Lp F p (μ.restrict s)))
          f :
        ↥(Lp F p (μ.restrict s))) ≤
    ‖f‖

Tactic:
norm_Lp_toLp_restrict_le s f

Premises used: ENNReal.toReal, MeasureTheory.norm_Lp_toLp_restrict_le, NNReal.toReal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
Y : Type u_2
E : Type u_3
F : Type u_4
mX : MeasurableSpace X
inst : NormedAddCommGroup E
𝕜 : Type u_5
inst_1 : NormedRing 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : Module 𝕜 F
inst_4 : IsBoundedSMul 𝕜 F
p_1 : ℝ≥0∞
μ_1 μ : Measure X
p : ℝ≥0∞
hp : Fact (1 ≤ p)
s : Set X
f : ↥(Lp F p μ)
⊢ norm (E := ↥(Lp F p (μ.restrict s)))
      (({ toFun := fun (f : ↥(Lp F p μ)) ↦ MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯, map_add' := ⋯, map_smul' := ⋯ :
              ↥(Lp F p μ) →ₗ[𝕜] ↥(Lp F p (μ.restrict s)) } :
            (a : ↥(Lp F p μ)) → ↥(Lp F p (μ.restrict s)))
          f :
        ↥(Lp F p (μ.restrict s))) ≤
    ‖f‖

Tactic:
exact norm_Lp_toLp_restrict_le s f

Premises used: MeasureTheory.norm_Lp_toLp_restrict_le
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
F : Type u_4
mX : MeasurableSpace X
𝕜 : Type u_5
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : Module 𝕜 F
inst_3 : IsBoundedSMul 𝕜 F
p : ℝ≥0∞
μ : Measure X
inst_4 : Fact (1 ≤ p)
s : Set X
f : ↥(Lp F p μ)
⊢ (↑(↑((LpToLpRestrictCLM X F 𝕜 μ p s : (a : ↥(Lp F p μ)) → ↥(Lp F p (μ.restrict s))) f) : X →ₘ[μ.restrict s] F) :
      X → F) =ᶠ[ae (μ.restrict s)]
    (↑(↑f : X →ₘ[μ] F) : X → F)

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

Premises used: MeasureTheory.Lp.memLp, 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
μ : Measure X
inst_1 : NormedSpace ℝ E
s : Set X
⊢ Fact (LE.le (α := ℝ≥0∞) 1 1)

Tactic:
haveI : Fact ((1 : ℝ≥0∞) ≤ 1) := ⟨le_rfl⟩
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : Measure X
inst_1 : NormedSpace ℝ E
s : Set X
this : Fact (LE.le (α := ℝ≥0∞) 1 1)
h :
  ∀ (f : ↥(Lp E 1 μ)),
    Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, (↑(↑f : X →ₘ[μ] E) : X → E) x ∂μ)
      ((integral (μ.restrict s) ∘ fun (f : ↥(Lp E 1 μ)) ↦
          (↑(↑((LpToLpRestrictCLM X E ℝ μ 1 s : (a : ↥(Lp E 1 μ)) → ↥(Lp E 1 (μ.restrict s))) f) :
                X →ₘ[μ.restrict s] E) :
            X → E))
        f)
⊢ Eq (α := (f : ↥(Lp E 1 μ)) → E) (fun (f : ↥(Lp E 1 μ)) ↦ ∫ (x : X) in s, (↑(↑f : X →ₘ[μ] E) : X → E) x ∂μ)
    (integral (μ.restrict s) ∘ fun (f : ↥(Lp E 1 μ)) ↦
      (↑(↑((LpToLpRestrictCLM X E ℝ μ 1 s : (a : ↥(Lp E 1 μ)) → ↥(Lp E 1 (μ.restrict s))) f) : X →ₘ[μ.restrict s] E) :
        X → E))

Tactic:
ext1 f
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : Measure X
inst_1 : NormedSpace ℝ E
s : Set X
this : Fact (LE.le (α := ℝ≥0∞) 1 1)
f : ↥(Lp E 1 μ)
h :
  Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, (↑(↑f : X →ₘ[μ] E) : X → E) x ∂μ)
    (integral (μ.restrict s)
      (↑(↑((LpToLpRestrictCLM X E ℝ μ 1 s : (a : ↥(Lp E 1 μ)) → ↥(Lp E 1 (μ.restrict s))) f) : X →ₘ[μ.restrict s] E) :
        X → E))
h₁ h₂ :
  Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, (↑(↑f : X →ₘ[μ] E) : X → E) x ∂μ)
    (∫ (a : X) in s, (↑(↑f : X →ₘ[μ] E) : X → E) a ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, (↑(↑f : X →ₘ[μ] E) : X → E) x ∂μ)
    ((integral (μ.restrict s) ∘ fun (f : ↥(Lp E 1 μ)) ↦
        (↑(↑((LpToLpRestrictCLM X E ℝ μ 1 s : (a : ↥(Lp E 1 μ)) → ↥(Lp E 1 (μ.restrict s))) f) : X →ₘ[μ.restrict s] E) :
          X → E))
      f)

Tactic:
rw [Function.comp_apply, integral_congr_ae (LpToLpRestrictCLM_coeFn ℝ s f)]

Premises used: MeasureTheory.LpToLpRestrictCLM_coeFn, Real, MeasureTheory.integral_congr_ae, Function.comp_apply