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)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
this : HasSum (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (‖f‖ ^ p.toReal)
rwa :
  ∀ (this : HasSum (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (HPow.hPow (α := ℝ) 0 p.toReal)),
    HasSum (α := ℝ) (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) 0
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : HasSum (α := ℝ) (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) 0),
    HasSum (α := ℝ) (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) 0
⊢ HasSum (α := ℝ) (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) 0

Tactic:
rwa [h, Real.zero_rpow hp.ne'] at this

Premises used: Real.zero_rpow, LT.lt.ne'
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
⊢ HasSum (α := ℝ) (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) 0

Tactic:
have hf : HasSum (fun i : α => ‖f i‖ ^ p.toReal) 0 := by
      have := lp.hasSum_norm hp f
      rwa [h, Real.zero_rpow hp.ne'] at this
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
hf : HasSum (α := ℝ) (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) 0
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)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
hf : HasSum (α := ℝ) (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) 0
⊢ ∀ (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)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
hf : HasSum (α := ℝ) (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) 0
this : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
⊢ Eq.{u_3 + 1} (α := α → ℝ) (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) 0

Tactic:
rw [hasSum_zero_iff_of_nonneg this] at hf

Premises used: hasSum_zero_iff_of_nonneg
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
hf : HasSum (α := ℝ) (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) 0
this : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
hf₁ : Eq.{u_3 + 1} (α := α → ℝ) (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) 0
⊢ ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal

Tactic:
rw [hasSum_zero_iff_of_nonneg this] at hf

Premises used: hasSum_zero_iff_of_nonneg
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
hf : Eq.{u_3 + 1} (α := α → ℝ) (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) 0
this : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
inr : ∀ (i : α), (↑f : (i : α) → E i) i = (↑0 : (i : α) → E i) i
⊢ f = 0

Tactic:
ext i
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
hf : Eq.{u_3 + 1} (α := α → ℝ) (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) 0
this : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
i : α
⊢ (↑f : (i : α) → E i) i = 0 ∧ p.toReal ≠ 0

Tactic:
simpa [Real.rpow_eq_zero_iff_of_nonneg (norm_nonneg (f i))] using congr_fun hf i

Premises used: Real.rpow_eq_zero_iff_of_nonneg, congr_fun, Subtype.val, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
hf : Eq.{u_3 + 1} (α := α → ℝ) (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) 0
this : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
i : α
⊢ (↑f : (i : α) → E i) i = 0 ∧ p.toReal ≠ 0

Tactic:
have : f i = 0 ∧ p.toReal ≠ 0 := by
      simpa [Real.rpow_eq_zero_iff_of_nonneg (norm_nonneg (f i))] using congr_fun hf i
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
hf : Eq.{u_3 + 1} (α := α → ℝ) (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) 0
this_1 : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
i : α
this : (↑f : (i : α) → E i) i = 0 ∧ p.toReal ≠ 0
⊢ (↑f : (i : α) → E i) i = (↑0 : (i : α) → E i) i

Tactic:
this.1

Premises used: And.left
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
hf : Eq.{u_3 + 1} (α := α → ℝ) (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) 0
this_1 : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
i : α
this : (↑f : (i : α) → E i) i = 0 ∧ p.toReal ≠ 0
⊢ (↑f : (i : α) → E i) i = (↑0 : (i : α) → E i) i

Tactic:
exact this.1

Premises used: And.left
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
rw : (↑f : (i : α) → E i) = (↑0 : (i : α) → E i) ↔ (↑f : (i : α) → E i) = 0
rw₁ rw₂ : (↑f : (i : α) → E i) = 0 ↔ (↑f : (i : α) → E i) = 0
⊢ f = 0 ↔ (↑f : (i : α) → E i) = 0

Tactic:
rw [lp.ext_iff, coeFn_zero]

Premises used: lp.coeFn_zero, lp.ext_iff
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
inl : ∀ ⦃f : ↥(lp E 0)⦄, ‖-f‖ = ‖f‖
inr : ∀ ⦃f : ↥(lp E ∞)⦄, ‖-f‖ = ‖f‖
inr₁ : ∀ (hp : 0 < p.toReal), ‖-f‖ = ‖f‖
⊢ ‖-f‖ = ‖f‖

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

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 : ↥(lp E 0)
⊢ ‖-f‖ = ‖f‖

Tactic:
simp only [norm_eq_card_dsupport, coeFn_neg, Pi.neg_apply, ne_eq, neg_eq_zero]

Premises used: neg_eq_zero, lp.norm_eq_card_dsupport, ne_eq, lp.coeFn_neg, Pi.neg_apply
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
inr : IsEmpty α → ‖-f‖ = ‖f‖
inr₁ : Nonempty α → ‖-f‖ = ‖f‖
⊢ ‖-f‖ = ‖f‖

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 ∞)
h : IsEmpty α
⊢ ‖-f‖ = ‖f‖

Tactic:
simp only [lp.eq_zero' f, neg_zero, norm_zero]

Premises used: lp.norm_zero, lp.eq_zero', neg_zero
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
h : Nonempty α
inr : IsLUB (Set.range fun (i : α) ↦ ‖(↑(-f) : (i : α) → E i) i‖) ‖f‖
⊢ ‖-f‖ = ‖f‖

Tactic:
apply (lp.isLUB_norm (-f)).unique

Premises used: lp.isLUB_norm, IsLUB.unique, Neg.neg
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
h : Nonempty α
⊢ IsLUB (Set.range fun (i : α) ↦ ‖(↑(-f) : (i : α) → E i) i‖) ‖f‖

Tactic:
simpa only [coeFn_neg, Pi.neg_apply, norm_neg] using lp.isLUB_norm f

Premises used: lp.isLUB_norm, lp.norm_neg, lp.coeFn_neg, Pi.neg_apply
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
hp : 0 < p.toReal
this : ‖-f‖ ^ p.toReal = ‖f‖ ^ p.toReal
⊢ ‖-f‖ = ‖f‖

Tactic:
Real.rpow_left_injOn hp.ne' (norm_nonneg' _) (norm_nonneg' _) this

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

Tactic:
exact Real.rpow_left_injOn hp.ne' (norm_nonneg' _) (norm_nonneg' _) this

Premises used: lp.norm_nonneg', LT.lt.ne', Real.rpow_left_injOn
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
hp : 0 < p.toReal
inr : ‖-f‖ ^ p.toReal = ‖f‖ ^ p.toReal
⊢ ‖-f‖ = ‖f‖

Tactic:
suffices ‖-f‖ ^ p.toReal = ‖f‖ ^ p.toReal by
      exact Real.rpow_left_injOn hp.ne' (norm_nonneg' _) (norm_nonneg' _) this
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
hp : 0 < p.toReal
inr : HasSum (fun (i : α) ↦ ‖(↑(-f) : (i : α) → E i) i‖ ^ p.toReal) (‖f‖ ^ p.toReal)
⊢ ‖-f‖ ^ p.toReal = ‖f‖ ^ p.toReal

Tactic:
apply (lp.hasSum_norm hp (-f)).unique

Premises used: lp.hasSum_norm, HasSum.unique, Neg.neg
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
hp : 0 < p.toReal
⊢ HasSum (fun (i : α) ↦ ‖(↑(-f) : (i : α) → E i) i‖ ^ p.toReal) (‖f‖ ^ p.toReal)

Tactic:
simpa only [coeFn_neg, Pi.neg_apply, _root_.norm_neg] using lp.hasSum_norm hp f

Premises used: lp.hasSum_norm, norm_neg, lp.coeFn_neg, Pi.neg_apply
-- 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)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (f g : ↥(lp E ∞)), ‖f + g‖ ≤ ‖f‖ + ‖g‖
inr : ∀ (hp' : 1 ≤ p.toReal), ‖f + g‖ ≤ ‖f‖ + ‖g‖
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖

Tactic:
rcases p.dichotomy with (rfl | hp')

Premises used: ENNReal.dichotomy, rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g : ↥(lp E ∞)
inl : IsEmpty α → ‖f + g‖ ≤ ‖f‖ + ‖g‖
inl₁ : Nonempty α → ‖f + g‖ ≤ ‖f‖ + ‖g‖
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖

Tactic:
cases isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g : ↥(lp E ∞)
h : IsEmpty α
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖

Tactic:
simp only [lp.eq_zero' f, zero_add, norm_zero, le_refl]

Premises used: le_refl, zero_add, lp.norm_zero, lp.eq_zero'
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g : ↥(lp E ∞)
h : Nonempty α
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖

Tactic:
(lp.isLUB_norm (f + g)).2 ?_

Premises used: lp.isLUB_norm, ENNReal.ofNNReal, Set.Mem, WithTop.some, And.right, HAdd.hAdd
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g : ↥(lp E ∞)
h : Nonempty α
inl : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖(↑(f + g) : (i : α) → E i) i‖)) (‖f‖ + ‖g‖)
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖

Tactic:
refine (lp.isLUB_norm (f + g)).2 ?_

Premises used: lp.isLUB_norm, And.right, HAdd.hAdd
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g : ↥(lp E ∞)
h : Nonempty α
i : α
⊢ (fun (i : α) ↦ ‖(↑(f + g) : (i : α) → E i) i‖) i ≤ ‖f‖ + ‖g‖

Tactic:
le_trans ?_ (add_mem_upperBounds_add
            (lp.isLUB_norm f).1 (lp.isLUB_norm g).1 ⟨_, ⟨i, rfl⟩, _, ⟨i, rfl⟩, rfl⟩)

Premises used: lp.isLUB_norm, And.left, And.intro, Exists.intro, add_mem_upperBounds_add, rfl, le_trans
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g : ↥(lp E ∞)
h : Nonempty α
i : α
inl :
  LE.le (α := ℝ) ((fun (i : α) ↦ ‖(↑(f + g) : (i : α) → E i) i‖) i)
    ((fun (x1 x2 : ℝ) ↦ x1 + x2) ((fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖) i)
      ((fun (i : α) ↦ ‖(↑g : (i : α) → E i) i‖) i))
⊢ (fun (i : α) ↦ ‖(↑(f + g) : (i : α) → E i) i‖) i ≤ ‖f‖ + ‖g‖

Tactic:
refine le_trans ?_ (add_mem_upperBounds_add
            (lp.isLUB_norm f).1 (lp.isLUB_norm g).1 ⟨_, ⟨i, rfl⟩, _, ⟨i, rfl⟩, rfl⟩)

Premises used: lp.isLUB_norm, And.left, And.intro, Exists.intro, add_mem_upperBounds_add, rfl, le_trans
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g : ↥(lp E ∞)
h : Nonempty α
i : α
⊢ LE.le (α := ℝ) ((fun (i : α) ↦ ‖(↑(f + g) : (i : α) → E i) i‖) i)
    ((fun (x1 x2 : ℝ) ↦ x1 + x2) ((fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖) i)
      ((fun (i : α) ↦ ‖(↑g : (i : α) → E i) i‖) i))

Tactic:
norm_add_le (f i) (g i)

Premises used: norm_add_le, Subtype.val
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g : ↥(lp E ∞)
h : Nonempty α
i : α
⊢ LE.le (α := ℝ) ((fun (i : α) ↦ ‖(↑(f + g) : (i : α) → E i) i‖) i)
    ((fun (x1 x2 : ℝ) ↦ x1 + x2) ((fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖) i)
      ((fun (i : α) ↦ ‖(↑g : (i : α) → E i) i‖) i))

Tactic:
exact norm_add_le (f i) (g i)

Premises used: norm_add_le, Subtype.val
-- 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)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
⊢ 0 < p.toReal

Tactic:
have hp'' : 0 < p.toReal := zero_lt_one.trans_le hp'
-- 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)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
hp'' : 0 < p.toReal
⊢ ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖

