awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
F : Type u_5
inst_2 : AddCommMonoid F
inst_3 : TopologicalSpace F
inst_4 : T2Space F
inst_5 : Fact (1 ≤ p)
hp : p ≠ ∞
f g : ↥(lp E p) →ₜ+ F
h : ∀ (i : α), f.comp (singleContinuousAddMonoidHom E p i) = g.comp (singleContinuousAddMonoidHom E p i)
x : ↥(lp E p)
h₁ h₂ h₃ :
  ∀ (this : HasSum (fun (i : α) ↦ lp.single (E := E) p i ((↑x : (i : α) → E i) i)) x),
    Eq.{u_5 + 1} (α := F) ((f : (a : ↥(lp E p)) → F) x : F) ((g : (a : ↥(lp E p)) → F) x : F)
h₄ :
  ∀ (this : HasSum (fun (i : α) ↦ lp.single (E := E) p i ((↑x : (i : α) → E i) i)) x),
    Eq.{u_5 + 1} (α := F)
      (∑' (b : α),
        Function.comp (β := ↥(lp E p)) (⇑f : (a : ↥(lp E p)) → F)
          (fun (i : α) ↦ lp.single (E := E) p i ((↑x : (i : α) → E i) i)) b)
      (∑' (b : α),
        Function.comp (β := ↥(lp E p)) (⇑g : (a : ↥(lp E p)) → F)
          (fun (i : α) ↦ lp.single (E := E) p i ((↑x : (i : α) → E i) i)) b)
h₅ :
  ∀ (this : HasSum (fun (i : α) ↦ lp.single (E := E) p i ((↑x : (i : α) → E i) i)) x) (i : α),
    Eq.{u_5 + 1} (α := F)
      (Function.comp (β := ↥(lp E p)) (⇑f : (a : ↥(lp E p)) → F)
        (fun (i : α) ↦ lp.single (E := E) p i ((↑x : (i : α) → E i) i)) i)
      (Function.comp (β := ↥(lp E p)) (⇑g : (a : ↥(lp E p)) → F)
        (fun (i : α) ↦ lp.single (E := E) p i ((↑x : (i : α) → E i) i)) i)
⊢ Eq.{u_5 + 1} (α := F) ((f : (a : ↥(lp E p)) → F) x : F) ((g : (a : ↥(lp E p)) → F) x : F)

Tactic:
classical
  have := lp.hasSum_single hp x
  rw [← (this.map f f.continuous).tsum_eq, ← (this.map g g.continuous).tsum_eq]
  congr! 2 with i
  exact DFunLike.congr_fun (h i) (x i)
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
inst_4 : DecidableEq α
F : Type u_5
inst_5 : AddCommMonoid F
inst_6 : Module 𝕜 F
inst_7 : TopologicalSpace F
inst_8 : T2Space F
inst_9 : Fact (1 ≤ p)
hp : p ≠ ∞
f g : ↥(lp E p) →L[𝕜] F
h : ∀ (i : α), f ∘SL singleContinuousLinearMap 𝕜 E p i = g ∘SL singleContinuousLinearMap 𝕜 E p i
⊢ f = g

Tactic:
ContinuousLinearMap.toContinuousAddMonoidHom_injective <|
    ext_continuousAddMonoidHom hp fun i => ContinuousLinearMap.toContinuousAddMonoidHom_inj.2 (h i)

Premises used: Iff.mpr, ContinuousLinearMap.toContinuousAddMonoidHom_injective, ContinuousLinearMap.toContinuousAddMonoidHom_inj, lp.ext_continuousAddMonoidHom
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p_1 q_1 : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
p q r : ℝ≥0∞
h : p ≤ q
x x_1 : ↥(lp E p)
h₁ :
  ∀ (x_2 : α),
    (↑(Subtype.mk (p := fun (x : PreLp E) ↦ Membership.mem (γ := AddSubgroup (PreLp E)) (lp E q) x)
              (↑(x + x_1) : PreLp E) ⋯) :
          (i : α) → E i)
        x_2 =
      (↑(HAdd.hAdd (α := ↥(lp E q))
              (Subtype.mk (p := fun (x : PreLp E) ↦ Membership.mem (γ := AddSubgroup (PreLp E)) (lp E q) x)
                (↑x : PreLp E) ⋯)
              (Subtype.mk (p := fun (x : PreLp E) ↦ Membership.mem (γ := AddSubgroup (PreLp E)) (lp E q) x)
                (↑x_1 : PreLp E) ⋯)) :
          (i : α) → E i)
        x_2
