awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
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 μ)
⊢ (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)
have 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
Tactic: filter_upwards [AEEqFun.coeFn_add f₁.val f₂.val] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
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 μ)
⊢ holder r B f (g₁ + g₂) = holder r B f g₁ + holder r B f g₂
have 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))
    sorry =
  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))
    sorry
Tactic: simp only [holder, ← MemLp.toLp_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
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 μ)
⊢ 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))
      ⋯
have 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)
Tactic: apply MemLp.toLp_congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
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 μ)
⊢ (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)
have 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
Tactic: filter_upwards [AEEqFun.coeFn_add g₁.val g₂.val] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
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 μ)
⊢ holder r B (c • f) g = c • holder r B f g
have 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))
    sorry =
  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))
    sorry
Tactic: simp only [holder, ← MemLp.toLp_const_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
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 μ)
⊢ 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))
      ⋯
have 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)
Tactic: apply MemLp.toLp_congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
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 μ)
⊢ (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)
have 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
Tactic: filter_upwards [Lp.coeFn_smul c f] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
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 μ)
⊢ holder r B f (c • g) = c • holder r B f g
have 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))
    sorry =
  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))
    sorry
Tactic: simp only [holder, ← MemLp.toLp_const_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
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 μ)
⊢ 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))
      ⋯