Tactic:
have hf₁ : ∀ i, 0 ≤ ‖f i‖ := fun i => norm_nonneg _
-- 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)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
hp'' : 0 < p.toReal
hf₁ : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖
⊢ ∀ (i : α), 0 ≤ ‖(↑g : (i : α) → E i) i‖

Tactic:
have hg₁ : ∀ i, 0 ≤ ‖g i‖ := fun i => norm_nonneg _
-- 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)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
hp'' : 0 < p.toReal
hf₁ : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖
hg₁ : ∀ (i : α), 0 ≤ ‖(↑g : (i : α) → E i) i‖
⊢ HasSum (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (‖f‖ ^ p.toReal)

Tactic:
have hf₂ := lp.hasSum_norm hp'' f
-- 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)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
hp'' : 0 < p.toReal
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)
⊢ HasSum (fun (i : α) ↦ ‖(↑g : (i : α) → E i) i‖ ^ p.toReal) (‖g‖ ^ p.toReal)

Tactic:
have hg₂ := lp.hasSum_norm hp'' g
-- 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)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
hp'' : 0 < p.toReal
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‖ ^ p.toReal) (‖g‖ ^ p.toReal)
inr :
  ∀ (C : ℝ) (hC₁ : 0 ≤ C) (hC₂ : C ≤ ‖f‖ + ‖g‖)
    (hCfg : HasSum (fun (i : α) ↦ (‖(↑f : (i : α) → E i) i‖ + ‖(↑g : (i : α) → E i) i‖) ^ p.toReal) (C ^ p.toReal)),
    ‖f + g‖ ≤ ‖f‖ + ‖g‖
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖

