awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ (↑(c • f) : (i : α) → E i) = c • (↑f : (i : α) → E i)

Tactic:
rfl

Premises used: 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 : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
inst_6 : ∀ (i : α), IsBoundedSMul.{u_2, u_4} 𝕜' (E i)
inst_7 : ∀ (i : α), SMulCommClass.{u_2, u_1, u_4} 𝕜' 𝕜 (E i)
⊢ SMulCommClass 𝕜' 𝕜 ↥(lp E p)

Tactic:
⟨fun _ _ _ => Subtype.ext <| smul_comm _ _ _⟩

Premises used: SMulCommClass.smul_comm, SMulCommClass.mk, Subtype.val, Subtype.ext
-- 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)
inst_7 : SMul 𝕜' 𝕜
inst_8 : ∀ (i : α), IsScalarTower.{u_2, u_1, u_4} 𝕜' 𝕜 (E i)
⊢ IsScalarTower 𝕜' 𝕜 ↥(lp E p)

Tactic:
⟨fun _ _ _ => Subtype.ext <| smul_assoc _ _ _⟩

Premises used: smul_assoc, IsScalarTower.mk, Subtype.val, Subtype.ext
-- 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)
inst_7 : (i : α) → Module.{u_1, u_4} 𝕜ᵐᵒᵖ (E i)
inst_8 : ∀ (i : α), IsCentralScalar.{u_1, u_4} 𝕜 (E i)
⊢ IsCentralScalar 𝕜 ↥(lp E p)

Tactic:
⟨fun _ _ => Subtype.ext <| op_smul_eq_smul _ _⟩

Premises used: IsCentralScalar.mk, Subtype.val, IsCentralScalar.op_smul_eq_smul, Subtype.ext
-- 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)
hp : p ≠ 0
c : 𝕜
f : ↥(lp E p)
inl : ∀ (hp : Ne (α := ℝ≥0∞) 0 0) (f : ↥(lp E 0)), ‖c • f‖ ≤ ‖c‖ * ‖f‖
inr : ∀ (hp : Ne (α := ℝ≥0∞) ∞ 0) (f : ↥(lp E ∞)), ‖c • f‖ ≤ ‖c‖ * ‖f‖
inr₁ : ∀ (hp : 0 < p.toReal), ‖c • f‖ ≤ ‖c‖ * ‖f‖
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖

Tactic:
rcases p.trichotomy with (rfl | rfl | hp)

Premises used: ENNReal.trichotomy, 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)
c : 𝕜
hp : Ne (α := ℝ≥0∞) 0 0
f : ↥(lp E 0)
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖

Tactic:
absurd rfl hp

Premises used: absurd, 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)
c : 𝕜
hp : Ne (α := ℝ≥0∞) 0 0
f : ↥(lp E 0)
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖

Tactic:
exact absurd rfl hp

Premises used: absurd, 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)
c : 𝕜
hp : Ne (α := ℝ≥0∞) ∞ 0
f : ↥(lp E ∞)
inr : IsEmpty α → ‖c • f‖ ≤ ‖c‖ * ‖f‖
inr₁ : Nonempty α → ‖c • f‖ ≤ ‖c‖ * ‖f‖
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖

Tactic:
cases isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- 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)
c : 𝕜
hp : Ne (α := ℝ≥0∞) ∞ 0
f : ↥(lp E ∞)
h : IsEmpty α
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖

Tactic:
simp [lp.eq_zero' f]

Premises used: lp.eq_zero'
-- 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)
c : 𝕜
hp : Ne (α := ℝ≥0∞) ∞ 0
f : ↥(lp E ∞)
h : Nonempty α
⊢ IsLUB ((fun (b : ℝ) ↦ ‖c‖ * b) '' Set.range fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖) (‖c‖ * ‖f‖)

Tactic:
have hfc := (lp.isLUB_norm f).mul_left (norm_nonneg c)
-- 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)
c : 𝕜
hp : Ne (α := ℝ≥0∞) ∞ 0
f : ↥(lp E ∞)
h : Nonempty α
hfc : IsLUB ((fun (b : ℝ) ↦ ‖c‖ * b) '' Set.range fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖) (‖c‖ * ‖f‖)
⊢ IsLUB (Set.range fun (x : α) ↦ ‖c‖ * ‖(↑f : (i : α) → E i) x‖) (‖c‖ * ‖f‖)

