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)
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‖
⊢ 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) (∑' (i : ι), (V i : (a : G i) → E) ((↑f : (i : ι) → G i) i)) ^ ENNReal.toReal 2 =
    ‖f‖ ^ 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
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
⊢ 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),
  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: 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
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))
⊢ 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 : ∀ (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
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
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
⊢ 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₁ : ∀ (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: 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 : OrthogonalFamily 𝕜 G V
inst_6 : DecidableEq ι
i : ι
x : G i
⊢ 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)
have 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)
Tactic: rw [hV.linearIsometry_apply, ← tsum_ite_eq i (fun _ ↦ V i x)]
-- 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
inst_6 : DecidableEq ι
i : ι
x : G i
⊢ 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)
have 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
Tactic: 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)
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
⊢ 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
have 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)
Tactic: ext j
-- 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
inst_6 : DecidableEq ι
i : ι
x : G i
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)
have 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)
Tactic: rw [lp.single_apply]
-- 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
inst_6 : DecidableEq ι
i : ι
x : G i
j : ι
⊢ 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)
have 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)
Tactic: split_ifs with h
-- 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
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)
⊢ 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)
have 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)
Tactic: split_ifs with h
-- 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
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) ((V i : (a : G i) → E) x : E)
have 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)
Tactic: subst h
Cleared hypotheses: i, x, h
-- 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
inst_6 : ∀ (i : ι), CompleteSpace.{u_4} (G i)
⊢ hV.linearIsometry (G := G).range = topologicalClosure (⨆ (i : ι), (V i).range)
have refine_1 : hV.linearIsometry (G := G).range ≤ topologicalClosure (⨆ (i : ι), (V i).range)
Tactic: refine le_antisymm ?_ ?_
-- 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
inst_6 : ∀ (i : ι), CompleteSpace.{u_4} (G i)
refine_1 : hV.linearIsometry (G := G).range ≤ topologicalClosure (⨆ (i : ι), (V i).range)
⊢ hV.linearIsometry (G := G).range = topologicalClosure (⨆ (i : ι), (V i).range)
have refine_2 : topologicalClosure (⨆ (i : ι), (V i).range) ≤ hV.linearIsometry (G := G).range
Tactic: refine le_antisymm ?_ ?_
-- 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
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)
have refine_1 : ∀ (x : Finset ι),
  ∑ b ∈ x, (fun (i : ι) ↦ ((V i : (a : G i) → E) ((↑f : (i : ι) → G i) i) : E)) b ∈
    (↑(toAddSubmonoid.{u_2, u_3} (R := 𝕜) (⨆ (i : ι), (V i).range)) : Set E)
Tactic: refine mem_closure_of_tendsto (hV.hasSum_linearIsometry f) (Eventually.of_forall ?_)
-- 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
inst_6 : ∀ (i : ι), CompleteSpace.{u_4} (G i)
f : ↥(lp G 2)
s : Finset ι
⊢ Membership.mem (γ := AddSubmonoid E) (toAddSubmonoid.{u_2, u_3} (R := 𝕜) (⨆ (i : ι), (V i).range))
    (∑ b ∈ s, (fun (i : ι) ↦ ((V i : (a : G i) → E) ((↑f : (i : ι) → G i) i) : E)) b)
have refine_1 : ∀ c ∈ s,
  Membership.mem.{u_3, u_3} (α := E) (γ := AddSubmonoid E) (toAddSubmonoid.{u_2, u_3} (R := 𝕜) (⨆ (i : ι), (V i).range))
    ((V c : (a : G c) → E) ((↑f : (i : ι) → G i) c) : E)
Tactic: refine sum_mem ?_
-- 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
inst_6 : ∀ (i : ι), CompleteSpace.{u_4} (G i)
f : ↥(lp G 2)
s : Finset ι
i : ι
h : i ∈ s
⊢ Membership.mem.{u_3, u_3} (α := E) (γ := AddSubmonoid E) (toAddSubmonoid.{u_2, u_3} (R := 𝕜) (⨆ (i : ι), (V i).range))
    ((V i : (a : G i) → E) ((↑f : (i : ι) → G i) i) : E)
have refine_1 : Membership.mem (α := E) (V i).range ((V i : (a : G i) → E) ((↑f : (i : ι) → G i) i) : E)
Tactic: refine mem_iSup_of_mem i ?_
-- 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
inst_6 : ∀ (i : ι), CompleteSpace.{u_4} (G i)
⊢ topologicalClosure (⨆ (i : ι), (V i).range) ≤ hV.linearIsometry (G := G).range
have refine_2 : ⨆ (i : ι), (V i).range ≤ hV.linearIsometry (G := G).range
Tactic: apply topologicalClosure_minimal
-- 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
inst_6 : ∀ (i : ι), CompleteSpace.{u_4} (G i)
refine_2 : ⨆ (i : ι), (V i).range ≤ hV.linearIsometry (G := G).range
⊢ topologicalClosure (⨆ (i : ι), (V i).range) ≤ hV.linearIsometry (G := G).range
have refine_2₁ : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑hV.linearIsometry (G := G).range : Set E)
Tactic: apply topologicalClosure_minimal
-- 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
inst_6 : ∀ (i : ι), CompleteSpace.{u_4} (G i)
⊢ ⨆ (i : ι), (V i).range ≤ hV.linearIsometry (G := G).range
have refine_2 : ∀ (i : ι), (V i).range ≤ hV.linearIsometry (G := G).range
Tactic: refine iSup_le ?_
-- 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
inst_6 : ∀ (i : ι), CompleteSpace.{u_4} (G i)
i : ι
x : G i
⊢ Membership.mem (α := E) hV.linearIsometry (G := G).range (((V i).toLinearMap : (a : G i) → E) x : E)
have h : Eq.{u_3 + 1} (α := E) ((hV.linearIsometry (G := G).toLinearMap : (a : ↥(lp G 2)) → E) (lp.single (E := G) 2 i x) : E)
  (((V i).toLinearMap : (a : G i) → E) x : E)
Tactic: use lp.single 2 i x