Tactic:
obtain ⟨C, hC₁, hC₂, hCfg⟩ :=
            Real.Lp_add_le_hasSum_of_nonneg hp' hf₁ hg₁ (norm_nonneg' _) (norm_nonneg' _) hf₂ hg₂

Premises used: lp.norm_nonneg', Real.Lp_add_le_hasSum_of_nonneg
-- 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)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
hp'' : 0 < p.toReal
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‖ ^ p.toReal) (‖g‖ ^ p.toReal)
C : ℝ
hC₁ : 0 ≤ C
hC₂ : C ≤ ‖f‖ + ‖g‖
hCfg : HasSum (fun (i : α) ↦ (‖(↑f : (i : α) → E i) i‖ + ‖(↑g : (i : α) → E i) i‖) ^ p.toReal) (C ^ p.toReal)
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖

Tactic:
le_trans ?_ hC₂

Premises used: le_trans
-- 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)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
hp'' : 0 < p.toReal
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‖ ^ p.toReal) (‖g‖ ^ p.toReal)
C : ℝ
hC₁ : 0 ≤ C
hC₂ : C ≤ ‖f‖ + ‖g‖
hCfg : HasSum (fun (i : α) ↦ (‖(↑f : (i : α) → E i) i‖ + ‖(↑g : (i : α) → E i) i‖) ^ p.toReal) (C ^ p.toReal)
inr : ‖f + g‖ ≤ C
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖

