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 : OrthogonalFamily 𝕜 G V
inst_6 : ∀ (i : ι), CompleteSpace.{u_4} (G i)
f : ↥(lp G 2)
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)
⊢ 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:
refine mem_closure_of_tendsto (hV.hasSum_linearIsometry f) (Eventually.of_forall ?_)

Premises used: Filter.Eventually.of_forall, OrthogonalFamily.hasSum_linearIsometry, mem_closure_of_tendsto
-- 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)
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)

Tactic:
sum_mem ?_

Premises used: Set.Mem, sum_mem
-- 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)
s : Finset ι
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)
⊢ 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)

Tactic:
refine sum_mem ?_

Premises used: sum_mem
-- 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)
s : Finset ι
i : ι
refine_1 :
  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)
⊢ 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)

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

Tactic:
mem_iSup_of_mem i ?_

Premises used: Set.Mem, Submodule.mem_iSup_of_mem
-- 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)
s : Finset ι
i : ι
h : i ∈ s
refine_1 : Membership.mem (α := E) (V i).range ((V i : (a : G i) → E) ((↑f : (i : ι) → G i) i) : E)
⊢ 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)

Tactic:
refine mem_iSup_of_mem i ?_

Premises used: Submodule.mem_iSup_of_mem
-- 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)
s : Finset ι
i : ι
h : i ∈ s
⊢ Membership.mem (α := E) (V i).range ((V i : (a : G i) → E) ((↑f : (i : ι) → G i) i) : E)

Tactic:
LinearMap.mem_range_self _ (f i)

Premises used: Set.Mem, LinearMap.mem_range_self, 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 : OrthogonalFamily 𝕜 G V
inst_6 : ∀ (i : ι), CompleteSpace.{u_4} (G i)
f : ↥(lp G 2)
s : Finset ι
i : ι
h : i ∈ s
⊢ Membership.mem (α := E) (V i).range ((V i : (a : G i) → E) ((↑f : (i : ι) → G i) i) : E)

Tactic:
exact LinearMap.mem_range_self _ (f i)

Premises used: LinearMap.mem_range_self, 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 : OrthogonalFamily 𝕜 G V
inst_6 : ∀ (i : ι), CompleteSpace.{u_4} (G i)
refine_2 : ⨆ (i : ι), (V i).range ≤ hV.linearIsometry (G := G).range
refine_2₁ : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑hV.linearIsometry (G := G).range : Set E)
⊢ topologicalClosure (⨆ (i : ι), (V i).range) ≤ hV.linearIsometry (G := G).range

Tactic:
apply topologicalClosure_minimal

Premises used: Submodule.topologicalClosure_minimal
-- 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)
⊢ ⨆ (i : ι), (V i).range ≤ hV.linearIsometry (G := G).range

Tactic:
iSup_le ?_

Premises used: Set.Mem, iSup_le
-- 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_2 : ∀ (i : ι), (V i).range ≤ hV.linearIsometry (G := G).range
⊢ ⨆ (i : ι), (V i).range ≤ hV.linearIsometry (G := G).range

Tactic:
refine iSup_le ?_

Premises used: iSup_le
-- 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)
i : ι
x : G i
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)
⊢ Membership.mem (α := E) hV.linearIsometry (G := G).range (((V i).toLinearMap : (a : G i) → E) x : E)

Tactic:
use lp.single 2 i x

Premises used: lp.single, OfNat.ofNat
-- 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)
i : ι
x : G i
⊢ 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:
hV.linearIsometry_apply_single x

Premises used: OrthogonalFamily.linearIsometry_apply_single
-- 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)
i : ι
x : G i
⊢ 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:
exact hV.linearIsometry_apply_single x

Premises used: OrthogonalFamily.linearIsometry_apply_single
-- 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)
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑hV.linearIsometry (G := G).range : Set E)

Tactic:
hV.linearIsometry.isometry.isUniformInducing.isComplete_range.isClosed

Premises used: IsComplete.isClosed, setOf, IsUniformInducing.isComplete_range, LinearIsometry.isometry, Isometry.isUniformInducing, Set.range, OrthogonalFamily.linearIsometry
-- 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)
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑hV.linearIsometry (G := G).range : Set E)

Tactic:
exact hV.linearIsometry.isometry.isUniformInducing.isComplete_range.isClosed

Premises used: IsComplete.isClosed, IsUniformInducing.isComplete_range, LinearIsometry.isometry, Isometry.isUniformInducing, OrthogonalFamily.linearIsometry
-- 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 refine_2₁ : topologicalClosure (⨆ (i : ι), (V i).range) ≤ hV.linearIsometry (G := G).range
⊢ hV.linearIsometry (G := G).range = topologicalClosure (⨆ (i : ι), (V i).range)