⊢ Subtype.mk (p := fun (x : PreLp E) ↦ Membership.mem (γ := AddSubgroup (PreLp E)) (lp E q) x) (↑(x + x_1) : PreLp E)
      ⋯ =
    HAdd.hAdd (α := ↥(lp E q))
      (Subtype.mk (p := fun (x : PreLp E) ↦ Membership.mem (γ := AddSubgroup (PreLp E)) (lp E q) x) (↑x : PreLp E) ⋯)
      (Subtype.mk (p := fun (x : PreLp E) ↦ Membership.mem (γ := AddSubgroup (PreLp E)) (lp E q) x) (↑x_1 : PreLp E) ⋯)

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p_1 q_1 : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
p q r : ℝ≥0∞
h : p ≤ q
x x_1 : ↥(lp E p)
x_2 : α
⊢ (↑(Subtype.mk (p := fun (x : PreLp E) ↦ Membership.mem (γ := AddSubgroup (PreLp E)) (lp E q) x) (↑(x + x_1) : PreLp E)
            ⋯) :
        (i : α) → E i)
      x_2 =
    (↑(HAdd.hAdd (α := ↥(lp E q))
            (Subtype.mk (p := fun (x : PreLp E) ↦ Membership.mem (γ := AddSubgroup (PreLp E)) (lp E q) x) (↑x : PreLp E)
              ⋯)
            (Subtype.mk (p := fun (x : PreLp E) ↦ Membership.mem (γ := AddSubgroup (PreLp E)) (lp E q) x)
              (↑x_1 : PreLp E) ⋯)) :
        (i : α) → E i)
      x_2

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p_1 q_1 : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
p q r : ℝ≥0∞
h : p ≤ q
x : 𝕜
x_1 : ↥(lp E p)
h₁ :
  ∀ (x_2 : α),
    (↑(Subtype.mk (p := fun (x : PreLp E) ↦ Membership.mem (γ := AddSubgroup (PreLp E)) (lp E q) x)
              (↑(x • x_1) : PreLp E) ⋯) :
          (i : α) → E i)
        x_2 =
      (↑(HSMul.hSMul (α := 𝕜) (β := ↥(lp E q)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
              (Subtype.mk (p := fun (x : PreLp E) ↦ Membership.mem (γ := AddSubgroup (PreLp E)) (lp E q) x)
                (↑x_1 : PreLp E) ⋯)) :
          (i : α) → E i)
        x_2
⊢ Subtype.mk (p := fun (x : PreLp E) ↦ Membership.mem (γ := AddSubgroup (PreLp E)) (lp E q) x) (↑(x • x_1) : PreLp E)
      ⋯ =
    HSMul.hSMul (α := 𝕜) (β := ↥(lp E q)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
      (Subtype.mk (p := fun (x : PreLp E) ↦ Membership.mem (γ := AddSubgroup (PreLp E)) (lp E q) x) (↑x_1 : PreLp E) ⋯)

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p_1 q_1 : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
p q r : ℝ≥0∞
h : p ≤ q
x : 𝕜
x_1 : ↥(lp E p)
x_2 : α
⊢ (↑(Subtype.mk (p := fun (x : PreLp E) ↦ Membership.mem (γ := AddSubgroup (PreLp E)) (lp E q) x) (↑(x • x_1) : PreLp E)
            ⋯) :
        (i : α) → E i)
      x_2 =
    (↑(HSMul.hSMul (α := 𝕜) (β := ↥(lp E q)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
            (Subtype.mk (p := fun (x : PreLp E) ↦ Membership.mem (γ := AddSubgroup (PreLp E)) (lp E q) x)
              (↑x_1 : PreLp E) ⋯)) :
        (i : α) → E i)
      x_2

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
p q : ℝ≥0∞
h : p ≤ q
f : ↥(lp E p)
h₁ : ∀ (x : α), (↑((linearMapOfLE 𝕜 E h : (a : ↥(lp E p)) → ↥(lp E q)) f) : (i : α) → E i) x = (↑f : (i : α) → E i) x
⊢ (↑((linearMapOfLE 𝕜 E h : (a : ↥(lp E p)) → ↥(lp E q)) f) : (i : α) → E i) = (↑f : (i : α) → E i)

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
p q : ℝ≥0∞
h : p ≤ q
f : ↥(lp E p)
x : α
⊢ (↑((linearMapOfLE 𝕜 E h : (a : ↥(lp E p)) → ↥(lp E q)) f) : (i : α) → E i) x = (↑f : (i : α) → E i) x

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
p q : ℝ≥0∞
h : p ≤ q
h₁ :
  ∀ (x : ↥(lp E p)) (x_1 : α),
    Eq.{u_4 + 1} (α := E x_1)
      ((↑((LinearMap.toAddMonoidHom (modM₁ := instModuleSubtypePreLpMemAddSubgroup (E := E)) (linearMapOfLE 𝕜 E h) :
                (a : ↥(lp E p)) → ↥(lp E q))
              x) :
          (i : α) → E i)
        x_1)
      ((↑((AddSubgroup.inclusion ⋯ : (a : ↥(lp E p)) → ↥(lp E q)) x) : (i : α) → E i) x_1)
⊢ Eq (α := ↥(lp E p) →+ ↥(lp E q))
    (LinearMap.toAddMonoidHom (modM₁ := instModuleSubtypePreLpMemAddSubgroup (E := E)) (linearMapOfLE 𝕜 E h))
    (AddSubgroup.inclusion ⋯)

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
p q : ℝ≥0∞
h : p ≤ q
x : ↥(lp E p)
x_1 : α
⊢ Eq.{u_4 + 1} (α := E x_1)
    ((↑((LinearMap.toAddMonoidHom (modM₁ := instModuleSubtypePreLpMemAddSubgroup (E := E)) (linearMapOfLE 𝕜 E h) :
              (a : ↥(lp E p)) → ↥(lp E q))
            x) :
        (i : α) → E i)
      x_1)
    ((↑((AddSubgroup.inclusion ⋯ : (a : ↥(lp E p)) → ↥(lp E q)) x) : (i : α) → E i) x_1)

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
p q r : ℝ≥0∞
hpq : p ≤ q
hqr : q ≤ r
h :
  ∀ (x : ↥(lp E p)) (x_1 : α),
    Eq.{u_4 + 1} (α := E x_1)
      ((↑((linearMapOfLE 𝕜 E hqr ∘ₗ linearMapOfLE 𝕜 E hpq : (a : ↥(lp E p)) → ↥(lp E r)) x) : (i : α) → E i) x_1)
      ((↑((linearMapOfLE 𝕜 E ⋯ : (a : ↥(lp E p)) → ↥(lp E r)) x) : (i : α) → E i) x_1)
⊢ Eq (α := ↥(lp E p) →ₗ[𝕜] ↥(lp E r)) (linearMapOfLE 𝕜 E hqr ∘ₗ linearMapOfLE 𝕜 E hpq) (linearMapOfLE 𝕜 E ⋯)

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
p q r : ℝ≥0∞
hpq : p ≤ q
hqr : q ≤ r
x : ↥(lp E p)
x_1 : α
⊢ Eq.{u_4 + 1} (α := E x_1)
    ((↑((linearMapOfLE 𝕜 E hqr ∘ₗ linearMapOfLE 𝕜 E hpq : (a : ↥(lp E p)) → ↥(lp E r)) x) : (i : α) → E i) x_1)
    ((↑((linearMapOfLE 𝕜 E ⋯ : (a : ↥(lp E p)) → ↥(lp E r)) x) : (i : α) → E i) x_1)

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p_1 q_1 : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
p q r : ℝ≥0∞
inst_4 : Fact (1 ≤ p)
i : α
x : ↥(lp E p)
⊢ p ≠ 0

Tactic:
have hp : p ≠ 0 := zero_lt_one.trans_le Fact.out |>.ne'
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p_1 q_1 : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
p q r : ℝ≥0∞
inst_4 : Fact (1 ≤ p)
i : α
x : ↥(lp E p)
hp : p ≠ 0
⊢ norm.{u_4} (E := E i) ((evalₗ E p i : (a : ↥(lp E p)) → E i) x : E i) ≤ 1 * ‖x‖

Tactic:
simpa only [evalₗ_apply, one_mul, ge_iff_le] using norm_apply_le_norm hp x i

Premises used: lp.norm_apply_le_norm, lp.evalₗ_apply, ge_iff_le, one_mul
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
⊢ UniformContinuous (α := ↥(lp E p))
    (Subtype.val (p := fun (x : PreLp E) ↦ Membership.mem (γ := AddSubgroup (PreLp E)) (lp E p) x))

Tactic:
uniformContinuous_pi.2 fun i ↦ (lipschitzWith_one_eval p i).uniformContinuous

Premises used: Iff.mpr, lp.lipschitzWith_one_eval, LipschitzWith.uniformContinuous, uniformContinuous_pi
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
C : ℝ
F : ι → ↥(lp E ∞)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
a : α
⊢ Tendsto (fun (k : ι) ↦ ‖(↑(F k) : (i : α) → E i) a‖) l (𝓝 ‖f a‖)

Tactic:
have : Tendsto (fun k => ‖F k a‖) l (𝓝 ‖f a‖) :=
    (Tendsto.comp (continuous_apply a).continuousAt hf).norm
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
C : ℝ
F : ι → ↥(lp E ∞)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
a : α
this : Tendsto (fun (k : ι) ↦ ‖(↑(F k) : (i : α) → E i) a‖) l (𝓝 ‖f a‖)
⊢ ‖f a‖ ≤ C

Tactic:
le_of_tendsto this (hCF.mono ?_)

Premises used: le_of_tendsto, Filter.Eventually.mono
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
C : ℝ
F : ι → ↥(lp E ∞)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
a : α
this : Tendsto (fun (k : ι) ↦ ‖(↑(F k) : (i : α) → E i) a‖) l (𝓝 ‖f a‖)
refine : ∀ (x : ι), ‖F x‖ ≤ C → ‖(↑(F x) : (i : α) → E i) a‖ ≤ C
⊢ ‖f a‖ ≤ C

Tactic:
refine le_of_tendsto this (hCF.mono ?_)

Premises used: le_of_tendsto, Filter.Eventually.mono
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
C : ℝ
F : ι → ↥(lp E ∞)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
a : α
this : Tendsto (fun (k : ι) ↦ ‖(↑(F k) : (i : α) → E i) a‖) l (𝓝 ‖f a‖)
k : ι
hCFk : ‖F k‖ ≤ C
⊢ ‖(↑(F k) : (i : α) → E i) a‖ ≤ C

Tactic:
(norm_apply_le_norm ENNReal.top_ne_zero (F k) a).trans hCFk

Premises used: lp.norm_apply_le_norm, LE.le.trans, ENNReal.top_ne_zero
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
C : ℝ
F : ι → ↥(lp E ∞)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
a : α
this : Tendsto (fun (k : ι) ↦ ‖(↑(F k) : (i : α) → E i) a‖) l (𝓝 ‖f a‖)
k : ι
hCFk : ‖F k‖ ≤ C
⊢ ‖(↑(F k) : (i : α) → E i) a‖ ≤ C

Tactic:
exact (norm_apply_le_norm ENNReal.top_ne_zero (F k) a).trans hCFk

Premises used: lp.norm_apply_le_norm, LE.le.trans, ENNReal.top_ne_zero
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
hp : p ≠ ∞
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
s : Finset α
⊢ p ≠ 0

Tactic:
have hp' : p ≠ 0 := (zero_lt_one.trans_le _i.elim).ne'
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
hp : p ≠ ∞
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
s : Finset α
hp' : p ≠ 0
⊢ 0 < p.toReal

Tactic:
have hp'' : 0 < p.toReal := ENNReal.toReal_pos hp' hp
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
hp : p ≠ ∞
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
s : Finset α
hp' : p ≠ 0
hp'' : 0 < p.toReal
G : ((a : α) → E a) → ℝ := fun (f : (a : α) → E a) ↦ ∑ a ∈ s, ‖f a‖ ^ p.toReal
⊢ Continuous[Pi.topologicalSpace, _] G

Tactic:
continuous_finsetSum s ?_

Premises used: continuous_finsetSum
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
hp : p ≠ ∞
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
s : Finset α
hp' : p ≠ 0
hp'' : 0 < p.toReal
G : ((a : α) → E a) → ℝ := fun (f : (a : α) → E a) ↦ ∑ a ∈ s, ‖f a‖ ^ p.toReal
refine : ∀ i ∈ s, Continuous[Pi.topologicalSpace, _] fun (f : (a : α) → E a) ↦ ‖f i‖ ^ p.toReal
⊢ Continuous[Pi.topologicalSpace, _] G

Tactic:
refine continuous_finsetSum s ?_

Premises used: continuous_finsetSum
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
hp : p ≠ ∞
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
s : Finset α
hp' : p ≠ 0
hp'' : 0 < p.toReal
G : ((a : α) → E a) → ℝ := fun (f : (a : α) → E a) ↦ ∑ a ∈ s, ‖f a‖ ^ p.toReal
a : α
_ : a ∈ s → Continuous[Pi.topologicalSpace, _] fun (f : (a : α) → E a) ↦ ‖f a‖ ^ p.toReal
⊢ a ∈ s → Continuous[Pi.topologicalSpace, _] fun (f : (a : α) → E a) ↦ ‖f a‖ ^ p.toReal

Tactic:
_
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
hp : p ≠ ∞
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
s : Finset α
hp' : p ≠ 0
hp'' : 0 < p.toReal
G : ((a : α) → E a) → ℝ := fun (f : (a : α) → E a) ↦ ∑ a ∈ s, ‖f a‖ ^ p.toReal
a : α
h : a ∈ s
⊢ Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : (a : α) → E a) ↦ f a

Tactic:
have : Continuous fun f : ∀ a, E a => f a := continuous_apply a
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
hp : p ≠ ∞
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
s : Finset α
hp' : p ≠ 0
hp'' : 0 < p.toReal
G : ((a : α) → E a) → ℝ := fun (f : (a : α) → E a) ↦ ∑ a ∈ s, ‖f a‖ ^ p.toReal
a : α
h : a ∈ s
this :
  Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : (a : α) → E a) ↦ f a
⊢ Continuous[Pi.topologicalSpace, _] fun (f : (a : α) → E a) ↦ ‖f a‖ ^ p.toReal

Tactic:
this.norm.rpow_const fun _ => Or.inr hp''.le

Premises used: LT.lt.le, Continuous.norm, Continuous.rpow_const, Or.inr
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
hp : p ≠ ∞
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
s : Finset α
hp' : p ≠ 0
hp'' : 0 < p.toReal
G : ((a : α) → E a) → ℝ := fun (f : (a : α) → E a) ↦ ∑ a ∈ s, ‖f a‖ ^ p.toReal
a : α
h : a ∈ s
this :
  Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : (a : α) → E a) ↦ f a