Tactic:
refine le_trans ?_ hC₂

Premises used: le_trans
-- 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)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
hp'' : 0 < p.toReal
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‖ ^ p.toReal) (‖g‖ ^ p.toReal)
C : ℝ
hC₁ : 0 ≤ C
hC₂ : C ≤ ‖f‖ + ‖g‖
hCfg : HasSum (fun (i : α) ↦ (‖(↑f : (i : α) → E i) i‖ + ‖(↑g : (i : α) → E i) i‖) ^ p.toReal) (C ^ p.toReal)
inr : ‖f + g‖ ^ p.toReal ≤ C ^ p.toReal
⊢ ‖f + g‖ ≤ C

Tactic:
rw [← Real.rpow_le_rpow_iff (norm_nonneg' (f + g)) hC₁ hp'']

Premises used: lp.norm_nonneg', HAdd.hAdd, Real.rpow_le_rpow_iff
-- 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)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
hp'' : 0 < p.toReal
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‖ ^ p.toReal) (‖g‖ ^ p.toReal)
C : ℝ
hC₁ : 0 ≤ C
hC₂ : C ≤ ‖f‖ + ‖g‖
hCfg : HasSum (fun (i : α) ↦ (‖(↑f : (i : α) → E i) i‖ + ‖(↑g : (i : α) → E i) i‖) ^ p.toReal) (C ^ p.toReal)
⊢ ‖f + g‖ ^ p.toReal ≤ C ^ p.toReal