Tactic:
classical
  refine le_antisymm ?_ ?_
  · rintro x ⟨f, rfl⟩
    refine mem_closure_of_tendsto (hV.hasSum_linearIsometry f) (Eventually.of_forall ?_)
    intro s
    rw [SetLike.mem_coe]
    refine sum_mem ?_
    intro i _
    refine mem_iSup_of_mem i ?_
    exact LinearMap.mem_range_self _ (f i)
  · apply topologicalClosure_minimal
    · refine iSup_le ?_
      rintro i x ⟨x, rfl⟩
      use lp.single 2 i x
      exact hV.linearIsometry_apply_single x
    exact hV.linearIsometry.isometry.isUniformInducing.isComplete_range.isClosed

Premises used: Submodule.topologicalClosure_minimal, IsComplete.isClosed, IsUniformInducing.isComplete_range, le_antisymm, LinearIsometry.isometry, SetLike.mem_coe, iSup_le, Isometry.isUniformInducing, OrthogonalFamily.linearIsometry, sum_mem, 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
inst_6 : ∀ (i : ι), CompleteSpace.{u_4} (G i)
hVortho : OrthogonalFamily 𝕜 G V
hVtotal : LE.le.{u_3} (α := Submodule 𝕜 E) ⊤ (topologicalClosure (⨆ (i : ι), (V i).range))
rw : Function.Surjective (α := ↥(lp G 2)) (β := E) (⇑hVortho.linearIsometry (G := G).toLinearMap : (a : ↥(lp G 2)) → E)
⊢ Function.Surjective (α := ↥(lp G 2)) (β := E) (⇑(hVortho.linearIsometry (G := G)) : (a : ↥(lp G 2)) → E)

Tactic:
rw [← LinearIsometry.coe_toLinearMap]

Premises used: LinearIsometry.coe_toLinearMap
-- 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
inst_6 : ∀ (i : ι), CompleteSpace.{u_4} (G i)
hVortho : OrthogonalFamily 𝕜 G V
hVtotal : LE.le.{u_3} (α := Submodule 𝕜 E) ⊤ (topologicalClosure (⨆ (i : ι), (V i).range))
⊢ Function.Surjective (α := ↥(lp G 2)) (β := E) (⇑hVortho.linearIsometry (G := G).toLinearMap : (a : ↥(lp G 2)) → E)

Tactic:
LinearMap.range_eq_top.mp
        (eq_top_iff.mpr <| hVtotal.trans_eq hVortho.range_linearIsometry.symm)

Premises used: Iff.mpr, LE.le.trans_eq, eq_top_iff, LinearMap.range_eq_top, OrthogonalFamily.range_linearIsometry, Iff.mp, Eq.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
inst_6 : ∀ (i : ι), CompleteSpace.{u_4} (G i)
hVortho : OrthogonalFamily 𝕜 G V
hVtotal : LE.le.{u_3} (α := Submodule 𝕜 E) ⊤ (topologicalClosure (⨆ (i : ι), (V i).range))
⊢ Function.Surjective (α := ↥(lp G 2)) (β := E) (⇑hVortho.linearIsometry (G := G).toLinearMap : (a : ↥(lp G 2)) → E)

Tactic:
exact LinearMap.range_eq_top.mp
        (eq_top_iff.mpr <| hVtotal.trans_eq hVortho.range_linearIsometry.symm)

Premises used: Iff.mpr, LE.le.trans_eq, eq_top_iff, LinearMap.range_eq_top, OrthogonalFamily.range_linearIsometry, Iff.mp, Eq.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
inst_3 : CompleteSpace E
F : ι → Submodule 𝕜 E
inst_4 : ∀ (i : ι), CompleteSpace.{u_3} ↥(F i)
hFortho : OrthogonalFamily.{u_2, u_3, u_1, u_3} 𝕜 (E := E) (fun (i : ι) ↦ ↥(F i)) fun (i : ι) ↦ (F i).subtypeₗᵢ
hFtotal : LE.le.{u_3} (α := Submodule 𝕜 E) ⊤ (topologicalClosure (⨆ (i : ι), F i))
⊢ LE.le.{u_3} (α := Submodule 𝕜 E) ⊤ (topologicalClosure (⨆ (i : ι), (F i).subtypeₗᵢ.range))

Tactic:
simpa [subtypeₗᵢ_toLinearMap, range_subtype] using hFtotal