Tactic:
simp_rw [← Set.range_comp, Function.comp_def] at hfc

Premises used: Set.range_comp, Function.comp_def
-- 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)
c : 𝕜
hp : Ne (α := ℝ≥0∞) ∞ 0
f : ↥(lp E ∞)
h : Nonempty α
hfc : IsLUB (Set.range fun (x : α) ↦ ‖c‖ * ‖(↑f : (i : α) → E i) x‖) (‖c‖ * ‖f‖)
⊢ 0 ≤ ‖c‖ * ‖f‖

Tactic:
positivity
-- 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)
c : 𝕜
hp : Ne (α := ℝ≥0∞) ∞ 0
f : ↥(lp E ∞)
h : Nonempty α
hfc : IsLUB (Set.range fun (x : α) ↦ ‖c‖ * ‖(↑f : (i : α) → E i) x‖) (‖c‖ * ‖f‖)
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖

Tactic:
exact norm_le_of_forall_le (by positivity)
      fun i ↦ norm_smul_le c (f i) |>.trans <| hfc.1 ⟨i, rfl⟩

Premises used: lp.norm_le_of_forall_le
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst_1 : (i : α) → NormedAddCommGroup (E i)
inst_2 : NormedRing 𝕜
inst_3 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_4 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp_1 : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p) := { nnnorm := fun (f : ↥(lp E p)) ↦ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ‖f‖ ⋯ }
⊢ ∀ (f : ↥(lp E p)), (↑‖f‖₊ : ℝ) = ‖f‖

Tactic:
have coe_nnnorm : ∀ f : lp E p, ↑‖f‖₊ = ‖f‖ := fun _ => rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst_1 : (i : α) → NormedAddCommGroup (E i)
inst_2 : NormedRing 𝕜
inst_3 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_4 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp_1 : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p) := { nnnorm := fun (f : ↥(lp E p)) ↦ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ‖f‖ ⋯ }
coe_nnnorm : ∀ (f : ↥(lp E p)), (↑‖f‖₊ : ℝ) = ‖f‖
this : ‖c • f‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖f‖₊) ^ p.toReal
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊), ‖c • f‖ ≤ ‖c‖ * ‖f‖
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖

Tactic:
rwa [NNReal.rpow_le_rpow_iff hp] at this

Premises used: NNReal.rpow_le_rpow_iff
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst_1 : (i : α) → NormedAddCommGroup (E i)
inst_2 : NormedRing 𝕜
inst_3 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_4 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp_1 : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p) := { nnnorm := fun (f : ↥(lp E p)) ↦ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ‖f‖ ⋯ }
coe_nnnorm : ∀ (f : ↥(lp E p)), (↑‖f‖₊ : ℝ) = ‖f‖
inr : ‖c • f‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖f‖₊) ^ p.toReal
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖

Tactic:
suffices ‖c • f‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖f‖₊) ^ p.toReal by
      rwa [NNReal.rpow_le_rpow_iff hp] at this
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst_1 : (i : α) → NormedAddCommGroup (E i)
inst_2 : NormedRing 𝕜
inst_3 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_4 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp_1 : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p) := { nnnorm := fun (f : ↥(lp E p)) ↦ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ‖f‖ ⋯ }
coe_nnnorm : ∀ (f : ↥(lp E p)), (↑‖f‖₊ : ℝ) = ‖f‖
inr :
  ∀ (inst : NNNorm ↥(lp E p)) (coe_nnnorm : ∀ (f : ↥(lp E p)), (↑‖f‖₊ : ℝ) = ‖f‖),
    ‖c • f‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖f‖₊) ^ p.toReal
⊢ ‖c • f‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖f‖₊) ^ p.toReal

Tactic:
clear_value inst
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst_1 : (i : α) → NormedAddCommGroup (E i)
inst_2 : NormedRing 𝕜
inst_3 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_4 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp_1 : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p)
coe_nnnorm : ∀ (f : ↥(lp E p)), (↑‖f‖₊ : ℝ) = ‖f‖
inr : ‖c • f‖₊ ^ p.toReal ≤ ‖c‖₊ ^ p.toReal * ‖f‖₊ ^ p.toReal
⊢ ‖c • f‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖f‖₊) ^ p.toReal

