awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
c : 𝕜
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
hfg :
  (fun (x : α) ↦
      (((B : (a : E) → F →L[𝕜] G) ((↑(↑(c • f) : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
        ((↑(↑g : α →ₘ[μ] F) : α → F) x)) =ᶠ[ae μ]
    HSMul.hSMul (β := α → G) c fun (x : α) ↦
      (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
        ((↑(↑g : α →ₘ[μ] F) : α → F) x)
⊢ MemLp.toLp
      (fun (x : α) ↦
        (((B : (a : E) → F →L[𝕜] G) ((↑(↑(c • f) : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
          ((↑(↑g : α →ₘ[μ] F) : α → F) x))
      ⋯ =
    MemLp.toLp
      (HSMul.hSMul (β := α → G) c fun (x : α) ↦
        (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
          ((↑(↑g : α →ₘ[μ] F) : α → F) x))
      ⋯

Tactic:
apply MemLp.toLp_congr

Premises used: MeasureTheory.MemLp.toLp_congr
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
c : 𝕜
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
h :
  ∀ (x : α) (hx : (↑(↑(c • f) : α →ₘ[μ] E) : α → E) x = (c • (↑(↑f : α →ₘ[μ] E) : α → E)) x),
    (((B : (a : E) → F →L[𝕜] G) ((↑(↑(c • f) : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
        ((↑(↑g : α →ₘ[μ] F) : α → F) x) =
      HSMul.hSMul (β := α → G) c
        (fun (x : α) ↦
          (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
            ((↑(↑g : α →ₘ[μ] F) : α → F) x))
        x
⊢ (fun (x : α) ↦
      (((B : (a : E) → F →L[𝕜] G) ((↑(↑(c • f) : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
        ((↑(↑g : α →ₘ[μ] F) : α → F) x)) =ᶠ[ae μ]
    HSMul.hSMul (β := α → G) c fun (x : α) ↦
      (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
        ((↑(↑g : α →ₘ[μ] F) : α → F) x)

Tactic:
filter_upwards [Lp.coeFn_smul c f] with x hx

Premises used: MeasureTheory.Lp.coeFn_smul
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
c : 𝕜
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
x : α
hx : (↑(↑(c • f) : α →ₘ[μ] E) : α → E) x = (c • (↑(↑f : α →ₘ[μ] E) : α → E)) x
⊢ (((B : (a : E) → F →L[𝕜] G) ((↑(↑(c • f) : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
      ((↑(↑g : α →ₘ[μ] F) : α → F) x) =
    HSMul.hSMul (β := α → G) c
      (fun (x : α) ↦
        (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
          ((↑(↑g : α →ₘ[μ] F) : α → F) x))
      x

Tactic:
simp [hx]
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
c : 𝕜
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
simp :
  MemLp.toLp
      (fun (x : α) ↦
        (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
          ((↑(↑(c • g) : α →ₘ[μ] F) : α → F) x))
      ⋯ =
    MemLp.toLp
      (HSMul.hSMul (β := α → G) c fun (x : α) ↦
        (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
          ((↑(↑g : α →ₘ[μ] F) : α → F) x))
      ⋯
⊢ holder r B f (c • g) = c • holder r B f g

Tactic:
simp only [holder, ← MemLp.toLp_const_smul]

Premises used: ContinuousLinearMap.holder, MeasureTheory.MemLp.toLp_const_smul
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
c : 𝕜
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
hfg :
  (fun (x : α) ↦
      (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
        ((↑(↑(c • g) : α →ₘ[μ] F) : α → F) x)) =ᶠ[ae μ]
    HSMul.hSMul (β := α → G) c fun (x : α) ↦
      (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
        ((↑(↑g : α →ₘ[μ] F) : α → F) x)
⊢ MemLp.toLp
      (fun (x : α) ↦
        (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
          ((↑(↑(c • g) : α →ₘ[μ] F) : α → F) x))
      ⋯ =
    MemLp.toLp
      (HSMul.hSMul (β := α → G) c fun (x : α) ↦
        (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
          ((↑(↑g : α →ₘ[μ] F) : α → F) x))
      ⋯

Tactic:
apply MemLp.toLp_congr

Premises used: MeasureTheory.MemLp.toLp_congr
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
c : 𝕜
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
h :
  ∀ (x : α) (hx : (↑(↑(c • g) : α →ₘ[μ] F) : α → F) x = (c • (↑(↑g : α →ₘ[μ] F) : α → F)) x),
    (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
        ((↑(↑(c • g) : α →ₘ[μ] F) : α → F) x) =
      HSMul.hSMul (β := α → G) c
        (fun (x : α) ↦
          (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
            ((↑(↑g : α →ₘ[μ] F) : α → F) x))
        x
⊢ (fun (x : α) ↦
      (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
        ((↑(↑(c • g) : α →ₘ[μ] F) : α → F) x)) =ᶠ[ae μ]
    HSMul.hSMul (β := α → G) c fun (x : α) ↦
      (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
        ((↑(↑g : α →ₘ[μ] F) : α → F) x)

Tactic:
filter_upwards [Lp.coeFn_smul c g] with x hx

Premises used: MeasureTheory.Lp.coeFn_smul
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
c : 𝕜
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
x : α
hx : (↑(↑(c • g) : α →ₘ[μ] F) : α → F) x = (c • (↑(↑g : α →ₘ[μ] F) : α → F)) x
⊢ (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
      ((↑(↑(c • g) : α →ₘ[μ] F) : α → F) x) =
    HSMul.hSMul (β := α → G) c
      (fun (x : α) ↦
        (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
          ((↑(↑g : α →ₘ[μ] F) : α → F) x))
      x

Tactic:
simp [hx]
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
inst_7 : Fact (1 ≤ p)
inst_8 : Fact (1 ≤ q)
inst_9 : Fact (1 ≤ r)
⊢ norm (E := ↥(Lp E p μ) →L[𝕜] ↥(Lp F q μ) →L[𝕜] ↥(Lp G r μ)) (holderL μ p q r B) ≤ ‖B‖

Tactic:
LinearMap.mkContinuous₂_norm_le _ (norm_nonneg B) _

Premises used: Set.Mem, ContinuousLinearMap.holderL, LinearMap.mkContinuous₂_norm_le, norm_nonneg
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
m : MeasurableSpace α
μ : Measure α
p q : ℝ≥0∞
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
inst_7 : Fact (1 ≤ p)
inst_8 : Fact (1 ≤ q)
inst_9 : p.HolderConjugate q
inst_10 : NormedSpace ℝ G
inst_11 : SMulCommClass ℝ 𝕜 G
inst_12 : CompleteSpace G
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
⊢ Eq.{u_5 + 1} (α := G)
    ((((lpPairing μ p q B : (a : ↥(Lp E p μ)) → ↥(Lp F q μ) →L[𝕜] G) f : ↥(Lp F q μ) →L[𝕜] G) : (a : ↥(Lp F q μ)) → G)
        g :
      G)
    (∫ (x : α),
        (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
          ((↑(↑g : α →ₘ[μ] F) : α → F) x) ∂μ :
      G)

Tactic:
simpa [lpPairing, ← L1.integral_eq', L1.integral_eq_integral] using
    integral_congr_ae <| B.coeFn_holder _ _

Premises used: MeasureTheory.integral_congr_ae, MeasureTheory.L1.integral_eq_integral, ContinuousLinearMap.lpPairing, MeasureTheory.L1.integral_eq', ContinuousLinearMap.coeFn_holder
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
⊢ f • g = MemLp.toLp ((↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E)) ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
rw :
  (↑(↑(MemLp.toLp ((↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E)) ⋯) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ]
    (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E)
⊢ (↑(↑(f • g) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E)

Tactic:
rw [smul_def]

Premises used: MeasureTheory.Lp.smul_def
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
⊢ (↑(↑(MemLp.toLp ((↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E)) ⋯) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ]
    (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E)

Tactic:
MemLp.coeFn_toLp _

Premises used: MeasureTheory.MemLp.coeFn_toLp
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
⊢ (↑(↑(MemLp.toLp ((↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E)) ⋯) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ]
    (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E)

Tactic:
exact MemLp.coeFn_toLp _

Premises used: MeasureTheory.MemLp.coeFn_toLp
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
simp :
  (eLpNorm (↑(↑(f • g) : α →ₘ[μ] E) : α → E) r μ).toReal ≤
    (eLpNorm (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) p μ * eLpNorm (↑(↑g : α →ₘ[μ] E) : α → E) q μ).toReal
⊢ ‖f • g‖ ≤ ‖f‖ * ‖g‖

Tactic:
simp only [Lp.norm_def, ← ENNReal.toReal_mul]

Premises used: ENNReal.toReal_mul, MeasureTheory.Lp.norm_def
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
⊢ eLpNorm (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) p μ * eLpNorm (↑(↑g : α →ₘ[μ] E) : α → E) q μ ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
refine :
  eLpNorm (↑(↑(f • g) : α →ₘ[μ] E) : α → E) r μ ≤
    eLpNorm (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) p μ * eLpNorm (↑(↑g : α →ₘ[μ] E) : α → E) q μ
⊢ (eLpNorm (↑(↑(f • g) : α →ₘ[μ] E) : α → E) r μ).toReal ≤
    (eLpNorm (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) p μ * eLpNorm (↑(↑g : α →ₘ[μ] E) : α → E) q μ).toReal

Tactic:
refine ENNReal.toReal_mono (by finiteness) ?_

Premises used: ENNReal.toReal_mono
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
rw :
  eLpNorm ((↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E)) r μ ≤
    eLpNorm (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) p μ * eLpNorm (↑(↑g : α →ₘ[μ] E) : α → E) q μ
⊢ eLpNorm (↑(↑(f • g) : α →ₘ[μ] E) : α → E) r μ ≤
    eLpNorm (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) p μ * eLpNorm (↑(↑g : α →ₘ[μ] E) : α → E) q μ

Tactic:
rw [eLpNorm_congr_ae (coeFn_lpSMul f g)]

Premises used: MeasureTheory.Lp.coeFn_lpSMul, MeasureTheory.eLpNorm_congr_ae
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
⊢ eLpNorm ((↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E)) r μ ≤
    eLpNorm (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) p μ * eLpNorm (↑(↑g : α →ₘ[μ] E) : α → E) q μ

Tactic:
eLpNorm_smul_le_mul_eLpNorm (Lp.aestronglyMeasurable g) (Lp.aestronglyMeasurable f)

Premises used: MeasureTheory.eLpNorm_smul_le_mul_eLpNorm, MeasureTheory.Lp.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
⊢ eLpNorm ((↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E)) r μ ≤
    eLpNorm (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) p μ * eLpNorm (↑(↑g : α →ₘ[μ] E) : α → E) q μ

Tactic:
exact eLpNorm_smul_le_mul_eLpNorm (Lp.aestronglyMeasurable g) (Lp.aestronglyMeasurable f)

Premises used: MeasureTheory.eLpNorm_smul_le_mul_eLpNorm, MeasureTheory.Lp.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f₁ f₂ : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
simp :
  Eq (α := ↥(Lp E r μ)) (MemLp.toLp ((↑(↑(f₁ + f₂) : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E)) ⋯)
    (MemLp.toLp
      ((↑(↑f₁ : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E) +
        (↑(↑f₂ : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E))
      ⋯)
⊢ (f₁ + f₂) • g = f₁ • g + f₂ • g

Tactic:
simp only [smul_def, ← MemLp.toLp_add]

Premises used: MeasureTheory.Lp.smul_def, MeasureTheory.MemLp.toLp_add
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f₁ f₂ : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
hfg :
  (↑(↑(f₁ + f₂) : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E) =ᶠ[ae μ]
    (↑(↑f₁ : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E) +
      (↑(↑f₂ : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E)
⊢ Eq (α := ↥(Lp E r μ)) (MemLp.toLp ((↑(↑(f₁ + f₂) : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E)) ⋯)
    (MemLp.toLp
      ((↑(↑f₁ : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E) +
        (↑(↑f₂ : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E))
      ⋯)

Tactic:
apply MemLp.toLp_congr

Premises used: MeasureTheory.MemLp.toLp_congr
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f₁ f₂ : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
h :
  ∀ (x : α)
    (hx :
      (↑((↑f₁ : α →ₘ[μ] 𝕜) + (↑f₂ : α →ₘ[μ] 𝕜)) : α → 𝕜) x =
        ((↑(↑f₁ : α →ₘ[μ] 𝕜) : α → 𝕜) + (↑(↑f₂ : α →ₘ[μ] 𝕜) : α → 𝕜)) x),
    ((↑(↑(f₁ + f₂) : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E)) x =
      ((↑(↑f₁ : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E) +
          (↑(↑f₂ : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E))
        x
⊢ (↑(↑(f₁ + f₂) : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E) =ᶠ[ae μ]
    (↑(↑f₁ : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E) +
      (↑(↑f₂ : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E)

Tactic:
filter_upwards [AEEqFun.coeFn_add f₁.val f₂.val] with x hx

Premises used: MeasureTheory.AEEqFun.coeFn_add, Subtype.val
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f₁ f₂ : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
x : α
hx :
  (↑((↑f₁ : α →ₘ[μ] 𝕜) + (↑f₂ : α →ₘ[μ] 𝕜)) : α → 𝕜) x = ((↑(↑f₁ : α →ₘ[μ] 𝕜) : α → 𝕜) + (↑(↑f₂ : α →ₘ[μ] 𝕜) : α → 𝕜)) x
⊢ ((↑(↑(f₁ + f₂) : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E)) x =
    ((↑(↑f₁ : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E) +
        (↑(↑f₂ : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E))
      x

Tactic:
simp [hx, add_smul]

Premises used: add_smul
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : ↥(Lp 𝕜 p μ)
g₁ g₂ : ↥(Lp E q μ)
simp :
  Eq (α := ↥(Lp E r μ)) (MemLp.toLp ((↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑(g₁ + g₂) : α →ₘ[μ] E) : α → E)) ⋯)
    (MemLp.toLp
      ((↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g₁ : α →ₘ[μ] E) : α → E) +
        (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g₂ : α →ₘ[μ] E) : α → E))
      ⋯)
⊢ f • (g₁ + g₂) = f • g₁ + f • g₂

Tactic:
simp only [smul_def, ← MemLp.toLp_add]

Premises used: MeasureTheory.Lp.smul_def, MeasureTheory.MemLp.toLp_add
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : ↥(Lp 𝕜 p μ)
g₁ g₂ : ↥(Lp E q μ)
apply :
  (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑(g₁ + g₂) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ]
    (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g₁ : α →ₘ[μ] E) : α → E) +
      (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g₂ : α →ₘ[μ] E) : α → E)
⊢ Eq (α := ↥(Lp E r μ)) (MemLp.toLp ((↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑(g₁ + g₂) : α →ₘ[μ] E) : α → E)) ⋯)
    (MemLp.toLp
      ((↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g₁ : α →ₘ[μ] E) : α → E) +
        (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g₂ : α →ₘ[μ] E) : α → E))
      ⋯)

Tactic:
apply MemLp.toLp_congr _ _ ?_

Premises used: MeasureTheory.MemLp.toLp_congr
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : ↥(Lp 𝕜 p μ)
g₁ g₂ : ↥(Lp E q μ)
h :
  ∀ (x : α)
    (hx :
      (↑((↑g₁ : α →ₘ[μ] E) + (↑g₂ : α →ₘ[μ] E)) : α → E) x =
        ((↑(↑g₁ : α →ₘ[μ] E) : α → E) + (↑(↑g₂ : α →ₘ[μ] E) : α → E)) x),
    ((↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑(g₁ + g₂) : α →ₘ[μ] E) : α → E)) x =
      ((↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g₁ : α →ₘ[μ] E) : α → E) +
          (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g₂ : α →ₘ[μ] E) : α → E))
        x
⊢ (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑(g₁ + g₂) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ]
    (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g₁ : α →ₘ[μ] E) : α → E) +
      (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g₂ : α →ₘ[μ] E) : α → E)

Tactic:
filter_upwards [AEEqFun.coeFn_add g₁.val g₂.val] with x hx

Premises used: MeasureTheory.AEEqFun.coeFn_add, Subtype.val
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : ↥(Lp 𝕜 p μ)
g₁ g₂ : ↥(Lp E q μ)
x : α
hx :
  (↑((↑g₁ : α →ₘ[μ] E) + (↑g₂ : α →ₘ[μ] E)) : α → E) x = ((↑(↑g₁ : α →ₘ[μ] E) : α → E) + (↑(↑g₂ : α →ₘ[μ] E) : α → E)) x
⊢ ((↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑(g₁ + g₂) : α →ₘ[μ] E) : α → E)) x =
    ((↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g₁ : α →ₘ[μ] E) : α → E) +
        (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g₂ : α →ₘ[μ] E) : α → E))
      x

Tactic:
simp [hx, smul_add]

Premises used: smul_add
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : ↥(Lp 𝕜 p μ)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
MemLp.zero (ε := E) |>.toLp_zero

Premises used: MeasureTheory.MemLp.zero, MeasureTheory.MemLp.toLp_zero
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : ↥(Lp 𝕜 p μ)
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ HSMul.hSMul (β := ↥(Lp E q μ)) f 0 = 0

Tactic:
convert! MemLp.zero (ε := E) |>.toLp_zero

Premises used: MeasureTheory.MemLp.zero, MeasureTheory.MemLp.toLp_zero
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : ↥(Lp 𝕜 p μ)
apply : HSMul.hSMul (β := α → E) (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) (↑(↑0 : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
apply MemLp.toLp_congr _ _ ?_

Premises used: MeasureTheory.MemLp.toLp_congr