awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
hpq : p.toReal.HolderConjugate q.toReal
f : ↥(lp E p)
g : ↥(lp E q)
hf₁ : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖
hg₁ : ∀ (i : α), 0 ≤ ‖(↑g : (i : α) → E i) i‖
hf₂ : HasSum (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (‖f‖ ^ p.toReal)
hg₂ : HasSum (fun (i : α) ↦ ‖(↑g : (i : α) → E i) i‖ ^ q.toReal) (‖g‖ ^ q.toReal)
obtain :
  ∀ (C : ℝ) (hC' : C ≤ ‖f‖ * ‖g‖) (hC : HasSum (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ * ‖(↑g : (i : α) → E i) i‖) C),
    (Summable (α := ℝ) fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ * ‖(↑g : (i : α) → E i) i‖) ∧
      ∑' (i : α), ‖(↑f : (i : α) → E i) i‖ * ‖(↑g : (i : α) → E i) i‖ ≤ ‖f‖ * ‖g‖
⊢ (Summable (α := ℝ) fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ * ‖(↑g : (i : α) → E i) i‖) ∧
    ∑' (i : α), ‖(↑f : (i : α) → E i) i‖ * ‖(↑g : (i : α) → E i) i‖ ≤ ‖f‖ * ‖g‖

Tactic:
obtain ⟨C, -, hC', hC⟩ :=
    Real.inner_le_Lp_mul_Lq_hasSum_of_nonneg hpq (norm_nonneg' _) (norm_nonneg' _) hf₁ hg₁ hf₂ hg₂

Premises used: Real.inner_le_Lp_mul_Lq_hasSum_of_nonneg, lp.norm_nonneg'
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
hpq : p.toReal.HolderConjugate q.toReal
f : ↥(lp E p)
g : ↥(lp E q)
hf₁ : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖
hg₁ : ∀ (i : α), 0 ≤ ‖(↑g : (i : α) → E i) i‖
hf₂ : HasSum (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (‖f‖ ^ p.toReal)
hg₂ : HasSum (fun (i : α) ↦ ‖(↑g : (i : α) → E i) i‖ ^ q.toReal) (‖g‖ ^ q.toReal)
C : ℝ
hC' : C ≤ ‖f‖ * ‖g‖
hC : HasSum (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ * ‖(↑g : (i : α) → E i) i‖) C
⊢ ∑' (b : α), ‖(↑f : (i : α) → E i) b‖ * ‖(↑g : (i : α) → E i) b‖ ≤ ‖f‖ * ‖g‖

Tactic:
rw [← hC.tsum_eq] at hC'

Premises used: HasSum.tsum_eq
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
hpq : p.toReal.HolderConjugate q.toReal
f : ↥(lp E p)
g : ↥(lp E q)
hf₁ : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖
hg₁ : ∀ (i : α), 0 ≤ ‖(↑g : (i : α) → E i) i‖
hf₂ : HasSum (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (‖f‖ ^ p.toReal)
hg₂ : HasSum (fun (i : α) ↦ ‖(↑g : (i : α) → E i) i‖ ^ q.toReal) (‖g‖ ^ q.toReal)
C : ℝ
hC' : C ≤ ‖f‖ * ‖g‖
hC : HasSum (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ * ‖(↑g : (i : α) → E i) i‖) C
hC'₁ : ∑' (b : α), ‖(↑f : (i : α) → E i) b‖ * ‖(↑g : (i : α) → E i) b‖ ≤ ‖f‖ * ‖g‖
⊢ HasSum (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ * ‖(↑g : (i : α) → E i) i‖) C

Tactic:
rw [← hC.tsum_eq] at hC'

Premises used: HasSum.tsum_eq
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
hpq : p.toReal.HolderConjugate q.toReal
f : ↥(lp E p)
g : ↥(lp E q)
hf₁ : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖
hg₁ : ∀ (i : α), 0 ≤ ‖(↑g : (i : α) → E i) i‖
hf₂ : HasSum (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (‖f‖ ^ p.toReal)
hg₂ : HasSum (fun (i : α) ↦ ‖(↑g : (i : α) → E i) i‖ ^ q.toReal) (‖g‖ ^ q.toReal)
C : ℝ
hC' : ∑' (b : α), ‖(↑f : (i : α) → E i) b‖ * ‖(↑g : (i : α) → E i) b‖ ≤ ‖f‖ * ‖g‖
hC : HasSum (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ * ‖(↑g : (i : α) → E i) i‖) C
⊢ (Summable (α := ℝ) fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ * ‖(↑g : (i : α) → E i) i‖) ∧
    ∑' (i : α), ‖(↑f : (i : α) → E i) i‖ * ‖(↑g : (i : α) → E i) i‖ ≤ ‖f‖ * ‖g‖

Tactic:
⟨hC.summable, hC'⟩

Premises used: HasSum.summable, And.intro
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
hpq : p.toReal.HolderConjugate q.toReal
f : ↥(lp E p)
g : ↥(lp E q)
hf₁ : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖
hg₁ : ∀ (i : α), 0 ≤ ‖(↑g : (i : α) → E i) i‖
hf₂ : HasSum (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (‖f‖ ^ p.toReal)
hg₂ : HasSum (fun (i : α) ↦ ‖(↑g : (i : α) → E i) i‖ ^ q.toReal) (‖g‖ ^ q.toReal)
C : ℝ
hC' : ∑' (b : α), ‖(↑f : (i : α) → E i) b‖ * ‖(↑g : (i : α) → E i) b‖ ≤ ‖f‖ * ‖g‖
hC : HasSum (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ * ‖(↑g : (i : α) → E i) i‖) C
⊢ (Summable (α := ℝ) fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ * ‖(↑g : (i : α) → E i) i‖) ∧
    ∑' (i : α), ‖(↑f : (i : α) → E i) i‖ * ‖(↑g : (i : α) → E i) i‖ ≤ ‖f‖ * ‖g‖

Tactic:
exact ⟨hC.summable, hC'⟩
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
hpq : p.toReal.HolderConjugate q.toReal
f : ↥(lp E p)
g : ↥(lp E q)
⊢ Summable (α := ℝ) fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ * ‖(↑g : (i : α) → E i) i‖

Tactic:
(lp.tsum_mul_le_mul_norm hpq f g).1

Premises used: And.left, lp.tsum_mul_le_mul_norm
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
hpq : p.toReal.HolderConjugate q.toReal
f : ↥(lp E p)
g : ↥(lp E q)
⊢ ∑' (i : α), ‖(↑f : (i : α) → E i) i‖ * ‖(↑g : (i : α) → E i) i‖ ≤ ‖f‖ * ‖g‖

Tactic:
(lp.tsum_mul_le_mul_norm hpq f g).2

Premises used: And.right, lp.tsum_mul_le_mul_norm
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : p ≠ 0
f : ↥(lp E p)
i : α
inl : ∀ (hp : Ne (α := ℝ≥0∞) ∞ 0) (f : ↥(lp E ∞)), ‖(↑f : (i : α) → E i) i‖ ≤ ‖f‖
inr : ∀ (hp' : p ≠ ∞), ‖(↑f : (i : α) → E i) i‖ ≤ ‖f‖
⊢ ‖(↑f : (i : α) → E i) i‖ ≤ ‖f‖

Tactic:
rcases eq_or_ne p ∞ with (rfl | hp')

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
i : α
hp : Ne (α := ℝ≥0∞) ∞ 0
f : ↥(lp E ∞)
⊢ Nonempty α

Tactic:
haveI : Nonempty α := ⟨i⟩
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
i : α
hp : Ne (α := ℝ≥0∞) ∞ 0
f : ↥(lp E ∞)
this : Nonempty α
⊢ ‖(↑f : (i : α) → E i) i‖ ≤ ‖f‖

Tactic:
(isLUB_norm f).1 ⟨i, rfl⟩

Premises used: lp.isLUB_norm, And.left, Exists.intro, rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
i : α
hp : Ne (α := ℝ≥0∞) ∞ 0
f : ↥(lp E ∞)
this : Nonempty α
⊢ ‖(↑f : (i : α) → E i) i‖ ≤ ‖f‖

Tactic:
exact (isLUB_norm f).1 ⟨i, rfl⟩

Premises used: lp.isLUB_norm, And.left, Exists.intro, rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : p ≠ 0
f : ↥(lp E p)
i : α
hp' : p ≠ ∞
⊢ 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)
hp : p ≠ 0
f : ↥(lp E p)
i_1 : α
hp' : p ≠ ∞
hp'' : 0 < p.toReal
i : α
⊢ 0 ≤ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : p ≠ 0
f : ↥(lp E p)
i : α
hp' : p ≠ ∞
hp'' : 0 < p.toReal
⊢ ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal

Tactic:
have : ∀ i, 0 ≤ ‖f i‖ ^ p.toReal := fun i ↦ by positivity
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : p ≠ 0
f : ↥(lp E p)
i : α
hp' : p ≠ ∞
hp'' : 0 < p.toReal
this : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
inr : ‖(↑f : (i : α) → E i) i‖ ^ p.toReal ≤ ‖f‖ ^ p.toReal
⊢ ‖(↑f : (i : α) → E i) i‖ ≤ ‖f‖

Tactic:
rw [← Real.rpow_le_rpow_iff (norm_nonneg _) (norm_nonneg' _) hp'']

Premises used: lp.norm_nonneg', Real.rpow_le_rpow_iff, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : p ≠ 0
f : ↥(lp E p)
i : α
hp' : p ≠ ∞
hp'' : 0 < p.toReal
this : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
⊢ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal ≤ ‖f‖ ^ p.toReal

Tactic:
le_hasSum (hasSum_norm hp'' f) i fun i _ => this i

Premises used: le_hasSum, lp.hasSum_norm
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : p ≠ 0
f : ↥(lp E p)
i : α
hp' : p ≠ ∞
hp'' : 0 < p.toReal
this : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
⊢ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal ≤ ‖f‖ ^ p.toReal

Tactic:
convert! le_hasSum (hasSum_norm hp'' f) i fun i _ => this i

Premises used: le_hasSum, lp.hasSum_norm
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst_1 : Fact (1 ≤ p)
i : α
x x_1 : ↥(lp E p)
simp_rw : ‖(↑(x - x_1) : (i : α) → E i) i‖ ≤ ‖x - x_1‖
⊢ dist ((↑x : (i : α) → E i) i) ((↑x_1 : (i : α) → E i) i) ≤ dist x x_1

Tactic:
simp_rw [dist_eq_norm, ← Pi.sub_apply, ← lp.coeFn_sub]

Premises used: dist_eq_norm, lp.coeFn_sub, Pi.sub_apply
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst_1 : Fact (1 ≤ p)
i : α
x x_1 : ↥(lp E p)
⊢ ‖(↑(x - x_1) : (i : α) → E i) i‖ ≤ ‖x - x_1‖

Tactic:
norm_apply_le_norm (zero_lt_one.trans_le Fact.out).ne' ..

Premises used: lp.norm_apply_le_norm, ENNReal.ofNNReal, WithTop.some, LT.lt.ne', zero_lt_one, LT.lt.trans_le, Fact.out
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst_1 : Fact (1 ≤ p)
i : α
x x_1 : ↥(lp E p)
⊢ ‖(↑(x - x_1) : (i : α) → E i) i‖ ≤ ‖x - x_1‖

Tactic:
exact norm_apply_le_norm (zero_lt_one.trans_le Fact.out).ne' ..

Premises used: lp.norm_apply_le_norm, LT.lt.ne', zero_lt_one, LT.lt.trans_le, Fact.out
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
rw : LE.le (α := ℝ) (∑ i ∈ s, ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal)
⊢ ∑ i ∈ s, ‖(↑f : (i : α) → E i) i‖ ^ p.toReal ≤ ‖f‖ ^ p.toReal

Tactic:
rw [lp.norm_rpow_eq_tsum hp f]

Premises used: lp.norm_rpow_eq_tsum
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
i : α
⊢ 0 ≤ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
⊢ ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal

Tactic:
have : ∀ i, 0 ≤ ‖f i‖ ^ p.toReal := fun i ↦ by positivity
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
this : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
⊢ LE.le (α := ℝ) (∑ i ∈ s, ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal)

Tactic:
Summable.sum_le_tsum _ (fun i _ => this i) ?_

Premises used: Summable.sum_le_tsum
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
this : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
refine : Summable (α := ℝ) fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
⊢ LE.le (α := ℝ) (∑ i ∈ s, ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal)

Tactic:
refine Summable.sum_le_tsum _ (fun i _ => this i) ?_

Premises used: Summable.sum_le_tsum
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
this : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
⊢ Summable (α := ℝ) fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal

Tactic:
(lp.memℓp f).summable hp

Premises used: lp.memℓp, Memℓp.summable
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
this : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
⊢ Summable (α := ℝ) fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal

Tactic:
exact (lp.memℓp f).summable hp

Premises used: lp.memℓp, Memℓp.summable
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : Nonempty α
f : ↥(lp E ∞)
C : ℝ
hCf : ∀ (i : α), ‖(↑f : (i : α) → E i) i‖ ≤ C
⊢ ‖f‖ ≤ C

Tactic:
(isLUB_norm f).2 ?_

Premises used: lp.isLUB_norm, And.right
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : Nonempty α
f : ↥(lp E ∞)
C : ℝ
hCf : ∀ (i : α), ‖(↑f : (i : α) → E i) i‖ ≤ C
refine : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖)) C
⊢ ‖f‖ ≤ C

Tactic:
refine (isLUB_norm f).2 ?_

Premises used: lp.isLUB_norm, And.right
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : Nonempty α
f : ↥(lp E ∞)
C : ℝ
hCf : ∀ (i : α), ‖(↑f : (i : α) → E i) i‖ ≤ C
i : α
⊢ (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖) i ≤ C

Tactic:
hCf i
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : Nonempty α
f : ↥(lp E ∞)
C : ℝ
hCf : ∀ (i : α), ‖(↑f : (i : α) → E i) i‖ ≤ C
i : α
⊢ (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖) i ≤ C

Tactic:
exact hCf i
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
C : ℝ
hC : 0 ≤ C
hCf : ∀ (i : α), ‖(↑f : (i : α) → E i) i‖ ≤ C
inl : IsEmpty α → ‖f‖ ≤ C
inr : Nonempty α → ‖f‖ ≤ C
⊢ ‖f‖ ≤ C

Tactic:
cases isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
C : ℝ
hC : 0 ≤ C
hCf : ∀ (i : α), ‖(↑f : (i : α) → E i) i‖ ≤ C
h : IsEmpty α
⊢ ‖f‖ ≤ C

Tactic:
simpa [eq_zero' f] using hC

Premises used: lp.eq_zero'
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
C : ℝ
hC : 0 ≤ C
hCf : ∀ (i : α), ‖(↑f : (i : α) → E i) i‖ ≤ C
h : Nonempty α
⊢ ‖f‖ ≤ C

Tactic:
norm_le_of_forall_le' C hCf

Premises used: lp.norm_le_of_forall_le'
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
C : ℝ
hC : 0 ≤ C
hCf : ∀ (i : α), ‖(↑f : (i : α) → E i) i‖ ≤ C
h : Nonempty α
⊢ ‖f‖ ≤ C

Tactic:
exact norm_le_of_forall_le' C hCf

Premises used: lp.norm_le_of_forall_le'
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
C : ℝ
hC : 0 ≤ C
f : ↥(lp E p)
hf rw : ∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal ≤ C ^ p.toReal
⊢ ‖f‖ ≤ C

Tactic:
rw [← Real.rpow_le_rpow_iff (norm_nonneg' _) hC hp, norm_rpow_eq_tsum hp]

Premises used: lp.norm_rpow_eq_tsum, lp.norm_nonneg', Real.rpow_le_rpow_iff
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
C : ℝ
hC : 0 ≤ C
f : ↥(lp E p)
hf : ∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal ≤ C ^ p.toReal
⊢ ∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal ≤ C ^ p.toReal

Tactic:
hf
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
C : ℝ
hC : 0 ≤ C
f : ↥(lp E p)
hf : ∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal ≤ C ^ p.toReal
⊢ ∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal ≤ C ^ p.toReal

Tactic:
exact hf
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
C : ℝ
hC : 0 ≤ C
f : ↥(lp E p)
hf : ∀ (s : Finset α), ∑ i ∈ s, ‖(↑f : (i : α) → E i) i‖ ^ p.toReal ≤ C ^ p.toReal
⊢ ‖f‖ ≤ C

Tactic:
norm_le_of_tsum_le hp hC (((lp.memℓp f).summable hp).tsum_le_of_sum_le hf)

Premises used: lp.norm_le_of_tsum_le, lp.memℓp, Summable.tsum_le_of_sum_le, Memℓp.summable
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
F : α → Type u_5
inst_1 : (i : α) → NormedAddCommGroup (F i)
p : ℝ≥0∞
hp : p ≠ 0
x : ↥(lp E p)
y : ↥(lp F p)
h : ∀ (i : α), ‖(↑x : (i : α) → E i) i‖ ≤ ‖(↑y : (i : α) → F i) i‖
inl :
  ∀ (hp : Ne (α := ℝ≥0∞) 0 0) {x : ↥(lp E 0)} {y : ↥(lp F 0)}
    (h : ∀ (i : α), ‖(↑x : (i : α) → E i) i‖ ≤ ‖(↑y : (i : α) → F i) i‖), ‖x‖ ≤ ‖y‖
inr :
  ∀ (hp : Ne (α := ℝ≥0∞) ∞ 0) {x : ↥(lp E ∞)} {y : ↥(lp F ∞)}
    (h : ∀ (i : α), ‖(↑x : (i : α) → E i) i‖ ≤ ‖(↑y : (i : α) → F i) i‖), ‖x‖ ≤ ‖y‖
inr₁ : ∀ (hp : 0 < p.toReal), ‖x‖ ≤ ‖y‖
⊢ ‖x‖ ≤ ‖y‖

Tactic:
obtain (rfl | rfl | hp) := p.trichotomy

Premises used: ENNReal.trichotomy, rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
F : α → Type u_5
inst_1 : (i : α) → NormedAddCommGroup (F i)
hp : Ne (α := ℝ≥0∞) 0 0
x : ↥(lp E 0)
y : ↥(lp F 0)
h : ∀ (i : α), ‖(↑x : (i : α) → E i) i‖ ≤ ‖(↑y : (i : α) → F i) i‖
⊢ ‖x‖ ≤ ‖y‖

Tactic:
hp rfl |>.elim

Premises used: False.elim, rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
F : α → Type u_5
inst_1 : (i : α) → NormedAddCommGroup (F i)
hp : Ne (α := ℝ≥0∞) 0 0
x : ↥(lp E 0)
y : ↥(lp F 0)
h : ∀ (i : α), ‖(↑x : (i : α) → E i) i‖ ≤ ‖(↑y : (i : α) → F i) i‖
⊢ ‖x‖ ≤ ‖y‖

Tactic:
exact hp rfl |>.elim

Premises used: False.elim, rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
F : α → Type u_5
inst_1 : (i : α) → NormedAddCommGroup (F i)
hp : Ne (α := ℝ≥0∞) ∞ 0
x : ↥(lp E ∞)
y : ↥(lp F ∞)
h : ∀ (i : α), ‖(↑x : (i : α) → E i) i‖ ≤ ‖(↑y : (i : α) → F i) i‖
⊢ 0 ≤ ‖y‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
F : α → Type u_5
inst_1 : (i : α) → NormedAddCommGroup (F i)
hp : Ne (α := ℝ≥0∞) ∞ 0
x : ↥(lp E ∞)
y : ↥(lp F ∞)
h : ∀ (i : α), ‖(↑x : (i : α) → E i) i‖ ≤ ‖(↑y : (i : α) → F i) i‖
⊢ ‖x‖ ≤ ‖y‖

Tactic:
exact norm_le_of_forall_le (by positivity) fun i ↦ (h i).trans <| norm_apply_le_norm hp y i

Premises used: lp.norm_apply_le_norm, lp.norm_le_of_forall_le, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
F : α → Type u_5
inst_1 : (i : α) → NormedAddCommGroup (F i)
p : ℝ≥0∞
hp_1 : p ≠ 0
x : ↥(lp E p)
y : ↥(lp F p)
h : ∀ (i : α), ‖(↑x : (i : α) → E i) i‖ ≤ ‖(↑y : (i : α) → F i) i‖
hp : 0 < p.toReal
s : Finset α
h₁ : ∀ i ∈ s, ‖(↑x : (i : α) → E i) i‖ ≤ ‖(↑y : (i : α) → F i) i‖
⊢ LE.le (α := ℝ) (∑ i ∈ s, ‖(↑x : (i : α) → E i) i‖ ^ p.toReal) (∑ i ∈ s, ‖(↑y : (i : α) → F i) i‖ ^ p.toReal)

Tactic:
gcongr with i _
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
F : α → Type u_5
inst_1 : (i : α) → NormedAddCommGroup (F i)
p : ℝ≥0∞
hp_1 : p ≠ 0
x : ↥(lp E p)
y : ↥(lp F p)
h : ∀ (i : α), ‖(↑x : (i : α) → E i) i‖ ≤ ‖(↑y : (i : α) → F i) i‖
hp : 0 < p.toReal
s : Finset α
i : α
h_1 : i ∈ s
⊢ ‖(↑x : (i : α) → E i) i‖ ≤ ‖(↑y : (i : α) → F i) i‖

Tactic:
h i
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
F : α → Type u_5
inst_1 : (i : α) → NormedAddCommGroup (F i)
p : ℝ≥0∞
hp_1 : p ≠ 0
x : ↥(lp E p)
y : ↥(lp F p)
h : ∀ (i : α), ‖(↑x : (i : α) → E i) i‖ ≤ ‖(↑y : (i : α) → F i) i‖
hp : 0 < p.toReal
s : Finset α
i : α
h_1 : i ∈ s
⊢ ‖(↑x : (i : α) → E i) i‖ ≤ ‖(↑y : (i : α) → F i) i‖

Tactic:
exact h i
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
F : α → Type u_5
inst_1 : (i : α) → NormedAddCommGroup (F i)
p : ℝ≥0∞
hp_1 : p ≠ 0
x : ↥(lp E p)
y : ↥(lp F p)
h : ∀ (i : α), ‖(↑x : (i : α) → E i) i‖ ≤ ‖(↑y : (i : α) → F i) i‖
hp : 0 < p.toReal
⊢ ‖x‖ ≤ ‖y‖

Tactic:
exact norm_le_of_forall_sum_le hp (norm_nonneg' _) fun s ↦ calc
      ∑ i ∈ s, ‖x i‖ ^ p.toReal
      _ ≤ ∑ i ∈ s, ‖y i‖ ^ p.toReal := by gcongr with i _; exact h i
      _ ≤ ‖y‖ ^ p.toReal := sum_rpow_le_norm_rpow hp y s

Premises used: Trans.trans, lp.sum_rpow_le_norm_rpow, lp.norm_nonneg', lp.norm_le_of_forall_sum_le, rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : NormedRing 𝕜'
inst_3 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_4 : (i : α) → Module.{u_2, u_4} 𝕜' (E i)
inst_5 : ∀ (i : α), SMulCommClass.{u_2, u_1, u_4} 𝕜' 𝕜 (E i)
⊢ SMulCommClass 𝕜' 𝕜 (PreLp E)

Tactic:
inferInstanceAs <| SMulCommClass 𝕜' 𝕜 (∀ i, E i)

Premises used: _private.0.lp.instSMulCommClassPreLp._proof_1
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : NormedRing 𝕜'
inst_3 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_4 : (i : α) → Module.{u_2, u_4} 𝕜' (E i)
inst_5 : SMul 𝕜' 𝕜
inst_6 : ∀ (i : α), IsScalarTower.{u_2, u_1, u_4} 𝕜' 𝕜 (E i)
⊢ IsScalarTower 𝕜' 𝕜 (PreLp E)

Tactic:
inferInstanceAs <| IsScalarTower 𝕜' 𝕜 (∀ i, E i)

Premises used: _private.0.lp.instIsScalarTowerPreLp._proof_1
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : NormedRing 𝕜'
inst_3 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_4 : (i : α) → Module.{u_2, u_4} 𝕜' (E i)
inst_5 : (i : α) → Module.{u_1, u_4} 𝕜ᵐᵒᵖ (E i)
inst_6 : ∀ (i : α), IsCentralScalar.{u_1, u_4} 𝕜 (E i)
⊢ IsCentralScalar 𝕜 (PreLp E)

Tactic:
inferInstanceAs <| IsCentralScalar 𝕜 (∀ i, E i)

Premises used: _private.0.lp.instIsCentralScalarPreLp._proof_1
-- 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)
c : 𝕜
f : ↥(lp E p)
⊢ Membership.mem (γ := AddSubgroup (PreLp E)) (lp E p) (c • (↑f : PreLp E))

Tactic:
(lp.memℓp f).const_smul c

Premises used: Memℓp.const_smul, Set.Mem, setOf, lp.memℓp, Memℓp, ite
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : NormedRing 𝕜'
inst_3 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_4 : (i : α) → Module.{u_2, u_4} 𝕜' (E i)
inst_5 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
inst_6 : ∀ (i : α), IsBoundedSMul.{u_2, u_4} 𝕜' (E i)
c : 𝕜
f : PreLp E
hf :
  Membership.mem (γ := Set (PreLp E))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (AddSubgroup.toAddSubmonoid (lp E p)))) f
⊢ Membership.mem (γ := Set (PreLp E))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (AddSubgroup.toAddSubmonoid (lp E p)))) (c • f)

Tactic:
simpa using mem_lp_const_smul c ⟨f, hf⟩

Premises used: Subtype.mk, lp.mem_lp_const_smul
-- 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)
⊢ Eq (α := AddSubgroup (PreLp E)) (Submodule.toAddSubgroup (module_M := instModulePreLp (E := E)) (lpSubmodule 𝕜 E p))
    (lp E p)

Tactic:
rfl

Premises used: lp, rfl