Tactic:
rw [NNReal.mul_rpow]

Premises used: NNReal.mul_rpow
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst_1 : (i : α) → NormedAddCommGroup (E i)
inst_2 : NormedRing 𝕜
inst_3 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_4 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp_1 : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p)
coe_nnnorm : ∀ (f : ↥(lp E p)), (↑‖f‖₊ : ℝ) = ‖f‖
⊢ HasSum (fun (i : α) ↦ ‖(↑(c • f) : (i : α) → E i) i‖ ^ p.toReal) (‖c • f‖ ^ p.toReal)

Tactic:
have hLHS := lp.hasSum_norm hp (c • f)
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst_1 : (i : α) → NormedAddCommGroup (E i)
inst_2 : NormedRing 𝕜
inst_3 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_4 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp_1 : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p)
coe_nnnorm : ∀ (f : ↥(lp E p)), (↑‖f‖₊ : ℝ) = ‖f‖
hLHS : HasSum (fun (i : α) ↦ ‖(↑(c • f) : (i : α) → E i) i‖ ^ p.toReal) (‖c • f‖ ^ p.toReal)
⊢ HasSum (fun (i : α) ↦ ‖c‖ ^ p.toReal * ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (‖c‖ ^ p.toReal * ‖f‖ ^ p.toReal)

Tactic:
have hRHS := (lp.hasSum_norm hp f).mul_left (‖c‖ ^ p.toReal)
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst_1 : (i : α) → NormedAddCommGroup (E i)
inst_2 : NormedRing 𝕜
inst_3 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_4 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp_1 : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p)
coe_nnnorm : ∀ (f : ↥(lp E p)), (↑‖f‖₊ : ℝ) = ‖f‖
hLHS : HasSum (fun (i : α) ↦ ‖(↑(c • f) : (i : α) → E i) i‖ ^ p.toReal) (‖c • f‖ ^ p.toReal)
hRHS : HasSum (fun (i : α) ↦ ‖c‖ ^ p.toReal * ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (‖c‖ ^ p.toReal * ‖f‖ ^ p.toReal)
⊢ HasSum (fun (a : α) ↦ ‖c‖₊ ^ p.toReal * ‖(↑f : (i : α) → E i) a‖₊ ^ p.toReal) (‖c‖₊ ^ p.toReal * ‖f‖₊ ^ p.toReal)

Tactic:
simp_rw [← coe_nnnorm, ← _root_.coe_nnnorm, ← NNReal.coe_rpow, ← NNReal.coe_mul,
      NNReal.hasSum_coe] at hRHS hLHS

Premises used: NNReal.coe_rpow, coe_nnnorm, NNReal.coe_mul, NNReal.hasSum_coe
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst_1 : (i : α) → NormedAddCommGroup (E i)
inst_2 : NormedRing 𝕜
inst_3 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_4 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp_1 : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p)
coe_nnnorm : ∀ (f : ↥(lp E p)), (↑‖f‖₊ : ℝ) = ‖f‖
hLHS : HasSum (fun (i : α) ↦ ‖(↑(c • f) : (i : α) → E i) i‖ ^ p.toReal) (‖c • f‖ ^ p.toReal)
hRHS : HasSum (fun (i : α) ↦ ‖c‖ ^ p.toReal * ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (‖c‖ ^ p.toReal * ‖f‖ ^ p.toReal)
hRHS₁ :
  HasSum (fun (a : α) ↦ ‖c‖₊ ^ p.toReal * ‖(↑f : (i : α) → E i) a‖₊ ^ p.toReal) (‖c‖₊ ^ p.toReal * ‖f‖₊ ^ p.toReal)
⊢ HasSum (fun (a : α) ↦ ‖(↑(c • f) : (i : α) → E i) a‖₊ ^ p.toReal) (‖c • f‖₊ ^ p.toReal)

Tactic:
simp_rw [← coe_nnnorm, ← _root_.coe_nnnorm, ← NNReal.coe_rpow, ← NNReal.coe_mul,
      NNReal.hasSum_coe] at hRHS hLHS

Premises used: NNReal.coe_rpow, coe_nnnorm, NNReal.coe_mul, NNReal.hasSum_coe
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst_1 : (i : α) → NormedAddCommGroup (E i)
inst_2 : NormedRing 𝕜
inst_3 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_4 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp_1 : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p)
coe_nnnorm : ∀ (f : ↥(lp E p)), (↑‖f‖₊ : ℝ) = ‖f‖
hRHS : HasSum (fun (a : α) ↦ ‖c‖₊ ^ p.toReal * ‖(↑f : (i : α) → E i) a‖₊ ^ p.toReal) (‖c‖₊ ^ p.toReal * ‖f‖₊ ^ p.toReal)
hLHS : HasSum (fun (a : α) ↦ ‖(↑(c • f) : (i : α) → E i) a‖₊ ^ p.toReal) (‖c • f‖₊ ^ p.toReal)
⊢ ‖c • f‖₊ ^ p.toReal ≤ ‖c‖₊ ^ p.toReal * ‖f‖₊ ^ p.toReal

