awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : (i : α) → StarAddMonoid (E i)
inst_2 : ∀ (i : α), NormedStarGroup.{u_4} (E i)
hp : Fact (LE.le (α := ℝ≥0∞) 1 0)
f : ↥(lp E 0)
⊢ False
have this : ENNReal.toReal 1 ≤ ENNReal.toReal 0
Tactic: have := ENNReal.toReal_mono ENNReal.zero_ne_top hp.elim
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
I : Type u_5
B : I → Type u_6
inst : (i : I) → NonUnitalNormedRing (B i)
f g : (i : I) → B i
hf : Memℓp (E := B) f ∞
hg : Memℓp (E := B) g ∞
⊢ Memℓp (E := B) (f * g) ∞
have rw : BddAbove (α := ℝ) (Set.range fun (i : I) ↦ ‖(f * g) i‖)
Tactic: rw [memℓp_infty_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
I : Type u_5
B : I → Type u_6
inst : (i : I) → NonUnitalNormedRing (B i)
f g : (i : I) → B i
hf : Memℓp (E := B) f ∞
hg : Memℓp (E := B) g ∞
⊢ BddAbove (α := ℝ) (Set.range fun (i : I) ↦ ‖(f * g) i‖)
have obtain : ∀ (Cf : ℝ) (hCf : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : I) ↦ ‖f i‖)) Cf) (Cg : ℝ)
  (hCg : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : I) ↦ ‖g i‖)) Cg),
  BddAbove (α := ℝ) (Set.range fun (i : I) ↦ ‖(f * g) i‖)