Tactic:
hasSum_le ?_ (lp.hasSum_norm hp'' (f + g)) hCfg

Premises used: hasSum_le, lp.hasSum_norm, HAdd.hAdd
-- 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)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
hp'' : 0 < p.toReal
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‖ ^ p.toReal) (‖g‖ ^ p.toReal)
C : ℝ
hC₁ : 0 ≤ C
hC₂ : C ≤ ‖f‖ + ‖g‖
hCfg : HasSum (fun (i : α) ↦ (‖(↑f : (i : α) → E i) i‖ + ‖(↑g : (i : α) → E i) i‖) ^ p.toReal) (C ^ p.toReal)
inr :
  ∀ (i : α),
    ‖(↑(f + g) : (i : α) → E i) i‖ ^ p.toReal ≤ (‖(↑f : (i : α) → E i) i‖ + ‖(↑g : (i : α) → E i) i‖) ^ p.toReal
⊢ ‖f + g‖ ^ p.toReal ≤ C ^ p.toReal

Tactic:
refine hasSum_le ?_ (lp.hasSum_norm hp'' (f + g)) hCfg

Premises used: hasSum_le, lp.hasSum_norm, HAdd.hAdd
-- 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)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
hp'' : 0 < p.toReal
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‖ ^ p.toReal) (‖g‖ ^ p.toReal)
C : ℝ
hC₁ : 0 ≤ C
hC₂ : C ≤ ‖f‖ + ‖g‖
hCfg : HasSum (fun (i : α) ↦ (‖(↑f : (i : α) → E i) i‖ + ‖(↑g : (i : α) → E i) i‖) ^ p.toReal) (C ^ p.toReal)
i : α
inr : ‖(↑(f + g) : (i : α) → E i) i‖ ≤ ‖(↑f : (i : α) → E i) i‖ + ‖(↑g : (i : α) → E i) i‖
⊢ ‖(↑(f + g) : (i : α) → E i) i‖ ^ p.toReal ≤ (‖(↑f : (i : α) → E i) i‖ + ‖(↑g : (i : α) → E i) i‖) ^ p.toReal

Tactic:
gcongr
-- 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)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
hp'' : 0 < p.toReal
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‖ ^ p.toReal) (‖g‖ ^ p.toReal)
C : ℝ
hC₁ : 0 ≤ C
hC₂ : C ≤ ‖f‖ + ‖g‖
hCfg : HasSum (fun (i : α) ↦ (‖(↑f : (i : α) → E i) i‖ + ‖(↑g : (i : α) → E i) i‖) ^ p.toReal) (C ^ p.toReal)
i : α
⊢ ‖(↑(f + g) : (i : α) → E i) i‖ ≤ ‖(↑f : (i : α) → E i) i‖ + ‖(↑g : (i : α) → E i) i‖

Tactic:
apply norm_add_le

Premises used: norm_add_le
-- 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 : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖

Tactic:
have hf₁ : ∀ i, 0 ≤ ‖f i‖ := fun i => 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‖
⊢ ∀ (i : α), 0 ≤ ‖(↑g : (i : α) → E i) i‖

Tactic:
have hg₁ : ∀ i, 0 ≤ ‖g i‖ := fun i => 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‖
⊢ HasSum (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (‖f‖ ^ p.toReal)

Tactic:
have hf₂ := lp.hasSum_norm hpq.pos f
-- 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)
⊢ HasSum (fun (i : α) ↦ ‖(↑g : (i : α) → E i) i‖ ^ q.toReal) (‖g‖ ^ q.toReal)

Tactic:
have hg₂ := lp.hasSum_norm hpq.symm.pos g