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)
f : (i : α) → E i
hf : Memℓp (E := E) f p
c : 𝕜
hp : 0 < p.toReal
this : Summable (α := ℝ≥0) fun (a : α) ↦ (‖c‖₊ * ‖f a‖₊) ^ p.toReal
⊢ Summable (α := ℝ≥0) fun (a : α) ↦ ‖c • f a‖₊ ^ p.toReal

Tactic:
NNReal.summable_of_le ?_ this

Premises used: NNReal.summable_of_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 : NormedRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
f : (i : α) → E i
hf : Memℓp (E := E) f p
c : 𝕜
hp : 0 < p.toReal
this : Summable (α := ℝ≥0) fun (a : α) ↦ (‖c‖₊ * ‖f a‖₊) ^ p.toReal
inr : ∀ (b : α), ‖c • f b‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖f b‖₊) ^ p.toReal
⊢ Summable (α := ℝ≥0) fun (a : α) ↦ ‖c • f a‖₊ ^ p.toReal

Tactic:
refine NNReal.summable_of_le ?_ this

Premises used: NNReal.summable_of_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 : NormedRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
f : (i : α) → E i
hf : Memℓp (E := E) f p
c : 𝕜
hp : 0 < p.toReal
this : Summable (α := ℝ≥0) fun (a : α) ↦ (‖c‖₊ * ‖f a‖₊) ^ p.toReal
i : α
inr : ‖c • f i‖₊ ≤ ‖c‖₊ * ‖f i‖₊
⊢ ‖c • f i‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖f 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 : (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)
f : (i : α) → E i
hf : Memℓp (E := E) f p
c : 𝕜
hp : 0 < p.toReal
this : Summable (α := ℝ≥0) fun (a : α) ↦ (‖c‖₊ * ‖f a‖₊) ^ p.toReal
i : α
⊢ ‖c • f i‖₊ ≤ ‖c‖₊ * ‖f i‖₊

Tactic:
apply nnnorm_smul_le

Premises used: nnnorm_smul_le
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
α : Type u_3
p : ℝ≥0∞
inst : NormedRing 𝕜
f : α → 𝕜
hf : Memℓp (E := fun (i : α) ↦ 𝕜) f p
c : 𝕜
⊢ Memℓp (E := fun (x : α) ↦ 𝕜) (fun (x : α) ↦ c * f x) p

Tactic:
hf.const_smul c

Premises used: Memℓp.const_smul
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f g : ↥(lp E p)
h : (↑f : (i : α) → E i) = (↑g : (i : α) → E i)
⊢ f = g

Tactic:
Subtype.ext h

Premises used: Subtype.ext
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : IsEmpty α
f : ↥(lp E p)
⊢ f = 0

Tactic:
Subsingleton.elim f 0

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
hpq : q ≤ p
⊢ LE.le (α := AddSubgroup (PreLp E)) (lp E q) (lp E p)

Tactic:
fun _ hf => Memℓp.of_exponent_ge hf hpq

Premises used: Set.Mem, setOf, Memℓp.of_exponent_ge, Memℓp, ite
-- 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)
⊢ Memℓp (E := E) (↑f : (i : α) → E i) p

Tactic:
f.prop

Premises used: Set.Mem, setOf, Subtype.prop, Memℓp, ite
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
⊢ Eq (α := (i : α) → E i) (↑0 : (i : α) → E i) 0

Tactic:
rfl

