awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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⟫)
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⟫)
⊢ 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⟫ : 𝕜)

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

Premises used: ContinuousLinearEquiv.map_tsum, RCLike.conjCLE, starRingEnd, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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)
⊢ 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:
?_
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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)
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑' (i : ι), ⟪(↑(f₁ + f₂) : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫)
    (∑' (i : ι),
      (⟪(↑f₁ : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫ + ⟪(↑f₂ : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫))

Tactic:
simp only [inner_add_left, Pi.add_apply, coeFn_add]

Premises used: lp.coeFn_add, inner_add_left, Pi.add_apply
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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₁ : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫ + ⟪(↑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⟫)

Tactic:
Summable.tsum_add ?_ ?_

Premises used: Summable.tsum_add
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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)
⊢ HAdd.hAdd (α := 𝕜) (∑' (i : ι), ⟪(↑f₁ : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫)
      (∑' (i : ι), ⟪(↑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⟫)

Tactic:
congr
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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⟫
calc_3 : 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⟫)

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

Premises used: Summable.tsum_add
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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)
⊢ 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:
congr
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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)
⊢ Summable.{u_2, u_1} (α := 𝕜) fun (i : ι) ↦ ⟪(↑f₁ : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫

Tactic:
summable_inner f₁ g

Premises used: lp.summable_inner
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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)
⊢ Summable.{u_2, u_1} (α := 𝕜) fun (i : ι) ↦ ⟪(↑f₁ : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫

Tactic:
exact summable_inner f₁ g

Premises used: lp.summable_inner
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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)
⊢ Summable.{u_2, u_1} (α := 𝕜) fun (i : ι) ↦ ⟪(↑f₂ : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫

Tactic:
summable_inner f₂ g

Premises used: lp.summable_inner
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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)
⊢ Summable.{u_2, u_1} (α := 𝕜) fun (i : ι) ↦ ⟪(↑f₂ : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫

Tactic:
exact summable_inner f₂ g

Premises used: lp.summable_inner
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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 : 𝕜
⊢ 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:
?_
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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 : 𝕜
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑' (i : ι), ⟪c • (↑f : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫)
    (∑' (i : ι),
      HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) ⟪(↑f : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫)

Tactic:
simp only [inner_smul_left]

Premises used: inner_smul_left
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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 : ι),
      HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) 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⟫ : 𝕜)

Tactic:
tsum_mul_left

Premises used: tsum_mul_left
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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 : 𝕜
⊢ 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:
?_
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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⟫)
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⟫ : 𝕜)
⊢ ∑' (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⟫ : 𝕜)

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
        _ = _ := ?_

Premises used: tsum_mul_left, starRingEnd, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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 : 𝕜
⊢ 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:
simp only [coeFn_smul, Pi.smul_apply]

Premises used: lp.coeFn_smul, Pi.smul_apply
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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 : 𝕜
⊢ 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:
congr
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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)
f g : ↥(lp G 2)
⊢ ⟪f, g⟫ = ∑' (i : ι), ⟪(↑f : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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)
f g : ↥(lp G 2)
⊢ HasSum (fun (i : ι) ↦ ⟪(↑f : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫) ⟪f, g⟫

Tactic:
(summable_inner f g).hasSum

Premises used: lp.summable_inner, Summable.hasSum
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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⟫

Tactic:
(hasSum_inner (lp.single 2 i a) f).unique ?_

Premises used: lp.single, lp.hasSum_inner, HasSum.unique, OfNat.ofNat
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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)
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⟫
⊢ ⟪lp.single (E := G) 2 i a, f⟫ = ⟪a, (↑f : (i : ι) → G i) i⟫

Tactic:
refine (hasSum_inner (lp.single 2 i a) f).unique ?_

Premises used: lp.single, lp.hasSum_inner, HasSum.unique, OfNat.ofNat
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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)
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⟫
⊢ 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:
simp_rw [lp.coeFn_single]

Premises used: lp.coeFn_single
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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 (b' : ι) ↦ if b' = i then ⟪a, (↑f : (i : ι) → G i) i⟫ else 0) ⟪a, (↑f : (i : ι) → G i) i⟫

Tactic:
hasSum_ite_eq i ⟪a, f i⟫

