awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
𝕜_1 : Type u_2
𝕜'_1 : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
g : E → F
c_1 : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
L : E →SL[σ] F
c : 𝕜
f : ↥(Lp E p μ)
h :
  (↑(↑(L.compLp (c • f)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    (↑(↑(HSMul.hSMul (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') (L.compLp f)) : α →ₘ[μ] F) : α → F)
⊢ L.compLp (c • f) = HSMul.hSMul (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') (L.compLp f)

Tactic:
ext1
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
𝕜_1 : Type u_2
𝕜'_1 : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
g : E → F
c_1 : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
L : E →SL[σ] F
c : 𝕜
f : ↥(Lp E p μ)
h :
  ∀ (a : α) (ha1 : (↑(↑(c • f) : α →ₘ[μ] E) : α → E) a = (c • (↑(↑f : α →ₘ[μ] E) : α → E)) a)
    (ha2 : (↑(↑(L.compLp (c • f)) : α →ₘ[μ] F) : α → F) a = (L : (a : E) → F) ((↑(↑(c • f) : α →ₘ[μ] E) : α → E) a))
    (ha3 :
      (↑(↑(HSMul.hSMul (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') (L.compLp f)) : α →ₘ[μ] F) : α → F) a =
        HSMul.hSMul (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') (↑(↑(L.compLp f) : α →ₘ[μ] F) : α → F) a)
    (ha4 : (↑(↑(L.compLp f) : α →ₘ[μ] F) : α → F) a = (L : (a : E) → F) ((↑(↑f : α →ₘ[μ] E) : α → E) a)),
    (↑(↑(L.compLp (c • f)) : α →ₘ[μ] F) : α → F) a =
      (↑(↑(HSMul.hSMul (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') (L.compLp f)) : α →ₘ[μ] F) : α → F) a
⊢ (↑(↑(L.compLp (c • f)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    (↑(↑(HSMul.hSMul (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') (L.compLp f)) : α →ₘ[μ] F) : α → F)

Tactic:
filter_upwards [Lp.coeFn_smul c f, coeFn_compLp L (c • f), Lp.coeFn_smul (σ c) (L.compLp f),
      coeFn_compLp L f] with _ ha1 ha2 ha3 ha4

Premises used: MeasureTheory.Lp.coeFn_smul, ContinuousLinearMap.compLp, HSMul.hSMul, ContinuousLinearMap.coeFn_compLp, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
𝕜_1 : Type u_2
𝕜'_1 : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
g : E → F
c_1 : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
L : E →SL[σ] F
c : 𝕜
f : ↥(Lp E p μ)
a : α
ha1 : (↑(↑(c • f) : α →ₘ[μ] E) : α → E) a = (c • (↑(↑f : α →ₘ[μ] E) : α → E)) a
ha2 : (↑(↑(L.compLp (c • f)) : α →ₘ[μ] F) : α → F) a = (L : (a : E) → F) ((↑(↑(c • f) : α →ₘ[μ] E) : α → E) a)
ha3 :
  (↑(↑(HSMul.hSMul (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') (L.compLp f)) : α →ₘ[μ] F) : α → F) a =
    HSMul.hSMul (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') (↑(↑(L.compLp f) : α →ₘ[μ] F) : α → F) a
ha4 : (↑(↑(L.compLp f) : α →ₘ[μ] F) : α → F) a = (L : (a : E) → F) ((↑(↑f : α →ₘ[μ] E) : α → E) a)
⊢ (↑(↑(L.compLp (c • f)) : α →ₘ[μ] F) : α → F) a =
    (↑(↑(HSMul.hSMul (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') (L.compLp f)) : α →ₘ[μ] F) : α → F) a

Tactic:
simp only [ha1, ha2, ha3, ha4, Pi.smul_apply, map_smulₛₗ]

Premises used: MulActionSemiHomClass.map_smulₛₗ, Pi.smul_apply
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
inst_7 : Fact (1 ≤ p)
L : E →SL[σ] F
f : ↥(Lp E p μ)
⊢ EventuallyEq.{u_1, u_5} (β := F) (ae μ)
    (↑(↑((compLpL p μ L : (a : ↥(Lp E p μ)) → ↥(Lp F p μ)) f) : α →ₘ[μ] F) : α → F) fun (a : α) ↦
    (L : (a : E) → F) ((↑(↑f : α →ₘ[μ] E) : α → E) a)

Tactic:
L.coeFn_compLp f

Premises used: Filter.EventuallyEq, ContinuousLinearMap.coeFn_compLp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
inst_7 : Fact (1 ≤ p)
L L' : E →SL[σ] F
h :
  ∀ (f : ↥(Lp E p μ)),
    Eq (α := ↥(Lp F p μ)) ((compLpL p μ (L + L') : (a : ↥(Lp E p μ)) → ↥(Lp F p μ)) f : ↥(Lp F p μ))
      ((HAdd.hAdd (α := ↥(Lp E p μ) →SL[σ] ↥(Lp F p μ)) (compLpL p μ L) (compLpL p μ L') :
            (a : ↥(Lp E p μ)) → ↥(Lp F p μ))
          f :
        ↥(Lp F p μ))
⊢ compLpL p μ (L + L') = HAdd.hAdd (α := ↥(Lp E p μ) →SL[σ] ↥(Lp F p μ)) (compLpL p μ L) (compLpL p μ L')

Tactic:
ext1 f
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
inst_7 : Fact (1 ≤ p)
L L' : E →SL[σ] F
f : ↥(Lp E p μ)
⊢ Eq (α := ↥(Lp F p μ)) ((compLpL p μ (L + L') : (a : ↥(Lp E p μ)) → ↥(Lp F p μ)) f : ↥(Lp F p μ))
    ((HAdd.hAdd (α := ↥(Lp E p μ) →SL[σ] ↥(Lp F p μ)) (compLpL p μ L) (compLpL p μ L') :
          (a : ↥(Lp E p μ)) → ↥(Lp F p μ))
        f :
      ↥(Lp F p μ))

Tactic:
add_compLp L L' f

Premises used: Set.Mem, ContinuousLinearMap.compLp, ContinuousLinearMap.add_compLp, LipschitzWith.compLp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
inst_7 : Fact (1 ≤ p)
L L' : E →SL[σ] F
f : ↥(Lp E p μ)
⊢ Eq (α := ↥(Lp F p μ)) ((compLpL p μ (L + L') : (a : ↥(Lp E p μ)) → ↥(Lp F p μ)) f : ↥(Lp F p μ))
    ((HAdd.hAdd (α := ↥(Lp E p μ) →SL[σ] ↥(Lp F p μ)) (compLpL p μ L) (compLpL p μ L') :
          (a : ↥(Lp E p μ)) → ↥(Lp F p μ))
        f :
      ↥(Lp F p μ))

Tactic:
exact add_compLp L L' f

Premises used: ContinuousLinearMap.add_compLp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
inst_7 : Fact (1 ≤ p)
𝕜'' : Type u_8
inst_8 : NormedRing 𝕜''
inst_9 : Module 𝕜'' F
inst_10 : IsBoundedSMul 𝕜'' F
inst_11 : SMulCommClass 𝕜' 𝕜'' F
c : 𝕜''
L : E →SL[σ] F
h :
  ∀ (f : ↥(Lp E p μ)),
    Eq (α := ↥(Lp F p μ)) ((compLpL p μ (c • L) : (a : ↥(Lp E p μ)) → ↥(Lp F p μ)) f : ↥(Lp F p μ))
      ((HSMul.hSMul (β := ↥(Lp E p μ) →SL[σ] ↥(Lp F p μ)) c (compLpL p μ L) : (a : ↥(Lp E p μ)) → ↥(Lp F p μ)) f :
        ↥(Lp F p μ))
⊢ compLpL p μ (c • L) = HSMul.hSMul (β := ↥(Lp E p μ) →SL[σ] ↥(Lp F p μ)) c (compLpL p μ L)

Tactic:
ext1 f
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
inst_7 : Fact (1 ≤ p)
𝕜'' : Type u_8
inst_8 : NormedRing 𝕜''
inst_9 : Module 𝕜'' F
inst_10 : IsBoundedSMul 𝕜'' F
inst_11 : SMulCommClass 𝕜' 𝕜'' F
c : 𝕜''
L : E →SL[σ] F
f : ↥(Lp E p μ)
⊢ Eq (α := ↥(Lp F p μ)) ((compLpL p μ (c • L) : (a : ↥(Lp E p μ)) → ↥(Lp F p μ)) f : ↥(Lp F p μ))
    ((HSMul.hSMul (β := ↥(Lp E p μ) →SL[σ] ↥(Lp F p μ)) c (compLpL p μ L) : (a : ↥(Lp E p μ)) → ↥(Lp F p μ)) f :
      ↥(Lp F p μ))

Tactic:
smul_compLp c L f

Premises used: ContinuousLinearMap.smul_compLp, ContinuousLinearMap.compLp, LipschitzWith.compLp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
inst_7 : Fact (1 ≤ p)
𝕜'' : Type u_8
inst_8 : NormedRing 𝕜''
inst_9 : Module 𝕜'' F
inst_10 : IsBoundedSMul 𝕜'' F
inst_11 : SMulCommClass 𝕜' 𝕜'' F
c : 𝕜''
L : E →SL[σ] F
f : ↥(Lp E p μ)
⊢ Eq (α := ↥(Lp F p μ)) ((compLpL p μ (c • L) : (a : ↥(Lp E p μ)) → ↥(Lp F p μ)) f : ↥(Lp F p μ))
    ((HSMul.hSMul (β := ↥(Lp E p μ) →SL[σ] ↥(Lp F p μ)) c (compLpL p μ L) : (a : ↥(Lp E p μ)) → ↥(Lp F p μ)) f :
      ↥(Lp F p μ))

Tactic:
exact smul_compLp c L f

Premises used: ContinuousLinearMap.smul_compLp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
inst_7 : Fact (1 ≤ p)
L : E →SL[σ] F
⊢ norm (E := ↥(Lp E p μ) →SL[σ] ↥(Lp F p μ)) (compLpL p μ L) ≤ ‖L‖

Tactic:
LinearMap.mkContinuous_norm_le _ (norm_nonneg _) _

Premises used: Set.Mem, LinearMap.mkContinuous_norm_le, ContinuousLinearMap.compLpL, norm_nonneg
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
𝕜_1 : Type u_2
𝕜'_1 : Type u_3
E : Type u_4
F_1 : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F_1
g_1 : E → F_1
c : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F_1
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
F : Type u_8
G : Type u_9
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
B : G →L[𝕜] E →L[𝕜] F
g h : G
h₁ :
  ∀ (f : ↥(Lp E p μ)),
    EventuallyEq.{u_1, u_8} (β := F) (ae μ)
      (↑(↑((compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) (g + h)) : (a : ↥(Lp E p μ)) → ↥(Lp F p μ)) f) : α →ₘ[μ] F) : α → F)
      (↑(↑((HAdd.hAdd (α := ↥(Lp E p μ) →ₗ[𝕜] ↥(Lp F p μ)) (compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) g))
                    (compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) h)) :
                  (a : ↥(Lp E p μ)) → ↥(Lp F p μ))
                f) :
            α →ₘ[μ] F) :
        α → F)
⊢ compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) (g + h)) =
    HAdd.hAdd (α := ↥(Lp E p μ) →ₗ[𝕜] ↥(Lp F p μ)) (compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) g))
      (compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) h))

Tactic:
ext f
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
𝕜_1 : Type u_2
𝕜'_1 : Type u_3
E : Type u_4
F_1 : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F_1
g_1 : E → F_1
c : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F_1
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
F : Type u_8
G : Type u_9
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
B : G →L[𝕜] E →L[𝕜] F
g h : G
f : ↥(Lp E p μ)
x : α
hx :
  Eq.{u_8 + 1} (α := F)
    ((↑(↑(compLp.{u_1, u_4, u_8, u_6, u_6} (𝕜 := 𝕜) (𝕜' := 𝕜) (σ := RingHom.id 𝕜) ((B : (a : G) → E →L[𝕜] F) (g + h))
                  f) :
              α →ₘ[μ] F) :
          α → F)
        x :
      F)
    ((((B : (a : G) → E →L[𝕜] F) (g + h) : E →L[𝕜] F) : (a : E) → F) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F)
hg :
  Eq.{u_8 + 1} (α := F)
    ((↑(↑(compLp.{u_1, u_4, u_8, u_6, u_6} (𝕜 := 𝕜) (𝕜' := 𝕜) (σ := RingHom.id 𝕜) ((B : (a : G) → E →L[𝕜] F) g) f) :
              α →ₘ[μ] F) :
          α → F)
        x :
      F)
    ((((B : (a : G) → E →L[𝕜] F) g : E →L[𝕜] F) : (a : E) → F) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F)
hh :
  Eq.{u_8 + 1} (α := F)
    ((↑(↑(compLp.{u_1, u_4, u_8, u_6, u_6} (𝕜 := 𝕜) (𝕜' := 𝕜) (σ := RingHom.id 𝕜) ((B : (a : G) → E →L[𝕜] F) h) f) :
              α →ₘ[μ] F) :
          α → F)
        x :
      F)
    ((((B : (a : G) → E →L[𝕜] F) h : E →L[𝕜] F) : (a : E) → F) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F)
hadd :
  (↑(↑(HAdd.hAdd (α := ↥(Lp F p μ))
                (compLp.{u_1, u_4, u_8, u_6, u_6} (𝕜 := 𝕜) (𝕜' := 𝕜) (σ := RingHom.id 𝕜) ((B : (a : G) → E →L[𝕜] F) g)
                  f)
                (compLp.{u_1, u_4, u_8, u_6, u_6} (𝕜 := 𝕜) (𝕜' := 𝕜) (σ := RingHom.id 𝕜) ((B : (a : G) → E →L[𝕜] F) h)
                  f)) :
            α →ₘ[μ] F) :
        α → F)
      x =
    HAdd.hAdd (α := α → F) (β := α → F)
      (↑(↑(compLp.{u_1, u_4, u_8, u_6, u_6} (𝕜 := 𝕜) (𝕜' := 𝕜) (σ := RingHom.id 𝕜) ((B : (a : G) → E →L[𝕜] F) g) f) :
            α →ₘ[μ] F) :
        α → F)
      (↑(↑(compLp.{u_1, u_4, u_8, u_6, u_6} (𝕜 := 𝕜) (𝕜' := 𝕜) (σ := RingHom.id 𝕜) ((B : (a : G) → E →L[𝕜] F) h) f) :
            α →ₘ[μ] F) :
        α → F)
      x
⊢ (((B : (a : G) → E →L[𝕜] F) (g + h) : E →L[𝕜] F) : (a : E) → F) ((↑(↑f : α →ₘ[μ] E) : α → E) x) =
    HAdd.hAdd (α := α → F) (β := α → F)
      (↑(↑(compLp.{u_1, u_4, u_8, u_6, u_6} (𝕜 := 𝕜) (𝕜' := 𝕜) (σ := RingHom.id 𝕜) ((B : (a : G) → E →L[𝕜] F) g) f) :
            α →ₘ[μ] F) :
        α → F)
      (↑(↑(compLp.{u_1, u_4, u_8, u_6, u_6} (𝕜 := 𝕜) (𝕜' := 𝕜) (σ := RingHom.id 𝕜) ((B : (a : G) → E →L[𝕜] F) h) f) :
            α →ₘ[μ] F) :
        α → F)
      x

Tactic:
simp only [map_add, add_apply, Pi.add_apply, hg, hh]

Premises used: map_add, ContinuousLinearMap.add_apply, Pi.add_apply
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
𝕜_1 : Type u_2
𝕜'_1 : Type u_3
E : Type u_4
F_1 : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F_1
g_1 : E → F_1
c_1 : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F_1
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
F : Type u_8
G : Type u_9
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
B : G →L[𝕜] E →L[𝕜] F
c : 𝕜
g : G
h :
  ∀ (f : ↥(Lp E p μ)),
    EventuallyEq.{u_1, u_8} (β := F) (ae μ)
      (↑(↑((compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) (c • g)) : (a : ↥(Lp E p μ)) → ↥(Lp F p μ)) f) : α →ₘ[μ] F) : α → F)
      (↑(↑((HSMul.hSMul (α := 𝕜) (β := ↥(Lp E p μ) →ₗ[𝕜] ↥(Lp F p μ)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
                    (compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) g)) :
                  (a : ↥(Lp E p μ)) → ↥(Lp F p μ))
                f) :
            α →ₘ[μ] F) :
        α → F)
⊢ compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) (c • g)) =
    HSMul.hSMul (α := 𝕜) (β := ↥(Lp E p μ) →ₗ[𝕜] ↥(Lp F p μ)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) g))

Tactic:
ext f
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
𝕜_1 : Type u_2
𝕜'_1 : Type u_3
E : Type u_4
F_1 : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F_1
g_1 : E → F_1
c_1 : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F_1
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
F : Type u_8
G : Type u_9
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
B : G →L[𝕜] E →L[𝕜] F
c : 𝕜
g : G
f : ↥(Lp E p μ)
h :
  ∀ (x : α)
    (hx :
      (↑(↑((HSMul.hSMul (β := E →L[𝕜] F) c ((B : (a : G) → E →L[𝕜] F) g : E →L[𝕜] F)).compLp f) : α →ₘ[μ] F) : α → F)
          x =
        (HSMul.hSMul (β := E →L[𝕜] F) c ((B : (a : G) → E →L[𝕜] F) g : E →L[𝕜] F) : (a : E) → F)
          ((↑(↑f : α →ₘ[μ] E) : α → E) x))
    (hg :
      Eq.{u_8 + 1} (α := F)
        ((↑(↑(compLp.{u_1, u_4, u_8, u_6, u_6} (𝕜 := 𝕜) (𝕜' := 𝕜) (σ := RingHom.id 𝕜) ((B : (a : G) → E →L[𝕜] F) g) f) :
                  α →ₘ[μ] F) :
              α → F)
            x :
          F)
        ((((B : (a : G) → E →L[𝕜] F) g : E →L[𝕜] F) : (a : E) → F) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F))
    (hsmul :
      (↑(↑(HSMul.hSMul (β := ↥(Lp F p μ)) c
                    (compLp.{u_1, u_4, u_8, u_6, u_6} (𝕜 := 𝕜) (𝕜' := 𝕜) (σ := RingHom.id 𝕜)
                      ((B : (a : G) → E →L[𝕜] F) g) f)) :
                α →ₘ[μ] F) :
            α → F)
          x =
        HSMul.hSMul (β := α → F) c
          (↑(↑(compLp.{u_1, u_4, u_8, u_6, u_6} (𝕜 := 𝕜) (𝕜' := 𝕜) (σ := RingHom.id 𝕜) ((B : (a : G) → E →L[𝕜] F) g)
                    f) :
                α →ₘ[μ] F) :
            α → F)
          x),
    Eq.{u_8 + 1} (α := F)
      ((↑(↑((compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) (c • g)) : (a : ↥(Lp E p μ)) → ↥(Lp F p μ)) f) : α →ₘ[μ] F) : α → F)
        x)
      ((↑(↑((HSMul.hSMul (α := 𝕜) (β := ↥(Lp E p μ) →ₗ[𝕜] ↥(Lp F p μ)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
                      (compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) g)) :
                    (a : ↥(Lp E p μ)) → ↥(Lp F p μ))
                  f) :
              α →ₘ[μ] F) :
          α → F)
        x)
⊢ EventuallyEq.{u_1, u_8} (β := F) (ae μ)
    (↑(↑((compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) (c • g)) : (a : ↥(Lp E p μ)) → ↥(Lp F p μ)) f) : α →ₘ[μ] F) : α → F)
    (↑(↑((HSMul.hSMul (α := 𝕜) (β := ↥(Lp E p μ) →ₗ[𝕜] ↥(Lp F p μ)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
                  (compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) g)) :
                (a : ↥(Lp E p μ)) → ↥(Lp F p μ))
              f) :
          α →ₘ[μ] F) :
      α → F)

Tactic:
filter_upwards [(c • B g).coeFn_compLp f, (B g).coeFn_compLp f,
      Lp.coeFn_smul c ((B g).compLp f)] with x hx hg hsmul

Premises used: MeasureTheory.Lp.coeFn_smul, ContinuousLinearMap.compLp, HSMul.hSMul, ContinuousLinearMap.coeFn_compLp, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
𝕜_1 : Type u_2
𝕜'_1 : Type u_3
E : Type u_4
F_1 : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F_1
g_1 : E → F_1
c_1 : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F_1
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
F : Type u_8
G : Type u_9
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
B : G →L[𝕜] E →L[𝕜] F
c : 𝕜
g : G
f : ↥(Lp E p μ)
x : α
hx :
  (↑(↑((HSMul.hSMul (β := E →L[𝕜] F) c ((B : (a : G) → E →L[𝕜] F) g : E →L[𝕜] F)).compLp f) : α →ₘ[μ] F) : α → F) x =
    (HSMul.hSMul (β := E →L[𝕜] F) c ((B : (a : G) → E →L[𝕜] F) g : E →L[𝕜] F) : (a : E) → F)
      ((↑(↑f : α →ₘ[μ] E) : α → E) x)
hg :
  Eq.{u_8 + 1} (α := F)
    ((↑(↑(compLp.{u_1, u_4, u_8, u_6, u_6} (𝕜 := 𝕜) (𝕜' := 𝕜) (σ := RingHom.id 𝕜) ((B : (a : G) → E →L[𝕜] F) g) f) :
              α →ₘ[μ] F) :
          α → F)
        x :
      F)
    ((((B : (a : G) → E →L[𝕜] F) g : E →L[𝕜] F) : (a : E) → F) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F)
hsmul :
  (↑(↑(HSMul.hSMul (β := ↥(Lp F p μ)) c
                (compLp.{u_1, u_4, u_8, u_6, u_6} (𝕜 := 𝕜) (𝕜' := 𝕜) (σ := RingHom.id 𝕜) ((B : (a : G) → E →L[𝕜] F) g)
                  f)) :
            α →ₘ[μ] F) :
        α → F)
      x =
    HSMul.hSMul (β := α → F) c
      (↑(↑(compLp.{u_1, u_4, u_8, u_6, u_6} (𝕜 := 𝕜) (𝕜' := 𝕜) (σ := RingHom.id 𝕜) ((B : (a : G) → E →L[𝕜] F) g) f) :
            α →ₘ[μ] F) :
        α → F)
      x
⊢ Eq.{u_8 + 1} (α := F)
    ((↑(↑((compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) (c • g)) : (a : ↥(Lp E p μ)) → ↥(Lp F p μ)) f) : α →ₘ[μ] F) : α → F)
      x)
    ((↑(↑((HSMul.hSMul (α := 𝕜) (β := ↥(Lp E p μ) →ₗ[𝕜] ↥(Lp F p μ)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
                    (compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) g)) :
                  (a : ↥(Lp E p μ)) → ↥(Lp F p μ))
                f) :
            α →ₘ[μ] F) :
        α → F)
      x)

Tactic:
simp [hx, hsmul, hg]
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
𝕜_1 : Type u_2
𝕜'_1 : Type u_3
E : Type u_4
F_1 : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F_1
g : E → F_1
c_1 : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F_1
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
F : Type u_8
G : Type u_9
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
inst_11 : Fact (1 ≤ p)
B : G →L[𝕜] E →L[𝕜] F
c : G
f : ↥(Lp E p μ)
simp :
  norm (E := ↥(Lp F p μ))
      (compLp.{u_1, u_4, u_8, u_6, u_6} (𝕜 := 𝕜) (𝕜' := 𝕜) (σ := RingHom.id 𝕜) ((B : (a : G) → E →L[𝕜] F) c) f) ≤
    ‖B‖ * ‖c‖ * ‖f‖
⊢ norm (E := ↥(Lp F p μ))
      ((((compLpₗ₂ p μ B : (a : G) → ↥(Lp E p μ) →ₗ[𝕜] ↥(Lp F p μ)) c : ↥(Lp E p μ) →ₗ[𝕜] ↥(Lp F p μ)) :
            (a : ↥(Lp E p μ)) → ↥(Lp F p μ))
          f :
        ↥(Lp F p μ)) ≤
    ‖B‖ * ‖c‖ * ‖f‖

Tactic:
simp only [compLpₗ₂_apply, compLpₗ_apply]

Premises used: ContinuousLinearMap.compLpₗ_apply, ContinuousLinearMap.compLpₗ₂_apply
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
𝕜_1 : Type u_2
𝕜'_1 : Type u_3
E : Type u_4
F_1 : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F_1
g : E → F_1
c_1 : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F_1
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
F : Type u_8
G : Type u_9
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
inst_11 : Fact (1 ≤ p)
B : G →L[𝕜] E →L[𝕜] F
c : G
f : ↥(Lp E p μ)
grw : norm (E := E →L[𝕜] F) ((B : (a : G) → E →L[𝕜] F) c : E →L[𝕜] F) * ‖f‖ ≤ ‖B‖ * ‖c‖ * ‖f‖
grw₁ grw₂ : ‖B‖ * ‖c‖ * ‖f‖ ≤ ‖B‖ * ‖c‖ * ‖f‖
⊢ norm (E := ↥(Lp F p μ))
      (compLp.{u_1, u_4, u_8, u_6, u_6} (𝕜 := 𝕜) (𝕜' := 𝕜) (σ := RingHom.id 𝕜) ((B : (a : G) → E →L[𝕜] F) c) f) ≤
    ‖B‖ * ‖c‖ * ‖f‖

Tactic:
grw [norm_compLp_le, le_opNorm]

Premises used: ContinuousLinearMap.norm_compLp_le, ContinuousLinearMap.le_opNorm
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
𝕜 : Type u_6
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
F : Type u_8
G : Type u_9
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fact (1 ≤ p)
B : G →L[𝕜] E →L[𝕜] F
g : G
f : ↥(Lp E p μ)
⊢ Eq (α := ↥(Lp F p μ))
    ((((compLpL₂ p μ B : (a : G) → ↥(Lp E p μ) →L[𝕜] ↥(Lp F p μ)) g : ↥(Lp E p μ) →L[𝕜] ↥(Lp F p μ)) :
          (a : ↥(Lp E p μ)) → ↥(Lp F p μ))
        f :
      ↥(Lp F p μ))
    (compLp.{u_1, u_4, u_8, u_6, u_6} (𝕜 := 𝕜) (𝕜' := 𝕜) (σ := RingHom.id 𝕜) ((B : (a : G) → E →L[𝕜] F) g) f :
      ↥(Lp F p μ))

Tactic:
rfl

Premises used: ContinuousLinearMap.compLp, rfl, LipschitzWith.compLp