Premises used: rfl
-- 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)
⊢ (↑(-f) : (i : α) → E i) = -(↑f : (i : α) → E i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f g : ↥(lp E p)
⊢ (↑(f + g) : (i : α) → E i) = (↑f : (i : α) → E i) + (↑g : (i : α) → E i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
x : ↥(lp E p)
⊢ (coeFnAddMonoidHom E p : (a : ↥(lp E p)) → (i : α) → E i) x = (↑x : (i : α) → E i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
f : ι → ↥(lp E p)
s : Finset ι
⊢ Eq (α := (i : α) → E i) (↑(∑ i ∈ s, f i) : (i : α) → E i) (∑ i ∈ s, (↑(f i) : (i : α) → E i))

Tactic:
(lp E p).val_finsetSum f s

Premises used: AddSubgroup.val_finsetSum, Set.Mem, lp, PreLp
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f g : ↥(lp E p)
⊢ (↑(f - g) : (i : α) → E i) = (↑f : (i : α) → E i) - (↑g : (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)
f : ↥(lp E p)
hp : p = 0
subst : (f : ↥(lp E 0)) → ℝ
⊢ ℝ

Tactic:
subst hp
-- 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)
f : ↥(lp E 0)
⊢ ℝ

Tactic:
exact ((lp.memℓp f).finite_dsupport.toFinset.card : ℝ)

Premises used: lp.memℓp, Nat.cast, Set.Finite.toFinset, Finset.card, Memℓp.finite_dsupport
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E 0)
⊢ ‖f‖ = (↑⋯.toFinset (s := {i : α | (↑f : (i : α) → E i) i ≠ 0}).card : ℝ)

Tactic:
dif_pos rfl

Premises used: dif_pos, rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
⊢ ‖f‖ = ⨆ (i : α), ‖(↑f : (i : α) → E i) i‖

Tactic:
rfl

Premises used: iSup, dite, rfl, ite
-- 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 ∞)
⊢ IsLUB (α := ℝ) (Set.range fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖) (⨆ (i : α), ‖(↑f : (i : α) → E i) i‖)

Tactic:
isLUB_ciSup (lp.memℓp f)

Premises used: isLUB_ciSup, lp.memℓp
-- 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 ∞)
⊢ IsLUB (α := ℝ) (Set.range fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖) (⨆ (i : α), ‖(↑f : (i : α) → E i) i‖)

Tactic:
exact isLUB_ciSup (lp.memℓp f)