Tactic: obtain ⟨⟨Cf, hCf⟩, ⟨Cg, hCg⟩⟩ := hf.bddAbove, hg.bddAbove
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
I : Type u_5
B : I → Type u_6
inst : (i : I) → NonUnitalNormedRing (B i)
f g : (i : I) → B i
hf : Memℓp (E := B) f ∞
hg : Memℓp (E := B) g ∞
Cf : ℝ
hCf : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : I) ↦ ‖f i‖)) Cf
Cg : ℝ
hCg : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : I) ↦ ‖g i‖)) Cg
⊢ BddAbove (α := ℝ) (Set.range fun (i : I) ↦ ‖(f * g) i‖)
have refine : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : I) ↦ ‖(f * g) i‖)) (Cf * Cg)
Tactic: refine ⟨Cf * Cg, ?_⟩
-- 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)
I : Type u_5
B : I → Type u_6
inst_1 : (i : I) → NonUnitalNormedRing (B i)
inst_2 : (i : I) → StarRing (B i)
inst_3 : ∀ (i : I), NormedStarGroup.{u_6} (B i)
inst_4 : ∀ (i : I), CStarRing.{u_6} (B i)
f : ↥(lp B ∞)
⊢ ‖f‖ * ‖f‖ ≤ ‖star f * f‖
have rw : ‖f‖ ≤ √‖star f * f‖
Tactic: rw [← sq, ← Real.le_sqrt (norm_nonneg _) (norm_nonneg _)]
-- 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)
I : Type u_5
B : I → Type u_6
inst_1 : (i : I) → NonUnitalNormedRing (B i)
inst_2 : (i : I) → StarRing (B i)
inst_3 : ∀ (i : I), NormedStarGroup.{u_6} (B i)
inst_4 : ∀ (i : I), CStarRing.{u_6} (B i)
f : ↥(lp B ∞)
⊢ ‖f‖ ≤ √‖star f * f‖
have refine : ∀ (i : I), ‖(↑f : (i : I) → B i) i‖ ≤ √‖star f * f‖
Tactic: refine lp.norm_le_of_forall_le ‖star f * f‖.sqrt_nonneg fun i => ?_
-- 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)
I : Type u_5
B : I → Type u_6
inst_1 : (i : I) → NonUnitalNormedRing (B i)
inst_2 : (i : I) → StarRing (B i)
inst_3 : ∀ (i : I), NormedStarGroup.{u_6} (B i)
inst_4 : ∀ (i : I), CStarRing.{u_6} (B i)
f : ↥(lp B ∞)
i : I
⊢ ‖(↑f : (i : I) → B i) i‖ ≤ √‖star f * f‖
have rw : ‖star ((↑f : (i : I) → B i) i) * (↑f : (i : I) → B i) i‖ ≤ ‖star f * f‖
Tactic: rw [Real.le_sqrt (norm_nonneg _) (norm_nonneg _), sq, ← CStarRing.norm_star_mul_self]
-- 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)
I : Type u_5
B : I → Type u_6
inst_1 : (i : I) → NormedRing (B i)
inst_2 : ∀ (i : I), NormOneClass.{u_6} (B i)
inst_3 : Nonempty I
⊢ norm (E := ↥(lp B ∞)) 1 = 1
have simp_rw : Eq (α := ℝ) (⨆ (i : I), norm.{u_6} (E := B i) ((↑1 : (i : I) → B i) i)) 1
Tactic: simp_rw [lp.norm_eq_ciSup, infty_coeFn_one, Pi.one_apply, norm_one, ciSup_const]
-- 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)
I : Type u_5
B : I → Type u_6
inst_1 : (i : I) → NormedRing (B i)
inst_2 : ∀ (i : I), NormOneClass.{u_6} (B i)
inst_3 : Nonempty I
simp_rw : Eq (α := ℝ) (⨆ (i : I), norm.{u_6} (E := B i) ((↑1 : (i : I) → B i) i)) 1
⊢ norm (E := ↥(lp B ∞)) 1 = 1
have simp_rw₁ : Eq (α := ℝ) (⨆ (i : I), norm.{u_6} (E := B i) (1 i)) 1
Tactic: simp_rw [lp.norm_eq_ciSup, infty_coeFn_one, Pi.one_apply, norm_one, ciSup_const]
-- 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)
I : Type u_5
B : I → Type u_6
inst_1 : (i : I) → NormedRing (B i)
inst_2 : ∀ (i : I), NormOneClass.{u_6} (B i)
inst_3 : Nonempty I
simp_rw : Eq (α := ℝ) (⨆ (i : I), norm.{u_6} (E := B i) ((↑1 : (i : I) → B i) i)) 1
simp_rw₁ : Eq (α := ℝ) (⨆ (i : I), norm.{u_6} (E := B i) (1 i)) 1
⊢ norm (E := ↥(lp B ∞)) 1 = 1
have simp_rw₂ : Eq (α := ℝ) (⨆ (i : I), norm.{u_6} (E := B i) 1) 1
Tactic: simp_rw [lp.norm_eq_ciSup, infty_coeFn_one, Pi.one_apply, norm_one, ciSup_const]
-- 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)
I : Type u_5
B : I → Type u_6
inst_1 : (i : I) → NormedRing (B i)
inst_2 : ∀ (i : I), NormOneClass.{u_6} (B i)
inst_3 : Nonempty I
simp_rw : Eq (α := ℝ) (⨆ (i : I), norm.{u_6} (E := B i) ((↑1 : (i : I) → B i) i)) 1
simp_rw₁ : Eq (α := ℝ) (⨆ (i : I), norm.{u_6} (E := B i) (1 i)) 1
simp_rw₂ : Eq (α := ℝ) (⨆ (i : I), norm.{u_6} (E := B i) 1) 1
⊢ norm (E := ↥(lp B ∞)) 1 = 1
have simp_rw₃ : Eq (α := ℝ) (⨆ (i : I), 1) 1
Tactic: simp_rw [lp.norm_eq_ciSup, infty_coeFn_one, Pi.one_apply, norm_one, ciSup_const]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
I : Type u_5
B : I → Type u_6
inst : NormedField 𝕜
inst_1 : (i : I) → NormedRing (B i)
inst_2 : (i : I) → NormedAlgebra.{u_1, u_6} 𝕜 (B i)
inst_3 : ∀ (i : I), NormOneClass.{u_6} (B i)
k : 𝕜
⊢ Memℓp (E := B) ((algebraMap 𝕜 ((i : I) → B i) : (a : 𝕜) → (i : I) → B i) k) ∞
have rw : Memℓp (E := B) (HSMul.hSMul (β := (i : I) → B i) k 1) ∞
Tactic: rw [Algebra.algebraMap_eq_smul_one]
-- 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_1 q : ℝ≥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)
inst_4 : DecidableEq α
p : ℝ≥0∞
i : α
a : E i
⊢ Membership.mem (γ := AddSubgroup (PreLp E)) (lp E p) (Pi.single (M := E) i a)
have refine : Set.Finite.{u_3} (α := α) {i_1 : α | Pi.single (M := E) i a i_1 ≠ 0}
Tactic: refine (memℓp_zero ?_).of_exponent_ge zero_le
-- 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_1 q : ℝ≥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)
inst_4 : DecidableEq α
p : ℝ≥0∞
i : α
a : E i
⊢ Set.Finite.{u_3} (α := α) {i_1 : α | Pi.single (M := E) i a i_1 ≠ 0}
have refine : Subset (α := Set α) {i_1 : α | Pi.single (M := E) i a i_1 ≠ 0} {i}
Tactic: refine (Set.finite_singleton i).subset ?_
-- 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_1 q : ℝ≥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)
inst_4 : DecidableEq α
p : ℝ≥0∞
i : α
a : E i
j : α
⊢ ¬Pi.single (M := E) i a j = 0 → j = i
have rw : ¬j = i → Pi.single (M := E) i a j = 0
Tactic: rw [not_imp_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
α : Type u_3
inst : NormedRing 𝕜
inst_1 : DecidableEq α
i : α
⊢ Eq (α := ↥(lp (fun (x : α) ↦ 𝕜) 0)) ((zeroBasis : (a : α) → ↥(lp (fun (x : α) ↦ 𝕜) 0)) i : ↥(lp (fun (x : α) ↦ 𝕜) 0))
    (lp.single (E := fun (x : α) ↦ 𝕜) 0 i 1 : ↥(lp (fun (x : α) ↦ 𝕜) 0))
have h : ∀ (x : α),
  Eq.{u_1 + 1} (α := 𝕜) ((↑((zeroBasis : (a : α) → ↥(lp (fun (x : α) ↦ 𝕜) 0)) i) : (i : α) → 𝕜) x : 𝕜)
    ((↑(lp.single (E := fun (x : α) ↦ 𝕜) 0 i 1) : (i : α) → 𝕜) x : 𝕜)
Tactic: ext
-- 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)
inst_1 : DecidableEq α
hp : 0 < p.toReal
f : (i : α) → E i
s : Finset α
⊢ norm (E := ↥(lp E p)) (∑ i ∈ s, lp.single (E := E) p i (f i)) ^ p.toReal = ∑ i ∈ s, ‖f i‖ ^ p.toReal
have refine : HasSum (α := ℝ)
  (fun (i : α) ↦ norm.{u_4} (E := E i) ((↑(∑ i ∈ s, lp.single (E := E) p i (f i)) : (i : α) → E i) i) ^ p.toReal)
  (∑ i ∈ s, ‖f i‖ ^ p.toReal)