Premises used: Inner.inner, hasSum_ite_eq, Subtype.val, SummationFilter.unconditional
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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)
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
⊢ 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:
convert! hasSum_ite_eq i ⟪a, f i⟫ using 1
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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)
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
⊢ 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:
ext j
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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⟫
neg : ∀ (h : ¬j = i), ⟪Pi.single (M := G) i a j, (↑f : (i : ι) → G i) j⟫ = 0
⊢ ⟪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:
split_ifs with h
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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
pos : ∀ (a : G j), ⟪Pi.single (M := G) j a j, (↑f : (i : ι) → G i) j⟫ = ⟪a, (↑f : (i : ι) → G i) j⟫
⊢ ⟪Pi.single (M := G) i a j, (↑f : (i : ι) → G i) j⟫ = ⟪a, (↑f : (i : ι) → G i) i⟫

Tactic:
subst h
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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
pos pos₁ : ⟪a, (↑f : (i : ι) → G i) j⟫ = ⟪a, (↑f : (i : ι) → G i) j⟫
⊢ ⟪Pi.single (M := G) j a j, (↑f : (i : ι) → G i) j⟫ = ⟪a, (↑f : (i : ι) → G i) j⟫

Tactic:
rw [Pi.single_eq_same]

Premises used: Pi.single_eq_same
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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⟫ = 0

Tactic:
simp [Pi.single_eq_of_ne h]

Premises used: Pi.single_eq_of_ne
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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)
⊢ ⟪f, lp.single (E := G) 2 i a⟫ = ⟪(↑f : (i : ι) → G i) i, a⟫

Tactic:
simpa [inner_conj_symm] using congr_arg conj (inner_single_left (𝕜 := 𝕜) i a f)

Premises used: congr_arg, lp.inner_single_left, starRingEnd, DFunLike.coe, inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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)
rw : Summable (α := ℝ) fun (i : ι) ↦ HPow.hPow (β := ℕ) ‖(↑f : (i : ι) → G i) i‖ 2
⊢ Summable.{u_3, u_1} (α := E) fun (i : ι) ↦ (V i : (a : G i) → E) ((↑f : (i : ι) → G i) i)

Tactic:
rw [hV.summable_iff_norm_sq_summable]

Premises used: OrthogonalFamily.summable_iff_norm_sq_summable
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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 : ι) ↦ ‖(↑f : (i : ι) → G i) i‖ ^ ENNReal.toReal 2

Tactic:
(lp.memℓp f).summable _

Premises used: lp.memℓp, Memℓp.summable
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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
convert! : 0 < ENNReal.toReal 2
⊢ Summable (α := ℝ) fun (i : ι) ↦ HPow.hPow (β := ℕ) ‖(↑f : (i : ι) → G i) i‖ 2

Tactic:
convert! (lp.memℓp f).summable _

Premises used: lp.memℓp, Memℓp.summable
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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 : ι
h h₁ h₂ h₃ : HPow.hPow (β := ℕ) ‖(↑f : (i : ι) → G i) x‖ 2 = HPow.hPow (β := ℕ) ‖(↑f : (i : ι) → G i) x‖ 2
⊢ HPow.hPow (β := ℕ) ‖(↑f : (i : ι) → G i) x‖ 2 = ‖(↑f : (i : ι) → G i) x‖ ^ ENNReal.toReal 2

Tactic:
norm_cast
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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)
⊢ 0 < ENNReal.toReal 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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 g : ↥(lp G 2)
⊢ ∑' (i : ι), (V i : (a : G i) → E) ((↑(f + g) : (i : ι) → G i) i) =
    HAdd.hAdd (α := E) (∑' (i : ι), (V i : (a : G i) → E) ((↑f : (i : ι) → G i) i))
      (∑' (i : ι), (V i : (a : G i) → E) ((↑g : (i : ι) → G i) i))

Tactic:
simp only [(hV.summable_of_lp f).tsum_add (hV.summable_of_lp g), lp.coeFn_add, Pi.add_apply,
      LinearIsometry.map_add]

Premises used: LinearIsometry.map_add, lp.coeFn_add, OrthogonalFamily.summable_of_lp, Pi.add_apply, Summable.tsum_add
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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
c : 𝕜
f : ↥(lp G 2)
⊢ ∑' (i : ι), (V i : (a : G i) → E) ((↑(c • f) : (i : ι) → G i) i) =
    HSMul.hSMul (α := 𝕜) (β := E) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (∑' (i : ι), (V i : (a : G i) → E) ((↑f : (i : ι) → G i) i))

Tactic:
simpa only [LinearIsometry.map_smul, Pi.smul_apply, lp.coeFn_smul] using
      (hV.summable_of_lp f).tsum_const_smul c

Premises used: LinearIsometry.map_smul, Summable.tsum_const_smul, OrthogonalFamily.summable_of_lp, lp.coeFn_smul, Pi.smul_apply
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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)
⊢ 0 < ENNReal.toReal 2

Tactic:
simp