awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.Floor
Goal:
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : TopologicalSpace R
inst_4 : OrderTopology R
inst_5 : MeasurableSpace R
inst_6 : OpensMeasurableSpace R
n : R
h : ⌈n⌉₊ = 0
⊢ MeasurableSet.{u_2} (α := R) (ceil ⁻¹' {⌈n⌉₊})

Tactic:
simp_all [Nat.preimage_ceil_of_ne_zero, -ceil_eq_zero]

Premises used: Nat.ceil_eq_zero, Nat.preimage_ceil_of_ne_zero
-- Module: Mathlib.MeasureTheory.Function.Floor
Goal:
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : TopologicalSpace R
inst_4 : OrderTopology R
inst_5 : MeasurableSpace R
inst_6 : OpensMeasurableSpace R
n : R
h : ⌈n⌉₊ ≠ 0
⊢ MeasurableSet.{u_2} (α := R) (ceil ⁻¹' {⌈n⌉₊})

Tactic:
simp_all [Nat.preimage_ceil_of_ne_zero, -ceil_eq_zero]

Premises used: Nat.ceil_eq_zero, Nat.preimage_ceil_of_ne_zero
-- Module: Mathlib.MeasureTheory.Function.Floor
Goal:
α : Type u_1
R : Type u_2
inst : MeasurableSpace α
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : FloorSemiring R
inst_4 : TopologicalSpace R
inst_5 : OrderTopology R
inst_6 : MeasurableSpace R
inst_7 : OpensMeasurableSpace R
f : α → R
hf : Measurable f
⊢ Measurable (β := ℕ) fun (x : α) ↦ ⌈f x⌉₊

Tactic:
Nat.measurable_ceil.comp hf

Premises used: Measurable.comp, Nat.measurable_ceil
-- 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
f : α → E
g : α → F
hf : MemLp f p μ
hg : MemLp g q μ
⊢ MemLp.{u_1, u_5} (ε := G) (fun (x : α) ↦ (((B : (a : E) → F →L[𝕜] G) (f x) : F →L[𝕜] G) : (a : F) → G) (g x)) r μ

Tactic:
MeasureTheory.MemLp.of_bilin (r := r) (B · ·) ‖B‖₊ hf hg
    (B.aestronglyMeasurable_comp₂ hf.1 hg.1) (.of_forall fun _ ↦ B.le_opNorm₂ _ _)

Premises used: NNNorm.nnnorm, MeasureTheory.MemLp.of_bilin, ContinuousLinearMap.aestronglyMeasurable_comp₂, Filter.Eventually.of_forall, ContinuousLinearMap.le_opNorm₂, And.left, DFunLike.coe
-- 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 α
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
f : α → E
g : α → F
C : ℝ
hf1 : AEStronglyMeasurable f μ
hf2 : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ C
hg : Integrable g μ
⊢ Integrable.{u_5, u_1} (ε := G) (fun (x : α) ↦ (((B : (a : E) → F →L[𝕜] G) (f x) : F →L[𝕜] G) : (a : F) → G) (g x)) μ

Tactic:
memLp_one_iff_integrable.1 <| B.memLp_of_bilin 1 (memLp_top_of_bound hf1 C hf2)
    (memLp_one_iff_integrable.2 hg)

Premises used: Iff.mpr, MeasureTheory.memLp_top_of_bound, ContinuousLinearMap.memLp_of_bilin, Iff.mp, OfNat.ofNat, MeasureTheory.memLp_one_iff_integrable
-- 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 α
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
f : α → E
g : α → F
C : ℝ
hf : Integrable f μ
hg1 : AEStronglyMeasurable g μ
hg2 : ∀ᵐ (a : α) ∂μ, ‖g a‖ ≤ C
⊢ Integrable.{u_5, u_1} (ε := G) (fun (x : α) ↦ (((B : (a : E) → F →L[𝕜] G) (f x) : F →L[𝕜] G) : (a : F) → G) (g x)) μ

Tactic:
B.flip.integrable_of_bilin_of_bdd_left C hg1 hg2 hf

Premises used: ContinuousLinearMap.integrable_of_bilin_of_bdd_left, ContinuousLinearMap.flip
-- 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
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
rw :
  (↑(↑(MemLp.toLp
              (fun (x : α) ↦
                (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
                  ((↑(↑g : α →ₘ[μ] F) : α → F) x))
              ⋯) :
          α →ₘ[μ] G) :
      α → G) =ᶠ[ae μ]
    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 g) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ] fun (x : α) ↦
    (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
      ((↑(↑g : α →ₘ[μ] F) : α → F) x)

Tactic:
rw [holder]

Premises used: ContinuousLinearMap.holder
-- 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
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
⊢ (↑(↑(MemLp.toLp
              (fun (x : α) ↦
                (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
                  ((↑(↑g : α →ₘ[μ] F) : α → F) x))
              ⋯) :
          α →ₘ[μ] G) :
      α → G) =ᶠ[ae μ]
    fun (x : α) ↦
    (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
      ((↑(↑g : α →ₘ[μ] F) : α → F) x)

Tactic:
MemLp.coeFn_toLp _

Premises used: MeasureTheory.MemLp.coeFn_toLp
-- 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
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
⊢ (↑(↑(MemLp.toLp
              (fun (x : α) ↦
                (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
                  ((↑(↑g : α →ₘ[μ] F) : α → F) x))
              ⋯) :
          α →ₘ[μ] G) :
      α → G) =ᶠ[ae μ]
    fun (x : α) ↦
    (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
      ((↑(↑g : α →ₘ[μ] F) : α → F) x)

Tactic:
exact MemLp.coeFn_toLp _

Premises used: MeasureTheory.MemLp.coeFn_toLp
-- 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
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
simp_rw :
  eLpNorm (↑(↑(holder r B f g) : α →ₘ[μ] G) : α → G) r μ ≤
    ‖B‖ₑ * eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ * eLpNorm (↑(↑g : α →ₘ[μ] F) : α → F) q μ
⊢ ‖holder r B f g‖₊ ≤ ‖B‖₊ * ‖f‖₊ * ‖g‖₊

Tactic:
simp_rw [← ENNReal.coe_le_coe, ENNReal.coe_mul, ← enorm_eq_nnnorm, Lp.enorm_def]

Premises used: ENNReal.coe_le_coe, enorm_eq_nnnorm, ENNReal.coe_mul, MeasureTheory.Lp.enorm_def
-- 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
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
apply :
  eLpNorm.{u_1, u_5} (ε := G)
      (fun (x : α) ↦
        (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
          ((↑(↑g : α →ₘ[μ] F) : α → F) x))
      r μ ≤
    ‖B‖ₑ * eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ * eLpNorm (↑(↑g : α →ₘ[μ] F) : α → F) q μ
⊢ eLpNorm (↑(↑(holder r B f g) : α →ₘ[μ] G) : α → G) r μ ≤
    ‖B‖ₑ * eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ * eLpNorm (↑(↑g : α →ₘ[μ] F) : α → F) q μ

Tactic:
apply eLpNorm_congr_ae (coeFn_holder B f g) |>.trans_le

Premises used: Eq.trans_le, MeasureTheory.eLpNorm_congr_ae, ContinuousLinearMap.coeFn_holder
-- 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
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
⊢ eLpNorm.{u_1, u_5} (ε := G)
      (fun (x : α) ↦
        (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
          ((↑(↑g : α →ₘ[μ] F) : α → F) x))
      r μ ≤
    ‖B‖ₑ * eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ * eLpNorm (↑(↑g : α →ₘ[μ] F) : α → F) q μ

Tactic:
eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm (Lp.memLp f).1 (Lp.memLp g).1 (B · ·) ‖B‖₊
    (.of_forall fun _ ↦ B.le_opNorm₂ _ _)

Premises used: MeasureTheory.Lp.memLp, MeasureTheory.AEEqFun.cast, NNNorm.nnnorm, Filter.Eventually.of_forall, ContinuousLinearMap.le_opNorm₂, And.left, MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm, Subtype.val, DFunLike.coe
-- 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
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
⊢ eLpNorm.{u_1, u_5} (ε := G)
      (fun (x : α) ↦
        (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
          ((↑(↑g : α →ₘ[μ] F) : α → F) x))
      r μ ≤
    ‖B‖ₑ * eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ * eLpNorm (↑(↑g : α →ₘ[μ] F) : α → F) q μ

Tactic:
exact eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm (Lp.memLp f).1 (Lp.memLp g).1 (B · ·) ‖B‖₊
    (.of_forall fun _ ↦ B.le_opNorm₂ _ _)

Premises used: MeasureTheory.Lp.memLp, MeasureTheory.AEEqFun.cast, NNNorm.nnnorm, Filter.Eventually.of_forall, ContinuousLinearMap.le_opNorm₂, And.left, MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm, Subtype.val, DFunLike.coe
-- 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
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
⊢ ‖holder r B f g‖ ≤ ‖B‖ * ‖f‖ * ‖g‖

Tactic:
NNReal.coe_le_coe.mpr <| nnnorm_holder_apply_apply_le B f g

Premises used: Iff.mpr, ContinuousLinearMap.nnnorm_holder_apply_apply_le, NNReal.toReal, NNReal.coe_le_coe
-- 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
f₁ f₂ : ↥(Lp E p μ)
g : ↥(Lp F q μ)
simp :
  MemLp.toLp
      (fun (x : α) ↦
        (((B : (a : E) → F →L[𝕜] G) ((↑(↑(f₁ + f₂) : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
          ((↑(↑g : α →ₘ[μ] F) : α → F) x))
      ⋯ =
    MemLp.toLp
      (HAdd.hAdd (α := α → G)
        (fun (x : α) ↦
          (((B : (a : E) → F →L[𝕜] G) ((↑(↑f₁ : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
            ((↑(↑g : α →ₘ[μ] F) : α → F) x))
        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₁ + f₂) g = holder r B f₁ g + holder r B f₂ g

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

Premises used: ContinuousLinearMap.holder, MeasureTheory.MemLp.toLp_add
-- 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
f₁ f₂ : ↥(Lp E p μ)
g : ↥(Lp F q μ)
hfg :
  (fun (x : α) ↦
      (((B : (a : E) → F →L[𝕜] G) ((↑(↑(f₁ + f₂) : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
        ((↑(↑g : α →ₘ[μ] F) : α → F) x)) =ᶠ[ae μ]
    HAdd.hAdd (α := α → G)
      (fun (x : α) ↦
        (((B : (a : E) → F →L[𝕜] G) ((↑(↑f₁ : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
          ((↑(↑g : α →ₘ[μ] F) : α → F) x))
      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₁ + f₂) : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
          ((↑(↑g : α →ₘ[μ] F) : α → F) x))
      ⋯ =
    MemLp.toLp
      (HAdd.hAdd (α := α → G)
        (fun (x : α) ↦
          (((B : (a : E) → F →L[𝕜] G) ((↑(↑f₁ : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
            ((↑(↑g : α →ₘ[μ] F) : α → F) x))
        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
f₁ f₂ : ↥(Lp E p μ)
g : ↥(Lp F q μ)
h :
  ∀ (x : α)
    (hx :
      (↑((↑f₁ : α →ₘ[μ] E) + (↑f₂ : α →ₘ[μ] E)) : α → E) x =
        ((↑(↑f₁ : α →ₘ[μ] E) : α → E) + (↑(↑f₂ : α →ₘ[μ] E) : α → E)) x),
    (((B : (a : E) → F →L[𝕜] G) ((↑(↑(f₁ + f₂) : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
        ((↑(↑g : α →ₘ[μ] F) : α → F) x) =
      HAdd.hAdd (α := α → G) (β := α → G)
        (fun (x : α) ↦
          (((B : (a : E) → F →L[𝕜] G) ((↑(↑f₁ : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
            ((↑(↑g : α →ₘ[μ] F) : α → F) x))
        (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₁ + f₂) : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
        ((↑(↑g : α →ₘ[μ] F) : α → F) x)) =ᶠ[ae μ]
    HAdd.hAdd (α := α → G)
      (fun (x : α) ↦
        (((B : (a : E) → F →L[𝕜] G) ((↑(↑f₁ : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
          ((↑(↑g : α →ₘ[μ] F) : α → F) x))
      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 [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_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
f₁ f₂ : ↥(Lp E p μ)
g : ↥(Lp F q μ)
x : α
hx :
  (↑((↑f₁ : α →ₘ[μ] E) + (↑f₂ : α →ₘ[μ] E)) : α → E) x = ((↑(↑f₁ : α →ₘ[μ] E) : α → E) + (↑(↑f₂ : α →ₘ[μ] E) : α → E)) x
⊢ (((B : (a : E) → F →L[𝕜] G) ((↑(↑(f₁ + f₂) : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
      ((↑(↑g : α →ₘ[μ] F) : α → F) x) =
    HAdd.hAdd (α := α → G) (β := α → G)
      (fun (x : α) ↦
        (((B : (a : E) → F →L[𝕜] G) ((↑(↑f₁ : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
          ((↑(↑g : α →ₘ[μ] F) : α → F) x))
      (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
f : ↥(Lp E p μ)
g₁ 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)
          ((↑(↑(g₁ + g₂) : α →ₘ[μ] F) : α → F) x))
      ⋯ =
    MemLp.toLp
      (HAdd.hAdd (α := α → G)
        (fun (x : α) ↦
          (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
            ((↑(↑g₁ : α →ₘ[μ] F) : α → F) x))
        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 (g₁ + g₂) = holder r B f g₁ + holder r B f g₂

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

Premises used: ContinuousLinearMap.holder, MeasureTheory.MemLp.toLp_add
-- 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
f : ↥(Lp E p μ)
g₁ g₂ : ↥(Lp F q μ)
hfg :
  (fun (x : α) ↦
      (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
        ((↑(↑(g₁ + g₂) : α →ₘ[μ] F) : α → F) x)) =ᶠ[ae μ]
    HAdd.hAdd (α := α → G)
      (fun (x : α) ↦
        (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
          ((↑(↑g₁ : α →ₘ[μ] F) : α → F) x))
      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)
          ((↑(↑(g₁ + g₂) : α →ₘ[μ] F) : α → F) x))
      ⋯ =
    MemLp.toLp
      (HAdd.hAdd (α := α → G)
        (fun (x : α) ↦
          (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
            ((↑(↑g₁ : α →ₘ[μ] F) : α → F) x))
        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
f : ↥(Lp E p μ)
g₁ g₂ : ↥(Lp F q μ)
h :
  ∀ (x : α)
    (hx :
      (↑((↑g₁ : α →ₘ[μ] F) + (↑g₂ : α →ₘ[μ] F)) : α → F) x =
        ((↑(↑g₁ : α →ₘ[μ] F) : α → F) + (↑(↑g₂ : α →ₘ[μ] F) : α → F)) x),
    (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
        ((↑(↑(g₁ + g₂) : α →ₘ[μ] F) : α → F) x) =
      HAdd.hAdd (α := α → G) (β := α → G)
        (fun (x : α) ↦
          (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
            ((↑(↑g₁ : α →ₘ[μ] F) : α → F) x))
        (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)
        ((↑(↑(g₁ + g₂) : α →ₘ[μ] F) : α → F) x)) =ᶠ[ae μ]
    HAdd.hAdd (α := α → G)
      (fun (x : α) ↦
        (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
          ((↑(↑g₁ : α →ₘ[μ] F) : α → F) x))
      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 [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_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
f : ↥(Lp E p μ)
g₁ g₂ : ↥(Lp F q μ)
x : α
hx :
  (↑((↑g₁ : α →ₘ[μ] F) + (↑g₂ : α →ₘ[μ] F)) : α → F) x = ((↑(↑g₁ : α →ₘ[μ] F) : α → F) + (↑(↑g₂ : α →ₘ[μ] F) : α → F)) x
⊢ (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
      ((↑(↑(g₁ + g₂) : α →ₘ[μ] F) : α → F) x) =
    HAdd.hAdd (α := α → G) (β := α → G)
      (fun (x : α) ↦
        (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
          ((↑(↑g₁ : α →ₘ[μ] F) : α → F) x))
      (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) ((↑(↑(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))
      ⋯
⊢ holder r B (c • f) g = c • holder r B f g

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

Premises used: ContinuousLinearMap.holder, MeasureTheory.MemLp.toLp_const_smul