have 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)
Tactic: apply MemLp.toLp_congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
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 μ)
⊢ (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)
have 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
Tactic: filter_upwards [Lp.coeFn_smul c g] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
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) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E)
have rw : (↑(↑(MemLp.toLp ((↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E)) sorry) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ]
  (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E)
Tactic: rw [smul_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
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‖ ≤ ‖f‖ * ‖g‖
have simp : (eLpNorm (↑(↑(f • g) : α →ₘ[μ] E) : α → E) r μ).toReal ≤
  (eLpNorm (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) p μ * eLpNorm (↑(↑g : α →ₘ[μ] E) : α → E) q μ).toReal
Tactic: simp only [Lp.norm_def, ← ENNReal.toReal_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
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 μ).toReal ≤
    (eLpNorm (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) p μ * eLpNorm (↑(↑g : α →ₘ[μ] E) : α → E) q μ).toReal
have refine : eLpNorm (↑(↑(f • g) : α →ₘ[μ] E) : α → E) r μ ≤
  eLpNorm (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) p μ * eLpNorm (↑(↑g : α →ₘ[μ] E) : α → E) q μ
Tactic: refine ENNReal.toReal_mono (by finiteness) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
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 μ
have rw : eLpNorm ((↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E)) r μ ≤
  eLpNorm (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) p μ * eLpNorm (↑(↑g : α →ₘ[μ] E) : α → E) q μ
Tactic: rw [eLpNorm_congr_ae (coeFn_lpSMul f g)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
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 μ)
⊢ (f₁ + f₂) • g = f₁ • g + f₂ • g
have simp : Eq (α := ↥(Lp E r μ)) (MemLp.toLp ((↑(↑(f₁ + f₂) : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E)) sorry)
  (MemLp.toLp
    ((↑(↑f₁ : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E) +
      (↑(↑f₂ : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E))
    sorry)
Tactic: simp only [smul_def, ← MemLp.toLp_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
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 μ)
⊢ Eq (α := ↥(Lp E r μ)) (MemLp.toLp ((↑(↑(f₁ + f₂) : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E)) ⋯)
    (MemLp.toLp
      ((↑(↑f₁ : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E) +
        (↑(↑f₂ : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E))
      ⋯)
have hfg : (↑(↑(f₁ + f₂) : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E) =ᶠ[ae μ]
  (↑(↑f₁ : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E) +
    (↑(↑f₂ : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E)
Tactic: apply MemLp.toLp_congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
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 μ)
⊢ (↑(↑(f₁ + f₂) : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E) =ᶠ[ae μ]
    (↑(↑f₁ : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E) +
      (↑(↑f₂ : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E)
have h : ∀ (x : α)
  (hx :
    (↑((↑f₁ : α →ₘ[μ] 𝕜) + (↑f₂ : α →ₘ[μ] 𝕜)) : α → 𝕜) x =
      ((↑(↑f₁ : α →ₘ[μ] 𝕜) : α → 𝕜) + (↑(↑f₂ : α →ₘ[μ] 𝕜) : α → 𝕜)) x),
  ((↑(↑(f₁ + f₂) : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E)) x =
    ((↑(↑f₁ : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E) +
        (↑(↑f₂ : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E))
      x
Tactic: filter_upwards [AEEqFun.coeFn_add f₁.val f₂.val] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
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 μ)
⊢ f • (g₁ + g₂) = f • g₁ + f • g₂
have simp : Eq (α := ↥(Lp E r μ)) (MemLp.toLp ((↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑(g₁ + g₂) : α →ₘ[μ] E) : α → E)) sorry)
  (MemLp.toLp
    ((↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g₁ : α →ₘ[μ] E) : α → E) +
      (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g₂ : α →ₘ[μ] E) : α → E))
    sorry)
Tactic: simp only [smul_def, ← MemLp.toLp_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
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 μ)
⊢ Eq (α := ↥(Lp E r μ)) (MemLp.toLp ((↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑(g₁ + g₂) : α →ₘ[μ] E) : α → E)) ⋯)
    (MemLp.toLp
      ((↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g₁ : α →ₘ[μ] E) : α → E) +
        (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g₂ : α →ₘ[μ] E) : α → E))
      ⋯)
have apply : (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑(g₁ + g₂) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ]
  (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g₁ : α →ₘ[μ] E) : α → E) +
    (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g₂ : α →ₘ[μ] E) : α → E)
Tactic: apply MemLp.toLp_congr _ _ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
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 μ)
⊢ (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑(g₁ + g₂) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ]
    (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g₁ : α →ₘ[μ] E) : α → E) +
      (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g₂ : α →ₘ[μ] E) : α → E)
have 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
Tactic: filter_upwards [AEEqFun.coeFn_add g₁.val g₂.val] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
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 μ)
⊢ HSMul.hSMul (β := ↥(Lp E q μ)) f 0 = 0
have h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: convert! MemLp.zero (ε := E) |>.toLp_zero
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
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)
have apply : HSMul.hSMul (β := α → E) (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) (↑(↑0 : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
Tactic: apply MemLp.toLp_congr _ _ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
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 μ)
⊢ HSMul.hSMul (β := α → E) (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) (↑(↑0 : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
have h : ∀ (x : α) (hx : Eq.{u_4 + 1} (α := E) ((↑(↑0 : α →ₘ[μ] E) : α → E) x) (0 x)),
  HSMul.hSMul (β := α → E) (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) (↑(↑0 : α →ₘ[μ] E) : α → E) x = 0 x
Tactic: filter_upwards [Lp.coeFn_zero E q μ] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
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 μ)
x : α
hx : Eq.{u_4 + 1} (α := E) ((↑(↑0 : α →ₘ[μ] E) : α → E) x) (0 x)
⊢ HSMul.hSMul (β := α → E) (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) (↑(↑0 : α →ₘ[μ] E) : α → E) x = 0 x
have h : HSMul.hSMul (β := E) ((↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) x) (0 x) = 0 x
Tactic: rw [Pi.smul_apply', hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
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 E q μ)
⊢ HSMul.hSMul (α := ↥(Lp 𝕜 p μ)) 0 f = 0
have h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: convert! MemLp.zero (ε := E) |>.toLp_zero
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
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 E q μ)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have apply : HSMul.hSMul (α := α → 𝕜) (↑(↑0 : α →ₘ[μ] 𝕜) : α → 𝕜) (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
Tactic: apply MemLp.toLp_congr _ _ ?_