Premises used: isLUB_ciSup, lp.memℓp
-- 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)
dsimp :
  (if hp : p = 0 then
      Eq.rec (motive := fun (x : ℝ≥0∞) (x_1 : 0 = x) ↦ (f : ↥(lp E x)) → ℝ)
        (fun (f : ↥(lp E 0)) ↦ (↑⋯.toFinset (s := {i : α | ¬(↑f : (i : α) → E i) i = 0}).card : ℝ)) ⋯ f
    else
      if p = ∞ then ⨆ (i : α), ‖(↑f : (i : α) → E i) i‖
      else HPow.hPow (α := ℝ) (∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (1 / p.toReal)) =
    HPow.hPow (α := ℝ) (∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (1 / p.toReal)
⊢ ‖f‖ = HPow.hPow (α := ℝ) (∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (1 / p.toReal)

Tactic:
dsimp [norm]

Premises used: Norm.norm
-- 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)
rw :
  ∀ (hp : 0 < p ∧ p < ∞) (f : ↥(lp E p)),
    (if hp : p = 0 then
        Eq.rec (motive := fun (x : ℝ≥0∞) (x_1 : 0 = x) ↦ (f : ↥(lp E x)) → ℝ)
          (fun (f : ↥(lp E 0)) ↦ (↑⋯.toFinset (s := {i : α | ¬(↑f : (i : α) → E i) i = 0}).card : ℝ)) ⋯ f
      else
        if p = ∞ then ⨆ (i : α), ‖(↑f : (i : α) → E i) i‖
        else HPow.hPow (α := ℝ) (∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (1 / p.toReal)) =
      HPow.hPow (α := ℝ) (∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (1 / p.toReal)
⊢ (if hp : p = 0 then
      Eq.rec (motive := fun (x : ℝ≥0∞) (x_1 : 0 = x) ↦ (f : ↥(lp E x)) → ℝ)
        (fun (f : ↥(lp E 0)) ↦ (↑⋯.toFinset (s := {i : α | ¬(↑f : (i : α) → E i) i = 0}).card : ℝ)) ⋯ f
    else
      if p = ∞ then ⨆ (i : α), ‖(↑f : (i : α) → E i) i‖
      else HPow.hPow (α := ℝ) (∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (1 / p.toReal)) =
    HPow.hPow (α := ℝ) (∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (1 / p.toReal)

Tactic:
rw [ENNReal.toReal_pos_iff] at hp

Premises used: ENNReal.toReal_pos_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 ∧ p < ∞
f : ↥(lp E p)
rw :
  (if p = ∞ then ⨆ (i : α), ‖(↑f : (i : α) → E i) i‖
    else HPow.hPow (α := ℝ) (∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (1 / p.toReal)) =
    HPow.hPow (α := ℝ) (∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (1 / p.toReal)
rw₁ rw₂ :
  HPow.hPow (α := ℝ) (∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (1 / p.toReal) =
    HPow.hPow (α := ℝ) (∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (1 / p.toReal)
⊢ (if hp : p = 0 then
      Eq.rec (motive := fun (x : ℝ≥0∞) (x_1 : 0 = x) ↦ (f : ↥(lp E x)) → ℝ)
        (fun (f : ↥(lp E 0)) ↦ (↑⋯.toFinset (s := {i : α | ¬(↑f : (i : α) → E i) i = 0}).card : ℝ)) ⋯ f
    else
      if p = ∞ then ⨆ (i : α), ‖(↑f : (i : α) → E i) i‖
      else HPow.hPow (α := ℝ) (∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (1 / p.toReal)) =
    HPow.hPow (α := ℝ) (∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (1 / p.toReal)

Tactic:
rw [dif_neg hp.1.ne', if_neg hp.2.ne]

Premises used: dif_neg, LT.lt.ne', And.right, And.left, if_neg, LT.lt.ne
-- 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)
rw :
  HPow.hPow (α := ℝ) (∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (1 / p.toReal * p.toReal) =
    ∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
hx : LE.le (α := ℝ) 0 (∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal)
⊢ ‖f‖ ^ p.toReal = ∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal

Tactic:
rw [norm_eq_tsum_rpow hp, ← Real.rpow_mul]

Premises used: lp.norm_eq_tsum_rpow, Real.rpow_mul
-- 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)
field_simp :
  HPow.hPow (α := ℝ) (β := ℝ) (∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) 1 =
    ∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
⊢ HPow.hPow (α := ℝ) (∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (1 / p.toReal * p.toReal) =
    ∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal

Tactic:
field_simp
-- 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)
⊢ HPow.hPow (α := ℝ) (β := ℝ) (∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) 1 =
    ∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal

Tactic:
simp
-- 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)
⊢ LE.le (α := ℝ) 0 (∑' (i : α), ‖(↑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)
rw :
  HasSum (α := ℝ) (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal)
⊢ HasSum (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (‖f‖ ^ p.toReal)

Tactic:
rw [norm_rpow_eq_tsum hp]

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)
⊢ HasSum (α := ℝ) (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal)

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

Premises used: lp.memℓp, Summable.hasSum, 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)
⊢ HasSum (α := ℝ) (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal)

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

Premises used: lp.memℓp, Summable.hasSum, Memℓp.summable
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
x : ↥(lp E p)
inl : ∀ {x : ↥(lp E 0)}, ‖toNorm (E := E) x‖ = ‖x‖
inr : ∀ {x : ↥(lp E ∞)}, ‖toNorm (E := E) x‖ = ‖x‖
inr₁ : ∀ (hp : 0 < p.toReal), ‖toNorm (E := E) x‖ = ‖x‖
⊢ ‖toNorm (E := E) x‖ = ‖x‖

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

Tactic:
simp [norm_eq_card_dsupport]

Premises used: lp.norm_eq_card_dsupport
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
x : ↥(lp E ∞)
⊢ ‖toNorm (E := E) x‖ = ‖x‖

Tactic:
simp [norm_eq_ciSup]

Premises used: lp.norm_eq_ciSup
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
x : ↥(lp E p)
hp : 0 < p.toReal
⊢ ‖toNorm (E := E) x‖ = ‖x‖

Tactic:
simp [norm_eq_tsum_rpow hp]

Premises used: lp.norm_eq_tsum_rpow
-- 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)), 0 ≤ ‖f‖
inr : ∀ (f : ↥(lp E ∞)), 0 ≤ ‖f‖
inr₁ : ∀ (hp : 0 < p.toReal), 0 ≤ ‖f‖
⊢ 0 ≤ ‖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)
⊢ 0 ≤ ‖f‖

Tactic:
simp [lp.norm_eq_card_dsupport f]

Premises used: lp.norm_eq_card_dsupport
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
inr : ∀ (_i : IsEmpty α), 0 ≤ ‖f‖
inr₁ : ∀ (_i : Nonempty α), 0 ≤ ‖f‖
⊢ 0 ≤ ‖f‖

Tactic:
rcases isEmpty_or_nonempty α with _i | _i

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 ∞)
_i : IsEmpty α
⊢ LE.le (α := ℝ) 0 (⨆ (i : α), ‖(↑f : (i : α) → E i) i‖)

Tactic:
simp [Real.iSup_of_isEmpty]

Premises used: Real.iSup_of_isEmpty
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
_i : Nonempty α
inr : ∀ (inhabited_h : Inhabited α), 0 ≤ ‖f‖
⊢ 0 ≤ ‖f‖

Tactic:
inhabit α
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
_i : Nonempty α
inhabited_h : Inhabited α
⊢ 0 ≤ ‖f‖

Tactic:
(norm_nonneg (f default)).trans ((lp.isLUB_norm f).1 ⟨default, rfl⟩)

Premises used: lp.isLUB_norm, Inhabited.default, And.left, Exists.intro, LE.le.trans, Subtype.val, norm_nonneg, rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
_i : Nonempty α
inhabited_h : Inhabited α
⊢ 0 ≤ ‖f‖

Tactic:
exact (norm_nonneg (f default)).trans ((lp.isLUB_norm f).1 ⟨default, rfl⟩)

Premises used: lp.isLUB_norm, Inhabited.default, And.left, Exists.intro, LE.le.trans, Subtype.val, norm_nonneg, rfl
-- 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 : 0 ≤ HPow.hPow (α := ℝ) (∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (1 / p.toReal)
⊢ 0 ≤ ‖f‖

Tactic:
rw [lp.norm_eq_tsum_rpow hp f]

Premises used: lp.norm_eq_tsum_rpow
-- 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
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)
hp : 0 < p.toReal
⊢ 0 ≤ HPow.hPow (α := ℝ) (∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (1 / p.toReal)

Tactic:
exact Real.rpow_nonneg (tsum_nonneg fun i ↦ by positivity) _

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

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

Tactic:
simp [lp.norm_eq_card_dsupport]

Premises used: lp.norm_eq_card_dsupport
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
⊢ norm (E := ↥(lp E ∞)) 0 = 0

Tactic:
simp [lp.norm_eq_ciSup]

Premises used: lp.norm_eq_ciSup
-- 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
inr : HPow.hPow (α := ℝ) (∑' (i : α), norm.{u_4} (E := E i) ((↑0 : (i : α) → E i) i) ^ p.toReal) (1 / p.toReal) = 0
⊢ norm (E := ↥(lp E p)) 0 = 0

Tactic:
rw [lp.norm_eq_tsum_rpow hp]

Premises used: lp.norm_eq_tsum_rpow
-- 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
⊢ 1 / p.toReal ≠ 0

Tactic:
have hp' : 1 / p.toReal ≠ 0 := one_div_ne_zero hp.ne'
-- 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
hp' : 1 / p.toReal ≠ 0
⊢ HPow.hPow (α := ℝ) (∑' (i : α), norm.{u_4} (E := E i) ((↑0 : (i : α) → E i) i) ^ p.toReal) (1 / p.toReal) = 0

Tactic:
simpa [Real.zero_rpow hp.ne'] using Real.zero_rpow hp'

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

Tactic:
norm_zero

Premises used: lp.norm_zero
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
⊢ norm (E := ↥(lp E p)) 0 = 0

Tactic:
exact norm_zero

Premises used: lp.norm_zero
-- 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)
refine : ∀ (h : ‖f‖ = 0), f = 0
⊢ ‖f‖ = 0 ↔ f = 0

Tactic:
refine ⟨fun h => ?_, by rintro rfl; exact norm_zero⟩
-- 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
inl : ∀ {f : ↥(lp E 0)} (h : ‖f‖ = 0), f = 0
inr : ∀ {f : ↥(lp E ∞)} (h : ‖f‖ = 0), f = 0
inr₁ : ∀ (hp : 0 < p.toReal), f = 0
⊢ f = 0

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)
h : ‖f‖ = 0
inl : ∀ (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
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E 0)
h : ‖f‖ = 0
i : α
⊢ Eq.{u_3 + 1} (α := Set α) {i : α | ¬(↑f : (i : α) → E i) i = 0} ∅

Tactic:
simpa [lp.norm_eq_card_dsupport f] using h

Premises used: lp.norm_eq_card_dsupport
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E 0)
h : ‖f‖ = 0
i : α
⊢ Eq.{u_3 + 1} (α := Set α) {i : α | ¬(↑f : (i : α) → E i) i = 0} ∅

Tactic:
have : { i : α | ¬f i = 0 } = ∅ := by simpa [lp.norm_eq_card_dsupport f] using h
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E 0)
h : ‖f‖ = 0
i : α
this : Eq.{u_3 + 1} (α := Set α) {i : α | ¬(↑f : (i : α) → E i) i = 0} ∅
⊢ (¬(↑f : (i : α) → E i) i = 0) = False

Tactic:
have : (¬f i = 0) = False := congr_fun this i
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E 0)
h : ‖f‖ = 0
i : α
this_1 : Eq.{u_3 + 1} (α := Set α) {i : α | ¬(↑f : (i : α) → E i) i = 0} ∅
this : (¬(↑f : (i : α) → E i) i = 0) = False
inl inl₁ inl₂ : ¬¬(↑f : (i : α) → E i) i = 0 → ¬False → (↑f : (i : α) → E i) i = (↑0 : (i : α) → E i) i
inl₃ inl₄ inl₅ : (↑f : (i : α) → E i) i = 0 → ¬False → (↑f : (i : α) → E i) i = (↑0 : (i : α) → E i) i
⊢ (↑f : (i : α) → E i) i = (↑0 : (i : α) → E i) i

Tactic:
tauto
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
h : ‖f‖ = 0
inr : ∀ (_i : IsEmpty α), f = 0
inr₁ : ∀ (_i : Nonempty α), f = 0
⊢ f = 0

Tactic:
rcases isEmpty_or_nonempty α with _i | _i

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 : ‖f‖ = 0
_i : IsEmpty α
⊢ f = 0

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
h : ‖f‖ = 0
_i : Nonempty α
⊢ IsLUB (α := ℝ) (Set.range fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖) 0

Tactic:
simpa [h] using lp.isLUB_norm f

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

Tactic:
have H : IsLUB (Set.range fun i => ‖f i‖) 0 := by simpa [h] using lp.isLUB_norm f
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
h : ‖f‖ = 0
_i : Nonempty α
H : IsLUB (α := ℝ) (Set.range fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖) 0
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
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
h : ‖f‖ = 0
_i : Nonempty α
H : IsLUB (α := ℝ) (Set.range fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖) 0
i : α
⊢ ‖(↑f : (i : α) → E i) i‖ = 0

Tactic:
have : ‖f i‖ = 0 := le_antisymm (H.1 ⟨i, rfl⟩) (norm_nonneg _)
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
h : ‖f‖ = 0
_i : Nonempty α
H : IsLUB (α := ℝ) (Set.range fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖) 0
i : α
this : ‖(↑f : (i : α) → E i) i‖ = 0
⊢ (↑f : (i : α) → E i) i = (↑0 : (i : α) → E i) i

Tactic:
simpa using 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
⊢ HasSum (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (‖f‖ ^ p.toReal)

Tactic:
have := lp.hasSum_norm hp f