Tactic: refine (hasSum_norm hp (∑ i ∈ s, lp.single p i (f i))).unique ?_
-- 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)
inst_1 : DecidableEq α
hp : 0 < p.toReal
f : (i : α) → E i
s : Finset α
⊢ HasSum (α := ℝ)
    (fun (i : α) ↦ norm.{u_4} (E := E i) ((↑(∑ i ∈ s, lp.single (E := E) p i (f i)) : (i : α) → E i) i) ^ p.toReal)
    (∑ i ∈ s, ‖f i‖ ^ p.toReal)
have simp : HasSum (α := ℝ) (fun (i : α) ↦ ‖if i ∈ s then f i else 0‖ ^ p.toReal) (∑ i ∈ s, ‖f i‖ ^ p.toReal)
Tactic: simp only [lp.coeFn_single, coeFn_sum, Finset.sum_apply, Finset.sum_pi_single]
-- 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)
inst_1 : DecidableEq α
hp : 0 < p.toReal
f : (i : α) → E i
s : Finset α
⊢ HasSum (α := ℝ) (fun (i : α) ↦ ‖if i ∈ s then f i else 0‖ ^ p.toReal) (∑ i ∈ s, ‖f i‖ ^ p.toReal)
have h : ∀ i ∉ s, ‖if i ∈ s then f i else 0‖ ^ p.toReal = 0
Tactic: have h : ∀ i ∉ s, ‖ite (i ∈ s) (f i) 0‖ ^ p.toReal = 0 := fun i hi ↦ by
    simp [if_neg hi, Real.zero_rpow 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)