⊢ Continuous[Pi.topologicalSpace, _] fun (f : (a : α) → E a) ↦ ‖f a‖ ^ p.toReal

Tactic:
exact this.norm.rpow_const fun _ => Or.inr hp''.le

Premises used: LT.lt.le, Continuous.norm, Continuous.rpow_const, Or.inr
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
hp : p ≠ ∞
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
s : Finset α
hp' : p ≠ 0
hp'' : 0 < p.toReal
G : ((a : α) → E a) → ℝ := fun (f : (a : α) → E a) ↦ ∑ a ∈ s, ‖f a‖ ^ p.toReal
⊢ Continuous[Pi.topologicalSpace, _] G

Tactic:
have hG : Continuous G := by
    refine continuous_finsetSum s ?_
    intro a _
    have : Continuous fun f : ∀ a, E a => f a := continuous_apply a
    exact this.norm.rpow_const fun _ => Or.inr hp''.le
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
hp : p ≠ ∞
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
s : Finset α
hp' : p ≠ 0
hp'' : 0 < p.toReal
G : ((a : α) → E a) → ℝ := fun (f : (a : α) → E a) ↦ ∑ a ∈ s, ‖f a‖ ^ p.toReal
hG : Continuous[Pi.topologicalSpace, _] G
⊢ ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C ^ p.toReal

