awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
f g : ↥(lp G 2)
⊢ Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (∑' (i : ι), ⟪(↑g : (i : ι) → G i) i, (↑f : (i : ι) → G i) i⟫) : 𝕜)
    (∑' (i : ι), ⟪(↑f : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫ : 𝕜)
have conj : Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (∑' (i : ι), ⟪(↑g : (i : ι) → G i) i, (↑f : (i : ι) → G i) i⟫) : 𝕜)
  ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (∑' (i : ι), ⟪(↑g : (i : ι) → G i) i, (↑f : (i : ι) → G i) i⟫) : 𝕜)
Tactic: calc
        conj _ = conj (∑' i, ⟪g i, f i⟫) := by congr
        _ = ∑' i, conj ⟪g i, f i⟫ := RCLike.conjCLE.map_tsum
        _ = ∑' i, ⟪f i, g i⟫ := by simp only [inner_conj_symm]
        _ = _ := by congr
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
f g : ↥(lp G 2)
conj :
  Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (∑' (i : ι), ⟪(↑g : (i : ι) → G i) i, (↑f : (i : ι) → G i) i⟫) : 𝕜)
    ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (∑' (i : ι), ⟪(↑g : (i : ι) → G i) i, (↑f : (i : ι) → G i) i⟫) : 𝕜)
⊢ Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (∑' (i : ι), ⟪(↑g : (i : ι) → G i) i, (↑f : (i : ι) → G i) i⟫) : 𝕜)
    (∑' (i : ι), ⟪(↑f : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫ : 𝕜)
have conj₁ : Eq.{u_2 + 1} (α := 𝕜) (∑' (i : ι), (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(↑g : (i : ι) → G i) i, (↑f : (i : ι) → G i) i⟫)
  (∑' (i : ι), ⟪(↑f : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫)
Tactic: calc
        conj _ = conj (∑' i, ⟪g i, f i⟫) := by congr
        _ = ∑' i, conj ⟪g i, f i⟫ := RCLike.conjCLE.map_tsum
        _ = ∑' i, ⟪f i, g i⟫ := by simp only [inner_conj_symm]
        _ = _ := by congr
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
f g : ↥(lp G 2)
conj :
  Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (∑' (i : ι), ⟪(↑g : (i : ι) → G i) i, (↑f : (i : ι) → G i) i⟫) : 𝕜)
    ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (∑' (i : ι), ⟪(↑g : (i : ι) → G i) i, (↑f : (i : ι) → G i) i⟫) : 𝕜)
conj₁ :
  Eq.{u_2 + 1} (α := 𝕜) (∑' (i : ι), (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(↑g : (i : ι) → G i) i, (↑f : (i : ι) → G i) i⟫)
    (∑' (i : ι), ⟪(↑f : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫)
⊢ Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (∑' (i : ι), ⟪(↑g : (i : ι) → G i) i, (↑f : (i : ι) → G i) i⟫) : 𝕜)
    (∑' (i : ι), ⟪(↑f : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫ : 𝕜)
have conj₂ : Eq.{u_2 + 1} (α := 𝕜) (∑' (i : ι), ⟪(↑f : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫)
  (∑' (i : ι), ⟪(↑f : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫)
Tactic: calc
        conj _ = conj (∑' i, ⟪g i, f i⟫) := by congr
        _ = ∑' i, conj ⟪g i, f i⟫ := RCLike.conjCLE.map_tsum
        _ = ∑' i, ⟪f i, g i⟫ := by simp only [inner_conj_symm]
        _ = _ := by congr
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
f₁ f₂ g : ↥(lp G 2)
⊢ ∑' (i : ι), ⟪(↑(f₁ + f₂) : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫ =
    HAdd.hAdd (α := 𝕜) (∑' (i : ι), ⟪(↑f₁ : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫)
      (∑' (i : ι), ⟪(↑f₂ : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫)
have calc_1 : Eq.{u_2 + 1} (α := 𝕜) (∑' (i : ι), ⟪(↑(f₁ + f₂) : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫)
  (∑' (i : ι), ⟪(↑(f₁ + f₂) : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫)
Tactic: calc
        _ = ∑' i, ⟪(f₁ + f₂) i, g i⟫ := ?_
        _ = ∑' i, (⟪f₁ i, g i⟫ + ⟪f₂ i, g i⟫) := by
          simp only [inner_add_left, Pi.add_apply, coeFn_add]
        _ = (∑' i, ⟪f₁ i, g i⟫) + ∑' i, ⟪f₂ i, g i⟫ := Summable.tsum_add ?_ ?_
        _ = _ := by congr
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
f₁ f₂ g : ↥(lp G 2)
calc_1 :
  Eq.{u_2 + 1} (α := 𝕜) (∑' (i : ι), ⟪(↑(f₁ + f₂) : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫)
    (∑' (i : ι), ⟪(↑(f₁ + f₂) : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫)
⊢ ∑' (i : ι), ⟪(↑(f₁ + f₂) : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫ =
    HAdd.hAdd (α := 𝕜) (∑' (i : ι), ⟪(↑f₁ : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫)
      (∑' (i : ι), ⟪(↑f₂ : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫)
have calc_2 : Summable.{u_2, u_1} (α := 𝕜) fun (i : ι) ↦ ⟪(↑f₁ : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫
Tactic: calc
        _ = ∑' i, ⟪(f₁ + f₂) i, g i⟫ := ?_
        _ = ∑' i, (⟪f₁ i, g i⟫ + ⟪f₂ i, g i⟫) := by
          simp only [inner_add_left, Pi.add_apply, coeFn_add]
        _ = (∑' i, ⟪f₁ i, g i⟫) + ∑' i, ⟪f₂ i, g i⟫ := Summable.tsum_add ?_ ?_
        _ = _ := by congr
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
f₁ f₂ g : ↥(lp G 2)
calc_1 :
  Eq.{u_2 + 1} (α := 𝕜) (∑' (i : ι), ⟪(↑(f₁ + f₂) : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫)
    (∑' (i : ι), ⟪(↑(f₁ + f₂) : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫)
calc_2 : Summable.{u_2, u_1} (α := 𝕜) fun (i : ι) ↦ ⟪(↑f₁ : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫
⊢ ∑' (i : ι), ⟪(↑(f₁ + f₂) : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫ =
    HAdd.hAdd (α := 𝕜) (∑' (i : ι), ⟪(↑f₁ : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫)
      (∑' (i : ι), ⟪(↑f₂ : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫)
have calc_3 : Summable.{u_2, u_1} (α := 𝕜) fun (i : ι) ↦ ⟪(↑f₂ : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫
Tactic: calc
        _ = ∑' i, ⟪(f₁ + f₂) i, g i⟫ := ?_
        _ = ∑' i, (⟪f₁ i, g i⟫ + ⟪f₂ i, g i⟫) := by
          simp only [inner_add_left, Pi.add_apply, coeFn_add]
        _ = (∑' i, ⟪f₁ i, g i⟫) + ∑' i, ⟪f₂ i, g i⟫ := Summable.tsum_add ?_ ?_
        _ = _ := by congr
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
f g : ↥(lp G 2)
c : 𝕜
⊢ ∑' (i : ι), ⟪(↑(c • f) : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫ =
    HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (∑' (i : ι), ⟪(↑f : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫ : 𝕜)
have calc_1 : Eq.{u_2 + 1} (α := 𝕜) (∑' (i : ι), ⟪(↑(c • f) : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫)
  (∑' (i : ι), ⟪c • (↑f : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫)
Tactic: calc
        _ = ∑' i, ⟪c • f i, g i⟫ := ?_
        _ = ∑' i, conj c * ⟪f i, g i⟫ := by simp only [inner_smul_left]
        _ = conj c * ∑' i, ⟪f i, g i⟫ := tsum_mul_left
        _ = _ := ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
f g : ↥(lp G 2)
c : 𝕜
calc_1 :
  Eq.{u_2 + 1} (α := 𝕜) (∑' (i : ι), ⟪(↑(c • f) : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫)
    (∑' (i : ι), ⟪c • (↑f : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫)
⊢ ∑' (i : ι), ⟪(↑(c • f) : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫ =
    HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (∑' (i : ι), ⟪(↑f : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫ : 𝕜)
have calc_2 : HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
    (∑' (i : ι), ⟪(↑f : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫ : 𝕜) =
  HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
    (∑' (i : ι), ⟪(↑f : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫ : 𝕜)
Tactic: calc
        _ = ∑' i, ⟪c • f i, g i⟫ := ?_
        _ = ∑' i, conj c * ⟪f i, g i⟫ := by simp only [inner_smul_left]
        _ = conj c * ∑' i, ⟪f i, g i⟫ := tsum_mul_left
        _ = _ := ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
G : ι → Type u_4
inst_1 : (i : ι) → NormedAddCommGroup (G i)
inst_2 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
inst_3 : DecidableEq ι
i : ι
a : G i
f : ↥(lp G 2)
⊢ ⟪lp.single (E := G) 2 i a, f⟫ = ⟪a, (↑f : (i : ι) → G i) i⟫
have refine : HasSum (fun (i_1 : ι) ↦ ⟪(↑(lp.single (E := G) 2 i a) : (i : ι) → G i) i_1, (↑f : (i : ι) → G i) i_1⟫)
  ⟪a, (↑f : (i : ι) → G i) i⟫
Tactic: refine (hasSum_inner (lp.single 2 i a) f).unique ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
G : ι → Type u_4
inst_1 : (i : ι) → NormedAddCommGroup (G i)
inst_2 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
inst_3 : DecidableEq ι
i : ι
a : G i
f : ↥(lp G 2)
⊢ HasSum (fun (i_1 : ι) ↦ ⟪(↑(lp.single (E := G) 2 i a) : (i : ι) → G i) i_1, (↑f : (i : ι) → G i) i_1⟫)
    ⟪a, (↑f : (i : ι) → G i) i⟫
have simp_rw : HasSum (fun (i_1 : ι) ↦ ⟪Pi.single (M := G) i a i_1, (↑f : (i : ι) → G i) i_1⟫) ⟪a, (↑f : (i : ι) → G i) i⟫
Tactic: simp_rw [lp.coeFn_single]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
G : ι → Type u_4
inst_1 : (i : ι) → NormedAddCommGroup (G i)
inst_2 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
inst_3 : DecidableEq ι
i : ι
a : G i
f : ↥(lp G 2)
⊢ HasSum (fun (i_1 : ι) ↦ ⟪Pi.single (M := G) i a i_1, (↑f : (i : ι) → G i) i_1⟫) ⟪a, (↑f : (i : ι) → G i) i⟫
have h : Eq (α := ι → 𝕜) (fun (i_1 : ι) ↦ ⟪Pi.single (M := G) i a i_1, (↑f : (i : ι) → G i) i_1⟫) fun (b' : ι) ↦
  if b' = i then ⟪a, (↑f : (i : ι) → G i) i⟫ else 0
Tactic: convert! hasSum_ite_eq i ⟪a, f i⟫ using 1
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
G : ι → Type u_4
inst_1 : (i : ι) → NormedAddCommGroup (G i)
inst_2 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
inst_3 : DecidableEq ι
i : ι
a : G i
f : ↥(lp G 2)
⊢ Eq (α := ι → 𝕜) (fun (i_1 : ι) ↦ ⟪Pi.single (M := G) i a i_1, (↑f : (i : ι) → G i) i_1⟫) fun (b' : ι) ↦
    if b' = i then ⟪a, (↑f : (i : ι) → G i) i⟫ else 0
have h : ∀ (j : ι), ⟪Pi.single (M := G) i a j, (↑f : (i : ι) → G i) j⟫ = if j = i then ⟪a, (↑f : (i : ι) → G i) i⟫ else 0
Tactic: ext j
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
G : ι → Type u_4
inst_1 : (i : ι) → NormedAddCommGroup (G i)
inst_2 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
inst_3 : DecidableEq ι
i : ι
a : G i
f : ↥(lp G 2)
j : ι
⊢ ⟪Pi.single (M := G) i a j, (↑f : (i : ι) → G i) j⟫ = if j = i then ⟪a, (↑f : (i : ι) → G i) i⟫ else 0
have pos : ∀ (h : j = i), ⟪Pi.single (M := G) i a j, (↑f : (i : ι) → G i) j⟫ = ⟪a, (↑f : (i : ι) → G i) i⟫
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
G : ι → Type u_4
inst_1 : (i : ι) → NormedAddCommGroup (G i)
inst_2 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
inst_3 : DecidableEq ι
i : ι
a : G i
f : ↥(lp G 2)
j : ι
pos : ∀ (h : j = i), ⟪Pi.single (M := G) i a j, (↑f : (i : ι) → G i) j⟫ = ⟪a, (↑f : (i : ι) → G i) i⟫
⊢ ⟪Pi.single (M := G) i a j, (↑f : (i : ι) → G i) j⟫ = if j = i then ⟪a, (↑f : (i : ι) → G i) i⟫ else 0
have neg : ∀ (h : ¬j = i), ⟪Pi.single (M := G) i a j, (↑f : (i : ι) → G i) j⟫ = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
G : ι → Type u_4
inst_1 : (i : ι) → NormedAddCommGroup (G i)
inst_2 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
inst_3 : DecidableEq ι
i : ι
a : G i
f : ↥(lp G 2)
j : ι
h : j = i
⊢ ⟪Pi.single (M := G) i a j, (↑f : (i : ι) → G i) j⟫ = ⟪a, (↑f : (i : ι) → G i) i⟫
have pos : ∀ (a : G j), ⟪Pi.single (M := G) j a j, (↑f : (i : ι) → G i) j⟫ = ⟪a, (↑f : (i : ι) → G i) j⟫
Tactic: subst h
Cleared hypotheses: i, a, h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
G : ι → Type u_4
inst_1 : (i : ι) → NormedAddCommGroup (G i)
inst_2 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
inst_3 : DecidableEq ι
f : ↥(lp G 2)
j : ι
a : G j
⊢ ⟪Pi.single (M := G) j a j, (↑f : (i : ι) → G i) j⟫ = ⟪a, (↑f : (i : ι) → G i) j⟫
have pos : ⟪a, (↑f : (i : ι) → G i) j⟫ = ⟪a, (↑f : (i : ι) → G i) j⟫
Tactic: rw [Pi.single_eq_same]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
inst_5 : CompleteSpace E
V : (i : ι) → LinearIsometry.{u_2, u_2, u_4, u_3} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
f : ↥(lp G 2)
⊢ Summable.{u_3, u_1} (α := E) fun (i : ι) ↦ (V i : (a : G i) → E) ((↑f : (i : ι) → G i) i)
have rw : Summable (α := ℝ) fun (i : ι) ↦ HPow.hPow (β := ℕ) ‖(↑f : (i : ι) → G i) i‖ 2
Tactic: rw [hV.summable_iff_norm_sq_summable]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
inst_5 : CompleteSpace E
V : (i : ι) → LinearIsometry.{u_2, u_2, u_4, u_3} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
f : ↥(lp G 2)
⊢ Summable (α := ℝ) fun (i : ι) ↦ HPow.hPow (β := ℕ) ‖(↑f : (i : ι) → G i) i‖ 2
have h : ∀ (x : ι), HPow.hPow (β := ℕ) ‖(↑f : (i : ι) → G i) x‖ 2 = ‖(↑f : (i : ι) → G i) x‖ ^ ENNReal.toReal 2
Tactic: convert! (lp.memℓp f).summable _
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
inst_5 : CompleteSpace E
V : (i : ι) → LinearIsometry.{u_2, u_2, u_4, u_3} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
f : ↥(lp G 2)
h : ∀ (x : ι), HPow.hPow (β := ℕ) ‖(↑f : (i : ι) → G i) x‖ 2 = ‖(↑f : (i : ι) → G i) x‖ ^ ENNReal.toReal 2
⊢ Summable (α := ℝ) fun (i : ι) ↦ HPow.hPow (β := ℕ) ‖(↑f : (i : ι) → G i) i‖ 2
have convert! : 0 < ENNReal.toReal 2
Tactic: convert! (lp.memℓp f).summable _
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
inst_5 : CompleteSpace E
V : (i : ι) → LinearIsometry.{u_2, u_2, u_4, u_3} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
f : ↥(lp G 2)
x : ι
⊢ HPow.hPow (β := ℕ) ‖(↑f : (i : ι) → G i) x‖ 2 = ‖(↑f : (i : ι) → G i) x‖ ^ ENNReal.toReal 2
have h : HPow.hPow (β := ℕ) ‖(↑f : (i : ι) → G i) x‖ 2 = HPow.hPow (β := ℕ) ‖(↑f : (i : ι) → G i) x‖ 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (hypothesis)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
inst_5 : CompleteSpace E
V : (i : ι) → LinearIsometry.{u_2, u_2, u_4, u_3} (RingHom.id 𝕜) (G i) E
hV_1 hV : OrthogonalFamily 𝕜 G V
f : ↥(lp G 2)
⊢ norm.{u_3} (E := E)
      (({ toFun := fun (f : ↥(lp G 2)) ↦ ∑' (i : ι), (V i : (a : G i) → E) ((↑f : (i : ι) → G i) i), map_add' := ⋯,
              map_smul' := ⋯ : ↥(lp G 2) →ₗ[𝕜] E } :
            (a : ↥(lp G 2)) → E)
          f :
        E) =
    ‖f‖
have H : 0 < ENNReal.toReal 2
Tactic: have H : 0 < (2 : ℝ≥0∞).toReal := by simp
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
inst_5 : CompleteSpace E
V : (i : ι) → LinearIsometry.{u_2, u_2, u_4, u_3} (RingHom.id 𝕜) (G i) E
hV_1 hV : OrthogonalFamily 𝕜 G V
f : ↥(lp G 2)
H : 0 < ENNReal.toReal 2
⊢ norm.{u_3} (E := E)
      (({ toFun := fun (f : ↥(lp G 2)) ↦ ∑' (i : ι), (V i : (a : G i) → E) ((↑f : (i : ι) → G i) i), map_add' := ⋯,
              map_smul' := ⋯ : ↥(lp G 2) →ₗ[𝕜] E } :
            (a : ↥(lp G 2)) → E)
          f :
        E) =
    ‖f‖
have suffices : norm.{u_3} (E := E) (∑' (i : ι), (V i : (a : G i) → E) ((↑f : (i : ι) → G i) i)) ^ ENNReal.toReal 2 =
  ‖f‖ ^ ENNReal.toReal 2
Tactic: suffices ‖∑' i : ι, V i (f i)‖ ^ (2 : ℝ≥0∞).toReal = ‖f‖ ^ (2 : ℝ≥0∞).toReal by
        exact Real.rpow_left_injOn H.ne' (norm_nonneg _) (norm_nonneg _) this
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
inst_5 : CompleteSpace E
V : (i : ι) → LinearIsometry.{u_2, u_2, u_4, u_3} (RingHom.id 𝕜) (G i) E
hV_1 hV : OrthogonalFamily 𝕜 G V
f : ↥(lp G 2)
H : 0 < ENNReal.toReal 2
⊢ norm.{u_3} (E := E) (∑' (i : ι), (V i : (a : G i) → E) ((↑f : (i : ι) → G i) i)) ^ ENNReal.toReal 2 =
    ‖f‖ ^ ENNReal.toReal 2
have refine : Tendsto (fun (s : Finset ι) ↦ ∑ b ∈ s, (fun (i : ι) ↦ ‖(↑f : (i : ι) → G i) i‖ ^ ENNReal.toReal 2) b)
  (SummationFilter.unconditional ι).filter
  (𝓝 (norm.{u_3} (E := E) (∑' (i : ι), (V i : (a : G i) → E) ((↑f : (i : ι) → G i) i)) ^ ENNReal.toReal 2))
Tactic: refine tendsto_nhds_unique ?_ (lp.hasSum_norm H f)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
inst_5 : CompleteSpace E
V : (i : ι) → LinearIsometry.{u_2, u_2, u_4, u_3} (RingHom.id 𝕜) (G i) E
hV_1 hV : OrthogonalFamily 𝕜 G V
f : ↥(lp G 2)
H : 0 < ENNReal.toReal 2
⊢ Tendsto (fun (s : Finset ι) ↦ ∑ b ∈ s, (fun (i : ι) ↦ ‖(↑f : (i : ι) → G i) i‖ ^ ENNReal.toReal 2) b)
    (SummationFilter.unconditional ι).filter
    (𝓝 (norm.{u_3} (E := E) (∑' (i : ι), (V i : (a : G i) → E) ((↑f : (i : ι) → G i) i)) ^ ENNReal.toReal 2))
have h : Eq.{u_1 + 1} (α := Finset ι → ℝ)
  (fun (s : Finset ι) ↦ ∑ b ∈ s, (fun (i : ι) ↦ ‖(↑f : (i : ι) → G i) i‖ ^ ENNReal.toReal 2) b) fun (a : Finset ι) ↦
  norm.{u_3} (E := E) (∑ b ∈ a, (fun (i : ι) ↦ ((V i : (a : G i) → E) ((↑f : (i : ι) → G i) i) : E)) b) ^
    ENNReal.toReal 2
Tactic: convert! (hV.summable_of_lp f).hasSum.norm.rpow_const (Or.inr H.le) using 1
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
inst_5 : CompleteSpace E
V : (i : ι) → LinearIsometry.{u_2, u_2, u_4, u_3} (RingHom.id 𝕜) (G i) E
hV_1 hV : OrthogonalFamily 𝕜 G V
f : ↥(lp G 2)
H : 0 < ENNReal.toReal 2
⊢ Eq.{u_1 + 1} (α := Finset ι → ℝ)
    (fun (s : Finset ι) ↦ ∑ b ∈ s, (fun (i : ι) ↦ ‖(↑f : (i : ι) → G i) i‖ ^ ENNReal.toReal 2) b) fun (a : Finset ι) ↦
    norm.{u_3} (E := E) (∑ b ∈ a, (fun (i : ι) ↦ ((V i : (a : G i) → E) ((↑f : (i : ι) → G i) i) : E)) b) ^
      ENNReal.toReal 2
have h : ∀ (s : Finset ι),
  ∑ b ∈ s, (fun (i : ι) ↦ ‖(↑f : (i : ι) → G i) i‖ ^ ENNReal.toReal 2) b =
    norm.{u_3} (E := E) (∑ b ∈ s, (fun (i : ι) ↦ ((V i : (a : G i) → E) ((↑f : (i : ι) → G i) i) : E)) b) ^
      ENNReal.toReal 2
Tactic: ext s
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
inst_5 : CompleteSpace E
V : (i : ι) → LinearIsometry.{u_2, u_2, u_4, u_3} (RingHom.id 𝕜) (G i) E
hV_1 hV : OrthogonalFamily 𝕜 G V
f : ↥(lp G 2)
⊢ norm.{u_3} (E := E)
      (({ toFun := fun (f : ↥(lp G 2)) ↦ ∑' (i : ι), (V i : (a : G i) → E) ((↑f : (i : ι) → G i) i), map_add' := ⋯,
              map_smul' := ⋯ : ↥(lp G 2) →ₗ[𝕜] E } :
            (a : ↥(lp G 2)) → E)
          f :
        E) =
    ‖f‖
have needed : 0 < ENNReal.toReal 2
Tactic: classical
      -- needed for lattice instance on `Finset ι`, for `Filter.atTop_neBot`
      have H : 0 < (2 : ℝ≥0∞).toReal := by simp
      suffices ‖∑' i : ι, V i (f i)‖ ^ (2 : ℝ≥0∞).toReal = ‖f‖ ^ (2 : ℝ≥0∞).toReal by
        exact Real.rpow_left_injOn H.ne' (norm_nonneg _) (norm_nonneg _) this
      refine tendsto_nhds_unique ?_ (lp.hasSum_norm H f)
      convert! (hV.summable_of_lp f).hasSum.norm.rpow_const (Or.inr H.le) using 1
      ext s
      exact mod_cast (hV.norm_sum f s).symm
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
inst_5 : CompleteSpace E
V : (i : ι) → LinearIsometry.{u_2, u_2, u_4, u_3} (RingHom.id 𝕜) (G i) E
hV_1 hV : OrthogonalFamily 𝕜 G V
f : ↥(lp G 2)
needed : 0 < ENNReal.toReal 2
⊢ norm.{u_3} (E := E)
      (({ toFun := fun (f : ↥(lp G 2)) ↦ ∑' (i : ι), (V i : (a : G i) → E) ((↑f : (i : ι) → G i) i), map_add' := ⋯,
              map_smul' := ⋯ : ↥(lp G 2) →ₗ[𝕜] E } :
            (a : ↥(lp G 2)) → E)
          f :
        E) =
    ‖f‖
have needed₁ : ∀ (H : 0 < ENNReal.toReal 2),
  norm.{u_3} (E := E)
      (({ toFun := fun (f : ↥(lp G 2)) ↦ ∑' (i : ι), (V i : (a : G i) → E) ((↑f : (i : ι) → G i) i), map_add' := sorry,
              map_smul' := sorry : ↥(lp G 2) →ₗ[𝕜] E } :
            (a : ↥(lp G 2)) → E)
          f :
        E) =
    ‖f‖
Tactic: classical
      -- needed for lattice instance on `Finset ι`, for `Filter.atTop_neBot`
      have H : 0 < (2 : ℝ≥0∞).toReal := by simp
      suffices ‖∑' i : ι, V i (f i)‖ ^ (2 : ℝ≥0∞).toReal = ‖f‖ ^ (2 : ℝ≥0∞).toReal by
        exact Real.rpow_left_injOn H.ne' (norm_nonneg _) (norm_nonneg _) this
      refine tendsto_nhds_unique ?_ (lp.hasSum_norm H f)
      convert! (hV.summable_of_lp f).hasSum.norm.rpow_const (Or.inr H.le) using 1
      ext s
      exact mod_cast (hV.norm_sum f s).symm