inst_1 : DecidableEq α
hp : 0 < p.toReal
f : (i : α) → E i
s : Finset α
h : ∀ i ∉ s, ‖if i ∈ s then f i else 0‖ ^ p.toReal = 0
i : α
hi : i ∈ s
⊢ ‖f i‖ ^ p.toReal = ‖if i ∈ s then f i else 0‖ ^ p.toReal
have rw : ‖f i‖ ^ p.toReal = ‖f i‖ ^ p.toReal
Tactic: rw [if_pos hi]
-- 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)
inst_1 : DecidableEq α
hp : 0 < p.toReal
f : (i : α) → E i
s : Finset α
h : ∀ i ∉ s, ‖if i ∈ s then f i else 0‖ ^ p.toReal = 0
⊢ HasSum (α := ℝ) (fun (i : α) ↦ ‖if i ∈ s then f i else 0‖ ^ p.toReal) (∑ i ∈ s, ‖f i‖ ^ p.toReal)
have h' : ∀ i ∈ s, ‖f i‖ ^ p.toReal = ‖if i ∈ s then f i else 0‖ ^ p.toReal
Tactic: have h' : ∀ i ∈ s, ‖f i‖ ^ p.toReal = ‖ite (i ∈ s) (f i) 0‖ ^ p.toReal := by
    intro i hi
    rw [if_pos hi]
-- 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)
inst_1 : DecidableEq α
hp : 0 < p
i : α
x : E i
⊢ norm (E := ↥(lp E p)) (lp.single (E := E) p i x) = ‖x‖
have this : Nonempty α
Tactic: haveI : Nonempty α := ⟨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)
inst_1 : DecidableEq α
i : α
x : E i
this : Nonempty α
hp : LT.lt (α := ℝ≥0∞) 0 ∞
⊢ norm (E := ↥(lp E ∞)) (lp.single (E := E) ∞ i x) = ‖x‖
have top : ⨆ (i_1 : α), ‖Pi.single (M := E) i x i_1‖ = ‖x‖
Tactic: simp only [norm_eq_ciSup, lp.coeFn_single]
-- 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)
inst_1 : DecidableEq α
i : α
x : E i
this : Nonempty α
hp : LT.lt (α := ℝ≥0∞) 0 ∞
⊢ ⨆ (i_1 : α), ‖Pi.single (M := E) i x i_1‖ = ‖x‖
have top : ∀ (j : α), ‖Pi.single (M := E) i x j‖ ≤ ‖x‖
Tactic: refine
      ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun j => ?_) fun n hn => ⟨i, hn.trans_eq ?_⟩
-- 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)
inst_1 : DecidableEq α
i : α
x : E i
this : Nonempty α
hp : LT.lt (α := ℝ≥0∞) 0 ∞
top : ∀ (j : α), ‖Pi.single (M := E) i x j‖ ≤ ‖x‖
⊢ ⨆ (i_1 : α), ‖Pi.single (M := E) i x i_1‖ = ‖x‖
have top₁ : ∀ (n : ℝ) (hn : n < ‖x‖), ‖x‖ = ‖Pi.single (M := E) i x i‖
Tactic: refine
      ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun j => ?_) fun n hn => ⟨i, hn.trans_eq ?_⟩