Tactic:
le_of_tendsto (hG.continuousAt.tendsto.comp hf) ?_

Premises used: le_of_tendsto, Continuous.continuousAt, ContinuousAt.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
hp : p ≠ ∞
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
s : Finset α
hp' : p ≠ 0
hp'' : 0 < p.toReal
G : ((a : α) → E a) → ℝ := fun (f : (a : α) → E a) ↦ ∑ a ∈ s, ‖f a‖ ^ p.toReal
hG : Continuous[Pi.topologicalSpace, _] G
refine : ∀ᶠ (c : ι) in l, (G ∘ id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) c ≤ C ^ p.toReal
⊢ ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C ^ p.toReal

Tactic:
refine le_of_tendsto (hG.continuousAt.tendsto.comp hf) ?_

Premises used: le_of_tendsto, Continuous.continuousAt, ContinuousAt.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
hp : p ≠ ∞
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
s : Finset α
hp' : p ≠ 0
hp'' : 0 < p.toReal
G : ((a : α) → E a) → ℝ := fun (f : (a : α) → E a) ↦ ∑ a ∈ s, ‖f a‖ ^ p.toReal
hG : Continuous[Pi.topologicalSpace, _] G
⊢ ∀ᶠ (c : ι) in l, (G ∘ id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) c ≤ C ^ p.toReal

