-- Mathlib/Analysis/InnerProductSpace/l2Space.lean
theorem dense_span (b : HilbertBasis ι 𝕜 E) :
    (span 𝕜 (Set.range b)).topologicalClosure = ⊤

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x : E
s : Finset ι
⊢ ∑ x_1 ∈ s, ↑(b.repr x) x_1 • b x_1 ∈ (span 𝕜 (Set.range ⇑b)).toAddSubmonoid

Tactic:
refine sum_mem ?_

Result:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x : E
s : Finset ι
⊢ ∀ c ∈ s, ↑(b.repr x) c • b c ∈ (span 𝕜 (Set.range ⇑b)).toAddSubmonoid

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
⊢ (span 𝕜 (Set.range ⇑b)).topologicalClosure = ⊤

Tactic:
rw [eq_top_iff]

Result:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
⊢ ⊤ ≤ (span 𝕜 (Set.range ⇑b)).topologicalClosure

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x : E
⊢ ∀ (x_1 : Finset ι), ∑ b_1 ∈ x_1, (fun i => ↑(b.repr x) i • b i) b_1 ∈ ↑(span 𝕜 (Set.range ⇑b)).toAddSubmonoid

Tactic:
intro s

Result:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x : E
s : Finset ι
⊢ ∑ b_1 ∈ s, (fun i => ↑(b.repr x) i • b i) b_1 ∈ ↑(span 𝕜 (Set.range ⇑b)).toAddSubmonoid

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
⊢ ⊤ ≤ (span 𝕜 (Set.range ⇑b)).topologicalClosure

Tactic:
rintro x -

Result:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x : E
⊢ x ∈ (span 𝕜 (Set.range ⇑b)).topologicalClosure

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x : E
⊢ x ∈ (span 𝕜 (Set.range ⇑b)).topologicalClosure

Tactic:
refine mem_closure_of_tendsto (b.hasSum_repr x) (Eventually.of_forall ?_)

Result:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x : E
⊢ ∀ (x_1 : Finset ι), ∑ b_1 ∈ x_1, (fun i => ↑(b.repr x) i • b i) b_1 ∈ ↑(span 𝕜 (Set.range ⇑b)).toAddSubmonoid

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x : E
s : Finset ι
⊢ ∀ c ∈ s, ↑(b.repr x) c • b c ∈ (span 𝕜 (Set.range ⇑b)).toAddSubmonoid

Tactic:
rintro i -

Result:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x : E
s : Finset ι
i : ι
⊢ ↑(b.repr x) i • b i ∈ (span 𝕜 (Set.range ⇑b)).toAddSubmonoid

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x : E
s : Finset ι
i : ι
⊢ b i ∈ span 𝕜 (Set.range ⇑b)

Tactic:
exact subset_span ⟨i, rfl⟩

Result:
no goals

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
⊢ (span 𝕜 (Set.range ⇑b)).topologicalClosure = ⊤

Tactic:
classical
  rw [eq_top_iff]
  rintro x -
  refine mem_closure_of_tendsto (b.hasSum_repr x) (Eventually.of_forall ?_)
  intro s
  simp only [SetLike.mem_coe]
  refine sum_mem ?_
  rintro i -
  refine smul_mem _ _ ?_
  exact subset_span ⟨i, rfl⟩

Result:
no goals

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x : E
s : Finset ι
i : ι
⊢ ↑(b.repr x) i • b i ∈ (span 𝕜 (Set.range ⇑b)).toAddSubmonoid

Tactic:
refine smul_mem _ _ ?_

Result:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x : E
s : Finset ι
i : ι
⊢ b i ∈ span 𝕜 (Set.range ⇑b)

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x : E
s : Finset ι
⊢ ∑ b_1 ∈ s, (fun i => ↑(b.repr x) i • b i) b_1 ∈ ↑(span 𝕜 (Set.range ⇑b)).toAddSubmonoid

Tactic:
simp only [SetLike.mem_coe]

Result:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x : E
s : Finset ι
⊢ ∑ x_1 ∈ s, ↑(b.repr x) x_1 • b x_1 ∈ (span 𝕜 (Set.range ⇑b)).toAddSubmonoid