-- 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)
inst_1 : DecidableEq α
i : α
x : E i
this : Nonempty α
hp : LT.lt (α := ℝ≥0∞) 0 ∞
j : α
⊢ ‖Pi.single (M := E) i x j‖ ≤ ‖x‖
have top : ‖Pi.single (M := E) i x i‖ ≤ ‖x‖
Tactic: obtain rfl | hij := Decidable.eq_or_ne i j
Cleared hypotheses: j
-- 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)
inst_1 : DecidableEq α
i : α
x : E i
this : Nonempty α
hp : LT.lt (α := ℝ≥0∞) 0 ∞
j : α
top : ‖Pi.single (M := E) i x i‖ ≤ ‖x‖
⊢ ‖Pi.single (M := E) i x j‖ ≤ ‖x‖
have top₁ : ∀ (hij : i ≠ j), ‖Pi.single (M := E) i x j‖ ≤ ‖x‖
Tactic: obtain rfl | hij := Decidable.eq_or_ne i j
-- 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)
inst_1 : DecidableEq α
i : α
x : E i
this : Nonempty α
hp : LT.lt (α := ℝ≥0∞) 0 ∞
⊢ ‖Pi.single (M := E) i x i‖ ≤ ‖x‖
have top : ‖x‖ ≤ ‖x‖
Tactic: rw [Pi.single_eq_same]
-- 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)
inst_1 : DecidableEq α
i : α
x : E i
this : Nonempty α
hp : LT.lt (α := ℝ≥0∞) 0 ∞
j : α
hij : i ≠ j
⊢ ‖Pi.single (M := E) i x j‖ ≤ ‖x‖
have top : 0 ≤ ‖x‖
Tactic: rw [Pi.single_eq_of_ne' hij, _root_.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)
inst_1 : DecidableEq α
i : α
x : E i
this : Nonempty α
hp : LT.lt (α := ℝ≥0∞) 0 ∞
n : ℝ
hn : n < ‖x‖
⊢ ‖x‖ = ‖Pi.single (M := E) i x i‖
have top : ‖x‖ = ‖x‖
Tactic: rw [Pi.single_eq_same]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
α : Type u_3
E : α → Type u_4
p_1 : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
i : α
x : E i
this : Nonempty α
p : ℝ≥0
hp : 0 < (↑p : ℝ≥0∞)
⊢ norm (E := ↥(lp E (↑p : ℝ≥0∞))) (lp.single (E := E) (↑p : ℝ≥0∞) i x) = ‖x‖
have this₁ : 0 < (↑p : ℝ≥0∞).toReal
Tactic: have : 0 < (p : ℝ≥0∞).toReal := by simpa using hp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p_1 : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
i : α
x : E i
this_1 : Nonempty α
p : ℝ≥0
hp : 0 < (↑p : ℝ≥0∞)
this : 0 < (↑p : ℝ≥0∞).toReal
⊢ norm (E := ↥(lp E (↑p : ℝ≥0∞))) (lp.single (E := E) (↑p : ℝ≥0∞) i x) = ‖x‖
have rw : 0 ≤ ‖Pi.single (M := E) i x i‖
Tactic: rw [norm_eq_tsum_rpow this, tsum_eq_single i, lp.coeFn_single, one_div,
      Real.rpow_rpow_inv _ this.ne', Pi.single_eq_same]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p_1 : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
i : α
x : E i
this_1 : Nonempty α
p : ℝ≥0
hp : 0 < (↑p : ℝ≥0∞)
this : 0 < (↑p : ℝ≥0∞).toReal
rw : 0 ≤ ‖Pi.single (M := E) i x i‖
⊢ norm (E := ↥(lp E (↑p : ℝ≥0∞))) (lp.single (E := E) (↑p : ℝ≥0∞) i x) = ‖x‖
have coe : ∀ (b' : α),
  b' ≠ i → norm (E := E b') ((↑(lp.single (E := E) (↑p : ℝ≥0∞) i x) : (i : α) → E i) b' : E b') ^ (↑p : ℝ≥0∞).toReal = 0
Tactic: rw [norm_eq_tsum_rpow this, tsum_eq_single i, lp.coeFn_single, one_div,
      Real.rpow_rpow_inv _ this.ne', Pi.single_eq_same]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p_1 : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
i : α
x : E i
this_1 : Nonempty α
p : ℝ≥0
hp : 0 < (↑p : ℝ≥0∞)
this : 0 < (↑p : ℝ≥0∞).toReal
j : α
hji : j ≠ i
⊢ norm (E := E j) ((↑(lp.single (E := E) (↑p : ℝ≥0∞) i x) : (i : α) → E i) j : E j) ^ (↑p : ℝ≥0∞).toReal = 0
have coe : ‖Pi.single (M := E) i x j‖ ^ (↑p : ℝ≥0∞).toReal = 0
Tactic: rw [lp.coeFn_single, Pi.single_eq_of_ne hji, _root_.norm_zero, Real.zero_rpow this.ne']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p_1 : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
i : α
x : E i
this_1 : Nonempty α
p : ℝ≥0
hp : 0 < (↑p : ℝ≥0∞)
this : 0 < (↑p : ℝ≥0∞).toReal
j : α
hji : j ≠ i
coe : ‖Pi.single (M := E) i x j‖ ^ (↑p : ℝ≥0∞).toReal = 0
⊢ norm (E := E j) ((↑(lp.single (E := E) (↑p : ℝ≥0∞) i x) : (i : α) → E i) j : E j) ^ (↑p : ℝ≥0∞).toReal = 0
have coe₁ : norm.{u_4} (E := E j) 0 ^ (↑p : ℝ≥0∞).toReal = 0
Tactic: rw [lp.coeFn_single, Pi.single_eq_of_ne hji, _root_.norm_zero, Real.zero_rpow this.ne']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p_1 : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
i : α
x : E i
this_1 : Nonempty α
p : ℝ≥0
hp : 0 < (↑p : ℝ≥0∞)
this : 0 < (↑p : ℝ≥0∞).toReal
j : α
hji : j ≠ i
coe : ‖Pi.single (M := E) i x j‖ ^ (↑p : ℝ≥0∞).toReal = 0
coe₁ : norm.{u_4} (E := E j) 0 ^ (↑p : ℝ≥0∞).toReal = 0
⊢ norm (E := E j) ((↑(lp.single (E := E) (↑p : ℝ≥0∞) i x) : (i : α) → E i) j : E j) ^ (↑p : ℝ≥0∞).toReal = 0
have coe₂ : HPow.hPow (α := ℝ) 0 (↑p : ℝ≥0∞).toReal = 0
Tactic: rw [lp.coeFn_single, Pi.single_eq_of_ne hji, _root_.norm_zero, Real.zero_rpow this.ne']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p_1 : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
i : α
x : E i
this_1 : Nonempty α
p : ℝ≥0
hp : 0 < (↑p : ℝ≥0∞)
this : 0 < (↑p : ℝ≥0∞).toReal
j : α
hji : j ≠ i
coe : ‖Pi.single (M := E) i x j‖ ^ (↑p : ℝ≥0∞).toReal = 0
coe₁ : norm.{u_4} (E := E j) 0 ^ (↑p : ℝ≥0∞).toReal = 0
coe₂ : HPow.hPow (α := ℝ) 0 (↑p : ℝ≥0∞).toReal = 0
⊢ norm (E := E j) ((↑(lp.single (E := E) (↑p : ℝ≥0∞) i x) : (i : α) → E i) j : E j) ^ (↑p : ℝ≥0∞).toReal = 0
have coe₃ : Eq (α := ℝ) 0 0
Tactic: rw [lp.coeFn_single, Pi.single_eq_of_ne hji, _root_.norm_zero, Real.zero_rpow this.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)
inst_1 : DecidableEq α
hp : 0 < p
i : α
x : E i
this : Nonempty α
⊢ norm (E := ↥(lp E p)) (lp.single (E := E) p i x) = ‖x‖
have top : ∀ (hp : LT.lt (α := ℝ≥0∞) 0 ∞), norm (E := ↥(lp E ∞)) (lp.single (E := E) ∞ i x) = ‖x‖
Tactic: induction p with
  | top =>
    simp only [norm_eq_ciSup, lp.coeFn_single]
    refine
      ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun j => ?_) fun n hn => ⟨i, hn.trans_eq ?_⟩
    · obtain rfl | hij := Decidable.eq_or_ne i j
      · rw [Pi.single_eq_same]
      · rw [Pi.single_eq_of_ne' hij, _root_.norm_zero]
        exact norm_nonneg _
    · rw [Pi.single_eq_same]
  | coe p =>
    have : 0 < (p : ℝ≥0∞).toReal := by simpa using hp
    rw [norm_eq_tsum_rpow this, tsum_eq_single i, lp.coeFn_single, one_div,
      Real.rpow_rpow_inv _ this.ne', Pi.single_eq_same]
    · exact norm_nonneg _
    · intro j hji
      rw [lp.coeFn_single, Pi.single_eq_of_ne hji, _root_.norm_zero, Real.zero_rpow this.ne']
Cleared hypotheses: 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)
inst_1 : DecidableEq α
hp : 0 < p
i : α
x : E i
this : Nonempty α
top : ∀ (hp : LT.lt (α := ℝ≥0∞) 0 ∞), norm (E := ↥(lp E ∞)) (lp.single (E := E) ∞ i x) = ‖x‖
⊢ norm (E := ↥(lp E p)) (lp.single (E := E) p i x) = ‖x‖
have coe : ∀ (p : ℝ≥0) (hp : 0 < (↑p : ℝ≥0∞)), norm (E := ↥(lp E (↑p : ℝ≥0∞))) (lp.single (E := E) (↑p : ℝ≥0∞) i x) = ‖x‖
Tactic: induction p with
  | top =>
    simp only [norm_eq_ciSup, lp.coeFn_single]
    refine
      ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun j => ?_) fun n hn => ⟨i, hn.trans_eq ?_⟩
    · obtain rfl | hij := Decidable.eq_or_ne i j
      · rw [Pi.single_eq_same]
      · rw [Pi.single_eq_of_ne' hij, _root_.norm_zero]
        exact norm_nonneg _
    · rw [Pi.single_eq_same]
  | coe p =>
    have : 0 < (p : ℝ≥0∞).toReal := by simpa using hp
    rw [norm_eq_tsum_rpow this, tsum_eq_single i, lp.coeFn_single, one_div,
      Real.rpow_rpow_inv _ this.ne', Pi.single_eq_same]
    · exact norm_nonneg _
    · intro j hji
      rw [lp.coeFn_single, Pi.single_eq_of_ne hji, _root_.norm_zero, Real.zero_rpow this.ne']
Cleared hypotheses: 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)
inst_1 : DecidableEq α
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
⊢ ‖f‖ ^ p.toReal - ‖f - ∑ i ∈ s, lp.single (E := E) p i ((↑f : (i : α) → E i) i)‖ ^ p.toReal =
    ∑ i ∈ s, ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
have refine : HasSum (α := ℝ)
  (fun (b : α) ↦
    ‖(↑f : (i : α) → E i) b‖ ^ p.toReal -
      ‖(↑(f - ∑ i ∈ s, lp.single (E := E) p i ((↑f : (i : α) → E i) i)) : (i : α) → E i) b‖ ^ p.toReal)
  (∑ i ∈ s, ‖(↑f : (i : α) → E i) i‖ ^ p.toReal)
Tactic: refine ((hasSum_norm hp f).sub (hasSum_norm hp (f - ∑ i ∈ s, lp.single p i (f i)))).unique ?_
-- 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)
inst_1 : DecidableEq α
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
F : α → ℝ :=
  fun (i : α) ↦
    ‖(↑f : (i : α) → E i) i‖ ^ p.toReal -
      ‖(↑(f - ∑ i ∈ s, lp.single (E := E) p i ((↑f : (i : α) → E i) i)) : (i : α) → E i) i‖ ^ p.toReal
i : α
hi : i ∉ s
⊢ F i = 0
have suffices : ‖(↑f : (i : α) → E i) i‖ ^ p.toReal -
    ‖(↑f : (i : α) → E i) i - if i ∈ s then (↑f : (i : α) → E i) i else 0‖ ^ p.toReal =
  0
Tactic: suffices ‖f i‖ ^ p.toReal - ‖f i - ite (i ∈ s) (f i) 0‖ ^ p.toReal = 0 by
      simpa only [coeFn_sub, coeFn_sum, lp.coeFn_single, Pi.sub_apply, Finset.sum_apply,
        Finset.sum_pi_single, F] using 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)
inst_1 : DecidableEq α
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
F : α → ℝ :=
  fun (i : α) ↦
    ‖(↑f : (i : α) → E i) i‖ ^ p.toReal -
      ‖(↑(f - ∑ i ∈ s, lp.single (E := E) p i ((↑f : (i : α) → E i) i)) : (i : α) → E i) i‖ ^ p.toReal
⊢ HasSum (α := ℝ)
    (fun (b : α) ↦
      ‖(↑f : (i : α) → E i) b‖ ^ p.toReal -
        ‖(↑(f - ∑ i ∈ s, lp.single (E := E) p i ((↑f : (i : α) → E i) i)) : (i : α) → E i) b‖ ^ p.toReal)
    (∑ i ∈ s, ‖(↑f : (i : α) → E i) i‖ ^ p.toReal)
have hF : ∀ i ∉ s, F i = 0
Tactic: have hF : ∀ i ∉ s, F i = 0 := by
    intro i hi
    suffices ‖f i‖ ^ p.toReal - ‖f i - ite (i ∈ s) (f i) 0‖ ^ p.toReal = 0 by
      simpa only [coeFn_sub, coeFn_sum, lp.coeFn_single, Pi.sub_apply, Finset.sum_apply,
        Finset.sum_pi_single, F] using this
    simp only [if_neg hi, sub_zero, sub_self]