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)
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:
have H : 0 < (2 : ℝ≥0∞).toReal := by simp
-- 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)
H : 0 < ENNReal.toReal 2
this :
  norm.{u_3} (E := E) (∑' (i : ι), (V i : (a : G i) → E) ((↑f : (i : ι) → G i) i)) ^ ENNReal.toReal 2 =
    ‖f‖ ^ 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‖

Tactic:
Real.rpow_left_injOn H.ne' (norm_nonneg _) (norm_nonneg _) this

Premises used: LT.lt.ne', Real.rpow_left_injOn, norm_nonneg
-- 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)
H : 0 < ENNReal.toReal 2
this :
  norm.{u_3} (E := E) (∑' (i : ι), (V i : (a : G i) → E) ((↑f : (i : ι) → G i) i)) ^ ENNReal.toReal 2 =
    ‖f‖ ^ 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‖

Tactic:
exact Real.rpow_left_injOn H.ne' (norm_nonneg _) (norm_nonneg _) this

Premises used: LT.lt.ne', Real.rpow_left_injOn, norm_nonneg
-- 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)
H : 0 < ENNReal.toReal 2
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
⊢ 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‖

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
-- 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)
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

Tactic:
tendsto_nhds_unique ?_ (lp.hasSum_norm H f)

Premises used: lp.hasSum_norm, tendsto_nhds_unique
-- 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)
H : 0 < ENNReal.toReal 2
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))
⊢ 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:
refine tendsto_nhds_unique ?_ (lp.hasSum_norm H f)

Premises used: lp.hasSum_norm, tendsto_nhds_unique
-- 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)
H : 0 < ENNReal.toReal 2
⊢ Tendsto
    (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)
    (SummationFilter.unconditional ι).filter
    (𝓝 (norm.{u_3} (E := E) (∑' (b : ι), (V b : (a : G b) → E) ((↑f : (i : ι) → G i) b)) ^ ENNReal.toReal 2))

Tactic:
(hV.summable_of_lp f).hasSum.norm.rpow_const (Or.inr H.le)

Premises used: Filter.Tendsto.norm, LT.lt.le, Filter.Tendsto.rpow_const, OrthogonalFamily.summable_of_lp, Summable.hasSum, Or.inr
-- 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)
H : 0 < ENNReal.toReal 2
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
⊢ 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:
convert! (hV.summable_of_lp f).hasSum.norm.rpow_const (Or.inr H.le) using 1

Premises used: Filter.Tendsto.norm, LT.lt.le, Filter.Tendsto.rpow_const, OrthogonalFamily.summable_of_lp, Summable.hasSum, Or.inr
-- 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)
H : 0 < ENNReal.toReal 2
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
⊢ 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:
ext s
-- 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)
H : 0 < ENNReal.toReal 2
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:
mod_cast (hV.norm_sum f s).symm

Premises used: Norm.norm, congrArg, cast, ENNReal.toReal_natCast, Nat.cast, funext, ENNReal.toReal, HPow.hPow, congr, Eq.refl, OrthogonalFamily.norm_sum, congrFun', OfNat.ofNat, Eq.symm, Subtype.val, Eq, DFunLike.coe, Finset.sum_congr, Finset.sum, Real.rpow_natCast, Eq.trans
-- 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)
H : 0 < ENNReal.toReal 2
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:
exact mod_cast (hV.norm_sum f s).symm

Premises used: OrthogonalFamily.norm_sum, Eq.symm, Subtype.val
-- 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)
needed : 0 < ENNReal.toReal 2
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' := ⋯,
                map_smul' := ⋯ : ↥(lp G 2) →ₗ[𝕜] E } :
              (a : ↥(lp G 2)) → E)
            f :
          E) =
      ‖f‖
needed₂ : 0 < ENNReal.toReal 2
needed₃ 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' := ⋯,
                map_smul' := ⋯ : ↥(lp G 2) →ₗ[𝕜] E } :
              (a : ↥(lp G 2)) → E)
            f :
          E) =
      ‖f‖
