awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
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
⊢ Summable (α := ℝ) fun (i : α) ↦ ‖(c • f) i‖ ^ p.toReal
have inr : Summable (α := ℝ) fun (i : α) ↦ ‖c • f i‖ ^ p.toReal
Tactic: dsimp only [Pi.smul_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
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
⊢ Summable (α := ℝ) fun (i : α) ↦ ‖c • f i‖ ^ p.toReal
have this : Summable (α := ℝ) fun (i : α) ↦ (↑(‖c‖₊ ^ p.toReal) : ℝ) * ‖f i‖ ^ p.toReal
Tactic: have := (hf.summable hp).mul_left (↑(‖c‖₊ ^ p.toReal) : ℝ)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
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 (α := ℝ) fun (i : α) ↦ (↑(‖c‖₊ ^ p.toReal) : ℝ) * ‖f i‖ ^ p.toReal
⊢ Summable (α := ℝ) fun (i : α) ↦ ‖c • f i‖ ^ p.toReal
have inr : ∀ (this : Summable (α := ℝ≥0) fun (a : α) ↦ (‖c‖₊ * ‖f a‖₊) ^ p.toReal),
  Summable (α := ℝ≥0) fun (a : α) ↦ ‖c • f a‖₊ ^ p.toReal
Tactic: simp_rw [← coe_nnnorm, ← NNReal.coe_rpow, ← NNReal.coe_mul, NNReal.summable_coe,
      ← NNReal.mul_rpow] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
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
have inr : ∀ (b : α), ‖c • f b‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖f b‖₊) ^ p.toReal
Tactic: refine NNReal.summable_of_le ?_ this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
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‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖f i‖₊) ^ p.toReal
have inr : ‖c • f i‖₊ ≤ ‖c‖₊ * ‖f i‖₊
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
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
⊢ ℝ
have subst : (f : ↥(lp E 0)) → ℝ
Tactic: subst hp
Cleared hypotheses: p, f, hp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
⊢ ‖f‖ = HPow.hPow (α := ℝ) (∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (1 / p.toReal)
have 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)) ↦ (↑sorry.toFinset (s := {i : α | ¬(↑f : (i : α) → E i) i = 0}).card : ℝ)) sorry 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: dsimp [norm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
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)
have 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)) ↦ (↑sorry.toFinset (s := {i : α | ¬(↑f : (i : α) → E i) i = 0}).card : ℝ)) sorry 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
Cleared hypotheses: hp, f
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
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)
have 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)
Tactic: rw [dif_neg hp.1.ne', if_neg hp.2.ne]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
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)
⊢ (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)
have 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)
Tactic: rw [dif_neg hp.1.ne', if_neg hp.2.ne]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
⊢ ‖f‖ ^ p.toReal = ∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
have rw : HPow.hPow (α := ℝ) (∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (1 / p.toReal * p.toReal) =
  ∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
Tactic: rw [norm_eq_tsum_rpow hp, ← Real.rpow_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
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
⊢ ‖f‖ ^ p.toReal = ∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
have hx : LE.le (α := ℝ) 0 (∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal)
Tactic: rw [norm_eq_tsum_rpow hp, ← Real.rpow_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
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 / p.toReal * p.toReal) =
    ∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
have field_simp : HPow.hPow (α := ℝ) (β := ℝ) (∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) 1 =
  ∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
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) (‖f‖ ^ p.toReal)
have rw : HasSum (α := ℝ) (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal)
Tactic: rw [norm_rpow_eq_tsum hp]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
x : ↥(lp E p)
⊢ ‖toNorm (E := E) x‖ = ‖x‖
have inl : ∀ {x : ↥(lp E 0)}, ‖toNorm (E := E) x‖ = ‖x‖
Tactic: obtain (rfl | rfl | hp) := p.trichotomy
Cleared hypotheses: p, x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
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‖
⊢ ‖toNorm (E := E) x‖ = ‖x‖
have inr : ∀ {x : ↥(lp E ∞)}, ‖toNorm (E := E) x‖ = ‖x‖
Tactic: obtain (rfl | rfl | hp) := p.trichotomy
Cleared hypotheses: p, x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
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‖
⊢ ‖toNorm (E := E) x‖ = ‖x‖
have inr₁ : ∀ (hp : 0 < p.toReal), ‖toNorm (E := E) x‖ = ‖x‖
Tactic: obtain (rfl | rfl | hp) := p.trichotomy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
⊢ 0 ≤ ‖f‖
have inl : ∀ (f : ↥(lp E 0)), 0 ≤ ‖f‖
Tactic: rcases p.trichotomy with (rfl | rfl | hp)
Cleared hypotheses: p, f
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
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‖
⊢ 0 ≤ ‖f‖
have inr : ∀ (f : ↥(lp E ∞)), 0 ≤ ‖f‖
Tactic: rcases p.trichotomy with (rfl | rfl | hp)
Cleared hypotheses: p, f
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
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‖
⊢ 0 ≤ ‖f‖
have inr₁ : ∀ (hp : 0 < p.toReal), 0 ≤ ‖f‖
Tactic: rcases p.trichotomy with (rfl | rfl | hp)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
⊢ 0 ≤ ‖f‖
have inr : ∀ (_i : IsEmpty α), 0 ≤ ‖f‖
Tactic: rcases isEmpty_or_nonempty α with _i | _i
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
inr : ∀ (_i : IsEmpty α), 0 ≤ ‖f‖
⊢ 0 ≤ ‖f‖
have inr₁ : ∀ (_i : Nonempty α), 0 ≤ ‖f‖
Tactic: rcases isEmpty_or_nonempty α with _i | _i
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
_i : Nonempty α
⊢ 0 ≤ ‖f‖
have inr : ∀ (inhabited_h : Inhabited α), 0 ≤ ‖f‖
Tactic: inhabit α
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
hp : 0 < p.toReal
⊢ 0 ≤ ‖f‖
have inr : 0 ≤ HPow.hPow (α := ℝ) (∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (1 / p.toReal)
Tactic: rw [lp.norm_eq_tsum_rpow hp f]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
⊢ norm (E := ↥(lp E p)) 0 = 0
have inl : norm (E := ↥(lp E 0)) 0 = 0
Tactic: rcases p.trichotomy with (rfl | rfl | hp)
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inl : norm (E := ↥(lp E 0)) 0 = 0
⊢ norm (E := ↥(lp E p)) 0 = 0
have inr : norm (E := ↥(lp E ∞)) 0 = 0
Tactic: rcases p.trichotomy with (rfl | rfl | hp)
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
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
⊢ norm (E := ↥(lp E p)) 0 = 0
have inr₁ : ∀ (hp : 0 < p.toReal), norm (E := ↥(lp E p)) 0 = 0
Tactic: rcases p.trichotomy with (rfl | rfl | hp)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
⊢ norm (E := ↥(lp E p)) 0 = 0
have inr : HPow.hPow (α := ℝ) (∑' (i : α), norm.{u_4} (E := E i) ((↑0 : (i : α) → E i) i) ^ p.toReal) (1 / p.toReal) = 0
Tactic: rw [lp.norm_eq_tsum_rpow hp]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
⊢ HPow.hPow (α := ℝ) (∑' (i : α), norm.{u_4} (E := E i) ((↑0 : (i : α) → E i) i) ^ p.toReal) (1 / p.toReal) = 0
have hp' : 1 / p.toReal ≠ 0
Tactic: have hp' : 1 / p.toReal ≠ 0 := one_div_ne_zero hp.ne'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
⊢ ‖f‖ = 0 ↔ f = 0
have refine : ∀ (h : ‖f‖ = 0), f = 0
Tactic: refine ⟨fun h => ?_, by rintro rfl; exact norm_zero⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
⊢ f = 0
have inl : ∀ {f : ↥(lp E 0)} (h : ‖f‖ = 0), f = 0
Tactic: rcases p.trichotomy with (rfl | rfl | hp)
Cleared hypotheses: p, f, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
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
⊢ f = 0
have inr : ∀ {f : ↥(lp E ∞)} (h : ‖f‖ = 0), f = 0
Tactic: rcases p.trichotomy with (rfl | rfl | hp)
Cleared hypotheses: p, f, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
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
⊢ f = 0
have inr₁ : ∀ (hp : 0 < p.toReal), f = 0
Tactic: rcases p.trichotomy with (rfl | rfl | hp)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E 0)
h : ‖f‖ = 0
⊢ f = 0
have inl : ∀ (i : α), (↑f : (i : α) → E i) i = (↑0 : (i : α) → E i) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E 0)
h : ‖f‖ = 0
i : α
⊢ (↑f : (i : α) → E i) i = (↑0 : (i : α) → E i) i
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
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 : (i : α) → E i) i
have this₁ : (¬(↑f : (i : α) → E i) i = 0) = False
Tactic: have : (¬f i = 0) = False := congr_fun this i
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
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
⊢ (↑f : (i : α) → E i) i = (↑0 : (i : α) → E i) i
have inl : ¬¬(↑f : (i : α) → E i) i = 0 → ¬False → (↑f : (i : α) → E i) i = (↑0 : (i : α) → E i) i
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
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
⊢ (↑f : (i : α) → E i) i = (↑0 : (i : α) → E i) i
have inl₃ : (↑f : (i : α) → E i) i = 0 → ¬False → (↑f : (i : α) → E i) i = (↑0 : (i : α) → E i) i
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
h : ‖f‖ = 0
⊢ f = 0
have inr : ∀ (_i : IsEmpty α), f = 0
Tactic: rcases isEmpty_or_nonempty α with _i | _i
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
h : ‖f‖ = 0
inr : ∀ (_i : IsEmpty α), f = 0
⊢ f = 0
have inr₁ : ∀ (_i : Nonempty α), f = 0
Tactic: rcases isEmpty_or_nonempty α with _i | _i
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
h : ‖f‖ = 0
_i : Nonempty α
⊢ f = 0
have H : 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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
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
⊢ f = 0
have inr : ∀ (i : α), (↑f : (i : α) → E i) i = (↑0 : (i : α) → E i) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
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 : (i : α) → E i) i
have this : ‖(↑f : (i : α) → E i) i‖ = 0
Tactic: have : ‖f i‖ = 0 := le_antisymm (H.1 ⟨i, rfl⟩) (norm_nonneg _)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
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
have this : HasSum (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (‖f‖ ^ p.toReal)
Tactic: have := lp.hasSum_norm hp f
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
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)
⊢ HasSum (α := ℝ) (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) 0
have 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
Tactic: rwa [h, Real.zero_rpow hp.ne'] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
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
⊢ HasSum (α := ℝ) (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) 0
have rwa₁ : ∀ (this : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
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
⊢ f = 0
have hf : 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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
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
⊢ f = 0
have this : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
Tactic: have : ∀ i, 0 ≤ ‖f i‖ ^ p.toReal := fun i ↦ by positivity
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
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
⊢ f = 0
have hf₁ : Eq.{u_3 + 1} (α := α → ℝ) (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) 0
Tactic: rw [hasSum_zero_iff_of_nonneg this] at hf
Cleared hypotheses: hf, this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
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
⊢ f = 0
have inr : ∀ (i : α), (↑f : (i : α) → E i) i = (↑0 : (i : α) → E i) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
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 : (i : α) → E i) i
have this₁ : (↑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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
⊢ f = 0 ↔ (↑f : (i : α) → E i) = 0
have rw : (↑f : (i : α) → E i) = (↑0 : (i : α) → E i) ↔ (↑f : (i : α) → E i) = 0
Tactic: rw [lp.ext_iff, coeFn_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
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
⊢ f = 0 ↔ (↑f : (i : α) → E i) = 0
have rw₁ : (↑f : (i : α) → E i) = 0 ↔ (↑f : (i : α) → E i) = 0
Tactic: rw [lp.ext_iff, coeFn_zero]