Tactic:
hasSum_mono hLHS hRHS fun i => ?_

Premises used: hasSum_mono
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst_1 : (i : α) → NormedAddCommGroup (E i)
inst_2 : NormedRing 𝕜
inst_3 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_4 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp_1 : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p)
coe_nnnorm : ∀ (f : ↥(lp E p)), (↑‖f‖₊ : ℝ) = ‖f‖
hRHS : HasSum (fun (a : α) ↦ ‖c‖₊ ^ p.toReal * ‖(↑f : (i : α) → E i) a‖₊ ^ p.toReal) (‖c‖₊ ^ p.toReal * ‖f‖₊ ^ p.toReal)
hLHS : HasSum (fun (a : α) ↦ ‖(↑(c • f) : (i : α) → E i) a‖₊ ^ p.toReal) (‖c • f‖₊ ^ p.toReal)
inr : ∀ (i : α), ‖(↑(c • f) : (i : α) → E i) i‖₊ ^ p.toReal ≤ ‖c‖₊ ^ p.toReal * ‖(↑f : (i : α) → E i) i‖₊ ^ p.toReal
⊢ ‖c • f‖₊ ^ p.toReal ≤ ‖c‖₊ ^ p.toReal * ‖f‖₊ ^ p.toReal

Tactic:
refine hasSum_mono hLHS hRHS fun i => ?_

Premises used: hasSum_mono
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst_1 : (i : α) → NormedAddCommGroup (E i)
inst_2 : NormedRing 𝕜
inst_3 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_4 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp_1 : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p)
coe_nnnorm : ∀ (f : ↥(lp E p)), (↑‖f‖₊ : ℝ) = ‖f‖
hRHS : HasSum (fun (a : α) ↦ ‖c‖₊ ^ p.toReal * ‖(↑f : (i : α) → E i) a‖₊ ^ p.toReal) (‖c‖₊ ^ p.toReal * ‖f‖₊ ^ p.toReal)
hLHS : HasSum (fun (a : α) ↦ ‖(↑(c • f) : (i : α) → E i) a‖₊ ^ p.toReal) (‖c • f‖₊ ^ p.toReal)
i : α
inr : ‖c • (↑f : (i : α) → E i) i‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖(↑f : (i : α) → E i) i‖₊) ^ p.toReal
⊢ ‖(↑(c • f) : (i : α) → E i) i‖₊ ^ p.toReal ≤ ‖c‖₊ ^ p.toReal * ‖(↑f : (i : α) → E i) i‖₊ ^ p.toReal

Tactic:
rw [← NNReal.mul_rpow, lp.coeFn_smul, Pi.smul_apply]