Tactic:
hCF.mono ?_

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
hp : p ≠ ∞
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
s : Finset α
hp' : p ≠ 0
hp'' : 0 < p.toReal
G : ((a : α) → E a) → ℝ := fun (f : (a : α) → E a) ↦ ∑ a ∈ s, ‖f a‖ ^ p.toReal
hG : Continuous[Pi.topologicalSpace, _] G
refine : ∀ (x : ι), ‖F x‖ ≤ C → (G ∘ id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) x ≤ C ^ p.toReal
⊢ ∀ᶠ (c : ι) in l, (G ∘ id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) c ≤ C ^ p.toReal

Tactic:
refine hCF.mono ?_

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
hp : p ≠ ∞
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
s : Finset α
hp' : p ≠ 0
hp'' : 0 < p.toReal
G : ((a : α) → E a) → ℝ := fun (f : (a : α) → E a) ↦ ∑ a ∈ s, ‖f a‖ ^ p.toReal
hG : Continuous[Pi.topologicalSpace, _] G
k : ι
hCFk : ‖F k‖ ≤ C
⊢ (G ∘ id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) k ≤ C ^ p.toReal

Tactic:
(lp.sum_rpow_le_norm_rpow hp'' (F k) s).trans ?_

Premises used: Multiset.sum, Multiset.foldr, lp.sum_rpow_le_norm_rpow, LE.le.trans, Finset.sum