Premises used: Submodule.subtypeₗᵢ_toLinearMap, Submodule.range_subtype
-- 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 : IsHilbertSum 𝕜 G V
w : ↥(lp G 2)
⊢ Eq.{u_3 + 1} (α := E) ((hV.linearIsometryEquiv (G := G).symm : (a : ↥(lp G 2)) → E) w : E)
    (∑' (i : ι), (V i : (a : G i) → E) ((↑w : (i : ι) → G i) i) : E)

Tactic:
simp [IsHilbertSum.linearIsometryEquiv, OrthogonalFamily.linearIsometry_apply]

Premises used: OrthogonalFamily.linearIsometry_apply, IsHilbertSum.linearIsometryEquiv
-- 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 : IsHilbertSum 𝕜 G V
w : ↥(lp G 2)
⊢ HasSum.{u_3, u_1} (α := E) (fun (i : ι) ↦ ((V i : (a : G i) → E) ((↑w : (i : ι) → G i) i) : E))
    ((hV.linearIsometryEquiv (G := G).symm : (a : ↥(lp G 2)) → E) w : E)

Tactic:
simp [IsHilbertSum.linearIsometryEquiv, OrthogonalFamily.hasSum_linearIsometry]

Premises used: OrthogonalFamily.hasSum_linearIsometry, IsHilbertSum.linearIsometryEquiv
-- 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
inst_6 : DecidableEq ι
hV : IsHilbertSum 𝕜 G V
i : ι
x : G i
⊢ Eq.{u_3 + 1} (α := E) ((hV.linearIsometryEquiv (G := G).symm : (a : ↥(lp G 2)) → E) (lp.single (E := G) 2 i x) : E)
    ((V i : (a : G i) → E) x : E)

Tactic:
simp [IsHilbertSum.linearIsometryEquiv, OrthogonalFamily.linearIsometry_apply_single]

Premises used: OrthogonalFamily.linearIsometry_apply_single, IsHilbertSum.linearIsometryEquiv
-- 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
inst_6 : DecidableEq ι
inst_7 : (i : ι) → DecidableEq (G i)
hV : IsHilbertSum 𝕜 G V
W₀ : Π₀ (i : ι), G i
⊢ Eq.{u_3 + 1} (α := E)
    ((hV.linearIsometryEquiv (G := G).symm : (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 only [map_dfinsuppSum, IsHilbertSum.linearIsometryEquiv_symm_apply_single]

Premises used: map_dfinsuppSum, IsHilbertSum.linearIsometryEquiv_symm_apply_single
-- 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
inst_6 : DecidableEq ι
inst_7 : (i : ι) → DecidableEq (G i)
hV : IsHilbertSum 𝕜 G V
W₀ : Π₀ (i : ι), G i
rw :
  (↑((hV.linearIsometryEquiv (G := G) : (a : E) → ↥(lp G 2)) (W₀.sum (β := G) fun (a : ι) ↦ (⇑(V a) : (a : G a) → E))) :
      (i : ι) → G i) =
    (⇑W₀ : (a : ι) → G a)
⊢ (↑(W₀.sum (β := G) fun (a : ι) (b : G a) ↦
          (hV.linearIsometryEquiv (G := G) : (a : E) → ↥(lp G 2)) ((V a : (a : G a) → E) b)) :
      (i : ι) → G i) =
    (⇑W₀ : (a : ι) → G a)

Tactic:
rw [← map_dfinsuppSum]

Premises used: map_dfinsuppSum
-- 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
inst_6 : DecidableEq ι
inst_7 : (i : ι) → DecidableEq (G i)
hV : IsHilbertSum 𝕜 G V
W₀ : Π₀ (i : ι), G i
rw :
  (↑((hV.linearIsometryEquiv (G := G) : (a : E) → ↥(lp G 2))
          ((hV.linearIsometryEquiv (G := G).symm : (a : ↥(lp G 2)) → E) (W₀.sum (β := G) (lp.single (E := G) 2)))) :
      (i : ι) → G i) =
    (⇑W₀ : (a : ι) → G a)
⊢ (↑((hV.linearIsometryEquiv (G := G) : (a : E) → ↥(lp G 2)) (W₀.sum (β := G) fun (a : ι) ↦ (⇑(V a) : (a : G a) → E))) :
      (i : ι) → G i) =
    (⇑W₀ : (a : ι) → G a)

Tactic:
rw [← hV.linearIsometryEquiv_symm_apply_dfinsupp_sum_single]

Premises used: IsHilbertSum.linearIsometryEquiv_symm_apply_dfinsupp_sum_single
-- 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
inst_6 : DecidableEq ι
inst_7 : (i : ι) → DecidableEq (G i)
hV : IsHilbertSum 𝕜 G V
W₀ : Π₀ (i : ι), G i
rw : (↑(W₀.sum (β := G) (lp.single (E := G) 2)) : (i : ι) → G i) = (⇑W₀ : (a : ι) → G a)
⊢ (↑((hV.linearIsometryEquiv (G := G) : (a : E) → ↥(lp G 2))
          ((hV.linearIsometryEquiv (G := G).symm : (a : ↥(lp G 2)) → E) (W₀.sum (β := G) (lp.single (E := G) 2)))) :
      (i : ι) → G i) =
    (⇑W₀ : (a : ι) → G a)

Tactic:
rw [LinearIsometryEquiv.apply_symm_apply]

Premises used: LinearIsometryEquiv.apply_symm_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
inst_6 : DecidableEq ι
inst_7 : (i : ι) → DecidableEq (G i)
hV : IsHilbertSum 𝕜 G V
W₀ : Π₀ (i : ι), G i
h : ∀ (i : ι), (↑(W₀.sum (β := G) (lp.single (E := G) 2)) : (i : ι) → G i) i = (W₀ : (a : ι) → G a) i
⊢ (↑(W₀.sum (β := G) (lp.single (E := G) 2)) : (i : ι) → G i) = (⇑W₀ : (a : ι) → G a)

Tactic:
ext i