Premises used: lp.coeFn_smul, NNReal.mul_rpow, Pi.smul_apply
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst_1 : (i : α) → NormedAddCommGroup (E i)
inst_2 : NormedRing 𝕜
inst_3 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_4 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp_1 : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p)
coe_nnnorm : ∀ (f : ↥(lp E p)), (↑‖f‖₊ : ℝ) = ‖f‖
hRHS : HasSum (fun (a : α) ↦ ‖c‖₊ ^ p.toReal * ‖(↑f : (i : α) → E i) a‖₊ ^ p.toReal) (‖c‖₊ ^ p.toReal * ‖f‖₊ ^ p.toReal)
hLHS : HasSum (fun (a : α) ↦ ‖(↑(c • f) : (i : α) → E i) a‖₊ ^ p.toReal) (‖c • f‖₊ ^ p.toReal)
i : α
inr : ‖c • (↑f : (i : α) → E i) i‖₊ ≤ ‖c‖₊ * ‖(↑f : (i : α) → E i) i‖₊
⊢ ‖c • (↑f : (i : α) → E i) i‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖(↑f : (i : α) → E i) i‖₊) ^ p.toReal

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst_1 : (i : α) → NormedAddCommGroup (E i)
inst_2 : NormedRing 𝕜
inst_3 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_4 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp_1 : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p)
coe_nnnorm : ∀ (f : ↥(lp E p)), (↑‖f‖₊ : ℝ) = ‖f‖
hRHS : HasSum (fun (a : α) ↦ ‖c‖₊ ^ p.toReal * ‖(↑f : (i : α) → E i) a‖₊ ^ p.toReal) (‖c‖₊ ^ p.toReal * ‖f‖₊ ^ p.toReal)
hLHS : HasSum (fun (a : α) ↦ ‖(↑(c • f) : (i : α) → E i) a‖₊ ^ p.toReal) (‖c • f‖₊ ^ p.toReal)
i : α
⊢ ‖c • (↑f : (i : α) → E i) i‖₊ ≤ ‖c‖₊ * ‖(↑f : (i : α) → E i) i‖₊

Tactic:
apply nnnorm_smul_le

Premises used: nnnorm_smul_le
-- 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)
inst_7 : Fact (1 ≤ p)
⊢ IsBoundedSMul 𝕜 ↥(lp E p)

Tactic:
IsBoundedSMul.of_norm_smul_le <| norm_const_smul_le (zero_lt_one.trans_le <| Fact.out).ne'

Premises used: Set.Mem, LT.lt.ne', zero_lt_one, LT.lt.trans_le, IsBoundedSMul.of_norm_smul_le, lp.norm_const_smul_le, Fact.out
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : Type u_5
inst : NormedAddCommGroup E
f : ↥(lp (fun (x : α) ↦ E) 1)
⊢ Summable (α := ℝ) fun (a : α) ↦ ‖‖(↑f : (i : α) → (fun (x : α) ↦ E) i) a‖‖

Tactic:
simpa using f.2.summable

Premises used: Memℓp.summable, Subtype.property
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : Type u_5
inst : NormedAddCommGroup E
f : ↥(lp (fun (x : α) ↦ E) 1)
⊢ ∑' (i : α), ‖(↑f : (i : α) → (fun (x : α) ↦ E) i) i‖ = ‖f‖

Tactic:
simp [norm_eq_tsum_rpow]