needed₅ :
  ∀ (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
needed₆ :
  ∀ (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))
h :
  ∀ (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
h₁ :
  ∀ (H : 0 < ENNReal.toReal 2) (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
⊢ 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‖

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
-- 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)
⊢ Eq.{u_3 + 1} (α := E) ((hV.linearIsometry (G := G) : (a : ↥(lp G 2)) → E) f : E)
    (∑' (i : ι), (V i : (a : G i) → E) ((↑f : (i : ι) → G i) i) : E)

Tactic:
rfl

Premises used: tsum, rfl
-- 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)
⊢ HasSum.{u_3, u_1} (α := E) (fun (i : ι) ↦ ((V i : (a : G i) → E) ((↑f : (i : ι) → G i) i) : E))
    ((hV.linearIsometry (G := G) : (a : ↥(lp G 2)) → E) f : E)

Tactic:
(hV.summable_of_lp f).hasSum

Premises used: OrthogonalFamily.summable_of_lp, Summable.hasSum, tsum
-- 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
inst_6 : DecidableEq ι
i : ι
x : G i
rw :
  Eq.{u_3 + 1} (α := E)
    (∑' (i_1 : ι), (V i_1 : (a : G i_1) → E) ((↑(lp.single (E := G) 2 i x) : (i : ι) → G i) i_1 : G i_1))
    (∑' (b' : ι), if b' = i then (V i : (a : G i) → E) x else 0)
⊢ Eq.{u_3 + 1} (α := E) ((hV.linearIsometry (G := G) : (a : ↥(lp G 2)) → E) (lp.single (E := G) 2 i x) : E)
    ((V i : (a : G i) → E) x : E)

Tactic:
rw [hV.linearIsometry_apply, ← tsum_ite_eq i (fun _ ↦ V i x)]

Premises used: tsum_ite_eq, OrthogonalFamily.linearIsometry_apply, DFunLike.coe, SummationFilter.unconditional
-- 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
inst_6 : DecidableEq ι
i : ι
x : G i
e_f :
  Eq (α := ι → E)
    (fun (i_1 : ι) ↦ (V i_1 : (a : G i_1) → E) ((↑(lp.single (E := G) 2 i x) : (i : ι) → G i) i_1 : G i_1))
    fun (b' : ι) ↦ if b' = i then (V i : (a : G i) → E) x else 0
⊢ Eq.{u_3 + 1} (α := E)
    (∑' (i_1 : ι), (V i_1 : (a : G i_1) → E) ((↑(lp.single (E := G) 2 i x) : (i : ι) → G i) i_1 : G i_1))
    (∑' (b' : ι), if b' = i then (V i : (a : G i) → E) x else 0)

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)
inst_5 : CompleteSpace E
V : (i : ι) → LinearIsometry.{u_2, u_2, u_4, u_3} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
inst_6 : DecidableEq ι
i : ι
x : G i
e_f :
  ∀ (j : ι),
    Eq.{u_3 + 1} (α := E) ((V j : (a : G j) → E) ((↑(lp.single (E := G) 2 i x) : (i : ι) → G i) j : G j) : E)
      (if j = i then (V i : (a : G i) → E) x else 0 : E)
⊢ Eq (α := ι → E)
    (fun (i_1 : ι) ↦ (V i_1 : (a : G i_1) → E) ((↑(lp.single (E := G) 2 i x) : (i : ι) → G i) i_1 : G i_1))
    fun (b' : ι) ↦ if b' = i then (V i : (a : G i) → E) x else 0

Tactic:
ext j
-- 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
inst_6 : DecidableEq ι
i : ι
x : G i
j : ι
e_f :
  Eq.{u_3 + 1} (α := E) ((V j : (a : G j) → E) (Pi.single (M := G) i x j) : E)
    (if j = i then (V i : (a : G i) → E) x else 0 : E)
⊢ Eq.{u_3 + 1} (α := E) ((V j : (a : G j) → E) ((↑(lp.single (E := G) 2 i x) : (i : ι) → G i) j : G j) : E)
    (if j = i then (V i : (a : G i) → E) x else 0 : E)

Tactic:
rw [lp.single_apply]

Premises used: lp.single_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 : OrthogonalFamily 𝕜 G V
inst_6 : DecidableEq ι
i : ι
x : G i
j : ι
pos :
  ∀ (h : j = i),
    Eq.{u_3 + 1} (α := E) ((V j : (a : G j) → E) (Pi.single (M := G) i x j) : E) ((V i : (a : G i) → E) x : E)
neg : ∀ (h : ¬j = i), Eq.{u_3 + 1} (α := E) ((V j : (a : G j) → E) (Pi.single (M := G) i x j) : E) (0 : E)
⊢ Eq.{u_3 + 1} (α := E) ((V j : (a : G j) → E) (Pi.single (M := G) i x j) : E)
    (if j = i then (V i : (a : G i) → E) x else 0 : E)

Tactic:
split_ifs with h
-- 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
inst_6 : DecidableEq ι
i : ι
x : G i
j : ι
h : j = i
pos :
  ∀ (x : G j),
    Eq.{u_3 + 1} (α := E) ((V j : (a : G j) → E) (Pi.single (M := G) j x j) : E) ((V j : (a : G j) → E) x : E)
⊢ Eq.{u_3 + 1} (α := E) ((V j : (a : G j) → E) (Pi.single (M := G) i x j) : E) ((V i : (a : G i) → E) x : E)

Tactic:
subst h
-- 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
inst_6 : DecidableEq ι
j : ι
x : G j
⊢ Eq.{u_3 + 1} (α := E) ((V j : (a : G j) → E) (Pi.single (M := G) j x j) : E) ((V j : (a : G j) → E) x : E)

Tactic:
simp
-- 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
inst_6 : DecidableEq ι
i : ι
x : G i
j : ι
h : ¬j = i
⊢ Eq.{u_3 + 1} (α := E) ((V j : (a : G j) → E) (Pi.single (M := G) i x j) : E) (0 : E)

Tactic:
simp [h]
-- 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
inst_6 : DecidableEq ι
inst_7 : (i : ι) → DecidableEq (G i)
W₀ : Π₀ (i : ι), G i
⊢ Eq.{u_3 + 1} (α := E)
    ((hV.linearIsometry (G := G) : (a : ↥(lp G 2)) → E) (W₀.sum (β := G) (lp.single (E := G) 2)) : E)
    (W₀.sum (β := G) fun (i : ι) ↦ (⇑(V i) : (a : G i) → E) : E)

Tactic:
simp
-- 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
inst_6 : ∀ (i : ι), CompleteSpace.{u_4} (G i)
⊢ hV.linearIsometry (G := G).range = topologicalClosure (⨆ (i : ι), (V i).range)

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- 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
inst_6 : ∀ (i : ι), CompleteSpace.{u_4} (G i)
refine_1 : hV.linearIsometry (G := G).range ≤ topologicalClosure (⨆ (i : ι), (V i).range)
refine_2 : topologicalClosure (⨆ (i : ι), (V i).range) ≤ hV.linearIsometry (G := G).range
⊢ hV.linearIsometry (G := G).range = topologicalClosure (⨆ (i : ι), (V i).range)

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- 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
inst_6 : ∀ (i : ι), CompleteSpace.{u_4} (G i)
f : ↥(lp G 2)
⊢ Membership.mem.{u_3, u_3} (α := E) (γ := Submodule 𝕜 E) (topologicalClosure (⨆ (i : ι), (V i).range))
    ((hV.linearIsometry (G := G).toLinearMap : (a : ↥(lp G 2)) → E) f : E)

Tactic:
mem_closure_of_tendsto (hV.hasSum_linearIsometry f) (Eventually.of_forall ?_)

Premises used: Set.Mem, setOf, Filter.Eventually.of_forall, OrthogonalFamily.hasSum_linearIsometry, closure, Set.sInter, mem_closure_of_tendsto