Premises used: lp.norm_eq_tsum_rpow
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E_1 : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E_1 i)
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
inst_5 : CompleteSpace E
f g : ↥(lp (fun (x : α) ↦ E) 1)
rw :
  Eq.{u_5 + 1} (α := E) (∑' (i : α), (↑(f + g) : (i : α) → (fun (x : α) ↦ E) i) i)
    (∑' (b : α), ((↑f : (i : α) → (fun (x : α) ↦ E) i) b + (↑g : (i : α) → (fun (x : α) ↦ E) i) b))
hf : Summable (↑f : (i : α) → (fun (x : α) ↦ E) i)
hg : Summable (↑g : (i : α) → (fun (x : α) ↦ E) i)
⊢ ∑' (i : α), (↑(f + g) : (i : α) → (fun (x : α) ↦ E) i) i =
    HAdd.hAdd (α := E) (∑' (i : α), (↑f : (i : α) → (fun (x : α) ↦ E) i) i)
      (∑' (i : α), (↑g : (i : α) → (fun (x : α) ↦ E) i) i)

Tactic:
rw [← Summable.tsum_add]

Premises used: Summable.tsum_add
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E_1 : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E_1 i)
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
inst_5 : CompleteSpace E
f g : ↥(lp (fun (x : α) ↦ E) 1)
⊢ Eq.{u_5 + 1} (α := E) (∑' (i : α), (↑(f + g) : (i : α) → (fun (x : α) ↦ E) i) i)
    (∑' (b : α), ((↑f : (i : α) → (fun (x : α) ↦ E) i) b + (↑g : (i : α) → (fun (x : α) ↦ E) i) b))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E_1 : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E_1 i)
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
inst_5 : CompleteSpace E
f g : ↥(lp (fun (x : α) ↦ E) 1)
⊢ Summable (α := ℝ) fun (a : α) ↦ ‖(↑f : (i : α) → (fun (x : α) ↦ E) i) a‖

Tactic:
simpa using f.2.summable

Premises used: Memℓp.summable, Subtype.property
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E_1 : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E_1 i)
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
inst_5 : CompleteSpace E
f g : ↥(lp (fun (x : α) ↦ E) 1)
⊢ Summable (α := ℝ) fun (a : α) ↦ ‖(↑g : (i : α) → (fun (x : α) ↦ E) i) a‖

Tactic:
simpa using g.2.summable

Premises used: Memℓp.summable, Subtype.property
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E_1 : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E_1 i)
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
inst_5 : CompleteSpace E
f g : ↥(lp (fun (x : α) ↦ E) 1)
⊢ Eq.{u_5 + 1} (α := E) (∑' (i : α), (↑(f + g) : (i : α) → (fun (x : α) ↦ E) i) i)
    (∑' (b : α), ((↑f : (i : α) → (fun (x : α) ↦ E) i) b + (↑g : (i : α) → (fun (x : α) ↦ E) i) b))

Tactic:
exacts [rfl, .of_norm (by simpa using f.2.summable), .of_norm (by simpa using g.2.summable)]

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E_1 : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E_1 i)
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
inst_5 : CompleteSpace E
c : 𝕜
f : ↥(lp (fun (x : α) ↦ E) 1)
simp :
  ∑' (i : α), (c • (↑f : (i : α) → E)) i =
    HSMul.hSMul (α := 𝕜) (β := E) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) (∑' (i : α), (↑f : (i : α) → E) i)
⊢ ∑' (i : α), (↑(c • f) : (i : α) → (fun (x : α) ↦ E) i) i =
    HSMul.hSMul (α := 𝕜) (β := E) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (∑' (i : α), (↑f : (i : α) → (fun (x : α) ↦ E) i) i)

Tactic:
simp only [coeFn_smul]

Premises used: lp.coeFn_smul
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E_1 : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E_1 i)
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
inst_5 : CompleteSpace E
c : 𝕜
f : ↥(lp (fun (x : α) ↦ E) 1)
⊢ Summable (α := ℝ) fun (a : α) ↦ ‖(↑f : (i : α) → E) a‖

Tactic:
simpa using f.2.summable

Premises used: Memℓp.summable, Subtype.property
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E_1 : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E_1 i)
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
inst_5 : CompleteSpace E
c : 𝕜
f : ↥(lp (fun (x : α) ↦ E) 1)
⊢ ∑' (i : α), (c • (↑f : (i : α) → E)) i =
    HSMul.hSMul (α := 𝕜) (β := E) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) (∑' (i : α), (↑f : (i : α) → E) i)

Tactic:
exact Summable.tsum_const_smul _ (.of_norm (by simpa using f.2.summable))

Premises used: Summable.of_norm, Summable.tsum_const_smul
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E_1 : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E_1 i)
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
inst_5 : CompleteSpace E
f : ↥(lp (fun (x : α) ↦ E) 1)
⊢ norm.{u_5} (E := E)
      (({ toFun := fun (f : ↥(lp (fun (x : α) ↦ E) 1)) ↦ ∑' (i : α), (↑f : (i : α) → (fun (x : α) ↦ E) i) i,
              map_add' := ⋯, map_smul' := ⋯ : ↥(lp (fun (x : α) ↦ E) 1) →ₗ[𝕜] E } :
            (a : ↥(lp (fun (x : α) ↦ E) 1)) → E)
          f :
        E) ≤
    1 * ‖f‖

Tactic:
simpa using norm_tsum_le f

Premises used: lp.norm_tsum_le
-- 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 : NormedDivisionRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp : p ≠ 0
c : 𝕜
f : ↥(lp E p)
inl : ‖HSMul.hSMul (α := 𝕜) 0 f‖ = norm.{u_1} (E := 𝕜) 0 * ‖f‖
inr : ∀ (hc : c ≠ 0), ‖c • f‖ = ‖c‖ * ‖f‖
⊢ ‖c • f‖ = ‖c‖ * ‖f‖

Tactic:
obtain rfl | hc := eq_or_ne c 0

Premises used: eq_or_ne, OfNat.ofNat, rfl